From ea2b6fa4d6479813c36ca0c0396c8d06437fb486 Mon Sep 17 00:00:00 2001 From: Hiroki KUMAZAKI Date: Fri, 23 Oct 2026 14:37:10 +0900 Subject: [PATCH] Prove and join paid two-target CRT stencil production --- research/crt-two-target-stencil/PROOF.md | 230 +++++++++++++ research/crt-two-target-stencil/README.md | 143 ++++++++ research/crt-two-target-stencil/RESULT.json | 146 ++++++++ research/crt-two-target-stencil/SOURCES.json | 96 ++++++ research/crt-two-target-stencil/TASK.json | 115 +++++++ research/crt-two-target-stencil/VERIFY.json | 42 +++ research/crt-two-target-stencil/producer.py | 111 ++++++ research/crt-two-target-stencil/verify.py | 339 +++++++++++++++++++ 8 files changed, 1222 insertions(+) create mode 100644 research/crt-two-target-stencil/PROOF.md create mode 100644 research/crt-two-target-stencil/README.md create mode 100644 research/crt-two-target-stencil/RESULT.json create mode 100644 research/crt-two-target-stencil/SOURCES.json create mode 100644 research/crt-two-target-stencil/TASK.json create mode 100644 research/crt-two-target-stencil/VERIFY.json create mode 100644 research/crt-two-target-stencil/producer.py create mode 100644 research/crt-two-target-stencil/verify.py diff --git a/research/crt-two-target-stencil/PROOF.md b/research/crt-two-target-stencil/PROOF.md new file mode 100644 index 0000000000..3fef7bd143 --- /dev/null +++ b/research/crt-two-target-stencil/PROOF.md @@ -0,0 +1,230 @@ +# Two-target unary stencil, dense mask, and exceptional repair + +This closes the two-target producer/consumer handoff of unpaidmoon's +[PR4644](../crt-joined-hole-repair/README.md). It specializes the existing +arbitrary-source algebra of Hiroki KUMAZAKI's +[PR4169](../crt-arbitrary-source-repair/PROOF.md) and uses ToikY's +[PR4208 producer helpers](../crt-unary-stencil-producer/PROOF.md), +[PR4201 scanner](../crt-dense-guard-scan/PROOF.md), and Ryanson Jonathan's +[PR4328 repair schedule](../pr4100-crt-repair-tariff/README.md). +The new result is a paid unary producer for two ordered disjoint windows, +joined to those interfaces. It is not a new generic repair theorem or a +complete bit-step implementation of a CRT switch. + +## 1. Domain and mathematical interfaces + +Let the seven unary input values satisfy + +```text +G >= 1, H >= 2G, K >= G+4, J0 >= 0, +J1 >= J0+K, Y >= J1+K, B >= 0. +``` + +Here `B` is the back-field width; write `b=2^G` for the compact radix. +Set `L=2H+Y+B`, `M=2^L`. A complete address, in MSB-first field order, is +`(u,t,y,back)` of widths `(H,H,Y,B)`. All field values are arbitrary, +including inactive high bits of `u,t` and the complete back field. Define, +for `i=0,1`, + +```text +u_i = floor(u/b^i) mod b, t_i = floor(t/b^i) mod b, +g_i = floor(y/2^(Ji+1)) mod 2^(K-1), +Q_i = (u_i < b-1) and (t_i < b-1) + and (2b <= g_i < 2^(K-1)-2b). +``` + +The good set is `Q=Q_0 intersect Q_1`. Its complement is +`E=(not Q_0) union (not Q_1)`: failure at either target marks a hole. +The intersection of the two failure sets is insufficient. + +For the repair statement let `f_0,f_1` be Boolean functions of the complete +`y` field, independent of `u,t,back`, that omit **both** target bits: + +```text +f_i(y xor 2^Jj) = f_i(y), for every y and i,j in {0,1}. +``` + +Let `S` be the pinned compact macro with digit `i` assigned to target `Ji`, +and let `T` leave `u,t,back` fixed and replace `y` by +`y xor (f_0(y)2^J0 + f_1(y)2^J1)`. The guard scan itself needs no source +functions. The independence premise is needed when joining it to `S,T`; +omission of each function's own target alone does not suffice (#4169 ยง7). + +## 2. Paid admission and stencil identity + +Each protected input is `LEFT, 1^n, END`, followed by an initially blank +tail, with its head at the permanent `LEFT`. The inherited validator pays +for checking that word and its immediate blank successor. It does not +decide the contents of an arbitrary infinite tail. The producer allocates +eleven fixed private unary roles and one owned stencil role, all initially +blank apart from permanent `LEFT` infrastructure. Its derived values are + +```text +HG=H-G, HGG=H-2G, KG=K-G, THREE=3, A=K-G-3, +TAIL=G+1, J0P=J0+1, J10=J1-J0, GAP=J1-J0-K, +YJ1=Y-J1, TOP=Y-J1-K. +``` + +These values are obtained by the inherited protected unary subtraction, +plus-one and constant-three scans. Positivity tests on `G,A`, together +with the subtraction underflow checks, enforce exactly the displayed +domain; all input values are nonnegative by unary representation. No host +geometry comparison admits an input. A failed subtraction writes no +partial output, so all allocated private words remain END-terminated for +rejection cleanup. On a grammar or arithmetic rejection, the private words +and empty stencil are erased and all heads return to `LEFT`, under the +representation contract above. + +Write `s^n` for `n` skip atoms, `d^G` for one separately delimited digit +interval, and `g^(K-1)` for one separately delimited guard interval. The +normal successful output is exactly + +```text +s^(H-2G) d^G d^G s^(H-2G) d^G d^G +s^(Y-J1-K) g^(K-1) s^1 s^(J1-J0-K) g^(K-1) s^(J0+1) s^B. +``` + +The two digit intervals in each field are, in scan order, digit 1 and +digit 0. They retain separate begin/end flags even when adjacent or when +`G=1`. The upper guard belongs to target `J1`; its following single skip +omits that target's parity bit. The lower guard belongs to target `J0`; +the following `J0+1` skips omit its parity and all lower bits. Thus a zero +gap is legal, while overlapping or reversed windows are rejected. + +Each guard consists of `A` leading atoms, one pivot and `TAIL` trailing +atoms. Since `A>=1`, its two threshold strings are exactly + +```text +low = 0^A 1 0^(G+1) = 2^(G+1), +high = 1^A 1 0^(G+1) = 2^(K-1)-2^(G+1). +``` + +Begin is set only on the first leading atom and end only on the last +trailing atom. Every other emitted cell is a canonical skip or digit +atom. The total length is `2H+Y+B`. The four digit intervals and two guard +intervals therefore test exactly the six conjuncts defining `Q`. + +This proves atom identity for every admitted geometry, including inactive +high digits, arbitrary gaps, tight guards and zero back width. The fixed +alphabet and fixed tape inventory do not depend on any input value. All +producer loops branch on tape symbols; coordinates and integer lengths in +this proof belong to the observer, not the executable producer. + +## 3. Exact producer and scanner action invoices + +One action is one `Tape.read`, `Tape.write` or one-cell `Tape.move`. +The inherited successful helper counts, including their head returns, are: + +| Helper | Actions | +| --- | ---: | +| Validate unary `n` | `4n+10` | +| Difference `a-b`, `0<=b<=a` | `8a+15` | +| Plus one on `a` | `8a+14` | +| Write three | `17` | +| Positive test on a positive word | `5` | +| Skip/digit/leading/trailing emission of `n` atoms | `6n+5` | +| Erase unary `n`, including END | `5n+7` | + +Let `N=G+H+K+Y+J0+J1+B`. Summing the eleven private values gives +`W=2H-4G+2Y-J0+2`. The literal successful sequence has these costs: + +| Stage | Actions | +| --- | ---: | +| Initialize eleven private words and the output | `36` | +| Validate seven inputs | `4N+70` | +| Positivity and unary arithmetic | `16H+16K+16Y-8G+8J1+175` | +| Emit stencil, END and return output head | `8L+63` | +| Erase eleven private words | `5W+77` | +| Final seven input-head checks | `7` | + +For the emission row there are fourteen helper calls emitting `L-3` +atoms and three directly written atoms: two guard pivots and the skipped +upper parity bit. The cost is +`6(L-3)+5*14+2*3+1+1+(2L+3)=8L+63`; the final term is the literal rewind. +Consequently + +```text +T_prod = 46H+20K+38Y-24G-J0+12J1+12B+438 + <= 70L+438. +``` + +The inequality uses `K<=Y`, `J1<=Y` and drops negative terms. This is an +all-size derivation from the helper counts, independently compared with +observed counters on finite cases. The producer has nineteen fixed roles. +Its exact visited cells, including input/output, markers and erased cells, +are `N+W+L+45 = 5H+K+4Y-3G+J1+2B+47 <= 6L+47`. + +The unchanged #4201 scanner admits this stencil. It conjoins each interval +test and outputs the complement, hence its bit at address `x` is exactly +`1_E(x)`. Its counter is erased, its input is protected and all three +heads return. Its established invoice is + +```text +T_scan = 8ML+15M+13L+18. +``` + +The composed producer/scanner has twenty-one fixed roles, cost exactly +`T_prod+T_scan <= 8ML+15M+83L+456`, and visited cells exactly +`N+W+2L+M+49 <= M+7L+51`. All seven geometry inputs remain unchanged, +all eleven producer work words and the scanner counter are blank, and +their heads are returned. The stencil and mask are owned outputs at LEFT. + +## 4. Joining the produced mask to the existing repair + +The parameter hypotheses above are the `r=2` instance of #4169: disjoint +windows, sufficient compact-digit width and the complete-target omission +condition. That proof gives a permutation `S` on the entire dirty address +rectangle, its explicit reverse word `S^-1`, and `S=T` on `Q` with +`S(Q)=T(Q)=Q`. It includes modular wrapping on exceptional addresses and +preserves the complete back field. This package does not infer those +properties from a finite permutation lookup. + +After `S`, the payload at a hole `x` originated at `S^-1(x)`. Its correct +key is `T(S^-1(x))`, using the current source values at every reverse-word +evaluation. This key permutes exactly `E`. The #4328 schedule extracts the +records marked by the produced mask, performs `L` stable binary bucket +passes, and reinserts the sorted keyed records into the marked addresses +in increasing order. Thus the payload of every origin `q` ends at `T(q)`; +good records were already correct. The mask and repair scratch are erased. +This caller then retires its owned stencil using the inherited marker-driven +eraser, including its END and head return, for an additional `5L+7` actions. +That retirement is separate from the producer/scanner output invoice above. + +For `h` holes and payload width `R`, the cited record/counter allowances +remain `9MR+5M` dense cells, `h(L+R)(9L+6)` sparse cells, and +`8M+4Lh+4L` counter cells, plus `h` key evaluations. This is the same +schedule and tariff, not a new all-bit invoice. The verifier's `RecordTape` +uses opaque records and width-weighted movements; its host key arithmetic +and indexing are not a literal bit-tape lowering. Producer/scanner actions +likewise exclude finite-control transitions and host observation. An exact +physical transition-table coefficient is not claimed by adding these +different models' meters. + +A valid-address test at reinsertion cannot establish payload correctness: +keys `S^-1(x)` alone still permute the holes. A complemented mask marks +`Q`, where `T(S^-1(x))=x`, and can also pass that test while leaving wrong +payloads. An intersection-of-failures mask misses addresses failing only +one target. The controls must check the intended mask and final payloads, +not merely successful reinsertion or key-set coverage. + +## 5. Evidence, attribution, and limits + +The verifier separately checks a grid of produced stencils and exact +action/space counts, and exhausts the declared small two-target geometries +through the scanner, reverse evaluator and record repair. Its stored +receipt specifies the actual cases and controls. These finite replays +test implementations; the quantified stencil and cost arguments above +apply beyond that grid. No larger-address replay is implied. + +Credit Cinna Davis/#4100 for the compact caller; ToikY/#4208 and #4201 for +the paid unary helpers and dense scanner; unpaidmoon/#4644 for the joined +one-target pipeline and this handoff; Ryanson Jonathan/#4328 for the +sparse tariff; Hiroki KUMAZAKI/#4169 for the arbitrary-source inverse; and +Douglas Colkitt and John-Michael Smith/#763 for the inherited compact and +exceptional-repair argument. Substantial OpenAI Codex assistance was used. + +Unary descriptor construction from the actual caller, variable target +count, last-`K` boundary targets, physical placement, ordinary interchanges, +paid binary inverse keys and a common complete machine invoice remain +outside this result. No selected frontier, exponent, full CRT supplier or +proof-assistant verification is changed or established here. diff --git a/research/crt-two-target-stencil/README.md b/research/crt-two-target-stencil/README.md new file mode 100644 index 0000000000..c18728a826 --- /dev/null +++ b/research/crt-two-target-stencil/README.md @@ -0,0 +1,143 @@ +# Paid two-target CRT stencil and repair join + +A protected unary producer now supplies the two-target stencil consumed by +ToikY's existing dense scanner. Its actual mask is then consumed by the retained +reverse-key repair. This answers open question 1 of unpaidmoon's +[PR4644](https://github.com/CrocSwap/integer-mult-bounds/pull/4644), which joined +one target only. The result is a scoped construction and cost proof with finite +implementation checks; it is not a new generic repair theorem or a new bound. + +## Interface and result + +The seven protected unary inputs `(G,H,K,Y,J0,J1,B)` satisfy + +```text +G>=1, H>=2G, K>=G+4, J0>=0, J1>=J0+K, Y>=J1+K, B>=0. +L=2H+Y+B, M=2^L; compact radix b=2^G. +``` + +`B` is a spectator width. Inputs have canonical LEFT/unary/END representation +and initially blank tails. The validator checks the word and its immediate +blank successor, not an arbitrary infinite tail. Addresses have fields +`(u,t,y,back)` of widths `(H,H,Y,B)` with arbitrary dirty values. + +For target `Ji`, digit `i` of both `u,t` must be less than `b-1`, and the +`K-1` guard bits above `Ji` must lie in `[2b,2^(K-1)-2b)`. The good set is the +intersection of the two predicates; the hole mask is the **union of their +failures**. The two source functions may depend on both guard windows but +must omit **both active target bits**, not merely their own bit. + +[producer.py](producer.py) uses eleven fixed private words, inherited paid +unary arithmetic and emission helpers, and only read/write/unit-move ports. +It preserves all seven inputs, erases its private data and END markers, and +returns every head. It also cleans up grammar/arithmetic rejection under the +representation contract. No host geometry test supplies the emitted stencil. + +[PROOF.md](PROOF.md) derives, for every admitted geometry: + +```text +Producer actions = 46H+20K+38Y-24G-J0+12J1+12B+438 <= 70L+438. +Producer visited cells = 5H+K+4Y-3G+J1+2B+47 <= 6L+47. +Producer + unchanged scanner actions <= 8ML+15M+83L+456. +Producer + scanner visited cells <= M+7L+51. +``` + +The producer/scanner composition has 21 fixed tape roles. The stencil and mask +are owned outputs. The retained repair consumes the real mask, uses +`T(S^-1(x))` keys at holes, restores all payloads and erases repair scratch. +This caller also retires its stencil for exactly `5L+7` further actions. +These counts charge reads, writes and unit moves; finite-control transitions +are not an exact physical transition-table tariff. The repair still has its +separate opaque-record/width-weighted model and host key arithmetic. Adding +those meters does not produce a complete bit-step invoice. + +## Evidence and reproduction + +[RESULT.json](RESULT.json) records: + +- 972 small geometries plus one long stencil, with independent interval-oracle + comparison, exact action/space formulas and opaque producer ports. +- Four full address spaces below: **180,224 addresses, 177,408 repaired holes**. + Every actual mask bit, forward/reverse macro, good-set invariant and final + payload is checked, including input/head restoration and scratch cleanup. +- Nine cleanly rejected geometry/grammar cases. Omitting the second digit test + misses 768 holes; omitting the upper guard misses 256. The paired choice + `f0=y[J1], f1=y[J0]` violates all-target independence and yields an actual + collision of the ideal map. + +| `(G,H,K,Y,J0,J1,B)` | Addresses | Holes | +| --- | ---: | ---: | +| `(1,2,5,10,0,5,0)` | 16,384 | 16,128 | +| `(1,2,5,10,0,5,1)` | 32,768 | 32,256 | +| `(1,3,5,10,0,5,0)` | 65,536 | 64,512 | +| `(1,2,5,12,1,7,0)` | 65,536 | 64,512 | + +The full replay uses cross-guard sources `f0=y[J0+1] xor y[J1+2]` and +`f1=y[J1+1] xor y[J0+2]`. Its complete-address cases have `G=1`; larger `G` +is covered only by the stencil grid and the quantified proof, not a larger +repair census. Universal inversion and repair statements remain cited from +the pinned predecessors. Finite examples do not prove those statements. + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/crt-two-target-stencil --check-only +python3.12 -B scripts/research_package.py --package research/crt-two-target-stencil +``` + +The registered runner executes ordinary and `-O` replay; both print +`PASS_CRT_TWO_TARGET_STENCIL`. Direct replay also works in a Git-free export: +`python3.12 -O -B research/crt-two-target-stencil/verify.py`. +The verifier authenticates thirteen live inputs before compiling their captured +source bytes, avoiding predecessor bytecode-cache imports. Ordinary replay +compares the frozen receipt and writes nothing; `--write-result` is an explicit +authoring operation. [SOURCES.json](SOURCES.json) pins base +`b91956876e5b4122fd89179f1b57557ff8378f15`, blobs and SHA256 values. + +## Scope, overlap and expansion decision + +[Task metadata](TASK.json) refines priority-revision-7 `uniform-transfer-audit` +to the producer boundary. [Discussion4985](https://github.com/CrocSwap/integer-mult-bounds/discussions/4985) +is the canonical claim/result. PR4201 already scans multi-target stencils and +PR4328 already repairs host-built multi-target masks. PR4904's two-target sharp +window audit concerns macro algebra and excludes tape repair. This package's +added value is paid stencil admission and its actual join, not those existing +capabilities. PR4716's current-state key audit and JoyboyBrian's newly published +[PR4982](https://github.com/CrocSwap/integer-mult-bounds/pull/4982) remain separate: +PR4982 lowers the key port at fixed `(u2,t2,y8)` geometry with a supplied ROM; +it does not supply this unary two-target stencil producer. + +The family decision is **narrow**: retain this local interface and stop. Caller +descriptor construction/transport and binary keys remain unknown here; the +existing record repair allowance is retained, not replaced. Variable target +count, last-`K` boundary targets, physical placement, ordinary interchanges and +a common complete machine invoice remain open. No full supplier, native/Lean +replay, proof-assistant acceptance or selected-frontier change is claimed. +Selected conditional kappa remains `.00302015`. + +## Open next questions + +1. Can one actual CRT caller construct, transport and restore these seven unary + descriptors within its complete allowance? First pin that caller and its + binary-to-unary representation; this package begins after that boundary. +2. Can a variable-size ordered target descriptor stream admit disjoint windows + with fixed tape roles and paid cleanup? First specify descriptor ownership, + overlap rejection and last-`K` handling. A fresh overlap/family decision and + full allowance must precede another implementation round. + +[The structured questions](TASK.json) state relevance and blockers. The current +[Discussion4709](https://github.com/CrocSwap/integer-mult-bounds/discussions/4709) +handoffs and PR4982 should be checked before assigning related key work. + +## Credit + +Cinna Davis/#4100 supplies the compact CRT caller. ToikY/#4208 and #4201 supply +the unary helpers and scanner; unpaidmoon/#4644 supplies the one-target join +and this handoff; Ryanson Jonathan/#4328 supplies the repair schedule/tariff; +Hiroki KUMAZAKI/#4169 supplies the arbitrary-source inverse. Douglas Colkitt and +John-Michael Smith/#763 supply the inherited compact and exceptional-repair +argument. All predecessor sources remain unchanged and pinned. + +Prepared by Hiroki KUMAZAKI (@kumagi) with substantial OpenAI Codex assistance, +including separate agent checks of the geometry and cost algebra. No independent +human review is claimed. Apache-2.0. diff --git a/research/crt-two-target-stencil/RESULT.json b/research/crt-two-target-stencil/RESULT.json new file mode 100644 index 0000000000..7b3f082bfd --- /dev/null +++ b/research/crt-two-target-stencil/RESULT.json @@ -0,0 +1,146 @@ +{ + "authenticated_inputs": 13, + "cases": [ + { + "addresses": 16384, + "good": 256, + "holes": 16128, + "mask_sha256": "5d1906a782234a5664d5b1478baaaea2becd207fe111676581c6fc64c40fca29", + "producer_actions": 1046, + "producer_visited_cells": 104, + "repair_record_cell_meters": { + "counter": 1034264, + "dense": 706048, + "evaluations": 16128, + "holes": 16128, + "sparse": 59157504 + }, + "repaired_payload_sha256": "1aafb9358a015cf404961552f72500acc8ab9270e7ef15974748ae0d13dabc63", + "scanner_actions": 2080968, + "shape": [ + 1, + 2, + 5, + 10, + 0, + 5, + 0 + ], + "stencil_retirement_actions": 77 + }, + { + "addresses": 32768, + "good": 512, + "holes": 32256, + "mask_sha256": "940573898dffadc2e700682169d1b8ab9de524b7cbf85dc7f400e6bbb8ae4477", + "producer_actions": 1058, + "producer_visited_cells": 106, + "repair_record_cell_meters": { + "counter": 2197530, + "dense": 1512960, + "evaluations": 32256, + "holes": 32256, + "sparse": 135475200 + }, + "repaired_payload_sha256": "c9fb5ed05fb95016c28e149e5b85cd23775c35d93f154eda0a967cd1be739802", + "scanner_actions": 4423893, + "shape": [ + 1, + 2, + 5, + 10, + 0, + 5, + 1 + ], + "stencil_retirement_actions": 82 + }, + { + "addresses": 65536, + "good": 1024, + "holes": 64512, + "mask_sha256": "d6aa8986b46423564183b50f27f9f8de53f42b8522c9863fa1a7f2aa37fa6242", + "producer_actions": 1092, + "producer_visited_cells": 109, + "repair_record_cell_meters": { + "counter": 4653084, + "dense": 3227648, + "evaluations": 64512, + "holes": 64512, + "sparse": 307593216 + }, + "repaired_payload_sha256": "c9b108a5a2e1ecaf27e1c01cfee60906590b192decefae1bc5c3416833641fca", + "scanner_actions": 9371874, + "shape": [ + 1, + 3, + 5, + 10, + 0, + 5, + 0 + ], + "stencil_retirement_actions": 87 + }, + { + "addresses": 65536, + "good": 1024, + "holes": 64512, + "mask_sha256": "59a3a7aac537019f5c0ab8769f0a0be1599963d70285470fd24284e85be5f431", + "producer_actions": 1145, + "producer_visited_cells": 114, + "repair_record_cell_meters": { + "counter": 4653084, + "dense": 3227648, + "evaluations": 64512, + "holes": 64512, + "sparse": 307593216 + }, + "repaired_payload_sha256": "e79996c0a14acf0d9759edce6340183c7ca48d4e28cf0370429d6b576762793d", + "scanner_actions": 9371874, + "shape": [ + 1, + 2, + 5, + 12, + 1, + 7, + 0 + ], + "stencil_retirement_actions": 87 + } + ], + "clean_rejections": 9, + "controls": { + "cross_target_ideal_collision": true, + "cross_target_source_rejected": true, + "omitted_tests": [ + { + "first_missing_hole": 2312, + "mismatch_count": 768, + "program": "omit_second_digit" + }, + { + "first_missing_hole": 8, + "mismatch_count": 256, + "program": "omit_second_guard" + } + ] + }, + "producer_grid": { + "grid_max_actions": 2003, + "grid_shapes": 972, + "large_actions": 26103, + "large_shape": [ + 7, + 31, + 17, + 500, + 9, + 400, + 23 + ], + "large_visited_cells": 2644 + }, + "status": "PASS_CRT_TWO_TARGET_STENCIL" +} diff --git a/research/crt-two-target-stencil/SOURCES.json b/research/crt-two-target-stencil/SOURCES.json new file mode 100644 index 0000000000..d333378aaf --- /dev/null +++ b/research/crt-two-target-stencil/SOURCES.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/crt-arbitrary-source-repair/PROOF.md", + "usage": "input", + "git_blob": "147633ce18d41f44cbd6bdc2030fcdf962b415a4", + "sha256": "1b8cb76afc6bf923c31377ba22c7675b3e563e3341fc5db0cd9d1057be4ee624" + }, + { + "path": "research/crt-arbitrary-source-repair/verify.py", + "usage": "input", + "git_blob": "813eafd24f031b046b2d4aaabdcb0950538980f1", + "sha256": "9a646116e430a242fc16c98d6e35c21290a00ccd9951145290b9a4bf5c007d48" + }, + { + "path": "research/crt-dense-guard-scan/PROOF.md", + "usage": "input", + "git_blob": "235d7405ffcf712ad3905c3077719554ade0790c", + "sha256": "c075a3c261bb824884f0da9f99fed227b15f9fac087bbdeb2c2cb861d4091f11" + }, + { + "path": "research/crt-dense-guard-scan/README.md", + "usage": "input", + "git_blob": "fd0dd321baa1592999677f212ffa77cbb1bb513c", + "sha256": "912595166aded8591819c1f4fccdd7bfa44361906a1466057f838a656e85f329" + }, + { + "path": "research/crt-dense-guard-scan/machine.py", + "usage": "input", + "git_blob": "ce763898bd7b4401bbab818c640a0593b65c9a82", + "sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7" + }, + { + "path": "research/crt-joined-hole-repair/PROOF.md", + "usage": "input", + "git_blob": "266100ea27e94c461ab9674c46ee5cf8ec8fea83", + "sha256": "0111d3802389cae2b11c168163d53117ab3d88ac37201911b4b658bb56a69470" + }, + { + "path": "research/crt-joined-hole-repair/README.md", + "usage": "input", + "git_blob": "2e3f50c146149640055cc1cc4e333552eb45d453", + "sha256": "ccbac5e3986a245c3590550ede0a74f196ac46d892415d1fc221e8e2253ae9ed" + }, + { + "path": "research/crt-joined-hole-repair/verify.py", + "usage": "input", + "git_blob": "8fe63a66bc716a8607671058fea53143afe8ac9a", + "sha256": "0caea522dd692a251d79d51a98705784f3b73374c98561d7cd1fd50aea0af637" + }, + { + "path": "research/crt-unary-stencil-producer/PROOF.md", + "usage": "input", + "git_blob": "d81a6cca7c433bc7fb015a41cc0f72bf9f676a5d", + "sha256": "4076e6041bedce5269c1d4e3d62f0e4213a4b2e790fe270b89b4b4f3363e08aa" + }, + { + "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/pr4100-crt-repair-tariff/README.md", + "usage": "input", + "git_blob": "1eba9122777570041acbd5ddcfee22ceb0e60703", + "sha256": "5953ed2ae02a609744df2274810d7016cd766f2e43bdf8f79047084ae55a0513" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "usage": "input", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + } + ] +} diff --git a/research/crt-two-target-stencil/TASK.json b/research/crt-two-target-stencil/TASK.json new file mode 100644 index 0000000000..7a84a0f1e8 --- /dev/null +++ b/research/crt-two-target-stencil/TASK.json @@ -0,0 +1,115 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "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": "PR4644 open question 1: prove and implement paid protected-unary admission of exactly two ordered disjoint CRT guard windows, then join its actual stencil and dense mask to the retained reverse-key repair.", + "scope_change_reason": "The card permits one caller-bound CRT implication. PR4644 supplied the one-target join but left two-target stencil production open; PR4201 and PR4328 already accept externally supplied multi-target stencils/masks. This result supplies and charges that missing producer boundary, not a new generic repair theorem.", + "bottleneck_link": "Removes host-generated stencil admission at the two-target CRT mask boundary. A complete fixed-tape supplier still needs paid caller descriptor transport, binary key services and a common complete tariff; this local result neither admits that supplier nor changes selected conditional kappa .00302015.", + "budget_minutes": 60, + "stop_rule": "Stop after a quantified two-target stencil/cleanup/action proof, fixed geometry grid, four exhaustive joined caller cases and semantic omission controls. No variable-target implementation campaign, binary-key lowering, full supplier replay or selected-frontier update.", + "outcome": "completed", + "evidence": "PROOF.md gives all-size two-target stencil identity, cleanup and exact producer action/space counts. RESULT.json records 972 small plus one long producer geometry, four complete caller cases (180224 addresses, 177408 holes), nine clean rejections, two omission controls and an all-target-independence collision control. VERIFY.json registers normal and optimized source-bound replay.", + "author": "Hiroki KUMAZAKI (@kumagi), with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in selection, implementation, proofs, verification, coordination and writing; separate Codex agents independently checked the geometry and action algebra. No independent human or proof-assistant acceptance claimed.", + "open_questions": [ + { + "question": "Can the actual CRT caller supply and transport these seven protected unary geometry words within its complete bit-step allowance?", + "why_it_matters": "The new producer charges consumption of admitted unary geometry, but its admission premise is not free caller construction.", + "first_step": "Pin one actual two-target caller, identify where G,H,K,Y,J0,J1,B reside, and account for binary-to-unary conversion, placement and eventual descriptor restoration.", + "blocked_by": "No paid descriptor transport contract is supplied here. PR4982 separately lowers a fixed-geometry binary key port; it is not this caller admission." + }, + { + "question": "Does a variable-size ordered target descriptor stream admit disjoint guards with a fixed tape inventory and explicit cleanup?", + "why_it_matters": "The present code deliberately unrolls exactly two targets; increasing sample size does not establish uniform target-count admission.", + "first_step": "Write the descriptor representation and ownership contract first, including repeated digit boundaries, overlap rejection and the last-K target convention; compare the full cost before implementation.", + "blocked_by": "A caller-owned descriptor stream and complete cost allowance, plus a fresh overlap/family decision, are required." + } + ], + "family_decision": { + "decision": "narrow", + "milestone": "local producer/consumer interface proof and author-checked replay", + "replacement": "The executable unary producer replaces host-built two-target stencil bytes. Every producer read/write/unit move and final stencil erasure is charged.", + "proved": "Under protected unary representation and disjoint full guards: producer shape, cleanup, exact primitive-action invoice and composition with cited scanner semantics.", + "constructively_upper_bounded": "Existing record/counter repair allowances, retained unchanged and checked on four complete fixtures.", + "unknown": "Actual caller construction/transport of unary descriptors, binary source/key work, physical placement and a common all-bit complete supplier invoice.", + "stop": "No downstream family expansion is inferred from this module; reassess a concrete caller and its complete allowance before further implementation." + }, + "upstream_checkpoint": { + "commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "priority_revision": 7, + "checked_at": "2026-10-23T05:35:24+00:00", + "relevant_changes": "Canonical main remains the round base; guidance, selected record and pinned predecessor bytes are unchanged." + }, + "overlap_check": { + "searched_at": "2026-10-23T05:35:46.853615+00:00", + "coverage": { + "head_local_notes": 6636, + "all_head_notes_searched": true, + "open_pr_bodies": 333, + "discussion_records": 4085, + "remote_complete_pagination": true + }, + "nearest_work": [ + "PR4644 one-target join (open question 1)", + "PR4208 one-target paid producer", + "PR4201 generic admitted-stencil scanner", + "PR4328 host-mask multi-target repair", + "PR4904 two-target sharp-window algebra (excludes tape repair)", + "PR4716 current-state query audit and PR4982 binary key port, exact head 67154122b2867e6dee5b9b25f2f1c862a3e81e95 (Discussion4709 claim updated to DONE)" + ], + "result": "No competing paid two-target producer claim found within this coverage. PR4201/4328 generic multi-target consumption remains predecessor work. Own claim is Discussion4985. Final refresh observed the binary-key claim completed as PR4982; scope remains distinct.", + "limits": "No arbitrary code diff or unpublished-work coverage; merged work searched through tracked notes/ledger and targeted recent CRT PR reads." + } +} diff --git a/research/crt-two-target-stencil/VERIFY.json b/research/crt-two-target-stencil/VERIFY.json new file mode 100644 index 0000000000..7bc0c13d1b --- /dev/null +++ b/research/crt-two-target-stencil/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/crt-arbitrary-source-repair/PROOF.md", + "research/crt-arbitrary-source-repair/verify.py", + "research/crt-dense-guard-scan/PROOF.md", + "research/crt-dense-guard-scan/README.md", + "research/crt-dense-guard-scan/machine.py", + "research/crt-joined-hole-repair/PROOF.md", + "research/crt-joined-hole-repair/README.md", + "research/crt-joined-hole-repair/verify.py", + "research/crt-unary-stencil-producer/PROOF.md", + "research/crt-unary-stencil-producer/README.md", + "research/crt-unary-stencil-producer/producer.py", + "research/pr4100-crt-repair-tariff/README.md", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Authenticate thirteen live inputs; check implementation consistency on 973 producer geometries and four exhaustive two-target repair fixtures; check cleanup, exact action invoices, omission/source controls and byte-identical frozen receipt." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Authenticate thirteen live inputs; check implementation consistency on 973 producer geometries and four exhaustive two-target repair fixtures; check cleanup, exact action invoices, omission/source controls and byte-identical frozen receipt." + } + ] +} diff --git a/research/crt-two-target-stencil/producer.py b/research/crt-two-target-stencil/producer.py new file mode 100644 index 0000000000..2be7dcd307 --- /dev/null +++ b/research/crt-two-target-stencil/producer.py @@ -0,0 +1,111 @@ +"""Two ordered CRT targets: protected unary geometry to a paid guard stencil. + +The seven protected unary inputs are G,H,K,Y,J0,J1,B. The runtime accesses +tapes only through the passed PR4208 marker-driven helpers and read/write/ +one-cell-move methods. It never reads host lengths, coordinates, action +counts or tape storage. The target blocks below are explicitly unrolled. + +The caller supplies the authenticated retained helper module as base and a +Tape factory whose tapes have the permanent LEFT infrastructure. This module +does no loading or I/O. Normal success returns (eleven private roles, stencil). +All private data and END markers are blank; all heads are at LEFT. Inputs +remain protected on success and on grammar/arithmetic rejection. + +ToikY's PR4208 supplies the unary arithmetic, emission and cleanup helpers; +PR4201 supplies the unchanged consumer and atom format; Cinna Davis supplies +the CRT guard predicate. Hiroki KUMAZAKI (@kumagi), with substantial OpenAI +Codex assistance. Apache-2.0. Full lineage and scope are in README/PROOF. +""" + + +def produce(G, H, K, Y, J0, J1, B, Tape, *, base, + omit_second_digit=False, omit_second_guard=False): + """Seven protected canonical unary words -> owned two-target stencil. + + Admits G>=1, H>=2G, K>=G+4, J1>=J0+K, Y>=J1+K. J0 and B + are nonnegative by unary syntax. Entry and malformed-input contracts + match the retained helper module, including the unique permanent LEFT + and initially blank tails. The two fixed mutation flags preserve output + length while removing digit1's test or the upper target's guard test. + They are faulty verification programs, not alternative admitted modes. + """ + HG, HGG, KG, THREE, A, TAIL, J0P, J10, GAP, YJ1, TOP = ( + Tape(), Tape(), Tape(), Tape(), Tape(), Tape(), Tape(), Tape(), + Tape(), Tape(), Tape()) + stencil = Tape() + work = (HG, HGG, KG, THREE, A, TAIL, J0P, J10, GAP, YJ1, TOP) + for tape in work: + base.empty_word(tape) + base.empty_word(stencil) + try: + for tape in (G, H, K, Y, J0, J1, B): + base.validate(tape) + base.positive(G) + base.difference(H, G, HG) + base.difference(HG, G, HGG) + base.difference(K, G, KG) + base.three(THREE) + base.difference(KG, THREE, A) + base.positive(A) + base.plus_one(G, TAIL) + base.plus_one(J0, J0P) + base.difference(J1, J0, J10) + base.difference(J10, K, GAP) + base.difference(Y, J1, YJ1) + base.difference(YJ1, K, TOP) + + stencil.move(1) + # MSB-first u field: inactive high part, digit1, then digit0. + base.skip(HGG, stencil) + if omit_second_digit: + base.skip(G, stencil) + else: + base.digit(G, stencil) + base.digit(G, stencil) + # The independent t field has the same two separate digit intervals. + base.skip(HGG, stencil) + if omit_second_digit: + base.skip(G, stencil) + else: + base.digit(G, stencil) + base.digit(G, stencil) + + base.skip(TOP, stencil) + # Upper target J1: K-1 higher guard bits, then its parity bit. + if omit_second_guard: + base.skip(A, stencil) + stencil.write(base.SKIP) + stencil.move(1) + base.skip(TAIL, stencil) + else: + base.leading_guard(A, stencil, True) + stencil.write(("G", False, False, "1", "1")) + stencil.move(1) + base.trailing_guard(TAIL, stencil) + stencil.write(base.SKIP) + stencil.move(1) + base.skip(GAP, stencil) + # Lower target J0: its separate guard and all lower/parity SKIP bits. + base.leading_guard(A, stencil, True) + stencil.write(("G", False, False, "1", "1")) + stencil.move(1) + base.trailing_guard(TAIL, stencil) + base.skip(J0P, stencil) + base.skip(B, stencil) + stencil.write(base.END) + base.rewind(stencil) + except ValueError: + # All arithmetic rejects before output construction. Every private + # subtraction output is still a complete END-terminated word on an + # underflow, so the retained eraser has a valid finite stop marker. + for tape in work: + base.erase(tape) + base.erase(stencil) + for tape in (G, H, K, Y, J0, J1, B): + base.rewind(tape) + raise + for tape in work: + base.erase(tape) + for tape in (G, H, K, Y, J0, J1, B): + base.rewind(tape) + return work, stencil diff --git a/research/crt-two-target-stencil/verify.py b/research/crt-two-target-stencil/verify.py new file mode 100644 index 0000000000..ff6bff5090 --- /dev/null +++ b/research/crt-two-target-stencil/verify.py @@ -0,0 +1,339 @@ +"""Source-bound two-target producer/consumer replay; read-only by default. + +Hiroki KUMAZAKI (@kumagi), substantial OpenAI Codex assistance. Apache-2.0. +Predecessor code and proofs retain the attribution in README/PROOF. +Host geometry/oracles and keys are verification work, not hidden tape steps. +""" +from __future__ import annotations + +import argparse +import hashlib +from itertools import product +import json +from pathlib import Path +import sys +import types + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SHAPES = ((1, 2, 5, 10, 0, 5, 0), (1, 2, 5, 10, 0, 5, 1), + (1, 3, 5, 10, 0, 5, 0), (1, 2, 5, 12, 1, 7, 0)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(): + data = {} + for row in json.loads((PACKAGE/'SOURCES.json').read_text())['files']: + if row['usage'] != 'input': + continue + raw = (ROOT/row['path']).read_bytes() + need(hashlib.sha256(raw).hexdigest() == row['sha256'], 'source SHA256 mismatch: '+row['path']) + need(hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == row['git_blob'], + 'source Git blob mismatch: '+row['path']) + data[row['path']] = raw + need(len(data) == 13, 'exact thirteen-input scope') + return data + + +def load(name, path, raw): + module = types.ModuleType(name) + module.__file__ = str(ROOT/path) + sys.modules[name] = module + exec(compile(raw, module.__file__, 'exec'), module.__dict__) + return module + + +def blank(machine, tape): + return tape.head == 0 and tape.cells[0] == machine.LEFT and all( + x == machine.BLANK for x in tape.cells[1:]) + + +class Ports: + """Observer-side registry; the producer sees only read/write/move ports.""" + def __init__(self, machine): + self.machine = machine + self.tapes = {} + self.calls = [0, 0, 0] + + def make(self, cells=None): + underlying = self.machine.Tape(cells) + owner = self + + class Port: + __slots__ = () + + def read(self): + owner.calls[0] += 1 + return underlying.read() + + def write(self, symbol): + owner.calls[1] += 1 + underlying.write(symbol) + + def move(self, direction): + owner.calls[2] += 1 + underlying.move(direction) + + port = Port() + self.tapes[port] = underlying + return port + + def unary(self, n): + return self.make([self.machine.LEFT]+['1']*n+[self.machine.END, self.machine.BLANK]) + + +def expected_atoms(shape): + """Independent address-interval oracle; never used by the producer.""" + g, h, k, y, j0, j1, back = shape + length = 2*h+y+back + ranges = [] + for start in (0, h): + for i in (0, 1): + ranges.append((start+h-(i+1)*g, start+h-i*g, 'D')) + for target in (j0, j1): + ranges.append((2*h+y-target-k, 2*h+y-target-1, 'G')) + low, high = 1 << (g+1), (1 << (k-1))-(1 << (g+1)) + result = [] + for position in range(length): + found = [(a, b, kind) for a, b, kind in ranges if a <= position < b] + need(len(found) <= 1, 'oracle disjoint intervals') + if not found: + result.append(('S', False, False, '0', '0')) + else: + a, b, kind = found[0] + shift = b-1-position + result.append((kind, position == a, position == b-1, + str((low >> shift) & 1) if kind == 'G' else '0', + str((high >> shift) & 1) if kind == 'G' else '0')) + return result + + +def producer_bill(shape): + g, h, k, y, j0, j1, back = shape + return 46*h+20*k+38*y-24*g-j0+12*j1+12*back+438 + + +def producer_space(shape): + g, h, k, y, j0, j1, back = shape + return 5*h+k+4*y-3*g+j1+2*back+47 + + +def produce(machine, base, producer, shape, **mutants): + ports = Ports(machine) + inputs = tuple(ports.unary(n) for n in shape) + before = [list(ports.tapes[p].cells) for p in inputs] + work, stencil = producer.produce(*inputs, ports.make, base=base, **mutants) + need(len(ports.tapes) == 19 and len(work) == 11, 'fixed nineteen producer roles') + need(all(ports.tapes[p].cells == old for p, old in zip(inputs, before)), 'protected unary inputs') + need(all(blank(machine, ports.tapes[p]) for p in work), 'producer work/END cleanup') + need(all(t.head == 0 for t in ports.tapes.values()), 'all producer heads returned') + tape = ports.tapes[stencil] + need(tape.cells[0] == machine.LEFT and tape.cells[-1] == machine.END, 'stencil markers') + actions = sum(t.actions for t in ports.tapes.values()) + need(actions == sum(ports.calls), 'independent primitive-call meter') + space = sum(len(t.cells) for t in ports.tapes.values()) + if not any(mutants.values()): + need(tape.cells[1:-1] == expected_atoms(shape), 'literal producer versus interval oracle') + need(actions == producer_bill(shape), 'exact producer action formula') + need(space == producer_space(shape), 'exact visited producer cells') + length = 2*shape[1]+shape[3]+shape[6] + need(actions <= 70*length+438 and space <= 6*length+47, 'linear producer bounds') + return tape, actions, space + + +def stencil_grid(machine, base, producer): + cases = 0 + largest = 0 + for g, extra, guard_extra, j0, gap, top, back in product( + range(1, 4), range(3), range(3), (0, 1, 3), (0, 1, 2), (0, 1), (0, 1)): + h, k = 2*g+extra, g+4+guard_extra + j1 = j0+k+gap + shape = g, h, k, j1+k+top, j0, j1, back + _, actions, _ = produce(machine, base, producer, shape) + largest = max(largest, actions) + cases += 1 + # A long stencil checks marker loops without enumerating its address cube. + large = (7, 31, 17, 500, 9, 400, 23) + _, actions, space = produce(machine, base, producer, large) + return dict(grid_shapes=cases, grid_max_actions=largest, + large_shape=large, large_actions=actions, large_visited_cells=space) + + +def rejects(machine, base, producer): + invalid = ((0, 2, 5, 10, 0, 5, 0), (2, 3, 6, 12, 0, 6, 0), + (1, 2, 4, 10, 0, 5, 0), (1, 2, 5, 10, 2, 1, 0), + (1, 2, 5, 10, 0, 4, 0), (1, 2, 5, 9, 0, 5, 0)) + tested = 0 + for shape in invalid + (SHAPES[0],)*3: + ports = Ports(machine) + inputs = tuple(ports.unary(n) for n in shape) + if tested == len(invalid): + ports.tapes[inputs[0]].cells[1] = 'x' + elif tested == len(invalid)+1: + ports.tapes[inputs[0]].cells[-1] = '1' + elif tested == len(invalid)+2: + ports.tapes[inputs[0]].head = 1 + before = [list(ports.tapes[p].cells) for p in inputs] + try: + producer.produce(*inputs, ports.make, base=base) + except ValueError: + pass + else: + raise ValueError('invalid geometry/grammar unexpectedly accepted') + need(all(ports.tapes[p].cells == old for p, old in zip(inputs, before)), 'reject preserves inputs') + need(all(t.head == 0 for t in ports.tapes.values()), 'reject restores heads') + need(all(blank(machine, t) for p, t in ports.tapes.items() if p not in inputs), + 'reject cleans private/output markers') + tested += 1 + return tested + + +def scan(machine, stencil): + before = list(stencil.cells) + length = len(before)-2 + previous = stencil.actions + counter, mask = machine.transduce(stencil) + invoice = stencil.actions-previous+counter.actions+mask.actions + need(stencil.cells == before and stencil.head == mask.head == 0, 'scanner protected input/heads') + need(blank(machine, counter), 'scanner work cleared') + need(invoice == 8*(1 << length)*length+15*(1 << length)+13*length+18, 'unchanged scanner invoice') + return mask, invoice + + +def expected_good(shape): + g, h, k, y, j0, j1, back = shape + return ((1 << g)-1)**4 * ((1 << (k-1))-(1 << (g+2)))**2 * ( + 1 << (2*(h-2*g)+y-2*(k-1)+back)) + + +def run_shape(machine, base, producer, joined, Word, crt, shape): + g, h, k, y, j0, j1, back = shape + length = 2*h+y+back + size = 1 << length + stencil, setup, visited = produce(machine, base, producer, shape) + mask, scanning = scan(machine, stencil) + bits = joined.read_mask(machine, mask) + need(len(bits) == size, 'complete scanner mask') + word = Word(g, h, y, (j0, j1), k) + + def source(current_y): + return (((current_y >> (j0+1)) ^ (current_y >> (j1+2))) & 1, + ((current_y >> (j1+1)) ^ (current_y >> (j0+2))) & 1) + + word.check_source(source) + arrived, ideal_at, keys = [None]*size, [None]*size, [None]*size + holes = [] + good = 0 + for address in range(size): + u, t, middle, tail = joined.split_address(address, h, y, back) + state = u, t, middle + per_target = [(((u >> (i*g)) % (1 << g)) != (1 << g)-1 + and ((t >> (i*g)) % (1 << g)) != (1 << g)-1 + and 2*(1 << g) <= ((middle >> (j+1)) % (1 << (k-1))) + < (1 << (k-1))-2*(1 << g)) for i, j in enumerate((j0, j1))] + hole = not all(per_target) + need(hole == (bits[address] == '1'), 'produced mask is union of target failures') + need(hole == (not word.good(state)) == (not crt.good(u, t, middle, + bits=g, positions=(j0, j1), guard=k)), 'both retained good predicates') + holes.append(hole) + out = word.run(state, source) + need(out == crt.compact(u, t, middle, source, bits=g, positions=(j0, j1), + ybits=y, control_bits=h), 'literal forward versus retained compact') + origin = word.run(state, source, inverse=True) + need(word.run(origin, source) == state, 'literal inverse/forward') + wanted = word.ideal(state, source) + need(word.good(out) == word.good(state) == word.good(wanted), 'good/bad invariance') + if not hole: + need(out == wanted, 'good endpoint equals ideal') + good += 1 + image = joined.pack_address(*out, tail, h, y, back) + need(arrived[image] is None, 'raw image injectivity') + arrived[image] = address + ideal_at[address] = joined.pack_address(*wanted, tail, h, y, back) + if hole: + keys[address] = joined.pack_address(*word.ideal(origin, source), tail, h, y, back) + need(good == expected_good(shape) and all(x is not None for x in arrived), 'exact product count and bijection') + mask_hash = hashlib.sha256(''.join(bits).encode()).hexdigest() + layout, meters = joined.repair(machine, mask, length, size, length, holes, keys, arrived) + need(all(layout[ideal_at[q]] == q for q in range(size)), 'complete ideal payload restoration') + need(meters['evaluations'] == size-good, 'repair evaluates keys only at holes') + dense, sparse, counter = joined.bounds(length, size, length, size-good) + need(meters['dense'] <= dense and meters['sparse'] <= sparse and meters['counter'] <= counter, + 'retained record-cell repair bounds') + need(blank(machine, mask), 'consumed mask cleanup') + # The stencil is owned output from the predecessor; this caller explicitly retires it. + old_actions = stencil.actions + base.erase(stencil) + retirement = stencil.actions-old_actions + need(retirement == 5*length+7 and blank(machine, stencil), 'owned stencil retirement') + return dict(shape=shape, addresses=size, good=good, holes=size-good, producer_actions=setup, + producer_visited_cells=visited, scanner_actions=scanning, + stencil_retirement_actions=retirement, mask_sha256=mask_hash, + repaired_payload_sha256=hashlib.sha256(b''.join(x.to_bytes(4,'little') for x in layout)).hexdigest(), + repair_record_cell_meters=meters) + + +def semantic_controls(machine, base, producer, joined, Word): + shape = SHAPES[0] + g, h, k, y, j0, j1, back = shape + word = Word(g, h, y, (j0, j1), k) + expected = [not word.good(joined.split_address(x,h,y,back)[:3]) for x in range(1 << (2*h+y+back))] + results = [] + for name in ('omit_second_digit', 'omit_second_guard'): + stencil, _, _ = produce(machine, base, producer, shape, **{name: True}) + mask, _ = scan(machine, stencil) + bits = joined.read_mask(machine, mask) + wrong = [i for i, (bit, want) in enumerate(zip(bits, expected)) if (bit == '1') != want] + need(wrong and all(expected[i] and bits[i] == '0' for i in wrong), 'omission under-detects holes') + results.append(dict(program=name, mismatch_count=len(wrong), first_missing_hole=wrong[0])) + def cross_source(value): + return (value >> j1) & 1, (value >> j0) & 1 + try: + word.check_source(cross_source) + except ValueError: + pass + else: + raise ValueError('source reading other active target accepted') + need(word.ideal((0,0,0),cross_source) == word.ideal((0,0,(1 << j0)|(1 << j1)),cross_source), + 'cross-target source produces an actual ideal collision') + return dict(omitted_tests=results, cross_target_source_rejected=True, cross_target_ideal_collision=True) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-result', action='store_true') + args = parser.parse_args() + sources = authenticate() + modules = [] + for name, path in ( + ('two_target_base','research/crt-unary-stencil-producer/producer.py'), + ('two_target_machine','research/crt-dense-guard-scan/machine.py'), + ('two_target_join','research/crt-joined-hole-repair/verify.py'), + ('two_target_word','research/crt-arbitrary-source-repair/verify.py'), + ('two_target_crt','research/unconditional-batched-crt/check_batched_crt.py')): + modules.append(load(name,path,sources[path])) + path = 'research/crt-two-target-stencil/producer.py' + producer = load('two_target_producer',path,(ROOT/path).read_bytes()) + base, machine, joined, reverse, crt = modules + result = dict(status='PASS_CRT_TWO_TARGET_STENCIL', authenticated_inputs=len(sources), + producer_grid=stencil_grid(machine,base,producer), + clean_rejections=rejects(machine,base,producer), + cases=[run_shape(machine,base,producer,joined,reverse.Word,crt,s) for s in SHAPES], + controls=semantic_controls(machine,base,producer,joined,reverse.Word)) + encoded = json.dumps(result,indent=2,sort_keys=True)+'\n' + path = PACKAGE/'RESULT.json' + if args.write_result: + path.write_text(encoded) + else: + need(path.read_text() == encoded, 'frozen RESULT.json differs; no files rewritten') + print(result['status']) + print(str(sum(r['addresses'] for r in result['cases']))+' addresses; '+str(sum(r['holes'] for r in result['cases']))+' repaired holes') + print('972 small and one long produced stencil; 9 cleaned rejections; 2 omission controls; source collision control') + + +if __name__ == '__main__': + main()