Skip to content

Commit 78cd258

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 Idris2 ABI proofs to genuinely compile and verify under 0.7.0 The src/interface/abi/{Types,Layout,Foreign}.idr files were scaffolded from a template and never compiler-checked. This makes the ephapaxiser ABI build clean (zero errors, zero warnings) under Idris2 0.7.0 with real proofs. Structural: - Move flat ABI files into nested Ephapaxiser/ABI/ layout so module paths match namespaces; add ephapaxiser-abi.ipkg package. Types.idr: - thisPlatform: replace %runElab stub (needed ElabReflection) with Linux. - DecEq Result / DecEq UsageCount: replace non-compiling `decEq _ _ = No absurd` catch-alls with explicit off-diagonal `No (\case Refl impossible)`. - createHandle: use `choose (ptr /= 0)` to solve the MkHandle nonNull auto proof instead of leaving it unsolved. - LinearResource: generalise MkHandle/MkLinearResource indices so the legal state-machine transitions (useResource/consumeResource) are expressible; implement the previous `?usedResource` hole. - cSizeOf/cAlignOf: dispatch over a first-order CType tag instead of matching on type-level applications (CInt p), which Idris2 cannot pattern-match. - CPtr: replace ill-typed `Bits (ptrSize p)` with cPtrBytes : Platform -> Nat. Layout.idr: - paddingFor: use Nat `minus` (Nat has no `-`). - Add sound decDivides + decFieldsAligned; checkCABI now returns a genuine CABICompliant witness; remove the ?fieldsAlignedProof hole. - Concrete layouts supply erased auto proofs {sizeCorrect = Oh} and {aligned = DivideBy 3 Refl} (24 = 3*8). - offsetInBounds: honest `Maybe (So ...)` via choose (the universally quantified form was unsound); drop verifyLayout/alignUpCorrect which could not typecheck symbolically; add alignUpDivides + verifyAllLayouts. Proofs.idr (new): machine-checked theorems — - resourceTrackerCompliant, consumeProofCompliant: C-ABI compliance built directly from per-field DivideBy witnesses. - okIsZero, doubleFreeIsSeven: pin the FFI result-code encoding. - consumedHasNoSuccessor, useProducesAcquiredToInUse: lifecycle invariants. .gitignore: ignore **/build/, *.ttc, *.ttm. 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 67baf69 commit 78cd258

6 files changed

Lines changed: 293 additions & 63 deletions

File tree

‎.gitignore‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,9 +15,14 @@ Thumbs.db
1515
/target/
1616
/_build/
1717
/build/
18+
**/build/
1819
/dist/
1920
/out/
2021

22+
# Idris2 compiled artefacts
23+
*.ttc
24+
*.ttm
25+
2126
# Dependencies
2227
/node_modules/
2328
/vendor/

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

File renamed without changes.

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

Lines changed: 70 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@ module Ephapaxiser.ABI.Layout
1717
import Ephapaxiser.ABI.Types
1818
import Data.Vect
1919
import Data.So
20+
import Data.Nat
21+
import Decidable.Equality
2022

2123
%default total
2224

@@ -30,24 +32,42 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
3032
paddingFor offset alignment =
3133
if offset `mod` alignment == 0
3234
then 0
33-
else alignment - (offset `mod` alignment)
35+
else minus alignment (offset `mod` alignment)
3436

3537
||| Proof that alignment divides aligned size
3638
public export
3739
data Divides : Nat -> Nat -> Type where
3840
DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
3941

42+
||| Sound decision procedure for divisibility. Returns a genuine
43+
||| `Divides n m` witness when `n` evenly divides `m`, otherwise Nothing.
44+
||| Division by zero is undecidable here and yields Nothing.
45+
public export
46+
decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
47+
decDivides Z _ = Nothing
48+
decDivides (S k) m =
49+
let q = m `div` (S k) in
50+
case decEq m (q * (S k)) of
51+
Yes prf => Just (DivideBy q prf)
52+
No _ => Nothing
53+
4054
||| Round up to next alignment boundary
4155
public export
4256
alignUp : (size : Nat) -> (alignment : Nat) -> Nat
4357
alignUp size alignment =
4458
size + paddingFor size alignment
4559

