Skip to content

Commit 80f7edc

Browse files
OlivierBBBOlivierBBB
authored
MISC flag soundness bug fix in the HUB (#698)
1 parent 56d4ca1 commit 80f7edc

File tree

34 files changed

+300
-224
lines changed

34 files changed

+300
-224
lines changed

‎hub/cancun/constraints/instruction-handling/call/precompiles/blake/generalities.lisp‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -34,10 +34,11 @@
3434

3535
(defconstraint precompile-processing---BLAKE2f---setting-MISC-flags
3636
(:guard (precompile-processing---BLAKE2f---standard-precondition))
37-
(eq! (weighted-MISC-flag-sum precompile-processing---BLAKE2f---misc-row-offset---BLAKE-parameter-extraction)
38-
(+ MISC_WEIGHT_OOB
39-
(* MISC_WEIGHT_MMU
40-
(precompile-processing---BLAKE2f---OOB-hub-success)))))
37+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
38+
(begin
39+
(eq! (weighted-MISC-flag-sum-sans-MMU precompile-processing---BLAKE2f---misc-row-offset---BLAKE-parameter-extraction) MISC_WEIGHT_OOB)
40+
(eq! (shift misc/MMU_FLAG precompile-processing---BLAKE2f---misc-row-offset---BLAKE-parameter-extraction) (precompile-processing---BLAKE2f---OOB-hub-success))
41+
))
4142

4243
(defconstraint precompile-processing---BLAKE2f---setting-first-OOB-instruction
4344
(:guard (precompile-processing---BLAKE2f---standard-precondition))

‎hub/cancun/constraints/instruction-handling/call/precompiles/blake/surviving_the_hub.lisp‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -28,10 +28,12 @@
2828

2929
(defconstraint precompile-processing---BLAKE2f---setting-second-MISC-flags
3030
(:guard (precompile-processing---BLAKE2f---surviving-the-HUB))
31-
(eq! (weighted-MISC-flag-sum precompile-processing---BLAKE2f---misc-row-offset---BLAKE-call-data-extraction)
32-
(+ MISC_WEIGHT_OOB
33-
(* MISC_WEIGHT_MMU
34-
(precompile-processing---BLAKE2f---OOB-ram-success)))))
31+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
32+
(begin
33+
(eq! (weighted-MISC-flag-sum-sans-MMU precompile-processing---BLAKE2f---misc-row-offset---BLAKE-call-data-extraction) MISC_WEIGHT_OOB)
34+
(eq! (shift misc/MMU_FLAG precompile-processing---BLAKE2f---misc-row-offset---BLAKE-call-data-extraction) (precompile-processing---BLAKE2f---OOB-ram-success))
35+
))
36+
3537

3638
(defconstraint precompile-processing---BLAKE2f---setting-the-second-OOB-instruction
3739
(:guard (precompile-processing---BLAKE2f---surviving-the-HUB))

‎hub/cancun/constraints/instruction-handling/call/precompiles/common/generalities.lisp‎

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -21,10 +21,13 @@
2121
(defun (precompile-processing---common---precondition) (* PEEK_AT_SCENARIO (scenario-shorthand---PRC---common-address-bit-sum)))
2222

2323

24-
(defconstraint precompile-processing---common---setting-MISC-module-flags (:guard (precompile-processing---common---precondition))
25-
(eq! (weighted-MISC-flag-sum 1)
26-
(+ (* MISC_WEIGHT_MMU (precompile-processing---common---OOB-extract-call-data))
27-
MISC_WEIGHT_OOB)))
24+
(defconstraint precompile-processing---common---setting-MISC-module-flags
25+
(:guard (precompile-processing---common---precondition))
26+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
27+
(begin
28+
(eq! (weighted-MISC-flag-sum-sans-MMU 1) MISC_WEIGHT_OOB)
29+
(eq! (shift misc/MMU_FLAG 1) (precompile-processing---common---OOB-extract-call-data))
30+
))
2831

2932
(defconstraint precompile-processing---common---setting-OOB-instruction (:guard (precompile-processing---common---precondition))
3033
(set-OOB-instruction---common precompile-processing---common---1st-misc-row---row-offset ;; offset

‎hub/cancun/constraints/instruction-handling/call/precompiles/modexp/success.lisp‎

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -33,10 +33,13 @@
3333
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
3434

3535

36-
(defconstraint precompile-processing---MODEXP---success-case---base-extraction-row---setting-module-flags (:guard (precompile-processing---MODEXP---success-case))
37-
(eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---base-extraction)
38-
(+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-modulus))
39-
MISC_WEIGHT_OOB)))
36+
(defconstraint precompile-processing---MODEXP---success-case---base-extraction-row---setting-module-flags
37+
(:guard (precompile-processing---MODEXP---success-case))
38+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
39+
(begin
40+
(eq! (weighted-MISC-flag-sum-sans-MMU precompile-processing---MODEXP---misc-row-offset---base-extraction) MISC_WEIGHT_OOB)
41+
(eq! (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---base-extraction) (precompile-processing---MODEXP---extract-modulus))
42+
))
4043

