diff --git a/research/k8-hpe450-binding/README.md b/research/k8-hpe450-binding/README.md new file mode 100644 index 0000000000..b98cac4f60 --- /dev/null +++ b/research/k8-hpe450-binding/README.md @@ -0,0 +1,115 @@ +# Binding an emitted k8 helper to the retained Lean pair + +Helper **450** in the seven-slot k8 word has an exact unit output row and +isolated input column in both emitted local orientations. Its actual wrapper +events name the same entrance/terminal pair as `HyperplaneEnd.Exact.pair3`, and +both regenerated wrapper monomials equal that Lean literal, including phase. +This package connects these finite facts in one reproducible certificate. + +This is a partial theorem-to-emission binding, not a new Lean theorem, supplier +admission or exponent improvement. The selected record is unchanged. + +The starting main commit is `ebedc0895eb4c06725af020bc1af165722b0a3ce`. +At that commit, the selected PR1094 source manifest pins the k8 slot record used +here. Its raw word content hash is +`c2b294300760e1fd6eeab8c22c4d13e4633dca40e52cac8da0d68163a76e3ca8`. +The raw word retained by Josie Elliston's independent owner audit is rebuilt +with the pinned native transport, emitter and wrapper generator. The resulting +canonical payload and **both complete event lists** must match the published +slot hashes. Gzip container bytes are not used to compare regenerated evidence. +All consumed source files, including the Clifford engine, are pinned in +[`SOURCES.json`](SOURCES.json). + +[`RESULT.json`](RESULT.json) records the following in each orientation: + +| Fact | Exact result | +|---|---| +| Complete emitted stream | 24,767 events; 19,693 scalar operations | +| Scalar domain | 704 local registers and eight private center registers | +| Helper's entrance and terminal frame IDs | `2` and `999` | +| Entrance / terminal dimensions | 1 / 8; residual width 7, two spectators | +| Pre / post wrapper positions, zero based | 7,852 / 24,562 | +| Frame path | `2 -> 31 -> 556 -> 751 -> 999`, increments `2,3,1,1` | +| Cleanup-tail touches | positions 16,495 and 16,507 | +| Helper's output row and input column | exactly the coordinate vector for register 450 | + +The checker enumerates each frame's finite span, tracks the emitted frame tags +and checks the wrapper order. Every scalar operand must carry its event's frame +tag. No scalar operation or climb on the helper occurs outside its wrappers; +its last scalar touch is in `cleanup_tail` and the final label remains `999`. +The actual recipe key is `2:999`. Its ten monomial fields, frame vectors and +width metadata are compared directly with `pair3` in the pinned Lean source. + +The scalar check is independent of the producers' full-matrix replay. Write the +scalar map as `M = G_m ... G_1`, retaining the emitted COPY and CLEAR operations. +Starting from `e_450^T`, reverse traversal multiplies this row by `G_m` through +`G_1`, giving the entire row `e_450^T M`. Separately, forward traversal applies +the gates to `e_450`, giving the entire column `M e_450`. All coefficients are +exact rational numbers. The resulting row and column are both unit vectors, +including zero coefficients on the private coordinates. Thus the scalar output +is independent of every other arbitrary input, and the helper's initial value +leaves no scalar residue in other registers. + +These are distinct obligations. One control inserts an extra read immediately +after the helper's last tail touch. Its output row stays restored, but its dirt +leaks to `L230` with coefficient `1/2` in the forward orientation, and to `L27` +with coefficient `1` in the backward orientation. The column check rejects it. +All **28 semantic controls** reach the mathematical checker without checksum +guards. They also cover omitted/changed tail gates, missing/misplaced wrappers, +wrong frame tags, global phases, translations and swapped wrapper sides. + +Under exact relabel recipes and the existing event-semantics correspondence, +the unit row gives the unwrapped residual `T_U T_E^-1`. The checked wrapper +placement gives `L^-1 T_U T_E^-1 R^-1`; the retained `exact_N_pair3` identity +identifies this with `C7` on seven coordinates and identity on two spectators. +The generic `hpe_block` statement is the relevant interface. This Python audit +does **not** instantiate a Lean event word or prove that serialization +correspondence. It does not discharge `RecipesExact` for all other emitted +climbs/adapters, physical footprints, ownership, whole-call hosting, the all-size +compiler, precision/tape bounds, complete costs or analytic transfer. It runs +neither a fresh Lean build nor the full selected supplier cold replay. + +Reproduce from the repository root with Python 3.12; only the standard library +is needed: + +```sh +python3.12 -B scripts/research_package.py --package research/k8-hpe450-binding +``` + +The registered replay regenerates temporary evidence, checks the complete saved +receipt and runs five tests. A separate dense matrix implementation cross-checks +all 512 three-operation words over an eight-operation alphabet, at all three +local coordinates. The tests also reject malformed coefficients, source drift +and a changed receipt, and replay an optimized source export without Git while +preserving its input bytes. Normal verification writes only temporary output; +`verify.py --write-result NEW_PATH` creates a receipt and refuses to overwrite it. + +The revision-2 task selector chose `formal-interface-lemma` with nonce +`7fff7b3cd0d148756c5fc7685585eb0a`. [`TASK.json`](TASK.json) records the refinement +and the [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1394#discussioncomment-18914238). +[PR1415](https://github.com/CrocSwap/integer-mult-bounds/pull/1415), inspected at +`0d8d2c3a96346756f02563b401a042ab97198e20`, already audits the three fixed operator +identities on all 512 basis inputs. This package addresses its emitted-helper +follow-up; it does not repeat that kernel audit or execute pending PR code. + +Credit belongs to Jeremy Kothe for the HPE Clifford formalization and k8 +construction, DreamingOfClouds for the wrapper and Lemma A/G work, icekylinx for +the retained compiler, Rohan Arun for the selected packing, Josie Elliston and +Sagar Thakrar for the retained k8 word/audit lineage, and @commdata2338 for +PR1415's semantic audit and follow-up question. The underlying realization work +of Chafik Boukhalfa, Zhihao Chen and the repository's other credited contributors +is retained unchanged. New work: Hanson Sun (@bbMisk), with substantial OpenAI +Codex assistance in analysis, implementation, validation and writing. +Apache-2.0; original source notices are unchanged. No independent human review +is claimed. + +## Open next questions + +- Can these finite facts be connected to `hpe_block` through an actual Lean + event word? Specify private COPY/CLEAR lifetimes and wrapper labels first. + This would reduce the manual serialization boundary; it is blocked on the + missing correspondence proof, not another finite identity check. +- Can helper 450 be traced through every actual T16 hosted invocation? Start + with the pinned owner map and chart/route evidence. This would connect the + local result to physical realization; exact compiled recipes and disjoint, + nonempty footprints remain separate obligations. diff --git a/research/k8-hpe450-binding/RESULT.json b/research/k8-hpe450-binding/RESULT.json new file mode 100644 index 0000000000..0622528203 --- /dev/null +++ b/research/k8-hpe450-binding/RESULT.json @@ -0,0 +1,662 @@ +{ + "status": "PASS_K8_HPE450_FINITE_BINDING", + "helper": 450, + "lean_pair": "HyperplaneEnd.Exact.pair3", + "recipe_key": "2:999", + "raw_word_content_sha256": "c2b294300760e1fd6eeab8c22c4d13e4633dca40e52cac8da0d68163a76e3ca8", + "canonical_content_sha256": "4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c", + "program_sha256": { + "forward": "071ecdacc0bb3ac16046aad4119ed551a945cb0ed6c57002a548a3e2232503d8", + "backward": "f36c5831106f5637102c6bedeec76ed2b223c6671ce42fd0eceed9ef24725b23" + }, + "input_sha256": { + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-local/inputs/phase-baseline/CANONICAL-WORD.json.gz": "e070ae2c78b4a1b644b418774af62b40d8d16e6ba89602f0474afb557d507c37", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_audit_and_transport.py": "c9a05ff291016b870b4fc925b317abd9c3a604c73ffc8920dfdbbeb475e20aa3", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_emit_local.py": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805", + "research/gauge44-slots/construction/slots/SLOT-PINS-k8.json": "55dd229684febecb80638eff9c6b3986623e8539c6c956753b350209c3e0efe2", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183", + "research/hyperplane-end-lean/HyperplaneEnd/Main.lean": "221a5126ec46141e5cba7689aaddd38746183ed15fa91ec229e32a16302b42a6", + "research/t16-owner-audit-seed67/inputs/k8-seven-slot-word.json.gz": "49596aa4ed4fd36cd4582fd0e8ddeb09fd80370a7d8aea1ede52a135b536d289", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_adapters_local.py": "eb0b5c6c7161e18dc22168da3211448d321586edd15bcfb4b4741174d36993cf", + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-global/vendor531/vendor/clifford/clifford_exact.py": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "research/community-frontier1094-audit/SELECTED-SOURCE.json": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b", + "research/e8-lemma-g-lean/LemmaG/Stream.lean": "7138f4b859d0574a803e99401f05ef5e0ec9eeac0eb480775cd9b86595c365f8" + }, + "recipe": { + "entrance_rank": 1, + "frame": 2, + "left": { + "linear_Z4": [ + 2, + 3, + 3, + 2, + 2, + 2, + 2, + 0, + 0 + ], + "matrix_rows": [ + 1, + 128, + 262, + 2, + 4, + 8, + 16, + 32, + 64 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 6, + 6, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 7, + "right": { + "linear_Z4": [ + 2, + 2, + 0, + 3, + 3, + 2, + 2, + 2, + 2 + ], + "matrix_rows": [ + 1, + 28, + 4, + 32, + 64, + 128, + 256, + 14, + 16 + ], + "offset": 511, + "phase": 1, + "quadratic_rows": [ + 0, + 12, + 2, + 26, + 24, + 0, + 0, + 0, + 0 + ] + }, + "terminal": 999, + "terminal_rank": 8, + "terminal_vectors": [ + 256, + 128, + 64, + 32, + 18, + 10, + 6, + 1 + ], + "vectors": [ + 30 + ] + }, + "orientations": { + "forward": { + "events": 24767, + "scalar_operations": 19693, + "local_registers": 704, + "private_registers": 8, + "pre_wrapper_index": 7852, + "post_wrapper_index": 24562, + "helper_climbs": [ + { + "index": 13948, + "phase": "B", + "from": 2, + "to": 31, + "rank": 2 + }, + { + "index": 14143, + "phase": "B", + "from": 31, + "to": 556, + "rank": 3 + }, + { + "index": 15146, + "phase": "B", + "from": 556, + "to": 751, + "rank": 1 + }, + { + "index": 16494, + "phase": "cleanup_tail", + "from": 751, + "to": 999, + "rank": 1 + } + ], + "helper_scalar_touches": [ + { + "index": 12769, + "phase": "B", + "event": [ + "scalar", + [ + "add", + [ + "L", + 157 + ], + [ + "L", + 450 + ], + 1, + 2 + ], + 2 + ] + }, + { + "index": 12771, + "phase": "B", + "event": [ + "scalar", + [ + "add", + [ + "L", + 219 + ], + [ + "L", + 450 + ], + 1, + 2 + ], + 2 + ] + }, + { + "index": 13949, + "phase": "B", + "event": [ + "scalar", + [ + "add", + [ + "L", + 450 + ], + [ + "L", + 230 + ], + 1, + 1 + ], + 31 + ] + }, + { + "index": 14144, + "phase": "B", + "event": [ + "scalar", + [ + "add", + [ + "L", + 508 + ], + [ + "L", + 450 + ], + 1, + 1 + ], + 556 + ] + }, + { + "index": 15147, + "phase": "B", + "event": [ + "scalar", + [ + "add", + [ + "L", + 219 + ], + [ + "L", + 450 + ], + -1, + 2 + ], + 751 + ] + }, + { + "index": 16495, + "phase": "cleanup_tail", + "event": [ + "scalar", + [ + "add", + [ + "L", + 508 + ], + [ + "L", + 450 + ], + -1, + 1 + ], + 999 + ] + }, + { + "index": 16507, + "phase": "cleanup_tail", + "event": [ + "scalar", + [ + "add", + [ + "L", + 450 + ], + [ + "L", + 230 + ], + -1, + 1 + ], + 999 + ] + } + ], + "unit_row": [ + [ + [ + "L", + 450 + ], + "1" + ] + ], + "isolated_column": [ + [ + [ + "L", + 450 + ], + "1" + ] + ], + "all_scalar_frame_tags_consistent": true, + "controls": [ + { + "name": "missing_pre_wrapper", + "rejected_by": "wrapper_enclosure" + }, + { + "name": "pre_names_full_terminal", + "rejected_by": "wrapper_terminal" + }, + { + "name": "missing_post_wrapper", + "rejected_by": "wrapper_inventory" + }, + { + "name": "post_before_last_touch", + "rejected_by": "post_wrapper_order" + }, + { + "name": "wrong_old_climb_frame", + "rejected_by": "climb_old_frame" + }, + { + "name": "wrong_scalar_frame", + "rejected_by": "scalar_frame" + }, + { + "name": "drop_final_tail_touch", + "rejected_by": "helper_unit_row" + }, + { + "name": "wrong_final_tail_sign", + "rejected_by": "helper_unit_row" + }, + { + "name": "restored_row_but_dirt_leak", + "rejected_by": "helper_isolated_column", + "unit_row_preserved": true, + "leaked_register": [ + "L", + 230 + ], + "exact_coefficient": "1/2" + }, + { + "name": "read_after_post_wrapper", + "rejected_by": "wrapper_enclosure" + }, + { + "name": "left_global_phase", + "rejected_by": "lean_recipe_binding" + }, + { + "name": "right_global_phase", + "rejected_by": "lean_recipe_binding" + }, + { + "name": "swapped_wrappers", + "rejected_by": "lean_recipe_binding" + }, + { + "name": "wrong_wrapper_translation", + "rejected_by": "lean_recipe_binding" + } + ] + }, + "backward": { + "events": 24767, + "scalar_operations": 19693, + "local_registers": 704, + "private_registers": 8, + "pre_wrapper_index": 7852, + "post_wrapper_index": 24562, + "helper_climbs": [ + { + "index": 13948, + "phase": "B", + "from": 2, + "to": 31, + "rank": 2 + }, + { + "index": 14143, + "phase": "B", + "from": 31, + "to": 556, + "rank": 3 + }, + { + "index": 15146, + "phase": "B", + "from": 556, + "to": 751, + "rank": 1 + }, + { + "index": 16494, + "phase": "cleanup_tail", + "from": 751, + "to": 999, + "rank": 1 + } + ], + "helper_scalar_touches": [ + { + "index": 12769, + "phase": "B", + "event": [ + "scalar", + [ + "add", + [ + "L", + 450 + ], + [ + "L", + 157 + ], + -1, + 2 + ], + 2 + ] + }, + { + "index": 12771, + "phase": "B", + "event": [ + "scalar", + [ + "add", + [ + "L", + 450 + ], + [ + "L", + 219 + ], + -1, + 2 + ], + 2 + ] + }, + { + "index": 13949, + "phase": "B", + "event": [ + "scalar", + [ + "add", + [ + "L", + 230 + ], + [ + "L", + 450 + ], + -1, + 1 + ], + 31 + ] + }, + { + "index": 14144, + "phase": "B", + "event": [ + "scalar", + [ + "add", + [ + "L", + 450 + ], + [ + "L", + 508 + ], + -1, + 1 + ], + 556 + ] + }, + { + "index": 15147, + "phase": "B", + "event": [ + "scalar", + [ + "add", + [ + "L", + 450 + ], + [ + "L", + 219 + ], + 1, + 2 + ], + 751 + ] + }, + { + "index": 16495, + "phase": "cleanup_tail", + "event": [ + "scalar", + [ + "add", + [ + "L", + 450 + ], + [ + "L", + 508 + ], + 1, + 1 + ], + 999 + ] + }, + { + "index": 16507, + "phase": "cleanup_tail", + "event": [ + "scalar", + [ + "add", + [ + "L", + 230 + ], + [ + "L", + 450 + ], + 1, + 1 + ], + 999 + ] + } + ], + "unit_row": [ + [ + [ + "L", + 450 + ], + "1" + ] + ], + "isolated_column": [ + [ + [ + "L", + 450 + ], + "1" + ] + ], + "all_scalar_frame_tags_consistent": true, + "controls": [ + { + "name": "missing_pre_wrapper", + "rejected_by": "wrapper_enclosure" + }, + { + "name": "pre_names_full_terminal", + "rejected_by": "wrapper_terminal" + }, + { + "name": "missing_post_wrapper", + "rejected_by": "wrapper_inventory" + }, + { + "name": "post_before_last_touch", + "rejected_by": "post_wrapper_order" + }, + { + "name": "wrong_old_climb_frame", + "rejected_by": "climb_old_frame" + }, + { + "name": "wrong_scalar_frame", + "rejected_by": "scalar_frame" + }, + { + "name": "drop_final_tail_touch", + "rejected_by": "helper_isolated_column" + }, + { + "name": "wrong_final_tail_sign", + "rejected_by": "helper_isolated_column" + }, + { + "name": "restored_row_but_dirt_leak", + "rejected_by": "helper_isolated_column", + "unit_row_preserved": true, + "leaked_register": [ + "L", + 27 + ], + "exact_coefficient": "1" + }, + { + "name": "read_after_post_wrapper", + "rejected_by": "wrapper_enclosure" + }, + { + "name": "left_global_phase", + "rejected_by": "lean_recipe_binding" + }, + { + "name": "right_global_phase", + "rejected_by": "lean_recipe_binding" + }, + { + "name": "swapped_wrappers", + "rejected_by": "lean_recipe_binding" + }, + { + "name": "wrong_wrapper_translation", + "rejected_by": "lean_recipe_binding" + } + ] + } + }, + "scope": "Finite scalar row/column, emitted frame tags, wrapper placement and literal recipe binding. No fresh Lean build or general JSON-to-Lean translation proof; exact lowering of other events, physical hosting, all-size compilation, costs and analytic transfer remain separate." +} diff --git a/research/k8-hpe450-binding/SOURCES.json b/research/k8-hpe450-binding/SOURCES.json new file mode 100644 index 0000000000..e9441e66ad --- /dev/null +++ b/research/k8-hpe450-binding/SOURCES.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "base_commit": "ebedc0895eb4c06725af020bc1af165722b0a3ce", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-local/inputs/phase-baseline/CANONICAL-WORD.json.gz", + "usage": "input", + "git_blob": "cbb49a627768c42e1ff752f43ccfcc56ffe2cb0b", + "sha256": "e070ae2c78b4a1b644b418774af62b40d8d16e6ba89602f0474afb557d507c37" + }, + { + "path": "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_audit_and_transport.py", + "usage": "input", + "git_blob": "d5d3509d90c01fd91dd00b78743287614b532e48", + "sha256": "c9a05ff291016b870b4fc925b317abd9c3a604c73ffc8920dfdbbeb475e20aa3" + }, + { + "path": "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_emit_local.py", + "usage": "input", + "git_blob": "534fdc71f7641c704575efc038363d7eb206b2df", + "sha256": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805" + }, + { + "path": "research/gauge44-slots/construction/slots/SLOT-PINS-k8.json", + "usage": "input", + "git_blob": "2702c368f4de0b671577aee9a0e2df41c1b27658", + "sha256": "55dd229684febecb80638eff9c6b3986623e8539c6c956753b350209c3e0efe2" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean", + "usage": "input", + "git_blob": "1af33a206a9ba6c4826b3a1516d104e770380869", + "sha256": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Main.lean", + "usage": "input", + "git_blob": "88fcee53762abdd2a17c9cc3a26fef74945f0171", + "sha256": "221a5126ec46141e5cba7689aaddd38746183ed15fa91ec229e32a16302b42a6" + }, + { + "path": "research/t16-owner-audit-seed67/inputs/k8-seven-slot-word.json.gz", + "usage": "input", + "git_blob": "723decbca8995e916d6f4b783aa3e1ddd4eb47fe", + "sha256": "49596aa4ed4fd36cd4582fd0e8ddeb09fd80370a7d8aea1ede52a135b536d289" + }, + { + "path": "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_adapters_local.py", + "usage": "input", + "git_blob": "8f77ccf02d01330a197e1c8127ac62b13923c57c", + "sha256": "eb0b5c6c7161e18dc22168da3211448d321586edd15bcfb4b4741174d36993cf" + }, + { + "path": "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-global/vendor531/vendor/clifford/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/e8-lemma-g-lean/LemmaG/Stream.lean", + "usage": "input", + "git_blob": "e89897190307a6f3fcfb858f8de00cc5a7f49b3e", + "sha256": "7138f4b859d0574a803e99401f05ef5e0ec9eeac0eb480775cd9b86595c365f8" + } + ] +} diff --git a/research/k8-hpe450-binding/TASK.json b/research/k8-hpe450-binding/TASK.json new file mode 100644 index 0000000000..6cda2c6827 --- /dev/null +++ b/research/k8-hpe450-binding/TASK.json @@ -0,0 +1,104 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 2, + "base_commit": "ebedc0895eb4c06725af020bc1af165722b0a3ce", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "starting_points": [ + "certificates/selected-result.json", + "research/hyperplane-end-lean/PROOF.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding" + ] + }, + "scope_status": "refined", + "actual_scope": "Bind raw helper 450 of the pinned seven-slot k8 word to Lean pair3: exact scalar row and column, actual emitted wrapper positions, frame chronology, and both serialized wrapper recipes.", + "scope_change_reason": "PR1415 already audits the three operator identities; its explicit next question is their connection to a real emitted helper. This narrows the audit to one current-word helper and leaves global hosting separate.", + "bottleneck_link": "Connect finite emitted-word facts to the actual hypotheses of the retained HPE helper theorem without changing the supplier or kappa.", + "budget_minutes": 60, + "stop_rule": "One helper, two local orientations, exact rational scalar checks and explicit semantic mutants; stop after 45 minutes of investigation and reserve 15 minutes for checking and handoff.", + "outcome": "completed", + "evidence": "RESULT.json: both 24,767-event orientations, 19,693 scalar operations each; exact helper450 unit row and isolated column; pair3 wrapper recipe and chronological frame binding; 28 semantic controls. test_verify.py independently checks 512 short words against dense matrices and tests source/receipt drift and optimized relocation.", + "author": "Hanson Sun (@bbMisk), with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for implementation, analysis, validation and prose; no independent human review.", + "open_questions": [ + { + "question": "Can these finite facts be exported as an actual Lean Event word and connected to hpe_block without a manual serialization boundary?", + "why_it_matters": "The Python row, frame and wrapper checks are evidence about serialized events; an explicit correspondence would reduce the remaining theorem-to-emission gap.", + "first_step": "Specify COPY/CLEAR private-register lifetimes and wrapper labels, then formalize their event translation for this one helper.", + "blocked_by": "No general JSON-to-Lean event-semantics correspondence is supplied here." + }, + { + "question": "Can this local helper binding be connected to every actual hosted invocation in the selected owner map?", + "why_it_matters": "The local certificate alone does not establish nonempty disjoint physical footprints or whole-call realization.", + "first_step": "Trace helper450 through the pinned T16 owner map and existing chart/route evidence, retaining exact call and source identities.", + "blocked_by": "Physical hosting and exact compiled recipes for all relevant events remain outside this local audit." + } + ], + "selection_nonce": "7fff7b3cd0d148756c5fc7685585eb0a", + "scope_key": "e3ffea67887eeb4c396c/k8-seven-slot/raw-helper450/pair3/emitted-boundary", + "nearest_overlap": [ + { + "pr": 1415, + "head": "0d8d2c3a96346756f02563b401a042ab97198e20", + "delta": "Actual selected-word helper and chronological/scalar hypotheses; no reimplementation of the 512-column kernel audit." + } + ], + "cost_effect": "No profile, precision or kappa change is proposed.", + "method": "Independently replay the chosen output row backwards and its input column forwards over exact rationals; independently track emitted labels and wrappers. Compare actual frames and recipes with pair3 literals.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1394#discussioncomment-18914238", + "submission_guidance_check": { + "main_commit": "81e81af67714bdc8d1693b0bf5c29468b92f62ff", + "priority_revision": 3, + "finding": "Revision 3 changes structural/packing priorities; the independent-verification track and assigned formal-interface-lemma card are unchanged. All live inputs and the selected result are unchanged from the starting main." + }, + "overlap_refresh": { + "searched_at": "2026-10-14T03:54:22.715496+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T03:53:55.501511+00:00", + "complete_pagination": true, + "records": 733 + }, + "discussions": { + "fetched_at": "2026-10-14T03:54:22.674363+00:00", + "complete_pagination": true, + "records": 244 + } + }, + "warnings": [], + "nearest_external_pr": { + "number": 1415, + "head": "0d8d2c3a96346756f02563b401a042ab97198e20" + }, + "finding": "Matches are PR1415, its discussion, this claim and this local package. No competing helper450 binding found in the helper coverage; not a novelty guarantee. PR diffs and arbitrary nested files are outside the overlap helper scope." + } +} diff --git a/research/k8-hpe450-binding/VERIFY.json b/research/k8-hpe450-binding/VERIFY.json new file mode 100644 index 0000000000..3c84195008 --- /dev/null +++ b/research/k8-hpe450-binding/VERIFY.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-global/vendor531/vendor/clifford/clifford_exact.py", + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-local/inputs/phase-baseline/CANONICAL-WORD.json.gz", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_adapters_local.py", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_audit_and_transport.py", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_emit_local.py", + "research/e8-lemma-g-lean/LemmaG/Stream.lean", + "research/gauge44-slots/construction/slots/SLOT-PINS-k8.json", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean", + "research/hyperplane-end-lean/HyperplaneEnd/Main.lean", + "research/t16-owner-audit-seed67/inputs/k8-seven-slot-word.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Rebuild pinned k8 emission; independently verify helper450 scalar row/column, frame tags, wrapper chronology and Lean pair3 recipe binding; reject 28 semantic controls and compare the full deterministic receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 300, + "checks": "Dense-matrix cross-check on all 512 three-operation words and three local coordinates; source/receipt mutation controls; read-only optimized source export without Git." + } + ] +} diff --git a/research/k8-hpe450-binding/test_verify.py b/research/k8-hpe450-binding/test_verify.py new file mode 100644 index 0000000000..3104297d69 --- /dev/null +++ b/research/k8-hpe450-binding/test_verify.py @@ -0,0 +1,136 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +# Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. +"""Dense algebra cross-check and source-export failure controls.""" +from fractions import Fraction +import importlib.util +import itertools +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("hpe450_verify", HERE / "verify.py") +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) + + +def dense_matrix(operations, registers): + """Independent full matrix evaluation, including arbitrary private inputs.""" + n = len(registers) + matrix = [[Fraction(i == j) for j in range(n)] for i in range(n)] + for op in operations: + target = registers.index(tuple(op[1])) + if op[0] == "clear": + matrix[target] = [Fraction(0)] * n + elif op[0] == "copy": + matrix[target] = matrix[registers.index(tuple(op[2]))].copy() + elif op[0] == "scale": + matrix[target] = [x * Fraction(op[2], op[3]) for x in matrix[target]] + else: + source = registers.index(tuple(op[2])) + matrix[target] = [a + Fraction(op[3], op[4]) * b + for a, b in zip(matrix[target], matrix[source])] + return matrix + + +class BindingTests(unittest.TestCase): + def test_sparse_row_and_column_against_dense_matrix(self): + registers = [("L", 0), ("L", 1), ("L", 2), ("C", 0)] + alphabet = [ + ["add", ["L", 0], ["L", 1], 1, 2], + ["add", ["L", 1], ["L", 2], -3, 4], + ["scale", ["L", 0], 2, -1], + ["clear", ["C", 0]], + ["copy", ["C", 0], ["L", 2]], + ["add", ["L", 1], ["C", 0], 1, 1], + ["add", ["C", 0], ["L", 0], 1, 4], + ["scale", ["C", 0], -1, 2], + ] + for word in itertools.product(alphabet, repeat=3): + matrix = dense_matrix(word, registers) + operations = [v.scalar(op) for op in word] + for helper in range(3): + row, column = v.scalar_row_column(operations, helper=helper) + self.assertEqual(row, {r: matrix[helper][j] for j, r in enumerate(registers) + if matrix[helper][j]}) + self.assertEqual(column, {r: matrix[i][helper] for i, r in enumerate(registers) + if matrix[i][helper]}) + + def test_restored_row_does_not_imply_isolated_column(self): + row, column = v.scalar_row_column([v.scalar(["add", ["L", 1], ["L", 0], 3, 2])], helper=0) + self.assertEqual(row, {("L", 0): 1}) + self.assertEqual(column, {("L", 0): 1, ("L", 1): Fraction(3, 2)}) + + def test_structural_failure_controls(self): + for op in (["scale", ["L", 0], 1, 0], ["scale", ["L", 0], True, 1], + ["copy", ["L", 0], ["L", 0]], ["add", ["L", -1], ["L", 1], 1, 1]): + with self.assertRaises(v.Reject): + v.scalar(op) + with self.assertRaisesRegex(v.Reject, "dependent_frame_basis"): + v.span([1, 2, 3]) + with self.assertRaisesRegex(v.Reject, "lean_pair_literal"): + v.literal_pair3("def pair3 : Pair := missing") + with self.assertRaisesRegex(v.Reject, "duplicate_json_key"): + json.loads('{"rank":7,"rank":8}', object_pairs_hook=v.unique_object) + self.assertNotEqual(v.encoded({"rank": 1}), v.encoded({"rank": True})) + + def test_source_tamper_is_rejected_before_execution(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + for row in v.read(HERE / "SOURCES.json")["files"]: + if row["usage"] == "input": + dest = root / row["path"] + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(v.ROOT / row["path"], dest) + self.assertEqual(v.source_check(root), v.source_check()) + with (root / v.SOURCE / "hpe_emit_local.py").open("a") as out: + out.write("\n# changed source\n") + with self.assertRaisesRegex(v.Reject, "source_hash"): + v.source_check(root) + + def test_read_only_optimized_export_and_corrupt_receipt(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + package = root / "research" / HERE.name + package.mkdir(parents=True) + for name in ("verify.py", "SOURCES.json", "RESULT.json"): + shutil.copyfile(HERE / name, package / name) + for row in v.read(HERE / "SOURCES.json")["files"]: + if row["usage"] == "input": + dest = root / row["path"] + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(v.ROOT / row["path"], dest) + files = list(root.rglob("*")) + files = [p for p in files if p.is_file()] + before = {p: p.read_bytes() for p in files} + for p in files: + p.chmod(0o444) + command = [sys.executable, "-I", "-O", "-B", str(package / "verify.py")] + env = dict(os.environ, PYTHONOPTIMIZE="2") + try: + result = subprocess.run(command, cwd=tmp, env=env, capture_output=True, text=True, timeout=180) + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertIn("PASS_K8_HPE450_FINITE_BINDING", result.stdout) + self.assertEqual(before, {p: p.read_bytes() for p in files}) + self.assertEqual(set(files), {p for p in root.rglob("*") if p.is_file()}) + receipt = package / "RESULT.json" + receipt.chmod(0o644) + bad = json.loads(receipt.read_text()) + bad["orientations"]["forward"]["pre_wrapper_index"] += 1 + receipt.write_text(json.dumps(bad)) + result = subprocess.run(command, cwd=tmp, capture_output=True, text=True, timeout=180) + self.assertNotEqual(result.returncode, 0) + self.assertIn("receipt_mismatch", result.stderr) + finally: + for p in files: + p.chmod(0o644) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/k8-hpe450-binding/verify.py b/research/k8-hpe450-binding/verify.py new file mode 100644 index 0000000000..04b46bd90d --- /dev/null +++ b/research/k8-hpe450-binding/verify.py @@ -0,0 +1,414 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +# Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. +"""Finite scalar/chronology/recipe binding for k8 helper 450; no Lean build. + +Pinned producers reconstruct the published event streams. This checker does +not import their replay functions: it pulls one output row backwards and +pushes one input column forwards using exact rational arithmetic. +""" +import argparse +import ast +import copy +from fractions import Fraction +import gzip +import hashlib +import json +import os +from pathlib import Path +import re +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +HELPER = 450 +RAW = "research/t16-owner-audit-seed67/inputs/k8-seven-slot-word.json.gz" +PINS = "research/gauge44-slots/construction/slots/SLOT-PINS-k8.json" +LEAN = "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean" +SOURCE = "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code" +VENDOR = "research/complex-k492-owner-repair/vendor/multicold" +ROUTING = VENDOR + "/vendor/pr558/vendor/pr552/complex-local/inputs/phase-baseline/CANONICAL-WORD.json.gz" +CLIFFORD = VENDOR + "/vendor/pr558/vendor/pr552/complex-global/vendor531/vendor/clifford/clifford_exact.py" +PHASES = ["zero_frame_precondition", "entry_adapters", "A", "centers", "B", + "cleanup_tail", "final", "exit_adapters", "full_frame_cleanup", "done"] + + +class Reject(ValueError): + def __init__(self, code, detail=""): + self.code = code + super().__init__(code + (": " + detail if detail else "")) + + +def need(ok, code, detail=""): + if not ok: + raise Reject(code, detail) + + +def unique_object(items): + out = {} + for key, value in items: + need(key not in out, "duplicate_json_key", key) + out[key] = value + return out + + +def read(path): + data = path.read_bytes() + if path.suffix == ".gz": + data = gzip.decompress(data) + return json.loads(data, object_pairs_hook=unique_object) + + +def encoded(obj): + return json.dumps(obj, sort_keys=True, separators=(",", ":"), allow_nan=False).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def source_check(root=ROOT): + manifest = read(HERE / "SOURCES.json") + rows = [r for r in manifest["files"] if r["usage"] == "input"] + for row in rows: + path = (root / row["path"]).resolve() + need(path.is_relative_to(root.resolve()), "source_path") + need(path.is_file() and sha(path.read_bytes()) == row["sha256"], + "source_hash", row["path"]) + return {row["path"]: row["sha256"] for row in rows} + + +def literal_pair3(text): + # Source pins fix this deliberately narrow parser's language and theorem. + matches = re.findall(r"^def pair3 : Pair := (.*?)\n\n", text, re.S | re.M) + need(len(matches) == 1, "lean_pair_literal") + data = ast.literal_eval(matches[0].replace("⟨", "[").replace("⟩", "]")) + need(isinstance(data, list) and len(data) == 4, "lean_pair_shape") + fields = ("quadratic_rows", "linear_Z4", "matrix_rows", "offset", "phase") + entrance, terminal, left, right = data + return entrance, terminal, dict(zip(fields, left, strict=True)), dict(zip(fields, right, strict=True)) + + +def span(rows): + points = {0} + for row in rows: + need(type(row) is int and 0 < row < 512, "frame_vector") + points |= {p ^ row for p in points} + need(len(points) == 2 ** len(rows), "dependent_frame_basis") + return frozenset(points) + + +def fraction(a, b): + # Inverse scales may serialize a negative denominator; Fraction normalizes it. + need(type(a) is int and type(b) is int and b != 0, "scalar_coefficient") + return Fraction(a, b) + + +def register(value): + need(isinstance(value, list) and len(value) == 2 and + value[0] in ("L", "C") and type(value[1]) is int and + 0 <= value[1] < (704 if value[0] == "L" else 8), "register") + return tuple(value) + + +def scalar(op): + need(isinstance(op, list) and op, "scalar_shape") + tag = op[0] + sizes = {"clear": 2, "copy": 3, "scale": 4, "add": 5} + need(tag in sizes and len(op) == sizes[tag], "scalar_shape") + target = register(op[1]) + source = register(op[2]) if tag in ("add", "copy") else None + need(source != target, "scalar_alias") + q = fraction(*op[3:5]) if tag == "add" else fraction(*op[2:4]) if tag == "scale" else None + return tag, target, source, q + + +def add_value(values, key, amount): + value = values.get(key, Fraction(0)) + amount + if value: + values[key] = value + else: + values.pop(key, None) + + +def scalar_row_column(ops, helper=HELPER): + """Compute e_h^T M and M e_h, including COPY and CLEAR exactly. + + Reverse row propagation multiplies a covector by each gate; it is not + inverse execution. CLEAR drops a coefficient; COPY transfers it to the + source and drops the previous target coefficient. + """ + column = {("L", helper): Fraction(1)} + for tag, target, source, q in ops: + if tag == "clear": + column.pop(target, None) + elif tag == "copy": + column.pop(target, None) + add_value(column, target, column.get(source, Fraction(0))) + elif tag == "scale": + value = column.pop(target, Fraction(0)) + add_value(column, target, q * value) + else: + add_value(column, target, q * column.get(source, Fraction(0))) + row = {("L", helper): Fraction(1)} + for tag, target, source, q in reversed(ops): + if tag == "clear": + row.pop(target, None) + elif tag == "copy": + value = row.pop(target, Fraction(0)) + add_value(row, source, value) + elif tag == "scale": + value = row.pop(target, Fraction(0)) + add_value(row, target, q * value) + else: + add_value(row, source, q * row.get(target, Fraction(0))) + return row, column + + +def sparse(values): + return [[list(key), str(value)] for key, value in sorted(values.items())] + + +def audit(canonical, events, recipe, pair): + """Semantic checks only: no source or event hashes gate the mutations.""" + c = canonical + need(c["v"] == 112 and c["R"] == 480 and c["h"] == 9 and + len(c["start"]) == len(c["final"]) == 704, "local_domain") + frames = c["frames"] + spaces = [span(rows) for rows in frames] + def frame(f): + need(type(f) is int and 0 <= f < len(frames), "frame_index") + return f + for f in c["start"] + c["final"]: + frame(f) + entrance, terminal = c["start"][HELPER], c["final"][HELPER] + E, U, left, right = pair + need(frames[entrance] == E and frames[terminal] == U, "lean_frame_binding") + need(len(spaces[entrance]) == 2 and len(spaces[terminal]) == 256 and + spaces[entrance] <= spaces[terminal], "helper_width") + for key, value in {"frame": entrance, "terminal": terminal, "vectors": E, + "terminal_vectors": U, "entrance_rank": 1, "terminal_rank": 8, + "rank": 7, "left": left, "right": right}.items(): + need(key in recipe and encoded(recipe[key]) == encoded(value), "lean_recipe_binding", key) + current = {("L", r): f for r, f in enumerate(c["start"])} + wrapped = {r for r in range(224, 704) if c["start"][r] != 0 or c["final"][r] != 1} + pre, post, phases, touches, climbs, ops = {}, {}, [], [], [], [] + for index, event in enumerate(events): + need(isinstance(event, list) and event, "event_shape") + tag = event[0] + if tag == "phase": + need(len(event) == 2 and len(phases) < len(PHASES) and + event[1] == PHASES[len(phases)], "phase_order") + phases.append(event[1]) + continue + need(phases and phases[-1] != "done", "event_outside_program") + phase = phases[-1] + if tag == "residual_adapter": + need(len(event) in (4, 5), "wrapper_shape") + kind, r, e = event[1:4] + need(type(r) is int and r in wrapped and e == c["start"][r], "wrapper_entrance") + end = c["final"][r] + need(event[4:] == ([end] if end != 1 else []), "wrapper_terminal") + if kind == "pre": + need(phase == "entry_adapters" and r not in pre and r not in post, "pre_wrapper_order") + pre[r] = index + else: + need(kind == "post" and phase == "full_frame_cleanup" and r in pre and + r not in post and current["L", r] == end, "post_wrapper_order") + post[r] = index + elif tag == "adapter": + need(len(event) == 4, "adapter_shape") + _, direction, r, f = event + need(type(r) is int and 0 <= r < 704 and current["L", r] == frame(f), "adapter_frame") + need((direction == "old_to_new" and phase == "entry_adapters" and r not in wrapped) or + (direction == "new_to_old" and phase == "exit_adapters" and + not (r >= 224 and c["final"][r] != 1)), "adapter_kind") + elif tag == "climb": + need(len(event) == 6, "climb_shape") + _, part, r, old, new, rank = event + need(type(r) is int and 0 <= r < 704 and part == phase and + current["L", r] == frame(old), "climb_old_frame") + frame(new) + need(spaces[old] < spaces[new] and type(rank) is int and + rank == len(frames[new]) - len(frames[old]), "climb_rank") + if r in wrapped: + need(r in pre and r not in post, "wrapper_enclosure") + current["L", r] = new + if r == HELPER: + climbs.append({"index": index, "phase": phase, "from": old, "to": new, "rank": rank}) + elif tag == "center": + need(len(event) == 5 and phase == "centers", "center_shape") + _, k, old, new, rank = event + need(type(k) is int and 0 <= k < 8 and current.get(("C", k)) == frame(old), "center_frame") + frame(new) + need((spaces[old] < spaces[new] or spaces[new] < spaces[old]) and + type(rank) is int and rank == abs(len(frames[new]) - len(frames[old])), "center_rank") + current["C", k] = new + elif tag == "scalar": + need(len(event) == 3, "scalar_event_shape") + f = frame(event[2]) + operation = scalar(event[1]) + op, target, source, _ = operation + if op == "clear": + need(target[0] == "C", "clear_local") + current[target] = f + operands = [target] + ([source] if source is not None else []) + for reg in operands: + if reg[0] == "L" and reg[1] in wrapped: + need(reg[1] in pre and reg[1] not in post, "wrapper_enclosure") + for reg in operands: + need(current.get(reg) == f, "scalar_frame", str(index)) + ops.append(operation) + if ("L", HELPER) in (target, source): + touches.append({"index": index, "phase": phase, "event": event}) + else: + raise Reject("unknown_event", str(tag)) + need(phases == PHASES and set(pre) == set(post) == wrapped, "wrapper_inventory") + need([current["L", r] for r in range(704)] == c["final"], "final_frames") + need(touches and pre[HELPER] < touches[0]["index"] < touches[-1]["index"] < post[HELPER], + "helper_wrapper_order") + need(touches[-1]["phase"] == "cleanup_tail" and + not any(t["phase"] == "full_frame_cleanup" for t in touches), "helper_last_tail") + row, column = scalar_row_column(ops) + unit = {("L", HELPER): Fraction(1)} + need(row == unit, "helper_unit_row", str(sparse(row))) + need(column == unit, "helper_isolated_column", str(sparse(column))) + return {"events": len(events), "scalar_operations": len(ops), "local_registers": 704, + "private_registers": 8, "pre_wrapper_index": pre[HELPER], + "post_wrapper_index": post[HELPER], "helper_climbs": climbs, + "helper_scalar_touches": touches, "unit_row": sparse(row), + "isolated_column": sparse(column), "all_scalar_frame_tags_consistent": True} + + +def controls(c, events, recipe, pair): + """All mutations reach the semantic checker; checksums are not consulted.""" + positive = audit(c, events, recipe, pair) + first = positive["helper_scalar_touches"][0]["index"] + last = positive["helper_scalar_touches"][-1]["index"] + pre = positive["pre_wrapper_index"] + post = positive["post_wrapper_index"] + climb = positive["helper_climbs"][0]["index"] + last_failure = "helper_unit_row" if events[last][1][1] == ["L", HELPER] else "helper_isolated_column" + cases = [] + def event_case(name, code, mutate): + bad = copy.deepcopy(events) + mutate(bad) + cases.append((name, code, c, bad, recipe)) + event_case("missing_pre_wrapper", "wrapper_enclosure", lambda es: es.pop(pre)) + event_case("pre_names_full_terminal", "wrapper_terminal", lambda es: es[pre].__setitem__(4, 1)) + event_case("missing_post_wrapper", "wrapper_inventory", lambda es: es.pop(post)) + event_case("post_before_last_touch", "post_wrapper_order", lambda es: es.insert(last, es.pop(post))) + event_case("wrong_old_climb_frame", "climb_old_frame", lambda es: es[climb].__setitem__(3, 0)) + event_case("wrong_scalar_frame", "scalar_frame", lambda es: es[first].__setitem__(2, 1)) + event_case("drop_final_tail_touch", last_failure, lambda es: es.pop(last)) + event_case("wrong_final_tail_sign", last_failure, lambda es: es[last][1].__setitem__(3, -es[last][1][3])) + # After the last touch h's row cannot change again. A new read of its dirty + # value tests the COLUMN obligation independently of the row. + extra = ["scalar", ["add", ["L", 230], ["L", HELPER], 1, 1], c["final"][HELPER]] + event_case("restored_row_but_dirt_leak", "helper_isolated_column", lambda es: es.insert(last + 1, extra)) + event_case("read_after_post_wrapper", "wrapper_enclosure", lambda es: es.insert(post + 1, extra)) + for side in ("left", "right"): + bad = copy.deepcopy(recipe) + bad[side]["phase"] = (bad[side]["phase"] + 1) % 4 + cases.append((side + "_global_phase", "lean_recipe_binding", c, events, bad)) + bad = copy.deepcopy(recipe) + bad["left"], bad["right"] = bad["right"], bad["left"] + cases.append(("swapped_wrappers", "lean_recipe_binding", c, events, bad)) + bad = copy.deepcopy(recipe) + bad["right"]["offset"] ^= 1 + cases.append(("wrong_wrapper_translation", "lean_recipe_binding", c, events, bad)) + rejected = [] + for name, code, word, program, rec in cases: + try: + audit(word, program, rec, pair) + except Reject as exc: + need(exc.code == code, "wrong_control_rejection", name + ": " + str(exc)) + record = {"name": name, "rejected_by": code} + if name == "restored_row_but_dirt_leak": + row, column = scalar_row_column([scalar(e[1]) for e in program if e[0] == "scalar"]) + need(row == {("L", HELPER): Fraction(1)}, "leak_control_row") + leaked = [(r, q) for r, q in sorted(column.items()) if r != ("L", HELPER)] + need(leaked, "leak_control_column") + record.update(unit_row_preserved=True, leaked_register=list(leaked[0][0]), + exact_coefficient=str(leaked[0][1])) + rejected.append(record) + else: + raise Reject("accepted_mutant", name) + return rejected + + +def rebuild(out, root=ROOT): + """Execute pinned producers sequentially, with assertions in fresh temp output.""" + env = dict(os.environ, MULTICOLD_SOURCE=str(root / VENDOR)) + for key in ("PYTHONOPTIMIZE", "PYTHONPATH", "PYTHONHOME"): + env.pop(key, None) + commands = [ + [root / SOURCE / "hpe_audit_and_transport.py", "--raw", root / RAW, + "--routing", root / ROUTING, "--out", out], + [root / SOURCE / "hpe_emit_local.py", out], + [root / SOURCE / "hpe_adapters_local.py", out / "CANONICAL-WORD.json.gz", + out / "RESIDUAL-ADAPTERS.json", out / "WRAPPER-CHECKS.json"], + ] + for command in commands: + result = subprocess.run([sys.executable, "-I", "-B", *map(str, command)], + cwd=root, env=env, capture_output=True, text=True, timeout=120) + need(result.returncode == 0, "producer_failed", str(command[0]) + "\n" + result.stdout[-1000:] + result.stderr[-1000:]) + cdata = gzip.decompress((out / "CANONICAL-WORD.json.gz").read_bytes()) + c = read(out / "CANONICAL-WORD.json.gz") + programs = read(out / "LOCAL-PROGRAMS.json.gz") + recipes = read(out / "RESIDUAL-ADAPTERS.json") + pins = read(root / PINS) + need(sha(gzip.decompress((root / RAW).read_bytes())) == pins["word_sha256"], "raw_word_pin") + need(sha(cdata) == pins["canonical_sha256"], "canonical_pin") + need(set(programs) == {"forward", "backward"}, "orientations") + for name in programs: + need(sha(encoded(programs[name])) == pins["program_sha256"][name], "program_pin", name) + return c, programs, recipes, pins + + +def compute(): + inputs = source_check() + selected_source = read(ROOT / "research/community-frontier1094-audit/SELECTED-SOURCE.json") + need(selected_source["files"][PINS] == inputs[PINS], "selected_slot_pin_binding") + with tempfile.TemporaryDirectory(prefix="k8-hpe450-") as tmp: + c, programs, recipes, pins = rebuild(Path(tmp) / "local") + pair = literal_pair3((ROOT / LEAN).read_text()) + key = f"{c['start'][HELPER]}:{c['final'][HELPER]}" + need(key in recipes["recipes"], "recipe_key") + recipe = recipes["recipes"][key] + results = {} + for name in ("forward", "backward"): + results[name] = audit(c, programs[name], recipe, pair) + results[name]["controls"] = controls(c, programs[name], recipe, pair) + need(source_check() == inputs, "sources_changed_during_replay") + return {"status": "PASS_K8_HPE450_FINITE_BINDING", "helper": HELPER, + "lean_pair": "HyperplaneEnd.Exact.pair3", "recipe_key": key, + "raw_word_content_sha256": pins["word_sha256"], + "canonical_content_sha256": pins["canonical_sha256"], + "program_sha256": pins["program_sha256"], "input_sha256": inputs, + "recipe": recipe, "orientations": results, + "scope": "Finite scalar row/column, emitted frame tags, wrapper placement and literal recipe binding. " + "No fresh Lean build or general JSON-to-Lean translation proof; exact lowering of other " + "events, physical hosting, all-size compilation, costs and analytic transfer remain separate."} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", type=Path, help="write a new receipt without overwriting an existing file") + args = parser.parse_args() + result = compute() + if args.write_result: + with args.write_result.open("x") as out: + out.write(json.dumps(result, indent=2) + "\n") + else: + need(encoded(result) == encoded(read(HERE / "RESULT.json")), "receipt_mismatch") + print(result["status"] + " helper=450 orientations=2 scalar_row_and_column=exact controls=28 no_new_kappa") + + +if __name__ == "__main__": + try: + main() + except (Reject, OSError, KeyError, TypeError, subprocess.SubprocessError) as exc: + raise SystemExit("FAIL: " + str(exc))