Skip to content

Commit b0cd266

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 3: compositionality of inductive invariants (conjunction is inductive) (#39)
* abi: prove inductive-invariant soundness (TLA+ INV1) in Tlaiser.ABI.Semantics 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). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * 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 --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 8f54595 commit b0cd266

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)