4144
(defconstraint precompile-processing---MODEXP---success-case---base-extraction-row---setting-the-OOB-instruction-which-decides-which-actual-parameters-to-extract (:guard (precompile-processing---MODEXP---success-case))
4245
(set-OOB-instruction---modexp-extract precompile-processing---MODEXP---misc-row-offset---base-extraction ;; offset

‎hub/cancun/constraints/instruction-handling/copy/generalities.lisp‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -150,10 +150,12 @@
150150
(shift PEEK_AT_ACCOUNT ROFF_EXTCODECOPY_NO_XAHOY_NO_REVERT_ACCOUNT_ROW)))))))
151151

152152
(defconstraint copy-instruction---setting-misc-row-module-flags (:guard (copy-instruction---standard-precondition))
153-
(eq! (weighted-MISC-flag-sum ROFF_COPY_INST_MISCELLANEOUS_ROW)
154-
(+ (* MISC_WEIGHT_MMU (copy-instruction---trigger_MMU))
155-
(* MISC_WEIGHT_MXP (copy-instruction---trigger_MXP))
156-
(* MISC_WEIGHT_OOB (copy-instruction---trigger_OOB)))))
153+
(begin
154+
(eq! (weighted-MISC-flag-sum-sans-MMU ROFF_COPY_INST_MISCELLANEOUS_ROW)
155+
(+ (* MISC_WEIGHT_MXP (copy-instruction---trigger_MXP))
156+
(* MISC_WEIGHT_OOB (copy-instruction---trigger_OOB))))
157+
(eq! (shift misc/MMU_FLAG ROFF_COPY_INST_MISCELLANEOUS_ROW) (copy-instruction---trigger_MMU))
158+
))
157159

158160
(defun (copy-instruction---trigger_OOB) (copy-instruction---is-RETURNDATACOPY))
159161
(defun (copy-instruction---trigger_MXP) (- 1 stack/RDCX))

‎hub/cancun/constraints/instruction-handling/create/constraints/generalities.lisp‎

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -38,12 +38,13 @@
3838
(create-instruction---current-context-is-static)))
3939

4040
(defconstraint create-instruction---setting-the-module-flags-of-the-miscellaneous-row (:guard (create-instruction---generic-precondition))
41-
(eq! (weighted-MISC-flag-sum CREATE_miscellaneous_row___row_offset)
42-
(+ (* MISC_WEIGHT_MMU (create-instruction---trigger_MMU))
43-
(* MISC_WEIGHT_MXP (create-instruction---trigger_MXP))
44-
(* MISC_WEIGHT_OOB (create-instruction---trigger_OOB))
45-
(* MISC_WEIGHT_STP (create-instruction---trigger_STP))
46-
)))
41+
(begin
42+
(eq! (shift misc/EXP_FLAG CREATE_miscellaneous_row___row_offset) 0)
43+
(eq! (shift misc/MMU_FLAG CREATE_miscellaneous_row___row_offset) (create-instruction---trigger_MMU))
44+
(eq! (shift misc/MXP_FLAG CREATE_miscellaneous_row___row_offset) (create-instruction---trigger_MXP))
45+
(eq! (shift misc/OOB_FLAG CREATE_miscellaneous_row___row_offset) (create-instruction---trigger_OOB))
46+
(eq! (shift misc/STP_FLAG CREATE_miscellaneous_row___row_offset) (create-instruction---trigger_STP))
47+
))
4748

4849
(defconstraint create-instruction---setting-the-MXP-instruction (:guard (create-instruction---generic-precondition))
4950
(if-not-zero (shift misc/MXP_FLAG CREATE_miscellaneous_row___row_offset)
@@ -202,4 +203,4 @@
202203
(if-not-zero (scenario-shorthand---CREATE---failure-condition) (eq! GAS_NEXT (- GAS_ACTUAL (create-instruction---full-gas-cost))))
203204
(if-not-zero (scenario-shorthand---CREATE---not-rebuffed-empty-init-code) (eq! GAS_NEXT (- GAS_ACTUAL (create-instruction---upfront-gas-cost))))
204205
(if-not-zero (scenario-shorthand---CREATE---not-rebuffed-nonempty-init-code) (eq! GAS_NEXT (- GAS_ACTUAL (create-instruction---full-gas-cost))))
205-
))
206+
))

