Skip to content

Commit 287133c

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). 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 - transaction_commit (TCommit, TwoPhase, PaxosCommit) A few obligations remain OMITTED: - Spec-specific: Inv2Next in Elevator_proof, Thm_TreeWithRoot and Thm_DT2 in EWD687a_proof, Refinement in EWD998PCal_proof. - Library-style: the multi-arg function-application unfolding lemmas in Elevator_proof, PermSeqsType in the allocator proofs, and MaximumProp in PaxosCommit_proof. Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
1 parent 8f94d8a commit 287133c

27 files changed

Lines changed: 4472 additions & 0 deletions

‎specifications/KeyValueStore/KeyValueStore_proof.tla‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
------------------------- MODULE KeyValueStore_proof -----------------------
2+
(***************************************************************************)
3+
(* TLAPS proof of *)
4+
(* THEOREM Spec => [](TypeInvariant /\ TxLifecycle) *)
5+
(* stated in KeyValueStore.tla. *)
6+
(***************************************************************************)
7+
EXTENDS KeyValueStore, TLAPS
8+
9+
Inv == TypeInvariant /\ TxLifecycle
10+
11+
THEOREM TypeAndLifecycle == Spec => []Inv
12+
<1>1. Init => Inv
13+
BY DEF Init, Inv, TypeInvariant, TxLifecycle, Store
14+
<1>2. Inv /\ [Next]_<<store, tx, snapshotStore, written, missed>> => Inv'
15+
<2> SUFFICES ASSUME Inv,
16+
[Next]_<<store, tx, snapshotStore, written, missed>>
17+
PROVE Inv'
18+
OBVIOUS
19+
<2>. USE DEF Inv, TypeInvariant, TxLifecycle, Store
20+
<2>1. ASSUME NEW t \in TxId, OpenTx(t)
21+
PROVE Inv'
22+
BY <2>1 DEF OpenTx
23+
<2>2. ASSUME NEW t \in tx, NEW k \in Key, NEW v \in Val, Add(t, k, v)
24+
PROVE Inv'
25+
BY <2>2 DEF Add
26+
<2>3. ASSUME NEW t \in tx, NEW k \in Key, NEW v \in Val, Update(t, k, v)
27+
PROVE Inv'
28+
BY <2>3 DEF Update
29+
<2>4. ASSUME NEW t \in tx, NEW k \in Key, Remove(t, k)
30+
PROVE Inv'
31+
BY <2>4 DEF Remove
32+
<2>5. ASSUME NEW t \in tx, RollbackTx(t)
33+
PROVE Inv'
34+
BY <2>5 DEF RollbackTx
35+
<2>6. ASSUME NEW t \in tx, CloseTx(t)
36+
PROVE Inv'
37+
BY <2>6 DEF CloseTx
38+
<2>7. CASE UNCHANGED <<store, tx, snapshotStore, written, missed>>
39+
BY <2>7
40+
<2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7 DEF Next
41+
<1>. QED BY <1>1, <1>2, PTL DEF Spec, Inv
42+
43+
============================================================================

‎specifications/MultiCarElevator/Elevator_proof.tla‎

Lines changed: 484 additions & 0 deletions
Large diffs are not rendered by default.

‎specifications/PaxosHowToWinATuringAward/Voting_proof.tla‎

