[rusholme]

What and why

Milestone 0, task 3 of the foundation plan (PLAN.md v5, 2026-10-20, held outside the repository until its rapid_docs page lands after milestone 3): a synthetic fixture and Part 3's proof steps 2, 4, 6, 8, 10, 11, 12 and 13 as a test suite in foundation.yml, against #275's schema and #276's operations, and the wall time of one change group at three sizes. Steps 1, 3, 5, 7 and 9 need the real stages and are milestone 3; none is faked here. No library code changes.

Files

• tests/db/proof/__init__.py (new, empty).
• tests/db/proof/fixture.py (new): World, a synthetic world on one connection: dataset D, survey S, field 1, filter 1, epochs (exposures) 1 and 2, SCAs 1 and 2, 24 sources per image at fixed positions. Runs and jobs go through create_run/create_job, every product is written as Parquet plus a manifest under file://<tmp>/job-<id>/attempt-<n>/ (with task 2's write_attempt) and loaded through publish. import_image (one difference image and its source set per job), associate (object set: predecessor's objects, this epoch's sources added to the sufficient sums, excluded source sets' members subtracted, this epoch's memberships; object ids from rapidpipe.science.spatial.radec_index), packets (one packet set per image key: packets index rows and forced rows), recipe (associate and packets over epochs, each set the next one's predecessor), cutover (the group that rebinds a recipe's objects and packets and makes its run live).
• tests/db/proof/test_steps.py (new): one test per step, below.
• tests/db/proof/timing.py (new): a script, not a test; CI does not run it. python tests/db/proof/timing.py N against a throwaway database with the schema applied (it adds rows, deletes none).
• .github/workflows/foundation.yml: pytest also runs tests/db/proof. db-migrations.yml: --ignore=tests/db/proof.

The steps, as asserted

• 2 Two associate jobs launched against set 1 (both expecting its binding), then published in turn: the first binds; the second is published, unbound, refusal = binding <id> is no longer open, its objects input and expects row recorded (job_show), no binding row of its own.
• 4 Run 2 (not live) runs both epochs over run 1's imports; one change group rebinds the object set, all four packet sets and the live binding: six rows opened and six closed under one group id; packets_official and objects_official show run 2's jobs only; every official packet row's job has exactly the inputs (object set, source set) its index row names.
• 6 undo of that group: run 1 is live again, packets_official and objects_official show run 1's jobs, none of the rows the cutover closed is reopened (the restored bindings are new rows), run 2's packet rows all still exist.
• 8 A packet job's publish is killed after its rows were loaded (observed inside the transaction: 24 index rows) and before commit: no packets or forced rows, job still launched. The retry (attempt 2, a new prefix) publishes 24 + 24 rows once and binds; a further call (attempt 3, no files) is a no-op, published_attempt stays 2.
• 10 Session A applies a group closing the object binding, uncommitted; session B's group closes an older diffimage binding and then the same object binding, and blocks; A commits; B refuses naming the object binding; the diffimage binding B had closed is still open and no row records B.
• 11 Session A holds the full cutover uncommitted; session B publishes a run-1 (live) packet job for epoch 2 SCA 1 expecting run 1's binding, and blocks; A commits; B's rows are published (24) and unbound, refusal names the expected binding; afterwards every open packet binding is run 2's, from A's group, one per key, and run 2 is live.
• 12 Cutover after epoch 1; epoch 2 then publishes and binds under run 2 (live); undo of the cutover refuses naming the object binding it opened, which has since moved, and official is unchanged; an explicit group restores run 1's epoch-1 packet sets and live binding; the epoch-2 object set and packet sets stay run 2's.
• 13 Epoch 1 SCA 1's difference image and source set are re-imported (fluxes doubled) and rebound automatically; the next associate job names the replacement source set as an input and the superseded one as an excludes row; the official set's nsources and sumflux equal the count and sum over members_official joined to sources for every object (2 members each), members_official returns no member of the superseded set, and its 24 sources and 24 memberships in set 1 still exist. With the excludes row removed this test fails (checked locally).

