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

.gitignore

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

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

@@ -19,6 +19,8 @@ module Phronesiser.ABI.Layout
 import Phronesiser.ABI.Types
 import Data.Vect
 import Data.So
+import Data.Nat
+import Decidable.Equality
 
 %default total
 
@@ -32,24 +34,40 @@ 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
+||| Proof that alignment divides aligned size: `m = k * n`.
 public export
 data Divides : Nat -> Nat -> Type where
   DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
 
+||| Sound decision procedure for divisibility. Returns a genuine
+||| `Divides n m` witness when `n` evenly divides `m`, otherwise Nothing.
+||| Division by zero is undecidable here and yields Nothing.
+public export
+decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
+decDivides Z _ = 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
+||| Decide whether the rounded-up size is divisible by the alignment. The
+||| general theorem needs div/mod lemmas from Data.Nat; here we *decide* it
+||| via `decDivides`, returning a genuine witness when it holds. (Previously
+||| `alignUpCorrect … = DivideBy … Refl`, whose `Refl` cannot typecheck for
+||| symbolic inputs.)
 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)
 
 --------------------------------------------------------------------------------
 -- Struct Field Layout
@@ -81,7 +99,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
@@ -90,23 +108,26 @@ 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
+||| Decide field alignment for every field, building a real `FieldsAligned`
+||| witness from per-field divisibility proofs.
 public export
-verifyLayout : (fields : Vect n 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"
+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)
 
 --------------------------------------------------------------------------------
 -- Platform-Specific Layouts
@@ -137,11 +158,15 @@ data CABICompliant : StructLayout -> Type where
     FieldsAligned layout.fields ->
     CABICompliant layout
 
-||| Check if layout follows C ABI
+||| Verify a layout against the C ABI alignment rules, returning a genuine
+||| `CABICompliant` proof (built from real per-field divisibility witnesses)
+||| or an error when some field offset is misaligned.
 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 "Field offsets are not correctly aligned for the C ABI"
 
 --------------------------------------------------------------------------------
 -- Phronesiser Constraint Struct Layout
@@ -160,11 +185,8 @@ constraintLayout =
     ]
     16  -- Total size: 16 bytes
     4   -- Alignment: 4 bytes
-
-||| Proof that constraint layout is valid
-export
-constraintLayoutValid : CABICompliant constraintLayout
-constraintLayoutValid = CABIOk constraintLayout ?constraintFieldsAligned
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 4 Refl}  -- 16 = 4 * 4
 
 --------------------------------------------------------------------------------
 -- Phronesiser Audit Result Struct Layout
@@ -183,11 +205,8 @@ auditResultLayout =
     ]
     16  -- Total size: 16 bytes
     4   -- Alignment: 4 bytes
-
-||| Proof that audit result layout is valid
-export
-auditResultLayoutValid : CABICompliant auditResultLayout
-auditResultLayoutValid = CABIOk auditResultLayout ?auditResultFieldsAligned
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 4 Refl}  -- 16 = 4 * 4
 
 --------------------------------------------------------------------------------
 -- Constraint Set Header Layout
@@ -204,23 +223,32 @@ constraintSetHeaderLayout =
     ]
     8   -- Total size: 8 bytes
     4   -- Alignment: 4 bytes
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 2 Refl}  -- 8 = 2 * 4
 
 --------------------------------------------------------------------------------
 -- Offset Calculation
 --------------------------------------------------------------------------------
 
-||| Calculate field offset with proof of correctness
+||| Look up a field's index and record by name in a layout.
 public export
-fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (n : Nat ** Field)
+fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (Nat, Field)
 fieldOffset layout name =
   case findIndex (\f => f.name == name) layout.fields of
-    Just idx => Just (finToNat idx ** index idx layout.fields)
+    Just idx => Just (finToNat idx, index idx layout.fields)
     Nothing => Nothing
 
-||| Proof that field offset is within struct bounds
+||| Decide whether a field lies within a struct's byte bounds, returning a
+||| genuine proof when `offset + size <= totalSize`. The previous signature
+||| asserted this for *every* field unconditionally, which is false (a field
+||| need not belong to the layout); this honest version decides it.
 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
 
 --------------------------------------------------------------------------------
 -- Constraint Array Layout
@@ -232,8 +260,22 @@ public export
 constraintArraySize : (count : Nat) -> Nat
 constraintArraySize count = 8 + (count * 16)
 
-||| Proof that constraint array size grows monotonically with count
+||| `j <= l` implies `j * c <= l * c`, by induction on the `LTE` witness.
+||| Genuine arithmetic lemma — no `believe_me`, no decision shortcut.
+public export
+scaleLteRight : (c : Nat) -> {j, l : Nat} -> LTE j l -> LTE (j * c) (l * c)
+scaleLteRight c LTEZero = LTEZero
+scaleLteRight c (LTESucc {left = a} {right = b} p) =
+  plusLteMonotoneLeft c (a * c) (b * c) (scaleLteRight c p)
+
+||| Proof that constraint array size grows monotonically with count.
+||| `constraintArraySize n = 8 + n * 16`, so this reduces to
+||| `8 + n*16 <= 8 + m*16`, discharged from `n <= m` via `scaleLteRight`
+||| and `plusLteMonotoneLeft`. The `<=` is the propositional `LTE`, the
+||| genuine order relation (the previous `So (... <= ...)` could not be
+||| proven for symbolic inputs, only decided).
 public export
