Skip to content

Commit 1692561

Browse files
hyperpolymathJonathan D.A. Jewellclaude
authored
ABI: make Idris2 proofs genuinely compile + add machine-checked theorems (#38)
* 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 * Normalize licensing to MPL-2.0 (code) + CC-BY-SA-4.0 (docs) Make the repo's licensing single and consistent, matching the wokelangiser reference policy and the merged iseriser pattern: - Remove contradictory PMPL-1.0-or-later / Palimpsest self-claims from README badges/footers, QUICKSTART, RSR_OUTLINE, STATE-VISUALIZER, and machine-readable governance (META, stapeln, deny.toml allow-list, copilot/AGENTIC SPDX directives, Trust/Must LICENSE-content checks, per-project CLAUDE.md). - Encode the docs split in REUSE dep5: *.adoc/*.md/docs/** -> CC-BY-SA-4.0, everything else -> MPL-2.0. - READMEs show MPL-2.0 (code) + CC-BY-SA-4.0 (docs) badges; full texts live in LICENSES/; root LICENSE stays MPL-2.0 for GitHub's licence chip. Preserves legitimate non-self references: cargo-deny's AGPL deny-list, the "never use AGPL" estate policy, and the Contributor Covenant CoC. Verified: standards/scripts/check-licence-consistency.sh passes; no residual PMPL/Palimpsest self-claims remain. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA * Fix idrisiser Idris2 ABI proofs to genuinely compile and verify The src/interface/abi ABI was scaffolded from a template and never compiler-checked. This makes all of it typecheck cleanly under Idris2 0.7.0 (zero errors, zero warnings) with genuine, machine-checked proofs. Types.idr: - Replace the %runElab thisPlatform stub (needs ElabReflection) with a plain value (Linux). - DecEq Result: replace the non-compiling `decEq _ _ = No absurd` catch-all with explicit off-diagonal disequality cases for all 30 ordered distinct constructor pairs (\case Refl impossible). - createHandle: solve the {auto 0 nonNull : So (ptr /= 0)} obligation via Data.So.choose instead of leaving it unsolved. Layout.idr: - paddingFor: use Data.Nat.minus instead of Nat subtraction (no Neg). - Add sound decDivides decision procedure (div + decEq) producing real Divides witnesses; replace the unsound `alignUpCorrect ... = DivideBy ... Refl` with alignUpDivides built on decDivides. - checkCABI: implement decFieldsAligned over the Vect of fields and build a genuine FieldsAligned witness; drop the ?fieldsAlignedProof hole. - offsetInBounds: change the unsound universally-quantified So return type to Maybe (So ...) decided via choose. - Add three concrete C-ABI struct layouts (proofEngineContext, proofObligation, handleData) with explicit erased proofs {sizeCorrect = Oh} and {aligned = DivideBy k Refl}; add verifyAllLayouts. Proofs.idr (new): machine-checked theorems — - proofEngineContextCompliant / proofObligationCompliant / handleDataCompliant: CABICompliant witnesses built directly from per-field DivideBy k Refl proofs (multiplication reduces at typecheck). - okIsZero, proofFailureIsFive: pin the FFI result-code encoding. - okNotNullPointer: distinct codes encode distinctly. Build packaging: - git mv flat files to src/interface/abi/Idrisiser/ABI/{Types,Layout, Foreign}.idr to match module namespaces. - Add src/interface/abi/idrisiser-abi.ipkg. - .gitignore: add **/build/, *.ttc, *.ttm. No believe_me / assert_total / idris_crash / postulate / %hint / holes. 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 7f1691c commit 1692561

6 files changed

Lines changed: 272 additions & 30 deletions

File tree

‎.gitignore‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -104,3 +104,8 @@ sync_report*.txt
104104
# Hypatia scan cache (local-only)
105105
.hypatia/
106106
target/
107+
108+
# Idris2 ABI proof build artefacts
109+
**/build/
110+
*.ttc
111+
*.ttm

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

File renamed without changes.

src/interface/abi/Layout.idr renamed to src/interface/abi/Idrisiser/ABI/Layout.idr

Lines changed: 122 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@ module Idrisiser.ABI.Layout
2121
import Idrisiser.ABI.Types
2222
import Data.Vect
2323
import Data.So
24+
import Data.Nat
25+
import Decidable.Equality
2426

2527
%default total
2628

@@ -36,7 +38,7 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
3638
paddingFor offset alignment =
3739
if offset `mod` alignment == 0
3840
then 0
39-
else alignment - (offset `mod` alignment)
41+
else minus alignment (offset `mod` alignment)
4042

4143
||| Proof that one natural number divides another
4244
public export
@@ -49,11 +51,29 @@ alignUp : (size : Nat) -> (alignment : Nat) -> Nat
4951
alignUp size alignment =
5052
size + paddingFor size alignment
5153

52-
||| Proof that alignUp always produces an aligned result
54+
||| Sound decision procedure for divisibility. Returns a genuine
55+
||| `Divides n m` witness when `n` evenly divides `m`, otherwise Nothing.
56+
||| Division by zero is undecidable here and yields Nothing.
5357
public export
54-
alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align)
55-
alignUpCorrect size align prf =
56-
DivideBy ((size + paddingFor size align) `div` align) Refl
58+
decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
59+
decDivides Z _ = Nothing
60+
decDivides (S k) m =
61+
let q = m `div` (S k) in
62+
case decEq m (q * (S k)) of
63+
Yes prf => Just (DivideBy q prf)
64+
No _ => Nothing
65+
66+
||| Sound divisibility check for an aligned size. The general theorem
67+
||| "alignUp size align is always divisible by align" needs div/mod lemmas
68+
||| from Data.Nat and is tracked as residual proof work; here we *decide* it
69+
||| via `decDivides`, which returns a genuine witness when it holds. For the
70+
||| concrete ABI layouts below, divisibility is proven outright (`DivideBy`).
71+
||| (Previously `alignUpCorrect … = DivideBy … Refl`, whose `Refl` cannot
72+
||| typecheck for symbolic inputs.)
73+
public export
74+
alignUpDivides : (size : Nat) -> (align : Nat) ->
75+
Maybe (Divides align (alignUp size align))
76+
alignUpDivides size align = decDivides align (alignUp size align)
5777

