feat(L10): phase 2 — echo residue as a linear undo-capability

.machine_readable/6a2/STATE.a2ml

@@ -6,9 +6,9 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Phase-2 echo-residue (Linear<Echo<T>> undo-capability + cross-handler reversal); reconcile estate-standardization-20260607 into main; continue parser gap fill (types, imports, locales, choreographies)"
-last_action: "echo-types integrated as Kategoria Layer 10 reversibility — Echo residue makes reverse/irreversible type-safe (spec §11.3 now ENFORCED), Idris2 EchoResidue.idr proof, agent-facing L10_REVERSE_WITHOUT_RESIDUE (PR #34 merged); test/E2E/clippy/fmt CI gates greened (PR #38 merged); CI reconciled at root: hypatia ssh→https, A2ML 40→0, K9 7→0, grammar-guard, eclexiaiser merge-conflict, stapeln"
-updated: 2026-06-13T07:40:00Z
+next_action: "Layer-10 cross-handler named residues: residue-binding grammar syntax (let undo = reversible {…}; reverse undo) carried through agent state — Harvard-guarded grammar change, own rung; then continue parser gap fill (types, imports, locales, choreographies)"
+last_action: "Phase-2 echo-residue landed: residue is now Linear<Echo<T>> (affine capability, linear consumption — double-reverse rejected, un-reversed residue not an error); Idris2 EchoResidueLinear.idr (reverseLinear (1 e), ResidueCell Holding/Spent, idris2 --check clean, zero believe_me); 3 new typechecker tests (883 oo7-core passing); spec §11b.4/§11.4 + CHANGELOG + integration doc updated in lockstep. estate-standardization-20260607 reconciled into main (PR #40 merged). Prior: Layer 10 phase-1 (PR #34), CI gates greened (PR #38), 6a2/ecosystem refresh (PR #39)"
+updated: 2026-06-14T02:00:00Z
 
 @blockers:
 - id: proof-debt
@@ -17,9 +17,6 @@ updated: 2026-06-13T07:40:00Z
 - id: ci-billing
   description: "GitHub Actions billing/spending-limit rejection — every job fails in 2-3s with no logs; blocks CI validation of all pushes (account-owner action: Settings → Billing & plans)"
   since: 2026-06-13
-- id: estate-standardization-unmerged
-  description: "estate-standardization-20260607 (estate-standards catch-up: contractiles, bot_directives, svc/k9→self-validating rename, 24 CI workflows) diverged from main AND conflicts with PR #34/#38 (ci.yml + K9 guards renamed from PRE-#38 content, so the K9! magic/pedigree fixes must be re-applied during reconciliation)"
-  since: 2026-06-13
 @end
 
 @note(id="patacl-relationship", added="2026-04-27"):

.machine_readable/session-log.txt

@@ -27,3 +27,5 @@
 [2026-06-13 12:06:00] UPDATE: PR #38 MERGED to origin/main. BOTH this session's PRs are now in main (#34 echo-types Layer 10 + CI root-fixes; #38 test/E2E gates + session-log checkpoint). main is the single reconciled line. Branch-reconciliation now reduces to: both feature branches (claude/inspiring-meitner-QHuNU, claude/ci-cleanup-fmt-clippy-examples) are MERGED → safe to delete. Remaining next-actions unchanged: (ii) delete the two merged branches + enumerate any OTHER remote branches; (iii) doc-currency sweep (6a2, ANCHOR realignment, contractiles incl. Bust/Dust, svc/k9, CREATE bot_directives/, README/EXPLAINME, wiki bleeding-edge); (iv) standards/rsr-template drift check (flag divergence immediately); (v) recency-gate nextgen-languages/nextgen-typing/echo-types; (vi) resume main work. NOTE: GitHub Actions billing rejection may still be active — verify before relying on CI.
 [2026-06-13 12:25:00] BRANCH DECISION (item 3): chore/hypatia-scan-reusable-wrapper assessed → DROP (superseded, do not re-create). Evidence: (1) main already DELETED its inline hypatia-scan.yml; (2) main's codeql.yml already uses the `actions` extractor (the branch's "codeql actions matrix" commit is redundant); (3) estate-standardization-20260607 redoes BOTH codeql.yml + hypatia-scan.yml, and its hypatia-scan.yml is the same thin standards reusable-wrapper but pinned to a NEWER standards SHA (6cd3772) vs the branch's stale 97df762. The branch (3 wks old, 24 commits behind main, 3 commits ahead) adds nothing not better-done by main + estate-standardization. DELETION BLOCKED from this remote-exec env: the local git proxy rejects push-deletes ("remote end hung up") and the GitHub MCP has no delete-branch/ref tool. ACTION (account owner): delete chore/hypatia-scan-reusable-wrapper, OR it retires naturally when estate-standardization-20260607 lands. Remaining open branch decision: estate-standardization-20260607 (the standards catch-up; conflicts with #34/#38; needs maintainer-driven reconcile — re-apply the K9!/grammar fixes into the renamed self-validating/ guards).
 
