Skip to content

Commit 1b395ed

Browse files
lemmyclaude
lemmy
and
claude
committed
v38 (Termination): Prove termination of the BlockingQueuePoisonApple spec.
TLAPS proof of all safety properties of (non-trivial/non-textbook) BlockingQueuePoisonApple, including the termination property that every consumer eventually dies after eating M Poison Apple slices. Co-authored-by: Claude Opus 4.7 <claude@anthropic.com>
1 parent 5cfaaa3 commit 1b395ed

3 files changed

Lines changed: 326 additions & 1 deletion

File tree

‎.github/workflows/main.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ jobs:
1818
- name: Install TLAPS
1919
run: tar -xzf tlapm-1.6.0-pre-x86_64-linux-gnu.tar.gz
2020
- name: Run TLAPS
21-
run: tlapm/bin/tlapm --cleanfp -I CommunityModules/ BlockingQueue.tla BlockingQueueSplit.tla BlockingQueueFair.tla
21+
run: tlapm/bin/tlapm --cleanfp -I CommunityModules/ BlockingQueue.tla BlockingQueueSplit.tla BlockingQueueFair.tla BlockingQueuePoisonApple_proofs.tla
2222
- name: Get (nightly) TLC
2323
run: wget https://nightly.tlapl.us/dist/tla2tools.jar
2424
- name: Run TLC

‎BlockingQueuePoisonApple_proofs.tla‎