5878
--------------------------------------------------------------------------------
5979
-- Struct Field Layout
@@ -126,7 +146,7 @@ record StructLayout where
126146

127147
||| Calculate total struct size including all padding
128148
public export
129-
calcStructSize : Vect n Field -> Nat -> Nat
149+
calcStructSize : Vect k Field -> Nat -> Nat
130150
calcStructSize [] align = 0
131151
calcStructSize (f :: fs) align =
132152
let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
@@ -135,23 +155,84 @@ calcStructSize (f :: fs) align =
135155

136156
||| Proof that every field in a struct is properly aligned
137157
public export
138-
data FieldsAligned : Vect n Field -> Type where
158+
data FieldsAligned : Vect k Field -> Type where
139159
NoFields : FieldsAligned []
140160
ConsField :
141161
(f : Field) ->
142-
(rest : Vect n Field) ->
162+
(rest : Vect k Field) ->
143163
Divides f.alignment f.offset ->
144164
FieldsAligned rest ->
145165
FieldsAligned (f :: rest)
146166

147-
||| Verify a struct layout is valid (size accounts for fields, alignment holds)
167+
||| Decide field alignment for every field, building a real `FieldsAligned`
168+
||| witness from per-field divisibility proofs.
148169
public export
149-
verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
150-
verifyLayout fields align =
151-
let size = calcStructSize fields align
152-
in case decSo (size >= sum (map (\f => f.size) fields)) of
153-
Yes prf => Right (MkStructLayout fields size align)
154-
No _ => Left "Invalid struct size: total size is less than sum of field sizes"
170+
decFieldsAligned : (fs : Vect k Field) -> Maybe (FieldsAligned fs)
171+
decFieldsAligned [] = Just NoFields
172+
decFieldsAligned (f :: fs) =
173+
case decDivides f.alignment f.offset of
174+
Nothing => Nothing
175+
Just dvd => case decFieldsAligned fs of
176+
Nothing => Nothing
177+
Just rest => Just (ConsField f fs dvd rest)
178+
179+
--------------------------------------------------------------------------------
180+
-- Concrete Idrisiser FFI Struct Layouts
181+
--------------------------------------------------------------------------------
182+
183+
||| C-compatible layout for the proof-engine context that the Zig FFI owns.
184+
||| Every field offset is a multiple of its alignment and the total size
185+
||| (48) is a multiple of the struct alignment (8): 48 = 6 * 8.
186+
public export
187+
proofEngineContextLayout : StructLayout
188+
proofEngineContextLayout =
189+
MkStructLayout
190+
[ MkField "handle_ptr" 0 8 8
191+
, MkField "model_ptr" 8 8 8
192+
, MkField "num_obligations" 16 4 4
193+
, MkField "discharged_count" 20 4 4
194+
, MkField "error_ptr" 24 8 8
195+
, MkField "error_len" 32 4 4
196+
, MkField "initialized" 36 4 4
197+
, MkField "padding" 40 8 8
198+
]
199+
48
200+
8
201+
{sizeCorrect = Oh}
202+
{aligned = DivideBy 6 Refl}
203+
204+
||| C-compatible layout for a single proof obligation passed across the FFI.
205+
||| Total size (32) is a multiple of the struct alignment (8): 32 = 4 * 8.
206+
public export
207+
proofObligationLayout : StructLayout
208+
proofObligationLayout =
209+
MkStructLayout
210+
[ MkField "source_ptr" 0 8 8
211+
, MkField "kind" 8 4 4
212+
, MkField "discharged" 12 4 4
213+
, MkField "prooftype_ptr" 16 8 8
214+
, MkField "prooftype_len" 24 4 4
215+
, MkField "padding" 28 4 4
216+
]
217+
32
218+
8
219+
{sizeCorrect = Oh}
220+
{aligned = DivideBy 4 Refl}
221+
222+
||| C-compatible layout for the opaque handle data block.
223+
||| Total size (16) is a multiple of the struct alignment (8): 16 = 2 * 8.
224+
public export
225+
handleDataLayout : StructLayout
226+
handleDataLayout =
227+
MkStructLayout
228+
[ MkField "ptr" 0 8 8
229+
, MkField "generation" 8 4 4
230+
, MkField "flags" 12 4 4
231+
]
232+
16
233+
8
234+
{sizeCorrect = Oh}
235+
{aligned = DivideBy 2 Refl}
155236

