ABI: make Idris2 proofs genuinely compile + add machine-checked theorems

.gitignore

@@ -15,6 +15,9 @@ Thumbs.db
 /target/
 /_build/
 /build/
+**/build/
+*.ttc
+*.ttm
 /dist/
 /out/
 

src/interface/abi/Layout.idr → src/interface/abi/Atsiser/ABI/Layout.idr

@@ -16,6 +16,8 @@ module Atsiser.ABI.Layout
 import Atsiser.ABI.Types
 import Data.Vect
 import Data.So
+import Data.Nat
+import Decidable.Equality
 
 %default total
 
@@ -29,24 +31,39 @@ 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 quotient and check m = q * (S k) by decidable
+||| equality. Division does not reduce during typechecking, so the equation
+||| is genuinely checked at runtime rather than asserted.
+public export
+decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
+decDivides Z _ = Nothing
+decDivides (S k) m =
+  let q = div m (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
+||| Decide that `alignUp size align` is divisible by `align`.
+||| Returns a genuine `Divides` witness when the quotient checks out, and
+||| `Nothing` otherwise (e.g. align = 0). A `Refl`-only proof is impossible
+||| here because division does not reduce during typechecking.
 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
+alignUpCorrect : (size : Nat) -> (align : Nat) -> Maybe (Divides align (alignUp size align))
+alignUpCorrect size align = decDivides align (alignUp size align)
 
 --------------------------------------------------------------------------------
 -- Ownership-Annotated Fields
@@ -109,7 +126,7 @@ ownedFieldCount layout = length (filter requiresOwnershipTracking (toList layout
 
 ||| Calculate total struct size with padding
 public export
-calcStructSize : Vect n Field -> Nat -> Nat
+calcStructSize : Vect len Field -> Nat -> Nat
 calcStructSize [] align = 0
 calcStructSize (f :: fs) align =
   let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
@@ -118,23 +135,30 @@ calcStructSize (f :: fs) align =
 
 ||| Proof that field offsets are correctly aligned
 public export
-data FieldsAligned : Vect n Field -> Type where
+data FieldsAligned : Vect len Field -> Type where
   NoFields : FieldsAligned []
   ConsField :
     (f : Field) ->
-    (rest : Vect n Field) ->
+    (rest : Vect len Field) ->
     Divides f.alignment f.offset ->
     FieldsAligned rest ->
     FieldsAligned (f :: rest)
 
-||| Verify a struct layout is valid
+||| Verify a struct layout is valid.
+||| Both erased obligations of `MkStructLayout` are discharged with genuine
+||| witnesses: the size bound via `choose`, and `Divides align size` via
+||| `decDivides`. If either fails to hold for the computed size, we report an
+||| error instead of fabricating a proof.
 public export
-verifyLayout : (name : String) -> (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
+verifyLayout : (name : String) -> (fields : Vect len Field) -> (align : Nat) -> Either String StructLayout
 verifyLayout name fields align =
-  let size = calcStructSize fields align
-   in case decSo (size >= sum (map (\f => f.size) fields)) of
-        Yes prf => Right (MkStructLayout name fields size align)
-        No _ => Left "Invalid struct size for \{name}"
+  let size = calcStructSize fields align in
+  case choose (size >= sum (map (\f => f.size) fields)) of
+    Right _ => Left "Invalid struct size for \{name}"
+    Left szOk => case decDivides align size of
+      Nothing => Left "Total size of \{name} is not aligned to \{show align}"
+      Just dvd => Right (MkStructLayout name fields size align
+                          {sizeCorrect = szOk} {aligned = dvd})
 
 --------------------------------------------------------------------------------
 -- Platform-Specific Layouts
@@ -165,11 +189,25 @@ data CABICompliant : StructLayout -> Type where
     FieldsAligned layout.fields ->
     CABICompliant layout
 
+||| Decide whether every field's offset is aligned to its alignment,
+||| building a FieldsAligned witness over the whole vector.
+public export
+decFieldsAligned : (fields : Vect len Field) -> Maybe (FieldsAligned fields)
+decFieldsAligned [] = Just NoFields
+decFieldsAligned (f :: rest) =
+  case decDivides f.alignment f.offset of
+    Nothing => Nothing
+    Just dvd => case decFieldsAligned rest of
+      Nothing => Nothing
+      Just restPrf => Just (ConsField f rest dvd restPrf)
+
 ||| 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 \{layout.structName} has misaligned fields"
 
 --------------------------------------------------------------------------------
 -- Ownership Graph for Structs
@@ -216,6 +254,8 @@ exampleOwnedLayout =
     ]
     16  -- Total size: 16 bytes
     8   -- Alignment: 8 bytes
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 2 Refl}  -- 16 = 2 * 8
 
 ||| Example: Layout for a struct with a borrowed pointer.
 ||| This is what atsiser generates when it finds:
@@ -231,6 +271,8 @@ exampleBorrowedLayout =
     ]
     16  -- Total size: 16 bytes (with padding)
     8   -- Alignment: 8 bytes
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 2 Refl}  -- 16 = 2 * 8
 
 --------------------------------------------------------------------------------
 -- Offset Calculation
