diff --git a/.github/workflows/idris2-abi.yml b/.github/workflows/idris2-abi.yml new file mode 100644 index 0000000..3759026 --- /dev/null +++ b/.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 diff --git a/Justfile b/Justfile index ae32a1f..951820c 100644 --- a/Justfile +++ b/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..." diff --git a/cartridges/README.adoc b/cartridges/README.adoc new file mode 100644 index 0000000..2c35887 --- /dev/null +++ b/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). diff --git a/cartridges/correspondence-cartridge.schema.json b/cartridges/correspondence-cartridge.schema.json new file mode 100644 index 0000000..1e00662 --- /dev/null +++ b/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." + } + } + } + } +} diff --git a/cartridges/reference/worked-examples.cartridge.json b/cartridges/reference/worked-examples.cartridge.json new file mode 100644 index 0000000..d2585eb --- /dev/null +++ b/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 } + ] + } + ] +} diff --git a/scripts/validate-cartridges.js b/scripts/validate-cartridges.js new file mode 100644 index 0000000..70a6c0d --- /dev/null +++ b/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); diff --git a/src/interface/Abi/README.adoc b/src/interface/Abi/README.adoc index a2f05f7..07cda21 100644 --- a/src/interface/Abi/README.adoc +++ b/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. diff --git a/src/interface/ffi/README.adoc b/src/interface/ffi/README.adoc new file mode 100644 index 0000000..39af8c3 --- /dev/null +++ b/src/interface/ffi/README.adoc @@ -0,0 +1,30 @@ +// SPDX-License-Identifier: MPL-2.0 += FFI seam — the correspondence model over C-ABI (Zig) + +The C-ABI mirror of the Idris2 ABI in `../Abi/` (`Abi.Carrier` + +`Abi.Correspondence`). Per the estate pattern, *Idris2 owns the ABI/proofs* and +*Zig owns the FFI/C boundary*; the two describe the same model and must agree. + +== Surface + +* `CorrespondenceKind` / `Pedagogy` / `Stratum` — C enums matching the Idris2 types. +* `nle_pedagogy_of(kind) -> Pedagogy` — the total pedagogy map. +* `nle_residue_is_iso(kind) -> u32` — true only for `cognate` (residue `None`). +* `nle_kind_name(kind)` — stable lowercase names. +* `nle_is_false_friend(surface, intention) -> u32` — the false-friend signature + (corresponds at `Surface` AND diverges at `Intention`). +* `nle_version()`. + +== Build / test + +Authored ahead of the toolchain (Zig may be absent in this environment). Run: + +[source,sh] +---- +zig test src/main.zig +zig test test/integration_test.zig +---- + +== Licence + +Original *MPL-2.0*. No AGPL / echo-types linkage — see `../Abi/README.adoc`. diff --git a/src/interface/ffi/build.zig b/src/interface/ffi/build.zig new file mode 100644 index 0000000..c54be06 --- /dev/null +++ b/src/interface/ffi/build.zig @@ -0,0 +1,16 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell +// +// FFI build configuration (Zig 0.15.2+). Minimal scaffolding: the FFI seam +// mirrors the Idris2 ABI in src/interface/Abi/. Run the unit tests directly: +// zig test src/main.zig +// zig test test/integration_test.zig + +const std = @import("std"); + +pub fn build(b: *std.Build) void { + _ = b.standardTargetOptions(.{}); + _ = b.standardOptimizeOption(.{}); + // Tests run via `zig test src/main.zig`. Expand to addStaticLibrary / + // addTest steps when the AffineScript host binding consumes this seam. +} diff --git a/src/interface/ffi/src/main.zig b/src/interface/ffi/src/main.zig new file mode 100644 index 0000000..560589d --- /dev/null +++ b/src/interface/ffi/src/main.zig @@ -0,0 +1,131 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell +// +// Nextgen Languages Evangeliser — FFI seam (Zig). +// +// The C-ABI mirror of the Idris2 ABI in src/interface/Abi/ (Abi.Carrier + +// Abi.Correspondence). Idris2 owns the proofs; Zig owns the C boundary. The two +// MUST agree: the enums and the pedagogy / false-friend semantics here mirror +// Abi.Correspondence exactly. Verify with: zig test src/main.zig +// +// Original MPL-2.0 — no AGPL/echo-types linkage (see ../Abi/README.adoc). + +const std = @import("std"); + +//============================================================================== +// Enums — must match Abi.Correspondence +//============================================================================== + +/// The six graded kinds of cross-language correspondence. +pub const CorrespondenceKind = enum(c_int) { + cognate = 0, + false_friend = 1, + antonym = 2, + alien_realization = 3, + novel = 4, + vanished = 5, +}; + +/// The pedagogy prescribed by each kind. +pub const Pedagogy = enum(c_int) { + transfer = 0, + warn = 1, + remap = 2, + bridge = 3, + teach_de_novo = 4, + re_route = 5, +}; + +/// Strata of meaning ("levels of objects"). +pub const Stratum = enum(c_int) { + surface = 0, + structure = 1, + intention = 2, + trope = 3, + invariant = 4, +}; + +//============================================================================== +// Total maps — mirror Idris2 `pedagogy` and `residueShape` +//============================================================================== + +/// pedagogy : CorrespondenceKind -> Pedagogy (total) +pub export fn nle_pedagogy_of(kind: CorrespondenceKind) Pedagogy { + return switch (kind) { + .cognate => .transfer, + .false_friend => .warn, + .antonym => .remap, + .alien_realization => .bridge, + .novel => .teach_de_novo, + .vanished => .re_route, + }; +} + +/// Is the kind's residue a true isomorphism (None)? Only Cognate. Returns 1/0. +pub export fn nle_residue_is_iso(kind: CorrespondenceKind) u32 { + return if (kind == .cognate) 1 else 0; +} + +/// A stable, lowercase name for a kind (static storage; do not free). +pub export fn nle_kind_name(kind: CorrespondenceKind) [*:0]const u8 { + return switch (kind) { + .cognate => "cognate", + .false_friend => "false-friend", + .antonym => "antonym", + .alien_realization => "alien-realization", + .novel => "novel", + .vanished => "vanished", + }; +} + +//============================================================================== +// The false-friend signature — mirrors Abi.Correspondence.isFalseFriendShape +//============================================================================== + +/// Corresponds at Surface AND diverges at Intention. Inputs are bool-as-u32 +/// (non-zero = holds). Returns 1 if the crossing is a false friend. +pub export fn nle_is_false_friend(surface_holds: u32, intention_holds: u32) u32 { + return if (surface_holds != 0 and intention_holds == 0) 1 else 0; +} + +//============================================================================== +// Version +//============================================================================== + +pub export fn nle_version() [*:0]const u8 { + return "0.1.0"; +} + +//============================================================================== +// Tests — mirror the Idris2 semantics +//============================================================================== + +test "pedagogy mapping is total and matches the ABI" { + try std.testing.expectEqual(Pedagogy.transfer, nle_pedagogy_of(.cognate)); + try std.testing.expectEqual(Pedagogy.warn, nle_pedagogy_of(.false_friend)); + try std.testing.expectEqual(Pedagogy.remap, nle_pedagogy_of(.antonym)); + try std.testing.expectEqual(Pedagogy.bridge, nle_pedagogy_of(.alien_realization)); + try std.testing.expectEqual(Pedagogy.teach_de_novo, nle_pedagogy_of(.novel)); + try std.testing.expectEqual(Pedagogy.re_route, nle_pedagogy_of(.vanished)); +} + +test "only cognate is a true isomorphism" { + try std.testing.expect(nle_residue_is_iso(.cognate) == 1); + try std.testing.expect(nle_residue_is_iso(.false_friend) == 0); + try std.testing.expect(nle_residue_is_iso(.vanished) == 0); +} + +test "false-friend signature: surface holds AND intention diverges" { + try std.testing.expect(nle_is_false_friend(1, 0) == 1); // BASIC = vs Erlang = + try std.testing.expect(nle_is_false_friend(1, 1) == 0); + try std.testing.expect(nle_is_false_friend(0, 0) == 0); + try std.testing.expect(nle_is_false_friend(0, 1) == 0); +} + +test "kind names are stable" { + try std.testing.expectEqualStrings("false-friend", std.mem.span(nle_kind_name(.false_friend))); +} + +test "version is non-empty" { + try std.testing.expect(std.mem.span(nle_version()).len > 0); +} diff --git a/src/interface/ffi/test/integration_test.zig b/src/interface/ffi/test/integration_test.zig new file mode 100644 index 0000000..51125ef --- /dev/null +++ b/src/interface/ffi/test/integration_test.zig @@ -0,0 +1,20 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell +// +// FFI integration tests — verify the Zig C-ABI mirror agrees with the Idris2 ABI +// (src/interface/Abi/Correspondence.idr). Run: zig test test/integration_test.zig + +const std = @import("std"); +const ffi = @import("../src/main.zig"); + +test "pedagogy mapping matches the ABI (spot checks)" { + try std.testing.expectEqual(ffi.Pedagogy.transfer, ffi.nle_pedagogy_of(.cognate)); + try std.testing.expectEqual(ffi.Pedagogy.warn, ffi.nle_pedagogy_of(.false_friend)); + try std.testing.expectEqual(ffi.Pedagogy.re_route, ffi.nle_pedagogy_of(.vanished)); +} + +test "false-friend signature matches the per-stratum rule" { + // surface-corresponds AND intention-diverges (e.g. BASIC = vs Erlang =) + try std.testing.expect(ffi.nle_is_false_friend(1, 0) == 1); + try std.testing.expect(ffi.nle_is_false_friend(1, 1) == 0); +} diff --git a/src/interface/host/Correspondence.affine b/src/interface/host/Correspondence.affine new file mode 100644 index 0000000..94d763c --- /dev/null +++ b/src/interface/host/Correspondence.affine @@ -0,0 +1,117 @@ +// SPDX-License-Identifier: MPL-2.0 +// Correspondence — the AffineScript host binding to the cross-language +// correspondence model. +// +// This mirrors the Idris2 ABI (src/interface/Abi/, which owns the proofs) and +// binds the Zig FFI symbols (src/interface/ffi/, prefix `nle_`, which owns the +// C boundary). Idris2 + Zig + this host module all describe ONE model. +// +// AUTHORED AHEAD OF THE TOOLCHAIN: the AffineScript compiler is not yet +// released, so this module is NOT YET COMPILED. The syntax follows the estate's +// .affine conventions (cf. the 7-tentacles agents); the exact C-FFI `extern` +// annotation and `if`-expression form are confirmed against the AffineScript +// FFI spec when the host toolchain ships. The model types + marshalling are the +// load-bearing part. + +module Correspondence; + +// The six graded kinds (mirrors Abi.Correspondence.CorrespondenceKind and the +// Zig `CorrespondenceKind` enum(c_int), discriminants 0..5). +pub type CorrespondenceKind = + | Cognate + | FalseFriend + | Antonym + | AlienRealization + | Novel + | Vanished + +// The pedagogy prescribed by each kind (mirrors Abi.Correspondence.Pedagogy). +pub type Pedagogy = + | Transfer + | Warn + | Remap + | Bridge + | TeachDeNovo + | ReRoute + +// Strata of meaning ("levels of objects"). +pub type Stratum = + | Surface + | Structure + | Intention + | Trope + | Invariant + +// A representative of a Concept in one language. +pub type Form = { + language: String, + surface: String, +} + +// A per-stratum verdict. +pub type StratumVerdict = { + stratum: Stratum, + holds: Bool, +} + +// A directed correspondence Form(from) -> Form(to): the classified crossing, +// its residue note, the per-stratum verdicts, and an optional witness path. +pub type Transition = { + concept: String, + from: Form, + to: Form, + kind: CorrespondenceKind, + residue: String, + strata: [StratumVerdict], + witness: Option, +} + +// --------------------------------------------------------------------------- +// FFI bindings to the Zig C-ABI seam (src/interface/ffi/, symbols nle_*). +// Integers crossing the boundary are the enum discriminants declared in +// src/interface/ffi/src/main.zig (CorrespondenceKind / Pedagogy as enum(c_int)). +// --------------------------------------------------------------------------- + +extern fn ffi_pedagogy_of(kind: Int) -> Int = "ffi" "nle_pedagogy_of"; +extern fn ffi_residue_is_iso(kind: Int) -> Int = "ffi" "nle_residue_is_iso"; +extern fn ffi_is_false_friend(surface: Int, intention: Int) -> Int = "ffi" "nle_is_false_friend"; + +// Marshalling between the AffineScript sum types and the C discriminants. +pub fn kind_to_int(k: CorrespondenceKind) -> Int { + match k { + Cognate => 0, + FalseFriend => 1, + Antonym => 2, + AlienRealization => 3, + Novel => 4, + Vanished => 5, + } +} + +pub fn int_to_pedagogy(n: Int) -> Pedagogy { + match n { + 0 => Transfer, + 1 => Warn, + 2 => Remap, + 3 => Bridge, + 4 => TeachDeNovo, + _ => ReRoute, + } +} + +// The pedagogy for a kind, via the verified FFI seam. +pub fn pedagogy_of(k: CorrespondenceKind) -> Pedagogy { + int_to_pedagogy(ffi_pedagogy_of(kind_to_int(k))) +} + +// Is the crossing a true isomorphism (residue None)? Only Cognate. +pub fn is_iso(k: CorrespondenceKind) -> Bool { + ffi_residue_is_iso(kind_to_int(k)) == 1 +} + +// The false-friend signature: corresponds at Surface AND diverges at Intention. +pub fn is_false_friend(surface_holds: Bool, intention_holds: Bool) -> Bool { + let s = if surface_holds { 1 } else { 0 }; + let i = if intention_holds { 1 } else { 0 }; + ffi_is_false_friend(s, i) == 1 +} diff --git a/src/interface/host/README.adoc b/src/interface/host/README.adoc new file mode 100644 index 0000000..8b26f1b --- /dev/null +++ b/src/interface/host/README.adoc @@ -0,0 +1,23 @@ +// SPDX-License-Identifier: MPL-2.0 += Host binding — the correspondence model in AffineScript + +The host-language side of the seam. `src/interface/Abi/` (Idris2) owns the +proofs, `src/interface/ffi/` (Zig) owns the C boundary, and this module is the +**AffineScript host binding** that consumes them: it mirrors the model types and +binds the Zig `nle_*` symbols via `extern fn`, so the host engine works in terms +of `CorrespondenceKind` / `Pedagogy` / `Transition` directly. + +== Status — compiler-gated + +The AffineScript compiler is **not yet released**, so `Correspondence.affine` is +**authored but not compiled**. Its syntax follows the estate's `.affine` +conventions (cf. the 7-tentacles agents); the precise C-FFI `extern` annotation +is confirmed against the AffineScript FFI spec when the host toolchain ships. +Until then the proofs live on the verified Idris2 side and the runnable logic on +the verified-in-CI Zig side; this module is the typed surface they converge on. + +== See also + +* `src/interface/Abi/` — Idris2 ABI (typechecks clean under Idris2 0.7/0.8). +* `src/interface/ffi/` — Zig FFI (C-ABI mirror; `zig test`). +* `docs/theory/CORRESPONDENCE-MODEL.adoc` — the design.