• 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
            • Definition
              • Transitions
              • Operations
                • Operations-author-round-pairs
                • Operations-faults-and-quora
                • Operations-leaders
                • Operations-previous-certificates
                • Operations-dags
                  • Path-to-author+round
                  • Certificate-causal-history
                • Operations-blockchain
                • Operations-voting
                • Operations-message-creation
              • States
              • Initialization
              • Events
          • 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
  • Operations

Operations-dags

Operations on DAGs.

We introduce operations on sets of certificates representing DAGs. Some operations on sets of certificates are introduced in certificates, but those are really about general sets of certificates, while the ones introduced here are more specific to DAGs.

Subtopics

Path-to-author+round
Retrieve the certificate with the given author and round reachable from a given certificate through the DAG edges.
Certificate-causal-history
Causal history of a certificate in a DAG.