Skip to content

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

Merged
hyperpolymath merged 11 commits into
mainfrom
claude/dreamy-sagan-1ukmue
Jun 18, 2026
Merged

Track 2: FFI seam + cartridge contract + Idris2 CI + AffineScript host binding#23
hyperpolymath merged 11 commits into
mainfrom
claude/dreamy-sagan-1ukmue

Conversation

@hyperpolymath

@hyperpolymath hyperpolymath commented Jun 18, 2026 •
edited
Loading

Copy link
Copy Markdown
Owner

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.ai/code/session_01A1BaAhqxUjkgVb1yg1sZap

claude added 9 commits June 18, 2026 10:30
@claude
docs(theory): add correspondence model — the engine that classifies, …
226b0b4 
…not translates

Canonical design spec for the comprehension/transfer engine: the
Concept/Form/Transition object model, the levels-of-objects strata, the
Dyadic+Echo formal carrier, and the Rosetta false-friends taxonomy
(cognate / false-friend / antonym / alien-realization / novel / vanished)
as graded Echo fibres.

Also records the engine<->cartridge division of labour, the
overlay-protocol / accessibility / PanLL-emit downstream contracts, and the
knot-theory honesty caveat. JTV grammar v2 is stubbed pending repo access.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1BaAhqxUjkgVb1yg1sZap
@claude
chore(standards): complete 6a2 manifest set + panic-attack gate + eNS…
ddd3d44 
…AID config

- Add the missing .machine_readable/6a2 manifests — AGENTIC, NEUROSYM,
  PLAYBOOK — completing the canonical six alongside STATE/META/ECOSYSTEM,
  tuned to the correspondence-engine identity (no-shame voice, classify-not-
  translate, toolchain-deferred build honesty, no-relicense guardrail).
- Add .github/workflows/static-analysis-gate.yml: panic-attack assail +
  hypatia scan + patch-bridge triage. Fails only on critical findings and
  skips gracefully when the binaries are unavailable in the runner.
- Add .machine_readable/ENSAID_CONFIG.a2ml: PanLL / eNSAID per-repo config
  with a correspondence-engine view-layer portfolio.
- Justfile: fix stale panic-attacker -> panic-attack references (tool renamed
  2026-02-08).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1BaAhqxUjkgVb1yg1sZap
