State Transition Rules and Invariants

State Transition Rules and Invariants

1. Initialization:

   • A single path from Uninitialized → Initialized is allowed on the first batch (prevBatchHash == 0).

   • currentForkId set to 1, marking the genesis commit’s creation.

2. Batch Submission:

   • Only unpaused state allows new batches.

   • Must build on the last commit hash (unless genesis).

   • commitHash must be unique or revert with DuplicateCommit.

3. Fork Management:

   • A new fork increments currentForkId.

   • Ties old forks above targetForkId as abandoned; can restore older forks if they become canonical again.

   • The first commit in a new fork references the chosen parent’s commit.

4. Access Control:

   • DEFAULT_ADMIN_ROLE can assign or remove roles.

   • APPENDER_ROLE needed to submit a batch.

   • FORKER_ROLE required for forking.

   • PAUSER_ROLE / UNPAUSER_ROLE for toggling pause.

5. Pause Control:

   • Paused or unpaused are the two states.

   • Mutating operations revert if paused.

   • The unpauser can resume normal operations.

6. Commit Registry:

   • _usedCommits[commitHash] tracks usage.

   • Once set, a commit can never be reused or deleted.

   • This ensures global uniqueness across all forks.

Invariants (must always hold true):

• Fork Integrity: currentForkId monotonically increases. Fork ancestry must remain traceable.

• Commit Integrity: Each commit has a valid parent (except genesis) and a strictly higher height than its parent.

• Canonical Batches: Must lie on the chain that leads from the current fork tip to genesis without encountering any fork that branches lower.

• Access Control: Roles are strictly enforced for each operation.

• Pausable: If paused, no new commits or forks can be created.