Skip to content

Experiment with Claude Opus 4.7 and TLAPS. #211

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lemmy wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Experiment with Claude Opus 4.7 and TLAPS. #211

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
43 changes: 43 additions & 0 deletions specifications/KeyValueStore/KeyValueStore_proof.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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

============================================================================
484 changes: 484 additions & 0 deletions specifications/MultiCarElevator/Elevator_proof.tla
View file
Open in desktop

Large diffs are not rendered by default.

142 changes: 142 additions & 0 deletions specifications/PaxosHowToWinATuringAward/Voting_proof.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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

============================================================================
14 changes: 14 additions & 0 deletions specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface_proof.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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

============================================================================
14 changes: 14 additions & 0 deletions specifications/SpecifyingSystems/AsynchronousInterface/Channel_proof.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
--------------------------- MODULE Channel_proof ---------------------------
(***************************************************************************)
(* TLAPS proof of the theorem stated in Channel.tla. *)
(***************************************************************************)
EXTENDS Channel, TLAPS

THEOREM TypeCorrect == Spec => []TypeInvariant
<1>1. Init => TypeInvariant
BY DEF Init
<1>2. TypeInvariant /\ [Next]_chan => TypeInvariant'
BY DEF TypeInvariant, Next, Send, Rcv
<1>. QED BY <1>1, <1>2, PTL DEF Spec

============================================================================
76 changes: 76 additions & 0 deletions specifications/SpecifyingSystems/CachingMemory/InternalMemory_proof.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
------------------------- MODULE InternalMemory_proof ----------------------
(***************************************************************************)
(* TLAPS proof of *)
(* *)
(* THEOREM ISpec => []TypeInvariant *)
(* *)
(* stated in InternalMemory.tla. *)
(* *)
(* TypeInvariant alone is not inductive: in Do(p), the next-state *)
(* expression accesses buf[p].adr / buf[p].op, which only makes sense *)
(* when buf[p] is in MReq. We strengthen TypeInvariant with *)
(* BufConsistent, which records the buf typing for each value of ctl[p]. *)
(***************************************************************************)
EXTENDS InternalMemory, TLAPS

BufConsistent ==
/\ \A p \in Proc : (ctl[p] = "rdy") => (buf[p] \in Val \cup {NoVal})
/\ \A p \in Proc : (ctl[p] = "busy") => (buf[p] \in MReq)
/\ \A p \in Proc : (ctl[p] = "done") => (buf[p] \in Val \cup {NoVal})

Inv == TypeInvariant /\ BufConsistent

LEMMA InvInductive == ISpec => []Inv
<1>1. IInit => Inv
BY DEF IInit, Inv, TypeInvariant, BufConsistent
<1>2. Inv /\ [INext]_<<memInt, mem, ctl, buf>> => Inv'
<2> SUFFICES ASSUME Inv,
[INext]_<<memInt, mem, ctl, buf>>
PROVE Inv'
OBVIOUS
<2>. USE DEF Inv, TypeInvariant, BufConsistent
<2>1. ASSUME NEW p \in Proc, Req(p)
PROVE Inv'
\* After Req(p): ctl[p]' = "busy", buf[p]' \in MReq. For q # p,
\* ctl/buf unchanged. mem unchanged.
BY <2>1 DEF Req
<2>2. ASSUME NEW p \in Proc, Do(p)
PROVE Inv'
\* Pre: ctl[p] = "busy", so buf[p] \in MReq, hence buf[p].adr \in Adr,
\* and buf[p].op \in {"Rd","Wr"}.
<3>1. buf[p] \in MReq
BY <2>2 DEF Do
<3>2. buf[p].adr \in Adr /\ buf[p].op \in {"Rd","Wr"}
BY <3>1 DEF MReq
<3>3. CASE buf[p].op = "Wr"
\* mem' \in [Adr->Val] because we update at adr \in Adr to val \in Val.
\* buf[p]' = NoVal \in Val \cup {NoVal}, ctl[p]' = "done".
<4>1. buf[p].val \in Val
BY <3>1, <3>3 DEF MReq
<4>2. mem' = [mem EXCEPT ![buf[p].adr] = buf[p].val]
BY <2>2, <3>3 DEF Do
<4>3. mem' \in [Adr -> Val]
BY <3>2, <4>1, <4>2
<4>. QED BY <2>2, <3>3, <4>3 DEF Do
<3>4. CASE buf[p].op = "Rd"
\* mem' = mem. buf[p]' = mem[buf[p].adr] \in Val. ctl[p]' = "done".
<4>1. mem' = mem
BY <2>2, <3>4 DEF Do
<4>2. mem[buf[p].adr] \in Val
BY <3>2
<4>. QED BY <2>2, <3>4, <4>1, <4>2 DEF Do
<3>. QED BY <3>2, <3>3, <3>4
<2>3. ASSUME NEW p \in Proc, Rsp(p)
PROVE Inv'
\* ctl[p]' = "rdy"; buf, mem unchanged. buf[p] was \in Val \cup {NoVal}
\* (since pre ctl[p] = "done"), so it remains so under "rdy".
BY <2>3 DEF Rsp
<2>4. CASE UNCHANGED <<memInt, mem, ctl, buf>>
BY <2>4
<2>. QED BY <2>1, <2>2, <2>3, <2>4 DEF INext
<1>. QED BY <1>1, <1>2, PTL DEF ISpec

THEOREM TypeCorrect == ISpec => []TypeInvariant
BY InvInductive, PTL DEF Inv

============================================================================
14 changes: 14 additions & 0 deletions specifications/SpecifyingSystems/Composing/Channel_proof.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
--------------------------- MODULE Channel_proof ---------------------------
Comment thread
lemmy marked this conversation as resolved.
(***************************************************************************)
(* TLAPS proof of the theorem stated in Channel.tla. *)
(***************************************************************************)
EXTENDS Channel, TLAPS

THEOREM TypeCorrect == Spec => []TypeInvariant
<1>1. Init => TypeInvariant
BY DEF Init
<1>2. TypeInvariant /\ [Next]_chan => TypeInvariant'
BY DEF TypeInvariant, Next, Send, Rcv
<1>. QED BY <1>1, <1>2, PTL DEF Spec

============================================================================
14 changes: 14 additions & 0 deletions specifications/SpecifyingSystems/Composing/HourClock_proof.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
-------------------------- MODULE HourClock_proof --------------------------
(***************************************************************************)
(* TLAPS proof of the theorem stated in HourClock.tla. *)
(***************************************************************************)
EXTENDS HourClock, TLAPS

THEOREM HCini_Invariant == HC => []HCini
<1>1. HCini => HCini
OBVIOUS
<1>2. HCini /\ [HCnxt]_hr => HCini'
BY DEF HCini, HCnxt
<1>. QED BY <1>1, <1>2, PTL DEF HC

============================================================================
Loading
Loading