Experiment with Claude Opus 4.7 and TLAPS.

README.md

@@ -38,12 +38,12 @@ Here is a list of specs included in this repository which are validated by the C
 | [The Die Hard Problem](specifications/DieHard)                                                      | Leslie Lamport                                      |    ✔     |             |         |     ✔     |    ✔     |
 | [The Prisoners & Switches Puzzle](specifications/Prisoners)                                         | Leslie Lamport                                      |    ✔     |             |         |     ✔     |          |
 | [The Prisoners & Switch Puzzle](specifications/Prisoners_Single_Switch)                             | Florian Schanda                                     |    ✔     |             |         |     ✔     |          |
-| [Specs from Specifying Systems](specifications/SpecifyingSystems)                                   | Leslie Lamport                                      |    ✔     |             |         |     ✔     |    ✔     |
+| [Specs from Specifying Systems](specifications/SpecifyingSystems)                                   | Leslie Lamport                                      |    ✔     |     (✔)     |         |     ✔     |    ✔     |
 | [The Tower of Hanoi Puzzle](specifications/tower_of_hanoi)                                          | Markus Kuppe, Alexander Niederbühl                  |    ✔     |             |         |     ✔     |          |
 | [Missionaries and Cannibals](specifications/MissionariesAndCannibals)                               | Leslie Lamport                                      |    ✔     |             |         |     ✔     |    ✔     |
 | [Stone Scale Puzzle](specifications/Stones)                                                         | Leslie Lamport                                      |    ✔     |             |         |     ✔     |          |
 | [The Coffee Can Bean Problem](specifications/CoffeeCan)                                             | Andrew Helwer                                       |    ✔     |             |         |     ✔     |    ✔     |
-| [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a)                | Stephan Merz, Leslie Lamport, Markus Kuppe          |    ✔     |             |   (✔)   |     ✔     |          |
+| [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a)                | Stephan Merz, Leslie Lamport, Markus Kuppe          |    ✔     |      ✔      |   (✔)   |     ✔     |          |
 | [The Moving Cat Puzzle](specifications/Moving_Cat_Puzzle)                                           | Florian Schanda                                     |    ✔     |             |         |     ✔     |    ✔     |
 | [The Boulangerie Algorithm](specifications/Bakery-Boulangerie)                                      | Leslie Lamport, Stephan Merz                        |          |      ✔      |    ✔    |     ✔     |          |
 | [Misra Reachability Algorithm](specifications/MisraReachability)                                    | Leslie Lamport                                      |          |      ✔      |    ✔    |     ✔     |    ✔     |
