diff --git a/docs/research/agent-procedure.md b/docs/research/agent-procedure.md index 9294c540bf..a5403868ef 100644 --- a/docs/research/agent-procedure.md +++ b/docs/research/agent-procedure.md @@ -139,6 +139,26 @@ historical catalogue, picker and baseline bytes remain intact. The replacement authenticates selected sources and checks metadata consistency; it is not a cold replay or supplier admission. +**Keep the complex-ceiling control in its historical context.** Four cards +(`complex-rank-shape-decoder`, `complex-new-helper-inventory`, +`centre-path-sharing` and `coverage-law-change`) name +`research/complex-local-word-ceiling/verify.py`. That frozen checker reads the +#1094 certificate schema and fails on selected #4470 with +`KeyError: 'complex_profile'`. Run the current selected orientation above, then +use the [authenticated historical replay](../../research/historical-complex-ceiling-replay/README.md) +for the card's original positive control: + +```sh +python3 -B scripts/research_package.py --package research/historical-complex-ceiling-replay +``` + +This executes the unchanged scientific checker and its controls against exact +#1094/#1042 inputs in a temporary tree. Its ceiling and `levers.py` budgets +belong to that historical word, coverage law and outer guard. Before screening +a changed current supplier, derive and source-bind the applicable complete cost +law; a historical pass does not make the old ceiling a cap on #4470. The card, +its pinned sources and the live selected record retain their bytes. + In a sparse checkout, the helper can validate omitted catalogue references when they are regular files in `HEAD` with matching skip-worktree index entries. It reports these as `sparse_checkout.omitted_catalogue_paths`. For absent paths, diff --git a/research/historical-complex-ceiling-replay/README.md b/research/historical-complex-ceiling-replay/README.md new file mode 100644 index 0000000000..221f124eea --- /dev/null +++ b/research/historical-complex-ceiling-replay/README.md @@ -0,0 +1,149 @@ +# Reproduce the historical complex-ceiling control without changing selection + +**Tooling repair; no new mathematical bound or supplier.** This package runs +Douglas Colkitt's unchanged PR1240 ceiling checker against its exact #1094 +selected record and #1042 comparison. It restores a runnable scientific +positive control for four research cards while preserving all predecessor +bytes and the current selected frontier. + +At base `7c472563474e60185e6ca101a17622133d047e56`, priority revision 7, +`complex-rank-shape-decoder`, `complex-new-helper-inventory`, +`centre-path-sharing` and `coverage-law-change` still start with +`research/complex-local-word-ceiling/verify.py`. With its inputs materialized, +that command raises `KeyError: 'complex_profile'`: selected #4470's certificate +has a productive-helper schema. The [existing handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132013) +already identified this mismatch. This contribution adds the actual historical +replay route; it does not claim to discover the mismatch. + +The original checker reproduces exactly: + +```text +PASS_COMPLEX_LOCAL_WORD_CEILING a_ceiling 0.00169005410908900006 kappa<= 0.0016872026453254019 +``` + +Those values describe **the #1094 model**. The selected conditional #4470 value +at this base is 0.00302015, under a different construction and accounting. +For current orientation run `python3 -B scripts/research_selected_baseline.py` +after materializing its source closure. A historical ceiling or lever budget +must not be applied to that current contract without a new applicable cost law. + +## Exact source and execution boundary + +The nine-file executable closure comprises the original `verify.py`, +`ceiling.py`, `RESULT.json`, `SOURCES.json`, two #1094 audit inputs, the #1042 +checkpoint and assembly, and the historical selected record. Every file is +SHA256-authenticated before any predecessor code runs. The three live input +pins in the original `SOURCES.json` are then independently reconciled with +that payload. The added #1042 pins also bind the actual predecessor comparison. + +The retained [historical-selected.json](historical-selected.json) is the exact +`certificates/selected-result.json` blob `ae6a99f28aa468649eb66a361e764d769363bf11` +at original base `e3bb23b4c6bae16ba277f9443e11257a0a37780a`, with SHA256 +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +Its original Git path is a provenance pin in [SOURCES.json](SOURCES.json); +the package-owned copy is authenticated by the wrapper and exported with it. +The current `certificates/checkpoints/frontier1094.json` has SHA256 +`bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129`. +It is byte-distinct and is not silently substituted for the old pin. + +Only the retained selected record is relocated, to its original path **inside +a fresh temporary tree**. All other inputs keep their paths and bytes. The +wrapper executes the unchanged checker as a separate isolated Python process, +preserving an explicitly requested `-O` level. It copies no bytecode or unrelated +repository files, uses a 90-second child timeout and never passes `--write`. +The original checker retains its exact `RESULT.json` comparison, #1042 check, +coverage and moment calculations and four original failure/dominance controls. + +The wrapper requires successful exit and the complete expected stdout, compares +all temporary input bytes after the positive replay, reauthenticates original +inputs at return, and checks the live selected record is unchanged when present. +The standalone verifier requires no Git, network or third-party dependencies. +The generic metadata command does use Git to authenticate provenance. In a +shallow checkout, fetch the public original base explicitly if it is absent: + +```sh +git fetch --depth 1 --no-tags https://github.com/CrocSwap/integer-mult-bounds.git e3bb23b4c6bae16ba277f9443e11257a0a37780a +``` + +This fetch is not a full-history ancestry audit. A committed Git-free export +contains everything needed for the standalone replay and avoids that lookup. + +## Reproduce and rejection coverage + +From the repository root, CPython 3.12 and the standard library: + +```sh +python3 -B scripts/research_package.py --package research/historical-complex-ceiling-replay --check-only +python3 -B scripts/research_package.py --package research/historical-complex-ceiling-replay +``` + +The registered commands run both normal and optimized modes. Direct commands +also work from an exported tree: + +```sh +python3 -I -W error -B research/historical-complex-ceiling-replay/verify.py +python3 -I -W error -O -B research/historical-complex-ceiling-replay/verify.py +``` + +Each mode includes: + +- The entire unchanged historical positive replay and its four original controls. +- Eighteen source-integrity controls: individually corrupt and remove every one + of the nine inputs, requiring the specific input's rejection. +- Three scientific-data controls in separate disposable trees. A changed owner + profile rejects with `profile mismatch`; an impossible #1042 endpoint rejects + with `previous endpoint above the ceiling`; a changed expected receipt rejects + with `RESULT.json differs`. These intentionally bypass only the wrapper's + earlier hash gate to test the unchanged scientific checker itself. +- Exact preservation of all source inputs and the live selected record. + +The final line is +`PASS_HISTORICAL_COMPLEX_CEILING_REPLAY context=PR1094 current_supplier_bound=false inputs=9 input_controls=18 scientific_controls=3 unchanged=true`. +The PR and [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4458#discussioncomment-19152822) +record measured runs, committed/export checks and hosted status. No full selected +cold replay, Lean, Docker, new cost law, independent human review or proof-kernel +acceptance is claimed. The underlying historical theorem keeps its original +scope and proof dependencies. + +## Task choice, overlap and credit + +The picker selected `complex-rank-shape-decoder` with nonce +`3d916505ccc35c2632298bca8333380c`. [TASK.json](TASK.json) explicitly changes the +scope from decoder synthesis to this first-step reproducibility repair. Its +original card and originating catalogue remain pinned. The standing procedure +links this route without changing the catalogue, allocation, frozen checkers +or scientific receipts. This complements #4906's generic-baseline navigation; +that change deliberately left named scientific replay commands alone. + +Entry overlap covered 304 open PR bodies and 4,625 Discussion records with +complete remote pagination at 18:55/18:57 UTC on October 23, 2026. Local note +coverage was sparse (9 of 7,267 tracked paths); directly relevant packages, +guidance, #4458/#1166 and targeted all-state PR searches were inspected. +Arbitrary diffs, omitted unrelated notes and unpublished work were not covered. +No claim of global novelty follows from these searches. + +Credit Douglas Colkitt and the original credited Claude assistance for PR1240, +the PR1012 coverage identity, and the #1094/#1042 construction and audit authors +retained in the original package. Mihir Srivastava's #4463/#4906 supply the +current-schema orientation and generic startup routing; lee-phys's #4631 and +the retained #4936/#5050 contributors supply sparse and source-loading follow-ups. +Dennis's existing historical-check replay and all repository workflow tools +retain their original credit. This focused copy needs only nine inputs; it +does not change those shared tools or their historical configurations. + +Prepared by Mihir Srivastava (@mihir-s-05) with substantial OpenAI Codex assistance +in inspection, implementation, documentation and verification; no subagents. +Apache-2.0. This is author-checked tooling evidence, not scientific approval. + +## Open next questions + +1. **Bind a current helper-inventory cost law.** Authenticate the selected closure + with `research_selected_baseline.py`, then derive the actual paid completion, + compiler and outer guard for a named changed invoice. This matters because + the historical cap is inapplicable to #4470. The missing complete law and + consumer bill are blockers; this replay does not supply them. +2. **Migrate the four emitted historical first steps.** Extend the exact-path + dependency inventory in [the startup compatibility note](../../docs/research/task-startup-compatibility.md) + before editing the pinned catalogue. Users who skip the standing procedure + still see the legacy command. Preserving historical task/source receipts + requires a separate migration decision; no catalogue repin is included here. diff --git a/research/historical-complex-ceiling-replay/SOURCES.json b/research/historical-complex-ceiling-replay/SOURCES.json new file mode 100644 index 0000000000..bf036e07c7 --- /dev/null +++ b/research/historical-complex-ceiling-replay/SOURCES.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "base_commit": "7c472563474e60185e6ca101a17622133d047e56", + "files": [ + { + "path": "certificates/checkpoints/frontier1042.json", + "usage": "input", + "git_blob": "f451ced6626a1f03aba6915ce23a136b01ebe51d", + "sha256": "207d1f49f113c585024b9d3c17eadbb8b1be17c1321e3d190aabe2f18ce1c5b7" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "pin": "head:e3bb23b4c6bae16ba277f9443e11257a0a37780a:certificates/selected-result.json" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/community-frontier1042-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "4e308dc23da97373d66e5d8d4a68b0661caea8e9", + "sha256": "093f35445812ea96fe1bfe6a3af7d769cb7f274e08f4fb30f71a17ed1161e54e" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/INDEPENDENT1094.json", + "usage": "input", + "git_blob": "009a385e26858058a18188364078d162aa6f9519", + "sha256": "301fb8a0e4ab7e3c383ff974c54c08178283b2a3453c5282757f692a3c7a4bfd" + }, + { + "path": "research/complex-local-word-ceiling/RESULT.json", + "usage": "input", + "git_blob": "77f55043a679dd722330f1e2499863e36376d9f9", + "sha256": "d91d6c46509875abf1f61de67c2609656d3dc685451299f83caa6f922493692d" + }, + { + "path": "research/complex-local-word-ceiling/SOURCES.json", + "usage": "input", + "git_blob": "c45a9995fe68f9b42c88c02e237269c60533ef96", + "sha256": "df587fbef4bb7c00f827f4a4eaddf2f4910ef19f6decf32984f1d32ac036de6a" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + { + "path": "research/complex-local-word-ceiling/verify.py", + "usage": "input", + "git_blob": "069f09de381a52ac91ec3edb372bd4536a051d91", + "sha256": "06b59955c69a2e7f49aa031d2ebaac2f39dbe107f4087122704f2a37ce9806d5" + } + ], + "retained_copy": { + "path": "research/historical-complex-ceiling-replay/historical-selected.json", + "source": "head:e3bb23b4c6bae16ba277f9443e11257a0a37780a:certificates/selected-result.json", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "verification": "The standalone verifier authenticates this package-owned input and reconciles it with the unchanged historical SOURCES.json. The standard provenance row above authenticates its original Git object; the package export retains the copy without a runtime Git dependency." + } +} diff --git a/research/historical-complex-ceiling-replay/TASK.json b/research/historical-complex-ceiling-replay/TASK.json new file mode 100644 index 0000000000..e83e6119bc --- /dev/null +++ b/research/historical-complex-ceiling-replay/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "7c472563474e60185e6ca101a17622133d047e56", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Restore the complex-rank-shape card's historical PR1094 ceiling control through an authenticated disposable replay, and distinguish it from current selected orientation.", + "scope_change_reason": "The assigned card's mandatory first command fails on selected PR4470 with KeyError: complex_profile. This is a reproducibility side result answering the existing source-binding handoff, not decoder synthesis or a new ceiling.", + "bottleneck_link": "A runnable, explicitly historical positive control prevents contributors from applying an obsolete coverage law to the productive-helper construction. The current cost law and complete consumer budget remain separate research obligations.", + "budget_minutes": 60, + "stop_rule": "Stop after unchanged historical scientific replay, source-integrity rejection controls, normal/optimized registered replay, committed/export byte checks and documented current-versus-historical routing. Do not expand to full supplier, Lean or Docker replay.", + "outcome": "completed", + "evidence": "The unchanged PR1240 checker reproduces its exact RESULT.json, #1042 comparison and four original controls. The wrapper checks nine exact inputs, eighteen missing/corrupt input cases and three independent scientific-data rejections. Publication and export results are reported in the PR and canonical Discussion.", + "author": "Mihir Srivastava (@mihir-s-05)", + "ai_assistance": "Substantial OpenAI Codex assistance with inspection, implementation, documentation and verification; no subagents, independent human review or proof-kernel acceptance.", + "open_questions": [ + { + "question": "Derive a source-bound cost law for changed helper inventories under selected PR4470.", + "why_it_matters": "The PR1094 ceiling is not a cap for the current productive-helper interface.", + "first_step": "Authenticate the selected source closure with research_selected_baseline.py, then bind the proposed invoice, paid completion, compiler and outer guards to that source.", + "blocked_by": "No such replacement cost law or complete consumer invoice is supplied by this replay repair." + }, + { + "question": "Migrate the four emitted historical first-step commands without invalidating frozen task/source receipts.", + "why_it_matters": "Users who skip the standing procedure still see the legacy direct command.", + "first_step": "Extend the exact-path compatibility inventory in task-startup-compatibility.md and distinguish historical live-pin drift from new dependency invalidation.", + "blocked_by": "The current catalogue is pinned by predecessor packages; their migration policy is a separate compatibility decision." + } + ], + "chooser_nonce": "3d916505ccc35c2632298bca8333380c", + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4458#discussioncomment-19152822", + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132013", + "selected_context": { + "commit": "7c472563474e60185e6ca101a17622133d047e56", + "kappa": "60403/20000000", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + "overlap": { + "open_prs": 304, + "prs_at": "2026-10-23T18:55:25Z", + "discussion_records": 4625, + "discussions_at": "2026-10-23T18:57:13Z", + "complete_remote_pagination": true, + "local_note_records_at_entry": 9, + "tracked_note_paths": 7267, + "limits": "Sparse local notes, no arbitrary diffs or unpublished work; directly relevant packages, current guidance, #4458/#1166 and targeted all-state PR searches inspected." + } +} diff --git a/research/historical-complex-ceiling-replay/VERIFY.json b/research/historical-complex-ceiling-replay/VERIFY.json new file mode 100644 index 0000000000..698bd859da --- /dev/null +++ b/research/historical-complex-ceiling-replay/VERIFY.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/checkpoints/frontier1042.json", + "research/community-frontier1042-audit/ASSEMBLY.json", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-frontier1094-audit/INDEPENDENT1094.json", + "research/complex-local-word-ceiling/RESULT.json", + "research/complex-local-word-ceiling/SOURCES.json", + "research/complex-local-word-ceiling/ceiling.py", + "research/complex-local-word-ceiling/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact nine-input authentication and frozen source-pin reconciliation; complete unchanged historical ceiling replay and original controls; eighteen input rejection cases; three scientific-data rejections; source and live-selection byte preservation." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact nine-input authentication and frozen source-pin reconciliation; complete unchanged historical ceiling replay and original controls; eighteen input rejection cases; three scientific-data rejections; source and live-selection byte preservation." + } + ] +} diff --git a/research/historical-complex-ceiling-replay/historical-selected.json b/research/historical-complex-ceiling-replay/historical-selected.json new file mode 100644 index 0000000000..ae6a99f28a --- /dev/null +++ b/research/historical-complex-ceiling-replay/historical-selected.json @@ -0,0 +1,222 @@ +{ + "status": "Maintainer-reviewed conditional finite construction; see the integration receipt for publication and PR resolution status", + "kappa": "836330098538459/500000000000000000", + "decimal": "0.001672660197076918", + "source_prs": [ + 1094, + 1087, + 1082, + 1074, + 1068, + 1065, + 1063, + 1061, + 1056, + 1055, + 1053, + 1050, + 1042, + 1031, + 1028, + 1022, + 1018, + 1005, + 1004, + 987, + 942, + 890, + 870, + 869, + 858, + 799, + 741, + 699, + 685, + 676, + 664, + 660, + 659, + 656, + 655, + 653, + 658, + 649, + 645, + 635, + 589, + 555, + 545, + 626, + 623, + 622, + 620, + 617, + 615, + 604, + 601, + 596, + 592, + 591, + 593, + 599, + 588, + 543, + 584, + 586, + 583, + 582, + 579, + 576, + 575, + 574, + 571, + 569, + 568, + 567, + 564, + 562, + 561, + 559, + 558, + 552, + 550, + 548, + 541, + 535, + 510, + 503, + 531, + 523, + 493, + 514, + 507, + 484, + 496, + 505, + 522, + 520, + 472, + 458, + 445, + 442, + 425, + 433, + 370, + 361, + 315 + ], + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "certificate": "research/community-frontier1094-audit/ASSEMBLY.json", + "certificate_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "proof": "docs/research/community-batch1099-review.md", + "proof_supplements": { + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "research/complex-571-free4fc8/NOTICE.md": "a4c084abdc1c7a9ac683eeb11124335d51cff8a6deba6ee92ba5a12bceaa2c97", + "research/complex-multicold/proof/CONSTRUCTION.md": "27ece5e1c11b90d97a808b56eff897b998c10e61016db95867f84e6e6aef132f", + "research/complex-multicold/vendor/pr559/PROOF.md": "d5d498edc56fdef8c5798af7f5ec66948bd2f66c553b9efe366cdaab01bd3453", + "research/structural-gain/frontier-composition/README.md": "70f0f791cbe3b2603f85d85bb9055aa0ee1df6dc06ba82fc1921356948312887", + "research/complex-joint-prefix/proof/CONSTRUCTION.md": "a92e610e7a598d99c612d1b63d1a03a49c0cd1e15ddd29fa55c465ddd8c18105", + "research/kernel-frame-coalescing/PROOF.md": "fa8b2f36b9590ee80ff45d3f7724f8c7de8ad29a29f366d5133010c77e41fe1b", + "research/complex-571-hpeq5/README.md": "4000b37f6c07c09d971dc4010ceb137c13340f3a8809d3272046ccaf746c3e2b", + "research/hyperplane-end-lean/PROOF.md": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9", + "docs/research/community-hyperplane599-review.md": "3298cd0d451541508af232cac72efbd7c10580e6c6ad493a855ab0faa01ade8c", + "research/complex-571-cold14-b3/README.md": "1945785785c153c7d0e8d4c071adabe626c1091b71721ff85d2d67191b376b96", + "research/complex-571-cold14-b3/PROOF-NOTE.md": "1cf592cbc8ab8e21d2dd8c1e945a5c64c6d5cde1216fb06e05a36c1c6ec6613d", + "scripts/verify_cold617_interface.py": "95d7a9094c05ad975fb72f5ab7605593003245a503c8456764987e512028fa6a", + "docs/research/community-cold617-review.md": "b3f2bcbae1249f1f651032022ce1e6e2bfb3f563ce580bf53671f50a074d7046", + "research/complex-k492-owner-repair/README.md": "ee5a1ace4828f7a073be97e95c2d931988774dd3a29a877e65abdf429aeec902", + "research/complex-k492-owner-repair/PROOF-NOTE.md": "337d70fe7abd9afca1d90954c23bde87f4dc27888cc1a6b4bb80506fd6fbf8c5", + "research/complex-k492-owner-repair/PROOF-NOTE-R.md": "22312bb347bdf159e6a01a45c47675e6170d33b258e2fd9ed52aee88fb92c0ed", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "scripts/verify_frontier626.py": "2207bd0ef04a19ef276869085afdedad80a0938fa75db5e1aa7ab73fd3429444", + "scripts/verify_frontier626_bindings.py": "cda63ff41c6d6e2e352c7bf75b84e690c0ce57e4ec6c0355573bb5d9b1f98280", + "scripts/verify_frontier588_bindings.py": "6d1932eea7b1936598118ea8e607b09c29b6e31b749ec41bbe0744ea4f0b606d", + "scripts/verify_hpe_lean_binding.py": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183", + "docs/research/community-frontier741-review.md": "4634694fa75ea9e749ecf19d3db3e4d82effe3b61a2efdf08ac5a97275fb676a", + "research/complex-sw4-frame8/PROVENANCE.md": "c7648719b01dd93af2c3a2c6e951a54711d13892dc4bd4339d16edb4c37c9bf0", + "research/e8-bit-p111-tuned/tune/README.md": "46c7917fb252949f38b7bcd88cf568efc282e3ea065b61d11e457e41673d0b2d", + "scripts/verify_frontier741.py": "215ee6a12de8dc2392e6811a1b8f2140035f6b2d2a0d2100ff4bd2fdcb8bb39b", + "scripts/verify_frontier741_bindings.py": "eff455167e2fd0bc9a67d35241d0e69d8edc58f3a23e776dcfe8f500ca8e8d67", + "docs/research/community-frontier799-review.md": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "scripts/verify_frontier799.py": "19fe1b32079095160dc00fe2f7df75e0fcbc82cff37f7159b755c8a63bd5ce99", + "scripts/verify_frontier799_bindings.py": "43897b3c99212d6134870898a1840f32898aa1b3679b299e654901568ad7e19b", + "research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md": "39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036", + "docs/research/community-frontier890-review.md": "cd03b7c2c6c09db2cfa89ae40133ae44e1deb6e32ec5ddd23aacecc9c50f2fea", + "scripts/verify_frontier890.py": "88ea38dbef62dd7c0dd46e212618520cc89213edddb2032800e5509993958175", + "scripts/verify_replay_coverage.py": "babe5941d7e6dac4248613ef01f950ee7bb6199e7355021aea4cf854fd1b91c5", + "scripts/verify_frontier741_bridge_coverage.py": "9a14f26762b6126eb54ed43db90371773374fe98733ada80ee871a74afa3b836", + "certificates/replay-coverage/pr741-sw4-v1.json": "7acd5033bc78e3f473718269edaa267c2785d84fbe95ccf6815a33dcf58c2756", + "research/complex-t21-owners/PROOF.md": "78721b32fceb34b21b8e77c95381c38c60276e72e6d9c2e9c6262cb347457def", + "research/complex-t21-owner-bound/PROOF.md": "2aa0aa6ec1d87402138564c38749b5ca0f058c16817efdf58a2685d2d90cb417", + "research/gauge44-barch/PROOF-NOTE-BARCH.md": "c24f211b09358b25d6cf47dd18e4bbd8bcf4ecf279e6f1c6c90613cfa230818d", + "research/complex-double-replica-owners/PROOF.md": "db99599e3966bec253c577c23915e2a2899c4c4e8568044efc11c7918b137bbc", + "docs/research/community-batch952-review.md": "04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b", + "scripts/verify_frontier942.py": "27c6713532d9f53f55dfff4884d55a2d9ae74b68156e37a44596c0418fbed5b7", + "research/complex-t37-owners/PROOF.md": "09b39ad0d5f1f59f54dcff15c16640f7a7acf27e6597660acaf957b95c7e8510", + "research/complex-t37-owners/ALL-T-PROOF.md": "4c0c71ccd0afb850538af1b467e5208b7eb3edd0260fded84e02a8c01dfc868b", + ".github/workflows/t37-owners.yml": "c13acc2902c007237103072b7ec10caf5ca21c1b319d27934f194af2f7d87026", + "docs/research/community-batch1047-review.md": "a6271faf5db0afe3ff7d24a34a3be7a959cdc33ee37784572fba014ee5358787", + "scripts/verify_frontier1042.py": "700fdcaeb6e8f57f6e63c71c2dd1652fc5b183e8d706cd092779bdc0d271e854", + "docs/research/community-batch1099-review.md": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb", + "scripts/verify_frontier1094.py": "c7e20f59968ed5736fb859735de4de207de3418083e37012310ebcded946b949", + "research/community-batch1099-audit/check_frontier1094.py": "2608ef213260a43d09a40b3429742f7a5f280861b54acae66400a7c29a123f51" + }, + "review": "docs/research/community-batch1099-review.md", + "validation": "docs/research/community-batch1099-integration.json", + "reproduce": "make frontier1094-verify", + "scope": "Finite composition under inherited all-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape, analytic and bit H1-H5 assumptions. Not a full Lean multiplication theorem.", + "previous_kappa": "1672188119205421/1000000000000000000", + "previous_record": "certificates/checkpoints/frontier1042.json", + "audited_source_head": "0fc329d0bec93ca7cd288eaea1295172e8789810", + "reviewed_dependency_heads": { + "588": "6d0e53b66c29abd17981881a09eaff41ac862d85", + "543": "2065fe4f72a914d907f1046603f5a36f17018535", + "568": "71c99ac935a33bb7b59a1b4a7af8725a939b0b90", + "569": "1424da81263a5305b35e4cf74ef686c275f03f3f", + "571": "b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3", + "575": "eac6f7e378ab622dac50a2fd4b7ef6eab014de44", + "583": "89be768f0157f5a3d8e4db69cf1748768605eac9", + "586": "4846fee5b06af770e9b3a10c36200f673d656725", + "591": "f622547244bf6d895a571a7b035142ba66279806", + "592": "1f471c445c06a45a32e2c47e8d74c8264b68356b", + "593": "fdb6dcc6d7bc29764c5b6b4d32b7fa050acf74a4", + "596": "7732dd5e46863ff294b5e443661cb9d99abf4e01", + "599": "bc13c8a3e000442606bd2dbe8583a17649ba6c32", + "601": "529ab7dcb59d5ea7a5798e9e06cf5b3aee8a1550", + "604": "1b795c5d7dea746ba310572585c0ef067574b4a6", + "615": "bf8a49a34350599763cced8592db81dc62c2c1c0", + "617": "904d62855723c00f8acef9a287a10768598fdeb2", + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "623": "e39a615ca601ce5d62abeb24f3fcdb8644ca1005", + "626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "589": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "741": "e516b1463606840a15f80aac1995d64ce0092e89", + "799": "80e6463157cfc80b85af09e7e2f14748fe2dac60", + "858": "ae2e25fee91540c83ceee5a60e3b07422ce21c7d", + "869": "73e86f69bf9a391e3c334999f7bbe3825dc42759", + "870": "b734850dc348800942f0ffd1f0723fdec7539b2b", + "890": "4b3bd8cbe8e3e81c44161017c9b72c905a8040a8", + "942": "1960cfa919a0945d0ca4cb14ea96237000037903", + "1004": "1974578f82a30158dd5fcdcdf226b83df8e7196f", + "1005": "779e80aef469bc3a28b19f1adde199871a9a22e3", + "1018": "eac7547cb191f875d5f5ea5f9bbb1d2b8c51c4ef", + "1022": "58618bcbfe88a252467755fc283c04c3db5ca4fd", + "1028": "be4bd89cb4483dcee43257200cd27601f938f13d", + "1031": "e900534f0beda892c726723524203b97471fb9a3", + "1042": "7e8ef087c02a77038a28a337a7ee3a77039cac0d", + "1094": "0fc329d0bec93ca7cd288eaea1295172e8789810", + "1087": "589d1cedf5ef5f231182f4ec86408616311a8af0", + "1082": "0c2e294ec204e83846d27344f829d15ed9ee7cc6", + "1074": "052afc128954f7b6a2b3c409eb4d72248e4020f2", + "1068": "cc71375eae4e8754da0f5d940cb519d66625fb2e", + "1065": "387d935e354a931d636e2c5e6ee63a6910f78a1b", + "1063": "d9377d32e0c97e41338e704c3960fd6f2fa73806", + "1061": "223f581afb1d63d5f8476a69040617e11bcd50e4", + "1056": "d0201efbd68c4acc9832b84bcc986c8781b83c4f", + "1055": "a8ea308976f1709eef0a328463f010cf51469277", + "1053": "6f92ce8884929c9fd4730c86a28e2e3735de02af", + "1050": "c87242f846cfab8c0b97fd889b5fecb0eacef939", + "987": "5142511af0437572aca71b35d1987cd2b47bb5e3" + } +} diff --git a/research/historical-complex-ceiling-replay/verify.py b/research/historical-complex-ceiling-replay/verify.py new file mode 100644 index 0000000000..4d0656d810 --- /dev/null +++ b/research/historical-complex-ceiling-replay/verify.py @@ -0,0 +1,175 @@ +#!/usr/bin/env python3 +"""Replay the unchanged PR1240 ceiling against its exact PR1094 context. + +Mihir Srivastava (@mihir-s-05), substantial OpenAI Codex assistance. +Apache-2.0. This is historical reproduction, not a current supplier bound. +""" +import hashlib +import json +from pathlib import Path +import subprocess +import sys +import tempfile + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = "research/historical-complex-ceiling-replay" +ORIGINAL = "research/complex-local-word-ceiling" +SELECTED = "certificates/selected-result.json" +RETAINED = PACKAGE + "/historical-selected.json" +PREVIOUS = "research/community-frontier1042-audit/ASSEMBLY.json" +INDEPENDENT = "research/community-frontier1094-audit/INDEPENDENT1094.json" +# Complete read closure of the unchanged verifier: code, expected output, +# original pins and the previously unpinned #1042 comparison. Only RETAINED +# moves, to SELECTED inside a fresh temporary tree. +PINS = { + RETAINED: "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "certificates/checkpoints/frontier1042.json": "207d1f49f113c585024b9d3c17eadbb8b1be17c1321e3d190aabe2f18ce1c5b7", + PREVIOUS: "093f35445812ea96fe1bfe6a3af7d769cb7f274e08f4fb30f71a17ed1161e54e", + "research/community-frontier1094-audit/ASSEMBLY.json": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + INDEPENDENT: "301fb8a0e4ab7e3c383ff974c54c08178283b2a3453c5282757f692a3c7a4bfd", + ORIGINAL + "/RESULT.json": "d91d6c46509875abf1f61de67c2609656d3dc685451299f83caa6f922493692d", + ORIGINAL + "/SOURCES.json": "df587fbef4bb7c00f827f4a4eaddf2f4910ef19f6decf32984f1d32ac036de6a", + ORIGINAL + "/ceiling.py": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc", + ORIGINAL + "/verify.py": "06b59955c69a2e7f49aa031d2ebaac2f39dbe107f4087122704f2a37ce9806d5", +} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def authenticated_inputs(root): + payload = {} + for name, expected in PINS.items(): + path = root / name + require(path.is_file() and not path.is_symlink(), "Missing/non-file input: " + name) + raw = path.read_bytes() + require(digest(raw) == expected, "Input SHA256 mismatch: " + name) + payload[SELECTED if name == RETAINED else name] = raw + # Reconcile the historical manifest itself, not just the new digest table. + historical = json.loads(payload[ORIGINAL + "/SOURCES.json"]) + for row in historical["files"]: + if row["usage"] == "input": + require(row["path"] in payload, "Uncovered historical input: " + row["path"]) + require(digest(payload[row["path"]]) == row["sha256"], + "Historical source pin mismatch: " + row["path"]) + return payload + + +def write_payload(root, payload): + for name, raw in payload.items(): + target = root / name + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(raw) + + +def run_original(root): + # No bytecode or unrelated code is copied. -I ignores inherited Python + # environment options; explicitly retain the requested optimization level. + options = ["-I", "-W", "error", "-B"] + if sys.flags.optimize: + options.append("-" + "O" * sys.flags.optimize) + return subprocess.run( + [sys.executable, *options, str(root / ORIGINAL / "verify.py")], + cwd=root, capture_output=True, text=True, encoding="utf-8", timeout=90, + check=False, + ) + + +def require_unchanged(root, payload): + for name, raw in payload.items(): + require((root / name).is_file() and (root / name).read_bytes() == raw, + "Replay changed input: " + name) + + +def input_controls(payload): + """Every declared input must reject both corruption and absence.""" + original_paths = {RETAINED if p == SELECTED else p: raw for p, raw in payload.items()} + with tempfile.TemporaryDirectory(prefix="ceiling-input-controls-") as directory: + root = Path(directory) + write_payload(root, original_paths) + for name, raw in original_paths.items(): + path = root / name + path.write_bytes(raw + b"\n") + try: + authenticated_inputs(root) + except ValueError as error: + require(str(error) == "Input SHA256 mismatch: " + name, + "Wrong corruption rejection: " + str(error)) + else: + raise ValueError("Corrupt input accepted: " + name) + path.unlink() + try: + authenticated_inputs(root) + except ValueError as error: + require(str(error) == "Missing/non-file input: " + name, + "Wrong omission rejection: " + str(error)) + else: + raise ValueError("Missing input accepted: " + name) + path.write_bytes(raw) + return 2 * len(original_paths) + + +def scientific_controls(payload): + """Exercise the old guards on disposable data after the wrapper's pin gate. + + The original checker code stays unchanged; these intentional mutations + require it to independently reject the damaged scientific evidence. + """ + cases = [] + independent = json.loads(payload[INDEPENDENT]) + independent["owner"]["profile"]["1"] += 1 + cases.append((INDEPENDENT, independent, "profile mismatch")) + previous = json.loads(payload[PREVIOUS]) + previous["complex_lower"] = "1" + cases.append((PREVIOUS, previous, "previous endpoint above the ceiling")) + receipt = json.loads(payload[ORIGINAL + "/RESULT.json"]) + receipt["status"] = "INVALID_CONTROL" + cases.append((ORIGINAL + "/RESULT.json", receipt, "RESULT.json differs")) + for name, damaged, message in cases: + with tempfile.TemporaryDirectory(prefix="ceiling-science-control-") as directory: + root = Path(directory) + write_payload(root, payload) + (root / name).write_text(json.dumps(damaged), encoding="utf-8") + result = run_original(root) + require(result.returncode != 0 and result.stdout.strip() == "FAIL: " + message, + "Historical guard did not reject: " + message + "\n" + result.stderr) + return len(cases) + + +def main(): + payload = authenticated_inputs(ROOT) + receipt = json.loads(payload[ORIGINAL + "/RESULT.json"]) + expected = (receipt["status"] + " a_ceiling " + receipt["ceiling"]["a_ceiling_decimal"] + + " kappa<= " + receipt["ceiling"]["kappa_upper_bound"]) + # The live selection is not an executable input. If present, ensure it is + # byte-identical at return; Git-free exports need not contain it. + active = ROOT / SELECTED + active_before = active.read_bytes() if active.is_file() else None + with tempfile.TemporaryDirectory(prefix="historical-complex-ceiling-") as directory: + root = Path(directory) + write_payload(root, payload) + result = run_original(root) + require(result.returncode == 0, "Historical replay failed:\n" + result.stdout + result.stderr) + require(result.stdout.strip() == expected and not result.stderr, + "Unexpected historical output:\n" + result.stdout + result.stderr) + require_unchanged(root, payload) + controls = input_controls(payload) + science = scientific_controls(payload) + require(authenticated_inputs(ROOT) == payload, "Source inputs changed during replay") + if active_before is not None: + require(active.read_bytes() == active_before, "Live selected record changed") + print(expected) + print("PASS_HISTORICAL_COMPLEX_CEILING_REPLAY", + "context=PR1094", "current_supplier_bound=false", + "inputs=" + str(len(PINS)), "input_controls=" + str(controls), + "scientific_controls=" + str(science), "unchanged=true") + + +if __name__ == "__main__": + main()