diff --git a/research/r420-block8-schedule/CANDIDATE.json b/research/r420-block8-schedule/CANDIDATE.json new file mode 100644 index 0000000000..d150b84906 --- /dev/null +++ b/research/r420-block8-schedule/CANDIDATE.json @@ -0,0 +1,911 @@ +{ + "format": "r420-positive-block-candidate-v1", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "source": "research/e8-bit-r420/data/bitE8mut-r420.json.gz", + "source_sha256": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", + "block_index": 8, + "frame": 550, + "b_slice": [ + 512, + 559 + ], + "slice_convention": "zero-based, start inclusive, end exclusive", + "registers": [ + 2, + 4, + 16, + 18, + 20, + 22, + 96, + 98, + 101, + 103, + 112, + 118 + ], + "operations": [ + [ + 6, + 3 + ], + [ + 0, + 7 + ], + [ + 9, + 7 + ], + [ + 9, + 2 + ], + [ + 10, + 8 + ], + [ + 5, + 9 + ], + [ + 9, + 8 + ], + [ + 11, + 10 + ], + [ + 11, + 4 + ], + [ + 4, + 8 + ], + [ + 4, + 3 + ], + [ + 11, + 6 + ], + [ + 10, + 5 + ], + [ + 6, + 7 + ], + [ + 8, + 4 + ], + [ + 4, + 5 + ], + [ + 0, + 1 + ], + [ + 3, + 0 + ], + [ + 11, + 0 + ], + [ + 3, + 6 + ], + [ + 10, + 3 + ], + [ + 5, + 11 + ], + [ + 3, + 4 + ], + [ + 7, + 11 + ], + [ + 2, + 5 + ], + [ + 6, + 5 + ], + [ + 0, + 5 + ], + [ + 9, + 5 + ], + [ + 1, + 0 + ], + [ + 8, + 6 + ] + ], + "seed": 801018, + "seed_role": "assignment seed 18 selects block 8; search RNG uses 801018", + "original_operations": [ + [ + 11, + 6 + ], + [ + 11, + 0 + ], + [ + 11, + 7 + ], + [ + 11, + 4 + ], + [ + 11, + 10 + ], + [ + 11, + 3 + ], + [ + 11, + 8 + ], + [ + 11, + 1 + ], + [ + 5, + 9 + ], + [ + 5, + 2 + ], + [ + 5, + 7 + ], + [ + 9, + 2 + ], + [ + 9, + 7 + ], + [ + 9, + 8 + ], + [ + 6, + 7 + ], + [ + 6, + 3 + ], + [ + 0, + 7 + ], + [ + 0, + 1 + ], + [ + 4, + 3 + ], + [ + 4, + 8 + ], + [ + 10, + 3 + ], + [ + 10, + 8 + ], + [ + 1, + 11 + ], + [ + 1, + 5 + ], + [ + 1, + 0 + ], + [ + 8, + 11 + ], + [ + 8, + 5 + ], + [ + 8, + 6 + ], + [ + 8, + 4 + ], + [ + 3, + 5 + ], + [ + 3, + 6 + ], + [ + 3, + 0 + ], + [ + 3, + 4 + ], + [ + 10, + 5 + ], + [ + 10, + 6 + ], + [ + 10, + 0 + ], + [ + 4, + 5 + ], + [ + 7, + 11 + ], + [ + 0, + 11 + ], + [ + 0, + 5 + ], + [ + 6, + 11 + ], + [ + 6, + 5 + ], + [ + 2, + 11 + ], + [ + 2, + 5 + ], + [ + 9, + 11 + ], + [ + 9, + 5 + ], + [ + 5, + 11 + ] + ], + "original_count": 47, + "candidate_count": 30, + "forward_plus_cleanup_saving": 34, + "integer_forward_matrix": [ + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1, + 3, + 1, + 1, + 1, + 1 + ], + [ + 2, + 3, + 1, + 1, + 1, + 1, + 1, + 3, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 2, + 1, + 1, + 1, + 1, + 2, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 3, + 1, + 1, + 1, + 3, + 1, + 1, + 0, + 0 + ], + [ + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 0, + 0 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 2, + 1, + 1, + 2, + 3, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 0, + 1, + 1, + 0, + 1, + 2, + 1, + 0, + 1, + 1 + ], + [ + 1, + 1, + 1, + 3, + 2, + 1, + 2, + 3, + 3, + 1, + 1, + 1 + ], + [ + 1, + 1, + 2, + 1, + 1, + 1, + 1, + 3, + 2, + 2, + 1, + 1 + ], + [ + 1, + 1, + 1, + 2, + 0, + 1, + 1, + 3, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 0, + 1, + 1, + 0, + 1, + 1, + 1, + 0, + 1, + 1 + ] + ], + "original_positive_reverse_matrix": [ + [ + 2, + 1, + 0, + 0, + 0, + 3, + 0, + 1, + 0, + 0, + 0, + 7 + ], + [ + 1, + 1, + 0, + 0, + 0, + 2, + 0, + 0, + 0, + 0, + 0, + 4 + ], + [ + 0, + 0, + 1, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 2 + ], + [ + 1, + 0, + 0, + 1, + 1, + 4, + 1, + 0, + 0, + 0, + 0, + 6 + ], + [ + 1, + 0, + 0, + 1, + 3, + 8, + 2, + 0, + 1, + 0, + 0, + 12 + ], + [ + 0, + 0, + 2, + 0, + 1, + 7, + 1, + 2, + 1, + 1, + 0, + 14 + ], + [ + 1, + 0, + 0, + 1, + 1, + 5, + 2, + 1, + 0, + 0, + 0, + 9 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 1 + ], + [ + 0, + 0, + 0, + 0, + 1, + 3, + 1, + 0, + 1, + 0, + 0, + 5 + ], + [ + 0, + 0, + 1, + 0, + 1, + 5, + 1, + 1, + 1, + 1, + 0, + 10 + ], + [ + 2, + 0, + 0, + 1, + 2, + 10, + 3, + 0, + 1, + 0, + 1, + 16 + ], + [ + 8, + 2, + 0, + 4, + 8, + 35, + 9, + 3, + 3, + 0, + 1, + 61 + ] + ], + "candidate_positive_reverse_matrix": [ + [ + 2, + 1, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 1 + ], + [ + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 0, + 1, + 1, + 2, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 0, + 1, + 3, + 4, + 2, + 0, + 1, + 0, + 0, + 2 + ], + [ + 0, + 0, + 0, + 0, + 1, + 3, + 1, + 0, + 1, + 1, + 0, + 2 + ], + [ + 1, + 0, + 0, + 1, + 1, + 3, + 2, + 1, + 0, + 0, + 0, + 1 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 1 + ], + [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 1, + 0, + 0, + 1 + ], + [ + 0, + 0, + 1, + 0, + 1, + 3, + 1, + 1, + 1, + 1, + 0, + 2 + ], + [ + 0, + 0, + 0, + 1, + 2, + 2, + 1, + 0, + 1, + 0, + 1, + 2 + ], + [ + 2, + 0, + 0, + 2, + 4, + 7, + 3, + 1, + 1, + 0, + 1, + 5 + ] + ], + "search": { + "method": "seeded two-sided nonnegative elementary-factor reduction", + "trials": 10000, + "completed": 144, + "successes": 10, + "stages": [ + { + "seed": 801018, + "trials": 10000, + "completed": 144, + "successes": 10, + "improvements": [ + { + "trial_one_based": 21, + "operations": 33 + }, + { + "trial_one_based": 318, + "operations": 30 + } + ], + "reduction_steps": 298194, + "dead_ends": 883, + "length_cutoffs": 8973 + } + ], + "move_order": "i then j; row before column; indices ascending", + "selection_cycle": [ + "uniform", + "maximum gain plus uniform [0,3)", + "maximum gain times uniform [0,1)", + "gain-squared weights", + "minimum gain plus uniform [0,3)", + "maximum square-root gain times uniform [0,1)" + ], + "cutoff": "stop a trial at current best length", + "complete_definition": "residual equals the ordered identity", + "success_definition": "complete and positive reverse matrix dominated", + "optimality_claim": false, + "excluded_exploration": { + "seed": 18, + "requested_trials": 50000, + "completed_trial_count": null, + "status": "interrupted before completion; partial count was not retained", + "improvements_observed": 0, + "used_to_select_candidate": false + } + }, + "limitations": [ + "Only the pinned phase-B block 8 is searched.", + "No claim of minimum length or exhaustive coverage is made.", + "Search includes only nonnegative row and column subtraction paths with diagonal entries at least one.", + "Integer transfer checks are finite circuit checks, not a formal verification of the multiplication theorem." + ], + "assignment_seed": 18, + "search_seed": 801018, + "search_seed_choice": "Manually fixed before the first search trial; arbitrary and distinct from assignment seed." +} diff --git a/research/r420-block8-schedule/CERTIFICATE.json b/research/r420-block8-schedule/CERTIFICATE.json new file mode 100644 index 0000000000..b550a4855c --- /dev/null +++ b/research/r420-block8-schedule/CERTIFICATE.json @@ -0,0 +1,570 @@ +{ + "block": { + "old_gates": 47, + "new_gates": 30, + "forward_matrix": [ + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1, + 3, + 1, + 1, + 1, + 1 + ], + [ + 2, + 3, + 1, + 1, + 1, + 1, + 1, + 3, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 2, + 1, + 1, + 1, + 1, + 2, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 3, + 1, + 1, + 1, + 3, + 1, + 1, + 0, + 0 + ], + [ + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 0, + 0 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 2, + 1, + 1, + 2, + 3, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 0, + 1, + 1, + 0, + 1, + 2, + 1, + 0, + 1, + 1 + ], + [ + 1, + 1, + 1, + 3, + 2, + 1, + 2, + 3, + 3, + 1, + 1, + 1 + ], + [ + 1, + 1, + 2, + 1, + 1, + 1, + 1, + 3, + 2, + 2, + 1, + 1 + ], + [ + 1, + 1, + 1, + 2, + 0, + 1, + 1, + 3, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 0, + 1, + 1, + 0, + 1, + 1, + 1, + 0, + 1, + 1 + ] + ], + "old_positive_reverse": [ + [ + 2, + 1, + 0, + 0, + 0, + 3, + 0, + 1, + 0, + 0, + 0, + 7 + ], + [ + 1, + 1, + 0, + 0, + 0, + 2, + 0, + 0, + 0, + 0, + 0, + 4 + ], + [ + 0, + 0, + 1, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 2 + ], + [ + 1, + 0, + 0, + 1, + 1, + 4, + 1, + 0, + 0, + 0, + 0, + 6 + ], + [ + 1, + 0, + 0, + 1, + 3, + 8, + 2, + 0, + 1, + 0, + 0, + 12 + ], + [ + 0, + 0, + 2, + 0, + 1, + 7, + 1, + 2, + 1, + 1, + 0, + 14 + ], + [ + 1, + 0, + 0, + 1, + 1, + 5, + 2, + 1, + 0, + 0, + 0, + 9 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 1 + ], + [ + 0, + 0, + 0, + 0, + 1, + 3, + 1, + 0, + 1, + 0, + 0, + 5 + ], + [ + 0, + 0, + 1, + 0, + 1, + 5, + 1, + 1, + 1, + 1, + 0, + 10 + ], + [ + 2, + 0, + 0, + 1, + 2, + 10, + 3, + 0, + 1, + 0, + 1, + 16 + ], + [ + 8, + 2, + 0, + 4, + 8, + 35, + 9, + 3, + 3, + 0, + 1, + 61 + ] + ], + "new_positive_reverse": [ + [ + 2, + 1, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 1 + ], + [ + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 0, + 1, + 1, + 2, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 0, + 1, + 3, + 4, + 2, + 0, + 1, + 0, + 0, + 2 + ], + [ + 0, + 0, + 0, + 0, + 1, + 3, + 1, + 0, + 1, + 1, + 0, + 2 + ], + [ + 1, + 0, + 0, + 1, + 1, + 3, + 2, + 1, + 0, + 0, + 0, + 1 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 1 + ], + [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 1, + 0, + 0, + 1 + ], + [ + 0, + 0, + 1, + 0, + 1, + 3, + 1, + 1, + 1, + 1, + 0, + 2 + ], + [ + 0, + 0, + 0, + 1, + 2, + 2, + 1, + 0, + 1, + 0, + 1, + 2 + ], + [ + 2, + 0, + 0, + 2, + 4, + 7, + 3, + 1, + 1, + 0, + 1, + 5 + ] + ], + "strict_reverse_entries": 32 + }, + "original": { + "columns": 660, + "scalar_additions": 26916, + "record_sha256": "f7e6cceaceb04d7bd70918981405dcead988a890cfca03b51e80d935f00a960f", + "copies": 9, + "erasures": 9, + "forward_positive_prefix": 144651, + "reverse_positive_prefix": 2270064, + "five_stage_payload_bits": 100, + "five_stage_payload": "998206739997057013039187410944", + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "paths_sha256": "ef52add0118de86406ed3c58d6ff53b06b127c05238895b475181e55b98021ca" + }, + "candidate": { + "columns": 660, + "scalar_additions": 26882, + "record_sha256": "46658af5872fe818c2aaae8696c2b0b91310cdc8d2195cd1c22253ff25dadd78", + "copies": 9, + "erasures": 9, + "forward_positive_prefix": 144651, + "reverse_positive_prefix": 2212684, + "five_stage_payload_bits": 100, + "five_stage_payload": "948381526944181330213048003584", + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "paths_sha256": "ef52add0118de86406ed3c58d6ff53b06b127c05238895b475181e55b98021ca" + }, + "word_content_sha256": "b187b77553eb2f806ab467c33fcd1e85236faa7d393decbf8491332a3c91be9b", + "controls": [ + "equal_forward_does_not_imply_reverse_domination", + "drop_operation", + "self_addition", + "boolean_wire", + "wrong_frame", + "swapped_register_binding", + "unpriced_cancelled_pair", + "missing_cleanup", + "stale_cleanup_passes_endpoint_but_fails_H4", + "illegal_frame_descent" + ] +} diff --git a/research/r420-block8-schedule/CLAIM.json b/research/r420-block8-schedule/CLAIM.json new file mode 100644 index 0000000000..f77654b249 --- /dev/null +++ b/research/r420-block8-schedule/CLAIM.json @@ -0,0 +1,19 @@ +{ + "track": "Bit supplier", + "assignment_seed": 18, + "seed_source": "Python secrets.randbelow(100), operating-system randomness, drawn once", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "start_utc": "2026-10-13T05:37:53Z", + "expected_finish_utc": "2026-10-13T06:22:53Z", + "coordination": "No pinned issues and no open sprint coordination issue found via GitHub API. Local claim.", + "candidates": [ + "R420 frame-zero compensation: reject due to overlapping forests and two-sided bases in PRs 733, 759, 774.", + "R420 fixed-order frame reduction: reject due to scoped negative results PRs 661, 711, 718.", + "R420 phase-B block 8: selected; exact source-wire map and literal cleanup, with positive-integer prefix domination." + ], + "scope": "Improve the fixed twelve-wire phase-B block 8 and its literal reverse cleanup. Seed selects block 18 mod 10 = 8. No other block, compensation, selected supplier or global assembly is changed.", + "method": "Bounded local positive-integer factor rescheduling; retain the ordered output map, arbitrary dirty-input restoration and native frame paths. Check complete primitive cost and prefix bounds.", + "expected_deliverable": "One frozen circuit with a portable exact verifier, rejection controls, source pins and a scoped research note. No new kappa without complete assembly.", + "overlap": "Read PR789 block7, PR790 block9 and PR774 decoder forests. Those do not change block8. This is a different concrete matrix and its complete native instruction saving, not a repeat of their certificate.", + "status": "claimed" +} diff --git a/research/r420-block8-schedule/SOURCES.json b/research/r420-block8-schedule/SOURCES.json new file mode 100644 index 0000000000..d7a5c0c8da --- /dev/null +++ b/research/r420-block8-schedule/SOURCES.json @@ -0,0 +1,15 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "source_pr543": "2065fe4f72a914d907f1046603f5a36f17018535", + "selected_consumer_pr626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "files": { + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", + "research/e8-bit-r420/code/xcheck.py": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424", + "research/e8-bit-r420/code/gen_l3.py": "d5c802447c99255db1bdfcae62b2116bfc9612c9dc9000d41aa4f5f2fec9f2f2", + "research/e8-bit-r420/code/nodeopt.py": "6a5896f60b1fe05c41ab28ce822dff782c635e12d0c74fad20b5ce2a4010fa3f", + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53" + }, + "native_dependencies": "The independent native harness pins its exact exporter, staging script, three C++ checker files, JSON header and portable header in native.py.", + "scope": "Committed immutable inputs are pinned by exact bytes. Regenerated words are compared by canonical decompressed JSON." +} diff --git a/research/r420-block8-schedule/native.py b/research/r420-block8-schedule/native.py new file mode 100644 index 0000000000..8dcd5e34b1 --- /dev/null +++ b/research/r420-block8-schedule/native.py @@ -0,0 +1,181 @@ +#!/usr/bin/env python3 +"""Replay two R420 words through unchanged, pinned native cohort checkers. + +Usage: python3 -B native.py ORIGINAL.json.gz CANDIDATE.json.gz OUTPUT_DIR +Requires a C++17 compiler and Boost headers. CXX and BOOST_INCLUDE are supported. +Outputs must be outside this repository. No hosted or outer assembly is run. +Jerry Lin, with substantial OpenAI Codex assistance; Apache-2.0. +""" +import gzip +import hashlib +import json +import os +from pathlib import Path +import platform +import shlex +import subprocess +import sys + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / 'research/e8-bit-carrier-skeleton' +BIT = PACKAGE / 'code/bit' +CHECKERS = BIT / 'checkers' +PINS = { + 'code/bit/export_records.py': '8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3', + 'code/bit/regression/stage_cohort.py': '6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a', + 'code/bit/checkers/legality_h.cpp': '6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3', + 'code/bit/checkers/columns_h.cpp': 'd1297f9052be4f2496e1ff2a77e4db2c0cdbd7d460d489b4c03e50bf317238ce', + 'code/bit/checkers/columns_k.cpp': '1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2', + 'code/bit/checkers/json.hpp': 'aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63', + 'portable-include/bits/stdc++.h': '420094be2af295eed03a983dd66debbbe9cfb78d8252859f4498a615a0074b99', +} + + +def need(condition, message): + if not condition: + raise RuntimeError(message) + + +def read_json(path): + with (gzip.open(path, 'rt') if str(path).endswith('.gz') else open(path)) as stream: + return json.load(stream) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def canonical(word): + return digest(json.dumps(word, sort_keys=True, separators=(',', ':')).encode()) + + +def run(args, log, reject=False): + result = subprocess.run([str(x) for x in args], text=True, stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, env={**os.environ, 'PYTHONDONTWRITEBYTECODE': '1'}) + log.write_text(result.stdout) + need((result.returncode != 0) if reject else (result.returncode == 0), + f'Unexpected exit {result.returncode}: {shlex.join([str(x) for x in args])}; see {log}') + return result + + +def export(word_path, directory): + directory.mkdir(parents=True, exist_ok=True) + run([sys.executable, '-I', '-B', BIT / 'export_records.py', word_path, directory / 'records'], + directory / 'export.log') + run([sys.executable, '-I', '-B', BIT / 'regression/stage_cohort.py', directory / 'records', + directory / 'records', directory / 'cin', directory / 'cout'], directory / 'stage.log') + + +def replay(word_path, directory, binaries): + word = read_json(word_path) + need((word['h'], word['v'], word['R'], len(word['ret'])) == (8, 120, 420, 9), 'Not an R420 word') + export(word_path, directory) + cout = directory / 'cout' + run([binaries / 'legality', directory / 'cin', cout, cout / 'legality.json'], directory / 'legality.log') + legality = read_json(cout / 'legality.json') + need(legality['status'] == 'PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE', 'Legality failed') + need(legality['copies'] == legality['erasures'] == 9, 'Wrong copy count') + receipts = {} + for name, stages, omissions in [('columns_h', 5, 6), ('columns_k2', 5, 6), + ('columns_k4', 9, 18), ('columns_k5', 11, 24)]: + run([binaries / name, cout / 'COHORT249-RECORDS.bin', cout / (name + '.json')], directory / (name + '.log')) + receipt = read_json(cout / (name + '.json')) + suffix = 'FIVE_STAGE' if stages == 5 else 'BRIDGED_STAGE' + need(receipt['status'] == f'PASS_NEW_COHORT249_ALL_{suffix}_FORMAL_COLUMNS_AND_PREFIX_BILL', 'Columns failed') + need(receipt['formal_columns_checked'] == (stages - 1) * 120 + 420, 'Wrong column count') + need(len(receipt['stages']) == stages, 'Wrong stage count') + need(receipt['bridge_additions'] == omissions * 120, 'Wrong bridge count') + controls = receipt['negative_controls'] + need(len(controls) == omissions and all(x['rejected'] for x in controls), 'Omitted bridge accepted') + need(dict(receipt['local_raw_H']) == dict(legality['paid_histogram']), 'Histogram mismatch') + need(receipt['local_scalar_additions'] == legality['common_frame_ADDs'], 'ADD count mismatch') + receipts[name] = receipt + five = receipts['columns_h'] + need({k: v for k, v in five.items() if k != 'seconds'} == + {k: v for k, v in receipts['columns_k2'].items() if k != 'seconds'}, 'K2 regression failed') + bounds = five['signed_lift_prefix'] + need([x['reverse'] for x in bounds] == [False, True], 'Wrong prefix orientations') + forward, backward = [int(x['cancellation_free_signed_row_l1_upper']) for x in bounds] + local_payload = 64 * forward ** 3 * backward ** 2 + need(local_payload == int(five['payload_prefix_upper']) < 2 ** 104, 'Wrong five-stage prefix bound') + schedule_bounds = {} + for pairs in (2, 4, 5): + receipt = receipts[f'columns_k{pairs}'] + need(receipt['signed_lift_prefix'] == bounds and + int(receipt['payload_prefix_upper']) == local_payload, 'Local prefix disagreement') + bound = 2 ** (6 * (pairs - 1)) * forward ** (pairs + 1) * backward ** pairs + schedule_bounds[str(2 * pairs + 1)] = {'upper': str(bound), 'bits': bound.bit_length()} + # Delete one actual cleanup XOR. Legality remains valid; every formal-column checker must reject it. + mutant = json.loads(json.dumps(word)) + removed = [mutant['C'][0][0], mutant['C'][0][1], mutant['C'][0][2].pop()] + if not mutant['C'][0][2]: + del mutant['C'][0] + mutant_path = directory / 'missing-cleanup.json.gz' + with gzip.open(mutant_path, 'wt') as stream: + json.dump(mutant, stream, separators=(',', ':')) + bad = directory / 'missing-cleanup' + export(mutant_path, bad) + run([binaries / 'legality', bad / 'cin', bad / 'cout', bad / 'cout/legality.json'], bad / 'legality.log') + rejected = [] + for name in receipts: + result = run([binaries / name, bad / 'cout/COHORT249-RECORDS.bin', bad / 'cout' / (name + '.json')], + bad / (name + '.log'), reject=True) + need('local defining-decoder full formal column' in result.stdout, 'Unexpected mutation failure') + rejected.append(name) + return {'word_content_sha256': canonical(word), 'record_sha256': digest((cout / 'COHORT249-RECORDS.bin').read_bytes()), + 'gates': {phase: len(word[phase]) for phase in 'DABC'}, + 'legality': legality, 'forward_signed_row_l1_upper': str(forward), + 'reverse_signed_row_l1_upper': str(backward), 'local_raw_H': five['local_raw_H'], + 'five_stage_payload_upper': str(local_payload), 'five_stage_payload_bits': local_payload.bit_length(), + 'whole_scalar_schedule_prefix_bounds': schedule_bounds, + 'formal_columns': {str(s): receipts[n]['formal_columns_checked'] for n, s in + [('columns_h', 5), ('columns_k4', 9), ('columns_k5', 11)]}, + 'omitted_bridge_controls': {'5': 6, '9': 18, '11': 24}, 'K2_equals_five_stage': True, + 'missing_cleanup_control': {'removed_frame_destination_source': removed, + 'legality_passed': True, 'rejected_by': rejected}} + + +def main(): + need(len(sys.argv) == 4, __doc__) + original, candidate, out = [Path(x).resolve() for x in sys.argv[1:]] + need(out != ROOT and ROOT not in out.parents, 'Output directory must be outside this repository') + need(not out.exists(), 'Use a new output directory to avoid stale receipts') + for path, expected in PINS.items(): + need(digest((PACKAGE / path).read_bytes()) == expected, f'Source pin mismatch: {path}') + out.mkdir(parents=True) + binaries = out / 'bin' + binaries.mkdir(exist_ok=True) + cxx = shlex.split(os.environ.get('CXX', 'c++')) + boost = os.environ.get('BOOST_INCLUDE') + if not boost: + boost = next((p for p in ('/usr/include', '/usr/local/include', '/opt/homebrew/include') + if (Path(p) / 'boost/multiprecision/cpp_int.hpp').exists()), None) + need(boost is not None, 'Set BOOST_INCLUDE to the Boost header directory') + base = cxx + ['-O2', '-std=c++17', '-DHDIM=8', '-DNCOPY=9', + '-I' + str(PACKAGE / 'portable-include'), '-I' + str(CHECKERS), '-I' + boost] + commands = [] + for name, source, options in [('legality', 'legality_h.cpp', []), ('columns_h', 'columns_h.cpp', [])] + [ + (f'columns_k{k}', 'columns_k.cpp', [f'-DKPAIRS={k}']) for k in (2, 4, 5)]: + flags = [] if name == 'legality' else ['-DVPORTS=120', '-DRHELP=420'] + command = base + flags + options + ['-o', str(binaries / name), str(CHECKERS / source)] + commands.append(command) + run(command, out / (name + '-build.log')) + result = {'status': 'PASS_NATIVE_R420_LOCAL_REPLAY', 'source_package': str(PACKAGE.relative_to(ROOT)), + 'source_sha256': PINS, 'compile_commands': commands, + 'environment': {'python': platform.python_version(), 'platform': platform.platform(), + 'compiler': subprocess.check_output(cxx + ['--version'], text=True).splitlines()[0], + 'boost_include': boost}, + 'prefix_scope': 'The unchanged K4/K5 receipts retain the five-stage payload formula. Whole scalar schedule bounds here multiply local forward/reverse bounds and one factor 2 per bridge shear. These are not hosted physical prefix bills.', + 'remaining_obligations': ['Signed decoder evidence beyond F2 column replay', + 'Mutable-basis common-label realization and exact-bank completion', + 'Hosted physical replay, routing, pricing, and outer assembly'], + 'words': {}} + for name, path in [('original', original), ('candidate', candidate)]: + print(f'Replaying {name}: {path}', flush=True) + result['words'][name] = replay(path, out / name, binaries) + (out / 'native-summary.json').write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + print('PASS:', out / 'native-summary.json') + + +if __name__ == '__main__': + main() diff --git a/research/r420-block8-schedule/search.py b/research/r420-block8-schedule/search.py new file mode 100644 index 0000000000..c4e5428e7b --- /dev/null +++ b/research/r420-block8-schedule/search.py @@ -0,0 +1,215 @@ +#!/usr/bin/env python3 +"""Bounded positive-integer factor search for selected R420 phase-B block 8. + +Prepared by Jerry Lin with substantial OpenAI Codex assistance; Apache-2.0. +The search starts from the pinned integer forward matrix. Each step removes +one elementary positive row or column factor without making any entry negative +or reducing a diagonal entry below one. A completed factorization must end at +the ordered identity. Its literal reverse positive matrix must be entrywise +at most the original reverse matrix. This is a finite heuristic search, not a +claim of minimum length among all circuits or within the reduction class. + +Run from any directory with Python 3; this writes CANDIDATE.json beside this file. +Only the Python standard library is required. +""" +import argparse +import gzip +import hashlib +import json +from pathlib import Path +import random + +ROOT = Path(__file__).resolve().parents[2] +SOURCE = ROOT / "research/e8-bit-r420/data/bitE8mut-r420.json.gz" +SOURCE_SHA256 = "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784" +BASE_COMMIT = "66849e1475c930fd7732b1a0067ffee7e1e95f60" +BLOCK = 8 +FRAME = 550 +N = 12 +IDENTITY = [[int(i == j) for j in range(N)] for i in range(N)] +STAGES = [(801018, 10000)] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def transfer(operations): + matrix = [row[:] for row in IDENTITY] + for dst, src in operations: + matrix[dst] = [x + y for x, y in zip(matrix[dst], matrix[src])] + return matrix + + +def dominated(left, right): + return all(x <= y for a, b in zip(left, right) for x, y in zip(a, b)) + + +def extract(): + raw = SOURCE.read_bytes() + require(hashlib.sha256(raw).hexdigest() == SOURCE_SHA256, "source hash mismatch") + word = json.loads(gzip.decompress(raw)) + indexed = [(i, gate) for i, gate in enumerate(word["B"]) if gate[0] == FRAME] + first, last = indexed[0][0], indexed[-1][0] + 1 + require([i for i, _ in indexed] == list(range(first, last)), "block is not contiguous") + registers = sorted({r for _, (_, dst, srcs) in indexed for r in [dst, *srcs]}) + require(len(registers) == N, "wrong register count") + require(all(len(gate[2]) == 1 for _, gate in indexed), "source gate is not unary") + operations = [(registers.index(dst), registers.index(srcs[0])) + for _, (_, dst, srcs) in indexed] + require([first, last] == [512, 559], "wrong phase-B slice") + require(len(operations) == 47, "wrong source operation count") + return registers, [first, last], operations + + +def choices(matrix): + moves = [] + for i in range(N): + for j in range(N): + if i == j: + continue + # Remove a left factor: row i := row i - row j. + if matrix[i][i] > matrix[j][i] and all( + x >= y for x, y in zip(matrix[i], matrix[j])): + moves.append((sum(matrix[j]), "r", i, j)) + # Remove a right factor: column j := column j - column i. + if matrix[j][j] > matrix[j][i] and all( + matrix[k][j] >= matrix[k][i] for k in range(N)): + moves.append((sum(matrix[k][i] for k in range(N)), "c", i, j)) + return moves + + +def select(moves, mode, rng): + if mode == 0: + return rng.choice(moves) + if mode == 1: + return max(moves, key=lambda move: move[0] + rng.random() * 3) + if mode == 2: + return max(moves, key=lambda move: move[0] * rng.random()) + if mode == 3: + return rng.choices(moves, weights=[move[0] ** 2 for move in moves])[0] + if mode == 4: + return min(moves, key=lambda move: move[0] + rng.random() * 3) + return max(moves, key=lambda move: move[0] ** 0.5 * rng.random()) + + +def search(original): + target = transfer(original) + reverse_limit = transfer(original[::-1]) + best = original + records = [] + for seed, trials in STAGES: + rng = random.Random(seed) + record = {"seed": seed, "trials": trials, "completed": 0, + "successes": 0, "improvements": [], "reduction_steps": 0, + "dead_ends": 0, "length_cutoffs": 0} + for trial in range(trials): + matrix = [row[:] for row in target] + rows, columns = [], [] + while matrix != IDENTITY: + moves = choices(matrix) + if not moves: + record["dead_ends"] += 1 + break + _, kind, i, j = select(moves, trial % 6, rng) + if kind == "r": + matrix[i] = [x - y for x, y in zip(matrix[i], matrix[j])] + rows.append((i, j)) + else: + for k in range(N): + matrix[k][j] -= matrix[k][i] + columns.append((i, j)) + record["reduction_steps"] += 1 + if len(rows) + len(columns) >= len(best): + if matrix != IDENTITY: + record["length_cutoffs"] += 1 + break + if matrix != IDENTITY: + continue + record["completed"] += 1 + candidate = columns + rows[::-1] + require(transfer(candidate) == target, "search factorization mismatch") + if dominated(transfer(candidate[::-1]), reverse_limit): + record["successes"] += 1 + if len(candidate) < len(best): + best = candidate + record["improvements"].append( + {"trial_one_based": trial + 1, "operations": len(best)}) + records.append(record) + print(f"seed {seed}: {trials} trials; best {len(best)} operations", flush=True) + return best, records + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, default=Path(__file__).with_name("CANDIDATE.json")) + args = parser.parse_args() + registers, b_slice, original = extract() + candidate, records = search(original) + forward = transfer(original) + original_reverse = transfer(original[::-1]) + candidate_reverse = transfer(candidate[::-1]) + require(transfer(candidate) == forward, "candidate forward matrix mismatch") + require(dominated(candidate_reverse, original_reverse), "candidate reverse matrix exceeds source") + result = { + "format": "r420-positive-block-candidate-v1", + "base_commit": BASE_COMMIT, + "source": str(SOURCE.relative_to(ROOT)), + "source_sha256": SOURCE_SHA256, + "block_index": BLOCK, + "frame": FRAME, + "b_slice": b_slice, + "slice_convention": "zero-based, start inclusive, end exclusive", + "registers": registers, + "operations": candidate, + "seed": 801018, + "assignment_seed": 18, + "search_seed": 801018, + "seed_role": "assignment seed 18 selects block 8; search RNG uses 801018", + "search_seed_choice": "Manually fixed before the first search trial; arbitrary and distinct from assignment seed.", + "original_operations": original, + "original_count": len(original), + "candidate_count": len(candidate), + "forward_plus_cleanup_saving": 2 * (len(original) - len(candidate)), + "integer_forward_matrix": forward, + "original_positive_reverse_matrix": original_reverse, + "candidate_positive_reverse_matrix": candidate_reverse, + "search": { + "method": "seeded two-sided nonnegative elementary-factor reduction", + "trials": sum(r["trials"] for r in records), + "completed": sum(r["completed"] for r in records), + "successes": sum(r["successes"] for r in records), + "stages": records, + "move_order": "i then j; row before column; indices ascending", + "selection_cycle": [ + "uniform", "maximum gain plus uniform [0,3)", + "maximum gain times uniform [0,1)", "gain-squared weights", + "minimum gain plus uniform [0,3)", + "maximum square-root gain times uniform [0,1)"], + "cutoff": "stop a trial at current best length", + "complete_definition": "residual equals the ordered identity", + "success_definition": "complete and positive reverse matrix dominated", + "optimality_claim": False, + "excluded_exploration": { + "seed": 18, "requested_trials": 50000, + "completed_trial_count": None, + "status": "interrupted before completion; partial count was not retained", + "improvements_observed": 0, + "used_to_select_candidate": False, + }, + }, + "limitations": [ + "Only the pinned phase-B block 8 is searched.", + "No claim of minimum length or exhaustive coverage is made.", + "Search includes only nonnegative row and column subtraction paths with diagonal entries at least one.", + "Integer transfer checks are finite circuit checks, not a formal verification of the multiplication theorem.", + ], + } + destination = args.output + destination.write_text(json.dumps(result, indent=2) + "\n") + print(f"wrote {destination}; saves {result['forward_plus_cleanup_saving']} primitive operations") + + +if __name__ == "__main__": + main() diff --git a/research/r420-block8-schedule/verify.py b/research/r420-block8-schedule/verify.py new file mode 100644 index 0000000000..5e073dbcb3 --- /dev/null +++ b/research/r420-block8-schedule/verify.py @@ -0,0 +1,306 @@ +"""Exact replay of one R420 block replacement. Python standard library only. + +Jerry Lin, with substantial OpenAI Codex assistance; Apache-2.0. +The search is not imported. The original R420 checker is used separately for +the exact E8 geometry and its original H1-H5 interface. +""" +import argparse +import copy +from fractions import Fraction +import gzip +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path +import struct +import sys +from collections import Counter + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +SOURCE = ROOT / "research/e8-bit-r420/data/bitE8mut-r420.json.gz" +CHECKER = ROOT / "research/e8-bit-r420/code/xcheck.py" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def matrix(operations, n=12): + rows = [[int(i == j) for j in range(n)] for i in range(n)] + for dst, src in operations: + rows[dst] = [a + b for a, b in zip(rows[dst], rows[src])] + return rows + + +def dominated(smaller, larger): + return all(a <= b for x, y in zip(smaller, larger) for a, b in zip(x, y)) + + +def extract(word): + blocks = [] + for frame, items in itertools.groupby(enumerate(word["B"]), lambda x: x[1][0]): + items = list(items) + if len(word["frames"][frame]) == 12: + blocks.append((frame, items)) + require(len(blocks) == 10, "source block count") + frame, items = blocks[8] + start, end = items[0][0], items[-1][0] + 1 + registers = sorted({r for _, (_, dst, srcs) in items for r in [dst] + srcs}) + require((frame, start, end) == (550, 512, 559), "source block location") + require(len(registers) == 12 and all(r < word["v"] for r in registers), "source block wires") + require(all(len(g[2]) == 1 for _, g in items), "source block is not unary") + index = {r: i for i, r in enumerate(registers)} + operations = [[index[g[1]], index[g[2][0]]] for _, g in items] + return frame, start, end, registers, operations + + +def certify_block(word, recipe): + frame, start, end, registers, old = extract(word) + require(type(recipe["block_index"]) is int and recipe["block_index"] == 8, "block index") + require(recipe["frame"] == frame and recipe["b_slice"] == [start, end], "block binding") + require(recipe["registers"] == registers, "ordered register binding") + operations = recipe["operations"] + require(isinstance(operations, list) and 0 < len(operations) < len(old), "strict primitive saving") + for pair in operations: + require(isinstance(pair, list) and len(pair) == 2, "gate shape") + require(all(type(x) is int and 0 <= x < 12 for x in pair), "gate wire") + require(pair[0] != pair[1], "self addition") + forward = matrix(operations) + old_reverse, new_reverse = matrix(reversed(old)), matrix(reversed(operations)) + require(forward == matrix(old), "integer forward map") + require(dominated(new_reverse, old_reverse), "positive reverse domination") + return dict(old_gates=len(old), new_gates=len(operations), forward_matrix=forward, + old_positive_reverse=old_reverse, new_positive_reverse=new_reverse, + strict_reverse_entries=sum(a < b for x, y in zip(new_reverse, old_reverse) + for a, b in zip(x, y))) + + +def replace(word, recipe): + frame, start, end, registers, _ = extract(word) + result = copy.deepcopy(word) + result["B"][start:end] = [[frame, registers[d], [registers[s]]] for d, s in recipe["operations"]] + full = next(i for i, f in enumerate(word["frames"]) if len(f) == 120) + v = word["v"] + result["C"] = [[full, d, list(ss)] for _, d, ss in reversed(result["A"] + result["B"]) + if not v <= d < 2 * v] + return result + + +def rank(lines): + basis = {} + for row in lines: + row = list(map(Fraction, row)) + for p, old in sorted(basis.items()): + c = row[p] + row = [a - c * b for a, b in zip(row, old)] + pivot = next((i for i, x in enumerate(row) if x), None) + if pivot is not None: + scale = row[pivot] + basis[pivot] = [x / scale for x in row] + return len(basis) + + +def records(word, dimensions): + """Build the primitive stream independently of the predecessor exporter.""" + v, n = word["v"], 2 * word["v"] + word["R"] + current = list(word["start"]) + events = [] + paths = [[f] for f in current] + + def move(r, frame): + if current[r] != frame: + old = current[r] + require(set(word["frames"][old]) <= set(word["frames"][frame]), "frame nesting") + require(dimensions[old] < dimensions[frame], "strict frame growth") + events.append((0, r, old, frame, dimensions[frame] - dimensions[old], 0)) + paths[r].append(frame) + current[r] = frame + + def gates(section, phase): + for frame, dst, srcs in word[section]: + require(len({dst, *srcs}) == 1 + len(srcs), "duplicate gate operand") + for r in [dst] + srcs: + move(r, frame) + events.extend((1, dst, src, 1, frame, phase) for src in srcs) + + gates("D", 1) + gates("A", 2) + for k, center in enumerate(word["ret"]): + frame = current[center] + events.append((2, center, n, frame, 0, dimensions[frame])) + events.extend((1, v + t, n, 1, 0, 3) for t, row in enumerate(word["scatter"]) if k in row) + events.append((3, center, n, frame, 0, 0)) + gates("B", 4) + gates("C", 5) + for r, f in enumerate(word["final"]): + move(r, f) + return events, paths + + +def replay(word, events, reverse=False, positive=False): + v, n = word["v"], 2 * word["v"] + word["R"] + values = [1] * (n + 1) if positive else [1 << r for r in range(n)] + [0] + maximum, opened = 1, None + for op, a, b, _, _, _ in reversed(events) if reverse else events: + if op == 0: + continue + if reverse and op in (2, 3): + op = 5 - op + if op == 1: + require(a != n and (b != n or opened is not None), "copy lifecycle") + require(a != opened, "copied source changed") + values[a] = values[a] + values[b] if positive else values[a] ^ values[b] + maximum = max(maximum, values[a]) if positive else maximum + elif op == 2: + require(opened is None and b == n, "copy opening") + values[n], opened = values[a], a + else: + require(op == 3 and opened == a and b == n, "copy closing") + values[n], opened = 0, None + require(opened is None, "open copy at exit") + if positive: + return maximum + expected = [1 << r for r in range(n)] + [0] + for t in range(v): + expected[v + t] ^= 1 << t + require(values == expected, "all-column endpoint") + return n + + +def word_summary(word, dimensions): + events, paths = records(word, dimensions) + for reverse in (False, True): + replay(word, events, reverse) + forward = replay(word, events, positive=True) + backward = replay(word, events, reverse=True, positive=True) + histogram = Counter(e[4] for e in events if e[0] == 0) + histogram.update(e[5] for e in events if e[0] == 2) + payload = 64 * forward ** 3 * backward ** 2 + require(payload < 2 ** 104, "local payload cap") + return dict(columns=2 * word["v"] + word["R"], scalar_additions=sum(e[0] == 1 for e in events), + record_sha256=sha(b"".join(struct.pack("<6i", *event) for event in events)), + copies=sum(e[0] == 2 for e in events), erasures=sum(e[0] == 3 for e in events), + forward_positive_prefix=forward, reverse_positive_prefix=backward, + five_stage_payload_bits=payload.bit_length(), five_stage_payload=str(payload), + paid_histogram={str(k): v for k, v in sorted(histogram.items())}, + rank_mass=sum(k * v for k, v in histogram.items()), paths_sha256=sha(canonical(paths))), events, paths + + +def source_check(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for required in (SOURCE, CHECKER): + path = required.relative_to(ROOT).as_posix() + require(path in pins["files"], "missing source pin: " + path) + for path, digest in pins["files"].items(): + require(sha((ROOT / path).read_bytes()) == digest, "source hash: " + path) + + +def import_checker(): + spec = importlib.util.spec_from_file_location("r420_original_checker", CHECKER) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def reject(action, reason): + try: + action() + except ValueError as exc: + require(reason in str(exc), "wrong negative-control reason: " + str(exc)) + return + raise ValueError("negative control was accepted: " + reason) + + +def controls(word, recipe, candidate, dimensions, checker): + results = [] + shorter, longer = [(1, 2), (0, 1)], [(0, 1), (0, 2), (1, 2)] + require(matrix(shorter, 3) == matrix(longer, 3), "three-wire forward calibration") + reject(lambda: require(dominated(matrix(reversed(longer), 3), matrix(reversed(shorter), 3)), + "positive reverse domination"), "positive reverse domination") + results.append("equal_forward_does_not_imply_reverse_domination") + for label, edit, reason in ( + ("drop_operation", lambda r: r["operations"].pop(0), "integer forward map"), + ("self_addition", lambda r: r["operations"].__setitem__(0, [0, 0]), "self addition"), + ("boolean_wire", lambda r: r["operations"][0].__setitem__(0, True), "gate wire"), + ("wrong_frame", lambda r: r.__setitem__("frame", 549), "block binding"), + ("swapped_register_binding", lambda r: r["registers"].reverse(), "ordered register binding"), + ("unpriced_cancelled_pair", lambda r: r["operations"].extend([[0, 1], [0, 1]]), "integer forward map"), + ): + mutant = copy.deepcopy(recipe) + edit(mutant) + reject(lambda: certify_block(word, mutant), reason) + results.append(label) + mutant = copy.deepcopy(candidate) + mutant["C"].pop(158) + reject(lambda: word_summary(mutant, dimensions), "all-column endpoint") + results.append("missing_cleanup") + stale = copy.deepcopy(candidate) + stale["C"] = copy.deepcopy(word["C"]) + word_summary(stale, dimensions) # Both lists invert the same F2 map. + require(not checker.Word(stale).interface()[0]["H4_C_literal_reverse_at_full"], "stale cleanup H4 control") + results.append("stale_cleanup_passes_endpoint_but_fails_H4") + mutant = copy.deepcopy(candidate) + mutant["B"][512][0] = word["start"][mutant["B"][512][1]] + reject(lambda: records(mutant, dimensions), "frame nesting") + results.append("illegal_frame_descent") + return results + + +def verify(output=None): + source_check() + word = json.loads(gzip.decompress(SOURCE.read_bytes())) + recipe = json.loads((HERE / "CANDIDATE.json").read_text()) + block = certify_block(word, recipe) + candidate = replace(word, recipe) + dimensions = [rank([word["lines"][i] for i in frame]) for frame in word["frames"]] + before, _, old_paths = word_summary(word, dimensions) + after, _, new_paths = word_summary(candidate, dimensions) + require(old_paths == new_paths, "changed frame paths") + require(before["paid_histogram"] == after["paid_histogram"], "changed paid profile") + require(before["scalar_additions"] - after["scalar_additions"] == 2 * (block["old_gates"] - block["new_gates"]), + "complete primitive saving") + require(after["forward_positive_prefix"] <= before["forward_positive_prefix"] and + after["reverse_positive_prefix"] <= before["reverse_positive_prefix"], "complete positive prefixes") + checker = import_checker() + original_check = checker.check(word) + require(original_check[0].fdim == dimensions, "independent frame ranks") + require(all(original_check[3].values()) and all(original_check[4].values()), "original interface") + changed = checker.Word(candidate) + changed.full() + hypotheses, conclusions, _ = changed.interface() + require(all(hypotheses.values()) and all(conclusions.values()), "candidate interface") + report = dict(block=block, original=before, candidate=after, + word_content_sha256=sha(canonical(candidate)), + controls=controls(word, recipe, candidate, dimensions, checker)) + expected = json.loads((HERE / "CERTIFICATE.json").read_text()) + require(report == expected, "certificate mismatch") + if output: + with gzip.GzipFile(filename=str(output), mode="wb", mtime=0) as stream: + stream.write(canonical(candidate)) + print("PASS_R420_BLOCK8_SCHEDULE gates=%d->%d ADDs=%d->%d columns=660 controls=%d rank_mass=%d kappa=not_recomputed" % + (block["old_gates"], block["new_gates"], before["scalar_additions"], after["scalar_additions"], + len(report["controls"]), after["rank_mass"])) + return report + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output-word", type=Path, help="Write the rebuilt word to a new file.") + args = parser.parse_args() + if args.output_word: + require(not args.output_word.exists(), "output file already exists") + require(HERE not in args.output_word.resolve().parents and SOURCE.parent not in args.output_word.resolve().parents, + "output must be outside source packages") + verify(args.output_word)