Track 2: FFI seam + cartridge contract + Idris2 CI + AffineScript host binding

.github/workflows/idris2-abi.yml

@@ -0,0 +1,44 @@
+# SPDX-License-Identifier: MPL-2.0
+# Idris2 ABI typecheck — verifies the formally-typed seam (abi.ipkg) actually
+# typechecks. Builds Idris2 v0.7.0 from source via Chez Scheme (the same path
+# verified locally; the ABI typechecks clean under Idris2 0.7/0.8).
+name: Idris2 ABI
+
+on:
+  pull_request:
+    paths: ['abi.ipkg', 'src/interface/Abi/**', '.github/workflows/idris2-abi.yml']
+  push:
+    branches: [main, master]
+    paths: ['abi.ipkg', 'src/interface/Abi/**', '.github/workflows/idris2-abi.yml']
+
+permissions:
+  contents: read
+
+jobs:
+  typecheck:
+    name: idris2 --typecheck abi.ipkg
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - name: Install Chez Scheme + build tools
+        run: |
+          sudo apt-get update -qq
+          sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -qq \
+            chezscheme make gcc libgmp-dev
+
+      - name: Build Idris2 v0.7.0 from source
+        run: |
+          git clone --branch v0.7.0 --depth 1 \
+            https://github.com/idris-lang/Idris2.git "$HOME/Idris2"
+          cd "$HOME/Idris2"
+          make bootstrap SCHEME=chezscheme
+          make install
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+
+      - name: Typecheck the ABI
+        run: |
+          idris2 --version
+          idris2 --typecheck abi.ipkg

Justfile

@@ -76,6 +76,11 @@ validate:
     @echo "🔍 Validating project..."
     deno task validate
 
+# Validate cartridges against the correspondence schema (Deno + ajv)
+validate-cartridges:
+    @echo "🧩 Validating cartridges..."
+    @deno run -A --no-lock scripts/validate-cartridges.js
+
 # Validate RSR compliance
 validate-rsr:
     @echo "🔍 Validating RSR Bronze-level compliance..."

cartridges/README.adoc

@@ -0,0 +1,56 @@
+// SPDX-License-Identifier: MPL-2.0
+= Cartridges — per-language correspondence packs
+
+*We build the engine + this contract; the community authors cartridges.* A
+**cartridge** is a per-language pack of correspondence *facts* the engine
+classifies and teaches. The engine is language-agnostic; a cartridge supplies the
+language-specific knowledge.
+
+== What a cartridge declares
+
+For each cross-language `transition` (a directed Form(from) -> Form(to)):
+
+* `concept` — the invariant / trope it instantiates (e.g. `name-binding`);
+* `from` / `to` — the `Form`s (`language` slug + `surface` snippet);
+* `kind` — the `CorrespondenceKind`: `cognate` / `false-friend` / `antonym` /
+  `alien-realization` / `novel` / `vanished`;
+* `residue` — the Echo-fibre grade (`none` / `inverted` / `lossy` /
+  `absent-source` / `absent-target`) + a note of what is lost, added, or inverted;
+* `strata` (optional) — per-stratum verdicts; the *false-friend signature* is
+  `surface: true` AND `intention: false`;
+* `narrative` (optional) — shame-free guidance (celebrate / minimise / better /
+  safety / example);
+* `witness` (optional) — a path to a proof/test anchoring the claim, used where
+  the certifiable math pays.
+
+This vocabulary mirrors the Idris2 ABI at `src/interface/Abi/Correspondence.idr`
+and the Zig FFI at `src/interface/ffi/`, so cartridges, proofs, and the C
+boundary all describe one model.
+
+== Schema and reference
+
+* Schema: `correspondence-cartridge.schema.json` (JSON Schema draft 2020-12).
+* Reference: `reference/worked-examples.cartridge.json` — one transition per kind,
+  using the canonical examples from `docs/theory/CORRESPONDENCE-MODEL.adoc`.
+
+== Authoring a cartridge
+
+. Copy the reference pack and replace its transitions with your language pair(s).
+. Validate against the schema, e.g. with any JSON Schema validator:
++
+[source,sh]
+----
+# example (Deno):
+deno run --allow-read npm:ajv-cli validate \
+  -s cartridges/correspondence-cartridge.schema.json \
+  -d cartridges/reference/worked-examples.cartridge.json
+----
+. Choose your own `spdx` for your cartridge — the engine does not dictate it.
+
+Estate-wide cartridges live in `hyperpolymath/standards` (`standards/cartridges/`);
+this directory holds the schema this engine defines plus its reference pack.
+
+== Licence
+
+The schema and reference pack here are *MPL-2.0*. Cartridge authors license their
+own packs as they choose (the `spdx` field).

