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..d09dd5c3b5 --- /dev/null +++ b/research/u8-b-cancellation-seed32/NOTICE.md @@ -0,0 +1,20 @@ +# 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. + +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/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..d475a5d052 --- /dev/null +++ b/research/u8-b-cancellation-seed32/README.md @@ -0,0 +1,78 @@ +# 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 +PASS_U8_B_SHEAR_PACKAGE_CLOSURE normal_and_optimized=PASS relocated=PASS controls=4 +``` + +## 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. + +`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 +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 +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/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 new file mode 100644 index 0000000000..7c476d1816 --- /dev/null +++ b/research/u8-b-cancellation-seed32/test_package.py @@ -0,0 +1,80 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Test complete replay, byte equality, relocation and missing/corrupted inputs.""" +import json +from pathlib import Path +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