From b0388fc54f68087603b253465c1c35bb5e364531 Mon Sep 17 00:00:00 2001 From: Hao Yan Date: Tue, 13 Oct 2026 14:20:36 +0800 Subject: [PATCH 1/2] Research: shorten historical R480 quad 1 with exact dirty-input replay Prepared for Hao Yan (@FanPUYen) with substantial OpenAI Codex assistance. Finite construction only; no new kappa. --- research/r480-quad-seed1/CLAIM.json | 17 + research/r480-quad-seed1/EXPECTED.json | 89 +++++ research/r480-quad-seed1/NATIVE-EXPECTED.json | 228 +++++++++++++ .../r480-quad-seed1/NATIVE-VALIDATION.json | 208 ++++++++++++ research/r480-quad-seed1/README.md | 217 +++++++++++++ research/r480-quad-seed1/SOURCES.json | 40 +++ research/r480-quad-seed1/VALIDATION.json | 124 +++++++ research/r480-quad-seed1/discover.py | 175 ++++++++++ research/r480-quad-seed1/independent_check.py | 304 ++++++++++++++++++ research/r480-quad-seed1/native_replay.py | 228 +++++++++++++ research/r480-quad-seed1/recipe.json | 293 +++++++++++++++++ research/r480-quad-seed1/verify.py | 298 +++++++++++++++++ 12 files changed, 2221 insertions(+) create mode 100644 research/r480-quad-seed1/CLAIM.json create mode 100644 research/r480-quad-seed1/EXPECTED.json create mode 100644 research/r480-quad-seed1/NATIVE-EXPECTED.json create mode 100644 research/r480-quad-seed1/NATIVE-VALIDATION.json create mode 100644 research/r480-quad-seed1/README.md create mode 100644 research/r480-quad-seed1/SOURCES.json create mode 100644 research/r480-quad-seed1/VALIDATION.json create mode 100644 research/r480-quad-seed1/discover.py create mode 100644 research/r480-quad-seed1/independent_check.py create mode 100644 research/r480-quad-seed1/native_replay.py create mode 100644 research/r480-quad-seed1/recipe.json create mode 100644 research/r480-quad-seed1/verify.py diff --git a/research/r480-quad-seed1/CLAIM.json b/research/r480-quad-seed1/CLAIM.json new file mode 100644 index 0000000000..e084968d94 --- /dev/null +++ b/research/r480-quad-seed1/CLAIM.json @@ -0,0 +1,17 @@ +{ + "track": "bit supplier", + "assignment_seed": 1, + "seed_source": "Python secrets.randbelow(100), operating-system randomness", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "started_utc": "2026-10-13T06:01:47Z", + "expected_finish": "2026-10-13T14:42:00+08:00", + "verification_reserved_from": "2026-10-13T14:32:00+08:00", + "object": "PR503/PR510 historical R480 phase-A quad circuits, starting at quad index 1", + "method": "Bounded exact positive-integer row-subtraction resynthesis, preserving each full dirty-input transfer matrix and requiring entrywise nonincrease of the reverse nonnegative transfer; same wires and frame, literal reverse cleanup.", + "domain": "At most the 60 phase-A quad blocks, cyclic order starting with seed modulo 60; stop at first certified strict improvement or time budget.", + "expected_deliverable": "One finite circuit construction or scoped negative search receipt with exact replay, source pins and rejection controls; no kappa claim.", + "alternatives_considered": ["R489 cleanup synthesis", "R420 block factorization"], + "selection_reason": "R420 is heavily covered by current PRs. Searches for R480 and quad identify historical boundary verification but no R480 quad resynthesis.", + "coordination": "Open-issue and sprint searches found only issue 650 (discussion request), no pinned sprint coordination issue. Local claim used; no reservation issue created.", + "overlap_context": [503,510,691,754,789,790,810] +} diff --git a/research/r480-quad-seed1/EXPECTED.json b/research/r480-quad-seed1/EXPECTED.json new file mode 100644 index 0000000000..2ead01e1fa --- /dev/null +++ b/research/r480-quad-seed1/EXPECTED.json @@ -0,0 +1,89 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "baseline": { + "cost": { + "paid_histogram": { + "1": 1200, + "2": 1440, + "4": 180, + "6": 120, + "8": 9 + }, + "rank_mass": 5592, + "total_xors": 33958, + "xor_by_phase": { + "A": 3246, + "B": 600, + "C": 3246, + "D": 26298, + "scatter": 568 + } + }, + "scalar": { + "columns": 720, + "raw_norm_sha256": "9e7d4add1470f34ce42df44fc735d08eab1259ab07d52fbb2af42c04905070d1", + "unsigned_raw_peak": 176135 + } + }, + "candidate": { + "cost": { + "paid_histogram": { + "1": 1200, + "2": 1440, + "4": 180, + "6": 120, + "8": 9 + }, + "rank_mass": 5592, + "total_xors": 33946, + "xor_by_phase": { + "A": 3240, + "B": 600, + "C": 3240, + "D": 26298, + "scatter": 568 + } + }, + "scalar": { + "columns": 720, + "raw_norm_sha256": "1ffb4b096c8adb690c0cda1d8d331d83cc1ca92a7ff52c6d64802ed32cc7542a", + "unsigned_raw_peak": 176135 + } + }, + "candidate_content_sha256": "16f8f177f622a507b0f817df3e7b1e49212d3a3e0cb92348ef24e790e890712f", + "frame_paths_sha256": "2b384919c4b79258e608ceac2f71a9fa44d47d1b9e65c8fb55413de0388fd71a", + "negative_controls": [ + "omit_quad_gate_0", + "omit_quad_gate_1", + "omit_quad_gate_2", + "omit_quad_gate_3", + "omit_quad_gate_4", + "omit_quad_gate_5", + "omit_quad_gate_6", + "omit_quad_gate_7", + "omit_quad_gate_8", + "omit_quad_gate_9", + "omit_quad_gate_10", + "omit_quad_gate_11", + "reverse_gate_order", + "boolean_as_integer", + "false_reverse_certificate", + "missing_cleanup_structure", + "missing_cleanup_dirt", + "missing_dirty_compensation", + "frame_zero_substitution", + "missing_scatter_read" + ], + "quad": { + "frame": 303, + "index": 1, + "new_gates": 12, + "old_gates": 18, + "rational_rank": 4, + "reverse_strict_entries": 13 + }, + "recipe_sha256": "76fb68793429a724335cfb8ec99fc6969a804bce5d1313ba2bef6a07cd96ba35", + "scope": "Finite circuit construction; unchanged paid profile; no new kappa or all-size proof.", + "source_word_sha256": "92e399e9a486b55229b5624632ac54f800dd9e022f2aee97f1e5f264bbc0ef5c", + "status": "PASS_R480_QUAD_SEED1" +} diff --git a/research/r480-quad-seed1/NATIVE-EXPECTED.json b/research/r480-quad-seed1/NATIVE-EXPECTED.json new file mode 100644 index 0000000000..8de89aafdf --- /dev/null +++ b/research/r480-quad-seed1/NATIVE-EXPECTED.json @@ -0,0 +1,228 @@ +{ + "baseline": { + "gram_frames": 672, + "gram_prime_witnesses": [ + 2 + ], + "interface": { + "cleanup_gates": 2708, + "cleanup_source_gates": 577, + "phase_B_reads_of_sources": 120, + "source_destination_gates_A": 577, + "source_write_frame_dims": { + "4": 577 + }, + "sources_rewritten": 117, + "status": "PASS_PR425_INTERFACE_HYPOTHESES" + }, + "legality": { + "common_frame_ADDs": 33958, + "copies": 9, + "erasures": 9, + "nested_MOVEs": 2940, + "paid_histogram": [ + [ + 1, + 1200 + ], + [ + 2, + 1440 + ], + [ + 4, + 180 + ], + [ + 6, + 120 + ], + [ + 8, + 9 + ] + ], + "rank_mass": 5592, + "records": 36916 + }, + "local_columns": 720, + "local_invoice": { + "local_raw_H": [ + [ + 1, + 1200 + ], + [ + 2, + 1440 + ], + [ + 4, + 180 + ], + [ + 6, + 120 + ], + [ + 8, + 9 + ] + ], + "local_scalar_additions": 33958, + "payload_prefix_bits": 102, + "payload_prefix_upper": "4921056267806722187755121024000", + "signed_lift_prefix": [ + { + "bits": 18, + "cancellation_free_signed_row_l1_upper": "176135", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "3751204", + "reverse": true + } + ] + }, + "negative_controls": { + "interface": 2, + "record_generic": 6, + "record_mutable_source": 3, + "word_generic": 6, + "word_mutable_source": 5 + }, + "stages": { + "eleven": { + "bridge_additions": 2880, + "formal_columns_checked": 1680, + "omitted_bridge_controls_rejected": 24 + }, + "five": { + "bridge_additions": 720, + "formal_columns_checked": 960, + "omitted_bridge_controls_rejected": 6 + }, + "nine": { + "bridge_additions": 2160, + "formal_columns_checked": 1440, + "omitted_bridge_controls_rejected": 18 + } + }, + "word_content_sha256": "8639e22008c24a5690dd250eba702fe5fca85ddd036dcbec20baba77b7e213ba" + }, + "candidate": { + "gram_frames": 672, + "gram_prime_witnesses": [ + 2 + ], + "interface": { + "cleanup_gates": 2702, + "cleanup_source_gates": 577, + "phase_B_reads_of_sources": 120, + "source_destination_gates_A": 577, + "source_write_frame_dims": { + "4": 577 + }, + "sources_rewritten": 117, + "status": "PASS_PR425_INTERFACE_HYPOTHESES" + }, + "legality": { + "common_frame_ADDs": 33946, + "copies": 9, + "erasures": 9, + "nested_MOVEs": 2940, + "paid_histogram": [ + [ + 1, + 1200 + ], + [ + 2, + 1440 + ], + [ + 4, + 180 + ], + [ + 6, + 120 + ], + [ + 8, + 9 + ] + ], + "rank_mass": 5592, + "records": 36904 + }, + "local_columns": 720, + "local_invoice": { + "local_raw_H": [ + [ + 1, + 1200 + ], + [ + 2, + 1440 + ], + [ + 4, + 180 + ], + [ + 6, + 120 + ], + [ + 8, + 9 + ] + ], + "local_scalar_additions": 33946, + "payload_prefix_bits": 102, + "payload_prefix_upper": "4920888351098140423688534400000", + "signed_lift_prefix": [ + { + "bits": 18, + "cancellation_free_signed_row_l1_upper": "176135", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "3751140", + "reverse": true + } + ] + }, + "negative_controls": { + "interface": 2, + "record_generic": 6, + "record_mutable_source": 3, + "word_generic": 6, + "word_mutable_source": 5 + }, + "stages": { + "eleven": { + "bridge_additions": 2880, + "formal_columns_checked": 1680, + "omitted_bridge_controls_rejected": 24 + }, + "five": { + "bridge_additions": 720, + "formal_columns_checked": 960, + "omitted_bridge_controls_rejected": 6 + }, + "nine": { + "bridge_additions": 2160, + "formal_columns_checked": 1440, + "omitted_bridge_controls_rejected": 18 + } + }, + "word_content_sha256": "16f8f177f622a507b0f817df3e7b1e49212d3a3e0cb92348ef24e790e890712f" + }, + "inherited_manifest_sha256": "7f25c41d0400ef5adf763eae6e166003a9b59e5a655b860c04b052f6731c7297", + "status": "PASS_R480_QUAD_SEED1_NATIVE_LOCAL_REPLAY" +} diff --git a/research/r480-quad-seed1/NATIVE-VALIDATION.json b/research/r480-quad-seed1/NATIVE-VALIDATION.json new file mode 100644 index 0000000000..ad34343d22 --- /dev/null +++ b/research/r480-quad-seed1/NATIVE-VALIDATION.json @@ -0,0 +1,208 @@ +{ + "boost_archive_sha256": "1bed88e40401b2cb7a1f76d4bab499e352fa4d0c5f31c0dbae64e24d34d7513b", + "boost_archive_url": "https://archives.boost.io/release/1.86.0/source/boost_1_86_0.tar.bz2", + "boost_version": "1_86", + "boost_version_header_sha256": "65cc1b27e846afe00c2a8aeccd4fdc849d298a7d2fe0609a4afca489f91129f5", + "candidate_content_sha256": "16f8f177f622a507b0f817df3e7b1e49212d3a3e0cb92348ef24e790e890712f", + "commands": [ + { + "command": "{python} -I -B {repo}/research/r480-quad-seed1/verify.py --out {work}/constructed", + "exit_code": 0, + "name": "primary-verifier" + }, + { + "command": "c++ -O2 -std=c++17 -DHDIM=8 -DNCOPY=9 -I{repo}/research/e8-bit-carrier-skeleton/portable-include -I{repo}/research/e8-bit-carrier-skeleton/code/bit/checkers -I{boost_include} -o {work}/bin/legality {repo}/research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp", + "exit_code": 0, + "name": "compile-legality" + }, + { + "command": "c++ -O2 -std=c++17 -DHDIM=8 -I{repo}/research/e8-bit-carrier-skeleton/portable-include -I{repo}/research/e8-bit-carrier-skeleton/code/bit/checkers -I{boost_include} -o {work}/bin/legality_ncopy_h {repo}/research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp", + "exit_code": 0, + "name": "compile-legality_ncopy_h" + }, + { + "command": "c++ -O2 -std=c++17 -DHDIM=8 -DNCOPY=9 -DVPORTS=120 -DRHELP=480 -I{repo}/research/e8-bit-carrier-skeleton/portable-include -I{repo}/research/e8-bit-carrier-skeleton/code/bit/checkers -I{boost_include} -o {work}/bin/columns_h {repo}/research/e8-bit-carrier-skeleton/code/bit/checkers/columns_h.cpp", + "exit_code": 0, + "name": "compile-columns_h" + }, + { + "command": "c++ -O2 -std=c++17 -DHDIM=8 -DNCOPY=9 -DVPORTS=120 -DRHELP=480 -DKPAIRS=2 -I{repo}/research/e8-bit-carrier-skeleton/portable-include -I{repo}/research/e8-bit-carrier-skeleton/code/bit/checkers -I{boost_include} -o {work}/bin/columns_k2 {repo}/research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp", + "exit_code": 0, + "name": "compile-columns_k2" + }, + { + "command": "c++ -O2 -std=c++17 -DHDIM=8 -DNCOPY=9 -DVPORTS=120 -DRHELP=480 -DKPAIRS=4 -I{repo}/research/e8-bit-carrier-skeleton/portable-include -I{repo}/research/e8-bit-carrier-skeleton/code/bit/checkers -I{boost_include} -o {work}/bin/columns_k4 {repo}/research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp", + "exit_code": 0, + "name": "compile-columns_k4" + }, + { + "command": "c++ -O2 -std=c++17 -DHDIM=8 -DNCOPY=9 -DVPORTS=120 -DRHELP=480 -DKPAIRS=5 -I{repo}/research/e8-bit-carrier-skeleton/portable-include -I{repo}/research/e8-bit-carrier-skeleton/code/bit/checkers -I{boost_include} -o {work}/bin/columns_k5 {repo}/research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp", + "exit_code": 0, + "name": "compile-columns_k5" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/independent/relax.py {work}/baseline/rchk", + "exit_code": 0, + "name": "baseline-relax" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/independent/checkword.py {repo}/research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz {repo}/research/e8-bit-carrier-skeleton/code/pricing", + "exit_code": 1, + "name": "baseline-stock-refusal" + }, + { + "command": "{python} -I -B {work}/baseline/rchk/checkword_mut.py {repo}/research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz {repo}/research/e8-bit-carrier-skeleton/code/pricing", + "exit_code": 0, + "name": "baseline-all720" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/independent/interface.py {repo}/research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz --json {work}/baseline/interface.json", + "exit_code": 0, + "name": "baseline-interface" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/independent/mutate_mut.py {repo}/research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz {work}/baseline/rchk/checkword_mut.py {repo}/research/e8-bit-carrier-skeleton/code/pricing {repo}/research/e8-bit-carrier-skeleton/code/bit/independent/interface.py", + "exit_code": 0, + "name": "baseline-word-controls" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/export_records.py {repo}/research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz {work}/baseline/records", + "exit_code": 0, + "name": "baseline-export" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py {work}/baseline/records {work}/baseline/records {work}/baseline/cin {work}/baseline/cout", + "exit_code": 0, + "name": "baseline-cohort" + }, + { + "command": "{work}/bin/legality {work}/baseline/cin {work}/baseline/cout {work}/baseline/cout/legality.json", + "exit_code": 0, + "name": "baseline-legality" + }, + { + "command": "{work}/bin/columns_h {work}/baseline/cout/COHORT249-RECORDS.bin {work}/baseline/cout/columns_h.json", + "exit_code": 0, + "name": "baseline-columns_h" + }, + { + "command": "{work}/bin/columns_k2 {work}/baseline/cout/COHORT249-RECORDS.bin {work}/baseline/cout/columns_k2.json", + "exit_code": 0, + "name": "baseline-columns_k2" + }, + { + "command": "{work}/bin/columns_k4 {work}/baseline/cout/COHORT249-RECORDS.bin {work}/baseline/cout/columns_k4.json", + "exit_code": 0, + "name": "baseline-columns_k4" + }, + { + "command": "{work}/bin/columns_k5 {work}/baseline/cout/COHORT249-RECORDS.bin {work}/baseline/cout/columns_k5.json", + "exit_code": 0, + "name": "baseline-columns_k5" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/mutate_records.py {work}/baseline/records {work}/baseline/cin {work}/baseline/cout {work}/bin/legality {work}/bin/columns_k5 {work}/bin/legality_ncopy_h", + "exit_code": 0, + "name": "baseline-record-controls" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/mutate_records_mut.py {repo}/research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz {work}/baseline/records {work}/baseline/cin {work}/baseline/cout {work}/bin/legality {work}/bin/columns_h {work}/bin/columns_k5", + "exit_code": 0, + "name": "baseline-source-record-controls" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/checkers/gram_frames.py {work}/baseline/records --gram e8ham --h 8 --positive", + "exit_code": 0, + "name": "baseline-gram" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/independent/relax.py {work}/candidate/rchk", + "exit_code": 0, + "name": "candidate-relax" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/independent/checkword.py {work}/constructed/word.json.gz {repo}/research/e8-bit-carrier-skeleton/code/pricing", + "exit_code": 1, + "name": "candidate-stock-refusal" + }, + { + "command": "{python} -I -B {work}/candidate/rchk/checkword_mut.py {work}/constructed/word.json.gz {repo}/research/e8-bit-carrier-skeleton/code/pricing", + "exit_code": 0, + "name": "candidate-all720" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/independent/interface.py {work}/constructed/word.json.gz --json {work}/candidate/interface.json", + "exit_code": 0, + "name": "candidate-interface" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/independent/mutate_mut.py {work}/constructed/word.json.gz {work}/candidate/rchk/checkword_mut.py {repo}/research/e8-bit-carrier-skeleton/code/pricing {repo}/research/e8-bit-carrier-skeleton/code/bit/independent/interface.py", + "exit_code": 0, + "name": "candidate-word-controls" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/export_records.py {work}/constructed/word.json.gz {work}/candidate/records", + "exit_code": 0, + "name": "candidate-export" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py {work}/candidate/records {work}/candidate/records {work}/candidate/cin {work}/candidate/cout", + "exit_code": 0, + "name": "candidate-cohort" + }, + { + "command": "{work}/bin/legality {work}/candidate/cin {work}/candidate/cout {work}/candidate/cout/legality.json", + "exit_code": 0, + "name": "candidate-legality" + }, + { + "command": "{work}/bin/columns_h {work}/candidate/cout/COHORT249-RECORDS.bin {work}/candidate/cout/columns_h.json", + "exit_code": 0, + "name": "candidate-columns_h" + }, + { + "command": "{work}/bin/columns_k2 {work}/candidate/cout/COHORT249-RECORDS.bin {work}/candidate/cout/columns_k2.json", + "exit_code": 0, + "name": "candidate-columns_k2" + }, + { + "command": "{work}/bin/columns_k4 {work}/candidate/cout/COHORT249-RECORDS.bin {work}/candidate/cout/columns_k4.json", + "exit_code": 0, + "name": "candidate-columns_k4" + }, + { + "command": "{work}/bin/columns_k5 {work}/candidate/cout/COHORT249-RECORDS.bin {work}/candidate/cout/columns_k5.json", + "exit_code": 0, + "name": "candidate-columns_k5" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/mutate_records.py {work}/candidate/records {work}/candidate/cin {work}/candidate/cout {work}/bin/legality {work}/bin/columns_k5 {work}/bin/legality_ncopy_h", + "exit_code": 0, + "name": "candidate-record-controls" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/mutate_records_mut.py {work}/constructed/word.json.gz {work}/candidate/records {work}/candidate/cin {work}/candidate/cout {work}/bin/legality {work}/bin/columns_h {work}/bin/columns_k5", + "exit_code": 0, + "name": "candidate-source-record-controls" + }, + { + "command": "{python} -I -B {repo}/research/e8-bit-carrier-skeleton/code/bit/checkers/gram_frames.py {work}/candidate/records --gram e8ham --h 8 --positive", + "exit_code": 0, + "name": "candidate-gram" + }, + { + "command": "c++ --version", + "exit_code": 0, + "name": "compiler-version" + } + ], + "compiler": "Apple clang version 21.0.0 (clang-2100.1.1.101)\nTarget: arm64-apple-darwin25.5.0\nThread model: posix\nInstalledDir: /Library/Developer/CommandLineTools/usr/bin", + "inherited_manifest_sha256": "7f25c41d0400ef5adf763eae6e166003a9b59e5a655b860c04b052f6731c7297", + "native_driver_sha256": "5aeccaf96c5d622a607aa5aef63c183c20921845729acb6b317b489dd1f3354c", + "native_expected_sha256": "2b91efc5b2ffad0ebc3a828c8aa4b5949835ffcf35f57ed83823f029e1138c44", + "post_run_semantic_extractor_check": "PASS: final semantic_case results equal NATIVE-EXPECTED.json for both completed native runs. Command path normalization subsequently corrected to use {python}.", + "python": "3.12.14", + "scope": "Local finite/native replay only; no global hosting replay or exponent improvement.", + "source_word_sha256": "92e399e9a486b55229b5624632ac54f800dd9e022f2aee97f1e5f264bbc0ef5c", + "status": "PASS_R480_QUAD_SEED1_NATIVE_LOCAL_REPLAY" +} diff --git a/research/r480-quad-seed1/README.md b/research/r480-quad-seed1/README.md new file mode 100644 index 0000000000..4feb255724 --- /dev/null +++ b/research/r480-quad-seed1/README.md @@ -0,0 +1,217 @@ +# R480 quad 1: twelve fewer scalar XORs, no new κ + +**Finite bit-circuit construction.** The historical #503/#510 R480 word's +quad 1 changes from 18 to 12 XORs, with six further XORs removed from its +literal reverse cleanup. Complete local scalar work is **33,958 → 33,946**. +Every one of the 720 register frame paths, all 480 dirty helpers, nine copied +totals, and the paid recursive histogram are unchanged. This is a small +constant-cost improvement to a historical supplier, not a new selected bound. + +Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +The selected record on that base is #626/#543, with +κ = `51110230636731/31250000000000000`. It is not changed here. +[SOURCES.json](SOURCES.json) pins the actual inputs and predecessor heads; +[CLAIM.json](CLAIM.json) records assignment seed **1**, candidate selection +and the local sprint claim. No coordination issue was found. + +During submission refresh, main advanced to +`7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261`: the selected result became +#741/#589, κ = `1661202643272239/1000000000000000000`. Its new selected +record and maintainer review were read. All eight consumed input files and +the inherited checker package remain unchanged. This contribution still +targets the historical R480 circuit. The old selected-record hash is retained +as dated context, not imposed as a replay dependency on today's mutable pointer. + +## Reproduce + +Python 3.9+ and the standard library suffice for the primary certificate: + +```sh +python3 -I -B research/r480-quad-seed1/verify.py --out /tmp/r480-quad-seed1 +``` + +Expected final line: + +```text +PASS_R480_QUAD_SEED1 quad=1 XORs=33958->33946 saved=12 columns=720 controls=20 kappa=unchanged +``` + +The command compares all evidence with [EXPECTED.json](EXPECTED.json), and +writes the complete candidate word and receipt to the requested directory. +It imports no producer or inherited checker code. Normal and optimized +Python both enforce its checks. + +Independent set-valued replay and exact rational frame checks: + +```sh +python3 -I -B research/r480-quad-seed1/independent_check.py \ + --word /tmp/r480-quad-seed1/word.json.gz +``` + +Expected JSON status: `PASS_INDEPENDENT_SET_VALUED_DIRTY_INPUT_REPLAY`; +720 columns and 16 rejected controls. The implementation uses support sets, +not the primary verifier's packed bit masks. + +To reproduce the single completed synthesis attempt: + +```sh +python3 -I -B research/r480-quad-seed1/discover.py --output /tmp/r480-recipe.json +cmp /tmp/r480-recipe.json research/r480-quad-seed1/recipe.json +``` + +There is no solver or network dependency. Discovery started at quad +`seed % 60 = 1` and stopped at the first strict improvement, attempt 0. +Only one attempt on that quad was completed; no other quad was searched. +The original budget allowed up to 60 quads in cyclic order. The replay +deliberately repeats only the completed attempt, with at most 17 subtraction +steps. This is a witness, not an optimality or impossibility claim. + +Optional native replay needs a C++17 compiler and Boost headers. It reuses +the unchanged, manifest-pinned predecessor checker chain: + +```sh +BOOST_INCLUDE=/path/to/boost python3 -B research/r480-quad-seed1/native_replay.py \ + --work /tmp/r480-native-replay +``` + +The driver rejects optimized Python because the inherited checkers use +assertions. [NATIVE-EXPECTED.json](NATIVE-EXPECTED.json) contains the compact +semantic receipt. Gzip container bytes are not used to compare regenerated +words: canonical decompressed JSON is checked. + +## Exact change and proof + +The source is `research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz`. +Replace the zero-based half-open slice `A[621:639]`, frame 303 (rational rank +four). The ordered wires are `[487, 504, 550, 574, 598, 622]`; all are existing +helpers. In local wire indices, the new ordered pairs `(destination, source)` +are: + +```text +(2,5) (3,4) (0,1) (0,3) (0,5) (2,3) +(5,2) (3,2) (1,2) (4,0) (5,4) (3,0) +``` + +Each pair is one XOR, with both operands at frame 303. No temporary register, +source-access operation, preparation or unpriced restoration is added. +`C` is regenerated as the literal reverse of `A` at FULL; `B` writes targets +only. All other fields are byte-for-byte equal as JSON data, including the +dirty compensation `D`, retained totals, scatter, and all initial/final frames. + +Replacing XOR by ordinary positive integer addition, both old and new +forward blocks have the complete transfer matrix + +```text +1 1 0 1 1 1 +0 1 1 1 1 1 +0 0 1 1 1 1 +1 1 1 3 3 2 +1 1 0 1 2 1 +1 1 1 2 3 3 +``` + +Thus the maps agree over F₂ on six arbitrary independent inputs, including +all dirty contributions. This is stronger than checking only the source +components present at this particular circuit location. The unchanged rest +of `A/scatter/B` consequently has the same complete scalar action. Each XOR +is an involution over F₂, so the regenerated literal `C` restores every +source/helper. `D` remains exactly the same correction. The full word still +maps `(x,s,y)` to `(x,s,y+x)`; both fresh implementations check all 720 columns. +Literal positive-addition cleanup is **not** asserted to be an inverse over +the integers: the inverse statement here is over F₂. The native signed +inverse checks use their original coefficient-sign convention. + +For cancellation-free bounds, the reversed positive transfer matrices in +[recipe.json](recipe.json) satisfy `N_new <= N_old` entrywise, with 13 strict +entries. Their row sums are respectively `[9,2,7,5,2,3]` and +`[39,26,13,5,2,5]`. The forward positive matrix is equal. All intermediate +bounds in either replacement block only increase, so each is bounded by +that block's endpoint. At corresponding endpoints the new nonnegative +bound is equal or smaller. Multiplying by the unchanged nonnegative maps +before/after the blocks preserves this order. This proves nonincrease of +the maximum-norm bound, including the reverse word; it does not assume that +fewer gates alone imply a smaller bound. Native replay checks the actual +COPY/erase and stage conventions separately. + +Each of the six wires is touched at the same frame, and the preceding and +following frame visits are unchanged. Therefore each full frame path is +unchanged. Exact rational nesting is independently checked. No altered +delivery model, helper lifetime or boundary interface is introduced. + +## Complete accounting and scope + +| Scalar XOR terms | Original | Candidate | +|---|---:|---:| +| Dirty compensation D | 26,298 | 26,298 | +| A, including all source reads | 3,246 | 3,240 | +| Scatter | 568 | 568 | +| B | 600 | 600 | +| Complete literal cleanup C | 3,246 | 3,240 | +| Total | 33,958 | 33,946 | + +The complete local paid profile remains +`H={1:1200, 2:1440, 4:180, 6:120, 8:9}`, rank mass 5,592. +The last term charges all nine full-rank copied totals. Native replay also +checks their nine erasures. No recursive child is removed. The native +record count is 36,916 → 36,904, with all 2,940 MOVEs unchanged. + +In the inherited nine-stage/32-replica layout there are 288 local calls. +The scalar delta would therefore be 3,456 additions in the corresponding +emitted program. This is an accounting consequence, **not a freshly emitted +or hosted global receipt**. Under exactly the old ownership/interface +assumptions, the recursive recurrence is unchanged: its complete historical +profile is +`P={1:345600,2:430080,4:67200,6:49920,7:23040,8:2592}`, with `m=64`, +`W=30720`. This profile includes the idle work. The inherited moment test is + +```text +M(c) = sum_r [r P_r / (m W)] (m/r)^c + + [32 m sum_r P_r / (10^16 W)] m^c. +``` + +Every term, including the bad-branch allowance, is unchanged. The reduced +scalar work affects only a finite overhead constant, so this package claims +neither a higher bit saving nor a higher κ. These historical global numbers +are source-pinned context, not a newly checked global invoice. The selected +#543 word at the original base and the new #741/#589 suppliers are not +replaced or reassembled. + +Native finite checks pass for both words: 960 five-stage, 1,440 nine-stage, +and 1,680 eleven-stage columns, with 6/18/24 omitted-bridge controls. +Forward prefix is unchanged at 176,135; reverse prefix decreases from +3,751,204 to 3,751,140. Both payload bounds occupy 102 bits, below the +inherited 104-bit limit. The detailed validation and failed repository-wide +check are recorded in [VALIDATION.json](VALIDATION.json). + +Remaining obligations are the inherited all-size compiler, common-label and +mutable-basis realization, whole-call correlated-helper hosting, normalized +residuals, compressed windows/restored work, common grid, precision/tape, +exact recovery and analytic transfer. Full global hosting, the 47 outer +inequalities, remote CI and Lean were not replayed here. Finite certificates +are not a formal proof of the multiplication theorem or a practical-runtime +speedup measurement. + +## Provenance and overlap + +DreamingOfClouds supplied #503's R480 adaptation and #510's nine-stage +pipeline; eumemic supplied #493's carrier skeleton, generator, mutable-source +checks and frozen plan. Retain their [#503 notice](../e8-r480-dead-totals/NOTICE.md) +and [#493 notice](../e8-bit-carrier-skeleton/NOTICE.md), including Zhihao Chen +(#425/#386), Dylan Crow (#370), DaysSky (#442/#381), chafreaky +(#445/#451/#472/#458), icekylinx, Dugongue, Jacob Sussman and the cumulative +lineage. All original bytes and notices remain unchanged. + +@mtpsl’s pending [#691](https://github.com/CrocSwap/integer-mult-bounds/pull/691) +uses the related positive-integer/reverse-domination criterion for **R420 +quad 13**. This package independently instantiates that criterion on **R480 +quad 1**, with a distinct source, dirty-input map, circuit and receipt. +[#754](https://github.com/CrocSwap/integer-mult-bounds/pull/754) synthesizes +R420 cleanup windows; #789/#790/#810 change R420 phase-B blocks. No pending +implementation is imported or combined here. The ledger marks #503/#510 +incorporated and the base-selected #543 bit supplier incorporated; +unreviewed PR titles do not change the selected frontier. + +Prepared for **Hao Yan (@FanPUYen)** with substantial **OpenAI Codex** +assistance in synthesis, implementation, independent checking and writing. +The separate implementations were produced by cooperating AI workers; +no independent human peer review is claimed. New work is Apache-2.0. diff --git a/research/r480-quad-seed1/SOURCES.json b/research/r480-quad-seed1/SOURCES.json new file mode 100644 index 0000000000..1f58fbd44f --- /dev/null +++ b/research/r480-quad-seed1/SOURCES.json @@ -0,0 +1,40 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "base_selected_record_context": { + "kappa": "51110230636731/31250000000000000", + "path": "certificates/selected-result.json", + "scope": "Historical context at base only; not a circuit input or a binding on future selected records.", + "sha256": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53" + }, + "dependency_heads": { + "493": "c3a9a436b84fe44fdc223a5784d84736d1c2d3c7", + "503": "3f27147013fdd4fa0aed825cb47bff3376c452eb", + "510": "64edee18af02aab0c1696b677a0287dd0146381b" + }, + "files": { + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + "research/e8-bit-carrier-skeleton/code/skeleton/gen.py": "7cdcf48078ed4beacd2e240aa8145e4aa6984558748d07659cb1b252786e073a", + "research/e8-r480-dead-totals/NOTICE.md": "90e0b76e6f7c15bda8d854ec5bc6e07e4553ec1f73c86b17c35bd77b0abc4438", + "research/e8-r480-dead-totals/README.md": "8a2c494ffe729b903a87548a4ac68a56ceb81d45e4f786985f18c1091897fe2f", + "research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz": "92e399e9a486b55229b5624632ac54f800dd9e022f2aee97f1e5f264bbc0ef5c", + "research/e8-r480-nine-stage/EXPECTED.json": "883f7a1a84f31d9e4430e348bc8d9c1ec10210b206ff602dbe126349056af13d", + "research/e8-r480-nine-stage/README.md": "14ba6d703dde9429c82c546199affe855c147ccfd5012fc13da9f18cdf0b5dda", + "research/e8-r480-nine-stage/code/assemble9.py": "4bf6768224a3fac81ccda26df24f3763f9a4fbc35ad62bef2888595cdae519fe" + }, + "related_work_not_imported": { + "691": { + "author": "mtpsl", + "head": "ee6b9175fe006c11871802866c487b5ecc1a93a4", + "relation": "same positive-integer/reverse-majorization criterion on different R420 quad13" + } + }, + "submission_refresh": { + "all_eight_consumed_inputs_unchanged": true, + "main": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "selected_kappa": "1661202643272239/1000000000000000000", + "selected_prs": [ + 741, + 589 + ] + } +} diff --git a/research/r480-quad-seed1/VALIDATION.json b/research/r480-quad-seed1/VALIDATION.json new file mode 100644 index 0000000000..17dba58b1e --- /dev/null +++ b/research/r480-quad-seed1/VALIDATION.json @@ -0,0 +1,124 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "checks": [ + { + "columns": 720, + "command": "python3 -I -B research/r480-quad-seed1/verify.py --out OUT", + "negative_controls": 20, + "result": "PASS_R480_QUAD_SEED1" + }, + { + "command": "python3 -I -O -B research/r480-quad-seed1/verify.py --out OUT", + "result": "PASS; byte-identical exact certificate" + }, + { + "columns": 720, + "command": "python3 -I -B research/r480-quad-seed1/independent_check.py --word OUT/word.json.gz", + "negative_controls": 16, + "result": "PASS_INDEPENDENT_SET_VALUED_DIRTY_INPUT_REPLAY" + }, + { + "command": "python3 -I -O -B research/r480-quad-seed1/discover.py --output RECIPE", + "result": "byte-identical recipe.json" + }, + { + "command": "BOOST_INCLUDE=HEADERS python3 -B research/r480-quad-seed1/native_replay.py --work NEW_OUT", + "receipt": "NATIVE-VALIDATION.json", + "result": "PASS_R480_QUAD_SEED1_NATIVE_LOCAL_REPLAY" + }, + { + "command": "python3 -B scripts/verify_selected_result.py", + "result": "PASS selected record, exact kappa, original source inventory and proof supplement: 51110230636731/31250000000000000" + } + ], + "claims": [ + "finite circuit construction only", + "no new kappa", + "no optimality", + "no practical runtime speedup measurement" + ], + "date": "2026-10-13", + "not_run": [ + "global hosting rediscovery", + "changed-word global owner/template replay", + "outer 47-inequality assembly", + "selected frontier cold replay", + "Lean", + "remote CI" + ], + "overlap_refresh": { + "distinction": "R480 quad1; PR691 changes R420 quad13. No pending source imported. R480 matches only historical boundary formalizations in the final targeted query.", + "latest_pr_seen": 814, + "no_coordination_issue": true, + "queries": [ + "is:open R480", + "is:open quad", + "is:open cleanup", + "is:open bit", + "is:issue is:open", + "is:issue sprint" + ], + "related_author": "mtpsl", + "related_pr691_head": "ee6b9175fe006c11871802866c487b5ecc1a93a4" + }, + "packaging": { + "discovery": { + "exit_code": 0, + "expected_text": null + }, + "expected_evidence_drift": { + "exit_code": 1, + "expected_text": "exact evidence certificate" + }, + "recipe_boolean": { + "exit_code": 1, + "expected_text": "recipe integer type" + }, + "recipe_primitive": { + "exit_code": 1, + "expected_text": "full integer forward transfer" + }, + "relocated_independent": { + "exit_code": 0, + "expected_text": "PASS_INDEPENDENT_SET_VALUED_DIRTY_INPUT_REPLAY" + }, + "relocated_optimized_primary": { + "exit_code": 0, + "expected_text": "PASS_R480_QUAD_SEED1" + }, + "source_drift": { + "exit_code": 1, + "expected_text": "source drift" + }, + "without_mutable_selected_record": { + "exit_code": 0, + "result": "PASS; only the eight consumed inputs are required" + } + }, + "packaging_scope": "Minimal copy of this package and all eight SOURCES.json inputs, no Git metadata; launched from outside a path containing spaces. Primary and independent checks run under optimized Python. Every mutation was restored before the next test.", + "platform": "macOS-26.5-arm64-arm-64bit", + "primary_python": "3.9.6", + "repository_wide_attempt": { + "command": "make verify", + "exit_code": 2, + "first_failure": "copied_centers_producer.py -> scripts/structured_bulk/complex.py:51: AttributeError: int has no attribute bit_count", + "interpretation": "System Python 3.9.6 cannot execute this inherited code. No full-suite pass is claimed; expensive repository-wide replay was not repeated.", + "location": "untouched detached worktree at exact base (separate from contribution)", + "passed": [ + "audit_community_candidate.py", + "audit_followup_candidate.py" + ], + "python": "3.9.6" + }, + "review": "Separate AI worker reviewed exact matrices, frame/accounting implications and primary verifier; independent set-valued interpreter imports no producer or primary verifier. No independent human review claimed.", + "status": "PASS_SCOPED_FINITE_CONSTRUCTION_VALIDATION", + "submission_refresh": { + "all_eight_consumed_inputs_unchanged": true, + "main": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "selected_kappa": "1661202643272239/1000000000000000000", + "selected_prs": [ + 741, + 589 + ] + } +} diff --git a/research/r480-quad-seed1/discover.py b/research/r480-quad-seed1/discover.py new file mode 100644 index 0000000000..d02b6d64ba --- /dev/null +++ b/research/r480-quad-seed1/discover.py @@ -0,0 +1,175 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +# Prepared for haoyan with substantial OpenAI Codex assistance. +# The source circuit is DreamingOfClouds' R480 adaptation of eumemic's +# carrier-skeleton construction; see ../e8-r480-dead-totals/NOTICE.md. +"""Reproduce the first bounded seed-1 quad factorization attempt (Python 3.9+). + +The source is pinned by SHA256. Start at quad 1 in the source's 60-quad +phase-A stage. Subtract componentwise dominated rows of its exact integer +transfer matrix, while accumulating the corresponding unsigned literal +reverse transfer. Reject any subtraction whose reverse transfer would +exceed the source entrywise. Choose eligible rows with seed-1 weighted +sampling, using the cube of the source-row sum as the weight. + +The completed search consists of one attempt on quad 1, stopped at the +first strict improvement. It establishes a witness, not optimality. This +script repeats only that attempt; it never searches additional quads. +It emits deterministic JSON to stdout, or to --output PATH. +""" + +import argparse +import gzip +import hashlib +import json +import random +import sys +from pathlib import Path + +SOURCE = "research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz" +SOURCE_SHA256 = "92e399e9a486b55229b5624632ac54f800dd9e022f2aee97f1e5f264bbc0ef5c" +SEED = 1 + + +def require(condition, message): + """Checks must also run when Python is invoked with -O.""" + if not condition: + raise ValueError(message) + + +def identity(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def transfer(ops, n): + rows = identity(n) + for d, s in ops: + require(0 <= d < n and 0 <= s < n and d != s, + "invalid local operation") + rows[d] = [x + y for x, y in zip(rows[d], rows[s])] + return rows + + +def dominated(left, right): + return all(x <= y for a, b in zip(left, right) for x, y in zip(a, b)) + + +def extract_quad(word): + runs = [] + for index, gate in enumerate(word["A"]): + require(len(gate) == 3, "malformed phase-A gate") + frame = gate[0] + if runs and runs[-1][2] == frame: + runs[-1][1] = index + 1 + else: + runs.append([index, index + 1, frame]) + twelve_line_runs = [run for run in runs if len(word["frames"][run[2]]) == 12] + require(len(twelve_line_runs) == 70, "expected 60 quads and 10 Q-nodes") + quads = twelve_line_runs[:60] + require(all(quads[i][1] == quads[i + 1][0] for i in range(59)), + "quad stage is not contiguous") + start, end, frame = quads[SEED % 60] + require((start, end, frame) == (621, 639, 303), "seed-start quad changed") + gates = word["A"][start:end] + require(all(len(sources) == 1 for _, _, sources in gates), + "quad does not consist of single-source XORs") + wires = sorted({wire for _, dst, sources in gates for wire in [dst] + sources}) + require(wires == [487, 504, 550, 574, 598, 622], "quad wire set changed") + indices = {wire: i for i, wire in enumerate(wires)} + ops = [(indices[dst], indices[source]) + for _, dst, sources in gates for source in sources] + return start, end, frame, wires, ops + + +def discover(source_path): + compressed = source_path.read_bytes() + require(hashlib.sha256(compressed).hexdigest() == SOURCE_SHA256, + "source SHA256 mismatch") + word = json.loads(gzip.decompress(compressed)) + require(word["format"] == "bitE8/1+mut" and word["R"] == 480, + "unexpected source format or register count") + start, end, frame, wires, old_ops = extract_quad(word) + n = len(wires) + forward = transfer(old_ops, n) + old_reverse = transfer(list(reversed(old_ops)), n) + remaining = [row[:] for row in forward] + reverse = identity(n) + reduction = [] + rng = random.Random(SEED) + + # One attempt, at most old_count - 1 operations: the candidate must + # strictly reduce the number of single-source XORs. + for _ in range(len(old_ops) - 1): + eligible = [] + for dst in range(n): + if sum(remaining[dst]) == 1: + continue + for src in range(n): + if dst == src or remaining[dst][dst] <= remaining[src][dst]: + continue + if not all(x >= y for x, y in zip(remaining[dst], remaining[src])): + continue + if not all(x + y <= bound for x, y, bound in + zip(reverse[dst], reverse[src], old_reverse[dst])): + continue + eligible.append((dst, src, sum(remaining[src]))) + require(bool(eligible), "the recorded first attempt has no admissible continuation") + dst, src, _ = rng.choices(eligible, weights=[weight ** 3 for _, _, weight in eligible])[0] + remaining[dst] = [x - y for x, y in zip(remaining[dst], remaining[src])] + reverse[dst] = [x + y for x, y in zip(reverse[dst], reverse[src])] + reduction.append((dst, src)) + if remaining == identity(n): + break + + require(remaining == identity(n), "first attempt did not finish within its gate budget") + new_ops = list(reversed(reduction)) + new_reverse = transfer(reduction, n) + require(len(new_ops) < len(old_ops), "candidate is not a strict gate reduction") + require(transfer(new_ops, n) == forward, "candidate changes full integer forward transfer") + require(new_reverse == reverse, "reverse accumulator mismatch") + require(dominated(new_reverse, old_reverse), "candidate increases reverse transfer") + require({r for pair in new_ops for r in pair} == set(range(n)), + "candidate fails to use every original wire at the common frame") + + return { + "source": SOURCE, + "seed": SEED, + "quad_index": SEED % 60, + "A_start": start, + "A_end": end, + "frame_id": frame, + "wires": wires, + "old_ops": old_ops, + "new_ops": new_ops, + "forward_matrix": forward, + "old_reverse_matrix": old_reverse, + "new_reverse_matrix": new_reverse, + "attempt": 0, + "coverage_before": [], + "source_sha256": SOURCE_SHA256, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--source", type=Path, + default=Path(__file__).resolve().parents[2] / SOURCE) + parser.add_argument("--seed", type=int, default=SEED, + help="recorded assignment seed (must be 1)") + parser.add_argument("--output", type=Path, help="write deterministic recipe here instead of stdout") + args = parser.parse_args() + require(args.seed == SEED, "this reproduction is restricted to assignment seed 1") + recipe = discover(args.source) + encoded = json.dumps(recipe, indent=2) + "\n" + if args.output is None: + sys.stdout.write(encoded) + else: + args.output.write_text(encoded, encoding="utf-8") + + +if __name__ == "__main__": + try: + main() + except (ValueError, OSError, KeyError, TypeError) as exc: + print("discovery failed: {}".format(exc), file=sys.stderr) + sys.exit(1) diff --git a/research/r480-quad-seed1/independent_check.py b/research/r480-quad-seed1/independent_check.py new file mode 100644 index 0000000000..13373fceef --- /dev/null +++ b/research/r480-quad-seed1/independent_check.py @@ -0,0 +1,304 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +# Prepared for Hao Yan (@FanPUYen) with substantial OpenAI Codex assistance. +# The original circuit is DreamingOfClouds' PR #503/#510 R480 adaptation of +# eumemic's PR #493 carrier skeleton. The mutable-source interface follows +# Zhihao Chen's PR #425, as documented in the predecessor package. +"""Independent set-valued audit of the seed-1 R480 six-wire replacement. + +No producer, synthesis, pricing, or primary-verifier module is imported. Every +register carries a set of formal input columns and addition is symmetric +difference. The six-wire check treats its inputs as independently dirty even +though they are correlated at the actual point in the complete word. + +This checks finite word semantics over F2 and the inherited mutable-source interface. +It does not prove the all-size compiler, a finite-prefix invoice, or a saving +constant. The positive-integer transfer certificate is checked separately. + +Usage: python independent_check.py --word /path/to/full-word.json[.gz] +""" + +from __future__ import annotations + +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction +import gzip +import hashlib +import json +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ORIGINAL = HERE.parent / "e8-r480-dead-totals/data/bitE8mut-r480.json.gz" +ORIGINAL_SHA256 = "92e399e9a486b55229b5624632ac54f800dd9e022f2aee97f1e5f264bbc0ef5c" +START, END, FRAME = 621, 639, 303 +WIRES = (487, 504, 550, 574, 598, 622) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load_word(path): + raw = Path(path).read_bytes() + return json.loads(gzip.decompress(raw) if raw[:2] == b"\x1f\x8b" else raw) + + +def digest(value): + return hashlib.sha256( + json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + ).hexdigest() + + +def reduced_basis(rows): + """Canonical rational row reduction, independent of the word generators.""" + rows = [[Fraction(x) for x in row] for row in rows] + pivot_row = 0 + for col in range(8): + candidates = [i for i in range(pivot_row, len(rows)) if rows[i][col]] + if not candidates: + continue + chosen = candidates[0] + rows[pivot_row], rows[chosen] = rows[chosen], rows[pivot_row] + factor = rows[pivot_row][col] + rows[pivot_row] = [x / factor for x in rows[pivot_row]] + for i in range(len(rows)): + if i != pivot_row: + factor = rows[i][col] + rows[i] = [x - factor * y for x, y in zip(rows[i], rows[pivot_row])] + pivot_row += 1 + return tuple(tuple(row) for row in rows[:pivot_row]) + + +class Frames: + def __init__(self, word): + self.bases = [reduced_basis([word["lines"][r] for r in frame]) + for frame in word["frames"]] + self.ranks = [len(basis) for basis in self.bases] + zero = [i for i, rank in enumerate(self.ranks) if rank == 0] + full = [i for i, rank in enumerate(self.ranks) if rank == 8] + require(len(zero) == len(full) == 1, "unique zero and full frames") + self.zero, self.full = zero[0], full[0] + self.nested_cache = {} + + def nested(self, lower, upper): + pair = lower, upper + if pair not in self.nested_cache: + combined = self.bases[lower] + self.bases[upper] + self.nested_cache[pair] = reduced_basis(combined) == self.bases[upper] + return self.nested_cache[pair] + + +def check_interface(word, frames): + v = word["v"] + n = 2 * v + word["R"] + is_target = lambda r: v <= r < 2 * v + is_z = lambda r: 0 <= r < n and not is_target(r) + for section in ("D", "A", "B", "C"): + for f, destination, sources in word[section]: + if is_z(destination): + require(all(is_z(s) for s in sources), "target feeds source/helper") + require(all(f == frames.zero and is_target(d) + and all(2 * v <= s < n for s in sources) + for f, d, sources in word["D"]), "dirty correction interface") + require(all(is_z(d) for _, d, _ in word["A"]), "A writes target") + require(all(is_target(d) for _, d, _ in word["B"]), "B writes source/helper") + require(all(f == frames.full and is_z(d) and all(is_z(s) for s in sources) + for f, d, sources in word["C"]), "cleanup interface") + z_gates = [[frames.full, d, sources] for section in ("A", "B") + for _, d, sources in word[section] if is_z(d)] + require(word["C"] == list(reversed(z_gates)), "cleanup is not literal inverse") + require(len(word["scatter"]) == v + and all(type(k) is int and 0 <= k < len(word["ret"]) + for row in word["scatter"] for k in row), "scatter interface") + require(all(2 * v <= q < n for q in word["ret"]), "total is not a helper") + + +def replay(word, frames, track_frames=True): + """All formal columns at once, represented by Python sets (not bit masks).""" + v = word["v"] + n = 2 * v + word["R"] + state = [{i} for i in range(n)] + current = list(word["start"]) + paths = [[f] for f in current] + climbs = Counter() + + def climb(register, frame): + previous = current[register] + if frame == previous: + return + require(frames.ranks[previous] < frames.ranks[frame] + and frames.nested(previous, frame), "non-nested frame climb") + climbs[frames.ranks[frame] - frames.ranks[previous]] += 1 + current[register] = frame + paths[register].append(frame) + + def run(gates): + for frame, destination, sources in gates: + registers = [destination] + sources + require(type(frame) is int and 0 <= frame < len(frames.bases), "invalid frame") + require(all(type(r) is int and 0 <= r < n for r in registers) + and len(set(registers)) == len(registers), "invalid gate registers") + if track_frames: + for register in registers: + climb(register, frame) + for source in sources: + state[destination].symmetric_difference_update(state[source]) + + run(word["D"]) + if track_frames: + require(all(current[r] == frames.zero for r in range(v, n)), "D moved non-source") + run(word["A"]) + if track_frames: + require(all(current[v + t] == frames.zero for t in range(v)), "target left zero before scatter") + require(all(current[q] == frames.full for q in word["ret"]), "total not at full frame") + totals = [set(state[q]) for q in word["ret"]] + for t, row in enumerate(word["scatter"]): + for k in row: + state[v + t].symmetric_difference_update(totals[k]) + run(word["B"]) + run(word["C"]) + if track_frames: + for register, frame in enumerate(word["final"]): + climb(register, frame) + return state, paths, climbs + + +def require_identity_plus_source(state, v=120): + for register, support in enumerate(state): + expected = {register, register - v} if v <= register < 2 * v else {register} + require(support == expected, f"formal column map fails at register {register}") + + +def local_map(gates): + state = {wire: {i} for i, wire in enumerate(WIRES)} + for frame, destination, sources in gates: + require(frame == FRAME and destination in state and len(sources) == 1 + and sources[0] in state and sources[0] != destination, "local six-wire gate") + state[destination].symmetric_difference_update(state[sources[0]]) + return [sorted(state[wire]) for wire in WIRES] + + +def candidate_block(original, candidate): + require(candidate.keys() == original.keys(), "word schema changed") + require(all(candidate[key] == original[key] for key in original if key not in ("A", "C")), + "non-A/C data changed") + suffix_length = len(original["A"]) - END + new_end = len(candidate["A"]) - suffix_length + require(START < new_end < END, "replacement is not strictly shorter") + require(candidate["A"][:START] == original["A"][:START] + and candidate["A"][new_end:] == original["A"][END:], "A changed outside selected quad") + return candidate["A"][START:new_end] + + +def expect_rejected(name, operation): + try: + operation() + except ValueError as error: + return {"name": name, "rejected": True, "reason": str(error)} + raise ValueError(f"negative control accepted: {name}") + + +def controls(candidate, block, local_expected, frames): + results = [] + # Reflecting every deletion into C preserves literal source/helper cleanup; + # a clean-input-only test could miss the changed local dirty-helper action. + for omitted in range(len(block)): + mutant = deepcopy(candidate) + del mutant["A"][START + omitted] + mutant["C"] = [[frames.full, d, sources] for _, d, sources in reversed(mutant["A"])] + check_interface(mutant, frames) + shortened = block[:omitted] + block[omitted + 1:] + result = expect_rejected( + f"omit_local_gate_{omitted}_and_reflect_cleanup", + lambda gates=shortened: require(local_map(gates) == local_expected, + "arbitrary six-wire dirty-input map changed")) + output, _, _ = replay(mutant, frames, track_frames=False) + result["full_word_map_also_changed"] = any( + support != ({r, r - 120} if 120 <= r < 240 else {r}) + for r, support in enumerate(output)) + results.append(result) + + for name, predicate in (("omit_helper_cleanup", lambda d: d >= 240), + ("omit_source_cleanup", lambda d: d < 120)): + mutant = deepcopy(candidate) + index = next(i for i, (_, d, _) in enumerate(mutant["C"]) if predicate(d)) + del mutant["C"][index] + results.append(expect_rejected(name, lambda word=mutant: + require_identity_plus_source(replay(word, frames, False)[0]))) + + mutant = deepcopy(candidate) + removed = mutant["D"][0][2].pop(0) + result = expect_rejected("omit_one_dirty_correction_source", lambda: + require_identity_plus_source(replay(mutant, frames, False)[0])) + result["omitted_dirty_column"] = removed + results.append(result) + + mutant = deepcopy(candidate) + mutant["A"][START][0] = frames.zero + results.append(expect_rejected("move_one_local_gate_to_zero_frame", lambda: + replay(mutant, frames))) + return results + + +def audit(word_path): + require(hashlib.sha256(ORIGINAL.read_bytes()).hexdigest() == ORIGINAL_SHA256, + "pinned original word bytes changed") + original, candidate = load_word(ORIGINAL), load_word(word_path) + block = candidate_block(original, candidate) + frames = Frames(original) + expected_local = local_map(original["A"][START:END]) + require(local_map(block) == expected_local, "local arbitrary dirty-input map changed") + for word in (original, candidate): + check_interface(word, frames) + original_state, original_paths, original_climbs = replay(original, frames) + state, paths, climbs = replay(candidate, frames) + require_identity_plus_source(original_state) + require_identity_plus_source(state) + require(state == original_state, "original/candidate symbolic maps differ") + require(paths == original_paths, "a register's frame path changed") + require(climbs == original_climbs, "paid climb histogram changed") + negative_controls = controls(candidate, block, expected_local, frames) + return { + "status": "PASS_INDEPENDENT_SET_VALUED_DIRTY_INPUT_REPLAY", + "original_file_sha256": ORIGINAL_SHA256, + "candidate_content_sha256": digest(candidate), + "formal_columns": len(state), + "source_columns": 120, + "target_columns": 120, + "dirty_helper_columns": 480, + "all_source_and_helper_columns_restored": True, + "all_targets_add_exactly_their_source": True, + "local_arbitrary_dirty_input_columns": len(WIRES), + "local_matrix_supports": expected_local, + "interface_hypotheses_checked": True, + "selected_frame": FRAME, + "selected_frame_exact_rational_rank": frames.ranks[FRAME], + "all_720_register_frame_paths_identical": True, + "register_path_sha256": digest(paths), + "local_paid_climb_histogram": dict(sorted(climbs.items())), + "old_local_gate_count": END - START, + "new_local_gate_count": len(block), + "negative_controls": negative_controls, + "scope": "Finite word and local arbitrary dirty-input semantics; no prefix invoice, all-size compiler, or saving-constant claim.", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--word", type=Path, required=True) + parser.add_argument("--json", type=Path, help="optional receipt path") + args = parser.parse_args() + result = audit(args.word) + rendered = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.json: + args.json.parent.mkdir(parents=True, exist_ok=True) + args.json.write_text(rendered) + print(rendered, end="") + + +if __name__ == "__main__": + main() diff --git a/research/r480-quad-seed1/native_replay.py b/research/r480-quad-seed1/native_replay.py new file mode 100644 index 0000000000..541ea1b508 --- /dev/null +++ b/research/r480-quad-seed1/native_replay.py @@ -0,0 +1,228 @@ +#!/usr/bin/env python3 +"""Optional inherited local replay: Python standard library, C++17, Boost headers. + +Usage: BOOST_INCLUDE=/path/to/boost python native_replay.py --work /new/output +CXX defaults to c++; BOOST_INCLUDE defaults to /usr/include. This does not run +global template emission, hosting, assembly, or the repository-wide suite. + +Prepared for Hao Yan (@FanPUYen) with substantial OpenAI Codex assistance. +Apache-2.0. The replayed checkers are attributed to Dylan Crow and eumemic, +with their original Anthropic Claude assistance notices retained unchanged. +""" +import argparse +import gzip +import hashlib +import json +import os +import platform +import re +import shlex +import subprocess +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +PARENT = ROOT / "research/e8-bit-carrier-skeleton" +PARENT_MANIFEST_SHA256 = "7f25c41d0400ef5adf763eae6e166003a9b59e5a655b860c04b052f6731c7297" +SOURCE = ROOT / "research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz" +SOURCE_SHA256 = "92e399e9a486b55229b5624632ac54f800dd9e022f2aee97f1e5f264bbc0ef5c" + + +def require(value, message): + if not value: + raise ValueError(message) + + +def sha(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def content_sha(path): + w = json.loads(gzip.decompress(path.read_bytes())) + return hashlib.sha256(json.dumps(w, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + + +def pinned_parent(): + """Pin the full inherited package, including all imported checker helpers.""" + manifest = PARENT / "MANIFEST.sha256" + require(sha(manifest) == PARENT_MANIFEST_SHA256, "inherited manifest changed") + seen = set() + for row in manifest.read_text().splitlines(): + wanted, name = row.split(" ", 1) + path = (PARENT / name).resolve() + require(PARENT in path.parents and name not in seen, "invalid manifest path") + require(sha(path) == wanted, "inherited source changed: " + name) + seen.add(name) + require(len(seen) == 93, "inherited manifest file count") + # Refuse an unlisted Python/header sibling that could shadow a pinned import. + code = {str(p.relative_to(PARENT)) for p in PARENT.rglob("*") + if p.is_file() and p.suffix in (".py", ".h", ".hpp", ".cpp")} + require(code <= seen, "unlisted inherited code files") + require(sha(SOURCE) == SOURCE_SHA256, "R480 source word changed") + + +class Replay: + def __init__(self, work): + self.work = work + self.python = sys.executable + self.cxx = shlex.split(os.environ.get("CXX", "c++")) + require(bool(self.cxx), "empty CXX") + self.boost = Path(os.environ.get("BOOST_INCLUDE", "/usr/include")).resolve() + self.env = dict(os.environ, PYTHONDONTWRITEBYTECODE="1", PYTHONINTMAXSTRDIGITS="0", + TMPDIR=str(work / "tmp")) + (work / "tmp").mkdir() + (work / "logs").mkdir() + (work / "bin").mkdir() + self.commands = [] + + def normalized(self, value): + for old, new in ((self.python, "{python}"), (str(self.work), "{work}"), + (str(self.boost), "{boost_include}"), (str(ROOT), "{repo}")): + value = value.replace(old, new) + return value + + def run(self, name, command, expected_failure=None): + command = list(map(str, command)) + result = subprocess.run(command, env=self.env, capture_output=True, text=True) + (self.work / "logs" / (name + ".log")).write_text(result.stdout + result.stderr) + self.commands.append({"name": name, "command": self.normalized(shlex.join(command)), + "exit_code": result.returncode}) + (self.work / "commands.json").write_text(json.dumps(self.commands, indent=2) + "\n") + if expected_failure is None: + require(result.returncode == 0, name + " failed; see " + str(self.work / "logs" / (name + ".log"))) + else: + require(result.returncode != 0 and expected_failure in result.stderr, + name + " did not reject the expected control") + print("PASS " + name, flush=True) + return result.stdout + + def py(self, name, script, *args, expected_failure=None): + return self.run(name, [self.python, "-I", "-B", script, *args], expected_failure) + + def compile(self): + checkers = PARENT / "code/bit/checkers" + inc = ["-I" + str(PARENT / "portable-include"), "-I" + str(checkers), "-I" + str(self.boost)] + common = self.cxx + ["-O2", "-std=c++17", "-DHDIM=8"] + specs = [("legality", "legality_h.cpp", ["-DNCOPY=9"]), + ("legality_ncopy_h", "legality_h.cpp", [])] + for name, source, extra in (("columns_h", "columns_h.cpp", []), + ("columns_k2", "columns_k.cpp", ["-DKPAIRS=2"]), + ("columns_k4", "columns_k.cpp", ["-DKPAIRS=4"]), + ("columns_k5", "columns_k.cpp", ["-DKPAIRS=5"])): + specs.append((name, source, ["-DNCOPY=9", "-DVPORTS=120", "-DRHELP=480"] + extra)) + for name, source, extra in specs: + self.run("compile-" + name, common + extra + inc + + ["-o", self.work / "bin" / name, checkers / source]) + + def case(self, name, word): + d = self.work / name + d.mkdir() + bit = PARENT / "code/bit" + pricing = PARENT / "code/pricing" + binary = self.work / "bin" + py = lambda step, script, *args, **kwargs: self.py(name + "-" + step, script, *args, **kwargs) + py("relax", bit / "independent/relax.py", d / "rchk") + py("stock-refusal", bit / "independent/checkword.py", word, pricing, + expected_failure="x register written") + text = py("all720", d / "rchk/checkword_mut.py", word, pricing) + require("legality + exact F2 on all 720 columns: PASS" in text, "all-column receipt") + py("interface", bit / "independent/interface.py", word, "--json", d / "interface.json") + text = py("word-controls", bit / "independent/mutate_mut.py", word, + d / "rchk/checkword_mut.py", pricing, bit / "independent/interface.py") + require("6 word-level mutants and 5 mutable-source mutants rejected" in text and + "PASS interface.py: 2 hypothesis controls rejected" in text, "word controls receipt") + py("export", bit / "export_records.py", word, d / "records") + py("cohort", bit / "regression/stage_cohort.py", d / "records", d / "records", d / "cin", d / "cout") + co = d / "cout" + self.run(name + "-legality", [binary / "legality", d / "cin", co, co / "legality.json"]) + for checker in ("columns_h", "columns_k2", "columns_k4", "columns_k5"): + self.run(name + "-" + checker, + [binary / checker, co / "COHORT249-RECORDS.bin", co / (checker + ".json")]) + text = py("record-controls", bit / "mutate_records.py", d / "records", d / "cin", co, + binary / "legality", binary / "columns_k5", binary / "legality_ncopy_h") + require("PASS all 6 record-level negative controls rejected" in text, "record controls receipt") + text = py("source-record-controls", bit / "mutate_records_mut.py", word, d / "records", d / "cin", co, + binary / "legality", binary / "columns_h", binary / "columns_k5") + require("PASS all 3 record-level mutable-source mutants rejected" in text, "source record controls receipt") + text = py("gram", bit / "checkers/gram_frames.py", d / "records", "--gram", "e8ham", "--h", "8", "--positive") + require("672 frames checked, all nondegenerate and positive definite" in text and + "primes [2]" in text, "Gram receipt") + return semantic_case(word, d) + + +def semantic_case(word, directory): + """Only deterministic, independently computed receipt fields are frozen.""" + co = directory / "cout" + read = lambda name: json.loads((co / (name + ".json")).read_text()) + legality = read("legality") + require(legality["status"] == "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE", + "legality status") + five, k2 = read("columns_h"), read("columns_k2") + require({k: v for k, v in five.items() if k != "seconds"} == + {k: v for k, v in k2.items() if k != "seconds"}, "KPAIRS=2 must reproduce five-stage receipt") + stages = {} + for label, source, count in (("five", "columns_h", 5), ("nine", "columns_k4", 9), + ("eleven", "columns_k5", 11)): + receipt = read(source) + wanted = "PASS_NEW_COHORT249_ALL_" + ("FIVE_STAGE" if count == 5 else "BRIDGED_STAGE") + "_FORMAL_COLUMNS_AND_PREFIX_BILL" + require(receipt["status"] == wanted and len(receipt["stages"]) == count, "formal column status") + require(all(x["rejected"] for x in receipt["negative_controls"]), "omitted bridge control") + require(int(receipt["payload_prefix_upper"]) < (1 << 104), "payload prefix bound") + for key in ("local_scalar_additions", "local_raw_H", "signed_lift_prefix", "payload_prefix_bits", "payload_prefix_upper"): + require(receipt[key] == five[key], "stage-independent local invoice: " + key) + stages[label] = {key: receipt[key] for key in ("formal_columns_checked", "bridge_additions")} + stages[label]["omitted_bridge_controls_rejected"] = len(receipt["negative_controls"]) + return { + "word_content_sha256": content_sha(word), + "local_columns": 720, + "interface": json.loads((directory / "interface.json").read_text()), + "legality": {key: legality[key] for key in + ("records", "common_frame_ADDs", "nested_MOVEs", "copies", "erasures", "rank_mass", "paid_histogram")}, + "local_invoice": {key: five[key] for key in + ("local_scalar_additions", "local_raw_H", "signed_lift_prefix", "payload_prefix_bits", "payload_prefix_upper")}, + "stages": stages, + "negative_controls": {"word_generic": 6, "word_mutable_source": 5, "interface": 2, + "record_generic": 6, "record_mutable_source": 3}, + "gram_frames": 672, + "gram_prime_witnesses": [2], + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--work", required=True, type=Path, help="new output directory outside this package") + args = parser.parse_args() + require(not sys.flags.optimize, "run without Python -O; inherited checks use assertions") + work = args.work.resolve() + require(work != HERE and HERE not in work.parents and work != PARENT and PARENT not in work.parents, + "work directory must be outside this package and inherited sources") + require(not work.exists() or not any(work.iterdir()), "work directory must be absent or empty") + pinned_parent() + work.mkdir(parents=True, exist_ok=True) + replay = Replay(work) + replay.py("primary-verifier", HERE / "verify.py", "--out", work / "constructed") + replay.compile() + observed = {"status": "PASS_R480_QUAD_SEED1_NATIVE_LOCAL_REPLAY", + "inherited_manifest_sha256": PARENT_MANIFEST_SHA256, + "baseline": replay.case("baseline", SOURCE), + "candidate": replay.case("candidate", work / "constructed/word.json.gz")} + (work / "NATIVE-RESULT.json").write_text(json.dumps(observed, indent=2, sort_keys=True) + "\n") + expected = json.loads((HERE / "NATIVE-EXPECTED.json").read_text()) + require(observed == expected, "semantic native receipt differs from NATIVE-EXPECTED.json") + version = replay.run("compiler-version", replay.cxx + ["--version"]) + boost_header = replay.boost / "boost/version.hpp" + boost_version = re.search(r'^#define BOOST_LIB_VERSION "([^"]+)"', boost_header.read_text(), re.M) + validation = {"status": observed["status"], "python": platform.python_version(), + "compiler": version.strip(), "boost_version": boost_version.group(1) if boost_version else None, + "boost_version_header_sha256": sha(boost_header), + "native_expected_sha256": sha(HERE / "NATIVE-EXPECTED.json"), + "inherited_manifest_sha256": PARENT_MANIFEST_SHA256, + "commands": replay.commands, + "scope": "Local finite/native replay only; no global hosting replay or exponent improvement."} + (work / "VALIDATION.json").write_text(json.dumps(validation, indent=2) + "\n") + print(observed["status"] + " ADDs=33958->33946 prefix_bits=102 unchanged_paid_profile") + + +if __name__ == "__main__": + main() diff --git a/research/r480-quad-seed1/recipe.json b/research/r480-quad-seed1/recipe.json new file mode 100644 index 0000000000..96c75abd98 --- /dev/null +++ b/research/r480-quad-seed1/recipe.json @@ -0,0 +1,293 @@ +{ + "source": "research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz", + "seed": 1, + "quad_index": 1, + "A_start": 621, + "A_end": 639, + "frame_id": 303, + "wires": [ + 487, + 504, + 550, + 574, + 598, + 622 + ], + "old_ops": [ + [ + 0, + 1 + ], + [ + 0, + 3 + ], + [ + 0, + 4 + ], + [ + 0, + 5 + ], + [ + 1, + 2 + ], + [ + 1, + 3 + ], + [ + 1, + 4 + ], + [ + 1, + 5 + ], + [ + 2, + 3 + ], + [ + 2, + 4 + ], + [ + 2, + 5 + ], + [ + 3, + 4 + ], + [ + 5, + 0 + ], + [ + 5, + 2 + ], + [ + 5, + 4 + ], + [ + 4, + 0 + ], + [ + 3, + 0 + ], + [ + 3, + 2 + ] + ], + "new_ops": [ + [ + 2, + 5 + ], + [ + 3, + 4 + ], + [ + 0, + 1 + ], + [ + 0, + 3 + ], + [ + 0, + 5 + ], + [ + 2, + 3 + ], + [ + 5, + 2 + ], + [ + 3, + 2 + ], + [ + 1, + 2 + ], + [ + 4, + 0 + ], + [ + 5, + 4 + ], + [ + 3, + 0 + ] + ], + "forward_matrix": [ + [ + 1, + 1, + 0, + 1, + 1, + 1 + ], + [ + 0, + 1, + 1, + 1, + 1, + 1 + ], + [ + 0, + 0, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 3, + 3, + 2 + ], + [ + 1, + 1, + 0, + 1, + 2, + 1 + ], + [ + 1, + 1, + 1, + 2, + 3, + 3 + ] + ], + "old_reverse_matrix": [ + [ + 16, + 1, + 7, + 3, + 9, + 3 + ], + [ + 10, + 1, + 5, + 2, + 6, + 2 + ], + [ + 5, + 0, + 3, + 1, + 3, + 1 + ], + [ + 2, + 0, + 1, + 1, + 1, + 0 + ], + [ + 1, + 0, + 0, + 0, + 1, + 0 + ], + [ + 2, + 0, + 1, + 0, + 1, + 1 + ] + ], + "new_reverse_matrix": [ + [ + 2, + 1, + 3, + 1, + 1, + 1 + ], + [ + 0, + 1, + 1, + 0, + 0, + 0 + ], + [ + 1, + 0, + 3, + 1, + 1, + 1 + ], + [ + 2, + 0, + 1, + 1, + 1, + 0 + ], + [ + 1, + 0, + 0, + 0, + 1, + 0 + ], + [ + 0, + 0, + 1, + 0, + 1, + 1 + ] + ], + "attempt": 0, + "coverage_before": [], + "source_sha256": "92e399e9a486b55229b5624632ac54f800dd9e022f2aee97f1e5f264bbc0ef5c" +} diff --git a/research/r480-quad-seed1/verify.py b/research/r480-quad-seed1/verify.py new file mode 100644 index 0000000000..ab92c56635 --- /dev/null +++ b/research/r480-quad-seed1/verify.py @@ -0,0 +1,298 @@ +#!/usr/bin/env python3 +"""Exact local construction check; standard library, Python 3.9+. + +Prepared for Hao Yan (@FanPUYen) with substantial OpenAI Codex assistance. +Apache-2.0. Source construction: DreamingOfClouds #503/#510 and eumemic #493. +No producer or predecessor checker is imported. +""" +import argparse +import copy +import gzip +import hashlib +import json +from collections import Counter +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +SOURCE = "research/e8-r480-dead-totals/data/bitE8mut-r480.json.gz" +SOURCE_SHA = "92e399e9a486b55229b5624632ac54f800dd9e022f2aee97f1e5f264bbc0ef5c" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def transfer(operations, n): + """Rows are exact integer coefficients, without reduction modulo two.""" + rows = [[int(i == j) for j in range(n)] for i in range(n)] + for d, s in operations: + rows[d] = [a + b for a, b in zip(rows[d], rows[s])] + return rows + + +def rank(lines): + basis = {} + for line in lines: + row = list(map(Fraction, line)) + for pivot, old in sorted(basis.items()): + c = row[pivot] + row = [a - c * b for a, b in zip(row, old)] + pivot = next((j for j, x in enumerate(row) if x), None) + if pivot is not None: + c = row[pivot] + basis[pivot] = [x / c for x in row] + return len(basis) + + +def validate_recipe(w, recipe): + expected_keys = { + "source", "source_sha256", "seed", "quad_index", "A_start", "A_end", + "frame_id", "wires", "old_ops", "new_ops", "forward_matrix", + "old_reverse_matrix", "new_reverse_matrix", "attempt", "coverage_before", + } + require(set(recipe) == expected_keys, "recipe fields") + require(recipe["source"] == SOURCE and recipe["source_sha256"] == SOURCE_SHA, + "recipe source binding") + for key in ("seed", "quad_index", "A_start", "A_end", "frame_id", "attempt"): + require(type(recipe[key]) is int, "recipe integer type: " + key) + require((recipe["seed"], recipe["quad_index"], recipe["attempt"]) == (1, 1, 0), + "seed/coverage binding") + require(recipe["coverage_before"] == [], "search stopped at first quad") + a, b, frame = recipe["A_start"], recipe["A_end"], recipe["frame_id"] + require((a, b, frame) == (621, 639, 303), "quad location") + wires = recipe["wires"] + require(all(type(x) is int for x in wires), "wire integer types") + require(wires == [487, 504, 550, 574, 598, 622], "quad wire binding") + require(all(g[0] == frame and len(g[2]) == 1 for g in w["A"][a:b]), + "source quad shape") + index = {r: i for i, r in enumerate(wires)} + original = [[index[d], index[s]] for _, d, src in w["A"][a:b] for s in src] + for key in ("old_ops", "new_ops"): + require(type(recipe[key]) is list, "operations list") + for gate in recipe[key]: + require(type(gate) is list and len(gate) == 2 and + all(type(i) is int and 0 <= i < 6 for i in gate) and gate[0] != gate[1], + "invalid XOR primitive") + require(original == recipe["old_ops"], "source quad operations") + replacement = recipe["new_ops"] + require(len(replacement) == 12 < len(original) == 18, "strict gate saving") + forward = transfer(original, 6) + require(transfer(replacement, 6) == forward, "full integer forward transfer") + old_reverse = transfer(original[::-1], 6) + new_reverse = transfer(replacement[::-1], 6) + require(all(x <= y for nr, old in zip(new_reverse, old_reverse) + for x, y in zip(nr, old)), "reverse nonnegative majorization") + for key, value in (("forward_matrix", forward), + ("old_reverse_matrix", old_reverse), + ("new_reverse_matrix", new_reverse)): + require(type(recipe[key]) is list and len(recipe[key]) == 6 and + all(type(row) is list and len(row) == 6 and + all(type(x) is int and x >= 0 for x in row) for row in recipe[key]), + "matrix integer types") + require(recipe[key] == value, "matrix certificate: " + key) + return a, b, frame, wires + + +def construct(w, recipe): + a, b, frame, wires = validate_recipe(w, recipe) + out = copy.deepcopy(w) + out["A"][a:b] = [[frame, wires[d], [wires[s]]] for d, s in recipe["new_ops"]] + out["C"] = [[1, d, list(src)] for _, d, src in reversed(out["A"])] + return out + + +def scalar_replay(w): + n, v = 2 * w["v"] + w["R"], w["v"] + state = [1 << i for i in range(n)] + norm = [1] * n + def gate(d, sources): + for s in sources: + state[d] ^= state[s] + norm[d] += norm[s] + for phase in ("D", "A", "scatter", "B", "C"): + if phase == "scatter": + for t, row in enumerate(w[phase]): + gate(v + t, [w["ret"][k] for k in row]) + else: + for _, d, src in w[phase]: + gate(d, src) + expected = [((1 << i) ^ (1 << (i - v))) if v <= i < 2 * v else 1 << i + for i in range(n)] + require(state == expected, "all-column endpoint / arbitrary dirt restoration") + return {"columns": n, "unsigned_raw_peak": max(norm), "raw_norm_sha256": digest(norm)} + + +def paths(w): + n, v = 2 * w["v"] + w["R"], w["v"] + require(n == 720 and len(w["start"]) == n and len(w["final"]) == n, "dimensions") + result = [[f] for f in w["start"]] + frames = [set(row) for row in w["frames"]] + def touch(r, f): + require(type(r) is int and 0 <= r < n, "register index") + require(type(f) is int and 0 <= f < len(frames), "frame index") + old = result[r][-1] + require(frames[old] <= frames[f], "frame descent") + if old != f: + result[r].append(f) + for phase in ("D", "A", "B", "C"): + for f, d, src in w[phase]: + require(len(set([d] + src)) == 1 + len(src), "self-read / duplicate operand") + for r in [d] + src: + touch(r, f) + if phase == "D": + require(f == 0 and v <= d < 2 * v and all(s >= 2 * v for s in src), + "compensation interface") + elif phase == "A": + require(not v <= d < 2 * v and all(not v <= s < 2 * v for s in src), + "phase-A interface") + elif phase == "B": + require(v <= d < 2 * v and all(not v <= s < 2 * v for s in src), + "phase-B interface") + else: + require(f == 1 and all(not v <= r < 2 * v for r in [d] + src), + "cleanup interface") + require(w["C"] == [[1, d, list(src)] for _, d, src in reversed(w["A"])], + "literal reverse cleanup") + require(len(w["ret"]) == 9 and len(set(w["ret"])) == 9 and + all(2 * v <= r < n for r in w["ret"]), "retained helpers") + require(len(w["scatter"]) == v and + all(type(k) is int and 0 <= k < 9 for row in w["scatter"] for k in row), + "scatter interface") + for r, f in enumerate(w["final"]): + touch(r, f) + return result + + +def cost(w, path_list, dimensions): + histogram = Counter({8: len(w["ret"])}) # nine copied retained totals + for path in path_list: + for lo, hi in zip(path, path[1:]): + step = dimensions[hi] - dimensions[lo] + require(step > 0, "positive climb") + histogram[step] += 1 + xor = {p: sum(len(src) for _, _, src in w[p]) for p in ("D", "A", "B", "C")} + xor["scatter"] = sum(map(len, w["scatter"])) + return {"xor_by_phase": xor, "total_xors": sum(xor.values()), + "paid_histogram": {str(k): n for k, n in sorted(histogram.items())}, + "rank_mass": sum(k * n for k, n in histogram.items())} + + +def rejected(action, name): + try: + action() + except (ValueError, IndexError, KeyError, TypeError): + return name + raise ValueError("negative control unexpectedly accepted: " + name) + + +def controls(w, recipe, candidate): + checks = [] + # Test the local integer transfer after each deletion. The independent + # checker separately reflects these deletions into the literal cleanup. + for i in range(len(recipe["new_ops"])): + r = copy.deepcopy(recipe) + del r["new_ops"][i] + checks.append(rejected(lambda r=r: require(transfer(r["new_ops"], 6) == + recipe["forward_matrix"], "changed matrix"), "omit_quad_gate_%d" % i)) + r = copy.deepcopy(recipe) + r["new_ops"] = r["new_ops"][::-1] + checks.append(rejected(lambda: validate_recipe(w, r), "reverse_gate_order")) + r = copy.deepcopy(recipe) + r["new_ops"][0][0] = True + checks.append(rejected(lambda: validate_recipe(w, r), "boolean_as_integer")) + r = copy.deepcopy(recipe) + r["new_reverse_matrix"][0][0] += 1 + checks.append(rejected(lambda: validate_recipe(w, r), "false_reverse_certificate")) + bad = copy.deepcopy(candidate) + del bad["C"][0] + checks.append(rejected(lambda: paths(bad), "missing_cleanup_structure")) + checks.append(rejected(lambda: scalar_replay(bad), "missing_cleanup_dirt")) + bad = copy.deepcopy(candidate) + bad["D"][0][2].pop() + checks.append(rejected(lambda: scalar_replay(bad), "missing_dirty_compensation")) + bad = copy.deepcopy(candidate) + bad["A"][recipe["A_start"]][0] = 0 + checks.append(rejected(lambda: paths(bad), "frame_zero_substitution")) + bad = copy.deepcopy(candidate) + bad["scatter"][0] = bad["scatter"][0][1:] + checks.append(rejected(lambda: scalar_replay(bad), "missing_scatter_read")) + return checks + + +def verify(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + require(pins["base_commit"] == "66849e1475c930fd7732b1a0067ffee7e1e95f60", "base pin") + require(pins["files"][SOURCE] == SOURCE_SHA, "word pin") + for name, wanted in pins["files"].items(): + require(hashlib.sha256((ROOT / name).read_bytes()).hexdigest() == wanted, + "source drift: " + name) + w = json.loads(gzip.decompress((ROOT / SOURCE).read_bytes())) + recipe = json.loads((HERE / "recipe.json").read_text()) + candidate = construct(w, recipe) + require(all(candidate[k] == value for k, value in w.items() if k not in ("A", "C")), + "unrelated word fields changed") + baseline_paths, candidate_paths = paths(w), paths(candidate) + require(baseline_paths == candidate_paths, "all register frame paths unchanged") + used_frames = {f for path in baseline_paths for f in path} + dimensions = {f: rank([w["lines"][i] for i in w["frames"][f]]) for f in used_frames} + require(dimensions[303] == 4, "quad rational rank") + old_cost, new_cost = cost(w, baseline_paths, dimensions), cost(candidate, candidate_paths, dimensions) + require(old_cost["paid_histogram"] == new_cost["paid_histogram"], "paid profile unchanged") + old_scalar, new_scalar = scalar_replay(w), scalar_replay(candidate) + require(new_scalar["unsigned_raw_peak"] <= old_scalar["unsigned_raw_peak"], "raw magnitude bound") + require(old_cost["total_xors"] - new_cost["total_xors"] == 12, "complete saving") + control_names = controls(w, recipe, candidate) + evidence = { + "status": "PASS_R480_QUAD_SEED1", "base_commit": pins["base_commit"], + "source_word_sha256": SOURCE_SHA, "candidate_content_sha256": digest(candidate), + "recipe_sha256": digest(recipe), "frame_paths_sha256": digest(candidate_paths), + "quad": {"index": 1, "frame": 303, "rational_rank": dimensions[303], + "old_gates": 18, "new_gates": 12, + "reverse_strict_entries": sum(x < y for nr, old in zip(recipe["new_reverse_matrix"], + recipe["old_reverse_matrix"]) for x, y in zip(nr, old))}, + "baseline": {"cost": old_cost, "scalar": old_scalar}, + "candidate": {"cost": new_cost, "scalar": new_scalar}, + "negative_controls": control_names, + "scope": "Finite circuit construction; unchanged paid profile; no new kappa or all-size proof.", + } + return evidence, candidate + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path, help="write deterministic candidate word and evidence here") + parser.add_argument("--write-certificate", action="store_true", help="deliberately regenerate EXPECTED.json") + args = parser.parse_args() + evidence, candidate = verify() + formatted = json.dumps(evidence, indent=2, sort_keys=True) + "\n" + if args.write_certificate: + (HERE / "EXPECTED.json").write_text(formatted) + else: + require((HERE / "EXPECTED.json").read_text() == formatted, "exact evidence certificate") + if args.out: + out = args.out.resolve() + require(not out.is_relative_to(HERE) if hasattr(out, "is_relative_to") else HERE not in out.parents, + "output must be outside the package") + out.mkdir(parents=True, exist_ok=True) + (out / "word.json").write_bytes(canonical(candidate) + b"\n") + with (out / "word.json.gz").open("wb") as stream: + with gzip.GzipFile(filename="", fileobj=stream, mode="wb", mtime=0) as zipped: + zipped.write(canonical(candidate)) + (out / "evidence.json").write_text(formatted) + print("PASS_R480_QUAD_SEED1 quad=1 XORs=33958->33946 saved=12 columns=720 controls=%d kappa=unchanged" + % len(evidence["negative_controls"])) + + +if __name__ == "__main__": + main() From 83d547e30fed98682ffc6eacbeeaafa96cfb42fb Mon Sep 17 00:00:00 2001 From: Hao Yan Date: Tue, 13 Oct 2026 14:22:13 +0800 Subject: [PATCH 2/2] Record completed R480 sprint result and PR permission limitation --- research/r480-quad-seed1/CLAIM.json | 42 ++++++++++++++++++------ research/r480-quad-seed1/VALIDATION.json | 1 + 2 files changed, 33 insertions(+), 10 deletions(-) diff --git a/research/r480-quad-seed1/CLAIM.json b/research/r480-quad-seed1/CLAIM.json index e084968d94..1003a2e0c6 100644 --- a/research/r480-quad-seed1/CLAIM.json +++ b/research/r480-quad-seed1/CLAIM.json @@ -1,17 +1,39 @@ { - "track": "bit supplier", + "alternatives_considered": [ + "R489 cleanup synthesis", + "R420 block factorization" + ], "assignment_seed": 1, - "seed_source": "Python secrets.randbelow(100), operating-system randomness", "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", - "started_utc": "2026-10-13T06:01:47Z", - "expected_finish": "2026-10-13T14:42:00+08:00", - "verification_reserved_from": "2026-10-13T14:32:00+08:00", - "object": "PR503/PR510 historical R480 phase-A quad circuits, starting at quad index 1", - "method": "Bounded exact positive-integer row-subtraction resynthesis, preserving each full dirty-input transfer matrix and requiring entrywise nonincrease of the reverse nonnegative transfer; same wires and frame, literal reverse cleanup.", + "coordination": "Open-issue and sprint searches found only issue 650 (discussion request), no pinned sprint coordination issue. Local claim used; no reservation issue created.", "domain": "At most the 60 phase-A quad blocks, cyclic order starting with seed modulo 60; stop at first certified strict improvement or time budget.", "expected_deliverable": "One finite circuit construction or scoped negative search receipt with exact replay, source pins and rejection controls; no kappa claim.", - "alternatives_considered": ["R489 cleanup synthesis", "R420 block factorization"], + "expected_finish": "2026-10-13T14:42:00+08:00", + "method": "Bounded exact positive-integer row-subtraction resynthesis, preserving each full dirty-input transfer matrix and requiring entrywise nonincrease of the reverse nonnegative transfer; same wires and frame, literal reverse cleanup.", + "object": "PR503/PR510 historical R480 phase-A quad circuits, starting at quad index 1", + "overlap_context": [ + 503, + 510, + 691, + 754, + 789, + 790, + 810 + ], + "result_update": { + "compare_url": "https://github.com/CrocSwap/integer-mult-bounds/compare/main...FanPUYen:integer-mult-bounds:research/r480-quad-seed1?expand=1", + "finished_utc": "2026-10-13T06:21:58.761574+00:00", + "latest_overlap_pr": 816, + "published_branch": "https://github.com/FanPUYen/integer-mult-bounds/tree/research/r480-quad-seed1/research/r480-quad-seed1", + "pull_request": null, + "refreshed_main": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "result": "R480 quad1 18->12 XORs; complete word33958->33946; exact720-column and native5/9/11-stage checks pass; paid profile unchanged; no new kappa", + "status": "completed finite construction; branch published; PR creation blocked by integration permission", + "submission_error": "GitHub create_pull_request returned403 Resource not accessible by integration; no PR created" + }, + "seed_source": "Python secrets.randbelow(100), operating-system randomness", "selection_reason": "R420 is heavily covered by current PRs. Searches for R480 and quad identify historical boundary verification but no R480 quad resynthesis.", - "coordination": "Open-issue and sprint searches found only issue 650 (discussion request), no pinned sprint coordination issue. Local claim used; no reservation issue created.", - "overlap_context": [503,510,691,754,789,790,810] + "started_utc": "2026-10-13T06:01:47Z", + "track": "bit supplier", + "verification_reserved_from": "2026-10-13T14:32:00+08:00" } diff --git a/research/r480-quad-seed1/VALIDATION.json b/research/r480-quad-seed1/VALIDATION.json index 17dba58b1e..14dce23e6e 100644 --- a/research/r480-quad-seed1/VALIDATION.json +++ b/research/r480-quad-seed1/VALIDATION.json @@ -48,6 +48,7 @@ ], "overlap_refresh": { "distinction": "R480 quad1; PR691 changes R420 quad13. No pending source imported. R480 matches only historical boundary formalizations in the final targeted query.", + "immediate_pre_submission_latest_pr_seen": 816, "latest_pr_seen": 814, "no_coordination_issue": true, "queries": [