Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion blsdata/cancun/generalities/constancy_conditions.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -20,5 +20,5 @@

(defconstraint pair-of-inputs-constancy ()
(if-not-zero ACC_INPUTS
(if (will-remain-constant! ACC_INPUTS)
(if-zero (- (next ACC_INPUTS) ACC_INPUTS)
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Bug: Constancy Constraint Scope Narrowing

The pair-of-inputs-constancy constraint now checks ACC_INPUTS constancy only between adjacent rows. This replaces a will-remain-constant! call that likely validated it over a broader context, narrowing the validation scope. This change could allow ACC_INPUTS to vary in later steps, potentially leading to invalid state.

Additional Locations (1)

Fix in Cursor Fix in Web

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this rejected by go-corset ? The original version looked ok to me.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

no, they are probably equivalent, but I believe this way is more clear

(will-remain-constant! NONTRIVIAL_POP_BIT))))
2 changes: 1 addition & 1 deletion blsdata/prague/generalities/constancy_conditions.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -20,5 +20,5 @@

(defconstraint pair-of-inputs-constancy ()
(if-not-zero ACC_INPUTS
(if (will-remain-constant! ACC_INPUTS)
(if-zero (- (next ACC_INPUTS) ACC_INPUTS)
(will-remain-constant! NONTRIVIAL_POP_BIT))))
2 changes: 1 addition & 1 deletion oob/cancun/columns.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@
(ADD_FLAG :binary@prove)
(MOD_FLAG :binary@prove)
(BLS_REF_TABLE_FLAG :binary@prove)
(OUTGOING_INST :byte :display :opcode)
(OUTGOING_INST :i16 :display :opcode)
(OUTGOING_DATA :i128 :array [4])
(OUTGOING_RES_LO :i128))

Expand Down
8 changes: 4 additions & 4 deletions oob/cancun/constants.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -26,10 +26,10 @@
CT_MAX_MODEXP_PRICING 5
CT_MAX_MODEXP_EXTRACT 3
CT_MAX_POINT_EVALUATION 3
CT_MAX_BLS_G1_ADD 3
CT_MAX_BLS_G1_MSM 6
CT_MAX_BLS_G2_ADD 3
CT_MAX_BLS_G2_MSM 6
CT_MAX_BLS_G1_ADD 3
CT_MAX_BLS_G1_MSM 7
CT_MAX_BLS_G2_ADD 3
CT_MAX_BLS_G2_MSM 7
CT_MAX_BLS_PAIRING_CHECK 4
CT_MAX_BLS_MAP_FP_TO_G1 3
CT_MAX_BLS_MAP_FP2_TO_G2 3
Expand Down
2 changes: 1 addition & 1 deletion oob/cancun/lookups/oob-into-add.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
oob.ADD_FLAG)

