diff --git a/research/hpe-wrapper-event-binding/README.md b/research/hpe-wrapper-event-binding/README.md new file mode 100644 index 0000000000..c3841e33b9 --- /dev/null +++ b/research/hpe-wrapper-event-binding/README.md @@ -0,0 +1,150 @@ +# Bind actual HPE wrapper events to Lean recipe literals + +The opt-in checker accepts all **30 non-cold hyperplane-ended helpers** in both +regenerated selected k8 local programs. Each program has 24,767 events. The +actual pre/post events select `3:998` for 16 helpers and `2:999` for 14 helpers. +Their selected monomials equal the retained Lean `pair2` and `pair3` literals, +including global phase. Every helper's scalar and climb touches lie between +its wrappers, with consistent helper frame tags. + +This is a finite certificate-to-theorem-data binding. It proves no new Lean +statement and makes no supplier or kappa claim. The selected frontier and all +predecessor files remain unchanged. + +## What this adds + +Riquelme Soares's [PR #2706](https://github.com/CrocSwap/integer-mult-bounds/pull/2706), +head `94d77d2cf19b5fbf3d14cd145fc5fd6ad8d24bd6`, shows that two lightweight HPE +checkers do not inspect a synthetic `pre_wrappers` annotation. Those checkers +read canonical words and recipe records, not `LOCAL-PROGRAMS.json.gz`. +The real emitter instead writes events such as: + +```text +["residual_adapter", "pre", 450, 2, 999] +... actual helper touches ... +["residual_adapter", "post", 450, 2, 999] +``` + +The fifth field selects the `2:999` recipe, not the FULL-ended `"2"` recipe. +`factor_iff_pre` requires the executed right monomial to be the certified one. +The new checker reads those actual events and compares the selected right/left +monomials with the Lean pair data. An unused annotation cannot supply a missing +event, and changing that annotation alone does not change execution. + +This is **not a newly discovered production-checker defect**. The retained +`hpe_audit_local.py` already checks emitted wrapper references, order and +presence. Hanson Sun's [k8 helper-450 package](../k8-hpe450-binding/README.md) +also checks wrapper chronology throughout the word and binds helper 450's +recipe and scalar row/column to `pair3`. The new contribution is a reusable, +separately implemented event-to-literal check for every non-cold HPE helper. +It does not repeat the independent Clifford operator audit in +[PR #1415](../hpe-lean-semantic-binding/README.md). + +## Evidence and reproduction + +Base main is `bd1b3bc7174cddbfa4e30ac073dc134f48aa6e77`, priority revision 5. +[TASK.json](TASK.json) records the scope and +[the claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2703). +[SOURCES.json](SOURCES.json) pins every external input. [RESULT.json](RESULT.json) +records all 60 helper/orientation bindings and canonical JSON SHA256 digests +of the regenerated canonical word, complete programs and adapter records. +Gzip headers do not determine equality. + +Run from the repository root with standard-library Python 3.12: + +```sh +python3.12 -B scripts/research_package.py --package research/hpe-wrapper-event-binding +``` + +The registered command checks pins, regenerates the genuine k8 inputs in a +temporary directory, compares the receipt and runs ten tests. Direct commands: + +```sh +python3.12 -I -B research/hpe-wrapper-event-binding/verify.py +python3.12 -I -B -m unittest discover -s research/hpe-wrapper-event-binding -p test_verify.py +python3.12 -I -B research/hpe-wrapper-event-binding/verify.py --run /path/to/emitted/run +``` + +`--run` requires both orientations and checks the supplied artifacts, not their +membership in the selected construction. Without it, the pinned producer harness +reconstructs the selected k8 word and authenticates its canonical/program hashes +against `SLOT-PINS-k8.json`. The selected manifest's slot pin is also checked. +`--write-result NEW_PATH` writes a separate receipt and refuses to overwrite. +Normal verification never rewrites committed evidence. + +The ten tests include **360 per-helper rejection cases**. For both wrapper +sides of every helper in both orientations, they delete the event, omit its +terminal field or change its terminal to FULL. Further controls reject duplicate +and premature wrappers, reads after the post wrapper, an ordinary adapter in +place of a wrapper, changed global phases, substitution of the FULL recipe, +missing recipes, false integer fields, incorrect frame tags and unknown events. +A real CLI negative run also rejects a deleted pre-wrapper under `-O`. +Controls call the semantic checker without checksum rejection as a substitute. + +The tests and receipt replay passed locally on CPython 3.12.15 and 3.13.5 on +Linux. Ruff checks `E4,E7,E9,F,B,I,UP` pass. No Lean build or full +selected cold replay ran. + +## Independence and limits + +`binding.py` imports no producer checker. Its state machine tracks actual helper +touches and reads the event-selected recipe fields. The harness reuses only +`rebuild` from the pinned helper-450 package to generate and authenticate inputs; +it never calls that package's `audit`, `controls` or row/column routines. The +literal reader parses the same three retained data records, not a new proof of +their operator semantics. The original production wrapper audit is pinned as +context and is not the new oracle. + +Coverage excludes cold and FULL-ended helpers. A non-cold HPE pair absent from +the three Lean literals fails rather than silently disappearing from coverage. +The checker assumes the emitter's ZERO/FULL frame-ID convention and validates +it. It checks event grammar and the covered helpers' frame-tag continuity, not +all other roles' labels, subspace incidence or native recipes. + +Scalar endpoint restoration and isolated columns remain separate obligations. +So do `RecipesExact` for other events, serialization-to-Lean correspondence, +footprints, ownership, whole-call hosting, all-size compilation, precision/tape, +complete cost and analytic transfer. Wrapper identity alone does not discharge +`hrec` or instantiate `hpe_word_exact`. + +## Implementation bounds + +The checker has no recursive traversal. It admits at most 4,096 local registers, +4,096 frames with at most nine rows each, and 100,000 events per orientation. +JSON reads stop at 32 MiB of decoded data and reject duplicate keys. Functions +remain below 60 lines. Runtime contracts use exceptions, so `-O` cannot remove +them. Producer subprocesses retain their three explicit 120-second timeouts. + +Power-of-ten deviations for rules 3, 8 and 9 apply to managed-runtime allocation +and dynamic module loading. Python/JSON allocate during checking, but decoded +artifact and collection limits bound live input and state. Temporary producer +output is scoped and removed on every exit. Module loading has only two explicit +local targets, the new checker and the pinned producer harness. It is needed for +isolated script execution and reuse without copying frozen code. The local loader +compiles at most 1 MiB of source per target and never substitutes a timestamp-valid +bytecode cache for that source. The size-limit, optimized rejection, stale-cache +and genuine fixture tests exercise these controls. A future port requiring fixed +allocation must replace JSON/Python; a producer API would remove the dynamic import. +No independent subagent review capability was available in this session. + +## Open next questions + +Can an explicit emitted Lean event word discharge the remaining serialization +boundary? Start with the existing helper-450 row/column certificate and represent +its private COPY/CLEAR lifetimes and extended wrapper labels. This would connect +finite Python evidence to `hpe_block`; the blocker is a correspondence proof, +not another calculation of the three Clifford identities. Physical hosting and +complete supplier admission remain separate even after that proof. + +## Credit and license + +Nick Petalas contributed this successor check. Riquelme Soares supplied the +PR #2706 diagnosis. Hanson Sun supplied the reusable pinned k8 regeneration +harness and helper-450 binding. Jeremy Kothe supplied the HPE formalization and +k8 construction; DreamingOfClouds supplied the wrapper and Lemma A/G work; +icekylinx supplied the retained compiler. Rohan Arun, Josie Elliston and Sagar +Thakrar retain the selected packing, raw-word and independent-audit credit. +Underlying realization credit and notices remain those of the original packages. + +Apache-2.0. Substantial AI assistance covered analysis, implementation, +verification and writing. No independent human review is claimed. diff --git a/research/hpe-wrapper-event-binding/RESULT.json b/research/hpe-wrapper-event-binding/RESULT.json new file mode 100644 index 0000000000..d148e44a0e --- /dev/null +++ b/research/hpe-wrapper-event-binding/RESULT.json @@ -0,0 +1,520 @@ +{ + "status": "PASS_HPE_WRAPPER_EVENT_BINDING", + "input_sha256": { + "research/community-frontier1094-audit/SELECTED-SOURCE.json": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b", + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-global/vendor531/vendor/clifford/clifford_exact.py": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "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/local/hpe_audit_local.py": "6bd9a1e279c9c9e4f3767d9f82e537b559292906feb2ddab02f380fb6523a810", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_adapters_local.py": "eb0b5c6c7161e18dc22168da3211448d321586edd15bcfb4b4741174d36993cf", + "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/e8-lemma-g-lean/LemmaG/Stream.lean": "7138f4b859d0574a803e99401f05ef5e0ec9eeac0eb480775cd9b86595c365f8", + "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/k8-hpe450-binding/SOURCES.json": "bc670b79cad5a75807f1cb529fb5096328b88f144f07d0f44cd202c95d208e36", + "research/k8-hpe450-binding/verify.py": "8df80914e328bb24cfb138efb3dda290d550e803369b36cad8b52ffec8607355", + "research/t16-owner-audit-seed67/inputs/k8-seven-slot-word.json.gz": "49596aa4ed4fd36cd4582fd0e8ddeb09fd80370a7d8aea1ede52a135b536d289", + "scripts/verify_hpe_lean_binding.py": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03" + }, + "canonical_json_sha256": { + "canonical_word": "4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c", + "programs": "9f41d53659e9be84e20c661560c5687abbf5cd0660cdecbe01ad5eb29e6b8ee3", + "adapters": "c682e9ff1b347f89771c6800f46ad98c2bb92b91c5c88452d53a9e7f0180c35f" + }, + "orientations": { + "forward": { + "events": 24767, + "helpers": 30, + "bindings": [ + { + "helper": 448, + "recipe": "3:998", + "pre": 7850, + "first_touch": 12761, + "last_touch": 16503, + "post": 24560 + }, + { + "helper": 449, + "recipe": "3:998", + "pre": 7851, + "first_touch": 12765, + "last_touch": 16505, + "post": 24561 + }, + { + "helper": 450, + "recipe": "2:999", + "pre": 7852, + "first_touch": 12769, + "last_touch": 16507, + "post": 24562 + }, + { + "helper": 451, + "recipe": "2:999", + "pre": 7853, + "first_touch": 12773, + "last_touch": 16509, + "post": 24563 + }, + { + "helper": 452, + "recipe": "2:999", + "pre": 7854, + "first_touch": 12777, + "last_touch": 16511, + "post": 24564 + }, + { + "helper": 453, + "recipe": "2:999", + "pre": 7855, + "first_touch": 12781, + "last_touch": 16513, + "post": 24565 + }, + { + "helper": 454, + "recipe": "3:998", + "pre": 7856, + "first_touch": 12785, + "last_touch": 16515, + "post": 24566 + }, + { + "helper": 455, + "recipe": "3:998", + "pre": 7857, + "first_touch": 12789, + "last_touch": 16517, + "post": 24567 + }, + { + "helper": 484, + "recipe": "3:998", + "pre": 7886, + "first_touch": 12796, + "last_touch": 16519, + "post": 24574 + }, + { + "helper": 485, + "recipe": "3:998", + "pre": 7887, + "first_touch": 12797, + "last_touch": 16521, + "post": 24575 + }, + { + "helper": 508, + "recipe": "2:999", + "pre": 7910, + "first_touch": 12802, + "last_touch": 16523, + "post": 24586 + }, + { + "helper": 509, + "recipe": "2:999", + "pre": 7911, + "first_touch": 12803, + "last_touch": 16525, + "post": 24587 + }, + { + "helper": 531, + "recipe": "2:999", + "pre": 7933, + "first_touch": 13357, + "last_touch": 16643, + "post": 24602 + }, + { + "helper": 532, + "recipe": "2:999", + "pre": 7934, + "first_touch": 12808, + "last_touch": 16527, + "post": 24603 + }, + { + "helper": 533, + "recipe": "2:999", + "pre": 7935, + "first_touch": 12809, + "last_touch": 16529, + "post": 24604 + }, + { + "helper": 543, + "recipe": "2:999", + "pre": 7945, + "first_touch": 13408, + "last_touch": 16646, + "post": 24613 + }, + { + "helper": 554, + "recipe": "3:998", + "pre": 7956, + "first_touch": 8171, + "last_touch": 16629, + "post": 24620 + }, + { + "helper": 555, + "recipe": "3:998", + "pre": 7957, + "first_touch": 13374, + "last_touch": 16631, + "post": 24621 + }, + { + "helper": 556, + "recipe": "3:998", + "pre": 7958, + "first_touch": 12814, + "last_touch": 16531, + "post": 24622 + }, + { + "helper": 557, + "recipe": "3:998", + "pre": 7959, + "first_touch": 12815, + "last_touch": 16533, + "post": 24623 + }, + { + "helper": 566, + "recipe": "3:998", + "pre": 7968, + "first_touch": 12942, + "last_touch": 16633, + "post": 24630 + }, + { + "helper": 567, + "recipe": "3:998", + "pre": 7969, + "first_touch": 12851, + "last_touch": 16635, + "post": 24631 + }, + { + "helper": 584, + "recipe": "3:998", + "pre": 7986, + "first_touch": 12817, + "last_touch": 16535, + "post": 24646 + }, + { + "helper": 585, + "recipe": "3:998", + "pre": 7987, + "first_touch": 12821, + "last_touch": 16537, + "post": 24647 + }, + { + "helper": 586, + "recipe": "2:999", + "pre": 7988, + "first_touch": 8169, + "last_touch": 16638, + "post": 24648 + }, + { + "helper": 587, + "recipe": "2:999", + "pre": 7989, + "first_touch": 12830, + "last_touch": 16539, + "post": 24649 + }, + { + "helper": 588, + "recipe": "2:999", + "pre": 7990, + "first_touch": 8168, + "last_touch": 16641, + "post": 24650 + }, + { + "helper": 589, + "recipe": "2:999", + "pre": 7991, + "first_touch": 12839, + "last_touch": 16542, + "post": 24651 + }, + { + "helper": 590, + "recipe": "3:998", + "pre": 7992, + "first_touch": 12843, + "last_touch": 16544, + "post": 24652 + }, + { + "helper": 591, + "recipe": "3:998", + "pre": 7993, + "first_touch": 12847, + "last_touch": 16546, + "post": 24653 + } + ] + }, + "backward": { + "events": 24767, + "helpers": 30, + "bindings": [ + { + "helper": 448, + "recipe": "3:998", + "pre": 7850, + "first_touch": 12761, + "last_touch": 16503, + "post": 24560 + }, + { + "helper": 449, + "recipe": "3:998", + "pre": 7851, + "first_touch": 12765, + "last_touch": 16505, + "post": 24561 + }, + { + "helper": 450, + "recipe": "2:999", + "pre": 7852, + "first_touch": 12769, + "last_touch": 16507, + "post": 24562 + }, + { + "helper": 451, + "recipe": "2:999", + "pre": 7853, + "first_touch": 12773, + "last_touch": 16509, + "post": 24563 + }, + { + "helper": 452, + "recipe": "2:999", + "pre": 7854, + "first_touch": 12777, + "last_touch": 16511, + "post": 24564 + }, + { + "helper": 453, + "recipe": "2:999", + "pre": 7855, + "first_touch": 12781, + "last_touch": 16513, + "post": 24565 + }, + { + "helper": 454, + "recipe": "3:998", + "pre": 7856, + "first_touch": 12785, + "last_touch": 16515, + "post": 24566 + }, + { + "helper": 455, + "recipe": "3:998", + "pre": 7857, + "first_touch": 12789, + "last_touch": 16517, + "post": 24567 + }, + { + "helper": 484, + "recipe": "3:998", + "pre": 7886, + "first_touch": 12796, + "last_touch": 16519, + "post": 24574 + }, + { + "helper": 485, + "recipe": "3:998", + "pre": 7887, + "first_touch": 12797, + "last_touch": 16521, + "post": 24575 + }, + { + "helper": 508, + "recipe": "2:999", + "pre": 7910, + "first_touch": 12802, + "last_touch": 16523, + "post": 24586 + }, + { + "helper": 509, + "recipe": "2:999", + "pre": 7911, + "first_touch": 12803, + "last_touch": 16525, + "post": 24587 + }, + { + "helper": 531, + "recipe": "2:999", + "pre": 7933, + "first_touch": 13357, + "last_touch": 16643, + "post": 24602 + }, + { + "helper": 532, + "recipe": "2:999", + "pre": 7934, + "first_touch": 12808, + "last_touch": 16527, + "post": 24603 + }, + { + "helper": 533, + "recipe": "2:999", + "pre": 7935, + "first_touch": 12809, + "last_touch": 16529, + "post": 24604 + }, + { + "helper": 543, + "recipe": "2:999", + "pre": 7945, + "first_touch": 13408, + "last_touch": 16646, + "post": 24613 + }, + { + "helper": 554, + "recipe": "3:998", + "pre": 7956, + "first_touch": 8171, + "last_touch": 16629, + "post": 24620 + }, + { + "helper": 555, + "recipe": "3:998", + "pre": 7957, + "first_touch": 13374, + "last_touch": 16631, + "post": 24621 + }, + { + "helper": 556, + "recipe": "3:998", + "pre": 7958, + "first_touch": 12814, + "last_touch": 16531, + "post": 24622 + }, + { + "helper": 557, + "recipe": "3:998", + "pre": 7959, + "first_touch": 12815, + "last_touch": 16533, + "post": 24623 + }, + { + "helper": 566, + "recipe": "3:998", + "pre": 7968, + "first_touch": 12942, + "last_touch": 16633, + "post": 24630 + }, + { + "helper": 567, + "recipe": "3:998", + "pre": 7969, + "first_touch": 12851, + "last_touch": 16635, + "post": 24631 + }, + { + "helper": 584, + "recipe": "3:998", + "pre": 7986, + "first_touch": 12817, + "last_touch": 16535, + "post": 24646 + }, + { + "helper": 585, + "recipe": "3:998", + "pre": 7987, + "first_touch": 12821, + "last_touch": 16537, + "post": 24647 + }, + { + "helper": 586, + "recipe": "2:999", + "pre": 7988, + "first_touch": 8169, + "last_touch": 16638, + "post": 24648 + }, + { + "helper": 587, + "recipe": "2:999", + "pre": 7989, + "first_touch": 12830, + "last_touch": 16539, + "post": 24649 + }, + { + "helper": 588, + "recipe": "2:999", + "pre": 7990, + "first_touch": 8168, + "last_touch": 16641, + "post": 24650 + }, + { + "helper": 589, + "recipe": "2:999", + "pre": 7991, + "first_touch": 12839, + "last_touch": 16542, + "post": 24651 + }, + { + "helper": 590, + "recipe": "3:998", + "pre": 7992, + "first_touch": 12843, + "last_touch": 16544, + "post": 24652 + }, + { + "helper": 591, + "recipe": "3:998", + "pre": 7993, + "first_touch": 12847, + "last_touch": 16546, + "post": 24653 + } + ] + } + }, + "scope": "Actual pre/post event references, literal recipe fields and wrapper enclosure for every non-cold HPE helper. No scalar endpoint, native lowering, cold-helper, hosting, all-size, cost or analytic admission." +} diff --git a/research/hpe-wrapper-event-binding/SOURCES.json b/research/hpe-wrapper-event-binding/SOURCES.json new file mode 100644 index 0000000000..e7ecdf3ae8 --- /dev/null +++ b/research/hpe-wrapper-event-binding/SOURCES.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "base_commit": "bd1b3bc7174cddbfa4e30ac073dc134f48aa6e77", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "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/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/local/hpe_audit_local.py", + "usage": "input", + "git_blob": "17bccb64fdca54f329a3ce16e369449cb76c2802", + "sha256": "6bd9a1e279c9c9e4f3767d9f82e537b559292906feb2ddab02f380fb6523a810" + }, + { + "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-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/e8-lemma-g-lean/LemmaG/Stream.lean", + "usage": "input", + "git_blob": "e89897190307a6f3fcfb858f8de00cc5a7f49b3e", + "sha256": "7138f4b859d0574a803e99401f05ef5e0ec9eeac0eb480775cd9b86595c365f8" + }, + { + "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/k8-hpe450-binding/SOURCES.json", + "usage": "input", + "git_blob": "e9441e66add7a48d0ca8995a1a1c60c0d614c139", + "sha256": "bc670b79cad5a75807f1cb529fb5096328b88f144f07d0f44cd202c95d208e36" + }, + { + "path": "research/k8-hpe450-binding/verify.py", + "usage": "input", + "git_blob": "04b46bd90dd0a4ba807af1f044fe69d803eb6908", + "sha256": "8df80914e328bb24cfb138efb3dda290d550e803369b36cad8b52ffec8607355" + }, + { + "path": "research/t16-owner-audit-seed67/inputs/k8-seven-slot-word.json.gz", + "usage": "input", + "git_blob": "723decbca8995e916d6f4b783aa3e1ddd4eb47fe", + "sha256": "49596aa4ed4fd36cd4582fd0e8ddeb09fd80370a7d8aea1ede52a135b536d289" + }, + { + "path": "scripts/verify_hpe_lean_binding.py", + "usage": "input", + "git_blob": "d295b028edc531dfbfaa023370a9528bada35572", + "sha256": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03" + } + ] +} diff --git a/research/hpe-wrapper-event-binding/TASK.json b/research/hpe-wrapper-event-binding/TASK.json new file mode 100644 index 0000000000..4413e71f7d --- /dev/null +++ b/research/hpe-wrapper-event-binding/TASK.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 5, + "base_commit": "bd1b3bc7174cddbfa4e30ac073dc134f48aa6e77", + "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 actual emitted pre/post residual-adapter events for every non-cold HPE helper in both selected k8 orientations to the retained Lean pair literals, including wrapper enclosure and semantic failure controls.", + "scope_change_reason": "The independent-verification draw offered this formal-interface card. PR2706 diagnoses metadata-only checks; the production audit and helper450 chronology already exist. Add a reusable independent event-to-literal bridge for all 30 non-cold HPE helpers, not another Clifford identity proof or a claim of a production defect.", + "bottleneck_link": "Reduce a specific certificate-to-formal-data binding gap for the selected helper interface without claiming full hrec, supplier admission or a changed primitive budget.", + "budget_minutes": 60, + "stop_rule": "Stop when both pinned genuine orientations pass, every covered helper rejects missing or wrong-terminal wrappers, targeted recipe/order controls reject, and the opt-in CLI and registered replay pass. No family expansion or search.", + "outcome": "completed", + "evidence": "RESULT.json records 30 helper bindings and 24767 actual events per orientation. test_verify.py supplies 360 per-helper controls plus recipe/order/schema and real CLI optimized controls. README.md gives exact commands and limits.", + "author": "Nick Petalas", + "ai_assistance": "Substantial AI assistance in analysis, implementation, verification and writing; no independent human review claimed.", + "selection_seed": "e145f7b4c04e3ac5516d4d7fa2595a7b", + "scope_key": "e3ffea67887eeb4c396c-all-noncold-k8-event-recipe-binding", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2703#discussioncomment-18956980", + "predecessors": { + "PR2706": "94d77d2cf19b5fbf3d14cd145fc5fd6ad8d24bd6", + "selected_k8_binding": "research/k8-hpe450-binding/README.md", + "existing_production_event_audit": "research/complex-sw4-frame8/local/hpe_audit_local.py" + }, + "family_expansion_decision": "Narrow to a verification module. No construction expansion or full-cost claim; cold/native/hosting/consumer/restoration obligations not proved here remain unknown or inherited, not zero-priced.", + "freshness": { + "upstream_main": "25748c3cbcc80cbd7b5245b4be5fcb1213db393f", + "priority_revision": 5, + "checked_at_utc": "2026-10-15T19:51:16Z", + "relevant_change": "Main advanced with unrelated reviewed packages. Priority guidance, selected record and every declared input remain unchanged. Retain the original pinned scientific base and isolated branch; no input migration is needed.", + "overlap": "Complete pagination at submission checkpoint: 741 open PRs including drafts and 1377 discussion records. PR2706 remains open at the same exact head; matches are the predecessor and this claim/package. Title/body/package-note coverage is not a novelty proof." + }, + "open_questions": [ + { + "question": "Can an explicit emitted Lean event word discharge the remaining serialization boundary?", + "why_it_matters": "Connect finite event, recipe and existing helper450 scalar evidence to hpe_block without assuming Python serialization correspondence.", + "first_step": "Represent the helper450 invocation's private COPY/CLEAR lifetimes and extended wrapper labels in the retained event model.", + "blocked_by": "A semantic correspondence proof and remaining RecipesExact premises, not another finite Clifford identity check; physical hosting and complete admission remain separate." + } + ] +} diff --git a/research/hpe-wrapper-event-binding/VERIFY.json b/research/hpe-wrapper-event-binding/VERIFY.json new file mode 100644 index 0000000000..3727925728 --- /dev/null +++ b/research/hpe-wrapper-event-binding/VERIFY.json @@ -0,0 +1,50 @@ +{ + "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/local/hpe_audit_local.py", + "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/k8-hpe450-binding/SOURCES.json", + "research/k8-hpe450-binding/verify.py", + "research/t16-owner-audit-seed67/inputs/k8-seven-slot-word.json.gz", + "scripts/verify_hpe_lean_binding.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Reconstruct the pinned genuine k8 programs and compare every non-cold HPE wrapper event's selected monomial and enclosure with the saved 60-binding receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Genuine emitted positives, 360 per-helper deletion/terminal controls, literal/chronology/schema controls and real CLI rejection under optimization." + } + ] +} diff --git a/research/hpe-wrapper-event-binding/binding.py b/research/hpe-wrapper-event-binding/binding.py new file mode 100644 index 0000000000..6100f00a8f --- /dev/null +++ b/research/hpe-wrapper-event-binding/binding.py @@ -0,0 +1,174 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Check actual non-cold HPE wrapper events, not an auxiliary word annotation. + +This is a finite event-to-literal binding, not a scalar or native replay. +""" +import json + +MAX_REGISTERS = 4096 +MAX_FRAMES = 4096 +MAX_EVENTS = 100_000 +PHASES = ("zero_frame_precondition", "entry_adapters", "A", "centers", "B", + "cleanup_tail", "final", "exit_adapters", "full_frame_cleanup", "done") + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def integer(value, stop): + require(type(value) is int and 0 <= value < stop, "invalid integer index") + return value + + +def same(actual, expected): + # Unlike Python equality, JSON serialization distinguishes true from 1. + return json.dumps(actual, sort_keys=True, allow_nan=False) == json.dumps( + expected, sort_keys=True, allow_nan=False) + + +def target_states(word, pairs): + require(type(word["h"]) is int and word["h"] == 9, "expected nine-dimensional frames") + v = integer(word["v"], MAX_REGISTERS // 2) + n = 2 * v + integer(word["R"], MAX_REGISTERS) + require(0 < n <= MAX_REGISTERS, "register capacity exceeded") + frames = word["frames"] + require(2 <= len(frames) <= MAX_FRAMES, "frame capacity exceeded") + require(frames[0] == [] and frames[1] == [256, 128, 64, 32, 16, 8, 4, 2, 1], + "wrong ZERO or FULL frame convention") + for rows in frames: + require(type(rows) is list and len(rows) <= 9, "invalid frame basis") + for row in rows: + require(type(row) is int and 0 < row < 512, "invalid frame vector") + require(len(word["start"]) == len(word["final"]) == n, "register inventory") + for f in word["start"] + word["final"]: + integer(f, len(frames)) + states = {} + for r in range(2 * v, n): + e, u = word["start"][r], word["final"][r] + if e == 0 or u == 1: + continue # Cold and FULL-ended helpers are explicitly outside this check. + key = (tuple(frames[e]), tuple(frames[u])) + require(key in pairs, "non-cold HPE pair absent from Lean literals") + states[r] = {"entrance": e, "terminal": u, "pair": pairs[key], + "current": e, "pre": None, "post": None, + "first_touch": None, "last_touch": None} + require(states, "no non-cold HPE helpers") + return states, n, len(frames) + + +def wrapper(event, phase, index, state, recipes): + require(len(event) == 5, "HPE wrapper must name its terminal frame") + _, kind, _, e, u = event + require(type(e) is int and type(u) is int and + e == state["entrance"] and u == state["terminal"], "wrong wrapper pair") + key = f"{e}:{u}" + require(key in recipes, "missing event-selected recipe") + recipe = recipes[key] + require(type(recipe["rank"]) is int and recipe["rank"] == 7, "wrong residual rank") + side = "right" if kind == "pre" else "left" + require(same(recipe[side], state["pair"][side]), "event-selected monomial differs from Lean") + if kind == "pre": + require(phase == "entry_adapters" and state["pre"] is None and + state["post"] is None and state["current"] == e, "pre wrapper order") + else: + require(kind == "post" and phase == "full_frame_cleanup" and + state["pre"] is not None and state["post"] is None and + state["current"] == u, "post wrapper order") + state[kind] = index + + +def touch(state, index, frame): + require(state["pre"] is not None and state["post"] is None, + "helper touched outside wrappers") + require(state["current"] == frame, "helper frame mismatch") + if state["first_touch"] is None: + state["first_touch"] = index + state["last_touch"] = index + + +def operands(operation, n): + require(type(operation) is list and operation, "invalid scalar operation") + tag = operation[0] + sizes = {"clear": 2, "copy": 3, "scale": 4, "add": 5} + require(type(tag) is str and tag in sizes and len(operation) == sizes[tag], + "invalid scalar shape") + regs = operation[1:3] if tag in ("copy", "add") else operation[1:2] + for reg in regs: + require(type(reg) is list and len(reg) == 2 and reg[0] in ("L", "C"), + "invalid scalar register") + integer(reg[1], n) + if tag in ("add", "scale"): + numerator, denominator = operation[-2:] + require(type(numerator) is int and type(denominator) is int and + denominator != 0, "invalid scalar coefficient") + return regs + + +def instruction(event, phase, index, states, recipes, n, frame_count): + tag = event[0] + if tag == "residual_adapter": + require(len(event) in (4, 5) and event[1] in ("pre", "post"), "wrapper shape") + r = integer(event[2], n) + integer(event[3], frame_count) + if len(event) == 5: + integer(event[4], frame_count) + if r in states: + wrapper(event, phase, index, states[r], recipes) + elif tag == "adapter": + require(len(event) == 4 and event[1] in ("old_to_new", "new_to_old"), "adapter shape") + r = integer(event[2], n) + integer(event[3], frame_count) + require(r not in states, "ordinary adapter on an HPE helper") + elif tag == "climb": + require(len(event) == 6 and event[1] == phase, "climb shape or phase") + r = integer(event[2], n) + old, new = integer(event[3], frame_count), integer(event[4], frame_count) + require(type(event[5]) is int and 0 < event[5] <= 9, "climb rank") + if r in states: + touch(states[r], index, old) + states[r]["current"] = new + elif tag == "scalar": + require(len(event) == 3, "scalar event shape") + frame = integer(event[2], frame_count) + for tag, r in operands(event[1], n): + if tag == "L" and r in states: + touch(states[r], index, frame) + elif tag == "center": + require(len(event) == 5, "center shape") + integer(event[1], n) + integer(event[2], frame_count) + integer(event[3], frame_count) + require(type(event[4]) is int and 0 < event[4] <= 9, "center rank") + else: + raise ValueError("unknown emitted event tag") + + +def check(word, events, adapters, pairs): + """Bind every non-cold HPE helper; do not silently skip an unknown pair.""" + states, n, frame_count = target_states(word, pairs) + require(type(events) is list and 0 < len(events) <= MAX_EVENTS, "event capacity exceeded") + recipes = adapters["recipes"] + require(type(recipes) is dict and len(recipes) <= MAX_FRAMES, "recipe capacity exceeded") + phases = 0 + for index, event in enumerate(events): + require(type(event) is list and event, "invalid event") + if event[0] == "phase": + require(len(event) == 2 and phases < len(PHASES) and + event[1] == PHASES[phases], "phase order") + phases += 1 + else: + require(0 < phases < len(PHASES), "instruction outside invocation") + instruction(event, PHASES[phases - 1], index, states, recipes, n, frame_count) + require(phases == len(PHASES), "incomplete invocation") + bindings = [] + for r, state in sorted(states.items()): + pre, post = state["pre"], state["post"] + first, last = state["first_touch"], state["last_touch"] + require(pre is not None and post is not None and first is not None and + pre < first <= last < post, "missing wrapper or helper touch") + require(state["current"] == state["terminal"], "wrong final helper frame") + bindings.append({"helper": r, "recipe": f'{state["entrance"]}:{state["terminal"]}', + "pre": pre, "first_touch": first, "last_touch": last, "post": post}) + return {"events": len(events), "helpers": len(bindings), "bindings": bindings} diff --git a/research/hpe-wrapper-event-binding/test_verify.py b/research/hpe-wrapper-event-binding/test_verify.py new file mode 100644 index 0000000000..fcb8c600d1 --- /dev/null +++ b/research/hpe-wrapper-event-binding/test_verify.py @@ -0,0 +1,207 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Real emitted positives and mutations that reach the new semantic check.""" +import copy +import gzip +import importlib.util +import json +import os +import py_compile +import subprocess +import sys +import tempfile +import unittest +from collections import Counter +from pathlib import Path +from unittest.mock import patch + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("hpe_event_verify", HERE / "verify.py") +verify = importlib.util.module_from_spec(spec) +spec.loader.exec_module(verify) +binding = verify.binding + + +class EventBindingTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + verify.sources() + cls.temp = tempfile.TemporaryDirectory(prefix="hpe-event-tests-") + cls.addClassCleanup(cls.temp.cleanup) + cls.run_dir = Path(cls.temp.name) / "local" + cls.word, cls.programs, cls.adapters, _ = verify.fixture_module().rebuild(cls.run_dir) + cls.pairs = verify.literal_pairs() + cls.good = {name: binding.check(cls.word, events, cls.adapters, cls.pairs) + for name, events in cls.programs.items()} + + def test_actual_emitted_positives(self): + self.assertEqual(set(self.good), {"forward", "backward"}) + for row in self.good.values(): + self.assertEqual(row["events"], 24767) + self.assertEqual(row["helpers"], 30) + self.assertEqual(Counter(b["recipe"] for b in row["bindings"]), + {"3:998": 16, "2:999": 14}) + + def rejected(self, events, message, adapters=None, word=None): + with self.assertRaisesRegex(ValueError, message): + binding.check(self.word if word is None else word, events, + self.adapters if adapters is None else adapters, self.pairs) + + def test_every_actual_helper_requires_both_terminal_specific_wrappers(self): + controls = 0 + for name, row in self.good.items(): + events = self.programs[name] + for b in row["bindings"]: + for side in ("pre", "post"): + index = b[side] + with self.subTest(name=name, helper=b["helper"], side=side): + bad = events[:index] + events[index + 1:] + self.rejected(bad, "outside wrappers|missing wrapper") + bad = list(events) + bad[index] = events[index][:-1] + self.rejected(bad, "must name its terminal frame") + bad[index] = events[index][:-1] + [1] + self.rejected(bad, "wrong wrapper pair") + controls += 3 + self.assertEqual(controls, 360) + + def test_duplicate_and_misordered_wrappers(self): + for name, events in self.programs.items(): + b = next(b for b in self.good[name]["bindings"] if b["helper"] == 450) + for side in ("pre", "post"): + i = b[side] + self.rejected(events[:i] + [events[i]] + events[i:], side + " wrapper order") + bad = list(events) + post = bad.pop(b["post"]) + bad.insert(b["first_touch"], post) + self.rejected(bad, "post wrapper order") + extra = ["scalar", ["add", ["L", 230], ["L", 450], 1, 1], 999] + self.rejected(events[:b["post"] + 1] + [extra] + events[b["post"] + 1:], + "helper touched outside wrappers") + bad = list(events) + bad[b["pre"]] = ["adapter", "old_to_new", 450, 2] + self.rejected(bad, "ordinary adapter on an HPE helper") + + def test_event_selected_literal_fields_and_full_recipe(self): + for events in self.programs.values(): + for key in ("3:998", "2:999"): + for side in ("left", "right"): + bad = copy.deepcopy(self.adapters) + bad["recipes"][key][side]["phase"] ^= 1 + self.rejected(events, "monomial differs from Lean", adapters=bad) + bad = copy.deepcopy(self.adapters) + phase = bad["recipes"][key][side]["phase"] + if phase in (0, 1): + bad["recipes"][key][side]["phase"] = bool(phase) + self.rejected(events, "monomial differs from Lean", adapters=bad) + bad = copy.deepcopy(self.adapters) + full = bad["recipes"][key.split(":")[0]]["right"] + self.assertFalse(binding.same(full, bad["recipes"][key]["right"])) + bad["recipes"][key]["right"] = full + self.rejected(events, "monomial differs from Lean", adapters=bad) + bad = copy.deepcopy(self.adapters) + del bad["recipes"][key] + self.rejected(events, "missing event-selected recipe", adapters=bad) + + def test_phantom_metadata_cannot_supply_a_missing_event(self): + word = copy.deepcopy(self.word) + word["pre_wrappers"] = [{"helper": 450, "recipe": "2:999"}] + events = self.programs["forward"] + b = next(b for b in self.good["forward"]["bindings"] if b["helper"] == 450) + self.rejected(events[:b["pre"]] + events[b["pre"] + 1:], + "helper touched outside wrappers", word=word) + word["pre_wrappers"][0]["recipe"] = "2:FULL" + self.assertEqual(binding.check(word, events, self.adapters, self.pairs), self.good["forward"]) + + def test_frame_unknown_event_and_capacity_failures(self): + events = self.programs["forward"] + b = next(b for b in self.good["forward"]["bindings"] if b["helper"] == 450) + bad = list(events) + bad[b["first_touch"]] = list(events[b["first_touch"]]) + self.assertEqual(bad[b["first_touch"]][0], "scalar") + bad[b["first_touch"]][2] = 0 + self.rejected(bad, "helper frame mismatch") + self.rejected(events[:2] + [["unrecognised", 450]] + events[2:], "unknown emitted event") + with patch.object(binding, "MAX_EVENTS", len(events) - 1): + self.rejected(events, "event capacity exceeded") + with patch.object(binding, "MAX_REGISTERS", 600): + self.rejected(events, "register capacity exceeded") + with patch.object(binding, "MAX_FRAMES", len(self.word["frames"]) - 1): + self.rejected(events, "frame capacity exceeded") + word = copy.deepcopy(self.word) + word["start"][450] = True + self.rejected(events, "invalid integer index", word=word) + word = copy.deepcopy(self.word) + word["frames"][1] = [1] + self.rejected(events, "wrong ZERO or FULL frame convention", word=word) + pairs = dict(self.pairs) + del pairs[((30,), (256, 128, 64, 32, 18, 10, 6, 1))] + with self.assertRaisesRegex(ValueError, "pair absent from Lean"): + binding.check(self.word, events, self.adapters, pairs) + + def command(self, run, *extra): + return subprocess.run([sys.executable, "-I", "-B", *extra, str(HERE / "verify.py"), + "--run", str(run)], capture_output=True, text=True, timeout=30) + + def test_real_cli_positive_and_optimized_negative(self): + result = self.command(self.run_dir) + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertIn("PASS_HPE_WRAPPER_EVENT_BINDING", result.stdout) + existing = Path(self.temp.name) / "existing-result.json" + existing.write_bytes(b"keep") + result = subprocess.run([sys.executable, "-I", "-B", str(HERE / "verify.py"), + "--run", str(self.run_dir), "--write-result", str(existing)], + capture_output=True, text=True, timeout=30) + self.assertNotEqual(result.returncode, 0) + self.assertEqual(existing.read_bytes(), b"keep") + with tempfile.TemporaryDirectory(prefix="hpe-bad-event-") as tmp: + run = Path(tmp) + for name in ("CANONICAL-WORD.json.gz", "RESIDUAL-ADAPTERS.json"): + (run / name).write_bytes((self.run_dir / name).read_bytes()) + programs = copy.deepcopy(self.programs) + b = self.good["forward"]["bindings"][0] + del programs["forward"][b["pre"]] + (run / "LOCAL-PROGRAMS.json.gz").write_bytes(gzip.compress(json.dumps(programs).encode())) + result = self.command(run, "-O") + self.assertNotEqual(result.returncode, 0) + self.assertIn("helper touched outside wrappers", result.stderr) + self.assertNotIn("PASS_HPE_WRAPPER_EVENT_BINDING", result.stdout) + + def test_local_loader_uses_source_not_matching_timestamp_cache(self): + with tempfile.TemporaryDirectory(prefix="hpe-pyc-") as tmp: + path = Path(tmp) / "fixture.py" + path.write_text("VALUE = 9\n", encoding="utf-8") + stamp = path.stat() + py_compile.compile(str(path), doraise=True) + path.write_text("VALUE = 1\n", encoding="utf-8") + os.utime(path, ns=(stamp.st_atime_ns, stamp.st_mtime_ns)) + self.assertEqual(verify.load_module(path, "hpe_cache_fixture").VALUE, 1) + path.write_bytes(b" " * (1024 * 1024 + 1)) + with self.assertRaisesRegex(ValueError, "module exceeds 1 MiB limit"): + verify.load_module(path, "hpe_oversize_fixture") + + def test_source_hash_failure(self): + with tempfile.TemporaryDirectory(prefix="hpe-source-drift-") as tmp: + root = Path(tmp) + (root / "input.py").write_bytes(b"changed source") + manifest = {"files": [{"usage": "input", "path": "input.py", "sha256": "0" * 64}]} + with patch.object(verify, "ROOT", root), patch.object(verify, "read", return_value=manifest): + with self.assertRaisesRegex(ValueError, "source hash changed: input.py"): + verify.sources() + with patch.object(verify, "MAX_BYTES", 8): + with self.assertRaisesRegex(ValueError, "source exceeds 32 MiB limit"): + verify.sources() + + def test_json_duplicate_and_decoded_size_limits(self): + with tempfile.TemporaryDirectory(prefix="hpe-json-") as tmp: + path = Path(tmp) / "input.json.gz" + path.write_bytes(gzip.compress(b'{"a": 1, "a": 2}')) + with self.assertRaisesRegex(ValueError, "duplicate JSON key"): + verify.read(path) + path.write_bytes(gzip.compress(b" " * 65)) + with patch.object(verify, "MAX_BYTES", 64): + with self.assertRaisesRegex(ValueError, "decoded limit"): + verify.read(path) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/hpe-wrapper-event-binding/verify.py b/research/hpe-wrapper-event-binding/verify.py new file mode 100644 index 0000000000..71836c2e77 --- /dev/null +++ b/research/hpe-wrapper-event-binding/verify.py @@ -0,0 +1,148 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Bind actual emitted HPE wrappers to retained Lean literals; no new theorem.""" +import argparse +import ast +import gzip +import hashlib +import json +import re +import tempfile +import types +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def load_module(path, name): + # Execute these explicit local sources, never an mtime-valid .pyc instead. + with path.open("rb") as stream: + source = stream.read(1024 * 1024 + 1) + if len(source) > 1024 * 1024: + raise ValueError("local Python module exceeds 1 MiB limit") + module = types.ModuleType(name) + module.__file__ = str(path) + exec(compile(source, str(path), "exec"), module.__dict__) + return module + + +binding = load_module(HERE / "binding.py", "hpe_event_binding") +require = binding.require +same = binding.same +MAX_BYTES = 32 * 1024 * 1024 +LEAN = ROOT / "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean" + + +def unique_object(items): + result = {} + for key, value in items: + require(key not in result, "duplicate JSON key") + result[key] = value + return result + + +def read(path): + opener = gzip.open if path.suffix == ".gz" else open + with opener(path, "rb") as stream: + data = stream.read(MAX_BYTES + 1) + require(len(data) <= MAX_BYTES, "artifact exceeds 32 MiB decoded limit") + return json.loads(data, object_pairs_hook=unique_object) + + +def sources(): + rows = read(HERE / "SOURCES.json")["files"] + result = {} + for row in rows: + if row["usage"] == "input": + path = ROOT / row["path"] + with path.open("rb") as stream: + data = stream.read(MAX_BYTES + 1) + require(len(data) <= MAX_BYTES, "source exceeds 32 MiB limit: " + row["path"]) + digest = hashlib.sha256(data).hexdigest() + require(digest == row["sha256"], "source hash changed: " + row["path"]) + result[row["path"]] = digest + return result + + +def literal_pairs(): + # Only parse the data records. No Lean evaluation or theorem instantiation. + text = LEAN.read_text(encoding="utf-8") + pairs = {} + fields = ("quadratic_rows", "linear_Z4", "matrix_rows", "offset", "phase") + for n in (1, 2, 3): + matches = re.findall(rf"^def pair{n} : Pair := (.*?)\n\n", text, re.S | re.M) + require(len(matches) == 1, "missing or duplicate Lean pair literal") + entrance, terminal, left, right = ast.literal_eval( + matches[0].replace("⟨", "[").replace("⟩", "]")) + key = tuple(entrance), tuple(terminal) + require(key not in pairs, "duplicate Lean frame pair") + pairs[key] = {"left": dict(zip(fields, left, strict=True)), + "right": dict(zip(fields, right, strict=True))} + return pairs + + +def fixture_module(): + # The only dynamic target is the pinned producer harness. Its audit is not called. + path = ROOT / "research/k8-hpe450-binding/verify.py" + return load_module(path, "hpe_k8_producer") + + +def audit_run(run): + word = read(run / "CANONICAL-WORD.json.gz") + programs = read(run / "LOCAL-PROGRAMS.json.gz") + adapters = read(run / "RESIDUAL-ADAPTERS.json") + require(set(programs) == {"forward", "backward"}, "both local orientations required") + pairs = literal_pairs() + orientations = {name: binding.check(word, programs[name], adapters, pairs) + for name in ("forward", "backward")} + artifacts = {name: hashlib.sha256(json.dumps(data, sort_keys=True, + separators=(",", ":"), allow_nan=False).encode()).hexdigest() + for name, data in (("canonical_word", word), ("programs", programs), + ("adapters", adapters))} + return orientations, artifacts + + +def compute(run=None): + inputs = sources() + if run is None: + selected = read(ROOT / "research/community-frontier1094-audit/SELECTED-SOURCE.json") + slot = "research/gauge44-slots/construction/slots/SLOT-PINS-k8.json" + require(selected["files"][slot] == inputs[slot], "selected slot source mismatch") + with tempfile.TemporaryDirectory(prefix="hpe-event-binding-") as tmp: + run = Path(tmp) / "local" + producer = fixture_module() + # Re-read the serialized files instead of trusting returned Python objects. + producer.rebuild(run) + orientations, artifacts = audit_run(run) + else: + orientations, artifacts = audit_run(run) + require(sources() == inputs, "sources changed during replay") + return {"status": "PASS_HPE_WRAPPER_EVENT_BINDING", "input_sha256": inputs, + "canonical_json_sha256": artifacts, "orientations": orientations, + "scope": "Actual pre/post event references, literal recipe fields and wrapper enclosure " + "for every non-cold HPE helper. No scalar endpoint, native lowering, " + "cold-helper, hosting, all-size, cost or analytic admission."} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--run", type=Path, help="check an existing emitted run instead of regenerating k8") + parser.add_argument("--write-result", type=Path, help="create a new receipt; never overwrite") + args = parser.parse_args() + result = compute(args.run) + if args.write_result: + with args.write_result.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(result, indent=2) + "\n") + elif args.run is None: + require(same(result, read(HERE / "RESULT.json")), "receipt mismatch") + for name, row in result["orientations"].items(): + print(f'{name}: {row["helpers"]} non-cold HPE helpers, {row["events"]} events') + print(result["status"]) + + +if __name__ == "__main__": + try: + main() + except (ValueError, OSError, KeyError, TypeError, RecursionError) as exc: + raise SystemExit("FAIL: " + str(exc)) from None