@claude
Merge main (#19 spec + #20 hygiene) before identity re-point
c7a1281
@claude
docs(identity): re-point repo to the correspondence (classify-not-tra…
734c4b0 
…nslate) engine

Bring the public + machine-readable identity into line with the merged
correspondence-model spec (docs/theory/CORRESPONDENCE-MODEL.adoc):

- README.adoc, EXPLAINME.adoc, ROADMAP.adoc — Duolingo/Rosetta-Stone-for-PLs
  framing: a comprehension+transfer engine that *classifies* cross-language
  correspondences (Concept/Form/Transition + six CorrespondenceKinds), not an
  IDE / linter / universal translator. Engine-vs-cartridge split; feeds PanLL;
  no-shame transfer-first pedagogy; HAS accessibility; toolchain honesty.
- CLAUDE.md, .claude/CLAUDE.md — corrected overview + notes; policy tables
  preserved (Deno/Justfile/Zig/Idris2; ReScript banned in new code).
- .machine_readable/{STATE,META,ECOSYSTEM}.a2ml (+ 6a2/ copies) — corrected
  identity/purpose/ADRs/related-projects; filled empty + corrupted fields.

Licence labels left untouched (no relicensing): the pre-existing PMPL badge,
"Palimpsest License (MPL-2.0)" text, and ROADMAP "MPL-2.0-or-later" are flagged
to the owner, not edited. No SPDX identifiers changed.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1BaAhqxUjkgVb1yg1sZap
@claude
Merge main (#21 identity) before abstraction-model ABI
6a3bd0a
@claude
feat(abi): Idris2 ABI core — Concept/Form/Transition + six Correspond…
c8b2859 
…enceKinds

First slice of the abstraction-model pivot (track 2), authored as the formally-
typed ABI seam per the chosen "Idris2 ABI core first" approach:

- abi.ipkg — Idris2 package (sourcedir src/interface, depends base only)
- src/interface/Abi/Carrier.idr — Relation (refl/sym/trans + isEquivalence) and
  Residue (the Echo-fibre grades: None/Inverted/Lossy/AbsentSource/AbsentTarget)
- src/interface/Abi/Correspondence.idr — Concept/Form/Transition, the six
  CorrespondenceKinds, the Stratum ladder, total pedagogy + residueShape maps,
  and the precise false-friend signature (surface-corresponds AND intention-diverges)
- src/interface/Abi/README.adoc — seam overview + the cite-don't-import licence note

Licence: original MPL-2.0. Grounded in but NOT importing the Dyadic Relation
(proven-tests-and-benches, AGPL-3.0-or-later / son-shared) or the echo-types Echo
fibre — importing AGPL would relicense this MPL-2.0 repo by linkage, so the shapes
are re-expressed as fresh source. abi.ipkg depends on base only.

Verification deferred: no Idris2 in this environment; typecheck via
`idris2 --typecheck abi.ipkg` in a tooled session / CI.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1BaAhqxUjkgVb1yg1sZap
@claude
Merge main (#22 ABI core) before Zig FFI seam
22935e1
@claude
feat(ffi): Zig FFI seam — C-ABI mirror of the correspondence ABI
dd13b84 
Second slice of the abstraction-model pivot (track 2): the Zig FFI side of the
seam, mirroring the Idris2 ABI (src/interface/Abi/) over a C boundary. Per the
estate pattern Idris2 owns the ABI/proofs and Zig owns the FFI; the two describe
one model and must agree.

- src/interface/ffi/src/main.zig — CorrespondenceKind / Pedagogy / Stratum C
  enums + nle_pedagogy_of (total map), nle_residue_is_iso, nle_kind_name,
  nle_is_false_friend (the false-friend signature) and nle_version; unit tests
  mirror the Idris2 semantics.
- src/interface/ffi/test/integration_test.zig — cross-checks against the model.
- src/interface/ffi/build.zig — minimal Zig 0.15.2+ scaffolding.
- src/interface/ffi/README.adoc — seam overview + cite-don't-import licence note.

Licence: original MPL-2.0, no AGPL/echo-types linkage.
Verification deferred: no Zig in this environment; run `zig test src/main.zig`.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1BaAhqxUjkgVb1yg1sZap
@claude
feat(cartridges): correspondence cartridge contract + validator (veri…
021b227 
…fied)

The data-format half of the abstraction model: how community language packs
declare the correspondence FACTS the engine classifies. The kind / residue /
stratum vocabulary mirrors the Idris2 ABI (src/interface/Abi/Correspondence.idr)
and the Zig FFI.

- cartridges/correspondence-cartridge.schema.json — JSON Schema (draft 2020-12):
  transitions of concept / from / to / kind / residue / strata / narrative /
  witness, with enums mirroring the ABI.
- cartridges/reference/worked-examples.cartridge.json — reference pack: one
  transition per CorrespondenceKind (the canonical worked examples).
- cartridges/README.adoc — cartridge-authoring guide + engine/cartridge boundary.
- scripts/validate-cartridges.js — Deno + ajv validator (walks cartridges/).
- Justfile — `just validate-cartridges` recipe.

Verified locally: `deno run -A scripts/validate-cartridges.js` => 1/1 valid
(6 transitions, all six kinds). Fixed a schema bug found while verifying
($schema vs additionalProperties:false).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1BaAhqxUjkgVb1yg1sZap
@hyperpolymath hyperpolymath changed the title Abstraction model (track 2): Zig FFI seam — C-ABI mirror of the correspondence ABI Abstraction model (track 2): Zig FFI seam + cartridge contract (locally verified) Jun 18, 2026
claude added 2 commits June 18, 2026 13:02
@claude
docs(verify): record ABI typecheck; make cartridge validator lockfile…
47e19a6 
…-safe

- src/interface/Abi/README.adoc: the ABI typechecks clean under Idris2 0.8.0
  (idris2 --typecheck abi.ipkg; %default total, no escape hatches), verified
  locally — replacing the "not yet typechecked here" caveat.
- Justfile + scripts/validate-cartridges.js: run the validator with --no-lock
  so it no longer perturbs deno.lock.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1BaAhqxUjkgVb1yg1sZap
@claude
feat(ci+host): Idris2 ABI typecheck CI + AffineScript host binding
ec1f5dd 
- .github/workflows/idris2-abi.yml: builds Idris2 v0.7.0 from source (Chez) and
  runs `idris2 --typecheck abi.ipkg` on ABI changes — turns the local typecheck
  into a CI gate (mirrors the verified-clean local run).
- src/interface/host/Correspondence.affine: the AffineScript host binding — it
  mirrors the ABI types (CorrespondenceKind/Pedagogy/Stratum/Form/Transition)
  and binds the Zig nle_* FFI symbols via `extern fn`. Authored ahead of the
  AffineScript compiler (compiler-gated; not yet compiled); syntax follows the
  estate .affine conventions.
- src/interface/host/README.adoc.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A1BaAhqxUjkgVb1yg1sZap
@hyperpolymath hyperpolymath changed the title Abstraction model (track 2): Zig FFI seam + cartridge contract (locally verified) Track 2: FFI seam + cartridge contract + Idris2 CI + AffineScript host binding Jun 18, 2026
@hyperpolymath hyperpolymath marked this pull request as ready for review June 18, 2026 13:33
@hyperpolymath hyperpolymath merged commit 61cad3b into main Jun 18, 2026
43 checks passed
@hyperpolymath hyperpolymath deleted the claude/dreamy-sagan-1ukmue branch June 18, 2026 13:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@hyperpolymath @claude