(defclookup
oob-into-add
(oob-into-add :unchecked)
;; target columns
(
add.ARG_1
Expand Down
2 changes: 1 addition & 1 deletion oob/cancun/lookups/oob-into-mod.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
oob.MOD_FLAG)

(defclookup
oob-into-mod
(oob-into-mod :unchecked)
;; target columns
(
mod.ARG_1_HI
Expand Down
75 changes: 45 additions & 30 deletions oob/cancun/precompiles/common/bls/bls_msm.lisp
Original file line number Diff line number Diff line change
@@ -1,35 +1,39 @@
(module oob)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; For BLS_G1_MSM and BLS_G2_MSM ;;
;; ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun (prc-g1msm-prc-g2msm---standard-precondition)
(+ IS_BLS_G1_MSM
(defun (prc-g1msm-prc-g2msm---standard-precondition)
(+ IS_BLS_G1_MSM
IS_BLS_G2_MSM))
(defun (msm-pair-size)
(+ (* PRECOMPILE_CALL_DATA_UNIT_SIZE___BLS_G1_MSM IS_BLS_G1_MSM)
(defun (msm-pair-size)
(+ (* PRECOMPILE_CALL_DATA_UNIT_SIZE___BLS_G1_MSM IS_BLS_G1_MSM)
(* PRECOMPILE_CALL_DATA_UNIT_SIZE___BLS_G2_MSM IS_BLS_G2_MSM)))
(defun (max-discount)
(+ (* PRC_BLS_G1_MSM_MAX_DISCOUNT IS_BLS_G1_MSM)
(defun (max-discount)
(+ (* PRC_BLS_G1_MSM_MAX_DISCOUNT IS_BLS_G1_MSM)
(* PRC_BLS_G2_MSM_MAX_DISCOUNT IS_BLS_G2_MSM)))
(defun (msm-multiplication-cost)
(+ (* PRC_BLS_G1_MSM_MULTIPLICATION_COST IS_BLS_G1_MSM)
(defun (msm-multiplication-cost)
(+ (* PRC_BLS_G1_MSM_MULTIPLICATION_COST IS_BLS_G1_MSM)
(* PRC_BLS_G2_MSM_MULTIPLICATION_COST IS_BLS_G2_MSM)))
(defun (prc-g1msm-prc-g2msm---remainder) (shift OUTGOING_RES_LO 2))
(defun (prc-g1msm-prc-g2msm---cds-is-multiple-of-msm-pair-size) (shift OUTGOING_RES_LO 3))
(defun (prc-g1msm-prc-g2msm---num-inputs_msm-pair-size) (prc---cds))
(defun (prc-g1msm-prc-g2msm---cds-is-multiple-of-msm-pair-size) (shift OUTGOING_RES_LO 3))
(defun (prc-g1msm-prc-g2msm---num-inputs_msm-pair-size) (prc---cds))
(defun (prc-g1msm-prc-g2msm---num-inputs-gt-128) (shift OUTGOING_RES_LO 4))
(defun (prc-g1msm-prc-g2msm---num-inputs-leq-128) (- 1 (prc-g1msm-prc-g2msm---num-inputs-gt-128)))
(defun (prc-g1msm-prc-g2msm---discount) (shift OUTGOING_RES_LO 5))
(defun (prc-g1msm-prc-g2msm---insufficient-gas) (shift OUTGOING_RES_LO 6))
(defun (prc-g1msm-prc-g2msm---reference-table-discount) (shift OUTGOING_RES_LO 5))
(defun (prc-g1msm-prc-g2msm---discount)
(if-not-zero (prc-g1msm-prc-g2msm---num-inputs-leq-128)
(prc-g1msm-prc-g2msm---reference-table-discount)
(max-discount)))
(defun (prc-g1msm-prc-g2msm---msm-cost-numerator_msm-pair-size)
(* (prc-g1msm-prc-g2msm---num-inputs_msm-pair-size) (msm-multiplication-cost) (prc-g1msm-prc-g2msm---discount)))
(defun (prc-g1msm-prc-g2msm---precompile-cost) (shift OUTGOING_RES_LO 6))
(defun (prc-g1msm-prc-g2msm---insufficient-gas) (shift OUTGOING_RES_LO 7))
(defun (prc-g1msm-prc-g2msm---sufficient-gas) (- 1 (prc-g1msm-prc-g2msm---insufficient-gas)))
(defun (prc-g1msm-prc-g2msm---precompile-cost_msm-pair-size_PRC_BLS_MULTIPLICATION_MULTIPLIER) (* (prc-g1msm-prc-g2msm---num-inputs_msm-pair-size) (msm-multiplication-cost) (prc-g1msm-prc-g2msm---discount)))



(defconstraint prc-g1msm-prc-g2msm---mod-cds-by-msm-pair-size (:guard (* (assumption---fresh-new-stamp) (prc-g1msm-prc-g2msm---standard-precondition)))
(call-to-MOD 2 0 (prc---cds) 0 (msm-pair-size)))
Expand Down Expand Up @@ -63,27 +67,38 @@
(vanishes! (shift [OUTGOING_DATA 2] 5))
(vanishes! (shift [OUTGOING_DATA 3] 5))
(vanishes! (shift [OUTGOING_DATA 4] 5)))
(begin (noCall 5)
(eq! (prc-g1msm-prc-g2msm---discount) (max-discount))))))

(defconstraint prc-g1msm-prc-g2msm---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-g1msm-prc-g2msm---standard-precondition)))
(begin (noCall 5)))))

(defconstraint prc-g1msm-prc-g2msm---compute-precompile-cost-integer-division (:guard (* (assumption---fresh-new-stamp) (prc-g1msm-prc-g2msm---standard-precondition)))
(if-zero (prc-g1msm-prc-g2msm---cds-is-multiple-of-msm-pair-size)
(noCall 6)
(begin (vanishes! (shift ADD_FLAG 6))
(vanishes! (shift MOD_FLAG 6))
(eq! (shift WCP_FLAG 6) 1)
(eq! (shift MOD_FLAG 6) 1)
(vanishes! (shift WCP_FLAG 6))
(vanishes! (shift BLS_REF_TABLE_FLAG 6))
(eq! (shift OUTGOING_INST 6) EVM_INST_LT)
(eq! (shift OUTGOING_INST 6) EVM_INST_DIV)
(vanishes! (shift [OUTGOING_DATA 1] 6))
(eq! (shift [OUTGOING_DATA 2] 6) (prc---callee-gas))
(eq! (* (shift [OUTGOING_DATA 2] 6) (msm-pair-size)) (prc-g1msm-prc-g2msm---msm-cost-numerator_msm-pair-size))
(vanishes! (shift [OUTGOING_DATA 3] 6))
(eq! (* (shift [OUTGOING_DATA 4] 6) (msm-pair-size) PRC_BLS_MULTIPLICATION_MULTIPLIER)
(prc-g1msm-prc-g2msm---precompile-cost_msm-pair-size_PRC_BLS_MULTIPLICATION_MULTIPLIER)))))
(eq! (shift [OUTGOING_DATA 4] 6) PRC_BLS_MULTIPLICATION_MULTIPLIER))))
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Bug: Cost Calculation Error in Precompile Constraint

