iseriser: make Phase 0 ABI proofs genuinely compile and verify

.gitignore

@@ -16,6 +16,11 @@ Thumbs.db
 /_build/
 /build/
 /dist/
+
+# Idris2 proof build artifacts (any nested build/ dir + TTC output)
+**/build/
+*.ttc
+*.ttm
 /out/
 
 # Dependencies

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 = "Meta-framework that generates new -iser projects from a target language interop description"
-license-file = "LICENSE"
+license = "MPL-2.0"
 repository = "https://github.com/hyperpolymath/iseriser"
 keywords = ["meta-framework", "code-generation", "language-interop", "scaffolding"]
 categories = ["command-line-utilities", "development-tools"]

Justfile

@@ -14,6 +14,11 @@ build:
 test:
     cargo test
 
+# Type-check the Idris2 ABI formal proofs (requires idris2 >= 0.7.0)
+proofs:
+    cd src/interface/abi && idris2 --build iseriser-abi.ipkg
+    @echo "Idris2 ABI proofs type-check cleanly"
+
 # Run clippy lints
 lint:
     cargo clippy -- -D warnings

LICENSE

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

src/interface/abi/Iseriser/ABI/Layout.idr

@@ -0,0 +1,215 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Memory Layout Proofs for Iseriser
+
+module Iseriser.ABI.Layout
+
+import Iseriser.ABI.Types
+import Data.Vect
+import Data.So
+import Data.Nat
+import Decidable.Equality
+
+%default total
+
+public export
+paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
+paddingFor offset alignment =
+  if offset `mod` alignment == 0
+    then 0
+    else minus alignment (offset `mod` alignment)
+
+public export
+alignUp : (size : Nat) -> (alignment : Nat) -> Nat
+alignUp size alignment =
+  size + paddingFor size alignment
+
+||| 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
+
+||| 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
+alignUpDivides : (size : Nat) -> (align : Nat) ->
+                 Maybe (Divides align (alignUp size align))
+alignUpDivides size align = decDivides align (alignUp size align)
+
+public export
+record Field where
+  constructor MkField
+  name : String
+  offset : Nat
+  size : Nat
+  alignment : Nat
+
+public export
+nextFieldOffset : Field -> Nat
+nextFieldOffset f = alignUp (f.offset + f.size) f.alignment
+
+public export
+record StructLayout where
+  constructor MkStructLayout
+  fields : Vect n Field
+  totalSize : Nat
+  alignment : Nat
+  {auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))}
+  {auto 0 aligned : Divides alignment totalSize}
+
+public export
+calcStructSize : Vect k Field -> Nat -> Nat
+calcStructSize [] align = 0
+calcStructSize (f :: fs) align =
+  let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
+      lastSize = foldr (\field, _ => field.size) f.size fs
+   in alignUp (lastOffset + lastSize) align
+
+||| C-compatible layout for the language model data passed through FFI.
+public export
+languageModelDataLayout : StructLayout
+languageModelDataLayout =
+  MkStructLayout
+    [ MkField "name_ptr" 0 8 8
+    , MkField "name_len" 8 4 4
+    , MkField "num_features" 12 4 4
+    , MkField "features_ptr" 16 8 8
+    , MkField "target" 24 4 4
+    , MkField "padding" 28 4 4
+    ]
+    32
+    8
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 4 Refl}
+
+||| C-compatible layout for template data passed to the expansion engine.
+public export
+templateDataLayout : StructLayout
+templateDataLayout =
+  MkStructLayout
+    [ MkField "template_ptr" 0 8 8
+    , MkField "template_len" 8 4 4
+    , MkField "padding1" 12 4 4
+    , MkField "output_ptr" 16 8 8
+    , MkField "output_len" 24 4 4
+    , MkField "is_lang_spec" 28 4 4
+    ]
+    32
+    8
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 4 Refl}
+
+||| C-compatible layout for the generation context handle.
+public export
+generationContextLayout : StructLayout
+generationContextLayout =
+  MkStructLayout
+    [ MkField "model_ptr" 0 8 8
+    , MkField "templates_ptr" 8 8 8
+    , MkField "num_templates" 16 4 4
+    , MkField "artifacts_count" 20 4 4
+    , MkField "output_dir_ptr" 24 8 8
+    , MkField "output_dir_len" 32 4 4
+    , MkField "initialized" 36 4 4
+    , MkField "error_code" 40 4 4
+    , MkField "padding" 44 4 4
+    ]
+    48
+    8
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 6 Refl}
+
+||| Proof that every field offset in a layout is correctly aligned.
+public export
+data FieldsAligned : Vect k Field -> Type where
+  NoFields : FieldsAligned []
+  ConsField :
+    (f : Field) ->
+    (rest : Vect k Field) ->
+    Divides f.alignment f.offset ->
+    FieldsAligned rest ->
+    FieldsAligned (f :: rest)
+
+||| Decide field alignment for every field, building a real `FieldsAligned`
+||| witness from per-field divisibility proofs.
+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)
+
+||| Proof that a struct layout follows C ABI alignment rules.
+public export
+data CABICompliant : StructLayout -> Type where
+  CABIOk :
+    (layout : StructLayout) ->
+    FieldsAligned layout.fields ->
+    CABICompliant layout
+
+||| 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 =
+  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 iseriser layouts are C-ABI compliant. This now fails
+||| (Left) if any concrete layout is misaligned, rather than asserting it.
+public export
+verifyAllLayouts : Either String ()
+verifyAllLayouts = do
+  _ <- checkCABI languageModelDataLayout
+  _ <- checkCABI templateDataLayout
+  _ <- checkCABI generationContextLayout
+  Right ()
+
+||| All 64-bit platforms (Linux, Windows, MacOS, BSD) use 8-byte pointers and
+||| 4-byte ints, so the LanguageModelData layout is identical across them.
+public export
+verifyLanguageModelPortability : Either String ()
+verifyLanguageModelPortability = Right ()
+
+||| Look up a field's offset by name in a layout.
+public export
+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)
+    Nothing => Nothing
+
+||| 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) ->
+                 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/Iseriser/ABI/Proofs.idr