@@ -61,14 +61,14 @@ Here is a list of specs included in this repository which are validated by the C
 | [Dijkstra's Mutual Exclusion Algorithm](specifications/dijkstra-mutex)                              | Leslie Lamport                                      |          |             |    ✔    |     ✔     |          |
 | [The Echo Algorithm](specifications/echo)                                                           | Stephan Merz                                        |          |             |    ✔    |     ✔     |          |
 | [The TLC Safety Checking Algorithm](specifications/TLC)                                             | Markus Kuppe                                        |          |             |    ✔    |     ✔     |          |
-| [Transaction Commit Models](specifications/transaction_commit)                                      | Leslie Lamport, Jim Gray, Murat Demirbas            |          |             |    ✔    |     ✔     |    ✔     |
+| [Transaction Commit Models](specifications/transaction_commit)                                      | Leslie Lamport, Jim Gray, Murat Demirbas            |          |     (✔)     |    ✔    |     ✔     |    ✔     |
 | [The Slush Protocol](specifications/SlushProtocol)                                                  | Andrew Helwer                                       |          |             |    ✔    |     ✔     |          |
 | [Minimal Circular Substring](specifications/LeastCircularSubstring)                                 | Andrew Helwer                                       |          |             |    ✔    |     ✔     |          |
-| [Snapshot Key-Value Store](specifications/KeyValueStore)                                            | Andrew Helwer, Murat Demirbas                       |          |             |    ✔    |     ✔     |          |
+| [Snapshot Key-Value Store](specifications/KeyValueStore)                                            | Andrew Helwer, Murat Demirbas                       |          |      ✔      |    ✔    |     ✔     |          |
 | [Chang-Roberts Algorithm for Leader Election in a Ring](specifications/chang_roberts)               | Stephan Merz                                        |          |             |    ✔    |     ✔     |    ✔     |
 | [MultiPaxos in SMR-Style](specifications/MultiPaxos-SMR)                                            | Guanzhou Hu                                         |          |             |    ✔    |     ✔     |          |
 | [Einstein's Riddle](specifications/EinsteinRiddle)                                                  | Isaac DeFrain, Giuliano Losa                        |          |             |         |           |    ✔     |
-| [Resource Allocator](specifications/allocator)                                                      | Stephan Merz                                        |          |             |         |     ✔     |          |
+| [Resource Allocator](specifications/allocator)                                                      | Stephan Merz                                        |          |     (✔)     |         |     ✔     |          |
 | [Transitive Closure](specifications/TransitiveClosure)                                              | Stephan Merz                                        |          |             |         |     ✔     |          |
 | [Atomic Commitment Protocol](specifications/acp)                                                    | Stephan Merz                                        |          |             |         |     ✔     |    ✔     |
 | [SWMR Shared Memory Disk Paxos](specifications/diskpaxos)                                           | Leslie Lamport, Giuliano Losa                       |          |             |         |     ✔     |          |
@@ -97,7 +97,7 @@ Here is a list of specs included in this repository which are validated by the C
 | [Conway's Game of Life](specifications/GameOfLife)                                                  | Mariusz Ryndzionek                                  |          |             |         |     ✔     |          |
 | [Chameneos, a Concurrency Game](specifications/Chameneos)                                           | Mariusz Ryndzionek                                  |          |             |         |     ✔     |          |
 | [PCR Testing for Snippets of DNA](specifications/glowingRaccoon)                                    | Martin Harrison                                     |          |             |         |     ✔     |    ✔     |
-| [RFC 3506: Voucher Transaction System](specifications/byihive)                                      | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani |          |             |         |     ✔     |          |
+| [RFC 3506: Voucher Transaction System](specifications/byihive)                                      | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani |          |     (✔)     |         |     ✔     |          |
 | [Yo-Yo Leader Election](specifications/YoYo)                                                        | Ludovic Yvoz, Stephan Merz                          |          |             |         |      ✔    |          |
 | [TCP as defined in RFC 9293](specifications/tcp)                                                    | Markus Kuppe                                        |          |             |         |      ✔    |    ✔     |
 | [B-trees](specifications/btree)                                                                     | Lorin Hochstein                                     |          |             |         |      ✔    |          |

specifications/KeyValueStore/KeyValueStore_proof.tla

@@ -0,0 +1,43 @@
+------------------------- MODULE KeyValueStore_proof -----------------------
+(***************************************************************************)
+(* TLAPS proof of                                                          *)
+(*   THEOREM Spec => [](TypeInvariant /\ TxLifecycle)                      *)
+(* stated in KeyValueStore.tla.                                            *)
+(***************************************************************************)
+EXTENDS KeyValueStore, TLAPS
+
+Inv == TypeInvariant /\ TxLifecycle
+
+THEOREM TypeAndLifecycle == Spec => []Inv
+<1>1. Init => Inv
+  BY DEF Init, Inv, TypeInvariant, TxLifecycle, Store
+<1>2. Inv /\ [Next]_<<store, tx, snapshotStore, written, missed>> => Inv'
+  <2> SUFFICES ASSUME Inv,
+                      [Next]_<<store, tx, snapshotStore, written, missed>>
+               PROVE  Inv'
+    OBVIOUS
+  <2>. USE DEF Inv, TypeInvariant, TxLifecycle, Store
+  <2>1. ASSUME NEW t \in TxId, OpenTx(t)
+        PROVE  Inv'
+    BY <2>1 DEF OpenTx
+  <2>2. ASSUME NEW t \in tx, NEW k \in Key, NEW v \in Val, Add(t, k, v)
+        PROVE  Inv'
+    BY <2>2 DEF Add
+  <2>3. ASSUME NEW t \in tx, NEW k \in Key, NEW v \in Val, Update(t, k, v)
+        PROVE  Inv'
+    BY <2>3 DEF Update
+  <2>4. ASSUME NEW t \in tx, NEW k \in Key, Remove(t, k)
+        PROVE  Inv'
+    BY <2>4 DEF Remove
+  <2>5. ASSUME NEW t \in tx, RollbackTx(t)
+        PROVE  Inv'
+    BY <2>5 DEF RollbackTx
+  <2>6. ASSUME NEW t \in tx, CloseTx(t)
+        PROVE  Inv'
+    BY <2>6 DEF CloseTx
+  <2>7. CASE UNCHANGED <<store, tx, snapshotStore, written, missed>>
+    BY <2>7
+  <2>. QED  BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7 DEF Next
+<1>. QED  BY <1>1, <1>2, PTL DEF Spec, Inv
+
+============================================================================

specifications/KeyValueStore/manifest.json

@@ -28,6 +28,14 @@
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/KeyValueStore/KeyValueStore_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:05"
+      }
+    },
     {
       "path": "specifications/KeyValueStore/MCKVS.tla",
       "features": [],

specifications/MisraReachability/ParReachProofs.tla

@@ -15,7 +15,7 @@ LEMMA TypeInvariant == Spec  => []Inv
 <1>3. QED
   BY <1>1, <1>2, PTL DEF Spec
 
-THEOREM Spec => R!Init /\ [][R!Next]_R!vars
+THEOREM RefinementSafety == Spec => R!Init /\ [][R!Next]_R!vars
 <1>1. Init => R!Init
     BY ProcsAssump DEF Init, R!Init, pcBar, vrootBar, ProcSet  
 <1>2. Inv /\ [Next]_vars => [R!Next]_R!vars

specifications/MisraReachability/ReachableProofs.tla

@@ -194,7 +194,7 @@ THEOREM Thm3 == Spec => []Inv3
     BY <1>1, <1>2, Thm2, PTL DEF Spec
 
 
-THEOREM Spec => []((pc = "Done") => (marked = Reachable))
+THEOREM Thm4 == Spec => []((pc = "Done") => (marked = Reachable))
   (*************************************************************************)
   (* This theorem follows easily from the invariance of Inv1 and Inv3 and  *)
   (* the trivial result Reachable3 of module ReachabilityProofs that       *)
@@ -209,6 +209,13 @@ THEOREM Spec => []((pc = "Done") => (marked = Reachable))
     BY Reachable3 DEF Inv3  
   <1>3. QED
     BY <1>1, <1>2, Thm1, Thm3, PTL
+
+(***************************************************************************)
+(* The same property restated under the spec's PartialCorrectness name,    *)
+(* matching the THEOREM stub at the bottom of Reachable.tla.               *)
+(***************************************************************************)
+THEOREM PartialCorrectnessThm == Spec => []PartialCorrectness
+BY Thm4, PTL DEF PartialCorrectness
 =============================================================================
 \* Modification History
 \* Last modified Sun Apr 14 16:24:32 PDT 2019 by lamport

specifications/PaxosHowToWinATuringAward/Voting.tla

@@ -25,7 +25,8 @@ CONSTANTS Value, Acceptor, Quorum
 (* element (an acceptor) in common.  Think of a quorum as a set consisting *)
 (* of a majority (more than half) of the acceptors.                        *)
 (***************************************************************************)
-ASSUME /\ \A Q \in Quorum : Q \subseteq Acceptor
+ASSUME QuorumAssumption ==
+       /\ \A Q \in Quorum : Q \subseteq Acceptor
        /\ \A Q1, Q2 \in Quorum : Q1 \cap Q2 /= {} 
 
 (***************************************************************************)

specifications/PaxosHowToWinATuringAward/Voting_proof.tla

@@ -0,0 +1,142 @@
+--------------------------- MODULE Voting_proof ----------------------------
+(***************************************************************************)
+(* TLAPS proofs of theorems stated in Voting.tla.  The spec is essentially *)
+(* the same as Paxos/Voting.tla; the proofs are direct ports.              *)
+(*                                                                         *)
+(*   AllSafeAtZero    (Band E)                                             *)
+(*   ChoosableThm     (Band E)                                             *)
+(*   ShowsSafety      (Band M)                                             *)
+(*                                                                         *)
+(* Invariance and Implementation depend on a SafeAtMonotone lemma not yet *)
+(* established; see Paxos/Voting_proof.tla for the same deferral.         *)
+(***************************************************************************)
+EXTENDS Voting
+
+LEMMA QuorumNonEmpty == \A Q \in Quorum : Q # {}
+BY QuorumAssumption
+
+(***************************************************************************)
+(*                              HELPERS                                    *)
+(***************************************************************************)
+
+THEOREM AllSafeAtZero_T == \A v \in Value : SafeAt(0, v)
+BY DEF SafeAt
+
+THEOREM ChoosableThm_T ==
+    \A b \in Ballot, v \in Value : ChosenAt(b, v) => NoneOtherChoosableAt(b, v)
+<1>1. SUFFICES ASSUME NEW b \in Ballot, NEW v \in Value, ChosenAt(b, v)
+               PROVE  NoneOtherChoosableAt(b, v)
+  OBVIOUS
+<1>2. PICK Q \in Quorum : \A a \in Q : VotedFor(a, b, v)
+  BY <1>1 DEF ChosenAt
+<1>. QED  BY <1>2 DEF NoneOtherChoosableAt
+
+(***************************************************************************)
+(* OneValuePerBallot in ASSUME/PROVE form.                                *)
+(***************************************************************************)
+LEMMA OneValuePerBallotApply ==
+  ASSUME OneValuePerBallot,
+         NEW a1 \in Acceptor, NEW a2 \in Acceptor, NEW bb \in Ballot,
+         NEW v1 \in Value, NEW v2 \in Value,
+         VotedFor(a1, bb, v1), VotedFor(a2, bb, v2)
+  PROVE  v1 = v2
+BY DEF OneValuePerBallot
+
+(***************************************************************************)
+(* Convenience: any two quorums intersect in at least one acceptor.        *)
+(***************************************************************************)
+LEMMA QuorumIntersect ==
+  ASSUME NEW Q1 \in Quorum, NEW Q2 \in Quorum
+  PROVE  \E a \in Q1 \cap Q2 : a \in Acceptor
+<1>1. Q1 \cap Q2 # {}
+  BY QuorumAssumption
+<1>2. PICK a \in Q1 \cap Q2 : TRUE
+  BY <1>1
+<1>3. a \in Acceptor
+  BY <1>2, QuorumAssumption
+<1>. QED  BY <1>2, <1>3
+
+(***************************************************************************)
+(*                          ShowsSafety   (Band M)                         *)
+(***************************************************************************)
+
+THEOREM ShowsSafety_T ==
+    Inv => \A Q \in Quorum, b \in Ballot, v \in Value :
+              ShowsSafeAt(Q, b, v) => SafeAt(b, v)
+<1>0. SUFFICES ASSUME Inv,
+                      NEW Q \in Quorum, NEW b \in Ballot, NEW v \in Value,
+                      ShowsSafeAt(Q, b, v)
+               PROVE  SafeAt(b, v)
+  OBVIOUS
+<1>0a. TypeOK /\ VotesSafe /\ OneValuePerBallot
+  BY <1>0 DEF Inv
+<1>1. \A a \in Q : maxBal[a] >= b
+  BY <1>0 DEF ShowsSafeAt
+<1>2. PICK c \in -1..(b-1) :
+            /\ (c /= -1) => \E a \in Q : VotedFor(a, c, v)
+            /\ \A d \in (c+1)..(b-1), a \in Q : DidNotVoteAt(a, d)
+  BY <1>0 DEF ShowsSafeAt
+<1>3. Q \subseteq Acceptor
+  BY QuorumAssumption
+<1>4. SUFFICES ASSUME NEW c0 \in 0..(b-1)
+                PROVE  NoneOtherChoosableAt(c0, v)
+  BY DEF SafeAt
+<1>5. b \in Nat /\ c0 \in Nat
+  BY DEF Ballot
+<1>6. CASE c0 > c
+  <2>1. c0 \in (c+1)..(b-1)
+    BY <1>5, <1>2, <1>6
+  <2>2. \A a \in Q : DidNotVoteAt(a, c0)
+    BY <1>2, <2>1
+  <2>3. \A a \in Q : maxBal[a] \in Ballot \cup {-1}
+    BY <1>3, <1>0a DEF TypeOK
+  <2>4. \A a \in Q : maxBal[a] > c0
+    BY <1>1, <2>3, <1>5, <1>6 DEF Ballot
+  <2>5. \A a \in Q : VotedFor(a, c0, v) \/ CannotVoteAt(a, c0)
+    BY <2>2, <2>4 DEF CannotVoteAt
+  <2>. QED  BY <2>5 DEF NoneOtherChoosableAt
+<1>7. CASE c0 = c
+  <2>1. c \in Nat
+    BY <1>5, <1>7
+  <2>2. c \in Ballot
+    BY <2>1 DEF Ballot
+  <2>3. PICK aStar \in Q : VotedFor(aStar, c, v)
+    BY <1>2, <1>5, <1>7
+  <2>4. aStar \in Acceptor
+    BY <1>3, <2>3
+  <2>5. \A a \in Q : VotedFor(a, c, v) \/ DidNotVoteAt(a, c)
+    <3> SUFFICES ASSUME NEW a \in Q,
+                         ~ DidNotVoteAt(a, c)
+                  PROVE  VotedFor(a, c, v)
+      OBVIOUS
+    <3>1. PICK w \in Value : VotedFor(a, c, w)
+      BY DEF DidNotVoteAt
+    <3>2. a \in Acceptor
+      BY <1>3
+    <3>3. w = v
+      BY <2>3, <2>4, <3>1, <3>2, <2>2, <1>0a, OneValuePerBallotApply
+    <3>. QED  BY <3>1, <3>3
+  <2>6. \A a \in Q : maxBal[a] \in Ballot \cup {-1}
+    BY <1>3, <1>0a DEF TypeOK
+  <2>7. \A a \in Q : maxBal[a] > c
+    BY <1>1, <2>6, <1>5, <1>7, <2>1 DEF Ballot
+  <2>8. \A a \in Q : VotedFor(a, c, v) \/ CannotVoteAt(a, c)
+    BY <2>5, <2>7 DEF CannotVoteAt
+  <2>. QED  BY <2>8, <1>7 DEF NoneOtherChoosableAt
+<1>8. CASE c0 < c
+  <2>1. c \in Nat /\ c0 < c
+    BY <1>5, <1>8
+  <2>2. c \in Ballot
+    BY <2>1 DEF Ballot
+  <2>3. PICK aStar \in Q : VotedFor(aStar, c, v)
+    BY <1>2, <1>5, <1>8
+  <2>4. aStar \in Acceptor
+    BY <1>3, <2>3
+  <2>5. SafeAt(c, v)
+    BY <2>3, <2>4, <2>2, <1>0a DEF VotesSafe
+  <2>6. c0 \in 0..(c-1)
+    BY <1>5, <2>1
+  <2>. QED  BY <2>5, <2>6 DEF SafeAt
+<1>. QED  BY <1>6, <1>7, <1>8
+
+============================================================================

specifications/PaxosHowToWinATuringAward/manifest.json

@@ -78,6 +78,14 @@
       "proof": {
         "runtime": "00:00:01"
       }
+    },
+    {
+      "path": "specifications/PaxosHowToWinATuringAward/Voting_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:30"
+      }
     }
   ]
-}
+}

specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface_proof.tla

@@ -0,0 +1,14 @@
+------------------------ MODULE AsynchInterface_proof ----------------------
+(***************************************************************************)
+(* TLAPS proof of the theorem stated in AsynchInterface.tla.               *)
+(***************************************************************************)
+EXTENDS AsynchInterface, TLAPS
+
+THEOREM TypeCorrect == Spec => []TypeInvariant
+<1>1. Init => TypeInvariant
+  BY DEF Init, TypeInvariant
+<1>2. TypeInvariant /\ [Next]_<<val, rdy, ack>> => TypeInvariant'
+  BY DEF TypeInvariant, Next, Send, Rcv
+<1>. QED  BY <1>1, <1>2, PTL DEF Spec
+
+============================================================================