ABI: make Idris2 proofs genuinely compile + add machine-checked theorems (#33)

## Idris2 ABI proofs — genuinely compile + machine-checked theorems

Part of the family-wide ABI-proofs review, following the merged
**iseriser** reference. affinescriptiser has the richest ABI in the
family (full `ResourceKind`/`Linearity`/`Ownership`/`TrackedResource`
affine system).

**Note on the suspected blocker:** the Idris2 ABI proofs here **do**
compile and verify — the concern about AffineScript being mid-migration
affects the *target toolchain* (the AffineScript→typed-wasm path), not
the Idris2 ABI layer, which is self-contained. So this lands as real
proofs rather than a `PROOFS-BLOCKED.md`.

**Systemic fixes:** `decEq _ _ = No absurd` → explicit off-diagonal;
`{auto 0 nonNull}` smart constructors (`createHandle`,
`trackResource`/`MkTracked`) → `choose`-based; `paddingFor` `-` →
`minus`; real decision procedures replacing holes; 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>

Author: 3 people

.gitignore

@@ -18,6 +18,11 @@ Thumbs.db
 /dist/
 /out/
 
+# Idris2
+**/build/
+*.ttc
+*.ttm
+
 # Dependencies
 /node_modules/
 /vendor/

src/interface/abi/Foreign.idr …ace/abi/Affinescriptiser/ABI/Foreign.idrsrc/interface/abi/Foreign.idr renamed to src/interface/abi/Affinescriptiser/ABI/Foreign.idr src/interface/abi/Foreign.idr renamed to src/interface/abi/Affinescriptiser/ABI/Foreign.idr

@@ -16,6 +16,8 @@ module Affinescriptiser.ABI.Layout
 import Affinescriptiser.ABI.Types
 import Data.Vect
 import Data.So
+import Data.Nat
+import Decidable.Equality
 
 %default total
 
@@ -29,42 +31,65 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
 paddingFor offset alignment =
   if offset `mod` alignment == 0
     then 0
-    else alignment - (offset `mod` alignment)
+    else minus alignment (offset `mod` alignment)
 
 ||| Proof that alignment divides aligned size
 public export
 data Divides : Nat -> Nat -> Type where
   DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
 
+||| Sound decision procedure: does n divide m?
+||| For n = S k, compute the candidate quotient q = m `div` (S k) and check
+||| whether m really equals q * (S k). When it does, the equality witnesses
+||| `Divides n m` directly; otherwise we have no evidence and return Nothing.
+||| (Division by zero yields Nothing — zero divides nothing nonzero.)
+public export
+decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
+decDivides Z m = case decEq m Z of
+  Yes prf => Just (DivideBy Z (rewrite prf in Refl))
+  No _ => Nothing
+decDivides (S k) m =
+  let q = m `div` (S k) in
+  case decEq m (q * (S k)) of
+    Yes prf => Just (DivideBy q prf)
+    No _ => Nothing
+
 ||| Round up to next alignment boundary
 public export
 alignUp : (size : Nat) -> (alignment : Nat) -> Nat
 alignUp size alignment =
   size + paddingFor size alignment
 
-||| Proof that alignUp produces aligned result
+||| Sound divisibility check for an aligned size. The general theorem
+||| "alignUp size align is always divisible by align" needs div/mod lemmas and
+||| is tracked as residual proof work; here we *decide* it via `decDivides`,
+||| which returns a genuine witness when it holds. For the concrete ABI layouts
+||| below, divisibility is proven outright with `DivideBy`.
 public export
-alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align)
-alignUpCorrect size align prf =
-  DivideBy ((size + paddingFor size align) `div` align) Refl
+alignUpDivides : (size : Nat) -> (align : Nat) ->
+                 Maybe (Divides align (alignUp size align))
+alignUpDivides size align = decDivides align (alignUp size align)
 
 --------------------------------------------------------------------------------
 -- WASM Linear Memory Layout
 --------------------------------------------------------------------------------
 
-||| WASM page size is always 64KiB (65536 bytes)
+||| WASM page size is always 64KiB (65536 bytes).
+||| These memory-magnitude constants are `Integer` rather than `Nat`: the 4GiB
+||| product below is far too large to normalise as a unary `Nat` at
+||| type-checking time, and machine-memory sizes are naturally machine integers.
 public export
