From 33676ef7ca7d3c2989a1a673b2d8961dc95fef1f Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Tue, 20 Oct 2026 05:35:49 -0700 Subject: [PATCH 1/2] =?UTF-8?q?Audit=20uniform=20Bene=C5=A1=20compiler=20w?= =?UTF-8?q?ith=20charged=20sequential=20arena=20scans?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- research/crt-benes-scan/COLD-REPLAY.json | 52 ++ research/crt-benes-scan/COST-REVIEW.json | 117 +++++ research/crt-benes-scan/CROSS-CHECK.json | 60 +++ .../crt-benes-scan/INDEPENDENT-COST-REVIEW.md | 155 ++++++ research/crt-benes-scan/INITIAL-REVIEW.json | 79 +++ research/crt-benes-scan/INITIAL-REVIEW.md | 99 ++++ research/crt-benes-scan/NOTICE.md | 7 + research/crt-benes-scan/PROOF.md | 258 ++++++++++ research/crt-benes-scan/README.md | 94 ++++ research/crt-benes-scan/RESULT.json | 103 ++++ research/crt-benes-scan/SOURCE-PINS.json | 20 + research/crt-benes-scan/SOURCES.json | 36 ++ research/crt-benes-scan/TASK.json | 74 +++ research/crt-benes-scan/VERIFY.json | 86 ++++ research/crt-benes-scan/cross_check.py | 82 ++++ .../independent_benes_oracle.py | 136 ++++++ research/crt-benes-scan/verify.py | 450 ++++++++++++++++++ 17 files changed, 1908 insertions(+) create mode 100644 research/crt-benes-scan/COLD-REPLAY.json create mode 100644 research/crt-benes-scan/COST-REVIEW.json create mode 100644 research/crt-benes-scan/CROSS-CHECK.json create mode 100644 research/crt-benes-scan/INDEPENDENT-COST-REVIEW.md create mode 100644 research/crt-benes-scan/INITIAL-REVIEW.json create mode 100644 research/crt-benes-scan/INITIAL-REVIEW.md create mode 100644 research/crt-benes-scan/NOTICE.md create mode 100644 research/crt-benes-scan/PROOF.md create mode 100644 research/crt-benes-scan/README.md create mode 100644 research/crt-benes-scan/RESULT.json create mode 100644 research/crt-benes-scan/SOURCE-PINS.json create mode 100644 research/crt-benes-scan/SOURCES.json create mode 100644 research/crt-benes-scan/TASK.json create mode 100644 research/crt-benes-scan/VERIFY.json create mode 100644 research/crt-benes-scan/cross_check.py create mode 100644 research/crt-benes-scan/independent_benes_oracle.py create mode 100644 research/crt-benes-scan/verify.py diff --git a/research/crt-benes-scan/COLD-REPLAY.json b/research/crt-benes-scan/COLD-REPLAY.json new file mode 100644 index 0000000000..a7d055aac9 --- /dev/null +++ b/research/crt-benes-scan/COLD-REPLAY.json @@ -0,0 +1,52 @@ +{ + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files_stable": true, + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "reviewed_hashes": { + "PROOF.md": "c3eb4e14dc5ee0102cbf77c4a0e61db9989c2b8a0eaf7f0659a6e39373197474", + "README.md": "a27718895b2638555b9be078e5c265863d4d8075fd29506af3473b5deaa503cb", + "RESULT.json": "4902975cccde4312dd750c8dd8c092af1f8ddf383afc4e92d1bbb9bd5b435ca1", + "SOURCE-PINS.json": "e8e5c7320fb0bd1494e063eaa5aaf5f2f08562b80b72750081ea5a409eea5b1e", + "verify.py": "e8ff7800ffa267d2825009656b78ab1613544b55301982744ec0d99f38800913" + }, + "runs": [ + { + "argv_template": [ + "{python}", + "-I", + "-B", + "research/crt-benes-scan/verify.py" + ], + "exit_code": 0, + "receipt": { + "cases": 49, + "logical_accesses": 15984, + "result": "PASS_UNIFORM_BENES_SCAN_COMPONENT" + }, + "stderr": "" + }, + { + "argv_template": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "research/crt-benes-scan/verify.py" + ], + "exit_code": 0, + "receipt": { + "cases": 49, + "logical_accesses": 15984, + "result": "PASS_UNIFORM_BENES_SCAN_COMPONENT" + }, + "stderr": "" + } + ], + "schema_version": 1, + "scope": "isolated git-free copy of exact candidate and source inputs; no ROOT override", + "source_inputs_checked": 3, + "status": "PASS_COLD_REGISTERED_REPLAY", + "time_utc": "2026-10-20T12:32:47.579452+00:00" +} diff --git a/research/crt-benes-scan/COST-REVIEW.json b/research/crt-benes-scan/COST-REVIEW.json new file mode 100644 index 0000000000..ac368dfaa2 --- /dev/null +++ b/research/crt-benes-scan/COST-REVIEW.json @@ -0,0 +1,117 @@ +{ + "schema_version": 1, + "status": "PASS_INDEPENDENT_COST_ENCODING_OWNERSHIP_REVIEW", + "reviewer": "Independent OpenAI Codex review; not a human review", + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "scope": "Uniform finite-alphabet sequential simulation of retained Bene\u0161 compiler and its table queries", + "source_files": [ + { + "path": "research/unconditional-batched-crt/CRT.md", + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + } + ], + "review_file": { + "path": "INDEPENDENT-COST-REVIEW.md", + "sha256": "611a419923eaabc60922f2dc834eb5eb48bca4f77cfae7ddb5d75cd059c74693" + }, + "hypotheses": [ + "n=2^h with 1<=h<=ell<=p", + "Fixed-width bounded permutation/input/query encoding", + "At most O(p) axis control invocations", + "Full CRT offsets and numerical arithmetic supplied separately" + ], + "bounds": { + "compiler_and_query_time": "O(2^(3 ell) (p+2)^8)", + "up_to_p_axis_compiler_time": "O(2^(3 ell) (p+2)^9)", + "workspace": "O(2^ell (p+2)^3)", + "fits_retained_envelope": "O(2^(4 ell) (p+2)^16)" + }, + "excluded": [ + "Full CRT numerical evaluator", + "Production physical placement and guard validity", + "Payload machine implementation", + "Native or outer multiplication theorem", + "Finite-count proof of asymptotic constants" + ], + "credit": "Cinna Davis: predecessor full-scan simulation and Bene\u0161 compiler.", + "primary_package": "research/crt-benes-scan", + "primary_files_reviewed": [ + { + "path": "research/crt-benes-scan/verify.py", + "sha256": "e8ff7800ffa267d2825009656b78ab1613544b55301982744ec0d99f38800913" + }, + { + "path": "research/crt-benes-scan/PROOF.md", + "sha256": "c3eb4e14dc5ee0102cbf77c4a0e61db9989c2b8a0eaf7f0659a6e39373197474" + }, + { + "path": "research/crt-benes-scan/RESULT.json", + "sha256": "4902975cccde4312dd750c8dd8c092af1f8ddf383afc4e92d1bbb9bd5b435ca1" + }, + { + "path": "research/crt-benes-scan/README.md", + "sha256": "a27718895b2638555b9be078e5c265863d4d8075fd29506af3473b5deaa503cb" + }, + { + "path": "research/crt-benes-scan/SOURCE-PINS.json", + "sha256": "e8e5c7320fb0bd1494e063eaa5aaf5f2f08562b80b72750081ea5a409eea5b1e" + } + ], + "primary_bound_checked": { + "compiler_time": "O(2^(3ell)(p+2)^7)", + "visited_space": "O(2^ell(p+2)^3)", + "exact_arena_records": "N(h^2+3h+1)", + "exact_logical_accesses": "N^2+2Nh^2+(37Nh-35N)/2", + "arena_access_actions": "(26J+25)w", + "network_query_actions": "3(2h-1)N+3" + }, + "review_findings": { + "material_defects_remaining": [], + "clarifications_applied": [ + "Canonical bounded parameter and query encodings", + "Separate modeled input traffic from written admission/scalar lowering", + "Fixed reusable output-tape roles", + "Successful-call cleanup contract", + "All encoded query bytes validated" + ] + }, + "replay_helper": { + "path": "replay_primary.py", + "sha256": "883d36057327598de9ecd20b3829d6931c6cc1df88ff75f6e3dbde9d8c8d20d0" + }, + "replays": [ + { + "command": "python3 -B replay_primary.py PACKAGE SOURCE_CHECKOUT", + "exit_code": 0, + "elapsed_seconds": 1.895, + "stdout": { + "cases": 49, + "logical_accesses": 15984, + "result": "PASS_UNIFORM_BENES_SCAN_COMPONENT" + }, + "stderr": "" + }, + { + "command": "python3 -B -O replay_primary.py PACKAGE SOURCE_CHECKOUT", + "exit_code": 0, + "elapsed_seconds": 1.951, + "stdout": { + "cases": 49, + "logical_accesses": 15984, + "result": "PASS_UNIFORM_BENES_SCAN_COMPONENT" + }, + "stderr": "" + } + ], + "primary_unchanged_during_review": true, + "limitations": [ + "Independent AI review, not human review", + "No literal complete transition-table or proof-assistant certificate", + "Scalar/header lowering is written constructive proof, not executed microcode", + "Full CRT evaluator, placement and multiplication theorem excluded" + ] +} diff --git a/research/crt-benes-scan/CROSS-CHECK.json b/research/crt-benes-scan/CROSS-CHECK.json new file mode 100644 index 0000000000..9c39031662 --- /dev/null +++ b/research/crt-benes-scan/CROSS-CHECK.json @@ -0,0 +1,60 @@ +{ + "files": { + "cross_check.py": "7cbb63c76d75b9b25ebf3aedc93140423a75b69c3f8f3289d51e8e9516b647b0", + "independent_benes_oracle.py": "7a58689072b730201a6b4007f7b2524db2abff460a3116cfa42821fb2e1b63a5", + "verify.py": "e8ff7800ffa267d2825009656b78ab1613544b55301982744ec0d99f38800913" + }, + "runs": [ + { + "argv_template": [ + "{python}", + "-I", + "-B", + "cross_check.py", + "research/crt-benes-scan/verify.py", + "independent_benes_oracle.py" + ], + "exit_code": 0, + "receipt": { + "cases": 37, + "control_queries": 848, + "endpoint_columns": 200, + "oracle_sha256": "7a58689072b730201a6b4007f7b2524db2abff460a3116cfa42821fb2e1b63a5", + "owned_tables_sha256": "3eb220b80148af975bd92fa798b4e43e56ff3f15413a8cc42898ee695eed6d48", + "primary_sha256": "e8ff7800ffa267d2825009656b78ab1613544b55301982744ec0d99f38800913", + "scope": "source-pinned finite compiler/query equivalence and forward/reverse endpoints; not an asymptotic timing proof", + "status": "PASS_PRIMARY_VS_PREIMPLEMENTATION_ORACLE" + }, + "stderr": "" + }, + { + "argv_template": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "cross_check.py", + "research/crt-benes-scan/verify.py", + "independent_benes_oracle.py" + ], + "exit_code": 0, + "receipt": { + "cases": 37, + "control_queries": 848, + "endpoint_columns": 200, + "oracle_sha256": "7a58689072b730201a6b4007f7b2524db2abff460a3116cfa42821fb2e1b63a5", + "owned_tables_sha256": "3eb220b80148af975bd92fa798b4e43e56ff3f15413a8cc42898ee695eed6d48", + "primary_sha256": "e8ff7800ffa267d2825009656b78ab1613544b55301982744ec0d99f38800913", + "scope": "source-pinned finite compiler/query equivalence and forward/reverse endpoints; not an asymptotic timing proof", + "status": "PASS_PRIMARY_VS_PREIMPLEMENTATION_ORACLE" + }, + "stderr": "" + } + ], + "schema_version": 1, + "scope": "separate before-code FIFO semantic oracle against pinned primary fixed-scan compiler; finite evidence, no full CRT E theorem", + "status": "PASS_INDEPENDENT_PRIMARY_CROSSCHECK", + "time_utc": "2026-10-20T12:33:59.154066+00:00" +} diff --git a/research/crt-benes-scan/INDEPENDENT-COST-REVIEW.md b/research/crt-benes-scan/INDEPENDENT-COST-REVIEW.md new file mode 100644 index 0000000000..18cf0ce9f7 --- /dev/null +++ b/research/crt-benes-scan/INDEPENDENT-COST-REVIEW.md @@ -0,0 +1,155 @@ +# Independent cost review: retained Beneš compiler + +Reviewer: OpenAI Codex, acting independently of the primary implementation. +Source credit: Cinna Davis's retained `research/unconditional-batched-crt/CRT.md` +full-scan simulation argument and `check_batched_crt.py::benes` at canonical +main `12fa8c5c844be21bfefb38a19503fbd867a11244`. + +This is an audit of a conditional numerical compiler/query interface. It is +not a numerical CRT evaluator, payload permutation implementation, production +placement certificate, native/outer theorem, or independent human review. +Finite Python results are not an asymptotic cost proof. + +## A constructive uniform simulation bound + +Let `n=2^h`, `1<=h<=ell<=p`, and `B=p+2`. Input is a fixed-width encoded list of +exactly `n` integers, each with `O(B)` bits, together with encoded parameters. +An implementation validates that the list is a permutation of `[0,n)`. The +cost bound is for this bounded encoding; an unbounded malformed byte stream +is not silently included in the same input-size claim. + +A single finite-alphabet multitape machine can implement the following +simulation, with a tape count independent of `p`, `ell`, and recursion depth. + +1. Store every recursive node in one flattened work region. Reserve each + node's permutation, inverse, color vector, explicit pending-vertex stack, + child vectors, result layers, and a constant number of frame descriptors. + A complete binary tree determines the capacities from `h`; it is not a + separately supplied circuit or per-size advice. At depth `d`, the total + wire count is `n`. Keeping each node's complete result costs + `O(n(h-d))` entries at that depth. Thus all levels need `O(n B^2)` + fixed-width slots, including conservative descriptor and temporary space. + Each slot, including its address/type encoding, needs `O(B)` bits, so a + work region of `W=O(n B^3)` bits suffices. This also accommodates the + `O(log W)=O(B)`-bit global slot addresses. +2. Implement host recursion as a depth-first state machine whose pending + node, child phase, indices, and saved loop state live in those descriptors. + Push/pop and table copies are ordinary encoded reads/writes. No new tape + appears at a child call, and recursion/garbage collection is not free. +3. Avoid assuming a unit-cost `sorted`. At each node, range-check every image + and compare every pair for duplication. For a node of size `m`, this is + `O(m^2)` word actions. Across all nodes, + `sum_d 2^d(n/2^d)^2 < 2n^2`. The coloring loop pushes a vertex only once, + processes two incident edges when it pops it, and therefore takes `O(m)` + word actions, apart from validation. Building child vectors is `O(m)`. + The output has `2 log2(m)-1` tables of length `m`; merging child tables + therefore uses `O(m log m)` word actions. Across all nodes the latter is + `O(n h^2)`. A bound of `O(n^2 B^3)` elementary register/array actions is + ample for all loop management, encoded-address calculations and copies. + This loose allowance is not a measured finite-fixture count. +4. Replace each indexed array access by a complete sequential traversal of + the work region, plus return to its marked beginning. Decode/compare a + fixed-width slot address and increment the scan counter using at most + `O(B^2)` bit steps per visited encoded bit, an intentionally loose bound. + Keep the target address and read/write word on fixed scratch tapes. Thus + every abstract access, including descriptor access and stack access, + costs at most `O(W B^2)=O(n B^5)` bit steps. Any schoolbook arithmetic on + the `O(B)`-bit registers also fits this allowance. Sequential scan/return + moves every physical head; a symbolic reset or free random access is not + used. +5. Query a table by the same scans. A requested switch lookup or following + all `2h-1` layers adds at most `O(B)` such accesses, after reading/validating + its encoded query arguments. Direct and inverse address-map evaluation + can compile the inverse permutation as another bounded invocation or + follow the involutive layers in reverse. Copy any promised output to + its owned output region, then erase the work region and return all heads. + Allocation, output copying and cleanup are bounded by the same costs. + +The resulting conservative compiler-plus-query time is + +``` +O(n^2 B^3) * O(n B^5) = O(n^3 B^8), +``` + +and workspace is `O(n B^3)` bits, in addition to the promised input and owned +output. Since `n<=2^ell`, this is below a fixed multiple of +`2^(4 ell)(p+2)^16`. Up to `O(p)` separately compiled axis controls still cost +`O(2^(3 ell) B^9)` and fit the same generous envelope. Reuse the work region +between those invocations. This latter statement does not supply their +numerical offsets or prove the full CRT arithmetic routine's bound. + +## Pitfalls the primary proof must exclude + +- Array length and table entries are encoded bits, not unit-cost Python + integers, tuples or arbitrary record labels. +- `sorted`, dynamic allocation, tuple comprehensions, recursive calls and + list indexing need the explicit lowering above or another paid lowering. +- `run_network` table queries must pay for the current encoded address and + return heads after each scan; table lookup is not an oracle. +- Validation, inverse construction, DFS initialization, copying result layers, + reading input parameters, allocation, erasure and head returns must be + covered. Output preservation/ownership must be stated explicitly. +- Invalid-permutation rejection is part of the numerical compiler. Correct + network behavior on all padded record labels is a different finite semantic + property. Neither result proves that a source guard or target placement is + production-valid. +- Any query/compilation certificate must say which executable source bytes it + authenticates. Finite counts are evidence of that implementation's behavior; + they do not quantify the asymptotic simulation constant. + +Conclusion: no obstruction was found to a uniform finite-alphabet sequential +simulation inside the retained generous envelope. The explicit construction +above supplies a conditional bound for this compiler/query component. Its +mechanism is the predecessor's full-scan argument, not a new routing method. + +## Review of the submitted tagged-arena construction + +I separately read the submitted `verify.py`, `PROOF.md`, `README.md` and +`RESULT.json`. Its more specific all-node record census is +`J=N(h^2+3h+1)`, with five fields of width `w=4p+8` per record. The three +per-node arrays contribute `3Nh`, all result layers contribute `Nh^2`, +and the shared explicit DFS stack contributes `N` records. The stated +`B=5wJ` arena length, field widths and global-offset bound are sufficient. +Constant-depth nested loops need a fixed number of scalar roles, not a +host recursion stack. Candidate/supplied key buffers, all loop counters, +parameters, values and arithmetic temporaries fit the stated fixed bank. + +Independently counting the modeled operations gives: + +- One arena access: `(14J+1)w` arena actions and `(12J+24)w` key-tape + actions, summing to `(26J+25)w`. +- Arena initialization and complete erase/return: `6B` actions. +- Modeled protected permutation reading/return: `3Nh`; serialized network + writing/return: `3(2h-1)N`. +- One complete network query, owned bit and returns: `3(2h-1)N+3`. +- Pairwise-validation comparisons: `N^2-N-Nh/2`, plus `Nh` first reads. +- Nonleaf construction: `20N(h-1)` arena accesses. This counts `11m` + coloring/stack accesses, `2m` inverse accesses, and `7m` first/last/child + accesses at a node of size `m`; component-start and discovery counts + cancel their dependence on the number of connected components. +- Leaves: `3N/2`; bottom-up merging: `2N(h-1)^2`; root loading and output + serialization together: `2Nh`. + +These sum exactly to the implementation gate +`A=N^2+2Nh^2+(37Nh-35N)/2`, independently of the finite fixture receipts. +Its bound `O((A+J+1)B(p+2)^2)=O(N^3(p+2)^7)` is a valid conservative +written lowering. The more general bound above is deliberately looser. +Both fit the retained generous envelope, including at most `O(p)` repeated +component invocations. + +The final interface explicitly bounds canonical parameter encodings and +fixed-width query fields; arbitrary leading-zero streams are excluded. +Header decoding, host pre-admission length/format checks and bounded scalar +microcode are paid by the written lowering. They are not claimed as +executed tape-transition evidence. The modeled query now checks every +network byte for binary format. Successful calls preserve protected inputs, +serialize their owned output before clearing private work, and return heads. +Owned queried-bit and compiler-output tapes are fixed reusable physical +roles; retaining many answers requires separately paid transfer/storage. + +I found no material correctness, encoding, cost or output-ownership defect +in this component after those clarifications. Normal and optimized Python +replays are recorded in the accompanying portable receipt. They corroborate +the explicit arena implementation; the asymptotic argument is the written +construction, not an inference from their operation totals. No literal +finite-state transition table or proof-assistant verification is supplied. diff --git a/research/crt-benes-scan/INITIAL-REVIEW.json b/research/crt-benes-scan/INITIAL-REVIEW.json new file mode 100644 index 0000000000..dbce84e27e --- /dev/null +++ b/research/crt-benes-scan/INITIAL-REVIEW.json @@ -0,0 +1,79 @@ +{ + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "before_primary_implementation_read": true, + "files": { + "INITIAL-REVIEW.md": "f91aa4430ccfc52b5bf3329501567a73a2fe3f64b2af9b4a0ec11e213a9a8440", + "independent_benes_oracle.py": "7a58689072b730201a6b4007f7b2524db2abff460a3116cfa42821fb2e1b63a5" + }, + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "runs": [ + { + "argv_template": [ + "{python}", + "-I", + "-B", + "independent_benes_oracle.py" + ], + "exit_code": 0, + "receipt": { + "control_columns": 1630756, + "endpoint_columns": 324452, + "endpoint_sha256": "18eaafe42f0dac6b173dc4a2fa2fceb74064e89fe6d1a24306473e5be61ebd27", + "negative_control": { + "expected": 0, + "input": 0, + "mutation": "interchange the child selector parity", + "permutation": [ + 0, + 2, + 1, + 3 + ], + "wrong": 3 + }, + "permutations": 40394, + "scope": "separate levelwise FIFO semantic oracle; host arrays and queues do not certify fixed-tape costs", + "status": "PASS_INDEPENDENT_BENES_SEMANTICS" + }, + "stderr": "" + }, + { + "argv_template": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "independent_benes_oracle.py" + ], + "exit_code": 0, + "receipt": { + "control_columns": 1630756, + "endpoint_columns": 324452, + "endpoint_sha256": "18eaafe42f0dac6b173dc4a2fa2fceb74064e89fe6d1a24306473e5be61ebd27", + "negative_control": { + "expected": 0, + "input": 0, + "mutation": "interchange the child selector parity", + "permutation": [ + 0, + 2, + 1, + 3 + ], + "wrong": 3 + }, + "permutations": 40394, + "scope": "separate levelwise FIFO semantic oracle; host arrays and queues do not certify fixed-tape costs", + "status": "PASS_INDEPENDENT_BENES_SEMANTICS" + }, + "stderr": "" + } + ], + "schema_version": 1, + "scope": "separate semantic oracle and quantified sufficient simulation bounds; no full E evaluator certification", + "source4100": "337d04939571a637aeab54a0f58f54fde811663a", + "status": "PASS_PREIMPLEMENTATION_INDEPENDENT_REVIEW", + "time_utc": "2026-10-20T12:19:43.598825+00:00" +} diff --git a/research/crt-benes-scan/INITIAL-REVIEW.md b/research/crt-benes-scan/INITIAL-REVIEW.md new file mode 100644 index 0000000000..4d34f656ac --- /dev/null +++ b/research/crt-benes-scan/INITIAL-REVIEW.md @@ -0,0 +1,99 @@ +# Independent preimplementation Beneš review + +Source context: canonical main `12fa8c5c844be21bfefb38a19503fbd867a11244`, +priority revision 7, Cinna Davis PR4100 source +`337d04939571a637aeab54a0f58f54fde811663a`, `CRT.md` Sections 2--4 and +the retained `check_batched_crt.py` Beneš routine. No primary candidate +implementation was read before this review and its separate oracle. + +## Quantified sufficient bounds + +Let N=2^h, 1<=h<=ell<=p. Values, array offsets, node identifiers and loop +counters use O(p+2)-bit encoded words, choosing their fixed constant after +the arena format is fixed. A number of tapes independent of p,h suffices. + +Retain the complete recursion tree in one encoded arena. There are N-1 +nodes with widths at least two. (Allowing explicit singleton leaves gives +at most 2N-1.) At depth a, the node widths sum to N. Each node of width n +has 2log2(n)-1 complete n-entry Boolean control tables. Therefore retaining +all node control tables uses exactly + + sum_(a=0)^(h-1) N[2(h-a)-1] = N h^2 + +Boolean entries. Permutations, inverses, colors and component stacks add +O(Nh) encoded words. Node/frame descriptors add O(Nh) words even with a +generous encoding. Thus fixed-width storage is + + S = O(N(h+1)^2(p+2)) <= O(N(p+2)^3) bits. + +Use an explicit serialized continuation/frame stack, or top-down node +generation followed by bottom-up merging. A host language call stack is +not evidence for a fixed inventory of sequential tapes. + +At a width-n node, range/distinctness validation can use O(n^2) pairwise +comparisons, replacing the uncharged host `sorted` call. Summing these +comparisons over all nodes gives less than 2N^2. The two-colored graph is +the union of two fixed-point-free involutions, x<->x XOR 1 and +x<->pi^-1(pi(x) XOR 1), hence a union of even alternating cycles. Each +vertex is colored/pushed once. Coloring, inverse creation and child +construction total O(Nh) logical word operations; table assembly totals +O(Nh^2). A sufficient overall logical bound is + + Q = O(N^2 + N(h+1)^2). + +Full sequential scans replace every indexed arena access. Bound a scan, +position bookkeeping, arithmetic, clearing and return conservatively by +O(S(p+2)^2) per logical operation. Taking the much looser source envelope +Q<=O(N^2(p+2)^6) therefore gives + + T <= O(N^3(p+2)^11) <= O(2^(3ell)(p+2)^11). + +Initialization, finite header markers and final arena clearing/head returns +are O(S(p+2)^2), inside this envelope. A stored control query can scan the +root table, and is also within this bound. There is ample slack under the +source's 2^(4ell)(p+2)^16 expression, but this proves only the isolated +compiler/query implication. It does not certify all source axis controls, +CRT reconstruction, modular inverses, macro inversion or full E evaluator. + +## Checks a literal simulator must expose + +- Arena/stack capacities must be independent of host object allocation; + indexes and graph work are encoded on a fixed tape inventory. +- Every indexed read/write, pop/push, validation operation and return is + charged. Host list/dict accesses can implement a semantic oracle, not an + uncharged tape primitive. Host integer arithmetic is not constant time. +- Output controls omit their own target bit. The universal bit schedule + is 0,1,...,h-1,...,1,0. Reversing complete layers implements the inverse. +- If a compiler returns a network, it must copy/protect owned output before + clearing the private arena. If it returns one query bit, all private + structures may be cleared while preserving that bit. A returned host + network must not hide uncharged output storage or head returns. +- A conceptual full-arena scan tariff is distinct from an actually + executed cell/head model. Counts from a Python host trace must not be + described as literal sequential steps unless each scan is performed. + +## Separate finite semantic oracle + +`independent_benes_oracle.py` uses FIFO component coloring, explicit +top-down nodes and bottom-up table assembly. It was written before reading +the primary candidate. It is a semantic oracle using host queues/arrays, +not a tape-cost implementation. + +Ordinary replay passed all permutations at N=2,4,8 and 16 deterministic +shuffles each at N=16,32,64: 40,394 permutations, 324,452 endpoint columns, +1,630,756 control columns. Every control omits its target, all endpoints +equal their supplied permutations, and reverse layers invert them. +Swapping child-selector parity fails at permutation (0,2,1,3), input 0, +with wrong output 3 instead of 0. This guards against silent child-port +orientation errors. + +## Scope and credit + +Cinna Davis supplies the audited source compiler and proposed full bound; +the retained NOTICE preserves the Beneš/CRT and routing lineage. This is +separate-agent OpenAI Codex review, not independent human review or a +formal-kernel proof. No new kappa or selected-frontier change is asserted. + +Remaining obligations: authenticate the actual simulator and its complete +operation/arena trace, then separately bind every other component of the +full uniform E evaluator and its production caller. diff --git a/research/crt-benes-scan/NOTICE.md b/research/crt-benes-scan/NOTICE.md new file mode 100644 index 0000000000..6ca47019de --- /dev/null +++ b/research/crt-benes-scan/NOTICE.md @@ -0,0 +1,7 @@ +# Attribution and license + +New component proof, arena simulation, independent FIFO oracle and packaging: ToikY, with substantial OpenAI Codex assistance. Apache-2.0. Separate-agent reviews are not independent human reviews or proof-assistant acceptance. + +Cinna Davis supplies PR4100’s original Beneš compiler and full-scan simulation proposal. The three declared predecessor inputs remain unchanged, including their complete NOTICE lineage. Hiroki KUMAZAKI’s PR4174 provides reservoir/evaluator context; PR4187’s last-K lowering is separate and not imported. + +The initial oracle review predates primary-code inspection. The separate cost review confirms the encoded interface and written lowering, while finite tape-traffic evidence excludes unexecuted scalar/header microcode. All research claims remain scoped as described in PROOF.md and TASK.json. diff --git a/research/crt-benes-scan/PROOF.md b/research/crt-benes-scan/PROOF.md new file mode 100644 index 0000000000..af1ea10b9d --- /dev/null +++ b/research/crt-benes-scan/PROOF.md @@ -0,0 +1,258 @@ +# Uniform sequential-arena Beneš compiler and queried bit + +This is a component audit of Cinna Davis's PR4100 `CRT.md:94–116` and +retained `check_batched_crt.py:12–50`. The original compiler, cycle +coloring and proposed full-scan simulation are predecessor work. This +note supplies a uniform encoded schedule, explicit arena traffic and +owned-output cleanup. It does not supply the complete CRT evaluator. + +## 1. Exact component interface + +Inputs use canonical self-delimiting binary encodings of positive integers +`h,p` (for example Elias gamma), of total O(log(p+2)) bits, with +`1<=h<=p`, and a **complete** permutation of `N=2^h` wires, as N +consecutive h-bit words on a protected sequential input tape. The +source tape is preserved. The program rejects repeated or out-of-range +entries; it does not call an uncharged sorting routine. + +The owned output contains `(2h-1)N` Boolean table entries in layer-major, +then wire-major order. The known layer schedule is + +``` +0,1,...,h-1,h-2,...,0. +``` + +A second interface takes that protected encoded network and `layer,address` +in fixed fields of widths `max(1,ceil(log2(2h-1)))` and h, respectively, +scans the whole network, and returns one owned bit. There are no arbitrary +leading-zero header strings or unbounded encodings within this input domain. +The finite simulator receives the decoded header integers; canonical header +decoding is part of the written uniform lowering, not executed microcode. +On successful calls all input/output heads return to their left markers. All private arena, +key and bounded-register workspace is cleared and returned. Uniform +parameters are read as data; no size-specific code, advice table or +random-access oracle is supplied. + +The alphabet is fixed: bit zero, bit one, blank and boundary markers. +The number of sequential tapes is fixed. A constant number of binary +registers and arithmetic scratch regions may occupy a fixed tape bank; +their widths are data, not new tapes or control states. +The owned output and owned queried-bit tape are fixed **roles**, reused +after their consumer transfers/clears the previous result. Python Tape +objects in the fixture model configurations, not newly allocated physical +tapes. A caller retaining many answers must serialize them to a fixed +output region and pay its additional copy/head movements. + +## 2. Flattened recursion and explicit stack + +Use binary-heap node IDs: root 1 and children `2v,2v+1`. Nodes at depth +`a=0,...,h-1` have size `m=N/2^a` and height `s=h-a`. Leaves have m=2. +For each node preallocate arrays P, INV and COLOR of m words and OUT +with `(2s-1)m` Boolean entries. Preallocate one shared N-entry DFS stack. +Every entry is a fixed-width record + +``` +(node,kind,layer,index,value), each field w=4p+8 bits. +``` + +Record kinds form a fixed finite set. No dictionary, object pointer, +host-index lookup or tape per node is part of this program. The record +layout is generated by fixed nested counter loops over depth, node, +kind, layer and index. There are exactly + +``` +J = N(h²+3h+1) records, +B = 5wJ arena cells. (1) +``` + +Indeed the all-node Boolean tables contribute `Nh²` entries, since +`sum_(s=1)^h (2s-1)=h²`; the three other arrays contribute `3Nh` +and the shared stack contributes N. All widths are explicit, including +unused padding in the Boolean values. + +Every logical get or put constructs its four-field key on **one reused +key tape**. It scans all J records from the left marker, compares all +four key words, reads or replaces the matching value, continues to the +end and returns the arena head. It returns the key head after each +comparison, then clears and returns that scratch tape. There is one +matching record. It may skip an unmatched value by w consecutive +right moves; this is not a jump to an addressed record. + +Copy the incoming permutation to root P. Process nodes in increasing +depth, using only bounded loop counters: + +1. Validate each node's P by range checks and pairwise distinctness. +2. For m=2, write its one identical-bit switch table and continue. +3. Otherwise build INV; then visit initial wires in increasing order. + For an uncolored wire assign color zero and push it on the shared + encoded stack. Pop in LIFO order and inspect neighbors, in this + order, `x XOR 1`, `INV[P[x] XOR 1]`. Mark a newly discovered vertex + before pushing it. Clear each popped stack entry immediately. +4. Write first/last tables and both child permutations, exactly as in + the retained compiler. + +No Python recursion stack is used by `compile_stream`. The graph DFS +stack is the explicit arena array; its top is a bounded register. +Each vertex is pushed and popped once, so capacity N suffices. +At the end of each node the stack is empty and its slots are cleared. + +Then process depths in decreasing order. Interleave each pair of +child tables using child `x mod 2` and child wire `floor(x/2)`; +write parent layers shifted up by one. Finally copy the entire root +table into the owned output using charged arena gets and sequential +output writes. Only **after** serialization erase the whole private +arena and return its head. There is no returned host list that silently +owns an uncharged network copy. + +## 3. Source equivalence and endpoint + +The two input-neighbor relations are perfect matchings. Their union +is a disjoint union of alternating even cycles, allowing parallel +matching edges. Opposite colors exist. Mark-before-push means each +vertex enters the stack once. The traversal order within a node is +the same as the source, so component orientation and every resulting +color agree exactly, not just up to an equivalent network. + +Every input pair and every output pair has one member of each color. +For each color c, `floor(x/2) -> floor(P[x]/2)` is therefore a +permutation on m/2 wires. This proves child validation and permits +induction. Distinct child calls share no state: replacing source DFS +recursion by top-down construction and bottom-up assembly preserves +the returned tables byte for byte. The first/last tables and child +selector use precisely the source formulas. + +Induction gives the desired permutation endpoint. First and last +tables are equal on the two wires of their target pair because +matching colors differ. An interior table inherits target independence +from its child: flipping its higher target bit preserves the selected +child parity. Thus each returned queried bit is independent of its +own active target bit. This is a theorem about the component; it +does not establish the full CRT caller's simultaneous target omission. + +## 4. Traffic, scalar lowering and quantified bound + +There are three separate statements: the **executed arena/key cell +invoice**, the **written bounded-scalar lowering**, and the resulting +**uniform asymptotic bit bound**. The Python simulator is not a +complete finite-state transition-table certificate. + +For a logical arena access, the arena/key tapes execute exactly + +``` +26wJ + 25w read/write/one-cell-head actions. (2) +``` + +Arena key reads cost `8wJ`; unmatched value skips plus the matching +read/write cost `wJ+w`; arena return costs `5wJ`. Key comparisons +read/return `12wJ`, and constructing/clearing/returning its key costs +24w. Sum these terms to obtain (2). Initialization and final arena +erasure/returns add `6B`. The modeled protected input read/return costs `3Nh`; +this excludes the host pre-admission length/bit-format checks. Their sequential +implementation is separately charged in the written scalar lowering below. +Owned network writing/return costs `3(2h-1)N`. Each complete query scan, +return and one-bit owned output costs exactly `3(2h-1)N+3` tape actions. +These exact numbers exclude scalar instruction work, not its cost. + +The finite simulator batches a contiguous block read/write/move by +charging the corresponding number of repeated one-cell operations. +Such methods advance from the current head only. An expanded one-cell +execution is checked against the batched version on the same case. +They have identical tape contents, heads and traffic. Byte slices used +to batch those moves are not indexed logical-array access instructions. + +To lower the remaining control, use a fixed bank of O(1) w-bit +registers with binary counters. Every integer comparison, copy, +increment, halving, parity/XOR, add, or schoolbook product used here +has a fixed sequential implementation in O(w²) time and O(w²) scratch, +including local head returns. Key equality is a streaming equality +flag, not an uncharged comparison of host strings. Input bit-format +checks, record construction, all loop/index/key generation and query +selection counters are charged by the same conservative envelope. +The Python integer mirrors are observations of this bounded control; +they are not treated as unit-cost machine arithmetic. +The bank explicitly includes candidate and supplied four-word key +buffers, the decoded value, parameters, node/depth/layer/index/top +counters and a fixed number of temporary arithmetic words. These +are O(1) fixed-width roles, not host lists growing with N. Reading +encoded parameters and clearing/returning every such private role +are included in the envelope. + +The width also covers full arena offsets, rather than only wire IDs: + +``` +B <= 20 * 2^p * (p+2)^3 + <= 160 * 2^(4p) < 2^(4p+8) = 2^w. (3) +``` + +Here `p+2<=2^(p+1)` for p>=1. All node IDs, values, sentinels, +depth/layer indices, DFS tops and record/cell loop counters fit in w +bits. Observer-only accumulated receipt counters need not be runtime +registers. A product may use two w-bit registers while being reduced +to a known in-range result. No growing collection of scalar registers +is hidden in the bound. + +Let A be the number of logical arena accesses. Across depths, total +node-size is Nh. Pairwise validation uses `N²-N-Nh/2` comparisons; +initial reads add Nh. At a nonleaf node with m wires and c components, +coloring uses m initial tests, 2c component-start accesses, 2m stack +pop/clear accesses, 6m edge accesses and `2(m-c)` discovery writes: +exactly 11m. Inverse and first/last/child construction add 2m and 7m, +giving exactly 20m nonleaf accesses. Bottom-up assembly uses +`2N(h-1)²` accesses. Root loading/serialization add `N+(2h-1)N`; +leaves add `3N/2`. Thus the exact valid-input census and a convenient +conservative bound are + +``` +A = N² + 2Nh² + (37Nh-35N)/2, +A <= N² + 2Nh² + 24Nh + 3N = O(N²(p+2)²). (4) +``` + +The displayed bound is conservative; it is derived from the loops, +not fitted to finite receipts. Loop control outside scans has +O(A+J) iterations. Scan/key comparison control has O(B) elementary +cell/word iterations per access. Charging each bounded scalar +instruction by O(w²), including its register access, gives + +``` +T_compile = O((A+J+1) B (p+2)²) + = O(N³ (p+2)^7), (5) +visited space = O(B+(p+2)²+Nh) = O(N(p+2)^3). (6) +``` + +Owned output and protected input are included in visited space. +The fixed inventory is the arena, reused key tape, input, owned +output, and a fixed scalar-work bank. The queried-bit interface uses +the protected output, one new owned bit, and that same fixed bank; +its time O(N(p+2)^3) is absorbed by (5). Register-work erasure/returns +are included in the scalar envelope. All parameters have one uniform +encoded implementation, independent of input size. + +For the source family `1<=h<=ell<=p`, (5) is bounded by +`O(2^(3ell)(p+2)^7)`, hence by the stated `O(2^(4ell)(p+2)^16)` E +allowance after a fixed constant. Even O(p) such component invocations +fit that allowance. This comparison does **not** certify all the +other work charged to E: CRT reconstruction/modular inversion, +transported descriptors, macro inverse keys, parameter generation +and the complete evaluator remain separate obligations. + +## 5. Corroboration and remaining boundary + +`verify.py` checks exact retained source bytes before calling its +reference compiler. Its executed arena traffic covers every get/put, +all DFS data, table serialization, erasure and head returns. Scalar +microcode is justified by the written construction above; its complete +literal transition table is not emitted or executed. No native or +full outer replay is represented by these tests. + +Finite cases include all permutations on two/four wires, modular +rotations and other eight/sixteen-wire permutations. Every output +table is compared exactly to the retained source, every query and +its target independence is checked, and every wire endpoint is +checked. Mutation/admission controls cover malformed encodings, +duplicate permutations, an incorrect matching edge, and missing +arena/query head returns. All checks remain active under Python -O. + +The result is a scoped constructive component proof plus independently +replayable corroboration. It is not a complete CRT evaluator, physical +ordinary interchange, native/precision closure, multiplication theorem +or selected-frontier change. diff --git a/research/crt-benes-scan/README.md b/research/crt-benes-scan/README.md new file mode 100644 index 0000000000..33b8678615 --- /dev/null +++ b/research/crt-benes-scan/README.md @@ -0,0 +1,94 @@ +# Uniform sequential-arena Beneš component + +This audits the numerical compiler component in Cinna Davis's PR4100 +`CRT.md:94–116`, using the exact retained `benes` implementation. +The original cycle compiler and proposed full-scan simulation are +predecessor work. The new result is an explicit uniform arena schedule, +owned-output cleanup, quantified lowering and executed traffic model. +No new kappa or complete multiplication theorem is claimed. + +For an encoded permutation on `N=2^h` wires, `1<=h<=p`, the component +returns the exact source's layer-major Boolean tables while preserving +the input. It flattens the recursion tree, uses an encoded LIFO stack +for cycle coloring, and reads/writes each logical array entry by a +**complete sequential arena scan and head return**. One key tape is +reused throughout. No tape is allocated per node or query. + +[PROOF.md](PROOF.md) derives `O(N³(p+2)^7)` time and `O(N(p+2)^3)` +visited space with a fixed alphabet/tape inventory. Both source and +owned output are included. A protected-network query returns an owned +bit after a complete scan. For `h<=ell<=p`, even O(p) component calls +fit the source's generous `O(2^(4ell)(p+2)^16)` allowance. + +The executed simulator charges arena/key tape read/write/head traffic. +It batches contiguous one-cell moves with exact action counts and +cross-checks an expanded one-cell run. Python integers mirror bounded +scalar registers; their uniform bit lowering, all loop/index arithmetic +and parameter reads are charged in the **written proof**. This is not +an executed complete finite-state transition-table certificate. + +## Evidence and replay + +[RESULT.json](RESULT.json) records 49 finite cases: all 26 permutations +on two/four wires, 20 modular rotations, and two other eight-wire +permutations, plus one larger-p word-width case. Each encoded table matches the retained compiler +exactly; every queried control bit and target independence, full wire +endpoints, complete arena/key scans, owned output and cleanup/returns +are checked. Inputs include non-rotation permutations, not merely the +source caller's easiest constants. The explicit negative controls +check duplicate/malformed inputs, an incorrect coloring edge and +missing arena/query head returns, and a nonselected corrupt network bit. + +The three exact predecessor inputs are authenticated by SHA256 and +Git blob in [SOURCE-PINS.json](SOURCE-PINS.json). The verifier compiles +those authenticated source bytes directly rather than cached bytecode. +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -B research/crt-benes-scan/verify.py +python3.12 -I -O -W error -B research/crt-benes-scan/verify.py +``` + +Normal replay reproduces and compares the stored receipt without +rewriting it. `--write-result` is the explicit regeneration option. +Observer comparisons and source authentication are verification work; +they are not covert instructions of the claimed compiler. + +The six registered commands in [VERIFY.json](VERIFY.json) also run a +[separately written FIFO oracle](independent_benes_oracle.py): all permutations +on2/4/8wires plus48 deterministic larger cases,40,394permutations / +324,452endpoint columns /1,630,756control columns. Its child-port mutation +produces an exact wrong endpoint. [INITIAL-REVIEW.json](INITIAL-REVIEW.json) +records that oracle before reading the primary implementation. +A [source-pinned cross-check](cross_check.py) compares primary tables, +forward/inverse endpoints and848 queries on37 cases directly to that oracle; +[CROSS-CHECK.json](CROSS-CHECK.json) records its normal/optimized runs. + +[COST-REVIEW.json](COST-REVIEW.json) records the separate encoding/cost review. + +## Open next questions + +Bind this component to the **complete** uniform CRT control evaluator: +encoded moduli/CRT reconstruction, modular inverses, transported +split-axis descriptors, forward/inverse macro keys, their cleanup +and parameter construction. A feasible first step is one actual +root-axis query with all arithmetic loops and field reconstruction +lowered to sequential records. This package takes the encoded +permutation as input; it does not obtain that permutation for free +inside the full caller. + +The source's complete E bound, production placement and ordinary +interchange callee, sparse repair, last-K caller, precision/native +closure and outer multiplication theorem remain separate obligations. +Finite agreement and an asymptotic component bound do not certify them. + +## Credit + +Cinna Davis supplies PR4100's original compiler, CRT construction +and full-scan proposal. Douglas Colkitt and OpenAI's framework, +the retained routing/compact-control lineage, Hiroki KUMAZAKI's +PR4174 placement audit and the source NOTICE retain their credit. +This contribution supplies a component lowering and audit, not a +new Beneš mechanism or a full CRT theorem. Prepared with substantial +OpenAI Codex assistance. Apache-2.0. No independent human review or +proof-assistant formalization is claimed. diff --git a/research/crt-benes-scan/RESULT.json b/research/crt-benes-scan/RESULT.json new file mode 100644 index 0000000000..c64ff9af4f --- /dev/null +++ b/research/crt-benes-scan/RESULT.json @@ -0,0 +1,103 @@ +{ + "schema_version": 1, + "result": "PASS_UNIFORM_BENES_SCAN_COMPONENT", + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "source_inputs_checked": 3, + "finite": { + "cases": 49, + "categories": { + "all_permutations": 26, + "modular_rotation": 20, + "arbitrary": 2, + "wider_parameter": 1 + }, + "permutation_endpoints": 284, + "queried_control_bits": 1260, + "logical_accesses": 15984, + "records_scanned": 3583480, + "arena_and_key_tape_actions": 2102126536, + "maximum_arena_cells": 55680, + "maximum_dfs_entries": 2, + "expanded_one_cell_case": [ + 2, + 0, + 3, + 1 + ], + "receipt_sha256": "9d8ad5da3e02b124cc8d41d860f302dbe9fb0f21a5dac906e1867cfdfbb2e989", + "largest_case": { + "record_width_bits": 120, + "word_width_bits": 24, + "arena_records": 464, + "arena_cells": 55680, + "logical_accesses": 1672, + "get_calls": 1160, + "put_calls": 512, + "records_scanned": 775808, + "arena_and_key_scan_actions": 485107392, + "arena_initialization_cleanup_actions": 334080, + "arena_and_key_tape_actions": 485441472, + "private_arena_erased": true, + "private_heads_returned": true, + "h": 4, + "p": 4, + "wires": 16, + "input_bits": 64, + "input_tape_actions": 192, + "owned_output_bits": 112, + "owned_output_tape_actions": 336, + "validation_pairs": 208, + "dfs_pushes": 48, + "dfs_pops": 48, + "maximum_dfs_entries": 1, + "queries": 112, + "query_tape_actions": 37968, + "owned_output_sha256": "9b0ec2510d12d2e5eef1d354977cdf8a6a2d91987e2c342c685d4500db19ab06" + }, + "wider_parameter_case": { + "record_width_bits": 180, + "word_width_bits": 36, + "arena_records": 44, + "arena_cells": 7920, + "logical_accesses": 126, + "get_calls": 86, + "put_calls": 40, + "records_scanned": 5544, + "arena_and_key_scan_actions": 5302584, + "arena_initialization_cleanup_actions": 47520, + "arena_and_key_tape_actions": 5350104, + "private_arena_erased": true, + "private_heads_returned": true, + "h": 2, + "p": 7, + "wires": 4, + "input_bits": 8, + "input_tape_actions": 24, + "owned_output_bits": 12, + "owned_output_tape_actions": 36, + "validation_pairs": 8, + "dfs_pushes": 4, + "dfs_pops": 4, + "maximum_dfs_entries": 1, + "queries": 12, + "query_tape_actions": 468, + "owned_output_sha256": "dd69fd879e7b98463d5b172e1f59f244ab58d7fc768135c74af312edba5dd94e" + } + }, + "negative_controls": [ + "duplicate input permutation", + "incomplete input encoding", + "h exceeds p", + "wrong inverse-permutation matching edge", + "missing arena head return", + "missing query return and tariff", + "nonselected nonbinary network entry" + ], + "limitations": [ + "Executed model charges sequential tape cells/heads; bounded scalar lowering is the written proof.", + "Canonical header decoding and pre-admission format checks are written lowerings, not executed microcode.", + "No literal complete finite-state transition table or proof-assistant formalization.", + "Bene\u0161 component only; no full CRT arithmetic/control evaluator or production placement.", + "No ordinary interchange, precision/native/outer multiplication theorem or new kappa." + ] +} diff --git a/research/crt-benes-scan/SOURCE-PINS.json b/research/crt-benes-scan/SOURCE-PINS.json new file mode 100644 index 0000000000..f4c01fc0ec --- /dev/null +++ b/research/crt-benes-scan/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-benes-scan/SOURCES.json b/research/crt-benes-scan/SOURCES.json new file mode 100644 index 0000000000..3cd7684219 --- /dev/null +++ b/research/crt-benes-scan/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-benes-scan/TASK.json b/research/crt-benes-scan/TASK.json new file mode 100644 index 0000000000..2c4d31b34e --- /dev/null +++ b/research/crt-benes-scan/TASK.json @@ -0,0 +1,74 @@ +{ + "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": "Audit and lower the retained PR4100 Bene\u0161 permutation-to-switch-table compiler and table query to a uniform encoded fixed-tape scan procedure, with every indexed access, stack, allocation, cleanup and head return charged for1<=h<=ell<=p.", + "scope_change_reason": "The current E-evaluator handoff leaves complete control work open. This isolates one numerical compiler/query component, distinct from PR4187 tail lowering, PR4174 reservoir placement and PR4169 repair; full CRT arithmetic/control generation remains separate.", + "bottleneck_link": "Dense/sparse amortization requires a uniformly bounded numerical control computation. A literal lowered Bene\u0161 component with an explicit bit-cost proof supports that dependency without treating finite tables or Python indexing as a machine-cost theorem.", + "budget_minutes": 60, + "stop_rule": "Stop science by2026-10-20T12:58:26Z and reserve final15minutes until13:13:26Z for committed-byte/history/cold/hosted verification, refreshed main/overlap and handoff. Stop at one compiler/query implication whether positive, partial or negative.", + "outcome": "completed", + "evidence": "PROOF.md quantifies uniform finite-alphabet lowering and exact access/storage invoices; RESULT.json authenticates49 executed arena cases; independent FIFO oracle covers40394permutations; independent cost/encoding review pins stable algorithm and proof. Full CRT E excluded.", + "author": "ToikY, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance: primary implementation agent, separate mathematical/oracle agent, separate encoded-machine cost review agent and coordinating agent. No independent human review or proof-assistant acceptance.", + "open_questions": [ + { + "question": "Can the complete CRT numerical control evaluator be bound to the actual encoded source parameters, arithmetic and placed-coordinate descriptors within E(p,ell)?", + "why_it_matters": "The Bene\u0161 compiler/query is one component; full reconstruction, modular inverses, descriptor transport and gadget address maps remain necessary for the total evaluator bound.", + "first_step": "Reuse this source-pinned component and PR4174 descriptors, specify a uniform encoded CRT reconstruction/modular-arithmetic machine and price composition including all owned output, erasure and returns.", + "blocked_by": "Outside the present compiler/query component; no uncharged arithmetic oracle may be inferred." + } + ] +} diff --git a/research/crt-benes-scan/VERIFY.json b/research/crt-benes-scan/VERIFY.json new file mode 100644 index 0000000000..b63a399b7c --- /dev/null +++ b/research/crt-benes-scan/VERIFY.json @@ -0,0 +1,86 @@ +{ + "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": "Authenticate retained source,49 encoded arena cases, exact access/traffic/ownership and admission/semantic/head-return controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate retained source,49 encoded arena cases, exact access/traffic/ownership and admission/semantic/head-return controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent_benes_oracle.py" + ], + "timeout_seconds": 120, + "checks": "Separate FIFO compiler on40394permutations,324452endpoints,1630756target-independent controls and child-parity mutation." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent_benes_oracle.py" + ], + "timeout_seconds": 120, + "checks": "Separate FIFO compiler on40394permutations,324452endpoints,1630756target-independent controls and child-parity mutation." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/cross_check.py", + "{package}/verify.py", + "{package}/independent_benes_oracle.py" + ], + "timeout_seconds": 120, + "checks": "Hash-pin primary and preimplementation oracle;37 direct table/forward/reverse/query cases and exact logical-access census." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/cross_check.py", + "{package}/verify.py", + "{package}/independent_benes_oracle.py" + ], + "timeout_seconds": 120, + "checks": "Hash-pin primary and preimplementation oracle;37 direct table/forward/reverse/query cases and exact logical-access census." + } + ] +} diff --git a/research/crt-benes-scan/cross_check.py b/research/crt-benes-scan/cross_check.py new file mode 100644 index 0000000000..9e323de6dc --- /dev/null +++ b/research/crt-benes-scan/cross_check.py @@ -0,0 +1,82 @@ +"""Pin the primary scan compiler and compare a separately written FIFO oracle. + +This is finite semantic corroboration, not timing or a full CRT evaluator. +""" +import hashlib +from itertools import permutations +import json +from pathlib import Path +from random import Random +import sys +import types + + +PRIMARY_SHA256 = "e8ff7800ffa267d2825009656b78ab1613544b55301982744ec0d99f38800913" +ORACLE_SHA256 = "7a58689072b730201a6b4007f7b2524db2abff460a3116cfa42821fb2e1b63a5" + + +def load(path, name, expected=None): + path = Path(path) + data = path.read_bytes() + if expected is not None and hashlib.sha256(data).hexdigest() != expected: + raise ValueError("reviewed primary code changed") + module = types.ModuleType(name) + module.__file__ = str(path) + exec(compile(data, str(path), "exec"), module.__dict__) + return module + + +def main(): + primary = load(sys.argv[1], "_pinned_primary_benes", PRIMARY_SHA256) + independent = load(sys.argv[2], "_preimplementation_fifo_benes", ORACLE_SHA256) + cases = [] + for n in (2, 4): + cases.extend((tuple(p), n.bit_length() - 1) for p in permutations(range(n))) + rng = Random(4100) + for n, count in ((8, 8), (16, 2)): + for _ in range(count): + permutation = list(range(n)) + rng.shuffle(permutation) + cases.append((tuple(permutation), n.bit_length() - 1)) + cases.append(((0, 2, 1, 3), 7)) + count = columns = queries = 0 + digest = hashlib.sha256() + for permutation, p in cases: + n = len(permutation) + h = n.bit_length() - 1 + expected = independent.compile_levelwise(permutation) + encoded = b"".join(primary.word(x, h) for x in permutation) + network, invoice = primary.compile_stream(encoded, h, p) + actual = tuple(primary.unpack(network, h)) + if actual != expected: + raise ValueError("primary tables differ from separate FIFO compiler") + if invoice["arena_records"] != n * (h * h + 3 * h + 1): + raise ValueError("all-node storage census mismatch") + accesses = n * n + 2 * n * h * h + (37 * n * h - 35 * n) // 2 + if invoice["logical_accesses"] != accesses: + raise ValueError("independently derived access census mismatch") + for x, image in enumerate(permutation): + if independent.endpoint(actual, x) != image: + raise ValueError("direct permutation endpoint mismatch") + if independent.endpoint(tuple(reversed(actual)), image) != x: + raise ValueError("reverse-layer inverse endpoint mismatch") + for layer, (_, table) in enumerate(expected): + for address, wanted in enumerate(table): + answer, _ = primary.query_stream(network, h, layer, address) + if int(bytes(answer.data), 2) != wanted: + raise ValueError("queried bit differs from separate oracle") + queries += 1 + digest.update(bytes(network.data)) + count += 1 + columns += n + print(json.dumps({"status": "PASS_PRIMARY_VS_PREIMPLEMENTATION_ORACLE", + "cases": count, "endpoint_columns": columns, + "control_queries": queries, "owned_tables_sha256": digest.hexdigest(), + "primary_sha256": PRIMARY_SHA256, + "oracle_sha256": ORACLE_SHA256, + "scope": "source-pinned finite compiler/query equivalence and forward/reverse endpoints; not an asymptotic timing proof"}, + sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/crt-benes-scan/independent_benes_oracle.py b/research/crt-benes-scan/independent_benes_oracle.py new file mode 100644 index 0000000000..682d9a2b06 --- /dev/null +++ b/research/crt-benes-scan/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-benes-scan/verify.py b/research/crt-benes-scan/verify.py new file mode 100644 index 0000000000..e79a9ce3f3 --- /dev/null +++ b/research/crt-benes-scan/verify.py @@ -0,0 +1,450 @@ +"""Uniform sequential-arena Beneš component: cell/head model and scoped proof. + +Block tape methods batch repeated ONE-CELL operations, charging each cell. +They never perform an indexed arena lookup. Bounded scalar control is mirrored +by Python integers; its bit lowering is proved separately in PROOF.md. +""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path +import sys +import types + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +P, INV, COLOR, OUT, STACK = range(5) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def word(value, width): + need(isinstance(value, int) and 0 <= value < (1 << width), "encoded word range") + return format(value, "0%db" % width).encode() + + +class Tape: + """Alphabet {0,1,blank}, implicit left marker, one sequential head.""" + + def __init__(self, data=b"", expanded=False): + self.data = bytearray(data) + self.head = self.actions = 0 + self.expanded = expanded + + def read(self, count): + need(0 <= count and self.head + count <= len(self.data), "tape read bounds") + if self.expanded: + result = bytearray() + for _ in range(count): + result.append(self.data[self.head]) + self.head += 1 + self.actions += 2 + return bytes(result) + result = bytes(self.data[self.head:self.head + count]) + self.head += count + self.actions += 2 * count # count repetitions of READ; RIGHT. + return result + + def write(self, data): + if self.expanded: + for cell in data: + if self.head == len(self.data): + self.data.append(cell) + else: + self.data[self.head] = cell + self.head += 1 + self.actions += 2 + return + stop = self.head + len(data) + self.data[self.head:stop] = data + self.head = stop + self.actions += 2 * len(data) + + def skip(self, count): + need(0 <= count and self.head + count <= len(self.data), "tape move bounds") + if self.expanded: + for _ in range(count): + self.head += 1 + self.actions += 1 + else: + self.head += count + self.actions += count # count one-cell RIGHT operations. + + def rewind(self): + if self.expanded: + while self.head: + self.head -= 1 + self.actions += 1 + else: + self.actions += self.head + self.head = 0 + + def clear(self): + need(self.head == 0, "clear starts at left marker") + self.write(bytes(len(self.data))) # NUL encodes blank, distinct from ASCII 0/1. + self.rewind() + + +def descriptors(h): + n = 1 << h + for depth in range(h): + size = n >> depth + height = h - depth + for node in range(1 << depth, 1 << (depth + 1)): + for kind in (P, INV, COLOR): + for index in range(size): + yield (node, kind, 0, index), n if kind == COLOR else 0 + for layer in range(2 * height - 1): + for index in range(size): + yield (node, OUT, layer, index), 0 + for index in range(n): + yield (0, STACK, 0, index), n + + +class Arena: + """Fixed-width tagged records; EVERY get/put scans all records and returns.""" + + def __init__(self, h, p, expanded=False): + self.h, self.p, self.width = h, p, 4 * p + 8 + self.tape = Tape(expanded=expanded) + self.key_tape = Tape(expanded=expanded) + self.calls = self.records_scanned = self.scan_actions = 0 + self.key_actions = 0 + self.kinds = {"get": 0, "put": 0} + self.count = 0 + for key, initial in descriptors(h): + self.tape.write(b"".join(word(v, self.width) for v in key) + word(initial, self.width)) + self.count += 1 + self.tape.rewind() + n = 1 << h + need(self.count == n * (h * h + 3 * h + 1), "exact flattened arena census") + self.length = len(self.tape.data) + need(self.length == 5 * self.width * self.count, "fixed-width arena size") + + def access(self, key, value=None, omit_return=False): + need(self.tape.head == 0, "arena operation must start at left marker") + encoded = b"".join(word(v, self.width) for v in key) + key_tape = self.key_tape # One reused physical scratch tape, never a tape per call. + key_start = key_tape.actions + key_tape.write(encoded) + key_tape.rewind() + start = self.tape.actions + answer = None + found = 0 + for _ in range(self.count): + candidate = self.tape.read(4 * self.width) + supplied = key_tape.read(4 * self.width) + key_tape.rewind() + if candidate == supplied: + found += 1 + if value is None: + answer = int(self.tape.read(self.width), 2) + else: + self.tape.write(word(value, self.width)) + else: + self.tape.skip(self.width) + self.records_scanned += 1 + if not omit_return: + self.tape.rewind() + key_tape.clear() + need(found == 1, "tagged record must exist exactly once") + self.calls += 1 + self.kinds["get" if value is None else "put"] += 1 + self.scan_actions += self.tape.actions - start + self.key_actions += key_tape.actions - key_start + need(all(cell == 0 for cell in key_tape.data) and key_tape.head == 0, + "key scratch must be cleared/returned") + return answer + + def get(self, node, kind, index, layer=0): + return self.access((node, kind, layer, index)) + + def put(self, node, kind, index, value, layer=0): + self.access((node, kind, layer, index), value) + + def finish(self): + need(self.tape.head == 0, "arena final head return") + self.tape.clear() + need(all(cell == 0 for cell in self.tape.data), "private arena must be erased") + need(self.records_scanned == self.calls * self.count, "every logical access is a full scan") + # One matching value read/write adds w beyond the unmatched skip. + # The key tape is written, returned, reread/returned N times, erased/returned. + expected = self.calls * (26 * self.width * self.count + 25 * self.width) + need(self.scan_actions + self.key_actions == expected, "complete scan/key/head-return invoice") + return {"record_width_bits": 5 * self.width, + "word_width_bits": self.width, "arena_records": self.count, + "arena_cells": self.length, "logical_accesses": self.calls, + "get_calls": self.kinds["get"], "put_calls": self.kinds["put"], + "records_scanned": self.records_scanned, + "arena_and_key_scan_actions": self.scan_actions + self.key_actions, + "arena_initialization_cleanup_actions": 6 * self.length, + "arena_and_key_tape_actions": self.tape.actions + self.key_actions, + "private_arena_erased": True, "private_heads_returned": True} + + +def compile_stream(input_bits, h, p, expanded=False, wrong_neighbor=False): + """Uniform valid-input compiler; no host recursion, no indexed arena accesses. + + Input is the protected h-bit encoding of N permutation entries. Output is + the owned concatenation of the 2h-1 root switch tables, N bits per layer. + """ + need(isinstance(h, int) and isinstance(p, int) and 1 <= h <= p, "1<=h<=p") + n = 1 << h + need(len(input_bits) == n * h and all(cell in (48, 49) for cell in input_bits), + "complete binary permutation encoding") + incoming = Tape(input_bits, expanded=expanded) + arena = Arena(h, p, expanded) + for index in range(n): + arena.put(1, P, index, int(incoming.read(h), 2)) + incoming.rewind() + pushes = pops = max_stack = validation_pairs = 0 + + # Top-down recursion-tree schedule, not Python recursive calls. + for depth in range(h): + size = n >> depth + height = h - depth + for node in range(1 << depth, 1 << (depth + 1)): + # Explicit quadratic validation replaces the source's sorted call. + for x in range(size): + px = arena.get(node, P, x) + need(px < size, "permutation range") + for y in range(x): + need(arena.get(node, P, y) != px, "permutation distinctness") + validation_pairs += 1 + if size == 2: + bit = arena.get(node, P, 0) + arena.put(node, OUT, 0, bit) + arena.put(node, OUT, 1, bit) + continue + for x in range(size): + arena.put(node, INV, arena.get(node, P, x), x) + for initial in range(size): + if arena.get(node, COLOR, initial) != n: + continue + arena.put(node, COLOR, initial, 0) + top = 0 + arena.put(0, STACK, top, initial) + top += 1 + pushes += 1 + while top: + max_stack = max(max_stack, top) + top -= 1 + x = arena.get(0, STACK, top) + arena.put(0, STACK, top, n) + pops += 1 + for edge in (0, 1): + other = (x ^ 1 if edge == 0 else + arena.get(node, INV, arena.get(node, P, x) ^ (0 if wrong_neighbor else 1))) + opposite = arena.get(node, COLOR, x) ^ 1 + color = arena.get(node, COLOR, other) + if color == n: + arena.put(node, COLOR, other, opposite) + need(top < n, "encoded DFS capacity") + arena.put(0, STACK, top, other) + top += 1 + pushes += 1 + else: + need(color == opposite, "two perfect matching color constraints") + for x in range(size): + color = arena.get(node, COLOR, x) + arena.put(node, OUT, x, color ^ (x & 1), layer=0) + inverse = arena.get(node, INV, x) + last = arena.get(node, COLOR, inverse) ^ (x & 1) + arena.put(node, OUT, x, last, layer=2 * height - 2) + # Each input pair has exactly one representative of each color. + arena.put(2 * node + color, P, x // 2, arena.get(node, P, x) // 2) + + # Bottom-up assembly of complete child tables. + for depth in reversed(range(h - 1)): + size = n >> depth + height = h - depth + for node in range(1 << depth, 1 << (depth + 1)): + for layer in range(2 * height - 3): + for x in range(size): + value = arena.get(2 * node + (x & 1), OUT, x // 2, layer=layer) + arena.put(node, OUT, x, value, layer=layer + 1) + need(pushes == pops and max_stack <= n, "encoded DFS stack balanced") + # Serialize the OWNED root output before erasing every private arena cell. + output = Tape(expanded=expanded) + for layer in range(2 * h - 1): + for x in range(n): + output.write(word(arena.get(1, OUT, x, layer), 1)) + output.rewind() + # Observer gate: independently derived from validation/tree/DFS/merge sums. + expected_accesses = n * n + 2 * n * h * h + (37 * n * h - 35 * n) // 2 + need(arena.calls == expected_accesses, "derived exact logical-access census") + invoice = arena.finish() + invoice.update({"h": h, "p": p, "wires": n, + "input_bits": len(input_bits), "input_tape_actions": incoming.actions, + "owned_output_bits": len(output.data), "owned_output_tape_actions": output.actions, + "validation_pairs": validation_pairs, + "dfs_pushes": pushes, "dfs_pops": pops, "maximum_dfs_entries": max_stack}) + need(incoming.head == output.head == 0 and bytes(incoming.data) == input_bits, + "protected source/owned output return contract") + return output, invoice + + +def query_stream(network, h, layer, address, omit_return=False): + """Read one queried bit by a complete sequential scan, protecting network.""" + n = 1 << h + need(0 <= layer < 2 * h - 1 and 0 <= address < n, "query domain") + need(network.head == 0 and len(network.data) == n * (2 * h - 1), "complete network input") + selected = layer * n + address # bounded scalar multiplication; proof charges it. + before = network.actions + answer = Tape(expanded=network.expanded) + for index in range(len(network.data)): + value = network.read(1) + need(value in (b"0", b"1"), "binary network entry") + if index == selected: + answer.write(value) + if not omit_return: + network.rewind() + answer.rewind() + need(len(answer.data) == 1 and answer.data[0] in (48, 49), "owned query bit exists") + return answer, network.actions - before + answer.actions + + +def unpack(network, h): + """Observer only: compare owned encoded output to the retained source API.""" + n = 1 << h + schedule = list(range(h)) + list(reversed(range(h - 1))) + return [(bit, tuple(int(chr(v)) for v in network.data[layer * n:(layer + 1) * n])) + for layer, bit in enumerate(schedule)] + + +def run_case(permutation, p, source, expanded=False): + n = len(permutation) + h = n.bit_length() - 1 + incoming = b"".join(word(x, h) for x in permutation) + output, invoice = compile_stream(incoming, h, p, expanded) + expected = source.benes(permutation) + need(unpack(output, h) == expected, "byte-exact retained compiler output") + before = bytes(output.data) + queries = steps = 0 + for layer, (bit, table) in enumerate(expected): + for address in range(n): + encoded_value, actions = query_stream(output, h, layer, address) + value = int(bytes(encoded_value.data), 2) # Observer of the owned one-bit output. + need(value == table[address] == table[address ^ (1 << bit)], "exact queried target-independent bit") + need(actions == 3 * len(output.data) + 3, "complete query scan, owned bit and return") + queries += 1 + steps += actions + need(bytes(output.data) == before and output.head == 0, "query protects encoded network") + for address in range(n): + need(source.run_network(unpack(output, h), address) == permutation[address], "permutation endpoint") + invoice.update({"queries": queries, "query_tape_actions": steps, + "owned_output_sha256": hashlib.sha256(before).hexdigest()}) + return invoice + + +def rejected(call, label): + try: + call() + except ValueError: + return label + raise ValueError("negative control accepted: " + label) + + +def finite(source): + cases = [] + for n in (2, 4): + cases.extend(("all_permutations", tuple(p), n.bit_length() - 1) + for p in itertools.permutations(range(n))) + for n, moduli in ((4, (2, 3)), (8, (5, 7)), (16, (11,))): + for modulus in moduli: + offsets = range(modulus) if n <= 8 else (0, 1, 10) + cases.extend(("modular_rotation", source.rotation(n, modulus, c), n.bit_length() - 1) + for c in offsets) + cases.extend(("arbitrary", p, 3) for p in + ((7, 0, 6, 1, 5, 2, 4, 3), (1, 4, 7, 2, 5, 0, 3, 6))) + cases.append(("wider_parameter", (3, 2, 0, 1), 7)) + receipts = [] + digest = hashlib.sha256() + categories = {} + for category, permutation, p in cases: + invoice = run_case(permutation, p, source) + categories[category] = categories.get(category, 0) + 1 + digest.update(json.dumps([list(permutation), invoice], sort_keys=True).encode() + b"\n") + receipts.append(invoice) + # Compare expanded one-cell execution with batched sequential macros. + example = (2, 0, 3, 1) + fast = run_case(example, 2, source) + expanded = run_case(example, 2, source, expanded=True) + need(fast == expanded, "expanded cell execution matches batched macro trace") + return {"cases": len(cases), "categories": categories, + "permutation_endpoints": sum(r["wires"] for r in receipts), + "queried_control_bits": sum(r["queries"] for r in receipts), + "logical_accesses": sum(r["logical_accesses"] for r in receipts), + "records_scanned": sum(r["records_scanned"] for r in receipts), + "arena_and_key_tape_actions": sum(r["arena_and_key_tape_actions"] for r in receipts), + "maximum_arena_cells": max(r["arena_cells"] for r in receipts), + "maximum_dfs_entries": max(r["maximum_dfs_entries"] for r in receipts), + "expanded_one_cell_case": list(example), "receipt_sha256": digest.hexdigest(), + "largest_case": max(receipts, key=lambda row: row["wires"]), + "wider_parameter_case": receipts[-1]} + + +def mutations(source): + failures = [] + failures.append(rejected(lambda: compile_stream(word(0, 2) * 4, 2, 2), "duplicate input permutation")) + failures.append(rejected(lambda: compile_stream(b"001", 2, 2), "incomplete input encoding")) + failures.append(rejected(lambda: compile_stream(b"0110", 2, 1), "h exceeds p")) + failures.append(rejected(lambda: compile_stream(b"00100111", 2, 2, wrong_neighbor=True), + "wrong inverse-permutation matching edge")) + arena = Arena(1, 1) + arena.access((1, P, 0, 0), omit_return=True) + need(arena.tape.head != 0, "missing arena return mutant detected") + failures.append("missing arena head return") + network, _ = compile_stream(b"01", 1, 1) + _, actions = query_stream(network, 1, 0, 0, omit_return=True) + need(network.head != 0 and actions != 3 * len(network.data) + 3, "missing query return tariff detected") + failures.append("missing query return and tariff") + network, _ = compile_stream(b"01", 1, 1) + network.data[1] = 50 # A nonselected entry is not a binary bit. + failures.append(rejected(lambda: query_stream(network, 1, 0, 0), "nonselected nonbinary network entry")) + return failures + + +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" + module = types.ModuleType("_pinned_benes_scan_reference") + module.__file__ = str(ROOT / path) + sys.modules[module.__name__] = module + exec(compile(authenticated[path], module.__file__, "exec"), module.__dict__) + result = {"schema_version": 1, "result": "PASS_UNIFORM_BENES_SCAN_COMPONENT", + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "source_inputs_checked": len(authenticated), "finite": finite(module), + "negative_controls": mutations(module), + "limitations": ["Executed model charges sequential tape cells/heads; bounded scalar lowering is the written proof.", + "Canonical header decoding and pre-admission format checks are written lowerings, not executed microcode.", + "No literal complete finite-state transition table or proof-assistant formalization.", + "Beneš component only; no full CRT arithmetic/control evaluator or production placement.", + "No ordinary interchange, precision/native/outer multiplication 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"], "cases": result["finite"]["cases"], + "logical_accesses": result["finite"]["logical_accesses"]}, sort_keys=True)) + + +if __name__ == "__main__": + main() From 519d811cc48693ad9969d6d7994bef3940167005 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Tue, 20 Oct 2026 05:41:00 -0700 Subject: [PATCH 2/2] Retain exact helper referenced by independent cost review --- research/crt-benes-scan/replay_primary.py | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 research/crt-benes-scan/replay_primary.py diff --git a/research/crt-benes-scan/replay_primary.py b/research/crt-benes-scan/replay_primary.py new file mode 100644 index 0000000000..295df77238 --- /dev/null +++ b/research/crt-benes-scan/replay_primary.py @@ -0,0 +1,18 @@ +"""Review helper: run the primary verifier against an explicit source checkout.""" +import argparse +import importlib.util +from pathlib import Path +import sys + +parser = argparse.ArgumentParser(description=__doc__) +parser.add_argument("package") +parser.add_argument("source_checkout") +args = parser.parse_args() +package = Path(args.package).resolve() +spec = importlib.util.spec_from_file_location("_independent_review_primary", package / "verify.py") +module = importlib.util.module_from_spec(spec) +sys.modules[spec.name] = module +spec.loader.exec_module(module) +module.ROOT = Path(args.source_checkout).resolve() +sys.argv = [str(package / "verify.py")] +module.main()