Skip to content

Commit 4a40f0d

Browse files
OlivierBBBOlivierBBB
authored
Prover column after TXN_DATA redesign (#796)
1 parent 565e1b3 commit 4a40f0d

File tree

9 files changed

+377
-38
lines changed

9 files changed

+377
-38
lines changed

‎rlptxn/cancun/lookups/rlptxn_into_txndata.lisp‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@
1111
txndata.USER
1212
txndata.RLP
1313
txndata.USER_TXN_NUMBER
14+
txndata.prover___USER_TXN_NUMBER_MAX
1415
(txn-data-hub-view-cfi)
1516
txndata.rlp/REQUIRES_EVM_EXECUTION
1617
txndata.rlp/IS_DEPLOYMENT
@@ -35,6 +36,7 @@
3536
1
3637
1
3738
rlptxn.USER_TXN_NUMBER
39+
rlptxn.prover___USER_TXN_NUMBER_MAX
3840
rlptxn.CODE_FRAGMENT_INDEX
3941
rlptxn.REQUIRES_EVM_EXECUTION
4042
rlptxn.IS_DEPLOYMENT

‎rlptxn/cancun/prover/prover_columns_corset.lisp‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
(module rlptxn)
2+
3+
4+
5+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
6+
;; ;;
7+
;; Constraints verification ;;
8+
;; ;;
9+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
10+
11+
12+
13+
(defcolumns
14+
( prover___USER_TXN_NUMBER_MAX :i16 )
15+
)
16+
17+
(defalias
18+
USRMAX prover___USER_TXN_NUMBER_MAX
19+
)
20+
21+
22+
23+
(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX---constancy ()
24+
(if-not-zero USER_TXN_NUMBER
25+
(will-remain-constant! USRMAX)))
26+
27+
(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX---finalization
28+
(:domain {-1}) ;; ""
29+
(eq! USRMAX USER_TXN_NUMBER))
30+
31+
32+
33+
;; TOTL|USER|SYSF|SYSI|prover

‎todo‎

Lines changed: 0 additions & 29 deletions
This file was deleted.

‎txndata/cancun/generalities/flags_perspectives.lisp‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,9 @@
77
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
88

99

10-
(defun (perspective-sum) (+ RLP
11-
HUB
12-
CMPTN))
10+
(defun (perspective-sum) (force-bin (+ RLP
11+
HUB
12+
CMPTN)))
1313

1414
(defproperty perspective-sum-constraints---it-coincides-with-txn-flag-sum (eq! (perspective-sum) (txn-flag-sum)))
1515
(defconstraint perspective-sum-constraints---it-vanishes-initially (:domain {0}) (eq! (perspective-sum) 0)) ;; ""

‎txndata/cancun/prover/prover_columns_corset.lisp‎

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
(module txndata)
2+
3+
4+
5+
(defun
6+
(block-constancy COL)
7+
(if-not-zero (- (next BLK_NUMBER) (+ 1 BLK_NUMBER))
8+
(eq! (next COL) COL)))
9+
(defun
10+
(conflation-constancy COL)
11+
(if-not-zero (perspective-sum)
12+
(eq! (next COL) COL)))
13+
(defun
14+
(transaction-constancy COL)
15+
(if-not-zero (- (next TOTL_TXN_NUMBER) (+ 1 TOTL_TXN_NUMBER))
16+
(eq! (next COL) COL)))
17+
(defun
18+
(user-transaction-constancy COL)
19+
(if-not-zero (* (next USER ) USER )
20+
(eq! (next COL ) COL )))
21+
22+
23+
24+
25+
(defcomputedcolumn ( prover___RELATIVE_USER_TXN_NUMBER :i16 :fwd )
26+
(if-eq-else BLK_NUMBER (prev BLK_NUMBER)
27+
;; BLK# equality case
28+
(* USER (+ (prev prover___RELATIVE_USER_TXN_NUMBER) (- USER_TXN_NUMBER (prev USER_TXN_NUMBER))))
29+
;; BLK# change case
30+
0
31+
))
32+
33+
(defcomputedcolumn ( prover___IS_LAST_USER_TXN_OF_BLOCK :binary@prove :bwd )
34+
(if-eq-else (next TOTL_TXN_NUMBER) TOTL_TXN_NUMBER
35+
;; TOTL transaction number equality case
36+
(next prover___IS_LAST_USER_TXN_OF_BLOCK)
37+
;; BLK# change case
38+
(* (next SYSF) USER)
39+
))
40+
41+
(defalias
42+
RELUSR prover___RELATIVE_USER_TXN_NUMBER
43+
LSTUSR prover___IS_LAST_USER_TXN_OF_BLOCK
44+
)
45+
46+
47+
48+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
49+
;; ;;
50+
;; Property verification ;;
51+
;; ;;
52+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
53+
54+
55+
56+
(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---const (transaction-constancy RELUSR))
57+
(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---vanish (if-zero (perspective-sum) (vanishes! RELUSR)))
58+
(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---transition (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) (vanishes! RELUSR)))
59+
(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---increment (if-not-zero (- (next BLK_NUMBER) (+ BLK_NUMBER 1))
60+
(eq! (next RELUSR)
61+
(* (next USER) (+ RELUSR (- (next USER_TXN_NUMBER) USER_TXN_NUMBER))))))
62+
63+
(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---const (transaction-constancy LSTUSR) )
64+
(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---vanish (if-zero USER (vanishes! LSTUSR)) )
65+
(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---last (if-not-zero (- TOTL_TXN_NUMBER (prev TOTL_TXN_NUMBER))
66+
(eq! (prev LSTUSR)
67+
(* (prev USER) SYSF)))
68+
)
69+
70+
71+
72+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
73+
;; ;;
74+
;; Constraints verification ;;
75+
;; ;;
76+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
77+
78+
79+
80+
(defcolumns
81+
( prover___RELATIVE_USER_TXN_NUMBER_MAX :i16 )
82+
( prover___USER_TXN_NUMBER_MAX :i16 )
83+
)
84+
85+
(defalias
86+
RELMAX prover___RELATIVE_USER_TXN_NUMBER_MAX
87+
USRMAX prover___USER_TXN_NUMBER_MAX
88+
)
89+
90+
91+
92+
(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---const () (user-transaction-constancy RELMAX))
93+
(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---zero () (if-zero (perspective-sum)
94+
(vanishes! RELMAX)))
95+
(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---setting () (if-not-zero (* (- 1 (prev SYSF)) SYSF)
96+
(eq! (prev RELMAX) (prev RELUSR))))
97+
98+
(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX ()
99+
(begin
100+
(conflation-constancy USRMAX)
101+
(if-zero (perspective-sum)
102+
(vanishes! USRMAX))
103+
))
104+
105+
(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX---finalization
106+
(:domain {-1}) ;; ""
107+
(eq! USRMAX USER_TXN_NUMBER))
108+
109+
110+
111+
;; TOTL|USER|SYSF|SYSI|prover

