diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 0a18a03b4c..7f3c012504 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -2,6 +2,16 @@ ## Current selected-family replay +The selected #543 + #626 composition uses `.github/workflows/frontier626.yml`. +Its [completed Linux run](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/38317651752) +passed on 2026-10-13 at commit `ed49217ad6244f1d3bfe4588f122fa861849739c`. +The [preserved artifact reconciliation](../research/selected626-linux-reconciliation/README.md) +checks source equality to the sprint base, all six replay stages and exact +mathematical assembly agreement, with explicit limits for omitted payloads. +The older queued integration receipt is retained as historical evidence. + +## Historical selected-family replay through #588 + `.github/workflows/frontier588.yml` provides one complete cold check of #543 with #588 on Ubuntu 24.04 and Python 3.12. It installs NumPy, SymPy, SciPy, C++17 and Boost, checks the selected record and review evidence, rebuilds both diff --git a/docs/research/current-status.md b/docs/research/current-status.md index 630009d642..d439290771 100644 --- a/docs/research/current-status.md +++ b/docs/research/current-status.md @@ -5,6 +5,12 @@ See the [review](community-k492-review.md), [integration receipt](community-k492 [selected record](../../certificates/selected-result.json) and [PR ledger](pr-ledger.md). Public cold replay: `make frontier626-verify`. +The previously queued #626 Linux run completed successfully on 2026-10-13. +The [preserved evidence and offline checker](../../research/selected626-linux-reconciliation/README.md) +bind that run to its tested sources, six replay stages and exact assembly. +Three generated provenance digests differ from the committed assembly; the +linked reconciliation records their scope and the unavailable payloads. + The frozen round covers #618–#626. Eight scoped reviews complete; #620 remains partial pending portable research replays and validation of its solver/barrier claims. Earlier open reviews retain their ledger status. Inherited uniform, diff --git a/research/selected626-linux-reconciliation/CLAIM.md b/research/selected626-linux-reconciliation/CLAIM.md new file mode 100644 index 0000000000..8af7324759 --- /dev/null +++ b/research/selected626-linux-reconciliation/CLAIM.md @@ -0,0 +1,38 @@ +# Sprint claim + +- Track: research consolidation; OS-random assignment seed **95** (`secrets.randbelow(100)`). +- Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Object: the pending/queued Linux status in the selected #626 integration receipt, + for run `38317651752` at `ed49217ad6244f1d3bfe4588f122fa861849739c`. +- Method: inspect that exact completed run and its artifact; check all orchestrator + stages, log digests, exact composition and tested-source equality to the base. +- Deliverable: a preserved, offline-checkable provenance receipt with rejection + controls and a narrowly scoped current-status correction. No new kappa claim. +- Claim time: 2026-10-13 04:08 UTC. Expected finish: 04:30 UTC; final quarter + reserved for verification and handoff. +- Coordination: GitHub's pinned-issue list is empty, Discussions is disabled, + and the only open non-PR issue is #650 asking for Discussions. No reservation + issue was opened. Open PR titles and #675's body were checked for overlap. +- Candidates considered: (1) selected source-manifest completeness; + (2) #620 partial-review status versus predecessor attribution; + (3) queued-versus-completed #626 Linux evidence. Seed `95 % 3 = 2` selects + the third candidate after the overlap screen. The first two already have + explicit coverage in the selected checker/review; the third has a concrete + newly completed result to reconcile. + +Prepared by Josh Snider (`jsnider3`) with substantial OpenAI Codex assistance. +Apache-2.0. This claim is local because no sprint coordination issue exists. + +## Result — 2026-10-13 04:21 UTC + +Submitted [PR #695](https://github.com/CrocSwap/integer-mult-bounds/pull/695): +preserved the completed Linux evidence and checked 39 source objects, six replay +stages, 64 complex receipt substeps and 47 positive assembly margins. All 16 +rejection controls passed, including normal/optimized isolated runs from a +separate committed-files-only worktree. Selected-record and ledger checks passed. +The three differing generated provenance digests and unavailable CI payloads +are documented explicitly; no new kappa or full theorem is claimed. + +Final overlap check through #693 found no matching run reconciliation; upstream +main remained at the recorded base. No pinned sprint issue was available, so +this is the single local claim update with the result and handoff link. diff --git a/research/selected626-linux-reconciliation/EXPECTED.json b/research/selected626-linux-reconciliation/EXPECTED.json new file mode 100644 index 0000000000..d3c578df6b --- /dev/null +++ b/research/selected626-linux-reconciliation/EXPECTED.json @@ -0,0 +1,114 @@ +{ + "evidence_sha256": { + "artifact.zip": "1f1ad114e311f75d25fd6500db7ef0b8e15a4814aebc5c1edb01ec9288480355", + "artifacts.json": "d70261bfc7af4a9129ed5e2528fb039c72099110604d5ffa1ccb0832f070f379", + "jobs.json": "8b18b198ff47192f2e1bc76a79f14915440ae6e56bc5ad9f0833418e949e85c6", + "run.json": "6f963a2553e3e429da119f6b84294f90c565f592166f79cf0a63f3aa5659f626", + "workflow.log.gz": "0002ce6ad55392dcd4c4ac3f96635affff4169dfa0e5367a2d43c350fb8bb2c9" + }, + "workflow_steps": [ + "Set up job", + "Run actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1", + "Run actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97", + "Install verification dependencies", + "Check selected record and review evidence", + "Cold finite replay and exact composition binding", + "Require committed files unchanged", + "Run actions/upload-artifact@v4", + "Post Run actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97", + "Post Run actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1", + "Complete job" + ], + "complex_steps": [ + "actual-recompression-and-rebound-controls", + "admission-controls", + "bind-providers", + "ck-all-columns-native-frames", + "ck-all-phase-edges", + "ck-both-reflected-ledgers", + "ck-independent-local-controls", + "ck-normalized-wrappers", + "ck-step0-port_stage-construction", + "ck-step0-port_stage-native-audit", + "ck-step1-port_stage-construction", + "ck-step1-port_stage-native-audit", + "ck-step2-port_stage-construction", + "ck-step2-port_stage-native-audit", + "ck-step3-port_stage-construction", + "ck-step3-port_stage-native-audit", + "ck-step4-port_stage-construction", + "ck-step4-port_stage-native-audit", + "ck-step5-frame_regroup-construction", + "ck-step6-hyperplane_end-construction", + "ck-step6-hyperplane_end-controls", + "ck-step7-cold_end-construction", + "ck-step7-cold_end-controls", + "ck_504-step0-greedy_kernels-construction", + "ck_504-step0-greedy_kernels-omissions", + "ck_504-step1-frame_coalesce-construction", + "ck_504-step2-gate_move_coalesce-construction", + "conservative-and-native-exact-assembly", + "emit-controller", + "fresh-invoice", + "frozen558-full-replay", + "independent-controller-and-controls", + "jp8-all-columns-native-frames", + "jp8-all-phase-edges", + "jp8-base-k_triangle-construction", + "jp8-both-reflected-ledgers", + "jp8-independent-local-controls", + "jp8-normalized-wrappers", + "jp8-step0-port_stage-construction", + "jp8-step0-port_stage-native-audit", + "jp8-step1-port_stage-construction", + "jp8-step1-port_stage-native-audit", + "jp8-step2-port_stage-construction", + "jp8-step2-port_stage-native-audit", + "jp8-step3-port_stage-construction", + "jp8-step3-port_stage-native-audit", + "jp8-step4-frame_regroup-construction", + "jp8-step5-hyperplane_end-construction", + "jp8-step5-hyperplane_end-controls", + "jp8-step6-cold_end-construction", + "jp8-step6-cold_end-controls", + "jp8_504-step0-cold_kernel-construction", + "jp8_504-step0-cold_kernel-omissions", + "jp8_504-step1-multicut-construction", + "jp8_504-step1-multicut-omissions", + "jp8_504-step2-frozen558_scalar_audits-rank5", + "jp8_504-step2-frozen558_scalar_audits-static44", + "jp8_504-step3-joint_prefix-all-kernel-omissions", + "jp8_504-step3-joint_prefix-construction", + "jp8_504-step3-joint_prefix-independent-joint-prefix-and-coverage", + "jp8_504-step3-joint_prefix-rank5-omissions", + "k-triangle-control-empty-schedule", + "k-triangle-control-pr531-construct504", + "phase-timing-portability-controls" + ], + "assembly_digest_differences": [ + { + "path": [ + "template_sha256" + ], + "linux": "8aac9a65fe3b15889a0cdbc125bd80ab0e141578efccd25a7d338fd5ee3aae6e", + "committed": "22b41c45fdac1dcc7495311fe701f4697219654843558785ed72fae91df531b0" + }, + { + "path": [ + "input_sha256", + "owner_audit" + ], + "linux": "1de45f6b911f8ef6f9c134a1eaf1e1f03feac808e048f896c1099b121c061ce9", + "committed": "ec7bc4157e7ab1707bddf99994149c932b51365de7e742508fd182051ca57fc1" + }, + { + "path": [ + "input_sha256", + "fresh_invoice" + ], + "linux": "2219b0c60373d93f256ff255ce6de2af1605b4c61c18f45cb189f788c5bb5d96", + "committed": "367a73f744ea9b7dd6cca5fa3fda47175f560aa3d37e708c9fa1294dbd4b56eb" + } + ], + "workflow_log_sha256": "fbdc929e9bbf4ba9afb050b4c74f51322499dd388be3c861ff51a5754b39ebba" +} diff --git a/research/selected626-linux-reconciliation/README.md b/research/selected626-linux-reconciliation/README.md new file mode 100644 index 0000000000..a3a771094e --- /dev/null +++ b/research/selected626-linux-reconciliation/README.md @@ -0,0 +1,126 @@ +# Selected #626 Linux evidence reconciliation + +The published #626 integration receipt records run **38317651752** as queued. +That exact run completed successfully on **2026-10-13 at 02:10:06 UTC**. +This package preserves its artifact and checks the evidence linking that +execution to the selected #543 + #626 composition. Status: **research +consolidation / provenance verification; no new kappa**. + +The conditional result remains exactly +`51110230636731/31250000000000000 = 0.001635527380375392`. +The earlier queued receipt remains an unchanged historical snapshot. + +## Reproduce + +From a clone containing the two commits below, using Python 3.11+ and Git: + +```sh +python3 -I -B research/selected626-linux-reconciliation/verify.py +``` + +Expected: + +```text +PASS_PR626_LINUX_RECONCILIATION 6 stages, 64 substeps, 47 strict margins, 16 rejection controls +``` + +No network, third-party Python package, compilation, or supplier rerun is needed. +`--out /tmp/pr626-linux-report.json` writes the deterministic report. +The same command also works with `-O`; rejection checks use explicit exceptions. +A shallow clone must fetch the pinned commits first. This is an evidence check, +not a fresh execution of the supplier pipeline; that remains `make frontier626-verify`. + +## Exact evidence and source scope + +| Object | Pin | +|---|---| +| Sprint base | `66849e1475c930fd7732b1a0067ffee7e1e95f60` | +| Tested CI commit | `ed49217ad6244f1d3bfe4588f122fa861849739c` | +| Run, attempt | [38317651752](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/38317651752), attempt 1 | +| Job | [115038013572](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/38317651752/job/115038013572) | +| Artifact | `11784169747`, `frontier626-linux-python312` | +| Original ZIP SHA-256 | `1f1ad114e311f75d25fd6500db7ef0b8e15a4814aebc5c1edb01ec9288480355` | +| Selected #626 source | `660de893d27bb7abd1d5b01b1640207528a5c851` | +| Retained #543 source | `2065fe4f72a914d907f1046603f5a36f17018535` | + +`evidence/` retains the original ZIP, run metadata (selected API fields), full +job/artifact metadata, and losslessly compressed `gh run view --log` output. +`EXPECTED.json` also pins the decompressed log bytes. It pins those evidence +bytes, all workflow step names, all 64 complex receipt substeps, and the three +assembly digest differences. The ZIP hash matches GitHub's artifact metadata; +its bytes are an immutable downloaded input, not a regenerated container. + +`SOURCE-PINS.json` records Git object IDs. The checker independently queries +both commits and requires 39 identical objects for every selected package root, +all proof supplements, the complete `scripts/` tree, the workflow, Makefile, +selected record, source manifest, and selected assembly. It derives this coverage +from the selected record rather than accepting an arbitrary shortened list. +It also binds the complex receipt's package/spec and six dependency-manifest +SHA-256 values to the base's bytes. The intervening publication/ledger edits +are outside this source-equivalence claim. + +The archived run reports Ubuntu 24.04.5, image `20261004.327.1`, Python 3.12.15, +NumPy 2.5.4, SymPy 1.14.0, SciPy 1.18.1 and mpmath 1.3.0. The workflow installs +dependencies without version pins; these are observed versions from the log, +not a claim that a future installation will reproduce that environment. + +## What agrees, and what remains unavailable + +All six orchestrator stages have exit code zero and retained logs matching +their SHA-256 values: bit543, declarations, complex626, independent-owner, +helper-interface, and bindings. The complex receipt lists 64 successful +substeps; its result explicitly reports no baseline or local-output reuse. +The composition links to the exact archived complex receipt and assembly. + +Every assembly JSON field agrees with the committed certificate except these +three explicitly recorded paths: + +- `template_sha256` +- `input_sha256.owner_audit` +- `input_sha256.fresh_invoice` + +In particular, the paid profiles, moment intervals, source-engine hashes, +supplier endpoints, bootstrap data, controls, and all 47 strict outer margins +agree exactly. The checker additionally evaluates all 47 rational margins as +positive. The two source-engine/margin mutation controls update receipt links +consistently, so rejection tests mathematical-field comparison rather than +merely noticing a stale file hash. + +The workflow did **not** upload the generated template, owner audit, invoice, +all 64 substep logs, or separate `OWNER-CHECK.json`/`INTERFACE.json`. Their +execution is supported by the retained stage logs and receipts, but this package +cannot independently compare those omitted payloads or explain the three byte +digest differences. It does not assert that those differences are only gzip +metadata. The source already includes recompression controls; their recorded +success is evidence of execution, not a replacement for the missing payloads. + +Negative controls reject wrong heads/attempts, queued runs, skipped workflow +steps, detached artifacts, missing/failed replay stages, changed logs, broken +receipt links, wrong kappa, changed positive margins, altered engine hashes, +unrecorded provenance differences, and changed tested source objects. + +This is an offline consistency check of preserved GitHub evidence, not a signed +attestation or an independent mathematical reimplementation. It confirms one +completed run at a pinned source state. It does not establish other platforms, +newer PRs, optimality, or a full multiplication theorem. The selected review's +all-size compiler, common-label/mutable-basis, pooled hosting, residual, +precision/tape/recovery and analytic assumptions remain. + +## Attribution and sprint record + +Douglas Colkitt supplied the selected review, replay orchestration and CI. +Chafik Boukhalfa supplied #626's owner repair; Jeremy Kothe supplied #622/#623's +construction; eumemic supplied #543's bit supplier. GamingPuzzled's #620 lead +and the preceding supplier, recurrence and verification contributors retain +the attribution in the selected review and package notices. PR #675's +independent owner-boundary audit is distinct from this CI provenance check. + +Consolidation by Josh Snider (`jsnider3`) with substantial OpenAI Codex assistance. +Apache-2.0; this is not independent human peer review. [CLAIM.md](CLAIM.md) +records OS-random seed 95, candidates, scope and coordination checks. + +Local validation: normal and optimized isolated Python runs produced identical +reports; all 16 rejection controls passed. `make selected-record-check`, +`python3 -B scripts/verify_pr_reconciliation.py`, and `git diff --check` passed. +The selected suppliers were not rebuilt locally because this change reconciles +the already completed, preserved CI execution and changes no construction. diff --git a/research/selected626-linux-reconciliation/RESULT.json b/research/selected626-linux-reconciliation/RESULT.json new file mode 100644 index 0000000000..62051d8342 --- /dev/null +++ b/research/selected626-linux-reconciliation/RESULT.json @@ -0,0 +1,54 @@ +{ + "status": "PASS_PR626_LINUX_RECONCILIATION", + "run": 38317651752, + "ci_head": "ed49217ad6244f1d3bfe4588f122fa861849739c", + "base": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "kappa": "51110230636731/31250000000000000", + "replay_stages": 6, + "complex_substeps": 64, + "strict_assembly_margins": 47, + "assembly_digest_differences": [ + { + "path": [ + "template_sha256" + ], + "linux": "8aac9a65fe3b15889a0cdbc125bd80ab0e141578efccd25a7d338fd5ee3aae6e", + "committed": "22b41c45fdac1dcc7495311fe701f4697219654843558785ed72fae91df531b0" + }, + { + "path": [ + "input_sha256", + "owner_audit" + ], + "linux": "1de45f6b911f8ef6f9c134a1eaf1e1f03feac808e048f896c1099b121c061ce9", + "committed": "ec7bc4157e7ab1707bddf99994149c932b51365de7e742508fd182051ca57fc1" + }, + { + "path": [ + "input_sha256", + "fresh_invoice" + ], + "linux": "2219b0c60373d93f256ff255ce6de2af1605b4c61c18f45cb189f788c5bb5d96", + "committed": "367a73f744ea9b7dd6cca5fa3fda47175f560aa3d37e708c9fa1294dbd4b56eb" + } + ], + "source_objects_matched": 39, + "negative_controls": [ + "wrong_ci_head", + "wrong_attempt", + "queued_run", + "skipped_workflow_step", + "artifact_other_run", + "artifact_bad_digest", + "missing_helper_log", + "corrupt_owner_log", + "missing_helper_stage", + "failed_bit_stage", + "wrong_kappa", + "broken_receipt_link", + "changed_positive_margin", + "changed_source_engine_digest", + "changed_recorded_digest_difference", + "changed_tested_source" + ] +} diff --git a/research/selected626-linux-reconciliation/SOURCE-PINS.json b/research/selected626-linux-reconciliation/SOURCE-PINS.json new file mode 100644 index 0000000000..4cb8c2b349 --- /dev/null +++ b/research/selected626-linux-reconciliation/SOURCE-PINS.json @@ -0,0 +1,41 @@ +{ + ".github/workflows/frontier626.yml": "4e4ee39e73ffc5e4608f9734bab0a12f96510690", + "Makefile": "9d4d7808d26869d7b0d228bd92cffbc5697eb838", + "certificates/selected-result.json": "92a10096dee76479af88a897714b3818d8263141", + "docs/research/community-cold617-review.md": "ca1e7d4f971db844129b5c1bbd34373a71c3e673", + "docs/research/community-hyperplane599-review.md": "cc25932a93aa16c57f7d0255414bafe16eb71aa5", + "docs/research/community-k492-review.md": "11efcd07ae2b9d93d355c6adaf773dca70dbce91", + "research/community-k492-audit/SELECTED-SOURCE.json": "5f8725175afc095ff2da92e38af6ef4476c266da", + "research/community-k492-audit/pr626/replay/ASSEMBLY.json": "2e97b75bd8e74e8aa1b5fb83adcdc461aa07c398", + "research/complex-571-cold14-b3": "cffdf1744c6b4fc690ce5284f5ee92993d861064", + "research/complex-571-cold14-b3/PROOF-NOTE.md": "ee93419b8cf8da08bf8ff678a1d2f1a7f3011158", + "research/complex-571-cold14-b3/README.md": "a3d037b2b0135525c94f2ba7f4774424cc9931c4", + "research/complex-571-free4fc8/NOTICE.md": "78715c83efbb15294f83fb9f5436e0e091b4e554", + "research/complex-571-hpeq5/README.md": "806aafc1431738b7607213ad2b29ff49269b159e", + "research/complex-joint-prefix": "b50b62dfc181f1a395576963c5a5ce2ed8b820b5", + "research/complex-joint-prefix/proof/CONSTRUCTION.md": "b037060c014255431d7d74ba96e554b3fb1c5e18", + "research/complex-k492-owner-repair": "0bec96ae6a8c58535dab09bc6f01fa775412d91f", + "research/complex-k492-owner-repair/PROOF-NOTE-R.md": "a403cbeb77ea8b8187de6942ea5f74ca10e9c159", + "research/complex-k492-owner-repair/PROOF-NOTE.md": "0586ac5422f867035187cd55ed42c030b3d3b4b4", + "research/complex-k492-owner-repair/README.md": "58722c1a496f0c806e77c9d762eb00b0c53254f0", + "research/complex-multicold": "816cd09153701ba86aa9b70b88144f3db369dfb3", + "research/complex-multicold/proof/CONSTRUCTION.md": "1d4b6d6c17000f472108f2f62f834df5e4dee4de", + "research/complex-multicold/vendor/pr559/PROOF.md": "9adf304048b62c6db9250a611a8d4b0b60ed8276", + "research/direct-delivery504-global": "3c778f14be29a3ca3a30b478191d5b6406cc4591", + "research/e8-bit-carrier-skeleton": "0074582e358b1082d2f6f2a1d014b639284da1a7", + "research/e8-bit-r420": "d420f76f9ddfede0cd2fdfd690404e97081ce804", + "research/e8-bit-r420/README.md": "6751eba6f617292fc919e58d5a9f9f06ab037391", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean": "1af33a206a9ba6c4826b3a1516d104e770380869", + "research/hyperplane-end-lean/PROOF.md": "a94a2ac168c088a1282ea411766bc859178620df", + "research/kernel-frame-coalescing": "528aa1f0d5c7b355269228b33594976e70499832", + "research/kernel-frame-coalescing/PROOF.md": "d23ad096f7d3028981d46d31106318d2d5ec6ad3", + "research/promoted-kernel-coalescing/vendor/larger_gain": "3fc145ff30ab32534d805a5aa69b5746614b3eb7", + "research/structural-gain": "560627015ba5bca60900e54b7c8e0c072a40f1ef", + "research/structural-gain/frontier-composition/README.md": "45614683acf25bd2f1b664bb208d59a9305f58e4", + "scripts": "b5723e7ac6d178ee38dd9d1a1eff1491f3f57f67", + "scripts/verify_cold617_interface.py": "7892bf352d94f6835e5897ea8c7c982a9b096696", + "scripts/verify_frontier588_bindings.py": "8889873f431bb41fbc9b776bec7596875179cbec", + "scripts/verify_frontier626.py": "d7a9a290b8de66da0a32ffd43b741af90305ac28", + "scripts/verify_frontier626_bindings.py": "1e51d5313015620eaa4963d906f915ca9dfb6dcc", + "scripts/verify_hpe_lean_binding.py": "d295b028edc531dfbfaa023370a9528bada35572" +} diff --git a/research/selected626-linux-reconciliation/evidence/artifact.zip b/research/selected626-linux-reconciliation/evidence/artifact.zip new file mode 100644 index 0000000000..cab6ed9eb2 Binary files /dev/null and b/research/selected626-linux-reconciliation/evidence/artifact.zip differ diff --git a/research/selected626-linux-reconciliation/evidence/artifacts.json b/research/selected626-linux-reconciliation/evidence/artifacts.json new file mode 100644 index 0000000000..1eae176595 --- /dev/null +++ b/research/selected626-linux-reconciliation/evidence/artifacts.json @@ -0,0 +1 @@ +{"total_count":1,"artifacts":[{"id":11784169747,"node_id":"MDg6QXJ0aWZhY3QxMTc4NDE2OTc0Nw==","name":"frontier626-linux-python312","size_in_bytes":35904,"url":"https://api.github.com/repos/CrocSwap/integer-mult-bounds/actions/artifacts/11784169747","archive_download_url":"https://api.github.com/repos/CrocSwap/integer-mult-bounds/actions/artifacts/11784169747/zip","expired":false,"digest":"sha256:1f1ad114e311f75d25fd6500db7ef0b8e15a4814aebc5c1edb01ec9288480355","created_at":"2026-10-13T02:10:03Z","updated_at":"2026-10-13T02:10:03Z","expires_at":"2027-01-10T22:36:47Z","workflow_run":{"id":38317651752,"repository_id":1408136434,"head_repository_id":1408136434,"head_branch":"main","head_sha":"ed49217ad6244f1d3bfe4588f122fa861849739c"}}]} \ No newline at end of file diff --git a/research/selected626-linux-reconciliation/evidence/jobs.json b/research/selected626-linux-reconciliation/evidence/jobs.json new file mode 100644 index 0000000000..f4c6c43a08 --- /dev/null +++ b/research/selected626-linux-reconciliation/evidence/jobs.json @@ -0,0 +1 @@ +{"total_count":1,"jobs":[{"id":115038013572,"run_id":38317651752,"workflow_name":"Selected family 626 finite composition","head_branch":"main","run_url":"https://api.github.com/repos/CrocSwap/integer-mult-bounds/actions/runs/38317651752","run_attempt":1,"node_id":"CR_kwDOU-508s8AAAAayMzIhA","head_sha":"ed49217ad6244f1d3bfe4588f122fa861849739c","url":"https://api.github.com/repos/CrocSwap/integer-mult-bounds/actions/jobs/115038013572","html_url":"https://github.com/CrocSwap/integer-mult-bounds/actions/runs/38317651752/job/115038013572","status":"completed","conclusion":"success","created_at":"2026-10-12T22:36:47Z","started_at":"2026-10-13T01:59:12Z","completed_at":"2026-10-13T02:10:05Z","name":"replay","steps":[{"name":"Set up job","status":"completed","conclusion":"success","number":1,"started_at":"2026-10-13T01:59:13Z","completed_at":"2026-10-13T01:59:14Z"},{"name":"Run actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1","status":"completed","conclusion":"success","number":2,"started_at":"2026-10-13T01:59:14Z","completed_at":"2026-10-13T01:59:23Z"},{"name":"Run actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97","status":"completed","conclusion":"success","number":3,"started_at":"2026-10-13T01:59:23Z","completed_at":"2026-10-13T01:59:23Z"},{"name":"Install verification dependencies","status":"completed","conclusion":"success","number":4,"started_at":"2026-10-13T01:59:23Z","completed_at":"2026-10-13T01:59:51Z"},{"name":"Check selected record and review evidence","status":"completed","conclusion":"success","number":5,"started_at":"2026-10-13T01:59:51Z","completed_at":"2026-10-13T01:59:52Z"},{"name":"Cold finite replay and exact composition binding","status":"completed","conclusion":"success","number":6,"started_at":"2026-10-13T01:59:52Z","completed_at":"2026-10-13T02:10:01Z"},{"name":"Require committed files unchanged","status":"completed","conclusion":"success","number":7,"started_at":"2026-10-13T02:10:01Z","completed_at":"2026-10-13T02:10:02Z"},{"name":"Run actions/upload-artifact@v4","status":"completed","conclusion":"success","number":8,"started_at":"2026-10-13T02:10:02Z","completed_at":"2026-10-13T02:10:03Z"},{"name":"Post Run actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97","status":"completed","conclusion":"success","number":15,"started_at":"2026-10-13T02:10:03Z","completed_at":"2026-10-13T02:10:03Z"},{"name":"Post Run actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1","status":"completed","conclusion":"success","number":16,"started_at":"2026-10-13T02:10:03Z","completed_at":"2026-10-13T02:10:03Z"},{"name":"Complete job","status":"completed","conclusion":"success","number":17,"started_at":"2026-10-13T02:10:03Z","completed_at":"2026-10-13T02:10:03Z"}],"check_run_url":"https://api.github.com/repos/CrocSwap/integer-mult-bounds/check-runs/115038013572","labels":["ubuntu-24.04"],"runner_id":1000048998,"runner_name":"GitHub Actions 1000048998","runner_group_id":0,"runner_group_name":"GitHub Actions"}]} \ No newline at end of file diff --git a/research/selected626-linux-reconciliation/evidence/run.json b/research/selected626-linux-reconciliation/evidence/run.json new file mode 100644 index 0000000000..68bb585a10 --- /dev/null +++ b/research/selected626-linux-reconciliation/evidence/run.json @@ -0,0 +1 @@ +{"conclusion":"success","created_at":"2026-10-12T22:36:47Z","event":"push","head_repository":{"full_name":"CrocSwap/integer-mult-bounds"},"head_sha":"ed49217ad6244f1d3bfe4588f122fa861849739c","html_url":"https://github.com/CrocSwap/integer-mult-bounds/actions/runs/38317651752","id":38317651752,"path":".github/workflows/frontier626.yml","repository":{"full_name":"CrocSwap/integer-mult-bounds"},"run_attempt":1,"status":"completed","updated_at":"2026-10-13T02:10:06Z"} diff --git a/research/selected626-linux-reconciliation/evidence/workflow.log.gz b/research/selected626-linux-reconciliation/evidence/workflow.log.gz new file mode 100644 index 0000000000..e68c880a25 Binary files /dev/null and b/research/selected626-linux-reconciliation/evidence/workflow.log.gz differ diff --git a/research/selected626-linux-reconciliation/verify.py b/research/selected626-linux-reconciliation/verify.py new file mode 100644 index 0000000000..89f5d1bee9 --- /dev/null +++ b/research/selected626-linux-reconciliation/verify.py @@ -0,0 +1,246 @@ +#!/usr/bin/env python3 +"""Check preserved PR626 CI evidence; this does not rerun its mathematics. + +Josh Snider (jsnider3), with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from copy import deepcopy +from fractions import Fraction +from hashlib import sha256 +import gzip +import io +import json +from pathlib import Path +import subprocess +import zipfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE = '66849e1475c930fd7732b1a0067ffee7e1e95f60' +CI_HEAD = 'ed49217ad6244f1d3bfe4588f122fa861849739c' +RUN = 38317651752 +ARTIFACT = 11784169747 +STAGES = ['bit543', 'declarations', 'complex626', 'independent-owner', + 'helper-interface', 'bindings'] +MEMBERS = {'STEPS.json', 'RESULT.json', 'complex/ASSEMBLY.json', + 'complex/RECEIPT.json', 'complex/RESULT.json', 'complex/STAGES.json', + *(name + '.log' for name in STAGES)} +DIFFERING_PATHS = [('template_sha256',), ('input_sha256', 'owner_audit'), + ('input_sha256', 'fresh_invoice')] + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def digest(data): + return sha256(data).hexdigest() + + +def read_json(path): + return json.loads(path.read_bytes()) + + +def git(*args): + return subprocess.check_output(['git', '-C', str(ROOT), *args]) + + +def source_objects(commit, paths): + return {path: git('rev-parse', commit + ':' + path).decode().strip() + for path in paths} + + +def compare_sources(ci, base, expected): + require(ci == base == expected, 'Tested source objects differ from base/pins') + + +def archive_members(data): + with zipfile.ZipFile(io.BytesIO(data)) as archive: + names = archive.namelist() + require(len(names) == len(set(names)) and set(names) == MEMBERS, + 'Unexpected or missing artifact members') + return {name: archive.read(name) for name in names} + + +def check_evidence(run, jobs, artifacts, files, selected, assembly, expected): + require(run['id'] == RUN and run['head_sha'] == CI_HEAD and run['run_attempt'] == 1, + 'Wrong run, head or attempt') + require(run['repository']['full_name'] == 'CrocSwap/integer-mult-bounds' + and run['head_repository']['full_name'] == 'CrocSwap/integer-mult-bounds', + 'Wrong source repository') + require(run['path'] == '.github/workflows/frontier626.yml' + and run['event'] == 'push', 'Wrong workflow or event') + require((run['status'], run['conclusion']) == ('completed', 'success'), + 'Run did not complete successfully') + require(jobs['total_count'] == len(jobs['jobs']) == 1, 'Unexpected job inventory') + job = jobs['jobs'][0] + require(job['run_id'] == RUN and job['head_sha'] == CI_HEAD + and job['run_attempt'] == 1 and job['name'] == 'replay' + and job['status'] == 'completed' and job['conclusion'] == 'success', + 'Replay job identity/status mismatch') + steps = job['steps'] + require(len({s['name'] for s in steps}) == len(steps), 'Duplicate workflow step') + require(all(s['status'] == 'completed' and s['conclusion'] == 'success' for s in steps), + 'Failed or skipped workflow step') + require({s['name'] for s in steps} == set(expected['workflow_steps']), + 'Workflow step coverage changed') + require(artifacts['total_count'] == len(artifacts['artifacts']) == 1, + 'Unexpected artifact inventory') + artifact = artifacts['artifacts'][0] + require(artifact['id'] == ARTIFACT and artifact['name'] == 'frontier626-linux-python312' + and artifact['workflow_run']['id'] == RUN + and artifact['workflow_run']['head_sha'] == CI_HEAD, + 'Artifact is detached from tested run') + require(artifact['digest'] == 'sha256:' + expected['evidence_sha256']['artifact.zip'], + 'Artifact archive digest differs from GitHub metadata') + require(set(files) == MEMBERS, 'Unexpected or missing artifact members') + replay_steps = json.loads(files['STEPS.json']) + require([s['name'] for s in replay_steps] == STAGES, 'Replay stage coverage changed') + for step in replay_steps: + require(step['exit_code'] == 0, 'Failed replay stage: ' + step['name']) + require(digest(files[step['name'] + '.log']) == step['log_sha256'], + 'Replay log digest mismatch: ' + step['name']) + result = json.loads(files['RESULT.json']) + receipt = json.loads(files['complex/RECEIPT.json']) + actual = json.loads(files['complex/ASSEMBLY.json']) + complex_result = json.loads(files['complex/RESULT.json']) + require(result['status'] == 'PASS_REBUILT_PR543_PR626_COMPOSITION', + 'Composition binding did not pass') + kappa = Fraction(selected['kappa']) + require(kappa == Fraction(selected['decimal']) == Fraction(result['kappa']) + == Fraction(result['decimal']) == Fraction(actual['kappa']) + == Fraction(complex_result['kappa']), 'Exact selected result mismatch') + for name, field in [('complex/RECEIPT.json', 'complex_receipt_sha256'), + ('complex/ASSEMBLY.json', 'complex_assembly_sha256')]: + require(digest(files[name]) == result[field], 'Broken composition receipt binding') + for name in ('RESULT.json', 'ASSEMBLY.json'): + require(digest(files['complex/' + name]) == receipt['artifacts'][name], + 'Broken complex artifact binding') + require(receipt['status'] == complex_result['status'] + == 'PASS_COLD14_NATIVE_COMPLEX_AND_CITED_BIT', 'Complex replay did not pass') + require(complex_result['reused'] == {'baseline': False, 'locals': []}, + 'Complex replay reused earlier outputs') + require(len(receipt['steps']) == len(expected['complex_steps']) + and sorted(s['name'] for s in receipt['steps']) == expected['complex_steps'], + 'Complex substep coverage changed') + require(all(s['exit_code'] == 0 for s in receipt['steps']), 'Failed complex substep') + require(len(actual['outer']) == 47 and all(Fraction(v) > 0 for v in actual['outer'].values()), + 'Strict assembly margins changed') + require(result['bit_input_sha256'] == actual['input_sha256']['inputs/PR543-EXPECTED.json'], + 'Bit supplier binding changed') + require(complex_result['global_profile'] == actual['complex_profile'], 'Profile mismatch') + # Preserve all three differences explicitly; do not erase whole hash maps. + left, right, differences = deepcopy(actual), deepcopy(assembly), [] + for path in DIFFERING_PATHS: + a, b = left, right + for key in path[:-1]: + a, b = a[key], b[key] + av, bv = a.pop(path[-1]), b.pop(path[-1]) + differences.append({'path': list(path), 'linux': av, 'committed': bv}) + require(differences == expected['assembly_digest_differences'], + 'Recorded provenance differences changed') + require(left == right, 'Mathematical assembly fields differ') + return {'status': 'PASS_PR626_LINUX_RECONCILIATION', 'run': RUN, + 'ci_head': CI_HEAD, 'base': BASE, 'kappa': str(kappa), + 'replay_stages': len(replay_steps), 'complex_substeps': len(receipt['steps']), + 'strict_assembly_margins': len(actual['outer']), + 'assembly_digest_differences': differences} + + +def negative_controls(args): + controls = [] + + def reject(name, mutate, message): + changed = deepcopy(args) + mutate(changed) + try: + check_evidence(*changed) + except ValueError as error: + require(message in str(error), name + ': wrong rejection: ' + str(error)) + controls.append(name) + else: + raise ValueError('Invalid evidence accepted: ' + name) + + def mutate_json(data, member, mutate, rebind=False): + obj = json.loads(data[3][member]) + mutate(obj) + data[3][member] = json.dumps(obj).encode() + if rebind: + result = json.loads(data[3]['RESULT.json']) + result['complex_assembly_sha256'] = digest(data[3][member]) + receipt = json.loads(data[3]['complex/RECEIPT.json']) + receipt['artifacts']['ASSEMBLY.json'] = digest(data[3][member]) + data[3]['complex/RECEIPT.json'] = json.dumps(receipt).encode() + result['complex_receipt_sha256'] = digest(data[3]['complex/RECEIPT.json']) + data[3]['RESULT.json'] = json.dumps(result).encode() + + reject('wrong_ci_head', lambda a: a[0].update(head_sha=BASE), 'Wrong run') + reject('wrong_attempt', lambda a: a[0].update(run_attempt=2), 'Wrong run') + reject('queued_run', lambda a: a[0].update(status='queued'), 'did not complete') + reject('skipped_workflow_step', lambda a: a[1]['jobs'][0]['steps'][5].update(conclusion='skipped'), 'Failed or skipped') + reject('artifact_other_run', lambda a: a[2]['artifacts'][0]['workflow_run'].update(id=RUN + 1), 'detached') + reject('artifact_bad_digest', lambda a: a[2]['artifacts'][0].update(digest='sha256:' + '0' * 64), 'archive digest') + reject('missing_helper_log', lambda a: a[3].pop('helper-interface.log'), 'missing artifact') + reject('corrupt_owner_log', lambda a: a[3].update({'independent-owner.log': b'PASS fake'}), 'log digest') + reject('missing_helper_stage', lambda a: mutate_json(a, 'STEPS.json', lambda o: o.pop(4)), 'stage coverage') + reject('failed_bit_stage', lambda a: mutate_json(a, 'STEPS.json', lambda o: o[0].update(exit_code=1)), 'Failed replay') + reject('wrong_kappa', lambda a: mutate_json(a, 'RESULT.json', lambda o: o.update(kappa='1/100')), 'Exact selected') + reject('broken_receipt_link', lambda a: mutate_json(a, 'RESULT.json', lambda o: o.update(complex_receipt_sha256='0' * 64)), 'receipt binding') + reject('changed_positive_margin', lambda a: mutate_json(a, 'complex/ASSEMBLY.json', lambda o: o['outer'].update({next(iter(o['outer'])): '1'}), True), 'Mathematical assembly') + reject('changed_source_engine_digest', lambda a: mutate_json(a, 'complex/ASSEMBLY.json', lambda o: o['input_sha256'].update({'engines/moment.py': '0' * 64}), True), 'Mathematical assembly') + reject('changed_recorded_digest_difference', lambda a: mutate_json(a, 'complex/ASSEMBLY.json', lambda o: o.update(template_sha256='0' * 64), True), 'provenance differences') + return controls + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--out', type=Path, help='write deterministic report outside evidence inputs') + options = parser.parse_args() + expected = read_json(HERE / 'EXPECTED.json') + for name, pin in expected['evidence_sha256'].items(): + require(digest((HERE / 'evidence' / name).read_bytes()) == pin, + 'Frozen evidence bytes changed: ' + name) + require(digest(gzip.decompress((HERE / 'evidence/workflow.log.gz').read_bytes())) + == expected['workflow_log_sha256'], 'Original workflow log bytes changed') + pins = read_json(HERE / 'SOURCE-PINS.json') + selected = json.loads(git('show', BASE + ':certificates/selected-result.json')) + manifest = json.loads(git('show', BASE + ':' + selected['source_manifest'])) + paths = sorted(set(manifest['package_roots'] + list(selected['proof_supplements']) + + ['scripts', 'Makefile', '.github/workflows/frontier626.yml', + 'certificates/selected-result.json', selected['source_manifest'], + selected['certificate']])) + require(sorted(pins) == paths, 'Source comparison coverage changed') + compare_sources(source_objects(CI_HEAD, paths), source_objects(BASE, paths), pins) + assembly = json.loads(git('show', BASE + ':' + selected['certificate'])) + files = archive_members((HERE / 'evidence/artifact.zip').read_bytes()) + receipt = json.loads(files['complex/RECEIPT.json']) + package = 'research/complex-k492-owner-repair/' + require(receipt['manifest_sha256'] == digest(git('show', BASE + ':' + package + 'MANIFEST.json')) + and receipt['spec_sha256'] == digest(git('show', BASE + ':' + package + 'data/SPEC.json')), + 'Complex receipt source/spec differs from tested base') + spec = json.loads(git('show', BASE + ':' + package + 'data/SPEC.json')) + require(set(receipt['source_manifest_sha256']) == set(spec['build']['sources']), + 'Complex receipt source inventory changed') + for name, pin in receipt['source_manifest_sha256'].items(): + require(pin == digest(git('show', BASE + ':' + package + 'vendor/' + name + '/MANIFEST.json')), + 'Complex receipt dependency differs from tested base: ' + name) + args = [read_json(HERE / 'evidence' / (name + '.json')) for name in ('run', 'jobs', 'artifacts')] + args += [files, selected, assembly, expected] + report = check_evidence(*args) + report['source_objects_matched'] = len(paths) + report['negative_controls'] = negative_controls(args) + try: + compare_sources({'source': 'changed'}, {'source': 'base'}, {'source': 'base'}) + except ValueError: + report['negative_controls'].append('changed_tested_source') + else: + raise ValueError('Changed tested source accepted') + if options.out: + options.out.write_text(json.dumps(report, indent=2) + '\n') + print(report['status'], '6 stages, 64 substeps, 47 strict margins,', + str(len(report['negative_controls'])) + ' rejection controls') + + +if __name__ == '__main__': + main()