Skip to content

Commit 0ff8795

Browse files
lemmyclaude
lemmy
and
claude
committed
Add TLAPS proof companions for example specifications
Each affected directory now has a `<Spec>_proof.tla` module that mechanically checks the safety obligations of its TLA+ specification (typically Spec => []TypeInvariant, plus any SafetyInvariant or strengthened inductive invariant the spec defines). The original specifications themselves are not modified by this commit; the prior commit names a few previously-anonymous `ASSUME` blocks that the proofs cite by reference. Specifications covered: - KeyValueStore - MultiCarElevator/Elevator - PaxosHowToWinATuringAward/Voting - SpecifyingSystems chapters: AsynchronousInterface, FIFO, HourClock, Composing, Liveness, RealTime, CachingMemory, TLC - TwoPhase - allocator (Simple, Scheduling, Implementation) - byihive/VoucherLifeCycle - ewd687a/EWD687a - ewd998/EWD998PCal and EWD998 (TerminationDetection lifted to Spec => []...) - transaction_commit (TCommit, TwoPhase, PaxosCommit) - CoffeeCan, DieHard, MissionariesAndCannibals, SpanTree (TypeInvariant / TypeOK) - spanning (SntMsg) and glowingRaccoon clean+stages (TypeOK + primerPositive + preservationInvariant) - ReadersWriters (TypeOK + Safety: mutex + at-most-one-writer) - CigaretteSmokers (TypeOK + AtMostOne) - LamportMutex (BoundedNetwork, via NetworkInv pigeonhole) - TeachingConcurrency/Simple and SimpleRegular (TypeOK and Inv exposed as named theorems matching the .cfg invariants) Proof-only assumptions added in `*_proof.tla` (not in the spec): - CigaretteSmokers_proof: IngredientsFinite (Cardinality is already used inside the spec's own ASSUME, so finiteness is implicit). - ReadersWriters_proof: NumActorsIsNat (NumActors \in Nat). - Elevator_proof: ElevatorFloorDisjoint (Floor \cap Elevator = {}; a TLC modelling convention not stated in the spec). - SchedulingAllocator_proof, AllocatorImplementation_proof: ClientsFinite (the spec only assumes Resources finite). - EWD687a_proof: ProcsFinite (finite process set). - glowingRaccoon clean_proof and stages_proof: ConstantsAreNat (DNA, PRIMER \in Nat; without this Spec => []TypeOK is false). Spec ASSUMEs restated under a name in the proof file (no new fact): - CigaretteSmokers_proof: OffersAssumption. - spanning_proof: NoPrntFact. - SpanTree_proof: ConstantsAssumption. - CoffeeCan_proof: MaxBeanFact. Non-trivial proof obligations discharged: - PaxosCommit_proof: MaximumProp -- the recursive `Maximum` operator is shown to return the largest element of its (non-empty, finite, integer >= -1) input via well-founded induction on the strict-subset ordering, going through a hand-proved recursion equation for the inner CHOOSE'd recursive function. - SchedulingAllocator_proof: PermSeqsType -- analogous well-founded structural induction over `PermSeqs(S)`, plus an explicit finiteness assumption on `Clients` (added in the proof file only). - AllocatorImplementation_proof: PermSeqsType -- the same proof threaded through the `Sched!` instance. One sub-step (`Sched!PermSeqs(S) = PermsFn(S)[S]`) remains OMITTED because tlapm's INSTANCE expansion currently mangles the inner LET binding inside the LET-bound recursive function. - EWD687a_proof: TreeNodesNonNeutral, TreeStructure, TreeIsTree, Inv2GivesTreeBody, SpecGivesAlwaysTreeBody -- the structural half of TreeWithRoot (graph + non-neutral conjuncts) discharged from the existing Inv1 / Inv2 / NoCycle invariants. - CRDT_proof: the four previously OMITTED Sum lemmas (SumType, SumIsZero, SumWeaklyMonotonic, SumStronglyMonotonic) are reduced to SumFunctionNat, SumFunctionZero, SumFunctionMonotonic, and SumFunctionStrictlyMonotonic in the community-modules FunctionTheorems (strengthened and CI-verified in tlaplus/CommunityModules#124) via the trivial unfolding Sum(f) = SumFunction(f); FiniteSetTheorems is dropped from EXTENDS accordingly. The downstream Measure*/Gossip* lemmas and the OGLiveness / Convergence theorems that already cited these now check end-to-end (280 obligations). Remaining OMITTED obligations: - Elevator_proof: Inv2Next (the inductive step for the strengthened Inv2; each of its ~10 conjuncts is proven preserved per-action individually, only the full assembly is left), and four narrow function-evaluation lemmas (GetDirectionEval, GetDistanceEval, CanServiceCallEval, PeopleWaitingEval) that unfold a multi-arg `f[a, b]` definition -- a known tlapm/SMT/Zenon/Isabelle gap, cf. https://discuss.tlapl.us/msg01519.html. - EWD687a_proof: AreConnectedToLeader (constructing the path to Leader by iterating upEdge needs SimplePath/Cardinality reasoning), Thm_TreeWithRoot's QED (bridges TreeWithRoot's `LET ... IN [](...)` shape and the equivalent `[](LET ... IN ...)` that PTL would consume), and Thm_DT2 (Spec => DT2; needs an inductive invariant over msgs/rcvdUnacked/acks/sentUnacked). - AllocatorImplementation_proof: PermSeqsIsPermsFn, the equality `Sched!PermSeqs(S) = PermsFn(S)[S]`, blocked by tlapm rendering the INSTANCE-expanded inner LET binding as a self-recursive CHOOSE. - EWD998PCal_proof: Refinement (Spec => EWD998Spec); per-disjunct step-simulation requires bag-level lemmas plus the EWD998-level invariant `B = Sum(counter, Node)` for the token-pass disjunct. Also, the unique-token preservation conjunct of NetworkOK is deferred in PCalTypeOKInductive. Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
1 parent 92cf6dd commit 0ff8795

41 files changed

Lines changed: 6614 additions & 8 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎specifications/CigaretteSmokers/CigaretteSmokers_proof.tla‎

Lines changed: 305 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,305 @@
1+
--------------------- MODULE CigaretteSmokers_proof ---------------------------
2+
(***************************************************************************)
3+
(* TLAPS proofs of *)
4+
(* *)
5+
(* Spec => []TypeOK *)
6+
(* Spec => []AtMostOne *)
7+
(* *)
8+
(* AtMostOne (at most one smoker is smoking) is inductive together with *)
9+
(* TypeOK once we know `Ingredients` is finite. *)
10+
(***************************************************************************)
11+
EXTENDS CigaretteSmokers, FiniteSets, FiniteSetTheorems, TLAPS
12+
13+
(***************************************************************************)
14+
(* Ingredients is implicitly finite: the spec uses Cardinality on it. *)
15+
(***************************************************************************)
16+
ASSUME IngredientsFinite == IsFiniteSet(Ingredients)
17+
18+
(***************************************************************************)
19+
(* Type correctness. The dealer disjunct dealer \in Offers \/ dealer = {} *)
20+
(* is preserved trivially since both actions either set dealer to {} or *)
21+
(* nondeterministically choose dealer' \in Offers. *)
22+
(***************************************************************************)
23+
THEOREM TypeCorrect == Spec => []TypeOK
24+
<1>1. Init => TypeOK
25+
BY DEF Init, TypeOK
26+
<1>2. TypeOK /\ [Next]_vars => TypeOK'
27+
<2>. SUFFICES ASSUME TypeOK, [Next]_vars PROVE TypeOK'
28+
OBVIOUS
29+
<2>. USE DEF TypeOK
30+
<2>1. CASE startSmoking
31+
<3>. USE <2>1 DEF startSmoking
32+
<3>1. smokers' \in [Ingredients -> [smoking : BOOLEAN]]
33+
OBVIOUS
34+
<3>2. dealer' = {}
35+
OBVIOUS
36+
<3>. QED BY <3>1, <3>2
37+
<2>2. CASE stopSmoking
38+
<3>. USE <2>2 DEF stopSmoking
39+
<3>1. smokers' \in [Ingredients -> [smoking : BOOLEAN]]
40+
<4>. DEFINE r == ChooseOne(Ingredients, LAMBDA x : smokers[x].smoking)
41+
<4>1. smokers' = [smokers EXCEPT ![r].smoking = FALSE]
42+
BY DEF stopSmoking
43+
<4>. QED BY <4>1
44+
<3>2. dealer' \in Offers \/ dealer' = {}
45+
OBVIOUS
46+
<3>. QED BY <3>1, <3>2
47+
<2>3. CASE UNCHANGED vars
48+
BY <2>3 DEF vars
49+
<2>. QED BY <2>1, <2>2, <2>3 DEF Next
50+
<1>. QED BY <1>1, <1>2, PTL DEF Spec
51+
52+
(***************************************************************************)
53+
(* AtMostOne: at most one smoker is smoking. *)
54+
(* Combined invariant with TypeOK (TypeOK is needed to type-check the *)
55+
(* set comprehension). *)
56+
(***************************************************************************)
57+
SmokingSet == {r \in Ingredients : smokers[r].smoking}
58+
59+
LEMMA SmokingSetFinite ==
60+
ASSUME TypeOK
61+
PROVE /\ IsFiniteSet(SmokingSet)
62+
/\ Cardinality(SmokingSet) \in Nat
63+
<1>1. SmokingSet \subseteq Ingredients
64+
BY DEF SmokingSet
65+
<1>2. IsFiniteSet(SmokingSet)
66+
BY <1>1, IngredientsFinite, FS_Subset
67+
<1>3. Cardinality(SmokingSet) \in Nat
68+
BY <1>2, FS_CardinalityType
69+
<1>. QED BY <1>2, <1>3
70+
71+
LEMMA AtMostOneViaSmokingSet == AtMostOne <=> Cardinality(SmokingSet) <= 1
72+
BY DEF AtMostOne, SmokingSet
73+
74+
(***************************************************************************)
75+
(* The spec's unnamed ASSUME extracted as a fact for use in proofs. *)
76+
(***************************************************************************)
77+
LEMMA OffersFact ==
78+
/\ Offers \subseteq SUBSET Ingredients
79+
/\ \A n \in Offers : Cardinality(n) = Cardinality(Ingredients) - 1
80+
BY OffersAssumption
81+
82+
(***************************************************************************)
83+
(* Cardinality(Ingredients) >= 1 follows from the existence of any *)
84+
(* dealer \in Offers (Offers is non-empty by Init's `dealer \in Offers`, *)
85+
(* but more directly: any d \in Offers has |d| = |Ingredients| - 1 \in Nat *)
86+
(* which implies |Ingredients| >= 1. We don't actually need this for the *)
87+
(* proof of AtMostOne, just for OffersFact reasoning). *)
88+
(***************************************************************************)
89+
90+
LEMMA UniqueComplement2 ==
91+
ASSUME TypeOK, dealer \in Offers
92+
PROVE Cardinality({r \in Ingredients : {r} \cup dealer = Ingredients}) = 1
93+
<1>. USE DEF TypeOK
94+
<1>1. dealer \in SUBSET Ingredients
95+
BY OffersFact
96+
<1>2. Cardinality(dealer) = Cardinality(Ingredients) - 1
97+
BY OffersFact
98+
<1>3. IsFiniteSet(dealer)
99+
BY <1>1, IngredientsFinite, FS_Subset
100+
<1>4. Cardinality(dealer) \in Nat
101+
BY <1>3, FS_CardinalityType
102+
<1>5. Cardinality(Ingredients) \in Nat
103+
BY IngredientsFinite, FS_CardinalityType
104+
<1>6. Cardinality(Ingredients) > Cardinality(dealer)
105+
BY <1>2, <1>4, <1>5
106+
<1>7. dealer # Ingredients
107+
BY <1>3, IngredientsFinite, <1>6, FS_Subset, <1>1
108+
<1>. DEFINE missing == Ingredients \ dealer
109+
<1>9. IsFiniteSet(missing)
110+
BY IngredientsFinite, FS_Difference
111+
<1>10. Cardinality(missing) = Cardinality(Ingredients) - Cardinality(dealer)
112+
<2>1. Ingredients \cap dealer = dealer
113+
BY <1>1
114+
<2>2. Cardinality(missing) =
115+
Cardinality(Ingredients) - Cardinality(Ingredients \cap dealer)
116+
BY IngredientsFinite, FS_Difference
117+
<2>. QED BY <2>1, <2>2
118+
<1>11. Cardinality(missing) = 1
119+
BY <1>2, <1>4, <1>5, <1>10
120+
<1>12. PICK m : missing = {m}
121+
BY <1>9, <1>11, FS_Singleton
122+
<1>13. m \in Ingredients /\ m \notin dealer
123+
<2>1. m \in missing BY <1>12
124+
<2>. QED BY <2>1
125+
<1>14. \A r \in Ingredients : ({r} \cup dealer = Ingredients) => r = m
126+
<2>. SUFFICES ASSUME NEW r \in Ingredients,
127+
{r} \cup dealer = Ingredients
128+
PROVE r = m
129+
OBVIOUS
130+
<2>1. m \in {r} \cup dealer
131+
BY <1>13
132+
<2>. QED BY <2>1, <1>13
133+
<1>15. \A r \in Ingredients : (r = m) => ({r} \cup dealer = Ingredients)
134+
<2>. SUFFICES {m} \cup dealer = Ingredients
135+
OBVIOUS
136+
<2>1. {m} \cup dealer \subseteq Ingredients
137+
BY <1>1, <1>13
138+
<2>2. Ingredients \subseteq {m} \cup dealer
139+
<3>. SUFFICES ASSUME NEW i \in Ingredients
140+
PROVE i \in {m} \cup dealer
141+
OBVIOUS
142+
<3>1. CASE i \in dealer BY <3>1
143+
<3>2. CASE i \notin dealer
144+
<4>. i \in missing BY <3>2
145+
<4>. i = m BY <1>12
146+
<4>. QED OBVIOUS
147+
<3>. QED BY <3>1, <3>2
148+
<2>. QED BY <2>1, <2>2
149+
<1>16. {r \in Ingredients : {r} \cup dealer = Ingredients} = {m}
150+
<2>1. \A r \in Ingredients :
151+
(r \in {r2 \in Ingredients : {r2} \cup dealer = Ingredients})
152+
<=> r = m
153+
BY <1>14, <1>15
154+
<2>2. {r \in Ingredients : {r} \cup dealer = Ingredients} \subseteq {m}
155+
BY <2>1
156+
<2>3. {m} \subseteq {r \in Ingredients : {r} \cup dealer = Ingredients}
157+
BY <2>1, <1>13
158+
<2>. QED BY <2>2, <2>3
159+
<1>17. Cardinality({m}) = 1
160+
BY FS_Singleton
161+
<1>. QED BY <1>16, <1>17
162+
163+
(***************************************************************************)
164+
(* The smoking set after `startSmoking` equals the set of ingredients *)
165+
(* that complete the dealer. *)
166+
(***************************************************************************)
167+
LEMMA StartSmokingSmokingSet ==
168+
ASSUME TypeOK, startSmoking
169+
PROVE /\ smokers' \in [Ingredients -> [smoking : BOOLEAN]]
170+
/\ {r \in Ingredients : smokers'[r].smoking}
171+
= {r \in Ingredients : {r} \cup dealer = Ingredients}
172+
<1>. USE DEF TypeOK, startSmoking
173+
<1>1. smokers' = [r \in Ingredients |->
174+
[smoking |-> {r} \cup dealer = Ingredients]]
175+
OBVIOUS
176+
<1>2. smokers' \in [Ingredients -> [smoking : BOOLEAN]]
177+
BY <1>1
178+
<1>3. \A r \in Ingredients :
179+
smokers'[r].smoking = ({r} \cup dealer = Ingredients)
180+
BY <1>1
181+
<1>. QED BY <1>2, <1>3
182+
183+
(***************************************************************************)
184+
(* The smoking set after `stopSmoking` is a subset of the previous one. *)
185+
(***************************************************************************)
186+
LEMMA StopSmokingSmokingSet ==
187+
ASSUME TypeOK, stopSmoking
188+
PROVE /\ smokers' \in [Ingredients -> [smoking : BOOLEAN]]
189+
/\ {r \in Ingredients : smokers'[r].smoking}
190+
\subseteq {r \in Ingredients : smokers[r].smoking}
191+
<1>. USE DEF TypeOK, stopSmoking
192+
<1>. DEFINE r0 == ChooseOne(Ingredients, LAMBDA x : smokers[x].smoking)
193+
<1>1. smokers' = [smokers EXCEPT ![r0].smoking = FALSE]
194+
OBVIOUS
195+
<1>2. smokers' \in [Ingredients -> [smoking : BOOLEAN]]
196+
BY <1>1
197+
<1>3. \A r \in Ingredients :
198+
/\ r # r0 => smokers'[r] = smokers[r]
199+
/\ r = r0 => smokers'[r] = [smokers[r0] EXCEPT !.smoking = FALSE]
200+
BY <1>1
201+
<1>4. \A r \in Ingredients :
202+
smokers'[r].smoking => smokers[r].smoking
203+
<2>. SUFFICES ASSUME NEW r \in Ingredients, smokers'[r].smoking
204+
PROVE smokers[r].smoking
205+
OBVIOUS
206+
<2>1. CASE r = r0
207+
<3>1. smokers'[r] = [smokers[r0] EXCEPT !.smoking = FALSE]
208+
BY <1>3, <2>1
209+
<3>2. smokers'[r].smoking = FALSE
210+
BY <3>1
211+
<3>. QED BY <3>2
212+
<2>2. CASE r # r0
213+
<3>1. smokers'[r] = smokers[r]
214+
BY <1>3, <2>2
215+
<3>. QED BY <3>1
216+
<2>. QED BY <2>1, <2>2
217+
<1>. QED BY <1>2, <1>4
218+
219+
(***************************************************************************)
220+
(* Main inductive invariant. *)
221+
(***************************************************************************)
222+
Inv == TypeOK /\ AtMostOne
223+
224+
THEOREM AtMostOneCorrect == Spec => []AtMostOne
225+
<1>1. Init => Inv
226+
<2>. SUFFICES ASSUME Init PROVE Inv
227+
OBVIOUS
228+
<2>. USE DEF Init, Inv, TypeOK
229+
<2>1. TypeOK
230+
OBVIOUS
231+
<2>2. {r \in Ingredients : smokers[r].smoking} = {}
232+
OBVIOUS
233+
<2>3. AtMostOne
234+
<3>1. Cardinality({}) = 0
235+
BY FS_EmptySet
236+
<3>. QED BY <2>2, <3>1 DEF AtMostOne
237+
<2>. QED BY <2>1, <2>3
238+
<1>2. Inv /\ [Next]_vars => Inv'
239+
<2>. SUFFICES ASSUME Inv, [Next]_vars PROVE Inv'
240+
OBVIOUS
241+
<2>. USE DEF Inv
242+
<2>typok. TypeOK'
243+
\* Re-derive type-correctness step inline.
244+
<3>1. CASE startSmoking
245+
<4>. USE <3>1 DEF startSmoking, TypeOK
246+
<4>1. smokers' \in [Ingredients -> [smoking : BOOLEAN]]
247+
OBVIOUS
248+
<4>2. dealer' = {}
249+
OBVIOUS
250+
<4>. QED BY <4>1, <4>2
251+
<3>2. CASE stopSmoking
252+
<4>. USE <3>2 DEF stopSmoking, TypeOK
253+
<4>. DEFINE r0 == ChooseOne(Ingredients, LAMBDA x : smokers[x].smoking)
254+
<4>1. smokers' = [smokers EXCEPT ![r0].smoking = FALSE]
255+
OBVIOUS
256+
<4>2. smokers' \in [Ingredients -> [smoking : BOOLEAN]]
257+
BY <4>1
258+
<4>3. dealer' \in Offers \/ dealer' = {}
259+
OBVIOUS
260+
<4>. QED BY <4>2, <4>3
261+
<3>3. CASE UNCHANGED vars
262+
BY <3>3 DEF vars, TypeOK
263+
<3>. QED BY <3>1, <3>2, <3>3 DEF Next
264+
<2>amo. AtMostOne'
265+
<3>1. CASE startSmoking
266+
<4>1. dealer \in Offers
267+
BY <3>1 DEF startSmoking, TypeOK
268+
<4>2. {r \in Ingredients : smokers'[r].smoking}
269+
= {r \in Ingredients : {r} \cup dealer = Ingredients}
270+
BY <3>1, StartSmokingSmokingSet DEF Inv
271+
<4>3. Cardinality({r \in Ingredients : {r} \cup dealer = Ingredients}) = 1
272+
BY <4>1, UniqueComplement2 DEF Inv
273+
<4>4. Cardinality({r \in Ingredients : smokers'[r].smoking}) = 1
274+
BY <4>2, <4>3
275+
<4>. QED BY <4>4 DEF AtMostOne
276+
<3>2. CASE stopSmoking
277+
<4>1. {r \in Ingredients : smokers'[r].smoking}
278+
\subseteq {r \in Ingredients : smokers[r].smoking}
279+
BY <3>2, StopSmokingSmokingSet DEF Inv
280+
<4>2. IsFiniteSet({r \in Ingredients : smokers[r].smoking})
281+
/\ IsFiniteSet({r \in Ingredients : smokers'[r].smoking})
282+
<5>1. {r \in Ingredients : smokers[r].smoking} \subseteq Ingredients
283+
OBVIOUS
284+
<5>2. {r \in Ingredients : smokers'[r].smoking} \subseteq Ingredients
285+
OBVIOUS
286+
<5>. QED BY <5>1, <5>2, IngredientsFinite, FS_Subset
287+
<4>3. Cardinality({r \in Ingredients : smokers'[r].smoking})
288+
<= Cardinality({r \in Ingredients : smokers[r].smoking})
289+
BY <4>1, <4>2, FS_Subset
290+
<4>4. Cardinality({r \in Ingredients : smokers[r].smoking}) <= 1
291+
BY DEF AtMostOne
292+
<4>5. Cardinality({r \in Ingredients : smokers'[r].smoking}) \in Nat
293+
/\ Cardinality({r \in Ingredients : smokers[r].smoking}) \in Nat
294+
BY <4>2, FS_CardinalityType
295+
<4>. QED BY <4>3, <4>4, <4>5 DEF AtMostOne
296+
<3>3. CASE UNCHANGED vars
297+
<4>. smokers' = smokers
298+
BY <3>3 DEF vars
299+
<4>. QED BY DEF AtMostOne
300+
<3>. QED BY <3>1, <3>2, <3>3 DEF Next
301+
<2>. QED BY <2>typok, <2>amo
302+
<1>3. Inv => AtMostOne
303+
BY DEF Inv
304+
<1>. QED BY <1>1, <1>2, <1>3, PTL DEF Spec
305+
============================================================================

0 commit comments

Comments
 (0)