cartridges/correspondence-cartridge.schema.json

@@ -0,0 +1,105 @@
+{
+  "$schema": "https://json-schema.org/draft/2020-12/schema",
+  "$id": "https://hyperpolymath.dev/nextgen-languages-evangeliser/cartridges/correspondence-cartridge.schema.json",
+  "title": "Correspondence Cartridge",
+  "description": "SPDX-License-Identifier: MPL-2.0. A per-language correspondence pack for the Nextgen Languages Evangeliser engine. A cartridge declares the FACTS — which Forms instantiate which Concepts, and for each Transition its kind + residue + per-stratum verdicts — that the engine classifies. The vocabulary (kinds, strata, residue shapes) mirrors the Idris2 ABI at src/interface/Abi/Correspondence.idr. We build the engine + this contract; the community authors cartridges.",
+  "type": "object",
+  "required": ["spdx", "name", "version", "transitions"],
+  "additionalProperties": false,
+  "properties": {
+    "$schema": { "type": "string", "description": "Optional pointer to this schema (for editor / CI validation)." },
+    "spdx": {
+      "type": "string",
+      "description": "SPDX licence of THIS cartridge (the cartridge author's own choice; not dictated by the engine)."
+    },
+    "name": {
+      "type": "string",
+      "pattern": "^[a-z0-9]+(-[a-z0-9]+)*$",
+      "description": "Cartridge slug, e.g. 'js-to-erlang' or 'worked-examples'."
+    },
+    "version": { "type": "string", "description": "SemVer." },
+    "description": { "type": "string" },
+    "languages": {
+      "type": "array",
+      "items": { "type": "string" },
+      "description": "Language slugs this cartridge relates, e.g. ['javascript', 'erlang', 'jtv']."
+    },
+    "transitions": {
+      "type": "array",
+      "minItems": 1,
+      "items": { "$ref": "#/$defs/transition" }
+    }
+  },
+  "$defs": {
+    "form": {
+      "type": "object",
+      "required": ["language", "surface"],
+      "additionalProperties": false,
+      "properties": {
+        "language": { "type": "string", "description": "Language slug, e.g. 'erlang'." },
+        "surface": { "type": "string", "description": "The token / snippet, e.g. 'X = 5'." }
+      }
+    },
+    "stratumVerdict": {
+      "type": "object",
+      "required": ["stratum", "holds"],
+      "additionalProperties": false,
+      "properties": {
+        "stratum": {
+          "enum": ["surface", "structure", "intention", "trope", "invariant"],
+          "description": "Mirrors Abi.Correspondence.Stratum."
+        },
+        "holds": { "type": "boolean", "description": "Does the correspondence hold at this stratum?" }
+      }
+    },
+    "residue": {
+      "type": "object",
+      "required": ["shape"],
+      "additionalProperties": false,
+      "properties": {
+        "shape": {
+          "enum": ["none", "inverted", "lossy", "absent-source", "absent-target"],
+          "description": "The Echo-fibre grade; mirrors Abi.Carrier.Residue. 'none' = true iso; 'absent-source' = novel; 'absent-target' = vanished."
+        },
+        "note": { "type": "string", "description": "What is lost, added, or inverted." }
+      }
+    },
+    "narrative": {
+      "type": "object",
+      "additionalProperties": false,
+      "description": "Shame-free narrative. The voice stays celebrate / minimise / better / safety / example.",
+      "properties": {
+        "celebrate": { "type": "string" },
+        "minimise": { "type": "string" },
+        "better": { "type": "string" },
+        "safety": { "type": "string" },
+        "example": { "type": "string" }
+      }
+    },
+    "transition": {
+      "type": "object",
+      "required": ["concept", "from", "to", "kind", "residue"],
+      "additionalProperties": false,
+      "properties": {
+        "concept": { "type": "string", "description": "The Concept (invariant / trope), e.g. 'name-binding'." },
+        "from": { "$ref": "#/$defs/form" },
+        "to": { "$ref": "#/$defs/form" },
+        "kind": {
+          "enum": ["cognate", "false-friend", "antonym", "alien-realization", "novel", "vanished"],
+          "description": "The CorrespondenceKind; mirrors Abi.Correspondence.CorrespondenceKind."
+        },
+        "residue": { "$ref": "#/$defs/residue" },
+        "strata": {
+          "type": "array",
+          "items": { "$ref": "#/$defs/stratumVerdict" },
+          "description": "Per-stratum verdicts. The false-friend signature is surface:true AND intention:false."
+        },
+        "narrative": { "$ref": "#/$defs/narrative" },
+        "witness": {
+          "type": "string",
+          "description": "Optional path to a proof/test anchoring this claim (the invariant-path governance front-end) — used where the certifiable math pays."
+        }
+      }
+    }
+  }
+}

