From 62298c72b8ce2e3acd182f5c953c716e1d112be9 Mon Sep 17 00:00:00 2001 From: zachyking Date: Tue, 27 Oct 2026 13:25:37 +0000 Subject: [PATCH] Lower the checkpoint shadow budget default from 5 s to 1 s Evidence (release-1 soak, 0.5 calls/s, fresh history): the scheduled shadow check recomputes the full checkpoint body under the project write lock inside the budget. From about 5 h of history it stopped fitting 5 s reliably. Near that boundary a success (which resets the backoff) alternates with failures, so attempts stay about hourly and EACH is a 3.5 to 5 s write stall (metered calls of 3.3 to 5.1 s at six consecutive attempts). At lighter load this zone lasts days. With a 1 s default one shadow attempt holds the write lock for about 1 s. The trade: the cross-check covers less history. Estimated (scaled from the measurement, about 5 s at about 5 h on the soak host) it stops fitting after roughly an hour of history at 0.5 calls/s, later at lighter load. It was already ineffective beyond a few hours. The differential tests remain the primary assurance. Backoff, min interval and refusal semantics are unchanged: a mismatch still refuses. Adds a test pinning the default at 1 s, updates LIMITATIONS, CONFIGURATION, the claims text and the rendered FORMAL.md. Co-Authored-By: Claude Opus 5.5 --- docs/dev/CONFIGURATION.md | 6 ++++-- docs/dev/FORMAL.md | 2 +- docs/dev/LIMITATIONS.md | 10 +++++++++- formal/claims.json | 2 +- formal/kit-claims.json | 2 +- server/internal/api/checkpoint_cut.go | 11 +++++++++-- server/internal/api/checkpoint_cut_shadow_test.go | 3 +++ 7 files changed, 28 insertions(+), 8 deletions(-) diff --git a/docs/dev/CONFIGURATION.md b/docs/dev/CONFIGURATION.md index 8979b7be..2cf65d06 100644 --- a/docs/dev/CONFIGURATION.md +++ b/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. diff --git a/docs/dev/FORMAL.md b/docs/dev/FORMAL.md index 6ca8efca..8a7fe581 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 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 | +| `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 (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. | `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 26ec4a17..6fe0b85e 100644 --- a/docs/dev/LIMITATIONS.md +++ b/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 diff --git a/formal/claims.json b/formal/claims.json index 842af009..97cbf973 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) 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" diff --git a/formal/kit-claims.json b/formal/kit-claims.json index a4ca852b..1344079b 100644 --- a/formal/kit-claims.json +++ b/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", diff --git a/server/internal/api/checkpoint_cut.go b/server/internal/api/checkpoint_cut.go index 689be4d2..48e90058 100644 --- a/server/internal/api/checkpoint_cut.go +++ b/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 { diff --git a/server/internal/api/checkpoint_cut_shadow_test.go b/server/internal/api/checkpoint_cut_shadow_test.go index 29532153..09755678 100644 --- a/server/internal/api/checkpoint_cut_shadow_test.go +++ b/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) }