‎hub/cancun/constraints/instruction-handling/halting/return.lisp‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -220,13 +220,15 @@
220220
(return-instruction---return-at-capacity)
221221
))
222222

223-
(defconstraint return-instruction---setting-the-first-misc-row (:guard (return-instruction---standard-scenario-row))
224-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
225-
(eq! (weighted-MISC-flag-sum ROFF_RETURN___1ST_MISC_ROW)
226-
(+ (* MISC_WEIGHT_MMU (return-instruction---trigger_MMU))
227-
(* MISC_WEIGHT_MXP (return-instruction---trigger_MXP))
228-
(* MISC_WEIGHT_OOB (return-instruction---trigger_OOB))
229-
)))
223+
(defconstraint return-instruction---setting-the-first-misc-row
224+
(:guard (return-instruction---standard-scenario-row))
225+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
226+
(begin
227+
(eq! (shift misc/EXP_FLAG ROFF_RETURN___1ST_MISC_ROW) 0)
228+
(eq! (shift misc/MMU_FLAG ROFF_RETURN___1ST_MISC_ROW) (return-instruction---trigger_MMU))
229+
(eq! (shift misc/MXP_FLAG ROFF_RETURN___1ST_MISC_ROW) (return-instruction---trigger_MXP))
230+
(eq! (shift misc/OOB_FLAG ROFF_RETURN___1ST_MISC_ROW) (return-instruction---trigger_OOB))
231+
(eq! (shift misc/STP_FLAG ROFF_RETURN___1ST_MISC_ROW) 0)))
230232

231233
(defun (return-instruction---trigger_MXP) 1)
232234
(defun (return-instruction---trigger_OOB) (+ (return-instruction---exception-flag-MAXCSX) (scenario-shorthand---RETURN---nonempty-deployment)))

‎hub/cancun/constraints/instruction-handling/keccak.lisp‎

Lines changed: 32 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -32,27 +32,32 @@
3232
(defun (keccak-instruction---trigger_MMU) (* (- 1 XAHOY) (keccak-instruction---MXP-s1nznomxpx)))
3333
(defun (keccak-instruction---no-stack-exceptions) (* PEEK_AT_STACK stack/KEC_FLAG (- 1 stack/SUX stack/SOX)))
3434