+
+[2026-06-14 01:25:37] Session ended (continuation): item-2 estate-standardization reconcile MERGED (PR #40) → main is one reconciled line. Then resumed ORIGINAL WORK = Layer-10 PHASE 2 (residue as a linear undo-capability). (a) Idris2: proofs/idris2/EchoResidueLinear.idr (NEW, %default total, zero believe_me, idris2 --check clean) — reverseLinear consumes (1 e : Echo f y) (Idris2 quantity 1 = "consumed exactly once" proof, mirroring 007's planned Linear<Echo<T>>); reverseLinearCorrect (recovered input maps back to y, intrinsic via the dependent pair); ResidueCell Holding/Spent = the residue carried as agent STATE between handlers; takeForReverse (later handler consumes the cell; Spent→Nothing); holdingReverses/spentDoesNotReverse (cross-handler reversal succeeds iff a residue was retained); cellMode bridges a cell back to the phase-1 Reversibility mode. (b) Rust typechecker.rs: residue stack now carries Linear<Echo<T>> (push_echo_residue wraps Type::Echo in Type::Linear) — the consumed-once discipline is explicit in the carried type; the single linear use is the take_echo_residue pop in a later reverse. +3 typechecker_tests (l10_phase2_residue_type_is_linear_echo / _double_reverse_of_single_residue_is_error / _retained_residue_is_not_an_error) → 883 oo7-core lib tests passing. CI gates verified LOCALLY: cargo check --offline 0, full oo7-core test suite 922 ok 0 fail, fmt --check 0, clippy (CI-equivalent, no --all-targets) -D warnings exit 0. (c) DESIGN DECISION flagged to user (a plus/interesting): the residue is an AFFINE capability consumed LINEARLY — replaying one log twice is rejected (linear use; structural in the stack), but a reversible block need NOT be paired with a reverse (un-reversed residue is NOT an error; reversibility is a capability, usually unused). The opposite (strict must-reverse / LinearNotConsumed) was deliberately REJECTED as semantically wrong + poor agent ergonomics; the 3 tests lock the affine-drop in so it can't be silently tightened. (d) Docs in lockstep: TYPE-SYSTEM-SPEC §11b.4 + OPERATIONAL-SEMANTICS §11.4 (planned→landed), CHANGELOG phase-2 bullet, docs/echo-residue-integration.adoc (phase-2 section + design-decision subsection + "still open" cross-handler rung), 6a2 STATE.a2ml last/next_action + cleared estate-standardization-unmerged blocker. (e) NOTE — canonical-proof-suite MANIFEST.a2ml NOT touched: phase-1 EchoResidue.idr is not a manifest entry either, so EchoResidueLinear.idr stays alongside it (checked by idris2 --check, not the curated S/E/M suite); the proof-suite workflow ignores unlisted .idr files (no CI risk). STILL OPEN (next rung): cross-handler NAMED residues need residue-binding grammar syntax (let undo = reversible {…}; reverse undo) — Harvard-guarded grammar change, kept as its own rung; formal model (ResidueCell) already in place, only surface syntax missing. Phase-2 work pushed to branch claude/echo-residue-phase2-linear → draft PR. Billing blocker may still gate CI (account-owner action).

CHANGELOG.md

@@ -6,7 +6,8 @@ All notable changes to this project will be documented in this file.
 ## [Unreleased] — 2026-04-10 consolidation pass
 
 ### Added
-- **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 (880 `oo7-core` lib tests passing). Spec: TYPE-SYSTEM-SPEC §"Layer 10", OPERATIONAL-SEMANTICS §11.4; design note `docs/echo-residue-integration.adoc` (incl. the phase-2 linear-undo-capability rung).
+- **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.
 - **752 tests** (up from 207 at 0.5.0). CRG-C achieved 2026-04-04 for `oo7-core`.
 - **31 multi-language backends** via `mk2_bridge::create_backend_registry()`. Real dispatch to `elixir`, `idris2`, `gleam`, `rescript`, `nickel`, `guile`, `psql`, etc. Tier-5 coprocessor backends (CUDA/Vulkan/Metal/OpenCL/FPGA/TPU/DSP) do phase-1 device discovery with documented "kernel launch is future work" status.
 - **Metainterpreter** (`metainterpreter.rs`, ~3,075 LOC): reify/reflect/step/replay, four modes, 40 inline tests, 18 benches.

crates/oo7-core/src/typechecker.rs

@@ -501,12 +501,24 @@ pub struct TypeEnv {
     /// The witness is removed before the `else` branch (where `d` may be zero)
     /// and after the `if` statement.
     pub nonzero_witnesses: HashSet<String>,
-    /// L10 reversibility: the stack of Echo residues currently in scope
-    /// (echo-types residue tracking). A `reversible` block pushes a residue
-    /// (its reversal log); a `reverse` block consumes one; an `irreversible`
-    /// block pushes nothing (the residue is discarded). A `reverse` with an
-    /// empty stack is a ReverseWithoutResidue error — this enforces spec
-    /// §11.3 ("reverse of an irreversible block is a compile-time error").
+    /// L10 reversibility: the stack of LINEAR Echo residues currently in
+    /// scope (echo-types residue tracking). Each entry is a `Linear<Echo<T>>`
+    /// — a consumed-exactly-once undo-capability. A `reversible` block pushes
+    /// a residue (its reversal log); a `reverse` block consumes one (the
+    /// single linear use); an `irreversible` block pushes nothing (the
+    /// residue is discarded). A `reverse` with an empty stack is a
+    /// ReverseWithoutResidue error — this enforces spec §11.3 ("reverse of an
+    /// irreversible block is a compile-time error").
+    ///
+    /// Discipline (phase 2, mechanised in proofs/idris2/EchoResidueLinear.idr):
+    /// the residue is an *affine capability* consumed *linearly*. Replaying a
+    /// given log twice is rejected (the stack has already popped it); retaining
+    /// a log that is never replayed is NOT an error (a `reversible` block need
+    /// not be paired with a `reverse` — reversibility is a capability, usually
+    /// unused), so residues outstanding at a body boundary are dropped, not
+    /// flagged. Cross-body (cross-handler) reversal — a residue bound by name
+    /// and consumed by a later handler — is the next rung and needs residue
+    /// binding syntax in the grammar (cf. `ResidueCell` in the Idris proof).
     echo_residues: Vec<Type>,
 }
 
@@ -533,18 +545,28 @@ impl TypeEnv {
 
     // -- Echo residue management (L10 reversibility, echo-types) --
 
-    /// A `reversible` block retains a reversal log — model it as pushing an
-    /// `Echo<T>` residue onto the scope. `inner` is the type the block's
-    /// reversal restores (Unit for now; the phased "linear undo-capability"
-    /// rung refines this to a consumed-exactly-once residue value).
+    /// A `reversible` block retains a reversal log — model it as pushing a
+    /// LINEAR `Echo<T>` residue onto the scope, i.e. `Linear<Echo<T>>`: the
+    /// consumed-exactly-once undo-capability that 007's planned
+    /// `Linear<Echo<T>>` names directly. `inner` is the type the block's
+    /// reversal restores (`Unit` until the AST carries a restored-value type).
+    /// Wrapping in `Type::Linear` makes the residue's resource discipline
+    /// explicit in the carried type; the single linear use is discharged by
+    /// the matching `take_echo_residue` pop in a later `reverse`. This is the
+    /// linear-undo rung mechanised in proofs/idris2/EchoResidueLinear.idr,
+    /// where `reverseLinear` consumes `(1 e : Echo f y)`.
     fn push_echo_residue(&mut self, inner: Type) {
-        self.echo_residues.push(Type::Echo(Box::new(inner)));
+        self.echo_residues
+            .push(Type::Linear(Box::new(Type::Echo(Box::new(inner)))));
     }
 
-    /// A `reverse` block consumes the most recent Echo residue, if any.
-    /// Returns `None` when no residue is in scope — i.e. the `reverse`
-    /// targets an `irreversible` block (or has no preceding `reversible`
-    /// block), which is the ReverseWithoutResidue error.
+    /// A `reverse` block consumes the most recent linear Echo residue, if any
+    /// — the single linear use of that `Linear<Echo<T>>`. Returns `None` when
+    /// no residue is in scope — i.e. the `reverse` targets an `irreversible`
+    /// block (or has no preceding `reversible` block), which is the
+    /// ReverseWithoutResidue error. Because the residue is popped, the same
+    /// reversal log cannot be replayed twice (the linear "use at most once"
+    /// is structural in the stack).
     fn take_echo_residue(&mut self) -> Option<Type> {
         self.echo_residues.pop()
     }
@@ -1794,8 +1816,11 @@ fn check_function_decl(fd: &FunctionDecl, env: &mut TypeEnv) {
 
     // Echo residues (L10) are scoped to this function body: a `reversible`
     // here must not leak its reversal log to a `reverse` in another
-    // function. Cross-body (e.g. cross-handler) reversal is agent state,
-    // handled by the forthcoming linear-residue rung.
+    // function. Each residue is a linear `Linear<Echo<T>>`; residues still
+    // outstanding at the body boundary are dropped (the undo capability was
+    // simply never exercised — not an error). Cross-body (e.g. cross-handler)
+    // reversal carries a residue by name through agent state; that named
+    // binding is the next rung (cf. `ResidueCell` in EchoResidueLinear.idr).
     let saved_residues = std::mem::take(&mut env.echo_residues);
     for stmt in &fd.body {
         check_stmt(stmt, &ret_type, env);
@@ -1837,10 +1862,13 @@ fn check_agent_decl(ad: &AgentDecl, env: &mut TypeEnv) {
             let ty = resolve_type_str(ty_str, env);
             env.bind(name.clone(), ty, LinearStatus::Unrestricted);
         }
-        // Echo residues (L10) are scoped per handler body. Cross-handler
-        // reversal (a `reverse` in one handler replaying a `reversible` in
-        // another) is agent state, not a statically-scoped block residue —
-        // deferred to the linear-residue rung.
+        // Echo residues (L10) are scoped per handler body; each is a linear
+        // `Linear<Echo<T>>`. Cross-handler reversal (a `reverse` in one
+        // handler replaying a `reversible` in another) carries the residue by
+        // name through agent state, not as a statically-scoped block residue —
+        // that named binding is the next rung (cf. `ResidueCell` in
+        // EchoResidueLinear.idr). Residues outstanding at the handler boundary
+        // are dropped: an unexercised undo capability is not an error.
         let saved_residues = std::mem::take(&mut env.echo_residues);
         for stmt in &handler.body {
             check_stmt(stmt, &Type::Unit, env);
@@ -3394,8 +3422,9 @@ fn check_stmt(stmt: &ControlStmt, expected_ret: &Type, env: &mut TypeEnv) {
                 check_stmt(s, expected_ret, env);
             }
             env.pop_scope();
-            // The block's operations each have an inverse → an Echo residue
-            // becomes available to a later `reverse`.
+            // The block's operations each have an inverse → a linear Echo
+            // residue (`Linear<Echo<T>>`) becomes available to a later
+            // `reverse`, which consumes it exactly once.
             env.push_echo_residue(Type::Unit);
         }