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

## 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>

Author: 3 people

.gitignore

@@ -15,9 +15,14 @@ Thumbs.db
 /target/
 /_build/
 /build/
+**/build/
 /dist/
 /out/
 
+# Idris2 build artifacts
+*.ttc
+*.ttm
+
 # Dependencies
 /node_modules/
 /vendor/

src/interface/abi/Foreign.idr …nterface/abi/Eclexiaiser/ABI/Foreign.idrsrc/interface/abi/Foreign.idr renamed to src/interface/abi/Eclexiaiser/ABI/Foreign.idr src/interface/abi/Foreign.idr renamed to src/interface/abi/Eclexiaiser/ABI/Foreign.idr

@@ -18,6 +18,8 @@ module Eclexiaiser.ABI.Layout
 import Eclexiaiser.ABI.Types
 import Data.Vect
 import Data.So
+import Data.Nat
+import Decidable.Equality
 
 %default total
 
@@ -31,24 +33,38 @@ 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
 
+||| Decision procedure for divisibility.
+||| For n = S j, compute q = m `div` (S j) and check m = q * (S j).
+||| Division does not reduce definitionally, so we confirm the candidate
+||| witness via decidable equality on the (reducing) multiplication.
+public export
+decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
+decDivides Z m = Nothing
+decDivides (S j) m =
+  let q = m `div` (S j) in
+  case decEq m (q * (S j)) 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
+||| Decide whether alignUp produced a genuine multiple of the alignment.
+||| (alignUp is only a multiple of `align` when `align > 0`, so the
+||| witness is returned in Maybe rather than asserted unconditionally.)
 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
+alignUpAligned : (size : Nat) -> (align : Nat) -> Maybe (Divides align (alignUp size align))
+alignUpAligned size align = decDivides align (alignUp size align)
 
 --------------------------------------------------------------------------------
 -- Struct Field Layout
@@ -72,15 +88,15 @@ nextFieldOffset f = alignUp (f.offset + f.size) f.alignment
 public export
 record StructLayout where
   constructor MkStructLayout
-  fields : Vect n Field
+  fields : Vect len Field
   totalSize : Nat
   alignment : Nat
   {auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))}
   {auto 0 aligned : Divides alignment totalSize}
 
 ||| 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
@@ -89,23 +105,28 @@ 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
+        Left szPrf =>
+          case decDivides align size of
+            Just alPrf =>
+              Right (MkStructLayout fields size align
+                       {sizeCorrect = szPrf} {aligned = alPrf})
+            Nothing => Left "Total size is not a multiple of alignment"
+        Right _ => Left "Invalid struct size"
 
 --------------------------------------------------------------------------------
 -- Platform-Specific Layouts
@@ -136,11 +157,26 @@ data CABICompliant : StructLayout -> Type where
     FieldsAligned layout.fields ->
     CABICompliant layout
 
+||| Decide whether every field's offset is a multiple of its alignment,
+||| building a FieldsAligned witness directly from per-field decDivides.
+public export
+decFieldsAligned : (fs : Vect k Field) -> Maybe (FieldsAligned fs)
+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"
 
 --------------------------------------------------------------------------------
 -- EnergyMeasurement Layout
@@ -165,11 +201,19 @@ energyMeasurementLayout =
     ]
     32  -- Total size: 32 bytes (28 data + 4 padding)
     8   -- Alignment: 8 bytes
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 4 Refl}  -- 32 = 4 * 8
 
 ||| Proof that EnergyMeasurement layout is C-ABI compliant
 export
-energyMeasurementValid : CABICompliant energyMeasurementLayout
-energyMeasurementValid = CABIOk energyMeasurementLayout ?energyMeasurementAligned
+energyMeasurementValid : CABICompliant Layout.energyMeasurementLayout
+energyMeasurementValid =
+  CABIOk energyMeasurementLayout
+    (ConsField _ _ (DivideBy 0 Refl)    -- offset 0  = 0 * 8
+    (ConsField _ _ (DivideBy 1 Refl)    -- offset 8  = 1 * 8
+    (ConsField _ _ (DivideBy 2 Refl)    -- offset 16 = 2 * 8
+    (ConsField _ _ (DivideBy 6 Refl)    -- offset 24 = 6 * 4
+     NoFields))))
 
 --------------------------------------------------------------------------------
 -- CarbonQuery Layout
@@ -195,11 +239,20 @@ carbonQueryLayout =
     ]
     24  -- Total size: 24 bytes
     8   -- Alignment: 8 bytes
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 3 Refl}  -- 24 = 3 * 8
 
 ||| Proof that CarbonQuery layout is C-ABI compliant
 export
-carbonQueryValid : CABICompliant carbonQueryLayout
-carbonQueryValid = CABIOk carbonQueryLayout ?carbonQueryAligned
+carbonQueryValid : CABICompliant Layout.carbonQueryLayout
+carbonQueryValid =
+  CABIOk carbonQueryLayout
+    (ConsField _ _ (DivideBy 0 Refl)    -- offset 0  = 0 * 4
+    (ConsField _ _ (DivideBy 1 Refl)    -- offset 4  = 1 * 4
+    (ConsField _ _ (DivideBy 1 Refl)    -- offset 8  = 1 * 8
+    (ConsField _ _ (DivideBy 4 Refl)    -- offset 16 = 4 * 4
+    (ConsField _ _ (DivideBy 5 Refl)    -- offset 20 = 5 * 4
+     NoFields)))))
 
 --------------------------------------------------------------------------------
 -- BudgetEnforcement Layout