Lines changed: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
1+
--------------------------- MODULE Voting_proof ----------------------------
2+
(***************************************************************************)
3+
(* TLAPS proofs of theorems stated in Voting.tla. The spec is essentially *)
4+
(* the same as Paxos/Voting.tla; the proofs are direct ports. *)
5+
(* *)
6+
(* AllSafeAtZero (Band E) *)
7+
(* ChoosableThm (Band E) *)
8+
(* ShowsSafety (Band M) *)
9+
(* *)
10+
(* Invariance and Implementation depend on a SafeAtMonotone lemma not yet *)
11+
(* established; see Paxos/Voting_proof.tla for the same deferral. *)
12+
(***************************************************************************)
13+
EXTENDS Voting
14+
15+
LEMMA QuorumNonEmpty == \A Q \in Quorum : Q # {}
16+
BY QuorumAssumption
17+
18+
(***************************************************************************)
19+
(* HELPERS *)
20+
(***************************************************************************)
21+
22+
THEOREM AllSafeAtZero_T == \A v \in Value : SafeAt(0, v)
23+
BY DEF SafeAt
24+
25+
THEOREM ChoosableThm_T ==
26+
\A b \in Ballot, v \in Value : ChosenAt(b, v) => NoneOtherChoosableAt(b, v)
27+
<1>1. SUFFICES ASSUME NEW b \in Ballot, NEW v \in Value, ChosenAt(b, v)
28+
PROVE NoneOtherChoosableAt(b, v)
29+
OBVIOUS
30+
<1>2. PICK Q \in Quorum : \A a \in Q : VotedFor(a, b, v)
31+
BY <1>1 DEF ChosenAt
32+
<1>. QED BY <1>2 DEF NoneOtherChoosableAt
33+
34+
(***************************************************************************)
35+
(* OneValuePerBallot in ASSUME/PROVE form. *)
36+
(***************************************************************************)
37+
LEMMA OneValuePerBallotApply ==
38+
ASSUME OneValuePerBallot,
39+
NEW a1 \in Acceptor, NEW a2 \in Acceptor, NEW bb \in Ballot,
40+
NEW v1 \in Value, NEW v2 \in Value,
41+
VotedFor(a1, bb, v1), VotedFor(a2, bb, v2)
42+
PROVE v1 = v2
43+
BY DEF OneValuePerBallot
44+
45+
(***************************************************************************)
46+
(* Convenience: any two quorums intersect in at least one acceptor. *)
47+
(***************************************************************************)
48+
LEMMA QuorumIntersect ==
49+
ASSUME NEW Q1 \in Quorum, NEW Q2 \in Quorum
50+
PROVE \E a \in Q1 \cap Q2 : a \in Acceptor
51+
<1>1. Q1 \cap Q2 # {}
52+
BY QuorumAssumption
53+
<1>2. PICK a \in Q1 \cap Q2 : TRUE
54+
BY <1>1
55+
<1>3. a \in Acceptor
56+
BY <1>2, QuorumAssumption
57+
<1>. QED BY <1>2, <1>3
58+
59+
(***************************************************************************)
60+
(* ShowsSafety (Band M) *)
61+
(***************************************************************************)
62+
63+
THEOREM ShowsSafety_T ==
64+
Inv => \A Q \in Quorum, b \in Ballot, v \in Value :
65+
ShowsSafeAt(Q, b, v) => SafeAt(b, v)
66+
<1>0. SUFFICES ASSUME Inv,
67+
NEW Q \in Quorum, NEW b \in Ballot, NEW v \in Value,
68+
ShowsSafeAt(Q, b, v)
69+
PROVE SafeAt(b, v)
70+
OBVIOUS
71+
<1>0a. TypeOK /\ VotesSafe /\ OneValuePerBallot
72+
BY <1>0 DEF Inv
73+
<1>1. \A a \in Q : maxBal[a] >= b
74+
BY <1>0 DEF ShowsSafeAt
75+
<1>2. PICK c \in -1..(b-1) :
76+
/\ (c /= -1) => \E a \in Q : VotedFor(a, c, v)
77+
/\ \A d \in (c+1)..(b-1), a \in Q : DidNotVoteAt(a, d)
78+
BY <1>0 DEF ShowsSafeAt
79+
<1>3. Q \subseteq Acceptor
80+
BY QuorumAssumption
81+
<1>4. SUFFICES ASSUME NEW c0 \in 0..(b-1)
82+
PROVE NoneOtherChoosableAt(c0, v)
83+
BY DEF SafeAt
84+
<1>5. b \in Nat /\ c0 \in Nat
85+
BY DEF Ballot
86+
<1>6. CASE c0 > c
87+
<2>1. c0 \in (c+1)..(b-1)
88+
BY <1>5, <1>2, <1>6
89+
<2>2. \A a \in Q : DidNotVoteAt(a, c0)
90+
BY <1>2, <2>1
91+
<2>3. \A a \in Q : maxBal[a] \in Ballot \cup {-1}
92+
BY <1>3, <1>0a DEF TypeOK
93+
<2>4. \A a \in Q : maxBal[a] > c0
94+
BY <1>1, <2>3, <1>5, <1>6 DEF Ballot
95+
<2>5. \A a \in Q : VotedFor(a, c0, v) \/ CannotVoteAt(a, c0)
96+
BY <2>2, <2>4 DEF CannotVoteAt
97+
<2>. QED BY <2>5 DEF NoneOtherChoosableAt
98+
<1>7. CASE c0 = c
99+
<2>1. c \in Nat
100+
BY <1>5, <1>7
101+
<2>2. c \in Ballot
102+
BY <2>1 DEF Ballot
103+
<2>3. PICK aStar \in Q : VotedFor(aStar, c, v)
104+
BY <1>2, <1>5, <1>7
105+
<2>4. aStar \in Acceptor
106+
BY <1>3, <2>3
107+
<2>5. \A a \in Q : VotedFor(a, c, v) \/ DidNotVoteAt(a, c)
108+
<3> SUFFICES ASSUME NEW a \in Q,
109+
~ DidNotVoteAt(a, c)
110+
PROVE VotedFor(a, c, v)
111+
OBVIOUS
112+
<3>1. PICK w \in Value : VotedFor(a, c, w)
113+
BY DEF DidNotVoteAt
114+
<3>2. a \in Acceptor
115+
BY <1>3
116+
<3>3. w = v
117+
BY <2>3, <2>4, <3>1, <3>2, <2>2, <1>0a, OneValuePerBallotApply
118+
<3>. QED BY <3>1, <3>3
119+
<2>6. \A a \in Q : maxBal[a] \in Ballot \cup {-1}
120+
BY <1>3, <1>0a DEF TypeOK
121+
<2>7. \A a \in Q : maxBal[a] > c
122+
BY <1>1, <2>6, <1>5, <1>7, <2>1 DEF Ballot
123+
<2>8. \A a \in Q : VotedFor(a, c, v) \/ CannotVoteAt(a, c)
124+
BY <2>5, <2>7 DEF CannotVoteAt
125+
<2>. QED BY <2>8, <1>7 DEF NoneOtherChoosableAt
126+
<1>8. CASE c0 < c
127+
<2>1. c \in Nat /\ c0 < c
128+
BY <1>5, <1>8
129+
<2>2. c \in Ballot
130+
BY <2>1 DEF Ballot
131+
<2>3. PICK aStar \in Q : VotedFor(aStar, c, v)
132+
BY <1>2, <1>5, <1>8
133+
<2>4. aStar \in Acceptor
134+
BY <1>3, <2>3
135+
<2>5. SafeAt(c, v)
136+
BY <2>3, <2>4, <2>2, <1>0a DEF VotesSafe
137+
<2>6. c0 \in 0..(c-1)
138+
BY <1>5, <2>1
139+
<2>. QED BY <2>5, <2>6 DEF SafeAt
140+
<1>. QED BY <1>6, <1>7, <1>8
141+
142+
============================================================================

