diff --git a/docs/dev/CONFIGURATION.md b/docs/dev/CONFIGURATION.md index 4df3f36d..8979b7be 100644 --- a/docs/dev/CONFIGURATION.md +++ b/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 diff --git a/docs/dev/FORMAL.md b/docs/dev/FORMAL.md index 376183f4..6ca8efca 100644 --- a/docs/dev/FORMAL.md +++ b/docs/dev/FORMAL.md @@ -167,7 +167,7 @@ markers fails too). Edit the claims, not the table. | `cross-impl-refusal-vector` | differential-vectors | The native verifier, the cgo FFI and the WASM verifier produce the same refusal fields (ok, gateway_refusals, gateway_refusal_attempts, gateway_refusals_by_class, and whether a refusal shape issue is present) for the four committed rows: a refusals bundle, a legacy event_type-only bundle, an unknown-class bundle and the capstone with refusals; the report serializer always carries the three fields. | That the three targets agree on inputs outside the four rows. The detector runs the native replay only; the cgo and WASM replays run in the server and verifier jobs, and the expectations in the file come from the native verifier and are pinned to literals in the same test file. The vectors are signed by test-only keys. | `core`, `server`, `verifier` | none recorded | | `cgo-bundle-verify-heap-trim` | test | After each full-bundle verification through cgo (Core.VerifyBundle and Core.VerifyBundleWith, which VerifyBundleWithAuthority and VerifyBundleWithRoles call), the server asks glibc to return freed C-heap pages to the OS with malloc_trim(0), once per verification and after the bundle copy and the Rust result are freed; on a build whose C library is not glibc the call is a no-op. A server test seals 1000 generic records over 12 sessions with 10 checkpoints, verifies the resulting bundle once on each of 8 distinct locked OS threads and requires resident memory to grow by less than 32 MB (without the trim the same test grows about 50 MB); it skips with a message where the trim is not supported. | That memory is bounded: only the C-heap arenas touched by whole-bundle verification are trimmed, on glibc. Other allocators (musl, jemalloc, a different libc) are not covered, and on them nothing is returned. The cost of the verification itself (CPU, and the transient O(bundle) peak while it runs) and any Go-heap growth are unchanged. It does not address history growth: whole-history exports and verifications still grow with the project and are still capped at the single-bundle limit (a separate design). The test measures resident memory of one process on a 0.9 MB bundle with a 32 MB tolerance, so it detects retention of about one verification peak per thread, not small leaks, and it calls only VerifyBundleWith; the trim in VerifyBundle (no options) is covered by the mutant only because that mutant removes both. The trim is not run on the early return for a bundle with a NUL byte, which allocates nothing in C. | `server` | none recorded | | `oldest-uncovered-received-at` | test | The verifier reports oldest_uncovered_received_at: the earliest received_ts among the records that are not in the causal closure (the verifier's own committed set) of the frontier of the latest verified checkpoint; with no verified checkpoint, the earliest received_ts of all records; null when every record is covered. Tests on real verifier output check a young tail (the first record the tail adds), a checkpoint that omits a live session while another session grows (the omitted session's oldest record, not the growing tail), a bundle served with only an earlier checkpoint (rollback), a latest checkpoint whose frontier is behind an earlier one (only the latest counts), no checkpoint yet, and all records covered. The field is display-only and feeds no verdict. | That the timestamp is true: received_ts is the recorder's own clock reading, signed with the record, so a recorder that stamps old times can make a tail look old and one that stamps future times can make it look young; a consumer must treat the age as a display bound, not evidence. It does not say a checkpoint is correct or that an old uncovered record is an attack: a stalled checkpointer, an omitted session and a rollback all look the same here. A record with no canonical received_ts reports the epoch. Nothing here changes any verdict. | `core`, `formal-fast` | none recorded | -| `checkpoint-cut-incremental-equals-full` | property | 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. | 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. | `server` | none recorded | +| `checkpoint-cut-incremental-equals-full` | property | 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. | 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. | `server` | none recorded | | `incremental-read-continuity-snapshot` | property | GET /v2/records with after=&order=asc returns, oldest first, the records with insertion ordinal n+1 onward (at most limit, capped at 1000), and from the same repeatable-read snapshot the store's record total, the latest checkpoint (seq, hash, record_count) and, when at_seq= is given, the checkpoint with that seq (absent when the project has no such seq). The records are the same rows the store holds at those ordinals; next_after is after plus the page length and more says whether records remain past it. A store error, a checkpoint whose record_count cannot be read, or a page whose ordinals are not exactly after+1 onward (or that stops short of the total) is a 500, never an empty page, a count of zero or a 200 that repeats one record and hides another; a request that is not exactly this shape (order other than asc, a missing, negative or non-numeric after, at_seq without after, offset with after) is a 400. The rows read are the page plus two checkpoint rows, the same at 1, 3 and 12 months of history. The read runs no verification and builds no bundle. | That the records served are authentic: the read verifies nothing, so what a reader holds afterwards is a read frontier bound to a signed checkpoint that it can compare on the next read, not a verified one. That a reader detects an in-place rewrite below its frontier: that is the reader's rolling re-read, not this endpoint. That the snapshot is consistent across pages: each page is its own snapshot, so a reader must check the continuity fields (the checkpoint at its frontier seq, the latest seq, record counts and total) on every page. That the Postgres read uses the ordinal index in every plan: the Postgres cost test counts rows, and runs only in the Postgres CI job. | `server` | none recorded | | `session-heads-incremental-equals-full` | property | On Postgres, Heads(project, session) reads the session_heads table and returns exactly what the full scan (every record of the session that no record of the same project and session lists in parents, byte-sorted, never nil) returns, after every PutRecord of a random history: forks, merges, server-forced parents from another session, duplicate parents, several sessions and projects, idempotent replays, content-hash collapses and a replay carrying a different parent list. PutRecord changes session_heads only when it inserted a new row, in the transaction of that insert: it removes the new record's parents from the session's heads and adds the record, and a rolled-back transaction leaves the table as it was. Migration 0009 backfills the table from existing records (random DAG with cross-session, duplicate and dangling parents) to the same set, and the runtime-role check requires SELECT, INSERT and DELETE on it. The read costs one index lookup on (project, session) however long the session is. | Not that the table equals the full scan on every history: it is checked on seeded random histories and one migration fixture, not proved. A record that names a parent that is not yet in the store, when that parent is later inserted into the same session, is left listed as a head by the table although the full scan would not list it; the seal path does not produce that and the verifier rejects a missing parent. A writer that inserts into records without PutRecord (a test, an operator's SQL) leaves the table stale. Not the in-memory store, which scans the session on every seal. Not ProjectHeads, which still reads the whole project. Not that the planner uses the primary key index at any size or statistics: the soak measurement is recorded in the pull request, not asserted by a test. The seal-latency test (AVERIN_SEAL_LATENCY=1) is a manual measurement and is not part of this detector. Without AVERIN_TEST_DATABASE_URL the Postgres tests skip, so a local run without a database proves nothing about this claim. | `store-postgres`, `formal-fast` | none recorded | | `use-outcome-lookup-equals-scan` | property | The use-outcome lookups return exactly what the whole-session scan they replaced returned. Store.IntentRecord(project, session, recordID) finds the record of that session whose record_id is recordID and which carries a non-empty extensions.broker.kind, and Store.UseOutcomeFor(project, session, intentRef) returns the record_id of the first use_outcome record, in insertion order, of that session whose extensions.broker.use_outcome.intent_ref is intentRef. On Postgres and on the in-memory store, over seeded random histories in several sessions and projects (intents, outcomes, several outcomes for one intent, generic records carrying a use_outcome block or no broker kind, empty kind, a grant carrying a use_outcome block, records of the wrong JSON type or without a record_id, a 6000-byte intent_ref, idempotent replays, an intent_ref naming an intent of another session or project), api.intentAndOutcome's two lookups equal the scan for every record_id and intent_ref of the history and for absent, empty and unusual ones, in every session. A record_id reused in another session of the project is refused (ErrRecordIDConflict), so an intent cannot exist twice across sessions. On Postgres the intent lookup is answered through records_project_record_id_uniq and the outcome lookup through records_use_outcome_intent_idx (asserted from EXPLAIN on a 6000-row session), migration 0010 builds that index over existing rows (stamped v9 to v10 through the cutover, index valid and partial, lookups correct, a 6000-byte intent_ref still insertable), and a read error from either lookup propagates instead of reading as not found. | Not that the lookup equals the scan on every history: it is checked on seeded random histories, not proved. The Postgres lookups read exact JSON key names while the scan's Go decoder also accepts keys that differ only in letter case, so on a record with such keys the lookup is stricter (a sealed record never has them, and a generic record cannot set extensions.broker). With a historical non-unique record_id index the first row satisfying the scan's conditions is returned, which the tests do not exercise. An empty intent_record_id is answered from the session, not from the index (the API rejects it). Not the in-memory store's cost, which still scans the session. Not that the planner uses the indexes at any statistics or size beyond the 6000-row plan test; the latency numbers (AVERIN_INTENT_LATENCY=1) are a manual measurement recorded in the pull request, not part of this detector. Not the seal path, the rest of /v2/use-outcome or the exactly-once rule beyond the lookups it reads. Without AVERIN_TEST_DATABASE_URL the Postgres tests skip, so a local run without a database proves nothing about this claim. The api-level copy of the equivalence test (intentAndOutcomeScan) runs in the store-postgres job, not in this detector. | `store-postgres`, `formal-fast` | none recorded | diff --git a/docs/dev/LIMITATIONS.md b/docs/dev/LIMITATIONS.md index d1d15fd0..26ec4a17 100644 --- a/docs/dev/LIMITATIONS.md +++ b/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 diff --git a/formal/claims.json b/formal/claims.json index 2f2b9156..842af009 100644 --- a/formal/claims.json +++ b/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" diff --git a/formal/kit-claims.json b/formal/kit-claims.json index ce0a1d8f..a4ca852b 100644 --- a/formal/kit-claims.json +++ b/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", diff --git a/formal/mutants/checkpoint-cut-shadow-ignores-backoff.patch b/formal/mutants/checkpoint-cut-shadow-ignores-backoff.patch index bed1585e..8b0c8076 100644 --- a/formal/mutants/checkpoint-cut-shadow-ignores-backoff.patch +++ b/formal/mutants/checkpoint-cut-shadow-ignores-backoff.patch @@ -1,12 +1,13 @@ diff --git a/server/internal/api/checkpoint_cut.go b/server/internal/api/checkpoint_cut.go +index 689be4d..38b26b2 100644 --- a/server/internal/api/checkpoint_cut.go +++ b/server/internal/api/checkpoint_cut.go -@@ -350,7 +350,7 @@ func (s *Server) checkpointBodyChecked(st store.Store, projectID string) (map[st - if verified && !s.cut.latched.Load() && seq%every != 0 { - return body, nil +@@ -414,7 +414,7 @@ func (s *Server) checkpointBodyChecked(st store.Store, projectID string) (map[st + if verified && !s.cut.latched.Load() && s.shadowTooSoon(projectID) { + return body, nil // scheduled shadow, but the project's last attempt is inside the minimum interval } - if s.shadowWaiting(projectID) { + if false && s.shadowWaiting(projectID) { return body, nil // the last shadow of this project could not run: wait out its backoff, then try again } - s.mCutShadowChecks.Inc() + s.shadowAttempted(projectID) diff --git a/formal/mutants/checkpoint-cut-shadow-never-runs.patch b/formal/mutants/checkpoint-cut-shadow-never-runs.patch index a75dcff5..cac09b04 100644 --- a/formal/mutants/checkpoint-cut-shadow-never-runs.patch +++ b/formal/mutants/checkpoint-cut-shadow-never-runs.patch @@ -1,7 +1,8 @@ diff --git a/server/internal/api/checkpoint_cut.go b/server/internal/api/checkpoint_cut.go +index 689be4d..91af1c3 100644 --- a/server/internal/api/checkpoint_cut.go +++ b/server/internal/api/checkpoint_cut.go -@@ -347,7 +347,7 @@ func (s *Server) checkpointBodyChecked(st store.Store, projectID string) (map[st +@@ -408,7 +408,7 @@ func (s *Server) checkpointBodyChecked(st store.Store, projectID string) (map[st } seq, _ := body["checkpoint_seq"].(int64) _, verified := s.cut.verified.Load(projectID) @@ -9,4 +10,4 @@ diff --git a/server/internal/api/checkpoint_cut.go b/server/internal/api/checkpo + if true || verified && !s.cut.latched.Load() && seq%every != 0 { return body, nil } - if s.shadowWaiting(projectID) { + if verified && !s.cut.latched.Load() && s.shadowTooSoon(projectID) { diff --git a/formal/mutants/checkpoint-cut-shadow-skips-first-cut.patch b/formal/mutants/checkpoint-cut-shadow-skips-first-cut.patch index bc786c59..8ef53d7e 100644 --- a/formal/mutants/checkpoint-cut-shadow-skips-first-cut.patch +++ b/formal/mutants/checkpoint-cut-shadow-skips-first-cut.patch @@ -1,7 +1,8 @@ diff --git a/server/internal/api/checkpoint_cut.go b/server/internal/api/checkpoint_cut.go +index 689be4d..ba77f07 100644 --- a/server/internal/api/checkpoint_cut.go +++ b/server/internal/api/checkpoint_cut.go -@@ -347,7 +347,7 @@ func (s *Server) checkpointBodyChecked(st store.Store, projectID string) (map[st +@@ -408,7 +408,7 @@ func (s *Server) checkpointBodyChecked(st store.Store, projectID string) (map[st } seq, _ := body["checkpoint_seq"].(int64) _, verified := s.cut.verified.Load(projectID) @@ -9,4 +10,4 @@ diff --git a/server/internal/api/checkpoint_cut.go b/server/internal/api/checkpo + if (verified || true) && !s.cut.latched.Load() && seq%every != 0 { return body, nil } - if s.shadowWaiting(projectID) { + if verified && !s.cut.latched.Load() && s.shadowTooSoon(projectID) { diff --git a/formal/mutants/surface-shadow-min-interval-not-enforced.patch b/formal/mutants/surface-shadow-min-interval-not-enforced.patch new file mode 100644 index 00000000..b7013d55 --- /dev/null +++ b/formal/mutants/surface-shadow-min-interval-not-enforced.patch @@ -0,0 +1,13 @@ +diff --git a/server/internal/api/checkpoint_cut.go b/server/internal/api/checkpoint_cut.go +index 689be4d..bdf1e64 100644 +--- a/server/internal/api/checkpoint_cut.go ++++ b/server/internal/api/checkpoint_cut.go +@@ -411,7 +411,7 @@ func (s *Server) checkpointBodyChecked(st store.Store, projectID string) (map[st + if verified && !s.cut.latched.Load() && seq%every != 0 { + return body, nil + } +- if verified && !s.cut.latched.Load() && s.shadowTooSoon(projectID) { ++ if false && verified && !s.cut.latched.Load() && s.shadowTooSoon(projectID) { + return body, nil // scheduled shadow, but the project's last attempt is inside the minimum interval + } + if s.shadowWaiting(projectID) { diff --git a/formal/mutants/surface-shadow-min-interval-server-wide-timer.patch b/formal/mutants/surface-shadow-min-interval-server-wide-timer.patch new file mode 100644 index 00000000..66c14e1a --- /dev/null +++ b/formal/mutants/surface-shadow-min-interval-server-wide-timer.patch @@ -0,0 +1,22 @@ +diff --git a/server/internal/api/checkpoint_cut.go b/server/internal/api/checkpoint_cut.go +index 689be4d..96389d0 100644 +--- a/server/internal/api/checkpoint_cut.go ++++ b/server/internal/api/checkpoint_cut.go +@@ -128,7 +128,7 @@ func (s *Server) shadowTooSoon(projectID string) bool { + } + s.cut.mu.Lock() + defer s.cut.mu.Unlock() +- t, ok := s.cut.lastTry[projectID] ++ t, ok := s.cut.lastTry[""] + return ok && s.now().Sub(t) < ival + } + +@@ -139,7 +139,7 @@ func (s *Server) shadowAttempted(projectID string) { + if s.cut.lastTry == nil { + s.cut.lastTry = map[string]time.Time{} + } +- s.cut.lastTry[projectID] = s.now() ++ s.cut.lastTry[""] = s.now() + } + + // shadowWaiting reports whether the project's next shadow attempt is still inside its backoff. diff --git a/formal/mutants/surface-shadow-min-interval-timer-reset-on-skip.patch b/formal/mutants/surface-shadow-min-interval-timer-reset-on-skip.patch new file mode 100644 index 00000000..24fdb9ff --- /dev/null +++ b/formal/mutants/surface-shadow-min-interval-timer-reset-on-skip.patch @@ -0,0 +1,12 @@ +diff --git a/server/internal/api/checkpoint_cut.go b/server/internal/api/checkpoint_cut.go +index 689be4d..2ec4dd4 100644 +--- a/server/internal/api/checkpoint_cut.go ++++ b/server/internal/api/checkpoint_cut.go +@@ -412,6 +412,7 @@ func (s *Server) checkpointBodyChecked(st store.Store, projectID string) (map[st + return body, nil + } + if verified && !s.cut.latched.Load() && s.shadowTooSoon(projectID) { ++ s.shadowAttempted(projectID) + return body, nil // scheduled shadow, but the project's last attempt is inside the minimum interval + } + if s.shadowWaiting(projectID) { diff --git a/server/internal/api/checkpoint_cut.go b/server/internal/api/checkpoint_cut.go index d2df461c..689be4d2 100644 --- a/server/internal/api/checkpoint_cut.go +++ b/server/internal/api/checkpoint_cut.go @@ -15,10 +15,20 @@ import ( "github.com/feirai/averin/server/internal/store" ) -// DefaultCheckpointShadowEvery is how often (1 in N incremental cuts) the full computation is also run and -// compared. A mismatch refuses to sign. +// DefaultCheckpointShadowEvery is how often (1 in N incremental cuts) the full computation is scheduled to also +// run and be compared. A mismatch refuses to sign. A scheduled shadow only runs when the project's last shadow +// attempt is at least DefaultCheckpointShadowMinInterval old, so the effective cadence of the scheduled check is +// max(every 100th cut, once per hour per project). The first incremental cut after a start and every cut after +// a mismatch are not rate-limited. const DefaultCheckpointShadowEvery = 100 +// DefaultCheckpointShadowMinInterval is the least time between two shadow attempts of one project on the +// scheduled path (a verified project, nothing latched). The shadow is O(history) and runs under the project write +// lock, so at a high cut rate "every 100th cut" came due every few minutes and each run stalled the project for up +// to the shadow budget. This WEAKENS what the scheduled shadow covers: between two attempts an incorrect +// incremental cut is caught only by the per-cut count and contiguity guards, not by the full comparison. +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. @@ -39,8 +49,11 @@ type checkpointCutState struct { budget time.Duration // 0 means DefaultCheckpointShadowBudget backoff time.Duration // 0 means DefaultCheckpointShadowBackoff + minIval time.Duration // minimum time between scheduled shadow attempts; only tightened below the default via the builder + minSet bool // minIval was set explicitly (0 then means no rate limit) mu sync.Mutex retry map[string]shadowRetry // project -> when its next shadow attempt may run + lastTry map[string]time.Time // project -> start of its last shadow attempt, whatever the outcome } // shadowRetry is the backoff state of one project after a shadow that could not run. @@ -85,6 +98,50 @@ func (s *Server) WithCheckpointShadowBackoff(d time.Duration) *Server { return s } +// WithCheckpointShadowMinInterval sets the least time between two scheduled shadow attempts of one project +// (default DefaultCheckpointShadowMinInterval, 1 h). d < 0 is treated as 0, which disables the rate limit (the +// strictest setting); d above the default is clamped to it, so the knob can only tighten the check. +func (s *Server) WithCheckpointShadowMinInterval(d time.Duration) *Server { + if d < 0 { + d = 0 + } + if d > DefaultCheckpointShadowMinInterval { + d = DefaultCheckpointShadowMinInterval + } + s.cut.minIval = d + s.cut.minSet = true + return s +} + +func (s *Server) shadowMinInterval() time.Duration { + if !s.cut.minSet { + return DefaultCheckpointShadowMinInterval + } + return s.cut.minIval +} + +// shadowTooSoon reports whether the project's last shadow attempt is younger than the minimum interval. +func (s *Server) shadowTooSoon(projectID string) bool { + ival := s.shadowMinInterval() + if ival <= 0 { + return false + } + s.cut.mu.Lock() + defer s.cut.mu.Unlock() + t, ok := s.cut.lastTry[projectID] + return ok && s.now().Sub(t) < ival +} + +// shadowAttempted records the start of a shadow attempt (any outcome). +func (s *Server) shadowAttempted(projectID string) { + s.cut.mu.Lock() + defer s.cut.mu.Unlock() + if s.cut.lastTry == nil { + s.cut.lastTry = map[string]time.Time{} + } + s.cut.lastTry[projectID] = s.now() +} + // shadowWaiting reports whether the project's next shadow attempt is still inside its backoff. func (s *Server) shadowWaiting(projectID string) bool { s.cut.mu.Lock() @@ -321,7 +378,10 @@ func (s *Server) checkpointBody(projectID string, seq int64, prev string, hasPre // computation. The full body is also computed with the same created_ts, and signing is REFUSED unless the two are // byte-identical, when (a) the checkpoint being cut has seq % every == 0 (chosen per project from the checkpoint // itself, so no project can be skipped by a rotation of cuts, and a refused seq is retried as the same seq and -// shadowed again, also after a restart, so a refusal needs no stored state to stay a refusal), (b) it is the +// shadowed again, also after a restart, so a refusal needs no stored state to stay a refusal; this scheduled +// shadow is additionally rate-limited to one attempt per project per DefaultCheckpointShadowMinInterval, so its +// cadence is max(every 100th cut, once per hour per project) and a due cut inside that hour is signed +// incrementally without a shadow), (b) it is the // first incremental cut of the project since this process started and has not yet passed a shadow check (a base // altered while the process was down, and a first cut after migration), or (c) a mismatch has latched. An // incremental cut that disagrees with the definition must never reach a signature, because checkpoints are @@ -351,9 +411,13 @@ func (s *Server) checkpointBodyChecked(st store.Store, projectID string) (map[st if verified && !s.cut.latched.Load() && seq%every != 0 { return body, nil } + if verified && !s.cut.latched.Load() && s.shadowTooSoon(projectID) { + return body, nil // scheduled shadow, but the project's last attempt is inside the minimum interval + } if s.shadowWaiting(projectID) { return body, nil // the last shadow of this project could not run: wait out its backoff, then try again } + s.shadowAttempted(projectID) s.mCutShadowChecks.Inc() var full map[string]any ferr := st.WithBudget(s.shadowBudget(), func(b store.Store) error { diff --git a/server/internal/api/checkpoint_cut_exact_test.go b/server/internal/api/checkpoint_cut_exact_test.go index 0aa25dd6..43949ec5 100644 --- a/server/internal/api/checkpoint_cut_exact_test.go +++ b/server/internal/api/checkpoint_cut_exact_test.go @@ -32,7 +32,7 @@ func bogusBase(project string) func(store.Checkpoint) store.Checkpoint { func TestCheckpointCutShadowIsPerProject(t *testing.T) { st := store.NewMem() spy := newRowSpy(st) - s := api.New(mustCore(t), spy, "k0").WithAuth(auth.NewOpenStore()) + s := api.New(mustCore(t), spy, "k0").WithAuth(auth.NewOpenStore()).WithCheckpointShadowMinInterval(0) ha := newCutHistory(t, st, "A", 1) hb := newCutHistory(t, st, "B", 2) ha.plain() @@ -85,7 +85,7 @@ func TestCheckpointCutShadowIsPerProject(t *testing.T) { func TestCheckpointCutRefusalSurvivesRestart(t *testing.T) { st := store.NewMem() spy := newRowSpy(st) - s := api.New(mustCore(t), spy, "k0").WithAuth(auth.NewOpenStore()) + s := api.New(mustCore(t), spy, "k0").WithAuth(auth.NewOpenStore()).WithCheckpointShadowMinInterval(0) h := newCutHistory(t, st, "A", 5) h.plain() if _, err := cutOnce(t, s, spy, "A"); err != nil { diff --git a/server/internal/api/checkpoint_cut_mininterval_test.go b/server/internal/api/checkpoint_cut_mininterval_test.go new file mode 100644 index 00000000..cdf53a13 --- /dev/null +++ b/server/internal/api/checkpoint_cut_mininterval_test.go @@ -0,0 +1,199 @@ +package api_test + +import ( + "errors" + "testing" + "time" + + "github.com/feirai/averin/server/internal/api" + "github.com/feirai/averin/server/internal/auth" + "github.com/feirai/averin/server/internal/store" +) + +// defIval asks newMinRig to keep the default minimum interval. +const defIval = time.Duration(-1 << 62) + +// minRig is a server whose scheduled shadow is due on every 3rd cut, over a movable clock. minIval == defIval keeps the +// default minimum interval. +type minRig struct { + t *testing.T + st store.Store + spy *rowSpy + s *api.Server + hs map[string]*cutHistory + now time.Time +} + +func newMinRig(t *testing.T, minIval time.Duration, projects ...string) *minRig { + st := store.NewMem() + spy := newRowSpy(st) + r := &minRig{t: t, st: st, spy: spy, hs: map[string]*cutHistory{}, now: time.Date(2026, 10, 19, 0, 0, 0, 0, time.UTC)} + r.s = api.New(mustCore(t), spy, "k0").WithAuth(auth.NewOpenStore()). + WithCheckpointShadowEvery(3).WithCheckpointShadowBackoff(10 * time.Minute). + WithClock(func() time.Time { return r.now }) + if minIval != defIval { + r.s.WithCheckpointShadowMinInterval(minIval) + } + for _, p := range projects { + r.hs[p] = newCutHistory(t, st, p, 3) + r.cut(p) // seq 0: the full computation, no shadow + } + return r +} + +func (r *minRig) cut(p string) (store.Checkpoint, error) { + r.t.Helper() + r.hs[p].plain() + return cutOnce(r.t, r.s, r.spy, p) +} + +func (r *minRig) cuts(p string, n int) { + r.t.Helper() + for i := 0; i < n; i++ { + if _, err := r.cut(p); err != nil { + r.t.Fatal(err) + } + } +} + +func (r *minRig) checks() int64 { _, _, c, _ := r.s.CutStatsForTest(); return c } + +// Seq 3 and 6 are both due within one hour: only the first-cut shadow (seq 1) runs, the due ones are rate-limited. +// After the interval the next due cut (seq 9) shadows. +func TestCheckpointCutShadowMinIntervalLimitsScheduled(t *testing.T) { + r := newMinRig(t, defIval, "p") + r.cuts("p", 1) // seq 1: first incremental cut, always shadowed + if r.checks() != 1 { + t.Fatalf("first incremental cut: checks %d, want 1", r.checks()) + } + r.cuts("p", 5) // seq 2..6: seq 3 and 6 are due but inside the hour + if r.checks() != 1 { + t.Fatalf("due cuts inside the min interval must not shadow: checks %d, want 1", r.checks()) + } + r.now = r.now.Add(api.DefaultCheckpointShadowMinInterval + time.Second) + r.cuts("p", 3) // seq 7..9: seq 9 is due and the interval has passed + if r.checks() != 2 { + t.Fatalf("a due cut after the min interval must shadow: checks %d, want 2", r.checks()) + } +} + +// The first incremental cut of another project shadows even right after a shadow of the first. +func TestCheckpointCutShadowMinIntervalFirstCutIsPerProject(t *testing.T) { + r := newMinRig(t, defIval, "p", "q") + r.cuts("p", 1) + r.cuts("q", 1) + if r.checks() != 2 { + t.Fatalf("each project's first incremental cut shadows: checks %d, want 2", r.checks()) + } +} + +// Once a mismatch has latched, every cut shadows whatever the interval says. +func TestCheckpointCutShadowMinIntervalLatchedIgnoresInterval(t *testing.T) { + r := newMinRig(t, defIval, "p") + r.spy.tamper = bogusBase("p") + if _, err := r.cut("p"); err == nil { + t.Fatal("first incremental cut over a tampered base must refuse") + } + r.spy.tamper = nil + for i := 0; i < 4; i++ { // none of these is a due seq at the same time as the interval being open + b := r.checks() + _, _ = r.cut("p") + if r.checks() != b+1 { + t.Fatalf("latched: every cut must shadow (cut %d)", i) + } + } +} + +// A min interval of 0 restores the old cadence: every due cut shadows. +func TestCheckpointCutShadowMinIntervalZeroDisables(t *testing.T) { + r := newMinRig(t, 0, "p") + r.cuts("p", 6) // seq 1 (first), 3, 6 + if r.checks() != 3 { + t.Fatalf("min interval 0: checks %d, want 3", r.checks()) + } +} + +// A negative value is 0, and a value above the default is clamped to the default. +func TestCheckpointCutShadowMinIntervalClamp(t *testing.T) { + r := newMinRig(t, -time.Minute, "p") + r.cuts("p", 6) + if r.checks() != 3 { + t.Fatalf("negative min interval must behave as 0: checks %d, want 3", r.checks()) + } + r = newMinRig(t, 24*time.Hour, "p") + r.cuts("p", 1) + r.now = r.now.Add(api.DefaultCheckpointShadowMinInterval + time.Second) + r.cuts("p", 2) // seq 3 is due; a 24 h request is clamped to 1 h, so it shadows + if r.checks() != 2 { + t.Fatalf("a 24h request must clamp to the default 1h: checks %d, want 2", r.checks()) + } +} + +// A shadow that fails still sets the backoff, and the failed attempt counts toward the min interval. +func TestCheckpointCutShadowMinIntervalFailedAttemptCounts(t *testing.T) { + r := newMinRig(t, defIval, "p") + r.cuts("p", 1) // seq 1 verified, attempt at t0 + r.now = r.now.Add(api.DefaultCheckpointShadowMinInterval + time.Second) + r.spy.failFull = errors.New("boom") + r.cuts("p", 2) // seq 2 not due; seq 3 due and past the interval: shadow attempted, fails + if r.checks() != 2 || r.s.ShadowFailedForTest() != 1 { + t.Fatalf("checks %d failed %d, want 2 and 1", r.checks(), r.s.ShadowFailedForTest()) + } + r.spy.failFull = nil + r.now = r.now.Add(11 * time.Minute) // past the 10 min backoff, far inside the min interval + r.cuts("p", 3) // seq 6 is due + if r.checks() != 2 { + t.Fatalf("the failed attempt must count toward the min interval: checks %d, want 2", r.checks()) + } + r.now = r.now.Add(api.DefaultCheckpointShadowMinInterval) + r.cuts("p", 3) // seq 9 is due, interval and backoff both passed + if r.checks() != 3 { + t.Fatalf("checks %d, want 3", r.checks()) + } +} + +// The backoff itself still holds when the min interval is off. +func TestCheckpointCutShadowMinIntervalBackoffStillHolds(t *testing.T) { + r := newMinRig(t, 0, "p") + r.spy.failFull = errors.New("boom") + r.cuts("p", 1) // seq 1: unverified, shadow attempted and fails + r.cuts("p", 3) // inside the backoff, including the due seq 3 + if r.checks() != 1 { + t.Fatalf("the backoff must still suppress attempts: checks %d, want 1", r.checks()) + } +} + +// Safety side of the rate limit: under continuous cutting every project still gets a scheduled shadow about once an +// hour. Two verified projects are cut in rotation, one cut per minute each, for 180 minutes. Each project shadows on its +// first cut, then on the first due cut (seq % 3 == 0) at least an hour after its last attempt: seq 63 and seq 123. The +// timer must not be reset by a skipped due cut, and must be kept per project, not for the whole server. +func TestCheckpointCutShadowMinIntervalEachProjectStillShadowsHourly(t *testing.T) { + r := newMinRig(t, defIval, "p", "q") + r.cuts("p", 1) + r.cuts("q", 1) + for i := 0; i < 180; i++ { + r.now = r.now.Add(time.Minute) + r.cuts("p", 1) + r.cuts("q", 1) + } + if got := r.checks(); got != 6 { + t.Fatalf("scheduled shadows under continuous cutting: checks %d, want 6 (2 first cuts + 2 per project hourly)", got) + } +} + +// An unverified project (its first shadow could not run) is NOT rate-limited: after the 10 min backoff the next cut +// retries the shadow, at the default min interval, long before an hour has passed. +func TestCheckpointCutShadowMinIntervalUnverifiedIsExempt(t *testing.T) { + r := newMinRig(t, defIval, "p") + r.spy.failFull = errors.New("boom") + r.cuts("p", 1) // seq 1: the first incremental cut, shadow attempted and fails: still unverified + if r.checks() != 1 || r.s.ShadowFailedForTest() != 1 { + t.Fatalf("checks %d failed %d, want 1 and 1", r.checks(), r.s.ShadowFailedForTest()) + } + r.spy.failFull = nil + r.now = r.now.Add(11 * time.Minute) // past the backoff, far inside the min interval + r.cuts("p", 1) // seq 2: not a due seq, but the project is unverified + if r.checks() != 2 { + t.Fatalf("an unverified project must retry after the backoff, not after the min interval: checks %d, want 2", r.checks()) + } +} diff --git a/server/internal/api/checkpoint_cut_shadow_test.go b/server/internal/api/checkpoint_cut_shadow_test.go index 09d34e27..29532153 100644 --- a/server/internal/api/checkpoint_cut_shadow_test.go +++ b/server/internal/api/checkpoint_cut_shadow_test.go @@ -26,7 +26,7 @@ func newShadowRig(t *testing.T, budget time.Duration) *shadowRig { spy := newRowSpy(st) r := &shadowRig{t: t, st: st, spy: spy, now: time.Date(2026, 10, 19, 0, 0, 0, 0, time.UTC)} r.s = api.New(mustCore(t), spy, "k0").WithAuth(auth.NewOpenStore()). - WithCheckpointShadowEvery(1).WithCheckpointShadowBudget(budget).WithCheckpointShadowBackoff(10 * time.Minute). + WithCheckpointShadowEvery(1).WithCheckpointShadowMinInterval(0).WithCheckpointShadowBudget(budget).WithCheckpointShadowBackoff(10 * time.Minute). WithClock(func() time.Time { return r.now }) r.h = newCutHistory(t, st, "p", 3) r.h.plain() diff --git a/server/internal/api/checkpoint_cut_test.go b/server/internal/api/checkpoint_cut_test.go index 53da54fa..8fcd5d6c 100644 --- a/server/internal/api/checkpoint_cut_test.go +++ b/server/internal/api/checkpoint_cut_test.go @@ -431,7 +431,7 @@ func TestCheckpointCutRefusesAGapInTheNewGrants(t *testing.T) { func TestCheckpointCutShadowRefusesAMismatch(t *testing.T) { st := store.NewMem() spy := newRowSpy(st) - s := api.New(mustCore(t), spy, "k0").WithAuth(auth.NewOpenStore()).WithCheckpointShadowEvery(100) + s := api.New(mustCore(t), spy, "k0").WithAuth(auth.NewOpenStore()).WithCheckpointShadowEvery(100).WithCheckpointShadowMinInterval(0) h := newCutHistory(t, st, "p", 5) for i := 0; i < 5; i++ { h.plain() @@ -474,23 +474,36 @@ func TestCheckpointCutShadowRefusesAMismatch(t *testing.T) { } } -// TestCheckpointCutShadowCadence: with the default period, the first incremental cut after start and every cut whose -// checkpoint seq is a multiple of 100 are also computed in full. +// TestCheckpointCutShadowCadence: the first incremental cut after start is always computed in full. A cut whose +// checkpoint seq is a multiple of 100 is too, but only when the project's last shadow attempt is at least the min +// interval old. With the interval off (0) that is every such cut; with the default (1 h) and 250 cuts inside one +// hour, only the first-cut shadow runs. func TestCheckpointCutShadowCadence(t *testing.T) { - st := store.NewMem() - s := api.New(mustCore(t), st, "k0").WithAuth(auth.NewOpenStore()) - h := newCutHistory(t, st, "p", 9) - h.plain() - if _, err := cutOnce(t, s, st, "p"); err != nil { - t.Fatal(err) - } - for i := 0; i < 250; i++ { - h.plain() - if _, err := cutOnce(t, s, st, "p"); err != nil { - t.Fatal(err) - } - } - if inc, full, checks, mism := s.CutStatsForTest(); inc != 250 || full != 1 || checks != 3 || mism != 0 { - t.Fatalf("incremental %d full %d shadow checks %d mismatches %d; want 250, 1, 3 (the first cut after start, seq 100 and seq 200), 0", inc, full, checks, mism) + for _, tc := range []struct { + name string + ival time.Duration + checks int64 + }{{"interval off", 0, 3}, {"default interval", -1, 1}} { + t.Run(tc.name, func(t *testing.T) { + st := store.NewMem() + s := api.New(mustCore(t), st, "k0").WithAuth(auth.NewOpenStore()) + if tc.ival >= 0 { + s.WithCheckpointShadowMinInterval(tc.ival) + } + h := newCutHistory(t, st, "p", 9) + h.plain() + if _, err := cutOnce(t, s, st, "p"); err != nil { + t.Fatal(err) + } + for i := 0; i < 250; i++ { + h.plain() + if _, err := cutOnce(t, s, st, "p"); err != nil { + t.Fatal(err) + } + } + if inc, full, checks, mism := s.CutStatsForTest(); inc != 250 || full != 1 || checks != tc.checks || mism != 0 { + t.Fatalf("incremental %d full %d shadow checks %d mismatches %d; want 250, 1, %d, 0", inc, full, checks, mism, tc.checks) + } + }) } } diff --git a/server/internal/api/server.go b/server/internal/api/server.go index b088b7dc..76ce12a6 100644 --- a/server/internal/api/server.go +++ b/server/internal/api/server.go @@ -283,7 +283,7 @@ func New(core Sealer, st store.Store, signingKeyID string) *Server { mCheckpointsSealed: reg.Counter("averin_checkpoints_sealed_total", "Total checkpoints successfully sealed."), mCutShadowChecks: reg.Counter("averin_checkpoint_shadow_checks_total", - "Total incremental checkpoint cuts also computed in full and compared (1 in 100 by default)."), + "Total incremental checkpoint cuts also computed in full and compared (the first cut of a project after a start, then at most one per hour per project on every 100th cut, and every cut after a mismatch)."), mCutShadowMismatch: reg.Counter("averin_checkpoint_shadow_mismatch_total", "Total incremental checkpoint cuts that differed from the full computation. Each one REFUSED to sign; alert on any non-zero value."), mCutShadowFailed: reg.Counter("averin_checkpoint_shadow_failed_total", @@ -4032,8 +4032,9 @@ func (s *Server) cutBodyFull(st store.Store, projectID, created string) (map[str // backfillable. A deterministic checkpoint_id keeps the body reproducible for a given seq. // // The body is cut incrementally from the latest checkpoint when it can be (cutBodyIncremental, with the -// argument that it equals the full computation) and by the full computation otherwise. Every -// shadowEvery-th incremental cut ALSO computes the full body and refuses to sign when the two differ. +// argument that it equals the full computation) and by the full computation otherwise. Some incremental cuts +// ALSO compute the full body and refuse to sign when the two differ: which ones (sampled, per project, at most +// one scheduled shadow per hour) is defined in checkpointBodyChecked (checkpoint_cut.go). func (s *Server) createCheckpointTx(st store.Store, projectID string) (store.Checkpoint, error) { body, err := s.checkpointBodyChecked(st, projectID) if err != nil {