Repository navigation
Separate release bump and tag admission with retained decision evidence - #789
luisleo526 wants to merge 17 commits into
Conversation
Exercise the version-only reset before tagging, preserving tagged behavior. Add refusal controls for parent count, extra paths, version direction, catalog bytes, existing tags and inherited release stamp constraints.
Require each release phase to use its own exact-commit CI evidence. Keep the bump untagged until its checks finish, then authenticate and tag that same commit. Validate the two-file transition and preserve catalog assets.
Record advisory verification and complete workflow attempt history, bind the decision to received response bytes, and refuse changed run metadata before admission. Keep release receipts on refusal and honor declared catalog paths.
Use timezone-aware UTC and keep exact output assertions aligned with each test input. Preserve every release safety condition and mutation control.
Cover authenticated advisory creators and first-attempt actor refusals. Reject malformed advisory states before logging them, retain sanitized unexpected-exception receipts, and distinguish invalid triggering actors from changed attempt metadata. Keep parity as the only required status.
There was a problem hiding this comment.
Graphify reviewed this change.
Worth a look — the grounded gate found no coupling regressions or blocking issues, but 3 advisory finding(s) below merit a look before merge.
Not checked: tests were not run; formal verification proved 0 of 20 changed function(s) (2 sampled, not proven, 16 not verified).
Formal verification. 2 change(s) alter behavior, breaking input(s) attached. PR-changed functions: 4/20 verified (0 proven, 2 may-equivalent, 2 distinguished) · 16 not verified (5 vacuous, 11 unsupported).
Behavior changes: release\_bump\_workflow\_findings changes behavior, here is the input that shows it.
The verifier found a concrete input on which release\_bump\_workflow\_findings behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"workflow":"'\\\\t\\\\n'"\}, the old code produced \['release\.yml must keep the exact two\-file release bump writer, commit and atomic push', 'release\.yml must keep the unconditional release gate with its release App token for the App\-only main pu… but the new code produces \['release\.yml must keep the exact two\-phase release writer, untagged bump push and same\-SHA tag retry', 'release\.yml must keep the unconditional release gate with its release App token for the A… (outputs first differ at character 41). Paste that input straight into a regression test.
Behavior changes: release\_prebuilt\_workflow\_findings changes behavior, here is the input that shows it.
The verifier found a concrete input on which release\_prebuilt\_workflow\_findings behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"workflow":"'\\\\t\\\\n'"\}, the old code produced \['release\.yml prebuilt must retain needs: release before build', 'release\.yml prebuilt must retain workflow permissions: contents: write', 'release\.yml prebuilt must retain job permissions: conte… but the new code produces \['release\.yml prebuilt must retain needs: release before build', 'release\.yml prebuilt must retain workflow permissions: contents: write', 'release\.yml prebuilt must retain job permissions: conte…. Paste that input straight into a regression test.
Not verified on this run: runner\_findings (vacuous: never exercised), \_ci\_post\_jobs (unsupported), \_ci\_post\_proof (unsupported), \_ci\_post\_runs (unsupported), \_phase\_one (unsupported), \_read\_json (unsupported), \_read\_text (unsupported), \_release\_bump (unsupported), \_require\_ci\_post (unsupported), \_require\_release\_push (unsupported), and 6 more.
Graphify review — findings
Splits the release workflow into two dispatch phases: bump gates the dispatch SHA, pushes only the VERSION/reset-diff commit to main and prints its SHA, and tag tags that same commit and cuts the release once the commit's own full post-merge CI has ended green. The gate now takes the phase and dispatch_sha, writes a receipt that is uploaded as an artifact even on failure, and a new plan subcommand in ci_release_gate.py replaces the inline tag-list and version computation. In the tag phase the catalog step takes its base tag from HEAD^ and re-stamps from an existing tag when refs/tags/<tag> is present locally, so retry and first-run stamping both depend on the bump commit's tree and on local refs; dry_run now rehearses whichever phase is chosen.
Worth a look
- Tag-phase first run stamps the catalog diff from the bump commit's reset tree —
.github/workflows/release.yml:234· Escalate · medium- NOT verified (no proof, no reproducing execution) — needs human review
- Tag-phase idempotency check uses local refs, so a rerun after a pushed tag fails —
.github/workflows/release.yml· Escalate · medium- NOT verified (no proof, no reproducing execution) — needs human review
- Bump commit pushed with GITHUB_TOKEN may never get the 'own full CI' that the tag phase waits for —
.github/workflows/release.yml· Escalate · medium- NOT verified (no proof, no reproducing execution) — needs human review
Review partial — this diff was larger than one review pass covers, so later files were not reviewed; some findings may be missing.
Analysis details — impact, health, verification
Impact & health
Graphify review
Impact — 1756 functions depend on the 1747 functions this change touches.
Health — this change adds coupling hotspots:
- worse:
ci_workflow_findings()— 90 callers, 24 callees - worse:
build_diff()— 8 callers, 8 callees - worse:
do_check()— 3 callers, 17 callees - worse:
do_stamp()— 2 callers, 20 callees - worse:
do_stamp_tags()— 2 callers, 13 callees - new:
validate_release_transition()— 2 callers, 12 callees - new:
_collect_attempts()— 2 callers, 9 callees - worse:
_phase_one()— 2 callers, 8 callees - …and 8 more — each is listed as a finding
Verification — 1756 functions in the blast radius were not formally verified this run (proofs are advisory here).
Gate & verification
graphify gate
PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.
Advisory (not blocking):
- verification_scope: 1756 function(s) in the blast radius were not formally verified this run
Docs that may be stale (advisory)
AGENTS.md§ Build (lines 12-25): references changed symbolsreceiptCHANGELOG.md§ Unreleased (lines 8-190): references changed symbolsinventoryCHANGELOG.md§ Report sink and scratch spill (lines 898-1109): references changed symbolsreceiptCHANGELOG.md§ run_json and CLI (lines 1110-1202): references changed symbolsreceiptCHANGELOG.md§ Run-failure codes ([#351]) (lines 2351-2441): references changed symbolsinputsCHANGELOG.md§ Migration (lines 2605-2641): references changed symbolsinputsCHANGELOG.md§ 1.3.0 — 2026-10-06 (lines 2642-2803): references changed symbolsreceiptCHANGELOG.md§ State hashes (lines 2804-2839): references changed symbolstagsCHANGELOG.md§ State hashes (lines 3082-3114): references changed symbolstagsCHANGELOG.md§ 1.1.0 — 2026-10-04 (lines 3160-3374): references changed symbolsattempts
…and 10 more.
Formal verification
Behavior changes: release\_bump\_workflow\_findings changes behavior, here is the input that shows it.
The verifier found a concrete input on which release\_bump\_workflow\_findings behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"workflow":"'\\\\t\\\\n'"\}, the old code produced \['release\.yml must keep the exact two\-file release bump writer, commit and atomic push', 'release\.yml must keep the unconditional release gate with its release App token for the App\-only main pu… but the new code produces \['release\.yml must keep the exact two\-phase release writer, untagged bump push and same\-SHA tag retry', 'release\.yml must keep the unconditional release gate with its release App token for the A… (outputs first differ at character 41). Paste that input straight into a regression test.
Behavior changes: release\_prebuilt\_workflow\_findings changes behavior, here is the input that shows it.
The verifier found a concrete input on which release\_prebuilt\_workflow\_findings behaves differently before and after the change. If that change is intended, ship it; if not, this is your bug.
Guarantee: This difference was REPRODUCED, the verifier actually ran both versions on that input and saw them disagree. It is real, not an artifact.
Evidence: On input \{"workflow":"'\\\\t\\\\n'"\}, the old code produced \['release\.yml prebuilt must retain needs: release before build', 'release\.yml prebuilt must retain workflow permissions: contents: write', 'release\.yml prebuilt must retain job permissions: conte… but the new code produces \['release\.yml prebuilt must retain needs: release before build', 'release\.yml prebuilt must retain workflow permissions: contents: write', 'release\.yml prebuilt must retain job permissions: conte…. Paste that input straight into a regression test.
Could not verify: Could not verify runner\_findings.
The verifier did not have enough to check runner\_findings, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: non-vacuity: domain too small (only 2 distinct inputs exercised, need 3) — 'no divergence' would be near-vacuous
Could not verify: Could not verify \_ci\_post\_jobs.
The verifier did not have enough to check \_ci\_post\_jobs, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `api` is annotated `API` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_ci\_post\_proof.
The verifier did not have enough to check \_ci\_post\_proof, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `history` is annotated `History` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_ci\_post\_runs.
The verifier did not have enough to check \_ci\_post\_runs, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `api` is annotated `API` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_phase\_one.
The verifier did not have enough to check \_phase\_one, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `api` is annotated `API` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_read\_json.
The verifier did not have enough to check \_read\_json, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `api` is annotated `API` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_read\_text.
The verifier did not have enough to check \_read\_text, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `api` is annotated `API` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_release\_bump.
The verifier did not have enough to check \_release\_bump, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `api` is annotated `API` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_require\_ci\_post.
The verifier did not have enough to check \_require\_ci\_post, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `api` is annotated `API` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_require\_release\_push.
The verifier did not have enough to check \_require\_release\_push, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `api` is annotated `API` — outside the synthesizable primitive/collection set
Could not verify: Could not verify gate.
The verifier did not have enough to check gate, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 83 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly TypeError — names the real obstacle, not a sampling gap)
Could not verify: Could not verify gh\_api.
The verifier did not have enough to check gh\_api, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 41 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly FileNotFoundError — names the real obstacle, not a sampling gap)
Could not verify: Could not verify main.
The verifier did not have enough to check main, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 73 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly TypeError — names the real obstacle, not a sampling gap)
No difference found (not proven): No behavior difference found in \_\_init\_\_ (not a proof).
The verifier ran both versions of \_\_init\_\_ on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.
Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.
Note: An input the sampler did not try could still differ.
No difference found (not proven): No behavior difference found in \_run (not a proof).
The verifier ran both versions of \_run on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.
Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.
Note: An input the sampler did not try could still differ.
Could not verify: Could not verify do\_check.
The verifier did not have enough to check do\_check, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `cfg` is annotated `Config` — outside the synthesizable primitive/collection set
Could not verify: Could not verify do\_stamp.
The verifier did not have enough to check do\_stamp, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `cfg` is annotated `Config` — outside the synthesizable primitive/collection set
Could not verify: Could not verify newest\_tag.
The verifier did not have enough to check newest\_tag, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 3 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly NameError — names the real obstacle, not a sampling gap)
· 11 grounded finding(s) anchored inline below; 5 more finding(s) on lines outside this diff (see the check run).
| _fields(run, ("created_at", "updated_at", "run_started_at", "html_url"))) | ||
|
|
||
|
|
||
| def _observe_run(api: API, repo: str, run: dict, record: dict) -> None: |
There was a problem hiding this comment.
_observe_run()
fans out to 6 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| validation["outcome"] = "pending" | ||
|
|
||
|
|
||
| def _revalidate_runs(api: _GateReads) -> None: |
There was a problem hiding this comment.
_revalidate_runs()
fans out to 6 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return {"source": endpoint, "login": trigger, "permission": permission["permission"]} | ||
|
|
||
|
|
||
| def _collect_attempts(api: API, repo: str, run: dict, record: dict, *, |
There was a problem hiding this comment.
_collect_attempts()
fans out to 9 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
|
|
||
| def _release_bump(api: API, repo: str, sha: str) -> str: | ||
| _require_release_push(api, repo, sha) | ||
| def _release_bump(api: API, repo: str, sha: str, *, expected_parent: str | None = None, |
There was a problem hiding this comment.
_release_bump()
fans out to 10 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| def _require_ci_post(api: API, repo: str, sha: str, history: History) -> str: | ||
| proof, docs_skipped = _ci_post_proof(sha, history) | ||
| for docs_sha in docs_skipped: | ||
| def _require_ci_post(api: API, repo: str, sha: str, history: History, *, |
There was a problem hiding this comment.
_require_ci_post()
fans out to 11 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| "previous": release_version.previous_tag(parsed, release_version.parse_tags(tags))} | ||
|
|
||
|
|
||
| def _phase_one(api: API, repo: str, sha: str, *, allow_missing_pr: bool = False, |
There was a problem hiding this comment.
_phase_one()
fans out to 8 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
|
|
||
|
|
||
| def do_check(cfg: Config, git, require_tags: str | None = None) -> Outcome: | ||
| def do_check(cfg: Config, git, require_tags: str | None = None, *, |
There was a problem hiding this comment.
do_check()
fans out to 17 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return data | ||
|
|
||
|
|
||
| def release_stamp_diffs(cfg: Config, git, new_bytes: bytes, diff: dict, |
There was a problem hiding this comment.
release_stamp_diffs()
fans out to 7 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return diffs | ||
|
|
||
|
|
||
| def validate_release_transition(cfg: Config, git, *, expected_parent: str | None = None, |
There was a problem hiding this comment.
validate_release_transition()
fans out to 12 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return parent, version | ||
|
|
||
|
|
||
| def stamp_findings(diffs: list, to_version: str) -> list: |
There was a problem hiding this comment.
stamp_findings()
high coupling complexity (Ca·Ce = 15).
Grounded coupling-delta finding (deterministic), not an LLM guess.
Carry both strict admission forms in the hosted release workflow, retaining caller identity, artifact custody and exact-commit release evidence.
Keep historical matrix inputs independent from the phased release workflow and require both phase and dry-run boundaries on downstream publishing jobs.
Choose the expected guard and message from the complete dispatch declaration, while retaining strict workflow acceptance and both dry-run boundaries.
…hosted jobs WorkflowPinTests reads the #768 matrix rebuild of release.yml for its hosted-matrix contracts. That rebuild keeps the shipped two-phase release job, a combination the validator correctly refuses, and its single prebuilt job has no tag-phase guard. Four checks therefore failed. They now read the shipped workflow: - test_two_release_phases_stop_before_publication_until_tag_phase pins the exact job-level tag-phase if: of prebuilt-x86, prebuilt-arm and upload, and the closed job list. The notify-hub, gate, step-condition and writer pins are unchanged. - test_prebuilt_requires_release_success_without_failure_bypasses holds the release-success pin for the release job, both build jobs and the publishing upload job: needs: release on each build job, upload's exact needs: [release, prebuilt-x86, prebuilt-arm], no always(), !cancelled() or continue-on-error: outside comments, and no release_bump_workflow_findings. - test_prebuilt_failure_bypass_mutations_are_refused, both subtests, inserts each bypass into each build job and into upload and requires the same refusal. Each of those jobs first passes with the shipped "no continue-on-error" comment in it, so the pin is still shown to read keys, not words. The validator compares every split job header, so the pin now scans the build jobs and upload before the release job, and a refusal names its job and bypass. The other WorkflowPinTests tests keep reading the matrix rebuild. Co-Authored-By: Claude Opus 5.5 <[email protected]>
| 'release.yml job prebuilt-x86 must not receive the protected release ' | ||
| 'environment or release credentials', |
| 'release.yml must keep the exact two-phase release writer, ' | ||
| 'untagged bump push and same-SHA tag retry', |
| 'release.yml must keep the unconditional release gate with its release ' | ||
| 'App token for the App-only main pull_request barrier', |
| 'release.yml must always retain the exact release gate receipt artifact ' | ||
| 'before planning or publishing', |
| 'release.yml job prebuilt-x86 must not receive the protected release ' | ||
| 'environment or release credentials', |
| 'release.yml must keep the exact two-phase release writer, ' | ||
| 'untagged bump push and same-SHA tag retry', |
| 'release.yml must keep the unconditional release gate with its release ' | ||
| 'App token for the App-only main pull_request barrier', |
| 'release.yml must always retain the exact release gate receipt artifact ' | ||
| 'before planning or publishing', |
| 'release.yml must keep the exact two-phase release writer, ' | ||
| 'untagged bump push and same-SHA tag retry', |
| 'release.yml must keep the unconditional release gate ' | ||
| 'with its release App token for the App-only main pull_request barrier', |
Preserve phase-aware release admission while incorporating the current main toolchain contract. Keep both Eigen flag constants and the mode parameter, and update the planned-phase fixture to the typed PATH flag. Co-Authored-By: Codex <[email protected]>
Retain the tagged VERSION and catalog baseline before exact-head validation. Co-Authored-By: Codex <[email protected]>
|
Superseded by #818 (same change, rebuilt on the 1.11.1 train branch). |
Release admission separates version bumping from tagging and retains the evidence behind each decision. The bump phase pushes only the untagged VERSION/catalog-reset commit. After that commit's own CI completes, the tag phase validates its checked parent and publishes that same commit without another bump. Dry runs retain admission checks and publish nothing.
This revision combines the phase split with the hosted toolchain release builds on main. It retains caller identity, artifact custody, exact-commit release evidence and both strict admission forms. Every downstream publishing job requires the tag-phase and dry-run boundaries. Release-control tests distinguish the historical legacy, split hosted and phase-planned workflow forms.
The release gate requires
pineforge/parity. The existingpineforge/verifyproducer remains in place; its authenticated state or absence is printed and retained as advisory. ci-post verification profiles remain separate evidence and cannot supply a missing status.The guard retains rerun history, requires the original App push and authenticated maintainer rerun permissions, rejects red or duplicate proving jobs and incomplete history, and preserves the established docs-only classification. Relied-on run identities are read again uncached before admission. Refusals, unexpected exceptions and receipt-write failures remain nonzero. The always-run upload retains sanitized decision evidence; malformed advisory states are refused before entering an Actions output line.
Validation ran natively on linux/arm64 on parent commit 5262f98 (tree 48f64509). The head differs from it by one comment line in scripts/test_ci_release_gate.py, whose syntax tree is identical. These native receipts remain bound to the parent tree:
UNPROVEN_HOSTEDskip. That check requires execution on the final pull-request head in GitHub Actions; the native skip supplies no hosted proof.The differential replay of the fixed release-gate corpus remains open. Hosted workflow execution, asset uploads and parity are separate from this native guard/control validation. A changed candidate tree requires new evidence.
Existing merge-gate references in AGENTS.md, docs/ci.md and docs/reference/merge-gate-and-promotion.md still describe verification as required and remain a separate documentation follow-up. The release-admission sections are updated here. The existing ARM tarball retry branch, including
--clobber, remains unchanged; its overwrite semantics and missing retry coverage remain an explicit follow-up. The tag phase also re-uploads catalog JSON assets with--clobberwhen the release already exists, so that a re-run completes; its overwrite semantics are part of the same follow-up.🤖 Generated with Claude Code