harness+contracts: pin the oracle's claims, derive the proof-type registry

[Kiran01bm]

Follow-up to #87: the convergence oracle reads one snapshot, the load generator validates its spec and reports its races, and the proof-type registry is derived from the code instead of maintained by hand.

Why

The review of #87 landed after the merge. Three of its findings change what the harness proves rather than how it reads: the oracle ran its two symmetric differences and two counts in separate statements, so a divergence report could describe three different instants; StartLoad accepted a spec with zero workers or weights summing past one and ran nothing while the test went green; and the proof-type registry in pkg/preflight was a hand-typed list, so a new proof type that nobody added to it (which is how PrivilegedRole was missing from SAFETY.md) passed every check.

What

• internal/testutil convergence oracle: both EXCEPT directions and both counts run inside one read-only REPEATABLE READ transaction. EXCEPT replaces EXCEPT ALL because the primary key is always projected, so rows are distinct; ignoring the primary key is refused. Converged is the absence of differences; counts are diagnostic. The integration test seeds cross-category column types so dropping the ::text cast fails, and a 25-row divergence pins DifferenceLimit to the literal ids in each direction. AssertConverged takes t.Context().
• internal/testutil load generator: LoadSpec is validated up front and StartLoad fails the test on an invalid spec. Stop always returns the summary and joins the worker error with the deadline error. Expected serialization races are counted in Summary.Races, and the load test asserts they stay below the commit count so the FOR UPDATE choice is observable.
• internal/safety: a repository-wide test derives the proof-type set by shape (exported struct, all fields unexported, doc opens "<Name> proves") and requires SAFETY.md, the review checklist and the TCB model to each name every derived type, with sentinels guarding against a vacuous walk. preflight.PrivilegedRole is now listed in all three.
• copier.Chunk and copier.Watermark hold their bounds in unexported fields behind accessors so a chunk cannot be reshaped after the chunker mints it; checkpoint.Phase is documented as an opaque label and gains Terminal(); preflight.OwnerRole states what it proves.
• docs/testing.md describes the single-snapshot oracle and the primary-key rule.

Before / after

Before
┌──────────────────────┐   4 statements, 4 snapshots   ┌────────────────────────┐
│ convergence oracle   │──────────────────────────────▶│ report may mix instants│
└──────────────────────┘                               └────────────────────────┘
┌──────────────────────┐   any spec accepted           ┌────────────────────────┐
│ StartLoad            │──────────────────────────────▶│ 0 workers → green test │
└──────────────────────┘                               └────────────────────────┘
┌──────────────────────┐   hand-typed list             ┌────────────────────────┐
│ proof-type registry  │──────────────────────────────▶│ unlisted type unnoticed│
└──────────────────────┘                               └────────────────────────┘

After
┌──────────────────────┐   1 read-only REPEATABLE READ ┌────────────────────────┐
│ convergence oracle   │──────────────────────────────▶│ one instant per report │
└──────────────────────┘                               └────────────────────────┘
┌──────────────────────┐   Validate() then run         ┌────────────────────────┐
│ StartLoad            │──────────────────────────────▶│ bad spec fails test;   │
└──────────────────────┘                               │ Races counted          │
                                                       └────────────────────────┘
┌──────────────────────┐   derived by shape from code  ┌────────────────────────┐
│ internal/safety test │──────────────────────────────▶│ SAFETY.md / checklist /│
└──────────────────────┘                               │ TCB must name each one │
                                                       └────────────────────────┘

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.

[aparajon]

🤖 Review 1/2 — the convergence oracle (6e25df3a, 18 files +410/−115 over 432ad7a9)

Taking a post-merge review and turning the three findings that change what the harness proves into a PR is the right call, and the single-snapshot fix is the right shape: one read-only REPEATABLE READ transaction wrapping the catalog reads, both counts, and both directions, so a Report cannot describe four instants (convergence.go:53-71). The 25-row divergence test is a genuinely good pin — it makes DifferenceLimit and the ORDER BY both load-bearing, and asserting SourceCount == ShadowCount there proves in one line that counts cannot detect a value-only divergence.

Baseline: go build ./... clean; ./internal/..., ./pkg/copier, ./pkg/checkpoint, ./pkg/preflight all green. Twenty-four mutations, nine survived (two of the kills were compile-only, and one apparent kill turned out to be harness noise — see the note at the end of 2/2):

