• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Pfcs
      • Wp-gen
      • Dimacs-reader
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Riscv
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • 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
      • Aleo
        • Aleobft
          • Correctness
          • Definition
            • Initialization
            • Transitions
            • States
              • Committees
              • System-states
              • Certificates
                • Certificate-set-unequivocalp
                • Certificate-sets-unequivocalp
                • Cert-with-author+round
                • Certs-with-authors+round
                • Certs-with-author
                • Certs-with-round
                • Unequivocal-certs-with-authors+round
                • Unequivocal-cert-with-author+round
                • Certificate
                • Cert-set->author-set
                • Certificate-option
                • Cert-set->round-set
                • Certs-with-authors
                • Certificate-list-orderedp
                • Certs-with-signer
                • Certificate->signers
                • Certificate-list-evenp
                • Certificate->transactions
                • Certificate->previous
                • Certificate->author
                • Certificate->round
                • Certificate-set
                • Certificate-list
              • Messages
              • Transactions
              • Proposals
              • Validator-states
              • Blocks
              • Addresses
            • Events
            • Reachability
          • Library-extensions
        • Aleovm
        • Leo
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • States

Certificates

Certificates.

Validators generate and exchange certificates, which consist of proposals with endorsing signatures. Certificates are the vertices of the DAG, in the Narwhal part of AleoBFT.

Beside defining certificates, we also introduce operations on (sets of) certificates, particularly to retrieve certificates from sets according to author and/or round criteria. Since DAGs are represented as sets in validator states, these operations are usable (and in fact mainly used) on DAGs.

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.
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.
Certificate
Fixtype of certificates.
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.
Certificate-list-orderedp
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-list-evenp
Check if the round numbers of all the certificates in a list are even.
Certificate->transactions
List of transactions of (the proposal in) a certificate.
Certificate->previous
Set of references to previous certificates of (the proposal in) a certificate.
Certificate->author
Author of (the proposal in) a certificate.
Certificate->round
Round number of (the proposal in) a certificate.
Certificate-set
Fixtype of sets of certificates.
Certificate-list
Fixtype of lists of certificates.