feat(L10): rung 3b static half — cross-handler named residues

Roadmap item 2. A `reversible as <name>` in one handler is now reversible by
`reverse <name>` in ANOTHER handler of the same agent — the residue is carried
through agent state.

    agent ReversibleWorker {
      control {
        on receive(amount: Int) { reversible as undo { … } }  -- declares `undo`
        on error(reason: String) { reverse undo }             -- replays it
      }
    }

The per-handler isolation that previously severed this is lifted: `check_agent_decl`
collects, per agent, the set of names any handler declares (`agent_residue_names`)
before checking handlers. A cross-handler `reverse <name>` type-checks by
PRESENCE — the name is declared by some handler.

The discipline is honestly split:

- Within one handler, the rung-3a LINEAR discipline still holds: an in-body
  double-`reverse` is rejected. `take_named_residue` now returns a three-way
  `ResidueTake` (Took / AlreadySpent / NotPresent) so the in-body `AlreadySpent`
  error is not masked by agent-level presence.
- Across handlers, acceptance is by presence only — the once-only property is
  irreducibly RUNTIME (handler firing order is not statically known;
  `takeForReverse : Maybe`). The runtime replay is the remaining follow-on.
- Cross-FUNCTION carry stays rejected (functions don't share state).

3 new typechecker tests + `examples/cross_handler_reversibility.007`
(parse + typecheck + run all pass). 900 oo7-core lib tests pass; fmt + clippy
clean. Spec §11b.6 + docs/echo-residue-integration.adoc + CHANGELOG in lockstep.

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

Author: claude

.machine_readable/session-log.txt

@@ -45,3 +45,4 @@
 [2026-06-19 23:08:35] Roadmap item 1 (parser/typecheck gap-fill) — extend DuplicateDefinition to FUNCTION/TYPE/AGENT (branch claude/dup-detection-fn-type-agent off main). These three are gathered (gather_function/type/agent_decl) but silently last-win on redefinition; added Function/TypeDecl/Agent arms to check_duplicate_definitions (within-kind, keyed on (kind,name), per parsed top-level decl). SAFETY: text-grep flagged apparent dup agent names in 5 examples, but inspection showed the 2nd occurrence is always `agent Name(args)` in a supervisor children: list (a REFERENCE, not a top-level decl) — so the per-decl check ignores them; confirmed empirically (oo7 check on every example → zero false positives). 4 tests (dup fn/type/agent + agent-reference-in-supervisor-not-a-dup); fixed the regression snippet after learning `agent Name(args)` is only valid in supervisor children:, not as a control_stmt. 901 oo7-core lib pass (was 897); fmt+clippy clean. Also (answering user q on "done intra-body"): re-verified machine-checking with local provers — ROCQ 35/38 .v (3 walled: M2 mathcomp, E1_ndim+S3_ndim Coquelicot), AGDA 0/1 (M5-yoneda not-started), IDRIS2 16/16 incl L10. User roadmap remaining: (2) L10 rung 3b, (3) full proof suite green (write M5 agda; rocq holdouts CI-only), (4) consolidate. Pushing -> draft PR.
 
 [2026-06-19 23:57:43] Roadmap item 3 — PROOF SUITE GREEN + manifest status refresh (branch claude/proof-suite-status-refresh off main c9a9e92). Ran full canonical-proof-suite-runner with local toolchain (idris2 0.8 + agda 2.6.3 + Rocq 9.0; runner awk-portable since #47): Summary 35/37 passing, 2 regressed. KEY: M5-yoneda.agda is a COMPLETE 386-line self-contained Yoneda proof that compiles runner-style — my earlier agda 0/1 was the path/module-name trap (run from repo-root vs cd-into-dir+basename, same as idris). ~20 not-started-labelled rocq entries (M6-M14/S6-S10/E6-E11) also compile+define-symbol. Refreshed 21 not-started + 1 in-progress(M1) -> passing (sed, verified by the runner pass); M2(mathcomp) + E1(Coquelicot ndim port) kept prior CI-canonical passing (their dep sources gitlab.inria.fr/erratique.ch are 403 in this github-only env). Did NOT commit the runner-regenerated REPORT/STATUS/sidecars (they show M2/E1 as locally-regressed; nightly CI regenerates the canonical evidence with full toolchain) — reverted them. Manifest now 37/37 passing, parens 500/500 balanced, 37 entries parse, revision-log entry added, last-manifest-update bumped to 2026-06-19. Only roadmap item (4) CONSOLIDATE remains; rung-3b RUNTIME half is a separate follow-on. Pushing -> draft PR.
+[2026-06-19 23:49:09] Roadmap item 2 — L10 RUNG 3b STATIC HALF (branch claude/l10-rung3b-static off pre-#49 main). Design (chosen autonomously per user "just drive"): IMPLICIT per-agent scope, static-half-first. check_agent_decl now collects agent_residue_names (all handlers reversible-as bindings, recursive collector mirroring collect_linear_lets) BEFORE the handler loop; the per-handler named_residues isolation stays (intra-body 3a linear discipline). take_named_residue changed Result<(),String> -> 3-way enum ResidueTake{Took,AlreadySpent,NotPresent}; ReverseNamed arm: Took=ok(3a consume), AlreadySpent=in-body double-reverse error, NotPresent=ok IFF agent_residue_names.contains(target) [cross-handler presence, rung 3b] else reverse-without-residue. Key correctness: AlreadySpent (in-body double) NOT masked by agent-presence; cross-FUNCTION still rejected (functions dont populate the set); cross-handler once-only deferred to RUNTIME (firing order unknown, takeForReverse:Maybe). Verified via CLI: r1 cross-handler OK, r2 undeclared->error, r3 in-body-double->error. 3 typechecker tests + examples/cross_handler_reversibility.007 (parse+check+RUN all pass). 900 oo7-core lib pass; fmt+clippy clean. Docs lockstep: spec TYPE-SYSTEM-SPEC new 11b.6, docs/echo-residue-integration.adoc (rung-3b static landed / runtime-half still open), CHANGELOG. REMAINING: 3b runtime half (evaluator replay); roadmap (3) full suite green [write M5 agda], (4) consolidate. Pushing -> draft PR.

CHANGELOG.md

@@ -9,6 +9,7 @@ All notable changes to this project will be documented in this file.
 - **Layer 10 — Reversibility (Echo residue): echo-types integrated into the type system.** `reversible`/`irreversible`/`reverse` are no longer checked identically: `Type::Echo<T>` residues are tracked per body (`reversible` retains one, `irreversible` discards it, `reverse` consumes one), and a `reverse` with no residue is `ReverseWithoutResidue` — enforcing OPERATIONAL-SEMANTICS §11.3, previously unenforced. Grounded in echo-types' keystone `A ≃ Σ B (Echo f)` and mechanised in `proofs/idris2/EchoResidue.idr` (`encodeDecode`, `reverseAfterIrreversibleIllTyped`, `collapseHasNoSection`; `%default total`, zero `believe_me`). Surfaced to agents via `agent_api` code `L10_REVERSE_WITHOUT_RESIDUE` (+`mark_reversible`/`retain_echo` remediations). 4 new typechecker tests. Spec: TYPE-SYSTEM-SPEC §"Layer 10", OPERATIONAL-SEMANTICS §11.4; design note `docs/echo-residue-integration.adoc`.
 - **Layer 10 phase 2 — the residue is a linear undo-capability.** The checker's residue stack now carries `Linear<Echo<T>>` (was a bare `Echo<T>`), making the consumed-once discipline explicit in the type. Discipline: *affine capability, linear consumption* — a given reversal log is consumed at most once (a double `reverse` of one residue is rejected) yet a `reversible` block need not be paired with a `reverse` (an un-reversed residue is **not** an error; reversibility is a capability, usually unused). Mechanised in `proofs/idris2/EchoResidueLinear.idr` (`reverseLinear` consumes `(1 e : Echo f y)`; `ResidueCell` Holding/Spent = the residue as agent state; `holdingReverses`/`spentDoesNotReverse`; `%default total`, zero `believe_me`, `idris2 --check` clean). 3 new typechecker tests (883 `oo7-core` lib tests passing). Remaining rung: cross-handler *named* residues (residue-binding grammar syntax, Harvard-guarded — kept separate). Spec/docs updated in lockstep.
 - **Layer 10 phase 3 (rung 3a) — named residues within a body.** New surface syntax `reversible as <name> { … }` binds the echo residue to a name; `reverse <name>` replays it (anonymous `reversible {…}`/`reverse {…}` unchanged). 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/linear discipline: double `reverse <name>` is rejected (cell already `Spent`); a never-replayed binding is **not** an error; named residues are scoped per body (no cross-body leak). Additive AST variants `ReversibleAs`/`ReverseNamed` (existing variants untouched); grammar (`grammar.pest` + `spec/grammar.ebnf`), parser, typechecker (`named_residues` map + per-function/handler isolation), and the eval/codegen/formatter/dual-ast/metainterpreter/CFG/oracle pipeline all threaded. 2 parser + 5 typechecker tests (890 `oo7-core` lib tests passing; fmt clean, clippy `-D warnings` exit 0). Remaining rung 3b: cross-handler residues through agent state (irreducibly partly runtime — `takeForReverse : Maybe`). Spec: TYPE-SYSTEM-SPEC §11b.5; docs `docs/echo-residue-integration.adoc`.
+- **Layer 10 rung 3b (static half) — cross-handler named residues.** A `reversible as <name>` in one handler is now reversible by `reverse <name>` in *another* handler of the same agent — the residue is carried through agent state. The per-handler isolation that previously severed this is lifted to a per-agent `agent_residue_names` set collected up front; a cross-handler `reverse <name>` type-checks by **presence** (some handler declares it). The discipline is honestly split: within one handler the rung-3a *linear* discipline still holds (in-body double-`reverse` rejected), but cross-handler *once-only* is a **runtime** property — handler firing order is not statically known (`takeForReverse : Maybe`), so it is deferred to the runtime half. `take_named_residue` now returns a 3-way `ResidueTake` (`Took`/`AlreadySpent`/`NotPresent`) so the in-body double-reverse (`AlreadySpent`) is not masked by agent-level presence. Cross-*function* carry stays rejected (functions don't share state). 3 new typechecker tests + new `examples/cross_handler_reversibility.007` (parse + typecheck + run all pass). The runtime replay (evaluator executing the reversal log) is the remaining follow-on.
 - **Layer 10 proofs gated in the canonical proof suite.** The L10 echo-types proofs are now first-class suite entries (`audits/canonical-proof-suite/MANIFEST.a2ml`), gated nightly like the M/S/E classics: new `language` domain `L1` (`proofs/idris2/EchoResidue.idr`, headline `reverseAfterIrreversibleIllTyped`) and `L2` (`proofs/idris2/EchoResidueLinear.idr`, headline `reverseLinear`) — 37 entries total. Each gets the runner's banned-construct scan + `idris2 --check` + symbol-defined check; both verified locally (exit 0, zero banned constructs). The two files' "zero believe_me/assert_total/sorry" disclaimer comments were reworded so the substring banned-scan doesn't false-positive on the very tokens they disclaim. New end-to-end example `examples/named_reversibility.007` exercises `reversible as`/`reverse <name>` through the full pipeline (parse + typecheck + run all pass).
 - **`just gate` — one-command, billing-independent local green-check.** Runs every locally-faithful CI stage in sequence (rustfmt, clippy, `cargo test`, grammar-check, verify-harvard, e2e, `idris2 --check` of all 12 Idris proofs), continues past failures, and prints a per-stage PASS/FAIL/SKIP summary with a non-zero exit on any FAIL. Stages needing an absent toolchain (idris2) or an external GitHub action (A2ML/K9 validators, security scans) self-skip with a notice rather than failing, so it runs anywhere; the rocq canonical-proof-suite (needs Rocq 9) and external manifest/security scans stay CI/nightly-only. Verified GREEN on `main`. Distinct from `just ci` (build/test/lint/verify simulation) and `just check` (fast fmt/lint/test pre-commit).
 - **Import binding-collision detection.** The type checker now validates `import` declarations: every binding an import introduces — an `as` alias, each selective `from … import` item, or a bare `import a.b.c`'s last segment (`c`) — must be unique across the program. A collision (e.g. `import a as x` + `import b as x`, or `from m import abs, abs`) is now a `DuplicateImport` error instead of being silently accepted (imports were previously skipped by the gather pass entirely). Surfaced to agents via `agent_api` code `IMPORT_DUPLICATE_BINDING` (+`rename_import`/`remove_duplicate` remediations). Complements the existing `import_resolver` (which only detects *circular* imports). 4 new typechecker tests (894 `oo7-core` lib tests passing); `examples/imports.007` and the other import-bearing examples are unaffected.