Abstraction model (track 2): Idris2 ABI core — Concept/Form/Transition + CorrespondenceKind#22
Merged
Merged
Conversation
…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
…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
…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
…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
hyperpolymath
added a commit
that referenced
this pull request
Jun 18, 2026
…t 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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Abstraction-model pivot — track 2, first slice (Idris2 ABI core)
The first slice of the abstraction model, authored as the formally-typed ABI seam (the approach you picked: Idris2 ABI core first — policy-clean and verifiable-in-principle). It encodes the engine's model from the merged spec:
Files
abi.ipkg— Idris2 package (sourcedir = src/interface,depends = baseonly).src/interface/Abi/Carrier.idr—Relation(reflexive/symmetric/transitive +isEquivalence) andResidue, the grades of the Echo fibre:None(true iso) ·Inverted·Lossy·AbsentSource·AbsentTarget.src/interface/Abi/Correspondence.idr—Concept/Form/Transition; the sixCorrespondenceKinds (cognate / false-friend / antonym / alien-realization / novel / vanished); theStratumladder; totalpedagogyandresidueShapemaps; and the precise false-friend signatureisFalseFriendShape— corresponds atSurface∧ diverges atIntention.src/interface/Abi/README.adoc— seam overview + licence note.This seam is original MPL-2.0 code. It is grounded in but does not import:
Relationfromproven-tests-and-benches— which is AGPL-3.0-or-later (son-shared); importing it would relicense this MPL-2.0 repo by linkage;echo-types(Agda).So the shapes are re-expressed as fresh source and
abi.ipkgdepends onbaseonly. This is the AGPL↔MPL boundary I flagged earlier — handled by non-dependence rather than import.Verification (deferred — author-now / verify-in-CI)
No Idris2 in this environment, so this is not yet typechecked here. Verify with
idris2 --typecheck abi.ipkgin a tooled session / CI. It is written%default totalwith no escape hatches (nobelieve_me/assert_total/postulate).Next slices of track 2
src/interface/ffi/).Patterns/Narrative/Analyser) onto this model.🤖 Generated with Claude Code
https://claude.ai/code/session_01A1BaAhqxUjkgVb1yg1sZap
Generated by Claude Code