From 1b68038a84e10b298921965563e35b2426e734db Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 19:33:13 +0000 Subject: [PATCH] =?UTF-8?q?feat:=20EchoResidueCell=20=E2=80=94=20Agda=20mi?= =?UTF-8?q?rror=20of=20007's=20Holding/Spent=20once-only=20discipline?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit New `proofs/agda/EchoResidueCell.agda`: the Agda shadow of 007's `ResidueCell` (`proofs/idris2/EchoResidueLinear.idr`), the operational once-only half that `EchoReversibilityBridge` deferred as "runtime Holding/Spent bookkeeping". Under `--safe --without-K` the linear `(1 e)` quantity is unavailable, so once-only is enforced via the STATE MACHINE instead: - `ResidueCell f y = holding (Echo f y) | spent` - `takeForReverse : ResidueCell f y → Maybe A` (= the Idris partial form) - `consume` : Holding → Spent - `holding-reverses` / `spent-does-not-reverse` (↔ Idris `holdingReverses` / `spentDoesNotReverse`) - `once-only : takeForReverse (consume c) ≡ nothing` — the headline: after a reverse the cell is Spent, so a residue replays AT MOST ONCE. Honest scope: captures the once-PER-CELL discipline. Linear NON-DUPLICATION (nothing stops copying a `holding` cell) needs `@0`-style erasure and remains the documented next slice. `--safe --without-K`, zero postulates. Wired into All.agda, 7 headlines pinned in Smoke.agda, classified in echo-kernel-note.adoc + MAP.adoc (kernel-guard PASS). EchoResidueCell + Smoke.agda + All.agda all exit 0. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We --- docs/echo-types/MAP.adoc | 13 +++- docs/echo-types/echo-kernel-note.adoc | 2 +- proofs/agda/All.agda | 1 + proofs/agda/EchoResidueCell.agda | 89 +++++++++++++++++++++++++++ proofs/agda/Smoke.agda | 17 +++++ 5 files changed, 119 insertions(+), 3 deletions(-) create mode 100644 proofs/agda/EchoResidueCell.agda diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index 152163d..afbded1 100644 --- a/docs/echo-types/MAP.adoc +++ b/docs/echo-types/MAP.adoc @@ -483,9 +483,18 @@ postulates. `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`). +* Proofs: `proofs/agda/EchoResidueCell.agda` — the Agda mirror of 007's + `ResidueCell` (`holding` / `spent`) operational once-only discipline. + `takeForReverse : ResidueCell f y → Maybe A` (= the Idris partial form), + `consume` (Holding→Spent), `holding-reverses` / `spent-does-not-reverse` + (↔ Idris `holdingReverses` / `spentDoesNotReverse`), and the headline + `once-only` — after `consume`, a further `takeForReverse` is always + `nothing` (the state-machine form of the `(1 e)` linear consumption). * 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). + content, plus the once-PER-CELL replay discipline as a state machine. + 007's linear NON-DUPLICATION quantity `(1 e : Echo f y)` is NOT re-proved + in Agda (nothing stops copying a `holding` cell) — the full + quantity-semantics port (`@0`-style erasure) is the documented next slice. === Tropical / Dyadic `[REAL*]` Bridge domains enumerated in `docs/EchoBridges.md` (JanusKey / CNO / diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc index 8fc793d..f7cc508 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`, `EchoReversibilityBridge`, + `EchoEphapaxBridge`, `EchoReversibilityBridge`, `EchoResidueCell`, `EchoThermodynamicsFinite`, `EchoIntegration`, `EchoAccess`, `EchoCost`, `EchoCostInstance`, `EchoSearch`, `EchoSearchInstance`, `EchoExampleAbsInt`, `EchoExampleParser`, `EchoExampleProvenance`, diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 0efd576..7b06ec4 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -37,6 +37,7 @@ open import AntiEchoTropicalGeneric open import EchoIntegration open import EchoCNOBridge open import EchoReversibilityBridge +open import EchoResidueCell open import EchoApprox open import EchoApproxInstance diff --git a/proofs/agda/EchoResidueCell.agda b/proofs/agda/EchoResidueCell.agda new file mode 100644 index 0000000..696903b --- /dev/null +++ b/proofs/agda/EchoResidueCell.agda @@ -0,0 +1,89 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +-- +-- EchoResidueCell: the Agda mirror of 007's `ResidueCell` (Holding / Spent) +-- operational once-only reversal discipline, under --safe --without-K. +-- +-- 007's Layer-10 reversibility runtime (and its Idris2 spec +-- `proofs/idris2/EchoResidueLinear.idr`) represents an armed undo as a +-- `ResidueCell f y` that is either `Holding` a residue or `Spent`. +-- `takeForReverse` replays a Holding cell (recovering the input) and returns +-- `nothing` on a Spent cell; consuming a cell transitions it Holding → Spent, +-- so a residue reverses AT MOST ONCE. +-- +-- The Idris version enforces once-only via the LINEAR quantity `(1 e : Echo f +-- y)`. Agda has no such quantity under `--safe`, so this module enforces it +-- via the STATE MACHINE instead: `consume` makes the cell `Spent`, and +-- `once-only` proves that a second `takeForReverse` after `consume` is always +-- `nothing`. This is the operational half that `EchoReversibilityBridge` +-- deferred as "runtime Holding/Spent bookkeeping": the bridge's +-- `takeForReverse` is the *total* `Just`-branch (a bare `Echo f y → A`); here +-- it is the partial `ResidueCell f y → Maybe A` with the cell carrying the +-- Holding/Spent state. +-- +-- Honest scope: this captures the once-PER-CELL discipline operationally. It +-- does NOT model linear NON-DUPLICATION (nothing stops a caller copying a +-- `holding` cell before consuming) — that needs the `(1 e)` quantity / an +-- `@0`-style erasure encoding and remains the documented next slice. + +{-# OPTIONS --safe --without-K #-} + +module EchoResidueCell where + +open import Level using (Level; _⊔_) +open import Data.Product.Base using (proj₁) +open import Data.Maybe.Base using (Maybe; just; nothing) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +open import Echo using (Echo; echo-intro) + +private variable + a b : Level + A : Set a + B : Set b + +-- A residue cell over the visible output `y`: either `holding` an echo +-- residue, or `spent`. (= the Idris `ResidueCell`; `holding` takes a bare +-- `Echo f y` rather than a linear `(1 e)` — see the honest-scope note above.) +data ResidueCell {a b} {A : Set a} {B : Set b} (f : A → B) (y : B) + : Set (a ⊔ b) where + holding : Echo f y → ResidueCell f y + spent : ResidueCell f y + +-- Replay the cell: a `holding` cell yields the recovered input; a `spent` +-- cell yields `nothing`. (= the Idris `takeForReverse`.) +takeForReverse : {f : A → B} {y : B} → ResidueCell f y → Maybe A +takeForReverse (holding e) = just (proj₁ e) +takeForReverse spent = nothing + +-- Consuming a cell transitions `holding → spent` (`spent` stays `spent`). +-- This is the cell-state effect of a `reverse ` in 007. +consume : {f : A → B} {y : B} → ResidueCell f y → ResidueCell f y +consume (holding _) = spent +consume spent = spent + +-- A `holding` cell armed from `x` reverses to exactly `x` +-- (= Idris `holdingReverses`). +holding-reverses : (f : A → B) (x : A) → + takeForReverse (holding (echo-intro f x)) ≡ just x +holding-reverses f x = refl + +-- A `spent` cell never reverses (= Idris `spentDoesNotReverse`). +spent-does-not-reverse : {f : A → B} {y : B} → + takeForReverse {f = f} {y} spent ≡ nothing +spent-does-not-reverse = refl + +-- Consuming a `holding` cell spends it. +consume-spends : {f : A → B} {y : B} (e : Echo f y) → + consume (holding e) ≡ spent +consume-spends _ = refl + +-- THE once-only theorem: after consuming ANY cell, a further `takeForReverse` +-- is always `nothing` — a residue reverses at most once. This is the +-- state-machine form of the Idris `(1 e)` linear-consumption guarantee, and +-- the operational content of 007's cross-handler "once-only" property that +-- the rung-3b *static* check could only approximate by presence. +once-only : {f : A → B} {y : B} (c : ResidueCell f y) → + takeForReverse (consume c) ≡ nothing +once-only (holding _) = refl +once-only spent = refl diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index eccc1d2..bfd4bc3 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -107,6 +107,23 @@ open import EchoReversibilityBridge using ; no-recovery-once-dropped ) +-- EchoResidueCell — the Agda mirror of 007's `ResidueCell` (Holding/Spent) +-- operational once-only reversal discipline. `takeForReverse` replays a +-- `holding` cell / fails on `spent`; `consume` transitions Holding→Spent; +-- `once-only` is the headline — after `consume`, a further `takeForReverse` +-- is always `nothing` (the state-machine form of the Idris `(1 e)` linear +-- consumption). `holding-reverses` / `spent-does-not-reverse` mirror the +-- Idris `holdingReverses` / `spentDoesNotReverse`. +open import EchoResidueCell using + ( ResidueCell + ; takeForReverse + ; consume + ; holding-reverses + ; spent-does-not-reverse + ; consume-spends + ; once-only + ) + -- EchoNoSectionGeneric — raises the example-level -- `no-section-collapse-to-residue` to a uniform structural theorem. -- Generic headline `no-section-of-collapsing-map`: any collapsing