Nonforking-anchors-p-of-next
Preservation of the invariant:
if the invariant holds in a system state,
it also holds in the next system state.
The only kind of event that may modify the committed anchors
is commit, whose preservation proof is explained below.
For the other five kinds of events, the proof of preservation is easy,
because committed-anchors does not change
as proved in committed-anchors-of-next,
and so if there was no fork before there is no fork after either.
To prove the preservation of anchor non-forking under commit,
we need to show that, in the new state,
the committed anchor sequences of any two validators do not fork.
There are a few cases to consider.
If neither of those two validator is the one that commits anchors,
their committed anchor sequences do not change,
and thus if they were not forking before, they are still not forking.
This case is covered by the local lemma case-others,
whose proof is easy by using committed-anchors-of-commit-next
to rewrite committed-anchors to the previous values.
Otherwise, at least one of the validators must be val,
i.e. the one that commits anchors.
If both validators are val, then the non-forking is trivial:
this case does not even need a lemma;
it gets taken care of in the proof of
nonforking-anchors-p-of-commit-next-lemma,
which is the main lemma that proves the final theorem.
So below we consider the possible cases of
one validator being val
and the other being a different one val0.
There are three cases to consider,
based on whether the last committed round of val0
is equal to, or less than, or greater than
the newly committed round of val,
which is one less than the current round of val.
That is, the three cases are whether last committed round of val0 is
aligned with, behind, or ahead of the newly committed round of val:
these three cases are covered by the three local lemmas
case-other-aligned, case-other-behind, and case-other-ahead,
which we now explain.
Common to the three cases and lemmas
is the handling of the committed-anchors calls.
The one on val0 is reduced to the old value,
via the committed-anchors-of-commit-next rule,
and then the :expand hint turns that into
a call of collect-all-anchors.
But the one on val is rewritten
not via committed-anchors-of-commit-next,
which would result in an append,
but via committed-anchors-of-commit-next-to-collect-all-anchors,
which produces directly a call of collect-all-anchors.
For this to work, it is critical that
committed-anchors-of-commit-next-to-collect-all-anchors
is introduced after committed-anchors-of-commit-next,
and thus it is reliably tried first by ACL2,
according to its ordered history of events.
The reason why we use an :expand hint,
instead of just enabling committed-anchors,
is that it would interfere with the two rewrite rules.
Any case, this strategy results in lists-noforkp
applied to two calls of collect-all-anchors,
in all three lemmas.
Another commonality among the three lemmas is that
they do not need the hypothesis that
nonforking-anchors-p holds on the old state.
That hypothesis is not needed, because we prove the non-forking
directly on the two calls of collect-all-anchors
that result from the proof strategy described above.
Note that, when the committed anchors of val are extended,
they may become aligned with, or behind, or ahead of,
the committed anchors of val0,
regardless of whether, in the old state,
they were aligned, or behind, or ahead;
it is indeed simpler to just consider the two new anchor sequences,
without regard to the two old anchor sequences.
In the lemma case-other-aligned,
the last anchor committed by val0 (which does not change),
and the new anchor committed by val,
are the same certificate,
because they are at the same round (by hypothesis of the case),
and because the leader at that common round is also the same,
given that committees agree across val and val0.
The fact that the two certificate are equal
is proved via cert-with-author+round-of-unequivocal-sets,
and then the key theorem is collect-all-anchors-of-unequivocal-dags,
which says that the anchors collected from a common certificate
are the same in the two validators.
The rest of the hints in the proof serve to
relieve hypotheses of these two key theorems we use.
In the lemma case-other-behind,
the last anchor committed by val0 (which does not change)
is behind the new anchor committed by val.
We already proved in omni-paths-p-implied
that, since the last anchor of val0 has at least f+1 votes,
there are paths to it in every DAG (including the one of val),
from certificates at least two rounds ahead.
By hypothesis of the case, the new anchor committed by val
is ahead of the last anchor of val0,
and they are all at even rounds,
so it is at least two rounds ahead.
So the key theorem we apply here is
collect-all-anchors-to-append-of-collect-anchors-dags,
which lets us rewrite the new anchors committed by val,
expressed as a call of collect-all-anchors as explained above,
as an append of something (irrelevant here) to
the anchors committed by val0,
from which lists-noforkp follows
(via enabled rules about that function).
The rest of the hints in case-other-behind
serve to relieve the hypotheses of the key theorem we use in the proof.
In the lemma case-other-ahead,
the last anchor committed by val0 (which does not change)
is ahead of the new anchor committed by val.
The key theorem in this proof is again
collect-all-anchors-to-append-of-collect-anchors-dags,
with the roles of the validators swapped.
But here we can no longer obtain
the omni-paths property directly from an invariant as in the previous case.
But the property still holds,
given that the new committed anchor of val
has more than f voting stake.
So we prove, just before the lemma for the case,
the theorem dag-omni-paths-p-when-commit-possiblep,
which says that the omni-paths property holds
when commit-possiblep holds.
The key theorem in that proof is dag-omni-paths-p-holds,
whose hypotheses are all fairly direct to relieve,
but note that we need to use
stake-of-successors-to-leader-stake-votes
as a bridge between the greater than f hypothesis
of dag-omni-paths-p-holds,
which is in terms of successors,
and the greater than f check performed by commit-possiblep,
which is in terms of leader-stake-votes.
Back to the lemma case-other-ahead,
we use the just proved dag-omni-paths-p-when-commit-possiblep
to relieve the hypothesis about omni-paths of
collect-all-anchors-to-append-of-collect-anchors-dags.
So the proof of this case-other-ahead
is fairly similar to case-other-behind,
except for how we discharge the omni-paths hypothesis.
The local lemma nonforking-anchors-p-of-commit-next-lemma
uses the four case-... lemmas described above.
Since the lemma is over generic val1 and val2,
we need to instantiate each the three latter lemmas twice,
with val0 playing the role of val1 or val2.
The lemma case-others is only used once,
because it is already formulated on val1 and val2.
Attempting to use these four lemmas just as rewrite rules
does not make the proof succeed:
they would probably necessitate a :cases hint
corresponding to the cases of the lemmas,
but the :use hint looks simpler and shorter.
From nonforking-anchors-p-of-commit-next-lemma,
the main theorem nonforking-anchors-p-of-commit-next
easily follows.
Definitions and Theorems
Theorem: nonforking-anchors-p-of-create-next
(defthm nonforking-anchors-p-of-create-next
(implies (and (nonforking-anchors-p systate)
(system-committees-fault-tolerant-p systate)
(backward-closed-p systate)
(no-self-endorsed-p systate)
(signer-records-p systate)
(signer-quorum-p systate)
(unequivocal-dags-p systate)
(same-committees-p systate)
(last-anchor-present-p systate)
(create-possiblep cert systate))
(nonforking-anchors-p (create-next cert systate))))
Theorem: nonforking-anchors-p-of-accept-next
(defthm nonforking-anchors-p-of-accept-next
(implies (and (nonforking-anchors-p systate)
(system-committees-fault-tolerant-p systate)
(backward-closed-p systate)
(signer-quorum-p systate)
(unequivocal-signed-certs-p systate)
(unequivocal-dags-p systate)
(same-committees-p systate)
(last-anchor-present-p systate)
(accept-possiblep msg systate)
(messagep msg))
(nonforking-anchors-p (accept-next msg systate))))
Theorem: nonforking-anchors-p-of-advance-next
(defthm nonforking-anchors-p-of-advance-next
(implies (and (nonforking-anchors-p systate)
(advance-possiblep val systate))
(nonforking-anchors-p (advance-next val systate))))
Theorem: dag-omni-paths-p-when-commit-possiblep
(defthm dag-omni-paths-p-when-commit-possiblep
(implies
(and (backward-closed-p systate)
(signer-quorum-p systate)
(unequivocal-dags-p systate)
(same-committees-p systate)
(dag-previous-quorum-p systate)
(in val0 (correct-addresses systate))
(commit-possiblep val systate)
(addressp val))
(dag-omni-paths-p
(cert-with-author+round
(leader-at-round
(1- (validator-state->round (get-validator-state val systate)))
(active-committee-at-round
(1-
(validator-state->round (get-validator-state val systate)))
(validator-state->blockchain
(get-validator-state val systate))))
(1- (validator-state->round (get-validator-state val systate)))
(validator-state->dag (get-validator-state val systate)))
(validator-state->dag (get-validator-state val0 systate)))))
Theorem: nonforking-anchors-p-of-commit-next-lemma
(defthm nonforking-anchors-p-of-commit-next-lemma
(implies
(and (nonforking-anchors-p systate)
(backward-closed-p systate)
(last-blockchain-round-p systate)
(ordered-blockchain-p systate)
(signer-quorum-p systate)
(unequivocal-dags-p systate)
(same-committees-p systate)
(dag-previous-quorum-p systate)
(last-anchor-present-p systate)
(omni-paths-p systate)
(commit-possiblep val systate)
(addressp val)
(in val1 (correct-addresses systate))
(in val2 (correct-addresses systate)))
(lists-noforkp
(committed-anchors
(get-validator-state val1 (commit-next val systate)))
(committed-anchors
(get-validator-state val2 (commit-next val systate))))))
Theorem: nonforking-anchors-p-of-commit-next
(defthm nonforking-anchors-p-of-commit-next
(implies (and (nonforking-anchors-p systate)
(backward-closed-p systate)
(last-blockchain-round-p systate)
(ordered-blockchain-p systate)
(signer-quorum-p systate)
(unequivocal-dags-p systate)
(same-committees-p systate)
(dag-previous-quorum-p systate)
(last-anchor-present-p systate)
(omni-paths-p systate)
(commit-possiblep val systate)
(addressp val))
(nonforking-anchors-p (commit-next val systate))))
Theorem: nonforking-anchors-p-of-event-next
(defthm nonforking-anchors-p-of-event-next
(implies (and (nonforking-anchors-p systate)
(system-committees-fault-tolerant-p systate)
(backward-closed-p systate)
(last-blockchain-round-p systate)
(ordered-blockchain-p systate)
(no-self-endorsed-p systate)
(signer-records-p systate)
(unequivocal-signed-certs-p systate)
(signer-quorum-p systate)
(unequivocal-dags-p systate)
(same-committees-p systate)
(dag-previous-quorum-p systate)
(last-anchor-present-p systate)
(omni-paths-p systate)
(event-possiblep event systate))
(nonforking-anchors-p (event-next event systate))))
