• 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
            • Correctness
            • Definition
              • Initialization
              • Transitions
                • Transitions-receive-certificate
                • Transitions-create-certificate
                • Dags
                  • Path-to-author+round
                  • Successors
                  • Certificate-causal-history
                  • Paths-in-unequivocal-closed-dags
                  • Predecessors
                  • Unequivocal-previous-certificates
                  • Certificate-previous-in-dag-p
                  • Certificates-dag-paths-p
                  • Causal-histories-in-unequivocal-closed-dags
                  • Dag-predecessor-cardinality-p
                  • Dag-rounds-in-committees-p
                  • Path-to-previous
                  • Path-to-author+round-set-to-path-to-author+round
                  • Dag-committees-p
                  • Dag-closedp
                  • Path-to-author+round-transitive
                  • Path-to-author+round-to-cert-with-author+round
                  • In-of-certificate-causal-history
                  • Path-to-predecessor
                  • Path-from-successor
                  • Certificate-causal-history-subset-when-path
                  • Path-to-head-of-predecessors
                • Transitions-advance-round
                • Events-next
                • Events-possiblep
                • Event-next
                • Elections
                • Transitions-commit-anchors
                • Transitions-store-certificate
                • Event-possiblep
                • Anchors
                • Blockchains
                • Transitions-timer-expires
              • States
              • Events
          • 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
  • Transitions

Dags

DAGs.

As defined in validator-state, we model a DAG as a set of certificates. Here we introduce operations on DAGs (as certificate sets) that are more DAG-specific than the operations on certificate sets defined in the certificates book. By `DAG-specific' we mean those operations that take into account the edges of the DAG, as opposed to treating the DAG as just a set of vertices as the operations in the certificates book do. The edges are represented as the previous component of certificates, so they are part of the vertices, in terms of data structures.

Subtopics

Path-to-author+round
Retrieve the certificate with the given author and round reachable from a given certificate through the DAG edges.
Successors
Set of the certificates in a DAG that are successors of a certificate in a DAG.
Certificate-causal-history
Causal history of a certificate in a DAG.
Paths-in-unequivocal-closed-dags
Some theorems about paths in unequivocal, backward-closed DAGs.
Predecessors
Set of the certificates in a DAG that are precedessors of a certificate in a DAG.
Unequivocal-previous-certificates
Some theorems about retrieving the previous certificates of a certificate in unequivocal DAGs.
Certificate-previous-in-dag-p
Check if all the previous certificates referenced by a given certificate are in a given DAG.
Certificates-dag-paths-p
Check if a list of zero or more certificates are all in a DAG and are connected by paths.
Causal-histories-in-unequivocal-closed-dags
Some theorems about causal histories in unequivocal, backward-closed DAGs.
Dag-predecessor-cardinality-p
Check if the number of precedessor certificates of each certificate in a DAG is 0 if the certificate's round is 1 or the quorum of the active committee at the previous round if the certificate's round is not 1.
Dag-rounds-in-committees-p
Check if the (one or more) authors of the certificates in each round of a DAG are members of the active committee at that round.
Path-to-previous
In an unequivocal DAG, there is always a path between a certificate and each of its predecessors.
Path-to-author+round-set-to-path-to-author+round
In an unequivocal DAG, if a certificate has a path to an author and round, then any set including the certificate has a path to that author and round, and it results in the same certificate.
Dag-committees-p
Check if the active committee at the round of every certificate in a DAG can be calculated from a given blockchain.
Dag-closedp
Check if a DAG is backward-closed.
Path-to-author+round-transitive
Transitivity of DAG paths.
Path-to-author+round-to-cert-with-author+round
If a certificate in an unequivocal DAG has a path to a certain author and round, the path ends up at the certificate retrieved via that author and round.
In-of-certificate-causal-history
Characterization of the members of a certificate's causal history.
Path-to-predecessor
There is a path from a certificate to each of its predecessors.
Path-from-successor
In an unequivocal DAG, there is a path to a certificate from each of its successors.
Certificate-causal-history-subset-when-path
In an unequivocal DAG, if there is a path between two certificates, the causal history of the destination of the path is a subset of the causal history of the source of the path.
Path-to-head-of-predecessors
There is a path from a certificate to the first of its predecessors, assuming that it has predecessors.