Skip to content

Commit 023539d

Browse files
OlivierBBBOlivierBBB
authored
Osaka constraints debugging 2 (#838)
1 parent 23389a5 commit 023539d

File tree

3 files changed

+25
-18
lines changed

3 files changed

+25
-18
lines changed

‎hub/osaka/constraints/instruction-handling/call/precompiles/NSRs_and_flag_sums_II.lisp‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@
9090
))
9191
;; non stack rows shorthands
9292
(defun (precompile-processing---nsr-RIPEMD-160-FKTH) precompile-processing---nsr-standard-failure)
93-
(defun (precompile-processing---nsr-RIPEMD-160-success) precompile-processing---nsr-standard-success) ;; ""
93+
(defun (precompile-processing---nsr-RIPEMD-160-success) precompile-processing---nsr-standard-success)
9494
;; flag sum shorthands
9595
(defun (precompile-processing---flag-sum-RIPEMD-160-FKTH) (precompile-processing---flag-sum-standard-failure))
9696
(defun (precompile-processing---flag-sum-RIPEMD-160-success) (precompile-processing---flag-sum-standard-success))
@@ -214,7 +214,7 @@
214214
;; ECADD non stack rows shorthands
215215
(defun (precompile-processing---nsr-ECADD-FKTH) precompile-processing---nsr-standard-failure)
216216
(defun (precompile-processing---nsr-ECADD-FKTR) precompile-processing---nsr-standard-failure)
217-
(defun (precompile-processing---nsr-ECADD-success) precompile-processing---nsr-standard-success) ;; ""
217+
(defun (precompile-processing---nsr-ECADD-success) precompile-processing---nsr-standard-success)
218218
;; ECADD flag sum shorthands
219219
(defun (precompile-processing---flag-sum-ECADD-FKTH) (precompile-processing---flag-sum-standard-failure))
220220
(defun (precompile-processing---flag-sum-ECADD-FKTR) (precompile-processing---flag-sum-standard-failure))
@@ -379,7 +379,7 @@
379379
;; P256_VERIFY non stack rows shorthands
380380
(defun (precompile-processing---nsr-P256-VERIFY-FKTH) precompile-processing---nsr-standard-failure)
381381
(defun (precompile-processing---nsr-P256-VERIFY-FKTR) precompile-processing---nsr-standard-failure)
382-
(defun (precompile-processing---nsr-P256-VERIFY-success) precompile-processing---nsr-standard-success) ;; ""
382+
(defun (precompile-processing---nsr-P256-VERIFY-success) precompile-processing---nsr-standard-success)
383383
;; P256_VERIFY flag sum shorthands
384384
(defun (precompile-processing---flag-sum-P256-VERIFY-FKTH) (precompile-processing---flag-sum-standard-failure))
385385
(defun (precompile-processing---flag-sum-P256-VERIFY-FKTR) (precompile-processing---flag-sum-standard-failure))

