Add TransactionMutations module — instantiate no-section-of-collapsing-map for SQL transaction rollback safety (consumer: affinescript db-theory #2) #174

Context (consumer)

AffineScript has just shipped its db-theory #2 milestone in affinescript#526 — a new stdlib/Transaction.affine module exposing SQL transactions as an affine-bounded resource. Per owner directive 2026-06-01, every AffineScript proof must first audit echo-types, reuse if applicable, extend upstream with proofs if not, then cross-document.

The Transaction-safety obligations are stated in docs/academic/proofs/db-theory-2-transaction-safety.md, specifically:

• #DB-2.1 rollback-discards-writes — if a Tx is consumed by tx_rollback, every subsequent query answer matches the pre-tx_begin state (writes leak no observable signal).
• #DB-2.2 commit-promotes-writes — dual.
• #DB-2.3 savepoint-locality — nested rollback-to-savepoint discards writes since the savepoint, outer Tx remains live.

Audit summary

hyperpolymath/echo-types already carries the structural primitives:

1. EchoLinear.LEcho + weaken : LEcho linear → LEcho affine with no-section-weaken.
2. EchoSecurity.Security record + exit-collapses-at / audit-no-recovery-at.
3. EchoNoSectionGeneric.no-section-of-collapsing-map ← the generic lemma the Transaction proof reduces to.

What is missing: a Transaction-specific instantiation. The Security-record template is the natural shape, parameterised by the write-set carrier and the rollback receipt.

Proposed module shape

module TransactionMutations where

open import EchoNoSectionGeneric using (no-section-of)
open import EchoSecurity using (Security)

-- 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

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

-- The collapse map: every (WriteSet, RollbackLog) pair lands at trivial.
rollback-collapses-at :
  {T : Set} (ws : WriteSet T) → RollbackLog ws → Trivial
rollback-collapses-at _ _ = trivial

-- The headline lemma: no recovery of the discarded WriteSet from the
-- trivial receipt — instance of the existing generic no-section lemma.
rollback-discards-writes :
  {T : Set} (ws : WriteSet T) →
  no-section-of (rollback-collapses-at ws)
rollback-discards-writes ws = EchoNoSectionGeneric.no-section-of-collapsing-map _

A sibling TransactionSecurity.agda provides a Security instance:

TransactionSecurity : {T : Set} → WriteSet T → Security
TransactionSecurity ws = record
  { Resource          = WriteSet _
  ; Receipt           = RollbackLog ws
  ; exit              = rollback-collapses-at ws
  ; exit-collapses-at = rollback-discards-writes ws
  -- audit-no-recovery-at follows from the no-section reduction.
  }

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; the safety theorem closes the loop by saying that the one consumption that discards (rollback) is observationally equivalent to never having started.

This is Security-instantiation #1 outside the original region-exit audit setting — establishing the pattern that any bracketed-mutation resource (transactions, scoped capabilities, scoped logs) can reduce to the same generic lemma.

Acceptance criteria

• TransactionMutations.agda lands with WriteSet, RollbackLog, rollback-collapses-at, rollback-discards-writes definitions.
• TransactionSecurity.agda provides the Security instance, reduces to no-section-of-collapsing-map.
• No new axioms / postulates introduced (Print Assumptions clean).
• One-line entry in docs/echo-types/theorem-index.md (or wherever the audited-lemma list lives).
• Back-link: drop the resulting upstream commit SHA / module path into the affinescript cross-doc at docs/academic/proofs/db-theory-2-transaction-safety.md.

Non-scope

• Concrete commit/rollback semantics for any specific RDBMS — that lives in the consumer (affinescript) and ground-truth implementations (sqlite3, postgres, ...).
• The Mutation and Timestamp types — these are placeholder; the proof goes through with any inhabitable carrier. Choose whatever fits the existing echo-types convention.