fix: plug txnData constraints (#47)

Consensys · Dec 18, 2023 · 0276025 · 0276025
1 parent 405afa4
commit 0276025
Show file tree

Hide file tree

Showing 5 changed files with 31 additions and 31 deletions.
diff --git a/Makefile b/Makefile
@@ -75,6 +75,10 @@ TABLES := $(wildcard lookup_tables/tables/*lisp)
 
 TRM := trm/columns.lisp trm/constraints.lisp
 
+TXN_DATA := txn_data/columns.lisp txn_data/constraints.lisp \
+	txn_data/lookups/into_rlp_addr.lisp txn_data/lookups/into_rlp_txn.lisp txn_data/lookups/into_rlp_txrcpt.lisp txn_data/lookups/into_rom_lex.lisp txn_data/lookups/into_wcp.lisp \
+	# txn_data/lookups/from_hub.lisp txn_data/lookups/into_btc.lisp 
+
 WCP := wcp/columns.lisp wcp/constraints.lisp \
 	   # wcp/hub_into_wcp.lisp \
 

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/logInfo/lookups/loginfo-to-rlprcpt.lisp b/logInfo/lookups/loginfo-to-rlprcpt.lisp
@@ -1,12 +1,3 @@
-(defpurefun (subphaseId-rlp-txrcpt)
-  (+ (reduce +
-             (for i [1 : 5] (* i [rlpTxRcpt.PHASE i])))
-     (* 6 rlpTxRcpt.IS_PREFIX)
-     (* 12 rlpTxRcpt.IS_TOPIC)
-     (* 24 rlpTxRcpt.IS_DATA)
-     (* 48 rlpTxRcpt.DEPTH_1)
-     (* 96 rlpTxRcpt.IS_TOPIC rlpTxRcpt.INDEX_LOCAL))) ;;TODO, doublon, already define in txnData->rlpRcpt lookup
-
 (deflookup 
   logInfo-into-rlpTxnRcpt
   ;reference columns

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
@@ -33,16 +33,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,7 +264,11 @@
          (if-zero TYPE2
                   (vanishes! (shift OUTGOING_HI 6)))))
 
-(defconstraint verticalization (:guard (remained-constant! ABS))
+;; 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)))
@@ -346,7 +351,7 @@
          ;;  (= (shift WCP_RES_LO     6) ???) ;; unknown
          ))
 
-(defconstraint comparisons (:guard (remained-constant! ABS))
+(defconstraint comparisons (:guard (first-row-trigger))
   (begin (sufficient_balance)
          (sufficient_gas_limit)
          (upper_limit_for_refunds)
@@ -361,7 +366,7 @@
 ;;    2.11 Gas and gas price constraints    ;;
 ;;                                          ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(defconstraint gas_and_gas_price (:guard (remained-constant! ABS))
+(defconstraint gas_and_gas_price (:guard (first-row-trigger))
   (begin  ;; constraining INIT_GAS
          (= IGAS
             (- (gas_limit) (shift WCP_ARG_TWO_LO 1)))
@@ -382,7 +387,7 @@
 ;;    2.11 Verticalisation for RlpTxnRcpt    ;;
 ;;                                           ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(defconstraint verticalisation-rlp-txn-rcpt (:guard (remained-constant! ABS))
+(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)