// SPDX-License-Identifier: CC-BY-SA-4.0
// SPDX-FileCopyrightText: 2024-2026 hyperpolymath (Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>)
= DB-Theory ++#++2 — Transaction Safety (Rollback-Discards-Writes)

*Status*: Carrier wired (`stdlib/Transaction.affine`, codegen, Deno-ESM
smoke); formal proof obligation *pending upstream against
`hyperpolymath/echo-types`*.

== 1. The obligation

Let `Tx` be the opaque affine handle returned by `tx++_++begin(d: Db)`
in `stdlib/Transaction.affine`. Let `t : Tx` be such a handle, and let
`σ₀` be the database state immediately before `tx++_++begin(d)`. Let `W`
be the multiset of mutating SQL statements (`INSERT`, `UPDATE`,
`DELETE`, schema mutations) executed against `d` (or any handle aliased
through `tx++_++db(t)`) between `tx++_++begin(d)` and the consumption of
`t`.

*Safety property ++#++DB-2.1 (rollback-discards-writes)*: if `t` is
consumed by `tx++_++rollback(t)`, then for every query `q` issued
against `d` _after_ the rollback, the answer to `q` is precisely the
answer it would have had over `σ₀` (i.e. as if `W` had never happened).

*Safety property ++#++DB-2.2 (commit-promotes-writes)*: if `t` is
consumed by `tx++_++commit(t)`, then for every query `q` issued after
the commit, the answer is the same as serially applying `W` to `σ₀`.

*Safety property ++#++DB-2.3 (savepoint locality)*: if a savepoint `s`
is opened with `tx++_++savepoint(t, s)`, mutations `W++_++s` are issued,
and then `tx++_++rollback++_++to(t, s)` is called, the database state
mid-transaction reverts to the state at `tx++_++savepoint(t, s)` while
leaving the outer transaction live.

== 2. Echo-types audit (2026-06-01)

Per owner directive, every proof in AffineScript must first audit
`hyperpolymath/echo-types`, reuse if applicable, extend upstream *with
proofs* if not, then cross-document.

*Audit finding* (full report under
`tasklist/sub-agent reports/2026-06-01-transaction-echo-audit`):
echo-types has no Transaction-specific instantiation today, but carries
three reusable abstractions:

[arabic]
. `EchoLinear.LEcho` {plus} the `weaken : LEcho linear → LEcho affine`
collapse map, with `no-section-weaken` proving no recovery after
weakening.
. `EchoSecurity.Security` record {plus} `exit-collapses-at` /
`audit-no-recovery-at` — the boundary-collapse template structurally
mirrors rollback-discards-writes.
. `EchoNoSectionGeneric.no-section-of-collapsing-map` — the generic
lemma the Transaction proof reduces to.

== 3. Proposed upstream extension

A new module `TransactionMutations.agda` in echo-types, structured as
follows:

[source,agda]
----
module TransactionMutations where

-- The write-set carrier: an opaque set of mutations parametrised by
-- the table-type T being mutated.
record WriteSet (T : Set) : Set where
  field
    applied : List Mutation     -- audit trail
    -- Algebra: `empty`, `append`, `compose` give a monoid action on
    -- DbState — the action and its laws are deferred to a separate
    -- module to keep this carrier import-light.

-- The rollback log is the witness that a WriteSet was discarded.
record RollbackLog {T : Set} (ws : WriteSet T) : Set where
  field
    discarded-at : Timestamp
    -- The trivial receipt: rollback emits no recoverable signal.
    receipt : Trivial

-- The collapse map that powers the safety proof: every WriteSet
-- rolls back to the trivial receipt, and the generic
-- no-section-of-collapsing-map (already in echo-types) gives the
-- no-recovery lemma free.
rollback-collapses-at :
  {T : Set} (ws : WriteSet T) → RollbackLog ws → Trivial
rollback-collapses-at _ _ = trivial

rollback-discards-writes :
  {T : Set} (ws : WriteSet T) →
  EchoNoSectionGeneric.no-section-of (rollback-collapses-at ws)
rollback-discards-writes ws = no-section-of-collapsing-map _
----

The Security-record instance lives in a sibling
`TransactionSecurity.agda`, parametrising `EchoSecurity.Security` by
`(Resource := WriteSet T)`, `(Receipt := RollbackLog ws)`,
`(exit := rollback-collapses-at ws)`.

== 4. Cross-doc seam

* AffineScript stdlib: `stdlib/Transaction.affine` carries the safety
obligation statement in its module-level docstring and references this
file by name.
* AffineScript codegen {plus} smoke: `lib/codegen++_++deno.ml` and
`tests/codegen-deno/transaction++_++smoke.++{++affine,harness.mjs}`
_witness_ the property at the Node runtime level by snapshotting tables
on `txBegin` and restoring on `txRollback`. The witness is not a proof —
it’s an executable check that the runtime mock observes the same
invariant the formal proof will eventually establish.
* Echo-types upstream: tracked at
https://github.com/hyperpolymath/echo-types/issues/174[`hyperpolymath/echo-types++#++174`]
— proposes the new `TransactionMutations.agda` module shape (and sibling
`TransactionSecurity.agda` providing the `Security` instance) reducing
to the existing `EchoNoSectionGeneric.no-section-of-collapsing-map`.
Acceptance criteria include zero new axioms (`Print Assumptions` clean)
and a back-link from the upstream commit SHA into this document.

== 5. Why this matters

Transactions are the canonical user-facing application of affine
resource discipline to data: the type system already enforces "`at most
one consumption`" of `Tx`, and the safety theorem closes the loop by
saying that the _one_ consumption that discards (rollback) is
observationally equivalent to never having started. This is the proof
every database textbook assumes — having it mechanised against an
echo-types carrier means AffineScript’s transaction surface inherits the
same "`no recovery from boundary collapse`" story echo-types already
proves for region-exit auditing.