-wasmPageSize : Nat
+wasmPageSize : Integer
 wasmPageSize = 65536
 
 ||| Maximum WASM linear memory: 4GiB (65536 pages)
 public export
-wasmMaxPages : Nat
+wasmMaxPages : Integer
 wasmMaxPages = 65536
 
-||| Maximum WASM linear memory in bytes
+||| Maximum WASM linear memory in bytes (4 294 967 296)
 public export
-wasmMaxMemory : Nat
+wasmMaxMemory : Integer
 wasmMaxMemory = wasmPageSize * wasmMaxPages
 
 ||| A region in WASM linear memory
@@ -151,7 +176,7 @@ record StructLayout where
 
 ||| Calculate total struct size with padding
 public export
-calcStructSize : Vect n Field -> Nat -> Nat
+calcStructSize : Vect k Field -> Nat -> Nat
 calcStructSize [] align = 0
 calcStructSize (f :: fs) align =
   let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
@@ -160,23 +185,25 @@ calcStructSize (f :: fs) align =
 
 ||| Proof that field offsets are correctly aligned
 public export
-data FieldsAligned : Vect n Field -> Type where
+data FieldsAligned : Vect k Field -> Type where
   NoFields : FieldsAligned []
   ConsField :
     (f : Field) ->
-    (rest : Vect n Field) ->
+    (rest : Vect k Field) ->
     Divides f.alignment f.offset ->
     FieldsAligned rest ->
     FieldsAligned (f :: rest)
 
 ||| Verify a struct layout is valid
 public export
-verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
+verifyLayout : (fields : Vect k Field) -> (align : Nat) -> Either String StructLayout
 verifyLayout fields align =
   let size = calcStructSize fields align
-   in case decSo (size >= sum (map (\f => f.size) fields)) of
-        Yes prf => Right (MkStructLayout fields size align)
-        No _ => Left "Invalid struct size"
+   in case choose (size >= sum (map (\f => f.size) fields)) of
+        Right _ => Left "Invalid struct size"
+        Left szPrf => case decDivides align size of
+          Nothing => Left "Total size is not a multiple of the alignment"
+          Just dvd => Right (MkStructLayout fields size align {sizeCorrect = szPrf} {aligned = dvd})
 
 --------------------------------------------------------------------------------
 -- WASM-Specific Layout Proofs
@@ -185,7 +212,7 @@ verifyLayout fields align =
 ||| Proof that a struct layout fits within a single WASM page
 public export
 data FitsInPage : StructLayout -> Type where
-  PageFit : (layout : StructLayout) -> {auto 0 ok : So (layout.totalSize <= wasmPageSize)} -> FitsInPage layout
+  PageFit : (layout : StructLayout) -> {auto 0 ok : So (natToInteger layout.totalSize <= Layout.wasmPageSize)} -> FitsInPage layout
 
 ||| Layout of the affine resource table in WASM linear memory
 ||| The resource table is a contiguous array of resource slots at a fixed
@@ -208,7 +235,7 @@ tableSize t = t.capacity * resourceLayoutSize t.platform
 ||| Proof that a resource table fits in WASM linear memory
 public export
 data TableInBounds : ResourceTable -> Type where
-  TableOk : (t : ResourceTable) -> {auto 0 ok : So (t.baseOffset + tableSize t <= wasmMaxMemory)} -> TableInBounds t
+  TableOk : (t : ResourceTable) -> {auto 0 ok : So (natToInteger (t.baseOffset + tableSize t) <= Layout.wasmMaxMemory)} -> TableInBounds t
 
 ||| Get the WASM region for the nth resource in a table
 public export
@@ -230,11 +257,25 @@ data CABICompliant : StructLayout -> Type where
     FieldsAligned layout.fields ->
     CABICompliant layout
 
+||| Decide whether every field of a vector is aligned (offset divisible by
+||| the field's alignment), producing a FieldsAligned witness when so.
+public export
+decFieldsAligned : (fields : Vect k Field) -> Maybe (FieldsAligned fields)
+decFieldsAligned [] = Just NoFields
+decFieldsAligned (f :: fs) =
+  case decDivides f.alignment f.offset of
+    Nothing => Nothing
+    Just dvd => case decFieldsAligned fs of
+      Nothing => Nothing
+      Just rest => Just (ConsField f fs dvd rest)
+
 ||| Check if layout follows C ABI
 public export
 checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
 checkCABI layout =
-  Right (CABIOk layout ?fieldsAlignedProof)
+  case decFieldsAligned layout.fields of
+    Just prf => Right (CABIOk layout prf)
+    Nothing => Left "Struct fields are not correctly aligned for C ABI"
 
 --------------------------------------------------------------------------------
 -- Example: Tracked File Descriptor Layout
@@ -254,6 +295,8 @@ trackedFDLayout =
     ]
     20   -- Total size: 20 bytes
     4    -- Alignment: 4 bytes (WASM native)
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 5 Refl}  -- 20 = 5 * 4
 
 --------------------------------------------------------------------------------
 -- Offset Calculation
