• 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
                    • Proposal-fix
                    • Proposalp
                    • Proposal-equiv
                    • Make-proposal
                    • Proposal->transactions
                    • Change-proposal
                    • Proposal->previous
                    • Proposal->round
                    • Proposal->author
                  • 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
  • Proposals

Proposal

Fixtype of proposals.

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

Fields
author — address
round — posp
transactions — transaction-list
previous — address-set

We model a proposal as consisting of:

  1. The address of the validator who authored the proposal.
  2. The round number of the proposal.
  3. The transactions that the validator is proposing for inclusion in the blockchain.
  4. The addresses that, together with the previous round number, identify the certificates from the previous round that this certificate references. When the proposal is turned into a certificate, these define the edges of the DAG. It is a system invariant, proved elsewhere, that certificates in DAGs are uniquely identified by their author and round.

We do not model cryptographic signatures explicitly. The presence of the author address in a proposal models the fact that the author signed the proposal.

Subtopics

Proposal-fix
Fixing function for proposal structures.
Proposalp
Recognizer for proposal structures.
Proposal-equiv
Basic equivalence relation for proposal structures.
Make-proposal
Basic constructor macro for proposal structures.
Proposal->transactions
Get the transactions field from a proposal.
Change-proposal
Modifying constructor for proposal structures.
Proposal->previous
Get the previous field from a proposal.
Proposal->round
Get the round field from a proposal.
Proposal->author
Get the author field from a proposal.