Skip to content

Commit 9d5e5d8

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
feat(abi): prove Conformant scaffold property (Layer 2 Semantics) (#73)
Add Iseriser.ABI.Semantics proving the headline domain property: a generated -iser scaffold is Conformant exactly when all five required components (Manifest, Idris2 ABI, Zig FFI, Codegen, Rust CLI) are present. Conformant is built from genuine Data.List.Elem membership obligations with no catch-all constructor, so a scaffold missing any component has no witness. Includes a sound+complete decConformant : (s) -> Dec (Conformant s), a soundness fact certifyConformantSound, a positive control (completeIsConformant via explicit Elem positions), and a negative control (ffiMissingNotConformant : Not (Conformant ffiMissing)). Non-vacuity confirmed: a deliberately-false Has Ffi witness for the FFI-missing scaffold is rejected by idris2. Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx Co-authored-by: Claude <noreply@anthropic.com>
1 parent 024dbbd commit 9d5e5d8

2 files changed

Lines changed: 204 additions & 0 deletions

File tree

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

Lines changed: 203 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,203 @@
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 iseriser (Layer 2 ABI).
5+
|||
6+
||| Headline: "Meta-framework that generates new -iser projects."
7+
|||
8+
||| A generated -iser scaffold is faithful only when ALL of the five
9+
||| architectural components named in the project doctrine are present:
10+
|||
11+
||| Manifest · Idris2 ABI · Zig FFI · Codegen · Rust CLI
12+
|||
13+
||| We model a scaffold as the set of components it actually produced, and
14+
||| prove a `Conformant` proposition that holds EXACTLY when every required
15+
||| component is present. The bad case (a scaffold missing any component)
16+
||| has no `Conformant` witness — this is enforced structurally, not by an
17+
||| opaque boolean. The decision procedure is sound AND complete, and the
18+
||| negative control shows a scaffold missing the FFI is provably not
19+
||| Conformant.
20+
21+
module Iseriser.ABI.Semantics
22+
23+
import Iseriser.ABI.Types
24+
import Data.List.Elem
25+
import Decidable.Equality
26+
27+
%default total
28+
29+
--------------------------------------------------------------------------------
30+
-- Faithful domain model
31+
--------------------------------------------------------------------------------
32+
33+
||| The five architectural components every generated -iser must contain.
34+
||| These mirror the doctrine in .claude/CLAUDE.md:
35+
||| Manifest, Idris2 ABI, Zig FFI, Codegen, Rust CLI.
36+
public export
37+
data Component : Type where
38+
Manifest : Component -- <name>.toml: user describes WHAT they want
39+
Abi : Component -- src/interface/abi: Idris2 formal proofs
40+
Ffi : Component -- ffi/zig: C-ABI bridge
41+
Codegen : Component -- src/codegen: target-language wrapper generation
42+
Cli : Component -- src/main.rs: Rust orchestrator
43+
44+
||| A generated scaffold is the (finite) list of components it produced.
45+
public export
46+
record Scaffold where
47+
constructor MkScaffold
48+
components : List Component
49+
50+
--------------------------------------------------------------------------------
51+
-- Decidable equality on Component (needed for membership)
52+
--------------------------------------------------------------------------------
53+
54+
public export
55+
DecEq Component where
56+
decEq Manifest Manifest = Yes Refl
57+
decEq Abi Abi = Yes Refl
58+
decEq Ffi Ffi = Yes Refl
59+
decEq Codegen Codegen = Yes Refl
60+
decEq Cli Cli = Yes Refl
61+
62+
decEq Manifest Abi = No (\case Refl impossible)
63+
decEq Manifest Ffi = No (\case Refl impossible)
64+
decEq Manifest Codegen = No (\case Refl impossible)
65+
decEq Manifest Cli = No (\case Refl impossible)
66+
decEq Abi Manifest = No (\case Refl impossible)
67+
decEq Abi Ffi = No (\case Refl impossible)
68+
decEq Abi Codegen = No (\case Refl impossible)
69+
decEq Abi Cli = No (\case Refl impossible)
70+
decEq Ffi Manifest = No (\case Refl impossible)
71+
decEq Ffi Abi = No (\case Refl impossible)
72+
decEq Ffi Codegen = No (\case Refl impossible)
73+
decEq Ffi Cli = No (\case Refl impossible)
74+
decEq Codegen Manifest = No (\case Refl impossible)
75+
decEq Codegen Abi = No (\case Refl impossible)
76+
decEq Codegen Ffi = No (\case Refl impossible)
77+
decEq Codegen Cli = No (\case Refl impossible)
78+
decEq Cli Manifest = No (\case Refl impossible)
79+
decEq Cli Abi = No (\case Refl impossible)
80+
decEq Cli Ffi = No (\case Refl impossible)
81+
decEq Cli Codegen = No (\case Refl impossible)
82+
83+
--------------------------------------------------------------------------------
84+
-- The headline property: Conformant
85+
--------------------------------------------------------------------------------
86+
87+
||| `Has c s` is a genuine membership obligation: component `c` is in the
88+
||| scaffold's produced component list. There is NO way to construct it for
89+
||| an absent component (it reduces to `Data.List.Elem`, which has no
90+
||| inhabitant for the empty list).
91+
public export
92+
Has : Component -> Scaffold -> Type
93+
Has c s = Elem c (components s)
94+
95+
||| A scaffold is `Conformant` EXACTLY when each of the five required
96+
||| components is present. Each field is a real membership proof; the
97+
||| proposition is uninhabited the moment any component is missing.
98+
||| (No catch-all constructor: this cannot be faked.)
99+
public export
100+
data Conformant : Scaffold -> Type where
101+
MkConformant :
102+
Has Manifest s
103+
-> Has Abi s
104+
-> Has Ffi s
105+
-> Has Codegen s
106+
-> Has Cli s
107+
-> Conformant s
108+
109+
--------------------------------------------------------------------------------
110+
-- Sound + complete decision procedure
111+
--------------------------------------------------------------------------------
112+
113+
||| Decide membership of a component in a scaffold.
114+
decHas : (c : Component) -> (s : Scaffold) -> Dec (Has c s)
115+
decHas c s = isElem c (components s)
116+
117+
||| Decide whether a scaffold is Conformant. Returns a REAL proof when all
118+
||| five components are present, and a refutation when any is missing. The
119+
||| refutation projects the relevant field out of a hypothetical witness, so
120+
||| completeness is machine-checked (not asserted).
121+
public export
122+
decConformant : (s : Scaffold) -> Dec (Conformant s)
123+
decConformant s =
124+
case decHas Manifest s of
125+
No nm => No (\(MkConformant m _ _ _ _) => nm m)
126+
Yes m => case decHas Abi s of
127+
No na => No (\(MkConformant _ a _ _ _) => na a)
128+
Yes a => case decHas Ffi s of
129+
No nf => No (\(MkConformant _ _ f _ _) => nf f)
130+
Yes f => case decHas Codegen s of
131+
No ng => No (\(MkConformant _ _ _ g _) => ng g)
132+
Yes g => case decHas Cli s of
133+
No nc => No (\(MkConformant _ _ _ _ c) => nc c)
134+
Yes c => Yes (MkConformant m a f g c)
135+
136+
--------------------------------------------------------------------------------
137+
-- Certifier + soundness fact
138+
--------------------------------------------------------------------------------
139+
140+
||| Map a scaffold to a `ProofStatus`-shaped verdict reusing the ABI's
141+
||| `Result` codes: `Ok` means Conformant, `InvalidLanguage` means a
142+
||| required component is missing.
143+
public export
144+
certifyConformant : (s : Scaffold) -> Result
145+
certifyConformant s =
146+
case decConformant s of
147+
Yes _ => Ok
148+
No _ => InvalidLanguage
149+
150+
||| Soundness of the certifier: if it returns `Ok`, a genuine `Conformant`
151+
||| witness exists. Proven by case-analysis on the SAME decision the
152+
||| certifier uses; the `No` branch is impossible because `Ok = InvalidLanguage`
153+
||| is absurd.
154+
public export
155+
certifyConformantSound :
156+
(s : Scaffold)
157+
-> certifyConformant s = Ok
158+
-> Conformant s
159+
certifyConformantSound s prf with (decConformant s)
160+
certifyConformantSound s prf | Yes ok = ok
161+
certifyConformantSound s Refl | No _ impossible
162+
163+
--------------------------------------------------------------------------------
164+
-- Positive control: a complete scaffold IS Conformant
165+
--------------------------------------------------------------------------------
166+
167+
||| A faithfully complete scaffold — all five components, in canonical order.
168+
public export
169+
completeScaffold : Scaffold
170+
completeScaffold = MkScaffold [Manifest, Abi, Ffi, Codegen, Cli]
171+
172+
||| Explicit witness that the complete scaffold is Conformant. Each `Has`
173+
||| proof is a concrete `Elem` position into the literal list above, so this
174+
||| type-checks by reduction with no appeal to the decision procedure.
175+
public export
176+
completeIsConformant : Conformant Semantics.completeScaffold
177+
completeIsConformant =
178+
MkConformant
179+
Here -- Manifest at position 0
180+
(There Here) -- Abi at position 1
181+
(There (There Here)) -- Ffi at position 2
182+
(There (There (There Here))) -- Codegen at position 3
183+
(There (There (There (There Here)))) -- Cli at position 4
184+
185+
--------------------------------------------------------------------------------
186+
-- Negative control: a scaffold missing the FFI is NOT Conformant
187+
--------------------------------------------------------------------------------
188+
189+
||| A scaffold that produced everything EXCEPT the Zig FFI bridge.
190+
public export
191+
ffiMissingScaffold : Scaffold
192+
ffiMissingScaffold = MkScaffold [Manifest, Abi, Codegen, Cli]
193+
194+
||| Machine-checked refutation: with no `Ffi` component, no `Conformant`
195+
||| witness can exist. We pull the `Has Ffi` field out of any hypothetical
196+
||| witness and discharge it — `Ffi` is not among the four present
197+
||| components, so every membership position is impossible.
198+
public export
199+
ffiMissingNotConformant : Not (Conformant Semantics.ffiMissingScaffold)
200+
ffiMissingNotConformant (MkConformant _ _ f _ _) = noFfi f
201+
where
202+
noFfi : Not (Elem Ffi [Manifest, Abi, Codegen, Cli])
203+
noFfi (There (There (There (There prf)))) impossible

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

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

0 commit comments

Comments
 (0)