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

.claude/CLAUDE.md

@@ -27,7 +27,7 @@ cargo test
 ## Key Design Decisions
 
 - Follows hyperpolymath ABI-FFI standard (Idris2 ABI, Zig FFI)
-- MPL-2.0 license
+- MPL-2.0 license (code) + CC-BY-SA-4.0 (docs); full texts in LICENSES/
 - RSR (Rhodium Standard Repository) template
 - Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 

.github/workflows/rhodibot.yml

@@ -4,7 +4,7 @@
 # Reads root-hygiene rules and auto-fixes what it can:
 #   - Delete banned files (AI.djot, duplicate CONTRIBUTING.adoc, stale snapshots)
 #   - Rename misnamed files (AI.a2ml → 0-AI-MANIFEST.a2ml)
-#   - Fix SPDX headers (AGPL → PMPL in dotfiles)
+#   - Fix SPDX headers (AGPL → MPL-2.0 in dotfiles)
 #   - Create missing required files (SECURITY.md, CONTRIBUTING.md)
 #   - Report unfixable issues as PR comments
 #
@@ -87,7 +87,7 @@ jobs:
           for dotfile in .gitignore .gitattributes .editorconfig; do
             if [ -f "$dotfile" ] && grep -q "AGPL-3.0" "$dotfile" 2>/dev/null; then
               sed -i 's/AGPL-3.0-or-later/MPL-2.0/g; s/AGPL-3.0/MPL-2.0/g' "$dotfile"
-              FIXES="$FIXES\n- Fixed SPDX header in \`$dotfile\` (AGPL → PMPL)"
+              FIXES="$FIXES\n- Fixed SPDX header in \`$dotfile\` (AGPL → MPL-2.0)"
               CHANGED=true
             fi
           done

.gitignore

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

.machine_readable/compliance/reuse/dep5

@@ -52,3 +52,10 @@ License: MPL-2.0
 Files: cliff.toml
 Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}>
 License: MPL-2.0
+
+# Documentation prose is CC-BY-SA-4.0 (code/config is MPL-2.0).
+# Last-match-wins in the Debian copyright format, so this overrides the
+# `Files: *` default above for prose docs.
+Files: *.adoc *.md docs/* docs/**/*
+Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}>
+License: CC-BY-SA-4.0

.machine_readable/contractiles/must/Mustfile.a2ml

@@ -47,7 +47,7 @@ These are hard requirements — CI fails if any check fails.
 - severity: warning
 
 ### no-agpl
-- description: No AGPL-3.0 references (replaced by PMPL)
+- description: No AGPL-3.0 references (replaced by MPL-2.0)
 - run: "! grep -r 'AGPL-3.0' .gitignore .gitattributes .editorconfig 2>/dev/null | head -1 | grep -q ."
 - severity: critical
 

.machine_readable/contractiles/trust/Trustfile.a2ml

@@ -34,7 +34,7 @@ is traceable.
 
 ### license-content
 - description: LICENSE contains expected identifier
-- run: grep -q 'PMPL\|MPL\|MIT\|Apache\|LGPL' LICENSE
+- run: grep -q 'MPL-2.0' LICENSE
 - severity: warning
 
 ### signed-by-ci

Cargo.toml

@@ -5,7 +5,7 @@ version = "0.1.0"
 edition = "2024"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
 description = "Enforce single-use linear type semantics on resources in existing code via Ephapax"
-license-file = "LICENSE"
+license = "MPL-2.0"
 repository = "https://github.com/hyperpolymath/ephapaxiser"
 keywords = ["ephapax", "linear-types", "resource-safety", "code-generation"]
 categories = ["command-line-utilities", "development-tools"]

LICENSE

@@ -1,3 +1,5 @@
+SPDX-License-Identifier: MPL-2.0
+
 Mozilla Public License Version 2.0
 ==================================
 

contractiles/trust/Trustfile.a2ml

@@ -16,7 +16,7 @@ Maximal trust by default — LLM may read, build, test, lint, format.
 
 ### license-content
 - description: LICENSE contains expected SPDX identifier
-- run: grep -q 'SPDX\|License\|MIT\|Apache\|PMPL\|MPL' LICENSE
+- run: grep -q 'SPDX\|MPL-2.0' LICENSE
 - severity: critical
 
 ### no-secrets-committed

docs/RSR_OUTLINE.adoc

@@ -1,6 +1,6 @@
 = RSR Template Repository
 
