Audit uniform Beneš compiler with charged sequential arena scans

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"
+}

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"
+  ]
+}

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"
+}

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.