Skip to content

Commit 66cfd79

Browse files
claudeclaude
committed
Fix Idris2 ABI proofs to genuinely compile and verify under 0.7.0
Make the src/interface/abi formal proofs compile cleanly (zero errors, zero warnings) under Idris2 0.7.0 and add machine-checked theorems. Buildability / layout: - Move flat Types/Layout/Foreign.idr into nested namespace dirs src/interface/abi/Affinescriptiser/ABI/ so file paths match the Affinescriptiser.ABI.* module namespaces. - Add src/interface/abi/affinescriptiser-abi.ipkg packaging all four modules. - .gitignore: add **/build/, *.ttc, *.ttm; do not commit the idris build dir. Types.idr: - thisPlatform: replace %runElab (ElabReflection not enabled) with plain WASM. - DecEq Result: replace the non-compiling "No absurd" catch-all with explicit off-diagonal cases (No (\case Refl impossible)) for every distinct pair. - createHandle / trackResource: solve the {auto 0 nonNull : So (ptr /= 0)} obligation via choose (ptr /= 0) instead of leaving it unsolved. - Add missing Eq Linearity instance (used by the Verify helpers). - CPtr: drop the non-existent Bits (ptrSize p) family; map platforms to the concrete Bits32/Bits64 primitives. - cSizeOf / cAlignOf: drop the unsound type-level matches on (CInt _)/(CSize _) (a reducible type-application cannot be pattern-matched, and it caused a type-checker memory blowup); keep the concrete Bits32/Bits64/Double clauses. - WASMOffsetValid: compare the 4GiB bound at Integer (via natToInteger) so the 4294967296 literal is not normalised to a unary Nat (which OOM-kills the checker); the proposition is unchanged. Layout.idr: - paddingFor: use minus (Data.Nat) instead of Nat subtraction with (-). - Add sound decDivides : (n m : Nat) -> Maybe (Divides n m) and decFieldsAligned, then implement checkCABI via decFieldsAligned instead of the ?fieldsAlignedProof hole. - Replace the bogus Refl-based alignUpCorrect (and its Bool-as-type hypothesis) with alignUpDivides, deciding divisibility honestly via decDivides. - offsetInBounds: change the unsound universally-quantified So return type to Maybe (So ...) implemented via choose. - verifyLayout: supply the StructLayout erased proofs (sizeCorrect via choose, aligned via decDivides) instead of omitting them. - trackedFDLayout: supply {sizeCorrect = Oh} and {aligned = DivideBy 5 Refl} (totalSize 20 = 5 * 4). - WASM memory-magnitude constants (wasmPageSize/wasmMaxPages/wasmMaxMemory) are Integer so the 4GiB product does not unary-normalise; FitsInPage/TableInBounds compare via natToInteger. - Rename the StructLayout-shadowed Vect length variable in standalone signatures to k; qualify Layout.wasmPageSize/Layout.wasmMaxMemory to avoid implicit-bind warnings. Proofs.idr (new): machine-checked theorems, all marked export: - trackedFDCompliant : CABICompliant Layout.trackedFDLayout, built directly with one DivideBy per field (offsets 0,4,8,12,16 = k*4). - okIsZero / affineViolationIsFive / resourceLeakIsSix pin the result-code encoding by Refl. - mutexIsLinear / fdIsAffine pin the default-linearity policy. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA
1 parent cca6b7e commit 66cfd79

6 files changed

Lines changed: 251 additions & 42 deletions

File tree

‎.gitignore‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,11 @@ Thumbs.db
1818
/dist/
1919
/out/
2020

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

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

File renamed without changes.

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

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

2022
%default total
2123

@@ -29,42 +31,65 @@ 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 candidate quotient q = m `div` (S k) and check
43+
||| whether m really equals q * (S k). When it does, the equality witnesses
44+
||| `Divides n m` directly; otherwise we have no evidence and return Nothing.
45+
||| (Division by zero yields Nothing — zero divides nothing nonzero.)
46+
public export
47+
decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
48+
decDivides Z m = case decEq m Z of
49+
Yes prf => Just (DivideBy Z (rewrite prf in Refl))
50+
No _ => Nothing
51+
decDivides (S k) m =
52+
let q = m `div` (S k) in
53+
case decEq m (q * (S k)) of
54+
Yes prf => Just (DivideBy q prf)
55+
No _ => Nothing
56+
3957
||| Round up to next alignment boundary
4058
public export
4159
alignUp : (size : Nat) -> (alignment : Nat) -> Nat
4260
alignUp size alignment =
4361
size + paddingFor size alignment
4462

45-
||| Proof that alignUp produces aligned result
63+
||| Sound divisibility check for an aligned size. The general theorem
64+
||| "alignUp size align is always divisible by align" needs div/mod lemmas and
65+
||| is tracked as residual proof work; here we *decide* it via `decDivides`,
66+
||| which returns a genuine witness when it holds. For the concrete ABI layouts
67+
||| below, divisibility is proven outright with `DivideBy`.
4668
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
69+
alignUpDivides : (size : Nat) -> (align : Nat) ->
70+
Maybe (Divides align (alignUp size align))
71+
alignUpDivides size align = decDivides align (alignUp size align)
5072

