Skip to content

Commit 480309d

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 7e6b6f7 commit 480309d

41 files changed

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

0 commit comments

Comments
 (0)