• 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
          • Aleobft-proposals
            • Correctness
            • Definition
              • Initialization
              • Transitions
                • Transitions-accept
                • Transitions-certify
                • Transitions-propose
                • Events-possiblep
                • Elections
                • Events-next
                • Event-possiblep
                • Event-next
                • Transitions-commit
                • Transitions-augment
                • Dags
                • Transitions-endorse
                • Transitions-advance
                • Blockchains
                  • Extend-blockchain
                  • Transactions-from-certificates
                • Anchors
              • States
              • Events
              • Reachability
          • 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

Blockchains

Blockchains.

As defined in validator-state, we model a blockchain as a list of blocks, growing from right to left (i.e. via cons).

Here we introduce operations on blockchains, specifically operations to extend blockchains. These operations are used to define what happens when a validator commits one or more anchors, each of which results in a block.

Subtopics

Extend-blockchain
Extend the blockchain with one or more anchors.
Transactions-from-certificates
Collect all the transactions from a set of certficates.