|
| 1 | +-- SPDX-License-Identifier: MPL-2.0 |
| 2 | +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | +-- |
| 4 | +-- EchoReversibilityBridge: the constructive discharge of the 007 language's |
| 5 | +-- Layer-10 reversibility (echo-residue) "phase-2" proof obligations against |
| 6 | +-- this library of record. |
| 7 | +-- |
| 8 | +-- 007 (https://github.com/hyperpolymath/007) models reversibility with an |
| 9 | +-- echo residue: `reversible as <name>` arms a residue cell holding an |
| 10 | +-- `Echo f y`, and `reverse <name>` consumes it to recover the input. Its |
| 11 | +-- Idris2 spec (`proofs/idris2/EchoResidue.idr`, |
| 12 | +-- `proofs/idris2/EchoResidueLinear.idr`) pins three obligations: |
| 13 | +-- |
| 14 | +-- 1. encode / decode round-trips — an irreversible `f` together with its |
| 15 | +-- residue is a total, reversible representation; |
| 16 | +-- 2. `reverseLinear : (1 e : Echo f y) → (x ** f x ≡ y)` — replaying a held |
| 17 | +-- residue recovers the input (the `Holding`/`takeForReverse = Just` |
| 18 | +-- branch of `ResidueCell`); |
| 19 | +-- 3. the linear discipline "affine capability, linear consumption" — the |
| 20 | +-- undo capability may be dropped (weakened) but, once dropped, the |
| 21 | +-- linear residue cannot be recovered (`Spent` does not reverse). |
| 22 | +-- |
| 23 | +-- This module re-states the *interface* those obligations describe and shows |
| 24 | +-- echo-types' own `Echo` / `EchoTotalCompletion` / `EchoLinear` satisfy it, |
| 25 | +-- under `--safe --without-K` with zero postulates. The Agda here is the |
| 26 | +-- source of truth; 007's Rust checker and Idris2 spec mirror this model. |
| 27 | + |
| 28 | +{-# OPTIONS --safe --without-K #-} |
| 29 | + |
| 30 | +module EchoReversibilityBridge where |
| 31 | + |
| 32 | +open import Level using (Level; _⊔_) |
| 33 | +open import Data.Product.Base using (Σ; _,_; proj₁) |
| 34 | +open import Function.Bundles using (_↔_; mk↔ₛ′) |
| 35 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
| 36 | +open import Relation.Nullary using (¬_) |
| 37 | + |
| 38 | +open import Echo using (Echo; echo-intro) |
| 39 | +open import EchoTotalCompletion using (encode; decode; decode-encode; encode-decode) |
| 40 | +open import EchoLinear using (linear; affine; LEcho; weaken; no-section-weaken) |
| 41 | + |
| 42 | +private variable |
| 43 | + a b : Level |
| 44 | + A : Set a |
| 45 | + B : Set b |
| 46 | + |
| 47 | +------------------------------------------------------------------------ |
| 48 | +-- Obligations 1 + 2: the reversible-completion interface, met by Echo. |
| 49 | +------------------------------------------------------------------------ |
| 50 | + |
| 51 | +-- The minimal data 007's reversibility model needs from a residue carrier: |
| 52 | +-- arm a residue from an input (`hold`), take-it-for-reverse to recover an |
| 53 | +-- input (`takeForReverse`), and the once-only correctness that replaying a |
| 54 | +-- freshly-armed residue returns the original input (`reverse-recovers`). |
| 55 | +-- |
| 56 | +-- `takeForReverse` here is the *total* `Just`-branch of 007's |
| 57 | +-- `takeForReverse : … → Maybe a`, i.e. `reverseLinear`'s witness extraction |
| 58 | +-- on a `Holding` cell; the `Maybe` wrapper is the runtime `Holding`/`Spent` |
| 59 | +-- bookkeeping, not part of the type-level correspondence. |
| 60 | +-- |
| 61 | +-- The residue carrier `Residue` is a parameter: an instance witnesses that a |
| 62 | +-- *particular* carrier (here `Echo f`) supports armed reversal. |
| 63 | +record ReversibleCompletion {a b} {A : Set a} {B : Set b} |
| 64 | + (f : A → B) (Residue : B → Set (a ⊔ b)) : Set (a ⊔ b) where |
| 65 | + field |
| 66 | + hold : (x : A) → Residue (f x) |
| 67 | + takeForReverse : {y : B} → Residue y → A |
| 68 | + reverse-recovers : (x : A) → takeForReverse (hold x) ≡ x |
| 69 | + |
| 70 | +-- echo-types' `Echo f` is such a carrier. `hold` is `echo-intro` (= 007's |
| 71 | +-- `encode` / the `Holding` cell); `takeForReverse` is the witness projection |
| 72 | +-- (= `reverseLinear`'s `fst`); recovery is `refl`, because |
| 73 | +-- `proj₁ (echo-intro f x) = proj₁ (x , refl) = x` definitionally. |
| 74 | +echo-reversible : (f : A → B) → ReversibleCompletion f (Echo f) |
| 75 | +echo-reversible f = record |
| 76 | + { hold = echo-intro f |
| 77 | + ; takeForReverse = proj₁ |
| 78 | + ; reverse-recovers = λ _ → refl |
| 79 | + } |
| 80 | + |
| 81 | +-- 007's narrative slogan — "an irreversible computation together with its |
| 82 | +-- echo residue is a reversible representation" — is exactly echo-types' |
| 83 | +-- totality iso read in the residue→input direction: the total echo space |
| 84 | +-- `Σ B (Echo f)` recovers the domain `A`. (The A→Σ direction is |
| 85 | +-- `EchoTotalCompletion.A↔ΣEcho`; this is its symmetric partner.) |
| 86 | +reversibility-via-totality : (f : A → B) → Σ B (Echo f) ↔ A |
| 87 | +reversibility-via-totality f = |
| 88 | + mk↔ₛ′ (decode f) (encode f) (decode-encode f) (encode-decode f) |
| 89 | + |
| 90 | +------------------------------------------------------------------------ |
| 91 | +-- Obligation 3: the phase-2 linear discipline. |
| 92 | +------------------------------------------------------------------------ |
| 93 | + |
| 94 | +-- "Affine capability": a live (linear) undo residue may always be weakened |
| 95 | +-- to an affine one — the capability dropped. Never an error in 007. |
| 96 | +capability-can-be-dropped : LEcho linear → LEcho affine |
| 97 | +capability-can-be-dropped = weaken |
| 98 | + |
| 99 | +-- "Linear consumption / Spent-does-not-reverse": there is NO section of |
| 100 | +-- `weaken` — once the residue is degraded (the undo dropped, the cell |
| 101 | +-- `Spent`) the linear residue cannot be recovered. This is echo-types' |
| 102 | +-- `no-section-weaken`, the library-of-record discharge of the irreversibility |
| 103 | +-- of dropping the capability. |
| 104 | +no-recovery-once-dropped : |
| 105 | + ¬ (Σ (LEcho affine → LEcho linear) |
| 106 | + (λ raise → ∀ e → raise (weaken e) ≡ e)) |
| 107 | +no-recovery-once-dropped = no-section-weaken |
0 commit comments