• 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
            • Correctness
              • Invariant-unequivocal-certificates
              • Invariant-same-certificates
              • Invariant-committed-redundant
              • Invariant-signers-have-author-round
              • Property-paths-to-voted-anchor
              • Properties-dags
              • 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
                • Operations-certificates-for-validators
                • Operations-dags-additional
                • Operations-anchors
                • Operations-unequivocal-certificates
                • Operations-fault-tolerance
                • Operations-blockchain-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-dynamic
          • Aleobft-arxiv
          • Aleobft-stake
          • 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

Operations-additional

Additional operations on system states and their components.

These operations are used to formulate and prove the correctness of the system, along with the ones defined in operations. Unlike the latter, these operations are not used to define the state transitions of the system; this is why they are grouped separately.

Subtopics

Operations-certificates-for-validators
Operations about certificates in actual or potential possession of validators.
Operations-dags-additional
Additional operations on DAGs.
Operations-anchors
Operations for anchors.
Operations-unequivocal-certificates
Operations about unequivocal certificates.
Operations-fault-tolerance
Operations about fault tolerance.
Operations-blockchain-additional
Additional operations on the blockchain.