|
| 1 | +// SPDX-License-Identifier: MPL-2.0 |
| 2 | +// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | +// |
| 4 | +// Transaction.affine — affine-bounded transactional scope for the |
| 5 | +// Sqlite stdlib (db-theory #2). |
| 6 | +// |
| 7 | +// A `Tx` is an opaque, affine handle returned by `tx_begin(db)` and |
| 8 | +// consumed *exactly once* by either `tx_commit(t)` or `tx_rollback(t)`. |
| 9 | +// While a `Tx` is live, all `db_execute` / `db_prepare` calls against |
| 10 | +// the same `Db` participate in the open transaction; on `tx_commit` |
| 11 | +// they atomically become visible to subsequent reads, on `tx_rollback` |
| 12 | +// they leak no writes (the safety property — see proof obligation |
| 13 | +// below). |
| 14 | +// |
| 15 | +// Nested scopes use savepoints (`tx_savepoint(t, name)` / `tx_release` |
| 16 | +// / `tx_rollback_to`), which is the standard SQLite-flavoured nesting |
| 17 | +// model (savepoints are NOT separate `Tx` handles — they share the |
| 18 | +// outer affine lifetime). |
| 19 | +// |
| 20 | +// **Affine discipline (carrier-level)** |
| 21 | +// Aliasing: `Tx` is `extern type`, opaque from the AffineScript side |
| 22 | +// — there is no copy constructor and no way to clone it. The host |
| 23 | +// adapter is required to invalidate the handle on commit / rollback |
| 24 | +// so that a use-after-consume turns into a host-side `Error`. |
| 25 | +// See `lib/codegen_deno.ml`'s `__as_txBegin` / `__as_txCommit` / |
| 26 | +// `__as_txRollback` contract for the JS side of this invariant. |
| 27 | +// |
| 28 | +// **Safety property (proof obligation #DB-2.1)** |
| 29 | +// `rollback-discards-writes` — for any `Tx t` returned by |
| 30 | +// `tx_begin(d)` and any sequence of `db_execute(d, ...)` issued while |
| 31 | +// `t` is live, if the lifetime ends with `tx_rollback(t)` then no |
| 32 | +// row visible to a `db_query*(d, ...)` issued *after* the rollback |
| 33 | +// reflects any of those executes. |
| 34 | +// |
| 35 | +// Status: pending against `hyperpolymath/echo-types` (see |
| 36 | +// `docs/proof-obligations/db-theory-2-transaction-safety.md`). |
| 37 | +// The echo-types audit (2026-06-01) found `LEcho.weaken` + |
| 38 | +// `EchoSecurity.Security` + `EchoNoSectionGeneric.no-section-of- |
| 39 | +// collapsing-map` carry the right shape but require a |
| 40 | +// `TransactionMutations.agda` instantiation upstream. Tracked at |
| 41 | +// the echo-types issue linked from the cross-doc file. |
| 42 | +// |
| 43 | +// **Why this is the natural db-theory #2** |
| 44 | +// Affine semantics maps directly to write-set isolation: an affine |
| 45 | +// resource is consumed exactly once, and the consumption is *the* |
| 46 | +// commit/abort decision. The same `(begin, commit, rollback)` shape |
| 47 | +// covers RDBMS transactions, Haskell STM atomic blocks, Clojure refs, |
| 48 | +// and Mnesia activities — picking SQLite as the first concrete |
| 49 | +// backend is purely the most useful one to ship first. |
| 50 | + |
| 51 | +module Transaction; |
| 52 | + |
| 53 | +pub extern type Tx; |
| 54 | + |
| 55 | +// ── Top-level transaction lifecycle ──────────────────────────────── |
| 56 | +// |
| 57 | +// `tx_begin` issues `BEGIN` on `d` and returns a fresh `Tx`. Exactly |
| 58 | +// one of `tx_commit` / `tx_rollback` must be called on the result; |
| 59 | +// the affine type system enforces "at most one", and host-side |
| 60 | +// invalidation enforces "use-after-consume is an error". |
| 61 | + |
| 62 | +pub extern fn tx_begin(d: Db) -> Tx; |
| 63 | + |
| 64 | +/// Issue `COMMIT`. Returns 0 on success. Invalidates `t` host-side. |
| 65 | +pub extern fn tx_commit(t: Tx) -> Int; |
| 66 | + |
| 67 | +/// Issue `ROLLBACK`. Returns 0 on success. Invalidates `t` host-side. |
| 68 | +/// **All writes issued during `t`'s lifetime are discarded** — this |
| 69 | +/// is the safety property formalised in proof obligation #DB-2.1. |
| 70 | +pub extern fn tx_rollback(t: Tx) -> Int; |
| 71 | + |
| 72 | +// ── Savepoints (nested scopes within a single Tx) ────────────────── |
| 73 | +// |
| 74 | +// Savepoints share the outer `Tx`'s affine lifetime. A savepoint is |
| 75 | +// named (string) and may be released (`tx_release`, forgets the |
| 76 | +// savepoint but keeps its writes within the outer scope) or rolled |
| 77 | +// back to (`tx_rollback_to`, discards writes issued since the |
| 78 | +// savepoint but keeps the outer `Tx` open). Both leave `t` valid. |
| 79 | +// |
| 80 | +// Naming convention is caller-controlled — SQLite uses string names, |
| 81 | +// and shadowing is per-name LIFO. Reusing a savepoint name is legal |
| 82 | +// but typically a programmer bug; the adapter does not guard it. |
| 83 | + |
| 84 | +pub extern fn tx_savepoint(t: Tx, name: String) -> Int; |
| 85 | +pub extern fn tx_release(t: Tx, name: String) -> Int; |
| 86 | +pub extern fn tx_rollback_to(t: Tx, name: String) -> Int; |
| 87 | + |
| 88 | +// ── Introspection ────────────────────────────────────────────────── |
| 89 | +// |
| 90 | +// `tx_db` returns the `Db` underlying `t` — useful for handing the |
| 91 | +// connection to a query function that takes `Db` (the type system |
| 92 | +// has no row-polymorphism over "Tx-or-Db", so this manual escape is |
| 93 | +// the pragmatic seam). The returned handle aliases the original |
| 94 | +// connection; calls against it participate in the open transaction. |
| 95 | + |
| 96 | +pub extern fn tx_db(t: Tx) -> Db; |
| 97 | + |
| 98 | +/// Returns 1 if `t` is still live (neither committed nor rolled back), |
| 99 | +/// 0 otherwise. Primarily for assertions and tests; production code |
| 100 | +/// should rely on the affine type system, not this runtime check. |
| 101 | +pub extern fn tx_is_live(t: Tx) -> Int; |
0 commit comments