‎specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface_proof.tla‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
------------------------ MODULE AsynchInterface_proof ----------------------
2+
(***************************************************************************)
3+
(* TLAPS proof of the theorem stated in AsynchInterface.tla. *)
4+
(***************************************************************************)
5+
EXTENDS AsynchInterface, TLAPS
6+
7+
THEOREM TypeCorrect == Spec => []TypeInvariant
8+
<1>1. Init => TypeInvariant
9+
BY DEF Init, TypeInvariant
10+
<1>2. TypeInvariant /\ [Next]_<<val, rdy, ack>> => TypeInvariant'
11+
BY DEF TypeInvariant, Next, Send, Rcv
12+
<1>. QED BY <1>1, <1>2, PTL DEF Spec
13+
14+
============================================================================

‎specifications/SpecifyingSystems/AsynchronousInterface/Channel_proof.tla‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
--------------------------- MODULE Channel_proof ---------------------------
2+
(***************************************************************************)
3+
(* TLAPS proof of the theorem stated in Channel.tla. *)
4+
(***************************************************************************)
5+
EXTENDS Channel, TLAPS
6+
7+
THEOREM TypeCorrect == Spec => []TypeInvariant
8+
<1>1. Init => TypeInvariant
9+
BY DEF Init
10+
<1>2. TypeInvariant /\ [Next]_chan => TypeInvariant'
11+
BY DEF TypeInvariant, Next, Send, Rcv
12+
<1>. QED BY <1>1, <1>2, PTL DEF Spec
13+
14+
============================================================================