@@ -226,11 +279,20 @@ budgetEnforcementLayout =
     ]
     40  -- Total size: 40 bytes (36 data + 4 padding)
     8   -- Alignment: 8 bytes
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 5 Refl}  -- 40 = 5 * 8
 
 ||| Proof that BudgetEnforcement layout is C-ABI compliant
 export
-budgetEnforcementValid : CABICompliant budgetEnforcementLayout
-budgetEnforcementValid = CABIOk budgetEnforcementLayout ?budgetEnforcementAligned
+budgetEnforcementValid : CABICompliant Layout.budgetEnforcementLayout
+budgetEnforcementValid =
+  CABIOk budgetEnforcementLayout
+    (ConsField _ _ (DivideBy 0 Refl)    -- offset 0  = 0 * 8
+    (ConsField _ _ (DivideBy 1 Refl)    -- offset 8  = 1 * 8
+    (ConsField _ _ (DivideBy 2 Refl)    -- offset 16 = 2 * 8
+    (ConsField _ _ (DivideBy 3 Refl)    -- offset 24 = 3 * 8
+    (ConsField _ _ (DivideBy 8 Refl)    -- offset 32 = 8 * 4
+     NoFields)))))
 
 --------------------------------------------------------------------------------
 -- Offset Calculation
@@ -244,7 +306,12 @@ fieldOffset layout name =
     Just idx => Just (finToNat idx ** index idx layout.fields)
     Nothing => Nothing
 
-||| Proof that field offset is within struct bounds
+||| Decide whether a field fits within the struct's total size.
+||| Returns a witness only when the bound genuinely holds (it is false
+||| in general), so the result is wrapped in Maybe.
 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 …interface/abi/Eclexiaiser/ABI/Layout.idrsrc/interface/abi/Layout.idr renamed to src/interface/abi/Eclexiaiser/ABI/Layout.idr src/interface/abi/Layout.idr renamed to src/interface/abi/Eclexiaiser/ABI/Layout.idr

@@ -0,0 +1,80 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Machine-checked ABI theorems for Eclexiaiser.
+|||
+||| This module carries the load-bearing correctness proofs for the
+||| eclexiaiser ABI: every concrete C-struct layout is proven C-ABI
+||| compliant by exhibiting a FieldsAligned witness directly (one
+||| DivideBy per field, with field.offset = k * field.alignment, which
+||| reduces by multiplication during typechecking), plus a couple of
+||| result-code encoding pins.
+
+module Eclexiaiser.ABI.Proofs
+
+import Eclexiaiser.ABI.Types
+import Eclexiaiser.ABI.Layout
+import Data.Vect
+
+%default total
+
+--------------------------------------------------------------------------------
+-- C-ABI Compliance of Concrete Struct Layouts
+--------------------------------------------------------------------------------
+
+||| EnergyMeasurement is C-ABI compliant: all field offsets are multiples
+||| of their alignment (0=0*8, 8=1*8, 16=2*8, 24=6*4).
+export
+energyMeasurementCompliant : CABICompliant Layout.energyMeasurementLayout
+energyMeasurementCompliant =
+  CABIOk Layout.energyMeasurementLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 6 Refl)
+     NoFields))))
+
+||| CarbonQuery is C-ABI compliant: offsets 0=0*4, 4=1*4, 8=1*8, 16=4*4, 20=5*4.
+export
+carbonQueryCompliant : CABICompliant Layout.carbonQueryLayout
+carbonQueryCompliant =
+  CABIOk Layout.carbonQueryLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 4 Refl)
+    (ConsField _ _ (DivideBy 5 Refl)
+     NoFields)))))
+
+||| BudgetEnforcement is C-ABI compliant: offsets 0=0*8, 8=1*8, 16=2*8,
+||| 24=3*8, 32=8*4.
+export
+budgetEnforcementCompliant : CABICompliant Layout.budgetEnforcementLayout
+budgetEnforcementCompliant =
+  CABIOk Layout.budgetEnforcementLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 8 Refl)
+     NoFields)))))
+
+--------------------------------------------------------------------------------
+-- Result-Code Encoding Pins
+--------------------------------------------------------------------------------
+
+||| The success code encodes to zero at the C boundary.
+export
+okIsZero : resultToInt Ok = 0
+okIsZero = Refl
+
+||| The budget-exceeded code encodes to 5 (matching the Zig FFI contract).
+export
+budgetExceededIsFive : resultToInt BudgetExceeded = 5
+budgetExceededIsFive = Refl
+
+||| Distinct result constructors encode to distinct integers: a concrete
+||| instance pinning that Ok (0) and Error (1) are not confusable.
+export
+okNotError : Not (resultToInt Ok = resultToInt Error)
+okNotError = \case Refl impossible