-
Notifications
You must be signed in to change notification settings - Fork 173
Clarify checker store invariant #1581
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from 10 commits
d2b2d2f
f96ed6f
bf22581
f6aeeb4
4369155
df4950b
82bcb99
a3285eb
d6cdb0e
965ed88
1725345
36675d4
c12ad41
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -16,7 +16,7 @@ This document contains rules and conventions for AI agents working on this codeb | |
| 6. **Every FSM `Registry.X.Get(...)` must have a matching preload, declared by the component that proposes the command** — The FSM apply path reads from the in-memory cache; a cache miss turns the read into a silent no-op. Each component that emits a proposal (the metadata converter, the index builder, the cluster-config reconciler, the idempotency-eviction scheduler, the mirror worker, admission) is responsible for declaring its own `preload.Needs` covering every key its apply path will read. There is NO central proposal→needs registry — coupling the preload package to every proposal type creates a single point that easily falls behind. The component knows what it reads; the component declares it. The shared `proposeTechnical` helper takes a `*preload.Needs` parameter the caller fills in (pass nil or an empty `Needs` when the apply path has no cache-keyed reads, e.g. cluster config / idempotency eviction). The preload populates the cache via `MirrorPreload` with a fresh value read at propose time (Pebble fallback on cache miss), and `PredictedIndex` catches mutations between propose and apply. | ||
| 7. **Never silently skip a "should not happen" branch** — A branch that is reachable only if an invariant is violated (nil where the contract says non-nil, a state we believe unreachable, a cache miss after a guaranteed preload, etc.) MUST surface a loud signal: `return fmt.Errorf("invariant: ...")` so it bubbles up, or `assert.Unreachable(...)` for SUT-level invariants exercised under antithesis. A silent `return nil` / `continue` on these branches hides real bugs — particularly catastrophic in the FSM apply path, where a no-op desyncs nodes from each other. Branches that represent genuine runtime conditions (cache miss as an expected outcome, stale proposal, deleted entity) keep their soft `return nil`. The distinction is whether the case is *expected* (soft skip OK) or *impossible by design* (must fail loudly). The comment must say *why* the case is impossible so a reader can decide whether to add a hard fail or relax the rule. | ||
|
|
||
| 8. **The audit log is the only source of truth — every other persisted dataset is a projection and must be verified by the checker** — Only `AuditEntry` (zone `Cold`, sub `Audit`) is cryptographically bound, via the hash chain that `state.BuildHashedHeaderPayload` + `processing.HashGenerator` produce and `checker.verifyAuditHashChain` verifies on every Check() run. Everything else stored in Pebble — `Log`, `AuditItem`, `AppliedProposal`, `LedgerLog.PurgedVolumes`, attribute caches (`Volume`, `Metadata`, `Transaction`, `Reference`, `Boundary`, etc.), reversion bitsets, idempotency keys, mirror cursors, chapters, bloom filters, signing keys, the read-side index — is a *projection* of orders that already live in the audit chain. Projections are rebuildable from the audit on demand, so we deliberately do NOT extend the hash chain to cover them (refactor over hash binding — see `feedback_audit_is_source_of_truth`). In exchange, **`internal/application/check/checker.go` MUST verify every projection it persists**: re-derive the value the projection should hold by replaying the audit (`ReplayLedgerLog`, `SimulateEphemeralPurge`, `partitionVolumes`, etc.) and compare to what is stored, emitting the matching `CHECK_STORE_ERROR_TYPE_*` event on divergence. A projection that the checker does not verify is a tampering vector — adding a new persisted projection without a matching compare* / collect* pass in the checker is the violation. The current passes are `compareVolumes`, `compareMetadata`, `compareTransactions`, `compareExclusionProjections` (AppliedProposal.TransientVolumes + LedgerLog.PurgedVolumes), `checkReversionInvariants`, `verifySealingHash`, `compareIdempotencyOutcomes` (frozen idempotency outcomes in SubIdempKeys vs the hash-chained AuditFailure/AuditSuccess that wrote them — the failure kind is re-derived from the chain-bound reason via `domain.KindForReason`, never stored), and `compareIndexes` (SubAttrIndex registry vs CreateIndex/DropIndex/RemovedMetadataFieldType/DeleteLedger logs — covers presence + identity; BuildStatus is intentionally excluded because it is purely informational on the cluster-wide registry entry — queries gate on the per-replica `IndexVersionState.CurrentVersion`, not on BuildStatus), and `compareMirrorV2LogID` (stored `LedgerBoundaries.last_mirror_v2_log_id` **==** `max(audited MirrorIngest.v2_log_id)` per ledger — a full equality check, `CHECK_STORE_ERROR_TYPE_MIRROR_V2LOGID_MISMATCH` on ANY divergence; the FSM enforces a contiguous applied prefix so at rest the two must be exactly equal, and the baseline floor is seeded from archived `Boundary` rows now included in the compact baseline snapshot; pre-field clusters are unsupported, no backfill leniency), and `compareSchema` (per-ledger `LedgerInfo.MetadataSchema` vs the replayed CreateLedger.initial_schema + SetMetadataFieldType/RemovedMetadataFieldType logs; under archived chapters the boundary schema is seeded from the baseline checkpoint, which carries LedgerInfo for this purpose), and `compareAccountTypes` (per-ledger `LedgerInfo.AccountTypes` vs the replayed AddAccountType/RemoveAccountType logs, baseline-seeded under archiving like the schema), and `compareLedgerPresence` (the live ledger set in the store must match the audit-derived set both ways: every audit-live ledger — CreateLedger with no later DeleteLedger, or a non-deleted baseline ledger under archiving — must have a *live* stored `LedgerInfo` else `MISSING_LEDGER` (covers an entry deleted outright OR tampered to a soft-deleted tombstone, which the compareSchema/compareAccountTypes loops skip), and every live stored `LedgerInfo` must be audit-backed else `UNAUDITED_LEDGER` (an injected empty ledger row carries no schema/types for the projection passes to flag). The audit-derived set is NEVER seeded from the live store — under archiving it comes from the baseline checkpoint, keeping the check independent of the data it verifies), and `compareReferences` (the SubAttrReference reference→txID uniqueness index vs the references replayed from CreatedTransaction/RevertedTransaction logs, baseline-seeded under archiving; verified both ways — missing, unaudited, and retargeted rows are all flagged; rows for deleted or cleanup-pending ledgers are skipped since they legitimately linger until a covering purge runs deleteLedgerData), and `compareBoundaries` (per-ledger `LedgerBoundaries` vs the checker’s re-derivation: NextTransactionId/NextLogId/PostingCount/RevertCount from the replayed logs plus the chain-bound AuditItem order effects — mirror fill-gap advances and NumscriptExecutionCount live on the orders, not the ledger-log stream — baseline-seeded under archiving; VolumeCount/MetadataCount/ReferenceCount are compared against a recount of the stored attribute rows they summarize, which their own passes verify entry-by-entry, so the chain is rows↔audit, counter↔rows; EphemeralEvictedCount/TransientUsedCount are intentionally excluded — informational, carried across restore, cf. BuildStatus); extend the list as new persisted projections land. **Known projection gaps**: `LedgerBoundaries.EphemeralEvictedCount` / `TransientUsedCount` are excluded from `compareBoundaries` and carried across restore rather than re-derived — informational counters (cf. BuildStatus); `LedgerInfo.DefaultEnforcementMode` and the ledger-metadata attribute (`SubAttrLedgerMetadata`) have no compare pass yet (both are rebuilt on restore by RebuildDelta). | ||
| 8. **The audit log is the only source of truth — every other persisted dataset is a projection and must be verified by the checker** — Only `AuditEntry` (zone `Cold`, sub `Audit`) is cryptographically bound, via the hash chain that `state.BuildHashedHeaderPayload` + `processing.HashGenerator` produce and `checker.verifyAuditHashChain` verifies on every Check() run. Everything else stored in Pebble — `Log`, `AuditItem`, `AppliedProposal`, `LedgerLog.PurgedVolumes`, attribute caches (`Volume`, `Metadata`, `Transaction`, `Reference`, `Boundary`, etc.), reversion bitsets, idempotency keys, mirror cursors, chapters, bloom filters, signing keys, the read-side index — is a *projection* of orders that already live in the audit chain. Projections are rebuildable from the audit on demand, so we deliberately do NOT extend the hash chain to cover them (refactor over hash binding — see `feedback_audit_is_source_of_truth`). In exchange, **`internal/application/check/checker.go` MUST verify every projection it persists**: re-derive the value the projection should hold by replaying the audit (`ReplayLedgerLog`, `SimulateEphemeralPurge`, `partitionVolumes`, etc.) and compare to what is stored, emitting the matching `CHECK_STORE_ERROR_TYPE_*` event on divergence. A projection that the checker does not verify is a tampering vector — adding a new persisted projection without a matching compare* / collect* pass in the checker is the violation. Two scope refinements: (a) this applies to the **primary FSM store** — the single store `Check()` opens and walks; **peer secondary stores** (`usagestore` counters, `readstore` index) are out of scope *by construction* since `Check()` never opens them and they are pure rebuildable caches whose corruption is a *rebuild* event, not an undetected integrity violation (serving a value through an API does not make it authoritative). (b) A primary-store projection may be exempted from a dedicated pass only when it is either (i) deterministically rebuildable from still-retained verified state through a real, *wired* rebuild path — not rebuildable merely in principle — or (ii) purely informational and intentionally carried across restore (cf. `BuildStatus`). These are distinct bases: of the *Known projection gaps* below, `DefaultEnforcementMode` and `SubAttrLedgerMetadata` qualify under (i) via `RebuildDelta`, while `EphemeralEvictedCount` / `TransientUsedCount` qualify under (ii) — they are NOT rebuilt by `RebuildDelta`, so the wired-rebuild basis must not be claimed for them. The current passes are `compareVolumes`, `compareMetadata`, `compareTransactions`, `compareExclusionProjections` (AppliedProposal.TransientVolumes + LedgerLog.PurgedVolumes), `checkReversionInvariants`, `verifySealingHash`, `compareIdempotencyOutcomes` (frozen idempotency outcomes in SubIdempKeys vs the hash-chained AuditFailure/AuditSuccess that wrote them — the failure kind is re-derived from the chain-bound reason via `domain.KindForReason`, never stored), and `compareIndexes` (SubAttrIndex registry vs CreateIndex/DropIndex/RemovedMetadataFieldType/DeleteLedger logs — covers presence + identity; BuildStatus is intentionally excluded because it is purely informational on the cluster-wide registry entry — queries gate on the per-replica `IndexVersionState.CurrentVersion`, not on BuildStatus), and `compareMirrorV2LogID` (stored `LedgerBoundaries.last_mirror_v2_log_id` **==** `max(audited MirrorIngest.v2_log_id)` per ledger — a full equality check, `CHECK_STORE_ERROR_TYPE_MIRROR_V2LOGID_MISMATCH` on ANY divergence; the FSM enforces a contiguous applied prefix so at rest the two must be exactly equal, and the baseline floor is seeded from archived `Boundary` rows now included in the compact baseline snapshot; pre-field clusters are unsupported, no backfill leniency), and `compareSchema` (per-ledger `LedgerInfo.MetadataSchema` vs the replayed CreateLedger.initial_schema + SetMetadataFieldType/RemovedMetadataFieldType logs; under archived chapters the boundary schema is seeded from the baseline checkpoint, which carries LedgerInfo for this purpose), and `compareAccountTypes` (per-ledger `LedgerInfo.AccountTypes` vs the replayed AddAccountType/RemoveAccountType logs, baseline-seeded under archiving like the schema), and `compareLedgerPresence` (the live ledger set in the store must match the audit-derived set both ways: every audit-live ledger — CreateLedger with no later DeleteLedger, or a non-deleted baseline ledger under archiving — must have a *live* stored `LedgerInfo` else `MISSING_LEDGER` (covers an entry deleted outright OR tampered to a soft-deleted tombstone, which the compareSchema/compareAccountTypes loops skip), and every live stored `LedgerInfo` must be audit-backed else `UNAUDITED_LEDGER` (an injected empty ledger row carries no schema/types for the projection passes to flag). The audit-derived set is NEVER seeded from the live store — under archiving it comes from the baseline checkpoint, keeping the check independent of the data it verifies), and `compareReferences` (the SubAttrReference reference→txID uniqueness index vs the references replayed from CreatedTransaction/RevertedTransaction logs, baseline-seeded under archiving; verified both ways — missing, unaudited, and retargeted rows are all flagged; rows for deleted or cleanup-pending ledgers are skipped since they legitimately linger until a covering purge runs deleteLedgerData), and `compareBoundaries` (per-ledger `LedgerBoundaries` vs the checker’s re-derivation: NextTransactionId/NextLogId/PostingCount/RevertCount from the replayed logs plus the chain-bound AuditItem order effects — mirror fill-gap advances and NumscriptExecutionCount live on the orders, not the ledger-log stream — baseline-seeded under archiving; VolumeCount/MetadataCount/ReferenceCount are compared against a recount of the stored attribute rows they summarize, which their own passes verify entry-by-entry, so the chain is rows↔audit, counter↔rows; EphemeralEvictedCount/TransientUsedCount are intentionally excluded — informational, carried across restore, cf. BuildStatus); extend the list as new persisted projections land. **Known projection gaps**: `LedgerBoundaries.EphemeralEvictedCount` / `TransientUsedCount` are excluded from `compareBoundaries` and carried across restore rather than re-derived — informational counters (cf. BuildStatus); `LedgerInfo.DefaultEnforcementMode` and the ledger-metadata attribute (`SubAttrLedgerMetadata`) have no compare pass yet (both are rebuilt on restore by RebuildDelta). | ||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. [Medium] Scope refinement (a) lists But Fix: drop the
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Fixed. Reworded to cite the |
||
|
|
||
| 9. **Never bypass the FSM coverage gate** — Every cache-attribute read on the FSM hot path MUST go through `Scope.GetX(...)` so the per-order `coverage_bits` admit it. Reading the underlying `Registry.X.KeyStore().M` (or any other parent-cache iterator) directly skips the gate and produces non-deterministic FSM behavior: the gate is what binds the order to the admission-declared preload set, and a direct read silently sees keys the proposer never declared. There is NO documented exception — paths that need to iterate (e.g. cascade-on-delete) MUST either declare the relevant `preload.Needs` upfront, defer the work to a lifecycle path (`batch.deleteLedgerData` + `MarkLedgerForCleanup`), or be rejected at design review. New helpers that scan the parent KeyStore from inside an order/TU handler are the violation, even when wrapped in a method on `WriteSet`. The coverage gate exists precisely so admission's declared key set is the FSM's only legitimate read horizon — under no circumstances should the apply path widen it on the fly. | ||
|
|
||
|
|
||
Uh oh!
There was an error while loading. Please reload this page.