Skip to content

Commit a95e0b8

Browse files
claudeclaude
committed
Add ABI Layer-3 invariant: affine composition law over disjoint variables
Introduces Affinescriptiser.ABI.Invariants, a second, deeper machine-checked theorem over the existing Layer-2 affine-usage model (Trace/AffineOk imported from Semantics, not redefined). Headline theorem (concatAffine): sequencing two affine-safe traces whose variable sets are disjoint yields an affine-safe trace — Disjoint t1 t2 -> AffineOk t1 -> AffineOk t2 -> AffineOk (t1 ++ t2) This is the soundness justification for the codegen concatenating two already-checked fragments over disjoint locals without re-checking. Converse structural law (suffixAffine): affine-safety is preserved under taking the suffix of a concatenation — AffineOk (t1 ++ t2) -> AffineOk t2. Supporting: elemAppSplit/elemAppRight/notElemApp membership-over-append lemmas; a sound+complete decision procedure decDisjoint for disjointness; consDisjoint compositional builder. Controls: positive (composedOk over disjoint [0,1],[2,3]), plus two negative controls (overlapNotDisjoint / overlapConcatNotAffine and wideGapDoubleUseNotAffine). All total, zero warnings; no believe_me, postulate, assert_total, idris_crash, %hint, or asserted equalities. Adversarially verified: a false AffineOk over an overlapping concat is rejected. Registers Invariants last in the .ipkg modules list. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
1 parent c963f18 commit a95e0b8

2 files changed

Lines changed: 253 additions & 0 deletions

File tree

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

