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

Constraints update for GAS columns generalities #457

Merged
merged 1 commit into from
Oct 15, 2024
Merged

Constraints update for GAS columns generalities #457

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
52 changes: 34 additions & 18 deletions hub/constraints/generalities/gas.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,27 +12,49 @@
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defconstraint gas-column-constancies ()
(defconstraint gas-columns---stamp-constancies ()
(begin (hub-stamp-constancy GAS_EXPECTED)
(hub-stamp-constancy GAS_ACTUAL)
(hub-stamp-constancy GAS_COST)
(hub-stamp-constancy GAS_NEXT)))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 4.4.2 Gas transition constraints ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; TODO: should be debug
(defconstraint gas-columns---automatic-vanishing ()
(begin
(if-zero TX_EXEC
(begin
(vanishes! GAS_EXPECTED)
(vanishes! GAS_ACTUAL)
(vanishes! GAS_COST)
(vanishes! GAS_NEXT)))))

(defun (non-oog-exceptions) (+ stack/SUX
stack/SOX
stack/MXPX
stack/OPCX
stack/RDCX
stack/JUMPX
stack/STATICX
stack/SSTOREX
stack/ICPX
stack/MAXCSX))

(defconstraint setting-GAS_NEXT (:guard TX_EXEC)
(begin
(if-zero XAHOY
(eq! GAS_NEXT (- GAS_ACTUAL GAS_COST))
(vanishes! GAS_NEXT))))
(defconstraint gas-columns---GAS_COST-vanishes-for-non-OOG-exceptions (:perspective stack)
(if-not-zero (non-oog-exceptions)
(vanishes! GAS_COST)))

;; we drop the stack perspective preconditions
(defconstraint gas-columns---GAS_NEXT-vanishes-in-case-of-an-exception ()
(if-not-zero XAHOY
(vanishes! GAS_NEXT)))

(defconstraint gas-transitions-at-hub-stamp-transition ()
(defconstraint gas-columns---setting-GAS_NEXT-outside-of-CALLs-and-CREATEs (:perspective stack)
(if-zero XAHOY
(if-zero (force-bool (+ stack/CREATE_FLAG stack/CALL_FLAG))
(eq! GAS_NEXT (- GAS_ACTUAL GAS_COST)))))

(defconstraint gas-columns---hub-stamp-transition-constraints ()
(begin
(if-not-zero (will-remain-constant! HUB_STAMP)
(if-not-zero TX_EXEC
Expand All @@ -42,9 +64,3 @@
(if-eq CN_NEW CALLER_CN (eq! (next GAS_ACTUAL) (+ (next GAS_EXPECTED) GAS_NEXT)))
(if-eq CN_NEW (+ 1 HUB_STAMP) (eq! (next GAS_ACTUAL) (next GAS_EXPECTED)))))))))
;; can't define GAS_EXPECTED at this level of generality

;; WARNING
;; this constraint will likely fail for exceptional instructions that only have static gas costs
(defconstraint gas-cost-only-matters-in-case-of-OOGX-or-no-exceptions (:perspective stack)
(if-zero (force-bin (+ OOGX (- 1 XAHOY)))
(vanishes! GAS_COST)))
Loading