Skip to content

Commit 45da2e0

Browse files
lemmyclaude
lemmy
and
claude
committed
ewd687a: prove DT1FromInv2 (Spec => []DT1Inv now complete)
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>
1 parent 3b328df commit 45da2e0

1 file changed

Lines changed: 300 additions & 12 deletions

File tree

‎specifications/ewd687a/EWD687a_proof.tla‎

Lines changed: 300 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -124,7 +124,6 @@ Inv2 == /\ TypeOK
124124
(***************************************************************************)
125125
(* The chain step. *)
126126
(* *)
127-
(* Sketch (formal proof below uses a finite-set/well-foundedness argument):*)
128127
(* Assume Inv2 and neutral(Leader). Suppose, for contradiction, that *)
129128
(* S == {p \in Procs \ {Leader} : ~neutral(p)} is non-empty. *)
130129
(* *)
@@ -135,18 +134,27 @@ Inv2 == /\ TypeOK
135134
(* is itself in S. *)
136135
(* *)
137136
(* So upEdge[_][1] defines a function f : S -> S with no fixed points. *)
138-
(* In a finite non-empty set, such an f must contain a cycle. Ruling out *)
139-
(* the cycle requires a separate "upEdge is acyclic" invariant which we *)
140-
(* do not establish here (it relies on the temporal ordering in which *)
141-
(* upEdges are set: a process always becomes a child only after its *)
142-
(* future parent has become non-neutral). *)
137+
(* In any non-empty set such an f might still admit a cycle, so we need an *)
138+
(* auxiliary invariant ruling out cycles in the upEdge graph. We use the *)
139+
(* following formulation: there is no non-empty set of in-tree non-leader *)
140+
(* processes that is closed under taking the parent. (Equivalently: every *)
141+
(* in-tree process can reach the leader by following upEdge.) *)
143142
(* *)
144-
(* The full TLAPS proof of acyclicity is delegated to future work; the *)
145-
(* lemma below is therefore left OMITTED. The other conjuncts of Inv2 *)
146-
(* are fully proved above. *)
143+
(* NoCycle is established inductively (NoCycleInductive below). All *)
144+
(* actions other than RcvMsg either leave upEdge unchanged or, in the *)
145+
(* case of SendAck removing p from the tree, leave p with no children *)
146+
(* (its OutEdges are quiescent), so any putative new closed set would *)
147+
(* already have been a closed set in the previous state. RcvMsg may *)
148+
(* attach a new process p to the tree with parent e[1]; if a closed set *)
149+
(* S' arose in the new state with p \in S', then by Counters and Inv2 *)
150+
(* conjunct 4 no other in-tree process points to p (since p was neutral, *)
151+
(* every OutEdge of p has sentUnacked = 0), so removing p from S' yields *)
152+
(* a smaller closed set in the previous state - contradicting the *)
153+
(* induction hypothesis. *)
147154
(***************************************************************************)
148-
LEMMA DT1FromInv2 == Inv2 => DT1Inv
149-
OMITTED
155+
NoCycle == \A S \in SUBSET (Procs \ {Leader}) :
156+
~ (/\ S # {}
157+
/\ \A q \in S : InTree(q) /\ upEdge[q][1] \in S)
150158

151159
LEMMA Inv2Inductive == Spec => []Inv2
152160
<1>1. Init => Inv2
@@ -531,8 +539,288 @@ LEMMA Inv2Inductive == Spec => []Inv2
531539
<2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6 DEF Next
532540
<1>. QED BY <1>1, <1>2, PTL DEF Spec
533541

542+
-----------------------------------------------------------------------------
543+
(***************************************************************************)
544+
(* Inductiveness of the auxiliary acyclicity invariant NoCycle (defined *)
545+
(* alongside Inv2 above). The proof depends on Inv2 (in particular *)
546+
(* Counters and conjunct 4) for the RcvMsg case. *)
547+
(***************************************************************************)
548+
LEMMA NoCycleInit == Init => NoCycle
549+
<1>. SUFFICES ASSUME Init,
550+
NEW S \in SUBSET (Procs \ {Leader}),
551+
S # {},
552+
\A q \in S : InTree(q) /\ upEdge[q][1] \in S
553+
PROVE FALSE
554+
BY DEF NoCycle
555+
<1>1. PICK q \in S : TRUE
556+
OBVIOUS
557+
<1>2. q \in Procs \ {Leader}
558+
OBVIOUS
559+
<1>3. upEdge[q] = NotAnEdge
560+
BY <1>2 DEF Init
561+
<1>4. ~ InTree(q)
562+
BY <1>3 DEF InTree
563+
<1>. QED BY <1>1, <1>4
564+
565+
LEMMA NoCycleStep == Inv2 /\ NoCycle /\ [Next]_vars => NoCycle'
566+
<1>. SUFFICES ASSUME Inv2, NoCycle, [Next]_vars
567+
PROVE NoCycle'
568+
OBVIOUS
569+
<1>. USE DEF Inv2, TypeOK, Counters, InTree, NotAnEdge
570+
<1>1. ASSUME NEW p \in Procs, SendMsg(p)
571+
PROVE NoCycle'
572+
<2>1. upEdge' = upEdge
573+
BY <1>1 DEF SendMsg
574+
<2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}),
575+
S # {},
576+
\A q \in S : InTree(q)' /\ upEdge'[q][1] \in S
577+
PROVE FALSE
578+
BY DEF NoCycle
579+
<2>2. \A q \in S : InTree(q) /\ upEdge[q][1] \in S
580+
BY <2>1
581+
<2>. QED BY <2>2 DEF NoCycle
582+
<1>2. ASSUME NEW p \in Procs, RcvAck(p)
583+
PROVE NoCycle'
584+
<2>1. upEdge' = upEdge
585+
BY <1>2 DEF RcvAck
586+
<2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}),
587+
S # {},
588+
\A q \in S : InTree(q)' /\ upEdge'[q][1] \in S
589+
PROVE FALSE
590+
BY DEF NoCycle
591+
<2>2. \A q \in S : InTree(q) /\ upEdge[q][1] \in S
592+
BY <2>1
593+
<2>. QED BY <2>2 DEF NoCycle
594+
<1>3. ASSUME NEW p \in Procs, Idle(p)
595+
PROVE NoCycle'
596+
<2>1. upEdge' = upEdge
597+
BY <1>3 DEF Idle
598+
<2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}),
599+
S # {},
600+
\A q \in S : InTree(q)' /\ upEdge'[q][1] \in S
601+
PROVE FALSE
602+
BY DEF NoCycle
603+
<2>2. \A q \in S : InTree(q) /\ upEdge[q][1] \in S
604+
BY <2>1
605+
<2>. QED BY <2>2 DEF NoCycle
606+
<1>4. CASE UNCHANGED vars
607+
<2>1. upEdge' = upEdge
608+
BY <1>4 DEF vars
609+
<2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}),
610+
S # {},
611+
\A q \in S : InTree(q)' /\ upEdge'[q][1] \in S
612+
PROVE FALSE
613+
BY DEF NoCycle
614+
<2>2. \A q \in S : InTree(q) /\ upEdge[q][1] \in S
615+
BY <2>1
616+
<2>. QED BY <2>2 DEF NoCycle
617+
<1>5. ASSUME NEW p \in Procs, SendAck(p)
618+
PROVE NoCycle'
619+
<2>0. PICK e \in InEdges(p) :
620+
/\ rcvdUnacked[e] > 0
621+
/\ rcvdUnacked' = [rcvdUnacked EXCEPT ![e] = @ - 1]
622+
/\ acks' = [acks EXCEPT ![e] = @ + 1]
623+
BY <1>5 DEF SendAck
624+
<2>1. upEdge' = IF neutral(p)' THEN [upEdge EXCEPT ![p] = NotAnEdge]
625+
ELSE upEdge
626+
BY <1>5 DEF SendAck
627+
<2>2. p # Leader
628+
<3>1. SUFFICES p = Leader => FALSE
629+
OBVIOUS
630+
<3>2. ASSUME p = Leader PROVE FALSE
631+
<4>1. e \in InEdges(Leader)
632+
BY <2>0, <3>2
633+
<4>2. InEdges(Leader) = {}
634+
BY EdgeFacts
635+
<4>. QED BY <4>1, <4>2
636+
<3>. QED BY <3>2
637+
<2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}),
638+
S # {},
639+
\A q \in S : InTree(q)' /\ upEdge'[q][1] \in S
640+
PROVE FALSE
641+
BY DEF NoCycle
642+
<2>case1. CASE ~ neutral(p)'
643+
<3>1. upEdge' = upEdge
644+
BY <2>1, <2>case1
645+
<3>2. \A q \in S : InTree(q) /\ upEdge[q][1] \in S
646+
BY <3>1
647+
<3>. QED BY <3>2 DEF NoCycle
648+
<2>case2. CASE neutral(p)'
649+
<3>1. upEdge' = [upEdge EXCEPT ![p] = NotAnEdge]
650+
BY <2>1, <2>case2
651+
<3>2. p \in DOMAIN upEdge
652+
BY <2>2
653+
<3>3. upEdge'[p] = NotAnEdge
654+
BY <3>1, <3>2
655+
<3>4. ~ InTree(p)'
656+
BY <3>3
657+
<3>5. p \notin S
658+
BY <3>4
659+
<3>6. \A q \in S : q # p
660+
BY <3>5
661+
<3>7. \A q \in S : upEdge'[q] = upEdge[q]
662+
BY <3>1, <3>6
663+
<3>8. \A q \in S : InTree(q) /\ upEdge[q][1] \in S
664+
BY <3>7
665+
<3>. QED BY <3>8 DEF NoCycle
666+
<2>. QED BY <2>case1, <2>case2
667+
<1>6. ASSUME NEW p \in Procs, RcvMsg(p)
668+
PROVE NoCycle'
669+
<2>0. PICK e \in InEdges(p) :
670+
/\ msgs[e] > 0
671+
/\ msgs' = [msgs EXCEPT ![e] = @ - 1]
672+
/\ rcvdUnacked' = [rcvdUnacked EXCEPT ![e] = @ + 1]
673+
/\ active' = [active EXCEPT ![p] = TRUE]
674+
/\ upEdge' = IF neutral(p) THEN [upEdge EXCEPT ![p] = e]
675+
ELSE upEdge
676+
/\ UNCHANGED <<acks, sentUnacked>>
677+
BY <1>6 DEF RcvMsg
678+
<2>1. p \in Procs \ {Leader} /\ e \in Edges /\ e[2] = p /\ e[1] # p /\ e[1] \in Procs
679+
BY <2>0, EdgeFacts DEF InEdges
680+
<2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}),
681+
S # {},
682+
\A q \in S : InTree(q)' /\ upEdge'[q][1] \in S
683+
PROVE FALSE
684+
BY DEF NoCycle
685+
<2>case1. CASE ~ neutral(p)
686+
<3>1. upEdge' = upEdge
687+
BY <2>0, <2>case1
688+
<3>2. \A q \in S : InTree(q) /\ upEdge[q][1] \in S
689+
BY <3>1
690+
<3>. QED BY <3>2 DEF NoCycle
691+
<2>case2. CASE neutral(p)
692+
<3>1. upEdge' = [upEdge EXCEPT ![p] = e]
693+
BY <2>0, <2>case2
694+
<3>2. p \in DOMAIN upEdge
695+
BY <2>1
696+
<3>caseA. CASE p \notin S
697+
<4>1. \A q \in S : q # p
698+
BY <3>caseA
699+
<4>2. \A q \in S : upEdge'[q] = upEdge[q]
700+
BY <3>1, <4>1
701+
<4>3. \A q \in S : InTree(q) /\ upEdge[q][1] \in S
702+
BY <4>2
703+
<4>. QED BY <4>3 DEF NoCycle
704+
<3>caseB. CASE p \in S
705+
<4>0. upEdge'[p] = e
706+
BY <3>1, <3>2
707+
<4>1. upEdge'[p][1] = e[1]
708+
BY <4>0
709+
<4>2. e[1] \in S
710+
BY <3>caseB, <4>1
711+
<4>3. e[1] # p
712+
BY <2>1
713+
<4>4. e[1] \in S \ {p}
714+
BY <4>2, <4>3
715+
<4>5. (S \ {p}) # {}
716+
BY <4>4
717+
<4>6. (S \ {p}) \in SUBSET (Procs \ {Leader})
718+
OBVIOUS
719+
<4>7. SUFFICES \A q \in S \ {p} : InTree(q) /\ upEdge[q][1] \in (S \ {p})
720+
BY <4>5, <4>6 DEF NoCycle
721+
<4>8. SUFFICES ASSUME NEW q \in S \ {p}
722+
PROVE InTree(q) /\ upEdge[q][1] \in (S \ {p})
723+
OBVIOUS
724+
<4>9. q \in S /\ q # p /\ q \in Procs \ {Leader}
725+
OBVIOUS
726+
<4>10. InTree(q)' /\ upEdge'[q][1] \in S
727+
BY <4>9
728+
<4>11. upEdge'[q] = upEdge[q]
729+
BY <3>1, <4>9
730+
<4>12. InTree(q)
731+
BY <4>10, <4>11
732+
<4>13. upEdge[q][1] \in S
733+
BY <4>10, <4>11
734+
<4>14. /\ upEdge[q] \in Edges
735+
/\ upEdge[q][2] = q
736+
/\ upEdge[q][1] \in Procs \ {q}
737+
/\ rcvdUnacked[upEdge[q]] >= 1
738+
BY <4>9, <4>12
739+
<4>15. sentUnacked[upEdge[q]] >= 1
740+
BY <4>14
741+
<4>16. upEdge[q][1] # p
742+
<5>1. SUFFICES ASSUME upEdge[q][1] = p PROVE FALSE
743+
OBVIOUS
744+
<5>2. upEdge[q] \in OutEdges(p)
745+
BY <5>1, <4>14 DEF OutEdges
746+
<5>3. sentUnacked[upEdge[q]] = 0
747+
BY <2>case2, <5>2 DEF neutral
748+
<5>. QED BY <4>15, <5>3
749+
<4>17. upEdge[q][1] \in (S \ {p})
750+
BY <4>13, <4>16
751+
<4>. QED BY <4>12, <4>17
752+
<3>. QED BY <3>caseA, <3>caseB
753+
<2>. QED BY <2>case1, <2>case2
754+
<1>. QED
755+
BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6 DEF Next
756+
757+
LEMMA NoCycleInductive == Spec => []NoCycle
758+
<1>1. Init => NoCycle
759+
BY NoCycleInit
760+
<1>2. Inv2 /\ NoCycle /\ [Next]_vars => NoCycle'
761+
BY NoCycleStep
762+
<1>3. Spec => []Inv2
763+
BY Inv2Inductive
764+
<1>. QED
765+
BY <1>1, <1>2, <1>3, PTL DEF Spec
766+
767+
(***************************************************************************)
768+
(* Discharge of DT1FromInv2 using Inv2 and the acyclicity invariant. *)
769+
(***************************************************************************)
770+
LEMMA DT1FromInv2 == Inv2 /\ NoCycle => DT1Inv
771+
<1>. SUFFICES ASSUME Inv2, NoCycle PROVE DT1Inv
772+
OBVIOUS
773+
<1>. USE DEF Inv2, TypeOK, Counters, InTree, NotAnEdge
774+
<1>. SUFFICES ASSUME neutral(Leader),
775+
NEW p0 \in Procs \ {Leader}
776+
PROVE neutral(p0)
777+
BY DEF DT1Inv
778+
<1>contra. ASSUME ~ neutral(p0) PROVE FALSE
779+
<2>. DEFINE S == {q \in Procs \ {Leader} : ~ neutral(q)}
780+
<2>3. p0 \in S
781+
BY <1>contra DEF S
782+
<2>4. S # {}
783+
BY <2>3
784+
<2>5. S \in SUBSET (Procs \ {Leader})
785+
BY DEF S
786+
<2>6. SUFFICES \A q \in S : InTree(q) /\ upEdge[q][1] \in S
787+
BY <2>4, <2>5 DEF NoCycle
788+
<2>7. SUFFICES ASSUME NEW q \in S
789+
PROVE InTree(q) /\ upEdge[q][1] \in S
790+
OBVIOUS
791+
<2>8. q \in Procs \ {Leader} /\ ~ neutral(q)
792+
BY DEF S
793+
<2>9. InTree(q)
794+
BY <2>8
795+
<2>10. /\ upEdge[q] \in Edges
796+
/\ upEdge[q][2] = q
797+
/\ upEdge[q][1] \in Procs \ {q}
798+
/\ rcvdUnacked[upEdge[q]] >= 1
799+
BY <2>8, <2>9
800+
<2>11. sentUnacked[upEdge[q]] >= 1
801+
BY <2>10
802+
<2>12. upEdge[q] \in OutEdges(upEdge[q][1])
803+
BY <2>10 DEF OutEdges
804+
<2>13. ~ neutral(upEdge[q][1])
805+
BY <2>11, <2>12 DEF neutral
806+
<2>14. upEdge[q][1] # Leader
807+
BY <2>13
808+
<2>15. upEdge[q][1] \in Procs \ {Leader}
809+
BY <2>10, <2>14
810+
<2>16. upEdge[q][1] \in S
811+
BY <2>13, <2>15 DEF S
812+
<2>. QED BY <2>9, <2>16
813+
<1>. QED BY <1>contra
814+
534815
THEOREM Thm_DT1Inv == Spec => []DT1Inv
535-
BY Inv2Inductive, DT1FromInv2, PTL
816+
<1>1. Spec => []Inv2
817+
BY Inv2Inductive
818+
<1>2. Spec => []NoCycle
819+
BY NoCycleInductive
820+
<1>3. Inv2 /\ NoCycle => DT1Inv
821+
BY DT1FromInv2
822+
<1>. QED
823+
BY <1>1, <1>2, <1>3, PTL
536824

537825
-----------------------------------------------------------------------------
538826
(***************************************************************************)

0 commit comments

Comments
 (0)