• 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
            • Correctness
              • Invariant-unequivocal-certificates
              • Invariant-same-certificates
              • Invariant-committed-redundant
              • Invariant-signers-have-author-round
              • Property-paths-to-voted-anchor
              • Properties-dags
                • Certificate-causal-history-of-unequivocal-dag-superset
                • Previous-certificates-of-unequivocal-dag-superset
                • Path-to-author+round-of-unequivocal-dag-superset
                • Previous-certificates-of-unequivocal-dags
                • Path-to-previous
                • Path-to-author+round-set-to-path-to-author+round
                • Certificate-causal-history-of-unequivocal-dags
                • Path-to-author+round-of-unequivocal-dags
                • Path-to-author+round-transitive
                • Path-to-author+round-to-cert-with-author+round
                • In-of-certificate-causal-history
                • Dag-previous-in-dag-p-of-intersect
                • Cert-with-author+round-when-path-to-author+round
                • Cardinality-of-outgoing-quorum
                • Certificate-causal-history-subset-when-path
                • Path-to-outgoing
                • Path-from-incoming
                • Cardinality-of-incoming-to-tally-leader-votes
              • Invariant-no-self-endorsed
              • Properties-certificate-retrieval
              • Invariant-last-anchor-voters
              • Invariant-blockchain-redundant
              • Invariant-previous-are-quorum
              • Invariant-no-self-buffer
              • Invariant-anchors-not-forking
              • Invariant-signers-are-validators
              • Invariant-previous-in-dag
              • Invariant-last-before-current
              • Invariant-last-anchor-present
              • Properties-anchors-extension
              • Invariant-unequivocal-dag
              • Property-paths-to-other-voted-anchor
              • Invariant-no-self-messages
              • Invariant-paths-to-other-last-anchor
              • Invariant-addresses
              • Invariant-last-is-even
              • Invariant-signers-are-quorum
              • Invariant-messages-to-correct
              • Properties-blockchain
              • Invariant-paths-to-last-anchor
              • Invariant-unequivocal-dags
              • Invariant-blockchain-not-forking
              • Operations-additional
              • Invariant-quorum
              • Invariant-dag-previous-are-quorum
              • Properties-anchors
              • Property-committed-anchors-of-next-event
              • Invariant-max-faulty
              • Property-last-anchor-of-next-event
              • Invariant-certificate-retrieval
              • Invariant-fault-tolerance
              • Invariant-dag-authors-are-validators
              • Invariant-causal-histories
            • Definition
          • Aleobft-stake2
          • 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
  • Correctness

Properties-dags

Some properties of the operations on DAGs.

Some of these come in two forms, analogous to the ones described in properties-certificate-retrieval: one form about the consistency of the growing DAG of a single validator, and one form about the consistency across DAGs of different validators. In fact, the proofs of these theorems about DAGs make use of those theorems about certificate retrieval.

Besides the ones mentioned just above, there are also other properties proved here, which do not come in pairs like that.

Subtopics

Certificate-causal-history-of-unequivocal-dag-superset
The causal history of a certificate in a backward-closed subset of an unequivocal DAG is the same in the superset.
Previous-certificates-of-unequivocal-dag-superset
The predecessor cerfificates of a certificate in a backward-closed subset of a DAG of unequivocal certificates are the same in the superset.
Path-to-author+round-of-unequivocal-dag-superset
The paths from a certificate in a backward-closed subset of a DAG of unequivocal certificates are the same in the superset.
Previous-certificates-of-unequivocal-dags
The predecessor certificates of a common certificate of two backward-closed unequivocal and mutually unequivocal DAGs are the same in the two DAGs.
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
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, assuming the DAG is unequivocal.
Certificate-causal-history-of-unequivocal-dags
The causal histories of a common certificate of two backward-closed unequivocal and mutually unequivocal DAGs are the same in the two DAGs.
Path-to-author+round-of-unequivocal-dags
The paths from a common certificate of two backward-closed unequivocal and mutually unequivocal DAGs are the same in the two DAGs.
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.
Dag-previous-in-dag-p-of-intersect
Intersecting two unequivocal backward-closed DAGs yields a backward-closed DAG.
Cert-with-author+round-when-path-to-author+round
If there is a path from a certificate in an unequivocal DAG then retrieving a certificate with that author and round results in a certificate.
Cardinality-of-outgoing-quorum
In a backward-closed unequivocal DAG whose certificates have a given number of precedessors, the number of outgoing certificates is equal to that number.
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-outgoing
There is a path from a certificate to each of its outgoing certificates.
Path-from-incoming
There is a path to a certificate from each of its incoming certificates.
Cardinality-of-incoming-to-tally-leader-votes
Relation between the number of incoming certificates and the number of `yes' votes to the certificate.