• 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
          • Definition
            • Initialization
            • Transitions
            • States
              • Committees
                • Max-faulty-for-total
                • Bonded-committee-at-round
                • Committee-members-stake
                • Active-committee-at-round
                • Update-committee-with-transaction
                • Committee-quorum-stake
                • Lookback
                • Committee-option
                • Update-committee-with-transaction-list
                • Committee-after-blocks
                  • Same-bonded-committees-p
                  • Same-active-committees-p
                  • Committee
                  • Committee-member-stake
                  • Committee-total-stake
                  • Committee-max-faulty-stake
                  • Committee-nonemptyp
                  • Committee-members
                  • Address-pos-map
                  • Genesis-committee
                • System-states
                • Certificates
                • Messages
                • Transactions
                • Proposals
                • Validator-states
                • Blocks
                • Addresses
              • Events
              • Reachability
            • 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
    • Committees

    Committee-after-blocks

    Calculate the committee after a list of blocks.

    Signature
    (committee-after-blocks blocks) → commtt
    Arguments
    blocks — Guard (block-listp blocks).
    Returns
    commtt — Type (committeep commtt).

    The list of blocks is the blockchain (of a validator), or a prefix of that blockchain (more on this later). We calculate the committee that results from updating the genesis committee with all the transactions in the blocks. Since, as explained in validator-state, the blockchain goes from right to left (i.e. the leftmost block is the newest and the rightmost block is the oldest), we update the genesis committee from right to left to arrive at the resulting committee.

    Definitions and Theorems

    Function: committee-after-blocks

    (defun committee-after-blocks (blocks)
      (declare (xargs :guard (block-listp blocks)))
      (let ((__function__ 'committee-after-blocks))
        (declare (ignorable __function__))
        (b* (((when (endp blocks))
              (genesis-committee))
             (commtt (committee-after-blocks (cdr blocks))))
          (update-committee-with-transaction-list
               (block->transactions (car blocks))
               commtt))))

    Theorem: committeep-of-committee-after-blocks

    (defthm committeep-of-committee-after-blocks
      (b* ((commtt (committee-after-blocks blocks)))
        (committeep commtt))
      :rule-classes :rewrite)

    Theorem: committee-after-blocks-of-block-list-fix-blocks

    (defthm committee-after-blocks-of-block-list-fix-blocks
      (equal (committee-after-blocks (block-list-fix blocks))
             (committee-after-blocks blocks)))

    Theorem: committee-after-blocks-block-list-equiv-congruence-on-blocks

    (defthm committee-after-blocks-block-list-equiv-congruence-on-blocks
      (implies (block-list-equiv blocks blocks-equiv)
               (equal (committee-after-blocks blocks)
                      (committee-after-blocks blocks-equiv)))
      :rule-classes :congruence)