proofs: db-theory carriers (#174, #176) + Veblen least-fixed-point rung

docs/echo-types/MAP.adoc

@@ -253,6 +253,24 @@ honest-bound matched-negative block.
   the `affine` mode in `EchoObservationalEquivalence`. Honest-bound:
   NOT side-channel-safe / cryptographic deniability / adaptive
   adversary. `proofs/agda/EchoDeniability.agda`. `[REAL]`
+* *Transaction (rollback safety, issue #174)* — `WriteSet` (staged
+  mutations) → `RollbackLog` collapsing audit boundary; `rollback`
+  admits no section, so a discarded write-set is unrecoverable from the
+  receipt alone (#DB-2.1). Packaged as a `Security` instance
+  (`transaction-security`), reducing to `no-section-of-collapsing-map`.
+  Honest-bound: NOT durability / isolation / commit-semantics (the
+  dual) / savepoint-locality / runtime-memory-zeroed.
+  `proofs/agda/EchoTransaction.agda`. `[REAL]`
+* *Selective projection (σ–π commutativity, issue #176)* — the Codd law
+  σ_p(π_S(R)) = π_S(σ_p(R)) for column-safe predicates, as an Echo-fibre
+  set-equality (`_⇔_` of the two result relations per projected value).
+  `SelectiveProjection` carries the column-safe factoring `p b ⇔ q
+  (projection b)`; `select-project-commute` is the commutativity;
+  `no-column-safe-lift` is the counterexample (a projected-away-column
+  predicate has no column-restricted lift, so σ/π do not commute).
+  Honest-bound: `_⇔_` is set-equality (full `_↔_` would need
+  proof-irrelevant predicates); NOT a runtime query planner.
+  `proofs/agda/EchoSelectiveProjection.agda`. `[REAL]`
 * *Aggregation (general, issue #175)* — aggregation-as-fold over a
   `Monoid`, with a `GroupAggregator` and the monoid-homomorphism law
   `aggregation-as-fold` (aggregating a concatenation = combining the

docs/echo-types/echo-kernel-note.adoc

@@ -125,7 +125,8 @@ kernel** — the boundary is real and lives outside this core.
   *Application/extension modules* (also added via the same sweep):
   `EchoEntropy`, `EchoLLEncoding`, `EchoProvenance`, `EchoSecurity`,
   `EchoProbabilisticSupport`, `EchoDifferential`, `EchoDeniability`,
-  `EchoAggregation`, `EchoVariance`
+  `EchoAggregation`, `EchoVariance`, `EchoTransaction`,
+  `EchoSelectiveProjection`
   are derived domain applications mapped under their own headings in
   MAP.adoc.  `EchoDeniability` formalises residue deniability: the
   perfect (constant / no-section) case and the partial (injective /

proofs/agda/All.agda

@@ -96,6 +96,8 @@ open import EchoDifferential     -- Perturbation tracking (audience-facing sensi
 -- and the injective/section-exists story (partial case), with the
 -- IsConstantOpener boundary tying deniability to the affine mode.
 open import EchoDeniability
+open import EchoTransaction      -- Transaction rollback safety (issue #174; Security instance)
+open import EchoSelectiveProjection  -- σ–π commutativity (issue #176; relational-algebra carrier)
 
 -- Narrative deliverable: curated index of "why Echo deserves a name".
 open import EchoCanonicalIdentitySuite
@@ -127,6 +129,7 @@ open import Ordinal.Brouwer.VeblenPhiNormal -- φ₁ a normal function; next-ε
 open import Ordinal.Brouwer.VeblenBinary    -- binary Veblen φ_α(β) + the diagonal Γ₀
 open import Ordinal.Brouwer.VeblenBinaryNormal -- every φ_α a normal function; φ_{α+1} enumerates fixed points of φ_α
 open import Ordinal.Brouwer.VeblenBinaryMono -- first-arg monotonicity; Γ₀ ≤′ φ_Γ₀(0) (diagonal pre-fixed point)
+open import Ordinal.Brouwer.VeblenBinaryLeast -- nextFix is the LEAST pre-fixed point; reverse-Γ₀ reduced to one closure
 open import Ordinal.Brouwer.StrictLeftMonoRefuted
 open import Ordinal.Brouwer.AdditivePrincipalGenericRefuted
 open import Ordinal.Buchholz.Syntax

proofs/agda/EchoSelectiveProjection.agda

@@ -0,0 +1,164 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+-- EchoSelectiveProjection: the relational-algebra selection/projection
+-- commutativity (the subset case) as an Echo-fibre statement. Closes
+-- echo-types#174's sibling echo-types#176 (consumer: affinescript
+-- db-theory #4, `stdlib/Select.affine`).
+--
+-- The classical law (Codd): for selection σ_p (predicate-driven row
+-- filter) and projection π_S (column-subset),
+--
+--     σ_p(π_S(R)) = π_S(σ_p(R))   when p references only columns in S,
+--     σ_p(π_S(R)) ≠ π_S(σ_p(R))   when p references a column NOT in S.
+--
+-- *Honest level.* "=" between relations is SET equality: same rows.
+-- The Echo formalisation states it as a per-projected-value LOGICAL
+-- equivalence `_⇔_` of the two result fibres (co-membership), which is
+-- exactly set-equality of the result relations. A full `_↔_` (with
+-- round-trips) would additionally require the predicate family to be
+-- proof-irrelevant (`is-prop`); set-equality does not, and `_⇔_` is the
+-- faithful level. See the companion remark.
+--
+-- *The column-safe condition.* "p references only columns in S" is
+-- formalised as: p factors through the projection — there is a
+-- predicate `q : S → Set` on the projected columns with `p b ⇔ q
+-- (projection b)` for every record `b`. This `factors` field IS the
+-- "uses only columns in S" hypothesis.
+--
+-- *The Echo content.* With `pf = projection ∘ f` (the projected map),
+-- `Echo pf s` is π_S(R) at projected value `s` — the rows projecting to
+-- `s`. The two composites:
+--
+--   ProjectSelect s  =  Σ (Echo pf s) (λ e → p (f (proj₁ e)))
+--       -- π_S(σ_p(R)) at s: rows projecting to s that satisfy p
+--   SelectProject s  =  Σ (Echo pf s) (λ _ → q s)
+--       -- σ_q(π_S(R)) at s: rows projecting to s, kept iff q holds at s
+--
+-- `select-project-commute` is `∀ s → ProjectSelect s ⇔ SelectProject s`.
+-- The proof is K-free: pattern-matching the fibre witness `pf x ≡ s` as
+-- `refl` (s a free variable, so --without-K-safe) collapses the
+-- transport, and the predicate move is exactly the `factors` field.
+--
+-- *The counterexample.* `no-column-safe-lift` shows a predicate that
+-- reads a projected-away column (`proj₂`, with projection `= proj₁`)
+-- admits NO column-restricted lift `q` at all: the records `(true,true)`
+-- and `(true,false)` share projection `true` but disagree on the
+-- predicate, so any `q true` would be both inhabited and empty. This is
+-- the "≠" direction: σ and π do not commute for such a predicate.
+--
+-- Headlines (pinned in Smoke.agda):
+--   * SelectiveProjection        -- the column-safe setup record
+--   * select-project-commute     -- σ–π commute (column-safe), per s
+--   * column-safe-example        -- worked column-safe instance
+--   * no-column-safe-lift        -- counterexample (non-column-safe ⇒ ✗)
+
+module EchoSelectiveProjection where
+
+open import Echo                  using (Echo)
+open import Data.Product.Base    using (Σ; _,_; proj₁; proj₂; _×_)
+open import Data.Bool.Base       using (Bool; true; false)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Nullary     using (¬_)
+
+----------------------------------------------------------------------
+-- Logical equivalence (set-equality level). Kept local and minimal —
+-- the σ–π law is co-membership of the two result relations, not a
+-- structure-carrying bijection.
+----------------------------------------------------------------------
+
+record _⇔_ (P Q : Set) : Set where
+  constructor equiv
+  field
+    to   : P → Q
+    from : Q → P
+
+----------------------------------------------------------------------
+-- The column-safe selection/projection setup.
+----------------------------------------------------------------------
+
+record SelectiveProjection {A B : Set} (f : A → B) (S : Set) : Set₁ where
+  field
+    projection : B → S          -- π_S
+    p          : B → Set        -- σ predicate on full records
+    q          : S → Set        -- its restriction to the projected columns
+    -- "p uses only columns in S": p factors through projection as q.
+    factors    : ∀ b → p b ⇔ q (projection b)
+
+  -- The projected map; `Echo pf s` = π_S(R) at projected value s.
+  pf : A → S
+  pf a = projection (f a)
+
+  -- π_S(σ_p(R)) at s : rows projecting to s that satisfy p.
+  ProjectSelect : S → Set
+  ProjectSelect s = Σ (Echo pf s) (λ e → p (f (proj₁ e)))
+
+  -- σ_q(π_S(R)) at s : rows projecting to s, kept iff q holds at s.
+  SelectProject : S → Set
+  SelectProject s = Σ (Echo pf s) (λ _ → q s)
+
+----------------------------------------------------------------------
+-- σ–π commute (column-safe): the two result relations co-inhabit at
+-- every projected value. Set-equality of σ_p(π_S(R)) and π_S(σ_p(R)).
+----------------------------------------------------------------------
+
+select-project-commute :
+  ∀ {A B : Set} {f : A → B} {S : Set} (sp : SelectiveProjection f S) (s : S) →
+  SelectiveProjection.ProjectSelect sp s ⇔ SelectiveProjection.SelectProject sp s
+select-project-commute {f = f} sp s = equiv to from
+  where
+    open SelectiveProjection sp
+    to : ProjectSelect s → SelectProject s
+    to ((x , refl) , pe) = (x , refl) , _⇔_.to (factors (f x)) pe
+    from : SelectProject s → ProjectSelect s
+    from ((x , refl) , qs) = (x , refl) , _⇔_.from (factors (f x)) qs
+
+----------------------------------------------------------------------
+-- Worked column-safe instance: 2-column Bool records, project to
+-- column 0, predicate "column 0 is true" — uses only the projected
+-- column, so it factors (the identity equivalence).
+----------------------------------------------------------------------
+
+column-safe-example : SelectiveProjection {Bool × Bool} {Bool × Bool} (λ b → b) Bool
+column-safe-example = record
+  { projection = proj₁
+  ; p          = λ b → proj₁ b ≡ true
+  ; q          = λ s → s ≡ true
+  ; factors    = λ b → equiv (λ z → z) (λ z → z)
+  }
+
+----------------------------------------------------------------------
+-- Counterexample (the "≠" direction): a predicate reading a
+-- projected-away column has NO column-restricted lift. `(true,true)`
+-- and `(true,false)` share projection `true` but disagree on
+-- `proj₂ · ≡ true`, so any candidate `q true` is both inhabited and
+-- empty. Hence σ and π do not commute for such a predicate.
+----------------------------------------------------------------------
+
+no-column-safe-lift :
+  ¬ Σ (Bool → Set) (λ q → ∀ b → (proj₂ b ≡ true) ⇔ q (proj₁ b))
+no-column-safe-lift (q , fac)
+  with _⇔_.from (fac (true , false)) (_⇔_.to (fac (true , true)) refl)
+... | ()
+
+----------------------------------------------------------------------
+-- Companion remark.
+--
+-- `_⇔_` (set-equality of the result relations) is the faithful level:
+-- relational-algebra equality is membership equality. Upgrading to a
+-- structure-preserving `_↔_` would need the predicate family to be
+-- proof-irrelevant (an `is-prop (p b)` field); under `--safe
+-- --without-K` that is an extra hypothesis, not free, and it adds no
+-- relational-algebra content. NOT claimed: σ–π commutativity for
+-- arbitrary (non-column-safe) predicates (refuted by
+-- `no-column-safe-lift`); any runtime query-planner behaviour (the
+-- decision of whether a predicate is column-safe lives in the
+-- consumer). The carrier encodes only the property.
+----------------------------------------------------------------------
+
+NotProved-arbitrary-predicate-commute : Set
+NotProved-arbitrary-predicate-commute = Bool
+
+NotProved-runtime-query-planner : Set
+NotProved-runtime-query-planner = Bool

proofs/agda/EchoTransaction.agda

@@ -0,0 +1,177 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+-- EchoTransaction: SQL transaction rollback safety as an instance of the
+-- generic no-section theorem. Closes echo-types#174 (consumer:
+-- affinescript db-theory #2, `stdlib/Transaction.affine`,
+-- `docs/academic/proofs/db-theory-2-transaction-safety.md` #DB-2.1).
+--
+-- !! HONEST BOUND, STATED UP FRONT !!
+--
+-- `rollback-discards-writes` is a TYPE-LEVEL guarantee that no pure Agda
+-- function reconstructs a discarded write-set from the rollback receipt
+-- alone (factored through
+-- `EchoNoSectionGeneric.no-section-of-collapsing-map`). It is NOT:
+--   * `durability`       — a claim about writes surviving a crash;
+--   * `isolation`        — a claim about concurrent-transaction visibility;
+--   * `commit-semantics` — #DB-2.2 commit-promotes-writes is the DUAL
+--                          (commit PRESERVES writes, so it is not a
+--                          no-section statement at all);
+--   * `savepoint-locality` — #DB-2.3 is a structural/runtime nesting
+--                          claim outside this carrier;
+--   * `runtime-memory-zeroed` — a claim about physical memory contents.
+-- Conflating any of these with `rollback-discards-writes` is the category
+-- error the matched-negative block at the bottom heads off. Same
+-- honest-bound discipline as `EchoSecurity` / `RegionExitAudit`
+-- (R-2026-05-18).
+--
+-- *Structural content (#DB-2.1).* A transaction's staged-but-uncommitted
+-- writes are an affine resource; `rollback` consumes that resource and
+-- emits a receipt that records only THAT a rollback occurred, never which
+-- writes were discarded. Two distinct write-sets therefore collapse to
+-- the same receipt, so `rollback` admits no section: a post-rollback
+-- caller holding only the receipt cannot type-check a function returning
+-- the discarded write-set. This is precisely "the one consumption that
+-- discards is observationally equivalent to never having started".
+--
+-- This is the first `Security` instance outside the original region-exit
+-- audit setting (`EchoSecurity.region-exit-audit-instance`), establishing
+-- that any bracketed-mutation resource — transactions, scoped
+-- capabilities, scoped logs — reduces to the same generic lemma.
+--
+-- Headlines (pinned in Smoke.agda):
+--
+--   * Mutation / WriteSet / RollbackLog  -- the carrier types
+--   * rollback                           -- the collapsing audit boundary
+--   * rollback-discards-writes           -- #DB-2.1, direct no-section
+--   * transaction-security               -- the `Security` instance
+--   * rollback-no-recovery               -- #DB-2.1 via the abstract theorem
+--
+-- Scope guardrail (Echo-vs-Σ clearance). `rollback-discards-writes` uses
+-- `no-section-of-collapsing-map` directly, whose three-line trans/sym/cong
+-- proof is the canonical non-trivial Echo-typed content; replacing it with
+-- a bare `Σ` + `_≡_` would lose the collapse/no-section content. The
+-- `NotProved-*` aliases pin the honest scope.
+
+module EchoTransaction where
+
+open import EchoNoSectionGeneric using (no-section-of-collapsing-map)
+open import EchoSecurity         using (Security; module SecurityTheorems)
+
+open import Data.Nat.Base   using (ℕ)
+open import Data.List.Base  using (List; []; _∷_)
+open import Data.Product.Base using (Σ)
+open import Data.Unit.Base  using (⊤; tt)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
+open import Relation.Nullary using (¬_)
+
+----------------------------------------------------------------------
+-- The carrier.
+--
+-- A `Mutation` is an opaque cell-write (address, value); a `WriteSet` is
+-- the ordered list a transaction has staged but not committed. The
+-- `RollbackLog` receipt is information-free: it records only that a
+-- rollback happened.
+----------------------------------------------------------------------
+
+data Mutation : Set where
+  set-cell : ℕ → ℕ → Mutation
+
+WriteSet : Set
+WriteSet = List Mutation
+
+data RollbackLog : Set where
+  rolled-back : RollbackLog
+
+-- The audit boundary: rollback collapses every write-set to the single
+-- receipt, discarding the staged mutations.
+rollback : WriteSet → RollbackLog
+rollback _ = rolled-back
+
+----------------------------------------------------------------------
+-- The audit witnesses: two distinct write-sets that collapse identically.
+----------------------------------------------------------------------
+
+ws₁ ws₂ : WriteSet
+ws₁ = []
+ws₂ = set-cell 0 1 ∷ []
+
+ws₁≢ws₂ : ws₁ ≢ ws₂
+ws₁≢ws₂ ()
+
+rollback-collapses : rollback ws₁ ≡ rollback ws₂
+rollback-collapses = refl
+
+----------------------------------------------------------------------
+-- #DB-2.1 rollback-discards-writes (headline): no pure function
+-- reconstructs a discarded write-set from the rollback receipt alone.
+----------------------------------------------------------------------
+
+rollback-discards-writes :
+  ¬ Σ (RollbackLog → WriteSet) (λ recover → ∀ ws → recover (rollback ws) ≡ ws)
+rollback-discards-writes =
+  no-section-of-collapsing-map rollback ws₁ ws₂ ws₁≢ws₂ rollback-collapses
+
+----------------------------------------------------------------------
+-- The same guarantee as a `Security` instance, so the transaction
+-- carrier joins the EchoSecurity audience family. A single transaction
+-- scope is the (trivial) `RegionId`; `audit-no-recovery-at` re-derives
+-- #DB-2.1 through the abstract theorem, witnessing that the instance is
+-- real (not merely structurally similar).
+----------------------------------------------------------------------
+
+transaction-security : Security
+transaction-security = record
+  { RegionId       = ⊤
+  ; Resource       = λ _ → WriteSet
+  ; Receipt        = λ _ → RollbackLog
+  ; exit           = λ _ → rollback
+  ; res₁           = λ _ → ws₁
+  ; res₂           = λ _ → ws₂
+  ; res-distinct   = λ _ → ws₁≢ws₂
+  ; exit-collapses = λ _ → rollback-collapses
+  }
+
+rollback-no-recovery :
+  (r : ⊤) →
+  ¬ Σ (RollbackLog → WriteSet) (λ recover → ∀ ws → recover (rollback ws) ≡ ws)
+rollback-no-recovery = SecurityTheorems.audit-no-recovery-at transaction-security
+
+----------------------------------------------------------------------
+-- Matched-negative block (HONEST BOUND, per R-2026-05-18 discipline).
+--
+-- `⊤`-aliased so `grep NotProved` catches them. A consumer citing
+-- `rollback-discards-writes` beyond these scopes is making a category
+-- error: the guarantee is exactly "no pure Agda function reconstructs
+-- the discarded write-set from the receipt alone, inside this model".
+----------------------------------------------------------------------
+
+NotProved-durability : Set
+NotProved-durability = ⊤
+
+NotProved-isolation : Set
+NotProved-isolation = ⊤
+
+NotProved-commit-semantics : Set      -- #DB-2.2 is the dual, not a no-section
+NotProved-commit-semantics = ⊤
+
+NotProved-savepoint-locality : Set    -- #DB-2.3 is structural/runtime
+NotProved-savepoint-locality = ⊤
+
+NotProved-runtime-memory-zeroed : Set
+NotProved-runtime-memory-zeroed = ⊤
+
+----------------------------------------------------------------------
+-- Companion remark.
+--
+-- #DB-2.2 (commit-promotes-writes) is the dual of #DB-2.1: commit
+-- PRESERVES the write-set, so it is an equality/section statement, not a
+-- no-section one — it belongs in a separate carrier and is deliberately
+-- not modelled here. #DB-2.3 (savepoint-locality) is a nesting/structural
+-- property of the transaction tree; it too is out of scope for this
+-- minimal rollback-safety carrier. The `Mutation` / `RollbackLog` types
+-- are placeholders chosen for inhabitability + a clean distinctness
+-- witness; the proof goes through for any carrier with two distinct
+-- write-sets collapsing to the same receipt.
+----------------------------------------------------------------------