Skip to content

Commit b3caa84

Browse files
hyperpolymathJonathan D.A. Jewellclaude
authored
ABI: make Idris2 proofs genuinely compile + add machine-checked theorems (#40)
## Idris2 ABI proofs — genuinely compile + machine-checked theorems Part of the family-wide ABI-proofs review. The hand-written ABI did **not** typecheck under Idris2 0.7.0; this makes it real and verified, following the merged **iseriser** reference. **Systemic fixes:** `decEq _ _ = No absurd` → explicit off-diagonal cases; `{auto 0 nonNull}` smart constructors → `choose`-based; `paddingFor` `-` → `minus`; real `decDivides`/`decFieldsAligned` replacing `?fieldsAlignedProof`; honest `offsetInBounds`; `thisPlatform` de-`%runElab`'d; buildable nested layout + ipkg; new `Proofs.idr` with real theorems. **Verified:** `idris2 --build` clean (0/0); adversarial re-verify found no `believe_me`/`postulate`/holes. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --- _Generated by [Claude Code](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 9ce2805 commit b3caa84

6 files changed

Lines changed: 194 additions & 30 deletions

File tree

‎.gitignore‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,9 @@ Thumbs.db
1515
/target/
1616
/_build/
1717
/build/
18+
**/build/
19+
*.ttc
20+
*.ttm
1821
/dist/
1922
/out/
2023

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

File renamed without changes.

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

Lines changed: 64 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,8 @@ module Atsiser.ABI.Layout
1616
import Atsiser.ABI.Types
1717
import Data.Vect
1818
import Data.So
19+
import Data.Nat
20+
import Decidable.Equality
1921

2022
%default total
2123

@@ -29,24 +31,39 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
2931
paddingFor offset alignment =
3032
if offset `mod` alignment == 0
3133
then 0
32-
else alignment - (offset `mod` alignment)
34+
else minus alignment (offset `mod` alignment)
3335

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

41+
||| Sound decision procedure: does `n` divide `m`?
42+
||| For n = S k, compute the quotient and check m = q * (S k) by decidable
43+
||| equality. Division does not reduce during typechecking, so the equation
44+
||| is genuinely checked at runtime rather than asserted.
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 = div m (S k) in
50+
case decEq m (q * (S k)) of
51+
Yes prf => Just (DivideBy q prf)
52+
No _ => Nothing
53+
3954
||| Round up to next alignment boundary
4055
public export
4156
alignUp : (size : Nat) -> (alignment : Nat) -> Nat
4257
alignUp size alignment =
4358
size + paddingFor size alignment
4459

45-
||| Proof that alignUp produces aligned result
60+
||| Decide that `alignUp size align` is divisible by `align`.
61+
||| Returns a genuine `Divides` witness when the quotient checks out, and
62+
||| `Nothing` otherwise (e.g. align = 0). A `Refl`-only proof is impossible
63+
||| here because division does not reduce during typechecking.
4664
public export
47-
alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align)
48-
alignUpCorrect size align prf =
49-
DivideBy ((size + paddingFor size align) `div` align) Refl
65+
alignUpCorrect : (size : Nat) -> (align : Nat) -> Maybe (Divides align (alignUp size align))
66+
alignUpCorrect size align = decDivides align (alignUp size align)
5067

