• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
        • Aleobft
          • Aleobft-static
          • Aleobft-stake2
          • Aleobft-dynamic
          • Aleobft-stake
            • Correctness
            • Definition
              • Initialization
              • Transitions
                • Transitions-create
                • Dags
                • Transitions-receive
                • Transitions-store
                • Transitions-advance
                • Elections
                • Event-next
                • Transitions-commit
                  • Commit-possiblep
                  • Commit-next
                • Event-possiblep
                • Events-possiblep
                • Events-next
                • Blockchains
                • Transitions-timeout
                • Anchors
              • States
              • Events
          • Aleobft-proposals
          • Library-extensions
        • Leo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Transitions

Transitions-commit

Transitions for anchor commitment.

Here we define the system state transitions caused by commit events.

An anchor commitment event involves just one correct validator.

This event can only happen in an odd round different from 1. The anchor at the preceding even round must be present, and it must have a sufficient stake of voters from the odd round. That anchor is committed, along with possibly more anchors that are reachable from that anchor and that have not been committed yet. Committing an anchor (the one in the even round voted from the odd round, or one reachable from it) amounts to generating a block, and adding it to the blockchain. Each block contains all the transactions from all the uncommitted certificates, linearized in some deterministic way.

An anchor commitment event does not involve the network.

Subtopics

Commit-possiblep
Check if a commit event is possible.
Commit-next
New state resulting from a commit event.