• 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
            • Correctness
            • Definition
              • Initialization
              • Transitions
              • States
                • Committees
                • System-states
                • Certificates
                • Messages
                • Validator-states
                  • Validator-state
                  • Address+pos-pairs-with-address
                  • Timer
                  • Address+pos
                  • Address+pos-set
                • Transactions
                • Blocks
                • Addresses
              • Events
          • 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
  • States

Validator-states

States of (correct) validators.

Validators have internal states. For correct validators, i.e. the ones that follow the protocol, the internal states must contain certain information that is prescribed by the protocol, which we model here. For faulty validators, i.e. the ones that do not (always) follow the protcol, we do not need to model the internal state, because what matters in our model is only the effect that faulty validators may have on correct ones, via messages exchanged over the network.

Subtopics

Validator-state
Fixtype of states of a (correct) validator.
Address+pos-pairs-with-address
Retrieve, from a set of pairs of addresses and positive integers, the pairs with a given address.
Timer
Fixtype of timer states.
Address+pos
Fixtype of pairs consisting of addresses and positive integers.
Address+pos-set
Fixtype of sets of pairs consisting of addresses and positive integers.