Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adding HUB constraints #494

Merged
merged 32 commits into from
Nov 5, 2024
+48 −49
Merged

Adding HUB constraints #494

Show file tree
Hide file tree
Changes from 30 commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
4ba5621
add HUB constraints
letypequividelespoubelles Oct 30, 2024
8bd3f94
typo
letypequividelespoubelles Oct 30, 2024
a2234f6
typo
letypequividelespoubelles Oct 30, 2024
837f08e
fix: removed stack consistency constraints
OlivierBBB Oct 30, 2024
16d3740
fix: make the constraints compile
OlivierBBB Oct 30, 2024
47fe220
Merge branch 'master' into 484-add-hub-constraints
OlivierBBB Oct 30, 2024
182ad13
fix: context consistency constraints
OlivierBBB Oct 30, 2024
7e018d1
fix: unexceptional RETURN's from message calls now always provide ret…
OlivierBBB Oct 30, 2024
b639c86
fix: unexceptional REVERT's now always provide return data, even in t…
OlivierBBB Oct 30, 2024
d04e219
fix: splitting the "REVERT setting context" constraint in two
OlivierBBB Oct 31, 2024
eb6bfec
fix: simplified GAS_COST for CALLDATACOPY + split the constraint
OlivierBBB Oct 31, 2024
b3790cf
fix: split GAS_COST for RETURNDATACOPY into SANS/WITH_COMPUTATION cases
OlivierBBB Oct 31, 2024
e3d7047
fix: splitting GAS_COST for CODECOPY
OlivierBBB Oct 31, 2024
0f5f552
fix: spliting GAS_COST for EXTCODECOPY
OlivierBBB Oct 31, 2024
1eb747f
fix: debug constraint had issue
OlivierBBB Oct 31, 2024
96f7c56
fix: TXN instruction family now uses is_ORIGIN and is_GASPRICE flags
OlivierBBB Oct 31, 2024
b6464f6
ras
OlivierBBB Oct 31, 2024
dc16d76
fix: mix up in SLOAD/SSTORE flags
OlivierBBB Oct 31, 2024
1399625
ras: splitting up the storage-instruction's "setting-values" into 3
OlivierBBB Oct 31, 2024
b58578e
ras: formatting + removed empty file
OlivierBBB Oct 31, 2024
409aa98
ras splitting of hub/generalities constraint
OlivierBBB Nov 1, 2024
91b79e9
fix: some renaming of jump instruction constriants
OlivierBBB Nov 1, 2024
74d9408
fix: splitting the MACHINE_STATE's "setting-stack-value" constraint in 3
OlivierBBB Nov 1, 2024
171c644
fix: remain faithful to spec
OlivierBBB Nov 1, 2024
4ee0ff8
fix: implemented the correct formula for MSIZE
OlivierBBB Nov 1, 2024
fb233c7
fix: create stack pattern STACK_STAMP typo for CREATE2's + renaming
OlivierBBB Nov 1, 2024
8a44249
ras: renaming
OlivierBBB Nov 4, 2024
5e82508
fix: using HUB_COLUMNS to merge stuff into arith-dev
OlivierBBB Nov 4, 2024
4ab67f2
Merge branch 'master' into 484-add-hub-constraints
OlivierBBB Nov 5, 2024
ae831ed
ras
OlivierBBB Nov 5, 2024
1ede9f5
ras
OlivierBBB Nov 5, 2024
bbc9587
typo
OlivierBBB Nov 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,7 @@ ZKEVM_MODULES_FOR_REFERENCE_TESTS := ${ALU} \
${EUC} \
${EXP} \
${GAS} \
${HUB_COLUMNS} \
${HUB} \
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is in ZKEVM_MODULES_FOR_REFERENCE_TESTS, which in any case blows up all over the place.

