From 0f368e53a9afefe1b2d402b7e17ccfbd4768fd1e Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 19:03:04 +0000 Subject: [PATCH 1/2] =?UTF-8?q?feat:=20EchoReversibilityBridge=20=E2=80=94?= =?UTF-8?q?=20discharge=20007=20L10=20reversibility=20obligations?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit New `proofs/agda/EchoReversibilityBridge.agda`: the constructive discharge of the 007 language's Layer-10 reversibility (echo-residue) "phase-2" proof obligations against echo-types as the library of record. 007 models reversibility with an echo residue (`reversible as`/`reverse`, the Idris2 `EchoResidue.idr`/`EchoResidueLinear.idr` spec); this module re-states the interface those obligations describe and shows echo-types' own structures satisfy it. - `ReversibleCompletion f Residue` — the interface 007's model needs: arm a residue (`hold`), take-it-for-reverse (`takeForReverse`), and once-only correctness (`reverse-recovers`). Residue carrier is a parameter. - `echo-reversible : ReversibleCompletion f (Echo f)` — `Echo f` satisfies it: `hold = echo-intro` (007's `encode`/`Holding`), `takeForReverse = proj₁` (`reverseLinear`'s witness), recovery `refl`. - `reversibility-via-totality : Σ B (Echo f) ↔ A` — the slogan iso (symmetric partner of `EchoTotalCompletion.A↔ΣEcho`): irreversible f + residue = reversible representation. - `capability-can-be-dropped` / `no-recovery-once-dropped` — the phase-2 "affine capability, linear consumption" discipline via `EchoLinear.weaken` / `no-section-weaken`. --safe --without-K, zero postulates. Wired into All.agda; five headlines pinned in Smoke.agda. EchoReversibilityBridge + Smoke.agda + All.agda all exit 0. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We --- proofs/agda/All.agda | 1 + proofs/agda/EchoReversibilityBridge.agda | 107 +++++++++++++++++++++++ proofs/agda/Smoke.agda | 15 ++++ 3 files changed, 123 insertions(+) create mode 100644 proofs/agda/EchoReversibilityBridge.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 9fd5313..0efd576 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -36,6 +36,7 @@ open import AntiEchoTropical open import AntiEchoTropicalGeneric open import EchoIntegration open import EchoCNOBridge +open import EchoReversibilityBridge open import EchoApprox open import EchoApproxInstance diff --git a/proofs/agda/EchoReversibilityBridge.agda b/proofs/agda/EchoReversibilityBridge.agda new file mode 100644 index 0000000..8f14078 --- /dev/null +++ b/proofs/agda/EchoReversibilityBridge.agda @@ -0,0 +1,107 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +-- +-- EchoReversibilityBridge: the constructive discharge of the 007 language's +-- Layer-10 reversibility (echo-residue) "phase-2" proof obligations against +-- this library of record. +-- +-- 007 (https://github.com/hyperpolymath/007) models reversibility with an +-- echo residue: `reversible as ` arms a residue cell holding an +-- `Echo f y`, and `reverse ` consumes it to recover the input. Its +-- Idris2 spec (`proofs/idris2/EchoResidue.idr`, +-- `proofs/idris2/EchoResidueLinear.idr`) pins three obligations: +-- +-- 1. encode / decode round-trips — an irreversible `f` together with its +-- residue is a total, reversible representation; +-- 2. `reverseLinear : (1 e : Echo f y) → (x ** f x ≡ y)` — replaying a held +-- residue recovers the input (the `Holding`/`takeForReverse = Just` +-- branch of `ResidueCell`); +-- 3. the linear discipline "affine capability, linear consumption" — the +-- undo capability may be dropped (weakened) but, once dropped, the +-- linear residue cannot be recovered (`Spent` does not reverse). +-- +-- This module re-states the *interface* those obligations describe and shows +-- echo-types' own `Echo` / `EchoTotalCompletion` / `EchoLinear` satisfy it, +-- under `--safe --without-K` with zero postulates. The Agda here is the +-- source of truth; 007's Rust checker and Idris2 spec mirror this model. + +{-# OPTIONS --safe --without-K #-} + +module EchoReversibilityBridge where + +open import Level using (Level; _⊔_) +open import Data.Product.Base using (Σ; _,_; proj₁) +open import Function.Bundles using (_↔_; mk↔ₛ′) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) +open import Relation.Nullary using (¬_) + +open import Echo using (Echo; echo-intro) +open import EchoTotalCompletion using (encode; decode; decode-encode; encode-decode) +open import EchoLinear using (linear; affine; LEcho; weaken; no-section-weaken) + +private variable + a b : Level + A : Set a + B : Set b + +------------------------------------------------------------------------ +-- Obligations 1 + 2: the reversible-completion interface, met by Echo. +------------------------------------------------------------------------ + +-- The minimal data 007's reversibility model needs from a residue carrier: +-- arm a residue from an input (`hold`), take-it-for-reverse to recover an +-- input (`takeForReverse`), and the once-only correctness that replaying a +-- freshly-armed residue returns the original input (`reverse-recovers`). +-- +-- `takeForReverse` here is the *total* `Just`-branch of 007's +-- `takeForReverse : … → Maybe a`, i.e. `reverseLinear`'s witness extraction +-- on a `Holding` cell; the `Maybe` wrapper is the runtime `Holding`/`Spent` +-- bookkeeping, not part of the type-level correspondence. +-- +-- The residue carrier `Residue` is a parameter: an instance witnesses that a +-- *particular* carrier (here `Echo f`) supports armed reversal. +record ReversibleCompletion {a b} {A : Set a} {B : Set b} + (f : A → B) (Residue : B → Set (a ⊔ b)) : Set (a ⊔ b) where + field + hold : (x : A) → Residue (f x) + takeForReverse : {y : B} → Residue y → A + reverse-recovers : (x : A) → takeForReverse (hold x) ≡ x + +-- echo-types' `Echo f` is such a carrier. `hold` is `echo-intro` (= 007's +-- `encode` / the `Holding` cell); `takeForReverse` is the witness projection +-- (= `reverseLinear`'s `fst`); recovery is `refl`, because +-- `proj₁ (echo-intro f x) = proj₁ (x , refl) = x` definitionally. +echo-reversible : (f : A → B) → ReversibleCompletion f (Echo f) +echo-reversible f = record + { hold = echo-intro f + ; takeForReverse = proj₁ + ; reverse-recovers = λ _ → refl + } + +-- 007's narrative slogan — "an irreversible computation together with its +-- echo residue is a reversible representation" — is exactly echo-types' +-- totality iso read in the residue→input direction: the total echo space +-- `Σ B (Echo f)` recovers the domain `A`. (The A→Σ direction is +-- `EchoTotalCompletion.A↔ΣEcho`; this is its symmetric partner.) +reversibility-via-totality : (f : A → B) → Σ B (Echo f) ↔ A +reversibility-via-totality f = + mk↔ₛ′ (decode f) (encode f) (decode-encode f) (encode-decode f) + +------------------------------------------------------------------------ +-- Obligation 3: the phase-2 linear discipline. +------------------------------------------------------------------------ + +-- "Affine capability": a live (linear) undo residue may always be weakened +-- to an affine one — the capability dropped. Never an error in 007. +capability-can-be-dropped : LEcho linear → LEcho affine +capability-can-be-dropped = weaken + +-- "Linear consumption / Spent-does-not-reverse": there is NO section of +-- `weaken` — once the residue is degraded (the undo dropped, the cell +-- `Spent`) the linear residue cannot be recovered. This is echo-types' +-- `no-section-weaken`, the library-of-record discharge of the irreversibility +-- of dropping the capability. +no-recovery-once-dropped : + ¬ (Σ (LEcho affine → LEcho linear) + (λ raise → ∀ e → raise (weaken e) ≡ e)) +no-recovery-once-dropped = no-section-weaken diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 9f1861c..eccc1d2 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -92,6 +92,21 @@ open import EchoTotalCompletion using ; encode-is-section-of-proj₁ ) +-- EchoReversibilityBridge — constructive discharge of the 007 language's +-- Layer-10 reversibility (echo-residue) phase-2 obligations against this +-- library of record. `ReversibleCompletion` is the interface 007's model +-- needs (arm / take-for-reverse / replay-recovers); `echo-reversible` shows +-- `Echo f` satisfies it; `reversibility-via-totality` is the slogan iso +-- `Σ B (Echo f) ↔ A`; `capability-can-be-dropped` / `no-recovery-once-dropped` +-- pin the phase-2 "affine capability, linear consumption" discipline. +open import EchoReversibilityBridge using + ( ReversibleCompletion + ; echo-reversible + ; reversibility-via-totality + ; capability-can-be-dropped + ; no-recovery-once-dropped + ) + -- EchoNoSectionGeneric — raises the example-level -- `no-section-collapse-to-residue` to a uniform structural theorem. -- Generic headline `no-section-of-collapsing-map`: any collapsing From 257138c4b272b7a5f6ffcd29aa04b24ff5102439 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 19:06:42 +0000 Subject: [PATCH 2/2] docs: classify EchoReversibilityBridge in kernel-note + MAP kernel-guard.sh's classification-drift lint (CI job `check`) requires every `Echo*.agda` to be named in `docs/echo-types/echo-kernel-note.adoc`. Add `EchoReversibilityBridge` to the Tier-2 module list (alongside the sibling cross-repo bridges `EchoCNOBridge` / `EchoEphapaxBridge`) and a descriptive MAP.adoc cross-repo-bridge entry. `sh scripts/kernel-guard.sh` now PASSes. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We --- docs/echo-types/MAP.adoc | 21 +++++++++++++++++++++ docs/echo-types/echo-kernel-note.adoc | 2 +- 2 files changed, 22 insertions(+), 1 deletion(-) diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index ffa468e..152163d 100644 --- a/docs/echo-types/MAP.adoc +++ b/docs/echo-types/MAP.adoc @@ -466,6 +466,27 @@ discharged by `coqc` on the ephapax side; no Lane 4 CI dependency. `formal/PRESERVATION-DESIGN.md` + `docs/echo-types/paper.adoc` §"Threats to validity"). +=== 007 L10 reversibility — echo-residue bridge `[REAL]` +Cross-repo navigability marker for the `hyperpolymath/007` language +project, whose Layer-10 reversibility model (`reversible as`/`reverse`, +specified in Idris2 `proofs/idris2/EchoResidue.idr` + +`EchoResidueLinear.idr`) is discharged against echo-types as the library +of record. The module re-states the interface 007's model needs and shows +echo-types' own structures satisfy it, under `--safe --without-K`, zero +postulates. + +* Proofs: `proofs/agda/EchoReversibilityBridge.agda` — + `ReversibleCompletion` (the arm / take-for-reverse / replay-recovers + interface), `echo-reversible` (`Echo f` satisfies it; `takeForReverse` + ↔ `reverseLinear`'s witness), `reversibility-via-totality : + Σ B (Echo f) ↔ A` (symmetric partner of + `EchoTotalCompletion.A↔ΣEcho`), and `capability-can-be-dropped` / + `no-recovery-once-dropped` (007 phase-2 "affine capability, linear + consumption" via `EchoLinear.weaken` / `no-section-weaken`). +* Scope: 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). + === Tropical / Dyadic `[REAL*]` Bridge domains enumerated in `docs/EchoBridges.md` (JanusKey / CNO / Tropical / Dyadic). Dyadic is mechanised; Tropical is named/early. diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc index f1c1740..8fc793d 100644 --- a/docs/echo-types/echo-kernel-note.adoc +++ b/docs/echo-types/echo-kernel-note.adoc @@ -82,7 +82,7 @@ kernel** — the boundary is real and lives outside this core. `EchoEpistemicResidue`, `EchoExamples`, `EchoGraded`, `EchoLinear`, `EchoPullback`, `EchoRelModel`, `EchoScope`, `EchoStabilityTests`, `EchoThermodynamics`, `EchoCNOBridge`, - `EchoEphapaxBridge`, + `EchoEphapaxBridge`, `EchoReversibilityBridge`, `EchoThermodynamicsFinite`, `EchoIntegration`, `EchoAccess`, `EchoCost`, `EchoCostInstance`, `EchoSearch`, `EchoSearchInstance`, `EchoExampleAbsInt`, `EchoExampleParser`, `EchoExampleProvenance`,