Skip to content

Commit 0680396

Browse files
claudeclaude
committed
abi(tlaiser): Layer-3 — inductive invariants compose (conjunction is inductive)
Add Tlaiser.ABI.Invariants, a deeper, distinct machine-checked theorem built over the SAME Layer-2 state-machine model (St/Init/Step/Reachable/Inv in Tlaiser.ABI.Semantics; no datatypes redefined). Layer-2 proved INV1 for one hand-crafted invariant. Layer-3 proves the meta-theorem that licenses modular invariant construction in TLA+/TLAPS: andInductive : IsInductive p -> IsInductive q -> IsInductive (And p q) "the conjunction of two inductive invariants is itself inductive." Contents: - IsInductive p: the two INV1 premises (established by Init, preserved by Step) packaged as a first-class value so inductiveness can be combined. - inductiveOnReachable: generic INV1 (any inductive p holds on all reachable states), proved once polymorphically. - andInductive: the headline composition theorem. - HolderCrit: a SECOND, independent concrete invariant ("the lock holder is Critical"), proved inductive from scratch (holderInit + holderStep over the existing Step relation), packaged as holderIsInductive. - combinedIsInductive / combinedOnReachable: Inv and HolderCrit composed via andInductive, yielding the conjunction on every reachable state with no new induction. - decHolderCrit: sound + complete Dec for the second invariant; certifyHolder reuses the Result ABI; certifyHolderReachableSound ties it together. - Controls: positive (inhabited reachable witness of the conjunction + decided Ok), negative (Not (HolderCrit (Idle,Idle,HeldBy0))), and a distinctness/non-vacuity control (HolderCrit holds but Inv fails on (Critical,Critical,Free) — proving the two predicates are genuinely different). Clean build, zero warnings; adversarial false statements rejected. No believe_me/postulate/assert_total/idris_crash. %default total throughout. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
1 parent ee9339e commit 0680396

2 files changed

Lines changed: 357 additions & 0 deletions

File tree

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

