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

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

Part of the family-wide ABI-proofs review. The hand-written ABI was
never compiler-checked and 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

@@ -117,3 +117,8 @@ deps/
 .cache/
 build/
 dist/
+
+# Idris2 build artefacts
+**/build/
+*.ttc
+*.ttm

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

@@ -19,6 +19,8 @@ module Verisimiser.ABI.Layout
 import Verisimiser.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.
+||| 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 (`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)
 
 --------------------------------------------------------------------------------
 -- 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"
 
 --------------------------------------------------------------------------------
 -- OctadRecord Layout
@@ -183,11 +208,26 @@ octadRecordLayout =
     ]
     80  -- Total size: 80 bytes
     8   -- Alignment: 8 bytes
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 10 Refl}
 
 ||| Proof that the OctadRecord layout is C-ABI compliant.
 export
-octadRecordValid : CABICompliant octadRecordLayout
-octadRecordValid = CABIOk octadRecordLayout ?octadFieldsAligned
+octadRecordValid : CABICompliant Layout.octadRecordLayout
+octadRecordValid =
+  CABIOk octadRecordLayout
+    (ConsField _ _ (DivideBy 0 Refl)   -- entity_id      0 / 8
+    (ConsField _ _ (DivideBy 2 Refl)   -- backend        8 / 4
+    (ConsField _ _ (DivideBy 3 Refl)   -- active_dims   12 / 4
+    (ConsField _ _ (DivideBy 2 Refl)   -- provenance    16 / 8
+    (ConsField _ _ (DivideBy 3 Refl)   -- temporal      24 / 8
+    (ConsField _ _ (DivideBy 4 Refl)   -- drift_score   32 / 8
+    (ConsField _ _ (DivideBy 5 Refl)   -- lineage       40 / 8
+    (ConsField _ _ (DivideBy 6 Refl)   -- constraints   48 / 8
+    (ConsField _ _ (DivideBy 7 Refl)   -- acl           56 / 8
+    (ConsField _ _ (DivideBy 8 Refl)   -- simulation    64 / 8
+    (ConsField _ _ (DivideBy 9 Refl)   -- metadata      72 / 8
+     NoFields)))))))))))
 
 --------------------------------------------------------------------------------
 -- ProvenanceEntry Layout
@@ -218,11 +258,21 @@ provenanceEntryLayout =
     ]
     88  -- Total size: 88 bytes
     8   -- Alignment: 8 bytes
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 11 Refl}
 
 ||| Proof that the ProvenanceEntry layout is C-ABI compliant.
 export
-provenanceEntryValid : CABICompliant provenanceEntryLayout
-provenanceEntryValid = CABIOk provenanceEntryLayout ?provenanceFieldsAligned
+provenanceEntryValid : CABICompliant Layout.provenanceEntryLayout
+provenanceEntryValid =
+  CABIOk provenanceEntryLayout
+    (ConsField _ _ (DivideBy 0 Refl)    -- hash           0 / 1
+    (ConsField _ _ (DivideBy 32 Refl)   -- previous_hash 32 / 1
+    (ConsField _ _ (DivideBy 8 Refl)    -- entity_id     64 / 8
+    (ConsField _ _ (DivideBy 18 Refl)   -- operation     72 / 4
+    (ConsField _ _ (DivideBy 19 Refl)   -- _padding      76 / 4
+    (ConsField _ _ (DivideBy 10 Refl)   -- timestamp     80 / 8
+     NoFields))))))
 
 --------------------------------------------------------------------------------
 -- DriftMeasurement Layout
@@ -248,11 +298,19 @@ driftMeasurementLayout =
     ]
     88  -- Total size: 88 bytes
     8   -- Alignment: 8 bytes
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 11 Refl}
 
 ||| Proof that the DriftMeasurement layout is C-ABI compliant.
 export
-driftMeasurementValid : CABICompliant driftMeasurementLayout
-driftMeasurementValid = CABIOk driftMeasurementLayout ?driftFieldsAligned
+driftMeasurementValid : CABICompliant Layout.driftMeasurementLayout
+driftMeasurementValid =
+  CABIOk driftMeasurementLayout
+    (ConsField _ _ (DivideBy 0 Refl)    -- entity_id      0 / 8
+    (ConsField _ _ (DivideBy 1 Refl)    -- overall_score  8 / 8
+    (ConsField _ _ (DivideBy 2 Refl)    -- scores        16 / 8
+    (ConsField _ _ (DivideBy 10 Refl)   -- measured_at   80 / 8
+     NoFields))))
 
 --------------------------------------------------------------------------------
 -- TemporalSnapshot Layout
@@ -284,25 +342,43 @@ temporalSnapshotLayout =
     ]
     48  -- Total size: 48 bytes
     8   -- Alignment: 8 bytes
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 6 Refl}
 
 ||| Proof that the TemporalSnapshot layout is C-ABI compliant.
 export
-temporalSnapshotValid : CABICompliant temporalSnapshotLayout
-temporalSnapshotValid = CABIOk temporalSnapshotLayout ?temporalFieldsAligned
+temporalSnapshotValid : CABICompliant Layout.temporalSnapshotLayout
+temporalSnapshotValid =
+  CABIOk temporalSnapshotLayout
+    (ConsField _ _ (DivideBy 0 Refl)    -- entity_id      0 / 8
+    (ConsField _ _ (DivideBy 1 Refl)    -- version        8 / 8
+    (ConsField _ _ (DivideBy 2 Refl)    -- valid_from    16 / 8
+    (ConsField _ _ (DivideBy 3 Refl)    -- valid_to      24 / 8
+    (ConsField _ _ (DivideBy 4 Refl)    -- snapshot_ptr  32 / 8
+    (ConsField _ _ (DivideBy 10 Refl)   -- snapshot_len  40 / 4
+    (ConsField _ _ (DivideBy 11 Refl)   -- operation     44 / 4
+     NoFields)))))))
 
 --------------------------------------------------------------------------------
 -- Offset Calculation
 --------------------------------------------------------------------------------
 
 ||| Calculate field offset with proof of correctness.
 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

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

@@ -0,0 +1,123 @@
+-- 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 VeriSimiser 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, the result-code 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 avoid routing them through `Nat` division, which is a
+||| primitive that does not reduce at the type level.
+
+module Verisimiser.ABI.Proofs
+
+import Verisimiser.ABI.Types
+import Verisimiser.ABI.Layout
+import Data.So
+import Data.Vect
+
+%default total
+
+--------------------------------------------------------------------------------
+-- The concrete FFI struct layouts are provably C-ABI compliant.
+--------------------------------------------------------------------------------
+
+||| Every field offset in the OctadRecord layout divides its alignment:
+||| 0|8, 8|4, 12|4, 16|8, 24|8, 32|8, 40|8, 48|8, 56|8, 64|8, 72|8.
+export
+octadRecordCompliant : CABICompliant Layout.octadRecordLayout
+octadRecordCompliant =
+  CABIOk octadRecordLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 4 Refl)
+    (ConsField _ _ (DivideBy 5 Refl)
+    (ConsField _ _ (DivideBy 6 Refl)
+    (ConsField _ _ (DivideBy 7 Refl)
+    (ConsField _ _ (DivideBy 8 Refl)
+    (ConsField _ _ (DivideBy 9 Refl)
+     NoFields)))))))))))
+
+||| Every field offset in the ProvenanceEntry layout is aligned:
+||| 0|1, 32|1, 64|8, 72|4, 76|4, 80|8.
+export
+provenanceEntryCompliant : CABICompliant Layout.provenanceEntryLayout
+provenanceEntryCompliant =
+  CABIOk provenanceEntryLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 32 Refl)
+    (ConsField _ _ (DivideBy 8 Refl)
+    (ConsField _ _ (DivideBy 18 Refl)
+    (ConsField _ _ (DivideBy 19 Refl)
+    (ConsField _ _ (DivideBy 10 Refl)
+     NoFields))))))
+
+||| Every field offset in the DriftMeasurement layout is aligned:
+||| 0|8, 8|8, 16|8, 80|8.
+export
+driftMeasurementCompliant : CABICompliant Layout.driftMeasurementLayout
+driftMeasurementCompliant =
+  CABIOk driftMeasurementLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 10 Refl)
+     NoFields))))
+
+||| Every field offset in the TemporalSnapshot layout is aligned:
+||| 0|8, 8|8, 16|8, 24|8, 32|8, 40|4, 44|4.
+export
+temporalSnapshotCompliant : CABICompliant Layout.temporalSnapshotLayout
+temporalSnapshotCompliant =
+  CABIOk temporalSnapshotLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 4 Refl)
+    (ConsField _ _ (DivideBy 10 Refl)
+    (ConsField _ _ (DivideBy 11 Refl)
+     NoFields)))))))
+
+--------------------------------------------------------------------------------
+-- Result-code round-trip: the encoding the Zig FFI depends on.
+--------------------------------------------------------------------------------
+
+export
+okIsZero : resultToInt Ok = 0
+okIsZero = Refl
+
+export
+nullPointerIsFour : resultToInt NullPointer = 4
+nullPointerIsFour = Refl
+
+--------------------------------------------------------------------------------
+-- Octad model invariants.
+--------------------------------------------------------------------------------
+
+||| The octad is exactly eight dimensions — the defining cardinality of the
+||| VeriSimDB model.
+export
+octadCardinality : length Types.allDimensions = 8
+octadCardinality = Refl
+
+||| The octad tag encoding the Zig FFI depends on: Simulation is the eighth
+||| (index 7) dimension.
+export
+simulationIsSeven : octadToInt Simulation = 7
+simulationIsSeven = Refl
+
+||| Tier 1 (piggyback) capabilities carry a static proof that they never write
+||| to the target database — the core safety guarantee of VeriSimiser.
+export
+provenanceIsPiggyback : dimensionTier Provenance = Tier1
+provenanceIsPiggyback = Refl