cartridges/reference/worked-examples.cartridge.json

@@ -0,0 +1,98 @@
+{
+  "$schema": "../correspondence-cartridge.schema.json",
+  "spdx": "MPL-2.0",
+  "name": "worked-examples",
+  "version": "0.1.0",
+  "description": "Reference cartridge: one correspondence per CorrespondenceKind, using the canonical worked examples from docs/theory/CORRESPONDENCE-MODEL.adoc. Proves the schema covers all six grades of the Echo fibre.",
+  "languages": ["python", "scheme", "basic", "erlang", "c", "julia", "jtv", "assembly", "rescript", "javascript"],
+  "transitions": [
+    {
+      "concept": "function-definition",
+      "from": { "language": "python", "surface": "def f(): ..." },
+      "to": { "language": "scheme", "surface": "(define (f) ...)" },
+      "kind": "cognate",
+      "residue": { "shape": "none" },
+      "strata": [
+        { "stratum": "surface", "holds": false },
+        { "stratum": "intention", "holds": true }
+      ],
+      "narrative": {
+        "celebrate": "You already define functions — this is the very same idea.",
+        "better": "`define` is just the Scheme spelling of `def`.",
+        "safety": "Same binding intent; verify before assuming it is only a rename.",
+        "example": "def f(): return 1   <->   (define (f) 1)"
+      }
+    },
+    {
+      "concept": "name-binding",
+      "from": { "language": "basic", "surface": "X = 5" },
+      "to": { "language": "erlang", "surface": "X = 5" },
+      "kind": "false-friend",
+      "residue": {
+        "shape": "lossy",
+        "note": "BASIC rebinds destructively; Erlang binds once and unifies — re-`=` fails a match rather than overwriting."
+      },
+      "strata": [
+        { "stratum": "surface", "holds": true },
+        { "stratum": "intention", "holds": false }
+      ],
+      "narrative": {
+        "celebrate": "You have used `=` for assignment for years — that intuition is real.",
+        "safety": "In Erlang `=` is single-assignment bind / unify, not store.",
+        "example": "X = 5, X = 6   %% the second match FAILS"
+      }
+    },
+    {
+      "concept": "array-indexing",
+      "from": { "language": "c", "surface": "a[0]" },
+      "to": { "language": "julia", "surface": "a[1]" },
+      "kind": "antonym",
+      "residue": { "shape": "inverted", "note": "0-based vs 1-based: the first element flips index." },
+      "strata": [
+        { "stratum": "surface", "holds": true },
+        { "stratum": "intention", "holds": true },
+        { "stratum": "structure", "holds": false }
+      ]
+    },
+    {
+      "concept": "subtraction",
+      "from": { "language": "c", "surface": "a - b" },
+      "to": { "language": "jtv", "surface": "uncall add a b" },
+      "kind": "alien-realization",
+      "residue": {
+        "shape": "lossy",
+        "note": "JTV is reversible / add-only: subtraction is `add` run backwards; divide via reversed repeated-add."
+      },
+      "strata": [
+        { "stratum": "intention", "holds": true },
+        { "stratum": "structure", "holds": false }
+      ]
+    },
+    {
+      "concept": "static-types",
+      "from": { "language": "assembly", "surface": "(no analog)" },
+      "to": { "language": "rescript", "surface": "let x: int = 5" },
+      "kind": "novel",
+      "residue": {
+        "shape": "absent-source",
+        "note": "Coming from assembly + JS there is no prior anchor for a static type system — teach de novo."
+      },
+      "strata": [
+        { "stratum": "intention", "holds": false }
+      ]
+    },
+    {
+      "concept": "early-return",
+      "from": { "language": "javascript", "surface": "return x" },
+      "to": { "language": "rescript", "surface": "x  /* last expression is the value */" },
+      "kind": "vanished",
+      "residue": {
+        "shape": "absent-target",
+        "note": "ReScript has no `return`; a block evaluates to its last expression — re-route the habit."
+      },
+      "strata": [
+        { "stratum": "intention", "holds": false }
+      ]
+    }
+  ]
+}