‎specifications/SpecifyingSystems/CachingMemory/InternalMemory_proof.tla‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
------------------------- MODULE InternalMemory_proof ----------------------
2+
(***************************************************************************)
3+
(* TLAPS proof of *)
4+
(* *)
5+
(* THEOREM ISpec => []TypeInvariant *)
6+
(* *)
7+
(* stated in InternalMemory.tla. *)
8+
(* *)
9+
(* TypeInvariant alone is not inductive: in Do(p), the next-state *)
10+
(* expression accesses buf[p].adr / buf[p].op, which only makes sense *)
11+
(* when buf[p] is in MReq. We strengthen TypeInvariant with *)
12+
(* BufConsistent, which records the buf typing for each value of ctl[p]. *)
13+
(***************************************************************************)
14+
EXTENDS InternalMemory, TLAPS
15+
16+
BufConsistent ==
17+
/\ \A p \in Proc : (ctl[p] = "rdy") => (buf[p] \in Val \cup {NoVal})
18+
/\ \A p \in Proc : (ctl[p] = "busy") => (buf[p] \in MReq)
19+
/\ \A p \in Proc : (ctl[p] = "done") => (buf[p] \in Val \cup {NoVal})
20+
21+
Inv == TypeInvariant /\ BufConsistent
22+
23+
LEMMA InvInductive == ISpec => []Inv
24+
<1>1. IInit => Inv
25+
BY DEF IInit, Inv, TypeInvariant, BufConsistent
26+
<1>2. Inv /\ [INext]_<<memInt, mem, ctl, buf>> => Inv'
27+
<2> SUFFICES ASSUME Inv,
28+
[INext]_<<memInt, mem, ctl, buf>>
29+
PROVE Inv'
30+
OBVIOUS
31+
<2>. USE DEF Inv, TypeInvariant, BufConsistent
32+
<2>1. ASSUME NEW p \in Proc, Req(p)
33+
PROVE Inv'
34+
\* After Req(p): ctl[p]' = "busy", buf[p]' \in MReq. For q # p,
35+
\* ctl/buf unchanged. mem unchanged.
36+
BY <2>1 DEF Req
37+
<2>2. ASSUME NEW p \in Proc, Do(p)
38+
PROVE Inv'
39+
\* Pre: ctl[p] = "busy", so buf[p] \in MReq, hence buf[p].adr \in Adr,
40+
\* and buf[p].op \in {"Rd","Wr"}.
41+
<3>1. buf[p] \in MReq
42+
BY <2>2 DEF Do
43+
<3>2. buf[p].adr \in Adr /\ buf[p].op \in {"Rd","Wr"}
44+
BY <3>1 DEF MReq
45+
<3>3. CASE buf[p].op = "Wr"
46+
\* mem' \in [Adr->Val] because we update at adr \in Adr to val \in Val.
47+
\* buf[p]' = NoVal \in Val \cup {NoVal}, ctl[p]' = "done".
48+
<4>1. buf[p].val \in Val
49+
BY <3>1, <3>3 DEF MReq
50+
<4>2. mem' = [mem EXCEPT ![buf[p].adr] = buf[p].val]
51+
BY <2>2, <3>3 DEF Do
52+
<4>3. mem' \in [Adr -> Val]
53+
BY <3>2, <4>1, <4>2
54+
<4>. QED BY <2>2, <3>3, <4>3 DEF Do
55+
<3>4. CASE buf[p].op = "Rd"
56+
\* mem' = mem. buf[p]' = mem[buf[p].adr] \in Val. ctl[p]' = "done".
57+
<4>1. mem' = mem
58+
BY <2>2, <3>4 DEF Do
59+
<4>2. mem[buf[p].adr] \in Val
60+
BY <3>2
61+
<4>. QED BY <2>2, <3>4, <4>1, <4>2 DEF Do
62+
<3>. QED BY <3>2, <3>3, <3>4
63+
<2>3. ASSUME NEW p \in Proc, Rsp(p)
64+
PROVE Inv'
65+
\* ctl[p]' = "rdy"; buf, mem unchanged. buf[p] was \in Val \cup {NoVal}
66+
\* (since pre ctl[p] = "done"), so it remains so under "rdy".
67+
BY <2>3 DEF Rsp
68+
<2>4. CASE UNCHANGED <<memInt, mem, ctl, buf>>
69+
BY <2>4
70+
<2>. QED BY <2>1, <2>2, <2>3, <2>4 DEF INext
71+
<1>. QED BY <1>1, <1>2, PTL DEF ISpec
72+
73+
THEOREM TypeCorrect == ISpec => []TypeInvariant
74+
BY InvInductive, PTL DEF Inv
75+
76+
============================================================================

‎specifications/SpecifyingSystems/Composing/Channel_proof.tla‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
--------------------------- MODULE Channel_proof ---------------------------
2+
(***************************************************************************)
3+
(* TLAPS proof of the theorem stated in Channel.tla. *)
4+
(***************************************************************************)
5+
EXTENDS Channel, TLAPS
6+
7+
THEOREM TypeCorrect == Spec => []TypeInvariant
8+
<1>1. Init => TypeInvariant
9+
BY DEF Init
10+
<1>2. TypeInvariant /\ [Next]_chan => TypeInvariant'
11+
BY DEF TypeInvariant, Next, Send, Rcv
12+
<1>. QED BY <1>1, <1>2, PTL DEF Spec
13+
14+
============================================================================

‎specifications/SpecifyingSystems/Composing/HourClock_proof.tla‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
-------------------------- MODULE HourClock_proof --------------------------
2+
(***************************************************************************)
3+
(* TLAPS proof of the theorem stated in HourClock.tla. *)
4+
(***************************************************************************)
5+
EXTENDS HourClock, TLAPS
6+
7+
THEOREM HCini_Invariant == HC => []HCini
8+
<1>1. HCini => HCini
9+
OBVIOUS
10+
<1>2. HCini /\ [HCnxt]_hr => HCini'
11+
BY DEF HCini, HCnxt
12+
<1>. QED BY <1>1, <1>2, PTL DEF HC
13+
14+
============================================================================

0 commit comments

Comments
 (0)