${LIBRARY} \
${LOG_DATA} \
${LOG_INFO} \
Expand Down
4 changes: 2 additions & 2 deletions hub/constraints/generalities/context.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,9 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;; (defconstraint setting-the-context-may-change-flag ()
;; (defconstraint generalitie---setting-the-CONTEXT_MAY_CHANGE-flag ()
OlivierBBB marked this conversation as resolved.
Show resolved Hide resolved
;; (begin
;; (is-binary CMC)
;; (is-binary CMC) ;; column already declared :binary@prove
;; (hub-stamp-constancy CMC)
;; (if-zero TX_EXEC (vanishes! CMC))
;; (if-not-zero PEEK_AT_STACK
Expand Down
69 changes: 34 additions & 35 deletions hub/constraints/generalities/exceptions.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,28 +42,29 @@



(defconstraint exception-flags-are-binary (:perspective stack)
(begin
(is-binary SUX )
(is-binary SOX )
(is-binary MXPX )
(is-binary OOGX )
(is-binary RDCX )
(is-binary JUMPX )
(is-binary STATICX )
(is-binary SSTOREX )
(is-binary ICPX )
(is-binary MAXCSX )
(is-binary OPCX )
))
;; ;; These columns are already marked binary@prove in their respective definitions
;; (defconstraint generalities---exceptions---stack-exception-flags-are-binary (:perspective stack)
;; (begin
;; (is-binary SUX )
;; (is-binary SOX )
;; (is-binary MXPX )
;; (is-binary OOGX )
;; (is-binary RDCX )
;; (is-binary JUMPX )
;; (is-binary STATICX )
;; (is-binary SSTOREX )
;; (is-binary ICPX )
;; (is-binary MAXCSX )
;; (is-binary OPCX )
;; ))


(defconstraint exception-flags-are-exclusive (:perspective stack)
(is-binary (exception_flag_sum)))
(defconstraint generalities---exceptions---stack-exception-flags-are-exclusive (:perspective stack)
(is-binary (exception_flag_sum)))


(defconstraint exception-flags-are-stack-constant (:perspective stack)
(stack-row-constancy (weighted_exception_flag_sum)))
(defconstraint generalities---exceptions---exception-flags-are-stack-constant (:perspective stack)
(stack-row-constancy (weighted_exception_flag_sum)))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
Expand All @@ -73,15 +74,15 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defconstraint automatic-exception-flag-vanishing (:perspective stack)
(begin
(eq! INVALID_FLAG OPCX)
(if-zero MXP_FLAG (vanishes! MXPX))
(if-zero JUMP_FLAG (vanishes! JUMPX))
(if-zero STATIC_FLAG (vanishes! STATICX))
(if-not-zero (- INSTRUCTION EVM_INST_RETURNDATACOPY) (vanishes! RDCX))
(if-not-zero (- INSTRUCTION EVM_INST_SSTORE) (vanishes! SSTOREX))
(if-not-zero (- INSTRUCTION EVM_INST_RETURN) (vanishes! (+ ICPX MAXCSX)))))
(defconstraint generalities---exceptions---automatic-stack-exception-flag-vanishing (:perspective stack)
(begin
(eq! INVALID_FLAG OPCX)
(if-zero MXP_FLAG (vanishes! MXPX))
(if-zero JUMP_FLAG (vanishes! JUMPX))
(if-zero STATIC_FLAG (vanishes! STATICX))
(if-not-zero (- INSTRUCTION EVM_INST_RETURNDATACOPY) (vanishes! RDCX))
(if-not-zero (- INSTRUCTION EVM_INST_SSTORE) (vanishes! SSTOREX))
(if-not-zero (- INSTRUCTION EVM_INST_RETURN) (vanishes! (+ ICPX MAXCSX)))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
Expand All @@ -91,11 +92,9 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; we deal with those constraints in context.lisp along side CMC

;; (defconstraint exception_ahoy ()
;; (begin
;; (is-binary XAHOY)
;; (hub-stamp-constancy XAHOY)
;; (if-zero TX_EXEC (vanishes! XAHOY))
;; (if-not-zero PEEK_AT_STACK
;; (eq! (exception_flag_sum) XAHOY))))
;; (defconstraint generalities---exceptions---setting-the-EXCEPTIONS_AHOY-flag ()
;; (begin
;; (is-binary XAHOY) ;; column already declared :binary@prove
;; (hub-stamp-constancy XAHOY)
;; (if-zero TX_EXEC (eq! XAHOY 0))
;; (if-not-zero PEEK_AT_STACK (eq! XAHOY (exception_flag_sum)))))
24 changes: 12 additions & 12 deletions hub/constraints/generalities/program_counter.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,16 +1,16 @@
(module hub)

(defconstraint PC-stamp-constancy ()
(begin
(hub-stamp-constancy PC)
(hub-stamp-constancy PC_NEW)))
(defconstraint generalities---program-counter---stamp-constancy ()
(begin
(hub-stamp-constancy PC)
(hub-stamp-constancy PC_NEW)))

(defconstraint PC-automatic-vanishing-outside-of-EXEC-phase ()
(if-zero TX_EXEC
(begin
(vanishes! PC)
(vanishes! PC_NEW))))
(defconstraint generalities---program-counter---automatic-vanishing-outside-of-EXEC-phase ()
(if-zero TX_EXEC
(begin
(vanishes! PC)
(vanishes! PC_NEW))))

(defconstraint PC-automatic-update (:guard PEEK_AT_STACK)
(if-zero (force-bin (+ stack/PUSHPOP_FLAG stack/JUMP_FLAG))
(eq! PC_NEW (+ 1 PC))))
(defconstraint generalities---program-counter---automatic-update (:guard PEEK_AT_STACK)
(if-zero (force-bin (+ stack/PUSHPOP_FLAG stack/JUMP_FLAG))
(eq! PC_NEW (+ 1 PC))))
Loading