[zachyking]

Wave 2: held for the lead; do not merge before the v1.0.1 decision.

Closes the averin#59 low findings tracked in FeirAI/feir-ops#27.

Problem

After averin#59 the shadow comparison runs off the write lock, but phase 3 of a shadowed cut (base check, then seal) still ran on the caller's request context, while the shadow can take budget + 5 s. A client that hangs up after a matched comparison signed nothing, and on a latched project every cut is shadowed, so such a client never got a checkpoint stored and each attempt cost a full O(history) read with no backoff. When the could-not-run ALERT had been logged, a later failure left that ALERT claiming a signature that never happened. API.md also understated the latency bound, and four docs/comment statements were broader than the code.

Design

• Phase 3 runs under context.WithoutCancel(ctx) with its own 15 s bound (checkpointSignTimeout, above the 10 s lock wait limit), in the same goroutine. It still runs the unchanged O(1) base check first and signs only the compared bytes. The gate wait and phase 1 stay cancellable, so a client that is gone before the decision costs nothing.
• The witness append and TSA anchor in createCheckpoint are detached too (their existing 10 s bounds stay). Without that, a hung-up cut would be stored but neither witnessed nor anchored.
• compareShadow reports whether the full computation could not run (carried in shadowResult.unchecked). New logCutNotSigned writes one line starting WARNING (not ALERT) on any failure at the signing step, and after a failed read-snapshot commit that follows a could-not-run ALERT. ALERT texts, counters, latch, verified and backoff are unchanged and are not undone if signing then fails.
• Docs: full latency bound in API.md (earlier-cut wait, locked step, shadow budget + 5 s, signing step 15 s, witness 10 s, TSA 10 s, and that the defaults can exceed the 60 s HTTP write timeout); LIMITATIONS backoff wording, two-writer note and hang-up note; CONFIGURATION; the min-interval comment ("no longer holds the project write lock"); the failed-counter HELP; the orphaned createCheckpoint comment replaced by a correct one.

Invariants

1. Fail closed, unchanged: phase 3 seals only the compared bytes, only after the unchanged base check (createCheckpointTx is byte-identical). A mismatch or a full-computation refusal still returns in phase 2 before any lock or seal.
2. Latch, verified, counters, backoff, min interval: unchanged. No new metric.
3. A client hang-up is never a shadow failure, and now never a witness or anchor failure either.
4. Bounded: phase 3 at most 15 s before commit (+ the store's own 10 s commit bound). No new goroutine. Lock order unchanged (cut gate, write slot, guard).
5. Docs say nothing like "a hang-up always yields a checkpoint": the signing step can still fail, and the WARNING line says so.

Tests

• TestCheckpointCutShadowOffLockClientCancel (Mem) and ...ClientCancelPostgres rewritten: after a client hang-up the cut returns no error, seq 1 is stored, the body equals the compared body, checks 1, mismatch 0, failed 0, gate count 0.
• New ...ClientCancelWitnessedAndAnchored: witness holds exactly the new checkpoint and seq 1 is anchored. Confirmed locally that it fails with context canceled warnings when the witness/TSA detach is reverted.
• New ...SignStepIsBounded: with the could-not-run path and the project write lock held elsewhere, phase 3 returns context.DeadlineExceeded within its bound, nothing is stored, the failed counter stays 1, the log holds the ALERT then the WARNING with the could-not-run note (and no second ALERT), the next cut inside the backoff signs seq 1 unshadowed; also pins the default bound at 15 s (docs drift guard).
• New ...RacedBeforeSnapshot: closes the untested phase-2 base-check branch of shadowOffLock (raced 1, checks 0, mismatch 0, failed 0, next cut shadowed).
• Not unit-tested: a phase-2 read-snapshot commit failure after could-not-run (Mem snapshots have no commit); reviewed only.

Formal

Claim checkpoint-cut-incremental-equals-full: statement extended (snapshot base check; signing step not cancelled by the caller, own 15 s bound; response-time note in does_not_establish). Relocked covers: shadowOffLock, compareShadow, cutCheckpoint; the statement still holds for each (same bytes signed, same base check, same classification, ALERTs and counters; only the context of phase 3, a carried flag and a log line changed). No other cover changed. New mutants: checkpoint-cut-shadow-sign-on-caller-ctx, checkpoint-cut-shadow-sign-unbounded, checkpoint-cut-shadow-skips-snapshot-base-check; checkpoint-cut-shadow-cannot-run-refuses re-cut for the new return shape. All 26 mutants of the claim: 26 killed, 0 survived. FORMAL.md regenerated; legacy claims.json statement and proofs updated.

Gate output lines

make test-core: EXIT 0
make test-server: ok  github.com/feirai/averin/server/internal/api  128.177s ... EXIT 0 (go vet clean)
make test-server-postgres (own disposable postgres:16, removed): required Postgres tests ran and passed without skipped subtests
go test -race -count=3 ./internal/api -run TestCheckpointCut: ok  github.com/feirai/averin/server/internal/api  216.004s (CI does not use -race)
cargo clippy --all-targets -- -D warnings: EXIT 0
gofmt -l: clean
python3.12 scripts/formal/check_claims.py --claims formal/kit-claims.json: 792 check(s), 0 failure(s)
python3.12 scripts/check-claims.py: validated references and CI IDs for 53 claims; test_check_claims: Ran 19 tests OK
check_mutants.py over the 26 mutants of the claim: 26 killed, 0 survived, 0 error

Host note: the default python3 here is 3.8, where make check-claims fails on Path.is_relative_to (also on base, unrelated); the claim checks above ran under python3.12.

Dependencies

No dependency change and no Rust change, so sfw make supply-chain is not needed and feir-os deploy/eve-isolated/native-verifier/Cargo.lock needs no relock.

Risks

• A detached phase 3 holds the cut gate up to 15 s (+ commit) after the client left; same-project cuts wait on it (cancellably). Normally milliseconds.
• Witness/TSA calls now finish after a hang-up (up to 20 s, outbound). A client that hangs up and retries quickly now gets two stored checkpoints (the original completes), so up to one more TSA request per completed shadow.
• Docs state the defaults can exceed the 60 s HTTP write timeout (25 + 15 + 10 + 10 s); a per-handler write deadline for POST /v2/checkpoints is a separate follow-up.
• The averin#59 per-project duration gauge deviation still needs the lead's explicit acceptance on feir-ops#27 (no code here).

🤖 Generated with Claude Code