feat(abi): add Rust/SPARK ABI seam + abi-verify CI gate (Refs standards#134)

[hyperpolymath]

Summary

Estate language policy (standards/rhodium-standard-repositories/spec/LANGUAGE-POLICY.adoc §Terminology) requires Rust projects to be "designed to admit SPARK/Ada modules across a stable Idris2-typed boundary, with Zig as the FFI layer." Ephapax has a Coq formal/ metatheory and an Idris2 src/formal/ region/linearity metatheory but no named SPARK admission seam — standards#134 flags this as residual proof debt.

This PR is the scaffolding pass: name the obligations, give them a machine-checked file, gate them in CI. No new discharges — existing ones (splitLinearCoverage, noEscapeTheorem) are CITED from the seam; the vacuous-wrapper problem in regionSafetyExtract / noGCExtract is FLAGGED honestly (it's vacuous: body is the input unchanged, ROADMAP claiming them "complete" is misleading).

What's added

File	Role
src/abi/Ephapax/ABI/Types.idr	Boundary types: Qual, Ty, Term, CtxEntry/TypeCtx, SExpr, WasmExpr, RegionId. Constructor order ABI-significant, matches Rust enums in src/ephapax-{syntax,typing,ir,wasm}/.
src/abi/Ephapax/ABI/Invariants.idr	E1–E6 register (see table below).
src/abi/Ephapax/ABI/Foreign.idr	Zig/WASM-FFI boundary: InU32/InI32Magnitude (Integer-bounded, not Nat — carries the proof-of-work#63 unhang lesson), CompileResult C-ABI codes with round-trip discharge, and compileOkImpliesWasmTyped tying CompileOk to an E5 certificate.
src/abi/ephapax-abi.ipkg	Idris2 package for the Ephapax.ABI.* namespace.
.github/workflows/abi-verify.yml	HARD GATE — rebuilds the seam on every PR/push touching src/abi/** (snazzybucket/idris2 container). Mirrors proof-of-work's abi-verify.yml.
RUST-SPARK-STANCE.adoc	Top-level stance doc, structurally identical to proof-of-work's.

Invariant register

ID	Property	Status
E1	Type preservation	OWED — Coq preservationAdmitted (ephapax#92)
E2	Linear consumption	PARTIAL — head form DISCHARGED via splitLinearCoverage (PR#85); control-flow form OWED
E3	Region no-escape	PARTIAL — narrow form DISCHARGED via noEscapeTheorem; operational form OWED
E4	No-runtime-GC	OWED — noGCExtract is vacuous (returns input pair)
E5	WASM compilation correctness	OWED — no formalisation today
E6	IR lowering correctness	OWED — no formalisation today

Verification (local, Idris2 0.8.0)

cd src/abi && idris2 --build ephapax-abi.ipkg
# → EXIT 0, 3/3 modules built

Honest gaps surfaced by this audit

• regionSafetyExtract / noGCExtract in src/formal/Ephapax/Formal/RegionLinear.idr are vacuous — bodies are = ne and = (ne, lc) (return inputs unchanged). The proofs are sound (no escape hatches) but content-free. ROADMAP citing them as "regionSafetyTheorem" / "noGCTheorem" complete is therefore overstated — flagged in seam (E3, E4) and stance doc.
• No WASM compilation formalisation exists anywhere in the repo. E5 is the highest-leverage compiler-correctness gap.
• ephapax-parse-tests.ipkg fails on origin/main (testLexPositions/parseWithBuf undefined) — independent of the seam, flagged for awareness.

Bounds encoding (Integer not Nat)

Foreign.idr uses Integer for the u32/i32 bounds, not Nat, deliberately carrying the proof-of-work#63 lesson: a Nat constant of 2^32 under LT n bound in a constructor type forces the Idris2 0.8.0 elaborator to reduce the literal (~4×10⁹ S ctors) and hangs --build. The boundary predicate is So (natToInteger n < bound) instead — propositionally equivalent, no unary expansion. Don't rewrite back.

Refs

Refs standards#134 (NOT Closes — joint-close on agreement). #134 also has:

• ephapax#88 OPEN — 14 idris2/src/*.idr SPDX headers
• ephapax#92 OPEN — Qed. → Admitted. on preservation (honesty fix; this stance doc cites it)

Both are independent of this seam.

Test plan

• cd src/abi && idris2 --build ephapax-abi.ipkg → exit 0 locally (3/3 modules)
• abi-verify.yml green on this PR's CI run
• Existing Rust CI unaffected (src/abi/ is independent of src/ephapax-*/ crates)

🤖 Generated with Claude Code