the difference goes back to EXCEPT ALL             SURVIVED
the source-side cast is dropped                    killed   TestConvergenceOracle
the difference is unordered                        killed   TestConvergenceOracle
DifferenceLimit becomes 25                         killed   TestConvergenceOracle
the snapshot drops to READ COMMITTED               SURVIVED
the snapshot is no longer read-only                SURVIVED
Converged consults only the counts                 killed   TestConvergenceOracle
ignoring the primary key is allowed                killed   TestConvergenceOracle
the snapshot is rolled back, not committed         SURVIVED  (equivalent)

Converged() now calls a 3-row source and a 2-row shadow converged (blocking)

convergence.go:38-42 drops the count comparison, justified by:

The counts are diagnostic only: the primary key is always projected and both counts come from the same snapshot as the differences, so any count skew necessarily surfaces as a differing key.

and missingKeys switches EXCEPT ALL to EXCEPT on the same reasoning — "the primary key is always in the projection, so every projected row is already distinct and EXCEPT loses no multiplicity" (convergence.go:137-146). The premise is proven for one side only: primaryKeyColumn is called on the shadow (convergence.go:88), and the source is checked only for having the shadow's columns by name (:80-86). Nothing establishes that the projected key is unique in the source, and EXCEPT dedupes both inputs.

Probed against a real PostgreSQL 16 — a source without a primary key holding one row twice, a shadow holding it once:

CREATE TABLE zzdup.src    (id bigint, label text);
CREATE TABLE zzdup.shadow (id bigint PRIMARY KEY, label text);
INSERT INTO zzdup.src    VALUES (1,'a'),(1,'a'),(2,'b');
INSERT INTO zzdup.shadow VALUES (1,'a'),(2,'b');

PROBE sourceCount=3 shadowCount=2 differences=[] converged=true

The oracle reports convergence for relations that hold different numbers of rows. On 432ad7a9 this case was caught, because Converged() required the counts to match — so this is a loss of detection power, not a simplification, and it is a loss in TM-5's diff oracle specifically. docs/testing.md:91 states the same premise unconditionally ("the primary key, which every comparison projects so rows stay distinct").

Both mutants around this are unpinned, which is consistent: restoring EXCEPT ALL survives every test, and Converged consulting only the counts is killed, so the suite pins the direction the change kept and nothing pins the direction it dropped.

The fix is small and there are two options, and I'd take the first: introspect the source's primary key too and require it to be the same column — the code already has primaryKeyColumn and already walks the source's columns, so it is a few lines and it makes the distinctness premise true rather than assumed. Failing that, keep SourceCount == ShadowCount in Converged() as the cheap backstop; it costs nothing, since both counts already come from the same snapshot. Either way Converged()'s doc and docs/testing.md:88-91 should say which relation's key is proven unique.

The single-snapshot property itself is unpinned (med)

The change this PR leads with is the one nothing tests: dropping IsoLevel to pgx.ReadCommitted — which is exactly the per-statement-snapshot behavior the PR set out to remove — survives the whole suite, and so does dropping AccessMode: pgx.ReadOnly. Every test calls Diff against a quiescent pair, so no test can tell one snapshot from four.

This one is worth closing because the ingredients are already in the tree and in this PR: StartLoad gives you concurrent writers, and Report's own fields give you the assertion. A test that starts the load generator against a source, copies nothing, and calls Diff while writes are landing can assert the two counts and the two direction lists are mutually consistent — under READ COMMITTED a row inserted between the count query and the second direction query makes SourceCount and the reported keys disagree, which is precisely the "report may mix instants" row in the PR's own before/after diagram. It is the same shape as the assert.Less(summary.Races, committed) check: an assertion that only means something because the workload is live.

Two smaller notes on the same block:

• AccessMode: pgx.ReadOnly is the right belt for an oracle, and worth keeping even though nothing pins it — but the deferred tx.Rollback at :63 is doing real work only on the error path, and swapping Commit for Rollback at :67 is behaviourally identical here (a read-only snapshot releases the same way, and the deferred rollback then reports already-closed either way). I list that mutant as equivalent, not as a gap.
• missingKeys's doc now says "lowest DifferenceLimit primary keys" rather than "first" (:137-140). That is the change that makes the 25-row test's []int64{1..20} assertion deterministic rather than lucky, and it is worth having said out loud.