Where the proof needed something Part 1 does not say

• Which run an import belongs to. The imports are jobs under the first (live) recipe so they bind automatically; nothing in Part 1 names an import run.
• One import job per (epoch, SCA). A set job binds at most one key of its set product (db, tests, ci: the foundation schema in one file, proved on every push (foundation m0) #275: set children join on (product, job)), so each source set is its own job; the difference image goes in the same job as its source set.
• Expected bindings are resolved at create_job, as the loop would choose them. Step 2's two candidates must both be launched before either publishes; launching the second after the first published would have it expect the first's binding and bind, which is correct behaviour but not the step.
• Step 2's predecessor is set 1, not set 2. The fixture has two epochs, so the two candidates are epoch-2 associate jobs over set 1; the observation is the same.
• What a cutover carries. The proof's group rebinds the object set, every packet set and the live binding; the imported difference images and source sets are shared by both recipes and are not in it.
• Step 11's live-run job is a re-publication of one packet set (epoch 2, SCA 1) under the old recipe, expecting the binding the cutover closes.
• Step 12's "live epoch" is epoch 2 under the new recipe, after a cutover made at epoch 1, so the object binding the cutover opened moves. The "explicit partial group" restores every key still as the cutover left it, the live binding included (so run 1 is live again while the epoch-2 objects and packets stay run 2's); Part 1 does not say whether the live binding belongs in that group; it is a key still as expected, so it is in.
• Step 13: whether the replacement source set joins the next object set is not stated; the proof names it as an input, so the recomputed sums cover the replacement's sources, and asserts sums against members_official rather than against fixed numbers.
• Step 8's kill is a BaseException raised inside publish after the loads and before commit (by replacing the module's _bind for that call); the publisher rolls back exactly as a dropped connection would. A real SIGKILL of a process is not exercised.
• forced.rid is 0: the fixture imports no L2 rows.

Measurements

• Local, PostgreSQL 18.6 container on rr (16 CPUs, 61 GiB), no q3c: tests/db/test_schema.py test_publish.py test_change.py tests/db/proof: 23 passed, 1 skipped (q3c, CI only), under 3 s; three consecutive runs green. The proof alone: 8 passed in about 2 s. Without PGHOST: 8 errors, "PGHOST is not set; database tests need a database".

• Change-group wall time (timing.py, one change call closing N bindings and opening N on the same keys, fresh database per size, same host and container):

  N keys	wall time of one change group
  10,000	1.30 s
  100,000	13.18 s
  1,000,000	137.87 s

  Linear, about 0.14 ms per key: apply issues three statements per item (the close UPDATE, the held-binding SELECT, the INSERT), each a round trip from Python. The script ANALYZEs official after its bulk setup, the state autovacuum keeps a live table in.

• Finding, not fixed here (library code is task 2's and the next milestone's): on an unanalysed official, the same 10,000-key group took 14.2 s (three runs: 14.24, 14.19, 14.11 s), slower than 100,000 keys analysed. Probe-verified with EXPLAIN: with no statistics the planner answers _open's held-binding SELECT through official_open_product_job (product, job) and filters on key, scanning every open binding of the product per item, so the group is quadratic in N; after ANALYZE it uses official_open_product_key. At 100,000 keys autovacuum had analysed the table before the group ran (18.1 s cold, 13.2 s analysed). It bites a group that runs straight after a bulk load into a young table. Candidate remedies for a later PR: ANALYZE official in the publisher's post-commit ANALYZE, or set-based closes and opens in apply (one UPDATE ... FROM (VALUES ...) and one INSERT ... SELECT), which would also remove most of the per-key round trips.

Left for the next task

• Task 4 (retirement): foundation.yml runs tests/db and tests/cli whole once the old modules go, which picks tests/db/proof up with them; db-migrations.yml (with its --ignore list) is deleted. tests/db/proof/fixture.py is reusable for the verb tests (World.run, World.cutover give a ready change group).
• Milestone 3: steps 1, 3, 5, 7 and 9 on the real stages.

🤖 Generated with Claude Code