Sync Formal Modeling - P & Occult - #1115
Conversation
Wire the end-to-end source-cache replay contract frozen in docs/verification/sync-replay-6b/plan.md: SourceCacheCapability parsing and gating, lookup install/teardown with a transport deliverability probe (CO-6b-001: no production transport delivers this phase; such syncs run cold and never log warm), compat-record lifecycle with byte-match consume gating, fresh-page recording with scope stamping, replay handling with provenance enforcement — the sourceCacheWarm gate, hit-validator binding to the replay base, and a per-scope page lock covering replay copies AND record-page application — the warm/cold ErrReplayIntegrity verdict taxonomy, the CO-017 cross-version fold fence, produce-side guards blocking unreplayable shapes (child resource types, InsertResourceGrants) from seeding warm generations, and a sync token schema fence (reshaped fields take new keys; versioned tokens that fail to parse error loudly instead of downgrading to v0). Verified by the chaos-connector suites (gate matrix, collection semantics, ordering/pagination, interruption/resume, generational steady state), a bounded verdict-taxonomy enumeration, engine-seam sentinel-identity tests, benchmarks pinning the disabled-path and checkpoint-marshal costs, and mutation-verified instruments for every load-bearing guard. Three independent review rounds drove the hardening recorded as change orders CO-6b-003 through CO-6b-006; docs/verification/sync-replay-6b/evidence.md carries the full closure record, registered exclusions, and explicit limitations. Co-authored-by: Cursor <cursoragent@cursor.com>
…e triage, witness pin Closes both round-4 MAJORs: the chaos fixture now asserts no source-cache scope lock is held at sync end (with per-handler loud-failure cells, each defer site mutation-verified), and evidence.md gains the structural- coverage triage ledger with six new instruments for the branches it judged worth real tests. Minors: MaterializationWitnessReader promoted to a pinned named interface, the syncer asserts the exported deliverability probe, the shrunk-type-list permutation is a registered exclusion, and the token-fence/lock-hold/lock-cardinality wording is corrected. Co-authored-by: Cursor <cursoragent@cursor.com>
P track: MODEL_SPEC (walker+6b, frozen v6) with 47-cell calibrated sweep reproducing calibration cases 1-4; GRAPH_MODEL_SPEC (demand-graph runtime, frozen v4 + GS-CO-001..005) with 66-cell calibrated sweep over both lineage variants; curated counterexample traces. Occult track: equational laws (LAWS.md, 15 proved + 5 refused controls), trace-policy oracle set, MPST protocol projections, phantom-union derivation, and an executable demand-graph reference implementation checked by the same oracles. Bake-off protocol registered (GS-CO-005); verdict document to follow. Co-authored-by: Cursor <cursoragent@cursor.com>
….md) Runs the GS-CO-005 declared cells (12/12 on declared verdicts: G6 v1 zero-crash controls, G6b bound-1 probes, G5d seal-world probes via the new GSEALWORLD monitor) and assembles deliverable 4's written recommendation under the registered decision rule: tie on property satisfaction, S wins on the frozen mechanism tally (no new durable state class; session primitives demote to optimization), redo work symmetric, seal-world sets identical across variants. Co-authored-by: Cursor <cursoragent@cursor.com>
Deliverable 6/7's last leg: real pkg/sync executions now feed the trace-policy oracle. A test-only commit-order recorder (sync_trace_audit.go, the testQueueAudit pattern — nil in production, one pointer check per event) fires at the orchestration seams: consult (lookup resolution), the replay unit's clear+copy legs, scoped page-row commits, manifest publishes, durable checkpoints, and EndSync. The chaos harness records the reference source-cache scenario cold and warm, exports JSONL fixtures, and the Occult host renders them onto the canonical vocabulary and checks all five policies: 10/10 cells green, with planted-violation tests validating the bridge itself (dropped consult reds policy 1; un-regrounded resume reds policy 2). Rendering conventions (s1/s2 scope mapping, structural clear for non-resumed attempts) live in the renderer; the recorder stays purely observational. Co-authored-by: Cursor <cursoragent@cursor.com>
…path finding The trace-policy vocabulary gains ev_resume attempt boundaries: durable facts persist across the marker (checkpoint-durable hit-set, committed-row grounding, sync-scoped seal obligations) and only once-per-scope resets — the across-attempt replay re-copy is B5-legal at-least-once idempotence, the within-attempt duplicate stays the bug. Matrix grows to 40 cells (green_resume + red_ops_resume). The chaos harness exports a real crash/resume fixture (EffectCrash after the replay unit committed, resumed to seal by a new syncer); the oracle is 15/15 green, and TestRealTraceBridgeResumeMarkerLoadBearing proves the marker is load-bearing (stripping it reds once-per-scope). Finding: for a mid-chain cut the resume RE-RUNS the replay copy regardless of checkpoint cadence — checkpoints commit at batch boundaries and a page chain runs inside one batch, so a cut chain's MarkSourceCacheReplayed never reaches a checkpoint. The resume suite's comments claimed the restored replayed-set skips the copy; the trace recorder is the first instrument able to distinguish skip from idempotent re-copy and falsified that mechanism (convergence was always right, via B5 idempotence; the replayed-set's real skip role is within-attempt). Comments corrected, behavior pinned. Renderer note: consecutive checkpoints coalesce (verdict-preserving) because engine ground-evaluation cost roughly doubles per list element — recorded as an engine ask. Co-authored-by: Cursor <cursoragent@cursor.com>
The delta protocol's deletion entries (DeletedIds/DeletedPrincipalIds in the connector response — applied synchronously as row deletes, nothing durably stored) join the trace vocabulary as ev_delete, a WRITE with upsert's obligations: grounding (clear-before-write), quiescent-checkpoint dirtying, and seal-activity marking. - policies: ev_delete clauses across all five policies; four new fixtures (green delete + three reds) take the matrix to 60 cells - recorder: syncTraceDelete fires per committed store delete call in afterUpserts (canonical and principal-scoped legs) - exporter: tombstone delta chaos scenario with a content oracle (tombstoned row absent from the sealed artifact); fixture warm_replay_sync_tombstone.jsonl shows B3's within-page order (rows, tombstones, validator) directly in a real trace - renderer: structural clear now grants to the scope's first write of either kind; planted ungrounded-delete validation reds clear-before-upsert Real-trace oracle: 20/20 policy cells green across four fixtures. Co-authored-by: Cursor <cursoragent@cursor.com>
Executive wrap-up of the verification effort: the three-track verdict (calibration reds, bake-off verdict S, witnessed-conformant real traces), the findings register (design bugs fixed in spec, the resume-mechanism falsification, tooling asks), and the explicit guarantee/non-guarantee boundary (witnessed vs calibrated vs asserted linkage). README points at it as the entry document. Co-authored-by: Cursor <cursoragent@cursor.com>
Design-doc kickoff implementing the bake-off verdict: the frozen mechanism inventory, proposed model-to-Go referents (node = scoped action, output key = (rowKind, scopeKey) partition), the sibling-runtime-behind-a-capability strategy with a dual-run conformance gate, the verification plan keeping the trace oracle load-bearing, and the open questions that gate phase 1. Co-authored-by: Cursor <cursoragent@cursor.com>
The 25 trace.json replay files were ~183k lines — 90% of the branch diff. The committed evidence is now the human-readable counterexample.txt per red cell plus the sweep summaries; replays regenerate via each cell's `p check` line (reds reproduce at the find rates the run log states). gitignore pins the convention. Co-authored-by: Cursor <cursoragent@cursor.com>
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
| if o.s.state.SourceCacheReplayed(o.rowKind, o.scopeKey) { | ||
| // Duplicate page / lost-response retry: the copy already ran this | ||
| // sync. Replay is replacement, so re-running it would also wipe | ||
| // overlay rows upserted since. Skip the copy; apply the page's | ||
| // upserts/tombstones normally. | ||
| l.Debug("source-cache replay already completed for scope this sync; skipping copy", | ||
| zap.String("row_kind", string(o.rowKind)), | ||
| zap.String("scope_key", o.scopeKey), | ||
| ) | ||
| } else { | ||
| if o.s.previousSyncReader == nil { | ||
| return newReplayIntegrityError(ReplayVerdictCold, o.rowKind, o.scopeKey, | ||
| fmt.Errorf("no previous sync artifact available to replay from")) | ||
| } | ||
| // Bind the hit to the CURRENT replay base. The eligibility gates | ||
| // cannot distinguish two artifacts from the same connector and | ||
| // config (identical compat keys), so a previous artifact swapped | ||
| // between attempts — service-mode spare replaced by a | ||
| // rollback/restore — passes every gate while its rows for this | ||
| // scope may predate the state the connector actually revalidated. | ||
| // The recorded validator is the one the connector's verdict was | ||
| // computed against; the base we copy from must still publish | ||
| // exactly it. Mismatch, absence, and read failure are all cold: | ||
| // the copy's provenance cannot be established. | ||
| reader, ok := o.s.previousSyncReader.(sourceCacheEntryReader) | ||
| if !ok { | ||
| return newReplayIntegrityError(ReplayVerdictCold, o.rowKind, o.scopeKey, | ||
| fmt.Errorf("previous sync artifact exposes no source-cache surface to verify the replay base against the recorded hit")) | ||
| } | ||
| baseEntry, found, err := reader.LookupSourceCacheEntry(ctx, o.rowKind, o.scopeKey) | ||
| if err != nil { | ||
| return newReplayIntegrityError(ReplayVerdictCold, o.rowKind, o.scopeKey, | ||
| fmt.Errorf("reading the replay base's manifest entry to verify the recorded hit: %w", err)) | ||
| } | ||
| if !found { | ||
| return newReplayIntegrityError(ReplayVerdictCold, o.rowKind, o.scopeKey, | ||
| fmt.Errorf("replay base has no manifest entry for this scope: the recorded hit came from a different artifact")) | ||
| } | ||
| if baseEntry.CacheValidator != hitValidator { | ||
| return newReplayIntegrityError(ReplayVerdictCold, o.rowKind, o.scopeKey, | ||
| fmt.Errorf("replay base's validator does not match the one this sync's lookup returned: the previous artifact changed between attempts")) | ||
| } | ||
| res, err := o.s.sourceCacheStore.ReplaySourceCache(ctx, o.s.previousSyncReader, o.rowKind, o.scopeKey) | ||
| if err != nil { | ||
| return newReplayIntegrityError(replayCopyVerdict(err), o.rowKind, o.scopeKey, | ||
| fmt.Errorf("replay copy: %w", err)) | ||
| } | ||
| // Trace-audit the unit's legs in the store's contractual | ||
| // clear-then-copy order (TRACE_BRIDGE.md unit expansion). | ||
| o.s.testSyncTraceAudit.record(syncTraceClear, string(o.rowKind), o.scopeKey) | ||
| o.s.testSyncTraceAudit.record(syncTraceReplay, string(o.rowKind), o.scopeKey) | ||
| if res.NeedsExpansion && !o.s.dontExpandGrants { | ||
| o.s.state.SetNeedsExpansion() | ||
| } | ||
| o.s.state.MarkSourceCacheReplayed(o.rowKind, o.scopeKey) | ||
| l.Debug("source-cache replay copied previous sync's scope rows", | ||
| zap.String("row_kind", string(o.rowKind)), | ||
| zap.String("scope_key", o.scopeKey), | ||
| zap.Int64("rows", res.Rows), | ||
| ) | ||
| } |
There was a problem hiding this comment.
🟡 Suggestion: the once-per-scope guard is SourceCacheReplayed, but nothing rejects a SourceCacheReplay for a scope that already had SourceCacheRecord rows applied earlier in this sync. ReplaySourceCache is a replacement copy (clear destination scope, then copy the base), so a record→replay page order for one scope silently discards the fresh rows and then afterUpserts publishes a validator over the result — silent, durable, and it seeds the next warm sync. The scope lock added for N1 gives mutual exclusion but not ordering, and with EnqueuePageTokens sibling cursors the arrival order for one scope isn't the connector's to guarantee. Consider tracking "rows recorded for this scope this sync" in state and failing cold here, the same way the no-hit and validator-mismatch gates do, rather than resting on plan B5's "cross-page ordering follows page arrival order exactly".
| if o.pageRows > 0 { | ||
| // The page's row puts committed between beforeUpserts and here. | ||
| o.s.testSyncTraceAudit.record(syncTraceUpsert, string(o.rowKind), o.scopeKey) | ||
| } |
There was a problem hiding this comment.
🟡 Suggestion: o.pageRows is len(resp.GetList()) — the pre-filter count — but syncResources only calls putConnectorResources when bulkPutResoruces is non-empty, and filterConnectorData drops rows that fail validateConnectorResource. A resources page whose rows are all dropped therefore emits an upsert event with no committed write, which contradicts sync_trace_audit.go's stated contract ("every event corresponds to a store operation that actually committed"). Since the Occult trace oracle is the model-to-implementation bridge this PR rests on, a fabricated event weakens the evidence rather than production behavior. Consider recording from the actual write site (or from the post-filter row count) instead.
General PR Review: Sync Formal Modeling - P & OccultBlocking Issues: 0 | Suggestions: 1 | Threads Resolved: 0 Review SummaryScanned the full PR diff (155 files, ~31k additions) for security and correctness: the Risk triage (repo criteria §Risk Triage). Silence: YES — a wrong replay produces well-formed rows, not a crash. Durability: YES — c1z contents, checkpoint tokens, and the new manifest field outlive the process. Uncontrolled dimensions: YES — crash/checkpoint timing, worker schedule, and cross-SDK-version reads. Consumer distance: future SDK versions and the platform. Verdict: HIGH, remediation rung 3 (re-sync the fleet). The PR ships the instruments that class demands — differential cold-truth oracles, a Security IssuesNone found. Correctness IssuesNone found. Suggestions
Prompt for AI agents |
…d grounding)
The walker model's scenario-1 red was live in the shipped syncer: a warm
round cut after its replay copy committed but before its validator
published, upstream moving between attempts, and the resume's consult
missing meant the connector's fresh record round composed with the
crashed attempt's copied debris and sealed the union under the fresh
validator — which the next sync validates clean and replays forward.
Fix: a record round is a replacement listing, so before its first write
to a scope this attempt, a partition holding rows no completed round
published is cleared. New store surface ClearSourceCacheScope (the
replay clear leg standalone), groundRecordScope under the scope lock,
attempt-local grounded set so replay/record pages of one round never
re-ground over each other; published entries are untouched, preserving
multi-action accumulation.
Witnessed and pinned by TestChaosSourceCacheRecordFlipOverReplayDebris
(content oracle + the grounding clear visible in attempt 2's trace);
fixtured as warm_replay_sync_record_flip.jsonl, and record rounds now
emit a real ev_clear ("replacement rounds clear first", previously
structural, now witnessed). Oracle 25/25 green; full sync/dotc1z suites
and lint clean.
Co-authored-by: Cursor <cursoragent@cursor.com>
| func (o *sourceCachePageOps) groundRecordScope(ctx context.Context) error { | ||
| key := sourceCacheScopeKey(o.rowKind, o.scopeKey) | ||
| if _, done := o.s.sourceCacheScopeGrounded.Load(key); done { | ||
| return nil | ||
| } | ||
| _, published, err := o.s.sourceCacheStore.LookupSourceCacheEntry(ctx, o.rowKind, o.scopeKey) | ||
| if err != nil { | ||
| return newReplayIntegrityError(ReplayVerdictWarm, o.rowKind, o.scopeKey, | ||
| fmt.Errorf("record grounding: reading this sync's manifest entry: %w", err)) | ||
| } | ||
| if !published { | ||
| deleted, err := o.s.sourceCacheStore.ClearSourceCacheScope(ctx, o.rowKind, o.scopeKey) | ||
| if err != nil { | ||
| return newReplayIntegrityError(ReplayVerdictWarm, o.rowKind, o.scopeKey, | ||
| fmt.Errorf("record grounding: clearing un-attributed rows: %w", err)) | ||
| } |
There was a problem hiding this comment.
🟠 Bug: grounding assumes a resume always re-lists the scope from its root, but not every resume does. The crash path does restart from root (no checkpoint commits mid-chain), which is what the new witness test exercises — but the stop paths do checkpoint mid-batch: handleOperationError calls Checkpoint(ctx, true) after syncParallel returns (parallel_syncer.go:469, and checkpointOnStop at :487), and state.Marshal preserves PageToken for every op except SyncGrantExpansionOp. So a run-duration expiry (or external cancel) part-way through a paginated record round persists a mid-chain token, and already-finished sibling cursors from EnqueuePageTokens are gone from the action map entirely.
On that resume, the scope has no manifest entry yet (PutSourceCacheEntry only runs on the page that carries the validator), so groundRecordScope clears the whole partition — deleting rows attempt 1 durably committed for pages the resumed listing will never re-request. The round then publishes its validator over the truncated set, and the next sync's consult validates it clean and replays it forward: exactly the non-self-healing laundering this fix targets, with missing grants instead of phantom ones. This is silent + durable, and it now also applies to plain cold syncs of any MODE_READ_WRITE connector that paginates a scope.
Grounding needs to be conditioned on the round actually starting from the scope's root — e.g. blank the source-cache-scoped actions' page tokens at marshal time the way the expansion token is blanked, or carry a durable per-scope "grounded this sync" marker instead of the volatile attempt-local set.
| func (e *Engine) ClearSourceCacheScope(ctx context.Context, rowKind string, scopeKey string) (int64, error) { | ||
| var recordType byte | ||
| var prefix []byte |
There was a problem hiding this comment.
🟡 Suggestion: ClearSourceCacheScope now runs once per scope per attempt on the default record path, including every cold sync, and each call takes withWrite (serializing against all other writers), builds a NewIter over the scope prefix and allocates a NewRecordBatch even when the partition is born empty. BenchmarkSourceCachePageOps still documents that "no store I/O happens until beforeUpserts/afterUpserts, whose costs are engine-level and benchmarked in pkg/dotc1z/engine/pebble" — but there is no benchmark for this method, only BenchmarkSourceCacheReplay*. Per the repo's cost-contract rule, a new per-scope store operation on the hot path wants a stated cost-curve delta in scope count and a benchmark pinning the empty-partition case.
| clearScopeErr error | ||
| } | ||
|
|
||
| func (f *fakeSourceCacheStore) ClearSourceCacheScope(context.Context, sourcecache.RowKind, string) (int64, error) { | ||
| return 0, f.clearScopeErr | ||
| } |
There was a problem hiding this comment.
🟡 Suggestion: clearScopeErr is declared and read by the stub but never set by any test, so both groundRecordScope error paths (manifest-lookup failure and clear failure, each producing a ReplayVerdictWarm replay-integrity error) are unexercised, as is the "already grounded → skip" branch. Engine.ClearSourceCacheScope likewise has no direct unit test — the only coverage is the end-to-end chaos witness. A couple of table cases here would pin the verdict classification cheaply.
… (CO-6b-009) Connector session-store writes are durable in the artifact but commit outside the checkpoint mechanism, so a resumed attempt inherited the crashed attempt's cached premises — undetectably, since the connector's process restarted and sessions were the only surviving state. Under the source-cache protocol that channel can launder replay-era caches into rounds whose rows the resume re-grounds (the record-grounding fix clears the row partition; nothing re-validates session state derived from it). Sessions have no publish/validation concept, so the attempt boundary is the only fence 6b has. groundSessionStoreOnResume: a resumed attempt of a participating sync clears its session namespace before any connector RPC. Non-participating syncs keep the long-standing semantics; a capability-withdrawn resume (CO-6b-003) degrades wholesale as before. Witnessed both ways by TestChaosSourceCacheSessionGroundingOnResume (probe cleared on a participating resume, kept on a withdrawn one). The within-attempt remainder is contractual, pinned in pkg/sourcecache and pkg/session/README.md: replayed scopes produce no generation-side session state, and replay/record verdicts must come from upstream evidence, never session-cached answers. Change order CO-6b-008/009 registered in the 6b plan; REPORT finding extended. Co-authored-by: Cursor <cursoragent@cursor.com>
| if !ok { | ||
| return nil | ||
| } | ||
| if err := provider.SessionStore().Clear(ctx, sessions.WithSyncID(s.syncID)); err != nil { |
There was a problem hiding this comment.
🟡 Suggestion: this clears the store-side session surface, which sits below the connector's own session-store stack. The established clear (connectorbuilder.builder.Cleanup, connectorbuilder.go:377) goes through b.sessionStore — the same handle passed to list calls as SyncOpAttrs.Session (resource_syncer.go:142) — which in the _connector-service and lambda-server topologies is cli.NewLazyCachingSessionStore → session.MemorySessionCache (otter, 10-min write expiry, explicitly documented as "potentially used across syncs"). A crashed attempt runs no Cleanup, so if the connector process outlives the attempt its in-memory cache still holds the pre-crash values and Get serves them straight past this grounding — the exact stale premise CO-6b-009 fences. The witness test uses the direct in-process chaos transport with no caching layer, so it can't observe this. Either route the clear through the delivered session-store handle, or state the "connector process must not outlive the attempt / must not memoize session values across calls" assumption explicitly in pkg/sourcecache and pkg/session/README.md.
| if s.sourceCacheStore == nil { | ||
| return nil | ||
| } | ||
| provider, ok := s.store.(sessionStoreProvider) |
There was a problem hiding this comment.
🟡 Suggestion: this assertion can never fail — s.store is statically c1zstore.Store, which already declares SessionStore() sessions.SessionStore (pkg/dotc1z/c1zstore/c1zstore.go:62), so sessionStoreProvider is not an optional capability the way expandedGrantLayerStorer is. The !ok branch is unreachable dead code today, and if the field type is ever narrowed it turns into a silent disable of the fence (no error, no log). Prefer calling s.store.SessionStore() directly so a type change is a build break, or at minimum log/return an error on the missing-capability path.
…iene The engine author flagged our axiom universals as unconstrained (unconstrained-axiom-universal). Adopting the prescribed fix is not possible today: gating a rewrite universal on a userspace sort of free constructors requires membership evidence that axiom-side dispatch never receives, so member-only ground terms stop reducing (probed in all four documented membership forms; built-in classifiers gate correctly). New probe suite pins today's behavior and fails loudly when the engine closes the gap — the signal to constrain the modules. Modules document the discipline (head-guarded LHS on module-local constructors); lint noise dropped: canonical ∃, removed a require- shadowing declaration and stale per-line disable pragmas. Co-authored-by: Cursor <cursoragent@cursor.com>
| if o.rowKind == sourcecache.RowKindResources { | ||
| // The store contract requires Baton resource BIDs for resource | ||
| // tombstones; a malformed id is a connector bug that fails | ||
| // deterministically before any write, so it must not read warm. | ||
| for _, id := range canonical { | ||
| if !strings.HasPrefix(id, "bid:r:") { | ||
| return newReplayIntegrityError(ReplayVerdictCold, o.rowKind, o.scopeKey, | ||
| fmt.Errorf("resource tombstone %q is not a Baton resource BID (bid:r:...)", id)) | ||
| } | ||
| } | ||
| } | ||
| if len(canonical) > 0 { | ||
| if err := o.s.sourceCacheStore.DeleteSourceCacheRows(ctx, o.rowKind, o.scopeKey, canonical); err != nil { | ||
| return newReplayIntegrityError(ReplayVerdictWarm, o.rowKind, o.scopeKey, | ||
| fmt.Errorf("canonical-id tombstones: %w", err)) | ||
| } | ||
| o.s.testSyncTraceAudit.record(syncTraceDelete, string(o.rowKind), o.scopeKey) | ||
| } | ||
| principals := append(append([]string{}, o.replay.GetDeletedPrincipalIds()...), o.record.GetDeletedPrincipalIds()...) | ||
| if len(principals) > 0 { | ||
| if _, err := o.s.sourceCacheStore.DeleteSourceCacheRowsInScope(ctx, o.rowKind, o.scopeKey, principals); err != nil { | ||
| return newReplayIntegrityError(ReplayVerdictWarm, o.rowKind, o.scopeKey, | ||
| fmt.Errorf("principal-scoped tombstones: %w", err)) | ||
| } | ||
| o.s.testSyncTraceAudit.record(syncTraceDelete, string(o.rowKind), o.scopeKey) | ||
| } |
There was a problem hiding this comment.
🟡 Suggestion: the doc on afterUpserts says "Deterministic input-shape failures (a malformed tombstone id the store can never resolve) are cold — retrying them warm cannot succeed", but the only shape check implemented is the bid:r: prefix guard for resources; every other store rejection is classified ReplayVerdictWarm. DeleteSourceCacheRows still rejects a bid:r:-prefixed but otherwise malformed id via bid.ParseResourceBid, rejects ambiguous grant ids in DeleteGrantRecordsBounded, and can reject entitlement ids — all deterministic connector-input bugs that will re-fail identically on every retry. Latent today (nothing consumes the verdict until 6c), but once the runner ladder honors warm, these become an unbounded warm-retry loop instead of a cold fallback. Consider classifying DeleteSourceCacheRows / DeleteSourceCacheRowsInScope id-resolution failures as cold (e.g. a sentinel from the store's id-parse/ambiguity paths) rather than relying on the prefix approximation. (confidence: medium-high)
| // attempt debris) is cleared before the round's first write. | ||
| // Idempotent; deletes commit in bounded chunks, so retry converges. | ||
| // Returns rows deleted. | ||
| ClearSourceCacheScope(ctx context.Context, kind sourcecache.RowKind, scopeKey string) (int64, error) |
There was a problem hiding this comment.
🟡 Suggestion: SourceCacheStore is an exported interface and this PR adds three methods to it (ClearSourceCacheScope, PutSourceCacheCompat, GetSourceCacheCompat). Any downstream implementation — a test fake, an alternate store — stops compiling, and pkg/sdk/version.go is not touched in this PR, so there is no version signal for the break. Per .claude/skills/ci-review.md, signature-surface changes need at least a 0.x minor bump plus a note. The doc says it is "implemented ONLY by the Pebble engine", which keeps real-world blast radius small; if that is the intent, consider either unexporting it / moving it behind an internal package, or calling the break out in the PR description and bumping the version. (confidence: high on the change, medium on impact)
| p check -tc "$cell" -s "$S" -o "$OUT/$cell" > "$OUT/$cell.log" 2>&1 | ||
| ce=$(ls "$OUT/$cell"/BugFinding/walker_[0-9]*_[0-9]*.txt 2>/dev/null | head -1) | ||
| if [ -n "$ce" ]; then observed="RED"; else observed="GREEN"; fi | ||
| if [ "$observed" = "$expected" ]; then mark="ok"; else mark="MISMATCH"; mismatches=$((mismatches + 1)); fi |
There was a problem hiding this comment.
🟡 Suggestion: p check's exit status is discarded and the verdict is inferred purely from the absence of a counterexample file, so every way the checker can fail to produce output — p not installed, a P-spec compile error, a typo'd -tc name, OOM, a full disk — records observed=GREEN. Every GREEN-expected cell then reports ok, and the checked-in PCheckerOutput/sweep/summary.txt reads as partially-passing evidence for a run that never ran. The script already distrusts the "Found N bugs" tail; it should also distrust a silent no-output run. Capture rc=$? after p check and emit a third ERROR verdict (counted as a mismatch) when the checker exits nonzero or leaves no output directory. formal/graph/tools/sweep.sh:109 has the identical shape. (confidence: high)
…6b-009) The resume-time session-namespace clear shipped in ab99c65 was unsound: resume restores the action queue from the checkpoint and completed actions never re-run, so a wholesale clear destroys session caches whose producing work will not execute again (accumulate-then- consume). The change also rewrote the session contract to match the fix ("attempt-scoped") rather than fixing to the contract. The hazard analysis stands and is now documented honestly: session writes commit outside the checkpoint mechanism (verified in code, not model-derived — the formal models contain no session store), so a resumed attempt inherits the dead attempt's state including writes from beyond the restored cursor. Resolution is contractual (no once-only decisions via sessions; consult verdicts never from session caches; session state silently partial for replayed scopes), with the correct mechanical fence — checkpoint-consistent sessions via a volatile overlay flushed atomically with the checkpoint — registered as future work in the 6b plan. TestChaosSourceCacheSessionPersistsAcrossResume replaces the grounding test: the probe must survive resume with AND without the capability, standing guard against reintroducing a resume-time clear. Co-authored-by: Cursor <cursoragent@cursor.com>
| } | ||
| // Replay copy precedes the page's own rows (frozen order: replay copy → | ||
| // page upserts → page tombstones). | ||
| if err := scOps.beforeUpserts(ctx); err != nil { |
There was a problem hiding this comment.
🟡 Suggestion: the per-scope mutex acquired here is held until afterUpserts at line 2971, which spans the related-resource loop — including s.store.GetResource per grant and the s.getResourceFromConnector connector RPC at line 2939. The lock's stated purpose (beforeUpserts doc) is to keep the replay copy and the page's row application atomic per scope; it does not need to cover connector fetches. At workerCount > 1, every page of the same scope serializes behind those network calls, and a slow upstream stalls the whole scope. Consider narrowing the held window to beforeUpserts → PutGrants/afterUpserts by moving the related-resource fetch loop before beforeUpserts (it writes only unstamped resource rows).
| // ≤256 bytes, validators typically ETag/delta-token sized), re-sorted | ||
| // and re-serialized into the sync token on every checkpoint — | ||
| // O(scopes·log scopes) per checkpoint, pinned by | ||
| // BenchmarkStateMarshalSourceCacheSets. A connector whose scope count |
There was a problem hiding this comment.
🟡 Suggestion: this cost bound assumes "validators typically ETag/delta-token sized", but nothing enforces it. cache_validator is an unbounded connector-supplied proto string, and the only validation on the whole path is a non-emptiness check (pkg/dotc1z/source_cache.go:237, Engine.PutSourceCacheEntry). Its sibling input is capped — sourcecache.ValidateScopeKey rejects scope keys over 256 bytes. Before CO-6b-004 the validator was stored once in the Pebble manifest; now every warm-lookup hit copies it into sourceCacheHits, which Marshal re-serializes into the sync token on every checkpoint, so a connector emitting multi-KB (or worse) validators across many scopes multiplies checkpoint size and live memory with no gate. BenchmarkStateMarshalSourceCacheSets prices the curve but cannot bound it. Consider a sourcecache.ValidateCacheValidator length cap applied at PutSourceCacheEntry and at RecordSourceCacheHit.
| func (o *sourceCachePageOps) groundRecordScope(ctx context.Context) error { | ||
| key := sourceCacheScopeKey(o.rowKind, o.scopeKey) | ||
| if _, done := o.s.sourceCacheScopeGrounded.Load(key); done { | ||
| return nil | ||
| } | ||
| _, published, err := o.s.sourceCacheStore.LookupSourceCacheEntry(ctx, o.rowKind, o.scopeKey) | ||
| if err != nil { | ||
| return newReplayIntegrityError(ReplayVerdictWarm, o.rowKind, o.scopeKey, | ||
| fmt.Errorf("record grounding: reading this sync's manifest entry: %w", err)) | ||
| } | ||
| if !published { | ||
| deleted, err := o.s.sourceCacheStore.ClearSourceCacheScope(ctx, o.rowKind, o.scopeKey) | ||
| if err != nil { | ||
| return newReplayIntegrityError(ReplayVerdictWarm, o.rowKind, o.scopeKey, | ||
| fmt.Errorf("record grounding: clearing un-attributed rows: %w", err)) | ||
| } | ||
| o.s.testSyncTraceAudit.record(syncTraceClear, string(o.rowKind), o.scopeKey) | ||
| if deleted > 0 { | ||
| ctxzap.Extract(ctx).Warn("record grounding cleared un-attributed rows from a prior attempt", | ||
| zap.String("row_kind", string(o.rowKind)), | ||
| zap.String("scope_key", o.scopeKey), | ||
| zap.Int64("rows", deleted), | ||
| ) | ||
| } | ||
| } | ||
| o.s.sourceCacheScopeGrounded.Store(key, struct{}{}) | ||
| return nil |
There was a problem hiding this comment.
🟡 Suggestion (medium confidence): the "no published manifest entry ⇒ un-attributed debris" premise holds for a single paginated cursor (CO-6b-002 restarts it at its root), but not for a scope accumulated by several actions. FinishAction/FinishParentAction delete the completed action from st.actions/st.spawnedInFlight, so a sibling action that finished, stamped rows into scope S, and published no validator is not re-executed after a resume — yet the resumed attempt's first record page for S sees published == false and clears the whole partition. Those rows are then gone from the sealed artifact and, once a later action publishes S's validator, the truncated scope replays forward as if complete. This is the pattern the plan explicitly contemplates ("multi-action accumulation into shared scopes", and the EnqueuePageTokens planning-call fan-out documented on state.sourceCacheHits), so the manifest-entry exemption may be too narrow: consider also exempting scopes with a durable "written this sync by a completed action" marker, or requiring every action that stamps a shared scope to publish.
Worth a chaos cell: two actions (or two EnqueuePageTokens siblings) record into one scope, cut after the first finishes and before any validator publishes, then assert the first action's rows survive the resume.
| chaos-check: ## Run bounded representative chaos checks under race detection. | ||
| go test -race -count=1 ./internal/chaosconnector/... | ||
| go test -race -count=1 -timeout=10m -run '^TestChaosConnector(LostResponseThenFilesystemFailureResumes|ResourcesAndEntitlementsFaultMatrix|ListGrantsFaultMatrix|ReservedBatonIDOwnershipIsRejected|MalformedKnownAnnotationFailsWithoutSealing|ClearedNextPageTokenSealsOnlyVisiblePrefix|CancellationTerminatesAndColdResumes|DataPolicyLifecycleCorpus|ExternalPrincipalResumeUsesCurrentExternalAnswer|SQLiteExternalPrincipalResumeDegradesWithoutFailure|ExternalPrincipalCleanupUsesOnePassPerKeyspace)$$' ./pkg/sync | ||
| go test -race -count=1 -timeout=10m -run '^TestChaosSourceCache(GateMatrix|CollectionSemantics|InterruptResume|GenerationalSteadyState|CompatDriftOnResume|ReplayWithoutHitFailsCold|DriftedResumeRejectsRestoredReplay|DuplicateReplayCursorsParallel|UnsupportedShapesBlockReplaySeed)$$' ./pkg/sync |
There was a problem hiding this comment.
🟡 Suggestion: all nine names in this -run regex exist, but TestChaosSourceCacheRecordFlipOverReplayDebris — the named Go-side witness for CO-6b-008 (the phantom-union defect this branch found and fixed) — is not in the bounded set, so it only runs under chaos-full-check/nightly. The primary regression witness for the headline defect is worth having in the representative set.
| RecordSourceCacheHit(rowKind sourcecache.RowKind, scopeKey string, cacheValidator string) | ||
| SourceCacheHitValidator(rowKind sourcecache.RowKind, scopeKey string) (string, bool) | ||
| MarkSourceCacheReplayed(rowKind sourcecache.RowKind, scopeKey string) | ||
| SourceCacheReplayed(rowKind sourcecache.RowKind, scopeKey string) bool |
There was a problem hiding this comment.
🟡 Suggestion: sync.State is an exported interface, so adding four methods is a source-compatibility break for any downstream var _ sync.State = ... pin or wrapper. Impact is limited in practice — there is no exported way to inject a State into a syncer (newState is unexported and no SyncOpt accepts one), so this is a compile-pin break rather than a functional one. Still, per the repo's SDK criteria this plus the new exported surface (ErrReplayIntegrity, ReplayVerdict, SyncOpAttrs.Lookup, sourcecache.CompatKey) is minor-bump material and pkg/sdk/version.go is unchanged at v0.25.1.
Two findings from the PR's incremental review of the round-1 commit. The bake-off split regressed the audit: tools/bakeoff.sh carried sweep.sh's verdict logic but not its firing-monitor extraction, so a cell was audited for counterexample PRESENCE only. The six GREEN cells stayed protected (a spurious counterexample flips them to MISMATCH), but the six expected-RED cells would have recorded "ok" on a deadlock or liveness counterexample — below the "every red on its calibrated alarm" standard the calibration program rests on — and the committed summary carried none of the tags CALIBRATION.md's prose asserts. bakeoff.sh now extracts and records the alarm, and the regenerated run of record reads [EXEC-BOUND] on the two G6b probes and [SEAL-WORLD] on the four reachable-world probes, 12/12, zero mismatches. A verbatim port would not have sufficed: sweep.sh's alternation has SEAL-EXPECT but not SEAL-WORLD, which is exactly what the G5d cells assert, so those four reds would have been tagged empty. SEAL-WORLD is added to both scripts (output-neutral for the frozen 66 cells — the hyphenated string appears only in that assert's message) so a cell moved between the scripts keeps its tagging. CALIBRATION.md now states the audit property instead of only asserting the alarms. Also deleted the orphaned s_rogue / probe_rogue fixture from probeConstrainedSrc: round 1 moved the refusal assertion to probeBuiltinSrc (the module with a working positive), leaving that module's rogue term unreferenced and liable to read as still exercised. All three constrained-params probes pass. The review's third item (occult/README.md "all five policies") was already fixed in the round-2 dispositions. Co-authored-by: Cursor <cursoragent@cursor.com>
Round-3 review batch. The sweep/bake-off scripts previously ended on a
tee pipeline, so a drifted run read as a green make; now they fail
loudly:
- nonzero exit on any mismatch
- a counterexample-free nonzero p-check exit is CHECKER-ERROR, not
GREEN ("no bug found" from a checker that died is not evidence)
- an untagged red (firing monitor outside the alternation, or rg
missing - now guarded) is a MISMATCH
- the bake-off's declared alarms are ENFORCED, not just recorded, and
the graph alternation is hoisted into tools/alarms.sh (one copy,
sourced by both scripts)
- tcG5dS_W2 pins --sch-feedbackpct=20: its find is seed-bimodal under
uniform random (one full-10k seed explored 18 timelines and found
nothing; five other seeds all found within ~500 schedules at a 0.23%
buggy-schedule rate) - caught by the hardened gate's own first
parity run and registered in CALIBRATION.md
- refimpl: drop the write-only durable.checkpoint field (sibling of
the already-removed hasMarker)
Validated by a planted-violation harness (wrong alarm, unrecognized
monitor, checker crash, drift verdicts, missing rg - each fails with
the right summary line and exit status) and a full bake-off run
through the final script: 12/12 match, exit 0, committed summary
reproduced byte-for-byte. Refimpl build/vet and all four oracle tests
green.
Co-authored-by: Cursor <cursoragent@cursor.com>
| case "$rest" in *:*) | ||
| rest="${rest#*:}" | ||
| alarm="${rest%%:*}" | ||
| case "$rest" in *:*) strategy="${rest#*:}";; esac | ||
| ;; esac |
There was a problem hiding this comment.
🟡 Suggestion (medium confidence): the two scripts' CELLS grammars are now positionally incompatible — sweep.sh reads field 3 as strategy, bakeoff.sh reads it as alarm. Since moving a cell between the scripts is an anticipated operation (alarms.sh and the header comments both reason about it), a sweep entry like tcG2awWA_E:RED:--sch-feedbackpct=20 pasted here parses as alarm="--sch-feedbackpct=20", strategy="": the search pin is silently dropped and the alarm assertion can never match, so the cell permanently reports MISMATCH. For a GREEN cell the drop is fully silent, because the alarm branch is never entered. Consider rejecting a field-3 value that starts with -- (or that is not in MONITOR_ALTERNATION) with a loud parse error, matching the rest of this commit's "never fail quietly" posture.
| tcG5dE_W2:RED:SEAL-WORLD | ||
| tcG5dS_W2:RED:SEAL-WORLD:--sch-feedbackpct=20 |
There was a problem hiding this comment.
🟡 Suggestion (medium confidence): only the S leg of W2 gets the pin, but CALIBRATION.md's own diagnosis attributes the bimodality to the target ("Some seeds evidently cannot reach the target at all"), and both legs declare the same target {0→1, 1→1} (CALIBRATION.md:392-393). This commit also promotes a miss from a summary line to a nonzero exit that fails make formal-graph-bakeoff, and under GS-CO-005(d) a leg deviating from its declared verdict under exactly one variant is a divergence finding blocking Axis-3 citation — so a seed-unlucky tcG5dE_W2 would now surface as a variant asymmetry rather than a recognizable flake. Either pin the E leg too, or record its measured uniform-random find rate in CALIBRATION.md as the evidence that it is not bimodal.
Review items: - bakeoff.sh grammar guard: the fields are positional and the alarm is only consulted on the RED branch, so a strategy flag written in the alarm slot (cell:GREEN:--flag) was dropped SILENTLY - the cell ran without its intended search and still reported ok. Now rejected at parse time with the strategy-only form (cell:expected::--flag) in the message; validated with a planted scratch run (exit 2). - sweep headers now state the exit-status division of labor: p check's exit gates only the GREEN side (absence of a find from a checker that died proves nothing); a found counterexample stands regardless. - TRACE_BRIDGE Mapping 1: the graph overlay unit also announces upserts and tombstones, and its G8b composeDead INJECT branch announces the copy with NO clear at all - by design, that missing clear IS the tcG8bMut_P1 kill. Stated as the one exception so a hand-renderer cannot mask the injected red by supplying a clear the model never announced (review comment from the r3899 wave). - Makefile formal comment untangled: tag differences on multi-shape RED cells are exit-0 noise; a missed find fails the gate by design. Full-pass validation, all through the hardened scripts: - walker sweep 55/55, exit 0, summary byte-identical - graph sweep 66/66, exit 0, summary byte-identical - bake-off 12/12, exit 0, summary byte-identical (prior run) - Occult host suite green against the engine's ground-eval-perf branch (6785def4): full suite in ~32 min wall vs 75+ before - verdict-preserving across the laws, MPST, 140-cell policy matrix, real-trace fixtures (both standing red pins intact), and refimpl. Also: cell lists cross-checked against committed evidence (55/66/12 exact), both alternations verified to cover their monitors' full assert vocabularies, no stale counts or dead refs. Co-authored-by: Cursor <cursoragent@cursor.com>
| # shapes) diffs the summary but still exits 0, while a RED cell that | ||
| # MISSES its find fails the gate by design — that has happened once, | ||
| # from seed-bimodal search on a narrow target, and the remedy is a | ||
| # per-cell strategy pin (see the tcG5dS_W2 note in graph CALIBRATION). |
There was a problem hiding this comment.
🟡 Suggestion: this comment prescribes "a per-cell strategy pin" as the remedy for a missed RED find across both sweeps, but only formal/graph/tools/sweep.sh (field 3 = strategy) and bakeoff.sh (field 4) can express one — formal/walker/tools/sweep.sh parses cell:expected with ${entry##*:} and passes no strategy to p check, so a walker pin lands in expected and reports expected=--sch-feedbackpct=20 … MISMATCH rather than pinning anything. Either give the walker sweep the same optional strategy field (plus the grammar guard this commit adds to bakeoff.sh) or scope this sentence to the graph scripts.
A PR review comment on the sweep's cell list was stale on all three of its claims (it predates the trace-archive purge, the probe-cell row, and the rewritten archival contract), but re-running the cell-vs-row audit it implied found the real gap next door: scenario 4 (duplicate replay carriers, MODEL_SPEC §9 case 4) has been in every sweep since the v11 freeze yet never had a section in CALIBRATION.md. Added with the frozen verdicts; no cell or expectation changed. The graph log audits clean under the same check (its G3/G4/G6-G9 families are deliberately collective-prose sections). Co-authored-by: Cursor <cursoragent@cursor.com>
Review follow-up on the round-4 guard: (1) bakeoff.sh's alarm-slot guard matched only --* so a single-dash flag still fell through and was silently dropped on a GREEN cell — the exact failure the guard exists to stop; alarm names never begin with a dash, so -* is safe. (2) sweep.sh's mirror field (third field = strategy) had no shape check, so an entry pasted in from bakeoff's 4-field grammar handed p check an alarm name as a bogus positional argument; it now fails loudly at parse time with the grammar named. Both guards exercised via stub-checker runs: bad entries exit 2 before any checker call, good entries (real flag; empty-alarm form) still reach GREEN. Also answered the standing Makefile evidence note: the 2026-09-01 full pass re-ran every cell through the gated scripts and reproduced all committed summaries byte-identically, which is why no post-gate summary commit exists. Co-authored-by: Cursor <cursoragent@cursor.com>
| _, published, err := o.s.sourceCacheStore.LookupSourceCacheEntry(ctx, o.rowKind, o.scopeKey) | ||
| if err != nil { | ||
| return newReplayIntegrityError(ReplayVerdictWarm, o.rowKind, o.scopeKey, | ||
| fmt.Errorf("record grounding: reading this sync's manifest entry: %w", err)) | ||
| } | ||
| if !published { | ||
| deleted, err := o.s.sourceCacheStore.ClearSourceCacheScope(ctx, o.rowKind, o.scopeKey) | ||
| if err != nil { | ||
| return newReplayIntegrityError(ReplayVerdictWarm, o.rowKind, o.scopeKey, | ||
| fmt.Errorf("record grounding: clearing un-attributed rows: %w", err)) | ||
| } | ||
| o.s.testSyncTraceAudit.record(syncTraceClear, string(o.rowKind), o.scopeKey) | ||
| if deleted > 0 { | ||
| ctxzap.Extract(ctx).Warn("record grounding cleared un-attributed rows from a prior attempt", | ||
| zap.String("row_kind", string(o.rowKind)), | ||
| zap.String("scope_key", o.scopeKey), | ||
| zap.Int64("rows", deleted), | ||
| ) | ||
| } | ||
| } |
There was a problem hiding this comment.
🟠 Bug: "un-published rows" is not the same set as "crashed-attempt debris". The annotation proto explicitly allows a multi-page record round to carry an empty cache_validator on interim pages (SourceCacheRecord.cache_validator: "May be empty on interim pages of a multi-page scope"), so a round in progress has committed rows and no manifest entry. If the sync is cut after page N commits and checkpoints, the resume continues at page N+1 (action.PageToken), sourceCacheScopeGrounded is empty, LookupSourceCacheEntry finds nothing published, and ClearSourceCacheScope deletes pages 1..N — rows that will never be re-listed. The final page then publishes a validator over the truncated partition, so the sealed artifact silently loses rows and replays the truncated scope forward warm.
Suggest distinguishing "debris from a dead attempt" from "rows this round already committed" durably — e.g. record a per-(rowKind, scopeKey) round-grounding marker in the store as part of the same commit as the first grounded page, and skip the clear when the checkpointed action's page token shows the round is mid-flight rather than restarting.
| func (c *directClient) SetSourceCache(ctx context.Context, lookup sourcecache.Lookup) { | ||
| if setter, ok := c.server.(sourcecache.SetLookup); ok { | ||
| setter.SetSourceCache(ctx, lookup) | ||
| } | ||
| } |
There was a problem hiding this comment.
🟡 Suggestion: directClient (and GRPCClient at line 65) satisfy sourcecache.SetLookup structurally but silently drop the lookup when c.server is not a SetLookup, and neither implements sourcecache.LookupDeliverabilityProbe — so installSourceCacheLookup presumes them deliverable, sets sourceCacheWarm = true, and logs "warm" while the connector actually observes NoopLookup. That is exactly the CO-6b-001 false-warm shape the probe exists to close, and these are the only in-tree delivering transports, so a harness misconfiguration would produce silently vacuous warm-path tests. Consider implementing SourceCacheLookupDeliverable() on both (returning whether the server implements SetLookup).
| if err != nil { | ||
| // A token that DECLARES a version is a v1+ token whose full | ||
| // parse failed (corrupt, or a field's shape changed under a | ||
| // reused key). Falling back to v0 here would misparse it — | ||
| // the v0 struct ignores the unknown v1 fields, "succeeds" | ||
| // with an empty action stack, and the resume silently | ||
| // restarts as a fresh sync. Fail loud instead; only tokens | ||
| // without a version field are genuinely v0. | ||
| var probe struct { | ||
| Version *uint64 `json:"version"` | ||
| } | ||
| if probeErr := json.Unmarshal([]byte(input), &probe); probeErr == nil && probe.Version != nil { | ||
| return fmt.Errorf("syncer token declares version %d but failed to parse: %w", *probe.Version, err) |
There was a problem hiding this comment.
🟡 Suggestion: this converts a previously self-healing failure into a permanently wedged sync. The token lives in the store, so Sync → state.Unmarshal(currentStep) will return this same error on every subsequent attempt; nothing in pkg/tasks/c1api/full_sync.go or pkg/tasks/local/syncer.go reacts by abandoning the sync and starting a fresh one. Failing loud instead of silently restarting is the right direction, but the loud failure needs an escape hatch (a distinct sentinel error the runners can map to "discard the checkpoint and start cold", or an automatic fresh-sync fallback here) or a corrupt v1 token blocks the tenant indefinitely.
…ister unwitnessed-clause inventory Round-5 review found the first substantive gaps in several waves, all three verified real. (1) tc8overDelete_P8: P8-EXT-MISSING had no kill — the over-deletion direction of the external-principal seal clause was asserted, not calibrated (P8's other two clauses and the P6-C pattern both witness bidirectionally). The kill models a LATE stale-sweep whose predicate mistakes a live principal for stale; placement is itself a model fact: the engine-ordered early pass (delete-stale before copy) is structurally self-healing for over-deletion because the page-1 copy rewrites every listed id. Sweep regenerated: 56 cells, 0 mismatches. (2) pipeline_test.go discarded LoadExpressions' error — a silent failure there would turn every negative control vacuous (an empty e-graph refuses every equivalence, which is what the controls assert); now t.Fatalf like every other engine call, equivalence suites re-run green. (3) The remaining asserted-but-unwitnessed alarm strings (walker 3, graph 8) are inventoried in REPORT.md's standing limits and the graph CALIBRATION so the green matrices are not over-read; the graph eight are walker-inherited oracles whose graph-side implementations are calibrated only by review. Co-authored-by: Cursor <cursoragent@cursor.com>
|
|
||
| | cell | config | property | expected | observed | budget | | ||
| |---|---|---|---|---|---| | ||
| | tc3a_P1 | shipped (`hitValidatorBinding` ON) — the residual hole | P1 | RED | RED: `P1-CONTENT` is the archived sweep's first find (carrier-first/interleaved content shape); the `P1-ATTEST-SEAL` carrier-last shape (rows(B) sealed under entry V_A) is also live in the config — both require the re-consult's lookup-hit V_B to OVERWRITE the hit map before the carrier's LIVE hit read (last-write-wins rebind) | first find (0.34% of 10k — narrow: needs C dispatched after P's re-consult transition) | |
There was a problem hiding this comment.
🟡 Suggestion: This row still says ``P1-CONTENT is the archived sweep's first find, but this commit updates the archived run of record to `tc3a_P1 ... ok [P1-ATTEST-SEAL]` (`PCheckerOutput/sweep/summary.txt`). `tools/sweep.sh` explicitly designates CALIBRATION.md — not the script — as "the comparison surface for WHICH monitor fired," so the audit surface and the run of record now disagree and nothing mechanical catches it. Since the row already documents both shapes as live in this config, updating the parenthetical to name `P1-ATTEST-SEAL` as the current archive's find (and, if intended, noting that the first-find shape flipped when the `extOverDelete` config field changed the exploration order) restores the audit. (confidence: high)
| COVERAGE LIMIT of the frozen matrix (registered post-freeze; no cell | ||
| or expectation changed): eight of Monitors.p's 25 alarm strings fire | ||
| in no red cell — P1-CONTENT, P1-ATTEST-PUBLISH, P1-ATTEST-SEAL, | ||
| P1-ATTEST-EMPTY, P2-CONSULT, P2-STALENESS, P3'-COHERENCE, | ||
| PASS-BUDGET. They are the walker-inherited content/attestation/ |
There was a problem hiding this comment.
🟡 Suggestion: Scoped to "the frozen matrix" (the 66-cell sweep this paragraph follows), the count is nine, not eight: SEAL-WORLD also fires in no red cell of PCheckerOutput/sweep/summary.txt. It is witnessed only by the separate 12-cell bake-off matrix (PCheckerOutput/bakeoff/summary.txt, 4 cells), which tools/alarms.sh already records ("SEAL-WORLD is asserted only by the bake-off's tcG5d* cells"). A reader regenerating this inventory from the sweep summary alone gets a different answer than the registered one; a half-sentence qualifier naming SEAL-WORLD as bake-off-witnessed makes the count reproducible. REPORT.md's "8 of its 25" is fine as written since it says "frozen matrices" plural. (confidence: medium-high)
| # Walker calibration — run log | ||
|
|
||
| Status: COMPLETE. CURRENT GATE: the 56-cell full-matrix sweep, 0 | ||
| mismatches, every red on its calibrated alarm (`tools/sweep.sh`, 10k |
There was a problem hiding this comment.
🟡 Suggestion: The graph leg registers its unwitnessed-clause inventory in its own CALIBRATION.md and mirrors it to REPORT.md; the walker's three (P1-ATTEST-EMPTY, P1-ATTEST-PUBLISH, P2-CONSULT) are registered only in REPORT.md. Since this log is the run-of-record audit surface and its status line asserts "every red on its calibrated alarm," a matching COVERAGE LIMIT note here would keep the two legs symmetric and stop the 56-cell green from being over-read by a reader who only opens the walker log. (confidence: medium)
… the two-shape contract Both doc-only, closing the round-6 bot pass: the tc3a_P1 row now states its conformance contract explicitly (either P1-CONTENT or P1-ATTEST-SEAL is calibrated — which trips first is seed luck — and any OTHER alarm is real drift), so a reader diffing the run of record against this log has a check for the shape flip instead of a stale "first find" claim; and the walker log now carries the mirror of the graph's COVERAGE LIMIT block (P1-ATTEST-EMPTY, P1-ATTEST-PUBLISH, P2-CONSULT are asserted, not calibrated), kept minimal with the shared doctrine pointed at REPORT.md to avoid a third drifting copy. Co-authored-by: Cursor <cursoragent@cursor.com>
| if o.s.state.SourceCacheReplayed(o.rowKind, o.scopeKey) { | ||
| // Duplicate page / lost-response retry: the copy already ran this | ||
| // sync. Replay is replacement, so re-running it would also wipe | ||
| // overlay rows upserted since. Skip the copy; apply the page's | ||
| // upserts/tombstones normally. | ||
| l.Debug("source-cache replay already completed for scope this sync; skipping copy", | ||
| zap.String("row_kind", string(o.rowKind)), | ||
| zap.String("scope_key", o.scopeKey), | ||
| ) | ||
| } else { |
There was a problem hiding this comment.
🟡 Suggestion: the replay path never consults sourceCacheScopeGrounded, so the record→replay page order for one scope in one attempt is unguarded (the reverse order is). If a record-only page for scope S runs first, groundRecordScope clears/writes and marks the scope grounded; a later replay page for S then either (a) runs the replacement copy — ReplaySourceCache clears the destination scope, deleting the record page's fresh rows — or (b) with SourceCacheReplayed(S) restored from a prior attempt, skips the copy entirely after this attempt's grounding already cleared the base. Both end in a scope sealed under a published validator with rows missing, which the next sync validates clean and replays forward.
This needs the connector to emit both verdicts for one scope (out of contract), but every other out-of-contract shape in this file fails loud (two scope keys per page, duplicate annotations, deleted_principal_ids on entitlements) rather than silently producing a wrong durable artifact. Consider: if sourceCacheScopeGrounded already holds the key when the replay path is entered and the copy has not run this sync, return newReplayIntegrityError(ReplayVerdictCold, ...). Confidence: medium — the ordering permutation isn't covered by TestChaosSourceCacheOrderingAdversary. (Also worth noting the scope lock added for CO-6b-003/N1 makes record and replay pages mutually atomic but does not order them, so parallel mode leaves the arrival order to worker scheduling rather than the connector.)
|
subsumed into other work |
1 participant
Source-cache replay (phase 6b) + formal verification of sync scheduling
Status: not for merge as-is. This branch contains the phase 6b
implementation and the formal verification work that characterizes a
structural defect in its composition algorithm. The current algorithm can
seal artifacts containing permanently dead data presented as live (details
below), and that data then replays into subsequent warm syncs. The merge
path is the replacement runtime designed and verified on this branch
(RFC 0011), not the 6b composition as it stands. The branch is published as
the archive of record for both the implementation and its verification.
What's here
Three related bodies of work.
1. Source-cache replay orchestration (phase 6b) —
pkg/,internal/,proto/Warm syncs can reuse partitions of the previous sync's artifact instead of
refetching them. Connectors annotate page responses to either record a
partition (fresh rows, tagged with a validator string) or replay it
(copy the previous artifact's partition forward, optionally overlaying
changed rows and tombstoning deleted ones). The syncer orchestrates:
evidence before deciding; bounded to 4 round-trips per request);
together);
Touches
pkg/sync(orchestration),pkg/dotc1z/pkg/sourcecache(storage),
proto/pb(annotations),internal/chaosconnector(testharness). Verification evidence:
docs/verification/sync-replay-6b/.2. Formal verification of the scheduling semantics —
formal/(no production code)Two tools, for readers unfamiliar with them:
machines plus properties that must hold, and it mechanically explores
very large numbers of crash and interleaving schedules looking for a
violation, printing the exact schedule when it finds one.
system's operations and it proves or refuses claimed identities; it can
also evaluate invariant-checking functions over recorded event logs.
What was done with them:
trust by mechanically rediscovering known bugs before being believed
about anything else. Result: with the shipped mitigations ON, the
checker still seals a phantom union — individually truthful
connector responses composing into an artifact containing rows that no
longer exist upstream, which then replay warm into later syncs as
live data with unbounded staleness. This is the defect that blocks
merging 6b's composition as-is (
formal/walker/CALIBRATION.md,scenario 1; each red cell archives its counterexample schedule).
admitted by tracked demand, every output carries lineage, seal-time
obligations are checked against a closure oracle). Model-checking found
five design bugs during calibration — all fixed in the spec before any
code exists — and a structured bake-off between two lineage designs
selected observable-causal stamps (
formal/graph/BAKEOFF.md).composition, a deductive derivation showing the current composition
rule manufactures the phantom union, and conformance proofs for the
lookup negotiation protocol (
formal/occult/).Entry point:
formal/REPORT.md(verdicts, findings register, and anexplicit statement of what is and is not guaranteed).
3. The bridge: checking real executions against the formal invariants
pkg/syncgains a test-only event recorder(
pkg/sync/sync_trace_audit.go). It is a nil pointer in production —only test code can enable it, and test files are not compiled into
production binaries; each call site costs one nil check. Chaos tests run
the real syncer, export the recorded commit-order event logs, and an
Occult test suite verifies every exported execution obeys the ordering
and durability invariants (writes only into partitions cleared this sync,
publish before a checkpoint claims quiescence, seal only after
obligations are met — across cold, warm, crash/resume, and tombstone
executions). This instrument also falsified one piece of documented
resume behavior: a documented "skip the re-copy on resume" mechanism is
unreachable; the code is safe via idempotent re-copy instead. Comments
were corrected (
pkg/sync/chaos_source_cache_resume_test.go).Also included
docs/rfcs/0011-demand-graph-sync-runtime.md— the kickoff design docfor implementing the verified replacement runtime in
pkg/sync.Reviewer routing
Per
docs/REVIEW_CHECKLIST.md: the production-behavior changes are item1 plus the nil-guarded recorder call sites from item 3 — route HIGH
(silent/combinatorial subsystem). Item 2 is additive models and
documentation; the rest of item 3 is test code and fixtures.