From 6249a0e5c13afb08eedaec2478d81409565d5997 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Wed, 8 Oct 2025 23:14:45 +0200 Subject: [PATCH 1/9] feat: prover column constraints for TXN_DATA --- txndata/cancun/prover_columns.lisp | 76 +++++++++++++++++++ .../generalities/flags_perspectives.lisp | 6 +- 2 files changed, 79 insertions(+), 3 deletions(-) create mode 100644 txndata/cancun/prover_columns.lisp diff --git a/txndata/cancun/prover_columns.lisp b/txndata/cancun/prover_columns.lisp new file mode 100644 index 000000000..dfb2ebe1a --- /dev/null +++ b/txndata/cancun/prover_columns.lisp @@ -0,0 +1,76 @@ +(module txndata) + + +(defcolumns + ( prover___REL_USER_TXN_NUMBER :i16 ) + ( prover___REL_USER_TXN_NUMBER_MAX :i16 ) + ( prover___IS_LAST_USER_TXN_OF_BLOCK :i16 ) + ( prover___USER_TXN_NUMBER_MAX :i16 ) + ) + +(defalias + prv_RUSR prover___REL_USER_TXN_NUMBER + prv_RMAX prover___REL_USER_TXN_NUMBER_MAX + prv_LAST prover___IS_LAST_USER_TXN_OF_BLOCK + prv_UMAX prover___USER_TXN_NUMBER_MAX + ) + +(defun + (block-constancy COL) + (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) + (eq! (next COL) COL))) + +(defun + (conflation-constancy COL) + (if-not-zero (perspective-sum) + (eq! (next COL) COL))) + +(defun + (transaction-constancy COL) + (if-not-zero (- (next TOTL_TXN_NUMBER) TOTL_TXN_NUMBER) + (eq! (next COL) COL))) + + +(defconstraint prover-column-constraints---RUSR () + (begin + (block-constancy prv_RUSR) + (if-zero (perspective-sum) + (vanishes! prv_RUSR)) + (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) + (vanishes! prv_RUSR)) + (if-not-zero (- (next BLK_NUMBER) (+ BLK_NUMBER 1)) + (eq! (next prv_RUSR) + (+ prv_RUSR + (- (next USER_TXN_NUMBER) + USER_TXN_NUMBER)))) + )) + +(defconstraint prover-column-constraints---RMAX () + (begin + (block-constancy prv_RMAX) + (if-zero (perspective-sum) + (vanishes! prv_RMAX)) + (if-not-zero SYSF + (eq! prv_RMAX prv_RUSR)) + )) + +(defconstraint prover-column-constraints---LAST () + (begin + (transaction-constancy prv_LAST) + (if-zero USER + (vanishes! prv_LAST)) + (if-not-zero (- TOTL_TXN_NUMBER (next TOTL_TXN_NUMBER)) + (eq! (prev prv_LAST) + (* (prev USER) + SYSF))) + )) + +(defconstraint prover-column-constraints---UMAX () + (begin + (conflation-constancy prv_UMAX) + (if-zero (perspective-sum) + (vanishes! prv_UMAX)) + )) + +(defconstraint prover-column-constraints---UMAX---finalization (:domain {-1}) ;; "" + (eq! prv_UMAX USER_TXN_NUMBER)) diff --git a/txndata/prague/generalities/flags_perspectives.lisp b/txndata/prague/generalities/flags_perspectives.lisp index 9442fbfc6..428b8507a 100644 --- a/txndata/prague/generalities/flags_perspectives.lisp +++ b/txndata/prague/generalities/flags_perspectives.lisp @@ -7,9 +7,9 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun (perspective-sum) (+ RLP - HUB - CMPTN)) +(defun (perspective-sum) (force-bin (+ RLP + HUB + CMPTN))) (defproperty perspective-sum-constraints---it-coincides-with-txn-flag-sum (eq! (perspective-sum) (txn-flag-sum))) (defconstraint perspective-sum-constraints---it-vanishes-initially (:domain {0}) (eq! (perspective-sum) 0)) ;; "" From 209bbcdf0d832005650bafb2faeb15dd41a846d4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 10 Oct 2025 03:38:59 +0200 Subject: [PATCH 2/9] feat: prover TXN_DATA columns (Cancun) --- .../prover_columns.lispX} | 0 .../cancun/prover/prover_columns_corset.lisp | 111 ++++++++++++++++++ 2 files changed, 111 insertions(+) rename txndata/cancun/{prover_columns.lisp => prover/prover_columns.lispX} (100%) create mode 100644 txndata/cancun/prover/prover_columns_corset.lisp diff --git a/txndata/cancun/prover_columns.lisp b/txndata/cancun/prover/prover_columns.lispX similarity index 100% rename from txndata/cancun/prover_columns.lisp rename to txndata/cancun/prover/prover_columns.lispX diff --git a/txndata/cancun/prover/prover_columns_corset.lisp b/txndata/cancun/prover/prover_columns_corset.lisp new file mode 100644 index 000000000..b78fc2774 --- /dev/null +++ b/txndata/cancun/prover/prover_columns_corset.lisp @@ -0,0 +1,111 @@ +(module txndata) + + + +(defun + (block-constancy COL) + (if-not-zero (- (next BLK_NUMBER) (+ 1 BLK_NUMBER)) + (eq! (next COL) COL))) +(defun + (conflation-constancy COL) + (if-not-zero (perspective-sum) + (eq! (next COL) COL))) +(defun + (transaction-constancy COL) + (if-not-zero (- (next TOTL_TXN_NUMBER) (+ 1 TOTL_TXN_NUMBER)) + (eq! (next COL) COL))) +(defun + (user-transaction-constancy COL) + (if-not-zero (* (next USER ) USER ) + (eq! (next COL ) COL ))) + + + + +(defcomputedcolumn ( prover___RELATIVE_USER_TXN_NUMBER :i16 :fwd ) + (if-eq-else BLK_NUMBER (prev BLK_NUMBER) + ;; BLK# equality case + (* USER (+ (prev prover___RELATIVE_USER_TXN_NUMBER) (- USER_TXN_NUMBER (prev USER_TXN_NUMBER)))) + ;; BLK# change case + 0 + )) + +(defcomputedcolumn ( prover___IS_LAST_USER_TXN_OF_BLOCK :binary@prove :bwd ) + (if-eq-else (next TOTL_TXN_NUMBER) TOTL_TXN_NUMBER + ;; TOTL transaction number equality case + (next prover___IS_LAST_USER_TXN_OF_BLOCK) + ;; BLK# change case + (* (next SYSF) USER) + )) + +(defalias + RELUSR prover___RELATIVE_USER_TXN_NUMBER + LSTUSR prover___IS_LAST_USER_TXN_OF_BLOCK + ) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Property verification ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + + +(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---const (transaction-constancy RELUSR)) +(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---vanish (if-zero (perspective-sum) (vanishes! RELUSR))) +(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---transition (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) (vanishes! RELUSR))) +(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---increment (if-not-zero (- (next BLK_NUMBER) (+ BLK_NUMBER 1)) + (eq! (next RELUSR) + (* (next USER) (+ RELUSR (- (next USER_TXN_NUMBER) USER_TXN_NUMBER)))))) + +(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---const (transaction-constancy LSTUSR) ) +(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---vanish (if-zero USER (vanishes! LSTUSR)) ) +(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---last (if-not-zero (- TOTL_TXN_NUMBER (prev TOTL_TXN_NUMBER)) + (eq! (prev LSTUSR) + (* (prev USER) SYSF))) + ) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Constraints verification ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + + +(defcolumns + ( prover___RELATIVE_USER_TXN_NUMBER_MAX :i16 ) + ( prover___USER_TXN_NUMBER_MAX :i16 ) + ) + +(defalias + RELMAX prover___RELATIVE_USER_TXN_NUMBER_MAX + USRMAX prover___USER_TXN_NUMBER_MAX + ) + + + +(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---const () (user-transaction-constancy RELMAX)) +(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---zero () (if-zero (perspective-sum) + (vanishes! RELMAX))) +(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---setting () (if-not-zero (* (- 1 (prev SYSF)) SYSF) + (eq! (prev RELMAX) (prev RELUSR)))) + +(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX () + (begin + (conflation-constancy USRMAX) + (if-zero (perspective-sum) + (vanishes! USRMAX)) + )) + +(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX---finalization + (:domain {-1}) ;; "" + (eq! USRMAX USER_TXN_NUMBER)) + + + +;; TOTL|USER|SYSF|SYSI|prover From 7f57e02baed3376dbe2a04b79c8a3da6d7ce992c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 10 Oct 2025 03:39:12 +0200 Subject: [PATCH 3/9] feat: same for Prague/Osaka --- txndata/osaka/prover/prover_columns.lispX | 76 ++++++++++++ .../osaka/prover/prover_columns_corset.lisp | 111 ++++++++++++++++++ txndata/prague/prover/prover_columns.lispX | 76 ++++++++++++ .../prague/prover/prover_columns_corset.lisp | 111 ++++++++++++++++++ 4 files changed, 374 insertions(+) create mode 100644 txndata/osaka/prover/prover_columns.lispX create mode 100644 txndata/osaka/prover/prover_columns_corset.lisp create mode 100644 txndata/prague/prover/prover_columns.lispX create mode 100644 txndata/prague/prover/prover_columns_corset.lisp diff --git a/txndata/osaka/prover/prover_columns.lispX b/txndata/osaka/prover/prover_columns.lispX new file mode 100644 index 000000000..dfb2ebe1a --- /dev/null +++ b/txndata/osaka/prover/prover_columns.lispX @@ -0,0 +1,76 @@ +(module txndata) + + +(defcolumns + ( prover___REL_USER_TXN_NUMBER :i16 ) + ( prover___REL_USER_TXN_NUMBER_MAX :i16 ) + ( prover___IS_LAST_USER_TXN_OF_BLOCK :i16 ) + ( prover___USER_TXN_NUMBER_MAX :i16 ) + ) + +(defalias + prv_RUSR prover___REL_USER_TXN_NUMBER + prv_RMAX prover___REL_USER_TXN_NUMBER_MAX + prv_LAST prover___IS_LAST_USER_TXN_OF_BLOCK + prv_UMAX prover___USER_TXN_NUMBER_MAX + ) + +(defun + (block-constancy COL) + (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) + (eq! (next COL) COL))) + +(defun + (conflation-constancy COL) + (if-not-zero (perspective-sum) + (eq! (next COL) COL))) + +(defun + (transaction-constancy COL) + (if-not-zero (- (next TOTL_TXN_NUMBER) TOTL_TXN_NUMBER) + (eq! (next COL) COL))) + + +(defconstraint prover-column-constraints---RUSR () + (begin + (block-constancy prv_RUSR) + (if-zero (perspective-sum) + (vanishes! prv_RUSR)) + (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) + (vanishes! prv_RUSR)) + (if-not-zero (- (next BLK_NUMBER) (+ BLK_NUMBER 1)) + (eq! (next prv_RUSR) + (+ prv_RUSR + (- (next USER_TXN_NUMBER) + USER_TXN_NUMBER)))) + )) + +(defconstraint prover-column-constraints---RMAX () + (begin + (block-constancy prv_RMAX) + (if-zero (perspective-sum) + (vanishes! prv_RMAX)) + (if-not-zero SYSF + (eq! prv_RMAX prv_RUSR)) + )) + +(defconstraint prover-column-constraints---LAST () + (begin + (transaction-constancy prv_LAST) + (if-zero USER + (vanishes! prv_LAST)) + (if-not-zero (- TOTL_TXN_NUMBER (next TOTL_TXN_NUMBER)) + (eq! (prev prv_LAST) + (* (prev USER) + SYSF))) + )) + +(defconstraint prover-column-constraints---UMAX () + (begin + (conflation-constancy prv_UMAX) + (if-zero (perspective-sum) + (vanishes! prv_UMAX)) + )) + +(defconstraint prover-column-constraints---UMAX---finalization (:domain {-1}) ;; "" + (eq! prv_UMAX USER_TXN_NUMBER)) diff --git a/txndata/osaka/prover/prover_columns_corset.lisp b/txndata/osaka/prover/prover_columns_corset.lisp new file mode 100644 index 000000000..b78fc2774 --- /dev/null +++ b/txndata/osaka/prover/prover_columns_corset.lisp @@ -0,0 +1,111 @@ +(module txndata) + + + +(defun + (block-constancy COL) + (if-not-zero (- (next BLK_NUMBER) (+ 1 BLK_NUMBER)) + (eq! (next COL) COL))) +(defun + (conflation-constancy COL) + (if-not-zero (perspective-sum) + (eq! (next COL) COL))) +(defun + (transaction-constancy COL) + (if-not-zero (- (next TOTL_TXN_NUMBER) (+ 1 TOTL_TXN_NUMBER)) + (eq! (next COL) COL))) +(defun + (user-transaction-constancy COL) + (if-not-zero (* (next USER ) USER ) + (eq! (next COL ) COL ))) + + + + +(defcomputedcolumn ( prover___RELATIVE_USER_TXN_NUMBER :i16 :fwd ) + (if-eq-else BLK_NUMBER (prev BLK_NUMBER) + ;; BLK# equality case + (* USER (+ (prev prover___RELATIVE_USER_TXN_NUMBER) (- USER_TXN_NUMBER (prev USER_TXN_NUMBER)))) + ;; BLK# change case + 0 + )) + +(defcomputedcolumn ( prover___IS_LAST_USER_TXN_OF_BLOCK :binary@prove :bwd ) + (if-eq-else (next TOTL_TXN_NUMBER) TOTL_TXN_NUMBER + ;; TOTL transaction number equality case + (next prover___IS_LAST_USER_TXN_OF_BLOCK) + ;; BLK# change case + (* (next SYSF) USER) + )) + +(defalias + RELUSR prover___RELATIVE_USER_TXN_NUMBER + LSTUSR prover___IS_LAST_USER_TXN_OF_BLOCK + ) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Property verification ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + + +(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---const (transaction-constancy RELUSR)) +(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---vanish (if-zero (perspective-sum) (vanishes! RELUSR))) +(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---transition (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) (vanishes! RELUSR))) +(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---increment (if-not-zero (- (next BLK_NUMBER) (+ BLK_NUMBER 1)) + (eq! (next RELUSR) + (* (next USER) (+ RELUSR (- (next USER_TXN_NUMBER) USER_TXN_NUMBER)))))) + +(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---const (transaction-constancy LSTUSR) ) +(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---vanish (if-zero USER (vanishes! LSTUSR)) ) +(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---last (if-not-zero (- TOTL_TXN_NUMBER (prev TOTL_TXN_NUMBER)) + (eq! (prev LSTUSR) + (* (prev USER) SYSF))) + ) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Constraints verification ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + + +(defcolumns + ( prover___RELATIVE_USER_TXN_NUMBER_MAX :i16 ) + ( prover___USER_TXN_NUMBER_MAX :i16 ) + ) + +(defalias + RELMAX prover___RELATIVE_USER_TXN_NUMBER_MAX + USRMAX prover___USER_TXN_NUMBER_MAX + ) + + + +(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---const () (user-transaction-constancy RELMAX)) +(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---zero () (if-zero (perspective-sum) + (vanishes! RELMAX))) +(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---setting () (if-not-zero (* (- 1 (prev SYSF)) SYSF) + (eq! (prev RELMAX) (prev RELUSR)))) + +(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX () + (begin + (conflation-constancy USRMAX) + (if-zero (perspective-sum) + (vanishes! USRMAX)) + )) + +(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX---finalization + (:domain {-1}) ;; "" + (eq! USRMAX USER_TXN_NUMBER)) + + + +;; TOTL|USER|SYSF|SYSI|prover diff --git a/txndata/prague/prover/prover_columns.lispX b/txndata/prague/prover/prover_columns.lispX new file mode 100644 index 000000000..dfb2ebe1a --- /dev/null +++ b/txndata/prague/prover/prover_columns.lispX @@ -0,0 +1,76 @@ +(module txndata) + + +(defcolumns + ( prover___REL_USER_TXN_NUMBER :i16 ) + ( prover___REL_USER_TXN_NUMBER_MAX :i16 ) + ( prover___IS_LAST_USER_TXN_OF_BLOCK :i16 ) + ( prover___USER_TXN_NUMBER_MAX :i16 ) + ) + +(defalias + prv_RUSR prover___REL_USER_TXN_NUMBER + prv_RMAX prover___REL_USER_TXN_NUMBER_MAX + prv_LAST prover___IS_LAST_USER_TXN_OF_BLOCK + prv_UMAX prover___USER_TXN_NUMBER_MAX + ) + +(defun + (block-constancy COL) + (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) + (eq! (next COL) COL))) + +(defun + (conflation-constancy COL) + (if-not-zero (perspective-sum) + (eq! (next COL) COL))) + +(defun + (transaction-constancy COL) + (if-not-zero (- (next TOTL_TXN_NUMBER) TOTL_TXN_NUMBER) + (eq! (next COL) COL))) + + +(defconstraint prover-column-constraints---RUSR () + (begin + (block-constancy prv_RUSR) + (if-zero (perspective-sum) + (vanishes! prv_RUSR)) + (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) + (vanishes! prv_RUSR)) + (if-not-zero (- (next BLK_NUMBER) (+ BLK_NUMBER 1)) + (eq! (next prv_RUSR) + (+ prv_RUSR + (- (next USER_TXN_NUMBER) + USER_TXN_NUMBER)))) + )) + +(defconstraint prover-column-constraints---RMAX () + (begin + (block-constancy prv_RMAX) + (if-zero (perspective-sum) + (vanishes! prv_RMAX)) + (if-not-zero SYSF + (eq! prv_RMAX prv_RUSR)) + )) + +(defconstraint prover-column-constraints---LAST () + (begin + (transaction-constancy prv_LAST) + (if-zero USER + (vanishes! prv_LAST)) + (if-not-zero (- TOTL_TXN_NUMBER (next TOTL_TXN_NUMBER)) + (eq! (prev prv_LAST) + (* (prev USER) + SYSF))) + )) + +(defconstraint prover-column-constraints---UMAX () + (begin + (conflation-constancy prv_UMAX) + (if-zero (perspective-sum) + (vanishes! prv_UMAX)) + )) + +(defconstraint prover-column-constraints---UMAX---finalization (:domain {-1}) ;; "" + (eq! prv_UMAX USER_TXN_NUMBER)) diff --git a/txndata/prague/prover/prover_columns_corset.lisp b/txndata/prague/prover/prover_columns_corset.lisp new file mode 100644 index 000000000..b78fc2774 --- /dev/null +++ b/txndata/prague/prover/prover_columns_corset.lisp @@ -0,0 +1,111 @@ +(module txndata) + + + +(defun + (block-constancy COL) + (if-not-zero (- (next BLK_NUMBER) (+ 1 BLK_NUMBER)) + (eq! (next COL) COL))) +(defun + (conflation-constancy COL) + (if-not-zero (perspective-sum) + (eq! (next COL) COL))) +(defun + (transaction-constancy COL) + (if-not-zero (- (next TOTL_TXN_NUMBER) (+ 1 TOTL_TXN_NUMBER)) + (eq! (next COL) COL))) +(defun + (user-transaction-constancy COL) + (if-not-zero (* (next USER ) USER ) + (eq! (next COL ) COL ))) + + + + +(defcomputedcolumn ( prover___RELATIVE_USER_TXN_NUMBER :i16 :fwd ) + (if-eq-else BLK_NUMBER (prev BLK_NUMBER) + ;; BLK# equality case + (* USER (+ (prev prover___RELATIVE_USER_TXN_NUMBER) (- USER_TXN_NUMBER (prev USER_TXN_NUMBER)))) + ;; BLK# change case + 0 + )) + +(defcomputedcolumn ( prover___IS_LAST_USER_TXN_OF_BLOCK :binary@prove :bwd ) + (if-eq-else (next TOTL_TXN_NUMBER) TOTL_TXN_NUMBER + ;; TOTL transaction number equality case + (next prover___IS_LAST_USER_TXN_OF_BLOCK) + ;; BLK# change case + (* (next SYSF) USER) + )) + +(defalias + RELUSR prover___RELATIVE_USER_TXN_NUMBER + LSTUSR prover___IS_LAST_USER_TXN_OF_BLOCK + ) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Property verification ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + + +(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---const (transaction-constancy RELUSR)) +(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---vanish (if-zero (perspective-sum) (vanishes! RELUSR))) +(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---transition (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) (vanishes! RELUSR))) +(defproperty prover-column-constraints---RELATIVE_USER_TXN_NUMBER---increment (if-not-zero (- (next BLK_NUMBER) (+ BLK_NUMBER 1)) + (eq! (next RELUSR) + (* (next USER) (+ RELUSR (- (next USER_TXN_NUMBER) USER_TXN_NUMBER)))))) + +(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---const (transaction-constancy LSTUSR) ) +(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---vanish (if-zero USER (vanishes! LSTUSR)) ) +(defproperty prover-column-constraints---IS_LAST_USER_TXN_OF_BLOCK---last (if-not-zero (- TOTL_TXN_NUMBER (prev TOTL_TXN_NUMBER)) + (eq! (prev LSTUSR) + (* (prev USER) SYSF))) + ) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Constraints verification ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + + +(defcolumns + ( prover___RELATIVE_USER_TXN_NUMBER_MAX :i16 ) + ( prover___USER_TXN_NUMBER_MAX :i16 ) + ) + +(defalias + RELMAX prover___RELATIVE_USER_TXN_NUMBER_MAX + USRMAX prover___USER_TXN_NUMBER_MAX + ) + + + +(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---const () (user-transaction-constancy RELMAX)) +(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---zero () (if-zero (perspective-sum) + (vanishes! RELMAX))) +(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---setting () (if-not-zero (* (- 1 (prev SYSF)) SYSF) + (eq! (prev RELMAX) (prev RELUSR)))) + +(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX () + (begin + (conflation-constancy USRMAX) + (if-zero (perspective-sum) + (vanishes! USRMAX)) + )) + +(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX---finalization + (:domain {-1}) ;; "" + (eq! USRMAX USER_TXN_NUMBER)) + + + +;; TOTL|USER|SYSF|SYSI|prover From 2427a9a49a358faf72d5fe1297e070a931c436c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 10 Oct 2025 13:37:01 +0200 Subject: [PATCH 4/9] feat: new USER_TXN_NUMBER_MAX column in RLP_TXN --- .../cancun/prover/prover_columns_corset.lisp | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 rlptxn/cancun/prover/prover_columns_corset.lisp diff --git a/rlptxn/cancun/prover/prover_columns_corset.lisp b/rlptxn/cancun/prover/prover_columns_corset.lisp new file mode 100644 index 000000000..faf0d4621 --- /dev/null +++ b/rlptxn/cancun/prover/prover_columns_corset.lisp @@ -0,0 +1,33 @@ +(module rlptxn) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Constraints verification ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + + +(defcolumns + ( prover___USER_TXN_NUMBER_MAX :i16 ) + ) + +(defalias + USRMAX prover___USER_TXN_NUMBER_MAX + ) + + + +(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX---constancy () + (if-not-zero USER_TXN_NUMBER + (will-remain-constant! USRMAX))) + +(defconstraint prover-column-constraints---USER_TXN_NUMBER_MAX---finalization + (:domain {-1}) ;; "" + (eq! USRMAX USER_TXN_NUMBER)) + + + +;; TOTL|USER|SYSF|SYSI|prover From eb23072f6897dbffc0f60367c58b99dec34fe32b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 10 Oct 2025 13:37:35 +0200 Subject: [PATCH 5/9] feat: include the USER_TXN_MAX columns into RLP_TXN -> TXN_DATA lookup --- rlptxn/cancun/lookups/rlptxn_into_txndata.lisp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/rlptxn/cancun/lookups/rlptxn_into_txndata.lisp b/rlptxn/cancun/lookups/rlptxn_into_txndata.lisp index 66bd093d9..38bb9fae8 100644 --- a/rlptxn/cancun/lookups/rlptxn_into_txndata.lisp +++ b/rlptxn/cancun/lookups/rlptxn_into_txndata.lisp @@ -11,6 +11,7 @@ txndata.USER txndata.RLP txndata.USER_TXN_NUMBER + txndata.prover___USER_TXN_NUMBER_MAX (txn-data-hub-view-cfi) txndata.rlp/REQUIRES_EVM_EXECUTION txndata.rlp/IS_DEPLOYMENT @@ -35,6 +36,7 @@ 1 1 rlptxn.USER_TXN_NUMBER + rlptxn.prover___USER_TXN_NUMBER_MAX rlptxn.CODE_FRAGMENT_INDEX rlptxn.REQUIRES_EVM_EXECUTION rlptxn.IS_DEPLOYMENT From b6ab232181d2ddf081b1a9434d3a6d54862e2d01 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 10 Oct 2025 13:37:44 +0200 Subject: [PATCH 6/9] cleaning --- txndata/cancun/prover/prover_columns.lispX | 76 ---------------------- 1 file changed, 76 deletions(-) delete mode 100644 txndata/cancun/prover/prover_columns.lispX diff --git a/txndata/cancun/prover/prover_columns.lispX b/txndata/cancun/prover/prover_columns.lispX deleted file mode 100644 index dfb2ebe1a..000000000 --- a/txndata/cancun/prover/prover_columns.lispX +++ /dev/null @@ -1,76 +0,0 @@ -(module txndata) - - -(defcolumns - ( prover___REL_USER_TXN_NUMBER :i16 ) - ( prover___REL_USER_TXN_NUMBER_MAX :i16 ) - ( prover___IS_LAST_USER_TXN_OF_BLOCK :i16 ) - ( prover___USER_TXN_NUMBER_MAX :i16 ) - ) - -(defalias - prv_RUSR prover___REL_USER_TXN_NUMBER - prv_RMAX prover___REL_USER_TXN_NUMBER_MAX - prv_LAST prover___IS_LAST_USER_TXN_OF_BLOCK - prv_UMAX prover___USER_TXN_NUMBER_MAX - ) - -(defun - (block-constancy COL) - (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) - (eq! (next COL) COL))) - -(defun - (conflation-constancy COL) - (if-not-zero (perspective-sum) - (eq! (next COL) COL))) - -(defun - (transaction-constancy COL) - (if-not-zero (- (next TOTL_TXN_NUMBER) TOTL_TXN_NUMBER) - (eq! (next COL) COL))) - - -(defconstraint prover-column-constraints---RUSR () - (begin - (block-constancy prv_RUSR) - (if-zero (perspective-sum) - (vanishes! prv_RUSR)) - (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) - (vanishes! prv_RUSR)) - (if-not-zero (- (next BLK_NUMBER) (+ BLK_NUMBER 1)) - (eq! (next prv_RUSR) - (+ prv_RUSR - (- (next USER_TXN_NUMBER) - USER_TXN_NUMBER)))) - )) - -(defconstraint prover-column-constraints---RMAX () - (begin - (block-constancy prv_RMAX) - (if-zero (perspective-sum) - (vanishes! prv_RMAX)) - (if-not-zero SYSF - (eq! prv_RMAX prv_RUSR)) - )) - -(defconstraint prover-column-constraints---LAST () - (begin - (transaction-constancy prv_LAST) - (if-zero USER - (vanishes! prv_LAST)) - (if-not-zero (- TOTL_TXN_NUMBER (next TOTL_TXN_NUMBER)) - (eq! (prev prv_LAST) - (* (prev USER) - SYSF))) - )) - -(defconstraint prover-column-constraints---UMAX () - (begin - (conflation-constancy prv_UMAX) - (if-zero (perspective-sum) - (vanishes! prv_UMAX)) - )) - -(defconstraint prover-column-constraints---UMAX---finalization (:domain {-1}) ;; "" - (eq! prv_UMAX USER_TXN_NUMBER)) From e540b2006ca823f2ee1464b1e933ad06f1bc6cd0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 10 Oct 2025 13:51:46 +0200 Subject: [PATCH 7/9] cleaning --- txndata/osaka/prover/prover_columns.lispX | 76 ---------------------- txndata/prague/prover/prover_columns.lispX | 76 ---------------------- 2 files changed, 152 deletions(-) delete mode 100644 txndata/osaka/prover/prover_columns.lispX delete mode 100644 txndata/prague/prover/prover_columns.lispX diff --git a/txndata/osaka/prover/prover_columns.lispX b/txndata/osaka/prover/prover_columns.lispX deleted file mode 100644 index dfb2ebe1a..000000000 --- a/txndata/osaka/prover/prover_columns.lispX +++ /dev/null @@ -1,76 +0,0 @@ -(module txndata) - - -(defcolumns - ( prover___REL_USER_TXN_NUMBER :i16 ) - ( prover___REL_USER_TXN_NUMBER_MAX :i16 ) - ( prover___IS_LAST_USER_TXN_OF_BLOCK :i16 ) - ( prover___USER_TXN_NUMBER_MAX :i16 ) - ) - -(defalias - prv_RUSR prover___REL_USER_TXN_NUMBER - prv_RMAX prover___REL_USER_TXN_NUMBER_MAX - prv_LAST prover___IS_LAST_USER_TXN_OF_BLOCK - prv_UMAX prover___USER_TXN_NUMBER_MAX - ) - -(defun - (block-constancy COL) - (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) - (eq! (next COL) COL))) - -(defun - (conflation-constancy COL) - (if-not-zero (perspective-sum) - (eq! (next COL) COL))) - -(defun - (transaction-constancy COL) - (if-not-zero (- (next TOTL_TXN_NUMBER) TOTL_TXN_NUMBER) - (eq! (next COL) COL))) - - -(defconstraint prover-column-constraints---RUSR () - (begin - (block-constancy prv_RUSR) - (if-zero (perspective-sum) - (vanishes! prv_RUSR)) - (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) - (vanishes! prv_RUSR)) - (if-not-zero (- (next BLK_NUMBER) (+ BLK_NUMBER 1)) - (eq! (next prv_RUSR) - (+ prv_RUSR - (- (next USER_TXN_NUMBER) - USER_TXN_NUMBER)))) - )) - -(defconstraint prover-column-constraints---RMAX () - (begin - (block-constancy prv_RMAX) - (if-zero (perspective-sum) - (vanishes! prv_RMAX)) - (if-not-zero SYSF - (eq! prv_RMAX prv_RUSR)) - )) - -(defconstraint prover-column-constraints---LAST () - (begin - (transaction-constancy prv_LAST) - (if-zero USER - (vanishes! prv_LAST)) - (if-not-zero (- TOTL_TXN_NUMBER (next TOTL_TXN_NUMBER)) - (eq! (prev prv_LAST) - (* (prev USER) - SYSF))) - )) - -(defconstraint prover-column-constraints---UMAX () - (begin - (conflation-constancy prv_UMAX) - (if-zero (perspective-sum) - (vanishes! prv_UMAX)) - )) - -(defconstraint prover-column-constraints---UMAX---finalization (:domain {-1}) ;; "" - (eq! prv_UMAX USER_TXN_NUMBER)) diff --git a/txndata/prague/prover/prover_columns.lispX b/txndata/prague/prover/prover_columns.lispX deleted file mode 100644 index dfb2ebe1a..000000000 --- a/txndata/prague/prover/prover_columns.lispX +++ /dev/null @@ -1,76 +0,0 @@ -(module txndata) - - -(defcolumns - ( prover___REL_USER_TXN_NUMBER :i16 ) - ( prover___REL_USER_TXN_NUMBER_MAX :i16 ) - ( prover___IS_LAST_USER_TXN_OF_BLOCK :i16 ) - ( prover___USER_TXN_NUMBER_MAX :i16 ) - ) - -(defalias - prv_RUSR prover___REL_USER_TXN_NUMBER - prv_RMAX prover___REL_USER_TXN_NUMBER_MAX - prv_LAST prover___IS_LAST_USER_TXN_OF_BLOCK - prv_UMAX prover___USER_TXN_NUMBER_MAX - ) - -(defun - (block-constancy COL) - (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) - (eq! (next COL) COL))) - -(defun - (conflation-constancy COL) - (if-not-zero (perspective-sum) - (eq! (next COL) COL))) - -(defun - (transaction-constancy COL) - (if-not-zero (- (next TOTL_TXN_NUMBER) TOTL_TXN_NUMBER) - (eq! (next COL) COL))) - - -(defconstraint prover-column-constraints---RUSR () - (begin - (block-constancy prv_RUSR) - (if-zero (perspective-sum) - (vanishes! prv_RUSR)) - (if-not-zero (- (next BLK_NUMBER) BLK_NUMBER) - (vanishes! prv_RUSR)) - (if-not-zero (- (next BLK_NUMBER) (+ BLK_NUMBER 1)) - (eq! (next prv_RUSR) - (+ prv_RUSR - (- (next USER_TXN_NUMBER) - USER_TXN_NUMBER)))) - )) - -(defconstraint prover-column-constraints---RMAX () - (begin - (block-constancy prv_RMAX) - (if-zero (perspective-sum) - (vanishes! prv_RMAX)) - (if-not-zero SYSF - (eq! prv_RMAX prv_RUSR)) - )) - -(defconstraint prover-column-constraints---LAST () - (begin - (transaction-constancy prv_LAST) - (if-zero USER - (vanishes! prv_LAST)) - (if-not-zero (- TOTL_TXN_NUMBER (next TOTL_TXN_NUMBER)) - (eq! (prev prv_LAST) - (* (prev USER) - SYSF))) - )) - -(defconstraint prover-column-constraints---UMAX () - (begin - (conflation-constancy prv_UMAX) - (if-zero (perspective-sum) - (vanishes! prv_UMAX)) - )) - -(defconstraint prover-column-constraints---UMAX---finalization (:domain {-1}) ;; "" - (eq! prv_UMAX USER_TXN_NUMBER)) From f79e3b2f96bac51abab9add89bc1ec3571ab63ae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= <38285177+OlivierBBB@users.noreply.github.com> Date: Tue, 14 Oct 2025 12:58:39 +0200 Subject: [PATCH 8/9] Prover column after `TXN_DATA` redesign (#796) --- todo | 29 ------------------- .../generalities/flags_perspectives.lisp | 6 ++-- .../generalities/flags_perspectives.lisp | 6 ++-- 3 files changed, 6 insertions(+), 35 deletions(-) delete mode 100644 todo diff --git a/todo b/todo deleted file mode 100644 index b98536f9f..000000000 --- a/todo +++ /dev/null @@ -1,29 +0,0 @@ -✅ hub/columns/scenarios/precompiles.tex -✅ hub/scenario/generalities/precompiles.tex -✅ hub/scenario/shorthands/precompile.tex -✅ hub/instruction_handling/call/precompiles/common/generalities.tex -❌ hub/instruction_handling/call/precompiles/ecadd_ecmul_ecpairing/success.tex -✅ hub/instruction_handling/call/precompiles/ecadd_ecmul_ecpairing_bls/failure_KTR.tex -✅ hub/instruction_handling/call/precompiles/ecadd_ecmul_ecpairing_bls/success.tex -❌ hub/instruction_handling/call/precompiles/nsr_and_flagsum.tex -✅ hub/instruction_handling/call/precompiles/nsr_and_flagsum_I.tex -✅ hub/instruction_handling/call/precompiles/nsr_and_flagsum_II.tex - - - - - - - - - - -❌ Lisp erase -⚠️ Lisp todo -✅ Lisp done - - - -❌ Lisp ràf -⚠️ Lisp unclear -✅ Lisp done diff --git a/txndata/cancun/generalities/flags_perspectives.lisp b/txndata/cancun/generalities/flags_perspectives.lisp index 9442fbfc6..ad6014e3c 100644 --- a/txndata/cancun/generalities/flags_perspectives.lisp +++ b/txndata/cancun/generalities/flags_perspectives.lisp @@ -7,9 +7,9 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun (perspective-sum) (+ RLP - HUB - CMPTN)) +(defun (perspective-sum) (force-bin (+ RLP + HUB + CMPTN))) (defproperty perspective-sum-constraints---it-coincides-with-txn-flag-sum (eq! (perspective-sum) (txn-flag-sum))) (defconstraint perspective-sum-constraints---it-vanishes-initially (:domain {0}) (eq! (perspective-sum) 0)) ;; "" diff --git a/txndata/osaka/generalities/flags_perspectives.lisp b/txndata/osaka/generalities/flags_perspectives.lisp index 9442fbfc6..ad6014e3c 100644 --- a/txndata/osaka/generalities/flags_perspectives.lisp +++ b/txndata/osaka/generalities/flags_perspectives.lisp @@ -7,9 +7,9 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun (perspective-sum) (+ RLP - HUB - CMPTN)) +(defun (perspective-sum) (force-bin (+ RLP + HUB + CMPTN))) (defproperty perspective-sum-constraints---it-coincides-with-txn-flag-sum (eq! (perspective-sum) (txn-flag-sum))) (defconstraint perspective-sum-constraints---it-vanishes-initially (:domain {0}) (eq! (perspective-sum) 0)) ;; "" From 0e0b4e9a71bc6c4b9c2562dc2d6370abb901951a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= <38285177+OlivierBBB@users.noreply.github.com> Date: Mon, 20 Oct 2025 20:56:05 +0200 Subject: [PATCH 9/9] Prover columns revision (#810) --- txndata/cancun/prover/prover_columns_corset.lisp | 2 +- txndata/osaka/prover/prover_columns_corset.lisp | 2 +- txndata/prague/prover/prover_columns_corset.lisp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/txndata/cancun/prover/prover_columns_corset.lisp b/txndata/cancun/prover/prover_columns_corset.lisp index b78fc2774..b44e67de2 100644 --- a/txndata/cancun/prover/prover_columns_corset.lisp +++ b/txndata/cancun/prover/prover_columns_corset.lisp @@ -89,7 +89,7 @@ -(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---const () (user-transaction-constancy RELMAX)) +(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---const () (block-constancy RELMAX)) (defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---zero () (if-zero (perspective-sum) (vanishes! RELMAX))) (defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---setting () (if-not-zero (* (- 1 (prev SYSF)) SYSF) diff --git a/txndata/osaka/prover/prover_columns_corset.lisp b/txndata/osaka/prover/prover_columns_corset.lisp index b78fc2774..b44e67de2 100644 --- a/txndata/osaka/prover/prover_columns_corset.lisp +++ b/txndata/osaka/prover/prover_columns_corset.lisp @@ -89,7 +89,7 @@ -(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---const () (user-transaction-constancy RELMAX)) +(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---const () (block-constancy RELMAX)) (defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---zero () (if-zero (perspective-sum) (vanishes! RELMAX))) (defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---setting () (if-not-zero (* (- 1 (prev SYSF)) SYSF) diff --git a/txndata/prague/prover/prover_columns_corset.lisp b/txndata/prague/prover/prover_columns_corset.lisp index b78fc2774..b44e67de2 100644 --- a/txndata/prague/prover/prover_columns_corset.lisp +++ b/txndata/prague/prover/prover_columns_corset.lisp @@ -89,7 +89,7 @@ -(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---const () (user-transaction-constancy RELMAX)) +(defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---const () (block-constancy RELMAX)) (defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---zero () (if-zero (perspective-sum) (vanishes! RELMAX))) (defconstraint prover-column-constraints---RELATIVE_USER_TXN_NUMBER_MAX---setting () (if-not-zero (* (- 1 (prev SYSF)) SYSF)