Skip to content

Rate-limit the scheduled checkpoint shadow to once per hour per project - #52

Merged
zachyking merged 5 commits into
mainfrom
fix/shadow-min-interval
Oct 26, 2026
Merged

zachyking merged 5 commits into
mainfrom
fix/shadow-min-interval

Conversation

@zachyking

@zachyking zachyking commented Oct 26, 2026 •

Copy link
Copy Markdown
Member

Problem

The checkpoint shadow check (full O(history) computation) runs under the project write lock, inside a 5 s budget. For a verified project it runs on every cut with seq % 100 == 0. At a cut every 3 s that is about every 5 minutes, and in the 2026-10-21 proof run every metered call slower than 300 ms began on that grid (stall 0.35 s at 1 h of history, 1.4 s at 2.9 h).

Change

  • DefaultCheckpointShadowMinInterval = 1h and a per-project last-attempt time (any outcome).
  • A scheduled shadow (verified, not latched, seq % every == 0) runs only if the last attempt is at least that old. Otherwise the incremental body is signed as for any other cut.
  • Not rate-limited: the first incremental cut since start, and every cut once a mismatch has latched. The failure backoff is unchanged.
  • WithCheckpointShadowMinInterval(d): d < 0 is 0 (no limit), d above the default is clamped to it, so the knob only tightens. No env var, no flag.
  • This WEAKENS shadow coverage: cadence is max(every 100th cut, once per hour per project). Docs, doc comments, claims and the metric help say so. The remaining stall (one shadow per hour per project, and the first cut after every start, up to the 5 s budget) is stated in LIMITATIONS.

Formal

  • Statements in formal/kit-claims.json and formal/claims.json weakened to the new cadence. In claim checkpoint-cut-incremental-equals-full, relocked checkpointBodyChecked and newly covered and locked shadowTooSoon, shadowAttempted, shadowMinInterval and WithCheckpointShadowMinInterval. FORMAL.md re-rendered. Its does_not_establish states the real gap (lead follow-up e4bc93a): an incorrect cut can stay signed for AT LEAST an hour of cuts, until the first due seq after the hour, and longer under a backoff.
  • New mutants: surface-shadow-min-interval-not-enforced, surface-shadow-min-interval-timer-reset-on-skip and surface-shadow-min-interval-server-wide-timer, all killed (check_mutants.py --only). Three existing shadow mutant patches regenerated (context shift only, same edits).
  • Mutants killed: the new one, never-runs, skips-first-cut, ignores-backoff, cannot-run-refuses, mismatch-still-signs, global-counter.

Tests

New checkpoint_cut_mininterval_test.go (limit within the hour, shadow after the interval, per-project first cut, latched, interval 0, clamp, failed attempt counts toward both backoff and interval). Existing tests that need a due shadow inside the same hour now set the interval to 0.

Gates

make test-server, go vet, gofmt, both claim checks (753 checks, 0 failures; legacy 52 claims) all green. The lead added TestCheckpointCutShadowMinIntervalUnverifiedIsExempt, which kills the 'verified && dropped' mutation. The fix round added TestCheckpointCutShadowMinIntervalEachProjectStillShadowsHourly (rotation of two projects for 180 min, exact count 6).

🤖 Generated with Claude Code

zachyking and others added 5 commits October 26, 2026 12:49
The shadow check is O(history) and runs under the project write lock. At a
cut every 3 s, 1 in 100 came due every ~5 minutes and stalled writes for up
to the shadow budget. A scheduled shadow now also needs the project's last
shadow attempt to be at least DefaultCheckpointShadowMinInterval (1 h) old.
The first cut after a start and every cut after a mismatch are not limited.
The builder knob can only tighten the interval. Docs and claims state the
weaker cadence.

Co-Authored-By: Claude Opus 5.5 <[email protected]>
…adow

Add a rotation test (two projects, 180 minutes) that requires each project to
keep getting a scheduled shadow about once an hour, and two kit mutants (timer
reset on a skipped cut, server-wide timer). Cover the new helpers in the claim.
Remove the stray checkpoint_cut.go.orig.

Co-Authored-By: Claude Opus 5.5 <[email protected]>
…exemption

Review findings left after the fix round:
- The claim and LIMITATIONS said an incorrect cut 'can stay signed for up to
  an hour of cuts'. The gap is at least an hour: until the first cut whose seq
  is a multiple of 100 after the hour, longer under a backoff. Wording
  corrected (weaker, as docs must only get); FORMAL.md re-rendered.
- New test: an unverified project (first shadow could not run) retries after
  the 10 min backoff, not after the hour. Dropping 'verified &&' from the
  rate-limit condition now fails it.
- createCheckpointTx comment no longer says every 100th cut is checked.

Co-Authored-By: Claude Opus 5.5 <[email protected]>
@zachyking
zachyking merged commit 4d6e1f8 into main Oct 26, 2026
36 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant