Skip to content

Conversation

OlivierBBB
Copy link
Collaborator

@OlivierBBB OlivierBBB commented Oct 8, 2025

Note

Adds prover columns and constraints for relative/user transaction tracking across txndata variants, wires USER_TXN_NUMBER_MAX from rlptxn into txndata, and makes perspective-sum explicitly binary.

  • Prover columns:
    • txndata/{cancun,osaka,prague}:
      • Computed: prover___RELATIVE_USER_TXN_NUMBER, prover___IS_LAST_USER_TXN_OF_BLOCK with properties.
      • New columns: prover___RELATIVE_USER_TXN_NUMBER_MAX, prover___USER_TXN_NUMBER_MAX with constancy/finalization constraints.
    • rlptxn/cancun:
      • New column: prover___USER_TXN_NUMBER_MAX with constancy/finalization constraints.
  • Data flow:
    • Update rlptxn/cancun/lookups/rlptxn_into_txndata.lisp to map rlptxn.prover___USER_TXN_NUMBER_MAXtxndata.prover___USER_TXN_NUMBER_MAX.
  • Generalities:
    • txndata/prague/generalities/flags_perspectives.lisp: make perspective-sum binary via force-bin.

Written by Cursor Bugbot for commit 30ed81e. This will update automatically on new commits. Configure here.

cursor[bot]

This comment was marked as outdated.

cursor[bot]

This comment was marked as outdated.

cursor[bot]

This comment was marked as outdated.

(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))))))
Copy link

Choose a reason for hiding this comment

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

Bug: Block Number Mismatch Causes Increment Error

The RELATIVE_USER_TXN_NUMBER---increment property's condition (if-not-zero (- (next BLK_NUMBER) (+ BLK_NUMBER 1))) applies increment logic when (next BLK_NUMBER) is not BLK_NUMBER + 1. This conflicts with the RELUSR column's definition, which resets it to 0 on any block number change, leading to inconsistent behavior.

Additional Locations (2)

Fix in Cursor Fix in Web

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant