PostgreSQL basics and isolation audit, issue #32
This is the semantic evidence audit for #32, under the evidence policy in #31. It is not the subsequent code review. The fixed point is d5d278e375c165cec33c1df7e6795375b31d7202.
Coverage and inventory
The assigned surface is all nine lesson pages, six basics Scenarios, and sixteen isolation Scenarios in postgres/01-basics and postgres/02-isolation. Every source field, lesson paragraph, heading, catalog cell, SQL step, and assertion is inventoried in 32-claims.tsv. There are 778 original units and 850 current units, 1,628 total, across 31 source files. A unit can contain several related sentences; these are coverage-unit counts, not a claim of 1,628 distinct database guarantees. Introductory, concluding, and explanatory text is included, not just known weaknesses.
32-evidence-registry.json resolves each inventory row's P-number to its engine/version, SQL operations and isolation scope, source, assertions, and generated evidence. Original locations refer to the fixed point; current locations refer to this implementation. Original text is preserved to make removals and narrowing reviewable. Unchanged text inherits the explicit schedule and operation limits of its corrected source, rather than becoming a universal guarantee.
The 22 generated Transcripts and their timelines are source mirrors, not independent claims. All their SQL/status/results are covered by the inventoried SQL and assertion units; narrator notes, comments, and timeline labels have their own source units. The registry points to each generated part, the corresponding ledger.jsonl record, and its llms-full.txt section. Scenario claims also feed rendered page descriptions and TechArticle structured data through the existing site configuration. The full inventory and this disposition record are durable deliverables; raw command output and browser evidence remain temporary.
Semantic dispositions
| Decision | Subject | Disposition and evidence |
|---|---|---|
| A1 | Transaction boundaries and autocommit | Narrowed to successful individual statements sent separately, and later plain SELECTs at READ COMMITTED. Driver-issued BEGIN and multi-statement simple-query grouping are explicit exceptions. autocommit-visibility asserts a successful new statement after an autocommit error. PostgreSQL 18 transaction tutorial and protocol section 54.2.2.1 support the contracts. |
| A2 | Statement errors and recovery | Replaced “any error rejects every statement until ROLLBACK” with the demonstrated division-by-zero/25P02 explicit-transaction case. aborted-transaction asserts recovery after full rollback and that COMMIT after an error discards an earlier INSERT. Savepoint recovery is a separate demonstrated path. Connection loss and whole-transaction serialization recovery are not conflated with statement recovery. |
| A3 | Savepoints, release, and nesting | savepoint-recovery asserts preservation of the earlier INSERT after a uniqueness error. savepoint-nesting asserts destroyed inner and released outer savepoints with 3B001, recovery through a still-valid savepoint, and final rows 1 and 4. SQL command descriptions support general semantics. Removed version-unspecified ORM behavior and workload-specific performance claims. The I/O threshold beyond 64 open subxids per backend is Documented, not a measured benchmark. Read-only subtransactions receive no subxid; writing assigns nonvirtual IDs to the subtransaction and any ancestors that need them. |
| A4 | Transactional DDL and atomicity | Narrowed to transactional table writes, CREATE TABLE, and non-concurrent CREATE INDEX. ddl-rollback now asserts both relations exist for A, executes the previously only narrated uniqueness error, and asserts absence of the row and both relations after rollback. Removed the universal migration guarantee and unsupported exact error-code list for commands not executed here. CREATE INDEX CONCURRENTLY's transaction-block restriction is supported by its PostgreSQL 18 manual section. Sequences and external effects are explicitly excluded. |
| A5 | Snapshot timing and own writes | stable-snapshot proves that a commit after BEGIN but before A's first query is included, that later concurrent updates/inserts are excluded, that A's own update is visible, and that a later transaction sees all committed rows. Removed “every statement reads a frozen view” and scoped the stable snapshot to concurrent transactional-table changes, with own-write and sequence exceptions. |
| A6 | READ COMMITTED and waits | Plain SELECT visibility is distinguished from updating and locking commands. update-recheck asserts a wait followed by zero affected rows and final values 20/30. Removed single-updating-command consistency and “readers never block” claims; PostgreSQL 18 table-lock and target-version recheck contracts cover the exceptions. non-repeatable-read, phantom-read, and both halves of read-skew have literal outcome assertions. |
| A7 | Lost updates and retry | Scoped to values read and then written inside the demonstrated transactions. READ COMMITTED commits both stale writes and ends at 110. REPEATABLE READ rejects B with 40001, still ends at 110 before retry, then actually rereads 110 and commits 120 in a fresh attempt. Removed unobserved claims about application logs/monitoring, automatic retry, and immediate correctness for stale values from outside the transaction. |
| A8 | Concurrent target updates | concurrent-update-40001 asserts immediate rejection after a post-snapshot committed target change, wait-then-rejection on commit, and wait-then-success on rollback. The manual supports related DELETE/MERGE/locking-read rules; they are Documented rather than claimed as executed here. Unrelated changes, locks without changes, and targets absent from the snapshot are excluded from the blanket conflict rule. |
| A9 | Serializable and business rules | Serial equivalence is Documented for committed participating SERIALIZABLE transactions. Each transaction must preserve the rule when run serially, and all relevant writers must participate. Removed “only SERIALIZABLE can protect a rule”, universal first-committer selection, and unconditional retry-success advice. write-skew-serializable asserts B's rejection, one remaining doctor, and a fresh count-and-decline attempt. |
| A10 | Read-only report and SSI limits | read-only-anomaly now asserts receipt identities, amounts, and marker values rather than only row counts. Its serial-order contradiction is explained from the cashier, closer, and report reads. In this schedule the cashier is rejected, not universally every offending writer. Publication is explicitly a SELECT-result model; there is no printing or external receiver coverage. Conservative tracking and READ ONLY DEFERRABLE behavior remain versioned Documented contracts, not executions or performance measurements. |
| A11 | Catalog-wide guarantees | Each cell now states D, M, or an explicit dagger with a derivation. All 12 rows, including separately scoped G2-item and G2, are inventoried cell by cell. No predicate-write-skew execution or full Hermitage coverage is claimed. Untested READ COMMITTED write-skew/read-only cells say “Not executed here”; stronger-level existence examples are not presented as weaker-level demonstrations. Own writes, sequences, and separate-statement snapshot changes are scoped explicitly. |
| A12 | Dirty writes, intermediate reads, cycles, and OTV | Narrowed all four Scenarios to their asserted READ COMMITTED schedules. Dirty write means an uncommitted overwrite, not any mixed final state. The circular-flow schedule's two old reads are not serial-equivalent; it excludes dirty cross-reads without proving serializability. Intermediate-read and OTV notes no longer claim that every reader immediately sees a commit or that committed values can never be partially replaced. Universal exclusions in the catalog are supported by row-lock/snapshot contracts and marked derivations. |
Cross-surface handoff to #40
These occurrences are outside #32 and remain the shared-content audit's responsibility. Locations below refer to the fixed point, so later tickets can find the exact statements even if preceding audits move lines. Follow the corresponding Scenario source wherever a generated copy also occurs.
| Subject | Exact starting locations | Required reconciliation |
|---|---|---|
| Error-state recovery | docs/faq.md:32; docs/errors/55P03.md:3,11; docs/errors/57014.md:3,11,25 | Distinguish failed explicit transactions, autocommit errors, full rollback, savepoint recovery, connection loss, and fresh serialization attempts. A later SELECT succeeding outside BEGIN does not establish recovery inside a failed explicit transaction. |
| Snapshot and operation scope | docs/faq.md:52; docs/concepts/isolation-levels.md:45,57-59; docs/concepts/non-repeatable-read.md:21,45-46; docs/concepts/phantom-read.md:38; docs/concepts/dirty-read.md:28-33 | Plain SELECT contracts must include own writes and the applicable engine/level; UPDATE/DELETE and locking reads have separate target-version rules. Avoid promises about every statement or every function. |
| Dirty-write definition and no-wait promises | docs/concepts/isolation-anomalies.md:53-54; docs/concepts/isolation-anomalies.md:27; docs/concepts/anomalies-by-engine.md:24-28; docs/postgres/03-locking/row-locks.md:3,8,45 | An uncommitted overwrite is the dirty-write event. A mixed final state is not its definition. Mark all-level exclusions as contracts or derived guarantees, and distinguish row locks from conflicting table locks. |
| Retry and stale values | docs/faq.md:28,48,56; docs/errors/40001.md:3,11,29; docs/concepts/lost-update.md:36,47-54; docs/concepts/anomalies-by-engine.md:32,46 | 40001 rejects an attempt; only an executed successful fresh attempt establishes its result. State writer/transaction boundaries, rerun reads and decisions, and permit controlled failure instead of reporting a commit. Coordinate with #36's retry-pattern audit. |
| Cross-row rules, SSI, and catalog coverage | docs/concepts/write-skew.md:37; docs/concepts/anomalies-by-engine.md:33-34,59; docs/concepts/isolation-anomalies.md:27; docs/mysql/02-isolation/anomaly-catalog.md | Reconcile G2-item versus predicate G2, mark unexecuted cells, and state serial business-rule preservation and writer participation. The on-call SERIALIZABLE source is now classified G2-item. A deterministic victim is not a universal victim-selection rule. |
| Evidence promises and machine summaries | README.md:6,15,21-22,55-56,88-89; docs/about/methodology.md:11,20,54,62,67,75,85; docs/faq.md:3,8; scripts/gen-transcripts.ts:152-153; docs/public/llms.txt:4-5; docs/index.md:3,8,20; docs/start-here.md:46-48; docs/.vitepress/theme/components/HomeCurriculum.vue:16 | A green suite reproduces tested schedules, not every prose statement or every schedule. Separate Demonstrated, Documented, and Entailed support. The shared llms index and its generator must be corrected together; #32 changes only its assigned Scenario records and transcript sections. |
Verification record
Verification results and the fresh-context QA verdict are published in the issue completion comment. They must distinguish semantic audit, database execution, independent YAML drivers, generation stability, structural checks, and built-reader inspection. This inventory alone is not a passing runtime or browser check.
No in-scope unsupported claim is intentionally deferred. Predicate-write-skew execution, SERIALIZABLE READ ONLY DEFERRABLE execution, performance measurements, external publication, other engine versions, network faults, and crash durability are not covered by these Scenarios. Their presence in explanatory text is either removed, explicitly limited, or supported as a versioned contract rather than called Demonstrated behavior. The complete parent audit gate remains open until #33 through #40 are reconciled.