156237
--------------------------------------------------------------------------------
157238
-- Platform-Specific Layouts
@@ -189,11 +270,25 @@ data CABICompliant : StructLayout -> Type where
189270
FieldsAligned layout.fields ->
190271
CABICompliant layout
191272

192-
||| Check whether a layout follows C ABI rules
273+
||| Verify a layout against the C ABI alignment rules, returning a genuine
274+
||| `CABICompliant` proof (built from real per-field divisibility witnesses)
275+
||| or an error when some field offset is misaligned.
193276
public export
194277
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
195278
checkCABI layout =
196-
Right (CABIOk layout ?fieldsAlignedProof)
279+
case decFieldsAligned layout.fields of
280+
Just prf => Right (CABIOk layout prf)
281+
Nothing => Left "Field offsets are not correctly aligned for the C ABI"
282+
283+
||| Verify that all concrete idrisiser layouts are C-ABI compliant. Fails
284+
||| (Left) if any layout is misaligned, rather than asserting it.
285+
public export
286+
verifyAllLayouts : Either String ()
287+
verifyAllLayouts = do
288+
_ <- checkCABI proofEngineContextLayout
289+
_ <- checkCABI proofObligationLayout
290+
_ <- checkCABI handleDataLayout
291+
Right ()
197292

198293
--------------------------------------------------------------------------------
199294
-- Interface Contract Struct Layouts
@@ -222,7 +317,14 @@ fieldOffset layout name =
222317
Just idx => Just (finToNat idx ** index idx layout.fields)
223318
Nothing => Nothing
224319

