From 45fc0750436ae5cc14b95fba81c030a3d7df3412 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Tue, 20 Oct 2026 05:04:10 -0700 Subject: [PATCH] Audit conditional CRT last-K two-slice streaming tariff --- .../INDEPENDENT-REVIEW.md | 131 +++++++ research/crt-last-k-streaming/NOTICE.md | 7 + .../crt-last-k-streaming/PRIMARY-REVIEW.json | 94 +++++ research/crt-last-k-streaming/PROOF.md | 266 +++++++++++++ .../crt-last-k-streaming/R-ONE-PAYLOAD.json | 13 + research/crt-last-k-streaming/README.md | 119 ++++++ research/crt-last-k-streaming/REPORT.json | 68 ++++ research/crt-last-k-streaming/RESULT.json | 110 ++++++ .../crt-last-k-streaming/SOURCE-PINS.json | 20 + research/crt-last-k-streaming/SOURCES.json | 36 ++ research/crt-last-k-streaming/TASK.json | 80 ++++ research/crt-last-k-streaming/VERIFY.json | 84 ++++ .../independent_tail_check.py | 125 ++++++ .../r_one_payload_check.py | 49 +++ research/crt-last-k-streaming/verify.py | 359 ++++++++++++++++++ 15 files changed, 1561 insertions(+) create mode 100644 research/crt-last-k-streaming/INDEPENDENT-REVIEW.md create mode 100644 research/crt-last-k-streaming/NOTICE.md create mode 100644 research/crt-last-k-streaming/PRIMARY-REVIEW.json create mode 100644 research/crt-last-k-streaming/PROOF.md create mode 100644 research/crt-last-k-streaming/R-ONE-PAYLOAD.json create mode 100644 research/crt-last-k-streaming/README.md create mode 100644 research/crt-last-k-streaming/REPORT.json create mode 100644 research/crt-last-k-streaming/RESULT.json create mode 100644 research/crt-last-k-streaming/SOURCE-PINS.json create mode 100644 research/crt-last-k-streaming/SOURCES.json create mode 100644 research/crt-last-k-streaming/TASK.json create mode 100644 research/crt-last-k-streaming/VERIFY.json create mode 100644 research/crt-last-k-streaming/independent_tail_check.py create mode 100644 research/crt-last-k-streaming/r_one_payload_check.py create mode 100644 research/crt-last-k-streaming/verify.py diff --git a/research/crt-last-k-streaming/INDEPENDENT-REVIEW.md b/research/crt-last-k-streaming/INDEPENDENT-REVIEW.md new file mode 100644 index 0000000000..96499831b8 --- /dev/null +++ b/research/crt-last-k-streaming/INDEPENDENT-REVIEW.md @@ -0,0 +1,131 @@ +# Independent conditional review of the last-K CRT exception + +Reviewed against canonical main `12fa8c5c844be21bfefb38a19503fbd867a11244`, +PR4100 retained source `337d04939571a637aeab54a0f58f54fde811663a`, +`research/unconditional-batched-crt/CRT.md` Sections 2--4, and PR4174 +`5fec853f0c048871de3b8098d1e30d4ee19cda23` reservoir proof/allocator. +I did not read the primary candidate implementation before this verdict. + +## Verdict and exact assumptions + +The elementary tail construction is correct, conditional on (1) a Boolean +control independent of its target and the whole borrowed H-bit suffix; +(2) a uniform sequential evaluator with paid time E(p,ell), including its +required source-coordinate reconstruction; and (3) the stated paid ordinary +interchange at width one. No new source obstruction was found. + +This is more than a finite endpoint check only when accompanied by the +following two-block schedule and quantified tariff. It does not certify the +source's complete E bound, ordinary interchange construction, all CRT branches, +or multiplication theorem. + +## Coordinate convention and dependency transport + +Count physical address positions from the front/MSB, 0,...,L-1. +After PR4174 placement the layout is U,T,Y,B, with |U|=|T|=|B|=H. +The final physical Y bit is t=L-H-1. Its local arithmetic index inside Y +is zero. Source CRT.md's j_i are *arithmetic* Y indices; convert by +physical(j)=L-H-1-j before applying this proof. No reversal is free. + +This lemma applies to **any** target in Y. It does not classify the +source's exceptional set. In particular, arithmetic additions at index j +carry toward larger arithmetic indices, which are nearer Y's physical +front. The source's phrase "last K positions" must not be identified +with the physical-last K positions. A finite caller that runs all of its +targets through this legal elementary branch is not a production +classification of which targets require the exception. + +Let S exchange a target position q in Y with t (S=identity when q=t). +For a placed address z define g(z)=f(S(z)). An input original target bit +has moved to t, so g omits t. A possible dependency on the old last Y bit +has moved to q, which precedes t. The exchange touches no suffix position, +so g still omits B. All its dependencies therefore lie in the preceding +prefix P. If f also omits U,T, this remains true after the exchange. + +For q=t, skip both exchanges rather than invoke an equal-position primitive. +For multiple tail targets, restore S before the next target. Even if t is +another active target, the unchanged coordinate interpretation is thus +preserved. The CRT layer's controls omit every active target, so earlier +completed switches also leave pending controls invariant. + +## Explicit sequential two-block schedule + +For each complete prefix P, lexicographic source order is + + (P,0,B=0..2^H-1), (P,1,B=0..2^H-1). + +Evaluate g(P) once, using arbitrary fixed values for omitted t,B. Save its +single Boolean result. There are exactly N=2^(L-H-1) such evaluations. +Each target slice has A=2^H R payload bits, including arbitrary dirty data. + +On a fixed temporary tape, stream the first slice into a single A-bit +buffer. If g=0, rewind/copy it to owned output, then stream the second +slice there. If g=1, stream the second slice first, then rewind/copy the +buffer. Both cases preserve the order within a slice. Return to and erase +the same temporary interval after every prefix. The source head always +moves monotonically apart from its final return; the work and output +heads each make a fixed number of complete sweeps. No per-prefix tape is +allocated and no record addressing is needed. + +Thus the middle stage has exact endpoint t XOR=g(P), keeps B and every +other coordinate, and costs O(V+N(E+L^2)), allowing ample polynomial +coordinate/counter work. Its one-block buffer is 2^H R bits. Owned output, +preserved borrowed input, evaluator scratch and fixed work roles consume +O(V+E+L^2) visited space. Clearing and head returns are included. Paid S +and inverse S add at most two O(V) width-one calls, with O(V) space each. + +Conjugating gives S T_g S = T_f. Since f omits q, T_f is an involution, +so the inverse uses the same construction and restores every dirty address. + +## Conditional amortization + +For R>=1, H>=G=64(ell+ceil(log2(p+2))) and + + E <= C 2^(4ell) (p+2)^16, + +we have + + N E / V = E/(2^(H+1)R) + <= (C/(2R)) 2^(-60ell) (p+2)^(-48). + +The L^2 term is similarly absorbed under the actual L=O(p) caller. +There is no bad-density premise: every prefix owns its complete suffix. +Evaluating per record would instead cost (V/R)E and would invalidate this +invoice. At most K tail targets therefore cost O(VK), using constants +independent of p,ell and control truth tables. E remains a separately +unverified hypothesis in this review. + +PR4174 supplies the dependency-safe H suffix and coordinate descriptor; +its allocator alone does not prove the evaluator-time hypothesis. The +elementary branch does not require guard-good states or sparse-hole repair. + +## Independent finite evidence + +`independent_tail_check.py` uses explicit payload labels at every address, +then independently compares direct target flips to conjugation plus +adjacent two-block output. It covers every Boolean function of every +non-target Y bit for Y widths 1--4, suffix widths 1--2 and all targets. +All U,T,B coordinates are arbitrary dirty address coordinates. + +Ordinary replay passed 2,164 function/layout cases, 1,209,888 complete +address columns, 168,040 prepared complete fibers and 556 already-last-Y +cases. Inverse composition returns all labels. Omitting control conjugation +is detected, with first witness L=5,H=1,Ywidth=2,q=2,table=1: output +position 2 contains label 6 instead of 2. + +This Python checker uses host arrays and is a finite semantic oracle, +not an implementation of the fixed-tape machine or a timing proof. + +## Credit and remaining obligations + +Cinna Davis supplies the audited CRT tail idea and bound; Hiroki KUMAZAKI +supplies PR4174's constructive placement. Vlado Vojdanovski, Jose Manuel +and the retained compact/routing lineage retain their source credit. +This review was prepared by OpenAI Codex as a separate agent. It is not +independent human review or a formal-kernel proof. No new kappa is claimed. + +Next: authenticate the actual complete control evaluator with its +reconstruction/erasure/head returns inside E; independently establish the +ordinary width-one callee contract; then compose this branch with the raw +compact macro, full repair and complete CRT tariff. The selected frontier +is unchanged. diff --git a/research/crt-last-k-streaming/NOTICE.md b/research/crt-last-k-streaming/NOTICE.md new file mode 100644 index 0000000000..b4c3c61d15 --- /dev/null +++ b/research/crt-last-k-streaming/NOTICE.md @@ -0,0 +1,7 @@ +# Attribution and license + +New proof, verifier, independent oracle and packaging: ToikY, with substantial OpenAI Codex assistance. Apache-2.0. Separate-agent review is not independent human review. + +The elementary bit exchange, transformed control and complete-suffix amortization are Cinna Davis’s PR4100 construction. The retained three input files remain unchanged, including `research/unconditional-batched-crt/NOTICE.md` with its complete predecessor attribution. Hiroki KUMAZAKI (@kumagi), PR4174, supplies the reservoir/split-coordinate context; PR4169’s repair is complementary and not imported. + +INDEPENDENT-REVIEW.md, REPORT.json, PRIMARY-REVIEW.json and R-ONE-PAYLOAD.json are separate-agent receipts with local interpreter/temporary-directory paths replaced by portable labels for publication. Original receipts remain local; algorithm hashes and mathematical outputs are unchanged. The registered replay commands use this package’s copies. Source hashes in those receipts identify the reviewed algorithm bytes. diff --git a/research/crt-last-k-streaming/PRIMARY-REVIEW.json b/research/crt-last-k-streaming/PRIMARY-REVIEW.json new file mode 100644 index 0000000000..4cf1365082 --- /dev/null +++ b/research/crt-last-k-streaming/PRIMARY-REVIEW.json @@ -0,0 +1,94 @@ +{ + "additional_one_bit_payload_control": { + "command": [ + "python3.12", + "-I", + "-O", + "-W", + "error", + "-B", + "research/crt-last-k-streaming/r_one_payload_check.py", + "research/crt-last-k-streaming/verify.py" + ], + "exit_code": 0, + "receipt": { + "case_count": 15016, + "lengths": [ + 1, + 2, + 3 + ], + "primary_sha256": "623bde19c1b0ad08b9a0dcfb54c1cd849e5b4a3e697dd385541d578ad7bc6ec2", + "record_bits": 1, + "record_columns": 119440, + "scope": "every binary payload pattern and permitted Boolean control on complete small rectangles; tags are not charged as one bit", + "status": "PASS_R_ONE_PAYLOAD_CONTROL" + }, + "script_sha256": "87595c0dc14b274e7551dd730c8c135820e00e955bc921957fc23c940eb1b2b0" + }, + "independent_oracle_before_primary_read": "research/crt-last-k-streaming/REPORT.json", + "limitations": [ + "separate agents are not independent human review", + "no complete numerical E evaluator, ordinary callee or full CRT theorem certified" + ], + "resolved_findings": [ + "separate middle-stage scratch from total space with callee and owned intermediates", + "j=k has no intermediate cleanup; preserve original and final owned output", + "arbitrary-R log record-width overhead separately bounded by V" + ], + "reviewed_hashes": { + "PROOF.md": "1731ebe15893d48e9bcda003c74d31e354b86ae5d0c8ae7641e1a19054c84abd", + "README.md": "7b120762e00fd1b2a820ada45ec86e5fd1194faf2e05cae9978995bc95e94ff4", + "RESULT.json": "a1c2ed47e56746585b552a611084b1babefc4cb38868f4feb0f9759a8a922f25", + "SOURCE-PINS.json": "e9446850818c8377dfcfbffbd822cbd74b6d5f8edb89334767a6d2a75c469e7d", + "verify.py": "623bde19c1b0ad08b9a0dcfb54c1cd849e5b4a3e697dd385541d578ad7bc6ec2" + }, + "runs": [ + { + "command": [ + "python3.12", + "-I", + "-B", + "research/crt-last-k-streaming/verify.py" + ], + "exit_code": 0, + "stderr": "", + "stdout": { + "actual_caller_dirty_addresses": 4096, + "all_functions": 4328, + "dirty_addresses": 252060, + "result": "PASS_CONDITIONAL_CRT_LAST_K_STREAMING" + } + }, + { + "command": [ + "python3.12", + "-I", + "-O", + "-W", + "error", + "-B", + "research/crt-last-k-streaming/verify.py" + ], + "exit_code": 0, + "stderr": "", + "stdout": { + "actual_caller_dirty_addresses": 4096, + "all_functions": 4328, + "dirty_addresses": 252060, + "result": "PASS_CONDITIONAL_CRT_LAST_K_STREAMING" + } + } + ], + "scope_checks": [ + "physical q=L-H-1-j_Y convention; anytarget lemma does not select production exceptional set", + "13V exact middle-stage payload-only actions, excludes evaluator/counters/markers/Q/owned-intermediate erasure", + "unique payload tags encoded in R=L bits; oversized payloads rejected", + "actual root offset2=(15*7)^-1 mod11; exact pinned Bene\u0161 source tables and invalid padding included", + "source unchanged; E and ordinary callee remain explicit hypotheses", + "finite L=12,H=3 fixture is source control projection with suffix-only placement, not full production three-reservoir Y=[6,9) layout or PR4174 allocator; target positions0..3 are legal for generic q=1` bits in **physical MSB-first positions** +`0,...,L-1`. Every one of the `M=2^L` addresses has an arbitrary `R>=1`-bit +payload. Let `V=MR`. Let `0<=H x XOR ( f(x) * 2^(L-1-j) ). (1) +``` + +Omission of the target makes this an involution. Suffix omission is a +separate condition used for preparation reuse. There is no initialized +address coordinate and no valid-address-only premise. + +Write `k=L-H-1` for the last position before the suffix. The ordinary +callee is assumed to exchange physical address positions `j,k`, with +all other address coordinates preserved, in time at most `T_X(V)` using +a fixed inventory of tapes and at most `S_X(V)` visited workspace cells. +Denote that coordinate involution by `Q`. +The callee preserves its input, returns an owned output stream, and +satisfies its declared workspace/head-return contract within this tariff. +If `j=k`, it is the identity and no call is needed. This is a paid +**width-one** exchange, not a reversal or a width-H exchange. + +After this exchange write the address as `a|b|r`, where `a` has `k` bits, +`b` is at position `k`, and `r` has `H` bits. Define + +``` +g(a) = f( Q(a|0|0^H) ). (2) +``` + +For every `b,r`, `f(Q(a|b|r))=g(a)`: varying `b` varies the original +target, and varying `r` varies only the omitted suffix. All dependencies +of the transformed function now occur before `b`. + +Assume `g(a)` can be prepared on a fixed inventory of sequential work +tapes in at most `E_*` steps per `a`, **including** descriptor decoding, +workspace clearing and head returns. Its scratch length is at most +`E_*`, as follows for a sequential computation starting with blank +work tapes. More generally use any separately proved scratch bound +`S_*`; none of the endpoint argument requires a unit-cost evaluator. +This must be one **uniform encoded evaluator**, including the cost of +reading supplied control/descriptor parameters. There is no family of +size-specific compiled advice strings or uncharged oracle in E_*. + +The proposition is a sequential implementation of (1) with + +``` +F = 2^(L-H-1) = M / 2^(H+1) preparations, +T <= 2 T_X(V) + O(V + F(E_* + L + log(R+1))), (3) +middle-stage extra scratch + <= 2^(H+1) R + O(E_* + L + log(R+1)), (4) +total visited space + = O(V + S_X(V) + E_* + L + log(R+1)). (5) +``` + +on a number of tapes independent of `L,H,R` and of the number of +targets. The usual coefficient in `O` is fixed once the component +machines and encodings are fixed. No observed Python timing supplies it. +Equation (4) excludes the input/output streams and the ordinary callee's +workspace; it is not the complete construction's scratch bound. + +## 2. Literal sequential schedule + +Use four payload tapes: input, output, and two reusable staging tapes +`Z,O`. Their left markers are fixed. All evaluator and counter tapes +come from fixed inventories; loops do not allocate new tapes. + +Call `Q` first. Enumerate prefixes `a` in binary order. Each prefix +occurs on the payload tape as exactly two consecutive slices + +``` +[ a|0|r, r=0,...,2^H-1 ] [ a|1|r, r=0,...,2^H-1 ]. +``` + +For each prefix: + +1. Prepare and retain the single bit `g(a)`. +2. Read the first complete slice sequentially onto `Z` and return its + head. Read the second complete slice onto `O` and return its head. + Each slice has `S=2^H R` payload bits. +3. If `g(a)=0`, sequentially append `Z` and then `O` to output. If + `g(a)=1`, append `O` and then `Z`. Preserve order **inside** each + slice. Erase each staging cell as it is read and return both heads + to their left markers. There is no seek to an individual record. +4. Clear the control workspace, return its heads, and advance the + prefix counter. The two staging tapes are now reusable. + +Finally return the input and output heads, and apply `Q` again to +the output. This needs at most two width-one ordinary exchanges in +total, regardless of the distance between the exchanged coordinates. + +For j!=k, the first Q preserves the original source and owns an intermediate A. +The middle procedure preserves A while producing intermediate B. The +last Q preserves B and returns the final owned output. Then erase and +return the two private V-bit intermediate regions A,B by linear scans. +The original source and final owned output remain. These extra scans +cost O(V) in (3); they are outside the middle-stage 13V invoice below. +For j=k, skip both Q calls and run the middle procedure directly from +the preserved original source into the final owned output. There are +then no A/B intermediate regions to erase; in particular, neither the +original source nor the final output is cleared as an intermediate. + +At a prefix with `g(a)=1`, the record originally at `a|b|r` appears at +`a|(b XOR 1)|r`, with exactly the same `a,r` and payload. At a prefix +with `g(a)=0`, it stays at the same address. Thus the middle procedure +is the transformed switch, and conjugation by `Q` gives (1). +This argument covers arbitrary dirty payloads and arbitrary dirty +suffix coordinate values; it does not assume zero padding. The inverse +uses the same procedure, since each switch is an involution. + +## 3. Complete tariff and fixed workspace + +For clarity, count read, write and one-cell head move separately on +the four payload tapes. For each input payload bit, staging uses a +read and right move on input, a write and right move on its staging +tape, and one left move during return: **5** actions. Draining uses +a read, erase and right move on staging, a write and right move on +output, and one left move during return: **6** actions. Returning +the full input and output adds **2** actions per bit. Therefore the +middle-stage payload-bit portion is exactly **13V** actions in this model. +Markers, finite-state branching and counters add `O(V+F(L+log(R+1)))`; +they are excluded from that exact coefficient. The Python tape model +checks the payload-bit invoice only. + +There is no L-bit address test or evaluator call at each record. +To find slice ends, use the same H-bit suffix counter and R-bit-record +boundary encoding for all prefixes. A binary counter kept with its +least significant end at the return marker has total carry traversal +`O(2^H+H)` across a complete suffix enumeration: each position is +visited only when the lower positions carry. Repeating the bounded +number of staging/draining passes keeps this linear. An analogous +counter through each R-bit record costs `O(R+log(R+1))=O(R)` per +record. Initialization and prefix preparation cost at most the +additive per-prefix term in (3). Counter and evaluator tape heads +return to fixed markers; end markers need only constant extra cells +per staging tape. + +There are exactly F preparations, not M preparations. Clearing and +head returns are included in E_*, so all preparation work costs +`F E_*`. Input/output each occupy V bits and are roles of the payload +stream. The middle stage's extra payload scratch is at most the two slices, `2S`. +The evaluator's scratch is reusable across all prefixes, and no tape +is allocated per prefix, per source axis or per exceptional target. +The union of the fixed ordinary-callee, evaluator and staging/counter +inventories remains fixed. + +The input and owned output/intermediate streams occupy a constant +number of V-bit regions. They may be kept while the next Q callee +runs, so (5) also includes its visited workspace. A sequential callee +with blank work tapes visits at most O(T_X(V)) new cells; the actual +O(V)-time callee premise therefore gives S_X(V)=O(V). + +This proves (3)--(5) without assuming a random-access payload +operation. The verifier's direct array implementation of `Q` is +**only an endpoint oracle for the assumed ordinary callee**. It is +not included in the sequential payload invoice. + +## 4. Application to the placed CRT caller + +PR4100 Section 3 and Hiroki KUMAZAKI's PR4174 give the reservoir +placement context. We use its support/coordinate conclusion as an +explicit hypothesis, rather than importing or rechecking its entire +allocator: after the paid placement `P`, every relevant control omits +the complete back H-bit field, and its target lies in the middle Y +field. Retain `f_P(z)=f_original(P^-1(z))`. If a logical source axis +was split by placement, reconstruct it from its coordinate descriptor; +reading one old contiguous slice is not a valid substitute. + +The last bit of Y is physical position `L-H-1`, exactly k above. A +target specified as the numeric local bit `j_Y` of Y, with Y occupying +`[2H,L-H)`, is at physical position `L-H-1-j_Y`; there is no implicit +physical bit reversal. Equation (2) is then + +``` +g(a) = f_original(P^-1(Q(a|0|0^H))). +``` + +This lowering applies to **any** target in Y. We do not identify the +source's guard-defined exceptional set with the physical last K bits: +arithmetic carries run toward larger numeric bit indices. For the +following tariff it suffices that the independently chosen exceptional +set has at most K targets. Its guard geometry remains predecessor work. + +Each inverse placement is a known fixed set of block swaps, and Q +is one known coordinate swap. A deliberately naive sequential +reconstruction scans the encoded address once per requested original +bit, using `O(L^2)` steps and `O(L)` scratch. Descriptor decoding can +be charged to the same bound. This is polynomial overhead inside +preparation, not an uncharged constant per input record. + +Conditional on PR4100's stated numerical evaluator bound, enlarge +its fixed constant to cover this reconstruction and all preparation +returns/clearing. With `L=Theta(p)` the resulting E_* satisfies + +``` +E_* <= C 2^(4 ell) (p+2)^16, +G = 64(ell + ceil(log2(p+2))), H >= G. +``` + +These are premises, not a new certification of the numerical +algorithm or a derivation from the finite fixture. Exact integer +arithmetic gives + +``` +E_* / 2^H <= C 2^(-60 ell) (p+2)^(-48). +``` + +Consequently `F E_* = M E_*/2^(H+1) = O(M) = O(V)`. +The FL term in (3) is absorbed in E_* after increasing its fixed +constant, using L=Theta(p). Separately, `F log2(R+1)<=MR=V` for all +integer R>=1, so no extra relation between R and p is needed for that +counter term. The assumed width-one ordinary callee costs +`T_X(V)=O(V)`, so each elementary target costs `O(V)`. At most K +such targets cost `O(VK)`, with the same suffix and fixed inventories +reused and with all coordinate values restored except intended +target flips. The actual caller's controls omit all active target +bits, so sequential treatment agrees with its commuting layer. + +This complete-fiber reuse cannot be transferred to the sparse bad +holes: their occupancy need not supply complete suffix slices. +The compact word and its exceptional repair remain separate. + +## 5. Finite corroboration and boundary + +`verify.py` authenticates the three source inputs by SHA256 and Git +blob hash before loading the exact retained CRT control bytes. It +uses explicit checks active under optimized Python. `--write-result` +is an explicit receipt-generation option; normal verification compares +the reproduced result without rewriting it. + +The universal proposition is the written conditional proof above. +The tests corroborate its endpoint, transformed-control convention, +dirty suffix coverage, exact preparation count and payload invoice. +They do not time or implement the assumed E evaluator or ordinary +callee, do not validate the asymptotic reservoir cutoff using a tiny +fixture, and do not certify the complete CRT or multiplication theorem. + +The source-bound root-axis fixture is a **control projection**, using +L=12,H=3 and suffix-only transport of the unused axis-2 bits. It does +not instantiate the full three-reservoir placement or execute PR4174's +allocator. Its targets may lie outside the hypothetical three-field Y +range and are admitted by the general lemma's weaker `q=64(ell+ceil(log2(p+2)))`, and the +ordinary width-one callee's O(V) bound, preparation is amortized over +the complete omitted suffix. Each exception costs O(V), and at most K +exceptions cost O(VK). The new proof includes a conservative O(L²) +coordinate/descriptor reconstruction charge inside preparation. +The evaluator premise is uniform and includes reading supplied encoded +parameters; no size-specific advice or uncharged control oracle is admitted. + +## Evidence + +[verify.py](verify.py) authenticates the exact three predecessor inputs +listed in [SOURCE-PINS.json](SOURCE-PINS.json), compiles the authenticated +caller bytes directly and reproduces [RESULT.json](RESULT.json): + +- Every Boolean function on up to three permitted source bits across + 40 target/suffix layouts: **4,328 cases**, **252,060 dirty-address + endpoints**, each replayed forward and inverse. Suffix widths include + 0 through 3. The exact preparation and payload-only invoices are checked. +- A **source-bound root-axis control projection**, using the retained + CRT Beneš control algorithm for axis 3 with + moduli `(3,5,7,11)`, after moving the unused axis-2 reservoir to the back: + **all 4,096 dirty padded addresses**, **7 layers**, **114,688 target/suffix + omission checks**, exact forward root-axis rotation and full inverse. + Each layer uses **256 preparations**, rather than 4,096 per-record + preparations. This small geometry uses suffix-only transport and is + below the large-family cutoff. It does **not** execute the full + three-reservoir placement/allocator or identify a production tail set; + its targets need only satisfy the general lemma's `q int: + return (value >> (length - 1 - position)) & 1 + + +def exchange(value: int, first: int, second: int, length: int) -> int: + if bit(value, first, length) != bit(value, second, length): + value ^= (1 << (length - 1 - first)) | (1 << (length - 1 - second)) + return value + + +def transport_payload(payload: list[int], first: int, second: int, length: int) -> list[int]: + result = [-1] * len(payload) + for address, label in enumerate(payload): + result[exchange(address, first, second, length)] = label + return result + + +def source_value(address: int, truth_table: int, y_positions: tuple[int, ...], + target: int, length: int) -> int: + key = 0 + for position in y_positions: + if position != target: + key = 2 * key + bit(address, position, length) + return (truth_table >> key) & 1 + + +def direct(payload: list[int], truth_table: int, y_positions: tuple[int, ...], + target: int, length: int) -> list[int]: + result = [-1] * len(payload) + mask = 1 << (length - 1 - target) + for address, label in enumerate(payload): + control = source_value(address, truth_table, y_positions, target, length) + result[address ^ (mask * control)] = label + return result + + +def lowered(payload: list[int], truth_table: int, y_positions: tuple[int, ...], + target: int, length: int, suffix_width: int, + *, omit_conjugation: bool = False) -> tuple[list[int], dict[str, int]]: + last_y = length - suffix_width - 1 + placed = transport_payload(payload, target, last_y, length) + block_size = 1 << suffix_width + output = [] + preparations = 0 + for start in range(0, len(placed), 2 * block_size): + # The evaluator is invoked once for the entire two-block prefix fiber. + # Target and suffix may be replaced by zero because they are omitted. + original = start if omit_conjugation else exchange(start, target, last_y, length) + control = source_value(original, truth_table, y_positions, target, length) + preparations += 1 + first = placed[start:start + block_size] + second = placed[start + block_size:start + 2 * block_size] + if control: + output.extend(second) + output.extend(first) + else: + output.extend(first) + output.extend(second) + restored = transport_payload(output, target, last_y, length) + return restored, {"preparations": preparations, "buffer_records": block_size, + "width_one_exchanges": 0 if target == last_y else 2} + + +def main() -> None: + cases = columns = fibers = 0 + lost_transport_witness = None + last_y_cases = 0 + for suffix_width in (1, 2): + for y_width in range(1, 5): + length = 3 * suffix_width + y_width + positions = tuple(range(2 * suffix_width, length - suffix_width)) + payload = list(range(1 << length)) + for target in positions: + for table in range(1 << (1 << (y_width - 1))): + expected = direct(payload, table, positions, target, length) + actual, stats = lowered(payload, table, positions, target, length, suffix_width) + if actual != expected: + raise RuntimeError("complete dirty-state endpoint mismatch") + if stats["preparations"] != 1 << (length - suffix_width - 1): + raise RuntimeError("preparation was not charged once per complete fiber") + if sorted(actual) != payload: + raise RuntimeError("endpoint is not a full permutation") + if lowered(actual, table, positions, target, length, suffix_width)[0] != payload: + raise RuntimeError("inverse endpoint did not restore complete payload") + cases += 1 + columns += len(payload) + fibers += stats["preparations"] + if target == positions[-1]: + last_y_cases += 1 + if stats["width_one_exchanges"] != 0: + raise RuntimeError("identity last-Y exchange not eliminated") + elif lost_transport_witness is None: + wrong = lowered(payload, table, positions, target, length, suffix_width, + omit_conjugation=True)[0] + if wrong != expected: + index = next(i for i, pair in enumerate(zip(wrong, expected)) + if pair[0] != pair[1]) + lost_transport_witness = { + "length": length, "suffix_width": suffix_width, + "y_width": y_width, "target_physical": target, + "table": table, "output_position": index, + "expected_label": expected[index], "wrong_label": wrong[index], + } + if lost_transport_witness is None: + raise RuntimeError("missing-conjugation negative control was not detected") + print(json.dumps({"status": "PASS", "cases": cases, "columns": columns, + "prepared_complete_fibers": fibers, + "already_last_y_cases": last_y_cases, + "missing_conjugation_control": lost_transport_witness}, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/crt-last-k-streaming/r_one_payload_check.py b/research/crt-last-k-streaming/r_one_payload_check.py new file mode 100644 index 0000000000..d66fe5ed3e --- /dev/null +++ b/research/crt-last-k-streaming/r_one_payload_check.py @@ -0,0 +1,49 @@ +"""Independent follow-up control: true one-bit payloads, not unit-cost tags.""" +import hashlib +import json +from pathlib import Path +import sys +import types + + +def main(): + path = Path(sys.argv[1]) + data = path.read_bytes() + expected = "623bde19c1b0ad08b9a0dcfb54c1cd849e5b4a3e697dd385541d578ad7bc6ec2" + if hashlib.sha256(data).hexdigest() != expected: + raise ValueError("reviewed primary source changed") + module = types.ModuleType("_independently_reviewed_tail_payload") + module.__file__ = str(path) + exec(compile(data, str(path), "exec"), module.__dict__) + cases = columns = 0 + for length in range(1, 4): + for suffix in range(length): + for target in range(length - suffix): + dependencies = [k for k in range(length - suffix) if k != target] + for table in range(1 << (1 << len(dependencies))): + def control(word): + key = 0 + for k in dependencies: + key = 2 * key + ((word >> (length - 1 - k)) & 1) + return (table >> key) & 1 + + for pattern in range(1 << (1 << length)): + payload = [(pattern >> k) & 1 for k in range(1 << length)] + actual, invoice = module.lower_tail( + payload, length, suffix, 1, target, control) + if actual != module.direct_switch(payload, length, target, control): + raise ValueError("R=1 payload endpoint mismatch") + if invoice["payload_cell_head_steps"] != 13 * (1 << length): + raise ValueError("R=1 payload tariff mismatch") + cases += 1 + columns += len(payload) + print(json.dumps({"status": "PASS_R_ONE_PAYLOAD_CONTROL", + "case_count": cases, "record_columns": columns, + "lengths": [1, 2, 3], "record_bits": 1, + "primary_sha256": expected, + "scope": "every binary payload pattern and permitted Boolean control on complete small rectangles; tags are not charged as one bit"}, + sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/crt-last-k-streaming/verify.py b/research/crt-last-k-streaming/verify.py new file mode 100644 index 0000000000..5e62e353e6 --- /dev/null +++ b/research/crt-last-k-streaming/verify.py @@ -0,0 +1,359 @@ +"""Source-bound finite audit of the conditional last-K sequential lowering. + +The ordinary width-one exchange and the cost-bounded control evaluator are +explicit hypotheses, not supplied implementations. Tape is a cell/head model; +the proof, rather than Python timings, gives the quantified machine bound. +""" + +import argparse +import hashlib +import json +from pathlib import Path +import sys +import types + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +class Tape: + """A finite simulation of one sequential tape with one movable head.""" + + def __init__(self, cells=()): + self.cells = list(cells) + self.head = self.steps = self.maximum = 0 + + def read(self, erase=False): + need(self.head < len(self.cells), "read beyond tape contents") + value = self.cells[self.head] + need(value in (0, 1), "reading an erased cell") + self.steps += 2 # Read, then move one cell to the right. + if erase: + self.cells[self.head] = None + self.steps += 1 + self.head += 1 + self.maximum = max(self.maximum, self.head) + return value + + def write(self, value): + need(value in (0, 1), "nonbinary payload") + if self.head == len(self.cells): + self.cells.append(value) + else: + need(self.cells[self.head] is None, "overwriting a live staged bit") + self.cells[self.head] = value + self.steps += 2 # Write, then move one cell to the right. + self.head += 1 + self.maximum = max(self.maximum, self.head) + + def rewind(self): + # This macro expands into precisely head one-cell left moves. + self.steps += self.head + self.head = 0 + + +def stream_slices(bits, length, suffix, record_bits, prepare): + """Lower a|b|r -> a|(b XOR prepare(a))|r using four payload tapes. + + prepare is called ONCE for each complete pair of suffix slices. It is + deliberately not assigned a unit-cost-machine implementation here. + """ + need(isinstance(length, int) and length >= 1, "positive address length") + need(isinstance(suffix, int) and 0 <= suffix < length, "proper suffix") + need(isinstance(record_bits, int) and record_bits >= 1, "positive record width") + need(len(bits) == (1 << length) * record_bits, "complete rectangle required") + incoming, outgoing, zero, one = Tape(bits), Tape(), Tape(), Tape() + width = (1 << suffix) * record_bits + preparations = 0 + for prefix in range(1 << (length - suffix - 1)): + flip = prepare(prefix) + need(flip in (0, 1), "Boolean control") + preparations += 1 + for staged in (zero, one): + for _ in range(width): + staged.write(incoming.read()) + staged.rewind() + for staged in ((one, zero) if flip else (zero, one)): + for _ in range(width): + outgoing.write(staged.read(erase=True)) + staged.rewind() + incoming.rewind() + outgoing.rewind() + need(all(cell is None for staged in (zero, one) for cell in staged.cells), + "staging tapes must be erased and returned") + need(all(t.head == 0 for t in (incoming, outgoing, zero, one)), "payload head returns") + volume = len(bits) + steps = sum(t.steps for t in (incoming, outgoing, zero, one)) + need(steps == 13 * volume, "exact payload-only cell/head invoice") + return outgoing.cells, { + "volume_bits": volume, + "preparations": preparations, + "payload_cell_head_steps": steps, + "maximum_staging_bits": zero.maximum + one.maximum, + "payload_tapes": 4, + } + + +def exchange_address(word, length, a, b): + """MSB physical positions; semantic reference for the assumed callee.""" + different = ((word >> (length - 1 - a)) ^ (word >> (length - 1 - b))) & 1 + return word ^ (different << (length - 1 - a)) ^ (different << (length - 1 - b)) + + +def exchange_payload(records, length, a, b): + # This direct array reference checks the ordinary callee's ENDPOINT ONLY. + # Its random accesses are not part of stream_slices or its tape invoice. + result = [None] * len(records) + for address, record in enumerate(records): + result[exchange_address(address, length, a, b)] = record + return result + + +def lower_tail(records, length, suffix, record_bits, target, control, + transform=True, restore=True): + need(isinstance(record_bits, int) and record_bits >= 1, "positive record width") + need(all(isinstance(record, int) and 0 <= record < (1 << record_bits) + for record in records), "payload fits the declared record width") + need(0 <= target < length - suffix, "target outside omitted suffix") + last = length - suffix - 1 + placed = exchange_payload(records, length, target, last) + serialized = [((record >> bit) & 1) + for record in placed for bit in range(record_bits - 1, -1, -1)] + + def prepare(prefix): + # Both the target and suffix are set to zero. Omission makes their + # choice irrelevant. Reconstruct the pre-exchange control address. + representative = prefix << (suffix + 1) + original = exchange_address(representative, length, target, last) if transform else representative + return control(original) + + output, invoice = stream_slices(serialized, length, suffix, record_bits, prepare) + placed_output = [] + cursor = iter(output) + for _ in records: + record = 0 + for _ in range(record_bits): + record = 2 * record + next(cursor) + placed_output.append(record) + result = exchange_payload(placed_output, length, target, last) if restore else placed_output + invoice["ordinary_width_one_exchanges"] = 2 if target != last else 0 + return result, invoice + + +def direct_switch(records, length, target, control): + result = [None] * len(records) + mask = 1 << (length - 1 - target) + for address, record in enumerate(records): + destination = address ^ (mask if control(address) else 0) + need(result[destination] is None, "control violates switch independence") + result[destination] = record + return result + + +def all_functions(): + configurations = functions = addresses = 0 + digest = hashlib.sha256() + max_payload_ratio = 0 + for prefix_bits in range(4): + for suffix in range(4): + length = prefix_bits + suffix + 1 + records = list(range(1 << length)) + for target in range(length - suffix): + dependencies = [v for v in range(length - suffix) if v != target] + configurations += 1 + for table in range(1 << (1 << prefix_bits)): + def control(word): + key = 0 + for position in dependencies: + key = 2 * key + ((word >> (length - 1 - position)) & 1) + return (table >> key) & 1 + + result, invoice = lower_tail(records, length, suffix, length, target, control) + expected = direct_switch(records, length, target, control) + need(result == expected, "all Boolean functions/all dirty addresses") + recovered, repeated = lower_tail(result, length, suffix, length, target, control) + need(recovered == records, "all-function involution") + need(invoice == repeated, "payload-independent invoice") + need(invoice["preparations"] == 1 << prefix_bits, "one preparation per complete pair") + need(invoice["maximum_staging_bits"] == 2 * (1 << suffix) * length, + "two reusable complete slices") + max_payload_ratio = max(max_payload_ratio, + invoice["payload_cell_head_steps"] // invoice["volume_bits"]) + digest.update(bytes(result)) + functions += 1 + addresses += len(records) + return {"configurations": configurations, "functions": functions, + "dirty_address_checks": addresses, "forward_and_inverse_runs": 2 * functions, + "maximum_payload_step_ratio": max_payload_ratio, + "endpoint_sha256": digest.hexdigest()} + + +def caller_fixture(crt): + """Source-bound root-axis control projection, NOT full placed CRT.""" + # Original axes are physically 3,2,1,0. Logical widths (2,3,3,4). + # Exchange the unused root-right axis 2, positions [4,7), with the final + # three bits. This transports controls and can split their source axes. + # It is suffix-only transport, not the three-reservoir production placement. + length, suffix, record_bits = 12, 3, 12 + + def placement(word): + for a, b in ((4, 9), (5, 10), (6, 11)): + word = exchange_address(word, length, a, b) + return word + + networks = {c: crt.benes(crt.rotation(16, 11, c)) for c in range(11)} + need({tuple(bit for bit, table in net) for net in networks.values()} == {(0, 1, 2, 3, 2, 1, 0)}, + "actual root-axis common Beneš schedule") + + def values(word): + return word & 3, (word >> 2) & 7, (word >> 5) & 7, (word >> 8) & 15 + + def offset(word): + a0, a1, _, _ = values(word) + return (2 * crt.decode_group((a0, a1), (3, 5))) % 11 if a0 < 3 and a1 < 5 else 0 + + controls = [] + for layer in range(7): + def control(placed, layer=layer): + original = placement(placed) + return networks[offset(original)][layer][1][values(original)[3]] + controls.append(control) + + records = exchange_payload(list(range(1 << length)), length, 4, 9) + records = exchange_payload(records, length, 5, 10) + records = exchange_payload(records, length, 6, 11) + invoices = [] + omissions = 0 + for layer, control in enumerate(controls): + bit = networks[0][layer][0] + target = 3 - bit + for address in range(1 << length): + for position in (target, 9, 10, 11): + need(control(address) == control(address ^ (1 << (11 - position))), + "actual transported CRT control omits target and suffix") + omissions += 1 + expected = direct_switch(records, length, target, control) + records, invoice = lower_tail(records, length, suffix, record_bits, target, control) + need(records == expected, "actual CRT layer streaming endpoint") + invoices.append(invoice) + records = exchange_payload(records, length, 6, 11) + records = exchange_payload(records, length, 5, 10) + records = exchange_payload(records, length, 4, 9) + for source in range(1 << length): + target_value = values(source)[3] + target_value = ((target_value + offset(source)) % 11 if target_value < 11 else target_value) + destination = (source & 255) | (target_value << 8) + need(records[destination] == source, "all padded/dirty root-axis rotation payloads") + forward_placed = [None] * (1 << length) + for source, record in enumerate(records): + forward_placed[placement(source)] = record + for layer in reversed(range(7)): + target = 3 - networks[0][layer][0] + forward_placed, _ = lower_tail(forward_placed, length, suffix, record_bits, target, controls[layer]) + need(all(forward_placed[placement(address)] == address for address in range(1 << length)), + "full actual CRT inverse with dirty reservoir") + return {"domain": "source-bound root-axis control projection with suffix-only transport; not full three-reservoir placement or a production tail instance", + "moduli": [3, 5, 7, 11], "logical_widths": [2, 3, 3, 4], + "address_bits": length, "suffix_bits": suffix, "root_target_axis": 3, + "layers": 7, "dirty_addresses": 1 << length, + "target_and_suffix_omission_checks": omissions, + "preparations_per_layer": [i["preparations"] for i in invoices], + "payload_steps_per_layer": [i["payload_cell_head_steps"] for i in invoices], + "payload_permutation_sha256": hashlib.sha256( + b"".join(record.to_bytes(2, "big") for record in records)).hexdigest()} + + +def controls_and_tariff(): + length, suffix, target = 5, 1, 0 + records = list(range(1 << length)) + control = lambda word: (word >> 1) & 1 # Old final-Y bit moves to the old target. + expected = direct_switch(records, length, target, control) + stale, _ = lower_tail(records, length, suffix, length, target, control, transform=False) + unrestored, _ = lower_tail(records, length, suffix, length, target, control, restore=False) + need(stale != expected, "stale control transform mutant detected") + need(unrestored != expected, "omitted inverse exchange mutant detected") + dependent = lambda word: word & 1 + wrong, _ = lower_tail(records, length, suffix, length, target, dependent) + need(wrong != direct_switch(records, length, target, dependent), "suffix-dependence mutant detected") + rejected = [] + for label, call in [ + ("incomplete dirty suffix rectangle", lambda: stream_slices([0] * 31, 5, 1, 1, lambda a: 0)), + ("target inside suffix", lambda: lower_tail(records, 5, 1, 5, 4, control)), + ("non-Boolean preparation", lambda: stream_slices([0] * 32, 5, 1, 1, lambda a: 2)), + ("payload exceeds declared width", lambda: lower_tail([0, 2], 1, 0, 1, 0, lambda a: 0)), + ]: + try: + call() + except ValueError: + rejected.append(label) + else: + raise ValueError("negative control accepted: " + label) + # Exact arithmetic: C=1 coefficient is illustrative. The symbolic bound in + # PROOF.md retains arbitrary fixed C and does not infer it from examples. + tariffs = [] + for p, ell in ((2, 2), (63, 7), (1022, 10), (9240576, 24)): + logarithm = (p + 1).bit_length() # ceil(log2(p+2)) + g = 64 * (ell + logarithm) + e = (1 << (4 * ell)) * (p + 2) ** 16 + need(e * (1 << (60 * ell)) * (p + 2) ** 48 <= 1 << g, + "exact E/2^G inequality, no floating logarithm") + tariffs.append({"p": p, "ell": ell, "G": g, "H": g, + "E_coefficient_one_bits": e.bit_length(), + "one_preparation_per_records": 1 << (g + 1)}) + # Re-evaluating per record has M calls instead of M/2^(H+1); endpoint + # tests alone would miss this exact tariff regression. + _, invoice = lower_tail(records, length, suffix, length, target, control) + need(invoice["preparations"] == 8 and len(records) == 32, + "per-record preparation tariff mutant detected") + return {"semantic_mutants_detected": ["stale transformed control", "missing inverse exchange", + "control depends on supposedly omitted suffix"], + "admission_rejections": rejected, + "tariff_mutants_detected": ["E preparation repeated per record"], + "exact_integer_tariffs": tariffs} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", action="store_true") + args = parser.parse_args() + pins = json.loads((PACKAGE / "SOURCE-PINS.json").read_text()) + authenticated = {} + for row in pins: + data = (ROOT / row["path"]).read_bytes() + need(hashlib.sha256(data).hexdigest() == row["sha256"], "source SHA256: " + row["path"]) + need(hashlib.sha1(f"blob {len(data)}\0".encode() + data).hexdigest() == row["git_blob"], + "source Git blob: " + row["path"]) + authenticated[row["path"]] = data + path = "research/unconditional-batched-crt/check_batched_crt.py" + module = types.ModuleType("_authenticated_crt_tail_caller") + module.__file__ = str(ROOT / path) + sys.modules[module.__name__] = module + exec(compile(authenticated[path], module.__file__, "exec"), module.__dict__) + result = {"schema_version": 1, "result": "PASS_CONDITIONAL_CRT_LAST_K_STREAMING", + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "source_inputs_checked": len(authenticated), "all_functions": all_functions(), + "actual_crt_caller": caller_fixture(module), "negative_controls": controls_and_tariff(), + "limitations": ["Universal cost follows from the conditional written proof, not timing.", + "Ordinary width-one callee is a semantic hypothesis, not implemented.", + "Control evaluator and its E bound are hypotheses, not certified.", + "No full CRT, compact repair, multiplication theorem or new kappa."]} + output = PACKAGE / "RESULT.json" + if args.write_result: + output.write_text(json.dumps(result, indent=2) + "\n") + else: + need(json.loads(output.read_text()) == result, "stored result differs from replay") + print(json.dumps({"result": result["result"], + "all_functions": result["all_functions"]["functions"], + "dirty_addresses": result["all_functions"]["dirty_address_checks"], + "actual_caller_dirty_addresses": result["actual_crt_caller"]["dirty_addresses"]}, + sort_keys=True)) + + +if __name__ == "__main__": + main()