From 33a68bcf10c5d417df5099b33f1d299ba8c0a5de Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 19:31:50 +0000 Subject: [PATCH] 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 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- src/interface/abi/Iseriser/ABI/Semantics.idr | 203 +++++++++++++++++++ src/interface/abi/iseriser-abi.ipkg | 1 + 2 files changed, 204 insertions(+) create mode 100644 src/interface/abi/Iseriser/ABI/Semantics.idr diff --git a/src/interface/abi/Iseriser/ABI/Semantics.idr b/src/interface/abi/Iseriser/ABI/Semantics.idr new file mode 100644 index 0000000..b693dc2 --- /dev/null +++ b/src/interface/abi/Iseriser/ABI/Semantics.idr @@ -0,0 +1,203 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Flagship semantic proof for iseriser (Layer 2 ABI). +||| +||| Headline: "Meta-framework that generates new -iser projects." +||| +||| A generated -iser scaffold is faithful only when ALL of the five +||| architectural components named in the project doctrine are present: +||| +||| Manifest · Idris2 ABI · Zig FFI · Codegen · Rust CLI +||| +||| We model a scaffold as the set of components it actually produced, and +||| prove a `Conformant` proposition that holds EXACTLY when every required +||| component is present. The bad case (a scaffold missing any component) +||| has no `Conformant` witness — this is enforced structurally, not by an +||| opaque boolean. The decision procedure is sound AND complete, and the +||| negative control shows a scaffold missing the FFI is provably not +||| Conformant. + +module Iseriser.ABI.Semantics + +import Iseriser.ABI.Types +import Data.List.Elem +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- Faithful domain model +-------------------------------------------------------------------------------- + +||| The five architectural components every generated -iser must contain. +||| These mirror the doctrine in .claude/CLAUDE.md: +||| Manifest, Idris2 ABI, Zig FFI, Codegen, Rust CLI. +public export +data Component : Type where + Manifest : Component -- .toml: user describes WHAT they want + Abi : Component -- src/interface/abi: Idris2 formal proofs + Ffi : Component -- ffi/zig: C-ABI bridge + Codegen : Component -- src/codegen: target-language wrapper generation + Cli : Component -- src/main.rs: Rust orchestrator + +||| A generated scaffold is the (finite) list of components it produced. +public export +record Scaffold where + constructor MkScaffold + components : List Component + +-------------------------------------------------------------------------------- +-- Decidable equality on Component (needed for membership) +-------------------------------------------------------------------------------- + +public export +DecEq Component where + decEq Manifest Manifest = Yes Refl + decEq Abi Abi = Yes Refl + decEq Ffi Ffi = Yes Refl + decEq Codegen Codegen = Yes Refl + decEq Cli Cli = Yes Refl + + decEq Manifest Abi = No (\case Refl impossible) + decEq Manifest Ffi = No (\case Refl impossible) + decEq Manifest Codegen = No (\case Refl impossible) + decEq Manifest Cli = No (\case Refl impossible) + decEq Abi Manifest = No (\case Refl impossible) + decEq Abi Ffi = No (\case Refl impossible) + decEq Abi Codegen = No (\case Refl impossible) + decEq Abi Cli = No (\case Refl impossible) + decEq Ffi Manifest = No (\case Refl impossible) + decEq Ffi Abi = No (\case Refl impossible) + decEq Ffi Codegen = No (\case Refl impossible) + decEq Ffi Cli = No (\case Refl impossible) + decEq Codegen Manifest = No (\case Refl impossible) + decEq Codegen Abi = No (\case Refl impossible) + decEq Codegen Ffi = No (\case Refl impossible) + decEq Codegen Cli = No (\case Refl impossible) + decEq Cli Manifest = No (\case Refl impossible) + decEq Cli Abi = No (\case Refl impossible) + decEq Cli Ffi = No (\case Refl impossible) + decEq Cli Codegen = No (\case Refl impossible) + +-------------------------------------------------------------------------------- +-- The headline property: Conformant +-------------------------------------------------------------------------------- + +||| `Has c s` is a genuine membership obligation: component `c` is in the +||| scaffold's produced component list. There is NO way to construct it for +||| an absent component (it reduces to `Data.List.Elem`, which has no +||| inhabitant for the empty list). +public export +Has : Component -> Scaffold -> Type +Has c s = Elem c (components s) + +||| A scaffold is `Conformant` EXACTLY when each of the five required +||| components is present. Each field is a real membership proof; the +||| proposition is uninhabited the moment any component is missing. +||| (No catch-all constructor: this cannot be faked.) +public export +data Conformant : Scaffold -> Type where + MkConformant : + Has Manifest s + -> Has Abi s + -> Has Ffi s + -> Has Codegen s + -> Has Cli s + -> Conformant s + +-------------------------------------------------------------------------------- +-- Sound + complete decision procedure +-------------------------------------------------------------------------------- + +||| Decide membership of a component in a scaffold. +decHas : (c : Component) -> (s : Scaffold) -> Dec (Has c s) +decHas c s = isElem c (components s) + +||| Decide whether a scaffold is Conformant. Returns a REAL proof when all +||| five components are present, and a refutation when any is missing. The +||| refutation projects the relevant field out of a hypothetical witness, so +||| completeness is machine-checked (not asserted). +public export +decConformant : (s : Scaffold) -> Dec (Conformant s) +decConformant s = + case decHas Manifest s of + No nm => No (\(MkConformant m _ _ _ _) => nm m) + Yes m => case decHas Abi s of + No na => No (\(MkConformant _ a _ _ _) => na a) + Yes a => case decHas Ffi s of + No nf => No (\(MkConformant _ _ f _ _) => nf f) + Yes f => case decHas Codegen s of + No ng => No (\(MkConformant _ _ _ g _) => ng g) + Yes g => case decHas Cli s of + No nc => No (\(MkConformant _ _ _ _ c) => nc c) + Yes c => Yes (MkConformant m a f g c) + +-------------------------------------------------------------------------------- +-- Certifier + soundness fact +-------------------------------------------------------------------------------- + +||| Map a scaffold to a `ProofStatus`-shaped verdict reusing the ABI's +||| `Result` codes: `Ok` means Conformant, `InvalidLanguage` means a +||| required component is missing. +public export +certifyConformant : (s : Scaffold) -> Result +certifyConformant s = + case decConformant s of + Yes _ => Ok + No _ => InvalidLanguage + +||| Soundness of the certifier: if it returns `Ok`, a genuine `Conformant` +||| witness exists. Proven by case-analysis on the SAME decision the +||| certifier uses; the `No` branch is impossible because `Ok = InvalidLanguage` +||| is absurd. +public export +certifyConformantSound : + (s : Scaffold) + -> certifyConformant s = Ok + -> Conformant s +certifyConformantSound s prf with (decConformant s) + certifyConformantSound s prf | Yes ok = ok + certifyConformantSound s Refl | No _ impossible + +-------------------------------------------------------------------------------- +-- Positive control: a complete scaffold IS Conformant +-------------------------------------------------------------------------------- + +||| A faithfully complete scaffold — all five components, in canonical order. +public export +completeScaffold : Scaffold +completeScaffold = MkScaffold [Manifest, Abi, Ffi, Codegen, Cli] + +||| Explicit witness that the complete scaffold is Conformant. Each `Has` +||| proof is a concrete `Elem` position into the literal list above, so this +||| type-checks by reduction with no appeal to the decision procedure. +public export +completeIsConformant : Conformant Semantics.completeScaffold +completeIsConformant = + MkConformant + Here -- Manifest at position 0 + (There Here) -- Abi at position 1 + (There (There Here)) -- Ffi at position 2 + (There (There (There Here))) -- Codegen at position 3 + (There (There (There (There Here)))) -- Cli at position 4 + +-------------------------------------------------------------------------------- +-- Negative control: a scaffold missing the FFI is NOT Conformant +-------------------------------------------------------------------------------- + +||| A scaffold that produced everything EXCEPT the Zig FFI bridge. +public export +ffiMissingScaffold : Scaffold +ffiMissingScaffold = MkScaffold [Manifest, Abi, Codegen, Cli] + +||| Machine-checked refutation: with no `Ffi` component, no `Conformant` +||| witness can exist. We pull the `Has Ffi` field out of any hypothetical +||| witness and discharge it — `Ffi` is not among the four present +||| components, so every membership position is impossible. +public export +ffiMissingNotConformant : Not (Conformant Semantics.ffiMissingScaffold) +ffiMissingNotConformant (MkConformant _ _ f _ _) = noFfi f + where + noFfi : Not (Elem Ffi [Manifest, Abi, Codegen, Cli]) + noFfi (There (There (There (There prf)))) impossible diff --git a/src/interface/abi/iseriser-abi.ipkg b/src/interface/abi/iseriser-abi.ipkg index 4304c93..30954b2 100644 --- a/src/interface/abi/iseriser-abi.ipkg +++ b/src/interface/abi/iseriser-abi.ipkg @@ -9,3 +9,4 @@ modules = Iseriser.ABI.Types , Iseriser.ABI.Layout , Iseriser.ABI.Foreign , Iseriser.ABI.Proofs + , Iseriser.ABI.Semantics