From 19cf7a065115d28dd8ee37c0fb4b626d8ddf289a Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Tue, 20 Oct 2026 06:07:38 -0700 Subject: [PATCH] Bind explicit-width CRT shared rows to the complete padded caller --- .../crt-mixed-width-caller/COLD-REPLAY.json | 53 +++ .../crt-mixed-width-caller/CROSS-REPLAY.json | 71 ++++ research/crt-mixed-width-caller/EVIDENCE.md | 33 ++ .../INITIAL-REVIEW.json | 171 ++++++++++ .../crt-mixed-width-caller/INITIAL-REVIEW.md | 93 ++++++ .../PRIMARY-REVIEW.json | 285 ++++++++++++++++ .../crt-mixed-width-caller/PRIMARY-REVIEW.md | 69 ++++ research/crt-mixed-width-caller/PROOF.md | 200 +++++++++++ research/crt-mixed-width-caller/README.md | 87 +++++ research/crt-mixed-width-caller/RESULT.json | 221 +++++++++++++ .../crt-mixed-width-caller/SOURCE-PINS.json | 20 ++ research/crt-mixed-width-caller/SOURCES.json | 36 ++ research/crt-mixed-width-caller/TASK.json | 96 ++++++ research/crt-mixed-width-caller/VERIFY.json | 88 +++++ .../crt-mixed-width-caller/cross_check.py | 103 ++++++ .../independent_benes_oracle.py | 136 ++++++++ .../independent_mixed_oracle.py | 231 +++++++++++++ .../interface-review/COUNTEREXAMPLES.json | 79 +++++ .../INDEPENDENT-INTERFACE-REVIEW.md | 168 ++++++++++ .../interface-review/REPORT.json | 87 +++++ research/crt-mixed-width-caller/verify.py | 310 ++++++++++++++++++ 21 files changed, 2637 insertions(+) create mode 100644 research/crt-mixed-width-caller/COLD-REPLAY.json create mode 100644 research/crt-mixed-width-caller/CROSS-REPLAY.json create mode 100644 research/crt-mixed-width-caller/EVIDENCE.md create mode 100644 research/crt-mixed-width-caller/INITIAL-REVIEW.json create mode 100644 research/crt-mixed-width-caller/INITIAL-REVIEW.md create mode 100644 research/crt-mixed-width-caller/PRIMARY-REVIEW.json create mode 100644 research/crt-mixed-width-caller/PRIMARY-REVIEW.md create mode 100644 research/crt-mixed-width-caller/PROOF.md create mode 100644 research/crt-mixed-width-caller/README.md create mode 100644 research/crt-mixed-width-caller/RESULT.json create mode 100644 research/crt-mixed-width-caller/SOURCE-PINS.json create mode 100644 research/crt-mixed-width-caller/SOURCES.json create mode 100644 research/crt-mixed-width-caller/TASK.json create mode 100644 research/crt-mixed-width-caller/VERIFY.json create mode 100644 research/crt-mixed-width-caller/cross_check.py create mode 100644 research/crt-mixed-width-caller/independent_benes_oracle.py create mode 100644 research/crt-mixed-width-caller/independent_mixed_oracle.py create mode 100644 research/crt-mixed-width-caller/interface-review/COUNTEREXAMPLES.json create mode 100644 research/crt-mixed-width-caller/interface-review/INDEPENDENT-INTERFACE-REVIEW.md create mode 100644 research/crt-mixed-width-caller/interface-review/REPORT.json create mode 100644 research/crt-mixed-width-caller/verify.py diff --git a/research/crt-mixed-width-caller/COLD-REPLAY.json b/research/crt-mixed-width-caller/COLD-REPLAY.json new file mode 100644 index 0000000000..b40b4a5267 --- /dev/null +++ b/research/crt-mixed-width-caller/COLD-REPLAY.json @@ -0,0 +1,53 @@ +{ + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "reviewed_hashes": { + "PROOF.md": "ded150e3ab4da3561ac8623fd7d0041deb6f31dbf7b49a04dc19e0ba959c58d9", + "README.md": "c5126d2e1f381fe5a34b8e3350799ac4c3a58fe2def590b12ad4354da7b01ebf", + "RESULT.json": "2ba6f2e1661d8d9af0861eaf903bc596acd9bf0912b090389b1bc6d1f9898dd0", + "SOURCE-PINS.json": "e8e5c7320fb0bd1494e063eaa5aaf5f2f08562b80b72750081ea5a409eea5b1e", + "verify.py": "5e62787f3c4a8f1175ca7dea6c6b8ceff7863a3f879abd6245faf6aeb272fd45" + }, + "runs": [ + { + "argv_template": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "cwd_template": "{repository}", + "exit_code": 0, + "receipt": { + "padded_states": 16480, + "result": "PASS_EXPLICIT_WIDTH_SYNCHRONIZED_CRT_CALLER", + "row_checks": 229984 + }, + "stderr": "" + }, + { + "argv_template": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "cwd_template": "{repository}", + "exit_code": 0, + "receipt": { + "padded_states": 16480, + "result": "PASS_EXPLICIT_WIDTH_SYNCHRONIZED_CRT_CALLER", + "row_checks": 229984 + }, + "stderr": "" + } + ], + "schema_version": 1, + "scope": "exact git-free source-bound copy; no source-root override; logical caller only", + "source_inputs_checked": 3, + "status": "PASS_COLD_MIXED_CALLER_REPLAY", + "time_utc": "2026-10-20T13:04:24.760866+00:00" +} diff --git a/research/crt-mixed-width-caller/CROSS-REPLAY.json b/research/crt-mixed-width-caller/CROSS-REPLAY.json new file mode 100644 index 0000000000..dada0f14a1 --- /dev/null +++ b/research/crt-mixed-width-caller/CROSS-REPLAY.json @@ -0,0 +1,71 @@ +{ + "cross_helper_written_after_primary_read": true, + "files": { + "cross_check.py": "eb7a65c1129fe302ddf0cabb7cf73b178f905525c32b77768e2b14283c978def", + "independent_benes_oracle.py": "7a58689072b730201a6b4007f7b2524db2abff460a3116cfa42821fb2e1b63a5", + "independent_mixed_oracle.py": "8cdaedebd991fc0f73e74dd7b53e1c42f1e50d7b61e5b2e52d74134e2dafbdc4", + "verify.py": "5e62787f3c4a8f1175ca7dea6c6b8ceff7863a3f879abd6245faf6aeb272fd45" + }, + "oracle_primitives_written_before_primary_read": true, + "runs": [ + { + "argv_template": [ + "{python}", + "-I", + "-B", + "{package}/cross_check.py", + "{package}/verify.py", + "{package}/independent_mixed_oracle.py", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "cwd_template": "{repository}", + "exit_code": 0, + "receipt": { + "endpoint_sha256": "46209c8ca0f8b228236b5601150dafca35157003b507a6f6aad24aa0587489eb", + "forward_inverse_rows": 3064, + "literal_idle_specifications": 648, + "oracle_sha256": "8cdaedebd991fc0f73e74dd7b53e1c42f1e50d7b61e5b2e52d74134e2dafbdc4", + "primary_sha256": "5e62787f3c4a8f1175ca7dea6c6b8ceff7863a3f879abd6245faf6aeb272fd45", + "retained_source_sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", + "row_decoder_comparisons": 510, + "scope": "separate pre-code oracle against actual rows, including external ell/all-short and singleton cases; no E/tape theorem", + "states": 166, + "status": "PASS_PINNED_MIXED_CALLER_CROSSCHECK" + }, + "stderr": "" + }, + { + "argv_template": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/cross_check.py", + "{package}/verify.py", + "{package}/independent_mixed_oracle.py", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "cwd_template": "{repository}", + "exit_code": 0, + "receipt": { + "endpoint_sha256": "46209c8ca0f8b228236b5601150dafca35157003b507a6f6aad24aa0587489eb", + "forward_inverse_rows": 3064, + "literal_idle_specifications": 648, + "oracle_sha256": "8cdaedebd991fc0f73e74dd7b53e1c42f1e50d7b61e5b2e52d74134e2dafbdc4", + "primary_sha256": "5e62787f3c4a8f1175ca7dea6c6b8ceff7863a3f879abd6245faf6aeb272fd45", + "retained_source_sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", + "row_decoder_comparisons": 510, + "scope": "separate pre-code oracle against actual rows, including external ell/all-short and singleton cases; no E/tape theorem", + "states": 166, + "status": "PASS_PINNED_MIXED_CALLER_CROSSCHECK" + }, + "stderr": "" + } + ], + "schema_version": 1, + "scope": "bounded actual-row and two-sided endpoint comparison using the earlier independent compiler/bruteCRT oracle; no tape/E theorem", + "status": "PASS_PINNED_MIXED_CROSS_REPLAY", + "time_utc": "2026-10-20T13:06:30.039871+00:00" +} diff --git a/research/crt-mixed-width-caller/EVIDENCE.md b/research/crt-mixed-width-caller/EVIDENCE.md new file mode 100644 index 0000000000..463e0fdd5d --- /dev/null +++ b/research/crt-mixed-width-caller/EVIDENCE.md @@ -0,0 +1,33 @@ +# Review and replay boundary + +This package has a written all-size logical caller argument in PROOF.md. +Finite exhaustiveness is corroboration for the named rectangles, not an +all-size proof, physical implementation, full evaluator or new kappa. + +The six registered VERIFY.json commands run primary, preimplementation +independent oracle and pinned direct comparison in normal and optimized +Python. Default execution checks stored evidence without regenerating it. + +The separate FIFO compiler and brute scaled-CRT oracle were written before +reading the primary caller. INITIAL-REVIEW.md/json preserve that evidence. +The oracle's wider fixture uses ell=max(widths); the pinned direct crosscheck +additionally checks the submitted external ell=4 all-short fixture, both +literal idle rows, microscopic padding and the singleton identity caller. +Their different row counts therefore describe different explicit fixtures, +while their complete padded endpoint digests agree. + +The independent interface review is retained in interface-review/. +Its read-only report binds the exact primary five files inspected; it +provides mathematical/interface review, not a second implemented oracle. + +Every code helper referenced by these receipts is included. Root source +inputs stay byte-for-byte pinned through SOURCES.json/SOURCE-PINS.json. +Host arrays, caches, Python arithmetic and schedule event counts are not +fixed-tape machine steps. Actual placement, compact repair, ordinary callee, +complete E generation, precision/native/outer integration and independent +human or formal-kernel acceptance remain open. + +Credit: Cinna Davis's source CRT/Beneš work, Hiroki KUMAZAKI's PR4169/4174 +omission, inverse and placement work, Douglas Colkitt/OpenAI framework and +the retained source NOTICE lineage. Substantial OpenAI Codex assistance; +the separate reviewers are agents, not independent human reviewers. diff --git a/research/crt-mixed-width-caller/INITIAL-REVIEW.json b/research/crt-mixed-width-caller/INITIAL-REVIEW.json new file mode 100644 index 0000000000..15028b835f --- /dev/null +++ b/research/crt-mixed-width-caller/INITIAL-REVIEW.json @@ -0,0 +1,171 @@ +{ + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "before_primary_read": true, + "files": { + "INITIAL-REVIEW.md": "1e3537438f133b734b04113a68f74e68760c938ad370a4e55db783b21943f5f5", + "independent_benes_oracle.py": "7a58689072b730201a6b4007f7b2524db2abff460a3116cfa42821fb2e1b63a5", + "independent_mixed_oracle.py": "8cdaedebd991fc0f73e74dd7b53e1c42f1e50d7b61e5b2e52d74134e2dafbdc4" + }, + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "runs": [ + { + "argv_template": [ + "{python}", + "-I", + "-B", + "{package}/independent_mixed_oracle.py" + ], + "cwd_template": "{repository}", + "exit_code": 0, + "receipt": { + "compiler_sha256": "7a58689072b730201a6b4007f7b2524db2abff460a3116cfa42821fb2e1b63a5", + "negative_controls": { + "current_target_validity_gate": { + "expected": 2, + "input": 1, + "literal_trace": [ + 1, + 1, + 3, + 2 + ], + "modulus": 3, + "offset": 1, + "size": 4, + "wrong": 3 + }, + "low_minimal_width_substitution": { + "declared_size": 8, + "expected": 5, + "input": 5, + "modulus": 3, + "offset": 1, + "wrong": 6 + } + }, + "rectangles": [ + { + "active_target_omission_checks": 1638400, + "declared_widths": [ + 3, + 3, + 4, + 4 + ], + "dirty_columns": 16384, + "endpoint_sha256": "e4c5785f980c0918c32f70bcf40f2e24fe22c48be62e48a3ca1e40b6454a7f20", + "forward_inverse_global_rows": 458752, + "moduli": [ + 5, + 7, + 11, + 13 + ], + "valid_columns": 5005 + }, + { + "active_target_omission_checks": 640, + "declared_widths": [ + 3, + 3 + ], + "dirty_columns": 64, + "endpoint_sha256": "bb2d516611ac14374aa271977df68a398c6e70c91ef1e4d2a9aa6e01b9740083", + "forward_inverse_global_rows": 640, + "moduli": [ + 5, + 3 + ], + "valid_columns": 15 + } + ], + "scope": "independent mixed-row caller and brute scaled-CRT oracle; predecessor omission argument reused; no tape/E theorem", + "status": "PASS_PREIMPLEMENTATION_MIXED_CALLER_ORACLE" + }, + "stderr": "" + }, + { + "argv_template": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent_mixed_oracle.py" + ], + "cwd_template": "{repository}", + "exit_code": 0, + "receipt": { + "compiler_sha256": "7a58689072b730201a6b4007f7b2524db2abff460a3116cfa42821fb2e1b63a5", + "negative_controls": { + "current_target_validity_gate": { + "expected": 2, + "input": 1, + "literal_trace": [ + 1, + 1, + 3, + 2 + ], + "modulus": 3, + "offset": 1, + "size": 4, + "wrong": 3 + }, + "low_minimal_width_substitution": { + "declared_size": 8, + "expected": 5, + "input": 5, + "modulus": 3, + "offset": 1, + "wrong": 6 + } + }, + "rectangles": [ + { + "active_target_omission_checks": 1638400, + "declared_widths": [ + 3, + 3, + 4, + 4 + ], + "dirty_columns": 16384, + "endpoint_sha256": "e4c5785f980c0918c32f70bcf40f2e24fe22c48be62e48a3ca1e40b6454a7f20", + "forward_inverse_global_rows": 458752, + "moduli": [ + 5, + 7, + 11, + 13 + ], + "valid_columns": 5005 + }, + { + "active_target_omission_checks": 640, + "declared_widths": [ + 3, + 3 + ], + "dirty_columns": 64, + "endpoint_sha256": "bb2d516611ac14374aa271977df68a398c6e70c91ef1e4d2a9aa6e01b9740083", + "forward_inverse_global_rows": 640, + "moduli": [ + 5, + 3 + ], + "valid_columns": 15 + } + ], + "scope": "independent mixed-row caller and brute scaled-CRT oracle; predecessor omission argument reused; no tape/E theorem", + "status": "PASS_PREIMPLEMENTATION_MIXED_CALLER_ORACLE" + }, + "stderr": "" + } + ], + "schema_version": 1, + "scope": "literal mixed-height caller semantics; predecessor omission argument reused; no full E/tape theorem", + "status": "PASS_PREIMPLEMENTATION_MIXED_CALLER_REVIEW", + "time_utc": "2026-10-20T12:59:43.996931+00:00" +} diff --git a/research/crt-mixed-width-caller/INITIAL-REVIEW.md b/research/crt-mixed-width-caller/INITIAL-REVIEW.md new file mode 100644 index 0000000000..fe0470ce40 --- /dev/null +++ b/research/crt-mixed-width-caller/INITIAL-REVIEW.md @@ -0,0 +1,93 @@ +# Independent preimplementation mixed-width caller review + +Context: canonical main `12fa8c5c844be21bfefb38a19503fbd867a11244`, +priority 7, Cinna Davis's retained PR4100 CRT construction. Primary caller +code was not read before this oracle and analysis. The all-active-target +omission argument is predecessor coverage in PR4169/PR4174, not new here. + +## Declared widths and literal row embedding + +For a supplied global ell>=2 and each declared height h in {ell-1,ell}, +the full local Beneš program has 2h-1 rows on exactly 2^h wires. For h=ell +use local row r at global row r. For h=ell-1 put it at + + e(r)=r when r<=ell-2, and e(r)=r+2 otherwise. + +The omitted global rows are exactly ell-1 and ell. The map is strictly +increasing and injective into 0,...,2ell-2. Comparing the ascending and +descending portions of the universal bit sequence shows that each active +local row targets the same numerical bit as its global row. The idle rows +are identities; they must not read the nonexistent high bit of a short axis. + +The global ell convention must be explicit. If it is supplied separately +and every axis is short, preserve both all-idle rows. Replacing source ell +by max(h_i) silently would alter its literal schedule and potentially its +separate guard parameters. The finite oracle's two named fixtures choose +ell=max(h_i); its row embedding is checked independently for ell=2,...,64. + +## Caller correctness and reused omission argument + +Fix a balanced tree level. Its nodes are disjoint. Every active target lies +in a node's right child, and every numerical shift is determined only by +that node's left-child coordinates and fixed moduli. None of those left +coordinates is an active target at this level, so all shifts remain constant +through every global row. A switch table omits its own target bit, and reads +only its own other bits plus these unchanged left controls. It consequently +omits all active target bits, and simultaneous/serial target applications +commute. This is the predecessor argument, now applied to the declared row +embedding; placement, raw macros and repair remain separate. + +Completing the rows applies each axis's full declared-size modular rotation, +which fixes every target value >= its modulus at the endpoint. Intermediate +wire labels need not stay valid. Tree levels compose to the retained padded +balanced map. On globally valid tuples this equals the direct scaled-CRT +map. To invert the literal program, reverse tree levels and global rows, +using the same positive-offset tables from the current unchanged left child. +Every individual switch is an involution. No initialization of padded fields +or control values is assumed. + +Two tempting lowerings are invalid. Gating each microscopic switch on current +target validity can suppress the rest of a path that temporarily enters +padded labels. Replacing the declared-size network by a minimal-width network +on low bits can move invalid labels in the larger declared field. These are +mutation counterexamples, not claims of bugs in the retained predecessors. + +## Separate oracle evidence + +`independent_mixed_oracle.py` uses the earlier separate FIFO Beneš compiler, +retained byte-for-byte as `independent_benes_oracle.py` and authenticated by +SHA256. It reconstructs left-child scaled CRT integers by exhaustive search, +rather than calling the retained `decode_group` or primary implementation. +An atomic numerical rotation model and the direct globally valid CRT formula +are separate endpoint references. + +Before primary inspection, ordinary replay passed: + +- Moduli (5,7,11,13), declared heights (3,3,4,4): all 16,384 dirty tuples, + 5,005 valid tuples, 458,752 forward/inverse global-row executions, and + 1,638,400 active-target omission comparisons. +- Moduli (5,3), declared heights (3,3): all 64 dirty tuples, 15 valid tuples, + 640 forward/inverse global-row executions and 640 omission comparisons. + +Both padded endpoint maps are bijective, preserve the globally valid set, +agree with atomic rotations, and return every tuple under the literal inverse. +The first validity-gate witness is size4, s=3, c=1, x=1 with literal trace +(1,1,3,2): gated output3 differs from required2. The minimal-low-bit witness +is declared size8, s=3, c=1, x=5: wrong6 instead of fixed5. + +The oracle uses host arrays, caches and brute arithmetic. It is semantic +corroboration, not a fixed-tape, full E evaluator, raw macro, native/precision, +outer multiplication theorem or new-kappa certificate. Separate-agent Codex +review is not independent human review or proof-assistant verification. + +## Credit and remaining obligations + +Cinna Davis supplies PR4100's CRT factorization and source networks. PR4169 +and Hiroki KUMAZAKI's PR4174 retain credit for the simultaneous omission and +placement arguments. The unchanged earlier FIFO oracle supplies numerical +network semantics; no new Beneš routing mechanism is claimed. + +Remaining work includes the complete E evaluator, production reservoir and +exception classification, ordinary callee, raw compact macro/repair tariff, +and full numerical/native/outer theorem integration. Selected-frontier +certification remains outside scope. diff --git a/research/crt-mixed-width-caller/PRIMARY-REVIEW.json b/research/crt-mixed-width-caller/PRIMARY-REVIEW.json new file mode 100644 index 0000000000..ced31a243e --- /dev/null +++ b/research/crt-mixed-width-caller/PRIMARY-REVIEW.json @@ -0,0 +1,285 @@ +{ + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "credit": "Cinna Davis PR4100; Hiroki KUMAZAKI PR4169/PR4174; retained source NOTICE and earlier separate FIFO oracle; substantial OpenAI Codex assistance, not independent human review", + "cross_helper_after_primary_read": true, + "evidence": { + "cold_replay": [ + { + "argv_template": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "cwd_template": "{repository}", + "exit_code": 0, + "receipt": { + "padded_states": 16480, + "result": "PASS_EXPLICIT_WIDTH_SYNCHRONIZED_CRT_CALLER", + "row_checks": 229984 + }, + "stderr": "" + }, + { + "argv_template": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "cwd_template": "{repository}", + "exit_code": 0, + "receipt": { + "padded_states": 16480, + "result": "PASS_EXPLICIT_WIDTH_SYNCHRONIZED_CRT_CALLER", + "row_checks": 229984 + }, + "stderr": "" + } + ], + "pinned_cross_replay": [ + { + "argv_template": [ + "{python}", + "-I", + "-B", + "{package}/cross_check.py", + "{package}/verify.py", + "{package}/independent_mixed_oracle.py", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "cwd_template": "{repository}", + "exit_code": 0, + "receipt": { + "endpoint_sha256": "46209c8ca0f8b228236b5601150dafca35157003b507a6f6aad24aa0587489eb", + "forward_inverse_rows": 3064, + "literal_idle_specifications": 648, + "oracle_sha256": "8cdaedebd991fc0f73e74dd7b53e1c42f1e50d7b61e5b2e52d74134e2dafbdc4", + "primary_sha256": "5e62787f3c4a8f1175ca7dea6c6b8ceff7863a3f879abd6245faf6aeb272fd45", + "retained_source_sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", + "row_decoder_comparisons": 510, + "scope": "separate pre-code oracle against actual rows, including external ell/all-short and singleton cases; no E/tape theorem", + "states": 166, + "status": "PASS_PINNED_MIXED_CALLER_CROSSCHECK" + }, + "stderr": "" + }, + { + "argv_template": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/cross_check.py", + "{package}/verify.py", + "{package}/independent_mixed_oracle.py", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "cwd_template": "{repository}", + "exit_code": 0, + "receipt": { + "endpoint_sha256": "46209c8ca0f8b228236b5601150dafca35157003b507a6f6aad24aa0587489eb", + "forward_inverse_rows": 3064, + "literal_idle_specifications": 648, + "oracle_sha256": "8cdaedebd991fc0f73e74dd7b53e1c42f1e50d7b61e5b2e52d74134e2dafbdc4", + "primary_sha256": "5e62787f3c4a8f1175ca7dea6c6b8ceff7863a3f879abd6245faf6aeb272fd45", + "retained_source_sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", + "row_decoder_comparisons": 510, + "scope": "separate pre-code oracle against actual rows, including external ell/all-short and singleton cases; no E/tape theorem", + "states": 166, + "status": "PASS_PINNED_MIXED_CALLER_CROSSCHECK" + }, + "stderr": "" + } + ], + "preimplementation_oracle": [ + { + "argv_template": [ + "{python}", + "-I", + "-B", + "{package}/independent_mixed_oracle.py" + ], + "cwd_template": "{repository}", + "exit_code": 0, + "receipt": { + "compiler_sha256": "7a58689072b730201a6b4007f7b2524db2abff460a3116cfa42821fb2e1b63a5", + "negative_controls": { + "current_target_validity_gate": { + "expected": 2, + "input": 1, + "literal_trace": [ + 1, + 1, + 3, + 2 + ], + "modulus": 3, + "offset": 1, + "size": 4, + "wrong": 3 + }, + "low_minimal_width_substitution": { + "declared_size": 8, + "expected": 5, + "input": 5, + "modulus": 3, + "offset": 1, + "wrong": 6 + } + }, + "rectangles": [ + { + "active_target_omission_checks": 1638400, + "declared_widths": [ + 3, + 3, + 4, + 4 + ], + "dirty_columns": 16384, + "endpoint_sha256": "e4c5785f980c0918c32f70bcf40f2e24fe22c48be62e48a3ca1e40b6454a7f20", + "forward_inverse_global_rows": 458752, + "moduli": [ + 5, + 7, + 11, + 13 + ], + "valid_columns": 5005 + }, + { + "active_target_omission_checks": 640, + "declared_widths": [ + 3, + 3 + ], + "dirty_columns": 64, + "endpoint_sha256": "bb2d516611ac14374aa271977df68a398c6e70c91ef1e4d2a9aa6e01b9740083", + "forward_inverse_global_rows": 640, + "moduli": [ + 5, + 3 + ], + "valid_columns": 15 + } + ], + "scope": "independent mixed-row caller and brute scaled-CRT oracle; predecessor omission argument reused; no tape/E theorem", + "status": "PASS_PREIMPLEMENTATION_MIXED_CALLER_ORACLE" + }, + "stderr": "" + }, + { + "argv_template": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent_mixed_oracle.py" + ], + "cwd_template": "{repository}", + "exit_code": 0, + "receipt": { + "compiler_sha256": "7a58689072b730201a6b4007f7b2524db2abff460a3116cfa42821fb2e1b63a5", + "negative_controls": { + "current_target_validity_gate": { + "expected": 2, + "input": 1, + "literal_trace": [ + 1, + 1, + 3, + 2 + ], + "modulus": 3, + "offset": 1, + "size": 4, + "wrong": 3 + }, + "low_minimal_width_substitution": { + "declared_size": 8, + "expected": 5, + "input": 5, + "modulus": 3, + "offset": 1, + "wrong": 6 + } + }, + "rectangles": [ + { + "active_target_omission_checks": 1638400, + "declared_widths": [ + 3, + 3, + 4, + 4 + ], + "dirty_columns": 16384, + "endpoint_sha256": "e4c5785f980c0918c32f70bcf40f2e24fe22c48be62e48a3ca1e40b6454a7f20", + "forward_inverse_global_rows": 458752, + "moduli": [ + 5, + 7, + 11, + 13 + ], + "valid_columns": 5005 + }, + { + "active_target_omission_checks": 640, + "declared_widths": [ + 3, + 3 + ], + "dirty_columns": 64, + "endpoint_sha256": "bb2d516611ac14374aa271977df68a398c6e70c91ef1e4d2a9aa6e01b9740083", + "forward_inverse_global_rows": 640, + "moduli": [ + 5, + 3 + ], + "valid_columns": 15 + } + ], + "scope": "independent mixed-row caller and brute scaled-CRT oracle; predecessor omission argument reused; no tape/E theorem", + "status": "PASS_PREIMPLEMENTATION_MIXED_CALLER_ORACLE" + }, + "stderr": "" + } + ] + }, + "material_blockers": [], + "predecessor_coverage": "All-active-target omission and placement are credited PR4169/PR4174, not claimed new.", + "preimplementation_oracle_before_primary_read": true, + "remaining_obligations": [ + "full uniform E evaluator and transported source descriptors", + "production reservoir and exceptional-target integration", + "ordinary callee and raw compact macro/repair tariff", + "precision/native/outer multiplication theorem and frontier certification" + ], + "resolved_domain_point": "Global ell is supplied and is not silently normalized to max widths; all-short fixture retains both idles.", + "review_artifacts": { + "PRIMARY-REVIEW.md": "443335f0bfaec4fa6c5625cef2e8e82d2df91c8b953f25eb86e7c511c697219b", + "cross_check.py": "eb7a65c1129fe302ddf0cabb7cf73b178f905525c32b77768e2b14283c978def", + "independent_benes_oracle.py": "7a58689072b730201a6b4007f7b2524db2abff460a3116cfa42821fb2e1b63a5", + "independent_mixed_oracle.py": "8cdaedebd991fc0f73e74dd7b53e1c42f1e50d7b61e5b2e52d74134e2dafbdc4" + }, + "reviewed_hashes": { + "PROOF.md": "ded150e3ab4da3561ac8623fd7d0041deb6f31dbf7b49a04dc19e0ba959c58d9", + "README.md": "c5126d2e1f381fe5a34b8e3350799ac4c3a58fe2def590b12ad4354da7b01ebf", + "RESULT.json": "2ba6f2e1661d8d9af0861eaf903bc596acd9bf0912b090389b1bc6d1f9898dd0", + "SOURCE-PINS.json": "e8e5c7320fb0bd1494e063eaa5aaf5f2f08562b80b72750081ea5a409eea5b1e", + "verify.py": "5e62787f3c4a8f1175ca7dea6c6b8ceff7863a3f879abd6245faf6aeb272fd45" + }, + "schema_version": 1, + "scope": "literal declared-width global/local row caller and all-padded balanced endpoints/inverse; canonical logical coordinates only", + "status": "PASS_INDEPENDENT_MIXED_CALLER_REVIEW", + "time_utc": "2026-10-20T13:06:30.116374+00:00" +} diff --git a/research/crt-mixed-width-caller/PRIMARY-REVIEW.md b/research/crt-mixed-width-caller/PRIMARY-REVIEW.md new file mode 100644 index 0000000000..5887d1c8f3 --- /dev/null +++ b/research/crt-mixed-width-caller/PRIMARY-REVIEW.md @@ -0,0 +1,69 @@ +# Independent review of the explicit-width synchronized CRT caller + +Verdict: **pass within its logical caller scope**. No unresolved correctness +issue was found. The exact primary proof, code, source pins and result hashes +are recorded in `PRIMARY-REVIEW.json`. Separate-agent review is not independent +human review or proof-assistant verification. + +## Findings + +- The constructor takes ell explicitly and preserves declared widths. In + particular, the wider-padding fixture uses ell=4 with both heights3 and + retains both all-idle global rows instead of normalizing ell down. +- The row decoder correctly maps all local rows once in order. The short + network idles at globals ell-1 and ell. IDLE is represented by None and + branches before both target selection and table lookup; no phantom bit + with a zero coefficient is introduced. +- Per-axis networks use exactly 2^h_i wires. Offsets depend only on the + unchanged left child and fixed moduli. Those offsets are frozen for the + level, while each later table is queried at the current axis value. + The predecessor all-active-target omission argument therefore applies. + This argument and placement coverage are credited to PR4169/PR4174. +- Different target axes commute throughout a level. Removing idle rows + preserves each axis's complete local word, so interleaving realizes the + same endpoint as the retained serial arithmetic caller on every padded + tuple. The globally valid restriction gives the direct CRT map. +- Reversing levels and global rows uses the same positive-offset tables + in reverse order. This is the literal inverse. It agrees in endpoint + with the source's separately compiled negative-offset construction. +- Whole-network valid-set preservation is distinguished from transient + target validity and from pointwise fixation of globally invalid tuples. + The mutation with path (1,1,3,2) detects incorrect per-switch validity + gating. The wider-input compiled-helper failure is correctly described + as an API-domain boundary, not a predecessor theorem defect. +- Coordinates are canonical logical axes. No executed reservoir placement, + compact macro/repair, tape/E tariff or full physical CRT theorem is claimed. + +## Evidence + +Before primary inspection, the independent oracle used an earlier separate +FIFO network compiler and brute-force scaled-CRT reconstruction. Normal and +strict optimized runs covered all16,384 main dirty tuples and all64 wider +padding tuples, whole literal inverses, commutation/omission comparisons and +the direct globally valid formula. It remains byte-pinned and unchanged. + +The primary was replayed normally and under strict optimization from a +separate git-free copy with its three authenticated source inputs, without +source-root overrides. Both reproduced16,480 padded states and229,984 +forward row checks. The stored receipt was compared without rewriting it. + +The source-pinned `cross_check.py` was written after primary inspection to +apply the earlier oracle primitives. Both modes passed166 states,3,064 +forward/inverse rows,510 decoder comparisons and648 literal idle specs. +It includes supplied-ell/all-short fixtures and singleton axes. It validates +the hashes of primary code, preimplementation oracle and retained source; +the preimplementation oracle also authenticates its earlier FIFO helper. +All referenced helpers are retained beside the receipts. + +The independent full main and wider-padding endpoint digests agree with the +primary results. These are semantic checks, not machine timing evidence. + +## Remaining obligations and credit + +The complete uniform control evaluator, transported descriptors, production +reservoir and exception-set binding, ordinary callee, compact repair tariff, +precision/native/outer multiplication theorem and frontier certification +remain separate. Cinna Davis supplies the original CRT/network construction; +Hiroki KUMAZAKI's PR4169/PR4174 supplies existing omission/repair/placement +coverage. The unchanged earlier FIFO oracle supplies independent numerical +network semantics. No new kappa or selected-frontier change is asserted. diff --git a/research/crt-mixed-width-caller/PROOF.md b/research/crt-mixed-width-caller/PROOF.md new file mode 100644 index 0000000000..090d331da8 --- /dev/null +++ b/research/crt-mixed-width-caller/PROOF.md @@ -0,0 +1,200 @@ +# Explicit-width synchronized balanced CRT caller + +This binds Cinna Davis's PR4100 `CRT.md:76–92` to a literal global-row +decoder and a whole balanced-tree caller. The CRT factorization and +Beneš compiler are predecessor work. All-active-target omission is +already established in Hiroki KUMAZAKI's PR4169 `PROOF.md:304–334` +and assumed by PR4174's placement audit `PROOF.md:44–50`; it is not +a new theorem claimed here. The addition is the explicit-width +row/idle interface and its executable complete caller binding. + +## 1. Domain and coordinate convention + +Let d>=1 be a power of two and ell>=2. Axis i has declared width +`h_i in {ell-1,ell}` and modulus `2<=s_i<2^h_i`. All moduli are +pairwise coprime. Every tuple in + +``` +D = product_(i=0)^(d-1) {0,...,2^h_i-1} +``` + +is present, including arbitrary invalid padded values. No coordinate +is initialized. A tuple is globally valid exactly when every x_i=2, removing IDLE gives exactly +`0,...,2(ell-1)-2` in order, once each. In a nonidle row, +`q_(ell-1)(local(g))=q_ell(g)` and the bit lies inside the declared +axis. For the long width the same facts are immediate. + +IDLE has **no local row, no target bit and no table query**. It does +not refer to a nonexistent high bit with zero control. The implementation +represents it by `(axis,None,None,0)` and branches before table access. +Equation (1) is a particular explicit embedding, not a claim that no +other correctly specified interleaving could work. + +For an axis of width h_i, compile the permutation on its entire existing +`2^h_i` coordinates: + +``` +R_(i,c)(x) = (x+c) mod s_i if x=2, +pairwise coprime `2<=s_i<2^h_i`, and declared widths +`h_i in {ell-1,ell}`. Long axes use every global row. Short axes have +two literal idles, with **no target bit or table query**. Removing +idles recovers each source word exactly in order. Declared coordinate +widths are never silently shrunk to fit their moduli. + +The synchronized whole tree equals the retained arithmetic CRT +caller on every padded tuple. Reversing levels and rows gives its +inverse. Valid padding is preserved at whole-network/level endpoints; +intermediate switches can legitimately pass through invalid target +values. Globally invalid tuples are permuted bijectively and need +not be pointwise fixed. + +## Evidence and reproduction + +[verify.py](verify.py) authenticates the three predecessor inputs in +[SOURCE-PINS.json](SOURCE-PINS.json) by SHA256 and Git blob and compiles +those exact bytes, without cached predecessor bytecode. It reproduces +[RESULT.json](RESULT.json), covering: + +- All **16,384** padded tuples for moduli `(5,7,11,13)` and widths + `(3,3,4,4)`, including all **5,005** globally valid tuples, two tree + levels and genuinely mixed simultaneous target heights. +- All **64** tuples with moduli `(5,3)` and wider declared widths + `(3,3)`, retaining dirty values beyond the minimal target table. + Supplied ell=4 deliberately makes every axis short; its two idle + rows remain present rather than normalizing ell down to max width. +- All **32** tuples with moduli `(7,3)` and widths `(3,2)`, binding + the microscopic invalid-target mutation to a genuine CRT caller. +- Whole forward/inverse source comparisons, both inverse compositions, + distinct destinations covering each full rectangle, actual-row target + omission toggles and literal idle checks. Decoder checks cover + ell=2 through16; the written proof is quantified for all ell>=2. + +The main mutation returns `(1,3)` instead of `(1,2)` when it incorrectly +disables a micro-switch after the target temporarily becomes invalid. +Another witness prevents claiming that all globally invalid tuples +are pointwise fixed. Input controls reject malformed width, row, +axis-count, coprimality and strict-padding declarations. The minimal-width +compiled source helper is used only within its own width domain; +its wider-input failure is documented as a finite API boundary. + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -B research/crt-mixed-width-caller/verify.py +python3.12 -I -O -W error -B research/crt-mixed-width-caller/verify.py +``` + +Default verification reproduces and compares the stored receipt without +rewriting it. `--write-result` explicitly regenerates it. All checks +remain active under optimized Python. + +## Open next questions + +Bind the decoded rows and explicit declared widths to the full uniform +control evaluator, including CRT reconstruction/modular inverses, +transported split-axis descriptors, current intermediate states, +cleanup and head returns. The earlier sequential Beneš component +addresses one part of that tariff; this host caller does not price it. + +The fixtures use canonical logical axes, without executing reservoir +placement, compact repair or an ordinary interchange. No tape/E tariff, +full physical CRT implementation, precision/native/outer theorem or +new kappa is claimed. The selected frontier is unchanged. + +## Credit + +Cinna Davis supplies PR4100's CRT/network construction. Hiroki +KUMAZAKI (@kumagi), PR4169/4174, supplies the existing arbitrary-source +inverse/omission and reservoir/descriptor audits. Douglas Colkitt, +OpenAI and the retained routing/compact-control lineage keep their +predecessor credit; the pinned NOTICE preserves the source details. +New work is the explicit row/idle/declared-width caller binding and +its independent corroboration. Prepared with substantial OpenAI Codex +assistance. Apache-2.0. No independent human review or proof-assistant +formalization is claimed. diff --git a/research/crt-mixed-width-caller/RESULT.json b/research/crt-mixed-width-caller/RESULT.json new file mode 100644 index 0000000000..34b757851a --- /dev/null +++ b/research/crt-mixed-width-caller/RESULT.json @@ -0,0 +1,221 @@ +{ + "schema_version": 1, + "result": "PASS_EXPLICIT_WIDTH_SYNCHRONIZED_CRT_CALLER", + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "source_inputs_checked": 3, + "decoder": { + "ell_values": [ + 2, + 16 + ], + "height_cases": 30, + "literal_idles": 30, + "proof_scope": "all integer ell>=2; finite decoder check is corroboration" + }, + "fixtures": [ + { + "name": "mixed_four_axis", + "domain": "canonical logical axes; no reservoir placement or physical macro executed", + "hash_input_order": "lexicographic logical tuples, axis0 outermost; packed axis0 is least significant", + "hash_destination_encoding": "ceil(L/8) bytes per packed destination, big endian", + "moduli": [ + 5, + 7, + 11, + 13 + ], + "widths": [ + 3, + 3, + 4, + 4 + ], + "ell": 4, + "axes": 4, + "address_bits": 14, + "tree_levels": 2, + "global_rows_per_level": 7, + "padded_states": 16384, + "valid_states": 5005, + "invalid_states": 11379, + "forward_row_checks": 229376, + "actual_row_omission_toggles": 425984, + "literal_idle_checks": 32768, + "minimal_width_compiled_source_checks": 16384, + "changed_invalid_tuple": { + "input": [ + 0, + 1, + 0, + 13 + ], + "output": [ + 0, + 1, + 8, + 13 + ] + }, + "forward_permutation_sha256": "e4c5785f980c0918c32f70bcf40f2e24fe22c48be62e48a3ca1e40b6454a7f20", + "inverse_permutation_sha256": "b3e5ee89890cec9aff0e1ffe5453c297c1f208972261be8ddc43133fe4af6a8f" + }, + { + "name": "declared_wider_padding", + "domain": "canonical logical axes; no reservoir placement or physical macro executed", + "hash_input_order": "lexicographic logical tuples, axis0 outermost; packed axis0 is least significant", + "hash_destination_encoding": "ceil(L/8) bytes per packed destination, big endian", + "moduli": [ + 5, + 3 + ], + "widths": [ + 3, + 3 + ], + "ell": 4, + "axes": 2, + "address_bits": 6, + "tree_levels": 1, + "global_rows_per_level": 7, + "padded_states": 64, + "valid_states": 15, + "invalid_states": 49, + "forward_row_checks": 448, + "actual_row_omission_toggles": 320, + "literal_idle_checks": 128, + "minimal_width_compiled_source_checks": 0, + "changed_invalid_tuple": null, + "forward_permutation_sha256": "bb2d516611ac14374aa271977df68a398c6e70c91ef1e4d2a9aa6e01b9740083", + "inverse_permutation_sha256": "be78619e09de3a6fe9500f8efc7468bc6dc2992593512c7b51a97cd5924ffa06" + }, + { + "name": "microscopic_padding_validity", + "domain": "canonical logical axes; no reservoir placement or physical macro executed", + "hash_input_order": "lexicographic logical tuples, axis0 outermost; packed axis0 is least significant", + "hash_destination_encoding": "ceil(L/8) bytes per packed destination, big endian", + "moduli": [ + 7, + 3 + ], + "widths": [ + 3, + 2 + ], + "ell": 3, + "axes": 2, + "address_bits": 5, + "tree_levels": 1, + "global_rows_per_level": 5, + "padded_states": 32, + "valid_states": 21, + "invalid_states": 11, + "forward_row_checks": 160, + "actual_row_omission_toggles": 96, + "literal_idle_checks": 64, + "minimal_width_compiled_source_checks": 32, + "changed_invalid_tuple": null, + "forward_permutation_sha256": "b5842c1be9dfb835d761dbbcdb541dc417b12daf5a884aa9bf5b83706bf78ea0", + "inverse_permutation_sha256": "b33f88785bcae18fec6703cc8ee4b0aeb741aed5ba652a446adecbc848a9f930" + } + ], + "negative_controls": { + "target_validity_mutant": { + "moduli": [ + 7, + 3 + ], + "widths": [ + 3, + 2 + ], + "ell": 3, + "input": [ + 1, + 1 + ], + "correct": [ + 1, + 2 + ], + "wrong": [ + 1, + 3 + ], + "trace_before_rows": [ + { + "global_row": 0, + "before": [ + 1, + 1 + ], + "local_row": 0, + "target": 0 + }, + { + "global_row": 1, + "before": [ + 1, + 1 + ], + "local_row": 1, + "target": 1 + }, + { + "global_row": 2, + "before": [ + 1, + 3 + ], + "local_row": null, + "target": null + }, + { + "global_row": 3, + "before": [ + 1, + 3 + ], + "local_row": null, + "target": null + }, + { + "global_row": 4, + "before": [ + 1, + 3 + ], + "local_row": 2, + "target": 0 + } + ] + }, + "source_helper_api_boundary": "minimal-width finite source helper cannot index declared wider dirty target", + "invalid_pointwise_fixation_counterexample": { + "input": [ + 5, + 0, + 1, + 0 + ], + "output": [ + 5, + 0, + 1, + 6 + ] + }, + "admission_rejections": [ + "width outside ell-1/ell", + "global row outside schedule", + "non-power-of-two axes", + "noncoprime moduli", + "missing strict dyadic padding" + ] + }, + "limitations": [ + "Quantified caller/decoder proof is separate from finite corroboration.", + "All-target omission is predecessor coverage; this binds literal mixed-width rows.", + "Canonical logical-axis host model only; no reservoir or physical compact macro executed.", + "No tape/E tariff, full CRT implementation, precision/native/outer theorem or new kappa." + ] +} diff --git a/research/crt-mixed-width-caller/SOURCE-PINS.json b/research/crt-mixed-width-caller/SOURCE-PINS.json new file mode 100644 index 0000000000..f4c01fc0ec --- /dev/null +++ b/research/crt-mixed-width-caller/SOURCE-PINS.json @@ -0,0 +1,20 @@ +[ + { + "path": "research/unconditional-batched-crt/CRT.md", + "size": 15699, + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b", + "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "size": 11520, + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc" + }, + { + "path": "research/unconditional-batched-crt/NOTICE.md", + "size": 2380, + "sha256": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461", + "git_blob": "886a8fdee275f01b459cbd68ae2815dc9269502f" + } +] diff --git a/research/crt-mixed-width-caller/SOURCES.json b/research/crt-mixed-width-caller/SOURCES.json new file mode 100644 index 0000000000..3cd7684219 --- /dev/null +++ b/research/crt-mixed-width-caller/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/unconditional-batched-crt/CRT.md", + "usage": "input", + "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6", + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b" + }, + { + "path": "research/unconditional-batched-crt/NOTICE.md", + "usage": "input", + "git_blob": "886a8fdee275f01b459cbd68ae2815dc9269502f", + "sha256": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "usage": "input", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + } + ] +} diff --git a/research/crt-mixed-width-caller/TASK.json b/research/crt-mixed-width-caller/TASK.json new file mode 100644 index 0000000000..771b8fda25 --- /dev/null +++ b/research/crt-mixed-width-caller/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Bind the PR4100 balanced CRT caller to explicit declared axis widths h_i in {ell-1,ell}, literal global/local row and idle decoding, current-state controls and reverse level/row execution on every padded tuple.", + "scope_change_reason": "The live CRT evaluator handoff and actual PR4169/4174 sources leave a concrete mixed-width whole-tree row decoder unexecuted. Their omission, compact inverse and placement results remain predecessor work; this isolates the logical caller interface.", + "bottleneck_link": "The full control evaluator must know which actual axis bit is targeted at each shared row. An explicit declared-width and idle interface prevents silent width shrinking or invalid intermediate-state gating before physical lowering.", + "budget_minutes": 60, + "stop_rule": "Stop science by2026-10-20T13:36:14Z and reserve final15minutes until13:51:14Z for source/history, cold/hosted verification, refreshed main/overlap and handoff. Stop at one logical caller implication; no full E/tape or native/outer claim.", + "outcome": "completed", + "evidence": "PROOF.md gives the quantified row embedding and whole-tree endpoint/inverse argument. RESULT.json covers all16384 mixed-width padded tuples plus64 wider-declared and32 microscopic states; independent FIFO/brute-CRT oracle and interface reviews retained.", + "author": "ToikY, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance from a primary implementation agent, independent FIFO/brute-CRT oracle agent, separate interface/proof reviewer and coordinating agent. No independent human or formal-kernel acceptance.", + "open_questions": [ + { + "question": "Can these explicit declared widths, literal idle rows and current intermediate states be integrated into the full uniformly priced CRT control evaluator?", + "why_it_matters": "This logical interface does not price CRT arithmetic, descriptor transport, table construction/query, physical movement, cleanup or head returns.", + "first_step": "Combine the exact row decoder with existing PR4174 placed descriptors and PR4192 compiler component, then specify and charge the remaining encoded numerical evaluator and actual caller.", + "blocked_by": "Outside this logical caller audit; no full evaluator or physical implementation inferred." + } + ], + "freshness": { + "canonical_main": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "priority_revision": 7, + "checked_at": "2026-10-20T13:04:04Z", + "decision": "Continue frozen explicit-width logical caller; current-main guidance and scientific inputs unchanged.", + "overlap": { + "open_and_draft_pr_bodies": 312, + "pagination": [ + 100, + 100, + 100, + 12 + ], + "current_hub_and_4173": "read live; focused CRT Discussion search also checked", + "limitations": "Broader closed/code/Discussion coverage partial; no novelty certification.", + "predecessors_inspected": { + "4169": "835c3563ee7ede8ceaf329ede7372e50f7823136", + "4174": "5fec853f0c048871de3b8098d1e30d4ee19cda23" + }, + "distinct_new_work": "PR4193 shifted Gaussian conditioning at52e962e318423be1fe8ed9d705dba92067795b61 excluded." + } + } +} diff --git a/research/crt-mixed-width-caller/VERIFY.json b/research/crt-mixed-width-caller/VERIFY.json new file mode 100644 index 0000000000..cb28d22506 --- /dev/null +++ b/research/crt-mixed-width-caller/VERIFY.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/unconditional-batched-crt/CRT.md", + "research/unconditional-batched-crt/NOTICE.md", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source-pinned declared-width whole-tree caller, literal idles, all padded endpoints, inverse and semantic/admission controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source-pinned declared-width whole-tree caller, literal idles, all padded endpoints, inverse and semantic/admission controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent_mixed_oracle.py" + ], + "timeout_seconds": 120, + "checks": "Preimplementation separate FIFO compiler/brute scaled-CRT oracle on both complete padded rectangles." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent_mixed_oracle.py" + ], + "timeout_seconds": 120, + "checks": "Preimplementation separate FIFO compiler/brute scaled-CRT oracle on both complete padded rectangles." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/cross_check.py", + "{package}/verify.py", + "{package}/independent_mixed_oracle.py", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "timeout_seconds": 120, + "checks": "Pinned source-bound direct comparison of rows, literal idles, endpoints and inverse on mixed/wide/micro and identity callers." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/cross_check.py", + "{package}/verify.py", + "{package}/independent_mixed_oracle.py", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "timeout_seconds": 120, + "checks": "Pinned source-bound direct comparison of rows, literal idles, endpoints and inverse on mixed/wide/micro and identity callers." + } + ] +} diff --git a/research/crt-mixed-width-caller/cross_check.py b/research/crt-mixed-width-caller/cross_check.py new file mode 100644 index 0000000000..30903a73d6 --- /dev/null +++ b/research/crt-mixed-width-caller/cross_check.py @@ -0,0 +1,103 @@ +"""Pin primary caller and earlier independent oracle for a bounded cross-check.""" +import hashlib +from itertools import product +import json +from pathlib import Path +from random import Random +import sys +import types + + +PRIMARY_SHA256 = "5e62787f3c4a8f1175ca7dea6c6b8ceff7863a3f879abd6245faf6aeb272fd45" +ORACLE_SHA256 = "8cdaedebd991fc0f73e74dd7b53e1c42f1e50d7b61e5b2e52d74134e2dafbdc4" +SOURCE_SHA256 = "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + + +def load(path, name, expected): + path = Path(path) + data = path.read_bytes() + if hashlib.sha256(data).hexdigest() != expected: + raise ValueError("reviewed source bytes changed") + module = types.ModuleType(name) + module.__file__ = str(path) + exec(compile(data, str(path), "exec"), module.__dict__) + return module + + +def independent_row(oracle, state, moduli, widths, ell, level, global_row): + result = [] + for axis, shift in oracle.offsets(state, moduli, level).items(): + embedding = oracle.global_rows(widths[axis], ell) + if global_row not in embedding: + result.append((axis, None, None, 0)) + else: + row = embedding.index(global_row) + target, table = oracle.network(widths[axis], moduli[axis], shift)[row] + result.append((axis, row, target, table[state[axis]])) + return tuple(result) + + +def main(): + primary = load(sys.argv[1], "_pinned_mixed_primary", PRIMARY_SHA256) + oracle = load(sys.argv[2], "_before_primary_mixed_oracle", ORACLE_SHA256) + source = load(sys.argv[3], "_retained_mixed_source", SOURCE_SHA256) + decoder_checks = 0 + for ell in range(2, 17): + for height in (ell - 1, ell): + embedding = oracle.global_rows(height, ell) + for g in range(2 * ell - 1): + expected = embedding.index(g) if g in embedding else None + if primary.local_row(height, ell, g) != expected: + raise ValueError("literal decoder differs from independent embedding") + decoder_checks += 1 + rng = Random(4174) + mixed = set() + for packed in rng.sample(range(1 << 14), 64): + mixed.add((packed & 7, (packed >> 3) & 7, (packed >> 6) & 15, (packed >> 10) & 15)) + mixed.update(((5, 0, 1, 0), (0, 1, 0, 13))) + fixtures = [((5, 7, 11, 13), (3, 3, 4, 4), 4, sorted(mixed)), + ((5, 3), (3, 3), 4, product(range(8), repeat=2)), + ((7, 3), (3, 2), 3, product(range(8), range(4))), + ((3,), (2,), 3, ((x,) for x in range(4)))] + states = rows_checked = idle_specs = 0 + digest = hashlib.sha256() + for moduli, widths, ell, inputs in fixtures: + caller = primary.Caller(moduli, widths, ell, source) + for original in inputs: + original = tuple(original) + for reverse in (False, True): + state = original + levels = tuple(range(1, len(state).bit_length())) + for level in reversed(levels) if reverse else levels: + rows = tuple(range(2 * ell - 1)) + for g in reversed(rows) if reverse else rows: + expected = independent_row(oracle, state, moduli, widths, ell, level, g) + if caller.row(state, level, g) != expected: + raise ValueError("actual-row specification differs from independent oracle") + updated = list(state) + for axis, row, target, control in expected: + if row is None: + idle_specs += 1 + else: + updated[axis] ^= control << target + state = tuple(updated) + rows_checked += 1 + if state != caller.run(original, reverse=reverse): + raise ValueError("literal caller endpoint differs from independent program") + if state != oracle.atomic_endpoint(original, moduli, reverse=reverse): + raise ValueError("literal caller endpoint differs from atomic CRT oracle") + digest.update(oracle.encode(state, widths).to_bytes((sum(widths) + 7) // 8, "big")) + states += 1 + print(json.dumps({"status": "PASS_PINNED_MIXED_CALLER_CROSSCHECK", + "states": states, "forward_inverse_rows": rows_checked, + "row_decoder_comparisons": decoder_checks, + "literal_idle_specifications": idle_specs, + "endpoint_sha256": digest.hexdigest(), + "primary_sha256": PRIMARY_SHA256, "oracle_sha256": ORACLE_SHA256, + "retained_source_sha256": SOURCE_SHA256, + "scope": "separate pre-code oracle against actual rows, including external ell/all-short and singleton cases; no E/tape theorem"}, + sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/crt-mixed-width-caller/independent_benes_oracle.py b/research/crt-mixed-width-caller/independent_benes_oracle.py new file mode 100644 index 0000000000..682d9a2b06 --- /dev/null +++ b/research/crt-mixed-width-caller/independent_benes_oracle.py @@ -0,0 +1,136 @@ +"""Independent levelwise Beneš oracle; semantic arrays are not a tape model. + +No primary implementation is imported. FIFO component coloring and bottom-up +table assembly deliberately avoid the retained source's recursive DFS order. +""" +from collections import deque +from itertools import permutations +import hashlib +import json +from random import Random + + +def compile_levelwise(permutation): + permutation = tuple(permutation) + size = len(permutation) + if size < 2 or size & (size - 1) or sorted(permutation) != list(range(size)): + raise ValueError("dyadic permutation required") + pending = deque([((), permutation)]) + nodes = {} + order = [] + while pending: + path, images = pending.popleft() + order.append(path) + n = len(images) + if n == 2: + nodes[path] = {"layers": ((0, (images[0], images[0])),)} + continue + inverse = {image: x for x, image in enumerate(images)} + color = [-1] * n + for seed in range(n): + if color[seed] != -1: + continue + color[seed] = 0 + component = deque([seed]) + while component: + x = component.popleft() + for neighbor in (inverse[images[x] ^ 1], x ^ 1): + wanted = color[x] ^ 1 + if color[neighbor] == -1: + color[neighbor] = wanted + component.append(neighbor) + elif color[neighbor] != wanted: + raise ValueError("alternating-pair graph is not bipartite") + first = tuple(color[x] ^ (x & 1) for x in range(n)) + last = tuple(color[inverse[y]] ^ (y & 1) for y in range(n)) + nodes[path] = {"first": first, "last": last} + for c in (0, 1): + child = [None] * (n // 2) + for x in range(n): + if color[x] == c: + child[x // 2] = images[x] // 2 + pending.append((path + (c,), tuple(child))) + for path in reversed(order): + node = nodes[path] + if "layers" in node: + continue + left, right = [nodes[path + (c,)]["layers"] for c in (0, 1)] + n = len(node["first"]) + layers = [(0, node["first"])] + for layer in range(len(left)): + if left[layer][0] != right[layer][0]: + raise ValueError("children have different bit schedules") + table = tuple((left, right)[x & 1][layer][1][x // 2] for x in range(n)) + layers.append((1 + left[layer][0], table)) + layers.append((0, node["last"])) + node["layers"] = tuple(layers) + return nodes[()]["layers"] + + +def endpoint(layers, value): + for target, table in layers: + value ^= table[value] << target + return value + + +def check(permutation, digest): + size = len(permutation) + h = size.bit_length() - 1 + layers = compile_levelwise(permutation) + if tuple(bit for bit, _ in layers) != tuple(range(h)) + tuple(range(h - 2, -1, -1)): + raise ValueError("wrong universal target-bit schedule") + for target, table in layers: + for x in range(size): + if table[x] != table[x ^ (1 << target)]: + raise ValueError("control reads its own target") + for x, expected in enumerate(permutation): + actual = endpoint(layers, x) + if actual != expected or endpoint(tuple(reversed(layers)), actual) != x: + raise ValueError("forward/inverse permutation endpoint mismatch") + digest.update(bytes(endpoint(layers, x) for x in range(size))) + return len(layers) * size + + +def mutation_witness(): + for permutation in permutations(range(4)): + layers = compile_levelwise(permutation) + # A child table is indexed by x//2, while x&1 chooses its child. + # Swapping these child selectors is a genuine port-orientation bug. + target, table = layers[1] + broken = (layers[0], (target, tuple(table[x ^ 1] for x in range(4))), layers[-1]) + for x, expected in enumerate(permutation): + actual = endpoint(broken, x) + if actual != expected: + return {"permutation": list(permutation), "input": x, + "expected": expected, "wrong": actual, + "mutation": "interchange the child selector parity"} + raise ValueError("child-selector negative control was not detected") + + +def main(): + digest = hashlib.sha256() + cases = columns = control_columns = 0 + for size in (2, 4, 8): + for permutation in permutations(range(size)): + control_columns += check(permutation, digest) + cases += 1 + columns += size + rng = Random(4174) + for size in (16, 32, 64): + for _ in range(16): + permutation = list(range(size)) + rng.shuffle(permutation) + control_columns += check(permutation, digest) + cases += 1 + columns += size + print(json.dumps({"status": "PASS_INDEPENDENT_BENES_SEMANTICS", + "permutations": cases, "endpoint_columns": columns, + "control_columns": control_columns, + "endpoint_sha256": digest.hexdigest(), + "negative_control": mutation_witness(), + "scope": "separate levelwise FIFO semantic oracle; host arrays and queues do not certify fixed-tape costs"}, + sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/crt-mixed-width-caller/independent_mixed_oracle.py b/research/crt-mixed-width-caller/independent_mixed_oracle.py new file mode 100644 index 0000000000..528c36d131 --- /dev/null +++ b/research/crt-mixed-width-caller/independent_mixed_oracle.py @@ -0,0 +1,231 @@ +"""Independent mixed-height caller oracle, written before primary inspection. + +Uses the earlier separate FIFO network compiler and brute-force CRT decoding. +Host arrays/caches are semantic tools, not a fixed-tape time claim. +""" +from functools import lru_cache +import hashlib +from itertools import product +import json +from math import prod +from pathlib import Path +import types + + +COMPILER_SHA256 = "7a58689072b730201a6b4007f7b2524db2abff460a3116cfa42821fb2e1b63a5" + + +def load_compiler(): + path = Path(__file__).with_name("independent_benes_oracle.py") + data = path.read_bytes() + if hashlib.sha256(data).hexdigest() != COMPILER_SHA256: + raise ValueError("earlier separate FIFO compiler bytes changed") + module = types.ModuleType("_earlier_fifo_network_oracle") + module.__file__ = str(path) + exec(compile(data, str(path), "exec"), module.__dict__) + return module + + +COMPILER = load_compiler() + + +def global_rows(height, ell): + if not 1 <= height <= ell or height not in (ell - 1, ell): + raise ValueError("mixed adjacent heights required") + if height == ell: + return tuple(range(2 * height - 1)) + return tuple(r if r <= ell - 2 else r + 2 for r in range(2 * height - 1)) + + +@lru_cache(None) +def decode_by_search(values, moduli): + if any(x >= modulus for x, modulus in zip(values, moduli)): + return None + prefixes = [] + prefix = 1 + for modulus in moduli: + prefixes.append(prefix) + prefix *= modulus + candidates = [integer for integer in range(prefix) + if all((integer * pow(prefix_i, -1, modulus)) % modulus == value + for prefix_i, modulus, value in zip(prefixes, moduli, values))] + if len(candidates) != 1: + raise ValueError("scaled CRT residues do not select one integer") + return candidates[0] + + +def offsets(state, moduli, level): + group_size = 1 << level + shifts = {} + for start in range(0, len(state), group_size): + middle = start + group_size // 2 + lower = decode_by_search(tuple(state[start:middle]), tuple(moduli[start:middle])) + factor = prod(moduli[start:middle]) + for axis in range(middle, start + group_size): + shifts[axis] = (0 if lower is None else lower * pow(factor, -1, moduli[axis]) % moduli[axis]) + factor *= moduli[axis] + return shifts + + +@lru_cache(None) +def network(height, modulus, shift): + size = 1 << height + permutation = tuple((x + shift) % modulus if x < modulus else x for x in range(size)) + return COMPILER.compile_levelwise(permutation) + + +def atomic_endpoint(values, moduli, reverse=False): + state = list(values) + levels = range(1, len(state).bit_length()) + for level in reversed(tuple(levels)) if reverse else levels: + shifts = offsets(state, moduli, level) + for axis, shift in shifts.items(): + if state[axis] < moduli[axis]: + state[axis] = (state[axis] + (-shift if reverse else shift)) % moduli[axis] + return tuple(state) + + +def microscopic_endpoint(values, moduli, widths, reverse=False): + state = tuple(values) + ell = max(widths) + maps = [{g: r for r, g in enumerate(global_rows(height, ell))} for height in widths] + levels = tuple(range(1, len(state).bit_length())) + rows = tuple(range(2 * ell - 1)) + row_checks = omission_checks = 0 + for level in reversed(levels) if reverse else levels: + frozen = offsets(state, moduli, level) + for g in reversed(rows) if reverse else rows: + controls = {} + for axis, shift in frozen.items(): + r = maps[axis].get(g) + if r is not None: + target, table = network(widths[axis], moduli[axis], shift)[r] + if target != (g if g < ell else 2 * ell - 2 - g): + raise ValueError("local/global active target-bit mismatch") + controls[axis] = (target, table[state[axis]]) + snapshot = state + target_state = list(snapshot) + for axis, (target, flip) in controls.items(): + target_state[axis] ^= flip << target + for other, (other_target, _) in controls.items(): + changed = list(snapshot) + changed[other] ^= 1 << other_target + changed_offsets = offsets(changed, moduli, level) + r = maps[axis][g] + changed_flip = network(widths[axis], moduli[axis], changed_offsets[axis])[r][1][changed[axis]] + if changed_flip != flip: + raise ValueError("control reads an active target") + omission_checks += 1 + # Independently recompute controls after each reverse-ordered write. + sequential = list(snapshot) + for axis in reversed(tuple(controls)): + shift = offsets(sequential, moduli, level)[axis] + target, table = network(widths[axis], moduli[axis], shift)[maps[axis][g]] + sequential[axis] ^= table[sequential[axis]] << target + if sequential != target_state or offsets(target_state, moduli, level) != frozen: + raise ValueError("row commutation or frozen left-child controls failed") + state = tuple(target_state) + row_checks += 1 + return state, row_checks, omission_checks + + +def encode(values, widths): + result = shift = 0 + for value, width in zip(values, widths): + result |= value << shift + shift += width + return result + + +def check_rectangle(moduli, widths): + digest = hashlib.sha256() + images = set() + columns = valid_columns = rows = omissions = 0 + byte_width = (sum(widths) + 7) // 8 + for original in product(*(range(1 << h) for h in widths)): + actual, count, checked = microscopic_endpoint(original, moduli, widths) + expected = atomic_endpoint(original, moduli) + recovered, inverse_count, inverse_checked = microscopic_endpoint(actual, moduli, widths, reverse=True) + if actual != expected or recovered != original: + raise ValueError("all-padded endpoint or literal inverse mismatch") + valid = all(x < modulus for x, modulus in zip(original, moduli)) + if valid: + prefix = 1 + integer = 0 + prefixes = [] + for value, modulus in zip(original, moduli): + prefixes.append(prefix) + integer += value * prefix + prefix *= modulus + direct = tuple(integer * pow(prefix_i, -1, modulus) % modulus + for prefix_i, modulus in zip(prefixes, moduli)) + if actual != direct: + raise ValueError("valid global CRT endpoint mismatch") + valid_columns += 1 + if valid != all(x < modulus for x, modulus in zip(actual, moduli)): + raise ValueError("valid rectangle was not preserved") + images.add(actual) + digest.update(encode(actual, widths).to_bytes(byte_width, "big")) + rows += count + inverse_count + omissions += checked + inverse_checked + columns += 1 + if len(images) != columns: + raise ValueError("full padded endpoint is not bijective") + return {"moduli": list(moduli), "declared_widths": list(widths), + "dirty_columns": columns, "valid_columns": valid_columns, + "forward_inverse_global_rows": rows, + "active_target_omission_checks": omissions, + "endpoint_sha256": digest.hexdigest()} + + +def negative_controls(): + layers = network(2, 3, 1) + state = gated = 1 + trace = [state] + for target, table in layers: + state ^= table[state] << target + if gated < 3: + gated ^= table[gated] << target + trace.append(state) + if state != 2 or gated == state or 3 not in trace: + raise ValueError("current-target-validity mutant was not detected") + # Treating the minimal network as low-bit-only in a larger declared field + # moves an invalid padded value that the declared permutation must fix. + padded = 5 + low = padded & 3 + for target, table in layers: + low ^= table[low] << target + broken = (padded & ~3) | low + expected = COMPILER.endpoint(network(3, 3, 1), padded) + if expected != padded or broken == expected: + raise ValueError("minimal-width substitution mutant was not detected") + return {"current_target_validity_gate": {"size": 4, "modulus": 3, "offset": 1, + "input": 1, "literal_trace": trace, + "expected": state, "wrong": gated}, + "low_minimal_width_substitution": {"declared_size": 8, "modulus": 3, + "offset": 1, "input": padded, + "expected": expected, "wrong": broken}} + + +def main(): + for ell in range(2, 65): + for height in (ell - 1, ell): + mapping = global_rows(height, ell) + if len(mapping) != 2 * height - 1 or tuple(sorted(set(mapping))) != mapping: + raise ValueError("row embedding is not ordered and injective") + for r, g in enumerate(mapping): + local_bit = r if r < height else 2 * height - 2 - r + global_bit = g if g < ell else 2 * ell - 2 - g + if local_bit != global_bit: + raise ValueError("embedding does not preserve the common target bit") + print(json.dumps({"status": "PASS_PREIMPLEMENTATION_MIXED_CALLER_ORACLE", + "rectangles": [check_rectangle((5, 7, 11, 13), (3, 3, 4, 4)), + check_rectangle((5, 3), (3, 3))], + "negative_controls": negative_controls(), + "compiler_sha256": COMPILER_SHA256, + "scope": "independent mixed-row caller and brute scaled-CRT oracle; predecessor omission argument reused; no tape/E theorem"}, + sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/crt-mixed-width-caller/interface-review/COUNTEREXAMPLES.json b/research/crt-mixed-width-caller/interface-review/COUNTEREXAMPLES.json new file mode 100644 index 0000000000..412023edc7 --- /dev/null +++ b/research/crt-mixed-width-caller/interface-review/COUNTEREXAMPLES.json @@ -0,0 +1,79 @@ +{ + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "source_file": { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + }, + "micro_validity_counterexample": { + "declared_wires": 4, + "modulus": 3, + "offset": 1, + "start": 1, + "layers": [ + [ + 0, + [ + 0, + 0, + 1, + 1 + ] + ], + [ + 1, + [ + 0, + 1, + 0, + 1 + ] + ], + [ + 0, + [ + 1, + 1, + 1, + 1 + ] + ] + ], + "trace": [ + 1, + 1, + 3, + 2 + ], + "validity_trace": [ + true, + true, + false, + true + ], + "whole_endpoint": 2, + "consequence": "A valid target can traverse an invalid dyadic value inside its complete network. Do not gate each micro-switch by current target validity." + }, + "minimal_width_api_counterexample": { + "declared_widths": [ + 2, + 2 + ], + "moduli": [ + 3, + 2 + ], + "input": [ + 1, + 2 + ], + "direct_balanced_output": [ + 1, + 2 + ], + "compiled_balanced_error": { + "type": "IndexError", + "message": "tuple index out of range" + }, + "consequence": "Source compiled=True chooses minimal width for modulus 2 and cannot consume this declared-width padded target. Whole padded-state reference must use direct semantics or declared-width adaptation." + } +} diff --git a/research/crt-mixed-width-caller/interface-review/INDEPENDENT-INTERFACE-REVIEW.md b/research/crt-mixed-width-caller/interface-review/INDEPENDENT-INTERFACE-REVIEW.md new file mode 100644 index 0000000000..79ae8affc8 --- /dev/null +++ b/research/crt-mixed-width-caller/interface-review/INDEPENDENT-INTERFACE-REVIEW.md @@ -0,0 +1,168 @@ +# Independent mixed-width caller interface review + +Reviewer: independent OpenAI Codex review, not human or formal-kernel review. +Source: Cinna Davis's retained PR4100 `CRT.md` sections 1–2 and +`check_batched_crt.py` at canonical main +`12fa8c5c844be21bfefb38a19503fbd867a11244`. +This review concerns exact semantic composition and quantified interfaces. +There is no tape, bit-cost, E-evaluator, placement, precision or multiplication +theorem claim. Existing omission/allocator/inverse work in PR4169 and PR4174 +is predecessor work, not a new mechanism supplied by this note. + +## Quantified domain + +Let `d=2^m` for an integer `m>=0`. For a positive integer `ell`, each axis has +an explicitly declared integer width `h_i in {ell-1,ell}`, `h_i>=1`. Let +integer moduli satisfy `2<=s_i<2^(h_i)` and pairwise coprimality. These +conditions themselves exclude any purported width-one axis with modulus at +least two. The complete semantic domain is the padded Cartesian cube +`X=product_i [0,2^(h_i))`, not only the valid rectangle +`V=product_i [0,s_i)` and not only minimally encoded axes. For `d=1` there +are no tree levels and the caller is identity. Empty admitted parameter +families make no extra existence claim. + +At a balanced-tree level, each consecutive node splits into equal axis +halves `A,B`. Only axes in `B` are targets. Reconstruct `k_A` from its +current locally scaled child CRT coordinates when all of `A` is valid; +otherwise use offset zero. For target `i` in `B`, use + +``` +c_i = k_A * (S_A * P_(B,i))^(-1) mod s_i. +``` + +The inverse exists because the moduli are pairwise coprime. Crucially, +every coordinate in every left half `A` remains unchanged for the entire +level: level nodes are disjoint, and no coordinate in a left half is a +target of another node at that level. Thus its validity flag, reconstructed +integer and every offset are constant through all rows of that level. + +## Declared-width compilation and idle rows + +Compile each target permutation on its *declared* domain `2^(h_i)`: + +``` +rho_i(x) = (x+c_i) mod s_i for x=2h_i-1`, the local descriptor is idle, has no target bit and +has no table lookup. Appending zero controls to an existing bit is another +semantic identity, but inventing an extra coordinate or querying beyond the +axis's declared width is not an admissible implementation of idle padding. +Other explicit order-preserving placements of identity rows are possible; +the proof and inverse must use the same declared decoder. + +Each nonidle table is equal on the two values of its active-bit pair. +Its control depends only on its own other axis bits and the fixed left-half +controls. It is therefore independent of *every* simultaneously active +bit: its own by the Beneš invariant, other target axes' bits because they +are absent from its arguments. Distinct-axis operations commute in that +row. Idle descriptors are identities. This supplies the semantic omission +premise; it does not allocate physical borrowed fields or prove a machine +implementation of those controls. + +The source helper `balanced(...,compiled=True)` chooses +`(s_i-1).bit_length()` instead of the declared `h_i`. It is not a valid +reference API for all wider padded target states. The exact counterexample +in `COUNTEREXAMPLES.json` uses moduli `(3,2)`, declared widths `(2,2)` and +state `(1,2)`: direct source semantics return `(1,2)`, while the compiled +helper indexes outside a two-wire table. Use the direct source semantics +or an explicitly declared-width adaptation for the whole padded caller. + +## Intermediate validity and inverse order + +Each *complete* `rho_i` is a permutation, fixes every invalid target value +and preserves target validity. None of this says that every internal switch +preserves validity. The retained four-wire compiler with `s=3,c=1` sends +valid `x=1` through `1,1,3,2`. Disabling a micro-switch whenever its current +target is invalid strands this trajectory at 3 and destroys the endpoint; +there is also a collision with the originally invalid target 3. The +left-half validity flag may gate preparation because those controls are +constant through the level. Current target validity must not gate an +individual compiled switch. + +For exact inverse transcripts, reverse the tree levels, reverse the common +padded row order at each level, and apply the same table-controlled bit +flips. Every row map is an involution because its controls omit all active +bits; its simultaneous target operations commute. At inverse entry to a +level, all later forward levels have already been undone, so the left-half +controls agree with those of the forward level. Within the level they stay +unchanged. This proves exact inverse composition on *all* of `X`. +Compiling a negative modular offset yields the same complete inverse target +permutation, but that alone does not justify reversing a particular row +transcript or reusing different row tables. + +## Complete endpoint and valid restriction + +Inductively, a valid child group has locally scaled CRT coordinates +`Phi_A(a),Phi_B(a)`. Let `k_G=k_A+S_A*k_B`. For `i in B`, adding the offset +changes its coordinate to + +``` +k_B/P_(B,i) + k_A/(S_A*P_(B,i)) = k_G/P_(G,i) mod s_i. +``` + +For `i in A`, `k_G=k_A mod s_i`, so its coordinate already has the desired +value. This establishes the valid root restriction. On the complete padded +cube, each conditional level is a composition of target permutations +conditioned on unchanged left-half coordinates, hence a permutation. +It preserves the globally valid rectangle at complete-level boundaries and +therefore permutes its complement too. Dirty invalid states need not be +pointwise fixed; they are carried bijectively. The inverse proof applies +equally to them. Endpoint/validity conclusions are not asserted at internal +rows. + +No material obstruction is visible to this semantic interface. A submitted +implementation still needs an explicit local-row/idle decoder, declared-width +compilation, complete padded-state reference and the exact inverse order. +Finite exhaustive checks corroborate those choices but do not prove the +all-size theorem by their counts. + +## Final submitted caller review + +I read the submitted `research/crt-mixed-width-caller/{verify.py,PROOF.md, +README.md,RESULT.json,SOURCE-PINS.json}`. This is a read-only proof/interface +review; I did not author or change its implementation and do not represent +its stored finite receipt as an independently implemented oracle. + +The actual submitted decoder chooses a center-idle embedding, rather than +the simpler trailing-idle example above: short axes idle at global rows +`ell-1,ell`, use local `g` before those rows and local `g-2` afterwards. +For `g<=ell-2`, both active schedules use bit `g`. For `g>=ell+1`, the +short schedule uses `2(ell-1)-2-(g-2)=2ell-2-g`, exactly the long schedule's +bit. The `ell=2` post-idle range is empty. Removing the two idles therefore +recovers every local row in order, for every admitted ell, with no phantom +coordinate. The implementation retains the supplied global ell even when +all axes are short; it does not normalize ell to the maximum declared width. + +Each network is compiled on `2^h_i` entries. The row decoder returns its +idle descriptor before any network access. Each nonidle table is queried at +the current target-axis value. Only unchanged left-half offsets are frozen +at level entry. Increasing-depth and decreasing-depth schedules match the +claimed forward/inverse constructions. Both full padded-domain comparison +to source uncompiled arithmetic and the additional source compiled oracle +are used within their explicitly correct width domains. + +The validity counterexample is bound to a genuine admitted CRT caller: +moduli `(7,3)`, widths `(3,2)`, global ell 3, input `(1,1)`, right-target +offset 1. The short network visits invalid target 3 between valid endpoints; +incorrect target-validity gating returns `(1,3)` instead of `(1,2)`. +The source-helper wider-width witness and globally-invalid-but-moving +witness are also explicitly scoped as incorrect inference/API coverage +boundaries, not defects in the predecessor's mathematical construction. + +The submitted all-size proof correctly treats left controls as constant +through a level, preserves each axis's own row order, uses disjoint-axis +commutation to identify the complete level endpoint, and reverses both +levels and padded global rows for exact inversion. Global invalid tuples +are permuted; pointwise fixation is not asserted. Source Phi and predecessor +omission/allocator/inverse credit are retained. No tape/E or physical compact +execution claim is introduced. + +No material proof, declared-width, idle-row, inverse-order or padding-interface +defect remains in the reviewed submitted candidate. The accompanying report +pins exactly the files read. The finite Python receipt remains corroboration +of the separately quantified written result, and no human review or formal +kernel acceptance is claimed. diff --git a/research/crt-mixed-width-caller/interface-review/REPORT.json b/research/crt-mixed-width-caller/interface-review/REPORT.json new file mode 100644 index 0000000000..3f96d4b379 --- /dev/null +++ b/research/crt-mixed-width-caller/interface-review/REPORT.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "status": "PASS_INDEPENDENT_MIXED_WIDTH_CALLER_PROOF_INTERFACE_REVIEW", + "reviewer": "Independent OpenAI Codex; not human or formal-kernel review", + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "scope": "Declared mixed-width balanced CRT semantic caller, local row/idle decoder and all-padded-state inverse", + "source_files": [ + { + "path": "research/unconditional-batched-crt/CRT.md", + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + } + ], + "review_files": [ + { + "path": "INDEPENDENT-INTERFACE-REVIEW.md", + "sha256": "5f9fe0dc860b5d9f9eecc280f8f8d571fe3a0d5d30b375732536bff9db0844cd" + }, + { + "path": "COUNTEREXAMPLES.json", + "sha256": "6cd7a1d031680842a07b21afb29aa450c7f6d8d3635e2c45f3944ae4e8d3c1e3" + } + ], + "quantified_domain": [ + "d=2^m, m>=0", + "h_i in {ell-1,ell}, h_i>=1", + "2<=s_i<2^h_i, pairwise coprime", + "Every state in product_i [0,2^h_i)" + ], + "material_interface_requirements": [ + "Declared-width compilation, not source compiled helper minimal widths", + "Idle rows carry no phantom target bit or table query", + "Left-half controls remain unchanged for the whole tree level", + "Reverse whole padded row order and tree level order for exact inverse", + "Do not gate micro-switches by current target validity" + ], + "counterexamples_checked": [ + "N4,s3,c1,x1 trace1,1,3,2 disproves micro-switch validity invariance", + "Widths2,2 moduli3,2 state1,2: source compiled helper raises IndexError; direct endpoint1,2" + ], + "primary_implementation_reviewed": true, + "remaining_obligations": [ + "Production physical placement and borrowed-field restoration", + "Full numerical evaluator and tape/bit tariff", + "Compact repair and ordinary-callee execution", + "Precision/native/outer multiplication theorem", + "Independent human or formal-kernel acceptance" + ], + "credit": [ + "Cinna Davis: balanced factorization, modular rotations and Bene\u0161 source", + "PR4169 and PR4174: existing omission, allocator and inverse work" + ], + "primary_review_mode": "Read-only mathematical and interface inspection; no edits and no independently implemented caller supplied by this reviewer", + "primary_files_reviewed": [ + { + "path": "research/crt-mixed-width-caller/verify.py", + "sha256": "5e62787f3c4a8f1175ca7dea6c6b8ceff7863a3f879abd6245faf6aeb272fd45" + }, + { + "path": "research/crt-mixed-width-caller/PROOF.md", + "sha256": "ded150e3ab4da3561ac8623fd7d0041deb6f31dbf7b49a04dc19e0ba959c58d9" + }, + { + "path": "research/crt-mixed-width-caller/README.md", + "sha256": "c5126d2e1f381fe5a34b8e3350799ac4c3a58fe2def590b12ad4354da7b01ebf" + }, + { + "path": "research/crt-mixed-width-caller/RESULT.json", + "sha256": "2ba6f2e1661d8d9af0861eaf903bc596acd9bf0912b090389b1bc6d1f9898dd0" + }, + { + "path": "research/crt-mixed-width-caller/SOURCE-PINS.json", + "sha256": "e8e5c7320fb0bd1494e063eaa5aaf5f2f08562b80b72750081ea5a409eea5b1e" + } + ], + "primary_embedding_checked": "Short axes idle at global ell-1 and ell; local g before, g-2 after; supplied ell preserved on all-short inputs", + "material_findings_remaining": [], + "stored_primary_evidence_read_only": { + "marker": "PASS_EXPLICIT_WIDTH_SYNCHRONIZED_CRT_CALLER", + "fixtures": 3, + "padded_states": 16480, + "scope": "Stored receipt inspected; its replay is separately owned by the coordinating agent/oracle reviewer" + } +} diff --git a/research/crt-mixed-width-caller/verify.py b/research/crt-mixed-width-caller/verify.py new file mode 100644 index 0000000000..7980582b86 --- /dev/null +++ b/research/crt-mixed-width-caller/verify.py @@ -0,0 +1,310 @@ +"""Explicit-width synchronized CRT caller; source-bound finite corroboration. + +Logical address-permutation model only: no tape/E tariff is inferred. Source +Beneš/CRT arithmetic is authenticated and reused; global row decoding is new. +""" + +import argparse +import hashlib +import itertools +import json +import math +from pathlib import Path +import sys +import types + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def schedule(height): + need(type(height) is int and height >= 1, "positive network height") + return tuple(range(height)) + tuple(reversed(range(height - 1))) + + +def local_row(width, ell, global_row): + """None is a literal idle, with no target address bit or table query.""" + need(type(ell) is int and ell >= 2, "ell at least two") + need(type(width) is int and width in (ell - 1, ell), "declared width ell-1 or ell") + need(type(global_row) is int and 0 <= global_row < 2 * ell - 1, "global row range") + if width == ell: + return global_row + if global_row in (ell - 1, ell): + return None + return global_row if global_row < ell - 1 else global_row - 2 + + +class Caller: + def __init__(self, moduli, widths, ell, source): + self.moduli, self.widths = tuple(moduli), tuple(widths) + self.ell, self.source = ell, source + self.d = len(self.moduli) + need(self.d >= 1 and self.d & (self.d - 1) == 0, "power-of-two axis count") + need(len(self.widths) == self.d, "one declared width per axis") + need(type(ell) is int and ell >= 2, "ell at least two") + for modulus, width in zip(self.moduli, self.widths): + need(type(width) is int and width in (ell - 1, ell), "declared width family") + need(type(modulus) is int and 2 <= modulus < (1 << width), "strict dyadic padding") + need(all(math.gcd(a, b) == 1 for i, a in enumerate(self.moduli) for b in self.moduli[i + 1:]), + "pairwise coprime moduli") + self.levels = self.d.bit_length() - 1 + self.shifts = tuple(sum(self.widths[:i]) for i in range(self.d)) + self.length = sum(self.widths) + self._networks = {} # Finite host-model cache; no machine-cost claim. + + def state(self, values): + state = tuple(values) + need(len(state) == self.d and all(type(v) is int and 0 <= v < (1 << h) + for v, h in zip(state, self.widths)), + "complete declared padded state") + return state + + def valid(self, state): + return all(v < m for v, m in zip(state, self.moduli)) + + def pack(self, state): + return sum(value << shift for value, shift in zip(state, self.shifts)) + + def network(self, axis, offset): + key = axis, offset + if key not in self._networks: + height = self.widths[axis] + net = self.source.benes(self.source.rotation(1 << height, self.moduli[axis], offset)) + need(tuple(bit for bit, table in net) == schedule(height), "retained network schedule") + need(all(len(table) == 1 << height for bit, table in net), "declared width never shrunk") + self._networks[key] = net + return self._networks[key] + + def offsets(self, state, level): + """Only original left-child coordinates decide validity and offsets.""" + need(1 <= level <= self.levels, "balanced level range") + size = 1 << level + result = {} + for start in range(0, self.d, size): + middle = start + size // 2 + left = state[start:middle] + moduli = self.moduli[start:middle] + lower = self.source.decode_group(left, moduli) if all(v < m for v, m in zip(left, moduli)) else 0 + prefix = math.prod(moduli) + for axis in range(middle, start + size): + result[axis] = lower * pow(prefix, -1, self.moduli[axis]) % self.moduli[axis] + prefix *= self.moduli[axis] + return result + + def row(self, state, level, global_row, offsets=None, gate_invalid_target=False): + offsets = self.offsets(state, level) if offsets is None else offsets + result = [] + for axis, offset in offsets.items(): + row = local_row(self.widths[axis], self.ell, global_row) + if row is None: + result.append((axis, None, None, 0)) + continue + bit, table = self.network(axis, offset)[row] + need(0 <= bit < self.widths[axis], "no phantom address bit") + need(bit == schedule(self.ell)[global_row], "canonical active global bit alignment") + control = table[state[axis]] + if gate_invalid_target and state[axis] >= self.moduli[axis]: + control = 0 # Deliberately wrong: intermediate target validity is not invariant. + result.append((axis, row, bit, control)) + return tuple(result) + + @staticmethod + def apply(state, specifications): + result = list(state) + for axis, row, bit, control in specifications: + if row is None: + need(bit is None and control == 0, "idle has no target") + else: + result[axis] ^= control << bit + return tuple(result) + + def run(self, values, reverse=False, inspect=None, gate_invalid_target=False): + state = self.state(values) + levels = range(self.levels, 0, -1) if reverse else range(1, self.levels + 1) + for level in levels: + offsets = self.offsets(state, level) + level_input = state + rows = reversed(range(2 * self.ell - 1)) if reverse else range(2 * self.ell - 1) + for global_row in rows: + specs = self.row(state, level, global_row, offsets, gate_invalid_target) + if inspect is not None: + inspect(state, level, global_row, specs) + state = self.apply(state, specs) + need(self.valid(state) == self.valid(level_input), "valid set preserved at whole-level endpoint") + return state + + +def check_decoder(): + cases = idles = 0 + for ell in range(2, 17): + for width in (ell - 1, ell): + rows = [local_row(width, ell, g) for g in range(2 * ell - 1)] + need([r for r in rows if r is not None] == list(range(2 * width - 1)), + "every local row appears exactly once and in order") + for g, row in enumerate(rows): + if row is None: + idles += 1 + need(width == ell - 1 and g in (ell - 1, ell), "exact two idle locations") + else: + need(schedule(width)[row] == schedule(ell)[g], "active target bit exists and aligns") + cases += 1 + return {"ell_values": [2, 16], "height_cases": cases, "literal_idles": idles, + "proof_scope": "all integer ell>=2; finite decoder check is corroboration"} + + +def fixture(name, moduli, widths, ell, source): + caller = Caller(moduli, widths, ell, source) + domain = itertools.product(*(range(1 << h) for h in widths)) + count = valid = row_checks = omission_checks = idle_checks = 0 + endpoint_digest = hashlib.sha256() + inverse_digest = hashlib.sha256() + seen = bytearray(1 << caller.length) + changed_invalid = None + minimal = all(h == (m - 1).bit_length() for h, m in zip(widths, moduli)) + compiled_checks = 0 + + def inspect(state, level, g, specs): + nonlocal row_checks, omission_checks, idle_checks + row_checks += 1 + # Recomputed current left-child controls agree with the frozen level controls. + need(specs == caller.row(state, level, g), "freeze only unchanged left-child controls") + for axis, row, bit, control in specs: + if row is None: + idle_checks += 1 + need(bit is None and control == 0, "literal idle performs no phantom query") + continue + toggled = list(state) + toggled[axis] ^= 1 << bit + need(caller.row(tuple(toggled), level, g) == specs, "all active targets omitted at actual row") + omission_checks += 1 + + for state in domain: + count += 1 + forward = caller.run(state, inspect=inspect) + inverse = caller.run(state, reverse=True) + need(forward == source.balanced(state, moduli), "whole synchronized tree equals retained arithmetic caller") + need(inverse == source.balanced(state, moduli, reverse=True), "reverse rows/levels equal inverse CRT endpoint") + need(caller.run(forward, reverse=True) == state and caller.run(inverse) == state, + "two-sided all-padded inverse") + if minimal: + need(forward == source.balanced(state, moduli, compiled=True), "minimal-width compiled source oracle") + compiled_checks += 1 + if caller.valid(state): + valid += 1 + need(forward == source.direct(state, moduli), "direct CRT formula on complete valid subset") + elif forward != state and changed_invalid is None: + changed_invalid = {"input": list(state), "output": list(forward)} + need(caller.valid(state) == caller.valid(forward), "global invalid set preserved, not pointwise fixation") + destination = caller.pack(forward) + need(not seen[destination], "all declared dirty tuples permuted bijectively") + seen[destination] = 1 + endpoint_digest.update(destination.to_bytes((caller.length + 7) // 8, "big")) + inverse_digest.update(caller.pack(inverse).to_bytes((caller.length + 7) // 8, "big")) + need(all(seen), "complete padded destination coverage") + need(count == 1 << caller.length and valid == math.prod(moduli), "complete domain/valid count") + return {"name": name, "domain": "canonical logical axes; no reservoir placement or physical macro executed", + "hash_input_order": "lexicographic logical tuples, axis0 outermost; packed axis0 is least significant", + "hash_destination_encoding": "ceil(L/8) bytes per packed destination, big endian", + "moduli": list(moduli), "widths": list(widths), "ell": ell, + "axes": caller.d, "address_bits": caller.length, "tree_levels": caller.levels, + "global_rows_per_level": 2 * ell - 1, "padded_states": count, + "valid_states": valid, "invalid_states": count - valid, + "forward_row_checks": row_checks, "actual_row_omission_toggles": omission_checks, + "literal_idle_checks": idle_checks, "minimal_width_compiled_source_checks": compiled_checks, + "changed_invalid_tuple": changed_invalid, + "forward_permutation_sha256": endpoint_digest.hexdigest(), + "inverse_permutation_sha256": inverse_digest.hexdigest()} + + +def rejection(call, label): + try: + call() + except (ValueError, IndexError): + return label + raise ValueError("negative control accepted: " + label) + + +def negatives(source): + # A genuine CRT caller, not an isolated made-up switch predicate. + caller = Caller((7, 3), (3, 2), 3, source) + state = (1, 1) + trace = [] + right = caller.run(state, inspect=lambda x, level, g, specs: + trace.append({"global_row": g, "before": list(x), + "local_row": specs[0][1], "target": specs[0][2]})) + # Run the mutant manually: its purpose is to violate the endpoint, so do + # not apply the correct caller's endpoint-validity postcondition to it. + wrong = state + offsets = caller.offsets(state, 1) + for g in range(5): + wrong = caller.apply(wrong, caller.row(wrong, 1, g, offsets, gate_invalid_target=True)) + need(right == (1, 2) and wrong == (1, 3), "per-micro-layer target-validity mutant detected") + need(any(row["before"][1] == 3 for row in trace), "dirty target occurs between valid endpoints") + wider = Caller((5, 3), (3, 3), 3, source) + need(wider.run((0, 4)) == (0, 4), "declared wider padding endpoint") + boundary = rejection(lambda: source.balanced((0, 4), (5, 3), compiled=True), + "minimal-width finite source helper cannot index declared wider dirty target") + invalid = (5, 0, 1, 0) + full = Caller((5, 7, 11, 13), (3, 3, 4, 4), 4, source) + need(not full.valid(invalid) and full.run(invalid) == (5, 0, 1, 6), + "globally invalid tuple is not necessarily pointwise fixed") + return {"target_validity_mutant": {"moduli": [7, 3], "widths": [3, 2], "ell": 3, + "input": list(state), "correct": list(right), "wrong": list(wrong), + "trace_before_rows": trace}, + "source_helper_api_boundary": boundary, + "invalid_pointwise_fixation_counterexample": {"input": list(invalid), "output": [5, 0, 1, 6]}, + "admission_rejections": [ + rejection(lambda: local_row(2, 4, 0), "width outside ell-1/ell"), + rejection(lambda: local_row(3, 4, 7), "global row outside schedule"), + rejection(lambda: Caller((3, 5, 7), (3, 3, 3), 3, source), "non-power-of-two axes"), + rejection(lambda: Caller((3, 9), (4, 4), 4, source), "noncoprime moduli"), + rejection(lambda: Caller((3, 8), (3, 3), 3, source), "missing strict dyadic padding"), + ]} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", action="store_true") + args = parser.parse_args() + pins = json.loads((PACKAGE / "SOURCE-PINS.json").read_text()) + authenticated = {} + for row in pins: + data = (ROOT / row["path"]).read_bytes() + need(hashlib.sha256(data).hexdigest() == row["sha256"], "source SHA256: " + row["path"]) + need(hashlib.sha1(f"blob {len(data)}\0".encode() + data).hexdigest() == row["git_blob"], + "source Git blob: " + row["path"]) + authenticated[row["path"]] = data + path = "research/unconditional-batched-crt/check_batched_crt.py" + source = types.ModuleType("_mixed_width_authenticated_source") + source.__file__ = str(ROOT / path) + sys.modules[source.__name__] = source + exec(compile(authenticated[path], source.__file__, "exec"), source.__dict__) + result = {"schema_version": 1, "result": "PASS_EXPLICIT_WIDTH_SYNCHRONIZED_CRT_CALLER", + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", "source_inputs_checked": len(authenticated), + "decoder": check_decoder(), "fixtures": [ + fixture("mixed_four_axis", (5, 7, 11, 13), (3, 3, 4, 4), 4, source), + fixture("declared_wider_padding", (5, 3), (3, 3), 4, source), + fixture("microscopic_padding_validity", (7, 3), (3, 2), 3, source), + ], "negative_controls": negatives(source), + "limitations": ["Quantified caller/decoder proof is separate from finite corroboration.", + "All-target omission is predecessor coverage; this binds literal mixed-width rows.", + "Canonical logical-axis host model only; no reservoir or physical compact macro executed.", + "No tape/E tariff, full CRT implementation, precision/native/outer theorem or new kappa."]} + output = PACKAGE / "RESULT.json" + if args.write_result: + output.write_text(json.dumps(result, indent=2) + "\n") + else: + need(json.loads(output.read_text()) == result, "stored receipt differs from replay") + print(json.dumps({"result": result["result"], + "padded_states": sum(r["padded_states"] for r in result["fixtures"]), + "row_checks": sum(r["forward_row_checks"] for r in result["fixtures"])}, sort_keys=True)) + + +if __name__ == "__main__": + main()