Draft
Conversation
Add specifications/ewd687a/EWD687a_proof.tla. All 408 obligations
discharged by tlapm in ~38s (macbook pro M1).
Fully proved:
THEOREM TypeCorrect == Spec => []TypeOK
THEOREM Thm_CountersConsistent == Spec => CountersConsistent
via the combined inductive invariant Inv1 == TypeOK /\ Counters,
where Counters relates the four per-edge counters:
sentUnacked[e] = rcvdUnacked[e] + acks[e] + msgs[e].
TypeOK alone is not inductive (RcvAck/SendAck decrement counters).
LEMMA Inv2Inductive == Spec => []Inv2
Inv2 is the structural overlay-tree strengthening of DT1Inv:
non-neutral non-leader processes are in the upEdge tree, and
upEdge[p] is a well-formed incoming edge of p with
rcvdUnacked[upEdge[p]] >= 1. Inductiveness proved per action.
Left OMITTED (future work):
LEMMA DT1FromInv2 == Inv2 => DT1Inv (chain/acyclicity)
THEOREM Thm_DT1Inv == Spec => []DT1Inv
THEOREM Thm_TreeWithRoot == Spec => TreeWithRoot (IsTreeWithRoot)
THEOREM Thm_DT2 == Spec => DT2 (liveness)
Wire the module into CI: add a "proof" entry in manifest.json (picked
up by the data-driven Check proofs step in .github/workflows/CI.yml)
and flip the TLAPS Proof column in README.md.
Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Discharge the previously OMITTED LEMMA DT1FromInv2 by introducing an
auxiliary acyclicity invariant on the overlay tree, so the chain
Spec => []DT1Inv goes through end-to-end.
New invariant:
NoCycle == \A S \in SUBSET (Procs \ {Leader}) :
~ (/\ S # {}
/\ \A q \in S : InTree(q) /\ upEdge[q][1] \in S)
i.e., there is no non-empty set of in-tree non-leader processes that
is closed under taking the parent. Equivalently, every in-tree
process can reach the leader by following upEdge.
New lemmas:
LEMMA NoCycleInit == Init => NoCycle
LEMMA NoCycleStep == Inv2 /\ NoCycle /\ [Next]_vars => NoCycle'
LEMMA NoCycleInductive == Spec => []NoCycle
Inductiveness of NoCycle is by case analysis over Next. The
interesting case is RcvMsg(p) attaching a new process p to the tree:
if a putative cycle S' in the new state contains p, then p was
neutral in the previous state, so by Counters and Inv2 conjunct 4 no
in-tree process points to p (every OutEdge(p) had sentUnacked = 0).
Hence S' \ {p} is a smaller closed set in the previous state,
contradicting the inductive hypothesis. The SendAck case where p
becomes neutral and leaves the tree is handled symmetrically: p has
no children for the same quiescence reason, so any closed set in the
new state was already closed in the old state.
Discharge of the chain step:
LEMMA DT1FromInv2 == Inv2 /\ NoCycle => DT1Inv
Assume neutral(Leader) and a non-leader p0 with ~neutral(p0). The
set S == {q \in Procs \ {Leader} : ~neutral(q)} is non-empty, and by
Inv2 conjuncts 3-4 plus Counters it is closed under the parent
function (sentUnacked[upEdge[q]] >= 1 forces the parent to be
non-neutral, and neutral(Leader) keeps it out of {Leader}). This
contradicts NoCycle, so all non-leader processes are neutral.
Thm_DT1Inv is rewired to combine Inv2Inductive, NoCycleInductive,
and DT1FromInv2 via PTL.
Drafted by Claude Opus 4.7. All 642 TLAPS obligations discharged
in ~30s. Only Thm_TreeWithRoot and Thm_DT2 remain OMITTED.
Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add specifications/ewd687a/EWD687a_proof.tla. All 408 obligations discharged by tlapm in ~38s (macbook pro M1).
Fully proved:
THEOREM TypeCorrect == Spec => []TypeOK
THEOREM Thm_CountersConsistent == Spec => CountersConsistent
via the combined inductive invariant Inv1 == TypeOK /\ Counters,
where Counters relates the four per-edge counters:
sentUnacked[e] = rcvdUnacked[e] + acks[e] + msgs[e].
TypeOK alone is not inductive (RcvAck/SendAck decrement counters).
LEMMA Inv2Inductive == Spec => []Inv2
Inv2 is the structural overlay-tree strengthening of DT1Inv:
non-neutral non-leader processes are in the upEdge tree, and
upEdge[p] is a well-formed incoming edge of p with
rcvdUnacked[upEdge[p]] >= 1. Inductiveness proved per action.
Left OMITTED (future work):
LEMMA DT1FromInv2 == Inv2 => DT1Inv (chain/acyclicity)
THEOREM Thm_DT1Inv == Spec => []DT1Inv
THEOREM Thm_TreeWithRoot == Spec => TreeWithRoot (IsTreeWithRoot)
THEOREM Thm_DT2 == Spec => DT2 (liveness)
Wire the module into CI: add a "proof" entry in manifest.json (picked up by the data-driven Check proofs step in .github/workflows/CI.yml) and flip the TLAPS Proof column in README.md.