• 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
            • Correctness
            • Definition
              • Initialization
              • Transitions
              • States
                • Committees
                • System-states
                • Certificates
                  • Certificate-set-unequivocalp
                  • Certificate-sets-unequivocalp
                  • Cert-with-author+round
                  • Certificate
                  • Certs-with-authors+round
                  • Certs-with-author
                  • Certs-with-round
                  • Unequivocal-certs-with-authors+round
                  • Unequivocal-cert-with-author+round
                  • Cert-set->author-set
                  • Certificate-option
                  • Cert-set->round-set
                  • Certs-with-authors
                  • Certificates-ordered-even-p
                  • Certs-with-signer
                  • Certificate->signers
                  • Certificate-set
                  • Certificate-list
                • Messages
                • Transactions
                • Validator-states
                • Blocks
                • Addresses
              • Events
              • Reachability
          • Aleobft-dynamic
          • 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
  • States

Certificates

Certificates.

Validators generate and exchange certificates, which contain proposed transactions along with other information. Certificates are the vertices of the DAG.

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

In AleoBFT, there is a distinction between proposals and certificates, with the latter being an extension of the former with endorsing signatures. Currently we do not model proposals, but just certificates, because we treat the Narwhal aspects of AleoBFT somewhat abstractly; see transitions-create.

Subtopics

Certificate-set-unequivocalp
Check if a set of certificates is unequivocal.
Certificate-sets-unequivocalp
Check if two sets of certificates are mutually unequivocal.
Cert-with-author+round
Retrieve, from a set of certificates, a certificate with a given author and round.
Certificate
Fixtype of certificates.
Certs-with-authors+round
Retrieve, from a set of certificates, the subset of certificates with author in a given set and with a given round.
Certs-with-author
Retrieve, from a set of certificates, the subset of certificates with a given author.
Certs-with-round
Retrieve, from a set of certificates, the subset of certificates with a given round.
Unequivocal-certs-with-authors+round
Properties of certs-with-authors+round when used on unequivocal certificate sets.
Unequivocal-cert-with-author+round
Properties of cert-with-author+round when used on unequivocal certificate sets.
Cert-set->author-set
Lift certificate->author to sets.
Certificate-option
Fixtype of optional certificates.
Cert-set->round-set
Lift certificate->round to sets.
Certs-with-authors
Retrieve, from a set of certificates, the subset of certificates with author in a given set.
Certificates-ordered-even-p
Check if a list of certificates has even and strictly increasing (right to left) round numbers.
Certs-with-signer
Retrieve, from a set of certificates, the subset of certificates whose signers include a given address.
Certificate->signers
Signers of a certificate.
Certificate-set
Fixtype of sets of certificates.
Certificate-list
Fixtype of lists of certificates.