fix(coproc): decouple from Axiom.jl (own seam) + §4.8 path-3-disproved doc (#297)

Two follow-ups to #296 (which merged before these were committed).

**fix(coproc): decouple from Axiom.jl.** Per owner directive: Axiom.jl
was the design *model* (capability classes + linear buffers + thin FFI
seam, full coverage), **not** a dependency. Removes all 'forward to /
surface / import / co-own Axiom' framing from `Coproc.eph`, the Zig shim
(`TODO(axiom)`→`TODO(backend)`, drop Julia C-embedding), and the README
— ephapax owns its own seam, dispatching to a native backend it chooses.
Code unchanged (always a generic FFI boundary; only the narrative was
wrong). Adds `just build-coproc`/`test-coproc`. Documents honestly
(README + gaps **G6**) that the typed `Coproc` API is **not yet
consumable** — `import Coproc; Coproc.upload(…)` neither parses
(qualified `Coproc.Tensor`) nor resolves (import exposes no members):
the keystone gap stranding the whole stdlib. Seam reachable today only
via raw `__ffi` (42-vs-0 proof).

**docs(formal): §4.8 path (3) disproved.** Records that the
owner-approved leaf-rule strengthening was implemented + coqc-disproved
(false at type-erasing eliminators, `EDrop(EVar j)`); the real fork is
effect typing (A′).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

Justfile

@@ -15,6 +15,23 @@ build:
 build-wasm:
     cargo build --target wasm32-unknown-unknown
 
+# Build ephapax's own coprocessor seam (libephapax_coproc.so).
+# This is the native C-ABI seam ephapax reaches via __ffi (-L); it is NOT
+# coupled to any external framework. NOTE: the typed `Coproc` stdlib API is
+# not yet consumable by .eph programs (no module-import / qualified-access
+# in the v2 grammar — see docs/v2-grammar-and-codegen-gaps-2026-06-16.adoc);
+# today the seam is reachable only via raw `__ffi("eph_coproc_*", …)`.
+build-coproc:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    command -v zig >/dev/null 2>&1 || { echo "zig not found"; exit 1; }
+    zig build-lib -dynamic -O ReleaseSafe tools/coproc/ephapax_coproc.zig -femit-bin=libephapax_coproc.so
+    echo "built libephapax_coproc.so (run: ephapax run prog.eph -L libephapax_coproc.so)"
+
+# Run the coprocessor seam's own unit tests (Zig).
+test-coproc:
+    zig test tools/coproc/ephapax_coproc.zig
+
 # Structurally validate emitted wasm for the compilable fixture corpus.
 # Compiles each fixture and runs `wasm-tools validate`, failing on any
 # structurally invalid module. Authoritative CLI twin of the in-process

docs/v2-grammar-and-codegen-gaps-2026-06-16.adoc

@@ -110,3 +110,30 @@ the symbols or fail with a clean "FFI unsupported in the wasm target" error
 writing a broken `.wasm`. This is tracked as codegen debt; the coprocessor
 surface is unaffected because it dispatches via the interpreter's `__ffi`
 path, not wasm.
+
+== G6 — no working module-import + qualified-member access (THE keystone)
+
+A program cannot consume another module's API:
+
+----
+$ printf 'import Coproc\nfn t(): I64 =\n  Coproc.available(Coproc.Tensor)\n' > c.eph; ephapax check c.eph
+Parse error: Unexpected atom expression: construct_expr    # `Coproc.Tensor` (qualified) won't parse
+
+$ printf 'import Coproc\nfn t(): I64 =\n  available(Tensor)\n' > c.eph; ephapax check c.eph
+desugar error: unknown constructor `Tensor`               # `import` doesn't bring members into scope
+----
+
+So `import M; M.f(...)` neither parses (qualified `M.member` is rejected as a
+`construct_expr`) nor resolves (an `import` does not make `M`'s types /
+constructors / functions visible, even unqualified). This is the **keystone
+gap**: every stdlib module (`Region`, `Stream`, `Transactions`, `Prelude`,
+`Coproc`, …) is a typed surface that **nothing can consume**. It is why the
+coprocessor seam is reachable today only through raw `__ffi("eph_coproc_*",
+…)` rather than the typed `Coproc.upload`/`dispatch`/… API.
+
+*This is the single highest-leverage v2 toolchain item:* module-import +
+qualified-member access (the import resolver in
+`src/ephapax-cli/src/import_resolver.rs` already loads the import graph for
+multi-file `compile`, but the surface parser/desugarer does not expose
+imported members). Landing it unblocks consumption of the entire stdlib at
+once.

formal/ESCALATION-4.8-leaf-rule-region-liveness.md

@@ -6,6 +6,54 @@
 **Status:** OPEN — needs an owner design decision before any further L1
 preservation proof work. Raised 2026-06-16.
 
+> ## ⚠️ UPDATE 2026-06-16 — path (3) **proven insufficient**; the real fork is effect typing
+>
+> An implementation attempt of path (3) below (strengthen `T_Var_*_L1` with
+> `In r (free_regions T) -> In r R`) was carried to a coqc-verified
+> intermediate and **disproved**. Path (3) closes the variable leaf and every
+> *type-preserving* constructor, but `region_shrink_preserves_typing_l1_gen_m`
+> becomes a **false statement** at *type-erasing eliminators*.
+>
+> **Counterexample (coqc-checked shape).** `EDrop (EVar j)` with
+> `j : TString rr`, at `R = [rr]`:
+> - types via `T_Drop_L1` (TString is linear) + strengthened `T_Var` (which
+>   forces `In rr R`, satisfied by `In rr [rr]`); output type is `TUnit`;
+> - `expr_strictly_free_of_region rr (EDrop (EVar j)) = True` (no syntactic `rr`);
+> - `~ In rr (free_regions TUnit)` holds trivially (the Tofte-Talpin premise
+>   path (3)/region_shrink can supply);
+> - **yet** shrinking `rr` to `R = []` leaves the inner `EVar j : TString rr`
+>   untypable (`In rr [] = False`). So `region_shrink` is *false* here.
+>
+> The same shape hides inside a **lambda value** whose body uses-and-drops a
+> captured `TString rr` variable, so an `is_value` restriction does not rescue
+> it. **Root cause:** a closure / eliminator can depend on a region *without
+> exposing it in its result type*; the `~ In r (free_regions T)` premise
+> constrains only the *result* type, which these rules erase. This same gap
+> blocks all four targets (region_liveness's ~13 `subst_typing_gen_l1_m` call
+> sites thread the *substituted location's* region, which need not appear in
+> the sub-expression's output type; step_pop's 9 admits are the same "inner
+> step pops a region free in the sibling/outer type").
+>
+> **Therefore the decision is now sharper than (A)/(B)/(C) below:**
+> - **(A′) Adopt effect typing** — deprecate the bare-`TFun` lambda rules
+>   (`T_Lam_L1_Linear`/`_Affine`) and keep only the effect-typed
+>   `T_Lam_L1_*_Eff` (`TFunEff … R_in R_out`), whose `free_regions` already
+>   includes `R_in ++ R_out`. Then every region dependency is type-visible and
+>   the threading composes through eliminators. This is path (1), already
+>   half-built (the TFunEff "live line"). **Recommended — but it changes the
+>   accepted surface language: it rejects region-capturing bare-`TFun`
+>   closures. That rejection is the owner's call.**
+> - **(B′) A context-region-freedom precondition** on `region_shrink`
+>   ("no variable position `e` reads carries `rr` in its type"), a new
+>   predicate over `e × G` threaded from call sites. Heavier; no surface change.
+> - **(C′) Leave the four admits** — but note the path-(3) `T_Var` premise
+>   **cannot coexist with a green build** without (A′)/(B′), so status-quo means
+>   *also reverting* the `T_Var` strengthening (done — `formal/` is back to
+>   clean green-with-one-axiom).
+>
+> No code from the attempt remains; `formal/` is clean green-with-admits. The
+> recommendation below (plain "(A)") is **superseded** by (A′) above.
+
 **Why this is an escalation and not a patch.** `CLAUDE.md` →
 *Anti-pattern detector* lists "strengthened lemma signatures within the
 current judgment shape" and "sibling-region-disjointness side conditions"

stdlib/Coproc.eph

@@ -4,39 +4,40 @@
 //
 // Ephapax Coprocessor API — a THIN typed dispatch boundary (v2 grammar).
 //
-// This module implements NO coprocessor kernels. The ten capability classes
-// surface the EXISTING coprocessor suite in `Axiom.jl` (Julia) — the
-// DSP/Crypto/Math/PPU/GPU/VPU/TPU/QPU/NPU/FPGA backends behind Axiom's
-// `backend_coprocessor_*` generics. ephapax holds only a typed surface plus
-// a substructural safety gate; routing, fallback, and benchmarking stay in
-// Axiom (boundary kept clean — no porting).
+// This module implements NO coprocessor kernels and depends on NO external
+// framework. It is ephapax's OWN coprocessor dispatch surface. Its DESIGN —
+// typed capability classes, a linear device-buffer lifecycle, and a thin
+// C-ABI seam — follows the pattern Axiom.jl established (which demonstrated
+// this shape across the full range of coprocessor types). ephapax models
+// that pattern; it does NOT import, depend on, co-own, or forward to Axiom.
+// ephapax owns its own seam end-to-end.
 //
-// The single shared seam is a thin C ABI: `libephapax_coproc.so` (see
+// The shared seam is a thin C ABI: `libephapax_coproc.so` (see
 // `tools/coproc/ephapax_coproc.zig`) exports flat `eph_coproc_*` symbols
-// that forward to Axiom, mirroring how Axiom itself links Zig. ephapax
-// reaches them through its ordinary `__ffi(...)` path (load with
-// `-L libephapax_coproc.so`). When the library is absent each call falls
-// through to ephapax's `[ffi:stub]` -> 0 path, so the surface stays usable
-// with no coprocessor present.
+// that dispatch to whatever native coprocessor backend is linked behind
+// them. ephapax reaches them through its ordinary `__ffi(...)` path (load
+// with `-L libephapax_coproc.so`). When the library is absent each call
+// falls through to ephapax's `[ffi:stub]` -> 0 path, so the surface stays
+// usable with no coprocessor present.
 
 module Coproc
 
 // ── Capabilities ──────────────────────────────────────────────────────────
 //
-// The ten coprocessor classes, each mapping 1:1 onto an Axiom.jl
-// CoprocessorBackend. The declaration order documents the intent; the wire
-// contract with the Zig shim is made explicit by `cap_tag` below.
+// The ten coprocessor classes (the coverage this design targets). The
+// declaration order documents the intent; the wire contract with the Zig
+// shim is made explicit by `cap_tag` below.
 pub data Capability =
-  | Audio     // -> Axiom DSPBackend  (Audio PU / digital signal processing)
-  | Crypto    // -> Axiom CryptoBackend
-  | Maths     // -> Axiom MathBackend
-  | Physics   // -> Axiom PPUBackend  (physics processing unit)
-  | Gpu       // -> Axiom CUDA / Metal / ROCm
-  | Vector    // -> Axiom VPUBackend  (vector processing unit)
-  | Tensor    // -> Axiom TPUBackend  (tensor processing unit)
-  | Quantum   // -> Axiom QPUBackend  (quantum processing unit)
-  | Io        // -> Axiom NPUBackend / host I/O path
-  | Fpga      // -> Axiom FPGABackend
+  | Audio     // digital signal processing (audio PU)
+  | Crypto    // cryptographic acceleration
+  | Maths     // general numeric / math acceleration
+  | Physics   // physics processing unit
+  | Gpu       // general-purpose GPU
+  | Vector    // vector processing unit
+  | Tensor    // tensor processing unit
+  | Quantum   // quantum processing unit
+  | Io        // I/O / host offload path
+  | Fpga      // field-programmable gate array
 
 // An opaque handle to a buffer living on a coprocessor. LINEAR: once
 // uploaded it must be consumed EXACTLY ONCE — by `download` (pull the

tools/coproc/README.adoc

@@ -7,18 +7,21 @@ toc::[]
 
 == What this is
 
-A *thin typed dispatch boundary* that lets ephapax use the **existing**
-coprocessor suite in `Axiom.jl` (Julia) — the ten DSP/Crypto/Math/PPU/
-GPU/VPU/TPU/QPU/NPU/FPGA backends behind Axiom's `backend_coprocessor_*`
-generics — **without porting any kernel into ephapax**.
+ephapax's **own** *thin typed dispatch boundary* for coprocessors — ten
+capability classes (Audio/Crypto/Maths/Physics/GPU/Vector/Tensor/Quantum/
+IO/FPGA) reached over a single C-ABI seam, with the language's linear types
+guarding the device-buffer lifecycle.
 
-The boundary is deliberately clean (no framework internals cross into the
-language):
+The DESIGN follows the pattern Axiom.jl demonstrated (capability classes +
+linear buffers + a thin FFI seam, covering the full range of coprocessor
+types). ephapax *models* that pattern — it does **not** import, depend on,
+co-own, or forward to Axiom. The seam is ephapax's own, and the boundary is
+deliberately clean (no framework internals cross into the language):
 
 [cols="1,3"]
 |===
 | `stdlib/Coproc.eph` | The typed ephapax surface: a `Capability` sum type (the ten classes), a `cap_tag` wire-tag map, and a LINEAR `CoprocBuf` device-buffer handle with an `upload → dispatch* → (download \| release)` lifecycle. Type-checks under `ephapax check`.
-| `tools/coproc/ephapax_coproc.zig` | The single shared seam: a Zig shared library exporting a flat C ABI (`eph_coproc_*`, all `i64 (...) -> i64`). In a full build it forwards to Axiom via the Julia C-embedding API; the in-tree build is a STUB (reports unavailable, with one loopback for the seam test). Mirrors how Axiom itself links Zig.
+| `tools/coproc/ephapax_coproc.zig` | The single C-ABI seam: a Zig shared library exporting flat `eph_coproc_*` symbols (`i64 (...) -> i64`) that dispatch to whatever native coprocessor backend is linked behind them. The in-tree build is a STUB (reports unavailable, with one loopback for the seam test). No external framework, no Julia, no Axiom runtime.
 | ephapax `__ffi` path | ephapax reaches the seam through its ordinary foreign-call mechanism — no new language feature. Load with `-L libephapax_coproc.so`.
 |===
 
@@ -55,14 +58,30 @@ returns `42` with the shim linked, and falls through to ephapax's built-in
 `[ffi:stub] -> 0` when it is not — proving the `__ffi` path reaches this
 shim.
 
-== Wiring the real Axiom backend
+== Wiring status (honest)
 
-The `// TODO(axiom)` markers in `ephapax_coproc.zig` are the exact forwarder
-points. Each `eph_coproc_*` symbol selects the Axiom `CoprocessorBackend`
-struct from its capability tag and `jl_call`s the matching
-`Axiom.backend_coprocessor_*` generic (`Axiom.jl/src/backends/abstract.jl`),
-copying nothing out of Axiom. Axiom keeps all routing, fallback, and
-benchmarking; ephapax keeps the typed surface + the linear gate.
+*WIRED:* the seam build target (`just build-coproc` / `just test-coproc`),
+and the raw `__ffi` path reaching it (the 42-vs-0 proof above).
+
+*NOT YET WIRED:* no `.eph` program can use the *typed* `Coproc` API. The v2
+toolchain has no working module-import + qualified-member access, so
+`import Coproc; Coproc.upload(…)` neither parses (`Coproc.Tensor` →
+"construct_expr") nor resolves (`import` does not bring members into scope →
+"unknown constructor"). This is the **same keystone gap that strands the
+whole stdlib** (Region/Stream/… are equally un-consumable) — see
+`docs/v2-grammar-and-codegen-gaps-2026-06-16.adoc`. Until module-import lands,
+the seam is reachable only through raw `__ffi("eph_coproc_*", …)`. The typed
+surface is a *foundation*, not yet a consumable feature.
+
+== Wiring a real backend
+
+The `// TODO(backend)` markers in `ephapax_coproc.zig` are the exact
+extension points. Each `eph_coproc_*` symbol selects a coprocessor unit from
+its capability tag and dispatches to the native backend's kernel for that
+op. ephapax keeps the typed surface + the linear gate; the backend behind
+the seam owns routing, fallback, and kernels. The backend is ephapax's to
+choose (native, vendor SDK, or a separate process) — it is **not** part of,
+nor coupled to, any external framework.
 
 An optional `CoprocResult` round-trip proof for the status contract can be
 added to `src/abi/Ephapax/ABI/Foreign.idr` (mirroring `CompileResult`),