• 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
            • Correctness
            • Definition
              • Initialization
              • Transitions
              • States
                • Committees
                  • Update-committee-with-transaction
                  • Max-faulty-for-total
                  • Bonded-committee-at-round
                  • Active-committee-at-round
                  • Update-committee-with-transaction-list
                  • Committee-after-blocks
                  • Lookback
                  • Committee-quorum
                  • Committee-option
                  • Committee
                    • Committee-fix
                    • Committee-equiv
                    • Make-committee
                    • Committeep
                    • Committee->addresses
                    • Change-committee
                  • Committee-members
                  • Committee-total
                  • Committee-max-faulty
                  • Same-bonded-committees-p
                  • Same-active-committees-p
                  • Genesis-committee
                • System-states
                • Certificates
                • Messages
                • Validator-states
                • Transactions
                • Blocks
                • Addresses
              • Events
          • Aleobft-stake
          • 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
  • Committees

Committee

Fixtype of committees.

This is a product type introduced by fty::defprod.

Fields
addresses — address-set
Additional Requirements

The following invariant is enforced on the fields:

(not (emptyp addresses))

In our model, a committee is just a set of addresses, but we wrap it in a fixtype for greater abstraction and extensibility. When we generalize the model with stake, this committee fixtype will need to include the stake of each validator, besides the addresses of the validators.

Subtopics

Committee-fix
Fixing function for committee structures.
Committee-equiv
Basic equivalence relation for committee structures.
Make-committee
Basic constructor macro for committee structures.
Committeep
Recognizer for committee structures.
Committee->addresses
Get the addresses field from a committee.
Change-committee
Modifying constructor for committee structures.