Skip to content

Commit 6f102af

Browse files
hyperpolymathJonathan D.A. Jewellclaude
authored
iseriser: make Phase 0 ABI proofs genuinely compile and verify (#67)
* iseriser: make Phase 0 ABI proofs genuinely compile and verify The hand-written Idris2 ABI was never compiler-checked and did not typecheck under Idris2 0.7.0. Make the foundation real and machine-verified. Layout.idr - Discharge the two open holes: ?fieldsAlignedProof and ?offsetInBoundsProof. - Add a sound decDivides decision procedure (builds genuine m = k*n witnesses) and decFieldsAligned; checkCABI now returns a real CABICompliant proof or an error. - offsetInBounds had an unsound signature (claimed every field fits any layout); make it an honest decidable Maybe. - Fix paddingFor (Nat has no Neg; use minus) and give the three concrete struct layouts explicit alignment witnesses. - Replace alignUpCorrect's non-compiling Refl proof with a sound alignUpDivides decision; the general lemma is noted as residual work. Types.idr - FullyResolved and GenerationComplete carried no obligation; give them real So-proofs (no {{/}} markers remain; all seven categories present). - thisPlatform was a %runElab stub needing ElabReflection; make it total. - DecEq Result used `No absurd` with no Uninhabited instance; discharge the off-diagonal cases explicitly. - createHandle left the auto So (ptr /= 0) unsolved; use choose. Proofs.idr (new) - Machine-checked theorems: the three concrete FFI struct layouts are provably C-ABI aligned; Result→C-int pins; generation-completeness. Structure / tooling - Move ABI into src/interface/abi/Iseriser/ABI/ so it builds as an Idris2 package (matches the chapeliser layout); add iseriser-abi.ipkg. - Add `just proofs` recipe; ignore Idris build artifacts. - verification/proofs/ now documents and points at the verified proofs. Verified: `idris2 --build iseriser-abi.ipkg` clean (0 warnings); cargo test green (57 unit + 9 integration). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA * Add SPDX header to LICENSE and set Cargo.toml license field The governance/licence-consistency check requires an SPDX-License-Identifier header on the LICENSE file and a `license` field in the manifest. The LICENSE body is MPL-2.0 text, so stamp `SPDX-License-Identifier: MPL-2.0` (matching the actual body) and set `license = "MPL-2.0"` (replacing `license-file`). Verified with standards/scripts/check-licence-consistency.sh (passes). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA --------- Co-authored-by: Jonathan D.A. Jewell <paraordinate@yahoo.co.uk> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
1 parent c0eb925 commit 6f102af

11 files changed

Lines changed: 496 additions & 257 deletions

File tree

‎.gitignore‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,11 @@ Thumbs.db
1616
/_build/
1717
/build/
1818
/dist/
19+
20+
# Idris2 proof build artifacts (any nested build/ dir + TTC output)
21+
**/build/
22+
*.ttc
23+
*.ttm
1924
/out/
2025

2126
# Dependencies

‎Cargo.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ version = "0.1.0"
55
edition = "2024"
66
authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
77
description = "Meta-framework that generates new -iser projects from a target language interop description"
8-
license-file = "LICENSE"
8+
license = "MPL-2.0"
99
repository = "https://github.com/hyperpolymath/iseriser"
1010
keywords = ["meta-framework", "code-generation", "language-interop", "scaffolding"]
1111
categories = ["command-line-utilities", "development-tools"]

‎Justfile‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,11 @@ build:
1414
test:
1515
cargo test
1616

17+
# Type-check the Idris2 ABI formal proofs (requires idris2 >= 0.7.0)
18+
proofs:
19+
cd src/interface/abi && idris2 --build iseriser-abi.ipkg
20+
@echo "Idris2 ABI proofs type-check cleanly"
21+
1722
# Run clippy lints
1823
lint:
1924
cargo clippy -- -D warnings

‎LICENSE‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
SPDX-License-Identifier: MPL-2.0
2+
13
Mozilla Public License Version 2.0
24
==================================
35

src/interface/abi/Foreign.idr renamed to src/interface/abi/Iseriser/ABI/Foreign.idr

File renamed without changes.

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

Lines changed: 215 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,215 @@
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+
||| Memory Layout Proofs for Iseriser
5+
6+
module Iseriser.ABI.Layout
7+
8+
import Iseriser.ABI.Types
9+
import Data.Vect
10+
import Data.So
11+
import Data.Nat
12+
import Decidable.Equality
13+
14+
%default total
15+
16+
public export
17+
paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
18+
paddingFor offset alignment =
19+
if offset `mod` alignment == 0
20+
then 0
21+
else minus alignment (offset `mod` alignment)
22+
23+
public export
24+
alignUp : (size : Nat) -> (alignment : Nat) -> Nat
25+
alignUp size alignment =
26+
size + paddingFor size alignment
27+
28+
||| Proof that alignment divides aligned size: `m = k * n`.
29+
public export
30+
data Divides : Nat -> Nat -> Type where
31+
DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
32+
33+
||| Sound decision procedure for divisibility. Returns a genuine
34+
||| `Divides n m` witness when `n` evenly divides `m`, otherwise Nothing.
35+
||| Division by zero is undecidable here and yields Nothing.
36+
public export
37+
decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
38+
decDivides Z _ = Nothing
39+
decDivides (S k) m =
40+
let q = m `div` (S k) in
41+
case decEq m (q * (S k)) of
42+
Yes prf => Just (DivideBy q prf)
43+
No _ => Nothing
44+
45+
||| Sound divisibility check for an aligned size. The general theorem
46+
||| "alignUp size align is always divisible by align" needs div/mod lemmas
47+
||| from Data.Nat and is tracked as residual proof work; here we *decide* it
48+
||| via `decDivides`, which returns a genuine witness when it holds. For the
49+
||| concrete ABI layouts below, divisibility is proven outright (`DivideBy`).
50+
||| (Previously `alignUpCorrect … = DivideBy … Refl`, whose `Refl` cannot
51+
||| typecheck for symbolic inputs.)
52+
public export
53+
alignUpDivides : (size : Nat) -> (align : Nat) ->
54+
Maybe (Divides align (alignUp size align))
55+
alignUpDivides size align = decDivides align (alignUp size align)
56+
57+
public export
58+
record Field where
59+
constructor MkField
60+
name : String
61+
offset : Nat
62+
size : Nat
63+
alignment : Nat
64+
65+
public export
66+
nextFieldOffset : Field -> Nat
67+
nextFieldOffset f = alignUp (f.offset + f.size) f.alignment
68+
69+
public export
70+
record StructLayout where
71+
constructor MkStructLayout
72+
fields : Vect n Field
73+
totalSize : Nat
74+
alignment : Nat
75+
{auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))}
76+
{auto 0 aligned : Divides alignment totalSize}
77+
78+
public export
79+
calcStructSize : Vect k Field -> Nat -> Nat
80+
calcStructSize [] align = 0
81+
calcStructSize (f :: fs) align =
82+
let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
83+
lastSize = foldr (\field, _ => field.size) f.size fs
84+
in alignUp (lastOffset + lastSize) align
85+
86+
||| C-compatible layout for the language model data passed through FFI.
87+
public export
88+
languageModelDataLayout : StructLayout
89+
languageModelDataLayout =
90+
MkStructLayout
91+
[ MkField "name_ptr" 0 8 8
92+
, MkField "name_len" 8 4 4
93+
, MkField "num_features" 12 4 4
94+
, MkField "features_ptr" 16 8 8
95+
, MkField "target" 24 4 4
96+
, MkField "padding" 28 4 4
97+
]
98+
32
99+
8
100+
{sizeCorrect = Oh}
101+
{aligned = DivideBy 4 Refl}
102+
103+
||| C-compatible layout for template data passed to the expansion engine.
104+
public export
105+
templateDataLayout : StructLayout
106+
templateDataLayout =
107+
MkStructLayout
108+
[ MkField "template_ptr" 0 8 8
109+
, MkField "template_len" 8 4 4
110+
, MkField "padding1" 12 4 4
111+
, MkField "output_ptr" 16 8 8
112+
, MkField "output_len" 24 4 4
113+
, MkField "is_lang_spec" 28 4 4
114+
]
115+
32
116+
8
117+
{sizeCorrect = Oh}
118+
{aligned = DivideBy 4 Refl}
119+
120+
||| C-compatible layout for the generation context handle.
121+
public export
122+
generationContextLayout : StructLayout
123+
generationContextLayout =
124+
MkStructLayout
125+
[ MkField "model_ptr" 0 8 8
126+
, MkField "templates_ptr" 8 8 8
127+
, MkField "num_templates" 16 4 4
128+
, MkField "artifacts_count" 20 4 4
129+
, MkField "output_dir_ptr" 24 8 8
130+
, MkField "output_dir_len" 32 4 4
131+
, MkField "initialized" 36 4 4
132+
, MkField "error_code" 40 4 4
133+
, MkField "padding" 44 4 4
134+
]
135+
48
136+
8
137+
{sizeCorrect = Oh}
138+
{aligned = DivideBy 6 Refl}
139+
140+
||| Proof that every field offset in a layout is correctly aligned.
141+
public export
142+
data FieldsAligned : Vect k Field -> Type where
143+
NoFields : FieldsAligned []
144+
ConsField :
145+
(f : Field) ->
146+
(rest : Vect k Field) ->
147+
Divides f.alignment f.offset ->
148+
FieldsAligned rest ->
149+
FieldsAligned (f :: rest)
150+
151+
||| Decide field alignment for every field, building a real `FieldsAligned`
152+
||| witness from per-field divisibility proofs.
153+
public export
154+
decFieldsAligned : (fs : Vect k Field) -> Maybe (FieldsAligned fs)
155+
decFieldsAligned [] = Just NoFields
156+
decFieldsAligned (f :: fs) =
157+
case decDivides f.alignment f.offset of
158+
Nothing => Nothing
159+
Just dvd => case decFieldsAligned fs of
160+
Nothing => Nothing
161+
Just rest => Just (ConsField f fs dvd rest)
162+
163+
||| Proof that a struct layout follows C ABI alignment rules.
164+
public export
165+
data CABICompliant : StructLayout -> Type where
166+
CABIOk :
167+
(layout : StructLayout) ->
168+
FieldsAligned layout.fields ->
169+
CABICompliant layout
170+
171+
||| Verify a layout against the C ABI alignment rules, returning a genuine
172+
||| `CABICompliant` proof (built from real per-field divisibility witnesses)
173+
||| or an error when some field offset is misaligned.
174+
public export
175+
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
176+
checkCABI layout =
177+
case decFieldsAligned layout.fields of
178+
Just prf => Right (CABIOk layout prf)
179+
Nothing => Left "Field offsets are not correctly aligned for the C ABI"
180+
181+
||| Verify that all iseriser layouts are C-ABI compliant. This now fails
182+
||| (Left) if any concrete layout is misaligned, rather than asserting it.
183+
public export
184+
verifyAllLayouts : Either String ()
185+
verifyAllLayouts = do
186+
_ <- checkCABI languageModelDataLayout
187+
_ <- checkCABI templateDataLayout
188+
_ <- checkCABI generationContextLayout
189+
Right ()
190+
191+
||| All 64-bit platforms (Linux, Windows, MacOS, BSD) use 8-byte pointers and
192+
||| 4-byte ints, so the LanguageModelData layout is identical across them.
193+
public export
194+
verifyLanguageModelPortability : Either String ()
195+
verifyLanguageModelPortability = Right ()
196+
197+
||| Look up a field's offset by name in a layout.
198+
public export
199+
fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (Nat, Field)
200+
fieldOffset layout name =
201+
case findIndex (\f => f.name == name) layout.fields of
202+
Just idx => Just (finToNat idx, index idx layout.fields)
203+
Nothing => Nothing
204+
205+
||| Decide whether a field lies within a struct's byte bounds, returning a
206+
||| genuine proof when `offset + size <= totalSize`. The previous signature
207+
||| asserted this for *every* field unconditionally, which is false (a field
208+
||| need not belong to the layout); this honest version decides it.
209+
public export
210+
offsetInBounds : (layout : StructLayout) -> (f : Field) ->
211+
Maybe (So (f.offset + f.size <= layout.totalSize))
212+
offsetInBounds layout f =
213+
case choose (f.offset + f.size <= layout.totalSize) of
214+
Left ok => Just ok
215+
Right _ => Nothing

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

Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
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+
||| Machine-checked proofs over the iseriser ABI.
5+
|||
6+
||| These are not runtime tests — they are propositional statements the Idris2
7+
||| type checker must discharge at compile time. If any concrete ABI layout
8+
||| were misaligned, the result-code encoding wrong, or a decision procedure
9+
||| mis-defined, this module would fail to typecheck and the proof build would
10+
||| go red.
11+
|||
12+
||| The C-ABI compliance witnesses are built directly from per-field
13+
||| divisibility proofs (`DivideBy k Refl`, where `offset = k * alignment`).
14+
||| Multiplication reduces during type checking, so these are fully verified
15+
||| by the compiler; we avoid routing them through `Nat` division, which is a
16+
||| primitive that does not reduce at the type level.
17+
18+
module Iseriser.ABI.Proofs
19+
20+
import Iseriser.ABI.Types
21+
import Iseriser.ABI.Layout
22+
import Data.So
23+
import Data.Vect
24+
25+
%default total
26+
27+
--------------------------------------------------------------------------------
28+
-- The concrete FFI struct layouts are provably C-ABI compliant.
29+
--------------------------------------------------------------------------------
30+
31+
||| Every field offset in the LanguageModelData layout divides its alignment:
32+
||| 0|8, 8|4, 12|4, 16|8, 24|4, 28|4.
33+
export
34+
languageModelDataCompliant : CABICompliant Layout.languageModelDataLayout
35+
languageModelDataCompliant =
36+
CABIOk languageModelDataLayout
37+
(ConsField _ _ (DivideBy 0 Refl)
38+
(ConsField _ _ (DivideBy 2 Refl)
39+
(ConsField _ _ (DivideBy 3 Refl)
40+
(ConsField _ _ (DivideBy 2 Refl)
41+
(ConsField _ _ (DivideBy 6 Refl)
42+
(ConsField _ _ (DivideBy 7 Refl)
43+
NoFields))))))
44+
45+
||| Every field offset in the TemplateData layout is aligned:
46+
||| 0|8, 8|4, 12|4, 16|8, 24|4, 28|4.
47+
export
48+
templateDataCompliant : CABICompliant Layout.templateDataLayout
49+
templateDataCompliant =
50+
CABIOk templateDataLayout
51+
(ConsField _ _ (DivideBy 0 Refl)
52+
(ConsField _ _ (DivideBy 2 Refl)
53+
(ConsField _ _ (DivideBy 3 Refl)
54+
(ConsField _ _ (DivideBy 2 Refl)
55+
(ConsField _ _ (DivideBy 6 Refl)
56+
(ConsField _ _ (DivideBy 7 Refl)
57+
NoFields))))))
58+
59+
||| Every field offset in the GenerationContext layout is aligned:
60+
||| 0|8, 8|8, 16|4, 20|4, 24|8, 32|4, 36|4, 40|4, 44|4.
61+
export
62+
generationContextCompliant : CABICompliant Layout.generationContextLayout
63+
generationContextCompliant =
64+
CABIOk generationContextLayout
65+
(ConsField _ _ (DivideBy 0 Refl)
66+
(ConsField _ _ (DivideBy 1 Refl)
67+
(ConsField _ _ (DivideBy 4 Refl)
68+
(ConsField _ _ (DivideBy 5 Refl)
69+
(ConsField _ _ (DivideBy 3 Refl)
70+
(ConsField _ _ (DivideBy 8 Refl)
71+
(ConsField _ _ (DivideBy 9 Refl)
72+
(ConsField _ _ (DivideBy 10 Refl)
73+
(ConsField _ _ (DivideBy 11 Refl)
74+
NoFields)))))))))
75+
76+
--------------------------------------------------------------------------------
77+
-- Result-code round-trip: the encoding the Zig FFI depends on.
78+
--------------------------------------------------------------------------------
79+
80+
export
81+
okIsZero : resultToInt Ok = 0
82+
okIsZero = Refl
83+
84+
export
85+
nullPointerIsFive : resultToInt NullPointer = 5
86+
nullPointerIsFive = Refl
87+
88+
--------------------------------------------------------------------------------
89+
-- Generation completeness: the full required set is accepted; a short set isn't.
90+
--------------------------------------------------------------------------------
91+
92+
||| The complete set of seven categories is recognised as complete.
93+
export
94+
fullSetComplete : So (allCategoriesPresent Types.requiredCategories)
95+
fullSetComplete = Oh
96+
97+
||| A set missing RSRGovernance is correctly rejected as incomplete.
98+
export
99+
shortSetIncomplete : So (not (allCategoriesPresent
100+
[CargoToml, RustSource, Idris2ABI, ZigFFI, CIWorkflows, Documentation]))
101+
shortSetIncomplete = Oh

0 commit comments

Comments
 (0)