-constraintArrayMonotonic : (n : Nat) -> (m : Nat) -> (n <= m) ->
-                           So (constraintArraySize n <= constraintArraySize m)
-constraintArrayMonotonic n m prf = ?constraintArrayMonotonicProof
+constraintArrayMonotonic : (n : Nat) -> (m : Nat) -> LTE n m ->
+                           LTE (constraintArraySize n) (constraintArraySize m)
+constraintArrayMonotonic n m prf =
+  plusLteMonotoneLeft 8 (n * 16) (m * 16) (scaleLteRight 16 prf)

src/interface/abi/Phronesiser/ABI/Proofs.idr

@@ -0,0 +1,115 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Machine-checked proofs over the phronesiser ABI.
+|||
+||| These are not runtime tests — they are propositional statements the Idris2
+||| type checker must discharge at compile time. If any concrete ABI layout
+||| were misaligned, a result/modality/severity encoding wrong, or a decision
+||| procedure mis-defined, this module would fail to typecheck and the proof
+||| build would go red.
+|||
+||| The C-ABI compliance witnesses are built directly from per-field
+||| divisibility proofs (`DivideBy k Refl`, where `offset = k * alignment`).
+||| Multiplication reduces during type checking, so these are fully verified
+||| by the compiler; we never route them through `Nat` division, which is a
+||| primitive that does not reduce at the type level.
+
+module Phronesiser.ABI.Proofs
+
+import Phronesiser.ABI.Types
+import Phronesiser.ABI.Layout
+import Data.So
+import Data.Vect
+
+%default total
+
+--------------------------------------------------------------------------------
+-- The concrete FFI struct layouts are provably C-ABI compliant.
+--------------------------------------------------------------------------------
+
+||| ConstraintStruct layout: offsets 0,4,8,12 each 4-byte aligned, so
+||| 0 = 0*4, 4 = 1*4, 8 = 2*4, 12 = 3*4.
+export
+constraintLayoutCompliant : CABICompliant Layout.constraintLayout
+constraintLayoutCompliant =
+  CABIOk constraintLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+     NoFields))))
+
+||| AuditResultStruct layout: offsets 0,4,8,12 each 4-byte aligned.
+export
+auditResultLayoutCompliant : CABICompliant Layout.auditResultLayout
+auditResultLayoutCompliant =
+  CABIOk auditResultLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+     NoFields))))
+
+||| ConstraintSetHeader layout: offsets 0,4 each 4-byte aligned, so
+||| 0 = 0*4, 4 = 1*4.
+export
+constraintSetHeaderLayoutCompliant : CABICompliant Layout.constraintSetHeaderLayout
+constraintSetHeaderLayoutCompliant =
+  CABIOk constraintSetHeaderLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+     NoFields))
+
+--------------------------------------------------------------------------------
+-- Result-code encoding: the integers the Zig FFI depends on.
+--------------------------------------------------------------------------------
+
+export
+okIsZero : resultToInt Ok = 0
+okIsZero = Refl
+
+export
+constraintConflictIsSix : resultToInt ConstraintConflict = 6
+constraintConflictIsSix = Refl
+
+--------------------------------------------------------------------------------
+-- Deontic / severity encodings used across the FFI boundary.
+--------------------------------------------------------------------------------
+
+||| The three deontic modalities encode to 0, 1, 2 — pinned for the Zig side.
+export
+prohibitionIsTwo : modalityToInt Prohibition = 2
+prohibitionIsTwo = Refl
+
+||| Obligation and prohibition are genuinely distinct propositions: an action
+||| cannot be both obligatory and prohibited. (Re-exported as a Proofs-level
+||| theorem so the proof build pins the deontic contradiction directly.)
+export
+obligationNotProhibition : Obligation = Prohibition -> Void
+obligationNotProhibition Refl impossible
+
+||| Severity encodes Critical as the maximum code 4.
+export
+criticalIsFour : severityToInt Critical = 4
+criticalIsFour = Refl
+
+--------------------------------------------------------------------------------
+-- Constraint-array sizing is strictly determined and grows with count.
+--------------------------------------------------------------------------------
+
+||| An empty constraint array is exactly the 8-byte header.
+export
+emptyArrayIsHeader : constraintArraySize 0 = 8
+emptyArrayIsHeader = Refl
+
+||| One constraint occupies header (8) + one 16-byte struct = 24 bytes.
+export
+oneConstraintArraySize : constraintArraySize 1 = 24
+oneConstraintArraySize = Refl
+
+||| Monotonicity instantiated: a 2-element set is no larger than a 5-element
+||| set. Exercises `constraintArrayMonotonic` with a concrete `LTE` witness.
+export
+arrayGrows : LTE (constraintArraySize 2) (constraintArraySize 5)
+arrayGrows = constraintArrayMonotonic 2 5 (LTESucc (LTESucc LTEZero))