		Search-engine friendly clone of the ACL2 documentation.

Correctness

Unequivocal-dags-next

Invariant that DAGs are unequivocal: preservation.

As explained in unequivocal-dags-def-and-init, in order to prove that the non-equivocation of DAG is preserved by state transitions, we need to assume that the old state satisfies not only the non-equivocation of DAGs, but also the non-forking of blockchains. From that, here we prove that the new state satisfies the non-equivocation of DAGs.

At a high level, the reason why DAGs are unequivocal is the following. By contradiction, suppose that two validators (which may be the same) have two equivocal certificates in DAGs, one for each validator, i.e. the two certificates have the same author and round, but they are different certificates. Each certificate would be signed by a quorum of validators, in the active committee for the round of both certificates. Each validator calculates its own active committee for that round, but because of the assumed non-forking of blockchains, those two calculated active committees are the same (see same-committees-def-and-implied). Thus, by quorum intersection, and assuming that the committee is fault-tolerant, we must have at least one correct validator in both signer sets. But a correct validator would not have signed two different certificates with the same author and round, so the initial premise must not hold, i.e. there cannot exist equivocal certificates. The just mentioned fact that a correct validator does not sign two equivocal certificates amounts to the already proved invariant that the set of the certificates signed by a correct validator is unequivocal (see unequivocal-signed-certificates), which we use to prove this new invariant.

The above argument has to be spelled out more precisely for ACL2. The only two kinds of events that may extend DAGs (and could therefore potentially break non-equivocation) are create and store.

A create event concerns the (correct) author of the certificate, which checks that the signers, including itself, of the new certificate are in the active committee and form a quorum. If a validator (the author or other) had already, in its DAG, a different certificate with the same author and round, the two certificates must have at least one common correct signer, whose signed certificates would thus be equivocal, but we know they are not, as already proved in unequivocal-signed-certificates.

A store event concerns the (correct) validator who moves the certificate from the buffer to the DAG; the validator checks that the signers are in the active committee. If a validator (the one storing the certificate, or another one) had already, in its DAG, a different certificate with the same author and round, the two certificates must have at least one common correct signer, whose signed certificates would thus be equivocal, but we know they are not, as already proved in unequivocal-signed-certificates.

Elsewhere we prove that the invariant holds in every reachable state.

Subtopics

Unequivocal-dags-p-of-next: Preservation of the invariant: if the invariant holds in a system state, it also holds in the next system state.