The prc-g1msm-prc-g2msm---compute-precompile-cost-integer-division constraint performs a division but doesn't store the result into (shift OUTGOING_RES_LO 6). As a result, prc-g1msm-prc-g2msm---precompile-cost will not reflect the computed value, leading to an incorrect precompile cost.

Fix in Cursor Fix in Web


(defconstraint prc-g1msm-prc-g2msm---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-g1msm-prc-g2msm---standard-precondition)))
(if-zero (prc-g1msm-prc-g2msm---cds-is-multiple-of-msm-pair-size)
(noCall 7)
(begin (vanishes! (shift ADD_FLAG 7))
(vanishes! (shift MOD_FLAG 7))
(eq! (shift WCP_FLAG 7) 1)
(vanishes! (shift BLS_REF_TABLE_FLAG 7))
(eq! (shift OUTGOING_INST 7) EVM_INST_LT)
(vanishes! (shift [OUTGOING_DATA 1] 7))
(eq! (shift [OUTGOING_DATA 2] 7) (prc---callee-gas))
(vanishes! (shift [OUTGOING_DATA 3] 7))
(eq! (shift [OUTGOING_DATA 4] 7) (prc-g1msm-prc-g2msm---precompile-cost)))))
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we replace all the (shift [OUTGOING_DATA X] Y) with meaningful shorthand names ?

Copy link
Contributor Author

@lorenzogentile404 lorenzogentile404 Oct 1, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

yes, but I would prefer in a separated PR.


(defconstraint prc-g1msm-prc-g2msm---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-g1msm-prc-g2msm---standard-precondition)))
(begin (eq! (prc---hub-success)
(* (prc---cds-is-non-zero) (prc-g1msm-prc-g2msm---cds-is-multiple-of-msm-pair-size) (prc-g1msm-prc-g2msm---sufficient-gas)))
(if-zero (prc---hub-success)
(vanishes! (prc---return-gas))
(eq! (* (prc---return-gas) (msm-pair-size) PRC_BLS_MULTIPLICATION_MULTIPLIER)
(- (* (prc---callee-gas) (msm-pair-size) PRC_BLS_MULTIPLICATION_MULTIPLIER) (prc-g1msm-prc-g2msm---precompile-cost_msm-pair-size_PRC_BLS_MULTIPLICATION_MULTIPLIER))))))
(eq! (prc---return-gas)
(- (prc---callee-gas) (prc-g1msm-prc-g2msm---precompile-cost))))))
2 changes: 1 addition & 1 deletion oob/prague/columns.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@
(ADD_FLAG :binary@prove)
(MOD_FLAG :binary@prove)
(BLS_REF_TABLE_FLAG :binary@prove)
(OUTGOING_INST :byte :display :opcode)
(OUTGOING_INST :i16 :display :opcode)
(OUTGOING_DATA :i128 :array [4])
(OUTGOING_RES_LO :i128))