@@ -269,5 +312,8 @@ fieldOffset layout name =
 
 ||| Proof that field offset is within struct bounds
 public export
-offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
-offsetInBounds layout f = ?offsetInBoundsProof
+offsetInBounds : (layout : StructLayout) -> (f : Field) -> Maybe (So (f.offset + f.size <= layout.totalSize))
+offsetInBounds layout f =
+  case choose (f.offset + f.size <= layout.totalSize) of
+    Left ok => Just ok
+    Right _ => Nothing

src/interface/abi/Layout.idr …face/abi/Affinescriptiser/ABI/Layout.idrsrc/interface/abi/Layout.idr renamed to src/interface/abi/Affinescriptiser/ABI/Layout.idr src/interface/abi/Layout.idr renamed to src/interface/abi/Affinescriptiser/ABI/Layout.idr

@@ -0,0 +1,77 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Machine-checked theorems for the Affinescriptiser ABI.
+|||
+||| These theorems pin down the correctness of the concrete struct layouts and
+||| the FFI result-code encoding. They are checked by the Idris2 type checker:
+||| if a layout's field offsets stopped being correctly aligned, or the result
+||| encoding changed, this module would fail to compile.
+
+module Affinescriptiser.ABI.Proofs
+
+import Affinescriptiser.ABI.Types
+import Affinescriptiser.ABI.Layout
+import Data.Vect
+
+%default total
+
+--------------------------------------------------------------------------------
+-- Layout compliance
+--------------------------------------------------------------------------------
+
+||| The tracked-file-descriptor layout is C-ABI compliant: every field's offset
+||| is an exact multiple of that field's alignment.
+|||
+||| Field offsets: kind=0, linearity=4, ownership=8, padding=12, fd=16, each
+||| with alignment 4. The DivideBy witnesses give offset = k * 4 for each:
+||| 0=0*4, 4=1*4, 8=2*4, 12=3*4, 16=4*4. These multiplications reduce during
+||| typechecking, so the equalities hold by Refl.
+export
+trackedFDCompliant : CABICompliant Layout.trackedFDLayout
+trackedFDCompliant =
+  CABIOk Layout.trackedFDLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+      (ConsField _ _ (DivideBy 1 Refl)
+        (ConsField _ _ (DivideBy 2 Refl)
+          (ConsField _ _ (DivideBy 3 Refl)
+            (ConsField _ _ (DivideBy 4 Refl)
+              NoFields)))))
+
+--------------------------------------------------------------------------------
+-- Result-code encoding
+--------------------------------------------------------------------------------
+
+||| The success result encodes to the C integer 0, as required by callers that
+||| test the FFI return value against zero.
+export
+okIsZero : resultToInt Ok = 0
+okIsZero = Refl
+
+||| The affine-violation result encodes to 5, matching the dispatch in
+||| Foreign.analyse which maps 5 to AffineViolation.
+export
+affineViolationIsFive : resultToInt AffineViolation = 5
+affineViolationIsFive = Refl
+
+||| The resource-leak result encodes to 6, matching Foreign.analyse's mapping
+||| of 6 to ResourceLeak.
+export
+resourceLeakIsSix : resultToInt ResourceLeak = 6
+resourceLeakIsSix = Refl
+
+--------------------------------------------------------------------------------
+-- Default linearity
+--------------------------------------------------------------------------------
+
+||| Mutex locks default to Linear (exactly-once): failing to unlock is a bug, so
+||| the affine "at most once" relaxation is not permitted for them.
+export
+mutexIsLinear : defaultLinearity MutexLock = Linear
+mutexIsLinear = Refl
+
+||| File descriptors default to Affine (at most once) — the safe default for
+||| acquire/release resources.
+export
+fdIsAffine : defaultLinearity FileDescriptor = Affine
+fdIsAffine = Refl