From a2078691245ff8d2825def7048680759b695cb49 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 14 Oct 2026 00:30:27 -0700 Subject: [PATCH] Independently audit helper450 with exact forward basis execution --- .../k8-hpe450-forward-audit/AUDITED-PR.json | 39 +++ research/k8-hpe450-forward-audit/README.md | 84 +++++ research/k8-hpe450-forward-audit/RESULT.json | 169 +++++++++++ research/k8-hpe450-forward-audit/SOURCES.json | 66 ++++ research/k8-hpe450-forward-audit/TASK.json | 106 +++++++ .../k8-hpe450-forward-audit/VALIDATION.json | 105 +++++++ research/k8-hpe450-forward-audit/VERIFY.json | 26 ++ research/k8-hpe450-forward-audit/verify.py | 286 ++++++++++++++++++ 8 files changed, 881 insertions(+) create mode 100644 research/k8-hpe450-forward-audit/AUDITED-PR.json create mode 100644 research/k8-hpe450-forward-audit/README.md create mode 100644 research/k8-hpe450-forward-audit/RESULT.json create mode 100644 research/k8-hpe450-forward-audit/SOURCES.json create mode 100644 research/k8-hpe450-forward-audit/TASK.json create mode 100644 research/k8-hpe450-forward-audit/VALIDATION.json create mode 100644 research/k8-hpe450-forward-audit/VERIFY.json create mode 100644 research/k8-hpe450-forward-audit/verify.py diff --git a/research/k8-hpe450-forward-audit/AUDITED-PR.json b/research/k8-hpe450-forward-audit/AUDITED-PR.json new file mode 100644 index 0000000000..a11695ab42 --- /dev/null +++ b/research/k8-hpe450-forward-audit/AUDITED-PR.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "pr": 1611, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1611", + "head": "156cc788b5a8122b19686f015e5654b117e4389d", + "head_rechecked_at": "2026-10-14T07:25:02Z", + "files": [ + { + "path": "research/k8-hpe450-binding/README.md", + "git_blob": "b98cac4f60bf0dc948ae36829d1c4a9230c6f950" + }, + { + "path": "research/k8-hpe450-binding/RESULT.json", + "git_blob": "0622528203ff46dea954f63de9dc959246caeffa" + }, + { + "path": "research/k8-hpe450-binding/SOURCES.json", + "git_blob": "e9441e66add7a48d0ca8995a1a1c60c0d614c139" + }, + { + "path": "research/k8-hpe450-binding/TASK.json", + "git_blob": "6cda2c6827589d5a68d01ae4bf36ae2b1d843c60" + }, + { + "path": "research/k8-hpe450-binding/VERIFY.json", + "git_blob": "3c84195008ee5fa26564b5e8603c16635416922e" + }, + { + "path": "research/k8-hpe450-binding/test_verify.py", + "git_blob": "3104297d69f08c1a013684228d5d764accd16db7" + }, + { + "path": "research/k8-hpe450-binding/verify.py", + "git_blob": "04b46bd90dd0a4ba807af1f044fe69d803eb6908" + } + ], + "coverage": "All seven published package files read and matched to Git blobs. Static theorem-composition and scalar-checker review; the exact pending verifier was replayed separately with all 28 controls. New checker imports no pending code.", + "limitations": "No new Lean build, complete event translation, actual hosting, or full selected cold replay. This is agent corroboration, not independent human review." +} diff --git a/research/k8-hpe450-forward-audit/README.md b/research/k8-hpe450-forward-audit/README.md new file mode 100644 index 0000000000..4270eb39d1 --- /dev/null +++ b/research/k8-hpe450-forward-audit/README.md @@ -0,0 +1,84 @@ +# Independent forward audit of k8 helper 450 + +This package independently checks the scalar part of +[PR1611](https://github.com/CrocSwap/integer-mult-bounds/pull/1611) at +`156cc788b5a8122b19686f015e5654b117e4389d`: helper **450** of the pinned +seven-slot k8 word has a unit output row and an isolated input column in both +emitted local orientations. [RESULT.json](RESULT.json) records the passing exact +replay. No actionable discrepancy was found in the predecessor. + +The starting main is `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. The selected +PR1094 manifest pins the k8 slot record. Pinned ancestral transport and emitter +producers rebuild the canonical word and complete event lists, which match the +published slot hashes. The new checker +imports no PR1611 checker, pending package code or scalar replay function. +[SOURCES.json](SOURCES.json) records the consumed source pins. + +## Exact coverage and independence + +For each orientation, forward execution starts separately at every coordinate +vector of the **712-register** scalar domain: 704 local registers and eight +private centers. Each execution retains emitted ADD, SCALE, COPY and CLEAR +operations, using exact dyadic arithmetic. The checker records helper450's +output on every input basis vector, and every output coordinate for its own +input vector. Thus it checks all 712 entries of the helper's output row and its +complete dirt column, including arbitrary private inputs and their zero entries. +Across both orientations this is **1,424 input basis executions**; it is not a +comparison of every entry of the complete 712-by-712 scalar matrix. + +PR1611 obtains the output row by reverse covector propagation over exact +rationals. Here the row is assembled from independent forward executions. +The source producers and emitted inputs are shared; the scalar algorithm and +dyadic implementation are independently written. Each orientation has 24,767 +events and 19,693 scalar operations. Six semantic faults reject: dropping or +flipping the last helper ADD, and adding a dirt-leaking read. The extra read +preserves the row but leaks `1/2` to L230 forward and `1` to L27 backward. +The arithmetic check compares 4,624 dyadic operand pairs with `Fraction`; a +four-input dirty echo tests destructive COPY/CLEAR and inverse scales. + +The checked row is `delta(j,450)` and the checked column is `e_450`. +Linearity proves scalar output restoration for every arbitrary input and no +scalar leakage of its initial dirt. Column isolation is an additional finite +restoration obligation; the retained `hpe_block` theorem needs the unit row. + +## Conditional operator conclusion and replay + +PR1611 separately binds the actual wrapper events and exact serialized recipe +`2:999` to `HyperplaneEnd.Exact.pair3`, including phase. Under exact relabel +recipes and a valid correspondence from the emitted events to the formal word, +the unit row gives `T_U T_E^-1`. Correct wrappers give +`L^-1 T_U T_E^-1 R^-1`, and retained `exact_N_pair3` makes this `C7 tensor I4`. +This audit adds no new Lean theorem, operator-kernel check or physical endpoint +admission. COPY/CLEAR translation and private lifetimes, exact recipes for other +events, ownership/footprints, whole-call hosting, all-size compilation, +precision/tape bounds, complete costs and analytic transfer remain obligations. +The selected frontier, paid profile and kappa are unchanged. + +From the repository root, with standard-library Python 3.12: + +```sh +python3.12 -B scripts/research_package.py --package research/k8-hpe450-forward-audit +``` + +[TASK.json](TASK.json) records the revision-3 `formal-interface-lemma` refinement, +selection nonce and [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1394#discussioncomment-18918131). +The source-bound baseline passed as orientation only. The session reserves its +last quarter for verification and handoff; construction stops at 07:38 UTC. +[AUDITED-PR.json](AUDITED-PR.json) pins the reviewed package, and +[VALIDATION.json](VALIDATION.json) separates local execution from unclaimed CI. + +## Open next questions + +- Can this one helper be connected to an actual Lean event word? First specify + private COPY/CLEAR lifetimes and wrapper labels. The missing serialization + correspondence remains the blocker; more scalar examples do not remove it. +- Can the local helper be traced through each selected T16 hosted invocation? + Start with the pinned owner map and chart/route evidence; exact recipes and + nonempty disjoint footprints remain separate physical premises. + +Credit: Hanson Sun (@bbMisk), PR1611; Jeremy Kothe, HPE formalization and k8; +DreamingOfClouds, wrappers and Lemma A/G; icekylinx, compiler; Rohan Arun, packing; +Josie Elliston and Sagar Thakrar, word/audit lineage; @commdata2338, PR1415; +Chafik Boukhalfa, Zhihao Chen and all retained realization contributors. +New corroboration: @ToikY, with substantial OpenAI Codex assistance in analysis, +implementation, testing and writing. Apache-2.0; original notices retained; no independent human review claimed. diff --git a/research/k8-hpe450-forward-audit/RESULT.json b/research/k8-hpe450-forward-audit/RESULT.json new file mode 100644 index 0000000000..95992f7601 --- /dev/null +++ b/research/k8-hpe450-forward-audit/RESULT.json @@ -0,0 +1,169 @@ +{ + "status": "PASS_HPE450_FORWARD_BASIS_AUDIT", + "helper": 450, + "audited_pr": 1611, + "audited_head": "156cc788b5a8122b19686f015e5654b117e4389d", + "program_sha256": { + "forward": "071ecdacc0bb3ac16046aad4119ed551a945cb0ed6c57002a548a3e2232503d8", + "backward": "f36c5831106f5637102c6bedeec76ed2b223c6671ce42fd0eceed9ef24725b23" + }, + "input_sha256": { + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-local/inputs/phase-baseline/CANONICAL-WORD.json.gz": "e070ae2c78b4a1b644b418774af62b40d8d16e6ba89602f0474afb557d507c37", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_audit_and_transport.py": "c9a05ff291016b870b4fc925b317abd9c3a604c73ffc8920dfdbbeb475e20aa3", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_emit_local.py": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805", + "research/gauge44-slots/construction/slots/SLOT-PINS-k8.json": "55dd229684febecb80638eff9c6b3986623e8539c6c956753b350209c3e0efe2", + "research/t16-owner-audit-seed67/inputs/k8-seven-slot-word.json.gz": "49596aa4ed4fd36cd4582fd0e8ddeb09fd80370a7d8aea1ede52a135b536d289", + "research/community-frontier1094-audit/SELECTED-SOURCE.json": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + "arithmetic_control": { + "exact_arithmetic_pairs": 4624, + "invalid_coefficients_rejected": 3, + "dirty_echo_basis_inputs": 4, + "copy_clear_semantic_controls": 2 + }, + "orientations": { + "forward": { + "events": 24767, + "scalar_operations": 19693, + "basis_inputs": 712, + "output_row": [ + [ + [ + "L", + 450 + ], + "1" + ] + ], + "dirt_column": [ + [ + [ + "L", + 450 + ], + "1" + ] + ], + "private_input_coefficients": [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + "controls": { + "omitted_last_helper_add": { + "input": [ + "L", + 27 + ], + "output": [ + "L", + 450 + ], + "actual": "1", + "expected": "0" + }, + "flipped_last_helper_add": { + "input": [ + "L", + 27 + ], + "output": [ + "L", + 450 + ], + "actual": "2", + "expected": "0" + }, + "restored_row_but_dirt_leak": { + "input": [ + "L", + 450 + ], + "output": [ + "L", + 230 + ], + "actual": "1/2", + "expected": "0" + } + } + }, + "backward": { + "events": 24767, + "scalar_operations": 19693, + "basis_inputs": 712, + "output_row": [ + [ + [ + "L", + 450 + ], + "1" + ] + ], + "dirt_column": [ + [ + [ + "L", + 450 + ], + "1" + ] + ], + "private_input_coefficients": [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + "controls": { + "omitted_last_helper_add": { + "input": [ + "L", + 450 + ], + "output": [ + "L", + 27 + ], + "actual": "-1", + "expected": "0" + }, + "flipped_last_helper_add": { + "input": [ + "L", + 450 + ], + "output": [ + "L", + 27 + ], + "actual": "-2", + "expected": "0" + }, + "restored_row_but_dirt_leak": { + "input": [ + "L", + 450 + ], + "output": [ + "L", + 27 + ], + "actual": "1", + "expected": "0" + } + } + } + }, + "scope": "Exact finite scalar row/column corroboration only. No event-to-Lean translation, operator/recipe theorem, hosting, full cold replay or new kappa." +} diff --git a/research/k8-hpe450-forward-audit/SOURCES.json b/research/k8-hpe450-forward-audit/SOURCES.json new file mode 100644 index 0000000000..b816d8a0d7 --- /dev/null +++ b/research/k8-hpe450-forward-audit/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-local/inputs/phase-baseline/CANONICAL-WORD.json.gz", + "usage": "input", + "git_blob": "cbb49a627768c42e1ff752f43ccfcc56ffe2cb0b", + "sha256": "e070ae2c78b4a1b644b418774af62b40d8d16e6ba89602f0474afb557d507c37" + }, + { + "path": "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_audit_and_transport.py", + "usage": "input", + "git_blob": "d5d3509d90c01fd91dd00b78743287614b532e48", + "sha256": "c9a05ff291016b870b4fc925b317abd9c3a604c73ffc8920dfdbbeb475e20aa3" + }, + { + "path": "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_emit_local.py", + "usage": "input", + "git_blob": "534fdc71f7641c704575efc038363d7eb206b2df", + "sha256": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805" + }, + { + "path": "research/gauge44-slots/construction/slots/SLOT-PINS-k8.json", + "usage": "input", + "git_blob": "2702c368f4de0b671577aee9a0e2df41c1b27658", + "sha256": "55dd229684febecb80638eff9c6b3986623e8539c6c956753b350209c3e0efe2" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean", + "usage": "provenance", + "git_blob": "1af33a206a9ba6c4826b3a1516d104e770380869", + "sha256": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Main.lean", + "usage": "provenance", + "git_blob": "88fcee53762abdd2a17c9cc3a26fef74945f0171", + "sha256": "221a5126ec46141e5cba7689aaddd38746183ed15fa91ec229e32a16302b42a6" + }, + { + "path": "research/t16-owner-audit-seed67/inputs/k8-seven-slot-word.json.gz", + "usage": "input", + "git_blob": "723decbca8995e916d6f4b783aa3e1ddd4eb47fe", + "sha256": "49596aa4ed4fd36cd4582fd0e8ddeb09fd80370a7d8aea1ede52a135b536d289" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/e8-lemma-g-lean/LemmaG/Stream.lean", + "usage": "provenance", + "git_blob": "e89897190307a6f3fcfb858f8de00cc5a7f49b3e", + "sha256": "7138f4b859d0574a803e99401f05ef5e0ec9eeac0eb480775cd9b86595c365f8" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + } + ] +} diff --git a/research/k8-hpe450-forward-audit/TASK.json b/research/k8-hpe450-forward-audit/TASK.json new file mode 100644 index 0000000000..c284e35514 --- /dev/null +++ b/research/k8-hpe450-forward-audit/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "starting_points": [ + "certificates/selected-result.json", + "research/hyperplane-end-lean/PROOF.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently corroborate PR1611 helper450 scalar restoration in both pinned seven-slot k8 orientations: forward execution of every one of 712 input basis vectors, helper output row and complete helper dirt column.", + "scope_change_reason": "PR1611 already supplies the finite emitted-helper/pair3 binding. The allowed independent audit is narrowed to its scalar premise with a different algorithm; no new formal theorem, operator identity, supplier admission or kappa is claimed.", + "bottleneck_link": "Separate forward basis evaluation can corroborate the unit-row premise and isolated-column restoration without trusting the reverse-covector implementation; recipe exactness and event correspondence remain conditional.", + "budget_minutes": 60, + "stop_rule": "Session 2026-10-14 06:53:07..07:53:07 UTC; stop constructing at 07:38 UTC and reserve the final quarter for exact replay, metadata checks and a concise handoff. Stop after the two fixed orientations and stated semantic controls; no broader supplier replay or search.", + "outcome": "completed", + "evidence": "RESULT.json: PASS_HPE450_FORWARD_BASIS_AUDIT; each orientation has 24767 events, 19693 scalar operations and 712 forward input-basis executions (1424 total). Helper450 output row and complete dirt column are unit vectors; all eight private-input coefficients are zero. Six semantic faults reject, including a row-preserving dirt leak of 1/2 to L230 forward and 1 to L27 backward. Exact dyadic arithmetic agrees with Fraction on 4624 operand pairs, and three invalid coefficient controls reject. No actionable discrepancy was found in PR1611 at 156cc788b5a8122b19686f015e5654b117e4389d.", + "author": "@ToikY, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for source review, algorithm derivation, implementation, tests, validation and prose, with bounded subagent review and documentation. No independent human review is claimed.", + "open_questions": [ + { + "question": "Can helper450 be connected to hpe_block through an actual Lean Event word?", + "why_it_matters": "The finite scalar premise does not prove correspondence between serialized events and formal semantics.", + "first_step": "Specify the private COPY/CLEAR lifetimes and wrapper labels for this one emitted word, then prove its translation correspondence.", + "blocked_by": "No JSON-to-Lean event translation proof is supplied; all other RecipesExact hypotheses remain conditional." + }, + { + "question": "Can this local helper be traced through every actual selected T16 hosted invocation?", + "why_it_matters": "Local scalar restoration does not establish physical realization or disjoint hosting.", + "first_step": "Trace helper450 using the pinned owner map and existing chart/route evidence for each actual invocation.", + "blocked_by": "Exact compiled recipes and nonempty disjoint physical footprints remain separate premises." + } + ], + "selection_nonce": "9c92a140d6ff014ccc0bdd30a86e9981", + "scope_key": "e3ffea67887eeb4c396c/k8-seven-slot/helper450/independent-forward-basis-audit", + "method": "Evaluate every input coordinate vector forward through the emitted scalar program using exact dyadic pairs. Collect helper450 output components to reconstruct its row, and retain the full state for helper450 input to check its dirt column. Source producers only; no pending checker imports.", + "nearest_overlap": [ + { + "pr": 1611, + "head": "156cc788b5a8122b19686f015e5654b117e4389d", + "delta": "Same finite scalar facts, independently corroborated by forward basis execution instead of reverse covector propagation. No new identity or formal theorem claimed." + }, + { + "pr": 1415, + "head": "0d8d2c3a96346756f02563b401a042ab97198e20", + "delta": "Its operator-semantic audit is retained context; this package checks a real emitted helper scalar premise and does not repeat its 512-column complex kernels." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1394#discussioncomment-18918131", + "baseline": { + "status": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "scope": "Source-bound orientation only; not supplier admission or full cold replay." + }, + "cost_effect": "No paid profile, precision, construction, frontier or kappa change.", + "conditional_conclusion": "Given exact relabel recipes and an emitted-to-formal event correspondence, unit row plus correct pair3 wrappers yields L^-1 T_U T_E^-1 R^-1 = C7 tensor I4 by retained exact_N_pair3. COPY/CLEAR translation, other recipes, hosting, all-size compilation, precision/tape, costs and analytic transfer remain separate.", + "predecessor_credit": [ + "Hanson Sun (@bbMisk), PR1611", + "Jeremy Kothe, HPE exact formalization and k8", + "DreamingOfClouds, wrappers and Lemma A/G", + "icekylinx, retained compiler", + "Rohan Arun, selected packing", + "Josie Elliston and Sagar Thakrar, retained word/audit lineage", + "@commdata2338, PR1415 semantic audit and emitted-helper follow-up", + "Chafik Boukhalfa, Zhihao Chen and all retained realization contributors" + ], + "selection": { + "seed": "9c92a140d6ff014ccc0bdd30a86e9981", + "track": "independent-verification", + "task_id": "formal-interface-lemma", + "method": "Audit a formal theorem-to-certificate binding independently.", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea" + } +} diff --git a/research/k8-hpe450-forward-audit/VALIDATION.json b/research/k8-hpe450-forward-audit/VALIDATION.json new file mode 100644 index 0000000000..a88d528a38 --- /dev/null +++ b/research/k8-hpe450-forward-audit/VALIDATION.json @@ -0,0 +1,105 @@ +{ + "schema_version": 1, + "environment": { + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "platform": "macOS-26.5.2-arm64-arm-64bit", + "dependencies": "standard library only" + }, + "registered_replay": { + "argv": [ + "{python}", + "-B", + "scripts/research_package.py", + "--package", + "research/k8-hpe450-forward-audit" + ], + "exit_code": 0, + "wall_seconds": 5.716597666032612, + "verify_sha256": "7e495667951d96cd49aab3911627e402165d429bdb38565322a210252102626f" + }, + "standalone_export": [ + { + "check": "read_only_optimized_export_without_git", + "exit_code": 0, + "wall_seconds": 5.612142333295196, + "stdout": "PASS_HPE450_FORWARD_BASIS_AUDIT orientations=2 basis_inputs=1424 controls=6 no_new_kappa", + "file_count": 13 + }, + { + "check": "source_drift_rejected", + "exit_code": 1, + "stderr": "FAIL: source drift: research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_emit_local.py" + }, + { + "check": "receipt_corruption_rejected", + "exit_code": 1, + "stderr": "FAIL: receipt mismatch" + }, + { + "check": "overwrite_refused", + "exit_code": 1, + "existing_bytes_preserved": true + } + ], + "predecessor_direct_replay": { + "pr": 1611, + "head": "156cc788b5a8122b19686f015e5654b117e4389d", + "argv": [ + "{python}", + "-I", + "-B", + "research/k8-hpe450-binding/verify.py" + ], + "exit_code": 0, + "wall_seconds": 6.18948212498799, + "semantic_controls_rejected": 28, + "seven_package_blobs_verified": true + }, + "repository_checks": { + "package_metadata_and_pins": "PASS", + "selected_record": "PASS unchanged", + "onboarding_tests": { + "argv": [ + "{python}", + "-B", + "-m", + "unittest", + "discover", + "-s", + "tests", + "-p", + "test_research_onboarding.py", + "-v" + ], + "tests": 18, + "status": "PASS", + "wall_seconds": 3.272 + } + }, + "overlap": { + "open_prs": 393, + "fetched_at": "2026-10-14T07:25:02Z", + "numbered_pages": [ + 100, + 100, + 100, + 93, + 0 + ], + "drafts_included": true, + "limitations": "Pagination is not atomic while other contributors merge. Live Discussions1163,1166,1394 and active board read; full Discussion pagination unavailable. The offline helper warns about missing Discussion cache. No matches is not a novelty guarantee.", + "nearest": { + "1611": "same scalar premise, new independent forward-basis algorithm", + "1415": "retained complex operator kernels, not repeated", + "1697": "new all511 cold hyperplane operator audit, distinct" + } + }, + "not_run": [ + "fresh Lean/Mathlib build", + "event-to-Lean translation proof", + "actual physical hosting replay", + "full selected supplier cold replay", + "hosted CI" + ], + "review": "Two bounded subagents found no actionable correctness issue in the stated scope; this is agent review, not independent human review." +} diff --git a/research/k8-hpe450-forward-audit/VERIFY.json b/research/k8-hpe450-forward-audit/VERIFY.json new file mode 100644 index 0000000000..390b40d1cd --- /dev/null +++ b/research/k8-hpe450-forward-audit/VERIFY.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-local/inputs/phase-baseline/CANONICAL-WORD.json.gz", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_audit_and_transport.py", + "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_emit_local.py", + "research/gauge44-slots/construction/slots/SLOT-PINS-k8.json", + "research/t16-owner-audit-seed67/inputs/k8-seven-slot-word.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Regenerate both source-pinned local event streams; push all 712 basis inputs forward using exact dyadic arithmetic; certify helper450 unit row and isolated column; compare full deterministic receipt and reject six semantic mutants." + } + ] +} diff --git a/research/k8-hpe450-forward-audit/verify.py b/research/k8-hpe450-forward-audit/verify.py new file mode 100644 index 0000000000..7fdbc2d97b --- /dev/null +++ b/research/k8-hpe450-forward-audit/verify.py @@ -0,0 +1,286 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +# Prepared for @ToikY with substantial OpenAI Codex assistance. +"""Exact forward-basis corroboration of PR1611's scalar row/column claim. + +Uses the pinned main producers only. Does not import the pending PR checker, +its reverse covector implementation, or a producer replay function. +""" +import argparse +import copy +from fractions import Fraction +import gzip +import hashlib +import itertools +import json +import math +import os +from pathlib import Path +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +N = 712 +H = 450 +SOURCE = 'research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code' +VENDOR = 'research/complex-k492-owner-repair/vendor/multicold' +RAW = 'research/t16-owner-audit-seed67/inputs/k8-seven-slot-word.json.gz' +ROUTING = VENDOR + '/vendor/pr558/vendor/pr552/complex-local/inputs/phase-baseline/CANONICAL-WORD.json.gz' +PINS = 'research/gauge44-slots/construction/slots/SLOT-PINS-k8.json' + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def encoded(obj): + return json.dumps(obj, sort_keys=True, separators=(',', ':'), allow_nan=False).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def load(path): + data = path.read_bytes() + return json.loads(gzip.decompress(data) if path.suffix == '.gz' else data) + + +def normalize(n, e): + """Canonical n / 2**e, with odd n unless zero; e may be negative.""" + if not n: + return (0, 0) + absolute = abs(n) + shift = (absolute & -absolute).bit_length() - 1 + return (n >> shift, e - shift) + + +def coefficient(a, b): + require(type(a) is int and type(b) is int and b != 0, 'invalid coefficient') + if b < 0: + a, b = -a, -b + common = math.gcd(a, b) + a, b = a // common, b // common + require(b & (b - 1) == 0, 'non-dyadic coefficient') + return normalize(a, b.bit_length() - 1) + + +def plus(a, b): + if not a[0]: + return b + if not b[0]: + return a + e = max(a[1], b[1]) + return normalize((a[0] << (e - a[1])) + (b[0] << (e - b[1])), e) + + +def times(a, b): + return (a[0] * b[0], a[1] + b[1]) if a[0] and b[0] else (0, 0) + + +def rational(a): + return Fraction(a[0], 1 << a[1]) if a[1] >= 0 else Fraction(a[0] << -a[1]) + + +def wire(reg): + require(isinstance(reg, list) and len(reg) == 2 and type(reg[1]) is int, + 'invalid wire') + tag, index = reg + require(tag in ('L', 'C') and 0 <= index < (704 if tag == 'L' else 8), 'wire range') + return index + (704 if tag == 'C' else 0) + + +def label(index): + return ['L', index] if index < 704 else ['C', index - 704] + + +def decode(events): + ops = [] + for event in events: + if event[0] != 'scalar': + continue + op = event[1] + require(op[0] in ('clear', 'copy', 'scale', 'add'), 'unknown scalar') + tag = op[0] + require(len(op) == {'clear': 2, 'copy': 3, 'scale': 4, 'add': 5}[tag], 'scalar shape') + target = wire(op[1]) + source = wire(op[2]) if tag in ('copy', 'add') else None + require(source != target, 'scalar alias') + q = coefficient(*op[-2:]) if tag in ('scale', 'add') else None + ops.append((tag, target, source, q)) + return ops + + +def push(ops, basis, size=N): + """Literal forward execution on one basis input; no inverse/row pullback.""" + values = [(0, 0)] * size + values[basis] = (1, 0) + for tag, target, source, q in ops: + if tag == 'clear': + values[target] = (0, 0) + elif tag == 'copy': + values[target] = values[source] + elif tag == 'scale': + values[target] = times(values[target], q) + else: + values[target] = plus(values[target], times(values[source], q)) + return values + + +def all_inputs(ops): + column = None + for basis in range(N): + final = push(ops, basis) + require(final[H] == ((1, 0) if basis == H else (0, 0)), + 'helper row differs at ' + str(label(basis))) + if basis == H: + column = final + require(column == [(1, 0) if i == H else (0, 0) for i in range(N)], + 'helper dirt column leaks') + return {'basis_inputs': N, 'output_row': [[label(H), '1']], + 'dirt_column': [[label(H), '1']], 'private_input_coefficients': ['0'] * 8} + + +def witness(ops): + # Check the helper column first, then every remaining input if needed. + for basis in [H] + [i for i in range(N) if i != H]: + final = push(ops, basis) + if basis == H: + for out, value in enumerate(final): + wanted = (1, 0) if out == H else (0, 0) + if value != wanted: + return {'input': label(basis), 'output': label(out), + 'actual': str(rational(value)), 'expected': str(rational(wanted))} + wanted = (1, 0) if basis == H else (0, 0) + if final[H] != wanted: + return {'input': label(basis), 'output': label(H), + 'actual': str(rational(final[H])), 'expected': str(rational(wanted))} + raise ValueError('mutant preserves audited row and column') + + +def controls(events): + last = max(i for i, e in enumerate(events) if e[0] == 'scalar' and + ['L', H] in e[1][1:3]) + require(events[last][1][0] == 'add', 'last helper operation is not ADD') + cases = {} + bad = copy.deepcopy(events) + bad.pop(last) + cases['omitted_last_helper_add'] = witness(decode(bad)) + bad = copy.deepcopy(events) + bad[last][1][3] *= -1 + cases['flipped_last_helper_add'] = witness(decode(bad)) + bad = copy.deepcopy(events) + bad.insert(last + 1, ['scalar', ['add', ['L', 230], ['L', H], 1, 1], events[last][2]]) + cases['restored_row_but_dirt_leak'] = witness(decode(bad)) + # Independent row audit must still pass the dirt-leak control. + bad_ops = decode(bad) + require(all(push(bad_ops, i)[H] == ((1, 0) if i == H else (0, 0)) + for i in range(N)), 'leak unexpectedly alters helper row') + return cases + + +def arithmetic_control(): + # Fraction is only a small oracle, never the full-word implementation. + values = [coefficient(a, b) for a in range(-8, 9) for b in (1, 2, 4, -8)] + for a, b in itertools.product(values, repeat=2): + require(rational(plus(a, b)) == rational(a) + rational(b), 'dyadic add oracle') + require(rational(times(a, b)) == rational(a) * rational(b), 'dyadic multiply oracle') + for a, b in ((1, 0), (True, 1), (1, 3)): + try: + coefficient(a, b) + except ValueError: + pass + else: + raise ValueError('invalid coefficient accepted') + # Dirty COPY/CLEAR echo: all three local coordinates are unchanged and + # private scratch is zero, even when its input was arbitrary. + half = coefficient(1, 2) + toy = [('copy', 3, 1, None), ('add', 0, 3, half), ('clear', 3, None, None), + ('add', 0, 1, coefficient(-1, 2)), + ('scale', 2, None, coefficient(-2, 1)), + ('scale', 2, None, coefficient(-1, 2))] + for basis in range(4): + require(push(toy, basis, 4) == [(1, 0) if i == basis and i < 3 else (0, 0) + for i in range(4)], 'dirty echo map') + add_instead = [('add', 3, 1, (1, 0))] + toy[1:] + require(push(add_instead, 3, 4)[0] == half, 'COPY overwrite control') + no_clear = toy[:2] + toy[3:] + require(push(no_clear, 1, 4)[3] == (1, 0), 'CLEAR scratch control') + return {'exact_arithmetic_pairs': len(values) ** 2, 'invalid_coefficients_rejected': 3, + 'dirty_echo_basis_inputs': 4, 'copy_clear_semantic_controls': 2} + + +def source_bindings(): + rows = load(HERE / 'SOURCES.json')['files'] + inputs = {} + for row in rows: + if row['usage'] != 'input': + continue + path = (ROOT / row['path']).resolve() + require(path.is_relative_to(ROOT) and path.is_file(), 'source path') + require(sha(path.read_bytes()) == row['sha256'], 'source drift: ' + row['path']) + inputs[row['path']] = row['sha256'] + return inputs + + +def compute(): + inputs = source_bindings() + pins = load(ROOT / PINS) + selected = load(ROOT / 'research/community-frontier1094-audit/SELECTED-SOURCE.json') + require(selected['files'][PINS] == inputs[PINS], 'selected slot source binding') + require(sha(gzip.decompress((ROOT / RAW).read_bytes())) == pins['word_sha256'], 'raw pin') + env = dict(os.environ, MULTICOLD_SOURCE=str(ROOT / VENDOR)) + for key in ('PYTHONOPTIMIZE', 'PYTHONPATH', 'PYTHONHOME'): + env.pop(key, None) + with tempfile.TemporaryDirectory(prefix='hpe450-forward-') as tmp: + out = Path(tmp) / 'local' + commands = [ + [ROOT / SOURCE / 'hpe_audit_and_transport.py', '--raw', ROOT / RAW, + '--routing', ROOT / ROUTING, '--out', out], + [ROOT / SOURCE / 'hpe_emit_local.py', out], + ] + for cmd in commands: + run = subprocess.run([sys.executable, '-I', '-B', *map(str, cmd)], + cwd=ROOT, env=env, capture_output=True, text=True, timeout=120) + require(run.returncode == 0, 'producer failure: ' + run.stdout[-1000:] + run.stderr[-1000:]) + require(sha(gzip.decompress((out / 'CANONICAL-WORD.json.gz').read_bytes())) == + pins['canonical_sha256'], 'canonical pin') + programs = load(out / 'LOCAL-PROGRAMS.json.gz') + require(set(programs) == {'forward', 'backward'}, 'orientations') + result = {} + for name in ('forward', 'backward'): + events = programs[name] + require(sha(encoded(events)) == pins['program_sha256'][name], 'program pin') + ops = decode(events) + result[name] = dict(events=len(events), scalar_operations=len(ops), + **all_inputs(ops), controls=controls(events)) + require(source_bindings() == inputs, 'sources changed during run') + return {'status': 'PASS_HPE450_FORWARD_BASIS_AUDIT', 'helper': H, + 'audited_pr': 1611, 'audited_head': '156cc788b5a8122b19686f015e5654b117e4389d', + 'program_sha256': pins['program_sha256'], 'input_sha256': inputs, + 'arithmetic_control': arithmetic_control(), 'orientations': result, + 'scope': 'Exact finite scalar row/column corroboration only. No event-to-Lean ' + 'translation, operator/recipe theorem, hosting, full cold replay or new kappa.'} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-result', type=Path) + args = parser.parse_args() + result = compute() + if args.write_result: + with args.write_result.open('x') as stream: + stream.write(json.dumps(result, indent=2) + '\n') + else: + require(encoded(result) == encoded(load(HERE / 'RESULT.json')), 'receipt mismatch') + print(result['status'] + ' orientations=2 basis_inputs=1424 controls=6 no_new_kappa') + + +if __name__ == '__main__': + try: + main() + except (ValueError, OSError, KeyError, TypeError, subprocess.SubprocessError) as exc: + raise SystemExit('FAIL: ' + str(exc))