5173
--------------------------------------------------------------------------------
5274
-- WASM Linear Memory Layout
5375
--------------------------------------------------------------------------------
5476

55-
||| WASM page size is always 64KiB (65536 bytes)
77+
||| WASM page size is always 64KiB (65536 bytes).
78+
||| These memory-magnitude constants are `Integer` rather than `Nat`: the 4GiB
79+
||| product below is far too large to normalise as a unary `Nat` at
80+
||| type-checking time, and machine-memory sizes are naturally machine integers.
5681
public export
57-
wasmPageSize : Nat
82+
wasmPageSize : Integer
5883
wasmPageSize = 65536
5984

6085
||| Maximum WASM linear memory: 4GiB (65536 pages)
6186
public export
62-
wasmMaxPages : Nat
87+
wasmMaxPages : Integer
6388
wasmMaxPages = 65536
6489

65-
||| Maximum WASM linear memory in bytes
90+
||| Maximum WASM linear memory in bytes (4 294 967 296)
6691
public export
67-
wasmMaxMemory : Nat
92+
wasmMaxMemory : Integer
6893
wasmMaxMemory = wasmPageSize * wasmMaxPages
6994

7095
||| A region in WASM linear memory
@@ -151,7 +176,7 @@ record StructLayout where
151176

152177
||| Calculate total struct size with padding
153178
public export
154-
calcStructSize : Vect n Field -> Nat -> Nat
179+
calcStructSize : Vect k Field -> Nat -> Nat
155180
calcStructSize [] align = 0
156181
calcStructSize (f :: fs) align =
157182
let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
@@ -160,23 +185,25 @@ calcStructSize (f :: fs) align =
160185

161186
||| Proof that field offsets are correctly aligned
162187
public export
163-
data FieldsAligned : Vect n Field -> Type where
188+
data FieldsAligned : Vect k Field -> Type where
164189
NoFields : FieldsAligned []
165190
ConsField :
166191
(f : Field) ->
167-
(rest : Vect n Field) ->
192+
(rest : Vect k Field) ->
168193
Divides f.alignment f.offset ->
169194
FieldsAligned rest ->
170195
FieldsAligned (f :: rest)
171196

172197
||| Verify a struct layout is valid
173198
public export
174-
verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
199+
verifyLayout : (fields : Vect k Field) -> (align : Nat) -> Either String StructLayout
175200
verifyLayout fields align =
176201
let size = calcStructSize fields align
177-
in case decSo (size >= sum (map (\f => f.size) fields)) of
178-
Yes prf => Right (MkStructLayout fields size align)
179-
No _ => Left "Invalid struct size"
202+
in case choose (size >= sum (map (\f => f.size) fields)) of
203+
Right _ => Left "Invalid struct size"
204+
Left szPrf => case decDivides align size of
205+
Nothing => Left "Total size is not a multiple of the alignment"
206+
Just dvd => Right (MkStructLayout fields size align {sizeCorrect = szPrf} {aligned = dvd})
180207

181208
--------------------------------------------------------------------------------
182209
-- WASM-Specific Layout Proofs
@@ -185,7 +212,7 @@ verifyLayout fields align =
185212
||| Proof that a struct layout fits within a single WASM page
186213
public export
187214
data FitsInPage : StructLayout -> Type where
188-
PageFit : (layout : StructLayout) -> {auto 0 ok : So (layout.totalSize <= wasmPageSize)} -> FitsInPage layout
215+
PageFit : (layout : StructLayout) -> {auto 0 ok : So (natToInteger layout.totalSize <= Layout.wasmPageSize)} -> FitsInPage layout
189216

190217
||| Layout of the affine resource table in WASM linear memory
191218
||| The resource table is a contiguous array of resource slots at a fixed
@@ -208,7 +235,7 @@ tableSize t = t.capacity * resourceLayoutSize t.platform
208235
||| Proof that a resource table fits in WASM linear memory
209236
public export
210237
data TableInBounds : ResourceTable -> Type where
211-
TableOk : (t : ResourceTable) -> {auto 0 ok : So (t.baseOffset + tableSize t <= wasmMaxMemory)} -> TableInBounds t
238+
TableOk : (t : ResourceTable) -> {auto 0 ok : So (natToInteger (t.baseOffset + tableSize t) <= Layout.wasmMaxMemory)} -> TableInBounds t
212239

213240
||| Get the WASM region for the nth resource in a table
214241
public export
@@ -230,11 +257,25 @@ data CABICompliant : StructLayout -> Type where
230257
FieldsAligned layout.fields ->
231258
CABICompliant layout
232259

