fix: plug txnData constraints (#47)

Consensys · Feb 21, 2024 · 730afab · 730afab
1 parent 521b638
commit 730afab
Show file tree

Hide file tree

Showing 3 changed files with 37 additions and 38 deletions.
diff --git a/bin/columns.lisp b/bin/columns.lisp
@@ -5,7 +5,7 @@
   (ONE_LINE_INSTRUCTION :binary)
   (MLI :binary)
   (COUNTER :byte)
-  (INST :display :opcode)
+  (INST :byte :display :opcode)
   ARGUMENT_1_HI
   ARGUMENT_1_LO
   ARGUMENT_2_HI

diff --git a/txn_data/columns.lisp b/txn_data/columns.lisp
@@ -7,7 +7,7 @@
   BTC_NUM
   REL_TX_NUM_MAX
   REL_TX_NUM
-  CT
+  (CT :byte)
   FROM_HI
   FROM_LO
   NONCE
@@ -34,16 +34,16 @@
   REFUND_AMOUNT
   CUMULATIVE_CONSUMED_GAS
   (STATUS_CODE :binary)
-  PHASE_RLP_TXN
-  PHASE_RLP_TXNRCPT
+  (PHASE_RLP_TXN :byte)
+  (PHASE_RLP_TXNRCPT :byte)
   CODE_FRAGMENT_INDEX
   OUTGOING_HI
   OUTGOING_LO
   OUTGOING_RLP_TXNRCPT
   WCP_ARG_ONE_LO
   WCP_ARG_TWO_LO
   (WCP_RES_LO :binary)
-  WCP_INST)
+  (WCP_INST :byte :display :opcode))
 
 (defalias 
   ABS_MAX ABS_TX_NUM_MAX

diff --git a/txn_data/constraints.lisp b/txn_data/constraints.lisp
@@ -152,19 +152,20 @@
 ;;    2.5 Cumulative gas    ;;
 ;;                          ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(defconstraint cumulative-gas ()
-  (begin (if-zero ABS
-                  (vanishes! CUM_GAS))
-         (if-not-zero (will-remain-constant! BTC)
-                      ; BTC[i + 1] != BTC[i]
-                      (eq! (next CUMULATIVE_CONSUMED_GAS)
-                           (next (- GAS_LIMIT REFUND_AMOUNT))))
-         (if-not-zero (and (will-inc! BTC 1) (will-remain-constant! ABS))
-                      ; BTC[i + 1] != 1 + BTC[i] && ABS[i+1] != ABS[i] i.e. BTC[i + 1] == BTC[i] && ABS[i+1] == ABS[i] +1
-                      (eq! (next CUM_GAS)
-                           (+ CUM_GAS
-                              (next (- GAS_LIMIT REFUND_AMOUNT)))))))
-
+;;TODO reenable this constraint
+;;(defconstraint cumulative-gas ()
+;;  (begin (if-zero ABS
+;;                  (vanishes! CUM_GAS))
+;;         (if-not-zero (will-remain-constant! BTC)
+;;                      ; BTC[i + 1] != BTC[i]
+;;                      (eq! (next CUMULATIVE_CONSUMED_GAS)
+;;                           (next (- GAS_LIMIT REFUND_AMOUNT))))
+;;         (if-not-zero (and (will-inc! BTC 1) (will-remain-constant! ABS))
+;;                      ; BTC[i + 1] != 1 + BTC[i] && ABS[i+1] != ABS[i] i.e. BTC[i + 1] == BTC[i] && ABS[i+1] == ABS[i] +1
+;;                      (eq! (next CUM_GAS)
+;;                           (+ CUM_GAS
+;;                              (next (- GAS_LIMIT REFUND_AMOUNT)))))))
+;;
 ;;;;;;;;;;;;;;;;;;;;;;;
 ;;                   ;;
 ;;    2.6 Aliases    ;;
@@ -263,11 +264,14 @@
          (if-zero TYPE2
                   (vanishes! (shift OUTGOING_HI 6)))))
 
-;; ABS increments are 0/1
-(defconstraint verticalization (:guard (force-bool (remained-constant! ABS)))
-               (begin (setting_phase_numbers)
-                      (data_transfer)
-                      (vanishing_data_cells)))
+;; is non-zero for the first row of each tx
+(defun (first-row-trigger)
+  (- ABS (prev ABS)))
+
+(defconstraint verticalization (:guard (first-row-trigger))
+  (begin (setting_phase_numbers)
+         (data_transfer)
+         (vanishing_data_cells)))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;                       ;;
@@ -347,8 +351,7 @@
          ;;  (= (shift WCP_RES_LO     6) ???) ;; unknown
          ))
 
-;; ABS increments are 0/1
-(defconstraint comparisons (:guard (force-bool (remained-constant! ABS)))
+(defconstraint comparisons (:guard (first-row-trigger))
   (begin (sufficient_balance)
          (sufficient_gas_limit)
          (upper_limit_for_refunds)
@@ -363,10 +366,8 @@
 ;;    2.11 Gas and gas price constraints    ;;
 ;;                                          ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;; ABS increments are 0/1
-(defconstraint gas_and_gas_price (:guard (force-bool (remained-constant! ABS)))
-  (begin  ;; constraining INITIAL_GAS
+(defconstraint gas_and_gas_price (:guard (first-row-trigger))
+  (begin  ;; constraining INIT_GAS
          (= IGAS
             (- (gas_limit) (shift WCP_ARG_TWO_LO 1)))
          ;; constraining REFUND_AMOUNT
@@ -386,14 +387,12 @@
 ;;    2.11 Verticalisation for RlpTxnRcpt    ;;
 ;;                                           ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;; ABS increments are 0/1
-(defconstraint verticalisation-rlp-txn-rcpt (:guard (force-bool (remained-constant! ABS)))
-               (begin (eq! PHASE_RLP_TXNRCPT RLPRECEIPT_SUBPHASE_ID_TYPE)
-                      (eq! OUTGOING_RLP_TXNRCPT (tx_type))
-                      (eq! (next PHASE_RLP_TXNRCPT) RLPRECEIPT_SUBPHASE_ID_STATUS_CODE)
-                      (eq! (next OUTGOING_RLP_TXNRCPT) STATUS_CODE)
-                      (eq! (shift PHASE_RLP_TXNRCPT 2) RLPRECEIPT_SUBPHASE_ID_CUMUL_GAS)
-                      (eq! (shift OUTGOING_RLP_TXNRCPT 2) CUMULATIVE_CONSUMED_GAS)))
+(defconstraint verticalisation-rlp-txn-rcpt (:guard (first-row-trigger))
+  (begin (eq! PHASE_RLP_TXNRCPT RLPRECEIPT_SUBPHASE_ID_TYPE)
+         (eq! OUTGOING_RLP_TXNRCPT (tx_type))
+         (eq! (next PHASE_RLP_TXNRCPT) RLPRECEIPT_SUBPHASE_ID_STATUS_CODE)
+         (eq! (next OUTGOING_RLP_TXNRCPT) STATUS_CODE)
+         (eq! (shift PHASE_RLP_TXNRCPT 2) RLPRECEIPT_SUBPHASE_ID_CUMUL_GAS)
+         (eq! (shift OUTGOING_RLP_TXNRCPT 2) CUMULATIVE_CONSUMED_GAS)))