Lower the checkpoint shadow budget default from 5 s to 1 s

docs/dev/CONFIGURATION.md

@@ -203,10 +203,12 @@ statement timeout or runs out of the shadow's own time budget before it has prod
 contiguity guards) is signed, `averin_checkpoint_shadow_failed_total` is incremented, a line starting `ALERT` is
 logged, and that project's next shadow attempt waits for a backoff (10 minutes, doubling per consecutive failure
 up to 64 times that, reset when a shadow runs). A full body that was computed but came back over budget is still compared: a mismatch refuses, a match is
-signed and counted as failed (late) with the same backoff. The shadow's budget is 5 s by default and covers the
+signed and counted as failed (late) with the same backoff. The shadow's budget is 1 s by default (lowered from 5 s: see LIMITATIONS) and covers the
 WHOLE shadow: on Postgres the statement timeout is re-issued with the time that remains before every statement,
 so a checked cut never holds the project write guard for much longer than the budget (the ceiling is 20 s, below
-the 30 s statement timeout). Neither value has an environment variable; they are the `WithCheckpointShadowBudget`
+the 30 s statement timeout); each shadow attempt can hold the project write lock for up to about 1 s at the default. At 0.5 calls/s the full computation
+stops fitting 1 s after roughly an hour of history (an estimate scaled from the soak: about 5 s at about 5 h), after which the failed counter rises and only
+the differential tests and the per-cut guards hold the equality. Neither value has an environment variable; they are the `WithCheckpointShadowBudget`
 (ceiling 20 s) and `WithCheckpointShadowBackoff` options on the server. Alert on any non-zero rate of
 `averin_checkpoint_shadow_failed_total`: it means the shadow has stopped being effective for that history size.
 

docs/dev/LIMITATIONS.md

@@ -154,12 +154,20 @@ What this does not give:
   cut again as the same seq and checked again, also after a restart. After one mismatch
   (`averin_checkpoint_shadow_mismatch_total`, a log line starting `ALERT`) every cut is checked until the process
   restarts. The shadow computation is O(history) and runs inside the project write transaction, so a checked cut
-  takes as long as every cut did before, up to the shadow's own time budget (5 s by default, at most 20 s).
+  takes as long as every cut did before, up to the shadow's own time budget (1 s by default, at most 20 s): each scheduled shadow attempt can hold the
+  project write lock for up to about 1 s (a little more if the last statement overruns).
 - **The shadow stops being effective as history grows.** A shadow that cannot run (the full computation errors,
   hits the statement timeout, or runs out of that budget before producing a body) does not refuse: the incremental body is signed,
   `averin_checkpoint_shadow_failed_total` is incremented, an `ALERT` line is logged, and that project's next
   shadow waits for a backoff (not the next cut). A mismatch still refuses, and so does one found in a full body that came back over budget (a computed body is always compared; a match is signed and counted as late). The budget covers the whole shadow, not each statement. Once the full computation no longer
   fits its budget the counter rises on every attempt and the sampled check is effectively off for that project.
+  The default budget was lowered from 5 s to 1 s after the release-1 soak (about 0.5 calls/s, fresh history): the
+  full computation stopped fitting 5 s reliably from about 5 h of history, and near that boundary a success
+  (which resets the backoff) alternated with failures, so attempts stayed about hourly and each one was a 3.5 to
+  5 s write stall (metered calls of 3.3 to 5.1 s). The cost of the shorter budget is less coverage: as an
+  estimate scaled from that measurement (about 5 s at about 5 h on the soak host), the cross-check stops fitting
+  after roughly an hour of history at 0.5 calls/s, and later at lighter load. It was already ineffective beyond a
+  few hours. The differential tests are the primary assurance of the equality, not the shadow.
   What still holds the equality then is the differential tests (incremental equals full on random histories,
   in memory and on Postgres) and the guards every cut applies itself: the record count must equal the base count
   plus the records after it, every page of those records must hold exactly the next ordinals, and the new grants

formal/claims.json