This review was generated by Claude Code (claude-opus-5).

[aparajon]

🤖 Review 2/2 — the derived registry, the load generator, and the contracts

Deriving the proof-type set from code and moving the guard to internal/safety fixes the scope half of the earlier finding cleanly: a package-local test could not legitimately speak for SAFETY.md, and doc.go's one sentence says exactly why. The sentinels are the right instinct too — a walker that stops recognising the shape now fails loudly instead of passing over an empty set. And it found something real on its first run: PrivilegedRole was missing from all three registries and is now in all three.

a proof type loses its doc-comment prefix          SURVIVED
a proof type gains an exported field               SURVIVED
a proof type is dropped / renamed                  killed (compile — not a test kill)
StartLoad no longer validates the spec             SURVIVED
races are never counted                            SURVIVED
a vanished row becomes fatal                       SURVIVED
zero workers / empty mix / unbounded fraction      killed   TestLoadSpecValidate
Stop drops the worker error                        killed   TestStopReturnsSummaryAndWorkerErrorOnDeadline
Chunk.Lower returns the upper bound                killed   TestNewChunk
NewChunk accepts an inverted range                 killed   TestNewChunk
Watermark is always valid                          killed   TestWatermarkStates
Terminal forgets PhaseFailed                       killed   TestPhaseTerminal

The change that breaks the safety property is the change that hides the type from the guard (med)

isProofType recognises a proof type by shape: exported struct, at least one field, every field unexported, doc comment opening "<Name> proves " (proof_types_test.go:34-53). That is the right definition — it is SAFETY.md's own prescription — but the derived set is a filter, so failing the shape does not fail the test, it removes the type from the set. Both mutants that exploit this survive:

• Rewriting PrivilegedRole's doc comment so it no longer opens PrivilegedRole proves (privileges.go:115) silently drops it from the derived set. All three registries keep naming it, the guard passes, and nothing anywhere says the doc comment is load-bearing.
• Adding an exported field to PrivilegedRole also drops it from the set — and that is the mutation that matters, because an exported field is precisely what makes the type forgeable. preflight.PrivilegedRole{Leaked: "x"} becomes a legal composite literal from any package (a keyed literal may name exported fields even when unexported ones exist), so the proof is fabricable — and the guard's response is to stop tracking the type rather than to fail.

So the guard covers "someone adds a proof type and forgets a registry" and misses "someone stops a type from being a proof type." The second is the one that costs something. The cheap closure is the reverse direction: assert that every proof type each registry names is in the derived set. SAFETY.md's parenthetical is already fully structured for it — all eight of its `pkg.Name` mentions are derived types, zero false positives — so the check is free there.

Running that reverse check found a phantom immediately:

.agents/checks/review.md:18 — Dangerous APIs accept proof types (statement.Classified, PreflightedTable, …)

Classified does not exist. grep -rn Classified pkg internal returns nothing on this head, and nothing on 432ad7a9 either. It has been listed as the first proof type in the review checklist the whole time, and this PR edits that exact line to insert PrivilegedRole beside it. Either it needs restoring in code or dropping from the list — and a reverse check would have said so on the first run, which is the argument for adding one.

Two smaller notes on the same test:

• :103 overstates what is caught. "a proof type added, renamed, or dropped without updating all three lists fails here" — added and renamed do fail (the new name is absent from the registries). Dropped does not: the derived set shrinks and a stale registry entry is invisible. Worth trimming the claim to what holds, or adding the reverse check and keeping it.
• :106 walks "../../pkg" while doc.go speaks for the whole repository. Today that is complete — I ran the walker over ../.. and it yields the same eight types, internal/ defines none — so widening the root is free and closes the gap before the first proof type lands outside pkg/.

The registry guard is still switched off for the PRs that only touch prose (med)

.github/workflows/ci.yml: test is gated on needs.changes.outputs.code == 'true', and changes classes a file as code only when it is neither **/*.md nor docs/**. all-green fails only on failure or cancelled, so a skipped test is a pass. The registries this guard pins are SAFETY.md, .agents/checks/review.md, and docs/tcb-model.md — all three are markdown, so a PR that edits only them skips the only test that checks them. A docs-only PR deleting PrivilegedRole from SAFETY.md merges green today.

The move to internal/safety fixed the scope; the trigger condition is the other half, and it is a two-line change to the workflow (treat the three registry paths as code, or run the internal/safety package unconditionally). Not strictly this PR's job, but this PR is the one that makes the guard the repository's single answer for proof-type coverage, so it is the natural place to make it run.

Related, since both are open: #88 also rewrites the CopySwapTarget row in docs/tcb-model.md. git merge-tree --write-tree 6e25df3a 315e897a conflicts on SAFETY.md and .agents/checks/review.md — loud, fine — but docs/tcb-model.md auto-merges into two CopySwapTarget rows (merged :94 and :98) claiming different invariant sets. namesProofType is a Contains, so the new guard passes a duplicate twice, same as the old one did. Whichever lands second wants a rebase, not a merge.

Summary.Races counts the shutdown as a race (med-low)

expectedRace (workload.go:303-308) returns true for context.Canceled, which is correct for its original job — tolerate and keep going — but this PR gives it a second job, incrementing a counter (:191). Stop cancels the workers, so each worker's in-flight mutation returns context.Canceled and lands in Races before the loop notices the context is done. Every run therefore reports up to Workers races that are not races at all, and Summary's own doc enumerates what it counts — "a unique-key collision, a serialization failure, a deadlock, or a vanished row" (:128-131) — without mentioning cancellation.

At the integration test's scale (4 workers, 80/s, 2s) four spurious counts do not threaten assert.Less(summary.Races, committed), so this is not a flake today. It matters because Races is now a number a reader is invited to interpret: "a run whose Races dwarf its committed counts wrote far less than its spec suggests" is the doc's own framing, and the shutdown contribution is a fixed offset in it. Either check ctx.Err() == nil before g.race(), or split the predicate into the tolerate set (which keeps context.Canceled) and the count set (which doesn't).

Also unpinned around the counter: assert.Less(summary.Races, committed) holds for Races == 0, so removing the g.race() call entirely survives. If the assertion exists to make the FOR UPDATE choice observable — as the summary says — it wants a floor as well as a ceiling, or a separate assertion that some race occurred. And dropping pgx.ErrNoRows from the tolerated set also survives, so the vanished-row path the doc describes is never exercised; with 200 seeded rows and a delete weight of 1 in 4 over two seconds, the table never empties, so randomIDQuery never comes back empty.

StartLoad's validation is pinned, its wiring is not (low)

validate() is well covered — seven cases, exact messages, and all three weakening mutants die in TestLoadSpecValidate. But deleting require.NoError(t, spec.validate()) from StartLoad (workload.go:161) survives the whole suite: the guard's call site has no test, and the call site is the behavior the summary describes ("an invalid spec fails the test immediately rather than starting a generator that writes nothing"). One test that calls StartLoad with Workers: 0 under a testing.T stub, or asserting Stop on a zero-worker generator, closes it.

What the contracts got right

Every accessor mutant died, which is what you want from a contract change: Chunk.Lower returning the upper bound, NewChunk accepting an inverted range, Watermark.Valid returning true unconditionally, Phase.Terminal forgetting PhaseFailed. Making Chunk and Watermark fields unexported is the substantive part — NewChunk's lower <= upper check was previously advisory, since a caller could build Chunk{Lower: 4, Upper: 3} directly, and Watermark{Value: 7} could carry a value with Valid false. TestWatermarkStates pinning NewWatermark(0) as valid is the case worth having: a copied-through key of zero is real, and it is exactly the one a Value != 0 shortcut would get wrong.

Phase's doc earning the "opaque label" note is a good catch on its own terms — with PhaseFailed last in declaration order, any phase >= PhaseVerifying comparison would have read as plausible and been wrong. Terminal() gives callers the question they actually want, and TestPhaseTerminal covers Phase(0) as well as the named values.

One methodology note, since it nearly produced a wrong finding above. Running the mutation suite with ./pkg/preflight in the same pass produced kills for the Commit → Rollback mutant, with a different set of failing tests on each of two runs — TestCheckCreatePrivilegesRefusesEmptySearchPath once, TestCheckTableAbsentProvesFreeName the next. Re-running that mutant against only ./internal/testutil ./internal/safety passes twice, and the unmutated tree passes too, so those were container-pressure failures rather than the mutant. Worth knowing for this repo: the container-heavy packages can manufacture false kills when run alongside, and a kill whose failing test has nothing to do with the mutated line deserves a second look before it goes in a review.

Approving. The blocking item is the Converged() premise in 1/2 — that one changes what the oracle proves, and it is a few lines to make true.

This review was generated by Claude Code (claude-opus-5).

[aparajon]

🤖 Approving. Deriving the proof-type set from code and wrapping the oracle in a single read-only REPEATABLE READ snapshot are both the right shape, and the guard earned its place by finding PrivilegedRole missing from all three registries on its first run. Findings are in the two review comments; the one blocking item is the Converged() premise — a 3-row source against a 2-row shadow now reports converged, because the distinctness the doc relies on is introspected on the shadow only. A few lines either way.

This stamp was left by Claude Code (claude-opus-5).

[Kiran01bm]

🤖 Review response — created by Kiran's code review agent (Amp, Claude Opus 4.6) — pull/91, follow-up commit

Review addressed: pg-sprite-pr91-review.md (findings against 6e25df3a). Worktree
/Users/kmuddukrishna/code/pg-sprite-worktrees/cs0-review-followup, branch
kiran01bm/cs0-review-followup. Changes are staged, not committed.

#	Concern	Status
1	.agents/checks/review.md lists statement.Classified, a type that does not exist; the real proof is statement.Statement. Fix in all three registries.	fixed. The checklist entry is now statement.Statement, and the list is package-qualified throughout (preflight.PreflightedTable, …, dbconn.TableLock) so the new reverse check (see #2) covers every entry, not just the one that happened to be qualified. SAFETY.md and docs/tcb-model.md both name statement.Statement too — SAFETY in its proof-type list, the TCB model as a new row (statement.ParseOne → statement.Statement, encodes ST-7).
2	isProofType requires the doc to open "<Name> proves "; Statement's doc opened "Statement is …", so it never entered the derived set, and the one-directional assertion means the comment's "dropped … fails here" was false.	fixed, both ways. (a) statement.Statement's doc now opens "Statement proves the SQL it carries parsed as exactly one statement …", the shape SAFETY.md prescribes, so the derived set includes it and every registry is forced to name it. statement.DesiredSchema (ST-8, ParseDesired-only, all fields unexported — same shape, same gap) was given the same treatment and is named in all three registries. (b) The test now also walks registry → code: every code-font `pkg.Name` in a registry whose pkg is a package under pkg/ must be an exported type or function of that package, so a list entry that outlives its type fails. Mentions of foreign packages (time.Sleep, pgx.ParseConfig), file names (runner.go) and Type.Method pairs are skipped by construction; TestStaleMentions pins those shapes plus the exact statement.Classified case. The test comment now states what each direction catches. Verified by mutation: restoring statement.Classified fails with "Should be empty, but was [statement.Classified]"; removing statement.Statement from SAFETY.md fails with "SAFETY.md does not name the proof type Statement".
3	Summary.Races has no test that fails when g.race() stops incrementing.	fixed. TestLoadGeneratorCountsExpectedRaces seeds two rows and runs one delete-only worker against real PostgreSQL: it asserts Deletes == 2, DeletedIDs is exactly {1, 2}, every other commit counter is zero, Races > 0, and the table is empty. Each tick after the second delete hits pgx.ErrNoRows — the vanished-row race expectedRace already classifies. Verified by mutation: replacing g.race() with a bare continue fails the test at the Races assertion.
4	No convergence case creates a row-count skew, so the removed SourceCount == ShadowCount clause is untested; ideally also a concurrent writer during Diff.	fixed (skew); deferred (concurrent writer). Two new cases in TestConvergenceOracle: a shadow-only row (INSERT INTO shadow … id 31) yields exactly [{shadow-minus-source, [31]}] with counts 30/31, and deleting source id=3 yields exactly [{shadow-minus-source, [3, 31]}] with counts 29/31 — one-sided rows surface as keys, no phantom appears in the other direction, and Converged() is false both times. The concurrent-writer case is deferred: proving the single-snapshot claim needs a commit to land between two of Diff's statements, and the harness has no seam to interleave one without adding a test-only hook to production-shaped code. The claim rests on pgx.TxOptions{IsoLevel: RepeatableRead} on the one Tx every query runs on, which the reviewer independently verified.