260+
||| Decide whether every field of a vector is aligned (offset divisible by
261+
||| the field's alignment), producing a FieldsAligned witness when so.
262+
public export
263+
decFieldsAligned : (fields : Vect k Field) -> Maybe (FieldsAligned fields)
264+
decFieldsAligned [] = Just NoFields
265+
decFieldsAligned (f :: fs) =
266+
case decDivides f.alignment f.offset of
267+
Nothing => Nothing
268+
Just dvd => case decFieldsAligned fs of
269+
Nothing => Nothing
270+
Just rest => Just (ConsField f fs dvd rest)
271+
233272
||| Check if layout follows C ABI
234273
public export
235274
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
236275
checkCABI layout =
237-
Right (CABIOk layout ?fieldsAlignedProof)
276+
case decFieldsAligned layout.fields of
277+
Just prf => Right (CABIOk layout prf)
278+
Nothing => Left "Struct fields are not correctly aligned for C ABI"
238279

239280
--------------------------------------------------------------------------------
240281
-- Example: Tracked File Descriptor Layout
@@ -254,6 +295,8 @@ trackedFDLayout =
254295
]
255296
20 -- Total size: 20 bytes
256297
4 -- Alignment: 4 bytes (WASM native)
298+
{sizeCorrect = Oh}
299+
{aligned = DivideBy 5 Refl} -- 20 = 5 * 4
257300

258301
--------------------------------------------------------------------------------
259302
-- Offset Calculation
@@ -269,5 +312,8 @@ fieldOffset layout name =
269312

270313
||| Proof that field offset is within struct bounds
271314
public export
272-
offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
273-
offsetInBounds layout f = ?offsetInBoundsProof
315+
offsetInBounds : (layout : StructLayout) -> (f : Field) -> Maybe (So (f.offset + f.size <= layout.totalSize))
316+
offsetInBounds layout f =
317+
case choose (f.offset + f.size <= layout.totalSize) of
318+
Left ok => Just ok
319+
Right _ => Nothing

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

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
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 for the Affinescriptiser ABI.
5+
|||
6+
||| These theorems pin down the correctness of the concrete struct layouts and
7+
||| the FFI result-code encoding. They are checked by the Idris2 type checker:
8+
||| if a layout's field offsets stopped being correctly aligned, or the result
9+
||| encoding changed, this module would fail to compile.
10+
11+
module Affinescriptiser.ABI.Proofs
12+
13+
import Affinescriptiser.ABI.Types
14+
import Affinescriptiser.ABI.Layout
15+
import Data.Vect
16+
17+
%default total
18+
19+
--------------------------------------------------------------------------------
20+
-- Layout compliance
21+
--------------------------------------------------------------------------------
22+
23+
||| The tracked-file-descriptor layout is C-ABI compliant: every field's offset
24+
||| is an exact multiple of that field's alignment.
25+
|||
26+
||| Field offsets: kind=0, linearity=4, ownership=8, padding=12, fd=16, each
27+
||| with alignment 4. The DivideBy witnesses give offset = k * 4 for each:
28+
||| 0=0*4, 4=1*4, 8=2*4, 12=3*4, 16=4*4. These multiplications reduce during
29+
||| typechecking, so the equalities hold by Refl.
30+
export
31+
trackedFDCompliant : CABICompliant Layout.trackedFDLayout
32+
trackedFDCompliant =
33+
CABIOk Layout.trackedFDLayout
34+
(ConsField _ _ (DivideBy 0 Refl)
35+
(ConsField _ _ (DivideBy 1 Refl)
36+
(ConsField _ _ (DivideBy 2 Refl)
37+
(ConsField _ _ (DivideBy 3 Refl)
38+
(ConsField _ _ (DivideBy 4 Refl)
39+
NoFields)))))
40+
41+
--------------------------------------------------------------------------------
42+
-- Result-code encoding
43+
--------------------------------------------------------------------------------
44+
45+
||| The success result encodes to the C integer 0, as required by callers that
46+
||| test the FFI return value against zero.
47+
export
48+
okIsZero : resultToInt Ok = 0
49+
okIsZero = Refl
50+
51+
||| The affine-violation result encodes to 5, matching the dispatch in
52+
||| Foreign.analyse which maps 5 to AffineViolation.
53+
export
54+
affineViolationIsFive : resultToInt AffineViolation = 5
55+
affineViolationIsFive = Refl
56+
57+
||| The resource-leak result encodes to 6, matching Foreign.analyse's mapping
58+
||| of 6 to ResourceLeak.
59+
export
60+
resourceLeakIsSix : resultToInt ResourceLeak = 6
61+
resourceLeakIsSix = Refl
62+
63+
--------------------------------------------------------------------------------
64+
-- Default linearity
65+
--------------------------------------------------------------------------------
66+
67+
||| Mutex locks default to Linear (exactly-once): failing to unlock is a bug, so
68+
||| the affine "at most once" relaxation is not permitted for them.
69+
export
70+
mutexIsLinear : defaultLinearity MutexLock = Linear
71+
mutexIsLinear = Refl
72+
73+
||| File descriptors default to Affine (at most once) — the safe default for
74+
||| acquire/release resources.
75+
export
76+
fdIsAffine : defaultLinearity FileDescriptor = Affine
77+
fdIsAffine = Refl

0 commit comments

Comments
 (0)