From 09678a0791148b997219908002d630f835609f46 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 19:23:15 +0000 Subject: [PATCH] docs(L10): point reversibility note at the landed echo-types bridge The proof-side phase-2 bridge landed as echo-types' `EchoReversibilityBridge` (merged echo-types#249). Update `docs/echo-residue-integration.adoc`: the "natural next step" note now records the bridge as landed, and the Cross-repo bridge section describes its four headlines (`ReversibleCompletion`, `echo-reversible`, `reversibility-via-totality`, the `weaken`/`no-section` discipline) plus the honest scope (the linear-quantity port remains the next slice). Docs-only. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We --- docs/echo-residue-integration.adoc | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/docs/echo-residue-integration.adoc b/docs/echo-residue-integration.adoc index df235f1..ad16eb3 100644 --- a/docs/echo-residue-integration.adoc +++ b/docs/echo-residue-integration.adoc @@ -248,12 +248,30 @@ The replay uses a *per-variable delta*: `reversible as ` captures the before-image of only the fields its body mutates (a static scan of the body), and `reverse ` writes just those back — so unrelated state, including intervening `set`s by other handlers, survives the reversal. The proof-side -bridge lemma against echo-types remains the natural next step. +bridge lemma against echo-types has now landed — see the next section. == Cross-repo bridge (echo-types) `Type::Echo` corresponds to echo-types' `Echo f y`, and 007's CNO layer (`proofs/agda/CNO.agda`) already bridges to `echo-types/EchoCNOBridge`. A direct Agda bridge from the 007 reversibility model to echo-types' -`EchoTotalCompletion` / `EchoLinear` is the natural place to discharge the -phase-2 proof obligations against the upstream library of record. +`EchoTotalCompletion` / `EchoLinear` discharges the phase-2 proof obligations +against the upstream library of record. It has *landed* as +`echo-types/proofs/agda/EchoReversibilityBridge.agda` (`--safe --without-K`, +zero postulates): + +* `ReversibleCompletion` re-states the interface this model needs — arm a + residue (`hold`), take-it-for-reverse (`takeForReverse`), and the once-only + correctness that replay recovers the input (`reverse-recovers`); +* `echo-reversible` proves `Echo f` satisfies it (its `takeForReverse` is + `reverseLinear`'s witness extraction, the `Just`-branch of this model's + `takeForReverse : … → Maybe`); +* `reversibility-via-totality : Σ B (Echo f) ↔ A` is the slogan iso + ("irreversible f + residue = reversible representation"); +* `capability-can-be-dropped` / `no-recovery-once-dropped` pin the phase-2 + "affine capability, linear consumption" discipline via `EchoLinear.weaken` + / `no-section-weaken`. + +Honest scope: this is the type-level totality + recovery + linear→affine +no-section content. 007's linear `(1 e : Echo f y)` quantity is not re-proved +in Agda — the full quantity-semantics port is the documented next slice.