• 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
                  • Transaction
                  • Transaction-list
                • Proposals
                • 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

Transactions

Transactions.

Validators propose transactions for inclusion in the blockchain. Transactions have a rich structure. In fact, AleoBFT handles not only transactions, but also `solutions' and (possibly in the future) `ratifications', which together with transactions form `transmissions'.

However, most of these details are unimportant for our model. Our model sticks to the more common term `transaction', which can be thought as modeling also the other kinds of transmissions. Our model is concerned with two kinds of transactions: one to bond a validator (i.e. add the validator to the committee with some stake), and one to unbond a validator (i.e. remove the validator from the committee). So we consider these two kinds of transactions, plus an opaque one for all other kinds of transactions.

Subtopics

Transaction
Fixtype of transactions.
Transaction-list
Fixtype of lists of transactions.