Expand Down
8 changes: 4 additions & 4 deletions oob/prague/constants.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -26,10 +26,10 @@
CT_MAX_MODEXP_PRICING 5
CT_MAX_MODEXP_EXTRACT 3
CT_MAX_POINT_EVALUATION 3
CT_MAX_BLS_G1_ADD 3
CT_MAX_BLS_G1_MSM 6
CT_MAX_BLS_G2_ADD 3
CT_MAX_BLS_G2_MSM 6
CT_MAX_BLS_G1_ADD 3
CT_MAX_BLS_G1_MSM 7
CT_MAX_BLS_G2_ADD 3
CT_MAX_BLS_G2_MSM 7
CT_MAX_BLS_PAIRING_CHECK 4
CT_MAX_BLS_MAP_FP_TO_G1 3
CT_MAX_BLS_MAP_FP2_TO_G2 3
Expand Down
2 changes: 1 addition & 1 deletion oob/prague/lookups/oob-into-add.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
oob.ADD_FLAG)

(defclookup
oob-into-add
(oob-into-add :unchecked)
;; target columns
(
add.ARG_1
Expand Down
2 changes: 1 addition & 1 deletion oob/prague/lookups/oob-into-mod.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
oob.MOD_FLAG)

(defclookup
oob-into-mod
(oob-into-mod :unchecked)
;; target columns
(
mod.ARG_1_HI
Expand Down
51 changes: 33 additions & 18 deletions oob/prague/precompiles/common/bls/bls_msm.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -20,16 +20,20 @@
(+ (* PRC_BLS_G1_MSM_MULTIPLICATION_COST IS_BLS_G1_MSM)
(* PRC_BLS_G2_MSM_MULTIPLICATION_COST IS_BLS_G2_MSM)))
(defun (prc-g1msm-prc-g2msm---remainder) (shift OUTGOING_RES_LO 2))
(defun (prc-g1msm-prc-g2msm---cds-is-multiple-of-msm-pair-size) (shift OUTGOING_RES_LO 3))
(defun (prc-g1msm-prc-g2msm---num-inputs_msm-pair-size) (prc---cds))
(defun (prc-g1msm-prc-g2msm---cds-is-multiple-of-msm-pair-size) (shift OUTGOING_RES_LO 3))
(defun (prc-g1msm-prc-g2msm---num-inputs_msm-pair-size) (prc---cds))
(defun (prc-g1msm-prc-g2msm---num-inputs-gt-128) (shift OUTGOING_RES_LO 4))
(defun (prc-g1msm-prc-g2msm---num-inputs-leq-128) (- 1 (prc-g1msm-prc-g2msm---num-inputs-gt-128)))
(defun (prc-g1msm-prc-g2msm---discount) (shift OUTGOING_RES_LO 5))
(defun (prc-g1msm-prc-g2msm---insufficient-gas) (shift OUTGOING_RES_LO 6))
(defun (prc-g1msm-prc-g2msm---reference-table-discount) (shift OUTGOING_RES_LO 5))
(defun (prc-g1msm-prc-g2msm---discount)
(if-not-zero (prc-g1msm-prc-g2msm---num-inputs-leq-128)
(prc-g1msm-prc-g2msm---reference-table-discount)
(max-discount)))
(defun (prc-g1msm-prc-g2msm---msm-cost-numerator_msm-pair-size)
(* (prc-g1msm-prc-g2msm---num-inputs_msm-pair-size) (msm-multiplication-cost) (prc-g1msm-prc-g2msm---discount)))
(defun (prc-g1msm-prc-g2msm---precompile-cost) (shift OUTGOING_RES_LO 6))
(defun (prc-g1msm-prc-g2msm---insufficient-gas) (shift OUTGOING_RES_LO 7))
(defun (prc-g1msm-prc-g2msm---sufficient-gas) (- 1 (prc-g1msm-prc-g2msm---insufficient-gas)))
(defun (prc-g1msm-prc-g2msm---precompile-cost_msm-pair-size_PRC_BLS_MULTIPLICATION_MULTIPLIER) (* (prc-g1msm-prc-g2msm---num-inputs_msm-pair-size) (msm-multiplication-cost) (prc-g1msm-prc-g2msm---discount)))



(defconstraint prc-g1msm-prc-g2msm---mod-cds-by-msm-pair-size (:guard (* (assumption---fresh-new-stamp) (prc-g1msm-prc-g2msm---standard-precondition)))
(call-to-MOD 2 0 (prc---cds) 0 (msm-pair-size)))
Expand Down Expand Up @@ -63,27 +67,38 @@
(vanishes! (shift [OUTGOING_DATA 2] 5))
(vanishes! (shift [OUTGOING_DATA 3] 5))
(vanishes! (shift [OUTGOING_DATA 4] 5)))
(begin (noCall 5)
(eq! (prc-g1msm-prc-g2msm---discount) (max-discount))))))
(begin (noCall 5)))))

