Skip to content

Commit 61cad3b

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
Track 2: FFI seam + cartridge contract + Idris2 CI + AffineScript host binding (#23)
## Track 2 — abstraction model: surfaces, contract, CI, and host binding This PR grew (with your go-ahead) from the Zig FFI seam into the second wave of the abstraction-model pivot, on top of the merged Idris2 ABI core (#22). **Verified locally with a real toolchain** (Deno + Chez Scheme + Idris2 installed), not "looks fine." ### Contents 1. **Zig FFI seam** (`src/interface/ffi/`) — C-ABI mirror of the ABI: `CorrespondenceKind`/`Pedagogy`/`Stratum` enums + `nle_pedagogy_of` / `nle_residue_is_iso` / `nle_is_false_friend` / `nle_version`, with tests. 2. **Cartridge contract** (`cartridges/`) — JSON Schema (draft 2020-12) for per-language correspondence packs + a reference pack covering all six kinds + a committed validator (`scripts/validate-cartridges.js`, `just validate-cartridges`). 3. **Idris2 ABI typecheck CI** (`.github/workflows/idris2-abi.yml`) — builds Idris2 v0.7.0 and runs `idris2 --typecheck abi.ipkg` on ABI changes. 4. **AffineScript host binding** (`src/interface/host/Correspondence.affine`) — the host side that mirrors the ABI types and binds the Zig `nle_*` symbols. ### Verification (real, local) | Surface | Check | Result | |---|---|---| | Idris2 ABI (#22) | `idris2 --typecheck abi.ipkg` (Idris2 0.8.0, from source) | ✅ clean, `%default total`, no escape hatches | | Cartridge | `ajv` draft 2020-12 | ✅ valid — 6 transitions / all six kinds | | Zig FFI | `zig test` | ⚠️ Zig unobtainable in the authoring env — deferred to a tooled session/CI | | AffineScript host | compile | ⚠️ compiler-gated (AffineScript compiler unreleased) | The Idris2 typecheck now **also runs in CI here** (the `idris2-abi` job), so it's verified on a runner, not only locally. Verifying-for-real caught + fixed a genuine bug (cartridge `$schema` vs `additionalProperties: false`). ### Licence All new files MPL-2.0; no AGPL/echo-types linkage (the ABI/FFI *cite* the Dyadic/Echo design rather than importing it). No SPDX identifiers changed. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01A1BaAhqxUjkgVb1yg1sZap --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 7a2367f commit 61cad3b

13 files changed

Lines changed: 692 additions & 3 deletions

File tree

‎.github/workflows/idris2-abi.yml‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Idris2 ABI typecheck — verifies the formally-typed seam (abi.ipkg) actually
3+
# typechecks. Builds Idris2 v0.7.0 from source via Chez Scheme (the same path
4+
# verified locally; the ABI typechecks clean under Idris2 0.7/0.8).
5+
name: Idris2 ABI
6+
7+
on:
8+
pull_request:
9+
paths: ['abi.ipkg', 'src/interface/Abi/**', '.github/workflows/idris2-abi.yml']
10+
push:
11+
branches: [main, master]
12+
paths: ['abi.ipkg', 'src/interface/Abi/**', '.github/workflows/idris2-abi.yml']
13+
14+
permissions:
15+
contents: read
16+
17+
jobs:
18+
typecheck:
19+
name: idris2 --typecheck abi.ipkg
20+
runs-on: ubuntu-latest
21+
timeout-minutes: 30
22+
steps:
23+
- name: Checkout repository
24+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
25+
26+
- name: Install Chez Scheme + build tools
27+
run: |
28+
sudo apt-get update -qq
29+
sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -qq \
30+
chezscheme make gcc libgmp-dev
31+
32+
- name: Build Idris2 v0.7.0 from source
33+
run: |
34+
git clone --branch v0.7.0 --depth 1 \
35+
https://github.com/idris-lang/Idris2.git "$HOME/Idris2"
36+
cd "$HOME/Idris2"
37+
make bootstrap SCHEME=chezscheme
38+
make install
39+
echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
40+
41+
- name: Typecheck the ABI
42+
run: |
43+
idris2 --version
44+
idris2 --typecheck abi.ipkg

‎Justfile‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,11 @@ validate:
7676
@echo "🔍 Validating project..."
7777
deno task validate
7878

79+
# Validate cartridges against the correspondence schema (Deno + ajv)
80+
validate-cartridges:
81+
@echo "🧩 Validating cartridges..."
82+
@deno run -A --no-lock scripts/validate-cartridges.js
83+
7984
# Validate RSR compliance
8085
validate-rsr:
8186
@echo "🔍 Validating RSR Bronze-level compliance..."

‎cartridges/README.adoc‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
= Cartridges — per-language correspondence packs
3+
4+
*We build the engine + this contract; the community authors cartridges.* A
5+
**cartridge** is a per-language pack of correspondence *facts* the engine
6+
classifies and teaches. The engine is language-agnostic; a cartridge supplies the
7+
language-specific knowledge.
8+
9+
== What a cartridge declares
10+
11+
For each cross-language `transition` (a directed Form(from) -> Form(to)):
12+
13+
* `concept` — the invariant / trope it instantiates (e.g. `name-binding`);
14+
* `from` / `to` — the `Form`s (`language` slug + `surface` snippet);
15+
* `kind` — the `CorrespondenceKind`: `cognate` / `false-friend` / `antonym` /
16+
`alien-realization` / `novel` / `vanished`;
17+
* `residue` — the Echo-fibre grade (`none` / `inverted` / `lossy` /
18+
`absent-source` / `absent-target`) + a note of what is lost, added, or inverted;
19+
* `strata` (optional) — per-stratum verdicts; the *false-friend signature* is
20+
`surface: true` AND `intention: false`;
21+
* `narrative` (optional) — shame-free guidance (celebrate / minimise / better /
22+
safety / example);
23+
* `witness` (optional) — a path to a proof/test anchoring the claim, used where
24+
the certifiable math pays.
25+
26+
This vocabulary mirrors the Idris2 ABI at `src/interface/Abi/Correspondence.idr`
27+
and the Zig FFI at `src/interface/ffi/`, so cartridges, proofs, and the C
28+
boundary all describe one model.
29+
30+
== Schema and reference
31+
32+
* Schema: `correspondence-cartridge.schema.json` (JSON Schema draft 2020-12).
33+
* Reference: `reference/worked-examples.cartridge.json` — one transition per kind,
34+
using the canonical examples from `docs/theory/CORRESPONDENCE-MODEL.adoc`.
35+
36+
== Authoring a cartridge
37+
38+
. Copy the reference pack and replace its transitions with your language pair(s).
39+
. Validate against the schema, e.g. with any JSON Schema validator:
40+
+
41+
[source,sh]
42+
----
43+
# example (Deno):
44+
deno run --allow-read npm:ajv-cli validate \
45+
-s cartridges/correspondence-cartridge.schema.json \
46+
-d cartridges/reference/worked-examples.cartridge.json
47+
----
48+
. Choose your own `spdx` for your cartridge — the engine does not dictate it.
49+
50+
Estate-wide cartridges live in `hyperpolymath/standards` (`standards/cartridges/`);
51+
this directory holds the schema this engine defines plus its reference pack.
52+
53+
== Licence
54+
55+
The schema and reference pack here are *MPL-2.0*. Cartridge authors license their
56+
own packs as they choose (the `spdx` field).

‎cartridges/correspondence-cartridge.schema.json‎

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
{
2+
"$schema": "https://json-schema.org/draft/2020-12/schema",
3+
"$id": "https://hyperpolymath.dev/nextgen-languages-evangeliser/cartridges/correspondence-cartridge.schema.json",
4+
"title": "Correspondence Cartridge",
5+
"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.",
6+
"type": "object",
7+
"required": ["spdx", "name", "version", "transitions"],
8+
"additionalProperties": false,
9+
"properties": {
10+
"$schema": { "type": "string", "description": "Optional pointer to this schema (for editor / CI validation)." },
11+
"spdx": {
12+
"type": "string",
13+
"description": "SPDX licence of THIS cartridge (the cartridge author's own choice; not dictated by the engine)."
14+
},
15+
"name": {
16+
"type": "string",
17+
"pattern": "^[a-z0-9]+(-[a-z0-9]+)*$",
18+
"description": "Cartridge slug, e.g. 'js-to-erlang' or 'worked-examples'."
19+
},
20+
"version": { "type": "string", "description": "SemVer." },
21+
"description": { "type": "string" },
22+
"languages": {
23+
"type": "array",
24+
"items": { "type": "string" },
25+
"description": "Language slugs this cartridge relates, e.g. ['javascript', 'erlang', 'jtv']."
26+
},
27+
"transitions": {
28+
"type": "array",
29+
"minItems": 1,
30+
"items": { "$ref": "#/$defs/transition" }
31+
}
32+
},
33+
"$defs": {
34+
"form": {
35+
"type": "object",
36+
"required": ["language", "surface"],
37+
"additionalProperties": false,
38+
"properties": {
39+
"language": { "type": "string", "description": "Language slug, e.g. 'erlang'." },
40+
"surface": { "type": "string", "description": "The token / snippet, e.g. 'X = 5'." }
41+
}
42+
},
43+
"stratumVerdict": {
44+
"type": "object",
45+
"required": ["stratum", "holds"],
46+
"additionalProperties": false,
47+
"properties": {
48+
"stratum": {
49+
"enum": ["surface", "structure", "intention", "trope", "invariant"],
50+
"description": "Mirrors Abi.Correspondence.Stratum."
51+
},
52+
"holds": { "type": "boolean", "description": "Does the correspondence hold at this stratum?" }
53+
}
54+
},
55+
"residue": {
56+
"type": "object",
57+
"required": ["shape"],
58+
"additionalProperties": false,
59+
"properties": {
60+
"shape": {
61+
"enum": ["none", "inverted", "lossy", "absent-source", "absent-target"],
62+
"description": "The Echo-fibre grade; mirrors Abi.Carrier.Residue. 'none' = true iso; 'absent-source' = novel; 'absent-target' = vanished."
63+
},
64+
"note": { "type": "string", "description": "What is lost, added, or inverted." }
65+
}
66+
},
67+
"narrative": {
68+
"type": "object",
69+
"additionalProperties": false,
70+
"description": "Shame-free narrative. The voice stays celebrate / minimise / better / safety / example.",
71+
"properties": {
72+
"celebrate": { "type": "string" },
73+
"minimise": { "type": "string" },
74+
"better": { "type": "string" },
75+
"safety": { "type": "string" },
76+
"example": { "type": "string" }
77+
}
78+
},
79+
"transition": {
80+
"type": "object",
81+
"required": ["concept", "from", "to", "kind", "residue"],
82+
"additionalProperties": false,
83+
"properties": {
84+
"concept": { "type": "string", "description": "The Concept (invariant / trope), e.g. 'name-binding'." },
85+
"from": { "$ref": "#/$defs/form" },
86+
"to": { "$ref": "#/$defs/form" },
87+
"kind": {
88+
"enum": ["cognate", "false-friend", "antonym", "alien-realization", "novel", "vanished"],
89+
"description": "The CorrespondenceKind; mirrors Abi.Correspondence.CorrespondenceKind."
90+
},
91+
"residue": { "$ref": "#/$defs/residue" },
92+
"strata": {
93+
"type": "array",
94+
"items": { "$ref": "#/$defs/stratumVerdict" },
95+
"description": "Per-stratum verdicts. The false-friend signature is surface:true AND intention:false."
96+
},
97+
"narrative": { "$ref": "#/$defs/narrative" },
98+
"witness": {
99+
"type": "string",
100+
"description": "Optional path to a proof/test anchoring this claim (the invariant-path governance front-end) — used where the certifiable math pays."
101+
}
102+
}
103+
}
104+
}
105+
}

‎cartridges/reference/worked-examples.cartridge.json‎

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
{
2+
"$schema": "../correspondence-cartridge.schema.json",
3+
"spdx": "MPL-2.0",
4+
"name": "worked-examples",
5+
"version": "0.1.0",
6+
"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.",
7+
"languages": ["python", "scheme", "basic", "erlang", "c", "julia", "jtv", "assembly", "rescript", "javascript"],
8+
"transitions": [
9+
{
10+
"concept": "function-definition",
11+
"from": { "language": "python", "surface": "def f(): ..." },
12+
"to": { "language": "scheme", "surface": "(define (f) ...)" },
13+
"kind": "cognate",
14+
"residue": { "shape": "none" },
15+
"strata": [
16+
{ "stratum": "surface", "holds": false },
17+
{ "stratum": "intention", "holds": true }
18+
],
19+
"narrative": {
20+
"celebrate": "You already define functions — this is the very same idea.",
21+
"better": "`define` is just the Scheme spelling of `def`.",
22+
"safety": "Same binding intent; verify before assuming it is only a rename.",
23+
"example": "def f(): return 1 <-> (define (f) 1)"
24+
}
25+
},
26+
{
27+
"concept": "name-binding",
28+
"from": { "language": "basic", "surface": "X = 5" },
29+
"to": { "language": "erlang", "surface": "X = 5" },
30+
"kind": "false-friend",
31+
"residue": {
32+
"shape": "lossy",
33+
"note": "BASIC rebinds destructively; Erlang binds once and unifies — re-`=` fails a match rather than overwriting."
34+
},
35+
"strata": [
36+
{ "stratum": "surface", "holds": true },
37+
{ "stratum": "intention", "holds": false }
38+
],
39+
"narrative": {
40+
"celebrate": "You have used `=` for assignment for years — that intuition is real.",
41+
"safety": "In Erlang `=` is single-assignment bind / unify, not store.",
42+
"example": "X = 5, X = 6 %% the second match FAILS"
43+
}
44+
},
45+
{
46+
"concept": "array-indexing",
47+
"from": { "language": "c", "surface": "a[0]" },
48+
"to": { "language": "julia", "surface": "a[1]" },
49+
"kind": "antonym",
50+
"residue": { "shape": "inverted", "note": "0-based vs 1-based: the first element flips index." },
51+
"strata": [
52+
{ "stratum": "surface", "holds": true },
53+
{ "stratum": "intention", "holds": true },
54+
{ "stratum": "structure", "holds": false }
55+
]
56+
},
57+
{
58+
"concept": "subtraction",
59+
"from": { "language": "c", "surface": "a - b" },
60+
"to": { "language": "jtv", "surface": "uncall add a b" },
61+
"kind": "alien-realization",
62+
"residue": {
63+
"shape": "lossy",
64+
"note": "JTV is reversible / add-only: subtraction is `add` run backwards; divide via reversed repeated-add."
65+
},
66+
"strata": [
67+
{ "stratum": "intention", "holds": true },
68+
{ "stratum": "structure", "holds": false }
69+
]
70+
},
71+
{
72+
"concept": "static-types",
73+
"from": { "language": "assembly", "surface": "(no analog)" },
74+
"to": { "language": "rescript", "surface": "let x: int = 5" },
75+
"kind": "novel",
76+
"residue": {
77+
"shape": "absent-source",
78+
"note": "Coming from assembly + JS there is no prior anchor for a static type system — teach de novo."
79+
},
80+
"strata": [
81+
{ "stratum": "intention", "holds": false }
82+
]
83+
},
84+
{
85+
"concept": "early-return",
86+
"from": { "language": "javascript", "surface": "return x" },
87+
"to": { "language": "rescript", "surface": "x /* last expression is the value */" },
88+
"kind": "vanished",
89+
"residue": {
90+
"shape": "absent-target",
91+
"note": "ReScript has no `return`; a block evaluates to its last expression — re-route the habit."
92+
},
93+
"strata": [
94+
{ "stratum": "intention", "holds": false }
95+
]
96+
}
97+
]
98+
}

‎scripts/validate-cartridges.js‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Validate every *.cartridge.json under cartridges/ against the correspondence
3+
// schema (JSON Schema draft 2020-12). Deno + ajv.
4+
//
5+
// deno run -A --no-lock scripts/validate-cartridges.js
6+
// just validate-cartridges
7+
//
8+
// Exits non-zero if any cartridge fails — suitable for CI.
9+
10+
import Ajv2020 from "npm:ajv@8/dist/2020.js";
11+
12+
const dir = new URL("../cartridges/", import.meta.url);
13+
const schema = JSON.parse(
14+
await Deno.readTextFile(new URL("correspondence-cartridge.schema.json", dir)),
15+
);
16+
17+
const AjvCtor = Ajv2020.default ?? Ajv2020;
18+
const validate = new AjvCtor({ allErrors: true, strict: false }).compile(schema);
19+
20+
let count = 0;
21+
let bad = 0;
22+
23+
async function walk(d) {
24+
for await (const entry of Deno.readDir(d)) {
25+
const child = new URL(entry.name + (entry.isDirectory ? "/" : ""), d);
26+
if (entry.isDirectory) {
27+
await walk(child);
28+
continue;
29+
}
30+
if (!entry.name.endsWith(".cartridge.json")) continue;
31+
count++;
32+
const data = JSON.parse(await Deno.readTextFile(child));
33+
if (validate(data)) {
34+
console.log(`VALID ${entry.name} (${data.transitions.length} transitions)`);
35+
} else {
36+
bad++;
37+
console.error(`INVALID ${entry.name}`);
38+
console.error(JSON.stringify(validate.errors, null, 2));
39+
}
40+
}
41+
}
42+
43+
await walk(dir);
44+
console.log(`\n${count - bad}/${count} cartridges valid.`);
45+
Deno.exit(bad ? 1 : 0);

‎src/interface/Abi/README.adoc‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -34,8 +34,7 @@ The shapes are re-expressed here as fresh MPL-2.0 source rather than depended on
3434

3535
== Status
3636

37-
Authored ahead of the toolchain: Idris2 is not present in every environment, so
38-
this is verified by `idris2 --typecheck abi.ipkg` in a tooled session / CI, not
39-
yet in the authoring environment. The Zig FFI side of the seam
37+
*Typechecks clean* under Idris2 0.8.0 (`idris2 --typecheck abi.ipkg`; `%default
38+
total`, no escape hatches — verified 2026-06-18). The Zig FFI side of the seam
4039
(`src/interface/ffi/`) and the AffineScript host binding that consumes this ABI
4140
follow as later slices of the abstraction-model pivot.

0 commit comments

Comments
 (0)