formal: sync scheduling verification track (P models + Occult) - #1117
Merged
Conversation
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Contributor
General PR Review: formal: sync scheduling verification track (P models + Occult)Blocking Issues: 0 | Suggestions: 1 | Threads Resolved: 0 Review SummaryThe new commit is documentation-only in Risk triage (per Security IssuesNone found. Correctness IssuesNone found. Verified the new inventory against the model: Suggestions
Prompt for AI agents |
Two P model-checking projects and an Occult deductive track for the sync scheduler's crash/resume semantics, plus the specs, calibration logs, adversarial reviews, and synthesis report behind them. Purely additive: no production code, and the Occult host is a standalone Go module (root builds, tests, and lint do not touch it; it requires a sibling ../occult checkout to run). - formal/walker: the shipped design's model. 55 calibrated cells, 0 mismatches — every known bug class reds on its calibrated alarm (phantom union, session laundering and checkpoint consistency, hit rebind, warm drift, overlay placement, session elision, external principals) and every shipped/staged mitigation greens. - formal/graph: the demand-graph replacement runtime (frozen spec v4 after three adversarial rounds), 66-cell matrix plus the 12-cell bake-off that selected variant S (docs/rfcs/0011 is the kickoff). - formal/occult: 15 equational laws proved, the phantom union derived deductively, the syncer-connector protocol projected (MPST), and seven trace policies with a 140-cell verdict matrix; committed real-execution fixtures are judged by the same oracle. - formal/REPORT.md is the synthesis: findings register (two shipped defects among them), linkage grades, and standing limits. The trace-bridge fixture GENERATORS (the pkg/sync commit-order recorder and chaos exporters) land with the phase-6b PR; until then the committed JSONL fixtures are inert test data for the standalone oracle module. Co-authored-by: Cursor <cursoragent@cursor.com>
kans
force-pushed
the
kans/formal-verification
branch
from
August 31, 2026 20:56
6865ba2 to
060a83c
Compare
All eleven findings from the two automated review passes verified and dispositioned: bake-off cells split out of sweep.sh into a committed tools/bakeoff.sh (re-run 12/12 clean) so the test-plan command can no longer overwrite the frozen 66-cell evidence; both CALIBRATION.md status blocks rewritten to match their own committed evidence (walker 55-cell gate named, graph 66-cell freeze + completed bake-off named); the missing tc1c_P1_probe calibration row added; five-vs-seven policy count drift fixed across the coalescing note, refimpl comments, and policy-module fixture comments; policy 2's by-design cross-attempt regrounding blindness documented at ev_resume and in TRACE_BRIDGE.md; the dead structural-clear renderer branch now has an instrument-validation test; the vacuous non-member refusal control now runs against a module with a working positive; dead code in compression_test.go deleted; the stray 921KB solver checkpoint dropped and ignored; the Go 1.26 toolchain requirement documented. Affected host tests green; bake-off re-run through the new script, BAKEOFF-DONE cells=12 mismatches=0. Co-authored-by: Cursor <cursoragent@cursor.com>
Nine real findings from two independent static reviews, none verdict-flipping: TRACE_BRIDGE Mapping 1 rewritten against the actual announce vocabularies and labeled prose-only with a renderer-hazard warning; MS-CO-002 registered (torn rounds are stop-reachable, monitor-side exclusion, P3-prime narrowing recorded at spec, calibration, and code); graph digest session-field vacuity declared per SPEC 4a's closure clause; refimpl emits ev_delete and drops a dead field (all four scenarios re-run green through seven policies); policy 1 header and policy 5 scope corrected; REPORT red-pin overclaim, tc3a_P1 observed alarm, capable-engine fixture description, projection order dependency, and one five-vs-seven leftover fixed. Co-authored-by: Cursor <cursoragent@cursor.com>
Same change as the working branch: guarded wrappers (P checker, sibling ../occult checkout) for the sweeps, bake-off, and host suite; no installation targets. Co-authored-by: Cursor <cursoragent@cursor.com>
…argets commit The formal PR adds only the formal-* targets; the chaos-check / chaos-full-check source-cache patterns belong to the 6b branch whose tests are not on main. Co-authored-by: Cursor <cursoragent@cursor.com>
tools/bakeoff.sh lost sweep.sh's firing-monitor extraction in the round-1 split, so expected-RED cells were audited for counterexample presence only and would have recorded ok on a deadlock or liveness counterexample. The tag is restored (SEAL-WORLD added to both scripts — the G5d monitor was missing from sweep.sh's alternation), the bake-off summary regenerated with [EXEC-BOUND] / [SEAL-WORLD] tags at 12/12, and the calibration log now states the audit property. Also dropped the orphaned rogue fixture left in probeConstrainedSrc when the refusal control moved to probeBuiltinSrc. 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>
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>
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>
…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>
… 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>
Comment on lines
+32
to
+39
| COVERAGE LIMIT of the 56-cell matrix (the graph log carries the | ||
| mirror block for its leg; shared doctrine and both inventories in | ||
| REPORT.md's standing limits): three of this model's alarm strings | ||
| fire in no red cell — P1-ATTEST-EMPTY, P1-ATTEST-PUBLISH, and | ||
| P2-CONSULT. Each is a narrower sibling of a witnessed clause on the | ||
| same monitor (P1-ATTEST-SEAL, P1-CONTENT, and P2-STALENESS all have | ||
| reds); by this log's own doctrine the three are asserted, not | ||
| calibrated, and a green matrix says nothing about them. |
Contributor
There was a problem hiding this comment.
🟡 Suggestion: the block it mirrors states a denominator (graph/CALIBRATION.md:377 — "eight of Monitors.p's 25 alarm strings"), and the denominator is what makes the limit quantitative: the walker leg is 3 of 19 assert strings in PSpec/Monitors.p, which reads very differently from the graph's 8 of 25. Consider "three of this model's 19 alarm strings" so the two legs are comparable at a glance. (Low confidence — legibility only; the inventory itself is correct: P1-ATTEST-EMPTY, P1-ATTEST-PUBLISH, and P2-CONSULT are exactly the assert strings absent from every red row in the committed 56-cell summary, and each does sit on the same spec P1/spec P2 monitor as the witnessed clause named.)
kans
enabled auto-merge (squash)
September 1, 2026 18:16
gontzess
approved these changes
Sep 1, 2026
kans
added a commit
that referenced
this pull request
Sep 1, 2026
Single squashed implementation commit, rebased onto main after the formal verification track (#1117) landed separately. Contains the 6b branch through CO-6b-007 plus the production fixes made during the formal effort: - Capability parsing, warm/cold lookup installation with the deliverability probe (CO-6b-001), compat record write/gating, selection fingerprint, checkpointed hit/replay provenance with the warm gate, per-scope locks (CO-6b-004/006), warm-vs-cold ErrReplayIntegrity verdict taxonomy, CO-017 cross-version fold fence. - Record-round grounding (finding 0 of formal/REPORT.md): a record round is a replacement listing, so a partition holding rows no completed round published is cleared before the round's first write (groundRecordScope + engine ClearSourceCacheScope), witnessed by TestChaosSourceCacheRecordFlipOverReplayDebris. - CO-6b-009: session persistence semantics pinned contractually; wholesale resume-clear rejected as unsound. - Test-only commit-order trace recorder (sync_trace_audit.go) and the chaos trace oracle exporting the JSONL fixtures judged by the Occult trace bridge (formal/occult/TRACE_BRIDGE.md). - Source-cache chaos suites wired into chaos-check; verification packet under docs/verification/sync-replay-6b/; RFC 0010. Co-authored-by: Cursor <cursoragent@cursor.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Formal verification track for the sync scheduler's crash/resume semantics: two P model-checking projects plus an Occult deductive track, with the frozen specs, calibration logs, adversarial reviews, and synthesis report behind them.
formal/walker/— model of the shipped design. 55 calibrated cells, 0 mismatches: every known bug class reds on its calibrated alarm (phantom union, session laundering / checkpoint consistency, hit rebind, warm drift, overlay placement, session elision under replay, external principals), and every shipped or staged mitigation greens. Red counterexamples regenerate on demand (p check -tc <cell>, seconds-to-minutes to first find); the sweep summaries are archived underwalker/traces/.formal/graph/— the demand-graph replacement runtime (spec frozen at v4 after three adversarial review rounds), 66-cell matrix plus a 12-cell bake-off that selected variant S.docs/rfcs/0011is the kickoff RFC.formal/occult/— 15 equational laws proved, the phantom union derived deductively from an axiomatization of the broken composition, the syncer↔connector protocol projected per-role (MPST), and seven trace policies with a 140-cell verdict matrix. Committed real-execution fixtures are judged by the same oracle.formal/REPORT.md— the synthesis: findings register (two shipped defects among them), the three linkage grades, standing limits, and next steps.What this is not
No production code. Zero deletions. The Occult host is a standalone Go module — root builds,
go test ./..., and lint do not touch it, and running it requires a sibling../occultcheckout. The P sources need the P checker locally; nothing here runs in CI.The trace-bridge fixture generators (the
pkg/synccommit-order recorder and chaos exporters) land with the phase-6b PR; until then the committed JSONL fixtures are inert test data referenced by the standalone oracle module.Test plan
cd formal/walker && p compile -pp walker.pproj && tools/sweep.sh 10000— 55 cells, 0 mismatchescd formal/graph && p compile -pp graph.pproj && tools/sweep.sh— frozen matrix cleancd formal/occult/host && go test -timeout 90m ./...— laws, protocol, policy matrix, real-trace oracle (requires../occultcheckout)make lint/go test ./...are unaffected (no production paths touched)