Lines changed: 356 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,356 @@
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+
||| Layer-3 deepening for Tlaiser: COMPOSITIONALITY of inductive invariants.
5+
|||
6+
||| The Layer-2 flagship (`Tlaiser.ABI.Semantics.safetySound`) proves INV1 for
7+
||| ONE hand-crafted inductive invariant (`Inv`) and derives mutual exclusion.
8+
||| That establishes soundness of a *single* invariant. This module proves a
9+
||| strictly deeper, structurally different fact about the *space of invariants*
10+
||| itself:
11+
|||
12+
||| THE CONJUNCTION OF TWO INDUCTIVE INVARIANTS IS INDUCTIVE.
13+
|||
14+
||| In TLA+ practice this is exactly how large invariants are built and how the
15+
||| TLAPS proof manager decomposes them: one proves several smaller invariants
16+
||| independently, then conjoins them, relying on the meta-fact that
17+
||| inductiveness is closed under conjunction. We formalise that meta-fact
18+
||| abstractly over the SAME state machine, relations and reachability already
19+
||| defined in `Semantics` (we do NOT redefine `St`, `Init`, `Step`,
20+
||| `Reachable`).
21+
|||
22+
||| Concretely this module:
23+
||| 1. Abstracts "P is an inductive invariant" as `IsInductive P`
24+
||| (established by `Init`, preserved by `Step`) — the two INV1 premises,
25+
||| packaged so they can be manipulated as first-class values.
26+
||| 2. Proves the generic INV1 closure `inductiveOnReachable` once, for ANY
27+
||| inductive P (the Layer-2 proof was monomorphic in `Inv`).
28+
||| 3. Proves the COMPOSITION theorem `andInductive`: if `P` and `Q` are each
29+
||| inductive then `\s => (P s, Q s)` is inductive. This is the headline,
30+
||| and it is genuinely distinct from — and used to *strengthen* — the
31+
||| Layer-2 result.
32+
||| 4. Exhibits a SECOND, independent concrete invariant `HolderCrit`
33+
||| ("if a process holds the lock then that process is Critical"), proves
34+
||| it inductive from scratch, and shows it is NOT the same predicate as
35+
||| `Inv` (a reachable state distinguishes the *strength* of the two; and
36+
||| a non-reachable state inhabits one predicate but not the other).
37+
||| 5. COMPOSES `Inv` and `HolderCrit` via `andInductive` into a single
38+
||| conjoined inductive invariant that therefore holds on every reachable
39+
||| state — demonstrating modular invariant construction end to end.
40+
||| 6. Provides a sound+complete decision procedure for the second invariant,
41+
||| a positive control (an inhabited reachable witness of the conjunction)
42+
||| and a negative / non-vacuity control (a machine-checked `Not (...)`).
43+
|||
44+
||| Everything is built over the Layer-2 datatypes; no axioms, no `believe_me`,
45+
||| no `postulate`, no `assert_total`.
46+
|||
47+
||| @see https://lamport.azurewebsites.net/tla/tla.html (INV1, invariant conj.)
48+
49+
module Tlaiser.ABI.Invariants
50+
51+
import Tlaiser.ABI.Types
52+
import Tlaiser.ABI.Semantics
53+
54+
%default total
55+
56+
--------------------------------------------------------------------------------
57+
-- 1. "Inductive invariant", abstracted as a first-class value
58+
--------------------------------------------------------------------------------
59+
60+
||| A state predicate over the Layer-2 machine.
61+
public export
62+
0 Pred : Type
63+
Pred = St -> Type
64+
65+
||| `IsInductive p` packages the two INV1 premises for an arbitrary predicate
66+
||| `p`, over the EXISTING `Init` and `Step` relations from `Semantics`:
67+
||| * `establishes` : `p` holds on every initial state;
68+
||| * `preserves` : every `Step` from a `p`-state lands in a `p`-state.
69+
||| Making this a record lets us treat inductiveness as data we can combine
70+
||| (e.g. conjoin) — the move that distinguishes this layer from the Layer-2
71+
||| monomorphic proof.
72+
public export
73+
record IsInductive (0 p : Pred) where
74+
constructor MkIsInductive
75+
establishes : {0 s : St} -> Init s -> p s
76+
preserves : {0 s, t : St} -> p s -> Step s t -> p t
77+
78+
--------------------------------------------------------------------------------
79+
-- 2. Generic INV1: any inductive predicate holds on all reachable states
80+
--------------------------------------------------------------------------------
81+
82+
||| INV1, proved ONCE for an arbitrary inductive predicate (the Layer-2 version,
83+
||| `invInductive`, was specialised to the single predicate `Inv`). Induction on
84+
||| the `Reachable` derivation, discharging each case with the packaged premises.
85+
public export
86+
inductiveOnReachable : {0 p : Pred} -> IsInductive p ->
87+
{0 s : St} -> Reachable s -> p s
88+
inductiveOnReachable ind (ReachInit init) = ind.establishes init
89+
inductiveOnReachable ind (ReachStep r step) =
90+
ind.preserves (inductiveOnReachable ind r) step
91+
92+
--------------------------------------------------------------------------------
93+
-- 3. HEADLINE: inductiveness is closed under conjunction
94+
--------------------------------------------------------------------------------
95+
96+
||| The conjunction of two predicates, as a predicate.
97+
public export
98+
0 And : Pred -> Pred -> Pred
99+
And p q = \s => (p s, q s)
100+
101+
||| THE COMPOSITION THEOREM. If `p` and `q` are each inductive invariants of the
102+
||| machine, then so is their conjunction `And p q`. Each INV1 premise of the
103+
||| conjunction is discharged componentwise from the premises of `p` and `q`.
104+
||| This is the meta-theorem that licenses modular invariant construction.
105+
public export
106+
andInductive : {0 p, q : Pred} ->
107+
IsInductive p -> IsInductive q -> IsInductive (And p q)
108+
andInductive ip iq =
109+
MkIsInductive
110+
(\init => (ip.establishes init, iq.establishes init))
111+
(\(hp, hq), step => (ip.preserves hp step, iq.preserves hq step))
112+
113+
--------------------------------------------------------------------------------
114+
-- 4. The Layer-2 invariant `Inv`, repackaged as a first-class IsInductive value
115+
--------------------------------------------------------------------------------
116+
117+
||| `Inv` from Layer-2 is inductive — we already have the two discharged
118+
||| premises (`initEstablishes`, `stepPreserves`); here we merely repackage them
119+
||| as an `IsInductive` value so the composition machinery can consume it.
120+
public export
121+
invIsInductive : IsInductive Inv
122+
invIsInductive = MkIsInductive initEstablishes stepPreserves
123+
124+
--------------------------------------------------------------------------------
125+
-- 5. A SECOND, INDEPENDENT concrete invariant: "holder is Critical"
126+
--------------------------------------------------------------------------------
127+
128+
||| Per-process: "if process 0 holds the lock (`HeldBy0`) then it is Critical".
129+
||| Indexed by P0's location and the lock. This couples the lock to the holder's
130+
||| location in the *opposite* direction from `Coherent0`'s emphasis: it is the
131+
||| "held => critical" half, whereas `Inv`'s coherence carries "critical =>
132+
||| held" plus the cross-process exclusion. Distinct content, proved afresh.
133+
public export
134+
data Holder0 : Loc -> Lock -> Type where
135+
||| Lock held by P0 forces P0 = Critical.
136+
H0Crit : Holder0 Critical HeldBy0
137+
||| Lock not held by P0: no constraint on P0's location.
138+
H0Free : Holder0 a Free
139+
H0Other : Holder0 a HeldBy1
140+
141+
||| Per-process mirror for P1: "if P1 holds the lock then P1 is Critical".
142+
public export
143+
data Holder1 : Loc -> Lock -> Type where
144+
H1Crit : Holder1 Critical HeldBy1
145+
H1Free : Holder1 a Free
146+
H1Other : Holder1 a HeldBy0
147+
148+
||| The SECOND whole-state invariant: whichever process holds the single lock
149+
||| token is in its critical section. Genuinely different predicate from `Inv`.
150+
public export
151+
data HolderCrit : St -> Type where
152+
MkHolderCrit : Holder0 a lk -> Holder1 b lk -> HolderCrit (MkSt a b lk)
153+
154+
-- (5a) `HolderCrit` holds on the initial state ---------------------------------
155+
156+
||| Established by `Init`: the unique initial state `(Idle, Idle, Free)` has the
157+
||| lock free, so both holder constraints hold vacuously.
158+
public export
159+
holderInit : {0 s : St} -> Init s -> HolderCrit s
160+
holderInit InitState = MkHolderCrit H0Free H1Free
161+
162+
-- (5b) `HolderCrit` is preserved by every `Step` ------------------------------
163+
-- Helper lemmas keep each Step clause first-order and total.
164+
165+
||| A request transition keeps the lock unchanged; a `Holder0` fact transports
166+
||| across any location change because for a *fixed* lock it is determined only
167+
||| by the lock except in the `HeldBy0` case, and a requesting/releasing process
168+
||| in the relevant clauses is never the `HeldBy0`/Critical witness we must keep.
169+
||| We discharge preservation directly per Step constructor below instead, which
170+
||| is clearer than generic transport; these tiny lemmas cover the lock-retag
171+
||| cases (acquire/release) where the holder's own slot is fixed.
172+
173+
||| When P1 acquires (lock Free -> HeldBy1), P0's holder fact retags Free->HeldBy1.
174+
holder0FreeToHB1 : Holder0 a Free -> Holder0 a HeldBy1
175+
holder0FreeToHB1 H0Free = H0Other
176+
177+
||| When P0 acquires (lock Free -> HeldBy0), P1's holder fact retags Free->HeldBy0.
178+
holder1FreeToHB0 : Holder1 b Free -> Holder1 b HeldBy0
179+
holder1FreeToHB0 H1Free = H1Other
180+
181+
||| When P0 releases (lock HeldBy0 -> Free), P1's holder fact retags HeldBy0->Free.
182+
holder1HB0ToFree : Holder1 b HeldBy0 -> Holder1 b Free
183+
holder1HB0ToFree H1Other = H1Free
184+
185+
||| When P1 releases (lock HeldBy1 -> Free), P0's holder fact retags HeldBy1->Free.
186+
holder0HB1ToFree : Holder0 a HeldBy1 -> Holder0 a Free
187+
holder0HB1ToFree H0Other = H0Free
188+
189+
||| Preservation of the second invariant under every transition, by case
190+
||| analysis on `Step`. Acquire creates the `Critical`/`HeldBy_i` pairing
191+
||| (`H?Crit`); release returns the lock to `Free` (`H?Free`); request leaves
192+
||| the lock untouched so the (lock-determined) constraint on the *moving*
193+
||| process is re-derived and the other process's fact is unchanged.
194+
public export
195+
holderStep : {0 s, t : St} -> HolderCrit s -> Step s t -> HolderCrit t
196+
-- P0 Idle->Waiting, lock l unchanged. P0's constraint for any held-by-other / free
197+
-- lock is unconstrained (H0Free / H0Other); if l were HeldBy0 the source would need
198+
-- Holder0 Idle HeldBy0, which is uninhabited, so that case cannot arise.
199+
holderStep (MkHolderCrit H0Free h1) P0Request = MkHolderCrit H0Free h1
200+
holderStep (MkHolderCrit H0Other h1) P0Request = MkHolderCrit H0Other h1
201+
-- P1 Idle->Waiting, lock unchanged. Symmetric.
202+
holderStep (MkHolderCrit h0 H1Free) P1Request = MkHolderCrit h0 H1Free
203+
holderStep (MkHolderCrit h0 H1Other) P1Request = MkHolderCrit h0 H1Other
204+
-- P0 acquires: Waiting->Critical, lock Free->HeldBy0. P0 becomes the holder and
205+
-- is Critical (H0Crit); retag P1's free fact to HeldBy0.
206+
holderStep (MkHolderCrit _ h1) P0Acquire = MkHolderCrit H0Crit (holder1FreeToHB0 h1)
207+
-- P1 acquires: symmetric.
208+
holderStep (MkHolderCrit h0 _) P1Acquire = MkHolderCrit (holder0FreeToHB1 h0) H1Crit
209+
-- P0 releases: Critical->Idle, lock HeldBy0->Free. P0 no longer holds (H0Free);
210+
-- retag P1's HeldBy0 fact to Free.
211+
holderStep (MkHolderCrit _ h1) P0Release = MkHolderCrit H0Free (holder1HB0ToFree h1)
212+
-- P1 releases: symmetric.
213+
holderStep (MkHolderCrit h0 _) P1Release = MkHolderCrit (holder0HB1ToFree h0) H1Free
214+
215+
||| The second invariant, packaged as a first-class `IsInductive` value.
216+
public export
217+
holderIsInductive : IsInductive HolderCrit
218+
holderIsInductive = MkIsInductive holderInit holderStep
219+
220+
--------------------------------------------------------------------------------
221+
-- 6. COMPOSE the two invariants and reap the conjoined result on reachable states
222+
--------------------------------------------------------------------------------
223+
224+
||| The conjoined invariant `Inv ∧ HolderCrit`, proved inductive purely by
225+
||| feeding the two component proofs through the composition theorem. No new
226+
||| case analysis: this is the payoff of `andInductive`.
227+
public export
228+
combinedIsInductive : IsInductive (And Inv HolderCrit)
229+
combinedIsInductive = andInductive invIsInductive holderIsInductive
230+
231+
||| Headline Layer-3 corollary: the CONJUNCTION of the two independently-proved
232+
||| invariants holds on EVERY reachable state — obtained generically, not by
233+
||| re-running an induction over `Reachable`.
234+
public export
235+
combinedOnReachable : {0 s : St} -> Reachable s -> (Inv s, HolderCrit s)
236+
combinedOnReachable r = inductiveOnReachable combinedIsInductive r
237+
238+
--------------------------------------------------------------------------------
239+
-- 7. Decision procedure for the SECOND invariant (sound + complete)
240+
--------------------------------------------------------------------------------
241+
242+
||| `Holder0` is decidable for a concrete location/lock pair.
243+
decHolder0 : (a : Loc) -> (lk : Lock) -> Dec (Holder0 a lk)
244+
decHolder0 _ Free = Yes H0Free
245+
decHolder0 _ HeldBy1 = Yes H0Other
246+
decHolder0 Critical HeldBy0 = Yes H0Crit
247+
decHolder0 Idle HeldBy0 = No (\case H0Crit impossible)
248+
decHolder0 Waiting HeldBy0 = No (\case H0Crit impossible)
249+
250+
||| `Holder1` is decidable for a concrete location/lock pair.
251+
decHolder1 : (b : Loc) -> (lk : Lock) -> Dec (Holder1 b lk)
252+
decHolder1 _ Free = Yes H1Free
253+
decHolder1 _ HeldBy0 = Yes H1Other
254+
decHolder1 Critical HeldBy1 = Yes H1Crit
255+
decHolder1 Idle HeldBy1 = No (\case H1Crit impossible)
256+
decHolder1 Waiting HeldBy1 = No (\case H1Crit impossible)
257+
258+
||| Recover the P0-component from a whole-state `HolderCrit`.
259+
holderProj0 : HolderCrit (MkSt a b lk) -> Holder0 a lk
260+
holderProj0 (MkHolderCrit h0 _) = h0
261+
262+
||| Recover the P1-component from a whole-state `HolderCrit`.
263+
holderProj1 : HolderCrit (MkSt a b lk) -> Holder1 b lk
264+
holderProj1 (MkHolderCrit _ h1) = h1
265+
266+
||| Sound AND complete decision of the second invariant for any state.
267+
public export
268+
decHolderCrit : (s : St) -> Dec (HolderCrit s)
269+
decHolderCrit (MkSt a b lk) =
270+
case decHolder0 a lk of
271+
No notH0 => No (\hc => notH0 (holderProj0 hc))
272+
Yes h0 => case decHolder1 b lk of
273+
No notH1 => No (\hc => notH1 (holderProj1 hc))
274+
Yes h1 => Yes (MkHolderCrit h0 h1)
275+
276+
||| Certifier for the second invariant, reusing the existing `Result` ABI
277+
||| vocabulary: `Ok` iff the state satisfies `HolderCrit`, else `TlcError`.
278+
public export
279+
certifyHolder : (s : St) -> Result
280+
certifyHolder s = case decHolderCrit s of
281+
Yes _ => Ok
282+
No _ => TlcError
283+
284+
||| Soundness of that certifier on reachable states: every reachable state
285+
||| satisfies `HolderCrit` (it is a conjunct of `combinedOnReachable`), so it
286+
||| certifies `Ok`. Ties decision + reachability + composition together.
287+
public export
288+
certifyHolderReachableSound : (s : St) -> Reachable s -> certifyHolder s = Ok
289+
certifyHolderReachableSound s r with (decHolderCrit s)
290+
_ | Yes _ = Refl
291+
_ | No notHC = absurd (notHC (snd (combinedOnReachable r)))
292+
293+
--------------------------------------------------------------------------------
294+
-- 8. POSITIVE control: an inhabited reachable witness of the CONJUNCTION
295+
--------------------------------------------------------------------------------
296+
297+
||| POSITIVE control: the concrete reachable state `(Critical, Idle, HeldBy0)`
298+
||| (reached in `Semantics.reachP0Critical`) satisfies BOTH invariants at once —
299+
||| obtained through the composed inductive proof, exercising the whole pipeline.
300+
public export
301+
positiveControl : (Inv (MkSt Critical Idle HeldBy0), HolderCrit (MkSt Critical Idle HeldBy0))
302+
positiveControl = combinedOnReachable reachP0Critical
303+
304+
||| POSITIVE control, second face: the second invariant decides `Yes` on that
305+
||| same concrete state (the decision procedure agrees with the proof).
306+
public export
307+
positiveControlDecided : certifyHolder (MkSt Critical Idle HeldBy0) = Ok
308+
positiveControlDecided = Refl
309+
310+
--------------------------------------------------------------------------------
311+
-- 9. NEGATIVE / NON-VACUITY controls
312+
--------------------------------------------------------------------------------
313+
314+
||| NEGATIVE control #1 (the second invariant is non-trivial): the state
315+
||| `(Idle, Idle, HeldBy0)` — lock held by P0 yet P0 is Idle, NOT Critical —
316+
||| violates `HolderCrit`. Machine-checked `Not (...)`. This is the witness that
317+
||| `HolderCrit` actually constrains states (it is not all-inhabited), so the
318+
||| inductiveness result above is non-vacuous.
319+
||| There is no `Holder0 Idle HeldBy0` proof (no constructor pairs Idle with
320+
||| HeldBy0). Stated as a refuting helper with a top-level impossible clause.
321+
holder0IdleHB0Absurd : Not (Holder0 Idle HeldBy0)
322+
holder0IdleHB0Absurd H0Crit impossible
323+
324+
public export
325+
negativeControl : Not (HolderCrit (MkSt Idle Idle HeldBy0))
326+
negativeControl (MkHolderCrit h0 _) = holder0IdleHB0Absurd h0
327+
328+
||| NEGATIVE / DISTINCTNESS control #2 (the two invariants are GENUINELY
329+
||| DIFFERENT predicates — the second is not a restatement of `Inv`): we exhibit
330+
||| a single state that SATISFIES the second invariant `HolderCrit` yet VIOLATES
331+
||| the Layer-2 invariant `Inv`. Such a separating witness proves the two
332+
||| predicates are not equal as `St -> Type` (HolderCrit does NOT imply Inv), so
333+
||| this layer adds new, non-derivable content.
334+
|||
335+
||| Witness: `(Critical, Critical, Free)`. With the lock Free, neither process
336+
||| is the holder, so both `Holder0`/`Holder1` constraints hold vacuously
337+
||| (`H0Free`/`H1Free`) and `HolderCrit` is inhabited. But `Inv` requires both
338+
||| processes coherent with the (Free) lock, and `Coherent0 Critical Free` is
339+
||| uninhabited (Critical demands `HeldBy0`), so `Inv` fails. (Note: this state
340+
||| is mutual-exclusion-violating and is precisely UNREACHABLE — see
341+
||| `Semantics.badStateUnreachable` — which is *why* the strictly weaker
342+
||| `HolderCrit` cannot on its own imply mutual exclusion: it needs `Inv` as the
343+
||| second conjunct. That is the whole point of composing them.)
344+
public export
345+
holderHoldsButInvFails :
346+
(HolderCrit (MkSt Critical Critical Free), Not (Inv (MkSt Critical Critical Free)))
347+
holderHoldsButInvFails =
348+
( MkHolderCrit H0Free H1Free
349+
, invCriticalFreeAbsurd
350+
)
351+
where
352+
||| `Inv (Critical, Critical, Free)` is uninhabited: its P0 component would
353+
||| be `Coherent0 Critical Free`, which has no constructor.
354+
invCriticalFreeAbsurd : Not (Inv (MkSt Critical Critical Free))
355+
invCriticalFreeAbsurd (MkInv c0 _) = case c0 of
356+
C0CritHolds impossible

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,4 @@ modules = Tlaiser.ABI.Types
1010
, Tlaiser.ABI.Foreign
1111
, Tlaiser.ABI.Proofs
1212
, Tlaiser.ABI.Semantics
13+
, Tlaiser.ABI.Invariants

0 commit comments

Comments
 (0)