• 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
                    • System-statep
                    • System-state-fix
                    • System-state-equiv
                    • Make-system-state
                    • System-state->validators
                    • System-state->network
                    • Change-system-state
                  • Validators-state
                  • 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

System-state

Fixtype of system states.

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

Fields
validators — validators-state
network — message-set

This fixtype captures the state of the whole system of validators, i.e. the state of the whole protocol. It consists of a map from validator addresses to optional validator states (see validators-state), and a set of messages that models the state of the network (see message for a rationale of this model of the network).

As explained in system-states, the validators are all the possible ones, in the genesis committe as well as any future committee. Note that the system state does not have any information about the current committee, because that is a notion that every validator computes on its own, based on their view of the blockchain.

The only shared state is the network, which is shared in a very restricted way (as formalized by the state transitions), in terms of message sending and receiving. The rest of the system state is strictly partitioned among the validators, which communicate exclusively through network messages.

Subtopics

System-statep
Recognizer for system-state structures.
System-state-fix
Fixing function for system-state structures.
System-state-equiv
Basic equivalence relation for system-state structures.
Make-system-state
Basic constructor macro for system-state structures.
System-state->validators
Get the validators field from a system-state.
System-state->network
Get the network field from a system-state.
Change-system-state
Modifying constructor for system-state structures.