• 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
                • System-states
                  • Update-validator-state
                  • System-state
                  • Validators-state
                    • Validators-statep
                    • Validators-state-fix
                    • Validators-state-equiv
                  • Update-network-state
                  • Correct-addresses
                  • Get-validator-state
                  • Faulty-addresses
                  • Get-network-state
                  • All-addresses
                • 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
  • System-states

Validators-state

Fixtype of states of a collection of validators.

This map captures the state of all the validators in the system, which, as explained in system-states, is a potentially large set of all possible validators. The (unchanging) addresses are captured in the keys of the map, while the changeable states are the values of the map. The set of keys of this map does not change, because again these are all possible validators, not just a committee.

Since faulty validators may do almost arbitrary things (short of breaking cryptography, along with other well-defined and well-motivated restrictions), there is no need to actually model their internal states. So we use nil to model (the state of) faulty validators in this map. We model the behavior of faulty validators in terms of nondeterministic generation of messages for other (correct) validators; it also does not matter which messages are received by faulty validators, who can behave arbitrarily regardless of what they receive or not.

A basic assumption in our model is that a validator is either always correct or not. If not, it is considered faulty, no matter how small its deviation from correct behavior. In practice, this corresponds to a validator either running snarkOS and snarkVM or not; whether snarkOS and snarkVM correctly implement AleoBFT is a separate problem.

Subtopics

Validators-statep
Recognizer for validators-state.
Validators-state-fix
(validators-state-fix x) is a usual ACL2::fty omap fixing function.
Validators-state-equiv
Basic equivalence relation for validators-state structures.