transactional_rollback.007

-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
--
-- Example: L10 rung-3b runtime half — echo-residue cells + runtime replay.
--
-- `reverse <name>` now has an operational meaning: restore the agent to the
-- checkpoint captured by the matching `reversible as <name>`. The residue
-- channel is made explicit with a `residue <name>` agent member.
--
-- Runtime semantics (evaluator):
--   * `reversible as undo { ... }` captures a BEFORE-IMAGE DELTA of just the
--     fields its body mutates (`balance`) *before* the body runs (storing it as
--     a `Holding` cell keyed `undo`), then runs the body;
--   * `reverse undo` WRITES BACK those captured fields and marks the cell
--     `Spent`; a second `reverse undo` finds `Spent` and is a no-op (replay at
--     most once, the runtime witness of the Idris `takeForReverse : ... -> Maybe`).
--
-- The cell lives on the agent instance, so a delta captured in `debit` is
-- restorable by `reverse undo` in the *separate* `rollback` handler — the
-- cross-handler reversal the rung-3b static half could only check by presence.
--
-- Per-variable delta semantics: `reverse` restores only the fields the body
-- touched, leaving unrelated state (and intervening `set`s by other handlers)
-- intact. See TYPE-SYSTEM-SPEC §11b.8.

agent Transactional {
    -- Mutable agent state (§11b.7) is the substrate the residue cell snapshots.
    state balance: Int = 100

    -- Declare the residue cell explicitly (the "explicit state cell" design).
    residue undo

    control {
        -- Debit checkpoints the pre-debit balance under `undo`, then mutates.
        on debit(amount: Int) {
            reversible as undo {
                set balance = balance - amount
            }
        }

        -- Rollback replays the checkpoint, restoring `balance` to its
        -- pre-debit value — even though it ran in a different handler.
        on rollback(ignored: Int) {
            reverse undo
        }
    }
}