225-
||| Proof that a field's extent (offset + size) is within the struct bounds
320+
||| Decide whether a field lies within a struct's byte bounds, returning a
321+
||| genuine proof when `offset + size <= totalSize`. The previous signature
322+
||| asserted this for *every* field unconditionally, which is unsound (a field
323+
||| need not belong to the layout); this honest version decides it via `choose`.
226324
public export
227-
offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
228-
offsetInBounds layout f = ?offsetInBoundsProof
325+
offsetInBounds : (layout : StructLayout) -> (f : Field) ->
326+
Maybe (So (f.offset + f.size <= layout.totalSize))
327+
offsetInBounds layout f =
328+
case choose (f.offset + f.size <= layout.totalSize) of
329+
Left ok => Just ok
330+
Right _ => Nothing

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

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
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 idrisiser 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 Idrisiser.ABI.Proofs
19+
20+
import Idrisiser.ABI.Types
21+
import Idrisiser.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 proof-engine context layout divides its
32+
||| alignment: 0|8, 8|8, 16|4, 20|4, 24|8, 32|4, 36|4, 40|8.
33+
export
34+
proofEngineContextCompliant : CABICompliant Layout.proofEngineContextLayout
35+
proofEngineContextCompliant =
36+
CABIOk proofEngineContextLayout
37+
(ConsField _ _ (DivideBy 0 Refl)
38+
(ConsField _ _ (DivideBy 1 Refl)
39+
(ConsField _ _ (DivideBy 4 Refl)
40+
(ConsField _ _ (DivideBy 5 Refl)
41+
(ConsField _ _ (DivideBy 3 Refl)
42+
(ConsField _ _ (DivideBy 8 Refl)
43+
(ConsField _ _ (DivideBy 9 Refl)
44+
(ConsField _ _ (DivideBy 5 Refl)
45+
NoFields))))))))
46+
47+
||| Every field offset in the proof-obligation layout is aligned:
48+
||| 0|8, 8|4, 12|4, 16|8, 24|4, 28|4.
49+
export
50+
proofObligationCompliant : CABICompliant Layout.proofObligationLayout
51+
proofObligationCompliant =
52+
CABIOk proofObligationLayout
53+
(ConsField _ _ (DivideBy 0 Refl)
54+
(ConsField _ _ (DivideBy 2 Refl)
55+
(ConsField _ _ (DivideBy 3 Refl)
56+
(ConsField _ _ (DivideBy 2 Refl)
57+
(ConsField _ _ (DivideBy 6 Refl)
58+
(ConsField _ _ (DivideBy 7 Refl)
59+
NoFields))))))
60+
61+
||| Every field offset in the handle-data layout is aligned: 0|8, 8|4, 12|4.
62+
export
63+
handleDataCompliant : CABICompliant Layout.handleDataLayout
64+
handleDataCompliant =
65+
CABIOk handleDataLayout
66+
(ConsField _ _ (DivideBy 0 Refl)
67+
(ConsField _ _ (DivideBy 2 Refl)
68+
(ConsField _ _ (DivideBy 3 Refl)
69+
NoFields)))
70+
71+
--------------------------------------------------------------------------------
72+
-- Result-code encoding: the contract the Zig FFI depends on.
73+
--------------------------------------------------------------------------------
74+
75+
||| Success encodes as 0 — the FFI success sentinel.
76+
export
77+
okIsZero : resultToInt Ok = 0
78+
okIsZero = Refl
79+
80+
||| The proof-failure code encodes as 5, the highest result code.
81+
export
82+
proofFailureIsFive : resultToInt ProofFailure = 5
83+
proofFailureIsFive = Refl
84+
85+
||| Distinct result codes encode to distinct integers (Ok vs NullPointer),
86+
||| so the Zig side can disambiguate them.
87+
export
88+
okNotNullPointer : Not (resultToInt Ok = resultToInt NullPointer)
89+
okNotNullPointer = \case Refl impossible

src/interface/abi/Types.idr renamed to src/interface/abi/Idrisiser/ABI/Types.idr

Lines changed: 45 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ import Data.Bits
1616
import Data.So
1717
import Data.Vect
1818
import Data.List
19+
import Decidable.Equality
1920

2021
%default total
2122

@@ -27,12 +28,12 @@ import Data.List
2728
public export
2829
data Platform = Linux | Windows | MacOS | BSD | WASM
2930

30-
||| Compile-time platform detection
31+
||| The platform this build targets. Defaults to Linux; the Rust/Zig build
32+
||| layer overrides this via the codegen target selection. (Previously a
33+
||| `%runElab` stub that required ElabReflection and did not compile.)
3134
public export
3235
thisPlatform : Platform
33-
thisPlatform =
34-
%runElab do
35-
pure Linux -- Default; override with compiler flags per target
36+
thisPlatform = Linux
3637