-image:[Palimpsest-MPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"] image:[Palimpsest,link="https://github.com/hyperpolymath/palimpsest-license"]
+image:https://img.shields.io/badge/license-MPL--2.0-blue[MPL-2.0,link="LICENSES/MPL-2.0.txt"] image:https://img.shields.io/badge/docs-CC--BY--SA--4.0-blue[CC-BY-SA-4.0,link="LICENSES/CC-BY-SA-4.0.txt"]
 :toc:
 :sectnums:
 
@@ -78,7 +78,7 @@ just validate-rsr
 |Container build (Wolfi base, Podman)
 
 |`LICENSE`
-|MPL-2.0 (Palimpsest MPL)
+|MPL-2.0 (code) / CC-BY-SA-4.0 (docs)
 
 |`EXHIBIT-A-ETHICAL-USE.txt`
 |Ethical use guidelines (LICENSE Exhibit A)

docs/STATE-VISUALIZER.adoc

@@ -87,7 +87,7 @@ CONTAINER ECOSYSTEM (Phase 2)
 
 REPO INFRASTRUCTURE
   .machine_readable/                ██████████ 100%    STATE/META/ECOSYSTEM active
-  Governance & License              ██████████ 100%    PMPL & Ethical use verified
+  Governance & License              ██████████ 100%    MPL-2.0 & Ethical use verified
   Development Shells (Nix/Guix)     ██████████ 100%    Reproducible env stable
 
 ─────────────────────────────────────────────────────────────────────────────

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

@@ -17,6 +17,8 @@ module Ephapaxiser.ABI.Layout
 import Ephapaxiser.ABI.Types
 import Data.Vect
 import Data.So
+import Data.Nat
+import Decidable.Equality
 
 %default total
 
@@ -30,24 +32,42 @@ 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 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
+||| from Data.Nat 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`).
+||| (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
@@ -79,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
@@ -88,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)
 
 --------------------------------------------------------------------------------
 -- Resource Tracker Layout
@@ -131,11 +154,8 @@ resourceTrackerLayout =
     ]
     24  -- Total size: 24 bytes
     8   -- Alignment: 8 bytes
-
-||| Proof that the resource tracker layout is C-ABI compliant
-public export
-resourceTrackerCABI : CABICompliant resourceTrackerLayout
-resourceTrackerCABI = CABIOk resourceTrackerLayout ?resourceTrackerFieldsAligned
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 3 Refl}  -- 24 = 3 * 8
 
 ||| Proof that the resource tracker layout is valid for all platforms
 public export
@@ -172,6 +192,8 @@ consumeProofLayout =
     ]
     24
     8
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 3 Refl}  -- 24 = 3 * 8
 
 --------------------------------------------------------------------------------
 -- Platform-Specific Layouts
@@ -202,25 +224,45 @@ 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"
+
+||| Verify that all ephapaxiser layouts are C-ABI compliant. Fails (Left) if
+||| any concrete layout is misaligned, rather than asserting it.
+public export
+verifyAllLayouts : Either String ()
+verifyAllLayouts = do
+  _ <- checkCABI resourceTrackerLayout
+  _ <- checkCABI consumeProofLayout
+  Right ()
 
 --------------------------------------------------------------------------------
 -- Offset Calculation
 --------------------------------------------------------------------------------
 
-||| Calculate field offset with proof of correctness
+||| Look up a field's offset 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

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

@@ -0,0 +1,90 @@
+-- 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 ephapaxiser 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 lifecycle transition
+||| mis-stated, 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 Ephapaxiser.ABI.Proofs
+
+import Ephapaxiser.ABI.Types
+import Ephapaxiser.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 ResourceTracker layout divides its alignment:
+||| 0|8, 8|4, 12|4, 16|4, 20|4.
+export
+resourceTrackerCompliant : CABICompliant Layout.resourceTrackerLayout
+resourceTrackerCompliant =
+  CABIOk resourceTrackerLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 4 Refl)
+    (ConsField _ _ (DivideBy 5 Refl)
+     NoFields)))))
+
+||| Every field offset in the ConsumeProof layout divides its alignment:
+||| 0|8, 8|4, 12|4, 16|4, 20|4.
+export
+consumeProofCompliant : CABICompliant Layout.consumeProofLayout
+consumeProofCompliant =
+  CABIOk consumeProofLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 4 Refl)
+    (ConsField _ _ (DivideBy 5 Refl)
+     NoFields)))))
+
+--------------------------------------------------------------------------------
+-- Result-code round-trip: the encoding the Zig FFI depends on.
+--------------------------------------------------------------------------------
+
+export
+okIsZero : resultToInt Ok = 0
+okIsZero = Refl
+
+||| The double-free error code is pinned to 7, as the Zig FFI bridge expects.
+export
+doubleFreeIsSeven : resultToInt DoubleFree = 7
+doubleFreeIsSeven = Refl
+
+--------------------------------------------------------------------------------
+-- Linearity state machine: only the two legal transitions exist.
+--------------------------------------------------------------------------------
+
+||| Once a resource is consumed, no further transition out of it is valid —
+||| this is the formal use-after-free guard. `consumedIsFinal` discharges the
+||| absurd case for any successor state, so the proof is genuine (the type
+||| `ValidTransition Consumed next` is uninhabited).
+export
+consumedHasNoSuccessor : (next : ResourceLifecycle) ->
+                         ValidTransition Consumed next -> Void
+consumedHasNoSuccessor next = consumedIsFinal
+
+||| Using a freshly-acquired resource records exactly-once usage: the usage
+||| index of the returned resource is `UsedOnce`, witnessed structurally by
+||| the lifecycle transition `Acquired -> InUse`.
+export
+useProducesAcquiredToInUse :
+  (r : LinearResource Acquired Unused) ->
+  snd (useResource r) = AcquiredToInUse
+useProducesAcquiredToInUse (MkLinearResource _) = Refl