ABI Layer 5: end-to-end soundness capstone certificate (#76)

* feat(abi): prove Conformant scaffold property (Layer 2 Semantics)

Add Iseriser.ABI.Semantics proving the headline domain property: a
generated -iser scaffold is Conformant exactly when all five required
components (Manifest, Idris2 ABI, Zig FFI, Codegen, Rust CLI) are
present. Conformant is built from genuine Data.List.Elem membership
obligations with no catch-all constructor, so a scaffold missing any
component has no witness.

Includes a sound+complete decConformant : (s) -> Dec (Conformant s),
a soundness fact certifyConformantSound, a positive control
(completeIsConformant via explicit Elem positions), and a negative
control (ffiMissingNotConformant : Not (Conformant ffiMissing)).
Non-vacuity confirmed: a deliberately-false Has Ffi witness for the
FFI-missing scaffold is rejected by idris2.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

* abi: add Layer-3 Invariants (generation soundness + conformance closure)

Add Iseriser.ABI.Invariants over the existing Layer-2 Semantics model
(Component/Scaffold/Has/Conformant). Two new, deeper, distinct theorems:

  1. Generation soundness (correct-by-construction): genScaffold provably
     emits (s ** Conformant s) for any LanguageModel, with a corollary
     tying it back to the Layer-2 certifier (conformantCertifies).
  2. Upward-closure / monotonicity: conformantStable proves Conformance is
     preserved under extension, via a genuine Elem-weakening lemma
     (elemAppendRight) — an algebraic closure law, not the Layer-2 decision.

Includes a sound+complete Dec (decExtendConformant), a positive control
(extendedGeneratedConformant) and a non-vacuity negative control
(extendedBrokenNotConformant : Not ...). Builds clean with zero warnings;
adversarial false proof rejected. No believe_me/postulate/assert_total.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

* abi: seal ABI<->FFI seam with Layer-4 soundness proof (FfiSeam)

Add Iseriser.ABI.FfiSeam proving the resultToInt encoding is sound:
- intToResult decoder + resultRoundTrip (lossless/faithful encoding)
- resultToIntInjective derived from round-trip (distinct outcomes never
  collide on the wire)
- positive controls (concrete decodes by Refl) and a machine-checked
  non-vacuity control (resultToInt Ok /= resultToInt Error)

Genuine total proof: no believe_me/postulate/assert_total/etc. Registered
in iseriser-abi.ipkg; package builds clean with zero warnings.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

* abi(iseriser): add Layer-5 capstone ABI soundness certificate

Assemble the existing Layer-2/3/4 ABI proofs into one inhabited value,
Iseriser.ABI.Capstone.abiContractDischarged : ABISound, with fields:
  - flagship     : Conformant Semantics.completeScaffold
                   (reuses Semantics.completeIsConformant)
  - invariant    : Conformant (extend [Manifest] generatedScaffold)
                   (reuses Invariants.extendedGeneratedConformant)
  - ffiInjective : resultToInt injectivity
                   (reuses FfiSeam.resultToIntInjective)

Pure composition of already-exported witnesses: if any prior layer were
unsound the capstone would not typecheck. Adversarial check confirms a
wrong-type witness in the flagship slot is rejected. %default total, SPDX,
zero warnings. ipkg updated (Capstone listed last).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

---------

Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

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

@@ -0,0 +1,70 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Layer-5 CAPSTONE: the end-to-end ABI SOUNDNESS CERTIFICATE for iseriser.
+|||
+||| This module proves NO new domain theorem. Its sole job is to ASSEMBLE the
+||| already-discharged proof layers into ONE inhabited value, so that the full
+||| ABI contract is shown to hold *together*. The certificate ties the chain:
+|||
+|||   manifest/doctrine model  (Types: Component, Scaffold, Result)
+|||     -> Layer-2 flagship     (Semantics.completeIsConformant — the canonical
+|||                              positive control: the complete five-component
+|||                              scaffold IS Conformant)
+|||     -> Layer-3 invariant    (Invariants.extendedGeneratedConformant — the
+|||                              upward-closure / monotonicity witness: a
+|||                              generated-then-extended scaffold stays Conformant)
+|||     -> Layer-4 FFI seam     (FfiSeam.resultToIntInjective — distinct ABI
+|||                              outcomes never collide on the C wire)
+|||
+||| into a single end-to-end soundness statement. `abiContractDischarged` is the
+||| capstone value: it is constructed ENTIRELY from the existing exported
+||| witnesses/theorems of the prior layers. If ANY prior layer were unsound,
+||| this value would not typecheck. There is no fresh proof obligation here —
+||| only genuine composition.
+
+module Iseriser.ABI.Capstone
+
+import Iseriser.ABI.Types
+import Iseriser.ABI.Semantics
+import Iseriser.ABI.Invariants
+import Iseriser.ABI.FfiSeam
+
+%default total
+
+--------------------------------------------------------------------------------
+-- The capstone certificate
+--------------------------------------------------------------------------------
+
+||| `ABISound` bundles the KEY proven facts of the iseriser ABI into one record.
+||| Each field is the TYPE of an already-proven theorem from a prior layer; the
+||| only way to inhabit the record is to supply those real witnesses.
+|||
+|||   * `flagship`  : the Layer-2 flagship property holds on the canonical
+|||                   positive-control instance (`Semantics.completeScaffold` is
+|||                   `Conformant`).
+|||   * `invariant` : the Layer-3 deeper invariant holds — conformance is
+|||                   upward-closed under extension, witnessed on the generated
+|||                   scaffold extended by one component.
+|||   * `ffiInjective` : the Layer-4 FFI-seam guarantee — `resultToInt` is
+|||                   injective, so distinct ABI outcomes never collide on the
+|||                   wire. Stored as the full injectivity statement.
+public export
+record ABISound where
+  constructor MkABISound
+  flagship     : Conformant Semantics.completeScaffold
+  invariant    : Conformant (extend [Manifest] Invariants.generatedScaffold)
+  ffiInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b
+
+||| THE CAPSTONE. A single inhabited value assembled purely from the existing
+||| exported witnesses of Layers 2-4. Its mere existence certifies that the
+||| flagship property, the deeper invariant, and the FFI-seam injectivity are
+||| ALL simultaneously discharged for this ABI — manifest model -> ABI proofs
+||| -> FFI seam, sealed end to end.
+public export
+abiContractDischarged : ABISound
+abiContractDischarged =
+  MkABISound
+    completeIsConformant            -- Layer-2 flagship positive control
+    extendedGeneratedConformant     -- Layer-3 upward-closure invariant witness
+    resultToIntInjective            -- Layer-4 FFI-seam injectivity

src/interface/abi/iseriser-abi.ipkg

@@ -12,3 +12,4 @@ modules = Iseriser.ABI.Types
         , Iseriser.ABI.Semantics
         , Iseriser.ABI.Invariants
         , Iseriser.ABI.FfiSeam
+        , Iseriser.ABI.Capstone