named_reversibility.007

-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
--
-- Example: named reversibility (Layer 10 phase 3, rung 3a).
--
-- `reversible as <name> { ... }` binds this block's echo residue to a name;
-- a later `reverse <name>` in the SAME body replays it, consuming it exactly
-- once. This is the named counterpart to the anonymous `reversible {}` /
-- `reverse {}` forms (see reversibility.007), and is fully statically checked:
--
--   * a second `reverse undo` is a compile-time error (the residue is a linear
--     undo-capability, replayable at most once);
--   * never replaying a bound residue is NOT an error (it is affine — an undo
--     capability may simply go unused);
--   * a `reverse undo` with no matching `reversible as undo` in the same body
--     is the reverse-without-residue error.
--
-- Mechanised model: proofs/idris2/EchoResidueLinear.idr (ResidueCell
-- Holding/Spent); see spec/TYPE-SYSTEM-SPEC.adoc §11b.5.

agent NamedReversal {
    control {
        on receive(amount: Int) {
            -- Bind this block's echo residue to `undo`.
            reversible as undo {
                let snapshot = amount
            }

            -- ... later, in the same handler, replay it by name.
            reverse undo
        }
    }
}