diff --git a/research/hpe-axiom-inventory-audit/README.md b/research/hpe-axiom-inventory-audit/README.md new file mode 100644 index 0000000000..2563566317 --- /dev/null +++ b/research/hpe-axiom-inventory-audit/README.md @@ -0,0 +1,130 @@ +# HPE axiom-probe inventory audit + +The retained standalone HPE verifier can print `PASS` after its axiom checks +silently lose coverage. Removing all queries makes it report **0 results**. +Indenting all 42 queries has the same effect, although Lean 4.21 accepts the +indentation and emits the reports. This package reproduces that driver behavior +and supplies a proposed [repair](repair.patch). It establishes no false HPE +theorem and no new multiplication bound. + +The original driver, Lean files, selected record and frozen evidence are +unchanged. Apply the patch only in a separately reviewed successor. Its explicit +42-name inventory must be deliberately maintained when the intended theorem +inventory changes. + +## Evidence and repair + +The audited driver is `research/hyperplane-end-lean/verify.py`, SHA256 +`2b94b629b2c5d091b1a3ff06ce0fbee1cf178521ccb6ac97843c5c456dfd5eb8`, at base +`ebedc0895eb4c06725af020bc1af165722b0a3ce`. It derives `wanted` from lines that +start at column zero with `#print axioms`, then checks only that list. It has no +separate required inventory. Its report dictionary also overwrites duplicates. + +[verify.py](verify.py) runs the original and patched `main()` in temporary copies +of their pinned source inputs. **The build and probe subprocess results are +substituted test transcripts.** These are controlled driver tests, not historical +HPE logs or fresh HPE builds. [RESULT.json](RESULT.json) records all 100 cases. + +| Case | Original driver | Proposed repair | +|---|---|---| +| Complete 42-probe inventory | Accepts, reports 42 | Accepts, reports 42 | +| Import-only query file | Accepts, reports 0 | Rejects before building | +| Each single query omitted, with its report omitted | Accepts, reports 41, in all 42 cases | Rejects all 42 before building | +| All queries indented, healthy reports supplied | Accepts, reports 0 | Accepts, reports 42 | +| Indented queries, one forbidden dependency supplied | Accepts, reports 0 | Rejects | +| Duplicate or unexpected report | Accepts | Rejects | +| One report missing while its query remains | Rejects in all 42 cases | Preserves all 42 rejections | + +The repair checks the exact required query inventory before either expensive +subprocess. It then requires one report per required name and retains the +`propext`, `Classical.choice`, `Quot.sound` allowlist. Complete axiom-free, +reordered, indented and multiline-report controls pass. The tests reject four +weakened repairs: removing the query inventory guard, permitting duplicate +report overwrites, ignoring extra reports, or disabling the axiom allowlist. + +A separate **real Lean 4.21.0** run produced [fixtures/lean421.txt](fixtures/lean421.txt) +from three tiny [syntax fixtures](fixtures/ProbeSyntax.lean). It confirms the +message syntax, valid indentation, a permitted `propext` dependency and a +forbidden dependency. The fixture deliberately declares an extra axiom solely +as a negative control; it is not imported by any HPE theorem. Compiler/version, +source and output hashes are in [fixtures/LEAN.json](fixtures/LEAN.json). + +The six adversarial test groups also check source and receipt corruption, +transcript corruption, overwrite refusal, and a read-only relocated replay +under optimized Python. The registered replay passed on CPython 3.12.13; +standalone replay was also checked on CPython 3.14.6 with `-I -B -O`. + +## Reproduce + +From the repository root, with Git and Python 3.12; no Python dependencies: + +```sh +python3.12 -I -B scripts/research_package.py --package research/hpe-axiom-inventory-audit +``` + +Expected final line: + +```text +PASS_REGISTERED_RESEARCH_PACKAGE research/hpe-axiom-inventory-audit outcome=completed +``` + +To independently regenerate the small compiler transcript, using an actual +Lean 4.21.0 binary, rather than an elan shim: + +```sh +python3.12 -I -B research/hpe-axiom-inventory-audit/check_lean.py --lean /path/to/lean-4.21.0/bin/lean +``` + +Default verification is read-only. The optional `--write-receipt` and `--record` +modes refuse to overwrite evidence. [SOURCES.json](SOURCES.json) binds all 21 +consumed external files; the package runner additionally verifies Git provenance. + +## Limits + +The unmodified pinned probe file already contains all 42 expected names. These +experiments do not refute its previously recorded axiom results. A separate +immutable-source check would also detect a changed probe file; this result +concerns the standalone driver's coverage contract. + +No HPE/Mathlib build, Lean kernel replay of the HPE theorems, selected-construction +cold replay, supplier admission, or new kappa is claimed. The repaired driver +still trusts the invoked compiler and its output. Its source scanner and probe +parser are not a general Lean parser or a defense against fabricated output. +The full repaired HPE build remains an adoption check. + +## Open next questions + +Can the proposed repair be adopted while preserving the full pinned HPE build +and the 42 actual reports? This matters because the controlled tests establish +driver behavior, not full-build compatibility. The first step is to apply +`repair.patch` in an isolated successor and run the original combined HPE +verification with Lean/Mathlib 4.21.0. That requires the complete dependency +setup and an explicit decision about successor source pins; frozen receipts +must not be rewritten. The structured question is in [TASK.json](TASK.json). + +## Credit and scope + +Jeremy Kothe (`jeremykothe2`, PR593) supplied the audited HPE driver and formal +package; DreamingOfClouds supplied PR599 and the Lemma A/G lineage. Their +[source notice](../hyperplane-end-lean/NOTICE.md) retains the construction, +realization and Clifford credits. No predecessor implementation is vendored; +the proposed patch retains its notice. + +`commdata2338`'s [PR1415](https://github.com/CrocSwap/integer-mult-bounds/pull/1415) +already audits the three HPE pairs' operator semantics. WeberChen8128's +[PR893](https://github.com/CrocSwap/integer-mult-bounds/pull/893) already uses +exact command/report coverage for the separate PR236 historical corpus. The +general coverage principle is prior work; this contribution adds the specific +HPE failure reproductions, repair and executable controls. No code is imported +from either audit. + +The assigned `formal-interface-lemma` scope changed to this verification-coverage +prerequisite after overlap review. It is a tooling side result, not a new formal +lemma. [Discussion1593](https://github.com/CrocSwap/integer-mult-bounds/discussions/1593) +and [TASK.json](TASK.json) record the scope and overlap limits. + +Prepared for Hanson Sun (`bbMisk`) with substantial OpenAI Codex assistance in +investigation, implementation, verification and writing. No subagents or +independent human review. New material is Apache-2.0. Emulate was unavailable; +prose was checked against sources and executed evidence under the donor's +instruction to disclose that limitation. diff --git a/research/hpe-axiom-inventory-audit/RESULT.json b/research/hpe-axiom-inventory-audit/RESULT.json new file mode 100644 index 0000000000..83f63226be --- /dev/null +++ b/research/hpe-axiom-inventory-audit/RESULT.json @@ -0,0 +1,1758 @@ +{ + "status": "PASS_HPE_AXIOM_INVENTORY_AUDIT", + "scope": "Python control-flow audit using substituted subprocess results; real Lean 4.21 syntax fixture only, not an HPE build or theorem audit.", + "source_driver_sha256": "2b94b629b2c5d091b1a3ff06ce0fbee1cf178521ccb6ac97843c5c456dfd5eb8", + "source_queries_sha256": "4d989c6af78020485f81f68ea9c067c4525a6844bc1a474686c1f134e1fd4b86", + "repair_patch_sha256": "f673d4165d0f7c91d0de4be58e3491f22eabad2bf3f00d567e9e5a197e2d5e95", + "repaired_driver_sha256": "ba6be00623fc3836112cefece845b98829db7e908793a525f11d83678dfa5380", + "required_probes": [ + "HyperplaneEnd.pre_recipe", + "HyperplaneEnd.post_recipe", + "HyperplaneEnd.wrapped_block", + "HyperplaneEnd.factor_of_exact", + "HyperplaneEnd.factor_iff_pre", + "HyperplaneEnd.tail_labels", + "HyperplaneEnd.hpe_labels", + "HyperplaneEnd.residual_block", + "HyperplaneEnd.hpe_block", + "HyperplaneEnd.hpe_family", + "HyperplaneEnd.hpe_streams", + "HyperplaneEnd.hpe_word", + "HyperplaneEnd.hyperplane_width", + "HyperplaneEnd.Clifford.par9_spec", + "HyperplaneEnd.Clifford.cE", + "HyperplaneEnd.Clifford.cL_emb", + "HyperplaneEnd.Clifford.cL_eq_of_check", + "HyperplaneEnd.Exact.rTensor_C7", + "HyperplaneEnd.Exact.exact_N_of_check", + "HyperplaneEnd.Exact.check1", + "HyperplaneEnd.Exact.check2", + "HyperplaneEnd.Exact.check3", + "HyperplaneEnd.Exact.exact_N_pair1", + "HyperplaneEnd.Exact.exact_N_pair2", + "HyperplaneEnd.Exact.exact_N_pair3", + "HyperplaneEnd.Exact.exact_N", + "HyperplaneEnd.Exact.exact_N_nine", + "HyperplaneEnd.Exact.hpe_word_exact", + "HyperplaneEnd.labRun_climb", + "HyperplaneEnd.wellLabelled_climb", + "HyperplaneEnd.labRun_block", + "HyperplaneEnd.wellLabelled_block", + "HyperplaneEnd.mtail_wellLabelled", + "HyperplaneEnd.labRun_mtail", + "HyperplaneEnd.labRun_mtail_last", + "HyperplaneEnd.posts_spec", + "HyperplaneEnd.hpe_labels_multi", + "HyperplaneEnd.tail_eq_mtail", + "HyperplaneEnd.hpe_labels_tail", + "HyperplaneEnd.hpe_word_multi", + "HyperplaneEnd.exact_cold", + "HyperplaneEnd.cold_hyperplane_width" + ], + "driver_cases": 100, + "omitted_queries_rejected_before_build": 42, + "existing_missing_report_rejections_preserved": 42, + "real_lean_syntax_cases": 3, + "cases": [ + { + "case": "complete_allowed_inventory", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 42, + "subprocess_calls": 2, + "stdout_sha256": "18363cc2019fca46131206eed5eb0aac2499c8ea949da2fbf5f7a0b44749f7a6" + }, + "repaired": { + "accepted": true, + "exit_code": 0, + "reported_results": 42, + "subprocess_calls": 2, + "stdout_sha256": "18363cc2019fca46131206eed5eb0aac2499c8ea949da2fbf5f7a0b44749f7a6" + } + }, + { + "case": "complete_axiom_free_inventory", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 42, + "subprocess_calls": 2, + "stdout_sha256": "50da68ea6c262a9b6ef241981f21da5eccd04ebf45f9cfe55d56c0014081bcc8" + }, + "repaired": { + "accepted": true, + "exit_code": 0, + "reported_results": 42, + "subprocess_calls": 2, + "stdout_sha256": "50da68ea6c262a9b6ef241981f21da5eccd04ebf45f9cfe55d56c0014081bcc8" + } + }, + { + "case": "reordered_queries_and_reports", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 42, + "subprocess_calls": 2, + "stdout_sha256": "6de4155ecbe45ef8125d5caf996ec1725bd98ad2832271e32adb8f9d5770e97b" + }, + "repaired": { + "accepted": true, + "exit_code": 0, + "reported_results": 42, + "subprocess_calls": 2, + "stdout_sha256": "6de4155ecbe45ef8125d5caf996ec1725bd98ad2832271e32adb8f9d5770e97b" + } + }, + { + "case": "wrapped_allowed_axiom_lists", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 42, + "subprocess_calls": 2, + "stdout_sha256": "13eaf5296f9e41bba318ba58dea98161c2a677b153fb1acd752d359de119e2c7" + }, + "repaired": { + "accepted": true, + "exit_code": 0, + "reported_results": 42, + "subprocess_calls": 2, + "stdout_sha256": "13eaf5296f9e41bba318ba58dea98161c2a677b153fb1acd752d359de119e2c7" + } + }, + { + "case": "empty_inventory", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 0, + "subprocess_calls": 2, + "stdout_sha256": "60f597f9285c93ecf4045e4e96d0f247884525b481e574a0c5c827e3985dba1f" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_query:HyperplaneEnd.pre_recipe", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "3b3f79c76fcc4b855119b52b1930d94c4be468c8fa613b8662862a2e98fff6f3" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.pre_recipe", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "9e6a507f92f9c413c6a01fd071839fbe014bb7fc94cda7a5987a060c4bc97060" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "2b02a39be2bafc132aa1e5da0131b7535942a75969e334c4f8f0bb9083c429d8" + } + }, + { + "case": "omit_query:HyperplaneEnd.post_recipe", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "3c0cd5986563f12ae127e59ab460b2deb9fe93dfbec4a5d51a02b9037d68c9e8" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.post_recipe", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "7170159a8e4e46471fe423df935a47bca9360c06a0588996f044dafcce969c19" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "dcf354f12a16425c5c81e0e0021c1266a8b8b2477a803f28ab8e2769402d9178" + } + }, + { + "case": "omit_query:HyperplaneEnd.wrapped_block", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "1dd4e0f5114c6c4ec9dab9bf8c578f4670dd25069d18ba5e35bd4cceed59b77c" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.wrapped_block", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "9b1074497396c6ea9bac23ff6232d17da3e2c19de507fe801d362bacab24f71d" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "4f9b4f427a978a86ba135b90f1c62f2c0463a0a6a9f35ec36715da61b6642bf4" + } + }, + { + "case": "omit_query:HyperplaneEnd.factor_of_exact", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "86e7acebb07abdcb60d627a9f510e0dc58e3244cfdc70d4ce8f8b274d9402ebd" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.factor_of_exact", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "fa863d198c51d282841cc979c5f2e19d91de4123ec94aabb734efe763a6330f2" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "7bab356e1db5f601a43b1460a236ad2c2a952153aaa14fcbe66751dddb7c69cf" + } + }, + { + "case": "omit_query:HyperplaneEnd.factor_iff_pre", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "3c58105bd701cfd9e2e0d039dbe84353718326faaf6f52d7f1869dd2e5c93364" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.factor_iff_pre", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "f2cb53bd7edfb4e83bd8e1bdfc4a59795d16bdf839119af16e2776859f944a66" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "957c92d21ecf6056ded25f8ef16d518add956b6c377f19955ea9229b04e2691e" + } + }, + { + "case": "omit_query:HyperplaneEnd.tail_labels", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "20ad17dcc97d763985a0f96c115064c236069fb1c7d745b37e84bee66472865a" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.tail_labels", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "14731e2334f338511af56da851baf0fcb1b5ca25148b4ea5a32a806b35191e38" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "4de69d5a975d3d3400fc9bfd5c45f76eec8d850a24c0bf82101f1edff291d607" + } + }, + { + "case": "omit_query:HyperplaneEnd.hpe_labels", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "d9a7d7ce1684eb8a588d79f28e68cb56a6b7534fe16d6a75d74408b000f2891b" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.hpe_labels", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "9520974968734df85b44f18a77c586146711c285d065121eef11df4a10bebd73" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "266551c7f0323818dc66beb5a60eb30ad6f5ff82d354ca982c4ab73cb79163e6" + } + }, + { + "case": "omit_query:HyperplaneEnd.residual_block", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "de0a36c985060da781f20ab3da5f04879cd5720df52f518ed89291350fd87733" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.residual_block", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "6a74b1faae4bd7a4ff070c5f978a5999d16d56b0e296aaf6c179b99654c266c9" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "df055092f96821997f8db95dacb79ebd8be08867297b787964876b10cc8bcf13" + } + }, + { + "case": "omit_query:HyperplaneEnd.hpe_block", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "738cbd560bbd12620f293611595b98e04bf6ebeea7b2375e6d7faf4500964398" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.hpe_block", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "a8626605710a8431327ff8d2bb75729ff26f5c46397d603f847041d64592ccf9" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "af174ab1a01ebfba3a7450c9a5e8b51bdfc3651d47197e2ef0ce8f41c94e8ec4" + } + }, + { + "case": "omit_query:HyperplaneEnd.hpe_family", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "eccc103f6eb61d981348a5543121cc76dcb582655ded918309197db7bd2c81a2" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.hpe_family", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "53f8e57013bdeb681dbd3ea2f0e0f15c2ce0b493a8a731859d904c1a5af7f3b3" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "a5324d44eb3bf91aacff08ce7f8d74e04ade2d1f71ac701fc6475fef83092c15" + } + }, + { + "case": "omit_query:HyperplaneEnd.hpe_streams", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "9d65146beba3c47691fbce66b3128d74466272b44306b575b6703447e9822174" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.hpe_streams", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "03fade89b8d9d061694a12ea0bf1cf79e749c6a013053447094c1d9aadc4c9b7" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "bc51b3a496ceb04ef6b81c0bb4b0b6c941dd124042ad50acd9fffa220bdce9f1" + } + }, + { + "case": "omit_query:HyperplaneEnd.hpe_word", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "f5b67180f4fe522e1122ce3719f484716b8604fc07e8dac8400ecb17ee786297" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.hpe_word", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "dac262769303e119e06474cbf2dad1618fb9635709ab63f346fef0ef33760f9b" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "2c4e51df83e7403b87101123631f1c38ad77d32146b88f1a7919af73e60c26f7" + } + }, + { + "case": "omit_query:HyperplaneEnd.hyperplane_width", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "b003663247b29a3bef2aa1eb4a6fbe642f813a2835836632f968df1227f0d129" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.hyperplane_width", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "6e1068025dced810deb16d15c91773916ee09bee28b22e111670fb9b819a09ce" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "797f730d9f1108a02a668950897d56d9dc89788bd941f68cc1961478e051a7ed" + } + }, + { + "case": "omit_query:HyperplaneEnd.Clifford.par9_spec", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "7c1bf6794a66db2777e635700a839b1f9250a30e6e2ef50df12a2c256f62ee57" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Clifford.par9_spec", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "9e97060aa312f17ed7cc380160ac2659af6f9abebec0529e096950f54fdceb81" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "bd9f894578b40291da68dec12b15c892cbd7f6518b9a5ed73b6a9e99dec27684" + } + }, + { + "case": "omit_query:HyperplaneEnd.Clifford.cE", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "ec4ed58ecb0813deed2a202e8da744e6556aa4d185f1d11dcf8a109b04011022" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Clifford.cE", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "0edee6c7c4051c750f9a3e7d2104589afd6a51868be1c18cc3de434248f2812f" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "dcdecb65db93e0ed36573e29ec7be74f61946aec1733469ad35d68337d107502" + } + }, + { + "case": "omit_query:HyperplaneEnd.Clifford.cL_emb", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "3483fc830fa0427e335cf416a4cdcd680ca9d72439260caceca4d6b0a430267f" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Clifford.cL_emb", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "94a3d1026f0c9c8d0c34b301c4919967433d46f7e4d84f654534c0ced4322455" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "335ed258dc81a37dea86328fc24435f2869d736936ebea4e6ca6824259957674" + } + }, + { + "case": "omit_query:HyperplaneEnd.Clifford.cL_eq_of_check", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "fb368c2b14e27550db30555d4ce0c379521a7707fb564e44d849663f961524a8" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Clifford.cL_eq_of_check", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "0389e8539dc9542b8df85bc777ef4bcf309d024055274e89b9ebaf033be92e7b" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "b4c611f649c3470ee7d1f6122a33f9dc736f096088dc7c3aac9f6c8c698b4b38" + } + }, + { + "case": "omit_query:HyperplaneEnd.Exact.rTensor_C7", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "1cf8cb4e1f0f10312ab4cd84b8f388ed075ab93f520d8c050523bb9af8db9365" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Exact.rTensor_C7", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "1fe5185f9bc8d635cab6c2de292bcda56c0ba960ce32c1c606a87c3db27cac99" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "d2954a7bedb56593cebaa6bfbfc38dcab28224a40ba02c11c3043750bce0ff86" + } + }, + { + "case": "omit_query:HyperplaneEnd.Exact.exact_N_of_check", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "36b23ae16d237b47b63a1ec280abfa7679ac3c74c1e0cc748fb1fb9e4e65d162" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Exact.exact_N_of_check", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "a48b0b7a3e1c7f5a0272a5628fa878d8dc89e1f68ae04cd21292f9a5f4daf7fd" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "71638f3053f563df848d8e52eb5a073452df64da9aae9a851cdf8284ea8e660d" + } + }, + { + "case": "omit_query:HyperplaneEnd.Exact.check1", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "3be7fc2c0e7e1866168ddf9f1aad649b16f0bc9fce396aabf2ea8ee98f82a22f" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Exact.check1", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "714bd5d2ff8a93b2e0f8a0b424dece52fda3aca192379a683bc66d11b3bd37ab" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "14ecaf6ab13c1e1bbd1ef00585bb288eb6288b410b5dfa953458f30fe349c970" + } + }, + { + "case": "omit_query:HyperplaneEnd.Exact.check2", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "f90d7bb736a17a2094a1cba108884297e518e8c5a3239422041e2a0a35f30b26" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Exact.check2", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "d951d10e6ef6eb999f3206ab6e14044d1ee5ef6875801596391b90c1261c8462" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "1ca13f6697e34b84fd0f398c62def38c188f1d69458c2882d055bd4fff5a7044" + } + }, + { + "case": "omit_query:HyperplaneEnd.Exact.check3", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "5b9c7e685fcd40b7852b304f678921dfdcdac7cbdbc5e19cc97f7b54c419b598" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Exact.check3", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "d0fcb402818f1fb3c46cfbd965aaf452f8d2469f6a42697883842604d7be3d2f" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "b28ccd79f45131dafed159f2d0b8768a0589fa76cd3274f83018c4b6b5ef2a77" + } + }, + { + "case": "omit_query:HyperplaneEnd.Exact.exact_N_pair1", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "76902e5723914e967a8566dfbc3cfe6bca201884ac0039adf42b90090aca2a4d" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Exact.exact_N_pair1", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "fe22d981a6dd1dafe71bf541d6ed1111a72f8df4a6aef8478edcb8a2bc9660b9" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "b667507e79e421acbac69598b3cf8c5839900286a43aaed95df9ec9b3e2bf7a2" + } + }, + { + "case": "omit_query:HyperplaneEnd.Exact.exact_N_pair2", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "8a05f136fba90e6a58aa5e2dc5dbb7e905e498967a8ec06571da64b0cb5a6e9f" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Exact.exact_N_pair2", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "00125090eaa65329f77ff99818abe69e1c980e3b29e4eea8110a5d10532b1489" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "57400a5daf4ae70ce6244d2e7ada4edeeaf88b0964b3906d16413f0c59a775aa" + } + }, + { + "case": "omit_query:HyperplaneEnd.Exact.exact_N_pair3", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "91edbe0cae5fdae11decb270e46053029fc5dffe3b7ec66348f151073e7904e7" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Exact.exact_N_pair3", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "9c1afb2e020713da19602d6e86022766293d3e3ea4e1545a67fb4379711f0f28" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "3cbd1689cc9141a1dcd95cb77c8777e3f03387b94f84cae2cfc351d47d852321" + } + }, + { + "case": "omit_query:HyperplaneEnd.Exact.exact_N", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "6fd949805d180579d4f5d9d7fdb357fb3843832149f8f763eb50c375d45d2243" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Exact.exact_N", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "844bbee84862d4f59cf5c151d940bbb70235a89644972b0e555f8d78f423f818" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "12bc879f7710c83edb4c84b8ddc948f4542a67e4a3d108a0d01ef9b71d4bb4c5" + } + }, + { + "case": "omit_query:HyperplaneEnd.Exact.exact_N_nine", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "505375cf873ee39d8da2fdb739bd2f48c63465b6aff99b52a83792020c6e831a" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Exact.exact_N_nine", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "c7159a1d718bc123595172bf5977348f01e39fe72e04f43c996b121b8f8fe53c" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "20fbadac4a5b60e901c8ad229aaea6d718bc1d7ce4a3c5d8fd44cb8f20524c3a" + } + }, + { + "case": "omit_query:HyperplaneEnd.Exact.hpe_word_exact", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "3d38e9e13ec87d16de21e0a96253cf89fb264dcf72d6076c6eba2edc05d09e8d" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.Exact.hpe_word_exact", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "8b0e107da6ce958fa69648ba8de771e416c796cadbe42a50877bcd31d4feb092" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "e461fd5893094dfa58bca7d0b3afeaf847bc52929ab56c94096d897a39d7e0cd" + } + }, + { + "case": "omit_query:HyperplaneEnd.labRun_climb", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "399f6148d65508ffefa04e0765c502d813926fc378c2eb4dcb3d670e5bec286b" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.labRun_climb", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "c70f8f5a853018996a29ca45a0ca85a5788dd646113b927ef85ef1fe9cc0ba32" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "a4fdbbae8754c8ac4864a577509030b7e0f5085178e19aae28a1080f1917621d" + } + }, + { + "case": "omit_query:HyperplaneEnd.wellLabelled_climb", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "53ccbdd6a98a4fda1ad2c0195abc9aad5e68e27b50165a361601742b9dcd1c46" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.wellLabelled_climb", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "341e37e44a70cb33f6da1838e00b58b839b6edc8d69798b1cdaa1aea91e1f2a4" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "53c0671fd5ce56b3e82fdd71fdd107cd8924178df2d13e54be2577bf3d4407c9" + } + }, + { + "case": "omit_query:HyperplaneEnd.labRun_block", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "8dd1d75531cc7ba4b439850d63e9a1108a7388d4d681a892465e4e3b69b53a3f" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.labRun_block", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "e2eb929fd5d3ee868d7af9cafdf8ae9e52598230157f4f46f650c9626de7ff17" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "e0da61c7824cec1624ab5e8d8a05d73bb834298c6b2bccc13a8f22aecdf48819" + } + }, + { + "case": "omit_query:HyperplaneEnd.wellLabelled_block", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "2dbf4c7a7160a0d06861a9abf02fff16e576dbd176276e030484d55ed0a3a826" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.wellLabelled_block", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "04312ec27a39bfb0fbd6f3868bc32c4cff2af7edd5430dee49d6e159367403f4" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "b4498572de7583032f881efedad9bcd4258f6fea1fbb3e5817374b2f73126d66" + } + }, + { + "case": "omit_query:HyperplaneEnd.mtail_wellLabelled", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "e389fe76f6f3f07fb1ab3144dd7240d45e16f0b9502bb7dad66a929cd0d6d5d1" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.mtail_wellLabelled", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "bb81b23144e9efe6defdb998d06e728ed83e308410088910f523d030e50bcf65" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "196094691d995a4a40b6c4cb77aa8a309b44812dd773dfd127623168d51eab06" + } + }, + { + "case": "omit_query:HyperplaneEnd.labRun_mtail", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "57d49dfa188a0c520759e36d95fbf1650af458b80f7bf49419f713f6b37fc732" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.labRun_mtail", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "0cf779b64deacd4b895ecbba472d3d43d5a584add0ae360495f56d519afd4838" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "961019d492940f65edafd5d15e3e25ea794ae0364484d53aeb71f8da29e9cb14" + } + }, + { + "case": "omit_query:HyperplaneEnd.labRun_mtail_last", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "ae0f04a3bfdee30b24a919894a512f0fcffb6bbf4d7b7037ee3271542a1b932d" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.labRun_mtail_last", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "2af10a272dbdc010e3554cdbaa231751df561748b247f7afb62dce38dff70ece" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "e30ba9db3439a44c453e1bab716ddf23d3f6cfb9d50fba58a8a0bf528627c347" + } + }, + { + "case": "omit_query:HyperplaneEnd.posts_spec", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "b895e414539de50a3e16e609d3cdd4c266d44e6dae86d836978918e9e1b90ae8" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.posts_spec", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "cd19deb268bc6c1edf578a93b1126a23f301d649a75e5c67332bd8810166e062" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "0057c62fa72c5a1e5cc3882c83744499c1ff66029963b091690d983c03d995c4" + } + }, + { + "case": "omit_query:HyperplaneEnd.hpe_labels_multi", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "48141ebcefd7b71ac557743b226b6dc953c7d1231d51994f1f5c81187f66b3f8" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.hpe_labels_multi", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "c728bc58585877511690f6822b44672bdb312dd83cd102a03de7d91142fb75a9" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "6f9b50a17191e2c59810607c21c159cd75b37ac73dc0db9a420f1827ea4c385b" + } + }, + { + "case": "omit_query:HyperplaneEnd.tail_eq_mtail", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "a1228be0d0a614d0b7149f2f1e8329210f19853675998164dd832df7f5156816" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.tail_eq_mtail", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "296d56373768db43f196c2a8de04a6285e45521161835df65bf5993d73308d37" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "ae5076b132b1a563ffa42d1fad9161c6bf9fa70238e1fad0a976820321913535" + } + }, + { + "case": "omit_query:HyperplaneEnd.hpe_labels_tail", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "7da4f7c07c23d8995131ca44359f390a99996bcfe5f7d95806d49fa84c90a1ed" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.hpe_labels_tail", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "e0db8149c03ea2ea68ed962e78e97d2c377cecef979e21fa765a5589d93fe12a" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "74d94e705b2476fc0fe2d8d0ca29b7e234e0ce47413e0a28a1a5fc78fb2bff0d" + } + }, + { + "case": "omit_query:HyperplaneEnd.hpe_word_multi", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "5567bbdde345d80e5b18cf8b4a7efbe518ca73976756d11bed92cd2b1f8a24a9" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.hpe_word_multi", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "01b75d9ccdb4e92e8bdf26abd94d010c7a6ef528e6930e73773c9cecd2a8c1ca" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "5a4e876bc1116dfd7f311df1790a9ebb571effa80e2608096057188dec8d65bc" + } + }, + { + "case": "omit_query:HyperplaneEnd.exact_cold", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "e34a1fbb12fa4d3bb83a53bea5288e3e7c78b545bd75c313d975baed57f84d54" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.exact_cold", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "a16810837ff165c9e7b38515c7f40312b2be99c38c7864e6fa1644740728618c" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "bd376c400eb768ea721f56add51240298f73c5e39c9951ce1cf77b34065bfbd0" + } + }, + { + "case": "omit_query:HyperplaneEnd.cold_hyperplane_width", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "dba5dd86766b041e9d35dab6b494550d906c5d6c78b63d28d05311ad0959a654" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "omit_report:HyperplaneEnd.cold_hyperplane_width", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "ce87118535577b2ffd3984c0932a9e3ca1adf824251e625021d578417d12d018" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "b6524a0bec38cb881d8f9263af0bc81baa5d59ed0de19a9364f1bc696831fc84" + } + }, + { + "case": "indented_complete_inventory", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 0, + "subprocess_calls": 2, + "stdout_sha256": "950e962a5f3546ce977371a1503fa3c13a498ae0ba8cbc6bf6696a7e7e26236f" + }, + "repaired": { + "accepted": true, + "exit_code": 0, + "reported_results": 42, + "subprocess_calls": 2, + "stdout_sha256": "18363cc2019fca46131206eed5eb0aac2499c8ea949da2fbf5f7a0b44749f7a6" + } + }, + { + "case": "indented_forbidden_dependency", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 0, + "subprocess_calls": 2, + "stdout_sha256": "0fa427d83acaec61bd78928c4b58f5a946f152b42c609cea8ba3feebd41f821f" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "53f4f12a803f95a5e377fde4e6da0cf46c5e75a7fcb6358257a14a21538a1812" + } + }, + { + "case": "ordinary_forbidden_dependency", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "53f4f12a803f95a5e377fde4e6da0cf46c5e75a7fcb6358257a14a21538a1812" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "53f4f12a803f95a5e377fde4e6da0cf46c5e75a7fcb6358257a14a21538a1812" + } + }, + { + "case": "substitute_unrelated_theorem", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 42, + "subprocess_calls": 2, + "stdout_sha256": "0eb5addd12c70287e17735938248a21bf4b57a2c7a28a3a75ee94d20b207218e" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "duplicate_query", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 43, + "subprocess_calls": 2, + "stdout_sha256": "88a706e564adf205de2c8f16eb16e54d9989f7f3153a9895f2775acf12f37595" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "comment_out_one_query", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 41, + "subprocess_calls": 2, + "stdout_sha256": "3b3f79c76fcc4b855119b52b1930d94c4be468c8fa613b8662862a2e98fff6f3" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 0, + "stdout_sha256": "e91dfb442d93ca7ca1186182a051cacc9ca77ff75a3a83fda3687875dd59af2d" + } + }, + { + "case": "unexpected_report", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 42, + "subprocess_calls": 2, + "stdout_sha256": "30d3a0b6f89a7f46724f84be91ab302e0b47ea7dbb7148ab11d936eb8c8ebe3d" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "17edce60ce3c3ad4a232df0fa86a930b3602a4ccfa8a771a88caa9058833dbc6" + } + }, + { + "case": "duplicate_report", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 42, + "subprocess_calls": 2, + "stdout_sha256": "6c7a283593577decc5a2a353d5d1e13bd3700c32d5d11822c35336a3915fd8da" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "9bb294d0f83078e131320eda575c8f7fcfe70f896d7ebe521a815073694ca059" + } + }, + { + "case": "conflicting_duplicate_report", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 42, + "subprocess_calls": 2, + "stdout_sha256": "87ea5c978811d55350fa0ae35aa8fa78db8f9eb1610f852dd7b6114f9f110a40" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "d0fba5efe25fa08e440dd6406b1fd29ae250ac5ccfed4a95b626517049a8aa3c" + } + }, + { + "case": "conflicting_duplicate_report_reversed", + "original": { + "accepted": true, + "exit_code": 0, + "reported_results": 42, + "subprocess_calls": 2, + "stdout_sha256": "433c0a36e13384c259f4dec797d6c5ab78412d6cc1bb512a5da80798cd36bd74" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "9b0f8673d640f2657feebb6b1c2ec454e239acd5ce350d438484c16300c7fbc2" + } + }, + { + "case": "malformed_report", + "original": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "e9f7a524e2654b809b41fcde0d5d5cac3c5899289003db98edac6f7e22e07cb6" + }, + "repaired": { + "accepted": false, + "exit_code": 1, + "reported_results": null, + "subprocess_calls": 2, + "stdout_sha256": "1722e670ec756dec629a386f2b5e3a6d4c17a1fcab62fac34ae045b7cbb35eb8" + } + } + ] +} diff --git a/research/hpe-axiom-inventory-audit/SOURCES.json b/research/hpe-axiom-inventory-audit/SOURCES.json new file mode 100644 index 0000000000..681c6d9326 --- /dev/null +++ b/research/hpe-axiom-inventory-audit/SOURCES.json @@ -0,0 +1,144 @@ +{ + "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/e8-lemma-a-lean/LemmaA.lean", + "usage": "input", + "git_blob": "2cc601bdb5fdebc9a466ff028d4187365b50266a", + "sha256": "dcb29f406b352c608a89837ec95071ac01e9bcbe4671e01927c416e754e4c53d" + }, + { + "path": "research/e8-lemma-a-lean/LemmaA/Realize.lean", + "usage": "input", + "git_blob": "8917c5b7f7d86352fd0b505141a9047a4a676279", + "sha256": "3aa9afd36035afd94296ef410c647d5a8c6fb282f64062542c7070bb1d99a14f" + }, + { + "path": "research/e8-lemma-a-lean/LemmaA/Schedule.lean", + "usage": "input", + "git_blob": "0bdd775a0ffc2243295fb95c4db3dbd0c5f455d8", + "sha256": "2b1c8a1a0370e47bc0c4b353a03605b9ad7e385ba30b4ac3bec7ecf76f656a5f" + }, + { + "path": "research/e8-lemma-a-lean/LemmaA/Streams.lean", + "usage": "input", + "git_blob": "d3ad32fc95dec79006005b412b84d45051ecd92e", + "sha256": "345b264eae4ed037e632461fd7a55dd27c6b21e828167e3b441482d063cf547e" + }, + { + "path": "research/e8-lemma-a-lean/LemmaA/Tensor.lean", + "usage": "input", + "git_blob": "cd33a52ab5d137ffae5ece2e8762bd46610de776", + "sha256": "dcaba494eee73b8066d65326d9a8c3aea260f3b736eb1c5fbf7dfb7fe0c66baf" + }, + { + "path": "research/e8-lemma-g-lean/LemmaG.lean", + "usage": "input", + "git_blob": "ce3c72d19be21852f437674c995ba25363b60623", + "sha256": "ac5ab476d9c8e29de95b92844bdb3d9a59f108dfffb89c31ea65e413d0f4c09b" + }, + { + "path": "research/e8-lemma-g-lean/LemmaG/BitEntrance.lean", + "usage": "input", + "git_blob": "edff353bc4a2303aeddd28022ab3f6a442d6866b", + "sha256": "49872d04ec0cb0035a741075e3d593563a55ba8b5642cd225a8d06c166e890c8" + }, + { + "path": "research/e8-lemma-g-lean/LemmaG/Frames.lean", + "usage": "input", + "git_blob": "33db0a3236654a7ca294ba8b875856cc3e836ce1", + "sha256": "64e9bf83af211fd75ac2c7877b98604b11e2ba90b8e918435b92d0dcea0ccef7" + }, + { + "path": "research/e8-lemma-g-lean/LemmaG/Schedule.lean", + "usage": "input", + "git_blob": "d765e1ed741aaaaa5c1136c18961a8846f369083", + "sha256": "df2c5feb64185810038b5095abc41c5455de3499b584acfea53c607233703ebb" + }, + { + "path": "research/e8-lemma-g-lean/LemmaG/Stream.lean", + "usage": "input", + "git_blob": "e89897190307a6f3fcfb858f8de00cc5a7f49b3e", + "sha256": "7138f4b859d0574a803e99401f05ef5e0ec9eeac0eb480775cd9b86595c365f8" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd.lean", + "usage": "input", + "git_blob": "548c64f6083616e8a639bc54c0c171d40ebf177a", + "sha256": "60a7c1cb8f86b4c30fd4a94839801696cb673cf1e57ac3ed66c70da181b7bad5" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Clifford.lean", + "usage": "input", + "git_blob": "5970d81439b8bca2935a935d964779845a45057c", + "sha256": "c0c51407b4fa6ff230a79d5f3b07c83b7d1c4b433ce03513f0c4fb725bf3cbe1" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean", + "usage": "input", + "git_blob": "1af33a206a9ba6c4826b3a1516d104e770380869", + "sha256": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Labels.lean", + "usage": "input", + "git_blob": "8315bdda8db4993ef713b24a01ce0e7c1837dff1", + "sha256": "febdc3f1734281178b043d714ab70b197d1c34d58ad15462386060b821b80e0c" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Main.lean", + "usage": "input", + "git_blob": "88fcee53762abdd2a17c9cc3a26fef74945f0171", + "sha256": "221a5126ec46141e5cba7689aaddd38746183ed15fa91ec229e32a16302b42a6" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Multi.lean", + "usage": "input", + "git_blob": "7b92352426ce2b8ac71210be5e2ee0870e83cc06", + "sha256": "7e2fe000c44cf78ec4005b31db442dea266fc73e04d3fa8f941bdbcb5b367f66" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Tail.lean", + "usage": "input", + "git_blob": "11a43b6504705c5173552e8ffc617fce98b78064", + "sha256": "26846d2627cbf19f1b5378f50ef489e929dbc4d5214d6a911ff7457fbbe0b094" + }, + { + "path": "research/hyperplane-end-lean/NOTICE.md", + "usage": "input", + "git_blob": "2afcca845b1a40a5cc36450e825688c75791b5e4", + "sha256": "2ed2c5763f8dcb204351d3f9dd67bd6e04fa04b516b105f3c9e6ccceef4d344b" + }, + { + "path": "research/hyperplane-end-lean/PROOF.md", + "usage": "input", + "git_blob": "a94a2ac168c088a1282ea411766bc859178620df", + "sha256": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9" + }, + { + "path": "research/hyperplane-end-lean/PrintAxioms.lean", + "usage": "input", + "git_blob": "cc1a57e87c2775cade83e8ff8cc77ad56dbfaab4", + "sha256": "4d989c6af78020485f81f68ea9c067c4525a6844bc1a474686c1f134e1fd4b86" + }, + { + "path": "research/hyperplane-end-lean/verify.py", + "usage": "input", + "git_blob": "4323aaa9faed16d40821957bd190a60fe8011feb", + "sha256": "2b94b629b2c5d091b1a3ff06ce0fbee1cf178521ccb6ac97843c5c456dfd5eb8" + } + ] +} diff --git a/research/hpe-axiom-inventory-audit/TASK.json b/research/hpe-axiom-inventory-audit/TASK.json new file mode 100644 index 0000000000..fdb97dac5e --- /dev/null +++ b/research/hpe-axiom-inventory-audit/TASK.json @@ -0,0 +1,172 @@ +{ + "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": "changed", + "actual_scope": "Audit and repair the coverage of the 42 named HPE axiom probes in the retained Python driver; no new Lean theorem.", + "scope_change_reason": "The direct semantic HPE binding and PR540 source-binding handoffs are already covered by PR1415 and PR1273/1228/1231. This studies the verification driver coverage prerequisite instead.", + "bottleneck_link": "Side result: prevent successful verification output when named axiom obligations were silently omitted. It does not improve the multiplication exponent.", + "budget_minutes": 60, + "stop_rule": "One driver and 42 probes; stop if no reproducible false success or if a repair changes proof statements; reserve final time for controls and handoff.", + "outcome": "completed", + "evidence": "RESULT.json: 100 original/repaired driver cases with substituted subprocess results; 42 query omissions reject before build, 42 existing missing-report rejections remain. A separately executed Lean 4.21.0 three-probe syntax fixture confirms indentation and output forms. Six adversarial groups reject source/receipt/transcript mutations and four weakened repairs. No HPE build.", + "author": "Hanson Sun (@bbMisk), with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in investigation, implementation, verification and writing. No subagents or independent human review.", + "open_questions": [ + { + "question": "Can the proposed inventory repair be adopted while preserving a full pinned HPE build and its 42 actual axiom reports?", + "why_it_matters": "The bounded audit establishes driver control flow, not full Lean/Mathlib build compatibility.", + "first_step": "Apply repair.patch in an isolated successor, build the pinned Lean/Mathlib 4.21.0 environment and run the original combined HPE verifier.", + "blocked_by": "Complete dependency setup and an explicit maintainer decision about successor source pins; this package leaves frozen evidence unchanged." + } + ], + "selection": { + "seed": "3078f304ea3502df42d473cf570d1e27", + "track": "independent-verification", + "base_commit": "ebedc0895eb4c06725af020bc1af165722b0a3ce", + "priority_revision": 2, + "catalog_sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "task_id": "formal-interface-lemma", + "scope_key": "e3ffea67887eeb4c396c", + "method": "Audit a formal theorem-to-certificate binding independently." + }, + "selection_note": "An earlier chooser invocation was lost in a truncated tool response; the captured second invocation is retained here. No repeated search for a preferred track followed it.", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1593", + "protected_invariant": "A success from the repaired standalone driver requires exactly one allowed-axiom report for each of the 42 intended theorem names.", + "predecessor_heads": { + "593": "fdb6dcc6d7bc29764c5b6b4d32b7fa050acf74a4", + "599": "bc13c8a3e000442606bd2dbe8583a17649ba6c32", + "1415": "0d8d2c3a96346756f02563b401a042ab97198e20" + }, + "related_work": [ + { + "pr": 1415, + "relation": "HPE operator semantics; does not address the Python driver probe inventory." + }, + { + "pr": 893, + "relation": "Prior exact source-command and axiom-report coverage on PR236; the general pattern is credited prior work.", + "head": "5d8c2e96e0624efbadb182d9ee0a09ee65b70b48" + }, + { + "pr": 1273, + "relation": "PR540 literal source binding already covered; not repeated." + } + ], + "overlap_entry": { + "coverage": { + "open_prs": 727, + "discussion_records": 233, + "complete_pagination": true + }, + "fetched_at": "2026-10-14T03:35:05.144656+00:00", + "terms": [ + "formal-interface-lemma", + "hyperplane-end-lean", + "axiom inventory", + "probe inventory", + "empty probe", + "zero probe", + "axiom parser" + ], + "limits": "Open PR bodies and discussions plus local README/ledger; no exhaustive diff search, closed work only through retained local records. Not a novelty certificate." + }, + "prose_processing": "Emulate unavailable; the donor requested disclosure before unprocessed prose delivery. Prose checked directly against source and executed evidence.", + "submission_base": "81e81af67714bdc8d1693b0bf5c29468b92f62ff", + "main_refresh": "Started from ebedc0895eb4c06725af020bc1af165722b0a3ce; advanced to current main 81e81af67714bdc8d1693b0bf5c29468b92f62ff before submission. All 21 consumed input bytes are unchanged. Priority revision 3 was read; this already assigned verification scope remains applicable and retains its revision-2 provenance.", + "overlap_final": { + "searched_at": "2026-10-14T03:53:15.194874+00:00", + "terms": [ + "axiom inventory", + "probe inventory", + "HPE axiom", + "hyperplane-end-lean" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T03:52:46.473462+00:00", + "complete_pagination": true, + "records": 733 + }, + "discussions": { + "fetched_at": "2026-10-14T03:53:15.153918+00:00", + "complete_pagination": true, + "records": 244 + } + }, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "assessment": "Only this package and Discussion1593 match these focused terms. Prior broader searches identified PR1415 and the retained PR893 corpus audit; they are credited. Direct live checks confirm both cited heads unchanged, PR1415 open, PR893 merged, and no comments on the claim." + }, + "validation": { + "registered_replay": { + "python": "CPython 3.12.13", + "driver_cases": 100, + "adversarial_groups": 6, + "weakened_repairs_rejected": 4, + "result": "passed" + }, + "additional_interpreter": { + "python": "CPython 3.14.6", + "flags": [ + "-I", + "-B", + "-O" + ], + "result": "same committed RESULT.json" + }, + "live_syntax_fixture": { + "lean": "4.21.0", + "probes": 3, + "result": "stdout exactly matches fixtures/lean421.txt" + }, + "repository_workflow_tests": { + "command": "python3.12 -B -m unittest discover -s tests -p 'test_research_*.py'", + "tests": 20, + "result": "passed without skips" + }, + "not_run": [ + "full HPE/Mathlib build", + "selected construction cold replay", + "full multiplication theorem proof" + ] + } +} diff --git a/research/hpe-axiom-inventory-audit/VERIFY.json b/research/hpe-axiom-inventory-audit/VERIFY.json new file mode 100644 index 0000000000..b6d90dd266 --- /dev/null +++ b/research/hpe-axiom-inventory-audit/VERIFY.json @@ -0,0 +1,52 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-lemma-a-lean/LemmaA.lean", + "research/e8-lemma-a-lean/LemmaA/Realize.lean", + "research/e8-lemma-a-lean/LemmaA/Schedule.lean", + "research/e8-lemma-a-lean/LemmaA/Streams.lean", + "research/e8-lemma-a-lean/LemmaA/Tensor.lean", + "research/e8-lemma-g-lean/LemmaG.lean", + "research/e8-lemma-g-lean/LemmaG/BitEntrance.lean", + "research/e8-lemma-g-lean/LemmaG/Frames.lean", + "research/e8-lemma-g-lean/LemmaG/Schedule.lean", + "research/e8-lemma-g-lean/LemmaG/Stream.lean", + "research/hyperplane-end-lean/HyperplaneEnd.lean", + "research/hyperplane-end-lean/HyperplaneEnd/Clifford.lean", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean", + "research/hyperplane-end-lean/HyperplaneEnd/Labels.lean", + "research/hyperplane-end-lean/HyperplaneEnd/Main.lean", + "research/hyperplane-end-lean/HyperplaneEnd/Multi.lean", + "research/hyperplane-end-lean/HyperplaneEnd/Tail.lean", + "research/hyperplane-end-lean/NOTICE.md", + "research/hyperplane-end-lean/PROOF.md", + "research/hyperplane-end-lean/PrintAxioms.lean", + "research/hyperplane-end-lean/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source-bound original and repaired driver: 100 coverage cases, all 42 single omissions and all 42 missing-report controls, plus recorded real Lean syntax. No HPE build." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_audit.py", + "-v" + ], + "timeout_seconds": 120, + "checks": "Six adversarial groups: four weakened repairs, source/receipt/transcript corruption, overwrite refusal, and read-only optimized relocation." + } + ] +} diff --git a/research/hpe-axiom-inventory-audit/check_lean.py b/research/hpe-axiom-inventory-audit/check_lean.py new file mode 100644 index 0000000000..26261c6f50 --- /dev/null +++ b/research/hpe-axiom-inventory-audit/check_lean.py @@ -0,0 +1,54 @@ +#!/usr/bin/env python3 +"""Reproduce the small syntax fixture with an explicit Lean 4.21.0 binary. + +No Mathlib download or HPE build is involved. Apache-2.0; Hanson Sun with Codex. +""" +import argparse +import hashlib +import json +from pathlib import Path +import subprocess +import tempfile + +HERE = Path(__file__).resolve().parent + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--lean", required=True, type=Path) + parser.add_argument("--record", action="store_true", help="write new fixture evidence; refuse overwrite") + args = parser.parse_args() + lean = args.lean.resolve(strict=True) + version = subprocess.check_output([str(lean), "--version"], text=True, timeout=30).strip() + if not version.startswith("Lean (version 4.21.0,"): + raise ValueError("the syntax fixture requires Lean 4.21.0") + source = (HERE / "fixtures/ProbeSyntax.lean").read_bytes() + with tempfile.TemporaryDirectory(prefix="hpe-lean-syntax-") as temporary: + fixture = Path(temporary) / "ProbeSyntax.lean" + fixture.write_bytes(source) + process = subprocess.run([str(lean), str(fixture)], cwd=temporary, + text=True, capture_output=True, timeout=60, check=True) + if process.stderr: + raise ValueError("unexpected Lean stderr: " + process.stderr) + if args.record: + metadata = { + "scope": "Actual compiler output for three tiny syntax fixtures; no HPE theorem was compiled.", + "version": version, + "compiler_sha256": hashlib.sha256(lean.read_bytes()).hexdigest(), + "source_sha256": hashlib.sha256(source).hexdigest(), + "stdout_sha256": hashlib.sha256(process.stdout.encode()).hexdigest(), + "command": ["lean-4.21.0", "ProbeSyntax.lean"], + "exit_code": process.returncode, + } + with (HERE / "fixtures/lean421.txt").open("x", encoding="utf-8") as stream: + stream.write(process.stdout) + with (HERE / "fixtures/LEAN.json").open("x", encoding="utf-8") as stream: + json.dump(metadata, stream, indent=2) + stream.write("\n") + elif process.stdout != (HERE / "fixtures/lean421.txt").read_text(): + raise ValueError("Lean fixture output differs") + print("PASS_HPE_LEAN421_SYNTAX_FIXTURE probes=3 deliberately_forbidden_dependency=1 no_HPE_build") + + +if __name__ == "__main__": + main() diff --git a/research/hpe-axiom-inventory-audit/fixtures/LEAN.json b/research/hpe-axiom-inventory-audit/fixtures/LEAN.json new file mode 100644 index 0000000000..eeaf4bfcb0 --- /dev/null +++ b/research/hpe-axiom-inventory-audit/fixtures/LEAN.json @@ -0,0 +1,12 @@ +{ + "scope": "Actual compiler output for three tiny syntax fixtures; no HPE theorem was compiled.", + "version": "Lean (version 4.21.0, arm64-apple-darwin23.6.0, commit 6741444a63ee, Release)", + "compiler_sha256": "c89073b8a577a5914ead7b740d2ad996af1ad5ad5b4bfc2825e0bce2f01b6aa4", + "source_sha256": "c9fd50362a52eff474f5c52baa2a57dafc87485ac8b572758221a6a898cc5177", + "stdout_sha256": "2e741a3b87e01a0af9c7dd58cbe847a69930ae977c5fb0f14cb60a876ecddc15", + "command": [ + "lean-4.21.0", + "ProbeSyntax.lean" + ], + "exit_code": 0 +} diff --git a/research/hpe-axiom-inventory-audit/fixtures/ProbeSyntax.lean b/research/hpe-axiom-inventory-audit/fixtures/ProbeSyntax.lean new file mode 100644 index 0000000000..7657a6ad93 --- /dev/null +++ b/research/hpe-axiom-inventory-audit/fixtures/ProbeSyntax.lean @@ -0,0 +1,13 @@ +/- Syntax and negative-control fixture only. This is not an HPE theorem. + The explicit extra axiom below is deliberately forbidden by the audit. + Apache-2.0. Hanson Sun, with OpenAI Codex assistance. -/ +namespace HPEInventoryFixture +theorem clean : True := True.intro +theorem ext (p q : Prop) (h : p ↔ q) : p = q := propext h +axiom extra : False +theorem bad : False := extra +end HPEInventoryFixture + +#print axioms HPEInventoryFixture.clean +#print axioms HPEInventoryFixture.ext + #print axioms HPEInventoryFixture.bad diff --git a/research/hpe-axiom-inventory-audit/fixtures/lean421.txt b/research/hpe-axiom-inventory-audit/fixtures/lean421.txt new file mode 100644 index 0000000000..03670fae0c --- /dev/null +++ b/research/hpe-axiom-inventory-audit/fixtures/lean421.txt @@ -0,0 +1,3 @@ +'HPEInventoryFixture.clean' does not depend on any axioms +'HPEInventoryFixture.ext' depends on axioms: [propext] +'HPEInventoryFixture.bad' depends on axioms: [HPEInventoryFixture.extra] diff --git a/research/hpe-axiom-inventory-audit/repair.patch b/research/hpe-axiom-inventory-audit/repair.patch new file mode 100644 index 0000000000..7391c1c2a1 --- /dev/null +++ b/research/hpe-axiom-inventory-audit/repair.patch @@ -0,0 +1,117 @@ +--- a/research/hyperplane-end-lean/verify.py ++++ b/research/hyperplane-end-lean/verify.py +@@ -15,6 +15,52 @@ + + HERE = Path(__file__).resolve().parent + ALLOWED = {'propext', 'Classical.choice', 'Quot.sound'} ++ ++# Keep this independent of PrintAxioms.lean: omitted queries must fail closed. ++EXPECTED_RESULTS = ( ++ 'HyperplaneEnd.pre_recipe', ++ 'HyperplaneEnd.post_recipe', ++ 'HyperplaneEnd.wrapped_block', ++ 'HyperplaneEnd.factor_of_exact', ++ 'HyperplaneEnd.factor_iff_pre', ++ 'HyperplaneEnd.tail_labels', ++ 'HyperplaneEnd.hpe_labels', ++ 'HyperplaneEnd.residual_block', ++ 'HyperplaneEnd.hpe_block', ++ 'HyperplaneEnd.hpe_family', ++ 'HyperplaneEnd.hpe_streams', ++ 'HyperplaneEnd.hpe_word', ++ 'HyperplaneEnd.hyperplane_width', ++ 'HyperplaneEnd.Clifford.par9_spec', ++ 'HyperplaneEnd.Clifford.cE', ++ 'HyperplaneEnd.Clifford.cL_emb', ++ 'HyperplaneEnd.Clifford.cL_eq_of_check', ++ 'HyperplaneEnd.Exact.rTensor_C7', ++ 'HyperplaneEnd.Exact.exact_N_of_check', ++ 'HyperplaneEnd.Exact.check1', ++ 'HyperplaneEnd.Exact.check2', ++ 'HyperplaneEnd.Exact.check3', ++ 'HyperplaneEnd.Exact.exact_N_pair1', ++ 'HyperplaneEnd.Exact.exact_N_pair2', ++ 'HyperplaneEnd.Exact.exact_N_pair3', ++ 'HyperplaneEnd.Exact.exact_N', ++ 'HyperplaneEnd.Exact.exact_N_nine', ++ 'HyperplaneEnd.Exact.hpe_word_exact', ++ 'HyperplaneEnd.labRun_climb', ++ 'HyperplaneEnd.wellLabelled_climb', ++ 'HyperplaneEnd.labRun_block', ++ 'HyperplaneEnd.wellLabelled_block', ++ 'HyperplaneEnd.mtail_wellLabelled', ++ 'HyperplaneEnd.labRun_mtail', ++ 'HyperplaneEnd.labRun_mtail_last', ++ 'HyperplaneEnd.posts_spec', ++ 'HyperplaneEnd.hpe_labels_multi', ++ 'HyperplaneEnd.tail_eq_mtail', ++ 'HyperplaneEnd.hpe_labels_tail', ++ 'HyperplaneEnd.hpe_word_multi', ++ 'HyperplaneEnd.exact_cold', ++ 'HyperplaneEnd.cold_hyperplane_width', ++) + FORBIDDEN = re.compile(r'\b(sorry|admit|axiom|native_decide|implemented_by|extern|unsafe|opaque)\b|set_option\s+(?!maxHeartbeats|maxRecDepth)') + + +@@ -35,6 +81,34 @@ + return re.sub(r'--[^\n]*', ' ', src) + + ++def probe_inventory(source): ++ wanted = re.findall( ++ r"(?m)^[ \t]*#print[ \t]+axioms[ \t]+([\w.']+)[ \t]*$", ++ strip_comments(source), ++ ) ++ if len(wanted) != len(EXPECTED_RESULTS) or set(wanted) != set(EXPECTED_RESULTS): ++ fail('axiom probe inventory differs from the 42 required results') ++ return wanted ++ ++ ++def check_axiom_reports(output, wanted): ++ seen = {} ++ pattern = r"'([\w.']+)' (?:depends on axioms: \[([^\]]*)\]|does not depend on any axioms)" ++ for match in re.finditer(pattern, output): ++ name = match.group(1) ++ if name in seen: ++ fail(f'duplicate axiom report for {name}') ++ seen[name] = [] if match.group(2) is None else [ ++ a.strip() for a in match.group(2).split(',') if a.strip() ++ ] ++ if set(seen) != set(wanted): ++ fail('axiom reports differ from the required result inventory') ++ for name in wanted: ++ extra = set(seen[name]) - ALLOWED ++ if extra: ++ fail(f'{name} uses {sorted(extra)}') ++ ++ + def main(): + args = sys.argv[1:] + A, G = HERE.parent / 'e8-lemma-a-lean', HERE.parent / 'e8-lemma-g-lean' +@@ -45,23 +119,16 @@ + if m: fail(f'forbidden token {m.group(0)!r} in {p.name}') + print('sources: no sorry / admit / axiom / native_decide / unsafe / opaque / extern in %d files' % len(lean_files), flush=True) + ++ wanted = probe_inventory((HERE / 'PrintAxioms.lean').read_text(encoding='utf-8')) ++ + if '--no-cache' not in args: + run(['lake', 'exe', 'cache', 'get'], 3600) + out = run(['lake', 'build'], 3600) + print('\n'.join(l for l in out.splitlines() if 'warning' in l or 'error' in l or 'Build completed' in l), flush=True) + + out = run(['lake', 'env', 'lean', 'PrintAxioms.lean'], 1200) +- wanted = [l.split()[2] for l in (HERE / 'PrintAxioms.lean').read_text().splitlines() if l.startswith('#print axioms')] +- seen = {} +- for m in re.finditer(r"'([\w.']+)' depends on axioms: \[([^\]]*)\]", out): +- seen[m.group(1)] = [a.strip() for a in m.group(2).split(',') if a.strip()] +- for m in re.finditer(r"'([\w.']+)' does not depend on any axioms", out): +- seen[m.group(1)] = [] + print(out.strip(), flush=True) +- for name in wanted: +- if name not in seen: fail(f'no axiom report for {name}') +- extra = set(seen[name]) - ALLOWED +- if extra: fail(f'{name} uses {sorted(extra)}') ++ check_axiom_reports(out, wanted) + print(f'axioms: {len(wanted)} results, all within {sorted(ALLOWED)}') + if '--instances' in args: + for run_dir in args[args.index('--instances') + 1:]: diff --git a/research/hpe-axiom-inventory-audit/test_audit.py b/research/hpe-axiom-inventory-audit/test_audit.py new file mode 100644 index 0000000000..d925137fc5 --- /dev/null +++ b/research/hpe-axiom-inventory-audit/test_audit.py @@ -0,0 +1,119 @@ +"""Adversarial checks of the audit, its proposed repair and its evidence boundary.""" +import contextlib +import difflib +import importlib.util +import json +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("hpe_inventory_audit", HERE / "verify.py") +audit = importlib.util.module_from_spec(spec) +spec.loader.exec_module(audit) + + +@contextlib.contextmanager +def isolated(): + with tempfile.TemporaryDirectory(prefix="hpe-audit-control-") as temporary: + root = Path(temporary).resolve() + package = root / "research" / HERE.name + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__", "*.pyc")) + for name, data in audit.pinned_inputs().items(): + path = root / name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(data) + previous = audit.HERE, audit.ROOT + audit.HERE, audit.ROOT = package, root + try: + yield root, package + finally: + audit.HERE, audit.ROOT = previous + + +class AuditControls(unittest.TestCase): + def test_source_mutation_rejected(self): + with isolated() as (root, _): + path = root / audit.TARGET + path.write_bytes(path.read_bytes() + b"\n") + with self.assertRaisesRegex(ValueError, "source drift"): + audit.audit() + + def test_lean_transcript_mutation_rejected(self): + with isolated() as (_, package): + path = package / "fixtures/lean421.txt" + path.write_text(path.read_text().replace("HPEInventoryFixture.extra", "propext")) + with self.assertRaisesRegex(ValueError, "Lean transcript drift"): + audit.audit() + + def test_materially_weakened_repairs_detected(self): + original = (audit.ROOT / audit.TARGET).read_text() + # Apply the submitted patch once; every mutant starts from that source. + with isolated() as (root, package): + subprocess.run(["git", "apply", str(package / "repair.patch")], + cwd=root, capture_output=True, check=True, timeout=30) + fixed = (root / audit.TARGET).read_text() + mutations = { + "no_query_inventory": ( + "if len(wanted) != len(EXPECTED_RESULTS) or set(wanted) != set(EXPECTED_RESULTS):", + "if False:"), + "duplicate_reports_overwrite": ("if name in seen:", "if False:"), + "extra_reports_ignored": ("if set(seen) != set(wanted):", + "if set(wanted) - set(seen):"), + "forbidden_axioms_accepted": (" if extra:\n", " if False:\n"), + } + for label, (before, after) in mutations.items(): + with self.subTest(mutation=label), isolated() as (_, package): + self.assertEqual(fixed.count(before), 1) + mutant = fixed.replace(before, after) + patch = "".join(difflib.unified_diff(original.splitlines(True), mutant.splitlines(True), + fromfile="a/" + audit.TARGET, tofile="b/" + audit.TARGET)) + (package / "repair.patch").write_text(patch) + with self.assertRaisesRegex(ValueError, "repair behavior differs"): + audit.audit() + + def test_receipt_mutation_rejected(self): + with isolated() as (_, package): + path = package / "RESULT.json" + receipt = json.loads(path.read_text()) + receipt["omitted_queries_rejected_before_build"] = 0 + path.write_text(json.dumps(receipt)) + process = subprocess.run([sys.executable, "-I", "-B", str(package / "verify.py")], + capture_output=True, text=True, timeout=120) + self.assertNotEqual(process.returncode, 0) + self.assertIn("committed receipt differs", process.stderr) + + def test_receipt_overwrite_refused(self): + with isolated() as (_, package): + path = package / "RESULT.json" + before = path.read_bytes() + process = subprocess.run([sys.executable, "-I", "-B", str(package / "verify.py"), + "--write-receipt", str(path)], + capture_output=True, text=True, timeout=120) + self.assertNotEqual(process.returncode, 0) + self.assertIn("FileExistsError", process.stderr) + self.assertEqual(before, path.read_bytes()) + + def test_read_only_optimized_relocation(self): + with isolated() as (root, package): + files = [path for path in root.rglob("*") if path.is_file()] + before = {path.relative_to(root): path.read_bytes() for path in files} + for path in files: + path.chmod(0o444) + try: + process = subprocess.run([sys.executable, "-I", "-B", "-O", str(package / "verify.py")], + cwd=root, capture_output=True, text=True, timeout=120) + self.assertEqual(process.returncode, 0, process.stderr) + self.assertIn("driver_cases=100", process.stdout) + self.assertEqual(before, {path.relative_to(root): path.read_bytes() for path in files}) + self.assertEqual(set(before), {p.relative_to(root) for p in root.rglob("*") if p.is_file()}) + finally: + for path in files: + path.chmod(0o644) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/hpe-axiom-inventory-audit/verify.py b/research/hpe-axiom-inventory-audit/verify.py new file mode 100644 index 0000000000..eb6bfb1777 --- /dev/null +++ b/research/hpe-axiom-inventory-audit/verify.py @@ -0,0 +1,238 @@ +#!/usr/bin/env python3 +"""Reproduce HPE axiom-coverage failures and check a proposed repair. + +Apache-2.0. Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. +The driver experiments substitute subprocess results. They do not build Lean. +""" +import argparse +import contextlib +import hashlib +import io +import json +from pathlib import Path +import re +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +TARGET = "research/hyperplane-end-lean/verify.py" +PROBES = "research/hyperplane-end-lean/PrintAxioms.lean" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def pinned_inputs(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + files = {} + for item in manifest["files"]: + if item["usage"] != "input": + continue + name = item["path"] + path = (ROOT / name).resolve() + require(path.is_relative_to(ROOT), "input outside repository") + data = path.read_bytes() + require(sha(data) == item["sha256"], "source drift: " + name) + blob = sha_git_blob(data) + require(blob == item["git_blob"], "Git blob drift: " + name) + files[name] = data + require(TARGET in files and PROBES in files, "missing audited inputs") + return files + + +def sha_git_blob(data): + return hashlib.sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + + +def run_driver(implementation, directory, queries, transcript): + """Execute the real main(), stubbing only its expensive run() boundary.""" + (directory / PROBES).write_text(queries, encoding="utf-8") + namespace = {"__name__": "audited_hpe_driver", "__file__": str(directory / TARGET)} + exec(compile(implementation, str(directory / TARGET), "exec"), namespace) + calls = [] + + def captured_run(command, timeout): + calls.append(command) + if command == ["lake", "build"]: + require(timeout == 3600, "unexpected build timeout") + return "Build completed successfully.\n" + require(command == ["lake", "env", "lean", "PrintAxioms.lean"], + "unexpected subprocess: " + repr(command)) + require(timeout == 1200, "unexpected probe timeout") + return transcript + + namespace["run"] = captured_run + previous = sys.argv + sys.argv = ["verify.py", "--no-cache"] + output = io.StringIO() + code = 0 + try: + with contextlib.redirect_stdout(output): + try: + namespace["main"]() + except SystemExit as error: + code = error.code + finally: + sys.argv = previous + text = output.getvalue() + reported = re.findall(r"^axioms: (\d+) results,", text, flags=re.M) + return { + "accepted": code == 0 and text.rstrip().endswith("\nPASS"), + "exit_code": code, + "reported_results": int(reported[0]) if reported else None, + "subprocess_calls": len(calls), + "stdout_sha256": sha(text.encode()), + } + + +def report(name, axioms=()): + if not axioms: + return f"'{name}' does not depend on any axioms\n" + return f"'{name}' depends on axioms: [{', '.join(axioms)}]\n" + + +def audit(): + inputs = pinned_inputs() + original = inputs[TARGET].decode() + queries = inputs[PROBES].decode() + # This is the immutable source inventory, independently read from the pin. + lines = queries.splitlines(keepends=True) + names = [line.split()[2] for line in lines if line.startswith("#print axioms ")] + require(len(names) == len(set(names)) == 42, "unexpected source inventory") + healthy = "".join(report(name, ("propext", "Classical.choice", "Quot.sound")) + for name in names) + cases = [] + + def case(label, source, output, old_accept, new_accept, old_count=None): + cases.append((label, source, output, old_accept, new_accept, old_count)) + + case("complete_allowed_inventory", queries, healthy, True, True, 42) + case("complete_axiom_free_inventory", queries, + "".join(report(name) for name in names), True, True, 42) + case("reordered_queries_and_reports", "import HyperplaneEnd\n" + "".join( + f"#print axioms {name}\n" for name in reversed(names)), + "".join(report(name) for name in reversed(names)), True, True, 42) + case("wrapped_allowed_axiom_lists", queries, + healthy.replace("propext, Classical.choice, Quot.sound", + "propext,\n Classical.choice,\n Quot.sound"), True, True, 42) + case("empty_inventory", "import HyperplaneEnd\n", "", True, False, 0) + for name in names: + reduced_queries = "".join(line for line in lines if line != f"#print axioms {name}\n") + reduced_reports = "".join(report(other) for other in names if other != name) + case("omit_query:" + name, reduced_queries, reduced_reports, True, False, 41) + # Existing rejection is retained when only compiler output disappears. + case("omit_report:" + name, queries, reduced_reports, False, False) + indented = "".join(" " + line if line.startswith("#print axioms") else line + for line in lines) + case("indented_complete_inventory", indented, healthy, True, True, 0) + forbidden = "".join(report(name, ("sorryAx",)) if name == names[0] else report(name) + for name in names) + case("indented_forbidden_dependency", indented, forbidden, True, False, 0) + case("ordinary_forbidden_dependency", queries, forbidden, False, False) + first = names[0] + case("substitute_unrelated_theorem", queries.replace(first, "Nat.add_comm"), + healthy.replace(first, "Nat.add_comm"), True, False, 42) + case("duplicate_query", queries + f"#print axioms {first}\n", + healthy + report(first), True, False, 43) + case("comment_out_one_query", queries.replace(f"#print axioms {first}", + f"-- #print axioms {first}"), "".join(report(n) for n in names[1:]), True, False, 41) + case("unexpected_report", queries, healthy + report("Nat.add_comm"), True, False, 42) + case("duplicate_report", queries, healthy + report(first), True, False, 42) + case("conflicting_duplicate_report", queries, forbidden + report(first), True, False, 42) + case("conflicting_duplicate_report_reversed", queries, report(first) + forbidden, + True, False, 42) + case("malformed_report", queries, healthy.replace(f"'{first}'", "malformed", 1), + False, False) + + with tempfile.TemporaryDirectory(prefix="hpe-inventory-audit-") as temporary: + directory = Path(temporary) + for name, data in inputs.items(): + target = directory / name + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(data) + patch = HERE / "repair.patch" + for args in (["--check"], []): + subprocess.run(["git", "apply", *args, str(patch)], cwd=directory, + check=True, capture_output=True, timeout=30) + repaired = (directory / TARGET).read_text() + rows = [] + for label, source, output, old_accept, new_accept, old_count in cases: + old = run_driver(original, directory, source, output) + new = run_driver(repaired, directory, source, output) + require(old["accepted"] == old_accept, "original behavior differs: " + label) + require(new["accepted"] == new_accept, "repair behavior differs: " + label) + if old_count is not None: + require(old["reported_results"] == old_count, "original count differs: " + label) + if new_accept: + require(new["reported_results"] == 42, "repair failed full coverage: " + label) + # Query inventory changes must stop before either expensive subprocess. + if label.startswith("omit_query:") or label in { + "empty_inventory", "substitute_unrelated_theorem", "duplicate_query", + "comment_out_one_query", + }: + require(new["subprocess_calls"] == 0, "late inventory rejection: " + label) + rows.append({"case": label, "original": old, "repaired": new}) + + # A real, retained Lean 4.21 transcript checks the grammar separately. + fixture = (HERE / "fixtures/ProbeSyntax.lean").read_bytes() + transcript = (HERE / "fixtures/lean421.txt").read_text() + fixture_meta = json.loads((HERE / "fixtures/LEAN.json").read_text()) + require(sha(fixture) == fixture_meta["source_sha256"], "Lean fixture source drift") + require(sha(transcript.encode()) == fixture_meta["stdout_sha256"], "Lean transcript drift") + require(fixture_meta["version"].startswith("Lean (version 4.21.0,"), "wrong fixture Lean version") + parsed = re.findall(r"'([^']+)' (does not depend on any axioms|depends on axioms: \[[^\]]*\])", + transcript) + require([name for name, _ in parsed] == ["HPEInventoryFixture.clean", + "HPEInventoryFixture.ext", "HPEInventoryFixture.bad"], "real probe names differ") + ns = {"__name__": "repaired_probe_parser", "__file__": str(directory / TARGET)} + exec(compile(repaired, str(directory / TARGET), "exec"), ns) + for index, allowed in ((0, True), (1, True), (2, False)): + name, suffix = parsed[index] + rejected = False + with contextlib.redirect_stdout(io.StringIO()): + try: + ns["check_axiom_reports"](f"'{name}' {suffix}\n", [name]) + except SystemExit: + rejected = True + require(rejected != allowed, "real transcript classification differs: " + name) + + return { + "status": "PASS_HPE_AXIOM_INVENTORY_AUDIT", + "scope": "Python control-flow audit using substituted subprocess results; real Lean 4.21 syntax fixture only, not an HPE build or theorem audit.", + "source_driver_sha256": sha(inputs[TARGET]), + "source_queries_sha256": sha(inputs[PROBES]), + "repair_patch_sha256": sha((HERE / "repair.patch").read_bytes()), + "repaired_driver_sha256": sha(repaired.encode()), + "required_probes": names, + "driver_cases": len(rows), + "omitted_queries_rejected_before_build": len(names), + "existing_missing_report_rejections_preserved": len(names), + "real_lean_syntax_cases": 3, + "cases": rows, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-receipt", type=Path, help="write a new receipt; refuse to overwrite") + args = parser.parse_args() + result = audit() + rendered = json.dumps(result, indent=2) + "\n" + if args.write_receipt: + with args.write_receipt.open("x", encoding="utf-8") as stream: + stream.write(rendered) + else: + require(json.loads((HERE / "RESULT.json").read_text()) == result, "committed receipt differs") + print(f"{result['status']} probes=42 driver_cases={result['driver_cases']} real_lean_syntax_cases=3 no_HPE_build") + + +if __name__ == "__main__": + main()