3738
--------------------------------------------------------------------------------
3839
-- Interface Contract Types
@@ -207,7 +208,9 @@ resultToInt OutOfMemory = 3
207208
resultToInt NullPointer = 4
208209
resultToInt ProofFailure = 5
209210

210-
||| Results are decidably equal
211+
||| Results are decidably equal. The off-diagonal cases discharge the
212+
||| disequality explicitly; the previous `decEq _ _ = No absurd` did not
213+
||| compile (no `Uninhabited (x = y)` instance exists for these).
211214
public export
212215
DecEq Result where
213216
decEq Ok Ok = Yes Refl
@@ -216,7 +219,36 @@ DecEq Result where
216219
decEq OutOfMemory OutOfMemory = Yes Refl
217220
decEq NullPointer NullPointer = Yes Refl
218221
decEq ProofFailure ProofFailure = Yes Refl
219-
decEq _ _ = No absurd
222+
decEq Ok Error = No (\case Refl impossible)
223+
decEq Ok InvalidParam = No (\case Refl impossible)
224+
decEq Ok OutOfMemory = No (\case Refl impossible)
225+
decEq Ok NullPointer = No (\case Refl impossible)
226+
decEq Ok ProofFailure = No (\case Refl impossible)
227+
decEq Error Ok = No (\case Refl impossible)
228+
decEq Error InvalidParam = No (\case Refl impossible)
229+
decEq Error OutOfMemory = No (\case Refl impossible)
230+
decEq Error NullPointer = No (\case Refl impossible)
231+
decEq Error ProofFailure = No (\case Refl impossible)
232+
decEq InvalidParam Ok = No (\case Refl impossible)
233+
decEq InvalidParam Error = No (\case Refl impossible)
234+
decEq InvalidParam OutOfMemory = No (\case Refl impossible)
235+
decEq InvalidParam NullPointer = No (\case Refl impossible)
236+
decEq InvalidParam ProofFailure = No (\case Refl impossible)
237+
decEq OutOfMemory Ok = No (\case Refl impossible)
238+
decEq OutOfMemory Error = No (\case Refl impossible)
239+
decEq OutOfMemory InvalidParam = No (\case Refl impossible)
240+
decEq OutOfMemory NullPointer = No (\case Refl impossible)
241+
decEq OutOfMemory ProofFailure = No (\case Refl impossible)
242+
decEq NullPointer Ok = No (\case Refl impossible)
243+
decEq NullPointer Error = No (\case Refl impossible)
244+
decEq NullPointer InvalidParam = No (\case Refl impossible)
245+
decEq NullPointer OutOfMemory = No (\case Refl impossible)
246+
decEq NullPointer ProofFailure = No (\case Refl impossible)
247+
decEq ProofFailure Ok = No (\case Refl impossible)
248+
decEq ProofFailure Error = No (\case Refl impossible)
249+
decEq ProofFailure InvalidParam = No (\case Refl impossible)
250+
decEq ProofFailure OutOfMemory = No (\case Refl impossible)
251+
decEq ProofFailure NullPointer = No (\case Refl impossible)
220252

221253
--------------------------------------------------------------------------------
222254
-- Opaque Handles
@@ -228,12 +260,15 @@ public export
228260
data Handle : Type where
229261
MkHandle : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> Handle
230262

231-
||| Safely create a handle from a pointer value.
232-
||| Returns Nothing if the pointer is null.
263+
||| Safely create a handle from a pointer value. Uses `choose` to obtain a
264+
||| real `So (ptr /= 0)` witness for the non-null branch. (Previously
265+
||| `Just (MkHandle ptr)` left the `auto` proof unsolved and did not compile.)
233266
public export
234267
createHandle : Bits64 -> Maybe Handle
235-
createHandle 0 = Nothing
236-
createHandle ptr = Just (MkHandle ptr)
268+
createHandle ptr =
269+
case choose (ptr /= 0) of
270+
Left ok => Just (MkHandle ptr {nonNull = ok})
271+
Right _ => Nothing
237272

238273
||| Extract pointer value from handle (for FFI crossing)
239274
public export

0 commit comments

Comments
 (0)