Lines changed: 319 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,319 @@
1+
------------------- MODULE BlockingQueuePoisonApple_proofs ------------------
2+
(***************************************************************************)
3+
(* TLAPS proofs for the BlockingQueuePoisonApple module. Kept in a *)
4+
(* separate file so that the main specification stays free of TLAPS- *)
5+
(* related INSTANCE statements and assumptions. *)
6+
(* *)
7+
(* Run with *)
8+
(* tlapm --nofp -I /path/to/CommunityModules/modules *)
9+
(* BlockingQueuePoisonApple_proofs.tla *)
10+
(* so that the CommunityModules theorem files *)
11+
(* (FunctionTheorems with SumFunction theorems) are visible to TLAPS. *)
12+
(***************************************************************************)
13+
EXTENDS BlockingQueuePoisonApple
14+
15+
INSTANCE TLAPS
16+
INSTANCE FiniteSetTheorems
17+
INSTANCE SequenceTheorems
18+
INSTANCE FunctionTheorems
19+
20+
ASSUME FinAssumption ==
21+
/\ IsFiniteSet(Producers)
22+
/\ IsFiniteSet(Consumers)
23+
/\ Poison \notin Producers
24+
25+
(***************************************************************************)
26+
(* Step 1: TypeInv is itself inductive and is therefore a stand-alone *)
27+
(* invariant of Spec . *)
28+
(***************************************************************************)
29+
LEMMA TypeInvInit == Init => TypeInv
30+
BY Assumption, FinAssumption, FS_CardinalityType, EmptySeq DEF TypeInv, Init
31+
32+
LEMMA TypeInvInductive == TypeInv /\ [Next]_vars => TypeInv'
33+
<1> USE Assumption, FinAssumption, FS_CardinalityType
34+
DEF TypeInv, vars, NotifyOther, Wait
35+
<1> SUFFICES ASSUME TypeInv, [Next]_vars PROVE TypeInv' OBVIOUS
36+
<1>1. ASSUME NEW p \in Producers, Put(p, p) PROVE TypeInv'
37+
BY <1>1, AppendProperties DEF Put
38+
<1>2. ASSUME NEW c \in Consumers, Get(c) PROVE TypeInv'
39+
BY <1>2, HeadTailProperties DEF Get
40+
<1>. QED BY <1>1, <1>2 DEF Next
41+
42+
LEMMA TypeCorrect == Spec => []TypeInv
43+
BY TypeInvInit, TypeInvInductive, PTL DEF Spec
44+
45+
(***************************************************************************)
46+
(* Step 2: NoDeadlock follows from a strengthened invariant DInv that *)
47+
(* contains the two existential clauses guarding the empty / full buffer. *)
48+
(***************************************************************************)
49+
DInv ==
50+
/\ NoDeadlock
51+
/\ (buffer = <<>>) => \E p \in Producers : p \notin waitSet
52+
/\ (Len(buffer) = BufCapacity) => \E c \in Consumers : c \notin waitSet
53+
54+
THEOREM Safety == Spec => []NoDeadlock
55+
<1> USE Assumption, FinAssumption
56+
DEF TypeInv, NoDeadlock, DInv, vars, Wait, NotifyOther
57+
<1>1. Init => DInv BY EmptySeq DEF Init
58+
<1>2. TypeInv /\ DInv /\ [Next]_vars => DInv'
59+
<2> SUFFICES ASSUME TypeInv, DInv, [Next]_vars PROVE DInv' OBVIOUS
60+
<2>1. ASSUME NEW p \in Producers, Put(p, p) PROVE DInv' BY <2>1 DEF Put
61+
<2>2. ASSUME NEW c \in Consumers, Get(c) PROVE DInv' BY <2>2 DEF Get
62+
<2>. QED BY <2>1, <2>2 DEF Next
63+
<1>. QED BY <1>1, <1>2, TypeCorrect, PTL DEF Spec
64+
65+
(***************************************************************************)
66+
(* Step 3: QueueEmpty. Strengthen QueueEmpty into the inductive QInv: *)
67+
(* (A) Cardinality(PoisonsInBuf) + SumFunction(prod) = SumFunction(cons).*)
68+
(* The total of the remaining producer credits prod[p] plus the *)
69+
(* number of Poison items in the buffer equals the total of the *)
70+
(* remaining consumer credits cons[c] . *)
71+
(* (B) FIFO ordering. Every non-Poison item in the buffer is followed *)
72+
(* by a Poison further back, or some producer is still active. *)
73+
(* Together (A) and (B) force buffer to be empty whenever ap = ac = {}. *)
74+
(***************************************************************************)
75+
76+
\* Index set of Poison occurrences in the buffer.
77+
PoisonSet(buf) == { i \in 1..Len(buf) : buf[i] = Poison }
78+
PoisonsInBuf == PoisonSet(buffer)
79+
80+
QInv ==
81+
/\ Cardinality(PoisonsInBuf) + SumFunction(prod) = SumFunction(cons)
82+
/\ \A i \in 1..Len(buffer) : buffer[i] # Poison =>
83+
(\E p \in Producers : prod[p] > 0)
84+
\/ (\E j \in (i+1)..Len(buffer) : buffer[j] = Poison)
85+
86+
(***************************************************************************)
87+
(* Auxiliary lemmas about PoisonSet under Append and Tail. *)
88+
(***************************************************************************)
89+
90+
LEMMA PoisonSetFinite ==
91+
ASSUME NEW buf \in Seq(Producers \cup {Poison})
92+
PROVE IsFiniteSet(PoisonSet(buf))
93+
BY FS_Interval, FS_Subset DEF PoisonSet
94+
95+
LEMMA PoisonAppendOther ==
96+
ASSUME NEW buf \in Seq(Producers \cup {Poison}),
97+
NEW x \in Producers \cup {Poison}, x # Poison
98+
PROVE PoisonSet(Append(buf, x)) = PoisonSet(buf)
99+
BY AppendProperties, LenProperties DEF PoisonSet
100+
101+
LEMMA PoisonAppendPoison ==
102+
ASSUME NEW buf \in Seq(Producers \cup {Poison})
103+
PROVE /\ PoisonSet(Append(buf, Poison)) = PoisonSet(buf) \cup {Len(buf) + 1}
104+
/\ Cardinality(PoisonSet(Append(buf, Poison)))
105+
= Cardinality(PoisonSet(buf)) + 1
106+
<1>1. PoisonSet(Append(buf, Poison)) = PoisonSet(buf) \cup {Len(buf) + 1}
107+
BY AppendProperties, LenProperties DEF PoisonSet
108+
<1>2. (Len(buf) + 1) \notin PoisonSet(buf)
109+
BY LenProperties DEF PoisonSet
110+
<1>. QED BY <1>1, <1>2, PoisonSetFinite, FS_AddElement
111+
112+
LEMMA PoisonTail ==
113+
ASSUME NEW buf \in Seq(Producers \cup {Poison}), buf # <<>>
114+
PROVE Cardinality(PoisonSet(Tail(buf)))
115+
= Cardinality(PoisonSet(buf)) - (IF Head(buf) = Poison THEN 1 ELSE 0)
116+
<1> USE FinAssumption
117+
<1> DEFINE n == Len(buf)
118+
<1> DEFINE Shift == { j \in 2..n : buf[j] = Poison }
119+
<1>1. /\ Len(Tail(buf)) = n - 1 /\ n \in Nat /\ n >= 1
120+
/\ \A i \in 1..(n-1) : Tail(buf)[i] = buf[i + 1]
121+
/\ Head(buf) = buf[1]
122+
BY HeadTailProperties, LenProperties, EmptySeq
123+
<1>2. IsFiniteSet(Shift)
124+
BY FS_Interval, FS_Subset
125+
<1>3. PoisonSet(Tail(buf)) = { i \in 1..(n - 1) : buf[i + 1] = Poison }
126+
BY <1>1 DEF PoisonSet
127+
<1>4. Cardinality(PoisonSet(Tail(buf))) = Cardinality(Shift)
128+
<2> DEFINE f == [i \in PoisonSet(Tail(buf)) |-> i + 1]
129+
<2>1. f \in Bijection(PoisonSet(Tail(buf)), Shift)
130+
<3>1. f \in [PoisonSet(Tail(buf)) -> Shift] BY <1>3, <1>1
131+
<3>2. \A i, j \in PoisonSet(Tail(buf)) : f[i] = f[j] => i = j BY <1>3
132+
<3>3. \A k \in Shift : \E i \in PoisonSet(Tail(buf)) : f[i] = k
133+
<4> SUFFICES ASSUME NEW k \in Shift
134+
PROVE \E i \in PoisonSet(Tail(buf)) : f[i] = k
135+
OBVIOUS
136+
<4>1. (k - 1) \in PoisonSet(Tail(buf)) /\ f[k - 1] = k
137+
BY <1>3, <1>1
138+
<4>. QED BY <4>1
139+
<3>. QED BY <3>1, <3>2, <3>3, Fun_IsBij
140+
<2>2. IsFiniteSet(PoisonSet(Tail(buf)))
141+
BY <1>3, <1>1, FS_Interval, FS_Subset
142+
<2>. QED BY <2>1, <2>2, FS_Bijection DEF ExistsBijection
143+
<1>5. CASE Head(buf) = Poison
144+
<2>1. PoisonSet(buf) = Shift \cup {1}
145+
<3> SUFFICES ASSUME NEW i \in 1..n
146+
PROVE (buf[i] = Poison) <=> (i \in Shift \/ i = 1)
147+
BY DEF PoisonSet
148+
<3>. QED BY <1>1, <1>5
149+
<2>. QED BY <2>1, <1>4, <1>5, <1>2, FS_AddElement, FS_CardinalityType
150+
<1>6. CASE Head(buf) # Poison
151+
<2>1. PoisonSet(buf) = Shift
152+
<3> SUFFICES ASSUME NEW i \in 1..n
153+
PROVE (buf[i] = Poison) <=> i \in Shift
154+
BY DEF PoisonSet
155+
<3>. QED BY <1>1, <1>6
156+
<2>. QED BY <2>1, <1>4, <1>6, <1>2, FS_CardinalityType
157+
<1>. QED BY <1>5, <1>6
158+
159+
(***************************************************************************)
160+
(* The QInv components are well-typed. *)
161+
(***************************************************************************)
162+
LEMMA QInvTypes ==
163+
ASSUME TypeInv
164+
PROVE /\ SumFunction(prod) \in Nat
165+
/\ SumFunction(cons) \in Nat
166+
/\ Cardinality(PoisonsInBuf) \in Nat
167+
BY FinAssumption, FS_CardinalityType, SumFunctionNat, PoisonSetFinite
168+
DEF TypeInv, PoisonsInBuf
169+
170+
(***************************************************************************)
171+
(* Main inductive proof. *)
172+
(***************************************************************************)
173+
THEOREM QueueEmptyTheorem == Spec => QueueEmpty
174+
<1> DEFINE Inv == TypeInv /\ QInv
175+
<1> USE Assumption, FinAssumption, FS_CardinalityType
176+
DEF TypeInv, vars, NotifyOther, Wait, ap, ac, QueueEmpty, QInv
177+
<1>1. Init => Inv
178+
<2> SUFFICES ASSUME Init PROVE Inv OBVIOUS
179+
<2>1. TypeInv BY EmptySeq DEF Init
180+
<2>2. PoisonsInBuf = {} /\ Cardinality(PoisonsInBuf) = 0
181+
BY EmptySeq, FS_EmptySet DEF PoisonsInBuf, PoisonSet, Init
182+
<2>3. SumFunction(prod) = Cardinality(Consumers) * Cardinality(Producers)
183+
BY SumFunctionConst DEF Init
184+
<2>4. SumFunction(cons) = Cardinality(Producers) * Cardinality(Consumers)
185+
BY SumFunctionConst DEF Init
186+
<2>. QED BY <2>1, <2>2, <2>3, <2>4, EmptySeq DEF Init
187+
<1>2. Inv /\ [Next]_vars => Inv'
188+
<2> SUFFICES ASSUME Inv, [Next]_vars PROVE Inv' OBVIOUS
189+
<2>0. TypeInv' BY TypeInvInductive
190+
<2> USE QInvTypes DEF Inv
191+
<2>1. ASSUME NEW p \in Producers, Put(p, p) PROVE QInv'
192+
<3> USE <2>1
193+
<3>0. /\ prod \in [Producers -> 0..Cardinality(Consumers)]
194+
/\ buffer \in Seq(Producers \cup {Poison})
195+
/\ p \in Producers \cup {Poison}
196+
/\ DOMAIN prod = Producers
197+
BY DEF TypeInv
198+
<3>1. CASE /\ Len(buffer) < BufCapacity
199+
/\ buffer' = Append(buffer, p)
200+
/\ UNCHANGED prod
201+
/\ NotifyOther(Consumers)
202+
/\ UNCHANGED <<cons>>
203+
<4> USE <3>1
204+
<4>1. p # Poison BY DEF TypeInv
205+
<4>2. PoisonsInBuf' = PoisonsInBuf
206+
BY <4>1, <3>0, PoisonAppendOther DEF PoisonsInBuf
207+
<4>3. \A i \in 1..Len(buffer') : buffer'[i] # Poison =>
208+
(\E q \in Producers : prod'[q] > 0)
209+
\/ (\E j \in (i+1)..Len(buffer') : buffer'[j] = Poison)
210+
BY DEF Put
211+
<4>. QED BY <4>2, <4>3
212+
<3>2. CASE /\ Len(buffer) < BufCapacity
213+
/\ buffer' = Append(buffer, Poison)
214+
/\ prod' = [ prod EXCEPT ![p] = @ - 1]
215+
/\ NotifyOther(Consumers)
216+
/\ UNCHANGED <<cons>>
217+
<4> USE <3>2
218+
<4>1. SumFunction(prod') = SumFunction(prod) - 1
219+
BY <3>0, SumFunctionExcept
220+
<4>2. Cardinality(PoisonsInBuf') = Cardinality(PoisonsInBuf) + 1
221+
BY <3>0, PoisonAppendPoison DEF PoisonsInBuf
222+
<4>3. \A i \in 1..Len(buffer') : buffer'[i] # Poison =>
223+
\E j \in (i+1)..Len(buffer') : buffer'[j] = Poison
224+
<5> SUFFICES ASSUME NEW i \in 1..Len(buffer'), buffer'[i] # Poison
225+
PROVE \E j \in (i+1)..Len(buffer') : buffer'[j] = Poison
226+
OBVIOUS
227+
<5>1. /\ Len(buffer') = Len(buffer) + 1
228+
/\ buffer'[Len(buffer) + 1] = Poison
229+
BY AppendProperties, <3>0
230+
<5>2. (Len(buffer) + 1) \in (i+1)..Len(buffer') BY <5>1
231+
<5>. QED BY <5>1, <5>2
232+
<4>. QED BY <4>1, <4>2, <4>3
233+
<3>3. CASE /\ Len(buffer) = BufCapacity
234+
/\ Wait(p)
235+
/\ UNCHANGED prod
236+
/\ UNCHANGED <<cons>>
237+
BY <3>3 DEF Wait, PoisonsInBuf, PoisonSet
238+
<3>. QED BY <3>1, <3>2, <3>3 DEF Put
239+
<2>2. ASSUME NEW c \in Consumers, Get(c) PROVE QInv'
240+
<3> USE <2>2
241+
<3>0. /\ cons \in [Consumers -> 0..Cardinality(Producers)]
242+
/\ buffer \in Seq(Producers \cup {Poison})
243+
/\ DOMAIN cons = Consumers
244+
BY DEF TypeInv
245+
\* Helper for the FIFO part of QInv: when buffer' = Tail(buffer), any
246+
\* non-Poison item in buffer' shifts down from a non-Poison item in
247+
\* buffer that was witnessed by a Poison further back.
248+
<3>F. ASSUME /\ buffer # <<>>
249+
/\ buffer' = Tail(buffer)
250+
/\ UNCHANGED prod
251+
PROVE \A i \in 1..Len(buffer') : buffer'[i] # Poison =>
252+
(\E q \in Producers : prod'[q] > 0)
253+
\/ (\E j \in (i+1)..Len(buffer') : buffer'[j] = Poison)
254+
<4> USE <3>F
255+
<4>1. /\ Len(buffer') = Len(buffer) - 1
256+
/\ \A k \in 1..Len(buffer') : buffer'[k] = buffer[k+1]
257+
BY HeadTailProperties, <3>0
258+
<4> SUFFICES ASSUME NEW i \in 1..Len(buffer'), buffer'[i] # Poison
259+
PROVE (\E q \in Producers : prod'[q] > 0)
260+
\/ (\E j \in (i+1)..Len(buffer') : buffer'[j] = Poison)
261+
OBVIOUS
262+
<4>2. (i+1) \in 1..Len(buffer) /\ buffer[i+1] # Poison
263+
BY <4>1
264+
<4>3. (\E q \in Producers : prod[q] > 0)
265+
\/ (\E j \in (i+2)..Len(buffer) : buffer[j] = Poison)
266+
BY <4>2
267+
<4>4. ASSUME NEW j \in (i+2)..Len(buffer), buffer[j] = Poison
268+
PROVE \E j2 \in (i+1)..Len(buffer') : buffer'[j2] = Poison
269+
<5>1. (j-1) \in (i+1)..Len(buffer') /\ buffer'[j-1] = buffer[j]
270+
BY <4>1
271+
<5>. QED BY <5>1, <4>4
272+
<4>. QED BY <4>3, <4>4
273+
<3>1. CASE /\ buffer # <<>>
274+
/\ buffer' = Tail(buffer)
275+
/\ NotifyOther(Producers)
276+
/\ Head(buffer) # Poison
277+
/\ UNCHANGED <<prod, cons>>
278+
<4> USE <3>1
279+
<4>1. PoisonsInBuf' = PoisonSet(Tail(buffer)) BY DEF PoisonsInBuf
280+
<4>2. Cardinality(PoisonsInBuf') = Cardinality(PoisonsInBuf)
281+
BY <3>0, PoisonTail, <4>1 DEF PoisonsInBuf
282+
<4>. QED BY <4>2, <3>F
283+
<3>2. CASE /\ buffer # <<>>
284+
/\ buffer' = Tail(buffer)
285+
/\ NotifyOther(Producers)
286+
/\ Head(buffer) = Poison
287+
/\ cons' = [ cons EXCEPT ![c] = @ - 1]
288+
/\ UNCHANGED <<prod>>
289+
<4> USE <3>2
290+
<4>1. SumFunction(cons') = SumFunction(cons) - 1
291+
BY <3>0, SumFunctionExcept
292+
<4>2. /\ PoisonsInBuf' = PoisonSet(Tail(buffer))
293+
/\ Cardinality(PoisonSet(Tail(buffer)))
294+
= Cardinality(PoisonSet(buffer)) - 1
295+
BY <3>0, PoisonTail DEF PoisonsInBuf
296+
<4>. QED BY <4>1, <4>2, <3>F DEF PoisonsInBuf
297+
<3>3. CASE /\ buffer = <<>>
298+
/\ Wait(c)
299+
/\ UNCHANGED <<prod, cons>>
300+
BY <3>3 DEF Wait, PoisonsInBuf, PoisonSet
301+
<3>. QED BY <3>1, <3>2, <3>3 DEF Get
302+
<2>3. CASE UNCHANGED vars
303+
BY <2>3 DEF PoisonsInBuf, PoisonSet
304+
<2>. QED BY <2>0, <2>1, <2>2, <2>3 DEF Next
305+
<1>3. Inv => (ap \cup ac = {} => buffer = <<>>)
306+
<2> SUFFICES ASSUME Inv, ap \cup ac = {}, buffer # <<>> PROVE FALSE OBVIOUS
307+
<2>1. /\ \A p \in Producers : prod[p] = 0
308+
/\ \A c \in Consumers : cons[c] = 0
309+
OBVIOUS
310+
<2>2. SumFunction(prod) = 0 /\ SumFunction(cons) = 0
311+
BY <2>1, SumFunctionZero
312+
<2>3. PoisonsInBuf = {}
313+
BY <2>2, QInvTypes, FS_EmptySet, PoisonSetFinite DEF PoisonsInBuf
314+
<2>4. 1 \in 1..Len(buffer) /\ buffer[1] # Poison
315+
BY <2>3, EmptySeq DEF PoisonsInBuf, PoisonSet
316+
<2>. QED BY <2>1, <2>3, <2>4 DEF PoisonsInBuf, PoisonSet
317+
<1>. QED BY <1>1, <1>2, <1>3, PTL DEF Spec
318+
319+
=============================================================================

‎README.md‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,12 @@ This tutorial is work in progress. More chapters will be added in the future. In
1313

1414
--------------------------------------------------------------------------
1515

16+
### v38 (Termination): Prove termination of the BlockingQueuePoisonApple spec.
17+
18+
A TLAPS proof of all safety properties of `BlockingQueuePoisonApple`, including its termination property: every consumer eventually dies after eating `M` Poison Apple slices, where `M` is the number of producers. The proof lives in a separate `BlockingQueuePoisonApple_proofs.tla` module so the main spec stays free of TLAPS-specific declarations.
19+
20+
Notably, [Claude Opus 4.7](https://www.anthropic.com/) and I together found the inductive invariant and built the entire proof in mere hours. Compare this to the v33 refinement proof (pre-AI), which took roughly three weeks of manual labour to find the right invariants and to nudge the back-end provers across the finish line. Beyond the obvious productivity gain, the AI was particularly useful for proposing candidate invariants, splitting goals into the right intermediate lemmas, and recalling the exact CommunityModules / TLAPS standard-library theorems (`AppendProperties`, `HeadTailProperties`, `FS_CardinalityType`, the `SumFunction` lemmas, ...) needed at each step.
21+
1622
### v37 (Termination): Gradually terminate Consumers when Producers shutdown by sending Poison Apples.
1723

1824
Poison Pill variant where each producer sends `N` slices of a Poison Apple to `N` consumers. A consumer dies (terminates) when it has eaten `M` apple slices, where `M` is the number of producers.

0 commit comments

Comments
 (0)