From c9d2523a3d30b8f6b16cf038bf723a191342ff20 Mon Sep 17 00:00:00 2001 From: martinxxx9 Date: Tue, 13 Oct 2026 20:20:45 +0200 Subject: [PATCH 1/2] Research: document exact U8 B-stage shear rewrites --- research/u8-b-cancellation-seed32/CLAIM.md | 20 ++++++++ research/u8-b-cancellation-seed32/NOTICE.md | 12 +++++ research/u8-b-cancellation-seed32/PROOF.md | 28 +++++++++++ research/u8-b-cancellation-seed32/README.md | 50 +++++++++++++++++++ research/u8-b-cancellation-seed32/RESULT.json | 45 +++++++++++++++++ .../u8-b-cancellation-seed32/test_package.py | 10 ++++ 6 files changed, 165 insertions(+) create mode 100644 research/u8-b-cancellation-seed32/CLAIM.md create mode 100644 research/u8-b-cancellation-seed32/NOTICE.md create mode 100644 research/u8-b-cancellation-seed32/PROOF.md create mode 100644 research/u8-b-cancellation-seed32/README.md create mode 100644 research/u8-b-cancellation-seed32/RESULT.json create mode 100644 research/u8-b-cancellation-seed32/test_package.py diff --git a/research/u8-b-cancellation-seed32/CLAIM.md b/research/u8-b-cancellation-seed32/CLAIM.md new file mode 100644 index 0000000000..47c2d0889f --- /dev/null +++ b/research/u8-b-cancellation-seed32/CLAIM.md @@ -0,0 +1,20 @@ +# Sprint claim — U8 B-gate cancellation audit + +- Track / seed: complex supplier (20–39), OS-random assignment seed 32. +- Base commit: `abdc6a7002abdbcd9e21bfc5e1a795784deacfdf`. +- Current selected record: PR942 / T37, conditional kappa `1661960547713947/10^18`; no frontier edit is proposed. +- Three narrow candidates inspected: (1) coalesce fourteen dependency-safe repeated A additions, (2) delete four dependency-safe inverse B-addition pairs, (3) re-lower large cleanup coefficients. Seed 32 selects the B region; candidate (2) has the strongest favorable complete local budget because it removes work rather than changing coefficients. +- Claimed object: four apparent inverse add pairs in the selected U8 `native/local/CANONICAL-WORD.json.gz`, B indices 176/178, 194/196, 204/206, and 278/280. +- Method: source-pin the accepted replay archive; independently replay the exact scalar word on arbitrary basis columns before and after deleting each pair; prove a local commutation/cancellation criterion; regenerate the emitted local programs; compare exact semantic, frame, profile, macro, and primitive invoices; include single-deletion and dependency-touch negative controls. +- Expected deliverable: a scoped finite complex-supplier construction or a precise obstruction if native/frame admission fails. No new kappa without a complete supplier and outer reprice. +- Expected finish: 2026-10-13 21:00 CEST. +- Coordination: no pinned sprint coordination issue was found; recent open-PR title/body searches found no U8 B-cancellation claim, so this claim is local. + +## Final update + +Completed a finite complex-supplier construction. Four three-shear fragments were +rewritten exactly, saving four B-stage macros and 52 real-component primitives in +each orientation while preserving the full 728-column B map and local paid profile. +The standalone verifier and nine controls pass, as do the unchanged emitter/frame +auditor, optimized and relocated replays, selected-record checker and five selected +record tests. No global supplier reprice or new kappa is claimed. diff --git a/research/u8-b-cancellation-seed32/NOTICE.md b/research/u8-b-cancellation-seed32/NOTICE.md new file mode 100644 index 0000000000..f482831db9 --- /dev/null +++ b/research/u8-b-cancellation-seed32/NOTICE.md @@ -0,0 +1,12 @@ +# Notice and attribution + +The frozen selected U8 word and local verifier derive from the PR942/T37 closure and +its retained complex-supplier lineage: Jonathan Capalbo (#942), Chafik Boukhalfa +(#890/#741), Jeremy Kothe (#869/#870/#799), Hao Yan (#858), and the earlier work +credited by `research/complex-sw4-frame8/NOTICE.md` and the selected source manifest. + +The four shear rewrites, independent exact checker, proof note and controls were +prepared for martin Rv with substantial OpenAI assistance in research, mathematics, +implementation, verification and writing. No independent human review is claimed. +New material is offered under Apache-2.0. Existing source packages and notices are +unchanged. diff --git a/research/u8-b-cancellation-seed32/PROOF.md b/research/u8-b-cancellation-seed32/PROOF.md new file mode 100644 index 0000000000..b69cbe32b6 --- /dev/null +++ b/research/u8-b-cancellation-seed32/PROOF.md @@ -0,0 +1,28 @@ +# Three-shear rewrite + +For distinct registers `x`, `s`, and `y`, let `E(t <- u, q)` denote `t += q u`. +When no intervening operation writes `x` or `s`, the selected triples have the form + +`E(x <- s, a); E(y <- x, q); E(x <- s, -a)`. + +Applied to arbitrary incoming values, the outputs are + +- `x' = x`, +- `s' = s`, +- `y' = y + q(x + a s) = y + q x + q a s`. + +Therefore the triple equals + +`E(y <- x, q); E(y <- s, q a)`. + +All four concrete triples use one common frame, so the replacement introduces no +frame transition. `verify.py` checks this identity locally and checks the complete +1,918-event original and 1,914-event candidate B-stage matrices on all 728 arbitrary +input columns. The unchanged selected local emitter and independent frame/wrapper +auditor were also run during validation; both orientations retained the exact paid +profile and 192-bit allowance while saving 52 real-component primitives. + +This is a finite local construction. It does not establish that the four rewrites +can improve the selected exponent without rebuilding global hosting and the outer +invoice, and it does not discharge inherited all-size/compiler, physical realization, +precision/tape, exact-recovery or analytic-transfer assumptions. diff --git a/research/u8-b-cancellation-seed32/README.md b/research/u8-b-cancellation-seed32/README.md new file mode 100644 index 0000000000..b1ea065181 --- /dev/null +++ b/research/u8-b-cancellation-seed32/README.md @@ -0,0 +1,50 @@ +# Four exact U8 B-stage shear rewrites + +**Finite complex-supplier construction; no new kappa.** Four three-add fragments in +the selected PR942 U8 local word admit the exact rewrite + +`x += a*s; y += q*x; x -= a*s` -> `y += q*x; y += (q*a)*s`. + +The B stage drops from 1,918 to 1,914 scalar operations. Under the unchanged selected +binary-Horner invoice, each orientation saves 52 real-component primitives: +193,306 -> 193,254 forward and 193,354 -> 193,302 backward. All 728 arbitrary +columns and the paid rank profile are unchanged. + +## Reproduce + +From repository root, using Python 3.10+ and the standard library: + +```sh +python3 -I -B research/u8-b-cancellation-seed32/verify.py +python3 -I -B research/u8-b-cancellation-seed32/test_package.py +``` + +Expected: + +```text +PASS_U8_B_SHEAR_REWRITE_SEED32 rewrites=4 B=1918->1914 primitives=193306->193254/193354->193302 columns=728 controls=9 no_new_kappa +PASS_U8_B_SHEAR_PACKAGE deterministic_result=1 +``` + +## Evidence and scope + +`verify.py` pins the accepted `t37-replay.tar.gz` and canonical-word payload, applies +the four literal rewrites, compares complete exact sparse-rational B-stage matrices, +checks each symbolic three-register identity separately, reproduces baseline receipts, +and rejects nine controls: four single deletions, four wrong cross terms and one +intervening dependency touch. + +The unchanged `hpe_emit_local.py` and `hpe_audit_local.py` additionally passed on the +candidate during validation: 728 columns in each orientation, unchanged paid profile, +25 inherited frame/wrapper controls rejected, and prefix bounds of 55/72 bits under +the retained 192-bit allowance. These validation commands are source-bound to the +current repository but are not needed by the one-command independent replay. + +No global owner map, complete complex-supplier invoice or outer 47-inequality assembly +was rebuilt, so no kappa change is claimed. All-size/compiler, common-label and +mutable-source realization, whole-call hosting, physical routing, precision/tape, +exact recovery and analytic transfer remain inherited. Finite replay is not a formal +proof of the multiplication theorem. + +Base commit: `abdc6a7002abdbcd9e21bfc5e1a795784deacfdf`. OS-random assignment seed: +32 (complex-supplier track). The selected PR942 certificate remains unchanged. diff --git a/research/u8-b-cancellation-seed32/RESULT.json b/research/u8-b-cancellation-seed32/RESULT.json new file mode 100644 index 0000000000..6f66488a34 --- /dev/null +++ b/research/u8-b-cancellation-seed32/RESULT.json @@ -0,0 +1,45 @@ +{ + "all_exact_columns": 728, + "archive_sha256": "48285025105210b56a32d3d4d57a21b7591760acc709d38073e4dca339eb06fe", + "assignment_seed": 32, + "b_events": [ + 1918, + 1914 + ], + "backward_real_component_primitives": [ + 193354, + 193302 + ], + "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "canonical_word_sha256": "387a2266ffe006d20042221d967f67a4b18d9bb8de1cd1e01d4031b539fa74a5", + "controls_rejected": [ + "drop_first_0", + "drop_first_1", + "drop_first_2", + "drop_first_3", + "wrong_cross_term_0", + "wrong_cross_term_1", + "wrong_cross_term_2", + "wrong_cross_term_3", + "intervening_target_write" + ], + "forward_real_component_primitives": [ + 193306, + 193254 + ], + "new_kappa": false, + "paid_profile_unchanged": { + "1": 2548, + "2": 338, + "3": 446, + "4": 162, + "5": 72, + "8": 8 + }, + "real_component_primitives_saved_each_orientation": 52, + "rewrite_count": 4, + "scalar_macros_saved_each_orientation": 4, + "scope": "Exact finite B-stage identity and unchanged-emitter local admission; global hosting, outer pricing, all-size/compiler, precision/tape and analytic transfer are not rebuilt.", + "status": "PASS_U8_B_SHEAR_REWRITE_SEED32", + "track": "complex supplier" +} diff --git a/research/u8-b-cancellation-seed32/test_package.py b/research/u8-b-cancellation-seed32/test_package.py new file mode 100644 index 0000000000..decdd35706 --- /dev/null +++ b/research/u8-b-cancellation-seed32/test_package.py @@ -0,0 +1,10 @@ +#!/usr/bin/env python3 +import json, subprocess, sys, tempfile +from pathlib import Path +HERE=Path(__file__).resolve().parent +with tempfile.TemporaryDirectory() as d: + out=Path(d)/"RESULT.json" + p=subprocess.run([sys.executable,"-I","-B",str(HERE/"verify.py"),"--write-result",str(out)],capture_output=True,text=True,check=True) + assert p.stdout.strip().startswith("PASS_U8_B_SHEAR_REWRITE_SEED32") + assert json.loads(out.read_text())==json.loads((HERE/"RESULT.json").read_text()) +print("PASS_U8_B_SHEAR_PACKAGE deterministic_result=1") From e542ad18d87e71479152dc51935a326b6c53a6fe Mon Sep 17 00:00:00 2001 From: martinxxx9 Date: Wed, 14 Oct 2026 18:13:12 +0200 Subject: [PATCH 2/2] Restore complete U8 B-stage verifier and immutable input pins Publish the missing primary verifier and archive/member source pins. Reproduce the original result byte for byte, keep checks active under optimized Python, and exercise relocated replay plus four corrupted or missing input controls. Record the retained emitter and independent frame/wrapper audit evidence. --- research/u8-b-cancellation-seed32/NOTICE.md | 8 + research/u8-b-cancellation-seed32/README.md | 30 +- .../u8-b-cancellation-seed32/SOURCES.json | 13 + .../u8-b-cancellation-seed32/VALIDATION.json | 132 +++++++ .../u8-b-cancellation-seed32/test_package.py | 86 +++- research/u8-b-cancellation-seed32/verify.py | 367 ++++++++++++++++++ 6 files changed, 627 insertions(+), 9 deletions(-) create mode 100644 research/u8-b-cancellation-seed32/SOURCES.json create mode 100644 research/u8-b-cancellation-seed32/VALIDATION.json create mode 100644 research/u8-b-cancellation-seed32/verify.py diff --git a/research/u8-b-cancellation-seed32/NOTICE.md b/research/u8-b-cancellation-seed32/NOTICE.md index f482831db9..d09dd5c3b5 100644 --- a/research/u8-b-cancellation-seed32/NOTICE.md +++ b/research/u8-b-cancellation-seed32/NOTICE.md @@ -10,3 +10,11 @@ prepared for martin Rv with substantial OpenAI assistance in research, mathemati implementation, verification and writing. No independent human review is claimed. New material is offered under Apache-2.0. Existing source packages and notices are unchanged. + +The complete primary verifier and immutable input pins were reconstructed and +published in response to the maintainer review, with OpenAI Codex assistance. +Its scalar lowering and binary-Horner invoice follow +`research/complex-sw4-frame8/local/hpe_emit_local.py`, retaining the attributed +work of icekylinx and DreamingOfClouds with OpenAI Codex and Anthropic Claude +assistance, and the source package's full contributor lineage. Additional local +validation uses the attributed PR514/PR433 independent frame/wrapper auditor. diff --git a/research/u8-b-cancellation-seed32/README.md b/research/u8-b-cancellation-seed32/README.md index b1ea065181..d475a5d052 100644 --- a/research/u8-b-cancellation-seed32/README.md +++ b/research/u8-b-cancellation-seed32/README.md @@ -24,6 +24,7 @@ Expected: ```text PASS_U8_B_SHEAR_REWRITE_SEED32 rewrites=4 B=1918->1914 primitives=193306->193254/193354->193302 columns=728 controls=9 no_new_kappa PASS_U8_B_SHEAR_PACKAGE deterministic_result=1 +PASS_U8_B_SHEAR_PACKAGE_CLOSURE normal_and_optimized=PASS relocated=PASS controls=4 ``` ## Evidence and scope @@ -34,11 +35,38 @@ checks each symbolic three-register identity separately, reproduces baseline rec and rejects nine controls: four single deletions, four wrong cross terms and one intervening dependency touch. +`SOURCES.json` declares the complete immutable input closure: the already committed +`research/community-frontier942-audit/t37-replay.tar.gz` and the hashes of its +canonical word, baseline emitted programs, and baseline local receipts. The checker +reads only these pinned regular members, never extracts the archive, imports no +construction code, and needs no network access. It regenerates both complete baseline +programs, checks them against the archived programs and receipts, and replays the +candidate in both orientations using exact rational arithmetic. The generated result +must match the original committed `RESULT.json` byte for byte. + +The package test runs normal and optimized isolated Python processes, then repeats +them in a relocated fixture containing only this package and its declared archive. +It also requires rejection of missing source pins, changed archive bytes, a wrong +canonical-word member pin, and changed result bytes. All checks use explicit failures +and remain active with `-O`. + The unchanged `hpe_emit_local.py` and `hpe_audit_local.py` additionally passed on the candidate during validation: 728 columns in each orientation, unchanged paid profile, 25 inherited frame/wrapper controls rejected, and prefix bounds of 55/72 bits under the retained 192-bit allowance. These validation commands are source-bound to the -current repository but are not needed by the one-command independent replay. +original base and recorded with exact source digests in `VALIDATION.json`; they are +not needed by the one-command independent replay. To reproduce this additional +validation, create an empty directory and run (POSIX shell example): + +```sh +replay=$(mktemp -d) +python3 -I -B research/u8-b-cancellation-seed32/verify.py --write-candidate "$replay/CANONICAL-WORD.json.gz" +python3 -I -B research/complex-sw4-frame8/local/hpe_emit_local.py "$replay" +python3 -I -B research/complex-sw4-frame8/local/hpe_audit_local.py "$replay" +``` + +The restored verifier and committed source pins address the maintainer's review of +the incomplete submitted head `c9d2523a3d30b8f6b16cf038bf723a191342ff20`. No global owner map, complete complex-supplier invoice or outer 47-inequality assembly was rebuilt, so no kappa change is claimed. All-size/compiler, common-label and diff --git a/research/u8-b-cancellation-seed32/SOURCES.json b/research/u8-b-cancellation-seed32/SOURCES.json new file mode 100644 index 0000000000..8fdf8c97b6 --- /dev/null +++ b/research/u8-b-cancellation-seed32/SOURCES.json @@ -0,0 +1,13 @@ +{ + "schema": "u8-b-shear-immutable-inputs-v1", + "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "archive": { + "path": "research/community-frontier942-audit/t37-replay.tar.gz", + "sha256": "48285025105210b56a32d3d4d57a21b7591760acc709d38073e4dca339eb06fe" + }, + "members": { + "native/local/CANONICAL-WORD.json.gz": "387a2266ffe006d20042221d967f67a4b18d9bb8de1cd1e01d4031b539fa74a5", + "native/local/LOCAL-CHECKS.json": "a99aef882cd6f7631127fd8a116ad4bbaed60e3822455d4f846ae0f45b5af575", + "native/local/LOCAL-PROGRAMS.json.gz": "8b6a9e3a2411a04e5ca79ba6cd1dd449b21c95f65ca127475167d9b97c80a1ce" + } +} diff --git a/research/u8-b-cancellation-seed32/VALIDATION.json b/research/u8-b-cancellation-seed32/VALIDATION.json new file mode 100644 index 0000000000..1c428900e7 --- /dev/null +++ b/research/u8-b-cancellation-seed32/VALIDATION.json @@ -0,0 +1,132 @@ +{ + "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "environment": { + "platform": "Windows", + "python": "3.12.14" + }, + "independent_frame_wrapper_audit": { + "local": { + "backward": { + "all_exact_columns": 728, + "charged_payload_bits": 192, + "prefix_bits_upper": 72, + "prefix_l1_upper": "48299247708513087628079/16", + "private_work_erased": true + }, + "forward": { + "all_exact_columns": 728, + "charged_payload_bits": 192, + "prefix_bits_upper": 55, + "prefix_l1_upper": "6812058044968180837/256", + "private_work_erased": true + } + }, + "negative_controls_rejected": [ + "wrong_scale", + "missing_center", + "wrong_common_frame", + "wrong_child_rank", + "missing_pre_wrapper", + "missing_post_wrapper", + "wrapper_with_wrong_frame", + "wrapper_in_wrong_phase", + "wrapper_on_a_data_register", + "wrapper_on_a_target_register", + "wrapper_on_a_centre_register", + "hpe_pre_wrapper_resolved_to_full_recipe", + "hpe_post_wrapper_without_terminal_frame", + "hpe_post_wrapper_wrong_terminal_frame", + "hpe_tail_gate_at_full_frame", + "hpe_tail_climb_dropped", + "hpe_helper_exit_adapter_to_full", + "hpe_tail_gate_moved_into_full_cleanup", + "cold_hpe_pre_wrapper_replaced_by_identity_entry_adapter", + "cold_hpe_pre_wrapper_dropped", + "cold_hpe_post_wrapper_replaced_by_exit_adapter", + "cold_hpe_pre_wrapper_resolved_to_cold_full_convention", + "cold_hpe_wrapper_with_nonzero_entrance", + "cold_hpe_post_wrapper_wrong_terminal_frame", + "cold_hpe_premix_gate_before_pre_wrapper" + ], + "paid_profiles": { + "backward": { + "1": 2548, + "2": 338, + "3": 446, + "4": 162, + "5": 72, + "8": 8 + }, + "forward": { + "1": 2548, + "2": 338, + "3": 446, + "4": 162, + "5": 72, + "8": 8 + } + }, + "status": "PASS_INDEPENDENT_LOCAL_SCALAR_FRAME_AND_WRAPPER_REPLAY" + }, + "primary_and_package_replay": { + "normal_isolated": "PASS", + "optimized_isolated": "PASS", + "original_result_byte_equality": true, + "package_controls_rejected": [ + "missing_source_pins", + "archive_byte_mutation", + "canonical_member_pin_mutation", + "result_byte_mutation" + ], + "relocated_normal_isolated": "PASS", + "relocated_optimized_isolated": "PASS", + "rewrite_controls_rejected": 9 + }, + "prior_submitted_head": "c9d2523a3d30b8f6b16cf038bf723a191342ff20", + "retained_emitter_checks": { + "backward": { + "all_columns": 728, + "events": 24411, + "paid_profile": { + "1": 2548, + "2": 338, + "3": 446, + "4": 162, + "5": 72, + "8": 8 + }, + "private_centers_cleared": true, + "private_coefficient_stream_cleared_after_each_macro": true, + "real_component_primitive_bound": 193302, + "scalar_macros": 19209, + "sha256": "71afac81d844bd4a23fecfc138e1654dcbb34c17f8605fb45920db1727d48cfe" + }, + "forward": { + "all_columns": 728, + "events": 24411, + "paid_profile": { + "1": 2548, + "2": 338, + "3": 446, + "4": 162, + "5": 72, + "8": 8 + }, + "private_centers_cleared": true, + "private_coefficient_stream_cleared_after_each_macro": true, + "real_component_primitive_bound": 193254, + "scalar_macros": 19209, + "sha256": "bd6271c5b3a8563757d61d5f0353b136916b31f433c29da0bc39a65caecce1df" + } + }, + "scope": "Finite B-stage identity and local admission only; no global supplier reprice or new kappa.", + "trial_main": { + "base_head": "ae95f60feec79897b153dba6459bb3f9fd4d7b8e", + "patch_applies_cleanly": true, + "optimized_package_replay": "PASS" + }, + "validation_sources_at_original_base": { + "research/complex-sw4-frame8/local/hpe_audit_local.py": "6bd9a1e279c9c9e4f3767d9f82e537b559292906feb2ddab02f380fb6523a810", + "research/complex-sw4-frame8/local/hpe_emit_local.py": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805" + } +} diff --git a/research/u8-b-cancellation-seed32/test_package.py b/research/u8-b-cancellation-seed32/test_package.py index decdd35706..7c476d1816 100644 --- a/research/u8-b-cancellation-seed32/test_package.py +++ b/research/u8-b-cancellation-seed32/test_package.py @@ -1,10 +1,80 @@ #!/usr/bin/env python3 -import json, subprocess, sys, tempfile +# SPDX-License-Identifier: Apache-2.0 +"""Test complete replay, byte equality, relocation and missing/corrupted inputs.""" +import json from pathlib import Path -HERE=Path(__file__).resolve().parent -with tempfile.TemporaryDirectory() as d: - out=Path(d)/"RESULT.json" - p=subprocess.run([sys.executable,"-I","-B",str(HERE/"verify.py"),"--write-result",str(out)],capture_output=True,text=True,check=True) - assert p.stdout.strip().startswith("PASS_U8_B_SHEAR_REWRITE_SEED32") - assert json.loads(out.read_text())==json.loads((HERE/"RESULT.json").read_text()) -print("PASS_U8_B_SHEAR_PACKAGE deterministic_result=1") +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def run(package, optimized=False, arguments=(), failure=None): + flags = ["-I", "-B"] + (["-O"] if optimized else []) + process = subprocess.run([sys.executable, *flags, str(package / "verify.py"), *map(str, arguments)], + cwd=package, capture_output=True, text=True) + if failure is not None: + require(process.returncode != 0 and failure in process.stderr, + "packaging control was not rejected: " + failure) + require("PASS_U8_B_SHEAR_REWRITE_SEED32" not in process.stdout, "failed input reported success") + else: + require(process.returncode == 0, "verifier failed: " + process.stderr) + require(process.stdout.strip().startswith("PASS_U8_B_SHEAR_REWRITE_SEED32"), "success marker missing") + + +def main(): + expected = (HERE / "RESULT.json").read_bytes() + pins = json.loads((HERE / "SOURCES.json").read_bytes()) + with tempfile.TemporaryDirectory() as directory: + temporary = Path(directory) + for optimized in (False, True): + out = temporary / "RESULT.json" + run(HERE, optimized, ["--write-result", out]) + require(out.read_bytes() == expected, "deterministic result bytes differ") + + # Only the package and its declared immutable archive are copied. + relocated = temporary / "relocated" + package = relocated / "research" / HERE.name + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__")) + archive = relocated / pins["archive"]["path"] + archive.parent.mkdir(parents=True) + shutil.copyfile(ROOT / pins["archive"]["path"], archive) + for optimized in (False, True): + out = temporary / "relocated-result.json" + run(package, optimized, ["--write-result", out]) + require(out.read_bytes() == expected, "relocated result bytes differ") + + source_path = package / "SOURCES.json" + original_sources = source_path.read_bytes() + source_path.unlink() + run(package, True, failure="SOURCES.json") + source_path.write_bytes(original_sources) + + with archive.open("ab") as stream: + stream.write(b"corrupted archive") + run(package, True, failure="archive pin differs") + shutil.copyfile(ROOT / pins["archive"]["path"], archive) + + bad_pins = json.loads(original_sources) + bad_pins["members"]["native/local/CANONICAL-WORD.json.gz"] = "0" * 64 + source_path.write_text(json.dumps(bad_pins), encoding="utf-8") + run(package, True, failure="member pin differs") + source_path.write_bytes(original_sources) + + (package / "RESULT.json").write_bytes(expected + b"\n") + run(package, True, failure="committed deterministic result differs") + + print("PASS_U8_B_SHEAR_PACKAGE deterministic_result=1") + print("PASS_U8_B_SHEAR_PACKAGE_CLOSURE normal_and_optimized=PASS relocated=PASS controls=4") + + +if __name__ == "__main__": + main() diff --git a/research/u8-b-cancellation-seed32/verify.py b/research/u8-b-cancellation-seed32/verify.py new file mode 100644 index 0000000000..8e36bd0776 --- /dev/null +++ b/research/u8-b-cancellation-seed32/verify.py @@ -0,0 +1,367 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Reproduce the finite PR1115 shear rewrite from committed, immutable inputs. + +Prepared for Martin Rv with OpenAI Codex assistance. Scalar lowering and the +binary-Horner invoice follow the attributed complex-sw4-frame8 local emitter; +the sparse rational checker below imports no construction code. +""" +import argparse +from collections import Counter +import copy +from fractions import Fraction +import gzip +from hashlib import sha256 +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +REWRITE_INDICES = (176, 194, 204, 278) +WORD_MEMBER = "native/local/CANONICAL-WORD.json.gz" +CHECKS_MEMBER = "native/local/LOCAL-CHECKS.json" +PROGRAMS_MEMBER = "native/local/LOCAL-PROGRAMS.json.gz" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def load_inputs(): + pins = json.loads((HERE / "SOURCES.json").read_bytes()) + require(pins.get("schema") == "u8-b-shear-immutable-inputs-v1", "unsupported source schema") + require(set(pins["members"]) == {WORD_MEMBER, CHECKS_MEMBER, PROGRAMS_MEMBER}, + "immutable input inventory differs") + archive_path = (ROOT / pins["archive"]["path"]).resolve() + require(archive_path.is_relative_to(ROOT.resolve()), "archive path escapes repository") + require(sha256(archive_path.read_bytes()).hexdigest() == pins["archive"]["sha256"], + "archive pin differs") + payloads = {} + # Read only the three pinned regular members; never extract or execute members. + with tarfile.open(archive_path, "r:gz") as archive: + for name, expected in pins["members"].items(): + matches = [member for member in archive.getmembers() if member.name == name] + require(len(matches) == 1, "missing or duplicate input member: " + name) + member = matches[0] + require(member.isfile() and 0 <= member.size <= 16 * 1024 * 1024, + "invalid input member: " + name) + stream = archive.extractfile(member) + require(stream is not None, "unreadable input member: " + name) + payloads[name] = stream.read() + require(sha256(payloads[name]).hexdigest() == expected, "member pin differs: " + name) + word = json.loads(gzip.decompress(payloads[WORD_MEMBER])) + checks = json.loads(payloads[CHECKS_MEMBER]) + programs = json.loads(gzip.decompress(payloads[PROGRAMS_MEMBER])) + return pins, word, checks, programs + + +def shear_replacement(triple): + require(len(triple) == 3 and all(event[0] == "add" for event in triple), + "rewrite requires three adjacent additions") + first, middle, last = triple + x, source, target = first[1], first[2], middle[1] + require(len({x, source, target}) == 3 and middle[2] == x, + "rewrite register dependency differs") + require(last[1:3] == first[1:3] and first[-1] == middle[-1] == last[-1], + "rewrite register or common frame differs") + a, q = Fraction(first[3], first[4]), Fraction(middle[3], middle[4]) + require(a != 0 and q != 0 and Fraction(last[3], last[4]) == -a, + "rewrite inverse coefficient differs") + cross = a * q + return [list(middle), ["add", target, source, cross.numerator, cross.denominator, first[-1]]] + + +def rewritten_word(word): + candidate = copy.deepcopy(word) + for index in reversed(REWRITE_INDICES): + candidate["B"][index:index + 3] = shear_replacement(word["B"][index:index + 3]) + return candidate + + +def apply_scalar(rows, operation): + tag, target = operation[:2] + if tag == "clear": + rows[target] = {} + elif tag == "copy": + rows[target] = dict(rows[operation[2]]) + elif tag == "scale": + q = Fraction(operation[2], operation[3]) + rows[target] = {column: q * value for column, value in rows[target].items() if q * value} + else: + require(tag == "add", "unknown scalar operation: " + tag) + source, numerator, denominator = operation[2:5] + require(source != target, "self addition is outside the scalar interface") + q = Fraction(numerator, denominator) + row = rows.setdefault(target, {}) + for column, value in list(rows[source].items()): + updated = row.get(column, Fraction(0)) + q * value + if updated: + row[column] = updated + else: + row.pop(column, None) + + +def stage_matrix(events, columns, backward=False): + rows = {register: {register: Fraction(1)} for register in range(columns)} + for event in events: + event = list(event) + if backward: + if event[0] == "add": + event[1], event[2], event[3] = event[2], event[1], -event[3] + else: + event[2], event[3] = event[3], event[2] + apply_scalar(rows, event[:-1]) + return rows + + +def contains(smaller, larger): + for vector in smaller: + for pivot in larger: + if vector >> (pivot.bit_length() - 1) & 1: + vector ^= pivot + if vector: + return False + return True + + +def lowered(event, backward): + event = list(event) + if event[0] == "add": + target, source, numerator, denominator = event[1:5] + if backward: + target, source, numerator = source, target, -numerator + return ["add", ["L", target], ["L", source], numerator, denominator] + require(event[0] == "scale", "unsupported word operation") + numerator, denominator = event[2:4] + if backward: + numerator, denominator = denominator, numerator + return ["scale", ["L", event[1]], numerator, denominator] + + +def emit_program(word, backward): + """Lower the frozen scalar word using the retained frame/center convention.""" + frames, current = word["frames"], list(word["start"]) + v, columns = word["v"], 2 * word["v"] + word["R"] + entering = {r for r in range(2 * v, columns) if word["start"][r] != 0} + ended = {r for r in range(2 * v, columns) if word["final"][r] != 1} + wrapped = entering | ended + events = [["phase", "zero_frame_precondition"]] + + def scalar(operation, frame): + events.append(["scalar", operation, frame]) + + def climb(register, frame, phase): + old = current[register] + if old == frame: + return + require(contains(frames[old], frames[frame]), "non-nested frame climb") + rank = len(frames[frame]) - len(frames[old]) + require(rank > 0, "non-positive frame climb") + events.append(["climb", phase, register, old, frame, rank]) + current[register] = frame + + for event in word["precondition"] + word["compensation"]: + registers = event[1:3] if event[0] == "add" else event[1:2] + require(all(word["start"][r] == 0 for r in registers), "nonzero precondition frame") + scalar(lowered(event, backward), 0) + events.append(["phase", "entry_adapters"]) + for register, frame in enumerate(word["start"]): + if register in wrapped: + events.append(["residual_adapter", "pre", register, frame] + + ([word["final"][register]] if register in ended else [])) + else: + events.append(["adapter", "old_to_new", register, frame]) + phases = ["A", "centers", "B"] + (["cleanup_tail"] if word.get("tail") else []) + ["final"] + for phase in phases: + events.append(["phase", phase]) + if phase in ("A", "B", "cleanup_tail"): + for event in word["tail"] if phase == "cleanup_tail" else word[phase]: + registers = event[1:3] if event[0] == "add" else event[1:2] + for register in registers: + climb(register, event[-1], phase) + scalar(lowered(event, backward), event[-1]) + elif phase == "centers": + def level(register): + return word.get("target_levels", {}).get(str(register - v), 0) + require(all(current[r] == level(r) for r in range(v, 2 * v)), "center target frame differs") + for k, register in enumerate(word["centers"]): + frame = word["center_frames"][k] + require(current[register] == frame, "center source frame differs") + terms = [event for event in word["cut"] if event[2] == register] + path = [frame] + sorted({level(event[1]) for event in terms} - {frame}, + key=lambda item: -len(frames[item])) + private = ["C", k] + if not backward: + scalar(["clear", private], frame) + scalar(["copy", private, ["L", register]], frame) + for step in range(len(path)): + if step: + events.append(["center", k, path[step - 1], path[step], + len(frames[path[step - 1]]) - len(frames[path[step]])]) + for event in terms: + if level(event[1]) == path[step]: + scalar(["add", ["L", event[1]], private, event[3], event[4]], path[step]) + scalar(["clear", private], path[-1]) + else: + scalar(["clear", private], path[-1]) + for step in reversed(range(len(path))): + for event in terms: + if level(event[1]) == path[step]: + scalar(["add", private, ["L", event[1]], event[3], event[4]], path[step]) + if step: + events.append(["center", k, path[step], path[step - 1], + len(frames[path[step - 1]]) - len(frames[path[step]])]) + scalar(["add", ["L", register], private, -1, 1], frame) + scalar(["clear", private], frame) + else: + for register, frame in enumerate(word["final"]): + climb(register, frame, phase) + events.append(["phase", "exit_adapters"]) + for register, frame in enumerate(word["final"]): + if register not in ended: + events.append(["adapter", "new_to_old", register, frame]) + events.append(["phase", "full_frame_cleanup"]) + for event in word["cleanup"]: + registers = event[1:3] if event[0] == "add" else event[1:2] + require(all(word["final"][r] == 1 for r in registers), "cleanup frame differs") + scalar(lowered(event, backward), 1) + for register in sorted(wrapped): + events.append(["residual_adapter", "post", register, word["start"][register]] + + ([word["final"][register]] if register in ended else [])) + events.append(["phase", "done"]) + return events + + +def primitive_bound(operation): + if operation[0] in ("clear", "copy"): + return 1 + q = Fraction(*operation[3:5]) if operation[0] == "add" else Fraction(*operation[2:4]) + numerator, denominator = abs(q.numerator), q.denominator + require(numerator > 0 and denominator & (denominator - 1) == 0, "non-dyadic scalar") + if operation[0] == "scale": + require(numerator & (numerator - 1) == 0, "non-binary scale") + return abs(numerator.bit_length() - denominator.bit_length()) + int(q < 0) + return 3 + numerator.bit_length() - 1 + numerator.bit_count() + denominator.bit_length() - 1 + + +def replay_program(events, word, backward): + columns, v = 2 * word["v"] + word["R"], word["v"] + rows = {("L", r): {r: Fraction(1)} for r in range(columns)} + paid, macros, primitives = Counter(), 0, 0 + for event in events: + if event[0] == "climb": + paid[event[5]] += 1 + elif event[0] == "center": + paid[event[4]] += 1 + elif event[0] == "scalar": + operation = copy.deepcopy(event[1]) + macros += 1 + primitives += 2 * primitive_bound(operation) + operation[1] = tuple(operation[1]) + if operation[0] in ("add", "copy"): + operation[2] = tuple(operation[2]) + apply_scalar(rows, operation) + require(all(not row for register, row in rows.items() if register[0] == "C"), "private centers not cleared") + for register in range(columns): + expected = {register: Fraction(1)} + if backward and register < v: + expected[v + register] = Fraction(-1) + elif not backward and v <= register < 2 * v: + expected[register - v] = Fraction(1) + require(rows["L", register] == expected, "complete local map differs at register " + str(register)) + profile = {str(rank): count for rank, count in sorted(paid.items())} + require(profile == word["local_profile"], "paid rank profile differs") + return {"sha256": sha256(canonical(events)).hexdigest(), "events": len(events), + "scalar_macros": macros, "real_component_primitive_bound": primitives, + "paid_profile": profile, "all_columns": columns, "private_centers_cleared": True, + "private_coefficient_stream_cleared_after_each_macro": True} + + +def verify(): + pins, word, baseline_checks, baseline_programs = load_inputs() + columns = 2 * word["v"] + word["R"] + candidate = rewritten_word(word) + baseline_matrix = stage_matrix(word["B"], columns) + require(stage_matrix(candidate["B"], columns) == baseline_matrix, "complete B-stage map differs") + require(stage_matrix(candidate["B"], columns, True) == stage_matrix(word["B"], columns, True), + "inverse-transpose B-stage map differs") + for index in REWRITE_INDICES: + triple = word["B"][index:index + 3] + require(stage_matrix(triple, columns) == stage_matrix(shear_replacement(triple), columns), + "local three-register identity differs") + controls = [] + for k, index in enumerate(REWRITE_INDICES): + dropped = copy.deepcopy(word["B"]) + dropped.pop(index) + require(stage_matrix(dropped, columns) != baseline_matrix, "single-deletion control accepted") + controls.append("drop_first_" + str(k)) + for k, index in enumerate(REWRITE_INDICES): + wrong = copy.deepcopy(candidate["B"]) + cross = wrong[index - k + 1] + cross[3] = -cross[3] + require(stage_matrix(wrong, columns) != baseline_matrix, "wrong-cross-term control accepted") + controls.append("wrong_cross_term_" + str(k)) + triple = word["B"][REWRITE_INDICES[0]:REWRITE_INDICES[0] + 3] + touch = ["scale", triple[0][1], 2, 1, triple[0][-1]] + require(stage_matrix([triple[0], touch, triple[1], triple[2]], columns) != + stage_matrix([touch] + shear_replacement(triple), columns), "dependency-touch control accepted") + controls.append("intervening_target_write") + original, changed = {}, {} + for name, backward in (("forward", False), ("backward", True)): + events = emit_program(word, backward) + require(events == baseline_programs[name], "baseline emitted program differs: " + name) + original[name] = replay_program(events, word, backward) + require(original[name] == baseline_checks[name], "baseline receipt differs: " + name) + changed[name] = replay_program(emit_program(candidate, backward), candidate, backward) + require(original[name]["scalar_macros"] - changed[name]["scalar_macros"] == len(REWRITE_INDICES), + "scalar macro saving differs") + savings = [original[name]["real_component_primitive_bound"] - changed[name]["real_component_primitive_bound"] + for name in ("forward", "backward")] + require(savings[0] == savings[1] and savings[0] > 0, "orientation primitive savings differ") + result = { + "all_exact_columns": columns, "archive_sha256": pins["archive"]["sha256"], "assignment_seed": 32, + "b_events": [len(word["B"]), len(candidate["B"])], + "backward_real_component_primitives": [original["backward"]["real_component_primitive_bound"], + changed["backward"]["real_component_primitive_bound"]], + "base_commit": pins["base_commit"], "canonical_word_sha256": pins["members"][WORD_MEMBER], + "controls_rejected": controls, + "forward_real_component_primitives": [original["forward"]["real_component_primitive_bound"], + changed["forward"]["real_component_primitive_bound"]], + "new_kappa": False, "paid_profile_unchanged": changed["forward"]["paid_profile"], + "real_component_primitives_saved_each_orientation": savings[0], "rewrite_count": len(REWRITE_INDICES), + "scalar_macros_saved_each_orientation": len(word["B"]) - len(candidate["B"]), + "scope": "Exact finite B-stage identity and unchanged-emitter local admission; global hosting, outer pricing, all-size/compiler, precision/tape and analytic transfer are not rebuilt.", + "status": "PASS_U8_B_SHEAR_REWRITE_SEED32", "track": "complex supplier" + } + return result, candidate + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", type=Path) + parser.add_argument("--write-candidate", type=Path, help="write the verified candidate canonical word for local validation") + args = parser.parse_args() + result, candidate = verify() + receipt = (json.dumps(result, sort_keys=True, indent=2) + "\n").encode() + require(receipt == (HERE / "RESULT.json").read_bytes(), "committed deterministic result differs") + if args.write_result: + args.write_result.write_bytes(receipt) + if args.write_candidate: + args.write_candidate.write_bytes(gzip.compress(canonical(candidate), mtime=0)) + forward, backward = result["forward_real_component_primitives"], result["backward_real_component_primitives"] + print(f'{result["status"]} rewrites={result["rewrite_count"]} B={result["b_events"][0]}->{result["b_events"][1]} ' + f'primitives={forward[0]}->{forward[1]}/{backward[0]}->{backward[1]} ' + f'columns={result["all_exact_columns"]} controls={len(result["controls_rejected"])} no_new_kappa') + + +if __name__ == "__main__": + try: + main() + except (ValueError, OSError, KeyError, tarfile.TarError) as error: + raise SystemExit("FAIL_U8_B_SHEAR_REWRITE_SEED32: " + str(error)) from error