• 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
      • 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
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
        • Aleobft
          • Aleobft-static
          • Aleobft-dynamic
          • Aleobft-arxiv
          • Aleobft-stake
            • Correctness
              • Unequivocal-dags-def-and-init
              • Same-committees-def-and-implied
              • Signer-records
              • Dag-omni-paths
              • Unequivocal-dags-next
              • Quorum-intersection
              • Previous-quorum-def-and-init-and-next
              • Unequivocal-signed-certificates
              • Same-associated-certificates
              • Nonforking-anchors-def-and-init-and-next
              • Signed-previous-quorum
              • Successor-predecessor-intersection
              • Fault-tolerance
              • Last-anchor-voters-def-and-init-and-next
              • Signer-quorum
              • Committed-redundant-def-and-init-and-next
              • Nonforking-blockchains-def-and-init
              • Dag-committees
              • No-self-messages
              • Blockchain-redundant-def-and-init-and-next
              • Backward-closure
              • Anchors-extension
              • Nonforking-blockchains-next
              • No-self-endorsed
              • Associated-certificates
                • Associated-certs-of-next
                • Associated-certs
                • Associated-certs-when-init
              • Last-anchor-present
              • No-self-buffer
              • Signed-certificates
              • Last-blockchain-round
              • Dag-certificate-next
              • Omni-paths-def-and-implied
              • Simultaneous-induction
              • Ordered-even-blocks
              • Last-anchor-def-and-init
              • Last-anchor-next
              • Previous-quorum
              • Committed-anchor-sequences
              • Omni-paths
              • Last-anchor-voters
              • Unequivocal-dags
              • Signed-and-associated-cerificates
              • Nonforking-blockchains
              • Nonforking-anchors
              • Committed-redundant
              • Same-committees
              • Blockchain-redundant
            • Definition
          • Aleobft-proposals
          • Library-extensions
        • Leo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Community
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Correctness

Associated-certificates

Certificates associated to validators.

A validator has certificates in its DAG and buffer. But the network may contain messages, with certificates, that are addressed to the validator: even though the validator does not yet have those certificates (in its DAG or buffer), it may eventually have them, if and when the message is delivered. It is useful to introduce a notion for the certificates associated to a validator, in the sense of being in the DAG, or in the buffer, or in a message addressed to the validator.

We define this notion here, and we prove theorems about its initial value, and about how its value changes in response to events.

Subtopics

Associated-certs-of-next
How the certificates associated to a validator change (or not) for each transition.
Associated-certs
Certificates associated to a validator.
Associated-certs-when-init
Initially, validators have no associated certificates.