@@ -244,7 +286,11 @@ 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's offset+size fits within the struct's total size.
+||| Returns a proof when the bound holds, Nothing otherwise (it does not hold
+||| in general, so a universally-quantified return type would be unsound).
 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/Atsiser/ABI/Proofs.idr

@@ -0,0 +1,65 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Machine-checked theorems about the Atsiser ABI.
+|||
+||| These theorems pin down properties that the rest of the ABI relies on:
+|||   * the example struct layouts are genuinely C-ABI compliant
+|||     (every field offset is a multiple of its alignment), and
+|||   * the result-code encoding agrees with the C contract.
+|||
+||| Each compliance witness is built DIRECTLY (one `DivideBy` per field),
+||| because multiplication reduces during typechecking while division does
+||| not — so these are checked, not asserted.
+
+module Atsiser.ABI.Proofs
+
+import Atsiser.ABI.Types
+import Atsiser.ABI.Layout
+import Data.Vect
+
+%default total
+
+--------------------------------------------------------------------------------
+-- Struct Layout Compliance
+--------------------------------------------------------------------------------
+
+||| `exampleOwnedLayout` follows the C ABI: field `data` at offset 0 (= 0 * 8)
+||| and field `len` at offset 8 (= 1 * 8) are both aligned to 8.
+export
+exampleOwnedCompliant : CABICompliant Layout.exampleOwnedLayout
+exampleOwnedCompliant =
+  CABIOk Layout.exampleOwnedLayout
+    (ConsField _ _ (DivideBy 0 Refl)   -- data: offset 0 = 0 * 8
+      (ConsField _ _ (DivideBy 1 Refl) -- len:  offset 8 = 1 * 8
+        NoFields))
+
+||| `exampleBorrowedLayout` follows the C ABI: field `name` at offset 0 (= 0 * 8)
+||| aligned to 8, and field `flags` at offset 8 (= 2 * 4) aligned to 4.
+export
+exampleBorrowedCompliant : CABICompliant Layout.exampleBorrowedLayout
+exampleBorrowedCompliant =
+  CABIOk Layout.exampleBorrowedLayout
+    (ConsField _ _ (DivideBy 0 Refl)   -- name:  offset 0 = 0 * 8
+      (ConsField _ _ (DivideBy 2 Refl) -- flags: offset 8 = 2 * 4
+        NoFields))
+
+--------------------------------------------------------------------------------
+-- Result-Code Encoding
+--------------------------------------------------------------------------------
+
+||| The success code encodes to 0, as the C FFI contract requires.
+export
+okIsZero : resultToInt Ok = 0
+okIsZero = Refl
+
+||| The generic-error code encodes to 1, distinct from success.
+export
+errorIsOne : resultToInt Error = 1
+errorIsOne = Refl
+
+||| The result encoding is injective on the two codes that the FFI layer
+||| branches on most: success and bounds violation map to different integers.
+export
+okNotBounds : Not (resultToInt Ok = resultToInt BoundsViolation)
+okNotBounds = \case Refl impossible

src/interface/abi/Types.idr → src/interface/abi/Atsiser/ABI/Types.idr

@@ -17,6 +17,7 @@ module Atsiser.ABI.Types
 import Data.Bits
 import Data.So
 import Data.Vect
+import Decidable.Equality
 
 %default total
 
@@ -29,13 +30,10 @@ public export
 data Platform = Linux | Windows | MacOS | BSD | WASM
 
 ||| Compile-time platform detection
-||| This will be set during compilation based on target
+||| This is the default target; override with compiler flags as needed.
 public export
 thisPlatform : Platform
-thisPlatform =
-  %runElab do
-    -- Platform detection logic
-    pure Linux  -- Default, override with compiler flags
+thisPlatform = Linux
 
 --------------------------------------------------------------------------------
 -- Result Codes
@@ -81,7 +79,48 @@ DecEq Result where
   decEq NullPointer NullPointer = Yes Refl
   decEq OwnershipViolation OwnershipViolation = Yes Refl
   decEq BoundsViolation BoundsViolation = Yes Refl