@@ -1913,7 +1913,7 @@
     },
     {
       "id": "checkpoint-cut-incremental-equals-full",
-      "claim": "The server cuts a checkpoint from the latest checkpoint plus the records after it, and the body equals the one the full computation over the whole project would produce: sequence number and previous hash, record count (the base count plus the records after it), frontier (the base frontier minus the parents of the new records, plus the new records no new record names) and the grant-transparency head and per-broker head (the prior cumulative root folded over the grants after it, chained to the prior head). It refuses to sign when the new grants do not carry exactly the next broker_seq values, when the allocated maximum differs, when the store's record count differs from the base count plus the records after it, or when any page of the records after the base does not hold exactly the next ordinals in order (a record missing from the middle of the range), and it takes the full computation when there is no usable base. The cut whose checkpoint sequence number is a multiple of 100 (per project) and whose project has not had a shadow attempt in the last hour (so the scheduled shadow runs at most once per hour per project), the first incremental cut of a project after a process start, and every cut after a mismatch until restart, also compute the full body with the same timestamp and refuse to sign unless the two are identical; a refused sequence number is retried and shadow-checked again, so a restart does not let it through. A shadow that cannot run (the full computation errors, hits the statement timeout or exceeds its own time budget, 5 s by default and at most 20 s) does not refuse: the incremental body is signed, averin_checkpoint_shadow_failed_total is counted, an alert is logged and that project's next shadow waits for a backoff. The grant log counts a record as a grant only by exact-case keys and string values, as the verifier does. Not that the shadow keeps running as history grows (the full computation is O(history) and stops fitting its budget; the failed counter shows it, and from then on only the differential tests and the per-cut count and contiguity guards hold the equality), not that every unshadowed cut equals the full computation (the equality is argued in a code comment and checked on random histories; a divergence on an unshadowed cut is signed, because checkpoints are append-only, and is caught by the next shadowed cut of that project or by the verifier), that the latest stored checkpoint is intact (it is trusted as the base), that the full computation is cheap (it is O(history), used for the first cut and as the definition), or that a very large frontier costs nothing (every checkpoint carries it).",
+      "claim": "The server cuts a checkpoint from the latest checkpoint plus the records after it, and the body equals the one the full computation over the whole project would produce: sequence number and previous hash, record count (the base count plus the records after it), frontier (the base frontier minus the parents of the new records, plus the new records no new record names) and the grant-transparency head and per-broker head (the prior cumulative root folded over the grants after it, chained to the prior head). It refuses to sign when the new grants do not carry exactly the next broker_seq values, when the allocated maximum differs, when the store's record count differs from the base count plus the records after it, or when any page of the records after the base does not hold exactly the next ordinals in order (a record missing from the middle of the range), and it takes the full computation when there is no usable base. The cut whose checkpoint sequence number is a multiple of 100 (per project) and whose project has not had a shadow attempt in the last hour (so the scheduled shadow runs at most once per hour per project), the first incremental cut of a project after a process start, and every cut after a mismatch until restart, also compute the full body with the same timestamp and refuse to sign unless the two are identical; a refused sequence number is retried and shadow-checked again, so a restart does not let it through. A shadow that cannot run (the full computation errors, hits the statement timeout or exceeds its own time budget, 1 s by default and at most 20 s) does not refuse: the incremental body is signed, averin_checkpoint_shadow_failed_total is counted, an alert is logged and that project's next shadow waits for a backoff. The grant log counts a record as a grant only by exact-case keys and string values, as the verifier does. Not that the shadow keeps running as history grows (the full computation is O(history) and stops fitting its budget; the failed counter shows it, and from then on only the differential tests and the per-cut count and contiguity guards hold the equality), not that every unshadowed cut equals the full computation (the equality is argued in a code comment and checked on random histories; a divergence on an unshadowed cut is signed, because checkpoints are append-only, and is caught by the next shadowed cut of that project or by the verifier), that the latest stored checkpoint is intact (it is trusted as the base), that the full computation is cheap (it is O(history), used for the first cut and as the definition), or that a very large frontier costs nothing (every checkpoint carries it).",
       "class": "tested-implementation",
       "targets": [
         "Go server"

formal/kit-claims.json

@@ -3141,7 +3141,7 @@
         "surface-shadow-min-interval-timer-reset-on-skip",
         "surface-shadow-min-interval-server-wide-timer"
       ],
-      "does_not_establish": "That the incremental cut equals the full computation on every history: the equality is argued in the code comment and checked on random histories (sessions, forced older parents, grants, voids, idempotent retries, idle cuts) and by the shadow check on the cuts of sequence number a multiple of 100 that fall at least an hour after the project's last shadow attempt (so at most one scheduled shadow per hour per project, which is weaker than every 100th cut: an incorrect incremental cut can stay signed for at least an hour of cuts: until the first cut whose sequence number is a multiple of 100 after the hour has passed, and longer while a backoff after a shadow that could not run is in force) and on the first cut of each project after a start, so a divergence on any other cut is signed (a checkpoint is append-only) and is caught at the next shadowed cut of that project or by the verifier. That a corrupted or tampered latest checkpoint is detected on an unshadowed cut: the base is trusted as signed. That a refusal is remembered: it is not stored, it recurs because the refused sequence number is retried and shadow-checked again; a cut that was signed before the next shadowed one stays signed. That the Postgres ordinal and record count are right under concurrent writers (the store tests cover that). That the cost is constant for the frontier: a project with a very large frontier still carries it in every checkpoint. That the shadow keeps running as history grows: the full computation is O(history) and stops fitting its budget, the failed counter shows it, and from then on only the differential tests and the per-cut count and contiguity guards hold the equality. That the full computation, used for the first cut and as the definition, is cheap: it is O(history). The Postgres variants of the differential and cost tests run only in the Postgres CI job."
+      "does_not_establish": "That the incremental cut equals the full computation on every history: the equality is argued in the code comment and checked on random histories (sessions, forced older parents, grants, voids, idempotent retries, idle cuts) and by the shadow check on the cuts of sequence number a multiple of 100 that fall at least an hour after the project's last shadow attempt (so at most one scheduled shadow per hour per project, which is weaker than every 100th cut: an incorrect incremental cut can stay signed for at least an hour of cuts: until the first cut whose sequence number is a multiple of 100 after the hour has passed, and longer while a backoff after a shadow that could not run is in force) and on the first cut of each project after a start, so a divergence on any other cut is signed (a checkpoint is append-only) and is caught at the next shadowed cut of that project or by the verifier. That a corrupted or tampered latest checkpoint is detected on an unshadowed cut: the base is trusted as signed. That a refusal is remembered: it is not stored, it recurs because the refused sequence number is retried and shadow-checked again; a cut that was signed before the next shadowed one stays signed. That the Postgres ordinal and record count are right under concurrent writers (the store tests cover that). That the cost is constant for the frontier: a project with a very large frontier still carries it in every checkpoint. That the shadow keeps running as history grows: the full computation is O(history) and stops fitting its budget (1 s by default; an estimate scaled from the release-1 soak, about 5 s at about 5 h, puts that at roughly an hour of history at 0.5 calls/s), the failed counter shows it, and from then on only the differential tests and the per-cut count and contiguity guards hold the equality. That the full computation, used for the first cut and as the definition, is cheap: it is O(history). The Postgres variants of the differential and cost tests run only in the Postgres CI job."
     },
     {
       "id": "incremental-read-continuity-snapshot",

server/internal/api/checkpoint_cut.go

@@ -32,8 +32,15 @@ const DefaultCheckpointShadowMinInterval = time.Hour
 // The shadow's own time budget and the backoff after a shadow that could not run (lead decision, history
 // scaling PR2): the full computation is O(history) and stops completing as history grows, so it must neither
 // hold the project write guard for the whole statement timeout nor be retried on every cut.
+//
+// The default budget is 1 s (it was 5 s). Release-1 soak evidence: at about 0.5 calls/s the full computation
+// stopped fitting 5 s reliably from about 5 h of history, and near that boundary a success (which resets the
+// backoff) alternated with failures, so attempts stayed about hourly and EACH was a 3.5 to 5 s stall of the
+// project's writes. With 1 s one attempt holds the write lock for about 1 s at most. The trade: the cross-check
+// covers less history (an estimate scaled from that measurement: it stops fitting after roughly an hour of
+// history at 0.5 calls/s, later at lighter load); the differential tests stay the primary assurance.
 const (
-	DefaultCheckpointShadowBudget  = 5 * time.Second
+	DefaultCheckpointShadowBudget  = 1 * time.Second
 	MaxCheckpointShadowBudget      = 20 * time.Second // below the 30 s statement timeout, which it must never reach
 	DefaultCheckpointShadowBackoff = 10 * time.Minute
 	maxShadowBackoffDoublings      = 6 // the wait doubles per consecutive failure up to 64 times the base
@@ -73,7 +80,7 @@ func (s *Server) WithCheckpointShadowEvery(n int) *Server {
 	return s
 }
 
-// WithCheckpointShadowBudget sets the time budget of one shadow computation (default 5 s, at most 20 s, at
+// WithCheckpointShadowBudget sets the time budget of one shadow computation (default 1 s, at most 20 s, at
 // least 1 ms): a shadow that cannot finish inside it does not hold the project write guard any longer and counts
 // as "could not run", not as a mismatch.
 func (s *Server) WithCheckpointShadowBudget(d time.Duration) *Server {

server/internal/api/checkpoint_cut_shadow_test.go

@@ -170,6 +170,9 @@ func TestCheckpointCutShadowBudgetIsClamped(t *testing.T) {
 	if got := s.ShadowBudgetForTest(); got != api.MaxCheckpointShadowBudget {
 		t.Fatalf("effective budget %s after asking for 60s, want the ceiling %s", got, api.MaxCheckpointShadowBudget)
 	}
+	if api.DefaultCheckpointShadowBudget != time.Second {
+		t.Fatalf("default shadow budget %s, want 1s (a longer default stalls project writes for that long per attempt)", api.DefaultCheckpointShadowBudget)
+	}
 	if got := api.New(mustCore(t), store.NewMem(), "k0").ShadowBudgetForTest(); got != api.DefaultCheckpointShadowBudget {
 		t.Fatalf("default effective budget %s, want %s", got, api.DefaultCheckpointShadowBudget)
 	}