Repository navigation
Build and test compatible release archives - #736
Conversation
Build x86_64 archives in the pinned Bookworm image and check their real glibc requirements. Consume the packed bytes before upload. Keep prebuilt on its existing token-only credential surface, scope strict credential scanning to prebuilt, and pin the archive consumer with negative controls. Intentionally replace the documentation introduced by c70e828 and the intermediate wording introduced by f637684. These are the named deletions and reverts in docs/ci.md, with their resulting policy: - c70e828: "Linux x64 `prebuilt` uses `gkp-16cpu-32gb-amd64-128gb`." The release path now uses the corresponding on-demand protected label. - c70e828: "The protected 2 CPU/4 GB set fits each orchestration job:" Release and notify-hub use the on-demand 4 CPU/8 GB set; promotion and the ruleset probe retain their stated protected routing. - c70e828: "Docs uses the 4 CPU/8 GB set for Doxygen and Graphviz over the full public header set before uploading the site to Pages." The replacement paragraph preserves that allocation and purpose. - c70e828: "The x86_64 prebuilt set reserves 16 CPU/32 GB and 128 GB disk for compiling, staging and packing the static library." The replacement keeps those resources and names the preloaded image. - c70e828: "Both Linux artifact cells install `libeigen3-dev` with `sudo apt-get update` and `sudo apt-get install -y libeigen3-dev`;" ARM installs the Ubuntu package; x86_64 uses the pinned Bookworm package. - c70e828: "Eigen is not baked into the protected image." The x86_64 Docker build uses the immutable image's pinned Eigen package, and both builds verify the consumed headers before CMake. - c70e828: "Before CMake, x86_64 must read `Eigen/src/Core/util/Macros.h` and match exactly" now applies to both builds with explicit Eigen3_DIR. - f637684: "ARM installs exactly `libeigen3-dev=3.4.0-4`; x86_64 checks that package in its image." The replacement distinguishes the Ubuntu ARM package from Bookworm's exact 3.4.0-4 package. - f637684: "Hosted exceptions cover PR light jobs; release uses protected GKE and post light jobs use bare scalar GKE names." The preserved summary and detailed release inventory state the resulting hosted exceptions, protected release routing, and bare post light jobs. - f637684: the release table's "`gkp-2cpu-4gb-amd64`; x86_64 `prebuilt`:" wording is replaced by the explicit on-demand release label inventory. This commit preserves the complete tested archive-publication tree while making every intentional documentation deletion or revert explicit.
| self.assertTrue({'test_version_policy_mutation_breaks_real_rejection_assertion', | ||
| 'test_isoc23_policy_mutation_breaks_real_rejection_assertion'} <= names) |
| import sys | ||
| import tarfile | ||
| import tempfile | ||
| import unittest |
| import subprocess | ||
| import sys | ||
| import tempfile | ||
| import unittest |
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 5 changed function(s) (1 sampled, not proven, 4 not verified).
Formal verification. PR-changed functions: 1/5 verified (0 proven, 1 may-equivalent, 0 distinguished) · 4 not verified (4 vacuous).
Not verified on this run: app\_token\_environment\_findings (vacuous: never exercised), check\_commands (vacuous: never exercised), main (vacuous: never exercised), runner\_findings (vacuous: never exercised).
Graphify review — findings
Adds a Bookworm-container build path for the x86_64 release prebuilt: build_prebuilt_bookworm.sh admits the preloaded toolchain image against its pinned digest, builds inside it, then runs in --consume mode on the packed tarball (sidecar checksum, unpack, native host run) before upload. The generic Configure/Build/Install steps now run only for linux-aarch64, with Eigen3_DIR pinned and FetchContent disabled, and ARM gets its own Eigen 3.4.0 header assertion, while the existing x86_64 Eigen assertion still reads host headers rather than the container's. Adds a glibc-floor check over every staged .a/.so in dry-run and publish, keeping raw checker output and its real exit code (setup errors included), and sets persist-credentials: false on the prebuilt checkout. Moves release and notify-hub to on-demand runners to avoid preemption after tag push, and extends preflight and its tests to pin the new steps, labels, shard matrices and the glibc checker.
Worth a look
- Docker image config ID is compared to the pinned repository digest —
scripts/build_prebuilt_bookworm.sh:101· Escalate · high- NOT verified (no proof, no reproducing execution) — needs human review
- Configure/Build/Install now skipped for every non-aarch64 triple, including non-Linux slices —
.github/workflows/release.yml:450· Escalate · high- NOT verified (no proof, no reproducing execution) — needs human review
- x86 Eigen check validates host headers after the artifact was built elsewhere —
.github/workflows/release.yml:411· 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 — 1540 functions depend on the 1519 functions this change touches.
Health — this change adds coupling hotspots:
- worse:
ci_workflow_findings()— 81 callers, 24 callees - worse:
check_commands()— 22 callers, 5 callees - worse:
_job_values()— 29 callers, 3 callees - worse:
_job_block()— 17 callers, 3 callees - worse:
runner_findings()— 2 callers, 25 callees - new:
release_prebuilt_workflow_findings()— 6 callers, 6 callees - worse:
_holds_credentials()— 3 callers, 7 callees - worse:
main()— 1 callers, 13 callees - …and 4 more — each is listed as a finding
Verification — 1540 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: 1540 function(s) in the blast radius were not formally verified this run
Docs that may be stale (advisory)
AGENTS.md§ What this repo is (lines 5-11): references changed symbolssourceAGENTS.md§ Build (lines 12-25): references changed symbolsgitAGENTS.md§ Layout (lines 26-41): references changed symbolssourceAGENTS.md§ Conventions (lines 103-116): references changed symbolssourceAGENTS.md§ Safety rules (lines 117-127): references changed symbolssourceCHANGELOG.md§ Unreleased (lines 8-135): references changed symbolscopyCHANGELOG.md§ 1.9.1 — 2026-10-31 (lines 136-258): references changed symbolsempty,sourceCHANGELOG.md§ Breaking for hosts (lines 803-842): references changed symbolscommandCHANGELOG.md§ State hashes (lines 1234-1299): references changed symbolsentry,sourceCHANGELOG.md§ 1.6.0 — 2026-10-17 (lines 1781-1946): references changed symbolsentry
…and 10 more.
Formal verification
No difference found (not proven): No behavior difference found in \_holds\_credentials (not a proof).
The verifier ran both versions of \_holds\_credentials 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 app\_token\_environment\_findings.
The verifier did not have enough to check app\_token\_environment\_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 check\_commands.
The verifier did not have enough to check check\_commands, 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 90 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)
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 1 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)
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
· 6 grounded finding(s) anchored inline below; 6 more finding(s) on lines outside this diff (see the check run).
| @@ -0,0 +1,421 @@ | |||
| #!/usr/bin/env bash | |||
There was a problem hiding this comment.
build_prebuilt_bookworm.sh script
fans out to 9 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| raise | ||
|
|
||
|
|
||
| def discover(root: Path, root_fd: int, issues: list[dict]) -> tuple[list[dict], dict]: |
There was a problem hiding this comment.
discover()
fans out to 8 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| **context, reference=reference) | ||
|
|
||
|
|
||
| def inspect_target(root_fd: int, target: dict, directories: dict, |
There was a problem hiding this comment.
inspect_target()
fans out to 12 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return row | ||
|
|
||
|
|
||
| def main(argv: list[str] | None = None) -> int: |
There was a problem hiding this comment.
main()
fans out to 8 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return False | ||
|
|
||
|
|
||
| def _holds_credentials(workflow: str, body: str, *, effective_permissions: bool = False, |
There was a problem hiding this comment.
_holds_credentials()
fans out to 7 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return [] | ||
|
|
||
|
|
||
| def release_prebuilt_workflow_findings(workflow: str) -> list[str]: |
There was a problem hiding this comment.
release_prebuilt_workflow_findings()
fans out to 6 callees (efferent coupling); 6 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
|
Review of bd1fa2f (one commit on main ace3079; it replaces #733, whose last head was 74d0476). GO WITH ONE CONDITION: Condition
What I checked
Smaller points (P3)
|
Build and check Linux release archives with a digest-pinned Bookworm toolchain. Before upload, verify and unpack the packed archive, then link and run the native kernel host against its full shipped library.
Apply strict secret-expression checks only to prebuilt; retain main's credential behavior for every other job. Keep prebuilt token-only with its existing matrix and runner pins, and pin the delegated archive-consumer source. Correct the environment inventory and isolated workflow fixtures.
Validation on this head: whole preflight504tests and whole release-gate289tests passed across eight shards each. Updated-head required CI, final review and the first real archive-consumer dry run remain pending.
🤖 Generated with Claude Code