|
| 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 | +-- EchoResidueCell: the Agda mirror of 007's `ResidueCell` (Holding / Spent) |
| 5 | +-- operational once-only reversal discipline, under --safe --without-K. |
| 6 | +-- |
| 7 | +-- 007's Layer-10 reversibility runtime (and its Idris2 spec |
| 8 | +-- `proofs/idris2/EchoResidueLinear.idr`) represents an armed undo as a |
| 9 | +-- `ResidueCell f y` that is either `Holding` a residue or `Spent`. |
| 10 | +-- `takeForReverse` replays a Holding cell (recovering the input) and returns |
| 11 | +-- `nothing` on a Spent cell; consuming a cell transitions it Holding → Spent, |
| 12 | +-- so a residue reverses AT MOST ONCE. |
| 13 | +-- |
| 14 | +-- The Idris version enforces once-only via the LINEAR quantity `(1 e : Echo f |
| 15 | +-- y)`. Agda has no such quantity under `--safe`, so this module enforces it |
| 16 | +-- via the STATE MACHINE instead: `consume` makes the cell `Spent`, and |
| 17 | +-- `once-only` proves that a second `takeForReverse` after `consume` is always |
| 18 | +-- `nothing`. This is the operational half that `EchoReversibilityBridge` |
| 19 | +-- deferred as "runtime Holding/Spent bookkeeping": the bridge's |
| 20 | +-- `takeForReverse` is the *total* `Just`-branch (a bare `Echo f y → A`); here |
| 21 | +-- it is the partial `ResidueCell f y → Maybe A` with the cell carrying the |
| 22 | +-- Holding/Spent state. |
| 23 | +-- |
| 24 | +-- Honest scope: this captures the once-PER-CELL discipline operationally. It |
| 25 | +-- does NOT model linear NON-DUPLICATION (nothing stops a caller copying a |
| 26 | +-- `holding` cell before consuming) — that needs the `(1 e)` quantity / an |
| 27 | +-- `@0`-style erasure encoding and remains the documented next slice. |
| 28 | + |
| 29 | +{-# OPTIONS --safe --without-K #-} |
| 30 | + |
| 31 | +module EchoResidueCell where |
| 32 | + |
| 33 | +open import Level using (Level; _⊔_) |
| 34 | +open import Data.Product.Base using (proj₁) |
| 35 | +open import Data.Maybe.Base using (Maybe; just; nothing) |
| 36 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
| 37 | + |
| 38 | +open import Echo using (Echo; echo-intro) |
| 39 | + |
| 40 | +private variable |
| 41 | + a b : Level |
| 42 | + A : Set a |
| 43 | + B : Set b |
| 44 | + |
| 45 | +-- A residue cell over the visible output `y`: either `holding` an echo |
| 46 | +-- residue, or `spent`. (= the Idris `ResidueCell`; `holding` takes a bare |
| 47 | +-- `Echo f y` rather than a linear `(1 e)` — see the honest-scope note above.) |
| 48 | +data ResidueCell {a b} {A : Set a} {B : Set b} (f : A → B) (y : B) |
| 49 | + : Set (a ⊔ b) where |
| 50 | + holding : Echo f y → ResidueCell f y |
| 51 | + spent : ResidueCell f y |
| 52 | + |
| 53 | +-- Replay the cell: a `holding` cell yields the recovered input; a `spent` |
| 54 | +-- cell yields `nothing`. (= the Idris `takeForReverse`.) |
| 55 | +takeForReverse : {f : A → B} {y : B} → ResidueCell f y → Maybe A |
| 56 | +takeForReverse (holding e) = just (proj₁ e) |
| 57 | +takeForReverse spent = nothing |
| 58 | + |
| 59 | +-- Consuming a cell transitions `holding → spent` (`spent` stays `spent`). |
| 60 | +-- This is the cell-state effect of a `reverse <name>` in 007. |
| 61 | +consume : {f : A → B} {y : B} → ResidueCell f y → ResidueCell f y |
| 62 | +consume (holding _) = spent |
| 63 | +consume spent = spent |
| 64 | + |
| 65 | +-- A `holding` cell armed from `x` reverses to exactly `x` |
| 66 | +-- (= Idris `holdingReverses`). |
| 67 | +holding-reverses : (f : A → B) (x : A) → |
| 68 | + takeForReverse (holding (echo-intro f x)) ≡ just x |
| 69 | +holding-reverses f x = refl |
| 70 | + |
| 71 | +-- A `spent` cell never reverses (= Idris `spentDoesNotReverse`). |
| 72 | +spent-does-not-reverse : {f : A → B} {y : B} → |
| 73 | + takeForReverse {f = f} {y} spent ≡ nothing |
| 74 | +spent-does-not-reverse = refl |
| 75 | + |
| 76 | +-- Consuming a `holding` cell spends it. |
| 77 | +consume-spends : {f : A → B} {y : B} (e : Echo f y) → |
| 78 | + consume (holding e) ≡ spent |
| 79 | +consume-spends _ = refl |
| 80 | + |
| 81 | +-- THE once-only theorem: after consuming ANY cell, a further `takeForReverse` |
| 82 | +-- is always `nothing` — a residue reverses at most once. This is the |
| 83 | +-- state-machine form of the Idris `(1 e)` linear-consumption guarantee, and |
| 84 | +-- the operational content of 007's cross-handler "once-only" property that |
| 85 | +-- the rung-3b *static* check could only approximate by presence. |
| 86 | +once-only : {f : A → B} {y : B} (c : ResidueCell f y) → |
| 87 | + takeForReverse (consume c) ≡ nothing |
| 88 | +once-only (holding _) = refl |
| 89 | +once-only spent = refl |
0 commit comments