• 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
          • Aleobft-proposals
            • Correctness
            • Definition
              • Initialization
              • Transitions
              • States
                • Committees
                • System-states
                • Certificates
                • Transactions
                • Proposals
                  • Proposal
                  • Props-with-author+round
                  • Props-with-round
                  • Prop-set-unequivp
                  • Proposal-option
                  • Prop-set-none-author-p
                  • Prop-set-all-author-p
                  • Proposal-set
                • Messages
                • Validator-states
                • Blocks
                • Addresses
              • Events
              • Reachability
          • 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

Proposals

Proposals.

Validators generate and exchange proposals, which contain proposed transactions along with other information. Once they have enough endorsements, in the form of signatures, proposals are turned into certificates, which are the vertices of the DAG.

Proposals have a rich structure, but we model only the information needed for our purposes.

Subtopics

Proposal
Fixtype of proposals.
Props-with-author+round
Retrieve, from a set of proposals, the subset of proposals with a given author and round.
Props-with-round
Retrieve, from a set of proposals, the subset of proposals with a given round.
Prop-set-unequivp
Check if a set of proposals is unequivocal.
Proposal-option
Fixtype of optional proposals.
Prop-set-none-author-p
Check if none of the proposals in a set have a given author.
Prop-set-all-author-p
Check if all the proposals in a set have a given author.
Proposal-set
Fixtype of sets of proposals.