diff --git a/research/crt-mask-repair-bridge/PROOF.md b/research/crt-mask-repair-bridge/PROOF.md new file mode 100644 index 0000000000..e6138f3b6c --- /dev/null +++ b/research/crt-mask-repair-bridge/PROOF.md @@ -0,0 +1,140 @@ +# Scanner-owned CRT mask consumption / disposal contract + +Scope: one repaired switch layer of Cinna Davis's #4100 `CRT.md` §4, one target. The narrow +addition is consumption of the actual #4208/#4201 scanner-owned mask by marker-driven repair, +with disposal/head-return gates. Correctness below instantiates the inherited #2250/#4328 +repair argument under an explicit key premise; it is not a new repair algorithm or endpoint. +It neither executes key arithmetic on tapes nor closes the full caller or its asymptotic cost. + +## Setting + +Address space `A = {0,1}^L`, `L = 12`, `x = (u:2, t:2, y:8)`, MSB first. `S` is the literal +compact macro (ten shears), `T` the ideal controlled switch `y -> y xor (f(y) << j)`, +`good` the #4100 predicate (digits `u,t != 3`, the `K-1 = 5` bits above target `j` lie in +`[8,24)`). Facts used from predecessors (not re-proved here): + +* (F1) `S` and `T` are bijections of `A` preserving `good`, and `S = T` on `good` + (#4100 `check_compact_crt.py`; universal argument #4169 PROOF.md for a source `f` omitting + its targets). +* (F2) `S^-1` is computed at the CURRENT `y` by running the ten shears in reverse with negated + offsets (#4169). Hence `T o S^-1` is computable at one address without a table. +* (F3) The unchanged #4201 scanner outputs `mask[q] = 1` iff `q` is bad, from the stencil + produced by the unchanged #4208 producer, with exact invoices + `T_prod = 33H+25K+38Y-6G-J+12B+335` and `T_scan = 8ML+15M+13L+18`. +* (F4) Extraction, full-key stable two-bucket radix reinsertion and erasure are inherited + from #2250/#4328; #4328 supplies the CRT tariff, not a new result of this package. + +## Prior physical repair and the distinct boundary + +Jose Manuel's #3055 at `9dc841c9a101435fdd15e0f7623bf16b6d0363e9`, +`research/physical-complex-compact/PROOF.md` §§4–6 and `compact_streams.py`, already implements +encoded current-inverse destination keys, physical hole flags, stable two-bucket radix +repair, hole-key equality checks and disposal. His #3608 at +`c6020096322012f7cc41236c3ac15a6b6cd3f8b9`, `research/physical-sparse-xor-batch/PROOF.md` +and `sparse_engine.py`, implements encoded variable-pair control and reuses that repair +with owned-work return. These are physical-repair prior art, not merely host-array sketches. +Their resource arguments use long actual records to absorb polynomial control work; +they do not supply consumption of the CRT #4208/#4201 scanner-owned mask at `R = Θ(p)`. +See [README's exact-head comparison](README.md#exact-head-comparison-and-retained-credit) +for source links. This package claims that mask-consumption/disposal interface only, not +first physical repair, a new algorithm, a new endpoint or a new asymptotic tariff. + +Let `raw` be the stream after the macro: `raw[S(x)] = payload(x)`. Goal: `final[T(x)] = payload(x)`. + +## Contract of `bridge.repair` + +Tapes (fixed roles): `stencil, mask, counter, data, good, bad, b0, b1`. Inputs: `stencil` and +`mask` are the producer/scanner's own output tapes, `data` holds `raw` as `LEFT, (R,v)^M, END`, +`counter, good, bad, b0, b1` are physically blank (`LEFT` then `BLANK`). Key premise +(K): `key_function(addr)` returns `T(S^-1(addr))` as `L` bits for every `addr`. + +Postcondition: `data = final` (same length); `mask, stencil, counter, good, bad, b0, b1` are +physically blank apart from permanent `LEFT`; all heads at `LEFT`; the key function was +called once per marked address and on no other. + +## Proof + +**Counter.** `init_counter` writes `0^L END` (one `0` per stencil atom, so `L` is carried by the +stencil, never by a host integer). `advance` runs to `END` and applies the scanner's own +carry; it returns "wrapped" exactly after `2^L` increments, and the program raises if +"wrapped" disagrees with the mask `END`. So at the k-th loop iteration the counter spells +`k` (MSB first) and the mask cell read is `mask[k]` (mask and address space have equal length). + +**Split.** For `k` with `mask[k]=0` the record of `data[k]` is appended to `good` and no key is +read. For `mask[k]=1` the record and then `key_function(k)` (the address read off the counter +cells) are appended to `bad` as a block `R, key^L`. No other path touches `key_function`. +Hence `good` is the subsequence of `raw` at good addresses, `bad` the blocks at bad addresses +in address order, each carrying `key_k = T(S^-1(k))`. + +**Keys permute the holes.** By (F1), `S^-1` and `T` both preserve bad = complement of good, so +`k -> key_k` is a bijection of the bad set onto itself (also: `raw[k]` is the payload whose +ideal destination is `key_k`, because `payload(x)` sits at `S(x)` and `x = S^-1(k)`). + +**Radix.** One pass moves each block, stable, to `b0` or `b1` by the LAST key bit, rotating that +bit to the front of the key, then concatenates `b0 b1` into `bad`. After pass `i` the blocks are +stably ordered by original bits `b_0..b_{i-1}` (LSB first) and the key is the rotation of the +original by `i` places. This is the textbook LSD argument with the dropped bit re-attached. +After `L` passes the keys have their original orientation and the blocks are ordered by the full +key, with all keys distinct (keys are a permutation of the holes). The stencil is the pass +counter (`L` atoms), not a host integer. + +**Reinsertion.** The `r`-th smallest key is the `r`-th smallest bad address (the keys are +exactly the bad set). Walking addresses in order with the counter, a bad address takes the next +sorted block and the program compares its key bits with the counter bits, raising on any +difference; a good address takes the next `good` record. Thus `final[k] = payload(x)` where +`T(x) = k` for bad `k` (the block whose key is `k`), and for good `k` the record +`raw[k] = payload(S^-1(k))` with `T(S^-1 k) = k` by (F1) (`S = T` on good and `S^-1(k)` good). +Both streams end together or the program raises. So `final = T`-image of the payloads. QED. + +The reinsertion key check is necessary but NOT sufficient for correct keys: any bijection of +the holes passes it (`ideal_of_current`, `inverse_only`, `stale_source`, `guarded_identity` +keys all pass or fail it without the payloads being right). Correctness of the repair therefore +rests on premise (K); the verifier exercises these four wrong keys, counting a mode as detected only where it changes +some hole key (equivalent fixtures are recorded as such). + +**Ownership/erasure.** `erase` reads to `END`, blanks every cell including the allocated `END`, +and rewinds. `repair` ends by erasing `mask` (consumed), `stencil` (consumed), `good`, `bad`, +`counter`, and each pass erases `b0, b1`. Each role is then physically `LEFT, BLANK*`, so the +private roles can be reused by a later producer/scanner/repair invocation; the verifier asserts +blankness before every reuse. `data` is overwritten in place cell by cell (no extra length). +This local postcondition does not imply an uninterrupted all-tape inter-layer data handoff. + +**What a skipped clear costs.** Marker-driven reads stop at `END`, so stale cells beyond a +rewritten marker are not read by the next layer; skipping a clear is therefore a *state/ +ownership* defect that does not change that layer's output, and it is caught by the physical +blank gate, not by the payload comparison. The verifier states this and detects it by the gate. + +## Cost (explicit model) + +One action = one read, write, or one-cell move of the finite-alphabet cell/head model; a record +cell additionally counts `R = 12` bit-widths in the observer bit meter. With `M = 2^L`, `N` holes: + +* producer `T_prod` and scanner `T_scan` exactly as in (F3), unchanged; +* init `O(L)`; split `O(M L + N L)` (counter advance and address read are `O(L)` each) plus + `N` key-call interfaces of `O(L)` actions each; +* sort: `L` passes, each `O(N L)` actions (each block is scanned, its last key bit fetched and + the block rewritten), i.e. `O(N L^2)`; erase of buckets `O(N L)` per pass; +* reinsertion `O(M L + N L)`; final erasure `O(M + N (L+1) + L)`. + +The verifier reports exact observed counts per phase and per invocation. Key ARITHMETIC +(the host `key_function` body: ten shears, a Beneš table lookup and an ideal switch) is not +charged and is not on tapes; only the address-read/key-write interface actions are charged. +CRT.md's `E(p,ell)` and #4377's counting proof remain a conditional allowance, not payment +for the executed host callback. No #4377 tape evaluator is plugged in here. The displayed +local repair accounting does not establish a new `O(V)` tariff for this implementation. + +## Limits + +* Macro `S`, the raw stream and ideal-layout oracles, and the inter-layer payload handoff + are host-built. Within each repaired-layer invocation, producer/scanner and the remaining + repair actions are tape programs, with the host key callback explicitly excluded. +* The geometry is the unary one-target family of #4208 with the fixed `u2,t2,y8`; many-target + ordering and binary/transported geometry are not covered. +* `key_function` is not a tape program (stated above). The AST guardrail is a review aid. +* The existing #4169 ten-layer fixture already supplies the 4096-payload / 29,440-hole + forward/inverse endpoint and current-state inverse keys. Here it is **ten separate repaired-layer + invocations**, not an uninterrupted all-tape caller: host code extracts each output and + populates the next raw data tape, despite reuse of blank private roles. +* These finite invocations exercise the interface; the algebraic statement is the inherited + repair argument above for every `(L, f)` satisfying (F1)-(F3) and (K), not a universal + tape-evaluator, full-construction or multiplication theorem. Outcome remains `partial`. diff --git a/research/crt-mask-repair-bridge/README.md b/research/crt-mask-repair-bridge/README.md new file mode 100644 index 0000000000..4e7b8f91d6 --- /dev/null +++ b/research/crt-mask-repair-bridge/README.md @@ -0,0 +1,157 @@ +# One-target CRT scanner-mask consumption and disposal bridge + +**Claim type: a narrow scanner-owned-mask interface, exercised in ten repaired-layer +invocations of the #4100/#4169 fixture. Partial: unpaid host key arithmetic and host +macro/inter-layer streams remain. No new algorithm, endpoint, tariff, κ or full closure.** + +## Question + +`research/pr4100-crt-repair-tariff` (#4328) requests composition of the hole mask, key evaluator +and repair ownership/erasure contracts. #4208/#4201 produce a mask on tapes; #4169 supplies +current-state reverse keys and the ten-layer caller fixture; #4328 already supplies the CRT +repair algorithm/tariff, but builds its `MASK` from a host `good` list and keys from +`T[inv_S[x]]`. #4377 supplies a counting proof, not a tape evaluator plugged into this bridge. + +## What is joined (and run) + +The replay makes **ten separate repaired-layer invocations** using the existing #4169 fixture +(#4100 `check_compact_crt.py`: five Beneš layers for padded moduli 3 and 5 over all 4096 labeled +payloads, then the five reversed). Within each invocation: + +1. the **unchanged** #4208 `producer.py` builds the stencil from six unary geometry words + `G,H,K,Y,J,B = 2,2,6,8,j,0` (exact `33H+25K+38Y-6G-J+12B+335` invoice asserted); +2. the **unchanged** #4201 `machine.transduce` scans it into the owned BAD mask + (exact `8ML+15M+13L+18` invoice asserted; mask equals the source `good` predicate); +3. `bridge.py` consumes **that mask tape in place** — never a host good list: split by mask, + key evaluated at marked addresses only, `L = 12` stable full-key radix passes over + (payload, key) blocks, mask-driven reinsertion comparing the sorted key to the counter, + physical erasure of mask, stencil, counter, good/bad streams and both buckets, head return; +4. recycled physical tapes must be blank with head at `LEFT` before the next layer + (producer private roles are reused as good/bad/bucket roles). + +Label 780 reaches address 777 after layer 5 and returns to 780 after the inverse five. +Every layer is also checked equal to the pinned table-based `check_compact_crt.layer`. + +The macro/raw stream for each invocation and the payload handoff between invocations are +host-built Python adapters. Blank private-role reuse is checked, but the payload is extracted +and a new data tape is populated for the next invocation. This is **not an uninterrupted +all-tape caller**. The 4096-payload / 29,440-hole fixture and its forward/inverse endpoint +already occur in #4169; the added boundary is consumption of the scanner's actual mask, +marker-driven repair actions, and disposal/head-return gates. + +## Exact-head comparison and retained credit + +- **#2250 / #4328:** retain extraction, full `T(S^-1(q))` keys, stable two-bucket radix + reinsertion and erasure as existing algorithms. #4328 supplies the CRT tariff; this + package does not improve it or claim its asymptotic bound for this implementation. +- **#3055, `9dc841c9a101435fdd15e0f7623bf16b6d0363e9`:** Jose Manuel's + [physical Compact proof §§4–6](https://github.com/CrocSwap/integer-mult-bounds/blob/9dc841c9a101435fdd15e0f7623bf16b6d0363e9/research/physical-complex-compact/PROOF.md) + and [`compact_streams.py`](https://github.com/CrocSwap/integer-mult-bounds/blob/9dc841c9a101435fdd15e0f7623bf16b6d0363e9/research/physical-complex-compact/compact_streams.py) + already implement encoded current-inverse keys, hole flags, physical two-bucket stable + radix repair, destination checks and disposal. Its guard/key arithmetic is encoded; + its fast bound uses superpolynomially long records, unlike CRT's `R = Θ(p)` regime. +- **#3608, `c6020096322012f7cc41236c3ac15a6b6cd3f8b9`:** Jose Manuel's + [sparse XOR proof](https://github.com/CrocSwap/integer-mult-bounds/blob/c6020096322012f7cc41236c3ac15a6b6cd3f8b9/research/physical-sparse-xor-batch/PROOF.md) + and [`sparse_engine.py`](https://github.com/CrocSwap/integer-mult-bounds/blob/c6020096322012f7cc41236c3ac15a6b6cd3f8b9/research/physical-sparse-xor-batch/sparse_engine.py) + lower encoded variable source/target pairs and reuse #3055's physical repair, with + complete owned-work return and a long-record resource argument. Neither cited interface + consumes the #4208/#4201 CRT scanner-owned mask: that consumption/disposal boundary, + not first physical repair or a new endpoint, is the narrow addition here. +- **#4169:** retain both current-state inverse-word keys and the exact ten-layer + 4096-payload / 29,440-hole caller credit, not merely inverse-key attribution. + +## The unpaid point + +`bridge.evaluate_key` pays the tape actions that read the address cells and write the 12 key +bits. The mapping address -> `T(S^-1(q))` is `key_subroutine.ReverseWordKey`: the ten compact +shears run in reverse at the current `y` (kumagi's #4169), then the ideal switch. It is plain +Python integer arithmetic, called once per marked address, with no inverse table, no address loop +and no good-set test; the verifier compares it with #4169's `Word.run(inverse=True)` on every +address of every layer. **It is not a literal tape evaluator and its cost is not charged.** +CRT.md §4's `E(p,ell)` remains a conditional allowance; #4377's counting proof does not +pay for or realize the host callback executed here. Within the repair, the remaining actions +are reads/writes/one-cell moves with finite-control branching; the macro and layer adapters +remain host code. An AST guardrail (review aid only) rejects host arithmetic, indexing, +length primitives and observer reads outside `evaluate_key` in the repair module. + +## Evidence + +`PROOF.md` instantiates the inherited repair argument for every geometry satisfying the +predecessors' facts and the key premise. `verify.py --part caller` replays the 10 layers (also receipts +`RESULT-caller.json`); `--part controls` runs the negative controls (`RESULT-controls.json`): +wrong keys (`ideal_of_current`, `inverse_only`, `stale_source`, `guarded_identity`) fed +through the real program on the actual layer and on a callable-source fixture; a mode whose key +equals the correct key at every hole of a fixture is reported as equivalent there, not as detected, +and each mode must be discriminated on at least one fixture; zeroed mask (zero key calls, wrong records); one hole unmarked; +truncated mask; over-marked good address (output right, one good key evaluation counted); +key evaluation on every good address; skipped sort; skipped clear of each of mask, stencil, +good, bad, counter, buckets; omitted head return; producer geometry mutants through the real +scanner; damaged source bytes rejected before execution. A skipped clear does not change that +layer's payloads (marker-driven reads) and is caught by the physical-blank gate; the README +and PROOF say so rather than claim the payload check catches it. + +Exact per-phase action counts and the 12-bit-record weighted meter are in the receipts. + +The existing author record reports execution in Python 3.12.14 passing the ten repaired-layer +invocations and all semantic controls. Across those invocations: 29,440 marked-key calls, zero good-address +key evaluations, 133,110,830 repair actions and 226,260,150 record-bit-weighted repair +actions. The producer uses 8,422 actions and the scanner 4,548,300. The 2,266,880 key-interface +actions are included in the repair total, not added twice. Key arithmetic is excluded. + +The control receipt contains 24 detected violations and two distinct non-rejection outcomes: +the key-identical stale-source case and the correctly repaired but overcharged extra mark. +The callable parity source makes the stale-source mutant fail the actual hole-key check. + +An independent OpenAI-family verifier reviewed the Anthropic implementation and ran both +isolated optimized replay commands, comparing the existing receipts. The parent then ran +the complete registered package, which reported `PASS_REGISTERED_RESEARCH_PACKAGE` with +`outcome=partial`. Partial refers to the unpaid tape evaluator and host macro/layer handoff, +not to an incomplete execution of this package's two commands. These are retained execution +records, not a new replay of this documentation/attribution change. + +## Not covered + +The macro `S`, raw post-macro stream and inter-layer payload handoff are host-built. +One target per layer, unary one-target geometry only; no many-target ordering, binary or transported geometry; no +`E(p,ell)` tape evaluator; no asymptotic `O(V)` claim here (the key premise and `L = Θ(p)` +calibration are CRT.md's). + +## Live positioning and historical provenance + +At the inspected canonical main `fbc9ea0249746acca4f504d4fda2b84e0e36cf0d`, the selected result +is the conditional #4470 construction, `κ = 0.00302015`, with priority revision 7 retained. +This side contribution changes none of that selection or its transfer obligations. The +package's historical base remains `f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc` in `TASK.json` +and `SOURCES.json`; pinned predecessor bytes and receipts retain their original provenance. + +## Reproduce + +```sh +python3 scripts/research_package.py --package research/crt-mask-repair-bridge --check-only +python3.12 -I -B research/crt-mask-repair-bridge/verify.py --part caller +python3.12 -I -B research/crt-mask-repair-bridge/verify.py --part controls +python3.12 -I -B research/crt-mask-repair-bridge/verify.py --probe # one layer, quick +``` + +Write receipts with `--write` (once). Standard library only. + +## Open next questions + +1. **Replace the key premise by a literal tape program.** *Why:* it is the only unpaid + arithmetic inside the repair. *First step:* the ten reversed shears on the counter role for this geometry, + plugged into `evaluate_key` and metered. *Blocked by:* a literal CRT-data evaluator (#4192 follow-up). +2. **Macro, many targets and transported geometry.** *Why:* the raw stream and layer hand-off + are host-built. *First step:* the literal macro on the same data role. *Blocked by:* no pinned + tape macro or many-target producer. + +## Credit and AI disclosure + +Cinna Davis (#4100/#4088, CRT.md and original caller); Hiroki KUMAZAKI (@kumagi, #4169/#4174, +current-state reverse keys and the exact ten-layer fixture); ToikY (#4195/#4201/#4208, +scanner, producer); Jose Manuel (@jmbarrancoml, PR2250 repair and #3055/#3608 encoded physical +repair); Ryanson Jonathan (@pinterbanget, #4311/#4328/#4329, CRT tariff and handoff); +unpaidmoon (#4377, evaluator counting bound); Douglas Colkitt/OpenAI and the NOTICE lineage. +This package adds the scanner-mask consumption/disposal interface to their contracts. +Prepared for codyw912 with substantial Anthropic Claude implementation and OpenAI +coordination/verification assistance, including this OpenAI-family scope/attribution edit; +no human or formal-kernel review. Apache-2.0. diff --git a/research/crt-mask-repair-bridge/RESULT-caller.json b/research/crt-mask-repair-bridge/RESULT-caller.json new file mode 100644 index 0000000000..3edc61826d --- /dev/null +++ b/research/crt-mask-repair-bridge/RESULT-caller.json @@ -0,0 +1,213 @@ +{ + "actual_caller": { + "forward_payload_sha256": "abeaa4eef9cfc0bcd5d8787f7f8833f7a96265c68b6233c1eacf81fdfa3fa5c7", + "inverse_payload_sha256": "6b0751ba5e64fc9c13ddfb44778fa7d6a1f7d7aa9d6a5e38a1f0a1502c3fb9e3", + "label_780_forward_address": 777, + "label_780_inverse_address": 780, + "layers": [ + { + "direction": "forward", + "holes": 2944, + "key_interface_actions": 226688, + "phases": { + "erase_and_return": 225950, + "init_counter": 106, + "reinsert": 567693, + "sort": 11941445, + "split_and_keys": 575889 + }, + "producer_actions": 843, + "repair_actions": 13311083, + "repair_bit_weighted": 22626015, + "scanner_actions": 454830, + "schedule_index": 0, + "target": 0 + }, + { + "direction": "forward", + "holes": 2944, + "key_interface_actions": 226688, + "phases": { + "erase_and_return": 225950, + "init_counter": 106, + "reinsert": 567693, + "sort": 11941445, + "split_and_keys": 575889 + }, + "producer_actions": 842, + "repair_actions": 13311083, + "repair_bit_weighted": 22626015, + "scanner_actions": 454830, + "schedule_index": 1, + "target": 1 + }, + { + "direction": "forward", + "holes": 2944, + "key_interface_actions": 226688, + "phases": { + "erase_and_return": 225950, + "init_counter": 106, + "reinsert": 567693, + "sort": 11941445, + "split_and_keys": 575889 + }, + "producer_actions": 841, + "repair_actions": 13311083, + "repair_bit_weighted": 22626015, + "scanner_actions": 454830, + "schedule_index": 2, + "target": 2 + }, + { + "direction": "forward", + "holes": 2944, + "key_interface_actions": 226688, + "phases": { + "erase_and_return": 225950, + "init_counter": 106, + "reinsert": 567693, + "sort": 11941445, + "split_and_keys": 575889 + }, + "producer_actions": 842, + "repair_actions": 13311083, + "repair_bit_weighted": 22626015, + "scanner_actions": 454830, + "schedule_index": 3, + "target": 1 + }, + { + "direction": "forward", + "holes": 2944, + "key_interface_actions": 226688, + "phases": { + "erase_and_return": 225950, + "init_counter": 106, + "reinsert": 567693, + "sort": 11941445, + "split_and_keys": 575889 + }, + "producer_actions": 843, + "repair_actions": 13311083, + "repair_bit_weighted": 22626015, + "scanner_actions": 454830, + "schedule_index": 4, + "target": 0 + }, + { + "direction": "inverse", + "holes": 2944, + "key_interface_actions": 226688, + "phases": { + "erase_and_return": 225950, + "init_counter": 106, + "reinsert": 567693, + "sort": 11941445, + "split_and_keys": 575889 + }, + "producer_actions": 843, + "repair_actions": 13311083, + "repair_bit_weighted": 22626015, + "scanner_actions": 454830, + "schedule_index": 4, + "target": 0 + }, + { + "direction": "inverse", + "holes": 2944, + "key_interface_actions": 226688, + "phases": { + "erase_and_return": 225950, + "init_counter": 106, + "reinsert": 567693, + "sort": 11941445, + "split_and_keys": 575889 + }, + "producer_actions": 842, + "repair_actions": 13311083, + "repair_bit_weighted": 22626015, + "scanner_actions": 454830, + "schedule_index": 3, + "target": 1 + }, + { + "direction": "inverse", + "holes": 2944, + "key_interface_actions": 226688, + "phases": { + "erase_and_return": 225950, + "init_counter": 106, + "reinsert": 567693, + "sort": 11941445, + "split_and_keys": 575889 + }, + "producer_actions": 841, + "repair_actions": 13311083, + "repair_bit_weighted": 22626015, + "scanner_actions": 454830, + "schedule_index": 2, + "target": 2 + }, + { + "direction": "inverse", + "holes": 2944, + "key_interface_actions": 226688, + "phases": { + "erase_and_return": 225950, + "init_counter": 106, + "reinsert": 567693, + "sort": 11941445, + "split_and_keys": 575889 + }, + "producer_actions": 842, + "repair_actions": 13311083, + "repair_bit_weighted": 22626015, + "scanner_actions": 454830, + "schedule_index": 1, + "target": 1 + }, + { + "direction": "inverse", + "holes": 2944, + "key_interface_actions": 226688, + "phases": { + "erase_and_return": 225950, + "init_counter": 106, + "reinsert": 567693, + "sort": 11941445, + "split_and_keys": 575889 + }, + "producer_actions": 843, + "repair_actions": 13311083, + "repair_bit_weighted": 22626015, + "scanner_actions": 454830, + "schedule_index": 0, + "target": 0 + } + ], + "pool_size_after": 11, + "tapes_recycled_pool_hits": 9, + "totals": { + "calls": 29440, + "holes": 29440, + "interface": 2266880, + "producer": 8422, + "repair": 133110830, + "repair_bits": 226260150, + "scanner": 4548300 + } + }, + "geometry": { + "address_bits_L": 12, + "addresses": 4096, + "digit_bits_G": 2, + "guard_K": 6, + "t_bits": 2, + "u_bits": 2, + "y_bits": 8 + }, + "key_arithmetic_on_tape": false, + "scope": "One target per layer; macro S and inter-layer raw streams are host-built input adapters; address->key arithmetic is the explicit paid-elsewhere premise; no kappa", + "status": "PASS_CRT_MASK_REPAIR_BRIDGE_ONE_TARGET_KEY_PREMISE:caller" +} diff --git a/research/crt-mask-repair-bridge/RESULT-controls.json b/research/crt-mask-repair-bridge/RESULT-controls.json new file mode 100644 index 0000000000..9f52199310 --- /dev/null +++ b/research/crt-mask-repair-bridge/RESULT-controls.json @@ -0,0 +1,128 @@ +{ + "controls": [ + { + "control": "wrong key ideal_of_current [actual caller layer 2] misplaces 816 records", + "detected": true + }, + { + "control": "wrong key inverse_only [actual caller layer 2] misplaces 368 records", + "detected": true + }, + { + "control": "wrong key stale_source [actual caller layer 2]: key-identical to the correct key at every hole here, so equivalent (not counted as detected)", + "detected": false, + "equivalent": true + }, + { + "control": "wrong key guarded_identity [actual caller layer 2] misplaces 512 records", + "detected": true + }, + { + "control": "wrong key ideal_of_current [callable source parity(y>>1)] misplaces 1728 records", + "detected": true + }, + { + "control": "wrong key inverse_only [callable source parity(y>>1)] misplaces 1472 records", + "detected": true + }, + { + "control": "wrong key stale_source [callable source parity(y>>1)]: rejected by hole-key check", + "detected": true, + "hole_keys_changed": true + }, + { + "control": "wrong key guarded_identity [callable source parity(y>>1)] misplaces 512 records", + "detected": true + }, + { + "control": "missing mask (all good): 512 wrong, 0 keys", + "detected": true + }, + { + "control": "one hole unmarked: rejected (sorted key does not name the current hole)", + "detected": true + }, + { + "control": "truncated mask rejected", + "detected": true + }, + { + "control": "good address over-marked: output still correct, one extra key paid", + "extra_keys": 1, + "final_correct": true, + "good_addresses_evaluated": 1 + }, + { + "control": "good-address key evaluation: 1152 good addresses evaluated", + "detected": true + }, + { + "control": "skipped radix sort: rejected by hole-key check", + "detected": true + }, + { + "control": "skipped clear (keep_mask) leaves nonblank role", + "detected": true + }, + { + "control": "skipped clear (keep_stencil) leaves nonblank role", + "detected": true + }, + { + "control": "skipped clear (keep_good) leaves nonblank role", + "detected": true + }, + { + "control": "skipped clear (keep_bad) leaves nonblank role", + "detected": true + }, + { + "control": "skipped clear (keep_counter) leaves nonblank role", + "detected": true + }, + { + "control": "skipped clear (keep_buckets) leaves nonblank role", + "detected": true + }, + { + "control": "blank-reuse gate rejects uncleared good role", + "detected": true + }, + { + "control": "omitted data head return", + "detected": true + }, + { + "control": "producer mutant wrong_lower_pivot: scanner mask differs from source predicate", + "detected": true + }, + { + "control": "producer mutant wrong_upper_pivot: scanner mask differs from source predicate", + "detected": true + }, + { + "control": "producer mutant include_parity: scanner mask differs from source predicate", + "detected": true + }, + { + "control": "damaged scanner bytes rejected by pin before execution", + "detected": true + } + ], + "geometry": { + "address_bits_L": 12, + "addresses": 4096, + "digit_bits_G": 2, + "guard_K": 6, + "t_bits": 2, + "u_bits": 2, + "y_bits": 8 + }, + "guardrail": { + "functions": 13, + "status": "PASS_AST_SCOPE_GUARDRAIL_NOT_A_FORMAL_MACHINE_CERTIFICATE" + }, + "key_arithmetic_on_tape": false, + "scope": "One target per layer; macro S and inter-layer raw streams are host-built input adapters; address->key arithmetic is the explicit paid-elsewhere premise; no kappa", + "status": "PASS_CRT_MASK_REPAIR_BRIDGE_ONE_TARGET_KEY_PREMISE:controls" +} diff --git a/research/crt-mask-repair-bridge/SOURCES.json b/research/crt-mask-repair-bridge/SOURCES.json new file mode 100644 index 0000000000..079143d6d6 --- /dev/null +++ b/research/crt-mask-repair-bridge/SOURCES.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/crt-arbitrary-source-repair/verify.py", + "usage": "input", + "git_blob": "813eafd24f031b046b2d4aaabdcb0950538980f1", + "sha256": "9a646116e430a242fc16c98d6e35c21290a00ccd9951145290b9a4bf5c007d48" + }, + { + "path": "research/crt-dense-guard-scan/machine.py", + "usage": "input", + "git_blob": "ce763898bd7b4401bbab818c640a0593b65c9a82", + "sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7" + }, + { + "path": "research/crt-unary-stencil-producer/README.md", + "usage": "input", + "git_blob": "1abff6e1019a1b46d88447896325ae966db31351", + "sha256": "747255e3c7b58c9f7ba77ccaa82799628e66851091f35c408db1950a6c91bf47" + }, + { + "path": "research/crt-unary-stencil-producer/producer.py", + "usage": "input", + "git_blob": "dd357a0679c244e5d95b2b782bd70ea9f2507795", + "sha256": "8586d019a0a35390d36b944a2b764ec96682040b1abc42e29d740faf5a830bd0" + }, + { + "path": "research/crt-uniform-evaluator/PROOF.md", + "usage": "input", + "git_blob": "7175c780b63378963c00ea29d76a9d1d7f86bbf0", + "sha256": "a67dce487dfaf0f1748458cf052b85203654d63f84c4e362ae78fe1bae1a3d42" + }, + { + "path": "research/pr4100-crt-repair-tariff/README.md", + "usage": "input", + "git_blob": "1eba9122777570041acbd5ddcfee22ceb0e60703", + "sha256": "5953ed2ae02a609744df2274810d7016cd766f2e43bdf8f79047084ae55a0513" + }, + { + "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" + }, + { + "path": "research/unconditional-batched-crt/check_compact_crt.py", + "usage": "input", + "git_blob": "4804ceae32103840e7ffe77eb07ff50d393829df", + "sha256": "79ab80d0228af31e501272a7a3a32f1a0e8b99df72c3c550e552deccc3a7472b" + } + ] +} diff --git a/research/crt-mask-repair-bridge/TASK.json b/research/crt-mask-repair-bridge/TASK.json new file mode 100644 index 0000000000..d404d6cc13 --- /dev/null +++ b/research/crt-mask-repair-bridge/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "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": "Narrow #4208/#4201 scanner-owned-mask consumption/disposal interface: marker-driven fixed-role repair with blankness/head-return gates, exercised in ten separate repaired-layer invocations of #4169's existing #4100 fixture (4096 labeled payloads, 29440 holes, five forward then five inverse layers). #2250/#4328 supply the repair algorithm/CRT tariff; #4169 supplies current-state inverse keys and this exact fixture. Host key arithmetic is uncharged; macro/raw streams and inter-layer payload handoff are host Python. Not an uninterrupted all-tape caller, first physical repair, new algorithm, new endpoint, new tariff, kappa improvement or full closure.", + "scope_change_reason": "The card asks for one quantified #4100 step at its actual caller. This package isolates the actual scanner-mask ownership/disposal boundary requested by #4328, with one target per invocation. Exact-head comparison: Jose Manuel's #3055 at 9dc841c9a101435fdd15e0f7623bf16b6d0363e9 (physical-complex-compact/PROOF.md sections 4-6 and compact_streams.py) already implements encoded inverse keys, physical stable-radix repair, hole-key checks and disposal; #3608 at c6020096322012f7cc41236c3ac15a6b6cd3f8b9 (physical-sparse-xor-batch/PROOF.md and sparse_engine.py) supplies encoded variable-pair control reusing that repair. Their fast bounds use long actual records, not the CRT scanner-owned-mask boundary at R=Theta(p). Source links and comparison are in README.md and PROOF.md. Historical base/source pins remain unchanged. At inspected live main fbc9ea0249746acca4f504d4fda2b84e0e36cf0d the selected conditional #4470 kappa is 0.00302015, priority revision 7; this package does not change that selection.", + "bottleneck_link": "Side result under retained transfer obligations: consumes the scanner's actual mask in place rather than a host good-list reconstruction, with explicit disposal/head gates. Host address-to-key arithmetic, macro/raw streams and inter-layer handoff remain unpaid/unrealized on tape. #4377 is a counting proof, not a plugged-in evaluator or payment for the executed host callback.", + "budget_minutes": 240, + "stop_rule": "Stop at the scanner-owned-mask consumption/disposal interface and controls, exercised in ten repaired-layer invocations of the existing five-layer forward/inverse fixture; no many-target, binary-geometry, macro/layer-handoff or tape-evaluator expansion.", + "outcome": "partial", + "evidence": "Existing verify.py --part caller / --part controls receipts (RESULT-caller.json, RESULT-controls.json): literal producer/scanner bytes pinned and unchanged, actual mask consumed in place, ten repaired-layer invocations of #4169's 4096-payload/29440-hole fixture, label 780 -> 777 -> 780, local action meters and key/mask/clear/head/good-evaluation controls. Host key arithmetic is excluded from the meter; raw streams and inter-layer handoff are host-built. PROOF.md instantiates the inherited repair argument, not a new algorithm/endpoint or a complete caller theorem. No replay is claimed for this scope/attribution edit.", + "author": "Prepared for codyw912, retaining #2250/#4328 algorithm/tariff, Jose Manuel's #3055/#3608 encoded physical repair, and #4169 inverse-key/exact-fixture credit", + "ai_assistance": "Substantial Anthropic Claude implementation and OpenAI coordination/verification assistance, including an OpenAI-family scope/attribution edit. Existing records report parent-run registered caller/controls passing and a separate OpenAI-family verifier reviewing the Anthropic implementation and running isolated optimized replays against receipts; those are historical records, not new checks of this edit. No independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Can the address->key map T(S^-1(q)) be executed by a literal fixed-role tape program, with every bit step paid, in place of the key subroutine premise?", + "why_it_matters": "Host key arithmetic is uncharged; the E(p,ell) bound of #4377 is a counting proof, not a plugged-in tape evaluator or payment for the executed callback.", + "first_step": "Implement the ten shears of the compact word in reverse (unary/binary adders on the counter role) for this u2,t2,y8 geometry and replace key_function in bridge.evaluate_key, metering it.", + "blocked_by": "A literal evaluator for CRT data and Benes table lookup (#4192 follow-up); not supplied here." + }, + { + "question": "Does the bridge extend to the macro S itself and to many-target ordering/binary-transported geometry without a host-built raw stream?", + "why_it_matters": "The raw post-macro stream and inter-layer payload handoff are host-built. Ten repaired-layer invocations do not establish uninterrupted all-tape caller execution.", + "first_step": "Add the literal macro as the producer of the raw stream on the same data role and reuse the same producer/scanner roles for the next layer's geometry.", + "blocked_by": "No literal macro S tape program or many-target producer is pinned." + } + ] +} diff --git a/research/crt-mask-repair-bridge/VERIFY.json b/research/crt-mask-repair-bridge/VERIFY.json new file mode 100644 index 0000000000..e5686120cf --- /dev/null +++ b/research/crt-mask-repair-bridge/VERIFY.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/crt-arbitrary-source-repair/verify.py", + "research/crt-dense-guard-scan/machine.py", + "research/crt-unary-stencil-producer/README.md", + "research/crt-unary-stencil-producer/producer.py", + "research/crt-uniform-evaluator/PROOF.md", + "research/pr4100-crt-repair-tariff/README.md", + "research/unconditional-batched-crt/CRT.md", + "research/unconditional-batched-crt/NOTICE.md", + "research/unconditional-batched-crt/check_batched_crt.py", + "research/unconditional-batched-crt/check_compact_crt.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--part", + "caller" + ], + "timeout_seconds": 600, + "checks": "Ten actual #4100 Benes layers over all 4096 labeled payloads: unchanged producer->scanner->mask-driven repair; label 780->777->780; blank-reuse of physical tape roles; key addresses equal the scanner holes exactly; reverse-word key equals #4169 on every address." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--part", + "controls" + ], + "timeout_seconds": 600, + "checks": "Wrong keys, missing/damaged/truncated/over-marked masks, good-address key evaluation, skipped sort/clears/head return, producer geometry faults, damaged source pin, AST guardrail." + } + ] +} diff --git a/research/crt-mask-repair-bridge/bridge.py b/research/crt-mask-repair-bridge/bridge.py new file mode 100644 index 0000000000..826d62adbb --- /dev/null +++ b/research/crt-mask-repair-bridge/bridge.py @@ -0,0 +1,278 @@ +"""Joined one-target CRT repair on fixed tape roles (marker-driven, finite control). + +Chain: unary geometry -> producer (#4208) -> stencil -> scanner (#4201) -> owned BAD mask +-> THIS FILE: split by that mask / key subroutine at marked addresses only / L full-key +stable radix passes / mask-driven reinsertion / physical erasure of every consumed or private +role and return of every head. + +The tape program touches tapes only through read/write/move and branches only on read +symbols and fixed finite control. It never reads a host length, head coordinate, cell list, +action counter, address integer, hole list or inverse table. + +THE ONE UNPAID POINT is ``evaluate_key``: it pays tape actions to read the address cells and +write the key cells, but the address -> key arithmetic is the caller's ``key_function`` (the +explicit "one key costs E" premise of CRT.md section 4). It is Python integer arithmetic, NOT +a tape evaluator. + +Cells: markers LEFT/END/BLANK; bits "0"/"1" (counter, mask where 1 = bad, keys); +record cells ("R", payload) of 12 bits. Credit: Cinna Davis (#4100/#4088), kumagi (#4169), +ToikY (#4201, #4208), jmbarrancoml (PR2250 sparse repair), Ryanson Jonathan (#4328), +unpaidmoon (#4377). Apache-2.0. +""" + +LEFT, END, BLANK = "<", ">", "_" + + +def is_record(symbol): + return type(symbol) is tuple and symbol[0] == "R" + + +def is_bit(symbol): + return symbol == "0" or symbol == "1" + + +def rewind(tape): + while tape.read() != LEFT: + tape.move(-1) + + +def erase(tape): + """Blank every data cell and the END marker; keep permanent LEFT; return head.""" + rewind(tape) + tape.move(1) + while True: + symbol = tape.read() + tape.write(BLANK) + if symbol == END: + break + tape.move(1) + rewind(tape) + + +def init_counter(stencil, counter): + """One '0' per stencil atom (the stencil is the length ruler); heads return to LEFT.""" + stencil.move(1) + counter.move(1) + while True: + symbol = stencil.read() + if symbol == END: + counter.write(END) + break + counter.write("0") + stencil.move(1) + counter.move(1) + rewind(stencil) + rewind(counter) + + +def advance(counter, mask, increment): + """Counter head LEFT -> END, then the scanner's binary carry (head returns to LEFT). + The counter wraps exactly when the mask cell under the head is END.""" + counter.move(1) + while counter.read() != END: + counter.move(1) + more = increment(counter, False) + following = mask.read() + if more == (following == END): + raise ValueError("mask length differs from the stencil address space") + + +def evaluate_key(counter, out, key_function, meter): + """Interface actions are paid; ``key_function`` arithmetic is the explicit premise.""" + before = counter.actions + out.actions + counter.move(1) + bits = [] + while True: + symbol = counter.read() + if symbol == END: + break + bits.append(symbol) + counter.move(1) + rewind(counter) + key = key_function("".join(bits)) + for symbol in key: + out.write(symbol) + out.move(1) + meter["calls"] += 1 + meter["interface_actions"] += counter.actions + out.actions - before + + +def split(mask, data, counter, good, bad, b0, key_function, increment, meter, flags): + for tape in (mask, data, good, bad): + tape.move(1) + if "eval_good" in flags: # negative control only: b0 borrowed as key scratch + b0.move(1) + while True: + flag = mask.read() + if flag == END: + break + record = data.read() + if not is_record(record): + raise ValueError("payload stream shorter than mask") + if flag == "0": + good.write(record) + good.move(1) + if "eval_good" in flags: # negative control only + evaluate_key(counter, b0, key_function, meter) + elif flag == "1": + bad.write(record) + bad.move(1) + evaluate_key(counter, bad, key_function, meter) + else: + raise ValueError("mask alphabet") + mask.move(1) + data.move(1) + advance(counter, mask, increment) + if data.read() != END: + raise ValueError("payload stream longer than mask") + good.write(END) + bad.write(END) + for tape in (mask, data, good, bad): + rewind(tape) + if "eval_good" in flags: + b0.write(END) + erase(b0) + + +def copy_until_end(source, destination): + while True: + symbol = source.read() + if symbol == END: + return + destination.write(symbol) + destination.move(1) + source.move(1) + + +def one_pass(bad, b0, b1, flags): + """Stable split by the LAST key bit; that bit is rotated to the front of its key. + Pass i therefore splits on original key bit (LSB+i-1); after L passes the keys are in + their original orientation, ordered by the full key (stable LSD radix).""" + bad.move(1) + b0.move(1) + b1.move(1) + while True: + record = bad.read() + if record == END: + break + if not is_record(record): + raise ValueError("pair block must begin with its payload cell") + bad.move(1) + while is_bit(bad.read()): + bad.move(1) + bad.move(-1) + last = bad.read() + while not is_record(bad.read()): + bad.move(-1) + target = b1 if last == "1" else b0 + target.write(record) + target.move(1) + target.write(last) + target.move(1) + bad.move(1) + held = bad.read() + bad.move(1) + while is_bit(bad.read()): + target.write(held) + target.move(1) + held = bad.read() + bad.move(1) + b0.write(END) + b1.write(END) + for tape in (bad, b0, b1): + rewind(tape) + bad.move(1) + b0.move(1) + b1.move(1) + copy_until_end(b0, bad) + copy_until_end(b1, bad) + bad.write(END) + for tape in (bad, b0, b1): + rewind(tape) + if "keep_buckets" not in flags: + erase(b0) + erase(b1) + + +def sort_passes(stencil, bad, b0, b1, flags): + stencil.move(1) + while stencil.read() != END: + one_pass(bad, b0, b1, flags) + stencil.move(1) + rewind(stencil) + + +def reinsert(mask, counter, data, good, bad, increment): + """The counter is all-zero at LEFT: the split's last increment wrapped it.""" + for tape in (mask, data, good, bad): + tape.move(1) + while True: + flag = mask.read() + if flag == END: + break + if flag == "0": + record = good.read() + if not is_record(record): + raise ValueError("good stream exhausted") + good.move(1) + else: + record = bad.read() + if not is_record(record): + raise ValueError("keyed hole stream exhausted") + bad.move(1) + counter.move(1) + while True: + bit = counter.read() + if bit == END: + break + if bad.read() != bit: + raise ValueError("sorted key does not name the current hole") + bad.move(1) + counter.move(1) + rewind(counter) + data.write(record) + data.move(1) + mask.move(1) + advance(counter, mask, increment) + if good.read() != END or bad.read() != END: + raise ValueError("reinsertion streams not exhausted together") + for tape in (mask, good, bad): + rewind(tape) + + +def finish(tape, keep): + if keep: # negative control: skipped clear + rewind(tape) + else: + erase(tape) + + +def repair(stencil, mask, counter, data, good, bad, b0, b1, + key_function, increment, meter, flags=frozenset(), mark=None): + """Consume the scanner-owned ``mask`` directly. Return heads; erase every private or + consumed role (mask, stencil, good, bad, counter; buckets inside each pass). ``data`` + ends holding the repaired payload stream, head at LEFT. ``mark`` is an observer hook + called between phases by the verifier (never read by the tape program); + ``flags`` select named faulty programs for negative controls only.""" + init_counter(stencil, counter) + if mark is not None: + mark("init_counter") + split(mask, data, counter, good, bad, b0, key_function, increment, meter, flags) + if mark is not None: + mark("split_and_keys") + if "skip_sort" not in flags: + sort_passes(stencil, bad, b0, b1, flags) + if mark is not None: + mark("sort") + reinsert(mask, counter, data, good, bad, increment) + if mark is not None: + mark("reinsert") + finish(mask, "keep_mask" in flags) + finish(stencil, "keep_stencil" in flags) + finish(good, "keep_good" in flags) + finish(bad, "keep_bad" in flags) + finish(counter, "keep_counter" in flags) + if "omit_head_return" not in flags: + rewind(data) + if mark is not None: + mark("erase_and_return") diff --git a/research/crt-mask-repair-bridge/key_subroutine.py b/research/crt-mask-repair-bridge/key_subroutine.py new file mode 100644 index 0000000000..5771ae5562 --- /dev/null +++ b/research/crt-mask-repair-bridge/key_subroutine.py @@ -0,0 +1,85 @@ +"""Direct reverse-word key evaluator: an explicit PREMISE, not a tape program. + +For one repaired Benes layer (compact word u2,t2,y8, one target, guard K=6) this computes +the repair key T(S^-1(q)) at ONE address q by running the ten modular shears of the compact +word in reverse with negated offsets, each source load reading the CURRENT y (kumagi, +PR4169 ``Word.run(..., inverse=True)``), then applying the ideal controlled switch T. +It has no inverse table, no address loop and no good-set test. + +It is plain Python integer arithmetic. It is NOT a literal tape evaluator. The bridge pays +only the tape actions that hand it the address cells and write back the key cells; the +address -> key arithmetic is the "one key costs E(p, ell)" premise of CRT.md section 4 +(counted for general p, ell by PR4377, not realised on tapes here). + +The non-"correct" modes are the wrong-key negative controls named in PR4169/PR4328; the +verifier feeds them through the real repair program. +""" + +MODES = ("correct", "ideal_of_current", "inverse_only", "stale_source", "guarded_identity") + + +def source_function(table): + """Switch-control source f(y). ``table`` is either a 32-entry Benes control table indexed by + (a << 3) | b with a=(y>>3)&3, b=y&7 (the actual caller), or a callable y -> bit that omits + the target bit (negative-control fixtures).""" + if callable(table): + return table + return lambda y: table[(((y >> 3) & 3) << 3) | (y & 7)] + + +class ReverseWordKey: + def __init__(self, target, table, mode="correct"): + if mode not in MODES: + raise ValueError("unknown key mode") + self.target = target + self.source = source_function(table) + self.mode = mode + self.addresses = [] # observer log; the tape program never reads it + + def run(self, state, inverse, frozen=None): + """Ten shears of the compact word (forward) or their reverse negations.""" + u, t, y = state + target = self.target + sign = -1 if inverse else 1 + for step in (reversed(range(10)) if inverse else range(10)): + if step in (4, 9): + bit = self.source(y) if frozen is None else frozen + u = (u + sign * (bit if step == 4 else -bit)) & 3 + continue + shear = step if step < 4 else step - 5 + z = u & 1 + digit = t & 3 + bit = (y >> target) & 1 + if shear == 0: + y = (y + sign * ((2 * z * digit) << target)) & 255 + elif shear == 1: + t = (t + sign * bit) & 3 + elif shear == 2: + y = (y + sign * ((z * (1 - 2 * digit)) << target)) & 255 + else: + t = (t + sign * (-(bit ^ z))) & 3 + return u, t, y + + def ideal(self, state): + u, t, y = state + return u, t, y ^ (self.source(y) << self.target) + + def key_of(self, address_bits): + """MSB-first '0'/'1' string of the 12-bit address -> 12-bit key string.""" + address = 0 + for symbol in address_bits: + address = (address << 1) | (1 if symbol == "1" else 0) + self.addresses.append(address) + state = (address >> 10, (address >> 8) & 3, address & 255) + if self.mode == "correct": + out = self.ideal(self.run(state, True)) + elif self.mode == "ideal_of_current": + out = self.ideal(state) + elif self.mode == "inverse_only": + out = self.run(state, True) + elif self.mode == "stale_source": + out = self.ideal(self.run(state, True, frozen=self.source(state[2]))) + else: # guarded_identity: the good-set identity used as the bad inverse + out = self.ideal(self.ideal(state)) + u, t, y = out + return format((u << 10) | (t << 8) | y, "012b") diff --git a/research/crt-mask-repair-bridge/verify.py b/research/crt-mask-repair-bridge/verify.py new file mode 100755 index 0000000000..f98abb0924 --- /dev/null +++ b/research/crt-mask-repair-bridge/verify.py @@ -0,0 +1,620 @@ +#!/usr/bin/env python3 +"""Joined producer -> scanner -> mask-driven key repair, replayed on the actual #4100 caller. + +Host arrays below are VERIFICATION ORACLES and input/output adapters only: + - the raw post-macro stream (the macro S itself is not executed on tapes), + - the ideal-switch reference layout, + - the bad-address set used to audit which addresses the key subroutine saw. +The tape program (bridge.py, plus the unchanged producer and scanner) never reads them. +The address -> key arithmetic (key_subroutine.py) is an explicit paid-elsewhere premise. +""" +import argparse +import ast +from hashlib import sha256 +import json +from pathlib import Path +import sys +import tempfile +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +N_ADDRESS = 4096 +PAYLOAD_BITS = 12 + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def pin_ok(raw, row): + return (sha256(raw).hexdigest() == row["sha256"] + and __import__("hashlib").sha1(b"blob %d\0" % len(raw) + raw).hexdigest() == row["git_blob"]) + + +def authenticate(): + rows = json.loads((HERE / "SOURCES.json").read_text())["files"] + data = {} + for row in rows: + if row["usage"] != "input": + continue + raw = (ROOT / row["path"]).read_bytes() + need(pin_ok(raw, row), "source SHA256/Git blob mismatch: " + row["path"]) + data[row["path"]] = raw + phrases = {"research/unconditional-batched-crt/CRT.md": + ["T(S^-1(x)), sort those holes by this full key on fixed tapes", + "It does not sort the full input."], + "research/pr4100-crt-repair-tariff/README.md": + ["Compose the hole mask, key evaluator and repair into one fixed-tape", + "program."], + "research/crt-uniform-evaluator/PROOF.md": ["E(p, ell) = 2^{4 ell} (p+2)^{16}"]} + for path, needed in phrases.items(): + text = data[path].decode() + for phrase in needed: + need(" ".join(phrase.split()) in " ".join(text.split()), "source phrase missing: " + phrase) + return data + + +def load(name, path, data, aliases=()): + module = types.ModuleType(name) + module.__file__ = str(ROOT / path) + saved = {a: sys.modules.get(a) for a in aliases} + sys.modules[name] = module + for alias, target in aliases: + sys.modules[alias] = target + try: + exec(compile(data[path], str(ROOT / path), "exec", dont_inherit=True), module.__dict__) + finally: + for alias, _ in aliases: + sys.modules.pop(alias, None) + return module + + +def own(name): + path = HERE / (name + ".py") + module = types.ModuleType("bridge_" + name) + module.__file__ = str(path) + sys.modules["bridge_" + name] = module + exec(compile(path.read_bytes(), str(path), "exec", dont_inherit=True), module.__dict__) + return module + + +class Env: + def __init__(self): + data = authenticate() + self.data = data + P = "research/crt-dense-guard-scan/machine.py" + self.machine = load("pred_machine", P, data) + self.producer = load("pred_producer", "research/crt-unary-stencil-producer/producer.py", data) + self.original = load("pred_original", "research/unconditional-batched-crt/check_batched_crt.py", data) + self.caller = load("pred_caller", "research/unconditional-batched-crt/check_compact_crt.py", data, + aliases=(("check_batched_crt", self.original),)) + self.kumagi = load("pred_4169", "research/crt-arbitrary-source-repair/verify.py", data) + self.bridge = own("bridge") + self.keysub = own("key_subroutine") + machine = self.machine + + class BitTape(machine.Tape): + """Unchanged Tape plus an observer bit meter: payload record 12, other symbol 1.""" + + def __init__(self, cells=None): + super().__init__(cells) + self.bits = 0 + + @staticmethod + def weight(symbol): + return PAYLOAD_BITS if type(symbol) is tuple and symbol[0] == "R" else 1 + + def read(self): + symbol = super().read() + self.bits += self.weight(symbol) + return symbol + + def write(self, symbol): + self.bits += self.weight(symbol) + super().write(symbol) + + def move(self, direction): + self.bits += self.weight(self.cells[self.head]) + super().move(direction) + + self.BitTape = BitTape + self.pool = [] + self.base = {} + # The unchanged scanner bytes call Tape() for their counter and mask roles; route those + # allocations through the verifier's physical-blank pool (observer wiring, not program text). + machine.Tape = self.fresh + + # -- tape pool: recycled tapes must be physically blank with head at LEFT -------------- + def blank(self, tape): + return (tape.head == 0 and tape.cells[0] == self.machine.LEFT + and all(x == self.machine.BLANK for x in tape.cells[1:])) + + def fresh(self, check=True): + if self.pool: + tape = self.pool.pop() + if check: + need(self.blank(tape), "recycled tape not physically blank/head-returned") + else: + tape = self.BitTape() + self.base[id(tape)] = (tape.actions, getattr(tape, "bits", 0)) + return tape + + def since(self, tapes): + a = b = 0 + for t in tapes: + ba, bb = self.base.get(id(t), (0, 0)) + a += t.actions - ba + b += getattr(t, "bits", 0) - bb + return a, b + + +def unary(env, n): + tape = env.BitTape([env.machine.LEFT] + ["1"] * n + [env.machine.END]) + env.base[id(tape)] = (0, 0) + return tape + + +def schedule(env): + original = env.original + networks = [original.benes(original.rotation(8, 5, (2 * a) % 5 if a < 3 else 0)) for a in range(4)] + layers = [] + for index in range(5): + target = networks[0][index][0] + need(all(net[index][0] == target for net in networks), "common schedule") + table = [networks[a][index][1][b] for a in range(4) for b in range(8)] + need(all(table[(((y >> 3) & 3) << 3) | (y & 7)] == table[((((y ^ (1 << target)) >> 3) & 3) << 3) + | ((y ^ (1 << target)) & 7)] + for y in range(256)), "switch control omits its active target") + layers.append((target, table)) + return layers + + +def pack(u, t, y): + return (u << 10) | (t << 8) | y + + +def unpack(x): + return x >> 10, (x >> 8) & 3, x & 255 + + +def oracle_layer(env, values, target, table): + """Host reference only: S-raw stream, ideal switch layout, bad-address set.""" + original = env.original + fn = env.keysub.source_function(table) + raw = [None] * N_ADDRESS + ideal = [None] * N_ADDRESS + for x in range(N_ADDRESS): + u, t, y = unpack(x) + + out = pack(*original.compact(u, t, y, lambda yy: (fn(yy),), positions=(target,), ybits=8)) + need(raw[out] is None, "raw injection") + raw[out] = values[x] + dest = pack(u, t, y ^ (fn(y) << target)) + need(ideal[dest] is None, "ideal injection") + ideal[dest] = values[x] + bad = {q for q in range(N_ADDRESS) + if not original.good(*unpack(q), bits=2, positions=(target,), guard=6)} + return raw, ideal, bad + + +def run_layer(env, values, target, table, mode="correct", flags=frozenset(), stencil_mutant=None, + mask_hook=None, roles=None): + machine, producer, bridge, keysub = env.machine, env.producer, env.bridge, env.keysub + raw, ideal, bad_set = oracle_layer(env, values, target, table) + inputs = [unary(env, n) for n in (2, 2, 6, 8, target, 0)] # G,H,K,Y,J,B + work, stencil = producer.produce(*inputs, env.fresh, **(stencil_mutant or {})) + producer_tapes = inputs + list(work) + [stencil] + prod_actions, prod_bits = env.since(producer_tapes) + need(stencil_mutant is not None or prod_actions == 33 * 2 + 25 * 6 + 38 * 8 - 6 * 2 - target + 335, + "unchanged producer exact invoice") + need(all(env.blank(t) for t in work), "producer private work blank") + stencil_before = stencil.actions + counter, mask = machine.transduce(stencil) + scan_actions = (stencil.actions - stencil_before) + env.since([counter, mask])[0] + need(stencil_mutant is not None or scan_actions == 8 * N_ADDRESS * 12 + 15 * N_ADDRESS + 13 * 12 + 18, + "unchanged scanner exact invoice") + need(env.blank(counter) and mask.head == 0 and stencil.head == 0, "scanner returned/blanked") + mask_cells = list(mask.cells) + end = mask_cells.index(machine.END) # recycled tapes may carry stale blank cells past END + need(all(x == machine.BLANK for x in mask_cells[end + 1:]), "no stale data past the mask END") + scanned = mask_cells[1:end] + if stencil_mutant is not None: + if len(scanned) != N_ADDRESS or {q for q, b in enumerate(scanned) if b == "1"} != bad_set: + raise ValueError("mutated stencil mask differs from the source good predicate") + need(len(scanned) == N_ADDRESS, "one mask bit per address") + need({q for q, b in enumerate(scanned) if b == "1"} == bad_set, "scanner mask equals source good predicate") + if mask_hook is not None: + mask = mask_hook(mask, raw, ideal, bad_set) + if roles is None: + roles = (work[0], work[1], work[2], work[3]) # good, bad, b0, b1 recycled from producer + good, bad, b0, b1 = roles + data = env.BitTape([machine.LEFT] + [("R", v) for v in raw] + [machine.END]) + env.base[id(data)] = (0, 0) + key = keysub.ReverseWordKey(target, table, mode) + meter = {"calls": 0, "interface_actions": 0} + repair_tapes = [data, stencil, mask, counter, good, bad, b0, b1] + base = {id(t): (t.actions, getattr(t, "bits", 0)) for t in repair_tapes} + phases = [] + + def mark(name): + total = sum(t.actions - base[id(t)][0] for t in repair_tapes) + phases.append((name, total)) + + bridge.repair(stencil, mask, counter, data, good, bad, b0, b1, key.key_of, + machine.increment_and_return, meter, flags, mark) + repair_actions = sum(t.actions - base[id(t)][0] for t in repair_tapes) + repair_bits = sum((t.bits - base[id(t)][1]) if hasattr(t, "bits") else (t.actions - base[id(t)][0]) + for t in repair_tapes) # scanner-created roles carry only 1-bit symbols + phase_cost, last = {}, 0 + for name, total in phases: + phase_cost[name] = total - last + last = total + final = [c[1] for c in data.cells[1:-1]] + ownership = { + "protected_payload_stream_kept_length": len(data.cells) == N_ADDRESS + 2, + "all_roles_blank": all(env.blank(t) for t in (stencil, counter, good, bad, b0, b1)) and env.blank(mask), + "all_heads_returned": all(t.head == 0 for t in repair_tapes), + "good_addresses_evaluated": len(set(key.addresses) - bad_set), + "hole_addresses_missed": len(bad_set - set(key.addresses)), + "key_calls": meter["calls"], + "distinct_key_addresses": len(set(key.addresses)), + } + return dict(final=final, ideal=ideal, raw=raw, bad=len(bad_set), repair_actions=repair_actions, + repair_bits=repair_bits, phases=phase_cost, meter=meter, producer_actions=prod_actions, + scanner_actions=scan_actions, ownership=ownership, tapes=repair_tapes + list(work), + mask_cells_at_scanner_output=mask_cells, data=data, stencil=stencil, counter=counter, + mask=mask, roles=(good, bad, b0, b1), key=key, + producer_tapes=producer_tapes) + + +def recycle(env, result): + seen = set() + for t in result["tapes"] + result["producer_tapes"] + [result["mask"], result["counter"], result["stencil"]]: + if id(t) in seen or t is result["data"] or t.cells[0] != env.machine.LEFT: + continue + seen.add(id(t)) + if env.blank(t) and hasattr(t, "bits"): + env.pool.append(t) + + +def digest(values): + return sha256(b"".join(v.to_bytes(4, "little") for v in values)).hexdigest() + + +def actual_caller(env): + layers = schedule(env) + values = list(range(N_ADDRESS)) + rows, checked = [], [] + forward_hash = None + total = dict(producer=0, scanner=0, repair=0, repair_bits=0, calls=0, interface=0, holes=0) + sequence = [(i, layers[i], "forward") for i in range(5)] + [(i, layers[i], "inverse") for i in reversed(range(5))] + reused_tapes = 0 + for position, (index, (target, table), direction) in enumerate(sequence): + pool_before = len(env.pool) + result = run_layer(env, values, target, table) + reused_tapes += pool_before > 0 + need(result["final"] == result["ideal"], "repaired layer equals ideal switch layer") + own = result["ownership"] + need(own["all_roles_blank"] and own["all_heads_returned"], "ownership/return") + need(own["good_addresses_evaluated"] == 0 and own["hole_addresses_missed"] == 0 + and own["key_calls"] == result["bad"] == own["distinct_key_addresses"], + "keys evaluated exactly at the marked holes") + # Compare the key subroutine with the pinned table-based caller and #4169 Word on EVERY address. + word = env.kumagi.Word(2, 2, 8, (target,), 6) + source = lambda y, table=table: (table[(((y >> 3) & 3) << 3) | (y & 7)],) + for q in range(N_ADDRESS): + ref = word.pack(word.ideal(word.run(word.unpack(q), source, inverse=True), source)) + need(int(result["key"].__class__(target, table).key_of(format(q, "012b")), 2) == ref, + "reverse-word key equals #4169 T(S^-1(q))") + source_fn = lambda y, table=table: (table[(((y >> 3) & 3) << 3) | (y & 7)],) + table_final, table_count = env.caller.layer(values, target, source_fn) + need(table_final == result["final"] and table_count == result["bad"], + "agrees with the pinned table-based #4100 caller layer") + values = result["final"] + if position == 4: + forward_hash = digest(values) + need(values.index(780) == 777, "label 780 reaches address 777") + expected = [None] * N_ADDRESS + for x in range(N_ADDRESS): + u, t, y = unpack(x) + a, b = (y >> 3) & 3, y & 7 + nb = (b + 2 * a) % 5 if a < 3 and b < 5 else b + expected[pack(u, t, (y & ~7) | nb)] = x + need(values == expected, "five-layer endpoint equals padded CRT rotation") + for key_, field in (("producer", "producer_actions"), ("scanner", "scanner_actions"), + ("repair", "repair_actions"), ("repair_bits", "repair_bits")): + total[key_] += result[field] + total["calls"] += result["meter"]["calls"] + total["interface"] += result["meter"]["interface_actions"] + total["holes"] += result["bad"] + rows.append(dict(direction=direction, schedule_index=index, target=target, holes=result["bad"], + producer_actions=result["producer_actions"], scanner_actions=result["scanner_actions"], + repair_actions=result["repair_actions"], repair_bit_weighted=result["repair_bits"], + key_interface_actions=result["meter"]["interface_actions"], phases=result["phases"])) + recycle(env, result) + need(values == list(range(N_ADDRESS)), "inverse five layers restore all 4096 payloads") + need(values[780] == 780, "label 780 returns to address 780") + need(forward_hash is not None, "forward hash") + return dict(layers=rows, forward_payload_sha256=forward_hash, inverse_payload_sha256=digest(values), + label_780_forward_address=777, label_780_inverse_address=780, + totals=total, tapes_recycled_pool_hits=reused_tapes, + pool_size_after=len(env.pool)) + + +def expect_detected(label, check, rows): + need(check, "control not detected: " + label) + rows.append(dict(control=label, detected=True)) + + +def run_outcome(env, values, target, table, **kwargs): + """Run one layer and classify; exception capture is separate from expect_detected.""" + try: + result = run_layer(env, values, target, table, **kwargs) + except ValueError as exc: + env.pool.clear() + return dict(kind="rejected", message=str(exc)) + wrong = sum(a != b for a, b in zip(result["final"], result["ideal"])) + recycle(env, result) + return dict(kind="misplaced" if wrong else "equivalent", wrong=wrong) + + +def keys_differ(env, target, table, mode, bad_set): + """Observer: does ``mode`` change the key at some hole relative to the correct reverse-word key?""" + right = env.keysub.ReverseWordKey(target, table, "correct") + wrong = env.keysub.ReverseWordKey(target, table, mode) + return any(right.key_of(format(q, "012b")) != wrong.key_of(format(q, "012b")) for q in sorted(bad_set)) + + +def discriminating_fixture(env): + """First callable source omitting target bit 0 for which the stale-source key differs at a hole. + Deterministic candidate list; failing to find one is a verifier failure.""" + candidates = [("parity(y>>1)", lambda y: (y >> 1).bit_count() & 1), + ("(y>>1)&(y>>4)", lambda y: ((y >> 1) & (y >> 4)) & 1), + ("(y>>2)^(y>>5)&(y>>6)", lambda y: ((y >> 2) ^ ((y >> 5) & (y >> 6))) & 1)] + for name, source in candidates: + need(all(source(y) == source(y ^ 1) for y in range(256)), "candidate omits target bit 0") + bad_set = oracle_layer(env, list(range(N_ADDRESS)), 0, source)[2] + if keys_differ(env, 0, source, "stale_source", bad_set): + return name, source + raise ValueError("no discriminating stale-source fixture found") + + +def controls(env): + rows = [] + layers = schedule(env) + target, table = layers[2] # middle Benes layer, target bit 2 + values = list(range(N_ADDRESS)) + base = run_layer(env, values, target, table) + ideal = base["ideal"] + need(any(a != b for a, b in zip(base["raw"], ideal)), "control layer must have records the repair moves") + need(base["final"] == ideal, "control baseline correct") + holes = base["bad"] + recycle(env, base) + # Wrong keys, fed through the real repair program. A mode is only a control where it actually + # changes some hole key; at the actual layer a mode that never changes a key is recorded as an + # equivalent (and its output is checked correct) instead of being counted as detected. + discriminating = discriminating_fixture(env) + fixtures = [("actual caller layer 2", target, table), ("callable source " + discriminating[0], + 0, discriminating[1])] + detected_somewhere = {} + for name, f_target, f_table in fixtures: + bad_set = oracle_layer(env, values, f_target, f_table)[2] + for mode in env.keysub.MODES[1:]: + differs = keys_differ(env, f_target, f_table, mode, bad_set) + outcome = run_outcome(env, values, f_target, f_table, mode=mode) + if outcome["kind"] == "rejected": + need(differs, "key-identical mode cannot be rejected: " + mode) + need("sorted key" in outcome["message"] or "keyed hole" in outcome["message"], + "wrong key rejected for an unexpected reason: " + outcome["message"]) + rows.append(dict(control="wrong key " + mode + " [" + name + "]: rejected by hole-key check", + detected=True, hole_keys_changed=True)) + detected_somewhere[mode] = True + elif differs: + expect_detected("wrong key " + mode + " [" + name + "] misplaces %d records" % outcome["wrong"], + outcome["wrong"] > 0, rows) + detected_somewhere[mode] = True + else: + need(outcome["wrong"] == 0, "key-identical mode changed the output: " + mode) + rows.append(dict(control="wrong key " + mode + " [" + name + "]: key-identical to the correct " + "key at every hole here, so equivalent (not counted as detected)", + detected=False, equivalent=True)) + need(all(m in detected_somewhere for m in env.keysub.MODES[1:]), + "every wrong-key mode must be discriminated on at least one fixture") + # Missing / damaged masks consumed directly. + def zero_mask(mask, raw, ideal, bad_set): + for i in range(1, mask.cells.index(env.machine.END)): + mask.cells[i] = "0" + return mask + + result = run_layer(env, values, target, table, mask_hook=zero_mask) + wrong = sum(a != b for a, b in zip(result["final"], ideal)) + expect_detected("missing mask (all good): %d wrong, 0 keys" % wrong, + wrong > 0 and result["meter"]["calls"] == 0, rows) + recycle(env, result) + + def drop_hole(mask, raw, ideal, bad_set): + q = min(q for q in bad_set if raw[q] != ideal[q]) # a hole whose record must move + mask.cells[1 + q] = "0" + return mask + + outcome = run_outcome(env, values, target, table, mask_hook=drop_hole) + if outcome["kind"] == "rejected": + need("stream" in outcome["message"] or "sorted key" in outcome["message"], + "unmarked hole rejected for an unexpected reason: " + outcome["message"]) + rows.append(dict(control="one hole unmarked: rejected (" + outcome["message"] + ")", detected=True)) + else: + expect_detected("one hole unmarked: %d wrong" % outcome["wrong"], outcome["wrong"] > 0, rows) + + def truncate_mask(mask, raw, ideal, bad_set): + del mask.cells[mask.cells.index(env.machine.END) - 1] + return mask + + try: + run_layer(env, values, target, table, mask_hook=truncate_mask) + need(False, "truncated mask accepted") + except ValueError as exc: + need("mask length" in str(exc) or "stream" in str(exc), "truncated mask failure: " + str(exc)) + rows.append(dict(control="truncated mask rejected", detected=True)) + env.pool.clear() + + def over_mark(mask, raw, ideal, bad_set): + q = min(q for q in range(N_ADDRESS) if q not in bad_set) + mask.cells[1 + q] = "1" + return mask + + result = run_layer(env, values, target, table, mask_hook=over_mark) + over = dict(control="good address over-marked: output still correct, one extra key paid", + final_correct=result["final"] == ideal, extra_keys=result["meter"]["calls"] - holes, + good_addresses_evaluated=result["ownership"]["good_addresses_evaluated"]) + need(over["final_correct"] and over["extra_keys"] == 1 and over["good_addresses_evaluated"] == 1, + "over-marking is conservative but charged") + rows.append(over) + recycle(env, result) + # Key evaluation on good addresses. + result = run_layer(env, values, target, table, flags=frozenset({"eval_good"})) + expect_detected("good-address key evaluation: %d good addresses evaluated" % + result["ownership"]["good_addresses_evaluated"], + result["ownership"]["good_addresses_evaluated"] == N_ADDRESS - holes + and result["meter"]["calls"] > holes, rows) + recycle(env, result) + # Sort skipped. + outcome = run_outcome(env, values, target, table, flags=frozenset({"skip_sort"})) + if outcome["kind"] == "rejected": + need("sorted key" in outcome["message"], "skipped sort rejected for an unexpected reason: " + + outcome["message"]) + rows.append(dict(control="skipped radix sort: rejected by hole-key check", detected=True)) + else: + expect_detected("skipped radix sort: %d wrong" % outcome["wrong"], outcome["wrong"] > 0, rows) + env.pool.clear() + # Skipped clears and head return. + for flag in ("keep_mask", "keep_stencil", "keep_good", "keep_bad", "keep_counter", "keep_buckets"): + result = run_layer(env, values, target, table, flags=frozenset({flag})) + need(result["final"] == ideal, "skipped clear does not change this layer's output") + good, bad, b0, b1 = result["roles"] + left = {"keep_mask": result["mask"], "keep_stencil": result["stencil"], "keep_good": good, + "keep_bad": bad, "keep_counter": result["counter"], "keep_buckets": b1}[flag] + expect_detected("skipped clear (%s) leaves nonblank role" % flag, not env.blank(left), rows) + env.pool.clear() + # A skipped clear is a physical-state/ownership defect: the recycled-role blank gate rejects + # it. (Marker-driven reads would not otherwise notice stale cells beyond a rewritten END.) + result = run_layer(env, values, target, table, flags=frozenset({"keep_good"})) + dirty = result["roles"][0] + need(not env.blank(dirty), "dirty role") + env.pool.append(dirty) + rejected = False + try: + env.fresh(check=True) + except ValueError as exc: + rejected = "not physically blank" in str(exc) + need(rejected, "blank-reuse gate must reject an uncleared role") + rows.append(dict(control="blank-reuse gate rejects uncleared good role", detected=True)) + env.pool.clear() + result = run_layer(env, values, target, table, flags=frozenset({"omit_head_return"})) + expect_detected("omitted data head return", result["data"].head != 0, rows) + env.pool.clear() + # Producer geometry faults reach the actual scanner mask and then the repair. + for name in ("wrong_lower_pivot", "wrong_upper_pivot", "include_parity"): + try: + run_layer(env, values, target, table, stencil_mutant={name: True}) + need(False, "mutant mask matched source predicate") + except ValueError as exc: + need("mutated stencil mask" in str(exc), "producer mutant failure: " + str(exc)) + rows.append(dict(control="producer mutant " + name + ": scanner mask differs from source predicate", + detected=True)) + env.pool.clear() + # Damaged source bytes reject before execution. + with tempfile.TemporaryDirectory() as directory: + row = next(r for r in json.loads((HERE / "SOURCES.json").read_text())["files"] + if r["path"].endswith("crt-dense-guard-scan/machine.py")) + damaged = Path(directory) / "machine.py" + original = (ROOT / row["path"]).read_bytes() + need(pin_ok(original, row), "undamaged source passes its pin") + damaged.write_bytes(original + b"\nraise RuntimeError('UNAUTHENTICATED')\n") + need(not pin_ok(damaged.read_bytes(), row), "damaged source bytes must fail the pin before exec") + rows.append(dict(control="damaged scanner bytes rejected by pin before execution", detected=True)) + return rows + + +def guardrail(): + """Review aid, not a formal machine certificate: outside evaluate_key the tape program has + no host arithmetic/indexing/length primitives and no observer-field reads.""" + path = HERE / "bridge.py" + tree = ast.parse(path.read_text()) + forbidden = {"len", "range", "enumerate", "int", "str", "format", "sum", "min", "max", "pow", + "sorted", "list", "dict", "set", "tuple", "zip", "map", "abs", "bytes"} + observers = ("head", "cells", "reads", "writes", "moves", "actions", "bits") + checked = 0 + for fn in (n for n in tree.body if isinstance(n, ast.FunctionDef)): + if fn.name == "evaluate_key": + continue + for node in ast.walk(fn): + if isinstance(node, ast.Call) and isinstance(node.func, ast.Name): + need(node.func.id not in forbidden, "host primitive outside key interface: " + node.func.id) + if isinstance(node, ast.Attribute): + need(node.attr not in observers, "observer read outside key interface: " + node.attr) + if isinstance(node, ast.BinOp): + need(False, "host arithmetic outside key interface in " + fn.name) + if isinstance(node, ast.Subscript): + need(fn.name == "is_record", "indexing outside record-tag test in " + fn.name) + checked += 1 + return dict(status="PASS_AST_SCOPE_GUARDRAIL_NOT_A_FORMAL_MACHINE_CERTIFICATE", functions=checked) + + +def probe(): + """One forward layer: producer -> scanner -> repair, no 10-layer caller, no controls.""" + import time + start = time.time() + env = Env() + target, table = schedule(env)[0] + result = run_layer(env, list(range(N_ADDRESS)), target, table) + need(result["final"] == result["ideal"], "probe layer equals ideal switch layer") + own = result["ownership"] + need(own["all_roles_blank"] and own["all_heads_returned"] and own["good_addresses_evaluated"] == 0, + "probe ownership") + print(json.dumps(dict(target=target, holes=result["bad"], producer_actions=result["producer_actions"], + scanner_actions=result["scanner_actions"], repair_actions=result["repair_actions"], + repair_bits=result["repair_bits"], phases=result["phases"], meter=result["meter"], + ownership=own, seconds=round(time.time() - start, 1)), indent=2, sort_keys=True)) + return "PROBE_OK" + + +def run(part): + env = Env() + out = dict(status="PASS_CRT_MASK_REPAIR_BRIDGE_ONE_TARGET_KEY_PREMISE:" + part, + geometry=dict(u_bits=2, t_bits=2, y_bits=8, guard_K=6, digit_bits_G=2, address_bits_L=12, + addresses=N_ADDRESS), + key_arithmetic_on_tape=False, + scope="One target per layer; macro S and inter-layer raw streams are host-built input " + "adapters; address->key arithmetic is the explicit paid-elsewhere premise; no kappa") + if part == "caller": + out["actual_caller"] = actual_caller(env) + else: + out["controls"] = controls(env) + out["guardrail"] = guardrail() + return out + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write", action="store_true") + parser.add_argument("--part", choices=("caller", "controls")) + parser.add_argument("--probe", action="store_true") + args = parser.parse_args() + if args.probe: + print(probe()) + return + need(args.part is not None, "choose --part caller|controls (or --probe)") + result = run(args.part) + text = json.dumps(result, indent=2, sort_keys=True) + "\n" + receipt = HERE / ("RESULT-" + args.part + ".json") + if args.write: + receipt.write_text(text) + elif receipt.exists(): + need(json.loads(text) == json.loads(receipt.read_text()), "stored receipt differs from replay") + print(result["status"]) + + +if __name__ == "__main__": + main()