46-
||| Proof that alignUp produces aligned result
60+
||| Sound divisibility check for an aligned size. The general theorem
61+
||| "alignUp size align is always divisible by align" needs div/mod lemmas
62+
||| from Data.Nat and is tracked as residual proof work; here we *decide* it
63+
||| via `decDivides`, which returns a genuine witness when it holds. For the
64+
||| concrete ABI layouts below, divisibility is proven outright (`DivideBy`).
65+
||| (Previously `alignUpCorrect … = DivideBy … Refl`, whose `Refl` cannot
66+
||| typecheck for symbolic inputs.)
4767
public export
48-
alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align)
49-
alignUpCorrect size align prf =
50-
DivideBy ((size + paddingFor size align) `div` align) Refl
68+
alignUpDivides : (size : Nat) -> (align : Nat) ->
69+
Maybe (Divides align (alignUp size align))
70+
alignUpDivides size align = decDivides align (alignUp size align)
5171

5272
--------------------------------------------------------------------------------
5373
-- Struct Field Layout
@@ -79,7 +99,7 @@ record StructLayout where
7999

80100
||| Calculate total struct size with padding
81101
public export
82-
calcStructSize : Vect n Field -> Nat -> Nat
102+
calcStructSize : Vect k Field -> Nat -> Nat
83103
calcStructSize [] align = 0
84104
calcStructSize (f :: fs) align =
85105
let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
@@ -88,23 +108,26 @@ calcStructSize (f :: fs) align =
88108

89109
||| Proof that field offsets are correctly aligned
90110
public export
91-
data FieldsAligned : Vect n Field -> Type where
111+
data FieldsAligned : Vect k Field -> Type where
92112
NoFields : FieldsAligned []
93113
ConsField :
94114
(f : Field) ->
95-
(rest : Vect n Field) ->
115+
(rest : Vect k Field) ->
96116
Divides f.alignment f.offset ->
97117
FieldsAligned rest ->
98118
FieldsAligned (f :: rest)
99119

100-
||| Verify a struct layout is valid
120+
||| Decide field alignment for every field, building a real `FieldsAligned`
121+
||| witness from per-field divisibility proofs.
101122
public export
102-
verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
103-
verifyLayout fields align =
104-
let size = calcStructSize fields align
105-
in case decSo (size >= sum (map (\f => f.size) fields)) of
106-
Yes prf => Right (MkStructLayout fields size align)
107-
No _ => Left "Invalid struct size"
123+
decFieldsAligned : (fs : Vect k Field) -> Maybe (FieldsAligned fs)
124+
decFieldsAligned [] = Just NoFields
125+
decFieldsAligned (f :: fs) =
126+
case decDivides f.alignment f.offset of
127+
Nothing => Nothing
128+
Just dvd => case decFieldsAligned fs of
129+
Nothing => Nothing
130+
Just rest => Just (ConsField f fs dvd rest)
108131

109132
--------------------------------------------------------------------------------
110133
-- Resource Tracker Layout
@@ -131,11 +154,8 @@ resourceTrackerLayout =
131154
]
132155
24 -- Total size: 24 bytes
133156
8 -- Alignment: 8 bytes
134-
135-
||| Proof that the resource tracker layout is C-ABI compliant
136-
public export
137-
resourceTrackerCABI : CABICompliant resourceTrackerLayout
138-
resourceTrackerCABI = CABIOk resourceTrackerLayout ?resourceTrackerFieldsAligned
157+
{sizeCorrect = Oh}
158+
{aligned = DivideBy 3 Refl} -- 24 = 3 * 8
139159

140160
||| Proof that the resource tracker layout is valid for all platforms
141161
public export
@@ -172,6 +192,8 @@ consumeProofLayout =
172192
]
173193
24
174194
8
195+
{sizeCorrect = Oh}
196+
{aligned = DivideBy 3 Refl} -- 24 = 3 * 8
175197

176198
--------------------------------------------------------------------------------
177199
-- Platform-Specific Layouts
@@ -202,25 +224,45 @@ data CABICompliant : StructLayout -> Type where
202224
FieldsAligned layout.fields ->
203225
CABICompliant layout
204226

205-
||| Check if layout follows C ABI
227+
||| Verify a layout against the C ABI alignment rules, returning a genuine
228+
||| `CABICompliant` proof (built from real per-field divisibility witnesses)
229+
||| or an error when some field offset is misaligned.
206230
public export
207231
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
208232
checkCABI layout =
209-
Right (CABIOk layout ?fieldsAlignedProof)
233+
case decFieldsAligned layout.fields of
234+
Just prf => Right (CABIOk layout prf)
235+
Nothing => Left "Field offsets are not correctly aligned for the C ABI"
236+
237+
||| Verify that all ephapaxiser layouts are C-ABI compliant. Fails (Left) if
238+
||| any concrete layout is misaligned, rather than asserting it.
239+
public export
240+
verifyAllLayouts : Either String ()
241+
verifyAllLayouts = do
242+
_ <- checkCABI resourceTrackerLayout
243+
_ <- checkCABI consumeProofLayout
244+
Right ()
210245

