• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Pfcs
      • Wp-gen
      • Dimacs-reader
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Riscv
      • 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
      • Aleo
        • Aleobft
          • Correctness
            • Unequivocal-dags-def-and-init
              • Unequivocal-dags-p
              • Unequivocal-dags-p-when-init
            • Same-committees-def-and-implied
            • Dag-omni-paths
            • Signer-records
            • Unequivocal-dags-next
            • Quorum-intersection
            • Dag-previous-quorum-def-and-init-and-next
            • Unequivocal-signed-certificates
            • Signed-previous-quorum
            • Nonforking-anchors-def-and-init-and-next
            • Successor-predecessor-intersection
            • Fault-tolerance
            • Last-anchor-voters-def-and-init-and-next
            • Signer-quorum
            • Committed-redundant-def-and-init-and-next
            • Nonforking-blockchains-def-and-init
            • Blockchain-redundant-def-and-init-and-next
            • No-self-endorsed
            • Last-anchor-present
            • Anchors-extension
            • Nonforking-blockchains-next
            • Backward-closure
            • Last-blockchain-round
            • Dag-certificate-next
            • Omni-paths-def-and-implied
            • Ordered-blockchain
            • Simultaneous-induction
            • System-certificates
            • Last-anchor-def-and-init
            • Last-anchor-next
            • Dag-previous-quorum
            • Signed-certificates
            • Committed-anchor-sequences
            • Omni-paths
            • Last-anchor-voters
            • Unequivocal-dags
            • Nonforking-blockchains
            • Nonforking-anchors
            • Committed-redundant
            • Same-committees
            • Blockchain-redundant
          • Definition
          • Library-extensions
        • Aleovm
        • Leo
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Correctness

Unequivocal-dags-def-and-init

Invariant that DAGs are unequivocal: definition and establishment.

In the model of AleoBFT with static committees, certificates are unequivocal across the whole system, i.e. all the certificates in the system have unique combinations of author and round. With dynamic committees (with or without stake), this property must be weakened slightly in order to be proved. The reason is that, in our model, the system always includes all possible validators that may form committees. Consider, for simplicity, the first few rounds, and the genesis committee. Even with the fault tolerance assumptions formalized in fault-tolerance, there may well be a set of faulty validators, outside the genesis committee, who sign a new certificate that has the same author and round as an existing certificate, the latter having been properly created by the genesis committee. This event is perfectly possible according to our model of create. This equivocal certificate is broadcast to all correct validators, according to our model of reliable broadcast. However, our model of accept events says that a correct validator will move a certificate from the network to the DAG only if its signers form a quorum in the active committee. Therefore, in the hypothetical situation sketched above, a correct validator will not accept the equivocal certificate, which will forever sit in the network, but will never move into any DAG. So this is how the non-equivocation property must be weakened: it must only apply to the DAG, which is, after all, what matters, since blocks are generated from DAGs.

The non-equivocation of the DAG of a single validator, as expressed by certificate-set-unequivocalp applied to the DAG of the validator, could be proved from some already proved invariants. However, we need the more general non-equivocation of DAGs across multiple validators, namely that if two validators have two certificates (one each) in their DAGs with the same author and round, then they are equal certificates. The latter property is expressed by certificate-sets-unequivocalp applied to the DAGs of the two validators. The property for two validator subsumes the property for one validator, by choosing the two validators to be equal. So there is no point in proving non-equivocation for a single validator, which involves some work, and instead we prove non-equivocation for multiple validators, which we need anyhow, and then we obtain non-equivocation for single validator as a very simple consequence.

However, proving DAG non-equivocation for multiple validators relies on another invariant, namely that blockchains do not fork, which is defined in nonforking-blockchains-def-and-init. The reason is that we need the fact that different validators agree on the active committees at certain rounds; since the active committee is calculated from the blockchain, we need the fact that blockchains do not fork, so that the validators calculate the same committee (for their common blockchain prefixes). In turn, the non-forking of blockchains relies on the non-equivocation of DAG certificates. So the preservation of the two invariants must be proved at the same time by induction, because we need a sufficiently strong induction hypothesis, with both invariants available in the old state, from which we can prove that both invariants also hold on the new state.

Here we define the invariant about unequivocal DAGs (for multiple validators, as explained above), and we also prove that it holds in the initial states. In nonforking-blockchains-def-and-init we do the same for the invariant about non-forking blockchains, i.e. we define it and prove it holds in the initial states. Elsewhere we prove that each invariant holds in the new state if both hold in the old state, and finally we put everything together in an induction proof for both invariants (along with other invariants that are all inter-dependent).

Subtopics

Unequivocal-dags-p
Definition of the invariant: the DAGs of each pair of correct validators are mutually unequivocal.
Unequivocal-dags-p-when-init
Establishment of the invariant: the invariant holds in any initial system state.