5168
--------------------------------------------------------------------------------
5269
-- Ownership-Annotated Fields
@@ -109,7 +126,7 @@ ownedFieldCount layout = length (filter requiresOwnershipTracking (toList layout
109126

110127
||| Calculate total struct size with padding
111128
public export
112-
calcStructSize : Vect n Field -> Nat -> Nat
129+
calcStructSize : Vect len Field -> Nat -> Nat
113130
calcStructSize [] align = 0
114131
calcStructSize (f :: fs) align =
115132
let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
@@ -118,23 +135,30 @@ calcStructSize (f :: fs) align =
118135

119136
||| Proof that field offsets are correctly aligned
120137
public export
121-
data FieldsAligned : Vect n Field -> Type where
138+
data FieldsAligned : Vect len Field -> Type where
122139
NoFields : FieldsAligned []
123140
ConsField :
124141
(f : Field) ->
125-
(rest : Vect n Field) ->
142+
(rest : Vect len Field) ->
126143
Divides f.alignment f.offset ->
127144
FieldsAligned rest ->
128145
FieldsAligned (f :: rest)
129146

130-
||| Verify a struct layout is valid
147+
||| Verify a struct layout is valid.
148+
||| Both erased obligations of `MkStructLayout` are discharged with genuine
149+
||| witnesses: the size bound via `choose`, and `Divides align size` via
150+
||| `decDivides`. If either fails to hold for the computed size, we report an
151+
||| error instead of fabricating a proof.
131152
public export
132-
verifyLayout : (name : String) -> (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
153+
verifyLayout : (name : String) -> (fields : Vect len Field) -> (align : Nat) -> Either String StructLayout
133154
verifyLayout name fields align =
134-
let size = calcStructSize fields align
135-
in case decSo (size >= sum (map (\f => f.size) fields)) of
136-
Yes prf => Right (MkStructLayout name fields size align)
137-
No _ => Left "Invalid struct size for \{name}"
155+
let size = calcStructSize fields align in
156+
case choose (size >= sum (map (\f => f.size) fields)) of
157+
Right _ => Left "Invalid struct size for \{name}"
158+
Left szOk => case decDivides align size of
159+
Nothing => Left "Total size of \{name} is not aligned to \{show align}"
160+
Just dvd => Right (MkStructLayout name fields size align
161+
{sizeCorrect = szOk} {aligned = dvd})
138162

139163
--------------------------------------------------------------------------------
140164
-- Platform-Specific Layouts
@@ -165,11 +189,25 @@ data CABICompliant : StructLayout -> Type where
165189
FieldsAligned layout.fields ->
166190
CABICompliant layout
167191

192+
||| Decide whether every field's offset is aligned to its alignment,
193+
||| building a FieldsAligned witness over the whole vector.
194+
public export
195+
decFieldsAligned : (fields : Vect len Field) -> Maybe (FieldsAligned fields)
196+
decFieldsAligned [] = Just NoFields
197+
decFieldsAligned (f :: rest) =
198+
case decDivides f.alignment f.offset of
199+
Nothing => Nothing
200+
Just dvd => case decFieldsAligned rest of
201+
Nothing => Nothing
202+
Just restPrf => Just (ConsField f rest dvd restPrf)
203+
168204
||| Check if layout follows C ABI
169205
public export
170206
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
171207
checkCABI layout =
172-
Right (CABIOk layout ?fieldsAlignedProof)
208+
case decFieldsAligned layout.fields of
209+
Just prf => Right (CABIOk layout prf)
210+
Nothing => Left "Struct \{layout.structName} has misaligned fields"
173211

174212
--------------------------------------------------------------------------------
175213
-- Ownership Graph for Structs
@@ -216,6 +254,8 @@ exampleOwnedLayout =
216254
]
217255
16 -- Total size: 16 bytes
218256
8 -- Alignment: 8 bytes
257+
{sizeCorrect = Oh}
258+
{aligned = DivideBy 2 Refl} -- 16 = 2 * 8
219259

220260
||| Example: Layout for a struct with a borrowed pointer.
221261
||| This is what atsiser generates when it finds:
@@ -231,6 +271,8 @@ exampleBorrowedLayout =
231271
]
232272
16 -- Total size: 16 bytes (with padding)
233273
8 -- Alignment: 8 bytes
274+
{sizeCorrect = Oh}
275+
{aligned = DivideBy 2 Refl} -- 16 = 2 * 8
234276

235277
--------------------------------------------------------------------------------
236278
-- Offset Calculation
@@ -244,7 +286,11 @@ fieldOffset layout name =
244286
Just idx => Just (finToNat idx ** index idx layout.fields)
245287
Nothing => Nothing
246288

247-
||| Proof that field offset is within struct bounds
289+
||| Decide whether a field's offset+size fits within the struct's total size.
290+
||| Returns a proof when the bound holds, Nothing otherwise (it does not hold
291+
||| in general, so a universally-quantified return type would be unsound).
248292
public export
249-
offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
250-
offsetInBounds layout f = ?offsetInBoundsProof
293+
offsetInBounds : (layout : StructLayout) -> (f : Field) -> Maybe (So (f.offset + f.size <= layout.totalSize))
294+
offsetInBounds layout f = case choose (f.offset + f.size <= layout.totalSize) of
295+
Left ok => Just ok
296+
Right _ => Nothing

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

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
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 theorems about the Atsiser ABI.
5+
|||
6+
||| These theorems pin down properties that the rest of the ABI relies on:
7+
||| * the example struct layouts are genuinely C-ABI compliant
8+
||| (every field offset is a multiple of its alignment), and
9+
||| * the result-code encoding agrees with the C contract.
10+
|||
11+
||| Each compliance witness is built DIRECTLY (one `DivideBy` per field),
12+
||| because multiplication reduces during typechecking while division does
13+
||| not — so these are checked, not asserted.
14+
15+
module Atsiser.ABI.Proofs
16+
17+
import Atsiser.ABI.Types
18+
import Atsiser.ABI.Layout
19+
import Data.Vect
20+
21+
%default total
22+
23+
--------------------------------------------------------------------------------
24+
-- Struct Layout Compliance
25+
--------------------------------------------------------------------------------
26+
27+
||| `exampleOwnedLayout` follows the C ABI: field `data` at offset 0 (= 0 * 8)
28+
||| and field `len` at offset 8 (= 1 * 8) are both aligned to 8.
29+
export
30+
exampleOwnedCompliant : CABICompliant Layout.exampleOwnedLayout
31+
exampleOwnedCompliant =
32+
CABIOk Layout.exampleOwnedLayout
33+
(ConsField _ _ (DivideBy 0 Refl) -- data: offset 0 = 0 * 8
34+
(ConsField _ _ (DivideBy 1 Refl) -- len: offset 8 = 1 * 8
35+
NoFields))
36+
37+
||| `exampleBorrowedLayout` follows the C ABI: field `name` at offset 0 (= 0 * 8)
38+
||| aligned to 8, and field `flags` at offset 8 (= 2 * 4) aligned to 4.
39+
export
40+
exampleBorrowedCompliant : CABICompliant Layout.exampleBorrowedLayout
41+
exampleBorrowedCompliant =
42+
CABIOk Layout.exampleBorrowedLayout
43+
(ConsField _ _ (DivideBy 0 Refl) -- name: offset 0 = 0 * 8
44+
(ConsField _ _ (DivideBy 2 Refl) -- flags: offset 8 = 2 * 4
45+
NoFields))
46+
47+
--------------------------------------------------------------------------------
48+
-- Result-Code Encoding
49+
--------------------------------------------------------------------------------
50+
51+
||| The success code encodes to 0, as the C FFI contract requires.
52+
export
53+
okIsZero : resultToInt Ok = 0
54+
okIsZero = Refl
55+
56+
||| The generic-error code encodes to 1, distinct from success.
57+
export
58+
errorIsOne : resultToInt Error = 1
59+
errorIsOne = Refl
60+
61+
||| The result encoding is injective on the two codes that the FFI layer
62+
||| branches on most: success and bounds violation map to different integers.
63+
export
64+
okNotBounds : Not (resultToInt Ok = resultToInt BoundsViolation)
65+
okNotBounds = \case Refl impossible

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

Lines changed: 53 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ module Atsiser.ABI.Types
1717
import Data.Bits
1818
import Data.So
1919
import Data.Vect
20+
import Decidable.Equality
2021

2122
%default total
2223

@@ -29,13 +30,10 @@ public export
2930
data Platform = Linux | Windows | MacOS | BSD | WASM
3031

3132
||| Compile-time platform detection
32-
||| This will be set during compilation based on target
33+
||| This is the default target; override with compiler flags as needed.
3334
public export
3435
thisPlatform : Platform
35-
thisPlatform =
36-
%runElab do
37-
-- Platform detection logic
38-
pure Linux -- Default, override with compiler flags
36+
thisPlatform = Linux
3937

4038
--------------------------------------------------------------------------------
4139
-- Result Codes
@@ -81,7 +79,48 @@ DecEq Result where
8179
decEq NullPointer NullPointer = Yes Refl
8280
decEq OwnershipViolation OwnershipViolation = Yes Refl
8381
decEq BoundsViolation BoundsViolation = Yes Refl
84-
decEq _ _ = No absurd
82+
decEq Ok Error = No (\case Refl impossible)
83+
decEq Ok InvalidParam = No (\case Refl impossible)
84+
decEq Ok OutOfMemory = No (\case Refl impossible)
85+
decEq Ok NullPointer = No (\case Refl impossible)
86+
decEq Ok OwnershipViolation = No (\case Refl impossible)
87+
decEq Ok BoundsViolation = No (\case Refl impossible)
88+
decEq Error Ok = No (\case Refl impossible)
89+
decEq Error InvalidParam = No (\case Refl impossible)
90+
decEq Error OutOfMemory = No (\case Refl impossible)
91+
decEq Error NullPointer = No (\case Refl impossible)
92+
decEq Error OwnershipViolation = No (\case Refl impossible)
93+
decEq Error BoundsViolation = No (\case Refl impossible)
94+
decEq InvalidParam Ok = No (\case Refl impossible)
95+
decEq InvalidParam Error = No (\case Refl impossible)
96+
decEq InvalidParam OutOfMemory = No (\case Refl impossible)
97+
decEq InvalidParam NullPointer = No (\case Refl impossible)
98+
decEq InvalidParam OwnershipViolation = No (\case Refl impossible)
99+
decEq InvalidParam BoundsViolation = No (\case Refl impossible)
100+
decEq OutOfMemory Ok = No (\case Refl impossible)
101+
decEq OutOfMemory Error = No (\case Refl impossible)
102+
decEq OutOfMemory InvalidParam = No (\case Refl impossible)
103+
decEq OutOfMemory NullPointer = No (\case Refl impossible)
104+
decEq OutOfMemory OwnershipViolation = No (\case Refl impossible)
105+
decEq OutOfMemory BoundsViolation = No (\case Refl impossible)
106+
decEq NullPointer Ok = No (\case Refl impossible)
107+
decEq NullPointer Error = No (\case Refl impossible)
108+
decEq NullPointer InvalidParam = No (\case Refl impossible)
109+
decEq NullPointer OutOfMemory = No (\case Refl impossible)
110+
decEq NullPointer OwnershipViolation = No (\case Refl impossible)
111+
decEq NullPointer BoundsViolation = No (\case Refl impossible)
112+
decEq OwnershipViolation Ok = No (\case Refl impossible)
113+
decEq OwnershipViolation Error = No (\case Refl impossible)
114+
decEq OwnershipViolation InvalidParam = No (\case Refl impossible)
115+
decEq OwnershipViolation OutOfMemory = No (\case Refl impossible)
116+
decEq OwnershipViolation NullPointer = No (\case Refl impossible)
117+
decEq OwnershipViolation BoundsViolation = No (\case Refl impossible)
118+
decEq BoundsViolation Ok = No (\case Refl impossible)
119+
decEq BoundsViolation Error = No (\case Refl impossible)
120+
decEq BoundsViolation InvalidParam = No (\case Refl impossible)
121+
decEq BoundsViolation OutOfMemory = No (\case Refl impossible)
122+
decEq BoundsViolation NullPointer = No (\case Refl impossible)
123+
decEq BoundsViolation OwnershipViolation = No (\case Refl impossible)
85124

86125
--------------------------------------------------------------------------------
87126
-- Ownership State Machine
@@ -165,8 +204,9 @@ data Handle : Type where
165204
||| Returns Nothing if pointer is null
166205
public export
167206
createHandle : Bits64 -> Maybe Handle
168-
createHandle 0 = Nothing
169-
createHandle ptr = Just (MkHandle ptr)
207+
createHandle ptr = case choose (ptr /= 0) of
208+
Left ok => Just (MkHandle ptr {nonNull = ok})
209+
Right _ => Nothing
170210

171211
||| Extract pointer value from handle
172212
public export
@@ -281,19 +321,20 @@ data HasAlignment : Type -> Nat -> Type where
281321

282322
||| Size of C types (platform-specific)
283323
public export
324+
||| Note: `CInt p` / `CSize p` are type synonyms that reduce to `Bits32`/`Bits64`,
325+
||| so they are covered by the `Bits32`/`Bits64` cases below rather than matched
326+
||| as constructors (Idris2 cannot pattern-match on a type-level function).
284327
cSizeOf : (p : Platform) -> (t : Type) -> Nat
285-
cSizeOf p (CInt _) = 4
286-
cSizeOf p (CSize _) = if ptrSize p == 64 then 8 else 4
287328
cSizeOf p Bits32 = 4
288329
cSizeOf p Bits64 = 8
289330
cSizeOf p Double = 8
290331
cSizeOf p _ = ptrSize p `div` 8
291332

292333
||| Alignment of C types (platform-specific)
293334
public export
335+
||| As with `cSizeOf`, `CInt`/`CSize` reduce to `Bits32`/`Bits64` and are
336+
||| handled by those cases rather than matched as constructors.
294337
cAlignOf : (p : Platform) -> (t : Type) -> Nat
295-
cAlignOf p (CInt _) = 4
296-
cAlignOf p (CSize _) = if ptrSize p == 64 then 8 else 4
297338
cAlignOf p Bits32 = 4
298339
cAlignOf p Bits64 = 8
299340
cAlignOf p Double = 8

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
package atsiser-abi
3+
4+
sourcedir = "."
5+
6+
modules = Atsiser.ABI.Types
7+
, Atsiser.ABI.Layout
8+
, Atsiser.ABI.Foreign
9+
, Atsiser.ABI.Proofs

0 commit comments

Comments
 (0)