Skip to content

Commit bd08c30

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 2: prove affine usage (use-at-most-once) — flagship Idris2 proof (#37)
## Summary Raises affinescriptiser's Idris2 ABI to **Layer 2** with its first flagship semantic proof. Affinescriptiser's headline is affine + dependent types; this proves the **affine discipline**: a usage trace is `AffineOk` iff no variable is used more than once. A double-use trace has no `AffineOk` witness. Mirrors the estate flagship-proof pattern: faithful model, uninhabited bad case, sound+complete `Dec`, certifier proven sound (and complete), positive + negative controls. ## Changes - Adds `src/interface/abi/Affinescriptiser/ABI/Semantics.idr` — `AffineOk` over usage traces, `decAffineOk : Dec`, `certifyAffineSound`/`certifyAffineComplete`, and the negative control `doubleUseNotAffineOk : Not (AffineOk [0, 0])`. - Registers the module in the ABI `.ipkg`. ## RSR Quality Checklist ### Required - [x] Tests pass — ABI builds clean (see Testing) - [x] Linter clean — zero warnings - [x] No banned language patterns - [x] No banned functions (`believe_me`/`postulate`/… — genuine proof) - [x] SPDX headers present - [x] No secrets ### As Applicable - [x] ABI/FFI changes validated — additive proof; FFI untouched ## Testing Verified with **Idris2 0.7.0**: `idris2 --build affinescriptiser-abi.ipkg` → exit 0, zero warnings. **Adversarial check**: a deliberately-false proof was rejected. `build/` removed. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- _Generated by [Claude Code](https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent cc37b35 commit bd08c30

2 files changed

Lines changed: 159 additions & 0 deletions

File tree

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

Lines changed: 158 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,158 @@
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 Affinescriptiser (ABI Layer 2).
5+
|||
6+
||| Headline domain property: AFFINE USAGE. A resource (variable) may be used
7+
||| AT MOST ONCE. We model a program fragment as a *usage trace* — the ordered
8+
||| sequence of variable uses the codegen emits. The property `AffineOk` holds
9+
||| of a trace exactly when no variable is used twice: every use refers to a
10+
||| variable that has not yet appeared earlier in the trace.
11+
|||
12+
||| The key faithfulness point (mirroring the typedqliser InjectionFree
13+
||| exemplar): there is NO `AffineOk` constructor for the "bad case" (a repeated
14+
||| use). A double-use trace is therefore *uninhabited* at the proof level —
15+
||| the type checker can never construct a witness that a double-use program is
16+
||| affine-safe. We give a sound+complete decision procedure returning a real
17+
||| `Dec`, a certifier into the ABI `Result` type with a soundness theorem, and
18+
||| both a positive control (a witness for a safe trace) and a negative control
19+
||| (a machine-checked `Not` for a double-use trace).
20+
21+
module Affinescriptiser.ABI.Semantics
22+
23+
import Affinescriptiser.ABI.Types
24+
import Data.List.Elem
25+
import Decidable.Equality
26+
27+
%default total
28+
29+
--------------------------------------------------------------------------------
30+
-- Faithful domain model
31+
--------------------------------------------------------------------------------
32+
33+
||| A variable identifier. Concrete, decidable identity (Nat has DecEq).
34+
public export
35+
Var : Type
36+
Var = Nat
37+
38+
||| A usage trace: the ordered sequence of variable uses emitted by codegen.
39+
||| `[]` is the empty program; `v :: rest` means "use v, then run rest".
40+
public export
41+
Trace : Type
42+
Trace = List Var
43+
44+
--------------------------------------------------------------------------------
45+
-- The headline property: AffineOk
46+
--------------------------------------------------------------------------------
47+
48+
||| `AffineOk t` holds when no variable in trace `t` is used more than once.
49+
|||
50+
||| There are exactly two ways to be affine-safe:
51+
||| * the empty trace is trivially safe; and
52+
||| * a non-empty trace `v :: rest` is safe when `v` does NOT occur in `rest`
53+
||| (so this is `v`'s only use here) AND `rest` is itself safe.
54+
|||
55+
||| Crucially there is NO constructor for "v occurs again in rest" — a
56+
||| double-use trace simply has no inhabitant of this type. Affine safety is
57+
||| therefore a genuine structural invariant, not a runtime check.
58+
public export
59+
data AffineOk : Trace -> Type where
60+
||| The empty program uses nothing, so it is affine-safe.
61+
NilOk : AffineOk []
62+
||| Using `v` is safe when `v` is not used again later, and the rest is safe.
63+
ConsOk : (notLater : Not (Elem v rest)) -> AffineOk rest -> AffineOk (v :: rest)
64+
65+
--------------------------------------------------------------------------------
66+
-- Inversion lemmas (term-level, to avoid stuck case-of-Refl)
67+
--------------------------------------------------------------------------------
68+
69+
||| If `v :: rest` is affine-safe then `v` is not used again in `rest`.
70+
export
71+
headNotLater : AffineOk (v :: rest) -> Not (Elem v rest)
72+
headNotLater (ConsOk notLater _) = notLater
73+
74+
||| If `v :: rest` is affine-safe then `rest` is affine-safe.
75+
export
76+
tailOk : AffineOk (v :: rest) -> AffineOk rest
77+
tailOk (ConsOk _ ok) = ok
78+
79+
--------------------------------------------------------------------------------
80+
-- Sound + complete decision procedure
81+
--------------------------------------------------------------------------------
82+
83+
||| Decide affine safety of a trace. Returns a genuine `Dec (AffineOk t)`:
84+
||| a `Yes` carries a real proof, a `No` carries a real refutation built from
85+
||| the inversion lemmas above. No `believe_me`, no postulates.
86+
public export
87+
decAffineOk : (t : Trace) -> Dec (AffineOk t)
88+
decAffineOk [] = Yes NilOk
89+
decAffineOk (v :: rest) =
90+
case isElem v rest of
91+
-- v is used again later: any AffineOk witness would contradict it.
92+
Yes used => No (\ok => headNotLater ok used)
93+
No notLater =>
94+
case decAffineOk rest of
95+
Yes restOk => Yes (ConsOk notLater restOk)
96+
No restBad => No (\ok => restBad (tailOk ok))
97+
98+
--------------------------------------------------------------------------------
99+
-- Certifier into the ABI Result type + soundness theorem
100+
--------------------------------------------------------------------------------
101+
102+
||| Certify a trace: `Ok` when affine-safe, `AffineViolation` (an existing ABI
103+
||| Result code) when a variable is used more than once.
104+
public export
105+
certifyAffine : (t : Trace) -> Result
106+
certifyAffine t = case decAffineOk t of
107+
Yes _ => Ok
108+
No _ => AffineViolation
109+
110+
||| Soundness: if the certifier says `Ok`, the trace really is affine-safe.
111+
||| We recover the witness the decision procedure found.
112+
export
113+
certifyAffineSound : (t : Trace) -> certifyAffine t = Ok -> AffineOk t
114+
certifyAffineSound t prf with (decAffineOk t)
115+
certifyAffineSound t prf | Yes ok = ok
116+
certifyAffineSound t Refl | No _ impossible
117+
118+
||| Completeness (other direction): if the trace is affine-safe, the certifier
119+
||| says `Ok`. Together with soundness this makes `certifyAffine` exact.
120+
export
121+
certifyAffineComplete : (t : Trace) -> AffineOk t -> certifyAffine t = Ok
122+
certifyAffineComplete t ok with (decAffineOk t)
123+
certifyAffineComplete t ok | Yes _ = Refl
124+
certifyAffineComplete t ok | No bad = absurd (bad ok)
125+
126+
--------------------------------------------------------------------------------
127+
-- Positive control: an inhabited witness for a safe program
128+
--------------------------------------------------------------------------------
129+
130+
||| A safe trace uses three distinct variables once each: [0, 1, 2].
131+
||| The witness is explicit — each `Not (Elem ...)` is discharged by the
132+
||| `Uninhabited (Elem x [])` instance and off-diagonal Nat decisions, all
133+
||| of which reduce on concrete literals.
134+
export
135+
safeTraceAffineOk : AffineOk [0, 1, 2]
136+
safeTraceAffineOk =
137+
ConsOk (\el => case el of
138+
There (There el2) => absurd el2)
139+
(ConsOk (\el => case el of
140+
There el1 => absurd el1)
141+
(ConsOk absurd NilOk))
142+
143+
--------------------------------------------------------------------------------
144+
-- Negative control: a double-use program is NOT affine-safe
145+
--------------------------------------------------------------------------------
146+
147+
||| Variable 0 is used twice in [0, 0]. There is no `AffineOk` witness for it:
148+
||| the head's `notLater` proof would have to refute `Elem 0 [0]`, but `0` is
149+
||| right there (`Here`). Machine-checked refutation, the heart of the claim.
150+
export
151+
doubleUseNotAffineOk : Not (AffineOk [0, 0])
152+
doubleUseNotAffineOk ok = headNotLater ok Here
153+
154+
||| A subtler double-use: variable 5 is reused after an intervening distinct
155+
||| use of 7, in [5, 7, 5]. Still refuted: 5 reappears later in the tail.
156+
export
157+
spacedDoubleUseNotAffineOk : Not (AffineOk [5, 7, 5])
158+
spacedDoubleUseNotAffineOk ok = headNotLater ok (There Here)

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,3 +7,4 @@ modules = Affinescriptiser.ABI.Types
77
, Affinescriptiser.ABI.Layout
88
, Affinescriptiser.ABI.Foreign
99
, Affinescriptiser.ABI.Proofs
10+
, Affinescriptiser.ABI.Semantics

0 commit comments

Comments
 (0)