Lines changed: 252 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,252 @@
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+
||| Structural invariants for Affinescriptiser (ABI Layer 3).
5+
|||
6+
||| This module proves a SECOND, deeper property over the SAME affine-usage
7+
||| model defined in `Affinescriptiser.ABI.Semantics` (the `Trace`/`AffineOk`
8+
||| datatypes are imported, not redefined). Where Layer 2 establishes a
9+
||| sound+complete *checker* for a single trace ("no variable used twice"),
10+
||| Layer 3 establishes an *algebraic composition law* for that checker:
11+
|||
12+
||| COMPOSITION (the headline Layer-3 theorem):
13+
||| If two usage traces are each affine-safe AND their variable sets are
14+
||| disjoint, then their concatenation is affine-safe. Formally
15+
||| Disjoint t1 t2 -> AffineOk t1 -> AffineOk t2 -> AffineOk (t1 ++ t2)
16+
||| This is the soundness justification for the codegen *sequencing* two
17+
||| already-checked program fragments over disjoint locals into one fragment
18+
||| without re-running the whole affine check.
19+
|||
20+
||| DECOMPOSITION (the converse structural law):
21+
||| Affine-safety is preserved under taking the *suffix* of a concatenation:
22+
||| AffineOk (t1 ++ t2) -> AffineOk t2
23+
||| i.e. dropping a safe prefix can never break affine-safety of the rest.
24+
|||
25+
||| Both directions are genuine, machine-checked, total proofs. Disjointness is
26+
||| given a sound+complete decision procedure (`decDisjoint`). We supply a
27+
||| POSITIVE control (a concrete inhabited composition witness) and TWO NEGATIVE
28+
||| controls: a `Not` showing overlapping traces compose to an unsafe trace, and
29+
||| a `Not` showing a wide-gap double-use trace is rejected.
30+
|||
31+
||| Quality bar (identical to Layer 2): no believe_me, no idris_crash, no
32+
||| assert_total, no postulate, no sorry, no %hint hacks, no asserted equalities.
33+
34+
module Affinescriptiser.ABI.Invariants
35+
36+
import Affinescriptiser.ABI.Types
37+
import Affinescriptiser.ABI.Semantics
38+
import Data.List.Elem
39+
import Decidable.Equality
40+
41+
%default total
42+
43+
--------------------------------------------------------------------------------
44+
-- Membership-over-append lemmas (the technical core)
45+
--------------------------------------------------------------------------------
46+
47+
||| If `x` occurs in `xs ++ ys` then it occurs in `xs` or in `ys`.
48+
||| Proved by induction on `xs`. `Here`/`There` are constructor-headed, so the
49+
||| recursive case-splits reduce cleanly with no stuck `case ... of Refl`.
50+
export
51+
elemAppSplit : {0 x : Var} -> (xs : Trace) -> Elem x (xs ++ ys) -> Either (Elem x xs) (Elem x ys)
52+
elemAppSplit [] el = Right el
53+
elemAppSplit (y :: ys) Here = Left Here
54+
elemAppSplit (y :: ys) (There el) =
55+
case elemAppSplit ys el of
56+
Left inXs => Left (There inXs)
57+
Right inYs => Right inYs
58+
59+
||| Conversely, membership in `ys` injects into membership in `xs ++ ys`.
60+
||| Induction on `xs` again; each step is just one `There`.
61+
export
62+
elemAppRight : {0 x : Var} -> (xs : Trace) -> Elem x ys -> Elem x (xs ++ ys)
63+
elemAppRight [] el = el
64+
elemAppRight (y :: ys) el = There (elemAppRight ys el)
65+
66+
||| If `x` is in neither `xs` nor `ys`, it is not in `xs ++ ys`.
67+
||| This is the contrapositive of `elemAppSplit`, packaged for direct use.
68+
export
69+
notElemApp : {0 x : Var}
70+
-> (xs : Trace)
71+
-> Not (Elem x xs)
72+
-> Not (Elem x ys)
73+
-> Not (Elem x (xs ++ ys))
74+
notElemApp xs nxs nys el =
75+
case elemAppSplit xs el of
76+
Left inXs => nxs inXs
77+
Right inYs => nys inYs
78+
79+
--------------------------------------------------------------------------------
80+
-- Disjointness of variable sets
81+
--------------------------------------------------------------------------------
82+
83+
||| Two traces are `Disjoint` when no variable appears in both. This is the
84+
||| precondition under which sequencing two affine fragments stays affine: each
85+
||| fragment may reuse names internally only if those names do not collide.
86+
public export
87+
Disjoint : Trace -> Trace -> Type
88+
Disjoint xs ys = (v : Var) -> Elem v xs -> Not (Elem v ys)
89+
90+
||| The empty trace is disjoint from anything (vacuously: nothing is in `[]`).
91+
export
92+
disjointNilLeft : (ys : Trace) -> Disjoint [] ys
93+
disjointNilLeft ys v el = absurd el
94+
95+
||| Drop the head of the left trace and disjointness is preserved.
96+
export
97+
disjointTail : {0 x : Var} -> Disjoint (x :: xs) ys -> Disjoint xs ys
98+
disjointTail dj v inXs = dj v (There inXs)
99+
100+
||| The head of a disjoint left trace is not present in the right trace.
101+
||| `x` is bound explicitly (quantity 1) because we use it at the term level.
102+
export
103+
disjointHeadNotRight : {x : Var} -> Disjoint (x :: xs) ys -> Not (Elem x ys)
104+
disjointHeadNotRight dj = dj x Here
105+
106+
||| Build a disjointness witness by consing onto the left trace: if the new
107+
||| head `x` is absent from `ys` and `xs` is already disjoint from `ys`, then
108+
||| `x :: xs` is disjoint from `ys`. Matching on the LEFT membership refines the
109+
||| variable cleanly (avoiding the Nat-literal coverage pitfalls).
110+
export
111+
consDisjoint : {0 x : Var} -> Not (Elem x ys) -> Disjoint xs ys -> Disjoint (x :: xs) ys
112+
consDisjoint nx _ v Here = nx
113+
consDisjoint _ dxs v (There inXs) = dxs v inXs
114+
115+
--------------------------------------------------------------------------------
116+
-- Sound + complete decision procedure for disjointness
117+
--------------------------------------------------------------------------------
118+
119+
||| Decide whether two traces are disjoint. A `Yes` carries a real witness
120+
||| (a function refuting any shared membership), a `No` carries a real overlap.
121+
||| Built only from `isElem` (Data.List.Elem) and the structural lemmas above.
122+
public export
123+
decDisjoint : (xs : Trace) -> (ys : Trace) -> Dec (Disjoint xs ys)
124+
decDisjoint [] ys = Yes (disjointNilLeft ys)
125+
decDisjoint (x :: xs) ys =
126+
case isElem x ys of
127+
-- x is shared: the pair cannot be disjoint, since x is in both sides.
128+
Yes xInYs => No (\dj => disjointHeadNotRight dj xInYs)
129+
No xNotYs =>
130+
case decDisjoint xs ys of
131+
Yes djRest =>
132+
Yes (\v, inHead =>
133+
case inHead of
134+
Here => xNotYs
135+
There inXs => djRest v inXs)
136+
No notRest =>
137+
No (\dj => notRest (disjointTail dj))
138+
139+
--------------------------------------------------------------------------------
140+
-- HEADLINE Layer-3 theorem: composition of affine traces over disjoint vars
141+
--------------------------------------------------------------------------------
142+
143+
||| COMPOSITION. Sequencing two affine-safe traces whose variable sets are
144+
||| disjoint yields an affine-safe trace. Proved by induction on the structure
145+
||| of the first trace via its `AffineOk` witness:
146+
|||
147+
||| * `[] ++ t2` reduces to `t2`, whose safety we already have.
148+
||| * `(v :: vs) ++ t2` reduces to `v :: (vs ++ t2)`. The new `notLater`
149+
||| obligation — `v` not in `vs ++ t2` — is discharged by `notElemApp`:
150+
||| `v` is absent from `vs` (head of t1's witness) and absent from `t2`
151+
||| (disjointness). The tail is handled by recursion.
152+
export
153+
concatAffine : (t1 : Trace)
154+
-> Disjoint t1 t2
155+
-> AffineOk t1
156+
-> AffineOk t2
157+
-> AffineOk (t1 ++ t2)
158+
concatAffine [] _ _ ok2 = ok2
159+
concatAffine (v :: vs) dj (ConsOk nv ok1) ok2 =
160+
let notInVs : Not (Elem v vs) := nv
161+
notInT2 : Not (Elem v t2) := disjointHeadNotRight dj
162+
notInBoth : Not (Elem v (vs ++ t2)) := notElemApp vs notInVs notInT2
163+
restOk : AffineOk (vs ++ t2) := concatAffine vs (disjointTail dj) ok1 ok2
164+
in ConsOk notInBoth restOk
165+
166+
--------------------------------------------------------------------------------
167+
-- Converse structural law: affine-safety of a suffix
168+
--------------------------------------------------------------------------------
169+
170+
||| DECOMPOSITION. If a concatenation is affine-safe, so is its suffix `t2`.
171+
||| (Dropping a safe prefix never breaks the rest.) Induction on `t1`: each
172+
||| `ConsOk` we strip exposes the `AffineOk (vs ++ t2)` witness for recursion;
173+
||| the base case `[] ++ t2 = t2` returns the witness directly.
174+
export
175+
suffixAffine : (t1 : Trace) -> AffineOk (t1 ++ t2) -> AffineOk t2
176+
suffixAffine [] ok = ok
177+
suffixAffine (v :: vs) (ConsOk _ rest) = suffixAffine vs rest
178+
179+
--------------------------------------------------------------------------------
180+
-- Positive control: a concrete inhabited composition
181+
--------------------------------------------------------------------------------
182+
183+
||| Left fragment uses variables 0 and 1 (each once).
184+
export
185+
fragLeftOk : AffineOk [0, 1]
186+
fragLeftOk =
187+
ConsOk (\el => case el of
188+
There el1 => absurd el1)
189+
(ConsOk absurd NilOk)
190+
191+
||| Right fragment uses variables 2 and 3 (each once).
192+
export
193+
fragRightOk : AffineOk [2, 3]
194+
fragRightOk =
195+
ConsOk (\el => case el of
196+
There el1 => absurd el1)
197+
(ConsOk absurd NilOk)
198+
199+
||| 0 is not an element of [2,3]: the diagonal `Here`/`There Here` shapes would
200+
||| require 0 = 2 / 0 = 3 (automatically pruned), so only the empty tail
201+
||| `There (There el)` remains, discharged by `absurd`.
202+
zeroNotIn23 : Not (Elem (the Var 0) [2, 3])
203+
zeroNotIn23 (There (There el)) = absurd el
204+
205+
||| 1 is not an element of [2,3]. Same structure as `zeroNotIn23`.
206+
oneNotIn23 : Not (Elem (the Var 1) [2, 3])
207+
oneNotIn23 (There (There el)) = absurd el
208+
209+
||| The two fragments use disjoint variable sets {0,1} and {2,3}. Built
210+
||| compositionally with `consDisjoint` from the per-element refutations
211+
||| `zeroNotIn23` / `oneNotIn23` and the vacuous `disjointNilLeft` — a genuine
212+
||| witness, no assertion.
213+
export
214+
fragsDisjoint : Disjoint [0, 1] [2, 3]
215+
fragsDisjoint =
216+
consDisjoint zeroNotIn23 (consDisjoint oneNotIn23 (disjointNilLeft [2, 3]))
217+
218+
||| POSITIVE CONTROL: composing the two disjoint affine fragments produces an
219+
||| affine-safe trace [0,1,2,3] — built by the headline theorem, not by hand.
220+
export
221+
composedOk : AffineOk ([0, 1] ++ [2, 3])
222+
composedOk = concatAffine [0, 1] fragsDisjoint fragLeftOk fragRightOk
223+
224+
--------------------------------------------------------------------------------
225+
-- Negative control 1: overlapping fragments are NOT disjoint
226+
--------------------------------------------------------------------------------
227+
228+
||| Fragments [0,1] and [1,2] share variable 1, so they are NOT disjoint.
229+
||| Machine-checked refutation: any disjointness witness would have to refute
230+
||| `Elem 1 [1,2]`, but 1 is `Here`.
231+
export
232+
overlapNotDisjoint : Not (Disjoint [0, 1] [1, 2])
233+
overlapNotDisjoint dj = dj 1 (There Here) Here
234+
235+
||| And their concatenation [0,1,1,2] is genuinely unsafe: variable 1 occurs
236+
||| twice. No `AffineOk` witness exists — the head-1 obligation would have to
237+
||| refute `Elem 1 [1,2]`, which is `Here`.
238+
export
239+
overlapConcatNotAffine : Not (AffineOk ([0, 1] ++ [1, 2]))
240+
overlapConcatNotAffine ok = headNotLater (tailOk ok) Here
241+
242+
--------------------------------------------------------------------------------
243+
-- Negative control 2: a wide-gap double use is rejected
244+
--------------------------------------------------------------------------------
245+
246+
||| A reuse separated by several distinct intervening uses is still caught:
247+
||| variable 9 appears at the head and again after 4 other variables in
248+
||| [9, 1, 2, 3, 4, 9]. Refuted because 9 reappears later in the tail.
249+
export
250+
wideGapDoubleUseNotAffine : Not (AffineOk [9, 1, 2, 3, 4, 9])
251+
wideGapDoubleUseNotAffine ok =
252+
headNotLater ok (There (There (There (There Here))))

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,4 @@ modules = Affinescriptiser.ABI.Types
88
, Affinescriptiser.ABI.Foreign
99
, Affinescriptiser.ABI.Proofs
1010
, Affinescriptiser.ABI.Semantics
11+
, Affinescriptiser.ABI.Invariants

0 commit comments

Comments
 (0)