• 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
      • Riscv
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • 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
      • Aleo
        • Aleobft
          • Correctness
            • Unequivocal-dags-def-and-init
            • Same-committees-def-and-implied
            • Dag-omni-paths
            • Signer-records
            • Unequivocal-dags-next
            • Quorum-intersection
            • Dag-previous-quorum-def-and-init-and-next
            • Unequivocal-signed-certificates
            • Signed-previous-quorum
            • Nonforking-anchors-def-and-init-and-next
            • Successor-predecessor-intersection
            • Fault-tolerance
            • Last-anchor-voters-def-and-init-and-next
            • Signer-quorum
            • Committed-redundant-def-and-init-and-next
            • Nonforking-blockchains-def-and-init
            • Blockchain-redundant-def-and-init-and-next
            • No-self-endorsed
            • Last-anchor-present
            • Anchors-extension
            • Nonforking-blockchains-next
            • Backward-closure
            • Last-blockchain-round
            • Dag-certificate-next
            • Omni-paths-def-and-implied
            • Ordered-blockchain
              • Ordered-blockchain-p-of-next
              • Ordered-blockchain-p
              • Ordered-blockchain-p-when-init
              • Ordered-blockchain-p-of-events-next
              • Ordered-blockchain-p-when-reachable
            • Simultaneous-induction
            • System-certificates
            • Last-anchor-def-and-init
            • Last-anchor-next
            • Dag-previous-quorum
            • Signed-certificates
            • Committed-anchor-sequences
            • Omni-paths
            • Last-anchor-voters
            • Unequivocal-dags
            • Nonforking-blockchains
            • Nonforking-anchors
            • Committed-redundant
            • Same-committees
            • Blockchain-redundant
          • Definition
          • Library-extensions
        • Aleovm
        • Leo
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Correctness

Ordered-blockchain

Invariant that blocks in validators' blockchains have strictly increasing, even round numbers.

Blocks are committed in even rounds, so all the block round numbers are even. Furthermore, blocks are committed as rounds increase, so blocks have strictly increasing round numbers in the blockchain.

Subtopics

Ordered-blockchain-p-of-next
Preservation of the invariant: if the invariant holds in a system state, it also holds in the next system state.
Ordered-blockchain-p
Definition of the invariant: the blockchain of every correct validator has strictly increasing, even round numbers.
Ordered-blockchain-p-when-init
Establishment of the invariant: the invariant holds in any initial system state.
Ordered-blockchain-p-of-events-next
Preservation of the invariant by multiple transitions.
Ordered-blockchain-p-when-reachable
The invariant holds in every reachable state.