scripts/validate-cartridges.js

@@ -0,0 +1,45 @@
+// SPDX-License-Identifier: MPL-2.0
+// Validate every *.cartridge.json under cartridges/ against the correspondence
+// schema (JSON Schema draft 2020-12). Deno + ajv.
+//
+//   deno run -A --no-lock scripts/validate-cartridges.js
+//   just validate-cartridges
+//
+// Exits non-zero if any cartridge fails — suitable for CI.
+
+import Ajv2020 from "npm:ajv@8/dist/2020.js";
+
+const dir = new URL("../cartridges/", import.meta.url);
+const schema = JSON.parse(
+  await Deno.readTextFile(new URL("correspondence-cartridge.schema.json", dir)),
+);
+
+const AjvCtor = Ajv2020.default ?? Ajv2020;
+const validate = new AjvCtor({ allErrors: true, strict: false }).compile(schema);
+
+let count = 0;
+let bad = 0;
+
+async function walk(d) {
+  for await (const entry of Deno.readDir(d)) {
+    const child = new URL(entry.name + (entry.isDirectory ? "/" : ""), d);
+    if (entry.isDirectory) {
+      await walk(child);
+      continue;
+    }
+    if (!entry.name.endsWith(".cartridge.json")) continue;
+    count++;
+    const data = JSON.parse(await Deno.readTextFile(child));
+    if (validate(data)) {
+      console.log(`VALID    ${entry.name}  (${data.transitions.length} transitions)`);
+    } else {
+      bad++;
+      console.error(`INVALID  ${entry.name}`);
+      console.error(JSON.stringify(validate.errors, null, 2));
+    }
+  }
+}
+
+await walk(dir);
+console.log(`\n${count - bad}/${count} cartridges valid.`);
+Deno.exit(bad ? 1 : 0);

src/interface/Abi/README.adoc

@@ -34,8 +34,7 @@ The shapes are re-expressed here as fresh MPL-2.0 source rather than depended on
 
 == Status
 
-Authored ahead of the toolchain: Idris2 is not present in every environment, so
-this is verified by `idris2 --typecheck abi.ipkg` in a tooled session / CI, not
-yet in the authoring environment. The Zig FFI side of the seam
+*Typechecks clean* under Idris2 0.8.0 (`idris2 --typecheck abi.ipkg`; `%default
+total`, no escape hatches — verified 2026-06-18). The Zig FFI side of the seam
 (`src/interface/ffi/`) and the AffineScript host binding that consumes this ABI
 follow as later slices of the abstraction-model pivot.