Skip to content

Commit 8f54595

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
abi: prove inductive-invariant soundness (TLA+ INV1) in Tlaiser.ABI.Semantics (#38)
Add a flagship machine-checked semantic proof raising the Tlaiser Idris2 ABI to Layer 2. Models a two-process lock-based mutual-exclusion state machine (the canonical PlusCal example) with an Init predicate, a nondeterministic Step relation, and an inductive Reachable closure. Headline theorem (safetySound): mutual exclusion (Safe) holds on every reachable state. The engine is invInductive (TLA+ INV1): a strengthened, genuinely inductive invariant Inv that couples "process is Critical" to "process holds the lock" holds initially (initEstablishes) and is preserved by every transition (stepPreserves), hence holds on all reachable states; Safe is derived from Inv (invImpliesSafe). Includes a sound+complete Dec (decSafe), a Result-valued certifier with soundness (certifyReachableSound), a positive control (a real reachable Critical state, proven Safe) and negative controls (the (Critical,Critical) state has no Safe proof and is unreachable). The "both critical" bad case has no constructor, so a deliberately false safety witness is rejected by idris2 (non-vacuity verified). Builds clean (idris2 0.7.0, zero warnings). Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx Co-authored-by: Claude <noreply@anthropic.com>
1 parent d8da9f8 commit 8f54595

2 files changed

Lines changed: 353 additions & 0 deletions

File tree

‎src/interface/abi/Tlaiser/ABI/Semantics.idr‎

Lines changed: 352 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,352 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
||| Flagship semantic proof for Tlaiser: inductive-invariant soundness.
5+
|||
6+
||| Tlaiser's headline is "extract state machines and model-check with
7+
||| TLA+/PlusCal". The single most important thing a model checker establishes
8+
||| about a safety property is that it is an *inductive invariant*: it holds in
9+
||| the initial state(s) and is preserved by every step of the next-state
10+
||| relation. From those two facts, TLA+'s INV1 rule concludes the property
11+
||| holds in *every reachable state*. This module models that argument faithfully
12+
||| and proves it for real, end to end, for a two-process lock-based
13+
||| mutual-exclusion machine (the canonical PlusCal example).
14+
|||
15+
||| Model (deliberately minimal but genuine):
16+
||| * `St` is a concrete state: a control location for each of two processes
17+
||| plus a single shared lock token.
18+
||| * `Init` is the initial-state relation.
19+
||| * `Step` is the next-state *relation* (nondeterministic; several enabled
20+
||| transitions per state), as in a real TLA+ spec.
21+
||| * `Reachable s` is the inductive closure of `Init` under `Step` — exactly
22+
||| the set of states a model checker explores.
23+
||| * `Safe` is the headline safety property: the two processes are never both
24+
||| in their critical section (mutual exclusion).
25+
||| * `Inv` is a *strengthened, genuinely inductive* invariant that couples
26+
||| "process is Critical" to "process holds the lock". `Safe` follows from
27+
||| `Inv`, and `Inv` is preserved by every step.
28+
|||
29+
||| Headline theorem (`safetySound`): the safety property holds on every
30+
||| reachable state. The engine of the proof is `invInductive` (INV1): an
31+
||| inductive invariant holding initially and preserved by Step holds on all
32+
||| reachable states.
33+
|||
34+
||| @see https://lamport.azurewebsites.net/tla/tla.html (INV1 inference rule)
35+
36+
module Tlaiser.ABI.Semantics
37+
38+
import Tlaiser.ABI.Types
39+
import Decidable.Equality
40+
41+
%default total
42+
43+
--------------------------------------------------------------------------------
44+
-- A faithful state-machine model
45+
--------------------------------------------------------------------------------
46+
47+
||| Per-process control location. Idle -> Waiting -> Critical -> Idle. This is
48+
||| the canonical PlusCal mutual-exclusion control flow.
49+
public export
50+
data Loc = Idle | Waiting | Critical
51+
52+
||| Lock token: Free, or Held by a specific process (P0 / P1). A single token,
53+
||| so at most one process can hold it — this is what enforces mutual exclusion.
54+
public export
55+
data Lock = Free | HeldBy0 | HeldBy1
56+
57+
||| A state of the machine: the control location of each of the two processes
58+
||| and the shared lock.
59+
public export
60+
record St where
61+
constructor MkSt
62+
p0 : Loc
63+
p1 : Loc
64+
lock : Lock
65+
66+
--------------------------------------------------------------------------------
67+
-- The initial-state predicate (Init) and next-state relation (Step)
68+
--------------------------------------------------------------------------------
69+
70+
||| `Init s` holds exactly for the unique initial state: both idle, lock free.
71+
public export
72+
data Init : St -> Type where
73+
InitState : Init (MkSt Idle Idle Free)
74+
75+
||| The next-state relation. Each constructor is one enabled transition. A state
76+
||| typically has several successors (nondeterminism), as in a real TLA+ spec.
77+
|||
78+
||| Mutual exclusion is enforced *structurally* by the lock: a process can only
79+
||| enter Critical when it acquires the (single) lock, and acquiring requires the
80+
||| lock to be Free. This is the protocol whose safety we prove.
81+
public export
82+
data Step : St -> St -> Type where
83+
||| P0 requests the lock: Idle -> Waiting (lock unchanged).
84+
P0Request : Step (MkSt Idle q l) (MkSt Waiting q l)
85+
||| P1 requests the lock: Idle -> Waiting (lock unchanged).
86+
P1Request : Step (MkSt q Idle l) (MkSt q Waiting l)
87+
||| P0 acquires the free lock and enters Critical.
88+
P0Acquire : Step (MkSt Waiting q Free) (MkSt Critical q HeldBy0)
89+
||| P1 acquires the free lock and enters Critical.
90+
P1Acquire : Step (MkSt q Waiting Free) (MkSt q Critical HeldBy1)
91+
||| P0 leaves Critical, releasing the lock it holds.
92+
P0Release : Step (MkSt Critical q HeldBy0) (MkSt Idle q Free)
93+
||| P1 leaves Critical, releasing the lock it holds.
94+
P1Release : Step (MkSt q Critical HeldBy1) (MkSt q Idle Free)
95+
96+
--------------------------------------------------------------------------------
97+
-- Reachability: the inductive closure of Init under Step
98+
--------------------------------------------------------------------------------
99+
100+
||| `Reachable s` : `s` is reachable from an initial state by zero or more steps.
101+
||| This is precisely the set of states a model checker explores.
102+
public export
103+
data Reachable : St -> Type where
104+
||| Every initial state is reachable.
105+
ReachInit : Init s -> Reachable s
106+
||| If `s` is reachable and `s` steps to `t`, then `t` is reachable.
107+
ReachStep : Reachable s -> Step s t -> Reachable t
108+
109+
--------------------------------------------------------------------------------
110+
-- The headline safety property: mutual exclusion
111+
--------------------------------------------------------------------------------
112+
113+
||| `Safe s` : the two processes are never *both* Critical. Phrased as a
114+
||| proposition with NO constructor for the bad case `(Critical, Critical)` —
115+
||| there is simply no way to inhabit `Safe (MkSt Critical Critical _)`.
116+
public export
117+
data Safe : St -> Type where
118+
||| P0 is not critical: safe regardless of P1.
119+
Safe0 : Not (a = Critical) -> Safe (MkSt a b l)
120+
||| P1 is not critical: safe regardless of P0.
121+
Safe1 : Not (b = Critical) -> Safe (MkSt a b l)
122+
123+
--------------------------------------------------------------------------------
124+
-- The strengthened, genuinely inductive invariant
125+
--------------------------------------------------------------------------------
126+
127+
||| `LocLock l lk` : a single process's location is consistent with whether it
128+
||| holds the lock token `lk`. "Critical iff holds the lock."
129+
||| Indexed by the lock-ownership boolean for THIS process.
130+
public export
131+
data Coherent0 : Loc -> Lock -> Type where
132+
||| P0 is Critical exactly when the lock is HeldBy0.
133+
C0CritHolds : Coherent0 Critical HeldBy0
134+
||| P0 is not Critical: the lock is held by someone else or free.
135+
C0NotCritFree : Coherent0 Idle Free
136+
C0NotCritFreeW: Coherent0 Waiting Free
137+
C0NotCrit1I : Coherent0 Idle HeldBy1
138+
C0NotCrit1W : Coherent0 Waiting HeldBy1
139+
140+
public export
141+
data Coherent1 : Loc -> Lock -> Type where
142+
C1CritHolds : Coherent1 Critical HeldBy1
143+
C1NotCritFree : Coherent1 Idle Free
144+
C1NotCritFreeW: Coherent1 Waiting Free
145+
C1NotCrit0I : Coherent1 Idle HeldBy0
146+
C1NotCrit0W : Coherent1 Waiting HeldBy0
147+
148+
||| The full inductive invariant: both processes are coherent with the lock.
149+
||| Because "Critical iff holds the lock" and the lock is a single token, both
150+
||| processes cannot be Critical at once. This makes `Inv` strong enough to be
151+
||| preserved by every step (genuinely inductive), and strong enough to imply
152+
||| the headline `Safe` property.
153+
public export
154+
data Inv : St -> Type where
155+
MkInv : Coherent0 a lk -> Coherent1 b lk -> Inv (MkSt a b lk)
156+
157+
--------------------------------------------------------------------------------
158+
-- Inv implies the headline safety property
159+
--------------------------------------------------------------------------------
160+
161+
||| If P0 is Critical it must hold the lock (HeldBy0); then P1's coherence with
162+
||| HeldBy0 forces P1 to be non-Critical. Hence mutual exclusion. This is where
163+
||| the strengthening pays off — `Safe` is a *consequence* of `Inv`.
164+
public export
165+
invImpliesSafe : Inv s -> Safe s
166+
invImpliesSafe (MkInv c0 c1) = case c1 of
167+
C1CritHolds => Safe0 (notCritWhenLock1 c0) -- lk = HeldBy1 => P0 not Critical
168+
C1NotCritFree => Safe1 (\case Refl impossible)
169+
C1NotCritFreeW => Safe1 (\case Refl impossible)
170+
C1NotCrit0I => Safe1 (\case Refl impossible)
171+
C1NotCrit0W => Safe1 (\case Refl impossible)
172+
where
173+
||| When the lock is HeldBy1, P0's coherence rules out P0 = Critical.
174+
notCritWhenLock1 : Coherent0 a HeldBy1 -> Not (a = Critical)
175+
notCritWhenLock1 C0NotCrit1I = \case Refl impossible
176+
notCritWhenLock1 C0NotCrit1W = \case Refl impossible
177+
178+
--------------------------------------------------------------------------------
179+
-- Decision procedure for the headline safety property (sound + complete)
180+
--------------------------------------------------------------------------------
181+
182+
||| Loc equality is decidable.
183+
locDecEq : (x : Loc) -> (y : Loc) -> Dec (x = y)
184+
locDecEq Idle Idle = Yes Refl
185+
locDecEq Waiting Waiting = Yes Refl
186+
locDecEq Critical Critical = Yes Refl
187+
locDecEq Idle Waiting = No (\case Refl impossible)
188+
locDecEq Idle Critical = No (\case Refl impossible)
189+
locDecEq Waiting Idle = No (\case Refl impossible)
190+
locDecEq Waiting Critical = No (\case Refl impossible)
191+
locDecEq Critical Idle = No (\case Refl impossible)
192+
locDecEq Critical Waiting = No (\case Refl impossible)
193+
194+
||| The unique bad shape `(Critical, Critical, _)` has no `Safe` proof.
195+
bothCritNotSafe : Not (Safe (MkSt Critical Critical l))
196+
bothCritNotSafe (Safe0 f) = f Refl
197+
bothCritNotSafe (Safe1 f) = f Refl
198+
199+
||| Transport a `Safe` proof of an arbitrary state to the canonical bad shape,
200+
||| given that both locations are `Critical` (term-level transport, no stuck
201+
||| case-of-Refl). Top-level so its implicit args bind cleanly.
202+
safeToBadShape : {0 a, b : Loc} -> {0 l : Lock} ->
203+
a = Critical -> b = Critical ->
204+
Safe (MkSt a b l) -> Safe (MkSt Critical Critical l)
205+
safeToBadShape Refl Refl x = x
206+
207+
||| Sound and complete decision of the safety property for any state.
208+
public export
209+
decSafe : (s : St) -> Dec (Safe s)
210+
decSafe (MkSt a b l) =
211+
case locDecEq a Critical of
212+
No notCritA => Yes (Safe0 notCritA)
213+
Yes aCrit => case locDecEq b Critical of
214+
No notCritB => Yes (Safe1 notCritB)
215+
Yes bCrit => No (\sf => bothCritNotSafe (safeToBadShape aCrit bCrit sf))
216+
217+
--------------------------------------------------------------------------------
218+
-- Inductive-invariant hypotheses, discharged constructively
219+
--------------------------------------------------------------------------------
220+
221+
||| (1) The invariant holds on every initial state `(Idle, Idle, Free)`.
222+
public export
223+
initEstablishes : Init s -> Inv s
224+
initEstablishes InitState = MkInv C0NotCritFree C1NotCritFree
225+
226+
-- ---- coherence-preservation helper lemmas (all total, by case analysis) ----
227+
228+
||| P0 Idle->Waiting under unchanged lock stays coherent.
229+
idleToWaiting0 : Coherent0 Idle lk -> Coherent0 Waiting lk
230+
idleToWaiting0 C0NotCritFree = C0NotCritFreeW
231+
idleToWaiting0 C0NotCrit1I = C0NotCrit1W
232+
233+
||| P1 Idle->Waiting under unchanged lock stays coherent.
234+
idleToWaiting1 : Coherent1 Idle lk -> Coherent1 Waiting lk
235+
idleToWaiting1 C1NotCritFree = C1NotCritFreeW
236+
idleToWaiting1 C1NotCrit0I = C1NotCrit0W
237+
238+
||| When the lock was Free and P0 acquires it, re-tag P1's coherence with HeldBy0.
239+
||| P1 was coherent with Free (Idle or Waiting), so it stays non-Critical.
240+
freeToHeldBy0 : Coherent1 b Free -> Coherent1 b HeldBy0
241+
freeToHeldBy0 C1NotCritFree = C1NotCrit0I
242+
freeToHeldBy0 C1NotCritFreeW = C1NotCrit0W
243+
244+
||| When the lock was Free and P1 acquires it, re-tag P0's coherence with HeldBy1.
245+
freeToHeldBy1 : Coherent0 a Free -> Coherent0 a HeldBy1
246+
freeToHeldBy1 C0NotCritFree = C0NotCrit1I
247+
freeToHeldBy1 C0NotCritFreeW = C0NotCrit1W
248+
249+
||| When P0 releases (lock HeldBy0 -> Free), re-tag P1's coherence with Free.
250+
||| P1 was coherent with HeldBy0 (Idle or Waiting), so it stays non-Critical.
251+
heldBy0ToFree : Coherent1 b HeldBy0 -> Coherent1 b Free
252+
heldBy0ToFree C1NotCrit0I = C1NotCritFree
253+
heldBy0ToFree C1NotCrit0W = C1NotCritFreeW
254+
255+
||| When P1 releases (lock HeldBy1 -> Free), re-tag P0's coherence with Free.
256+
heldBy1ToFree : Coherent0 a HeldBy1 -> Coherent0 a Free
257+
heldBy1ToFree C0NotCrit1I = C0NotCritFree
258+
heldBy1ToFree C0NotCrit1W = C0NotCritFreeW
259+
260+
||| (2) The invariant is preserved by every transition. Proved by case analysis
261+
||| on `Step`. Each clause re-establishes coherence of *both* processes with the
262+
||| post-state lock. The acquire/release cases are where the lock discipline does
263+
||| the real work — and it now goes through because `Inv` carries the coupling.
264+
public export
265+
stepPreserves : Inv s -> Step s t -> Inv t
266+
-- P0 requests: P0 Idle->Waiting, lock unchanged. P0 was coherent with l while
267+
-- Idle; Waiting is coherent with the same l in every case. Re-derive from l.
268+
stepPreserves (MkInv c0 c1) P0Request = MkInv (idleToWaiting0 c0) c1
269+
stepPreserves (MkInv c0 c1) P1Request = MkInv c0 (idleToWaiting1 c1)
270+
-- P0 acquires: pre lock Free, P0 Waiting -> Critical, lock -> HeldBy0. P1 was
271+
-- coherent with Free (so P1 is Idle or Waiting, not Critical); re-tag with HeldBy0.
272+
stepPreserves (MkInv _ c1) P0Acquire = MkInv C0CritHolds (freeToHeldBy0 c1)
273+
stepPreserves (MkInv c0 _) P1Acquire = MkInv (freeToHeldBy1 c0) C1CritHolds
274+
-- P0 releases: P0 Critical -> Idle, lock HeldBy0 -> Free. P1 was coherent with
275+
-- HeldBy0 (so P1 not Critical); re-tag with Free.
276+
stepPreserves (MkInv _ c1) P0Release = MkInv C0NotCritFree (heldBy0ToFree c1)
277+
stepPreserves (MkInv c0 _) P1Release = MkInv (heldBy1ToFree c0) C1NotCritFree
278+
279+
--------------------------------------------------------------------------------
280+
-- The headline theorem: INV1 (inductive invariant => all reachable states)
281+
--------------------------------------------------------------------------------
282+
283+
||| INV1, machine-checked. If `Inv` holds on every initial state and is
284+
||| preserved by every `Step`, then `Inv` holds on every `Reachable` state.
285+
||| Proof by induction on the `Reachable` derivation — exactly the model
286+
||| checker's soundness argument for safety properties.
287+
public export
288+
invInductive : {0 s : St} -> Reachable s -> Inv s
289+
invInductive (ReachInit init) = initEstablishes init
290+
invInductive (ReachStep r step) = stepPreserves (invInductive r) step
291+
292+
||| Headline safety result: mutual exclusion holds on every reachable state.
293+
public export
294+
safetySound : {0 s : St} -> Reachable s -> Safe s
295+
safetySound r = invImpliesSafe (invInductive r)
296+
297+
--------------------------------------------------------------------------------
298+
-- Certifier
299+
--------------------------------------------------------------------------------
300+
301+
||| Certify the safety property for a state, using the existing `Result` ABI
302+
||| vocabulary: `Ok` iff the decision says the state is Safe, else `TlcError`.
303+
public export
304+
certifySafe : (s : St) -> Result
305+
certifySafe s = case decSafe s of
306+
Yes _ => Ok
307+
No _ => TlcError
308+
309+
||| Soundness of the certifier: every reachable state certifies `Ok`, because it
310+
||| provably satisfies the safety property. Ties the decision procedure, the
311+
||| reachability proof, and the headline theorem into one fact.
312+
public export
313+
certifyReachableSound : (s : St) -> Reachable s -> certifySafe s = Ok
314+
certifyReachableSound s r with (decSafe s)
315+
_ | Yes _ = Refl
316+
_ | No notS = absurd (notS (safetySound r))
317+
318+
--------------------------------------------------------------------------------
319+
-- POSITIVE control: an explicit reachable, safe witness
320+
--------------------------------------------------------------------------------
321+
322+
||| A concrete reachable state: from init, P0 requests then acquires the lock,
323+
||| ending in `(Critical, Idle, HeldBy0)`. Exercises the real transition relation.
324+
public export
325+
reachP0Critical : Reachable (MkSt Critical Idle HeldBy0)
326+
reachP0Critical =
327+
ReachStep
328+
(ReachStep (ReachInit InitState) P0Request) -- (Idle,Idle,Free) -> (Waiting,Idle,Free)
329+
P0Acquire -- -> (Critical,Idle,HeldBy0)
330+
331+
||| POSITIVE control: that reachable state satisfies the safety property.
332+
public export
333+
positiveControl : Safe (MkSt Critical Idle HeldBy0)
334+
positiveControl = safetySound reachP0Critical
335+
336+
--------------------------------------------------------------------------------
337+
-- NEGATIVE control: the bad state is genuinely excluded
338+
--------------------------------------------------------------------------------
339+
340+
||| NEGATIVE control: the mutual-exclusion-violating state `(Critical, Critical)`
341+
||| has NO safety proof. Machine-checked `Not (...)`.
342+
public export
343+
negativeControl : Not (Safe (MkSt Critical Critical HeldBy0))
344+
negativeControl = bothCritNotSafe
345+
346+
||| NEGATIVE control (stronger): the bad state is not even *reachable*. Since
347+
||| every reachable state is Safe, and the bad state contradicts Safe,
348+
||| reachability of the bad state is absurd. This is the real safety guarantee:
349+
||| the model checker would never produce a counterexample because none exists.
350+
public export
351+
badStateUnreachable : Not (Reachable (MkSt Critical Critical HeldBy0))
352+
badStateUnreachable r = negativeControl (safetySound r)

‎src/interface/abi/tlaiser-abi.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,4 @@ modules = Tlaiser.ABI.Types
99
, Tlaiser.ABI.Layout
1010
, Tlaiser.ABI.Foreign
1111
, Tlaiser.ABI.Proofs
12+
, Tlaiser.ABI.Semantics

0 commit comments

Comments
 (0)