@@ -0,0 +1,101 @@
+-- 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 iseriser 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 Iseriser.ABI.Proofs
+
+import Iseriser.ABI.Types
+import Iseriser.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 LanguageModelData layout divides its alignment:
+||| 0|8, 8|4, 12|4, 16|8, 24|4, 28|4.
+export
+languageModelDataCompliant : CABICompliant Layout.languageModelDataLayout
+languageModelDataCompliant =
+  CABIOk languageModelDataLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 6 Refl)
+    (ConsField _ _ (DivideBy 7 Refl)
+     NoFields))))))
+
+||| Every field offset in the TemplateData layout is aligned:
+||| 0|8, 8|4, 12|4, 16|8, 24|4, 28|4.
+export
+templateDataCompliant : CABICompliant Layout.templateDataLayout
+templateDataCompliant =
+  CABIOk templateDataLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 6 Refl)
+    (ConsField _ _ (DivideBy 7 Refl)
+     NoFields))))))
+
+||| Every field offset in the GenerationContext layout is aligned:
+||| 0|8, 8|8, 16|4, 20|4, 24|8, 32|4, 36|4, 40|4, 44|4.
+export
+generationContextCompliant : CABICompliant Layout.generationContextLayout
+generationContextCompliant =
+  CABIOk generationContextLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 4 Refl)
+    (ConsField _ _ (DivideBy 5 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 8 Refl)
+    (ConsField _ _ (DivideBy 9 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
+nullPointerIsFive : resultToInt NullPointer = 5
+nullPointerIsFive = Refl
+
+--------------------------------------------------------------------------------
+-- Generation completeness: the full required set is accepted; a short set isn't.
+--------------------------------------------------------------------------------
+
+||| The complete set of seven categories is recognised as complete.
+export
+fullSetComplete : So (allCategoriesPresent Types.requiredCategories)
+fullSetComplete = Oh
+
+||| A set missing RSRGovernance is correctly rejected as incomplete.
+export
+shortSetIncomplete : So (not (allCategoriesPresent
+  [CargoToml, RustSource, Idris2ABI, ZigFFI, CIWorkflows, Documentation]))
+shortSetIncomplete = Oh