‎hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__05__exponent_leading_word_extraction_and_analysis_row.lisp‎

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -32,9 +32,9 @@
3232
(:guard (precompile-processing---MODEXP---standard-precondition))
3333
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
3434
(begin
35-
(eq! (precompile-processing---MODEXP---call-EXP-to-analyze-leading-word) (precompile-processing---MODEXP---extract-leading-word) )
36-
(eq! (precompile-processing---MODEXP---call-MMU-to-extract-leading-word) (precompile-processing---MODEXP---extract-leading-word) )
37-
(eq! (precompile-processing---MODEXP---call-OOB-on-leading-word-row) 1 )
35+
(eq! (precompile-processing---MODEXP---call-OOB-on-leading-word-row) (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds) )
36+
(eq! (precompile-processing---MODEXP---call-EXP-to-analyze-leading-word) (precompile-processing---MODEXP---extract-leading-word) )
37+
(eq! (precompile-processing---MODEXP---call-MMU-to-extract-leading-word) (precompile-processing---MODEXP---extract-leading-word) )
3838
(eq! (+ (shift misc/MXP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)
3939
(shift misc/STP_FLAG precompile-processing---MODEXP---misc-row-offset---leading-word-analysis))
4040
0)
@@ -44,11 +44,12 @@
4444
(defconstraint precompile-processing---MODEXP---lead-log-analysis---setting-OOB-instruction
4545
(:guard (precompile-processing---MODEXP---standard-precondition))
4646
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
47-
(set-OOB-instruction---modexp-lead precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset
48-
(precompile-processing---MODEXP---bbs-normalized) ;; low part of bbs (base byte size)
49-
(precompile-processing---dup-cds) ;; call data size
50-
(precompile-processing---MODEXP---ebs-normalized) ;; low part of ebs (exponent byte size)
51-
))
47+
(if-not-zero (precompile-processing---MODEXP---call-OOB-on-leading-word-row)
48+
(set-OOB-instruction---modexp-lead precompile-processing---MODEXP---misc-row-offset---leading-word-analysis ;; offset
49+
(precompile-processing---MODEXP---bbs-normalized) ;; low part of bbs (base byte size)
50+
(precompile-processing---dup-cds) ;; call data size
51+
(precompile-processing---MODEXP---ebs-normalized) ;; low part of ebs (exponent byte size)
52+
)))
5253

5354
(defun (precompile-processing---MODEXP---extract-leading-word) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) ;; ""
5455
(defun (precompile-processing---MODEXP---cds-cutoff) (shift [misc/OOB_DATA 6] precompile-processing---MODEXP---misc-row-offset---leading-word-analysis)) ;; ""

‎hub/osaka/constraints/instruction-handling/call/precompiles/modexp/common/__06__pricing_row.lisp‎

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -23,23 +23,29 @@
2323
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2424

2525

26+
27+
(defun (precompile-processing---MODEXP---call-OOB-on-pricing-row) (shift misc/OOB_FLAG precompile-processing---MODEXP---misc-row-offset---pricing))
28+
29+
30+
2631
(defconstraint precompile-processing---MODEXP---pricing-analysis---setting-misc-module-flags
2732
(:guard (precompile-processing---MODEXP---standard-precondition))
2833
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2934
(eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---pricing)
30-
MISC_WEIGHT_OOB
35+
(* MISC_WEIGHT_OOB (precompile-processing---MODEXP---all-byte-sizes-are-in-bounds))
3136
))
3237

3338

3439
(defconstraint precompile-processing---MODEXP---pricing-analysis---setting-OOB-instruction
3540
(:guard (precompile-processing---MODEXP---standard-precondition))
3641
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
37-
(set-OOB-instruction---modexp-pricing precompile-processing---MODEXP---misc-row-offset---pricing ;; offset
38-
(precompile-processing---dup-call-gas) ;; call gas i.e. gas provided to the precompile
39-
(precompile-processing---dup-r@c) ;; return at capacity
40-
(precompile-processing---MODEXP---modexp-full-log) ;; leading (≤) word log of exponent
41-
(precompile-processing---MODEXP---max-mbs-bbs) ;; call data size
42-
))
42+
(if-not-zero (precompile-processing---MODEXP---call-OOB-on-pricing-row)
43+
(set-OOB-instruction---modexp-pricing precompile-processing---MODEXP---misc-row-offset---pricing ;; offset
44+
(precompile-processing---dup-call-gas) ;; call gas i.e. gas provided to the precompile
45+
(precompile-processing---dup-r@c) ;; return at capacity
46+
(precompile-processing---MODEXP---modexp-full-log) ;; leading (≤) word log of exponent
47+
(precompile-processing---MODEXP---max-mbs-bbs) ;; call data size
48+
)))
4349

4450
(defun (precompile-processing---MODEXP---ram-success) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---pricing))
4551
(defun (precompile-processing---MODEXP---return-gas) (shift [misc/OOB_DATA 5] precompile-processing---MODEXP---misc-row-offset---pricing))

0 commit comments

Comments
 (0)