(defconstraint prc-g1msm-prc-g2msm---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-g1msm-prc-g2msm---standard-precondition)))
(defconstraint prc-g1msm-prc-g2msm---compute-precompile-cost-integer-division (:guard (* (assumption---fresh-new-stamp) (prc-g1msm-prc-g2msm---standard-precondition)))
(if-zero (prc-g1msm-prc-g2msm---cds-is-multiple-of-msm-pair-size)
(noCall 6)
(begin (vanishes! (shift ADD_FLAG 6))
(vanishes! (shift MOD_FLAG 6))
(eq! (shift WCP_FLAG 6) 1)
(eq! (shift MOD_FLAG 6) 1)
(vanishes! (shift WCP_FLAG 6))
(vanishes! (shift BLS_REF_TABLE_FLAG 6))
(eq! (shift OUTGOING_INST 6) EVM_INST_LT)
(eq! (shift OUTGOING_INST 6) EVM_INST_DIV)
(vanishes! (shift [OUTGOING_DATA 1] 6))
(eq! (shift [OUTGOING_DATA 2] 6) (prc---callee-gas))
(eq! (* (shift [OUTGOING_DATA 2] 6) (msm-pair-size)) (prc-g1msm-prc-g2msm---msm-cost-numerator_msm-pair-size))
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Bug: EVM Division Precompile Constraint Error

The compute-precompile-cost-integer-division constraint misconfigures the EVM_INST_DIV operation. OUTGOING_DATA 2 is incorrectly constrained as a value related to the quotient, but it should be the dividend (numerator). The actual division result (the precompile cost) should come from OUTGOING_RES_LO.

Fix in Cursor Fix in Web

(vanishes! (shift [OUTGOING_DATA 3] 6))
(eq! (* (shift [OUTGOING_DATA 4] 6) (msm-pair-size) PRC_BLS_MULTIPLICATION_MULTIPLIER)
(prc-g1msm-prc-g2msm---precompile-cost_msm-pair-size_PRC_BLS_MULTIPLICATION_MULTIPLIER)))))
(eq! (shift [OUTGOING_DATA 4] 6) PRC_BLS_MULTIPLICATION_MULTIPLIER))))

(defconstraint prc-g1msm-prc-g2msm---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-g1msm-prc-g2msm---standard-precondition)))
(if-zero (prc-g1msm-prc-g2msm---cds-is-multiple-of-msm-pair-size)
(noCall 7)
(begin (vanishes! (shift ADD_FLAG 7))
(vanishes! (shift MOD_FLAG 7))
(eq! (shift WCP_FLAG 7) 1)
(vanishes! (shift BLS_REF_TABLE_FLAG 7))
(eq! (shift OUTGOING_INST 7) EVM_INST_LT)
(vanishes! (shift [OUTGOING_DATA 1] 7))
(eq! (shift [OUTGOING_DATA 2] 7) (prc---callee-gas))
(vanishes! (shift [OUTGOING_DATA 3] 7))
(eq! (shift [OUTGOING_DATA 4] 7) (prc-g1msm-prc-g2msm---precompile-cost)))))

(defconstraint prc-g1msm-prc-g2msm---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-g1msm-prc-g2msm---standard-precondition)))
(begin (eq! (prc---hub-success)
(* (prc---cds-is-non-zero) (prc-g1msm-prc-g2msm---cds-is-multiple-of-msm-pair-size) (prc-g1msm-prc-g2msm---sufficient-gas)))
(if-zero (prc---hub-success)
(vanishes! (prc---return-gas))
(eq! (* (prc---return-gas) (msm-pair-size) PRC_BLS_MULTIPLICATION_MULTIPLIER)
(- (* (prc---callee-gas) (msm-pair-size) PRC_BLS_MULTIPLICATION_MULTIPLIER) (prc-g1msm-prc-g2msm---precompile-cost_msm-pair-size_PRC_BLS_MULTIPLICATION_MULTIPLIER))))))
(eq! (prc---return-gas)
(- (prc---callee-gas) (prc-g1msm-prc-g2msm---precompile-cost))))))
2 changes: 1 addition & 1 deletion reftables/prague/bls_reftable.lisp
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(module blsreftable)

(defcolumns
(PRC_NAME :byte)
(PRC_NAME :i16)
(NUM_INPUTS :i8) ;; greatest value is 128
(DISCOUNT :i10) ;; greatest value is 1000
)
Loading