From f91f3e6868f6aebbf1647be54309e70a2ea1fa4d Mon Sep 17 00:00:00 2001 From: OlivierBBB Date: Thu, 10 Aug 2023 04:16:28 +0200 Subject: [PATCH 1/5] feat(implementation): transcribed the re-specified STP module --- stp/columns.lisp | 26 ++++ stp/constraints.lisp | 266 +++++++++++++++++++++++++++++++++++++++ stp/lookup_into_mod.lisp | 22 ++++ stp/lookup_into_wcp.lisp | 22 ++++ 4 files changed, 336 insertions(+) create mode 100644 stp/columns.lisp create mode 100644 stp/constraints.lisp create mode 100644 stp/lookup_into_mod.lisp create mode 100644 stp/lookup_into_wcp.lisp diff --git a/stp/columns.lisp b/stp/columns.lisp new file mode 100644 index 00000000..529e9908 --- /dev/null +++ b/stp/columns.lisp @@ -0,0 +1,26 @@ +(module stp) + +(defcolumns + STAMP + CT + (INST_TYPE :LOOBEAN) + (CCTV :LOOBEAN) + GAS_ACTUAL + GAS_MXP + GAS_COST + GAS_STIPEND + GAS_HI + GAS_LO + VAL_HI + VAL_LO + (TO_EXISTS :LOOBEAN) + (TO_WARM :LOOBEAN) + (OOGX :LOOBEAN) + (WCP_FLAG :LOOBEAN) + (DIV_FLAG :LOOBEAN) + EXO_INST + ARG_ONE_HI + ARG_ONE_LO + ARG_TWO_LO + RES_LO + ) diff --git a/stp/constraints.lisp b/stp/constraints.lisp new file mode 100644 index 00000000..65ba5dbb --- /dev/null +++ b/stp/constraints.lisp @@ -0,0 +1,266 @@ +(module stp) + +(defconst + DIV 0x04 + LT 0x10 + ISZERO 0x15 + max_ct_CALL 4 + max_ct_CREATE 2 + G_create 32000 + G_warmaccess 100 + G_coldaccountaccess 2600 + G_callvalue 9000 + G_newaccount 25000 + ) + +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.1 heartbeat ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint first-row (:domain {0}) + (vanishes! STAMP)) + +(defconstraint stamp-increments () + (vanishes! (* (will-inc STAMP 1) (will-remain-constant STAMP)))) + +(defconstraint initial-vanishings () + (if-zero STAMP + (begin + (vanishes! CT) + (vanishes! (+ WCP_FLAG MOD_FLAG))))) + +(defconstraint counter-reset () + (if-not-zero (will-remain-constant STAMP) + (vanishes! (next CT)))) + +(defconstraint heartbeat (:guard STAMP) + (if-zero INST_TYPE + ;; INST_TYPE = 0 i.e. dealing will CALL-type instructions + (if-eq-else CT max_ct_CALL + ;; CT == max_ct_CALL + (will-inc STAMP 1) + ;; CT != max_ct_CALL + (will-inc CT 1)) + ;; INST_TYPE = 1 i.e. dealing will CREATE-type instructions + (if-eq-else CT max_ct_CREATE + ;; CT == max_ct_CREATE + (will-inc STAMP 1) + ;; CT != max_ct_CREATE + (will-inc CT 1)))) + +(defconstraint final-row (:domain {-1}) + (if-not-zero STAMP + (if-zero INST_TYPE + ;; INST_TYPE = 0 <==> CALL-type instruction + (= CT max_ct_CALL) + ;; INST_TYPE = 1 <==> CREATE-type instruction + (= CT max_ct_CREATE)))) + + +;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.2 binary ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint binary-constraints () + (begin + (is-binary WCP_FLAG) + (is-binary MOD_FLAG) + (is-binary INST_TYPE) + (is-binary CCTV))) + +(defconstraint exclusive-flags () + (vanishes! (* WCP_FLAG MOD_FLAG))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.4 constancies ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint counter-constancies () + (begin + (counter-constancy CT GAS_ACTUAL) + (counter-constancy CT GAS_MXP) + (counter-constancy CT GAS_COST) + (counter-constancy CT GAS_STIPEND) + ; + (counter-constancy CT GAS_HI) + (counter-constancy CT GAS_LO) + ; + (counter-constancy CT VAL_HI) + (counter-constancy CT VAL_LO) + ; + (counter-constancy CT TO_EXISTS) + (counter-constancy CT TO_WARM) + ; + ; + (counter-constancy CT OOGX) + (counter-constancy CT INST_TYPE) + (counter-constancy CT CCTV))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 3.2 Constraints for CREATE-type instructions ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (first-row-of-CREATE) (* (did-remain-constant STAMP) INST_TYPE)) +(defun (create-gActual) GAS_ACTUAL) +(defun (create-gPrelim) (+ GAS_MXP G_create)) +(defun (create-gDiff) (- (create-gActual) (create-gPrelim))) +(defun (create-oneSixtyFourth) (shift RES_LO 2)) +(defun (create-LgDiff) (- (create-gDiff) (create-oneSixtyFourth))) + +(defconstraint CREATE-type (:guard (first-row-of-CREATE)) + (begin + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (vanishes! ARG_ONE_HI) + (= ARG_ONE_LO (create-gActual)) + (vanishes! ARG_TWO_LO) + (= EXO_INST LT) + (vanishes! RES_LO) + (= WCP_FLAG 1) + ;; (= DIV_FLAG 0) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i + 1 ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (vanishes! (next ARG_ONE_HI)) + (= (next ARG_ONE_LO) (create-gActual)) + (= (next ARG_TWO_LO) (create-gPrelim)) + (= (next EXO_INST) LT) + (= (next RES_LO) OOGX) + (= (next WCP_FLAG) 1) + ;; (= (next DIV_FLAG) 0) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i + 2 ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (vanishes! (shift ARG_ONE_HI 2)) + (= (shift ARG_ONE_LO 2) (create-gDiff)) + (= (shift ARG_TWO_LO 2) 64) + (= (shift EXO_INST 2) DIV) + ;; (= (shift RES_LO 2) ...) + (vanishes! (shift WCP_FLAG 2)) + (= (shift DIV_FLAG 2) (- 1 OOGX)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; Setting GAS_COST and GAS_STPD ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero OOGX + ;; OOGX == 0 + (begin + (= GAS_COST (+ (create-gPrelim) (create-LgDiff))) + (= GAS_STIPEND (create-LgDiff))) + ;; OOGX == 1 + (begin + (= GAS_COST (create-gPrelim)) + (vanishes! GAS_STIPEND))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 3.2 Constraints for CALL-type instructions ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; all of these definitions implicitly assume that the current row (i) is such that +;; - STAMP[i] != STAMP[i - 1] <= first row of the instruction +;; - INST_TYPE = 0 <= CALL-type instruction +(defun (first-row-of-CALL) (* (did-remain-constant STAMP) + (- 1 INST_TYPE))) +(defun (call-valueIsZero) (next RES_LO)) +(defun (call-gActual) GAS_ACTUAL) +(defun (call-gAccess) (+ (* TO_WARM G_warmaccess) + (* (- 1 TO_WARM) G_coldaccountaccess))) +(defun (call-gCreate) (* (- 1 TO_EXISTS) + G_newaccount)) +(defun (call-gTransfer) (* CCTV + (- 1 (valueIsZero)) + G_callvalue)) +(defun (call-gXtra) (+ (call-gAccess) + (call-gCreate) + (call-gTransfer))) +(defun (call-gPrelim) (+ GAS_MXP + (call-gXtra))) +(defun (call-oneSixtyFourths) (shift RES_LO 3)) +(defun (call-gDiff) (- (call-gActual) + (call-gPrelim))) +(defun (call-stpComp) (shift RES_LO 4)) +(defun (call-LgDiff) (- (call-gDiff) + (call-oneSixtyFourths))) +(defun (call-gMin) (+ (* (- 1 (call-stpComp)) (call-LgDiff)) + (* (call-stpComp) GAS_LO))) + + +(defconstraint CALL-type (:guard (first-row-of-CALL)) + (begin + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (vanishes! ARG_ONE_HI) + (= ARG_ONE_LO (call-gActual)) + (vanishes! ARG_TWO_LO) + (= EXO_INST LT) + (vanishes! RES_LO) + (= WCP_FLAG 1) + ;; (= DIV_FLAG 0) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i + 1 ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (= (next ARG_ONE_HI) VAL_HI) + (= (next ARG_ONE_LO) VAL_LO) + (vanishes! (next ARG_TWO_LO)) + (= (next EXO_INST) ISZERO) + ;; (= (next RES_LO) ...) + (= (next WCP_FLAG) CCTV) + (vanishes! (next DIV_FLAG)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i + 2 ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (vanishes! (shift ARG_ONE_HI 2)) + (= (shift ARG_ONE_LO 2) (call-gActual)) + (= (shift ARG_TWO_LO 2) (call-gPrelim)) + (= (shift EXO_INST 2) LT) + (= (shift RES_LO 2) OOGX) + (= (shift WCP_FLAG 2) 1) + ;; (vanishes! (shift DIV_FLAG 2)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i + 3 ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (vanishes! (shift ARG_ONE_HI 3)) + (if-zero OOGX (= (shift ARG_ONE_LO 3) (call-gDiff))) + (= (shift ARG_TWO_LO 3) 64) + (= (shift EXO_INST 3) DIV) + ;; (= (shift RES_LO 3) ...) + (vanishes! (shift WCP_FLAG 3)) + (= (shift DIV_FLAG 3) (- 1 OOGX)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i + 4 ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (= (shift ARG_ONE_HI 4) GAS_HI) + (= (shift ARG_ONE_LO 4) GAS_LO) + (if-zero OOGX (= (shift ARG_TWO_LO 4) (call-LgDiff))) + (= (shift EXO_INST 4) LT) + ;; (= (shift RES_LO 4) ...) + (= (shift WCP_FLAG 4) (- 1 OOGX)) + (vanishes! (shift DIV_FLAG 4)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; Setting GAS_COST and GAS_STPD ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero OOGX + ;; OOGX == 0 + (begin + (= GAS_COST (+ (call-gPrelim) (call-gMin))) + (= GAS_STIPEND (+ (call-gMin) + (* CCTV (- 1 (call-valueIsZero)) G_callstipend))) + ;; OOGX == 1 + (begin + (= GAS_COST (call-gPrelim)) + (vanishes! GAS_STIPEND)))))) diff --git a/stp/lookup_into_mod.lisp b/stp/lookup_into_mod.lisp new file mode 100644 index 00000000..8e51f3d1 --- /dev/null +++ b/stp/lookup_into_mod.lisp @@ -0,0 +1,22 @@ +(defplookup stp-into-mod + ; target columns (in MOD) + ( + mod.ARG_1_HI + mod.ARG_1_LO + mod.ARG_2_HI + mod.ARG_2_LO + mod.RES_HI + mod.RES_LO + mod.INST + ) + ; source columns (in STP) + ( + (* stp.ARG_ONE_HI stp.MOD_FLAG) + (* stp.ARG_ONE_LO stp.MOD_FLAG) + stp.ZERO + (* stp.ARG_TWO_LO stp.MOD_FLAG) + stp.ZERO + (* stp.RES_LO stp.MOD_FLAG) + (* stp.EXO_INST stp.MOD_FLAG) + ) +) diff --git a/stp/lookup_into_wcp.lisp b/stp/lookup_into_wcp.lisp new file mode 100644 index 00000000..f947063e --- /dev/null +++ b/stp/lookup_into_wcp.lisp @@ -0,0 +1,22 @@ +(defplookup stp-into-wcp + ; target colums (in WCP) + ( + wcp.ARG_1_HI + wcp.ARG_1_LO + wcp.ARG_2_HI + wcp.ARG_2_LO + wcp.RES_HI + wcp.RES_LO + wcp.INST + ) + ; source columns (in STP) + ( + (* stp.ARG_ONE_HI stp.WCP_FLAG) + (* stp.ARG_ONE_LO stp.WCP_FLAG) + stp.ZERO + (* stp.ARG_TWO_LO stp.WCP_FLAG) + stp.ZERO + (* stp.RES_LO stp.WCP_FLAG) + (* stp.EXO_INST stp.WCP_FLAG) + ) +) From 5d76db076855d828a65b18fd9ca51082616ed8cd Mon Sep 17 00:00:00 2001 From: OlivierBBB Date: Mon, 14 Aug 2023 16:41:54 +0200 Subject: [PATCH 2/5] feat: finished the bingo card constraints --- stp/columns.lisp | 43 +++-- stp/constraints.lisp | 356 +++++++++++++++++++++++++-------------- stp/lookup_into_mod.lisp | 6 +- stp/lookup_into_wcp.lisp | 6 +- 4 files changed, 268 insertions(+), 143 deletions(-) diff --git a/stp/columns.lisp b/stp/columns.lisp index 529e9908..4f8e43fe 100644 --- a/stp/columns.lisp +++ b/stp/columns.lisp @@ -3,24 +3,45 @@ (defcolumns STAMP CT - (INST_TYPE :LOOBEAN) - (CCTV :LOOBEAN) + CT_MAX + (INSTRUCTION_TYPE :BOOLEAN) + (CALL_CAN_TRANSFER_VALUE :BOOLEAN) + ;; GAS_ACTUAL GAS_MXP GAS_COST GAS_STIPEND + ;; GAS_HI GAS_LO VAL_HI VAL_LO - (TO_EXISTS :LOOBEAN) - (TO_WARM :LOOBEAN) - (OOGX :LOOBEAN) - (WCP_FLAG :LOOBEAN) - (DIV_FLAG :LOOBEAN) - EXO_INST - ARG_ONE_HI - ARG_ONE_LO - ARG_TWO_LO + ;; + (TO_EXISTS :BOOLEAN) + (TO_WARM :BOOLEAN) + (OUT_OF_GAS_EXCEPTION :BOOLEAN) + ;; + (ABORT :BOOLEAN) + CALL_STACK_DEPTH + FROM_BALANCE + TO_NONCE + (TO_HAS_CODE :BOOLEAN) + ;; + (WCP_FLAG :BOOLEAN) + (MOD_FLAG :BOOLEAN) + EXOGENOUS_MODULE_INSTRUCTION + ARG_1_HI + ARG_1_LO + ARG_2_LO RES_LO + ;; TODO find solution for this hack + ZERO + ) + +(defalias + INST_TYPE INSTRUCTION_TYPE + CCTV CALL_CAN_TRANSFER_VALUE + CSD CALL_STACK_DEPTH + OOGX OUT_OF_GAS_EXCEPTION + EXO_INST EXOGENOUS_MODAULE_INSTRUCTION ) diff --git a/stp/constraints.lisp b/stp/constraints.lisp index 65ba5dbb..dfa29521 100644 --- a/stp/constraints.lisp +++ b/stp/constraints.lisp @@ -3,14 +3,18 @@ (defconst DIV 0x04 LT 0x10 + GT 0x11 + EQ 0x14 ISZERO 0x15 - max_ct_CALL 4 - max_ct_CREATE 2 + max_CT_CALL 6 + max_CT_CALL_OOGX 2 + ;; CT_MAX_DELTA 4 G_create 32000 G_warmaccess 100 G_coldaccountaccess 2600 G_callvalue 9000 G_newaccount 25000 + G_callstipend 2300 ) ;;;;;;;;;;;;;;;;;;;;;;;;; @@ -23,7 +27,7 @@ (vanishes! STAMP)) (defconstraint stamp-increments () - (vanishes! (* (will-inc STAMP 1) (will-remain-constant STAMP)))) + (vanishes! (* (will-inc! STAMP 1) (will-remain-constant! STAMP)))) (defconstraint initial-vanishings () (if-zero STAMP @@ -32,31 +36,39 @@ (vanishes! (+ WCP_FLAG MOD_FLAG))))) (defconstraint counter-reset () - (if-not-zero (will-remain-constant STAMP) + (if-not-zero (will-remain-constant! STAMP) (vanishes! (next CT)))) (defconstraint heartbeat (:guard STAMP) - (if-zero INST_TYPE - ;; INST_TYPE = 0 i.e. dealing will CALL-type instructions - (if-eq-else CT max_ct_CALL - ;; CT == max_ct_CALL - (will-inc STAMP 1) - ;; CT != max_ct_CALL - (will-inc CT 1)) - ;; INST_TYPE = 1 i.e. dealing will CREATE-type instructions - (if-eq-else CT max_ct_CREATE - ;; CT == max_ct_CREATE - (will-inc STAMP 1) - ;; CT != max_ct_CREATE - (will-inc CT 1)))) + (begin + (= (+ CT_MAX + INST_TYPE + (* (- max_CT_CALL max_CT_CALL_OOGX) + OOGX)) + CT_MAX_CALL) + (if-eq-else CT CT_MAX + (will-inc! STAMP 1) + (will-inc! CT 1)))) + ;; (if-zero INST_TYPE + ;; ;; INST_TYPE = 0 i.e. dealing will CALL-type instructions + ;; (if-eq-else CT max_ct_CALL + ;; ;; CT == max_ct_CALL + ;; (will-inc! STAMP 1) + ;; ;; CT != max_ct_CALL + ;; (will-inc! CT 1)) + ;; ;; INST_TYPE = 1 i.e. dealing will CREATE-type instructions + ;; (if-eq-else CT max_ct_CREATE + ;; ;; CT == max_ct_CREATE + ;; (will-inc! STAMP 1) + ;; ;; CT != max_ct_CREATE + ;; (will-inc! CT 1))))) (defconstraint final-row (:domain {-1}) (if-not-zero STAMP (if-zero INST_TYPE - ;; INST_TYPE = 0 <==> CALL-type instruction - (= CT max_ct_CALL) - ;; INST_TYPE = 1 <==> CREATE-type instruction - (= CT max_ct_CREATE)))) + (= CT CT_MAX)))) +;; (= CT max_ct_CALL) ;; INST_TYPE = 0 <==> CALL-type instruction +;; (= CT max_ct_CREATE)))) ;; INST_TYPE = 1 <==> CREATE-type instruction ;;;;;;;;;;;;;;;;;;;;;; @@ -68,10 +80,15 @@ (defconstraint binary-constraints () (begin + (debug (is-binary INST_TYPE)) + (debug (is-binary CCTV)) + (debug (is-binary TO_EXISTS)) + (debug (is-binary TO_WARM)) + (debug (is-binary OOGX)) + (debug (is-binary TO_HAS_CODE)) + (debug (is-binary ABORT)) (is-binary WCP_FLAG) - (is-binary MOD_FLAG) - (is-binary INST_TYPE) - (is-binary CCTV))) + (is-binary MOD_FLAG))) (defconstraint exclusive-flags () (vanishes! (* WCP_FLAG MOD_FLAG))) @@ -100,10 +117,16 @@ (counter-constancy CT TO_EXISTS) (counter-constancy CT TO_WARM) ; + (counter-constancy CT CSD) + (counter-constancy CT FROM_BALANCE) + (counter-constancy CT FROM_HAS_CODE) + (counter-constancy CT TO_NONCE) + (counter-constancy CT ABORT) ; (counter-constancy CT OOGX) (counter-constancy CT INST_TYPE) - (counter-constancy CT CCTV))) + (counter-constancy CT CCTV) + (counter-constancy CT CT_MAX))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -112,57 +135,105 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun (first-row-of-CREATE) (* (did-remain-constant STAMP) INST_TYPE)) -(defun (create-gActual) GAS_ACTUAL) -(defun (create-gPrelim) (+ GAS_MXP G_create)) -(defun (create-gDiff) (- (create-gActual) (create-gPrelim))) -(defun (create-oneSixtyFourth) (shift RES_LO 2)) -(defun (create-LgDiff) (- (create-gDiff) (create-oneSixtyFourth))) +(defun (first-row-of-CREATE) (* (remained-constant! STAMP) INST_TYPE)) +(defun (first-row-of-unexceptional-CREATE) (* (first-row-of-CREATE) (- 1 OOGX))) +(defun (create-gActual) GAS_ACTUAL) +(defun (create-gPrelim) (+ GAS_MXP G_create)) +(defun (create-gDiff) (- (create-gActual) (create-gPrelim))) +(defun (create-oneSixtyFourth) (shift RES_LO 2)) +(defun (create-LgDiff) (- (create-gDiff) (create-oneSixtyFourth))) +(defun (create-abortSum) (+ (- 1 (shift RES_LO 3)) ;; <- evaluates to 1 iff CSD >= 1024 + (shift RES_LO 4) ;; <- evaluates to 1 iff CALL_VALUE > FROM_BALANCE + (- 1 (shift RES_LO 5)) ;; <- evaluates to 1 iff TO address has nonzero nonce + TO_HAS_CODE)) ;; <- evaluates to 1 iff TO address has nonempty code -(defconstraint CREATE-type (:guard (first-row-of-CREATE)) +;; common rows of all CREATE instructions +(defconstraint CREATE-type-common (:guard (first-row-of-CREATE)) (begin ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -------------> row i ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (vanishes! ARG_ONE_HI) - (= ARG_ONE_LO (create-gActual)) - (vanishes! ARG_TWO_LO) + (vanishes! ARG_1_HI) + (= ARG_1_LO (create-gActual)) + (vanishes! ARG_2_LO) (= EXO_INST LT) (vanishes! RES_LO) (= WCP_FLAG 1) - ;; (= DIV_FLAG 0) + ;; (= MOD_FLAG 0) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -------------> row i + 1 ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (vanishes! (next ARG_ONE_HI)) - (= (next ARG_ONE_LO) (create-gActual)) - (= (next ARG_TWO_LO) (create-gPrelim)) + (vanishes! (next ARG_1_HI)) + (= (next ARG_1_LO) (create-gActual)) + (= (next ARG_2_LO) (create-gPrelim)) (= (next EXO_INST) LT) (= (next RES_LO) OOGX) (= (next WCP_FLAG) 1) - ;; (= (next DIV_FLAG) 0) + ;; (= (next MOD_FLAG) 0) + )) + +;; rows of CREATE instructions that don't produce an OOGX +(defconstraint CREATE-type-no-exception (:guard (first-row-of-unexceptional-CREATE)) + (begin ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -------------> row i + 2 ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (vanishes! (shift ARG_ONE_HI 2)) - (= (shift ARG_ONE_LO 2) (create-gDiff)) - (= (shift ARG_TWO_LO 2) 64) + (vanishes! (shift ARG_1_HI 2)) + (= (shift ARG_1_LO 2) (create-gDiff)) + (= (shift ARG_2_LO 2) 64) (= (shift EXO_INST 2) DIV) ;; (= (shift RES_LO 2) ...) (vanishes! (shift WCP_FLAG 2)) - (= (shift DIV_FLAG 2) (- 1 OOGX)) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; Setting GAS_COST and GAS_STPD ;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (if-zero OOGX - ;; OOGX == 0 - (begin - (= GAS_COST (+ (create-gPrelim) (create-LgDiff))) - (= GAS_STIPEND (create-LgDiff))) - ;; OOGX == 1 - (begin - (= GAS_COST (create-gPrelim)) - (vanishes! GAS_STIPEND))))) + (= (shift MOD_FLAG 2) (- 1 OOGX)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i + 3 ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (vanishes! (shift ARG_1_HI 3)) + (= (shift ARG_1_LO 3) CSD) + (= (shift ARG_2_LO 3) 1024) + (= (shift EXO_INST 3) LT) + ;; (= (shift RES_LO 3) ...) + (= (shift WCP_FLAG 3) 1) + ;; (vanishes! (shift MOD_FLAG 3)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i + 4 ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (= (shift ARG_1_HI 4) VAL_HI) + (= (shift ARG_1_LO 4) VAL_LO) + (= (shift ARG_2_LO 4) FROM_BALANCE) + (= (shift EXO_INST 4) GT) + ;; (= (shift RES_LO 4) ...) + (= (shift WCP_FLAG 4) 1) + ;; (vanishes! (shift MOD_FLAG 4)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i + 5 ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (vanishes! (shift ARG_1_HI 5)) + (= (shift ARG_1_LO 5) TO_NONCE) + (vanishes! (shift ARG_2_LO 5)) + (= (shift EXO_INST 5) ISZERO) + ;; (= (shift RES_LO 5) ...) + (= (shift WCP_FLAG 5) 1) + ;; (vanishes! (shift MOD_FLAG 5)))) + )) + +(defconstraint CREATE-type-outputs (:guard (first-row-of-unexceptional-CREATE)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; Setting GAS_COST and GAS_STPD ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero OOGX + ;; OOGX == 0 + (begin + (= GAS_COST (+ (create-gPrelim) (create-LgDiff))) + (= GAS_STIPEND (create-LgDiff)) + (if-zero (create-abortSum) + (vanishes! ABORT) + (= ABORT 1))) + ;; OOGX == 1 + (begin + (= GAS_COST (create-gPrelim)) + (vanishes! GAS_STIPEND) + (vanishes! ABORT))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -173,94 +244,127 @@ ;; all of these definitions implicitly assume that the current row (i) is such that ;; - STAMP[i] != STAMP[i - 1] <= first row of the instruction ;; - INST_TYPE = 0 <= CALL-type instruction -(defun (first-row-of-CALL) (* (did-remain-constant STAMP) - (- 1 INST_TYPE))) -(defun (call-valueIsZero) (next RES_LO)) -(defun (call-gActual) GAS_ACTUAL) -(defun (call-gAccess) (+ (* TO_WARM G_warmaccess) - (* (- 1 TO_WARM) G_coldaccountaccess))) -(defun (call-gCreate) (* (- 1 TO_EXISTS) - G_newaccount)) -(defun (call-gTransfer) (* CCTV - (- 1 (valueIsZero)) - G_callvalue)) -(defun (call-gXtra) (+ (call-gAccess) - (call-gCreate) - (call-gTransfer))) -(defun (call-gPrelim) (+ GAS_MXP - (call-gXtra))) -(defun (call-oneSixtyFourths) (shift RES_LO 3)) -(defun (call-gDiff) (- (call-gActual) - (call-gPrelim))) -(defun (call-stpComp) (shift RES_LO 4)) -(defun (call-LgDiff) (- (call-gDiff) - (call-oneSixtyFourths))) -(defun (call-gMin) (+ (* (- 1 (call-stpComp)) (call-LgDiff)) - (* (call-stpComp) GAS_LO))) +(defun (first-row-of-CALL) (* (remained-constant! STAMP) (- 1 INST_TYPE))) +(defun (first-row-of-unexceptional-CREATE) (* (first-row-of-CALL) (- 1 OOGX))) +(defun (call-valueIsZero) (next RES_LO)) +(defun (call-gActual) GAS_ACTUAL) +(defun (call-gAccess) (+ (* TO_WARM G_warmaccess) + (* (- 1 TO_WARM) G_coldaccountaccess))) +(defun (call-gCreate) (* (- 1 TO_EXISTS) + G_newaccount)) +(defun (call-gTransfer) (* CCTV + (- 1 (call-valueIsZero)) + G_callvalue)) +(defun (call-gXtra) (+ (call-gAccess) + (call-gCreate) + (call-gTransfer))) +(defun (call-gPrelim) (+ GAS_MXP + (call-gXtra))) +(defun (call-oneSixtyFourths) (shift RES_LO 3)) +(defun (call-gDiff) (- (call-gActual) + (call-gPrelim))) +(defun (call-stpComp) (shift RES_LO 4)) +(defun (call-LgDiff) (- (call-gDiff) + (call-oneSixtyFourths))) +(defun (call-gMin) (+ (* (- 1 (call-stpComp)) (call-LgDiff)) + (* (call-stpComp) GAS_LO))) +(defun (call-abortSum) (+ (- 1 (shift RES_LO 5)) ;; <- evaluates to 1 iff CSD >= 1024 + (shift RES_LO 6))) ;; <- evaluates to 1 iff CALL_VALUE > FROM_BALANCE -(defconstraint CALL-type (:guard (first-row-of-CALL)) +;; common rows of all CREATE instructions +(defconstraint CALL-type-common (:guard (first-row-of-CALL)) (begin ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -------------> row i ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (vanishes! ARG_ONE_HI) - (= ARG_ONE_LO (call-gActual)) - (vanishes! ARG_TWO_LO) + (vanishes! ARG_1_HI) + (= ARG_1_LO (call-gActual)) + (vanishes! ARG_2_LO) (= EXO_INST LT) (vanishes! RES_LO) (= WCP_FLAG 1) - ;; (= DIV_FLAG 0) + ;; (= MOD_FLAG 0) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -------------> row i + 1 ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (= (next ARG_ONE_HI) VAL_HI) - (= (next ARG_ONE_LO) VAL_LO) - (vanishes! (next ARG_TWO_LO)) + (= (next ARG_1_HI) VAL_HI) + (= (next ARG_1_LO) VAL_LO) + (vanishes! (next ARG_2_LO)) (= (next EXO_INST) ISZERO) ;; (= (next RES_LO) ...) (= (next WCP_FLAG) CCTV) - (vanishes! (next DIV_FLAG)) + (vanishes! (next MOD_FLAG)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -------------> row i + 2 ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (vanishes! (shift ARG_ONE_HI 2)) - (= (shift ARG_ONE_LO 2) (call-gActual)) - (= (shift ARG_TWO_LO 2) (call-gPrelim)) + (vanishes! (shift ARG_1_HI 2)) + (= (shift ARG_1_LO 2) (call-gActual)) + (= (shift ARG_2_LO 2) (call-gPrelim)) (= (shift EXO_INST 2) LT) (= (shift RES_LO 2) OOGX) (= (shift WCP_FLAG 2) 1) - ;; (vanishes! (shift DIV_FLAG 2)) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; -------------> row i + 3 ;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (vanishes! (shift ARG_ONE_HI 3)) - (if-zero OOGX (= (shift ARG_ONE_LO 3) (call-gDiff))) - (= (shift ARG_TWO_LO 3) 64) - (= (shift EXO_INST 3) DIV) - ;; (= (shift RES_LO 3) ...) - (vanishes! (shift WCP_FLAG 3)) - (= (shift DIV_FLAG 3) (- 1 OOGX)) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; -------------> row i + 4 ;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (= (shift ARG_ONE_HI 4) GAS_HI) - (= (shift ARG_ONE_LO 4) GAS_LO) - (if-zero OOGX (= (shift ARG_TWO_LO 4) (call-LgDiff))) - (= (shift EXO_INST 4) LT) - ;; (= (shift RES_LO 4) ...) - (= (shift WCP_FLAG 4) (- 1 OOGX)) - (vanishes! (shift DIV_FLAG 4)) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; Setting GAS_COST and GAS_STPD ;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (if-zero OOGX - ;; OOGX == 0 - (begin - (= GAS_COST (+ (call-gPrelim) (call-gMin))) - (= GAS_STIPEND (+ (call-gMin) - (* CCTV (- 1 (call-valueIsZero)) G_callstipend))) - ;; OOGX == 1 - (begin - (= GAS_COST (call-gPrelim)) - (vanishes! GAS_STIPEND)))))) + ;; (vanishes! (shift MOD_FLAG 2)) + )) + +;; +(defconstraint CALL-type-no-exception (:guard (first-row-of-CALL-unexceptional) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i + 3 ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (vanishes! (shift ARG_1_HI 3)) + (if-zero OOGX (= (shift ARG_1_LO 3) (call-gDiff))) + (= (shift ARG_2_LO 3) 64) + (= (shift EXO_INST 3) DIV) + ;; (= (shift RES_LO 3) ...) + ;; (vanishes! (shift WCP_FLAG 3)) + (= (shift MOD_FLAG 3) 1) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i + 4 ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (= (shift ARG_1_HI 4) GAS_HI) + (= (shift ARG_1_LO 4) GAS_LO) + (= (shift ARG_2_LO 4) (call-LgDiff)) + (= (shift EXO_INST 4) LT) + ;; (= (shift RES_LO 4) ...) + (= (shift WCP_FLAG 4) 1) + ;; (vanishes! (shift MOD_FLAG 4)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i + 5 ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (vanishes! (shift ARG_1_HI 5)) + (= (shift ARG_1_LO 5) CSD) + (= (shift ARG_2_LO 5) 1024) + (= (shift EXO_INST 5) LT) + ;; (= (shift RES_LO 5) ...) + (= (shift WCP_FLAG 5) 1) + ;; (vanishes! (shift MOD_FLAG 5)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; -------------> row i + 6 ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (= (shift ARG_1_HI 6) VAL_HI) + (= (shift ARG_1_LO 6) VAL_LO) + (= (shift ARG_2_LO 6) FROM_BALANCE) + (= (shift EXO_INST 6) GT) + ;; (= (shift RES_LO 6) ...) + (= (shift WCP_FLAG 6) 1) + ;; (vanishes! (shift MOD_FLAG 6)) + ))) + +(defconstraint CALL-type-outputs (:guard (first-row-of-CALL)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; Setting GAS_COST and GAS_STPD ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero OOGX + ;; OOGX == 0 + (begin + (= GAS_COST (+ (call-gPrelim) (call-gMin))) + (= GAS_STIPEND (+ (call-gMin) + (* CCTV (- 1 (call-valueIsZero)) G_callstipend))) + (if-zero (call-abortSum) + (vanishes! ABORT) + (= ABORT 1))) + ;; OOGX == 1 + (begin + (= GAS_COST (call-gPrelim)) + (vanishes! GAS_STIPEND)))))) diff --git a/stp/lookup_into_mod.lisp b/stp/lookup_into_mod.lisp index 8e51f3d1..67f03895 100644 --- a/stp/lookup_into_mod.lisp +++ b/stp/lookup_into_mod.lisp @@ -11,10 +11,10 @@ ) ; source columns (in STP) ( - (* stp.ARG_ONE_HI stp.MOD_FLAG) - (* stp.ARG_ONE_LO stp.MOD_FLAG) + (* stp.ARG_1_HI stp.MOD_FLAG) + (* stp.ARG_1_LO stp.MOD_FLAG) stp.ZERO - (* stp.ARG_TWO_LO stp.MOD_FLAG) + (* stp.ARG_2_LO stp.MOD_FLAG) stp.ZERO (* stp.RES_LO stp.MOD_FLAG) (* stp.EXO_INST stp.MOD_FLAG) diff --git a/stp/lookup_into_wcp.lisp b/stp/lookup_into_wcp.lisp index f947063e..c37fa032 100644 --- a/stp/lookup_into_wcp.lisp +++ b/stp/lookup_into_wcp.lisp @@ -11,10 +11,10 @@ ) ; source columns (in STP) ( - (* stp.ARG_ONE_HI stp.WCP_FLAG) - (* stp.ARG_ONE_LO stp.WCP_FLAG) + (* stp.ARG_1_HI stp.WCP_FLAG) + (* stp.ARG_1_LO stp.WCP_FLAG) stp.ZERO - (* stp.ARG_TWO_LO stp.WCP_FLAG) + (* stp.ARG_2_LO stp.WCP_FLAG) stp.ZERO (* stp.RES_LO stp.WCP_FLAG) (* stp.EXO_INST stp.WCP_FLAG) From 8f77355ce582f37010b3aa3633e24a6b62a7abcc Mon Sep 17 00:00:00 2001 From: OlivierBBB Date: Mon, 14 Aug 2023 16:56:34 +0200 Subject: [PATCH 3/5] moved lookups to a dedicated folder --- stp/{lookup_into_mod.lisp => lookups/into_mod.lisp} | 0 stp/{lookup_into_wcp.lisp => lookups/into_wcp.lisp} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename stp/{lookup_into_mod.lisp => lookups/into_mod.lisp} (100%) rename stp/{lookup_into_wcp.lisp => lookups/into_wcp.lisp} (100%) diff --git a/stp/lookup_into_mod.lisp b/stp/lookups/into_mod.lisp similarity index 100% rename from stp/lookup_into_mod.lisp rename to stp/lookups/into_mod.lisp diff --git a/stp/lookup_into_wcp.lisp b/stp/lookups/into_wcp.lisp similarity index 100% rename from stp/lookup_into_wcp.lisp rename to stp/lookups/into_wcp.lisp From f3c28dc950d5f643302842f88390c7465ef3707a Mon Sep 17 00:00:00 2001 From: OlivierBBB Date: Mon, 14 Aug 2023 17:16:51 +0200 Subject: [PATCH 4/5] fix(corset-compiles): made corset compile --- stp/columns.lisp | 2 +- stp/constraints.lisp | 41 +++++++++++++++++++++-------------------- 2 files changed, 22 insertions(+), 21 deletions(-) diff --git a/stp/columns.lisp b/stp/columns.lisp index 4f8e43fe..5aa5c68d 100644 --- a/stp/columns.lisp +++ b/stp/columns.lisp @@ -43,5 +43,5 @@ CCTV CALL_CAN_TRANSFER_VALUE CSD CALL_STACK_DEPTH OOGX OUT_OF_GAS_EXCEPTION - EXO_INST EXOGENOUS_MODAULE_INSTRUCTION + EXO_INST EXOGENOUS_MODULE_INSTRUCTION ) diff --git a/stp/constraints.lisp b/stp/constraints.lisp index dfa29521..a6b11344 100644 --- a/stp/constraints.lisp +++ b/stp/constraints.lisp @@ -45,23 +45,23 @@ INST_TYPE (* (- max_CT_CALL max_CT_CALL_OOGX) OOGX)) - CT_MAX_CALL) + max_CT_CALL_OOGX) (if-eq-else CT CT_MAX (will-inc! STAMP 1) (will-inc! CT 1)))) - ;; (if-zero INST_TYPE - ;; ;; INST_TYPE = 0 i.e. dealing will CALL-type instructions - ;; (if-eq-else CT max_ct_CALL - ;; ;; CT == max_ct_CALL - ;; (will-inc! STAMP 1) - ;; ;; CT != max_ct_CALL - ;; (will-inc! CT 1)) - ;; ;; INST_TYPE = 1 i.e. dealing will CREATE-type instructions - ;; (if-eq-else CT max_ct_CREATE - ;; ;; CT == max_ct_CREATE - ;; (will-inc! STAMP 1) - ;; ;; CT != max_ct_CREATE - ;; (will-inc! CT 1))))) +;; (if-zero INST_TYPE +;; ;; INST_TYPE = 0 i.e. dealing will CALL-type instructions +;; (if-eq-else CT max_ct_CALL +;; ;; CT == max_ct_CALL +;; (will-inc! STAMP 1) +;; ;; CT != max_ct_CALL +;; (will-inc! CT 1)) +;; ;; INST_TYPE = 1 i.e. dealing will CREATE-type instructions +;; (if-eq-else CT max_ct_CREATE +;; ;; CT == max_ct_CREATE +;; (will-inc! STAMP 1) +;; ;; CT != max_ct_CREATE +;; (will-inc! CT 1))))) (defconstraint final-row (:domain {-1}) (if-not-zero STAMP @@ -119,7 +119,7 @@ ; (counter-constancy CT CSD) (counter-constancy CT FROM_BALANCE) - (counter-constancy CT FROM_HAS_CODE) + (counter-constancy CT TO_HAS_CODE) (counter-constancy CT TO_NONCE) (counter-constancy CT ABORT) ; @@ -233,7 +233,7 @@ (begin (= GAS_COST (create-gPrelim)) (vanishes! GAS_STIPEND) - (vanishes! ABORT))) + (vanishes! ABORT)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -245,7 +245,7 @@ ;; - STAMP[i] != STAMP[i - 1] <= first row of the instruction ;; - INST_TYPE = 0 <= CALL-type instruction (defun (first-row-of-CALL) (* (remained-constant! STAMP) (- 1 INST_TYPE))) -(defun (first-row-of-unexceptional-CREATE) (* (first-row-of-CALL) (- 1 OOGX))) +(defun (first-row-of-unexceptional-CALL) (* (first-row-of-CALL) (- 1 OOGX))) (defun (call-valueIsZero) (next RES_LO)) (defun (call-gActual) GAS_ACTUAL) (defun (call-gAccess) (+ (* TO_WARM G_warmaccess) @@ -308,7 +308,8 @@ )) ;; -(defconstraint CALL-type-no-exception (:guard (first-row-of-CALL-unexceptional) +(defconstraint CALL-type-no-exception (:guard (first-row-of-unexceptional-CALL)) + (begin ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -------------> row i + 3 ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -349,7 +350,7 @@ ;; (= (shift RES_LO 6) ...) (= (shift WCP_FLAG 6) 1) ;; (vanishes! (shift MOD_FLAG 6)) - ))) + )) (defconstraint CALL-type-outputs (:guard (first-row-of-CALL)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -367,4 +368,4 @@ ;; OOGX == 1 (begin (= GAS_COST (call-gPrelim)) - (vanishes! GAS_STIPEND)))))) + (vanishes! GAS_STIPEND)))) From f6436d09479d63938e7f5f5e418dbf675510fc20 Mon Sep 17 00:00:00 2001 From: OlivierBBB Date: Tue, 15 Aug 2023 22:20:14 +0200 Subject: [PATCH 5/5] fix: tagged exo_inst as byte column --- stp/columns.lisp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/stp/columns.lisp b/stp/columns.lisp index 5aa5c68d..7a21a26e 100644 --- a/stp/columns.lisp +++ b/stp/columns.lisp @@ -29,7 +29,7 @@ ;; (WCP_FLAG :BOOLEAN) (MOD_FLAG :BOOLEAN) - EXOGENOUS_MODULE_INSTRUCTION + (EXOGENOUS_MODULE_INSTRUCTION :BYTE) ARG_1_HI ARG_1_LO ARG_2_LO