feat(L10): phase 3 rung 3a — named echo residues within a body

[hyperpolymath]

What

L10 phase 3, rung 3a (the slice you chose: static core first). New surface syntax binds a reversal residue to a name and replays it by name, within a single body:

reversible as undo { … }   // bind this block's residue to `undo`
reverse undo               // replay it — consumes the residue exactly once

The anonymous reversible {…} / reverse {…} forms are unchanged. This is fully static — no runtime semantics, which is what makes it the dependable first slice.

Discipline (the affine cell the proof pins)

The named residue is tracked per body as a Holding(Linear<Echo<T>>) cell that reverse transitions to Spent — the static mirror of ResidueCell (Holding/Spent) in EchoResidueLinear.idr. Same affine capability, linear consumption rule as phase 2:

• Linear — a second reverse undo (cell already Spent) is the reverse-without-residue error.
• Affine — a reversible as undo { … } never followed by reverse undo is not an error.
• No leak — named residues are scoped per body (isolated at function + handler boundaries), so a reverse undo cannot reach a reversible as undo in another body. That's the soundness guard and the seam where rung 3b takes over.

Implementation (additive, compiler-guided)

• Grammar (grammar.pest + spec/grammar.ebnf): optional as <ident> on reversible; new reverse_named = "reverse" ident. Harvard-safe (control rules reference the shared ident token; the Harvard invariant guard passes).
• AST: additive variants ReversibleAs { binding, body } / ReverseNamed { target } — existing Reversible/Irreversible/Reverse untouched, so every exhaustive ControlStmt match was enumerated by the compiler and mirrored (codegen ×3, dual_ast, eval, formatter, metainterpreter, CFG, typechecker, oracle).
• Typechecker: per-body named_residues: HashMap<String, NamedResidueState> (Holding(Type)/Spent), bind_named_residue / take_named_residue, the two check_stmt arms, per-function + per-handler isolation.
• Parser: builders for the named forms.

Verified locally

• cargo test -p oo7-core → 890 lib tests (2 new parser + 5 new typechecker), 0 fail
• full-workspace cargo test → 0 failures
• cargo fmt -- --check → clean
• cargo clippy -- -D warnings (CI-equivalent) → exit 0
• Harvard invariant guard → OK; A2ML validator on 6a2/ → 0 errors

Tests

reversible_as_binds_named_residue, reverse_named_parses (parser); and (typechecker) named-reverse-ok, reverse-unknown-errs, double-reverse-errs, un-reversed-ok (affine), no-cross-function-leak.

Not in scope — rung 3b (next)

Cross-handler residues through agent state (a reversible in on receive replayed by a reverse in on error). That step is irreducibly partly runtime — no static analysis knows whether the earlier handler fired, so the Idris takeForReverse returns Maybe. It adds a residue cell in agent state + evaluator runtime Holding/Spent + the bridge lemma. The static name-resolution and affine discipline here carry straight over.

No new Idris was needed — reverseLinear / ResidueCell already model this rung. Spec: TYPE-SYSTEM-SPEC §11b.5; docs docs/echo-residue-integration.adoc.

CI may still be gated by the GitHub Actions billing/spending-limit rejection (account-owner action); all gates above were verified locally.

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

---

Generated by Claude Code