‎txndata/osaka/generalities/flags_perspectives.lisp‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,9 @@
77
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
88

99

10-
(defun (perspective-sum) (+ RLP
11-
HUB
12-
CMPTN))
10+
(defun (perspective-sum) (force-bin (+ RLP
11+
HUB
12+
CMPTN)))
1313

1414
(defproperty perspective-sum-constraints---it-coincides-with-txn-flag-sum (eq! (perspective-sum) (txn-flag-sum)))
1515
(defconstraint perspective-sum-constraints---it-vanishes-initially (:domain {0}) (eq! (perspective-sum) 0)) ;; ""

‎txndata/osaka/prover/prover_columns_corset.lisp‎

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
(module txndata)
2+
3+
4+
5+
(defun
6+
(block-constancy COL)
7+
(if-not-zero (- (next BLK_NUMBER) (+ 1 BLK_NUMBER))
8+
(eq! (next COL) COL)))
9+
(defun
10+
(conflation-constancy COL)
11+
(if-not-zero (perspective-sum)
12+
(eq! (next COL) COL)))
13+
(defun
14+
(transaction-constancy COL)
15+
(if-not-zero (- (next TOTL_TXN_NUMBER) (+ 1 TOTL_TXN_NUMBER))
16+
(eq! (next COL) COL)))
17+
(defun
18+
(user-transaction-constancy COL)
19+
(if-not-zero (* (next USER ) USER )
20+
(eq! (next COL ) COL )))
21+
22+
23+
24+
25+
(defcomputedcolumn ( prover___RELATIVE_USER_TXN_NUMBER :i16 :fwd )
26+
(if-eq-else BLK_NUMBER (prev BLK_NUMBER)
27+
;; BLK# equality case
28+
(* USER (+ (prev prover___RELATIVE_USER_TXN_NUMBER) (- USER_TXN_NUMBER (prev USER_TXN_NUMBER))))
29+
;; BLK# change case
30+
0
31+
))
32+
33+
(defcomputedcolumn ( prover___IS_LAST_USER_TXN_OF_BLOCK :binary@prove :bwd )
34+
(if-eq-else (next TOTL_TXN_NUMBER) TOTL_TXN_NUMBER
35+
;; TOTL transaction number equality case
36+
(next prover___IS_LAST_USER_TXN_OF_BLOCK)
37+
;; BLK# change case
38+
(* (next SYSF) USER)
39+
))
40+
41+
(defalias
42+
RELUSR prover___RELATIVE_USER_TXN_NUMBER
43+
LSTUSR prover___IS_LAST_USER_TXN_OF_BLOCK
44+
)
45+
46+
47+
48+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
49+
;; ;;
50+
;; Property verification ;;
51+
;; ;;
52+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
53+
54+
55+
56+
(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---const (transaction-constancy RELUSR))
57+
(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---vanish (if-zero (perspective-sum) (vanishes! RELUSR)))
58+
(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---transition (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) (vanishes! RELUSR)))
59+
(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---increment (if-not-zero (- (next BLK_NUMBER) (+ BLK_NUMBER 1))
60+
(eq! (next RELUSR)
61+
(* (next USER) (+ RELUSR (- (next USER_TXN_NUMBER) USER_TXN_NUMBER))))))
62+
63+
(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---const (transaction-constancy LSTUSR) )
64+
(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---vanish (if-zero USER (vanishes! LSTUSR)) )
65+
(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---last (if-not-zero (- TOTL_TXN_NUMBER (prev TOTL_TXN_NUMBER))
66+
(eq! (prev LSTUSR)
67+
(* (prev USER) SYSF)))
68+
)
69+
70+
71+
72+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
73+
;; ;;
74+
;; Constraints verification ;;
75+
;; ;;
76+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
77+
78+
79+
80+
(defcolumns
81+
( prover___RELATIVE_USER_TXN_NUMBER_MAX :i16 )
82+
( prover___USER_TXN_NUMBER_MAX :i16 )
83+
)
84+
85+
(defalias
86+
RELMAX prover___RELATIVE_USER_TXN_NUMBER_MAX
87+
USRMAX prover___USER_TXN_NUMBER_MAX
88+
)
89+
90+
91+
92+
(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---const () (user-transaction-constancy RELMAX))
93+
(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---zero () (if-zero (perspective-sum)
94+
(vanishes! RELMAX)))
95+
(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---setting () (if-not-zero (* (- 1 (prev SYSF)) SYSF)
96+
(eq! (prev RELMAX) (prev RELUSR))))
97+
98+
(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX ()
99+
(begin
100+
(conflation-constancy USRMAX)
101+
(if-zero (perspective-sum)
102+
(vanishes! USRMAX))
103+
))
104+
105+
(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX---finalization
106+
(:domain {-1}) ;; ""
107+
(eq! USRMAX USER_TXN_NUMBER))
108+
109+
110+
111+
;; TOTL|USER|SYSF|SYSI|prover

‎txndata/prague/generalities/flags_perspectives.lisp‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,9 @@
77
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
88

99

10-
(defun (perspective-sum) (+ RLP
11-
HUB
12-
CMPTN))
10+
(defun (perspective-sum) (force-bin (+ RLP
11+
HUB
12+
CMPTN)))
1313

1414
(defproperty perspective-sum-constraints---it-coincides-with-txn-flag-sum (eq! (perspective-sum) (txn-flag-sum)))
1515
(defconstraint perspective-sum-constraints---it-vanishes-initially (:domain {0}) (eq! (perspective-sum) 0)) ;; ""

0 commit comments

Comments
 (0)