<!-- SPDX-License-Identifier: MPL-2.0 -->
<!-- Copyright (c) 2026 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:

1. `EchoLinear.LEcho` + the `weaken : LEcho linear → LEcho affine` collapse map, with `no-section-weaken` proving no recovery after weakening.
2. `EchoSecurity.Security` record + `exit-collapses-at` / `audit-no-recovery-at` — the boundary-collapse template structurally mirrors rollback-discards-writes.
3. `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:

```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 + 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 [`hyperpolymath/echo-types#174`](https://github.com/hyperpolymath/echo-types/issues/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.
