From 2e3e47cba8685a16af3fd73ec670e542611c1571 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 20:14:57 +0000 Subject: [PATCH 1/2] iseriser: codegen emits verified, compiling Idris2 ABI (P2) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The scaffold generator still emitted the old flat, never-compiled ABI template: files at `src/interface/abi/{Types,Layout,Foreign}.idr` with a namespace they didn't match, a `Layout.idr` whose `modNatNZ ... == 0` proof does not reduce at the type level, no `Proofs.idr`, and no `.ipkg`. Every newly-generated -iser therefore started with a broken ABI — exactly the bug a prior session hand-fixed across the family. Rewrite the Idris2 ABI generators to emit the verified reference pattern, proven to compile clean under Idris2 0.7.0 (zero warnings, no believe_me/postulate/holes): - Nested modules at `src/interface/abi//ABI/{Types,Layout,Foreign, Proofs}.idr` so each file's path matches its namespace, plus `src/interface/abi/-abi.ipkg` (sourcedir=".", lists all four). - Types: `Result` with a complete `DecEq` (explicit off-diagonals, not `No absurd`), a non-null `Handle` built via `choose`, and a primitive enum with a tag-based `Eq` that is warning-free for any arity. - Layout: real `Divides`/`StructLayout`/`FieldsAligned` machinery and one concrete, provably C-ABI-compliant context layout. - Proofs: a non-vacuous `CABICompliant` theorem (each offset pinned by `DivideBy k Refl`, qualified layout name so it doesn't auto-bind), the result-code round-trip, and a Nat-level negative control. Verified: perturbing a field offset makes the proof fail to typecheck. Tests: assert the generated tree is self-consistent (every ipkg module present at its namespace path, no leftover template tokens, old flat path gone) and add an end-to-end test that runs `idris2 --build` on the generated ABI when the toolchain is present (no-op otherwise, so CI without idris2 stays green). Update the integration tests for the new paths and the real proof module. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH --- src/codegen/scaffold.rs | 707 +++++++++++++++++++++++++++++++------- tests/integration_test.rs | 21 +- 2 files changed, 598 insertions(+), 130 deletions(-) diff --git a/src/codegen/scaffold.rs b/src/codegen/scaffold.rs index ba3e478..db2f140 100644 --- a/src/codegen/scaffold.rs +++ b/src/codegen/scaffold.rs @@ -41,10 +41,12 @@ pub fn scaffold_repo(manifest: &Manifest, output_dir: &Path) -> ScaffoldResult { files.push(generate_codegen_mod_rs(&model)); files.push(generate_abi_mod_rs(&model)); - // Idris2 ABI + // Idris2 ABI (verified nested layout: /ABI/*.idr + -abi.ipkg) files.push(generate_idris2_types(&model)); files.push(generate_idris2_layout(&model)); files.push(generate_idris2_foreign(&model)); + files.push(generate_idris2_proofs(&model)); + files.push(generate_idris2_ipkg(&model)); // Zig FFI files.push(generate_zig_build(&model, &iser_name)); @@ -449,168 +451,122 @@ fn generate_abi_mod_rs(model: &LanguageModel) -> GeneratedFile { // File generators — Idris2 ABI // --------------------------------------------------------------------------- -/// Generate `src/interface/abi/Types.idr` — formal ABI type definitions. +/// Generate `src/interface/abi//ABI/Types.idr` — formal ABI type +/// definitions. Emits the verified-reference nested-module form that compiles +/// clean under Idris2 0.7.0 (see `verified_abi_*` templates below). fn generate_idris2_types(model: &LanguageModel) -> GeneratedFile { let module_prefix = idris2_module_name(model); - let primitives_data: String = if model.key_primitives.is_empty() { - " ||| No key primitives declared\n NoPrimitives : Primitive".to_string() + let iser_name = model.iser_name(); + + // Primitive constructors, one per key primitive (or a single placeholder). + let prim_ctors: String = if model.key_primitives.is_empty() { + " ||| No key primitives declared.\n NoPrimitives : Primitive".to_string() } else { model .key_primitives .iter() .map(|p| { - let constructor = to_idris_constructor(p); - format!(" ||| The `{}` primitive\n {} : Primitive", p, constructor) + let ctor = to_idris_constructor(p); + format!(" ||| The `{}` primitive.\n {} : Primitive", p, ctor) }) .collect::>() .join("\n") }; - let calling_conv = model.calling_convention(); - let deep_proofs = if model.needs_deep_abi_proofs() { - r#" -||| This language has a rich type system; deep ABI proofs are generated. -public export -data DeepProof : Type where - TypeSafe : DeepProof"# + // `primCode` clauses give each primitive a stable numeric tag. Comparing by + // tag yields a total, warning-free `Eq` for any arity (a direct structural + // `==` would need a catch-all that Idris flags as redundant for one ctor). + let prim_codes: String = if model.key_primitives.is_empty() { + "primCode NoPrimitives = 0".to_string() } else { - "" + model + .key_primitives + .iter() + .enumerate() + .map(|(i, p)| format!("primCode {} = {}", to_idris_constructor(p), i)) + .collect::>() + .join("\n") }; - let content = format!( - r#"-- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| ABI Type Definitions for {iser_name} -||| -||| Generated by iseriser for {lang_name} interop. -||| Calling convention: {calling_conv} - -module {module_prefix}.ABI.Types - -import Data.Bits -import Data.So -import Data.Vect - -%default total - --------------------------------------------------------------------------------- --- Primitives --------------------------------------------------------------------------------- - -||| Key primitives for {lang_name} FFI. -public export -data Primitive : Type where -{primitives_data} - --------------------------------------------------------------------------------- --- Result Codes --------------------------------------------------------------------------------- - -||| Result codes for FFI operations -public export -data Result : Type where - Ok : Result - Error : Result - InvalidInput : Result - NullPointer : Result + let content = VERIFIED_ABI_TYPES + .replace("__MODULE__", &module_prefix) + .replace("__ISER__", &iser_name) + .replace("__LANG__", &model.name) + .replace("__CONV__", model.calling_convention()) + .replace("__PRIM_CTORS__", &prim_ctors) + .replace("__PRIM_CODES__", &prim_codes); -||| Convert Result to C integer -public export -resultToInt : Result -> Bits32 -resultToInt Ok = 0 -resultToInt Error = 1 -resultToInt InvalidInput = 2 -resultToInt NullPointer = 3 -{deep_proofs} -"#, - iser_name = model.iser_name(), - lang_name = model.name, - calling_conv = calling_conv, - module_prefix = module_prefix, - primitives_data = primitives_data, - deep_proofs = deep_proofs, - ); GeneratedFile { - path: PathBuf::from("src/interface/abi/Types.idr"), + path: idris_abi_path(&module_prefix, "Types"), content, } } -/// Generate `src/interface/abi/Layout.idr` — memory layout verification. +/// Generate `src/interface/abi//ABI/Layout.idr` — memory-layout proofs. +/// Emits real `StructLayout` / `Divides` machinery and one concrete, provably +/// C-ABI-compliant context layout (the old `modNatNZ ... == 0` form did not +/// reduce at the type level and could not be discharged honestly). fn generate_idris2_layout(model: &LanguageModel) -> GeneratedFile { let module_prefix = idris2_module_name(model); - let content = format!( - r#"-- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| Memory Layout Verification for {iser_name} -||| Generated by iseriser. - -module {module_prefix}.ABI.Layout - -import {module_prefix}.ABI.Types -import Data.Bits - -%default total + let content = VERIFIED_ABI_LAYOUT + .replace("__MODULE__", &module_prefix) + .replace("__ISER__", &model.iser_name()); + GeneratedFile { + path: idris_abi_path(&module_prefix, "Layout"), + content, + } +} -||| Size of the context handle in bytes (8-byte aligned). -public export -contextSize : Nat -contextSize = 48 +/// Generate `src/interface/abi//ABI/Foreign.idr` — FFI declarations with +/// safe wrappers built on the non-null `Handle` and the `Result` decoder. +fn generate_idris2_foreign(model: &LanguageModel) -> GeneratedFile { + let module_prefix = idris2_module_name(model); + let content = VERIFIED_ABI_FOREIGN + .replace("__MODULE__", &module_prefix) + .replace("__ISER__", &model.iser_name()); + GeneratedFile { + path: idris_abi_path(&module_prefix, "Foreign"), + content, + } +} -||| Proof that context size is word-aligned. -public export -contextAligned : So (modNatNZ contextSize 8 SIsNonZero == 0) -contextAligned = Oh -"#, - iser_name = model.iser_name(), - module_prefix = module_prefix, - ); +/// Generate `src/interface/abi//ABI/Proofs.idr` — the machine-checked +/// theorems (C-ABI compliance, result-code round-trip, a negative control). +fn generate_idris2_proofs(model: &LanguageModel) -> GeneratedFile { + let module_prefix = idris2_module_name(model); + let content = VERIFIED_ABI_PROOFS + .replace("__MODULE__", &module_prefix) + .replace("__ISER__", &model.iser_name()); GeneratedFile { - path: PathBuf::from("src/interface/abi/Layout.idr"), + path: idris_abi_path(&module_prefix, "Proofs"), content, } } -/// Generate `src/interface/abi/Foreign.idr` — FFI function declarations. -fn generate_idris2_foreign(model: &LanguageModel) -> GeneratedFile { +/// Generate `src/interface/abi/-abi.ipkg` — the Idris2 package that +/// builds all four ABI modules. Build with `idris2 --build -abi.ipkg` +/// from `src/interface/abi/`. +fn generate_idris2_ipkg(model: &LanguageModel) -> GeneratedFile { let module_prefix = idris2_module_name(model); let iser_name = model.iser_name(); let content = format!( r#"-- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| Foreign Function Interface declarations for {iser_name} -||| Generated by iseriser. - -module {module_prefix}.ABI.Foreign - -import {module_prefix}.ABI.Types -import {module_prefix}.ABI.Layout +-- Idris2 package for the {iser_name} ABI formal proofs. +-- Build/check with: idris2 --build {iser_name}-abi.ipkg (from src/interface/abi/) +package {iser_name}-abi -%default total - -||| Initialise the {iser_name} engine. -export -%foreign "C:{iser_name}_init,lib{iser_name}" -{iser_name}_init : PrimIO Bits64 - -||| Free the {iser_name} context. -export -%foreign "C:{iser_name}_free,lib{iser_name}" -{iser_name}_free : Bits64 -> PrimIO () +sourcedir = "." -||| Get the library version string. -export -%foreign "C:{iser_name}_version,lib{iser_name}" -{iser_name}_version : PrimIO String +modules = {module_prefix}.ABI.Types + , {module_prefix}.ABI.Layout + , {module_prefix}.ABI.Foreign + , {module_prefix}.ABI.Proofs "#, iser_name = iser_name, module_prefix = module_prefix, ); GeneratedFile { - path: PathBuf::from("src/interface/abi/Foreign.idr"), + path: PathBuf::from(format!("src/interface/abi/{}-abi.ipkg", iser_name)), content, } } @@ -1128,6 +1084,386 @@ indent_size = 2 } } +// --------------------------------------------------------------------------- +// Verified Idris2 ABI templates +// --------------------------------------------------------------------------- +// +// These are the reference forms proven to compile clean under Idris2 0.7.0 +// (zero warnings, no `believe_me`/`postulate`/holes). Token `__MODULE__` is the +// module prefix (e.g. `Chapeliser`), `__ISER__` the repo name (e.g. +// `chapeliser`), `__LANG__` the source language, `__CONV__` the calling +// convention; `__PRIM_CTORS__` / `__PRIM_CODES__` are filled per manifest. +// Generated files live at `src/interface/abi/__MODULE__/ABI/*.idr` so the path +// matches the namespace, and are built via `__ISER__-abi.ipkg`. + +const VERIFIED_ABI_TYPES: &str = r#"-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| ABI Type Definitions for __ISER__ +||| +||| Generated by iseriser for __LANG__ interop. Calling convention: __CONV__. +||| +||| Machine-checked by Idris2 0.7.0: +||| cd src/interface/abi && idris2 --build __ISER__-abi.ipkg + +module __MODULE__.ABI.Types + +import Data.Bits +import Data.So +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- Primitives +-------------------------------------------------------------------------------- + +||| Key primitives for __LANG__ FFI. +public export +data Primitive : Type where +__PRIM_CTORS__ + +||| Stable numeric tag for each primitive. +public export +primCode : Primitive -> Bits32 +__PRIM_CODES__ + +||| Primitives compare by their numeric tag — total and warning-free for any +||| arity (a direct structural `==` would need a catch-all Idris flags as +||| redundant when there is a single constructor). +public export +Eq Primitive where + x == y = primCode x == primCode y + +-------------------------------------------------------------------------------- +-- Result Codes +-------------------------------------------------------------------------------- + +||| Result codes for FFI operations. The integer encoding is the contract the +||| Zig FFI layer depends on; it is pinned by proofs in __MODULE__.ABI.Proofs. +public export +data Result : Type where + Ok : Result + Error : Result + InvalidInput : Result + NullPointer : Result + +||| Convert a Result to its C integer code. +public export +resultToInt : Result -> Bits32 +resultToInt Ok = 0 +resultToInt Error = 1 +resultToInt InvalidInput = 2 +resultToInt NullPointer = 3 + +||| Results are decidably equal. Off-diagonal cases discharge the disequality +||| explicitly; `decEq _ _ = No absurd` does not compile (no `Uninhabited` +||| instance exists for these constructors). +public export +DecEq Result where + decEq Ok Ok = Yes Refl + decEq Error Error = Yes Refl + decEq InvalidInput InvalidInput = Yes Refl + decEq NullPointer NullPointer = Yes Refl + decEq Ok Error = No (\case Refl impossible) + decEq Ok InvalidInput = No (\case Refl impossible) + decEq Ok NullPointer = No (\case Refl impossible) + decEq Error Ok = No (\case Refl impossible) + decEq Error InvalidInput = No (\case Refl impossible) + decEq Error NullPointer = No (\case Refl impossible) + decEq InvalidInput Ok = No (\case Refl impossible) + decEq InvalidInput Error = No (\case Refl impossible) + decEq InvalidInput NullPointer = No (\case Refl impossible) + decEq NullPointer Ok = No (\case Refl impossible) + decEq NullPointer Error = No (\case Refl impossible) + decEq NullPointer InvalidInput = No (\case Refl impossible) + +-------------------------------------------------------------------------------- +-- Opaque Handle +-------------------------------------------------------------------------------- + +||| Opaque handle to a __ISER__ engine context. The non-null invariant is part +||| of the type, so a Handle can never wrap a null pointer. +public export +data Handle : Type where + MkHandle : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> Handle + +||| Safely build a Handle, returning Nothing for a null pointer. `choose` +||| supplies the real `So (ptr /= 0)` witness on the non-null branch. +public export +createHandle : Bits64 -> Maybe Handle +createHandle ptr = + case choose (ptr /= 0) of + Left ok => Just (MkHandle ptr {nonNull = ok}) + Right _ => Nothing + +||| Extract the raw pointer from a Handle. +public export +handlePtr : Handle -> Bits64 +handlePtr (MkHandle ptr) = ptr +"#; + +const VERIFIED_ABI_LAYOUT: &str = r#"-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Memory Layout Proofs for __ISER__ +||| +||| Generated by iseriser. Defines the C-ABI struct-layout machinery and one +||| concrete generation-context layout; Proofs.idr discharges its compliance. + +module __MODULE__.ABI.Layout + +import __MODULE__.ABI.Types +import Data.Vect +import Data.So +import Data.Nat +import Decidable.Equality + +%default total + +||| Padding needed to bring `offset` up to a multiple of `alignment`. +public export +paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat +paddingFor offset alignment = + if offset `mod` alignment == 0 + then 0 + else minus alignment (offset `mod` alignment) + +||| Round `size` up to the next multiple of `alignment`. +public export +alignUp : (size : Nat) -> (alignment : Nat) -> Nat +alignUp size alignment = size + paddingFor size alignment + +||| Proof that `n` divides `m`: `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. 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 + +||| A single named field within a C struct. +public export +record Field where + constructor MkField + name : String + offset : Nat + size : Nat + alignment : Nat + +||| A C-compatible struct layout. The erased proofs pin the total size to cover +||| all fields and to be a multiple of the struct 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} + +||| 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 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 field alignment. +public export +data CABICompliant : StructLayout -> Type where + CABIOk : + (layout : StructLayout) -> + FieldsAligned layout.fields -> + CABICompliant layout + +||| Verify a layout against the C-ABI alignment rules. +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" + +||| C-compatible layout for the __ISER__ generation-context handle. +||| Offsets: 0|8, 8|8, 16|4, 20|4, 24|4, 28|4; total 32, 8-byte aligned. +public export +contextLayout : StructLayout +contextLayout = + MkStructLayout + [ MkField "model_ptr" 0 8 8 + , MkField "state_ptr" 8 8 8 + , MkField "num_items" 16 4 4 + , MkField "item_count" 20 4 4 + , MkField "status" 24 4 4 + , MkField "error_code" 28 4 4 + ] + 32 + 8 + {sizeCorrect = Oh} + {aligned = DivideBy 4 Refl} +"#; + +const VERIFIED_ABI_FOREIGN: &str = r#"-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Foreign Function Interface declarations for __ISER__ +||| +||| Generated by iseriser. Implementations live in src/interface/ffi/src/main.zig +||| and must match the layouts and result codes proven here. + +module __MODULE__.ABI.Foreign + +import __MODULE__.ABI.Types +import __MODULE__.ABI.Layout + +%default total + +||| Decode a raw C result code into a Result. +public export +decodeResult : Bits32 -> Result +decodeResult 0 = Ok +decodeResult 1 = Error +decodeResult 2 = InvalidInput +decodeResult _ = NullPointer + +||| Initialise the __ISER__ engine; returns an opaque context pointer. +export +%foreign "C:__ISER___init, lib__ISER__" +prim__init : PrimIO Bits64 + +||| Safe wrapper: initialise the engine, returning a non-null Handle or Nothing. +export +init : IO (Maybe Handle) +init = do + ptr <- primIO prim__init + pure (createHandle ptr) + +||| Free the __ISER__ context. +export +%foreign "C:__ISER___free, lib__ISER__" +prim__free : Bits64 -> PrimIO () + +||| Safe wrapper: release the engine context. +export +free : Handle -> IO () +free h = primIO (prim__free (handlePtr h)) + +||| Get the library version string pointer. +export +%foreign "C:__ISER___version, lib__ISER__" +prim__version : PrimIO Bits64 + +||| Safe wrapper: retrieve the version string. +export +version : IO String +version = do + ptr <- primIO prim__version + pure (prim__getString ptr) + where + %foreign "support:idris2_getString, libidris2_support" + prim__getString : Bits64 -> String +"#; + +const VERIFIED_ABI_PROOFS: &str = r#"-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Machine-checked proofs over the __ISER__ ABI. +||| +||| These are compile-time propositions, not runtime tests. If any concrete +||| layout were misaligned or the result-code encoding wrong, this module would +||| fail to typecheck and the proof build would go red. + +module __MODULE__.ABI.Proofs + +import __MODULE__.ABI.Types +import __MODULE__.ABI.Layout +import Data.So +import Data.Vect + +%default total + +-------------------------------------------------------------------------------- +-- The concrete context layout is provably C-ABI compliant. +-------------------------------------------------------------------------------- + +||| Every field offset divides its alignment: 0|8, 8|8, 16|4, 20|4, 24|4, 28|4. +||| Each `DivideBy k Refl` forces `offset = k * alignment`; multiplication +||| reduces at the type level, so the compiler checks this outright. The layout +||| name is qualified (`Layout.contextLayout`) so it does not auto-bind as an +||| implicit in the theorem type. +export +contextLayoutCompliant : CABICompliant Layout.contextLayout +contextLayoutCompliant = + CABIOk contextLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 4 Refl) + (ConsField _ _ (DivideBy 5 Refl) + (ConsField _ _ (DivideBy 6 Refl) + (ConsField _ _ (DivideBy 7 Refl) + NoFields)))))) + +||| The struct alignment genuinely divides the total size (32 = 4 * 8). +export +alignmentDividesSize : + Divides (alignment Layout.contextLayout) (totalSize Layout.contextLayout) +alignmentDividesSize = DivideBy 4 Refl + +-------------------------------------------------------------------------------- +-- Result-code round-trip: the encoding the Zig FFI depends on. +-------------------------------------------------------------------------------- + +export +okIsZero : resultToInt Ok = 0 +okIsZero = Refl + +export +nullPointerIsThree : resultToInt NullPointer = 3 +nullPointerIsThree = Refl + +-------------------------------------------------------------------------------- +-- Negative control: the size invariant is not vacuously true. +-------------------------------------------------------------------------------- + +||| A declared size of 4 does NOT cover an 8-byte field — the coverage check +||| rejects it. If the size invariant were trivially true this would not hold. +||| (Uses Nat comparison, which reduces at the type level; Nat div/mod do not, +||| so they are kept out of proofs.) +export +undersizedRejected : So (not (the Nat 4 >= the Nat 8)) +undersizedRejected = Oh + +||| Positive companion: a declared size of 32 does cover 32 bytes of fields. +export +wellSizedAccepted : So (the Nat 32 >= the Nat 32) +wellSizedAccepted = Oh +"#; + // --------------------------------------------------------------------------- // Helpers // --------------------------------------------------------------------------- @@ -1143,6 +1479,15 @@ fn idris2_module_name(model: &LanguageModel) -> String { } } +/// Path to an ABI module file, matching its namespace. +/// E.g. ("Chapeliser", "Types") -> `src/interface/abi/Chapeliser/ABI/Types.idr`. +fn idris_abi_path(module_prefix: &str, module_name: &str) -> PathBuf { + PathBuf::from(format!( + "src/interface/abi/{}/ABI/{}.idr", + module_prefix, module_name + )) +} + /// Convert a primitive name to an Idris2 constructor name. /// E.g. "task" -> "TaskPrim", "forall" -> "ForallPrim". fn to_idris_constructor(prim: &str) -> String { @@ -1234,6 +1579,112 @@ description = "Chapel distributed computing -iser" assert_eq!(to_idris_constructor("sync"), "SyncPrim"); } + #[test] + fn test_idris_abi_path_matches_namespace() { + assert_eq!( + idris_abi_path("Chapeliser", "Types"), + PathBuf::from("src/interface/abi/Chapeliser/ABI/Types.idr") + ); + } + + /// The generated Idris2 ABI must be self-consistent: every module the ipkg + /// lists is emitted, and each sits at the path its namespace dictates. + #[test] + fn test_generated_abi_is_self_consistent() { + let manifest = test_manifest(); + let tmp = tempfile::tempdir().unwrap(); + let result = scaffold_repo(&manifest, tmp.path()); + let repo = result.repo().unwrap(); + let abi = tmp.path().join("chapeliser/src/interface/abi"); + + for module in ["Types", "Layout", "Foreign", "Proofs"] { + let p = abi.join(format!("Chapeliser/ABI/{}.idr", module)); + assert!(p.exists(), "missing ABI module {}", module); + let src = std::fs::read_to_string(&p).unwrap(); + assert!( + src.contains(&format!("module Chapeliser.ABI.{}", module)), + "{} has wrong module declaration", + module + ); + // No unsubstituted template tokens should survive (the `prim__*` + // FFI names legitimately contain `__`, so check the tokens by name). + for token in [ + "__MODULE__", + "__ISER__", + "__LANG__", + "__CONV__", + "__PRIM_CTORS__", + "__PRIM_CODES__", + ] { + assert!( + !src.contains(token), + "{} has leftover template token {}", + module, + token + ); + } + } + + let ipkg = std::fs::read_to_string(abi.join("chapeliser-abi.ipkg")).unwrap(); + for module in ["Types", "Layout", "Foreign", "Proofs"] { + assert!( + ipkg.contains(&format!("Chapeliser.ABI.{}", module)), + "ipkg omits {}", + module + ); + } + // Guard against the old flat, non-compiling form regressing. + assert!(!repo + .files + .iter() + .any(|f| f.path == PathBuf::from("src/interface/abi/Types.idr"))); + } + + /// End-to-end: a freshly generated -iser's Idris2 ABI must compile clean. + /// No-op (passes) where `idris2` is not installed, so CI without the + /// toolchain stays green; run in an idris2 environment for real coverage. + #[test] + fn test_generated_abi_compiles_with_idris2() { + use std::process::Command; + + let idris_ok = Command::new("idris2") + .arg("--version") + .output() + .map(|o| o.status.success()) + .unwrap_or(false); + if !idris_ok { + eprintln!("skipping: idris2 not on PATH"); + return; + } + + let manifest = test_manifest(); + let tmp = tempfile::tempdir().unwrap(); + let result = scaffold_repo(&manifest, tmp.path()); + assert!(result.is_success(), "scaffold failed"); + + let abi_dir = tmp.path().join("chapeliser/src/interface/abi"); + let out = Command::new("idris2") + .args(["--build", "chapeliser-abi.ipkg"]) + .current_dir(&abi_dir) + .output() + .expect("failed to run idris2"); + + let stdout = String::from_utf8_lossy(&out.stdout); + let stderr = String::from_utf8_lossy(&out.stderr); + assert!( + out.status.success(), + "generated ABI failed to build:\n{}\n{}", + stdout, + stderr + ); + // Zero-warning bar: the verified reference compiles without warnings. + assert!( + !stderr.to_lowercase().contains("warning"), + "generated ABI built with warnings:\n{}", + stderr + ); + } + #[test] fn test_files_written_to_disk() { let manifest = test_manifest(); @@ -1244,7 +1695,17 @@ description = "Chapel distributed computing -iser" let repo_root = tmp.path().join("chapeliser"); assert!(repo_root.join("Cargo.toml").exists()); assert!(repo_root.join("src/main.rs").exists()); - assert!(repo_root.join("src/interface/abi/Types.idr").exists()); + // ABI modules live at /ABI/*.idr so the path matches the namespace, + // plus the -abi.ipkg that builds them. + assert!(repo_root + .join("src/interface/abi/Chapeliser/ABI/Types.idr") + .exists()); + assert!(repo_root + .join("src/interface/abi/Chapeliser/ABI/Proofs.idr") + .exists()); + assert!(repo_root + .join("src/interface/abi/chapeliser-abi.ipkg") + .exists()); assert!(repo_root.join("ffi/zig/src/main.zig").exists()); assert!(repo_root.join(".github/workflows/ci.yml").exists()); // standards#89 sub-issue 1: regen trigger only. diff --git a/tests/integration_test.rs b/tests/integration_test.rs index 64a6c1f..504cdb2 100644 --- a/tests/integration_test.rs +++ b/tests/integration_test.rs @@ -97,9 +97,13 @@ fn test_full_pipeline_chapel() { assert!(root.join("Cargo.toml").exists(), "Cargo.toml missing"); assert!(root.join("src/main.rs").exists(), "src/main.rs missing"); assert!( - root.join("src/interface/abi/Types.idr").exists(), + root.join("src/interface/abi/Chapeliser/ABI/Types.idr").exists(), "Types.idr missing" ); + assert!( + root.join("src/interface/abi/chapeliser-abi.ipkg").exists(), + "chapeliser-abi.ipkg missing" + ); assert!( root.join("ffi/zig/src/main.zig").exists(), "main.zig missing" @@ -219,15 +223,18 @@ fn test_full_pipeline_dependent_types() { "dependent type language should have deep ABI proof docs" ); - // Verify the Idris2 Types.idr mentions deep proofs - let types_idr = repo + // Verify the generated ABI ships the real machine-checked proof module + // (the C-ABI compliance theorem), which superseded the old vacuous + // `DeepProof` stub. This theorem is non-vacuous: it pins each field offset + // via `DivideBy k Refl`, so a misaligned layout fails to typecheck. + let proofs_idr = repo .files .iter() - .find(|f| f.path.to_str().unwrap().contains("Types.idr")) - .unwrap(); + .find(|f| f.path.to_str().unwrap().contains("Proofs.idr")) + .expect("Proofs.idr should be generated"); assert!( - types_idr.content.contains("DeepProof"), - "Types.idr should contain DeepProof for dependent types" + proofs_idr.content.contains("CABICompliant"), + "Proofs.idr should contain the C-ABI compliance theorem" ); } From 25780148a5ec9cddce9a28b572f5595a051255a3 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 21:05:59 +0000 Subject: [PATCH 2/2] iseriser: auto-install pinned Zig toolchain in setup + devcontainer The Zig FFI bridge is half of the ABI-FFI standard, but nothing installed Zig: `.tool-versions` only lists it (commented), `setup.sh` stops at `just`, and the devcontainer's `postCreateCommand: just deps` referenced a `deps` recipe that did not exist. Unlike the other toolchain pieces, Zig is not distributed via GitHub releases, so it must come from ziglang.org. Add `scripts/install-zig.sh`: an idempotent, fail-soft installer for the pinned Zig 0.14.0 (arch/OS-aware, uses the system CA store the agent proxy populates, never --insecure). If ziglang.org is not on the session's egress allowlist the download 403s and the script exits 0 with an actionable message, so it never blocks setup or a session. Wire it in via the two paths the project already uses: - `setup.sh` gains a "Step 1b: Install Zig toolchain" that runs it. - a new `deps` Justfile recipe (installs Zig, warms Cargo) backs the devcontainer `postCreateCommand: just deps`, which previously errored. Once ziglang.org is allowlisted, future setups and dev containers install Zig automatically with no further change. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH --- Justfile | 6 +++++ scripts/install-zig.sh | 59 ++++++++++++++++++++++++++++++++++++++++++ setup.sh | 10 +++++++ 3 files changed, 75 insertions(+) create mode 100755 scripts/install-zig.sh diff --git a/Justfile b/Justfile index c71d2f8..5a28e1f 100644 --- a/Justfile +++ b/Justfile @@ -133,3 +133,9 @@ crg-badge: D) color="orange" ;; E) color="red" ;; F) color="critical" ;; \ *) color="lightgrey" ;; esac; \ echo "[![CRG $$grade](https://img.shields.io/badge/CRG-$$grade-$$color?style=flat-square)](https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades)" + +# Install dev dependencies (invoked by the devcontainer postCreateCommand). +# Installs the pinned Zig FFI toolchain, then warms the Cargo cache. +deps: + ./scripts/install-zig.sh + cargo fetch diff --git a/scripts/install-zig.sh b/scripts/install-zig.sh new file mode 100755 index 0000000..63edd64 --- /dev/null +++ b/scripts/install-zig.sh @@ -0,0 +1,59 @@ +#!/bin/sh +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# install-zig.sh — install the pinned Zig toolchain (the Zig FFI bridge half of +# the ABI-FFI standard). Idempotent and fail-soft: it never aborts the caller. +# +# Egress note: Zig is NOT distributed via GitHub releases, so it is fetched from +# ziglang.org. Inside a Claude Code session, outbound HTTPS goes through the +# policy-enforcing agent proxy; github.com is allowlisted by default but +# ziglang.org must be added explicitly, or this download returns 403. We use the +# system CA store the proxy already populated — never pass --insecure. +set -eu + +ZIG_VERSION="${ZIG_VERSION:-0.14.0}" +PREFIX="${ZIG_PREFIX:-/usr/local}" + +# Already at the pinned version? Done. +if command -v zig >/dev/null 2>&1 && [ "$(zig version 2>/dev/null)" = "$ZIG_VERSION" ]; then + echo "install-zig: zig $ZIG_VERSION already installed" + exit 0 +fi + +# Map host arch/OS to Zig's release naming. +case "$(uname -m)" in + x86_64|amd64) zarch="x86_64" ;; + aarch64|arm64) zarch="aarch64" ;; + *) echo "install-zig: unsupported arch $(uname -m); install Zig $ZIG_VERSION manually" >&2; exit 0 ;; +esac +case "$(uname -s)" in + Linux) zos="linux" ;; + Darwin) zos="macos" ;; + *) echo "install-zig: unsupported OS $(uname -s); install Zig $ZIG_VERSION manually" >&2; exit 0 ;; +esac + +tarball="zig-${zos}-${zarch}-${ZIG_VERSION}.tar.xz" +url="https://ziglang.org/download/${ZIG_VERSION}/${tarball}" +dest="${PREFIX}/lib/zig-${ZIG_VERSION}" + +tmp="$(mktemp -d)" +trap 'rm -rf "$tmp"' EXIT + +echo "install-zig: fetching $url" +if ! curl -fsSL --retry 2 -o "$tmp/$tarball" "$url"; then + echo "install-zig: download failed (HTTP error or blocked host)." >&2 + echo "install-zig: if this is a Claude Code session, add 'ziglang.org' to the" >&2 + echo " egress allowlist — github.com is allowed but ziglang.org is not." >&2 + exit 0 # fail-soft: a missing Zig must not block setup or session start +fi + +mkdir -p "$dest" "${PREFIX}/bin" +tar -xJf "$tmp/$tarball" -C "$dest" --strip-components=1 +ln -sf "$dest/zig" "${PREFIX}/bin/zig" + +if command -v zig >/dev/null 2>&1 && [ "$(zig version 2>/dev/null)" = "$ZIG_VERSION" ]; then + echo "install-zig: installed zig $(zig version)" +else + echo "install-zig: installed to ${PREFIX}/bin/zig — ensure ${PREFIX}/bin is on PATH" >&2 +fi diff --git a/setup.sh b/setup.sh index 92a4862..0d2b22e 100755 --- a/setup.sh +++ b/setup.sh @@ -195,6 +195,16 @@ main() { install_just || { fail "Cannot proceed without just"; exit 1; } printf "\n" + # Step 1b: Install the pinned Zig toolchain (the Zig FFI bridge half of the + # ABI-FFI standard). Best-effort — see scripts/install-zig.sh. + printf "%sStep 1b: Install Zig toolchain%s\n" "$BOLD" "$RESET" + if [ -x ./scripts/install-zig.sh ]; then + ./scripts/install-zig.sh || warn "Zig install skipped (see scripts/install-zig.sh)" + else + warn "scripts/install-zig.sh not found — skipping Zig install" + fi + printf "\n" + # Step 2: Check if we're in the repo directory if [ ! -f "Justfile" ] && [ ! -f "justfile" ]; then warn "Not in a repo directory (no Justfile found)"