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

docs/dev/CONFIGURATION.md

@@ -188,8 +188,10 @@ the pinned-key id — so a govder/averin key misalignment is visible in both met
 ### Checkpoint cut shadow check (no setting)
 
 Checkpoints are cut incrementally (see LIMITATIONS, "Checkpoint cut is incremental, with a sampled shadow check").
-The cut of checkpoint seq 100, 200, ... of each project, and the first incremental cut of each project after the
-process starts, are also computed in full and refused if they differ. There is no environment variable
+The first incremental cut of each project after the process starts, the cut of checkpoint seq 100, 200, ... of a
+project when its last shadow attempt is at least one hour old, and every cut after a mismatch, are also computed in
+full and refused if they differ. There is no setting for the one-hour minimum interval: production uses the default
+(a server builder can only tighten it). There is no environment variable
 to turn this off. Alert on `averin_checkpoint_shadow_mismatch_total > 0`: a mismatch refuses that checkpoint
 (`POST /v2/checkpoints` returns 500, "the incremental cut disagrees with the full computation"), logs a line
 starting `ALERT`, and makes every later cut a checked cut until the process restarts, except while a project waits out the backoff after a shadow that could not run (below): that project's incremental body is then signed unchecked. The refused seq is retried as

docs/dev/LIMITATIONS.md

@@ -136,8 +136,16 @@ What this does not give:
 - **The incremental cut trusts the latest stored checkpoint** as the base. It is signed, but the cut does not
   re-verify the signature or the chain below it. A latest checkpoint that was corrupted in the store (not by the
   signing key) is carried forward by every unshadowed cut.
-- **The check against the full computation is sampled, per project.** The cut of checkpoint seq 100, 200, ... of a
-  project also computes the full body and refuses to sign unless it is byte-identical
+- **The check against the full computation is sampled, per project, and rate-limited.** The cut of checkpoint seq
+  100, 200, ... of a project also computes the full body, but only if the project's last shadow attempt (whatever its
+  outcome) is at least one hour old (`DefaultCheckpointShadowMinInterval`), so the scheduled cadence is
+  max(every 100th cut, once per hour per project). This is weaker than a plain 1-in-100 sample: an incorrect
+  incremental cut can stay signed for at least an hour of cuts: until the first cut whose seq 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. The
+  limit exists because the shadow runs under the project write lock; at 1-in-100 and a cut every 3 s it ran every
+  ~5 minutes and each run stalled writes for up to its budget. The first cut after a start and every cut after a
+  mismatch are not rate-limited. The remaining stall: one shadow per hour per project, and the first cut after
+  every start, can each still hold the project write lock for up to the 5 s budget. A checked cut refuses to sign unless the full body is byte-identical
   (`averin_checkpoint_shadow_checks_total`); the sample is chosen from the checkpoint being cut, so it does not
   depend on how cuts of different projects interleave. The first incremental cut of each project after the process
   starts is also checked once, which covers a base changed while the process was down and the first cut after an

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), 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, 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).",
       "class": "tested-implementation",
       "targets": [
         "Go server"

formal/kit-claims.json

@@ -821,6 +821,18 @@
       "tier": "full",
       "claim": "checkpoint-cut-incremental-equals-full"
     },
