Repository navigation
docs(skills): hash imports and commit mutate.sh in verify-lane-schedule - #677
Conversation
…h-lane schedule Model-checks the ADR-50 push lane (SQLite and S3-WAL) against git pushes, push-upstream calls, runs, steals, retries, restores, crashes and shutdown. Nine code facts tie the model to both backends and the worker; fingerprints in the lane-schedule-fingerprints CI job flag covered-code changes. The NoCompletionAssumption probe records two findings: a push that dies after its authority CAS can lose its forward. Change-Id: I07baac11eba4d51333064aa0fb5e90dd84e48653 Signed-off-by: Thomas Kosiewski <tk@coder.com>
…e model variables Change-Id: Iafc903e2e9a284d33bd0cb076b93f5c621837eb2 Signed-off-by: Thomas Kosiewski <tk@coder.com>
…print the push-hold path Codex round 1 on #675: fingerprint the push-hold lifecycle, both refspec vars and LocalScheduler.Start; model pushes that record no intent; state that ref deletions are not forwarded by design. The model now counts a write as owed at its CAS, adds REST writes (OtherWriters.cfg) and a HeldRefsFresh probe that fails with no fault. Change-Id: I863914ac2567ec75ba1b8f92a9b68663b3816c6d Signed-off-by: Thomas Kosiewski <tk@coder.com>
…model forward-denied REST writes Codex round 2 on #675: fingerprint every function of events/refstore.go and githttp/publication.go and every push-hold helper in hydrate.go; add QuietRestWriters; state that rewrites are out of scope (plain forwards of a non-fast-forward fail as FailRejected by design). Change-Id: I6a4da0c6e58ec9300fa36353932fc34ae10d74a7 Signed-off-by: Thomas Kosiewski <tk@coder.com>
Codex round 3 on #675 asked for five more helpers (claimLeaseSlack, the failure classifier, NewLocalScheduler, the sync-claim suppression, handlePushUpstream). Covering whole files ends the per-helper list: any change in the 14 covered files now reports STALE. Change-Id: I42088c0ec10f00a00c7004fd9be576923f599a57 Signed-off-by: Thomas Kosiewski <tk@coder.com>
…ify-lane-schedule's blind spots Follow-up to #675 (Codex round 4 and the readiness advisor): fingerprint import specs, cover internal/sync/metastore.go and pushstatus.go, name the atomicity helpers outside coverage under When to run it, give every Left out item its user-visible harm, and commit the 9/9 mutation harness as mutate.sh. Change-Id: I4be6d2bf0160070be10f7be922e8e179635903aa Signed-off-by: Thomas Kosiewski <tk@coder.com>
Change-Id: Ife943e85c36acd3281a3071a45756fa7ecf964d3 Signed-off-by: Thomas Kosiewski <tk@coder.com>
Change-Id: I77018aa9fedeaaf89d276da9344109c733158a19 Signed-off-by: Thomas Kosiewski <tk@coder.com>
Change-Id: Id95ee33155672f161d8d5047907d2c63b1ef0bab Signed-off-by: Thomas Kosiewski <tk@coder.com>
|
@codex review |
|
@codex security review |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
Security findingsAdvisory findings (1)ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 496e76ac76
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
There was a problem hiding this comment.
🛡️ Codex Security Review
Here are some automated security review suggestions for this pull request.
Reviewed commit: 496e76ac76
ℹ️ About Codex security reviews in GitHub
This is an experimental Codex feature. Security reviews are triggered when:
- You comment "@codex security review"
- A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review
Once complete, Codex will leave suggestions, or a comment if no findings are found.
…baseline, and keep logs private Codex round 1 on #677. Also print how to fetch a sync commit that a squash merge left off main. Change-Id: Id075d4c0c56cf85a33cb21c9123adfe8440e73e6 Signed-off-by: Thomas Kosiewski <tk@coder.com>
|
@codex review |
|
@codex security review |
|
Codex Review: Didn't find any major issues. Another round soon, please! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
…ne-schedule text check.sh --fact NAME=FALSE sets one fact FALSE in the model only, and mutate.sh --model uses it to rerun the "each fact matters" result. mutate.sh checks for bash 4 and python3 up front. SKILL.md gives the mutate.sh command and its needs, labels the NoLostForward-only result as one-off, stops calling toRepoUpstream an atomicity helper, fixes the sample output and exit-3 wording, and gives a fetch hint that works for a squash-merge sync commit. _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_ Change-Id: Ib660a72209add89d9e3ef855c2828c33a4c8646b Signed-off-by: Thomas Kosiewski <tk@coder.com>
|
@codex review |
|
@codex security review |
|
Codex Review: Didn't find any major issues. More of your lovely PRs please. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
Why
#675 added
verify-lane-schedule, a formal check of the local push-lane schedule. Its review round 4 and its readiness advisor found that a few of the skill's claims overstated what it checks. The owner waived the open round-4 finding for #675 on the condition that this follow-up fixes it in the same run. This PR makes the skill match what it checks, and makes its Validation table rerunnable.What
facts/facts.gohashes import specs too. Before, a changed import path left every fingerprint unchanged. This is the round-4 finding on docs(skills): add verify-lane-schedule, a TLA+ check of the local push-lane schedule #675.internal/sync/metastore.go(the store adapter's error mapping) andinternal/sync/pushstatus.go(the upstream rejection parser) join the covered files.SQLite.inTx,S3WAL.mutateand itsrecoverhandling, andtoRepoUpstream.mutate.shis new. It breaks each of the 9 code facts once in the real Go source, checks that the package compiles, runscheck.sh --only <config>, and restores the file. It prints one line per mutation and a count line.check.shandfacts.gowording says "declarations", not "functions".mutate.shrestores the broken file on INT, TERM and EXIT, requires each config to pass unmodified before its breaks count, and keeps every log inside one privatemktemp -ddirectory.check.shand SKILL.md say how to fetch a sync commit that git does not know:git fetch --unshallow originin a shallow clone, and therefs/pull/*refspec for a sync commit recorded at a PR head.check.sh --fact <Name>=FALSEsets one fact FALSE in the model only.mutate.sh --modeluses it to rerun "each fact flipped in the model alone fails the same property".mutate.shchecks for bash 4 and a working python3 up front.mutate.shcommand and what it needs, labels theNoLostForward-only result as a one-off run, stops listingtoRepoUpstreamas an atomicity helper, and fixes the stale sample output and exit-3 wording.Validation
On the tree of head 5ad4ce9, with TLC_WORKERS=8. The full
check.shandmutate.shruns came before the last edit, which changed only how--factlooks up its name.mutate.sh --modelran after it.check.shfull run:RESULT: PASS. LaneSchedule.cfg explored 2,694,082 distinct states, OtherWriters.cfg 14,198,464 and Liveness.cfg 255,510. All three probes failed as expected.mutate.sh:COUNT: 9/9 mutations failed check.sh as expected, andgit statusshowed only the uncommitted skill files afterwards.mutate.sh --model:COUNT: 9/9.LaneSchedule.cfgwithINVARIANTS NoLostForwardonly:DoneKeepsPendingFALSE andRetryRemarksFALSE each failedNoLostForward.check.sh --factrefuses a name facts.go does not have (exit 3) and a value other than FALSE (exit 3).check.sh,mutate.sh),scripts/check-doc-links.py, andcheck.sh --fingerprints-only(exit 0).No product code changes.
Refs #675
Generated with
xum• Model:anthropic:claude-opus-5-5• Thinking:high