211246
--------------------------------------------------------------------------------
212247
-- Offset Calculation
213248
--------------------------------------------------------------------------------
214249

215-
||| Calculate field offset with proof of correctness
250+
||| Look up a field's offset by name in a layout.
216251
public export
217-
fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (n : Nat ** Field)
252+
fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (Nat, Field)
218253
fieldOffset layout name =
219254
case findIndex (\f => f.name == name) layout.fields of
220-
Just idx => Just (finToNat idx ** index idx layout.fields)
255+
Just idx => Just (finToNat idx, index idx layout.fields)
221256
Nothing => Nothing
222257

223-
||| Proof that field offset is within struct bounds
258+
||| Decide whether a field lies within a struct's byte bounds, returning a
259+
||| genuine proof when `offset + size <= totalSize`. The previous signature
260+
||| asserted this for *every* field unconditionally, which is false (a field
261+
||| need not belong to the layout); this honest version decides it.
224262
public export
225-
offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
226-
offsetInBounds layout f = ?offsetInBoundsProof
263+
offsetInBounds : (layout : StructLayout) -> (f : Field) ->
264+
Maybe (So (f.offset + f.size <= layout.totalSize))
265+
offsetInBounds layout f =
266+
case choose (f.offset + f.size <= layout.totalSize) of
267+
Left ok => Just ok
268+
Right _ => Nothing

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

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
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 ephapaxiser 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 lifecycle transition
9+
||| mis-stated, 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 Ephapaxiser.ABI.Proofs
19+
20+
import Ephapaxiser.ABI.Types
21+
import Ephapaxiser.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 ResourceTracker layout divides its alignment:
32+
||| 0|8, 8|4, 12|4, 16|4, 20|4.
33+
export
34+
resourceTrackerCompliant : CABICompliant Layout.resourceTrackerLayout
35+
resourceTrackerCompliant =
36+
CABIOk resourceTrackerLayout
37+
(ConsField _ _ (DivideBy 0 Refl)
38+
(ConsField _ _ (DivideBy 2 Refl)
39+
(ConsField _ _ (DivideBy 3 Refl)
40+
(ConsField _ _ (DivideBy 4 Refl)
41+
(ConsField _ _ (DivideBy 5 Refl)
42+
NoFields)))))
43+
44+
||| Every field offset in the ConsumeProof layout divides its alignment:
45+
||| 0|8, 8|4, 12|4, 16|4, 20|4.
46+
export
47+
consumeProofCompliant : CABICompliant Layout.consumeProofLayout
48+
consumeProofCompliant =
49+
CABIOk consumeProofLayout
50+
(ConsField _ _ (DivideBy 0 Refl)
51+
(ConsField _ _ (DivideBy 2 Refl)
52+
(ConsField _ _ (DivideBy 3 Refl)
53+
(ConsField _ _ (DivideBy 4 Refl)
54+
(ConsField _ _ (DivideBy 5 Refl)
55+
NoFields)))))
56+
57+
--------------------------------------------------------------------------------
58+
-- Result-code round-trip: the encoding the Zig FFI depends on.
59+
--------------------------------------------------------------------------------
60+
61+
export
62+
okIsZero : resultToInt Ok = 0
63+
okIsZero = Refl
64+
65+
||| The double-free error code is pinned to 7, as the Zig FFI bridge expects.
66+
export
67+
doubleFreeIsSeven : resultToInt DoubleFree = 7
68+
doubleFreeIsSeven = Refl
69+
70+
--------------------------------------------------------------------------------
71+
-- Linearity state machine: only the two legal transitions exist.
72+
--------------------------------------------------------------------------------
73+
74+
||| Once a resource is consumed, no further transition out of it is valid —
75+
||| this is the formal use-after-free guard. `consumedIsFinal` discharges the
76+
||| absurd case for any successor state, so the proof is genuine (the type
77+
||| `ValidTransition Consumed next` is uninhabited).
78+
export
79+
consumedHasNoSuccessor : (next : ResourceLifecycle) ->
80+
ValidTransition Consumed next -> Void
81+
consumedHasNoSuccessor next = consumedIsFinal
82+
83+
||| Using a freshly-acquired resource records exactly-once usage: the usage
84+
||| index of the returned resource is `UsedOnce`, witnessed structurally by
85+
||| the lifecycle transition `Acquired -> InUse`.
86+
export
87+
useProducesAcquiredToInUse :
88+
(r : LinearResource Acquired Unused) ->
89+
snd (useResource r) = AcquiredToInUse
90+
useProducesAcquiredToInUse (MkLinearResource _) = Refl

0 commit comments

Comments
 (0)