diff --git a/docs/research/pr-ledger.json b/docs/research/pr-ledger.json index c85277da8e..c0c611af80 100644 --- a/docs/research/pr-ledger.json +++ b/docs/research/pr-ledger.json @@ -6719,10 +6719,11 @@ "research/five-stage-gen4-banks" ], "github_state": "OPEN", - "unresolved_question": "Whole-current-PR incorporation is not established: 12 changed paths lack byte-identical coverage in main or its checked PR181 archive. Distinguish later equivalent edits, unique content and historical implementations before closure.", + "unresolved_question": "A contributor companion reconstructs the exact later target-prefix head from the historical package plus all 12 previously uncovered files and supplies scoped replay evidence. Maintainer acceptance and disposition of that later head remain pending; the earlier integrated checkpoint and its inherited theorem obligations are unchanged.", "closure": null, "reconciliation_evidence": [ - "research/pr-reconciliation-20261012/content-comparison.json" + "research/pr-reconciliation-20261012/content-comparison.json", + "research/pr279-target-prefix-reconciliation/RESULTS.json" ], "current_head_observed_in": "research/pr-reconciliation-20261012/ending-snapshot.json" }, diff --git a/docs/research/pr-ledger.md b/docs/research/pr-ledger.md index 341c9950c1..a0eb9ffe73 100644 --- a/docs/research/pr-ledger.md +++ b/docs/research/pr-ledger.md @@ -237,7 +237,7 @@ Each evidence link leads to the original scoped assessment. The JSON records exa | [#275](https://github.com/CrocSwap/integer-mult-bounds/pull/275) | lydakis | unreviewed | No exact-head review established; inspect contribution and dependencies. | | [#277](https://github.com/CrocSwap/integer-mult-bounds/pull/277) | hcg890 | unreviewed | No exact-head review established; inspect contribution and dependencies. | | [#278](https://github.com/CrocSwap/integer-mult-bounds/pull/278) | hcg890 | unreviewed | No exact-head review established; inspect contribution and dependencies. | -| [#279](https://github.com/CrocSwap/integer-mult-bounds/pull/279) | rohanarun | changed since review | [record 1](../../docs/research/community-pr279-integration.json) · [record 2](../../research/pr-reconciliation-20261012/content-comparison.json) | +| [#279](https://github.com/CrocSwap/integer-mult-bounds/pull/279) | rohanarun | changed since review | [record 1](../../docs/research/community-pr279-integration.json) · [record 2](../../research/pr-reconciliation-20261012/content-comparison.json) · [later-head source and contributor replay](../../research/pr279-target-prefix-reconciliation/README.md); maintainer disposition pending | | [#280](https://github.com/CrocSwap/integer-mult-bounds/pull/280) | utcorvusvolat-dotcom | unreviewed | No exact-head review established; inspect contribution and dependencies. | | [#281](https://github.com/CrocSwap/integer-mult-bounds/pull/281) | rohanarun | unreviewed | No exact-head review established; inspect contribution and dependencies. | | [#282](https://github.com/CrocSwap/integer-mult-bounds/pull/282) | chafreaky | unreviewed | No exact-head review established; inspect contribution and dependencies. | diff --git a/research/pr279-target-prefix-reconciliation/CLAIM.md b/research/pr279-target-prefix-reconciliation/CLAIM.md new file mode 100644 index 0000000000..44f225a3f4 --- /dev/null +++ b/research/pr279-target-prefix-reconciliation/CLAIM.md @@ -0,0 +1,25 @@ +# Sprint claim: PR279 target-prefix reconciliation + +- Track: research consolidation; OS CSPRNG seed 95 (raw uint32 44938895, + rejection threshold 4294967200), drawn 2026-10-13 05:54:31 UTC. +- Exact main base: 66849e1475c930fd7732b1a0067ffee7e1e95f60. +- Candidates: restore PR236 source package (already claimed by PR746); + reconcile PR210's later F2 movement fusion; reconcile PR279's later + target-prefix update. Seed 95 modulo 2 selects the second unclaimed task. +- Scope: explain and check the 12-file difference between reviewed PR279 head + 4d8c31eec7ae618645cb058101cb4e72a97268d3 and current head + 913ccc48a0bc1173709ea92280b96252256b7754. Resolve the vague missing-content + statement with exact source coverage and a scoped fresh replay of the + target-prefix update; do not change the selected frontier or acceptance status. +- Method: exact Git/source hashes, compare immutable source bytes, independently + inspect target-prefix algebra and frame/accounting changes, run the affected + pipeline with negative controls where feasible. Distinguish missing source + coverage from failed mathematics or a complete theorem proof. +- Deliverable: one attributed research consolidation package and focused PR, + a deterministic verification command, exact evidence and unresolved obligations. +- Expected finish: 2026-10-13 06:44 UTC (October 12, 11:44 p.m. America/Los_Angeles). + Reserve at least the final 12.5 minutes for verification and handoff. +- Coordination: GitHub reports no pinned issues. Open-PR metadata inspected, + refreshed through PR803 at 05:58 UTC. No matching PR279 reconciliation found. + Existing PR281/283/287/289/291 build later mechanisms, not this reconciliation. +- Attribution: prepared for mihir-s-05 with substantial OpenAI Codex assistance. diff --git a/research/pr279-target-prefix-reconciliation/EVIDENCE.json b/research/pr279-target-prefix-reconciliation/EVIDENCE.json new file mode 100644 index 0000000000..f99eb92849 --- /dev/null +++ b/research/pr279-target-prefix-reconciliation/EVIDENCE.json @@ -0,0 +1,54 @@ +{ + "schema": "pr279-target-prefix-replay-evidence/1", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "candidate_head": "913ccc48a0bc1173709ea92280b96252256b7754", + "recorded_at_utc": "2026-10-13T06:24:12.788109+00:00", + "environment": { + "python": "3.12.0 (tags/v3.12.0:0fb18b0, Oct 2 2023, 13:03:39) [MSC v.1935 64 bit (AMD64)]", + "implementation": "CPython", + "platform": "Windows-11-10.0.26300-SP0", + "sympy": "1.14.0", + "byteorder": "little" + }, + "executed_command": [ + "python", + "-X", + "utf8", + "-B", + "work/pr279-candidate/verify.py", + "--output", + "work/pr279-replay" + ], + "execution_context": "Workspace containing work/integer-mult-bounds checkout and byte-identical reconstructed work/pr279-candidate source; PYTHONUTF8=1.", + "public_reproduction": "python -X utf8 -B research/pr279-target-prefix-reconciliation/verify.py --replay --work ../pr279-replay-new", + "source_manifest_sha256": "f75a7190703e33d9d575fad294b0c9de0f4dcbe195e9f67557938077cd4dfd77", + "archive_sha256": "a955de158f9808354783ceefa744272d4591465012b76daba7afc855f7449685", + "files": { + "banks.json": "60abe0d6e917a0e3e712f93f31a73944a4eaf9e318478b8db6af722f1aa3a8a6", + "bit.json": "5a829d673a55e32552e5480a1054db58e6e596f12a21f6859e12d17e272875f6", + "certificate.json": "9c9da36253330348a4cb4c8680b16bd9b5abd5488ab4757694bcfca6f3b5f634", + "complex.json": "5dc1c58c2558b16ae970258bbedd033259563d9eb1f620b7027ce91cb42e38bf", + "descent.json": "2e09e50adadd49821e0b57f0e7ac8b767ec0a15528c5272ab18bab0d50113fd9", + "finite.json": "7011b82313b60cc51f35f03f8f4ac36edb970e81eaa8a69b5ec4722fe9b187f7", + "geometry.json": "e0aa792388bdf5b486fce764a6aa51ea2d3fc7346c970a8294eea111eca236be", + "global_result.json": "83dab8520fd6930f3ed79a1e506c4492572d960c16015e128c062a79638e63bc", + "math.json": "1ea917495fa18051c51b259f27aa3bc92034f0140f7b33dddb26ad3feb3b70ca", + "parity.json": "facfa44f803190c662a097da65a823cc139a20c69590aea187eb4cd84e620d2e", + "primes.json": "5e149c0a73a1e2385ac426c17aa19af1a0db490a9e589af96abe1de5078aa8b6", + "raw.json": "3748ff743d5cd200803af2b9886ddff914e47af85f78d33a14d80cea9f43aebb", + "scalar.json": "b8b04b3056d6a5e8766aea18bd65df2c250535f6f51151e64d732759b07501bf", + "target.json": "df557ad208fbbcb72cb35e7f1b01f9756be5763a30b98acfdabb287f57bd1275", + "verification.json": "75ad272e25b32ebf60545e97c4ac06d9c1feefc0cb6831089a8aa1552521f5a8", + "virtual.json": "07948db63b729e84dc6c505a8a4fa4bc52bb04c21a7029069a7d1a3c1c6e5f25", + "replay.log": "01324c83fc5c0c74350aa19f2da7a7511da1ad8fa1a5159e48d587e2b49212cf" + }, + "emitted_word": { + "encoding": "big-endian signed 32-bit integers, six per instruction", + "records": 723357, + "sha256": "f4e86f187ae025f47cae9424484419909a40f6df3a823cf5f7bd6999be126d7f" + }, + "source_ci_metadata_sha256": "9840b84cb82672306c925b763e76a48b10111c3744c6543d9e2a6a328d12ad54", + "scope": "Fresh execution of the unchanged candidate verifier. Archive contains stage receipts and exact certificate; the complete literal output and bases are regenerated by --replay. Container hashes bind stored evidence only. The emitted-word digest canonicalizes every instruction field, not its gzip bytes. No fresh gen4 discovery regeneration, selected-frontier replay, Lean build, repository-wide make verify, or new remote CI is claimed.", + "results_sha256": "93b374dc5cf6298a98f6084137d31826c40488585c1662fb4f5147ba8333da83", + "integration_base_commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261" +} diff --git a/research/pr279-target-prefix-reconciliation/NOTICE.md b/research/pr279-target-prefix-reconciliation/NOTICE.md new file mode 100644 index 0000000000..57b5f2097e --- /dev/null +++ b/research/pr279-target-prefix-reconciliation/NOTICE.md @@ -0,0 +1,24 @@ +# Attribution, license and scope + +This companion package is contributed under the repository's Apache-2.0 +license. Source files in `source-update.tar.gz` are exact public PR279 bytes at +`913ccc48a0bc1173709ea92280b96252256b7754`; their original license, attribution +and AI-assistance disclosures remain intact. Reconstruction also preserves +the historical package's LICENSE and every nested notice without alteration. + +Rohan Arun (rohanarun) contributed PR279's concave-descent retiming, target-prefix +selection and integration with Anthropic Claude assistance. His source credits +eumemic's PR268 for the target-prefix transform, with its stream-count adaptation. +DreamingOfClouds contributed the gen4 word and its integrated physical producers. +The inherited lineage includes Henry Grant (hcg890), Jacob Sussman, Evan McKinney, +Chafik Boukhalfa (chafreaky), Avi Eisenberg (ikeboy), Dugongue, sennemmi, +icekylinx, James Chang and other contributors retained in the source notices. +Douglas Colkitt prepared the maintainer checkpoint and reconciliation records. + +The source reconstruction, scoped reconciliation and new corruption controls +were prepared for mihir-s-05 with substantial OpenAI Codex assistance. Fresh +execution of a contributor's verifier is not a new independently implemented +mathematical verifier, an independent human review or a full theorem proof. + +The submitted original notices identify predecessor authorship; no exclusive +priority or endorsement by the named contributors is claimed. diff --git a/research/pr279-target-prefix-reconciliation/OVERLAP.json b/research/pr279-target-prefix-reconciliation/OVERLAP.json new file mode 100644 index 0000000000..ab2b57a469 --- /dev/null +++ b/research/pr279-target-prefix-reconciliation/OVERLAP.json @@ -0,0 +1,73 @@ +{ + "checked_at_utc": "2026-10-13T06:33:45.866572+00:00", + "open_pr_count": 637, + "highest_open_pr": 824, + "main_commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "pr279_head": "913ccc48a0bc1173709ea92280b96252256b7754", + "matching_reconciliation_found": false, + "related_prs": [ + { + "number": 806, + "head": "4189f39ec022b7d1f8adb6c394f80b2c31a3f9c5", + "title": "Audit #695: selected #626 provenance digest differences are timing and directory order, reproduced byte for byte" + }, + { + "number": 746, + "head": "ee3580bd708d82b5bdfda6a2bc3f0a34710be50e", + "title": "Research consolidation: restore reviewed PR236 source package" + }, + { + "number": 291, + "head": "5c296797e06101c74d15b0162dfe372c186ec330", + "title": "Conditional \u03ba = 7.44728650221677e-4: second concave-descent retiming (89 gates, constructed frames) after #290's kernel entries on the gen5 word" + }, + { + "number": 289, + "head": "04e14102a36a33b9f9eef4e4c76119fd6e54b445", + "title": "Extreme-meet frame retiming (87 gates) on target-compressed gen5 word: kappa = 7.44127392470948e-4" + }, + { + "number": 287, + "head": "9f85de891c5eec5de4e33a9185157c9e573bb315", + "title": "Conditional \u03ba = 7.44136146100942e-4: two concave-descent retimings (904 + 111 gates) and 220 target-prefix squares on #285's gen5 five-stage banks" + }, + { + "number": 283, + "head": "19d148bd7aa199378816cf1fb9ff746eb4d815da", + "title": "Conditional \u03ba = 7.26111344123732762670617e-4: gen4 response kernels and endpoint-aware composition of #279/#280" + }, + { + "number": 282, + "head": "841a99b8cf0609ce461b208ed6367463459dd7f5", + "title": "Conditional \u03ba = 7.24733001963261\u00b710\u207b\u2074: 695 collective response-kernel entries (per-entry cuts, entrances of any dimension) on #276's gen4 word, composed with #279's descent retiming (+0.258% over #276)" + }, + { + "number": 281, + "head": "7542b215a7ff49d264e2b4691ca7fa9bc3be82d9", + "title": "Conditional \u03ba = 7.25113717934416e-4: target-prefix compression (280 groups) composed with #280's gen4 retiming, early restorations and dirty entrances" + } + ], + "scope": "Checked open titles/descriptions, PR279 comments and review ledger; recent main integration leaves all consumed PR279 source and immutable context bytes unchanged. No pinned sprint issue exists.", + "recent_prs_checked": [ + { + "number": 824, + "title": "Tooling: 1.13x faster exact stage-pair audit with identical receipts", + "head": "2b342526350a3c36936feb7f3f50669fad2770b1" + }, + { + "number": 823, + "title": "Research construction: shorten historical R480 quad 1 by 12 XORs (no new kappa)", + "head": "83d547e30fed98682ffc6eacbeeaafa96cfb42fb" + }, + { + "number": 822, + "title": "Research: reuse dirty echo connectors (no new kappa)", + "head": "8c5e1b557f59bca29139c4c2dcc65edfb808372b" + }, + { + "number": 821, + "title": "Research audit: 286-to-160-bit prefix estimate for pinned #626 (no new kappa)", + "head": "6b832a6ba4dce8dd6e2fb0897dd4543364b932f8" + } + ] +} diff --git a/research/pr279-target-prefix-reconciliation/README.md b/research/pr279-target-prefix-reconciliation/README.md new file mode 100644 index 0000000000..900bf1343b --- /dev/null +++ b/research/pr279-target-prefix-reconciliation/README.md @@ -0,0 +1,191 @@ +# Reconcile PR279's later target-prefix source + +**Research consolidation; no new selected bound.** At main +`66849e1475c930fd7732b1a0067ffee7e1e95f60`, the central ledger identifies twelve +uncovered files in [PR279](https://github.com/CrocSwap/integer-mult-bounds/pull/279)'s +later head. They are a specific target-prefix update, +not a failure of the earlier reviewed construction. This companion preserves +the exact missing bytes and reconstructs the later package in a separate +directory. The historical package and its original receipts stay intact. + +| Source state | Exact commit | Conditional historical kappa | +|---|---|---| +| Reviewed and retained on main | `4d8c31eec7ae618645cb058101cb4e72a97268d3` | `90446448750933/125000000000000000` | +| Later PR279 head reconstructed here | `913ccc48a0bc1173709ea92280b96252256b7754` | `724098741932703/1000000000000000000` | + +The selected result at this contribution's original research base was #626 with #543, +`51110230636731/31250000000000000`. Neither historical value above replaces it. +During this run, main advanced to `7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261` +and selected #741 with #589, `1661202643272239/1000000000000000000`. +This contribution is rebased on that final integration base. Every consumed +historical package, workflow and immutable context byte is identical across +the two bases, so the completed mathematical replay remains applicable. +Both bases are recorded in the source and evidence inventories; the original +`base_commit` fields identify the research base, not the final PR parent. +The [original integration receipt](../../docs/research/community-pr279-integration.json) +explicitly pins the first head and labels the second as later and unreviewed. +The [original source comparison](../pr-reconciliation-20261012/content-comparison.json) +records 104 matching paths and 12 unresolved paths among 116 PR paths. + +## Exact source coverage + +[SOURCE.json](SOURCE.json) binds every reconstructed file to both its SHA-256 +and its Git blob ID. The historical package contains 113 files. The later +package contains 115: 103 unchanged files, ten modified files, and two additions. +The unchanged workflow is the 116th path in the PR inventory. The complete +historical inventory, workflow, original review receipt, and old comparison +are checked before reconstruction. + +[source-update.tar.gz](source-update.tar.gz) holds the twelve updated files +byte for byte. It is an input archive, not a patch applied to the selected +or historical source trees. Extracting the archive alone yields the twelve +changed files; `--extract` below reconstructs the complete candidate package. +The upstream package's own manifest must then cover every reconstructed file. +No network or Git checkout is required for that reconstruction. +The [pinned later source tree](https://github.com/CrocSwap/integer-mult-bounds/tree/913ccc48a0bc1173709ea92280b96252256b7754/research/five-stage-gen4-banks) +also permits direct review of the original files. + +| Updated files | Substantive change | +|---|---| +| `target-selection.json`, `target_transform.py` | Add the 220-square selection and literal target-prefix transform. | +| `portable_bit.py` | Execute the transform after the reviewed descent step and rebind its raw ledger. | +| `scalar_check.py` | Bind the changed event hash, 626,580 additions and coefficient counts. The scalar checker logic is unchanged. | +| `bank_check.py` | Recount 479,580 banked calls per replica, previously 480,680; rank mass is unchanged. | +| `finite_check.py` | Charge 626,580 weighted and 630,100 unit additions, previously 626,360 and 629,880. | +| `verify.py` | Require the later exact historical kappa after the same nine mandatory stages. | +| `README.md`, `PROOF.md`, `PR-STATEMENT.md`, `NOTICE.md` | Describe and credit the added stage. | +| `MANIFEST.json` | Bind the complete updated package. | + +All changes between the two pinned repository commits fall in this table. +The package's retained scalar decoder, bank templates, complex supplier, +prime checker, exact moment engines and assembly logic are unchanged. +The new transform's checks supplement the existing pipeline. + +## Mechanism and complete local cost + +Each disjoint square contains four targets. In the selected interval, the +prefix delivered to one dependent target is the F2 sum of the prefixes +delivered to the other three. Writing their arbitrary initial contents as +`d0, r1, r2, r3` and delivered prefixes as `P0, P1, P2, P3`, the setup changes +the dependent target to `d0 + r1 + r2 + r3`. Omitting its old prefix and adding +back the three completed retained targets gives +`d0 + P1 + P2 + P3 = d0 + P0`. Thus setup and restore both matter even when +the target initially contains arbitrary data. + +This argument needs the literal dependencies and the no-active-target-read +guard; a selection's announced counts alone do not establish it. The candidate +transform recomputes the prefix responses from the actual input word, checks +the guard, rebuilds every movement, and checks nesting, common frames, +nondegeneracy, endpoints and copied-center lifetimes. It replays all formal +columns in both directions and requires an omitted-setup mutation to fail. + +The 220 squares touch 880 targets. They remove 1,100 old prefix additions and +insert 660 setup plus 660 restore additions, a net **220 extra additions**. +The local paid profile changes by `{1: -220, 20: -220, 21: +220}`. That removes +220 recursive calls per invocation while preserving rank mass, because +`-220 - 20*220 + 21*220 = 0`. The five-stage bill drops from 483,146 to 482,046 +calls, and the banked bill from 480,680 to 479,580 per replica. Source accesses, +copies, helper restoration, banks and the inherited complex supplier remain +in the unchanged full finite replay. The quick command below only checks the +submitted schedule's accounting; it does not independently prove these +literal identities. + +## Reproduce and inspect + +Python 3.11 or later suffices for the source/evidence checks and corruption +controls. The full candidate replay also requires the inherited pinned +dependency `sympy==1.14.0`. + +```sh +python -X utf8 -B research/pr279-target-prefix-reconciliation/verify.py +python -X utf8 -B research/pr279-target-prefix-reconciliation/test_verify.py +``` + +The first command checks exact source coverage, the finite selection census +and the retained replay evidence. Its first line is: + +```text +PASS_PR279_SOURCE_RECONCILIATION old=113 current=115 modified=10 added=2 +``` + +For a fresh complete replay, choose a **new directory outside the repository**: + +```sh +python -X utf8 -B research/pr279-target-prefix-reconciliation/verify.py --replay --work ../pr279-replay-new +``` + +The wrapper reconstructs all 115 input files under `source/`, runs the +unmodified candidate `verify.py` with assertions enabled, and writes raw +output to `replay.log` and per-stage results to `replay/`. A successful run ends +with: + +```text +PASS_PR279_FRESH_REPLAY stages=9 kappa=724098741932703/1000000000000000000 +``` + +Use `--extract --work ../pr279-inspect-new` to reconstruct the source for +review without executing the mathematical verifier. Both actions reject an +existing destination. Checks remain enabled under `-I -O`; the full replay +always launches a normal assertion-enabled interpreter. + +## Evidence and review boundary + +The [result](RESULTS.json) and [replay evidence inventory](EVIDENCE.json) record +the exact source identity, environment, command and retained output hashes. +The complete fresh replay passed on Windows 11, CPython 3.12.0 and SymPy 1.14.0 +in 1,096.765 seconds. It checked all 19,930 formal columns, 27,349 distinct exact +basis determinants, 4,923,000 bank assignments and 370 charts, both moment +engines, and the finite assembly. The actual target-prefix omission control, +11 scalar controls, six prime controls and all nine mandatory-stage omission +controls passed. All 115 source files retained their input bytes. + +The companion's 13 tests pass both normally and under `-I -O`. They include +rejection of the actual historical replay as evidence for the later head, +missing/changed source, missing stages, unpaid restoration and archive +ambiguities. The literal-word fingerprint canonicalizes all six integer +fields of each instruction; a changed frame changes the fingerprint while a +changed gzip timestamp does not. Fresh replays compare this complete word +fingerprint rather than the regenerated gzip container. + +Checking the retained archive is a check of stored +evidence; `--replay` performs fresh mathematical execution. A complete nine-stage +finite replay is distinct from regenerating the unchanged gen4 discovery +outputs, rerunning the selected construction, running Lean, or observing +remote Linux CI. No such additional local execution is inferred. + +[SOURCE-CI.json](SOURCE-CI.json) separately records GitHub's completed successful +[run 38025932115](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/38025932115), +whose `head_sha` is the later `913ccc48...` head. Its dedicated immutable-replay +jobs report success on Python 3.11 and 3.13. This is historical run metadata, +not newly executed CI for this consolidation. It is also distinct from the +earlier head's run recorded in the original maintainer receipt. + +The inherited all-size compiler, weighted/common-ancestor charts, restored-row, +selector, routing, prime-supply, precision/recovery, complex symbolic and +analytic-transfer interfaces remain assumptions. This is not a formal proof +of the full multiplication theorem, a runtime benchmark, or a global optimum. +The consolidation makes the later head's source and scoped replay reviewable; +maintainer acceptance and PR disposition remain separate decisions. + +## Attribution and sprint scope + +Rohan Arun authored PR279's descent selection and integration with Anthropic +Claude assistance. The target-prefix transform is credited in his source to +eumemic's PR268; DreamingOfClouds supplied the gen4 word and package. Henry +Grant and Jacob Sussman's five-stage architecture, Evan McKinney's banks, +Chafik Boukhalfa's physical checkers, Avi Eisenberg's complex supplier and the +full source lineage retain their original notices in the reconstructed package. +Douglas Colkitt's reviewed checkpoint and reconciliation receipts supply the +historical context. See [NOTICE.md](NOTICE.md). + +This consolidation was prepared for **mihir-s-05** with substantial **OpenAI +Codex assistance** in source comparison, implementation, review, execution and +writing. It does not claim independent human peer review. Apache-2.0 applies. + +[CLAIM.md](CLAIM.md) records OS-random seed 95, the three candidate tasks, the +selection rule, the exact main base and overlap checks. No search for a stronger +bound was performed; the experiment is bounded by the single pinned 12-file +update and its complete finite verifier. + +[VALIDATION.md](VALIDATION.md) records the final integration checks, and +[OVERLAP.json](OVERLAP.json) records the pre-submission overlap refresh. diff --git a/research/pr279-target-prefix-reconciliation/RESULTS.json b/research/pr279-target-prefix-reconciliation/RESULTS.json new file mode 100644 index 0000000000..0f69db4666 --- /dev/null +++ b/research/pr279-target-prefix-reconciliation/RESULTS.json @@ -0,0 +1,60 @@ +{ + "schema": "pr279-target-prefix-reconciliation/1", + "status": "EXACT_LATER_SOURCE_PRESERVED_AND_FRESH_FINITE_REPLAY_PASSED", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "reviewed_head": "4d8c31eec7ae618645cb058101cb4e72a97268d3", + "candidate_head": "913ccc48a0bc1173709ea92280b96252256b7754", + "assignment_seed": 95, + "track": "research consolidation", + "coverage": { + "pr_paths": 116, + "previously_matched": 104, + "previously_unresolved": 12, + "retained_update_files": 12, + "modified_relative_to_reviewed": 10, + "added": 2, + "historical_package_files": 113, + "candidate_package_files": 115, + "unchanged_workflow": true, + "complete_candidate_manifest_checked": true + }, + "replay": { + "fresh_stages": [ + "banks", + "bit", + "complex", + "finite", + "math", + "primes", + "raw", + "scalar", + "virtual" + ], + "seconds": 1096.7649999999976, + "inputs_unchanged": true, + "historical_kappa": "724098741932703/1000000000000000000", + "formal_columns": 19930, + "prefix_groups": 220, + "setup_restore_additions": 1320, + "omitted_prefix_additions": 1100, + "local_paid_call_delta": -220, + "five_stage_paid_call_delta": -1100, + "rank_mass_delta": 0, + "scalar_controls": 11, + "determinant_bases": 27349, + "prime_controls": 6, + "bank_assignments": 4923000, + "bank_charts": 370, + "stage_omission_controls": 9 + }, + "evidence": [ + "SOURCE.json", + "EVIDENCE.json", + "SOURCE-CI.json" + ], + "remaining": "Maintainer acceptance and disposition of the later head; inherited all-size/compiler/chart/restored-row/selector/routing/prime/precision/recovery/complex-symbolic/analytic interfaces. No full multiplication theorem or independently implemented mathematical verifier is claimed.", + "selected_frontier_changed": false, + "github_pr279_closed": false, + "attribution": "Mihir Srivastava (mihir-s-05), with substantial OpenAI Codex assistance. Original PR279 and full predecessor notices retained.", + "integration_base_commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261" +} diff --git a/research/pr279-target-prefix-reconciliation/SOURCE-CI.json b/research/pr279-target-prefix-reconciliation/SOURCE-CI.json new file mode 100644 index 0000000000..4528360d33 --- /dev/null +++ b/research/pr279-target-prefix-reconciliation/SOURCE-CI.json @@ -0,0 +1,31 @@ +{ + "conclusion": "success", + "created_at": "2026-10-10T04:58:55Z", + "event": "pull_request", + "head_branch": "gen4-descent-retiming", + "head_sha": "913ccc48a0bc1173709ea92280b96252256b7754", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/actions/runs/38025932115", + "id": 38025932115, + "path": ".github/workflows/five-stage-gen4-banks.yml", + "run_attempt": 1, + "status": "completed", + "updated_at": "2026-10-10T05:12:31Z", + "observed_at_utc": "2026-10-13T06:13:57.076307+00:00", + "jobs": [ + { + "name": "immutable-replay (3.11)", + "conclusion": "SUCCESS", + "startedAt": "2026-10-10T04:58:57Z", + "completedAt": "2026-10-10T05:06:28Z", + "detailsUrl": "https://github.com/CrocSwap/integer-mult-bounds/actions/runs/38025932115/job/114136661983" + }, + { + "name": "immutable-replay (3.13)", + "conclusion": "SUCCESS", + "startedAt": "2026-10-10T04:58:57Z", + "completedAt": "2026-10-10T05:12:30Z", + "detailsUrl": "https://github.com/CrocSwap/integer-mult-bounds/actions/runs/38025932115/job/114136661845" + } + ], + "scope": "Historical GitHub run metadata observed for the pinned candidate head; not new CI on this consolidation branch and not a local replay." +} diff --git a/research/pr279-target-prefix-reconciliation/SOURCE.json b/research/pr279-target-prefix-reconciliation/SOURCE.json new file mode 100644 index 0000000000..e3137f3a02 --- /dev/null +++ b/research/pr279-target-prefix-reconciliation/SOURCE.json @@ -0,0 +1,697 @@ +{ + "schema": "pr279-target-prefix-source/1", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "reviewed_head": "4d8c31eec7ae618645cb058101cb4e72a97268d3", + "candidate_head": "913ccc48a0bc1173709ea92280b96252256b7754", + "historical_package": "research/five-stage-gen4-banks", + "historical_manifest_sha256": "99e202d9ffe5baf89e02796edbfc7095b2b227622eccf7b61afa01fd61aeb385", + "candidate_manifest_sha256": "f75a7190703e33d9d575fad294b0c9de0f4dcbe195e9f67557938077cd4dfd77", + "archive_sha256": "edc8731dc05a9bd275d6db60ed400e74ef82ac893d33d4603e5d2498c50b5533", + "changes": [ + { + "path": "MANIFEST.json", + "status": "modified", + "old_git_blob": "cf15e6982bddf102377b19ba51654ef7a1453b88", + "new_git_blob": "f921e2d70d4db935b21c34eb36d802e2d41d037c", + "old_sha256": "99e202d9ffe5baf89e02796edbfc7095b2b227622eccf7b61afa01fd61aeb385", + "new_sha256": "f75a7190703e33d9d575fad294b0c9de0f4dcbe195e9f67557938077cd4dfd77" + }, + { + "path": "NOTICE.md", + "status": "modified", + "old_git_blob": "816bce25a249171a211e9050b0ce25e065727a93", + "new_git_blob": "e61a36602a429382c01fa8e2e66298f5fa61ca54", + "old_sha256": "2784275e14c8164387ee984a60b06744094aea1ebd3246101990faa7f74080eb", + "new_sha256": "8bf55c9ed93c7be33e1931e0d0761abef84f9e87cd2e84fdcc46860e8b074f1c" + }, + { + "path": "PR-STATEMENT.md", + "status": "modified", + "old_git_blob": "f5492c4b2878367e27126755c56db7c3f3339dbc", + "new_git_blob": "71d6cdc26383ae75c89bb5f7a492b29065f8f73d", + "old_sha256": "ba70e873f04b00c1555b59b25390b14085972c541a5fffff5830c1259e6338c6", + "new_sha256": "ee22738a88886079e9bb7105cea7215186ca9502707d0312aa64a4e6f335c0f2" + }, + { + "path": "PROOF.md", + "status": "modified", + "old_git_blob": "14bade3a191127cb7ffce61d9d722c3e5ebd89f9", + "new_git_blob": "e6616b435377cdf225d4be13a1df603973a22049", + "old_sha256": "75cd7e51722ebcf826070aca4b289a72526d50264688d8c6bb298bf8a7dfef37", + "new_sha256": "8c6e1e5cab7add9021cf29036a5e6e8b90b11dc90bf71ce239fe049cd8464dfc" + }, + { + "path": "README.md", + "status": "modified", + "old_git_blob": "f5492c4b2878367e27126755c56db7c3f3339dbc", + "new_git_blob": "71d6cdc26383ae75c89bb5f7a492b29065f8f73d", + "old_sha256": "ba70e873f04b00c1555b59b25390b14085972c541a5fffff5830c1259e6338c6", + "new_sha256": "ee22738a88886079e9bb7105cea7215186ca9502707d0312aa64a4e6f335c0f2" + }, + { + "path": "bank_check.py", + "status": "modified", + "old_git_blob": "01122c82840ab316ca1131c658b65afe4d9997b6", + "new_git_blob": "1527c23f221eef2055b7c438b5cb88ebddd31cbc", + "old_sha256": "094549196d70d4504f2f189b4f7ae449fd3d01d083852b7d3d9258e9e6dcbf88", + "new_sha256": "e025a8b72a5b53b598d6c0df0b3395f94ddcde5d9a8ec1444af5e8844b6c0ea3" + }, + { + "path": "finite_check.py", + "status": "modified", + "old_git_blob": "4aa16fc59f31c8bf5255b5e409c630a584c7d0fa", + "new_git_blob": "01e67a71cc5c14cfeeb977776995ff52b65c20ae", + "old_sha256": "693a93308edcb44bc649b33a6ece1de4d93daefcead2eac36215d7c18730edbd", + "new_sha256": "1e51d4007eb839401f871179239ead75bdb7d2ddffe139db8014a25db636436e" + }, + { + "path": "portable_bit.py", + "status": "modified", + "old_git_blob": "b8dfa8b49d7445bc01ab83585337ecbf2267e86f", + "new_git_blob": "0729cd0075815b549b6c0f81822209f0d5d8aab4", + "old_sha256": "6fdb484f54c7b711e90affb44978584e95e0a6dd2b05e1351ed48aec190af1d5", + "new_sha256": "3d118c9904f7b28ac2c4cad199c10ec763adfc47f0725b43b7ed6f9dee3f31ee" + }, + { + "path": "scalar_check.py", + "status": "modified", + "old_git_blob": "cd33eefeaaf40af19e4c5c50eca5945746ad0ddc", + "new_git_blob": "3ea40001367fe8f52a52c94a37e59f5435a986b9", + "old_sha256": "bbc25d3df09bf0ce2cb92f623f46579b504b37a9447a144a6cd1cb8e63701b7f", + "new_sha256": "da3d46422afa4cd08ef3f303b65967ad222724be62e2a8da2e21d1086126f284" + }, + { + "path": "target-selection.json", + "status": "added", + "old_git_blob": null, + "new_git_blob": "ae709ae6a85f656de8a645a22a586e6d96905d99", + "old_sha256": null, + "new_sha256": "92a9228ffbd6a6b8506562c9e275afff13dc0e9c06cc29fb529154dc7f4b947b" + }, + { + "path": "target_transform.py", + "status": "added", + "old_git_blob": null, + "new_git_blob": "4203854d870b31a45317ee7d6e7e374dfd5d902c", + "old_sha256": null, + "new_sha256": "150634f980edc4a943e7ed456bf898968060ca6fb23517c909ee2461847bc29d" + }, + { + "path": "verify.py", + "status": "modified", + "old_git_blob": "06493572d41ff076dfddc1b068b8069b12205e3b", + "new_git_blob": "1af60e14b92b875c302fd716079b8df007c07555", + "old_sha256": "b06a583118061fec0c6523e10897eee98291f263b874f0d3f5fd9de5ef893238", + "new_sha256": "b96a8512587344683cb8c80f09d949b9ce956b66c865eedc08df277df2b84ef2" + } + ], + "historical_files": 113, + "candidate_files": { + "BANK-PROOF.md": { + "git_blob": "62560a4fb9c634c7d3684b8df657c30b8c750efd", + "sha256": "bbc328e05848a211c981288514380a4ba12fddaed16c9d23328b5764502be411", + "source": "historical_package" + }, + "LICENSE": { + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "source": "historical_package" + }, + "MANIFEST.json": { + "git_blob": "f921e2d70d4db935b21c34eb36d802e2d41d037c", + "sha256": "f75a7190703e33d9d575fad294b0c9de0f4dcbe195e9f67557938077cd4dfd77", + "source": "update_archive" + }, + "NOTICE.md": { + "git_blob": "e61a36602a429382c01fa8e2e66298f5fa61ca54", + "sha256": "8bf55c9ed93c7be33e1931e0d0761abef84f9e87cd2e84fdcc46860e8b074f1c", + "source": "update_archive" + }, + "PR-STATEMENT.md": { + "git_blob": "71d6cdc26383ae75c89bb5f7a492b29065f8f73d", + "sha256": "ee22738a88886079e9bb7105cea7215186ca9502707d0312aa64a4e6f335c0f2", + "source": "update_archive" + }, + "PROOF.md": { + "git_blob": "e6616b435377cdf225d4be13a1df603973a22049", + "sha256": "8c6e1e5cab7add9021cf29036a5e6e8b90b11dc90bf71ce239fe049cd8464dfc", + "source": "update_archive" + }, + "README.md": { + "git_blob": "71d6cdc26383ae75c89bb5f7a492b29065f8f73d", + "sha256": "ee22738a88886079e9bb7105cea7215186ca9502707d0312aa64a4e6f335c0f2", + "source": "update_archive" + }, + "UPSTREAM-PR234-NOTICE.md": { + "git_blob": "5f8fbb25c12781420284bc220a041592619e27c0", + "sha256": "ce978c8dfc8a2b36eed7a53014b1a792248b22ef4cee3edd8adab825a571c429", + "source": "historical_package" + }, + "UPSTREAM-PR234-PROOF.md": { + "git_blob": "dbd880696772b68c63af15336a4fe749550f1146", + "sha256": "c9722b07256758cd3b307dd46689f99984c66e16c3dd934f9c34e551620bfc0f", + "source": "historical_package" + }, + "bank_check.py": { + "git_blob": "1527c23f221eef2055b7c438b5cb88ebddd31cbc", + "sha256": "e025a8b72a5b53b598d6c0df0b3395f94ddcde5d9a8ec1444af5e8844b6c0ea3", + "source": "update_archive" + }, + "bank_template.py": { + "git_blob": "d2bd3c01654f23a51b08097c6f88775cef4eedbf", + "sha256": "ca97c34524b409621336c0d4046f26e8da156f4b657c9d94463d8025ddfdbb4a", + "source": "historical_package" + }, + "base_two_moment.py": { + "git_blob": "14a90fa0e788217856f070382c9e61bd7c603c61", + "sha256": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098", + "source": "historical_package" + }, + "code/complex_basis.py": { + "git_blob": "8c400798a5f25d366747b35cb55e985222039083", + "sha256": "52d68781eaf6d9decf02446a532a7336fcf15924a9f6781ba0833d038decb9f8", + "source": "historical_package" + }, + "code/complex_labels.py": { + "git_blob": "1f27d6de34a3695f02a268e4884cd3b7545e31be", + "sha256": "ff5d5e914ef1be0f0cc30283a1ee39089b77e4b572f09543e7313d126bd26256", + "source": "historical_package" + }, + "code/complex_scalars.py": { + "git_blob": "771057b56761363a8fc208728e8557c644829aa2", + "sha256": "fa035447c1f3a5e878dfc18a900942aa180d8bfde03cdce2d21d9bf8b8409429", + "source": "historical_package" + }, + "code/complex_splice.py": { + "git_blob": "11373d1d5720bd705cc187228aa4388c75912b09", + "sha256": "ed8f7f55530bab64e25b98ee614e1152ded8a6259c48d32b3ae26bab4b93848c", + "source": "historical_package" + }, + "code/geometry527.py": { + "git_blob": "1e9f9c0ff7785461fb8e13d47ecc7b2e63c2e6d4", + "sha256": "733a0f4bc946be5662c73e62ca287ef9ca9bc000e5de090947776c40a8ffc83f", + "source": "historical_package" + }, + "code/global_lowering.py": { + "git_blob": "3712adf522fed134fef6bd1249cae23073dcad79", + "sha256": "12e89150ef633d027d842378caa113a8240225d3dfdaac5177448c061e126206", + "source": "historical_package" + }, + "code/physical527.py": { + "git_blob": "82a1707f49ff01ce85af791c51203e32e051081e", + "sha256": "e5a1730f498ad355002f26de8881a02ad2fac119657ebdaa85017047e0cccdb1", + "source": "historical_package" + }, + "descent-selection.json": { + "git_blob": "786ca461303e0f4cdfa676d927853b0fe4dbefa9", + "sha256": "61341527ada3112a5db74b66b23994bc9786ae0d55dd657aea359c9f5c45bde4", + "source": "historical_package" + }, + "descent_transform.py": { + "git_blob": "9d6a8a797c4681c3399bec3232e8276da00f8760", + "sha256": "7bbaa371b04d2f9fcfab70a75594de2a59712cd770780e0172e41482fc5165fe", + "source": "historical_package" + }, + "finite_check.py": { + "git_blob": "01e67a71cc5c14cfeeb977776995ff52b65c20ae", + "sha256": "1e51d4007eb839401f871179239ead75bdb7d2ddffe139db8014a25db636436e", + "source": "update_archive" + }, + "gen4bit/NOTICE-PR200": { + "git_blob": "c2d7935d7f45a6878dc547d301c0f43abbb2fa90", + "sha256": "9e82089424092c1dabc2341a09ead255633d78c90dbdc199c4336ca1c0f3bdf4", + "source": "historical_package" + }, + "gen4bit/README.md": { + "git_blob": "911da50b1c5ed9ee77aca3e2c1ee6c5712872690", + "sha256": "7e037532a7469053c590164e9b347e90c9d21968d82920c8bacd73eaad1a6af0", + "source": "historical_package" + }, + "gen4bit/bit/base_word.py": { + "git_blob": "044f278fbe6a64303339de41a8643d444e4b5e9d", + "sha256": "9fe3a81b7561d2b09c086f63fac4626e88a32369ef8bc5579c94878de1218a89", + "source": "historical_package" + }, + "gen4bit/bit/word.py": { + "git_blob": "6b8d96043a541ffe58f4c95fa047e1291823d465", + "sha256": "85822e9cca5b1b2335c3704a3df2f3c6ef01e42d8328daacb33701d30cee80ab", + "source": "historical_package" + }, + "gen4bit/producer/data/arcs_p12.json": { + "git_blob": "983973aa70a6423dd815febe711b70d7a52d3d1b", + "sha256": "14c5453df6f0f00f09277a9546a58a87f9a3251bf7077d2bf8251a692fda1852", + "source": "historical_package" + }, + "gen4bit/producer/data/local_design_p12.json": { + "git_blob": "66ce6682bb17e6d3c29b8d461b0d2a92077abb5f", + "sha256": "d4ceb6bff765b9332a36735d626decc178415394fc8d8d1f7135f80a87829320", + "source": "historical_package" + }, + "gen4bit/producer/data/pair_module_p12.json": { + "git_blob": "57809df44bafe13271ce3b073af849af972319e7", + "sha256": "3c2fece831349f502aba9cf30a45cf5f9364571a659506e1bdfc4e74a879bb15", + "source": "historical_package" + }, + "gen4bit/producer/data/qmod_p12.json": { + "git_blob": "22bb0927cf1c6e4635cc92391a7e316d5688e0cc", + "sha256": "cad452e60c14a18887c32064e453b51992fbe0a1b9d3582017b8263bd8b2b62f", + "source": "historical_package" + }, + "gen4bit/producer/descent.py": { + "git_blob": "6bdafeb1db0e4275921e615f775ad143140020e8", + "sha256": "5284b4ad26ca6472d82d5ad1a5c1e470cb60696ff90adb1fee3922e2cc845ca5", + "source": "historical_package" + }, + "gen4bit/producer/make_physical.py": { + "git_blob": "a6f79038edcb5d45fd4eae4217373d8b02b6ca0d", + "sha256": "7af67360f14e4bae1535a5040f4dac60b3796ce6d9e6c92b9454ff2e33ab3e04", + "source": "historical_package" + }, + "gen4bit/producer/paired_cube_bit_word.py": { + "git_blob": "7b0d575f7ecf47e3b963d2f12ff580f0d0ea5a91", + "sha256": "7d21f1c4071d9b633b2a0349837fdc688cf01a271b4ee9e0323ec2a466d27965", + "source": "historical_package" + }, + "gen4bit/producer/regenerate.py": { + "git_blob": "aacaae266fc90845bb9b4fd07e21ec9d0691fe1e", + "sha256": "1d7817e6fc324d393bb749d35b57456ccb99716668fb472cbdf5d968c07aecef", + "source": "historical_package" + }, + "gen4bit/references/pr168-v4/SOURCE.json": { + "git_blob": "c57edcae252edc2fae5e1c6c6f916ed75e3b0dc1", + "sha256": "21a412177c9309d89472aabf4c67618d7a546811f7e68a5904304ae46a98d27c", + "source": "historical_package" + }, + "gen4bit/references/pr168-v4/research/paired-cube-bit/check_paired_cube_bit.py": { + "git_blob": "69d535a6c2e227a81d3396abf6fde2cbe2a6f629", + "sha256": "4d7c86cd999a1519e0dfb6dcf33a8f26e442a353c3665a0f06881216a260fbf3", + "source": "historical_package" + }, + "gen4bit/selected/bit/frames_p12.json.gz": { + "git_blob": "7d4d9858a97fc1aa6fe706f9c7763470605da1c2", + "sha256": "9cff6201bea778916d7ef5288fb3a0fca9893286c820ec0cb040472596f3af86", + "source": "historical_package" + }, + "gen4bit/selected/bit/graph_p12.json": { + "git_blob": "c3ae30feddb314d740b9c7aec3554985f48c31bb", + "sha256": "99b19c76100a5709a113a5d6da99fef3071616baea3e79080a54ca15f288882d", + "source": "historical_package" + }, + "gen4bit/selected/bit/kchron_p12.json": { + "git_blob": "f39b02e3f7854304b959c9a78664f178820e81e2", + "sha256": "4ce723bbfd8ec0a0652967c874ffc9ff2e8f24bf3af0df8344861db3e1b6c205", + "source": "historical_package" + }, + "gen4bit/selected/bit/profile_p12.json": { + "git_blob": "da422014b7215eaff452893f18b7125d751a8f9a", + "sha256": "aa7bbfadbb1321fdd4902521c042e370463b9afeb4b05c4e4ae372574d6223bb", + "source": "historical_package" + }, + "gen4bit/selected/bit/word_p12.json.gz": { + "git_blob": "6db28abe958c1ace2f25f0f8a96af9fe24047145", + "sha256": "a28a2b6e1ec6f6ea7d3f11327b65a1429243cff26ff61b9a7d2c56a6c29d80c1", + "source": "historical_package" + }, + "inputs/complex/LICENSE": { + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "source": "historical_package" + }, + "inputs/complex/NOTICE": { + "git_blob": "63aa295646734f62c4270e653811530f9a570d3a", + "sha256": "9419dd03a2f52cf8bdfc4d18216ce29f263ab583b27f01ced8e420985bcb7c81", + "source": "historical_package" + }, + "inputs/complex/gcert1-p11-pr193.json.gz": { + "git_blob": "a98026a72f574fce17edd94bcaff10e15a314736", + "sha256": "15251deb0c11e0504d7b297c9786818888a93f08b92b03c6c122784b70488633", + "source": "historical_package" + }, + "inputs/complex/retained/FINITE_BRIDGE.txt": { + "git_blob": "c1a88436113a1351f80c72bd08f6406ed5faa51d", + "sha256": "66d8f4ea8752abd89952d6674a636575a0db16e18b1c16e293f48f64242f0c46", + "source": "historical_package" + }, + "inputs/complex/retained/compact-control-layout.tex": { + "git_blob": "16f4d233471a7d189163ae7e7902becadecbba64", + "sha256": "2bc28e50f3eb092195294cafa81213e520f6d42e7935e9905ad8a6199e2a7c87", + "source": "historical_package" + }, + "inputs/complex/retained/compact-control-movement.tex": { + "git_blob": "06b6a9ef24245ac7b724c53a204635415b402357", + "sha256": "b963c3d2f4e1b7059aa289bb4b4ac89b688920bcf42f5b20d7698cdef0132cc6", + "source": "historical_package" + }, + "inputs/complex/retained/copied-centers-assembly.tex": { + "git_blob": "b0c69166c3048d27518355995e3e5b622722c696", + "sha256": "00117892971ae766188ace0af03030c44164fda105e42b70d84f52c3339a7dcb", + "source": "historical_package" + }, + "inputs/complex/retained/copied-centers-lemma.tex": { + "git_blob": "8933aaf508aa9d4c75ba1290913e02f6868d351d", + "sha256": "d0ce6d3d504996aadb098227885224e48df46101daec8893523a0a8b7364d8fe", + "source": "historical_package" + }, + "inputs/complex/retained/endpoint-gauge-complex.tex": { + "git_blob": "907a0ceda8df0317ddc7f2b71df5af2aa4d47dfc", + "sha256": "dfee33b0281e5551bb6927f757ff0240abade60ae1800f715afd88853ae0191e", + "source": "historical_package" + }, + "inputs/complex/retained/general-clifford-frames.tex": { + "git_blob": "0367eeb005298601f28a673861d6f71bf1d0ebbb", + "sha256": "c9bb9655b594583c6b4bab8cb485233f1d1e588f83858cf1e4c3530cee8fed54", + "source": "historical_package" + }, + "inputs/complex/retained/stopped-product-complex.tex": { + "git_blob": "4a9037137cd3158dbeca6d9e3b1881a599ebfcb5", + "sha256": "4738089103a4b263b3b0ef458f5ef35519c696f1ea871ae79e508d3720f5870a", + "source": "historical_package" + }, + "inputs/complex/source-pins.json": { + "git_blob": "5cb04b0c7275010f308d751666504b19d7fe6b91", + "sha256": "de0daf6847185d7a6911535e3012c1a91de1e32b5da8204beec26b37523ad569", + "source": "historical_package" + }, + "inputs/complex/sources/Work__Bridge__Cert.lean": { + "git_blob": "f7bdc3d903341a9546056cde124d642e2677318b", + "sha256": "5c24746a6330907b9b37d6064095035a58575d64ce793d6d7c9881121fdc3980", + "source": "historical_package" + }, + "inputs/complex/sources/Work__Bridge__Net.lean": { + "git_blob": "204f6d9cf902c85900f237bd99a23774e9a3f81b", + "sha256": "cf7d7d330b1bffe2e66712c873e647b13dc32db1ccfc0e0f4cd62ee6caf584f0", + "source": "historical_package" + }, + "inputs/complex/sources/Work__Carrier__Live.lean": { + "git_blob": "b8306527d64ae06271c6aa55c5e0b3ded85c651c", + "sha256": "6d0649eb62589e66057f044e1e2103fc42f3f57a1498f82a26565bd8eb4026d0", + "source": "historical_package" + }, + "inputs/complex/sources/Work__Carrier__Phases.lean": { + "git_blob": "305da15b5d129959a0696e2031289eea91ec1813", + "sha256": "71dc3dda23dfe510d5d53cbada3a6c540cd1dc2825503fda618a5bd6cfc3e812", + "source": "historical_package" + }, + "inputs/complex/sources/Work__Fourier__Main.lean": { + "git_blob": "9aa06b5bf28a2380ef9d54a0785ac2369f6012e4", + "sha256": "2e8e88efd4dcbdf0b1a6e39ce7eea8c5fd5ffee2faf360a8c0c9cba84c0e4ef3", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Chain__Geom.lean": { + "git_blob": "eb4490af8b0f5b97984d9dbdf345d86fe65d02c7", + "sha256": "c302f5834287421f11f3b0da7112fcde876cbc702896f2af4145b2d72ee393a2", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Chain__InvThm.lean": { + "git_blob": "d69fcb4992778bcd2d12596e365ee8483aa538a2", + "sha256": "ade7e7873da75ca63a4b5ce2f562dde9c12bfbb69d87d7ae831039ff790e5adb", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Chain__NetCert.lean": { + "git_blob": "6336ba076607f4229c58e51b01f35b8457effb88", + "sha256": "22ae34809466b4ac2a2c5cdde526f51ff246f5189f7c142b38aa4c0dcffb04a4", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Chain__NetDef.lean": { + "git_blob": "c13042eb43328f9771a5f85e83edb59810f3a006", + "sha256": "6e17a68b1e988969f6eb77000028f7ed877e687b8ad3976ec1707fcfe1d2f520", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Chain__NetStage.lean": { + "git_blob": "670f4c6a84b3453dd0b1bc0879fff3ecd9410919", + "sha256": "c122bc01392a6fdcc0bee918fed81804d3c9b1d3e071016dab65a4ed804ef0b6", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Chain__Phased.lean": { + "git_blob": "e68c42377f4fd0d0352ba697357d05f60333c8dc", + "sha256": "0de429c80231334f1ce92575c1e8ac382ca2d5e7d956767b547639a8941d9a8c", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Chain__WinB.lean": { + "git_blob": "951edde5cf5fdfb1dd5f7902499f3ccab961bf4a", + "sha256": "c33ec3fce09c0971c32ddcbb86d9383ffbe4c6d05cf36f20460005e6547bb845", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Data__B2Gp193Main.lean": { + "git_blob": "d7ecfebcea804af8209a0db3d89caa9ed364ea7a", + "sha256": "cb61f304da51f1dd0a2ec25bca4b63eb095eeb2863289e1e2bdee7c82beff48b", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Data__Glue.lean": { + "git_blob": "c6cbac38e3a2fbabac74610519e26fcc065f7ff5", + "sha256": "d5314f2b93a7f0e1c949fb502331825bfc6d9d8762d35f865443e7c95b6c7ef7", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Data__InstB2Gp193.lean": { + "git_blob": "9b9925ce268a9f757fd44913140a57df95315769", + "sha256": "9587ddb9961f44938032b609307ab91c0b0e757e3991f1ad95480dd50fd4f72b", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Data__P193Cert.lean": { + "git_blob": "3c3250279e66b56c9fee8a12c265ae2780ce4761", + "sha256": "d92ee6889be4753fc99f467bd84039743325123a1165128378b9c906a04f2703", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Data__P193Price.lean": { + "git_blob": "eeed011d64482adbdf0d6ff48a7c395a7252d57a", + "sha256": "0299bcd0fe255960eec682eef0f045f7e5cb1e4711af2aab4393526eae2caea3", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Data__P193ScalOK.lean": { + "git_blob": "3539192ac1d3a51641f7ba08fa06a8659b12bc0b", + "sha256": "479434815822e98f015e335361089c3788d00dc3dd39c2944f75410aa0c158fe", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Data__RateB2Gp193x.lean": { + "git_blob": "df563cde73a8f942e9c90189261dd6e8482d40f1", + "sha256": "6b40cac1481c931d47b1a092e382d04716ede0e785c492a2f2983e886a257c3f", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Data__Raw.lean": { + "git_blob": "499fa67e88ebfe0ad777081cb61def3f74de81ba", + "sha256": "aba94a004c94dcae7cf3047c88a6da9561555f4ebe8ab92e299e6ce09ee7aa66", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GCert__Data__SolutionB2Gp193x.lean": { + "git_blob": "0392e1f05bb89cca472c976391a649418dde186e", + "sha256": "45c768c9d71a7cc18bd6db74cb036db880d89580ca60557bb4a492280296b169", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GFrame__Engine__Adapt.lean": { + "git_blob": "24e261ad0862ba778f0e7f00d48756865b7f4eb8", + "sha256": "feec0a3828867968a5c7c2c30b86ed70449abc3c660a60ada67203a75bae2ef7", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GFrame__Engine__Letters.lean": { + "git_blob": "2eca6e713bfd47449b872a0462857806861be9d5", + "sha256": "34906dbf5ae16b5174db00b4881a5cc1d2e583b8c8806db6523a5e2f86565f09", + "source": "historical_package" + }, + "inputs/complex/sources/Work__GFrame__Engine__Level.lean": { + "git_blob": "6bd7cfa0c3f34bbd04fc445eceae0cc4d4c567fc", + "sha256": "80fb3daa9a45de0ed6da570eb4476b9104734be65d0116f58bcfcbcd67f771d0", + "source": "historical_package" + }, + "inputs/complex/sources/tools__gx__ORIGIN.md": { + "git_blob": "e28b355d0a271da6c8c7da8b6d68451817378bf1", + "sha256": "6ba897a9495ddadcf8558b93133fdfaf66fc35ce7fa2c53e2d5667335c315e0b", + "source": "historical_package" + }, + "inputs/complex/sources/tools__gx__gxbind.py": { + "git_blob": "fcb625619cb07a9be9594422357786ca6e3c4add", + "sha256": "9c9dcfac47f0535bf3aa8ebf7c662cdef0ebda50a9f0a9282b8f3cf34809f835", + "source": "historical_package" + }, + "inputs/complex/sources/tools__gx__gxconv.py": { + "git_blob": "49ebb65973a2403bb22aa32692762cd0522a0287", + "sha256": "dab7fec9f44c2d368ed334055d7126e202017feb46e41a8d86e2d998720f67c2", + "source": "historical_package" + }, + "inputs/complex/sources/tools__gx__gxcore.py": { + "git_blob": "3e3f0a3076f3c326e7833c74eceecb3436dd3185", + "sha256": "eb972c06fe8c322db2d9a8d9a7d05596e8f40c4ca8e5f42eb6df3c7361b5d517", + "source": "historical_package" + }, + "math_check.py": { + "git_blob": "e3453703bcb71d836c79a972c1069fa94287b4c0", + "sha256": "706d9e0a2e2092393914809109be39012c0182edf4eb1bb76bf05f9e51fde713", + "source": "historical_package" + }, + "moment.py": { + "git_blob": "1e43aaeaca1b9d1ff40b8805ca7ae3e6a219c392", + "sha256": "9d465c716c6b910ff66e1453e3bf0057608a787b5f5361be93781f42cb3370f7", + "source": "historical_package" + }, + "notices/PR210-coordinated-crossover-NOTICE": { + "git_blob": "d08cb66ac79144aa64d4fc2bfdfadd98ac3af624", + "sha256": "9fc5561c0995892dbdde777c713899486920c32d3562392f5f72377a4953bf98", + "source": "historical_package" + }, + "notices/PR230-NOTICE": { + "git_blob": "bc1cfc52a13bdaa887fae71017ab7df10eb14a90", + "sha256": "7dfbad087ee49b74fd5075d517eaa263c5dd3d4fbd4c69bfba34ee1cb55e837f", + "source": "historical_package" + }, + "notices/PR230-PROVENANCE.json": { + "git_blob": "ff39579387f862cc077309d4186ee188f0ae56ba", + "sha256": "19957e28a8ad26281bfe8bfaf8ae16191be53e729a8870a6154671b3384959d4", + "source": "historical_package" + }, + "notices/README.md": { + "git_blob": "7af7caa733abae0fd22e726a373b7a91f1f59bfa", + "sha256": "a4c288228cf8360d8d04c62b0f51177de5682d1f5d3bae341e6b850af766c26e", + "source": "historical_package" + }, + "notices/base-bit-PR200-PR202-NOTICE": { + "git_blob": "ba5ea80dd7e359d44cf1ffae63a7790f6e507739", + "sha256": "c9850418622aea8d1382a230306c940947b5da818f4854b4b272ed60cf239f6c", + "source": "historical_package" + }, + "notices/source527-loader-NOTICE.md": { + "git_blob": "47090d6e93ecf48e71019bd52b045bed31b5f889", + "sha256": "ee632728cc4d89565292d288f8289f483ac794b5d02cc6e42c2b2c43c43ff1d8", + "source": "historical_package" + }, + "outer.py": { + "git_blob": "43007488ad2c43187c77cc6798beff8b1cd76ad2", + "sha256": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c", + "source": "historical_package" + }, + "parity_transform.py": { + "git_blob": "30528550be3deaebd0e187e32fa6ecd1e72bba62", + "sha256": "9ed3ff2767c046d11aa1be248eaba93755740131745f673ad9d26a3e77e7b02a", + "source": "historical_package" + }, + "portable_bit.py": { + "git_blob": "0729cd0075815b549b6c0f81822209f0d5d8aab4", + "sha256": "3d118c9904f7b28ac2c4cad199c10ec763adfc47f0725b43b7ed6f9dee3f31ee", + "source": "update_archive" + }, + "portable_complex.py": { + "git_blob": "c068be3e1cb9aee54feed200d41d997c8081fed1", + "sha256": "797e144c0040d78a4731a6eaa61c0edb9803a08462f885ed014cbca9d9991d82", + "source": "historical_package" + }, + "prepare.py": { + "git_blob": "952bd727b46b9acd49fe3fae8f20b8951b22f1e3", + "sha256": "00b13cb18e2d1dd26f207a20a7183b9e357a92a9b2906371e6fae9cb8cc197b3", + "source": "historical_package" + }, + "prime_check.py": { + "git_blob": "052d2fe6cbc4c71569c4f9b7e0766f3ff87a3355", + "sha256": "0787711ebb7336f1b5800afa3e97ab664839d32ffb719ebd64e6ae0ca0ce592d", + "source": "historical_package" + }, + "prime_witnesses.py": { + "git_blob": "7f16d930302ae879c562dd58e085d9747fcac077", + "sha256": "98cd03bc9582e7bd0ab194c191ea8eea940539e510051443ab9fd3e572a364ab", + "source": "historical_package" + }, + "proof/FINITE_BIT_ACCOUNTING.md": { + "git_blob": "42a585d742660f9ed44ebd3ca2a9d1e0832bb0be", + "sha256": "602923520af184670170bf159fde7b4c72e79a72570eddd7746b7c97bc51fc5b", + "source": "historical_package" + }, + "proof/INTEGRATED_PROOF.md": { + "git_blob": "c624da6c5c1f8e44c8ecda24af477d11dfee8e12", + "sha256": "cff22391e71a50bad27a1e832d5c0a2c8b2446df55adb1297c8b1485b3761257", + "source": "historical_package" + }, + "proof/PARITY-CONTRACT.md": { + "git_blob": "fad6150b1f9987280f8e2dc72e3418eb85f3d8e6", + "sha256": "a9246be656e31f1a21d5ec714e002f51be0aa07c36e1528066a25b2c7a02db91", + "source": "historical_package" + }, + "proof/README.md": { + "git_blob": "19751671be8d4a206c60875f1ba4b7ff423edb89", + "sha256": "5f40cb6dda3992f98ffc43159af1be080bd6c18411bc7d02464f230993f3074f", + "source": "historical_package" + }, + "proof/copied-centers-lemma.tex": { + "git_blob": "8933aaf508aa9d4c75ba1290913e02f6868d351d", + "sha256": "d0ce6d3d504996aadb098227885224e48df46101daec8893523a0a8b7364d8fe", + "source": "historical_package" + }, + "proof/primary/03-motifs.tex": { + "git_blob": "cdb0ba527aa8df5d57c151183fd3893c1a7e21ab", + "sha256": "ed76761194988a01af77ead0ea6469cb5dcd29690ab985a0b5a4006b0f2b69bb", + "source": "historical_package" + }, + "proof/primary/LICENSE": { + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "source": "historical_package" + }, + "proof/primary/PROVENANCE.md": { + "git_blob": "bebdb72910e6a1af8535b206e1d1e9aa1637a562", + "sha256": "dd9054c58aa92c44b0ef5f691ad4dc52b8ead2f20a9843d4399d6c300d616023", + "source": "historical_package" + }, + "proof/primary/UPSTREAM-README.md": { + "git_blob": "c8cb3c3857907bf3465017b9f7ef1add4df5c29b", + "sha256": "8d1ceff898a4e0e681679f91c4def485820be9e99f04e4861f2ce601a364723e", + "source": "historical_package" + }, + "proof/three-stage-cover-bit.tex": { + "git_blob": "f05225d21f92cf8cef21b6e12601d5b4d61991f0", + "sha256": "47123a756f823c83a0d48cca2bf5add6472cd88410b13aed345e70c8834fb511", + "source": "historical_package" + }, + "proof/three-stage-cover-rows.tex": { + "git_blob": "590da4b892a08b9d5182fb3d8a983c6239dd27db", + "sha256": "6ad97a5cd7d6aecf978a81226e1c2763d37840caca130c61f3bf5c4ac111c5c8", + "source": "historical_package" + }, + "raw_ledger.py": { + "git_blob": "fc3713f25c9698ad9a46b7afcfa4e32c4c1a54ad", + "sha256": "6f2cc85faa35cd9f44e8ad542474bd560f325d633a43da6cb4c22377904f9066", + "source": "historical_package" + }, + "requirements.txt": { + "git_blob": "1ca5fd06160543f8bd736f1b51db6f42372c66f4", + "sha256": "25f9f1fb1988b230147a1d3092d34e09c069eb7a6c6d6df46b3973b9f2d36efc", + "source": "historical_package" + }, + "scalar/word.py": { + "git_blob": "95b9affd44ba9c50a4906f074457701f862f44ce", + "sha256": "e675d4eb9d90ff0b44279fae0b46f1a8b39f65421cc38454b70a6b75d0e10b42", + "source": "historical_package" + }, + "scalar_check.py": { + "git_blob": "3ea40001367fe8f52a52c94a37e59f5435a986b9", + "sha256": "da3d46422afa4cd08ef3f303b65967ad222724be62e2a8da2e21d1086126f284", + "source": "update_archive" + }, + "target-selection.json": { + "git_blob": "ae709ae6a85f656de8a645a22a586e6d96905d99", + "sha256": "92a9228ffbd6a6b8506562c9e275afff13dc0e9c06cc29fb529154dc7f4b947b", + "source": "update_archive" + }, + "target_transform.py": { + "git_blob": "4203854d870b31a45317ee7d6e7e374dfd5d902c", + "sha256": "150634f980edc4a943e7ed456bf898968060ca6fb23517c909ee2461847bc29d", + "source": "update_archive" + }, + "verify.py": { + "git_blob": "1af60e14b92b875c302fd716079b8df007c07555", + "sha256": "b96a8512587344683cb8c80f09d949b9ce956b66c865eedc08df277df2b84ef2", + "source": "update_archive" + }, + "virtual_check.py": { + "git_blob": "8538bd1297d61308cda6e6e275f0dd1fff91698b", + "sha256": "155144478a5c45d630c1b0d43cadbeb53b96306270fa4e0ad8c4d403d9045971", + "source": "historical_package" + } + }, + "scope": "Exact source reconstruction only; no mathematical acceptance inferred.", + "unchanged_workflow": { + "path": ".github/workflows/five-stage-gen4-banks.yml", + "sha256": "dc53e810a3bd16a38ac3681a39a23b0f61b1b5d6803d95ef6e4251860a03f448", + "git_blob": "4685189c841bc3902996f4d1465367032c43b14b" + }, + "context_sources": { + "docs/research/community-pr279-integration.json": "e790e42bbd0e57e3be92191309d3489ec91b738239622e69759604212b2d0f29", + "research/pr-reconciliation-20261012/content-comparison.json": "6c0fd53892c8d82a2c62f9bf1c589d5bd09309021bd4e579f8eab8f3575f484f" + }, + "integration_base_commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261" +} diff --git a/research/pr279-target-prefix-reconciliation/VALIDATION.md b/research/pr279-target-prefix-reconciliation/VALIDATION.md new file mode 100644 index 0000000000..1f45252c92 --- /dev/null +++ b/research/pr279-target-prefix-reconciliation/VALIDATION.md @@ -0,0 +1,42 @@ +# Validation receipt + +Research base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +Final integration base: `7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261`. +Environment and mathematical execution receipts are in `EVIDENCE.json`. + +The unmodified later PR279 verifier completed all nine mandatory stages in +1,096.765 seconds. It passed its target-prefix omitted-setup control, 11 scalar +controls, six prime controls and nine mandatory-stage omission controls. +The exact command actually executed is recorded in `EVIDENCE.json`; the +public `--replay` wrapper reconstructs the same source before invoking it. + +After rebasing, the source package, workflow and immutable context consumed +by this contribution were compared across both bases; there were no changes. +The executed source, the wrapper's extracted source, and the current +reconstruction all contain the same 115 files byte for byte. The completed +replay's 723,357 instruction sextuples match the stored canonical fingerprint. +This verifies that the completed replay applies to the final integration. + +The following checks passed on the final integration base: + +```sh +python -X utf8 -B research/pr279-target-prefix-reconciliation/verify.py +python -X utf8 -B -I -O research/pr279-target-prefix-reconciliation/verify.py +python -X utf8 -B research/pr279-target-prefix-reconciliation/test_verify.py +python -X utf8 -B -I -O research/pr279-target-prefix-reconciliation/test_verify.py +python -X utf8 -B -m unittest discover -s tests -p test_pr_reconciliation.py +python -X utf8 -B scripts/verify_pr_reconciliation.py +python -X utf8 -B scripts/verify_selected_result.py +``` + +- Companion source/evidence checks and 13 tests pass, including under `-I -O`. +- All 14 repository reconciliation unit tests pass. +- The reconciliation checker validates all 535 ledger entries. +- The selected-result checker validates + `1661202643272239/1000000000000000000` (#741 with #589). +- Source extraction to a new directory outside the repository succeeds. + +No selected construction was changed, and no cold selected-frontier replay, +Lean build, repository-wide `make verify`, or new remote CI execution is +claimed. Historical source CI is identified separately in `SOURCE-CI.json`. +Maintainer acceptance and the disposition of PR279 remain pending. diff --git a/research/pr279-target-prefix-reconciliation/replay-evidence.tar.gz b/research/pr279-target-prefix-reconciliation/replay-evidence.tar.gz new file mode 100644 index 0000000000..88700c018d Binary files /dev/null and b/research/pr279-target-prefix-reconciliation/replay-evidence.tar.gz differ diff --git a/research/pr279-target-prefix-reconciliation/source-update.tar.gz b/research/pr279-target-prefix-reconciliation/source-update.tar.gz new file mode 100644 index 0000000000..54dbfece9d Binary files /dev/null and b/research/pr279-target-prefix-reconciliation/source-update.tar.gz differ diff --git a/research/pr279-target-prefix-reconciliation/test_verify.py b/research/pr279-target-prefix-reconciliation/test_verify.py new file mode 100644 index 0000000000..96398ee034 --- /dev/null +++ b/research/pr279-target-prefix-reconciliation/test_verify.py @@ -0,0 +1,144 @@ +"""Source and evidence confusion controls for the exact PR279 reconstruction.""" +from copy import deepcopy +from array import array +from pathlib import Path +import importlib.util +import gzip +import io +import json +import tarfile +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('pr279_reconciliation', HERE / 'verify.py') +check = importlib.util.module_from_spec(spec) +spec.loader.exec_module(check) + + +class SourceControls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.source, cls.files = check.collect_candidate() + + def test_exact_candidate_and_schedule(self): + check.validate_candidate(self.source, self.files) + result = check.check_selection(self.files) + self.assertEqual(result['targets'], 880) + self.assertEqual(result['setup_restore_additions'], 1320) + self.assertEqual(result['five_stage_paid_call_delta'], -1100) + + def test_missing_new_transform_is_rejected(self): + files = dict(self.files) + del files['target_transform.py'] + with self.assertRaisesRegex(ValueError, 'Missing or additional'): + check.validate_candidate(self.source, files) + + def test_old_transform_receipt_cannot_replace_current_source(self): + files = dict(self.files) + files['verify.py'] = (check.ROOT / check.HISTORICAL / 'verify.py').read_bytes() + with self.assertRaisesRegex(ValueError, 'Changed candidate file: verify.py'): + check.validate_candidate(self.source, files) + + def test_changed_selection_and_extra_files_are_rejected(self): + files = dict(self.files) + files['target-selection.json'] += b' ' + with self.assertRaisesRegex(ValueError, 'Changed candidate file'): + check.validate_candidate(self.source, files) + files = dict(self.files) + files['unreviewed.py'] = b'print("PASS")\n' + with self.assertRaisesRegex(ValueError, 'Missing or additional'): + check.validate_candidate(self.source, files) + + def test_source_head_cannot_be_relabelled(self): + source = deepcopy(self.source) + source['candidate_head'] = check.REVIEWED + with self.assertRaisesRegex(ValueError, 'Unexpected source commit'): + check.validate_candidate(source, self.files) + + def test_omitted_restore_charge_is_rejected(self): + files = dict(self.files) + selection = json.loads(files['target-selection.json']) + selection['groups'][0]['extra_setup_restore_additions'] = 3 + files['target-selection.json'] = json.dumps(selection).encode() + with self.assertRaisesRegex(ValueError, 'Unpaid setup/restore'): + check.check_selection(files) + + def test_reconstruction_preserves_every_byte_and_refuses_overwrite(self): + with tempfile.TemporaryDirectory() as tmp: + destination = Path(tmp) / 'source' + check.reconstruct(self.files, destination) + self.assertEqual({p.relative_to(destination).as_posix(): p.read_bytes() + for p in destination.rglob('*') if p.is_file()}, self.files) + with self.assertRaises(FileExistsError): + check.reconstruct(self.files, destination) + + +class ArchiveControls(unittest.TestCase): + @staticmethod + def archive(names, symlink=False): + buffer = io.BytesIO() + with tarfile.open(fileobj=buffer, mode='w:gz') as archive: + for name in names: + info = tarfile.TarInfo(name) + if symlink: + info.type = tarfile.SYMTYPE + info.linkname = 'target_transform.py' + else: + info.size = 1 + archive.addfile(info, io.BytesIO(b'x')) + return buffer.getvalue() + + def test_duplicate_member_is_rejected(self): + with self.assertRaisesRegex(ValueError, 'Duplicate archive member'): + check.archive_files(self.archive(['a.py', 'a.py'])) + + def test_paths_and_symlinks_are_rejected(self): + for name in ('../a.py', '/a.py', 'C:/a.py', 'a\\b.py', 'a/../b.py'): + with self.subTest(name=name), self.assertRaisesRegex(ValueError, 'Invalid archive member'): + check.archive_files(self.archive([name])) + with self.assertRaisesRegex(ValueError, 'Invalid archive member'): + check.archive_files(self.archive(['a.py'], symlink=True)) + + def test_word_digest_ignores_container_time_but_binds_frames(self): + word = array('i', [1, 4, 7, -1, 21, 3]).tobytes() + canonical = check.canonical_records(gzip.compress(word, mtime=0)) + self.assertEqual(canonical, check.canonical_records(gzip.compress(word, mtime=100))) + wrong_frame = array('i', [1, 4, 7, -1, 20, 3]).tobytes() + self.assertNotEqual(canonical, check.canonical_records(gzip.compress(wrong_frame, mtime=0))) + + +class EvidenceControls(unittest.TestCase): + def setUp(self): + source = check.read_json(HERE / 'SOURCE.json') + self.manifest = source['candidate_manifest_sha256'] + self.report = dict( + status='PASS_IMMUTABLE_PARITY_FUSED_GEN4_FIVE_STAGE_BANKED_CONSTRUCTION', + manifest_sha256=self.manifest, files=114, inputs_unchanged=True, + kappa=check.KAPPA, fresh_stages=sorted(check.STAGES), + negative_controls=['omitted ' + stage + ' stage' for stage in sorted(check.STAGES)]) + + def test_historical_replay_is_not_current_evidence(self): + historical = check.read_json(check.ROOT / 'research/community-pr279-audit/verification.json') + with self.assertRaisesRegex(ValueError, 'Replay source mismatch'): + check.check_replay(historical, self.manifest) + + def test_each_missing_stage_is_rejected(self): + for stage in check.STAGES: + report = deepcopy(self.report) + report['fresh_stages'].remove(stage) + with self.subTest(stage=stage), self.assertRaisesRegex(ValueError, 'Incomplete fresh-stage'): + check.check_replay(report, self.manifest) + + def test_missing_negative_control_and_failed_run_are_rejected(self): + report = deepcopy(self.report) + report['negative_controls'].pop() + with self.assertRaisesRegex(ValueError, 'Missing stage-omission'): + check.check_replay(report, self.manifest) + self.report['status'] = 'FAIL' + with self.assertRaisesRegex(ValueError, 'Replay did not complete'): + check.check_replay(self.report, self.manifest) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/pr279-target-prefix-reconciliation/verify.py b/research/pr279-target-prefix-reconciliation/verify.py new file mode 100644 index 0000000000..9c992d8972 --- /dev/null +++ b/research/pr279-target-prefix-reconciliation/verify.py @@ -0,0 +1,293 @@ +#!/usr/bin/env python3 +"""Reconstruct the exact later PR279 head without replacing the reviewed package. + +The default command checks source coverage and retained evidence. --replay runs +the unchanged candidate verifier in a new directory. Apache-2.0; prepared for +mihir-s-05 with substantial OpenAI Codex assistance. +""" +from array import array +from collections import Counter +from hashlib import sha1, sha256 +from pathlib import Path, PurePosixPath +import argparse +import gzip +import io +import json +import os +import subprocess +import sys +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE = '66849e1475c930fd7732b1a0067ffee7e1e95f60' +REVIEWED = '4d8c31eec7ae618645cb058101cb4e72a97268d3' +CANDIDATE = '913ccc48a0bc1173709ea92280b96252256b7754' +KAPPA = '724098741932703/1000000000000000000' +HISTORICAL = 'research/five-stage-gen4-banks' +STAGES = {'virtual', 'raw', 'bit', 'scalar', 'primes', 'banks', 'complex', 'math', 'finite'} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def digest(data): + return sha256(data).hexdigest() + + +def git_blob(data): + return sha1(b'blob ' + str(len(data)).encode('ascii') + b'\0' + data).hexdigest() + + +def canonical_records(data): + """Bind every instruction field, independently of the gzip container bytes.""" + records = array('i') + require(records.itemsize == 4, 'Candidate instruction format requires 32-bit C ints') + records.frombytes(gzip.decompress(data)) + require(len(records) % 6 == 0, 'Incomplete instruction sextuple') + if sys.byteorder != 'big': + records.byteswap() + return dict(encoding='big-endian signed 32-bit integers, six per instruction', + records=len(records) // 6, sha256=digest(records.tobytes())) + + +def read_json(path): + return json.loads(path.read_text(encoding='utf-8')) + + +def archive_files(data): + """Read regular relative files, rejecting duplicate and unexpected path forms.""" + files = {} + with tarfile.open(fileobj=io.BytesIO(data), mode='r:gz') as archive: + for entry in archive: + path = PurePosixPath(entry.name) + require(entry.isfile() and not path.is_absolute() and + '..' not in path.parts and '\\' not in entry.name and + ':' not in entry.name and str(path) == entry.name, + 'Invalid archive member: ' + entry.name) + require(entry.name not in files, 'Duplicate archive member: ' + entry.name) + stream = archive.extractfile(entry) + require(stream is not None, 'Unreadable archive member: ' + entry.name) + files[entry.name] = stream.read() + return files + + +def validate_candidate(source, files): + require(source['base_commit'] == BASE and source['reviewed_head'] == REVIEWED and + source['candidate_head'] == CANDIDATE, 'Unexpected source commit') + require(source['historical_package'] == HISTORICAL, 'Unexpected historical package') + expected = source['candidate_files'] + require(len(expected) == 115 and set(files) == set(expected), + 'Missing or additional candidate file') + for name, pin in expected.items(): + require(digest(files[name]) == pin['sha256'] and git_blob(files[name]) == pin['git_blob'], + 'Changed candidate file: ' + name) + manifest = json.loads(files['MANIFEST.json']) + require(digest(files['MANIFEST.json']) == source['candidate_manifest_sha256'], + 'Wrong candidate manifest') + actual = {name: digest(data) for name, data in files.items() if name != 'MANIFEST.json'} + require(manifest['files'] == actual, 'Candidate manifest does not bind all inputs') + + +def collect_candidate(root=ROOT, package=HERE): + source = read_json(package / 'SOURCE.json') + archive = (package / 'source-update.tar.gz').read_bytes() + require(digest(archive) == source['archive_sha256'], 'Changed source archive') + updated = archive_files(archive) + changes = {row['path']: row for row in source['changes']} + require(len(changes) == len(source['changes']) == 12 and set(updated) == set(changes), + 'Missing or additional update member') + require(Counter(row['status'] for row in changes.values()) == {'modified': 10, 'added': 2}, + 'Unexpected update classification') + for name, pin in source['candidate_files'].items(): + require(pin['source'] == ('update_archive' if name in changes else 'historical_package'), + 'Incorrect coverage source: ' + name) + for name, pin in source['context_sources'].items(): + require(digest((root / name).read_bytes()) == pin, 'Changed historical context: ' + name) + workflow = source['unchanged_workflow'] + workflow_data = (root / workflow['path']).read_bytes() + require(digest(workflow_data) == workflow['sha256'] and + git_blob(workflow_data) == workflow['git_blob'], 'Changed historical workflow') + comparison = read_json(root / 'research/pr-reconciliation-20261012/content-comparison.json')['279'] + require(comparison['total'] == 116 and len(comparison['matched']) == 104 and + {row['path']: row['blob'] for row in comparison['unresolved']} == + {HISTORICAL + '/' + name: row['new_git_blob'] for name, row in changes.items()}, + 'Retained update does not resolve the recorded source gap') + historical = root / HISTORICAL + old_manifest = (historical / 'MANIFEST.json').read_bytes() + require(digest(old_manifest) == source['historical_manifest_sha256'], + 'Changed historical manifest') + old_pins = json.loads(old_manifest)['files'] + actual_names = {p.relative_to(historical).as_posix() for p in historical.rglob('*') if p.is_file()} + require(actual_names == set(old_pins) | {'MANIFEST.json'} and len(actual_names) == 113, + 'Historical inventory changed') + files = {} + for name in sorted(actual_names): + path = historical / name + require(not path.is_symlink() and path.resolve().is_relative_to(historical.resolve()), + 'Historical file escapes package: ' + name) + data = path.read_bytes() + if name != 'MANIFEST.json': + require(digest(data) == old_pins[name], 'Changed historical file: ' + name) + if name in changes: + row = changes[name] + require(digest(data) == row['old_sha256'] and git_blob(data) == row['old_git_blob'], + 'Historical update base mismatch: ' + name) + files[name] = data + for name, data in updated.items(): + row = changes[name] + require((name in files) == (row['status'] == 'modified'), 'Wrong change kind: ' + name) + require(digest(data) == row['new_sha256'] and git_blob(data) == row['new_git_blob'], + 'Update source identity mismatch: ' + name) + files[name] = data + validate_candidate(source, files) + return source, files + + +def check_selection(files): + """Check the submitted finite schedule and its advertised accounting, not its theorem.""" + selection = json.loads(files['target-selection.json']) + groups = selection['groups'] + require(len(groups) == 220, 'Wrong group count') + targets, delta = set(), Counter() + inserted = 0 + for row in groups: + ts = row['targets'] + require(len(ts) == len(set(ts)) == 4 and all(0 <= t < 1760 for t in ts), + 'Invalid target square') + require(not targets.intersection(ts), 'Overlapping target squares') + targets.update(ts) + dep = row['dependent'] + require(len(dep) == 1, 'Wrong dependency count') + target, retained = next(iter(dep.items())) + require(set(retained) == set(row['retained']) == set(ts) - {int(target)} and + len(retained) == 3, 'Invalid retained targets') + require(row['cut_record'] == selection['cut_record'] == 566579 and + row['close_after_record'] > row['cut_record'] and row['close_rank'] == 21, + 'Invalid cut/close contract') + require(row['local_histogram_delta'] == {'1': -1, '20': -1, '21': 1}, + 'Wrong local rank delta') + require(row['extra_setup_restore_additions'] == 2 * len(retained), + 'Unpaid setup/restore additions') + inserted += 2 * len(retained) + delta.update({int(k): v for k, v in row['local_histogram_delta'].items()}) + require(dict(delta) == {int(k): v for k, v in selection['expected_total_delta'].items()}, + 'Wrong total delta') + require(sum(rank * count for rank, count in delta.items()) == 0, + 'Rank mass changed') + return dict(groups=220, targets=len(targets), setup_restore_additions=inserted, + local_paid_call_delta=sum(delta.values()), + five_stage_paid_call_delta=5 * sum(delta.values()), + rank_mass_delta=0, + scope='Schedule/count consistency only; literal identities need --replay.') + + +def reconstruct(files, destination): + destination.mkdir(parents=True, exist_ok=False) + for name, data in files.items(): + path = destination / name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(data) + + +def check_replay(report, manifest_sha): + require(report.get('status') == 'PASS_IMMUTABLE_PARITY_FUSED_GEN4_FIVE_STAGE_BANKED_CONSTRUCTION', + 'Replay did not complete') + require(report.get('manifest_sha256') == manifest_sha and report.get('files') == 114, + 'Replay source mismatch') + require(report.get('inputs_unchanged') is True and report.get('kappa') == KAPPA, + 'Replay changed inputs or historical exponent') + require(set(report.get('fresh_stages', [])) == STAGES and len(report['fresh_stages']) == 9, + 'Incomplete fresh-stage coverage') + require(set(report.get('negative_controls', [])) == {'omitted ' + s + ' stage' for s in STAGES}, + 'Missing stage-omission controls') + + +def check_retained_evidence(package, source): + inventory = read_json(package / 'EVIDENCE.json') + require(inventory['candidate_head'] == CANDIDATE, 'Evidence head mismatch') + require(digest((package / 'RESULTS.json').read_bytes()) == inventory['results_sha256'], + 'Changed reconciliation result') + require(digest((package / 'SOURCE-CI.json').read_bytes()) == inventory['source_ci_metadata_sha256'], + 'Changed source CI metadata') + ci = read_json(package / 'SOURCE-CI.json') + require(ci['head_sha'] == CANDIDATE and ci['status'] == 'completed' and ci['conclusion'] == 'success', + 'CI metadata does not cover the candidate head') + archive = (package / 'replay-evidence.tar.gz').read_bytes() + require(digest(archive) == inventory['archive_sha256'], 'Changed evidence archive') + files = archive_files(archive) + require(set(files) == set(inventory['files']), 'Missing or additional evidence file') + for name, pin in inventory['files'].items(): + require(digest(files[name]) == pin, 'Changed evidence: ' + name) + report = json.loads(files['verification.json']) + check_replay(report, source['candidate_manifest_sha256']) + require(json.loads(files['certificate.json'])['kappa'] == KAPPA, 'Wrong evidence certificate') + require({stage + '.json' for stage in STAGES} | {'target.json', 'replay.log'} <= set(files), + 'Missing per-stage replay evidence') + target = json.loads(files['target.json']) + expected_target = dict( + status='PASS_EXACT_F2_TARGET_PREFIX_COMPRESSION', selected_groups=220, + targets=880, deleted_prefix_adds=1100, inserted_setup_restore_adds=1320, + remaining_payload_additions=626580, + local_histogram_delta={'1': -220, '20': -220, '21': 220}, + negative_control='omitted target-prefix setup rejected') + require(all(target.get(key) == value for key, value in expected_target.items()), + 'Wrong target-prefix evidence') + for name, key in [('target-selection.json', 'selection_sha256'), + ('target_transform.py', 'transform_sha256')]: + require(target.get(key) == source['candidate_files'][name]['sha256'], + 'Target receipt is from different source: ' + name) + for direction in ('forward', 'inverse'): + row = target[direction] + require(row['all_formal_columns'] == 19930 and + row['all_source_and_dirty_restored'] is True and + row['arbitrary_target_contents_preserved'] is True and + row['weighted_additions'] == 626580 and row['literal_unit_additions'] == 630100, + 'Incomplete target-prefix scalar evidence') + return dict(status='PASS_RETAINED_REPLAY_BINDING', fresh_execution=False, + retained_stages=sorted(STAGES), scope='Checks stored evidence; use --replay for a fresh run.') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + action = parser.add_mutually_exclusive_group() + action.add_argument('--replay', action='store_true') + action.add_argument('--extract', action='store_true', help='Reconstruct source for inspection without executing it') + parser.add_argument('--work', type=Path, help='New directory outside the repository') + args = parser.parse_args() + require((args.replay or args.extract) == (args.work is not None), + '--extract/--replay requires --work, and --work requires an action') + source, files = collect_candidate() + schedule = check_selection(files) + retained = check_retained_evidence(HERE, source) + print('PASS_PR279_SOURCE_RECONCILIATION old=113 current=115 modified=10 added=2', flush=True) + print(json.dumps({'schedule': schedule, 'retained_evidence': retained}, sort_keys=True), flush=True) + if args.replay or args.extract: + work = args.work.resolve() + require(not work.exists() and not work.is_relative_to(ROOT.resolve()), + 'Work directory must be new and outside the repository') + work.mkdir(parents=True) + candidate = work / 'source' + reconstruct(files, candidate) + if args.extract: + print('PASS_PR279_EXTRACTED_SOURCE ' + str(candidate)) + return + output = work / 'replay' + env = dict(os.environ, PYTHONUTF8='1') + env.pop('PYTHONOPTIMIZE', None) + command = [sys.executable, '-X', 'utf8', '-B', str(candidate / 'verify.py'), + '--output', str(output)] + with (work / 'replay.log').open('wb') as log: + result = subprocess.run(command, stdout=log, stderr=subprocess.STDOUT, env=env) + require(result.returncode == 0, 'Candidate replay failed; see ' + str(work / 'replay.log')) + check_replay(read_json(output / 'verification.json'), source['candidate_manifest_sha256']) + evidence = read_json(HERE / 'EVIDENCE.json') + require(canonical_records((output / 'records.bin.gz').read_bytes()) == evidence['emitted_word'], + 'Fresh literal instruction stream differs from the recorded replay') + print('PASS_PR279_FRESH_REPLAY stages=9 kappa=' + KAPPA) + + +if __name__ == '__main__': + main()