35-
(defconstraint keccak-instruction---setting-stack-pattern (:guard (keccak-instruction---no-stack-exceptions))
35+
(defconstraint keccak-instruction---setting-stack-pattern
36+
(:guard (keccak-instruction---no-stack-exceptions))
3637
(stack-pattern-2-1))
3738

38-
(defconstraint keccak-instruction---allowable-exceptions (:guard (keccak-instruction---no-stack-exceptions))
39+
(defconstraint keccak-instruction---allowable-exceptions
40+
(:guard (keccak-instruction---no-stack-exceptions))
3941
(eq! XAHOY
4042
(+ stack/MXPX
4143
stack/OOGX)))
4244

43-
(defconstraint keccak-instruction---setting-NSR-and-peeking-flags (:guard (keccak-instruction---no-stack-exceptions))
45+
(defconstraint keccak-instruction---setting-NSR-and-peeking-flags
46+
(:guard (keccak-instruction---no-stack-exceptions))
4447
(begin (eq! NON_STACK_ROWS (+ 1 CONTEXT_MAY_CHANGE))
4548
(eq! NON_STACK_ROWS
46-
(+ (shift PEEK_AT_MISCELLANEOUS 1)
49+
(+ (shift PEEK_AT_MISCELLANEOUS ROFF___KEC___MISCELLANEOUS_ROW)
4750
(* (shift PEEK_AT_CONTEXT 2) CONTEXT_MAY_CHANGE)))))
4851

49-
(defconstraint keccak-instruction---setting-MISC-flags (:guard (keccak-instruction---no-stack-exceptions))
50-
(eq! (weighted-MISC-flag-sum 1)
51-
(+ MISC_WEIGHT_MXP
52-
(* MISC_WEIGHT_MMU (keccak-instruction---trigger_MMU)))))
52+
(defconstraint keccak-instruction---setting-MISC-flags
53+
(:guard (keccak-instruction---no-stack-exceptions))
54+
(begin
55+
(eq! (weighted-MISC-flag-sum-sans-MMU ROFF___KEC___MISCELLANEOUS_ROW) MISC_WEIGHT_MXP)
56+
(eq! (shift misc/MMU_FLAG ROFF___KEC___MISCELLANEOUS_ROW) (keccak-instruction---trigger_MMU))))
5357

54-
(defconstraint keccak-instruction---setting-MXP-parameters (:guard (keccak-instruction---no-stack-exceptions))
55-
(set-MXP-instruction---single-mxp-offset-instructions 1 ;; row offset kappa
58+
(defconstraint keccak-instruction---setting-MXP-parameters
59+
(:guard (keccak-instruction---no-stack-exceptions))
60+
(set-MXP-instruction---single-mxp-offset-instructions ROFF___KEC___MISCELLANEOUS_ROW ;; row offset kappa
5661
EVM_INST_SHA3 ;; instruction
5762
0 ;; deploys (bit modifying the behaviour of RETURN pricing)
5863
(keccak-instruction---offset-hi) ;; source offset high
@@ -61,23 +66,24 @@
6166
(keccak-instruction---size-lo) ;; source size low
6267
))
6368

64-
(defconstraint keccak-instruction---setting-MMU-parameters (:guard (keccak-instruction---no-stack-exceptions))
69+
(defconstraint keccak-instruction---setting-MMU-parameters
70+
(:guard (keccak-instruction---no-stack-exceptions))
6571
(if-not-zero misc/MMU_FLAG
66-
(set-MMU-instruction---ram-to-exo-with-padding 1 ;; offset
67-
CN ;; source ID
68-
0 ;; target ID
69-
(+ 1 HUB_STAMP) ;; auxiliary ID
70-
;; src_offset_hi ;; source offset high
71-
(keccak-instruction---offset-lo) ;; source offset low
72-
;; tgt_offset_lo ;; target offset low
73-
(keccak-instruction---size-lo) ;; size
74-
;; ref_offset ;; reference offset
75-
(keccak-instruction---size-lo) ;; reference size
76-
0 ;; success bit
77-
;; limb_1 ;; limb 1
78-
;; limb_2 ;; limb 2
79-
EXO_SUM_WEIGHT_KEC ;; weighted exogenous module flag sum
80-
0 ;; phase
72+
(set-MMU-instruction---ram-to-exo-with-padding ROFF___KEC___MISCELLANEOUS_ROW ;; offset
73+
CN ;; source ID
74+
0 ;; target ID
75+
(+ 1 HUB_STAMP) ;; auxiliary ID
76+
;; src_offset_hi ;; source offset high
77+
(keccak-instruction---offset-lo) ;; source offset low
78+
;; tgt_offset_lo ;; target offset low
79+
(keccak-instruction---size-lo) ;; size
80+
;; ref_offset ;; reference offset
81+
(keccak-instruction---size-lo) ;; reference size
82+
0 ;; success bit
83+
;; limb_1 ;; limb 1
84+
;; limb_2 ;; limb 2
85+
EXO_SUM_WEIGHT_KEC ;; weighted exogenous module flag sum
86+
0 ;; phase
8187
)))
8288

8389
(defconstraint keccak-instruction---transferring-MXPX-to-stack

‎hub/cancun/constraints/instruction-handling/log.lisp‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -95,9 +95,10 @@
9595

9696
(defconstraint log-instruction---setting-MISC-module-flags (:guard (log-instruction---standard-hypothesis))
9797
(if-zero stack/STATICX
98-
(eq! (weighted-MISC-flag-sum ROFF_LOG___MISCELLANEOUS_ROW)
99-
(+ (* MISC_WEIGHT_MMU (trigger_MMU))
100-
MISC_WEIGHT_MXP))))
98+
(begin
99+
(eq! (weighted-MISC-flag-sum-sans-MMU ROFF_LOG___MISCELLANEOUS_ROW) MISC_WEIGHT_MXP)
100+
(eq! (shift misc/MMU_FLAG ROFF_LOG___MISCELLANEOUS_ROW) (log-instruction---trigger-MMU)))))
101+
101102

102103
(defconstraint log-instruction---MISC-row-setting-MXP-data (:guard (log-instruction---standard-hypothesis))
103104
(if-zero stack/STATICX
@@ -109,8 +110,8 @@
109110
(log-instruction---size-hi) ;; size high
110111
(log-instruction---size-lo)))) ;; size low
111112

112-
(defun (trigger_MMU) (* (- 1 CONTEXT_WILL_REVERT)
113-
(shift misc/MXP_SIZE_1_NONZERO_NO_MXPX ROFF_LOG___MISCELLANEOUS_ROW)))
113+
(defun (log-instruction---trigger-MMU) (* (- 1 CONTEXT_WILL_REVERT)
114+
(shift misc/MXP_SIZE_1_NONZERO_NO_MXPX ROFF_LOG___MISCELLANEOUS_ROW)))
114115

115116
(defconstraint log-instruction---MISC-row-setting-MMU-data (:guard (log-instruction---standard-hypothesis))
116117
(if-zero (force-bin stack/STATICX)

0 commit comments

Comments
 (0)