[zachyking]

Post-release 1: do not merge before the release-1 cut.

Closes the averin part of FeirAI/feir-ops#24 (wave-1 item averin-shadow-offlock). Design: ops-log/designs/wave1-averin-shadow-offlock.md, lead decisions: ops-log/designs/wave1-lead-decisions.md.

Problem

A shadowed checkpoint cut ran the full O(history) computation inside the project write transaction. On Postgres every write to the project waited for it, up to the shadow budget (1 s since #55). The budget was cut to 1 s to bound that stall, which also made the shadow stop fitting after about an hour of history.

Design

A cut that needs a shadow now runs in three steps.

1. Write lock, as every cut: incremental cut and the shadow decision. If a shadow is due, the transaction returns errShadowDue and rolls back having written nothing.
2. No write lock: shadowOffLock opens one repeatable-read snapshot S, reads the latest checkpoint first (a changed base returns errShadowRaced), takes created_ts after that read, and computes the incremental body and the full body at S with the same timestamp. They are compared byte for byte. The classification, counters, latch and ALERT texts are the old block moved unchanged (compareShadow). A mismatch returns here, before any lock or signature.
3. Write lock again, O(1): the latest checkpoint must still be the base (seq and hash) and the next seq must be base+1, else errShadowRaced and nothing is signed. Then the exact bytes compared in step 2 are sealed and stored. They are never recomputed.

A per-project cut gate (one slot, context-cancellable, ref-counted) is held across all steps of a cut, so cuts of one project in one process do not run two shadows at once. Writers never take it. Lock order is gate, then write guard. It is released before witness and TSA.

What is compared against what: both bodies are deterministic functions of S. Records and checkpoints are append-only and every write commits under the guard, so S is a prefix of the guard-serialized write sequence. The checkpoint signed is the full body at S.

Could a divergent checkpoint be signed before the comparison finishes?

• Shadowed cut, this process: no. Step 3 is reached only after a byte-identical match, or after "could not run" (where the incremental body is signed as before). A mismatch returns before any lock or signature. Exposure window: zero.
• Same-process cuts during the shadow: none are signed; they wait on the gate.
• Another writer process (outside the single-writer policy) cutting during the shadow: step 3 refuses and signs nothing (error, new counter averin_checkpoint_shadow_raced_total).
• Unshadowed cuts: unchanged, signed unseen. A divergence there is caught by the next shadowed cut or the offline verifier; the window stays at least an hour (more during a backoff).

Invariants

1. No body that differs from the full body at S, and none the full computation refuses, reaches the seal on a shadowed cut.
2. No O(history) work under the write lock on the incremental path (the no-usable-base full fallback is unchanged and still under the lock, D5).
3. Base pinning in step 3.
4. created_ts is taken after the snapshot's first read.
5. cut.incremental / cut.full move once per cut; shadow_checks_total once per attempt that reaches the full computation; mismatch and failed keep their meaning; ALERT texts byte-identical.
6. Decision logic, hourly rate limit, backoff and latch unchanged.
7. A client hang-up is not a failed shadow (step 2 runs detached, bounded by budget + 5 s).
8. No new lock cycle, no gate leak (asserted by tests).

Decisions taken (lead)

• D1 a shadowed checkpoint commits to its snapshot: records committed during the shadow go into the next checkpoint. It still covers everything committed before the cut request arrived. Consumers must not assume "the returned checkpoint covers everything committed before the response".
• D2 default budget 1 s to 20 s (the existing ceiling).
• D3 raced by another writer: return an error, never fall back to an unshadowed cut.
• D4 new counter averin_checkpoint_shadow_raced_total and gauge averin_checkpoint_shadow_last_duration_seconds. Note for the lead: the gauge is process-wide (the most recent shadow of any project), not per project. The metrics registry has no labelled gauge and a project label would be unbounded in a multi-tenant deployment. Say if per-project is wanted.
• D5, D6 not in this item (LIMITATIONS says there is no process-wide limit on concurrent shadows); D7 F1 is a separate PR.
• None of these decisions is marked owner-provisional for this item.

What this does not fix (stated in the docs)

• The shadow still uses database CPU, memory and one pool connection for up to the budget, and a shadowed cut's response takes up to that long. After a restart every project's first cut shadows at once.
• The "still compares for 24 h" clause is probably not met by this PR alone: with the 20 s budget the estimate (about 1 s of full computation per hour of history at 0.5 calls/s, not measured) puts the stopping point near 20 h. F1 (cheaper full computation) is the follow-up. The 24 h soak has to show it.

Tests

New checkpoint_cut_offlock_test.go: writes continue while the shadow is paused and nothing is stored before the comparison finishes, and the signed body equals the snapshot's body (Mem and Postgres); mismatch with writes continuing refuses and latches; raced by another writer process (Mem and Postgres) signs nothing, one checkpoint per seq; same-process cut waits on the gate and signs seq N+1; gate wait is cancellable; client cancel is not a failed shadow and stores nothing; in-transaction phase 1 returns the sentinel and writes nothing; a concurrent-writers hammer for the race detector. Existing tests keep their assertions; only the cutOnce helper changed (it calls the real cut), plus the one budget assertion (1 s to 20 s). The Postgres run proves a read-only repeatable-read transaction accepts the budget savepoint and SET LOCAL.

Formal: checkpoint-cut-incremental-equals-full restated in both registers (off-lock, base check, error on a moved base, snapshot coverage, 20 s, and the new does-not-establish items). Only checkpointBodyChecked changed among the existing covers (relocked: the statement still holds, the change is that the shadow block moved out of it); added covers for shadowOffLock, compareShadow, createCheckpointTx, cutCheckpoint, acquireCutGate. cutBodyIncremental, parseCutBase, checkGaplessGrantLogAfter, checkpointBody, the min-interval functions and cutBodyFull are byte-unchanged. Mutants re-cut: shadow-cannot-run-refuses, shadow-ignores-backoff. New: shadow-under-write-lock, shadow-skips-base-check, shadow-signs-current-state, shadow-no-cut-gate. All 21 mutants of the claim killed.

Gate output

All under nice -n 10 taskset -c 0-11; this host needs CGO_LDFLAGS=-ldl for the cgo link (old glibc), unrelated to the change.

make test-server           -> exit 0 (api 18.4s ok, store ok, all packages ok)
make test-server-postgres  -> required Postgres tests ran and passed without skipped subtests
go test -race -count=1 ./internal/api -run TestCheckpointCut -> ok (CI does not run -race)
make check-claims          -> validated references and CI IDs for 52 claims (textual check only)
formal/kit-claims.json     -> 764 check(s), 0 failure(s)
check_mutants.py           -> every mutant of the claim: 1 killed, 0 survived, 0 error

No dependency or core change, so no make test-core or supply-chain run.

Risks

Database load and pool occupancy for up to 20 s per shadow (R1, R3), cut latency up to the budget (R4), mutant patch churn. The govder four-plane e2e was not run (it cuts without concurrent writes).

🤖 Generated with Claude Code