-  decEq _ _ = No absurd
+  decEq Ok Error = No (\case Refl impossible)
+  decEq Ok InvalidParam = No (\case Refl impossible)
+  decEq Ok OutOfMemory = No (\case Refl impossible)
+  decEq Ok NullPointer = No (\case Refl impossible)
+  decEq Ok OwnershipViolation = No (\case Refl impossible)
+  decEq Ok BoundsViolation = No (\case Refl impossible)
+  decEq Error Ok = No (\case Refl impossible)
+  decEq Error InvalidParam = No (\case Refl impossible)
+  decEq Error OutOfMemory = No (\case Refl impossible)
+  decEq Error NullPointer = No (\case Refl impossible)
+  decEq Error OwnershipViolation = No (\case Refl impossible)
+  decEq Error BoundsViolation = No (\case Refl impossible)
+  decEq InvalidParam Ok = No (\case Refl impossible)
+  decEq InvalidParam Error = No (\case Refl impossible)
+  decEq InvalidParam OutOfMemory = No (\case Refl impossible)
+  decEq InvalidParam NullPointer = No (\case Refl impossible)
+  decEq InvalidParam OwnershipViolation = No (\case Refl impossible)
+  decEq InvalidParam BoundsViolation = No (\case Refl impossible)
+  decEq OutOfMemory Ok = No (\case Refl impossible)
+  decEq OutOfMemory Error = No (\case Refl impossible)
+  decEq OutOfMemory InvalidParam = No (\case Refl impossible)
+  decEq OutOfMemory NullPointer = No (\case Refl impossible)
+  decEq OutOfMemory OwnershipViolation = No (\case Refl impossible)
+  decEq OutOfMemory BoundsViolation = No (\case Refl impossible)
+  decEq NullPointer Ok = No (\case Refl impossible)
+  decEq NullPointer Error = No (\case Refl impossible)
+  decEq NullPointer InvalidParam = No (\case Refl impossible)
+  decEq NullPointer OutOfMemory = No (\case Refl impossible)
+  decEq NullPointer OwnershipViolation = No (\case Refl impossible)
+  decEq NullPointer BoundsViolation = No (\case Refl impossible)
+  decEq OwnershipViolation Ok = No (\case Refl impossible)
+  decEq OwnershipViolation Error = No (\case Refl impossible)
+  decEq OwnershipViolation InvalidParam = No (\case Refl impossible)
+  decEq OwnershipViolation OutOfMemory = No (\case Refl impossible)
+  decEq OwnershipViolation NullPointer = No (\case Refl impossible)
+  decEq OwnershipViolation BoundsViolation = No (\case Refl impossible)
+  decEq BoundsViolation Ok = No (\case Refl impossible)
+  decEq BoundsViolation Error = No (\case Refl impossible)
+  decEq BoundsViolation InvalidParam = No (\case Refl impossible)
+  decEq BoundsViolation OutOfMemory = No (\case Refl impossible)
+  decEq BoundsViolation NullPointer = No (\case Refl impossible)
+  decEq BoundsViolation OwnershipViolation = No (\case Refl impossible)
 
 --------------------------------------------------------------------------------
 -- Ownership State Machine
@@ -165,8 +204,9 @@ data Handle : Type where
 ||| Returns Nothing if pointer is null
 public export
 createHandle : Bits64 -> Maybe Handle
-createHandle 0 = Nothing
-createHandle ptr = Just (MkHandle ptr)
+createHandle ptr = case choose (ptr /= 0) of
+  Left ok => Just (MkHandle ptr {nonNull = ok})
+  Right _ => Nothing
 
 ||| Extract pointer value from handle
 public export
@@ -281,19 +321,20 @@ data HasAlignment : Type -> Nat -> Type where
 
 ||| Size of C types (platform-specific)
 public export
+||| Note: `CInt p` / `CSize p` are type synonyms that reduce to `Bits32`/`Bits64`,
+||| so they are covered by the `Bits32`/`Bits64` cases below rather than matched
+||| as constructors (Idris2 cannot pattern-match on a type-level function).
 cSizeOf : (p : Platform) -> (t : Type) -> Nat
-cSizeOf p (CInt _) = 4
-cSizeOf p (CSize _) = if ptrSize p == 64 then 8 else 4
 cSizeOf p Bits32 = 4
 cSizeOf p Bits64 = 8
 cSizeOf p Double = 8
 cSizeOf p _ = ptrSize p `div` 8
 
 ||| Alignment of C types (platform-specific)
 public export
+||| As with `cSizeOf`, `CInt`/`CSize` reduce to `Bits32`/`Bits64` and are
+||| handled by those cases rather than matched as constructors.
 cAlignOf : (p : Platform) -> (t : Type) -> Nat
-cAlignOf p (CInt _) = 4
-cAlignOf p (CSize _) = if ptrSize p == 64 then 8 else 4
 cAlignOf p Bits32 = 4
 cAlignOf p Bits64 = 8
 cAlignOf p Double = 8

src/interface/abi/atsiser-abi.ipkg

@@ -0,0 +1,9 @@
+-- SPDX-License-Identifier: MPL-2.0
+package atsiser-abi
+
+sourcedir = "."
+
+modules = Atsiser.ABI.Types
+        , Atsiser.ABI.Layout
+        , Atsiser.ABI.Foreign
+        , Atsiser.ABI.Proofs