Skip to content

Commit

Permalink
Adding HUB constraints (#494)
Browse files Browse the repository at this point in the history 
Signed-off-by: F Bojarski <ceciestunepoubelle@protonmail.ch>
Signed-off-by: Olivier Bégassat <38285177+OlivierBBB@users.noreply.github.com>
Co-authored-by: F Bojarski <ceciestunepoubelle@protonmail.ch>
  • Loading branch information
@OlivierBBB @letypequividelespoubelles
OlivierBBB and letypequividelespoubelles authored Nov 5, 2024
1 parent c33a440 commit 564f00e
Show file tree
Hide file tree
Showing 3 changed files with 48 additions and 49 deletions.
4 changes: 2 additions & 2 deletions hub/constraints/generalities/context.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,9 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;; (defconstraint setting-the-context-may-change-flag ()
;; (defconstraint generalities---setting-the-CONTEXT_MAY_CHANGE-flag ()
;; (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
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
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))))

0 comments on commit 564f00e

Please sign in to comment.