+    "surface-shadow-min-interval-timer-reset-on-skip": {
+      "tier": "full",
+      "claim": "checkpoint-cut-incremental-equals-full"
+    },
+    "surface-shadow-min-interval-server-wide-timer": {
+      "tier": "full",
+      "claim": "checkpoint-cut-incremental-equals-full"
+    },
+    "surface-shadow-min-interval-not-enforced": {
+      "tier": "full",
+      "claim": "checkpoint-cut-incremental-equals-full"
+    },
     "checkpoint-cut-skips-page-ordinal-check": {
       "tier": "fast",
       "claim": "checkpoint-cut-incremental-equals-full"
@@ -3011,7 +3023,7 @@
     {
       "id": "checkpoint-cut-incremental-equals-full",
       "$comment": "legacy register: checkpoint-cut-incremental-equals-full",
-      "statement": "The checkpoint cut reads the latest checkpoint and the records after it (not the whole history) and produces the same body as the full computation over the whole project: the same sequence number and previous hash, the record count as the base count plus the records after it, the frontier as the base frontier minus the parents of the new records plus the new records no new record names, and the grant-transparency head (and the per-broker head of a federated broker) as the prior head's cumulative root folded over the grants after it, chained to the prior head; it refuses to sign unless the new grants carry exactly the next broker_seq values and the allocated maximum matches, and refuses when the store's record count differs from the base count plus the records after it or when a page of the records after the base does not hold exactly the next ordinals in order; it takes the full computation when there is no usable base. A cut also computes the full body with the same timestamp and refuses to sign, with an alert and a counter, unless the two are identical, when the checkpoint being cut has a sequence number that is a multiple of 100 (chosen per project, so a rotation of projects cannot dodge it, and a refused sequence number is shadow-checked again after a restart), when it is the project's first incremental cut since the process started, and for every cut once a mismatch has been seen. A shadow that cannot run (the full computation errors, hits the statement timeout or runs out of its own time budget before producing a body) does not refuse: the incremental body is signed, a failed counter moves, an alert is logged and the project's next shadow waits for a backoff; a full body that was computed but came back over budget is still compared, a mismatch refuses and a match is signed and counted as late. The grant log counts a record as a grant or void tombstone only by exact-case keys and string values, as the verifier does; a record with a differently cased key or a value of another type is neither counted nor an error, in the full and the incremental cut alike. The rows a cut reads are the same at 1, 3 and 12 months of history.",
+      "statement": "The checkpoint cut reads the latest checkpoint and the records after it (not the whole history) and produces the same body as the full computation over the whole project: the same sequence number and previous hash, the record count as the base count plus the records after it, the frontier as the base frontier minus the parents of the new records plus the new records no new record names, and the grant-transparency head (and the per-broker head of a federated broker) as the prior head's cumulative root folded over the grants after it, chained to the prior head; it refuses to sign unless the new grants carry exactly the next broker_seq values and the allocated maximum matches, and refuses when the store's record count differs from the base count plus the records after it or when a page of the records after the base does not hold exactly the next ordinals in order; it takes the full computation when there is no usable base. A cut also computes the full body with the same timestamp and refuses to sign, with an alert and a counter, unless the two are identical, when the checkpoint being cut has a sequence number that is a multiple of 100 and the project has not had a shadow attempt (of any outcome) in the last hour (chosen per project, so a rotation of projects cannot dodge it; the scheduled shadow therefore runs at most once per hour per project, and a refused sequence number is shadow-checked again after a restart), when it is the project's first incremental cut since the process started, and for every cut once a mismatch has been seen. A shadow that cannot run (the full computation errors, hits the statement timeout or runs out of its own time budget before producing a body) does not refuse: the incremental body is signed, a failed counter moves, an alert is logged and the project's next shadow waits for a backoff; a full body that was computed but came back over budget is still compared, a mismatch refuses and a match is signed and counted as late. The grant log counts a record as a grant or void tombstone only by exact-case keys and string values, as the verifier does; a record with a differently cased key or a value of another type is neither counted nor an error, in the full and the incremental cut alike. The rows a cut reads are the same at 1, 3 and 12 months of history.",
       "method": "property",
       "artifacts": [
         "server/internal/api/checkpoint_cut.go",
@@ -3021,7 +3033,8 @@
         "server/internal/broker/transparency.go",
         "server/internal/store/store.go",
         "server/internal/api/checkpoint_cut_exact_test.go",
-        "server/internal/api/checkpoint_cut_shadow_test.go"
+        "server/internal/api/checkpoint_cut_shadow_test.go",
+        "server/internal/api/checkpoint_cut_mininterval_test.go"
       ],
       "gates": [
         "server"
@@ -3051,7 +3064,27 @@
         {
           "path": "server/internal/api/checkpoint_cut.go",
           "symbol": "checkpointBodyChecked",
-          "sha256": "81cdd54177dd574996f83c896a13cd782f4b78d475b2579ea12fcb0da1bf9dfd"
+          "sha256": "1857d2bd19ffee127f85facdb506dd712b498c14ea90083d1b0e0d6e63c03699"
+        },
+        {
+          "path": "server/internal/api/checkpoint_cut.go",
+          "symbol": "shadowTooSoon",
+          "sha256": "9fd3f6d3a1cffce9e1ea9461183cf97dd89e7a03b9dc79a0e5ea57be450d64bc"
+        },
+        {
+          "path": "server/internal/api/checkpoint_cut.go",
+          "symbol": "shadowAttempted",
+          "sha256": "29ab21c7729d3954ba6b7e3313d69d0ada8fc3a978793a4ec4d7ad13608f3934"
+        },
+        {
+          "path": "server/internal/api/checkpoint_cut.go",
+          "symbol": "shadowMinInterval",
+          "sha256": "3fe40626f6c3d01fa3b057748747152d9a53430882a795745c3c49c90c3a5eb5"
+        },
+        {
+          "path": "server/internal/api/checkpoint_cut.go",
+          "symbol": "WithCheckpointShadowMinInterval",
+          "sha256": "ce2e59efe91cb3703eb25264663534206c9cb59037ebd0e02060ba29a67b693f"
         },
         {
           "path": "server/internal/api/server.go",
@@ -3103,9 +3136,12 @@
         "checkpoint-cut-shadow-cannot-run-refuses",
         "checkpoint-cut-over-budget-full-body-not-compared",
         "checkpoint-cut-shadow-ignores-backoff",
-        "checkpoint-cut-skips-page-ordinal-check"
+        "checkpoint-cut-skips-page-ordinal-check",
+        "surface-shadow-min-interval-not-enforced",
+        "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 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, 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",