• 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
          • Aleobft-stake
          • Aleobft-proposals
            • Correctness
            • Definition
              • Initialization
              • Transitions
                • Transitions-accept
                • Transitions-certify
                • Transitions-propose
                • Events-possiblep
                • Elections
                • Events-next
                • Event-possiblep
                • Event-next
                • Transitions-commit
                • Transitions-augment
                • Dags
                  • Path-to-author+round
                  • Cert-causal-history
                  • Cert-previous-in-dag-p
                  • Dag-closedp
                • Transitions-endorse
                • Transitions-advance
                • Blockchains
                • Anchors
              • States
              • Events
              • Reachability
          • 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 certificates. By `DAG-specific' we mean 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 certificates 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.
Cert-causal-history
Causal history of a certificate in a DAG.
Cert-previous-in-dag-p
Check if all the previous certificates referenced by a given certificate are in a given DAG.
Dag-closedp
Check if a DAG is backward-closed.