|
|
|---|
|
|
|
|---|
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
A
An
Elsewhere we prove that the invariant holds in every reachable state.