|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | +-- SPDX-License-Identifier: MPL-2.0 |
| 3 | +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | + |
| 5 | +-- EchoTransaction: SQL transaction rollback safety as an instance of the |
| 6 | +-- generic no-section theorem. Closes echo-types#174 (consumer: |
| 7 | +-- affinescript db-theory #2, `stdlib/Transaction.affine`, |
| 8 | +-- `docs/academic/proofs/db-theory-2-transaction-safety.md` #DB-2.1). |
| 9 | +-- |
| 10 | +-- !! HONEST BOUND, STATED UP FRONT !! |
| 11 | +-- |
| 12 | +-- `rollback-discards-writes` is a TYPE-LEVEL guarantee that no pure Agda |
| 13 | +-- function reconstructs a discarded write-set from the rollback receipt |
| 14 | +-- alone (factored through |
| 15 | +-- `EchoNoSectionGeneric.no-section-of-collapsing-map`). It is NOT: |
| 16 | +-- * `durability` — a claim about writes surviving a crash; |
| 17 | +-- * `isolation` — a claim about concurrent-transaction visibility; |
| 18 | +-- * `commit-semantics` — #DB-2.2 commit-promotes-writes is the DUAL |
| 19 | +-- (commit PRESERVES writes, so it is not a |
| 20 | +-- no-section statement at all); |
| 21 | +-- * `savepoint-locality` — #DB-2.3 is a structural/runtime nesting |
| 22 | +-- claim outside this carrier; |
| 23 | +-- * `runtime-memory-zeroed` — a claim about physical memory contents. |
| 24 | +-- Conflating any of these with `rollback-discards-writes` is the category |
| 25 | +-- error the matched-negative block at the bottom heads off. Same |
| 26 | +-- honest-bound discipline as `EchoSecurity` / `RegionExitAudit` |
| 27 | +-- (R-2026-05-18). |
| 28 | +-- |
| 29 | +-- *Structural content (#DB-2.1).* A transaction's staged-but-uncommitted |
| 30 | +-- writes are an affine resource; `rollback` consumes that resource and |
| 31 | +-- emits a receipt that records only THAT a rollback occurred, never which |
| 32 | +-- writes were discarded. Two distinct write-sets therefore collapse to |
| 33 | +-- the same receipt, so `rollback` admits no section: a post-rollback |
| 34 | +-- caller holding only the receipt cannot type-check a function returning |
| 35 | +-- the discarded write-set. This is precisely "the one consumption that |
| 36 | +-- discards is observationally equivalent to never having started". |
| 37 | +-- |
| 38 | +-- This is the first `Security` instance outside the original region-exit |
| 39 | +-- audit setting (`EchoSecurity.region-exit-audit-instance`), establishing |
| 40 | +-- that any bracketed-mutation resource — transactions, scoped |
| 41 | +-- capabilities, scoped logs — reduces to the same generic lemma. |
| 42 | +-- |
| 43 | +-- Headlines (pinned in Smoke.agda): |
| 44 | +-- |
| 45 | +-- * Mutation / WriteSet / RollbackLog -- the carrier types |
| 46 | +-- * rollback -- the collapsing audit boundary |
| 47 | +-- * rollback-discards-writes -- #DB-2.1, direct no-section |
| 48 | +-- * transaction-security -- the `Security` instance |
| 49 | +-- * rollback-no-recovery -- #DB-2.1 via the abstract theorem |
| 50 | +-- |
| 51 | +-- Scope guardrail (Echo-vs-Σ clearance). `rollback-discards-writes` uses |
| 52 | +-- `no-section-of-collapsing-map` directly, whose three-line trans/sym/cong |
| 53 | +-- proof is the canonical non-trivial Echo-typed content; replacing it with |
| 54 | +-- a bare `Σ` + `_≡_` would lose the collapse/no-section content. The |
| 55 | +-- `NotProved-*` aliases pin the honest scope. |
| 56 | + |
| 57 | +module EchoTransaction where |
| 58 | + |
| 59 | +open import EchoNoSectionGeneric using (no-section-of-collapsing-map) |
| 60 | +open import EchoSecurity using (Security; module SecurityTheorems) |
| 61 | + |
| 62 | +open import Data.Nat.Base using (ℕ) |
| 63 | +open import Data.List.Base using (List; []; _∷_) |
| 64 | +open import Data.Product.Base using (Σ) |
| 65 | +open import Data.Unit.Base using (⊤; tt) |
| 66 | +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl) |
| 67 | +open import Relation.Nullary using (¬_) |
| 68 | + |
| 69 | +---------------------------------------------------------------------- |
| 70 | +-- The carrier. |
| 71 | +-- |
| 72 | +-- A `Mutation` is an opaque cell-write (address, value); a `WriteSet` is |
| 73 | +-- the ordered list a transaction has staged but not committed. The |
| 74 | +-- `RollbackLog` receipt is information-free: it records only that a |
| 75 | +-- rollback happened. |
| 76 | +---------------------------------------------------------------------- |
| 77 | + |
| 78 | +data Mutation : Set where |
| 79 | + set-cell : ℕ → ℕ → Mutation |
| 80 | + |
| 81 | +WriteSet : Set |
| 82 | +WriteSet = List Mutation |
| 83 | + |
| 84 | +data RollbackLog : Set where |
| 85 | + rolled-back : RollbackLog |
| 86 | + |
| 87 | +-- The audit boundary: rollback collapses every write-set to the single |
| 88 | +-- receipt, discarding the staged mutations. |
| 89 | +rollback : WriteSet → RollbackLog |
| 90 | +rollback _ = rolled-back |
| 91 | + |
| 92 | +---------------------------------------------------------------------- |
| 93 | +-- The audit witnesses: two distinct write-sets that collapse identically. |
| 94 | +---------------------------------------------------------------------- |
| 95 | + |
| 96 | +ws₁ ws₂ : WriteSet |
| 97 | +ws₁ = [] |
| 98 | +ws₂ = set-cell 0 1 ∷ [] |
| 99 | + |
| 100 | +ws₁≢ws₂ : ws₁ ≢ ws₂ |
| 101 | +ws₁≢ws₂ () |
| 102 | + |
| 103 | +rollback-collapses : rollback ws₁ ≡ rollback ws₂ |
| 104 | +rollback-collapses = refl |
| 105 | + |
| 106 | +---------------------------------------------------------------------- |
| 107 | +-- #DB-2.1 rollback-discards-writes (headline): no pure function |
| 108 | +-- reconstructs a discarded write-set from the rollback receipt alone. |
| 109 | +---------------------------------------------------------------------- |
| 110 | + |
| 111 | +rollback-discards-writes : |
| 112 | + ¬ Σ (RollbackLog → WriteSet) (λ recover → ∀ ws → recover (rollback ws) ≡ ws) |
| 113 | +rollback-discards-writes = |
| 114 | + no-section-of-collapsing-map rollback ws₁ ws₂ ws₁≢ws₂ rollback-collapses |
| 115 | + |
| 116 | +---------------------------------------------------------------------- |
| 117 | +-- The same guarantee as a `Security` instance, so the transaction |
| 118 | +-- carrier joins the EchoSecurity audience family. A single transaction |
| 119 | +-- scope is the (trivial) `RegionId`; `audit-no-recovery-at` re-derives |
| 120 | +-- #DB-2.1 through the abstract theorem, witnessing that the instance is |
| 121 | +-- real (not merely structurally similar). |
| 122 | +---------------------------------------------------------------------- |
| 123 | + |
| 124 | +transaction-security : Security |
| 125 | +transaction-security = record |
| 126 | + { RegionId = ⊤ |
| 127 | + ; Resource = λ _ → WriteSet |
| 128 | + ; Receipt = λ _ → RollbackLog |
| 129 | + ; exit = λ _ → rollback |
| 130 | + ; res₁ = λ _ → ws₁ |
| 131 | + ; res₂ = λ _ → ws₂ |
| 132 | + ; res-distinct = λ _ → ws₁≢ws₂ |
| 133 | + ; exit-collapses = λ _ → rollback-collapses |
| 134 | + } |
| 135 | + |
| 136 | +rollback-no-recovery : |
| 137 | + (r : ⊤) → |
| 138 | + ¬ Σ (RollbackLog → WriteSet) (λ recover → ∀ ws → recover (rollback ws) ≡ ws) |
| 139 | +rollback-no-recovery = SecurityTheorems.audit-no-recovery-at transaction-security |
| 140 | + |
| 141 | +---------------------------------------------------------------------- |
| 142 | +-- Matched-negative block (HONEST BOUND, per R-2026-05-18 discipline). |
| 143 | +-- |
| 144 | +-- `⊤`-aliased so `grep NotProved` catches them. A consumer citing |
| 145 | +-- `rollback-discards-writes` beyond these scopes is making a category |
| 146 | +-- error: the guarantee is exactly "no pure Agda function reconstructs |
| 147 | +-- the discarded write-set from the receipt alone, inside this model". |
| 148 | +---------------------------------------------------------------------- |
| 149 | + |
| 150 | +NotProved-durability : Set |
| 151 | +NotProved-durability = ⊤ |
| 152 | + |
| 153 | +NotProved-isolation : Set |
| 154 | +NotProved-isolation = ⊤ |
| 155 | + |
| 156 | +NotProved-commit-semantics : Set -- #DB-2.2 is the dual, not a no-section |
| 157 | +NotProved-commit-semantics = ⊤ |
| 158 | + |
| 159 | +NotProved-savepoint-locality : Set -- #DB-2.3 is structural/runtime |
| 160 | +NotProved-savepoint-locality = ⊤ |
| 161 | + |
| 162 | +NotProved-runtime-memory-zeroed : Set |
| 163 | +NotProved-runtime-memory-zeroed = ⊤ |
| 164 | + |
| 165 | +---------------------------------------------------------------------- |
| 166 | +-- Companion remark. |
| 167 | +-- |
| 168 | +-- #DB-2.2 (commit-promotes-writes) is the dual of #DB-2.1: commit |
| 169 | +-- PRESERVES the write-set, so it is an equality/section statement, not a |
| 170 | +-- no-section one — it belongs in a separate carrier and is deliberately |
| 171 | +-- not modelled here. #DB-2.3 (savepoint-locality) is a nesting/structural |
| 172 | +-- property of the transaction tree; it too is out of scope for this |
| 173 | +-- minimal rollback-safety carrier. The `Mutation` / `RollbackLog` types |
| 174 | +-- are placeholders chosen for inhabitability + a clean distinctness |
| 175 | +-- witness; the proof goes through for any carrier with two distinct |
| 176 | +-- write-sets collapsing to the same receipt. |
| 177 | +---------------------------------------------------------------------- |
0 commit comments