From a2f3ce7358e8103f6eccd404e594276e9ccc04d8 Mon Sep 17 00:00:00 2001 From: CubeJerry <80299683+CubeJerry@users.noreply.github.com> Date: Mon, 9 Nov 2026 00:44:54 +0800 Subject: [PATCH 1/3] research: construct a source-bound shrinking Gaussian halo consumer Execute local normalized tensor recovery from original rational reference band entries with a fixed reusable tape pool, complete movement and setup costs, error bounds, and independent original-matrix inverse checks. Prepared for @CubeJerry with substantial OpenAI Codex assistance. No new kappa; this commit is a component of the joined halo contribution. --- .../shrinking-reference-halo/OVERLAP.json | 292 ++ research/shrinking-reference-halo/PROOF.md | 578 +++ research/shrinking-reference-halo/README.md | 198 + research/shrinking-reference-halo/RESULT.json | 3662 +++++++++++++++++ .../shrinking-reference-halo/SOURCES.json | 72 + research/shrinking-reference-halo/TASK.json | 89 + research/shrinking-reference-halo/VERIFY.json | 82 + research/shrinking-reference-halo/engine.py | 385 ++ .../independent_inverse.py | 147 + .../independent_residual.py | 91 + research/shrinking-reference-halo/source.py | 114 + research/shrinking-reference-halo/tensor.py | 343 ++ research/shrinking-reference-halo/verify.py | 554 +++ 13 files changed, 6607 insertions(+) create mode 100644 research/shrinking-reference-halo/OVERLAP.json create mode 100644 research/shrinking-reference-halo/PROOF.md create mode 100644 research/shrinking-reference-halo/README.md create mode 100644 research/shrinking-reference-halo/RESULT.json create mode 100644 research/shrinking-reference-halo/SOURCES.json create mode 100644 research/shrinking-reference-halo/TASK.json create mode 100644 research/shrinking-reference-halo/VERIFY.json create mode 100644 research/shrinking-reference-halo/engine.py create mode 100644 research/shrinking-reference-halo/independent_inverse.py create mode 100644 research/shrinking-reference-halo/independent_residual.py create mode 100644 research/shrinking-reference-halo/source.py create mode 100644 research/shrinking-reference-halo/tensor.py create mode 100644 research/shrinking-reference-halo/verify.py diff --git a/research/shrinking-reference-halo/OVERLAP.json b/research/shrinking-reference-halo/OVERLAP.json new file mode 100644 index 0000000000..aabbd93b28 --- /dev/null +++ b/research/shrinking-reference-halo/OVERLAP.json @@ -0,0 +1,292 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "checked_utc": "2026-11-08 16:11:04 UTC", + "scope": "Original-reference band production and sequential shrinking-domain local tensor consumer; direct degree specialization, generic Horner stability, whole-period host service and outer recovery joins excluded.", + "queries": [ + { + "query": "\"shrinking\" \"halo\"", + "topn": 30, + "results": [] + }, + { + "query": "\"Horner\" \"halo\"", + "topn": 30, + "results": [] + }, + { + "query": "\"periodic\" \"inverse\" \"tape\"", + "topn": 30, + "results": [ + { + "number": 6788, + "title": "Prove the sharp inverse envelope under a column cap (no κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6788" + }, + { + "number": 6542, + "title": "Realize the sparse correction as a reversible nearest-grid map", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6542" + }, + { + "number": 6438, + "title": "Construct optimal unbiased reversible phase rounding (no κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6438" + }, + { + "number": 6426, + "title": "Prove necessary square-root degree growth for cyclic inverses (no κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6426" + }, + { + "number": 6072, + "title": "Joint denominator-13 decisions need fewer expected fair bits than separate calls", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6072" + }, + { + "number": 5859, + "title": "Prove the sharp inverse envelope with forbidden diagonals (no new κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5859" + }, + { + "number": 5260, + "title": "Replace 119 periodic inverse updates with a certified direct solve", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5260" + }, + { + "number": 5255, + "title": "Prove the sharp graph-support inverse norm envelope", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5255" + }, + { + "number": 5284, + "title": "Prove variable-gap precision and linear storage for cyclic band solves", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5284" + }, + { + "number": 5207, + "title": "Prove exact real Gaussian Schur fill signs for t <= 1/3 (no new κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5207" + }, + { + "number": 5216, + "title": "Prove weighted periodic Gaussian power bound and reduce complete inverse to120 terms", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5216" + }, + { + "number": 5159, + "title": "Complete the same-reference periodic rounded inverse service", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5159" + }, + { + "number": 4959, + "title": "Prove routing and Fourier component results with exact checks", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4959" + }, + { + "number": 4870, + "title": "Audit source-driven Gaussian halo copy enumeration (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4870" + }, + { + "number": 4217, + "title": "Audit #4100's HALO locality witness: exact error identity and sharp (2J-1)W radius (no new κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4217" + }, + { + "number": 1038, + "title": "Construction: reversible quadratic phases for the dirty stride solver (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1038" + }, + { + "number": 2313, + "title": "Research: execute certified Gaussian resampling through exact integer recovery", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2313" + }, + { + "number": 486, + "title": "Build binary compression halo boxes with fused streaming and sparse repair", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/486" + }, + { + "number": 929, + "title": "Research: four grouped cyclic inverse calls with one dirty connector (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/929" + } + ] + } + ], + "verified_pr_metadata": [ + { + "number": 1430, + "title": "Audit: quadratic rounding accumulation and linear-error Neumann evaluation (no new kappa)", + "state": "closed", + "merged": true, + "head": "1655c721a1c2aa92f584523afc93a192137cf910", + "base": "410026dc5513b87db92ae98571d1d5984c69a983", + "user": "bbMisk", + "updated_at": "2026-10-14T06:48:19Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1430" + }, + { + "number": 3851, + "title": "Implement normalized Gaussian compression cores on fixed tapes", + "state": "closed", + "merged": true, + "head": "7ab67b4a84d28cd562b9711aa315ca5b47822b37", + "base": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "user": "jmbarrancoml", + "updated_at": "2026-10-20T05:22:44Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3851" + }, + { + "number": 4100, + "title": "Propose unconditional κ = 0.00173097911567079247276057 via batched CRT", + "state": "closed", + "merged": true, + "head": "337d04939571a637aeab54a0f58f54fde811663a", + "base": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "user": "1337isnot1337", + "updated_at": "2026-10-20T11:36:03Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4100" + }, + { + "number": 4205, + "title": "Execute rounded Gaussian words against shared finite-core references", + "state": "closed", + "merged": true, + "head": "78c72e563173f3822fcb4efed9ceeccf05630258", + "base": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "user": "jmbarrancoml", + "updated_at": "2026-10-21T19:22:10Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4205" + }, + { + "number": 4253, + "title": "Lower rational FFT and conditioned Toeplitz programs to fixed Hadamard stages", + "state": "closed", + "merged": true, + "head": "ac14c1409c261d64d9856a5a473d8b7f2be8c302", + "base": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "user": "jmbarrancoml", + "updated_at": "2026-10-21T19:24:13Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4253" + }, + { + "number": 4415, + "title": "Answer #4371's open question 1: one coefficient's error path through #4100's transforms carries one factor of T (m = 1), so C = 5 suffices for b >= 13 (no new κ)", + "state": "closed", + "merged": true, + "head": "ebfa9588f5a1ca4c595b3ff837f24917d5dd7caf", + "base": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "user": "pinterbanget", + "updated_at": "2026-10-21T19:27:52Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4415" + }, + { + "number": 4870, + "title": "Audit source-driven Gaussian halo copy enumeration (no new kappa)", + "state": "closed", + "merged": true, + "head": "43a87adb92a25da168073280b206e15b70fbe42c", + "base": "624de9dc66858af0945e5f8a0942488d62280d43", + "user": "codyw912", + "updated_at": "2026-10-23T01:45:56Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4870" + }, + { + "number": 5159, + "title": "Complete the same-reference periodic rounded inverse service", + "state": "closed", + "merged": true, + "head": "ba435a39f69436f2f7ce5cc02f18879c8d8790f5", + "base": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "user": "JoyboyBrian", + "updated_at": "2026-10-23T11:56:46Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5159" + }, + { + "number": 5216, + "title": "Prove weighted periodic Gaussian power bound and reduce complete inverse to120 terms", + "state": "closed", + "merged": true, + "head": "1ea9efdc1d1d36757a5491bf7fdaa93597dcea67", + "base": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "user": "JoyboyBrian", + "updated_at": "2026-10-23T13:09:35Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5216" + }, + { + "number": 5260, + "title": "Replace 119 periodic inverse updates with a certified direct solve", + "state": "closed", + "merged": true, + "head": "65cdd6b36e002ce9d13bd96dbc504da90f77f2c9", + "base": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "user": "aliromman", + "updated_at": "2026-10-23T18:37:53Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5260" + }, + { + "number": 5284, + "title": "Prove variable-gap precision and linear storage for cyclic band solves", + "state": "closed", + "merged": true, + "head": "72269696a9c5ae5b1c0b469afdd3db08080635cf", + "base": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "user": "aliromman", + "updated_at": "2026-10-23T18:37:53Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5284" + }, + { + "number": 5325, + "title": "Join Tensor error bounds through compression and final restoration", + "state": "closed", + "merged": true, + "head": "bea42af24ee9850949a4b48d329a7dc85de72b11", + "base": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "user": "aliromman", + "updated_at": "2026-10-23T18:37:52Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5325" + }, + { + "number": 5986, + "title": "Reduce Gaussian inverse locality degree from p^42 to p^22 (no new κ)", + "state": "closed", + "merged": true, + "head": "31bbc7b22ea697437660a0af4c006e114b90710b", + "base": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "user": "petalas", + "updated_at": "2026-10-28T00:24:32Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5986" + }, + { + "number": 6490, + "title": "Reduce Horner oracle precision volume with increasing grids (no κ)", + "state": "open", + "merged": false, + "head": "4307d3a0cb8921b58ec2f229fdad41db25849932", + "base": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "user": "petalas", + "updated_at": "2026-11-03T01:01:48Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6490" + }, + { + "number": 6880, + "title": "Prove a rounded finite-core and sparse-halo composition bound (no new κ)", + "state": "open", + "merged": false, + "head": "e212af981b49c299de515f8c23dfb0e5b73e2e95", + "base": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "user": "CubeJerry", + "updated_at": "2026-11-08T15:01:00Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6880" + } + ], + "coverage_limits": [ + "Focused live title/body queries and cited predecessor source packages; not all historical diffs or unpublished work.", + "Search results omit status fields; cited status/head metadata were separately fetched by PR endpoint.", + "Lead surveyed canonical research-directory metadata and broader dependency landscape. This worker did not repeat a repository-wide archive survey.", + "Discussion posting unavailable to the lead; scope is recorded in the lead's local allocation manifest. No public advance reservation is asserted." + ] +} diff --git a/research/shrinking-reference-halo/PROOF.md b/research/shrinking-reference-halo/PROOF.md new file mode 100644 index 0000000000..c47fc7013b --- /dev/null +++ b/research/shrinking-reference-halo/PROOF.md @@ -0,0 +1,578 @@ +# A source-bound shrinking-domain Gaussian halo consumer + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. + +## 1. Result, scope and predecessor boundary + +This is a constructive local tensor result under a certified fixed-reference +row gap. It supplies the numerical consumer and its sequential data/page +protocol on one saved sparse rectangle. It does not prove the complete outer +Gaussian construction, admit the selected suppliers, or change kappa. + +The fixed-source Horner identity is classical. In this repository, #1430 already +uses it to control rounding under a fixed approximate oracle with norm at most +0.42; #6490 allocates precision across that oracle's calls. #5159 implements a +rounded whole-period action on one actual rational Gaussian Reference, with +coefficient error, data error and storage charged at a host-array interface. +#5216 improves its tail and #5260/#5284 supply direct-solve alternatives, also +without a complete physical sparse caller. #3851 implements a different +principal-core/Schur interface, with its own source parameters and gap. + +#6880 already proves direct row-gap locality, normalized nonlinear core/halo +composition, inward-rounded polynomial rows, and the specialization J=16p^4. +Those are not new claims here. That package leaves production of the global +polynomial coefficient pages and their physical access unpriced. #4100's HALO +argument permits a polynomial-time local correction but does not implement +the present recurrence, shrinking domains, or table/line schedule. + +The contribution is an explicit replacement for that remaining polynomial-row +interface: store only the original reference band, shrink the dependency +interval after every iteration, expose axes by sorting only sparse records, +reuse one page across every spectator line, and use eight fixed local tape +roles plus one protected coefficient archive. Its quantified all-size bill +includes reference production, repeated full archive scans, encoded controls, +scalar arithmetic, copies, head returns and retained blank backing. A full-axis +scan is retained explicitly in the generic theorem; it is absorbed only in the +specified balanced growing-group regime. + +The universal argument below is a written proof. The executable fixtures +corroborate it; neither finite traces nor separate AI review are formal-kernel +or independent human acceptance. + +## 2. Exact input contract + +For axis i, let H_i=I-E_i be a real rational matrix of period N_i. Let W_i be a +nonnegative integer with 2W_i=1, and choose an integer u_i>=0 with +a_i=2^u_i and a_i delta_i>=1. Choose one data/coefficient grid h=2^-q with +q>=max_i u_i. The incoming complex array has components on this grid and + + ||x||_* = max_r (|Re x_r| + |Im x_r|) <= R, + +where the executable interface takes an integer R>=1. A complex-modulus unit +disk input fits this interface with R=2. Every actual incoming line is checked +against its stated bound. The theorem does not infer an outer caller's input +radius merely from an exact ideal map. + +An output interval T_i=[t_i,t_i+m_i) is interpreted on the integer lift of the +physical circle. Set b_i=(J_i-1)W_i and + + D_i = [t_i-b_i, t_i+m_i+b_i), d_i = m_i+2b_i. + +Require d_i=u_i is required. The absolute component-l1 sum +of any partial accumulator is at most R*2^(2q): it is bounded by the source +term plus a partial sum of coefficient absolute values times R. A signed +carrier of 2q+ceil(log2(R+1))+2 bits is ample. Coefficient and data carriers +have q+O(log(R+1)) bits. The code checks the actual partial accumulator bound, +not just the final rounded result. + +Write y_k=(1/a_i) sum_(j=0)^(k-1) E_i^j x. Its norm is also at most R. +Subtract its recurrence from (1), evaluating the perturbation at the *actual* +z_k. If e_k=||z_k-y_k||_*, then + + e_(k+1) <= rho_i e_k + s_i h R + 2h, e_0=0. + +Therefore + + ||z_(J_i) - P_i x/a_i||_* <= nu_i, + P_i=sum_(j=0)^(J_i-1) E_i^j, + nu_i=(s_i R+2) h/delta_i. (2) + +The sharper finite geometric factor could be retained; (2) is sufficient. +The exact normalized polynomial and inverse both have induced norm at most +one, and the tail is + + ||P_i/a_i-H_i^-1/a_i||_infinity + <= tau_i = rho_i^J_i/(a_i delta_i). (3) + +These numerical estimates retain standard Neumann/Horner reasoning and the +whole-period predecessor's coefficient/data accounting. Their role here is +to certify the actual finite-precision sequential local program. + +## 4. The shrinking domain is exactly sufficient + +Define + + D_i^(k) = T_i + [-(J_i-k)W_i, (J_i-k)W_i], + 1 <= k <= J_i, + +where the notation denotes the corresponding half-open integer interval. +Compute z_1=Q_q(x/a_i) on D_i^(1)=D_i. To compute z_(k+1) on D_i^(k+1), +read its source x there and every previous neighbor within distance W_i. +Those neighbors lie in D_i^(k). The global coefficient for the corresponding +canonical row and offset is obtained from the already fixed band page. + +Induction on k now proves equality, bit for bit, with the restriction of the +full-period rounded recurrence (1). This statement does not require linearity +of rounding. It follows because each local update sees exactly the same +coefficient numerators, source numerator and prior neighbor numerators as the +global update. At k=J_i the returned interval is precisely T_i. + +This is not the polynomial of E restricted to T_i or to the eventual returned +rectangle. Such a restriction loses paths that leave and reenter it. The +program retains D_i^(k) until its use at the next step, then discards only the +two already unnecessary boundary strips. The initial padding is exactly the +maximum dependency distance of the degree J_i-1 polynomial. + +For h_axes axes processed in order, after completing axis i the maintained +rectangle is + + S_i = T_0 x ... x T_i x D_(i+1) x ... x D_(h_axes-1). (4) + +At the next axis, every needed neighbor differs only in that next coordinate. +The earlier coordinates therefore need no padding after their axes have +completed. The later coordinates must retain their complete original D_j. +Applying the one-axis induction to every spectator line proves exact agreement +with the corresponding restriction of the full-period nonlinear tensor +recurrence. That full-period recurrence is an analysis device, not an executed +dense algorithm. + +Compare this global rounded composition first with the product of P_i/a_i. +Each local error bound (2) holds at the actual incoming state, which has radius +R. Each exact P_i/a_i is a contraction. Telescoping against these exact maps +gives numerical error at most sum_i nu_i. Telescoping (3), using contraction +of both factors, then gives the complete inverse-tensor guarantee + + ||returned - [product_i (H_i^-1/a_i)] x |_T||_* + <= sum_i nu_i + R sum_i tau_i. (5) + +No factor depending on the global tensor dimension occurs in (5). No +assumption that the rounded program itself is additive or nonexpansive is +made. The proof applies to every global extension of the saved input with +radius at most R, since all omitted inverse dependence is explicitly funded +by (3). + +## 5. One sequential line and its exact invoice + +The global band table is ordered by canonical row, then by offsets -W_i to +W_i. A local page is ordered by lifted row, then by the same offsets. If D_i +wraps, one complete table scan emits its final-period part, and a second +complete scan emits its initial-period part. All skipped coefficients are +read and both complete scans return to the origin. No constant-cost global +row query, arbitrary seek or hidden page cache is assumed. + +`apply_line` uses the immutable source, immutable page, and two owned iterate +tapes. It forms z_1 by one source scan. During an update, a row reads the +2W_i+1 adjacent previous records in increasing order. Before the next output +row, the previous-state head walks back exactly 2W_i records. Thus the next +window advances by one. At the final row the head is at the end of the prior +live body. The source and page also make explicit forward skips and complete +returns. Before reusing an iterate role, the program clears its complete +previous live body, including all rows that existed before the next shrink. +It never substitutes the smaller newly produced length for that old length. + +Each role maintains a live-body length and a separate historical extent. All +cells at or beyond the live length are already zero. The invariant is true +on a fresh blank tape. A write extends the live length through its position; +the formerly unoccupied gap and remaining suffix were already blank. Clearing +the complete previous live body makes the live length zero and leaves the +invariant true. Thus a historical blank suffix remains paid in space without +being rescanned at every later reuse. Program transitions use this invariant +and encoded lengths, not an uncharged host inspection of the backing array. + +This distinction is necessary for the claimed tariff. A long L-sized line +followed by an A-sized face line must not pay L cells per clear on each short +line. That alternative adds a factor L/A and can consume the sparse volume +saving. The verifier executes a long-line/short-face/long-line history on the +same roles, checks actual blank suffixes independently, and compares an +executed counterfactual that clears the historical extent on every reuse. + +For target length m, the live lengths after k terms are +n_k=m+2(J_i-k)W_i. A complex line performs exactly + + 2s_i sum_(k=2)^J_i n_k + = 2s_i[(J_i-1)m + W_i(J_i-1)(J_i-2)] + +integer products and the same number of accumulator additions. It performs + + 2 sum_(k=1)^J_i n_k = 2[J_i m + W_i J_i(J_i-1)] + +component roundings. The fixed-source shifts, reads, output writes, +initialization, complete old-live-body erasure and all head motion are separately +counted. J_i=1 and W_i=0 are allowed by these formulas. + +Let w bound the numerical carriers and the entire encoded descriptor/control +block, including signed absolute origins, lengths, periods, iteration counts, +loop counters and local keys. A decoded scalar integer addition, shift, +comparison, multiplication or division is implemented by ordinary fixed-tape +binary arithmetic. Schoolbook multiplication/division costs O(w^2). Even +charging O(w^2) for each scalar encode/decode, rather than treating a host +integer shift as unit time, a line costs + + O(J_i d_i s_i w^2) bit operations. (6) + +Its source plus two iterate roles occupy at most 6d_i times the component +carrier width; its page occupies d_i s_i(q+2) bits. Add O(w) scalar/control +storage and the separately retained global archive. A returned output occupies +one of those two iterate roles, so it is not omitted from the space count. +Unused suffixes can remain allocated but are blank and are included in this +bound. `maximum_single_tape_extent` is only the largest individual tape; +the verifier separately sums every retained local role. + +The Python program executes every binary tape read/write and one-cell head +move. Its integer operations implement scalar-macro semantics; its elapsed +Python time is not asserted to equal the asymptotic bit bound (6). The proof +supplies the fixed-tape implementation and cost of those scalar macros. + +## 6. Complete local rectangle schedule and generic cost + +The payload has a fixed-width key comprising the nonnegative offsets within +the original D_i, followed by signed fixed-width real/imaginary numerators. +Let K=sum_i max(1,ceil(log2 d_i)); unused field encodings are not valid +coordinates. An initial lexicographic stream is encoded in one charged pass. +The same fixed key fields remain valid after an axis shrinks. Return converts +offsets back to lifted coordinates; the outer caller may reduce them modulo +the periods in another explicitly charged pass. + +To expose axis i, perform stable least-significant-bit distribution into two +fixed buckets. Process the bits of field i first, then the bits of the other +fields in reverse natural order. Concatenation of the zero and one buckets +after each pass leaves the other fields in natural lexicographic order, with +axis i innermost. Each pass scans and clears the entire live owned sparse body +and both live buckets; already blank retained tails obey the same invariant. +It never scans the dense +global data array. There are exactly K passes per axis. The conservative +scalar encode/decode convention above charges O(K C_i w^2) bit work for a +body with C_i records, rather than hiding key operations in a unit-cost word. + +After exposure, each complete spectator line is copied into one reusable +immutable line role, evaluated by Section 5, and emitted with target-only +keys into the alternate rectangle role. The local band page is produced +once per rectangle/axis, before its first line, and reused across all of those +lines. Only after the entire axis output is complete is the previous rectangle +cleared. Equation (4) gives the next live shape. After the final axis, natural +lexicographic order is already restored. + +There are eight local roles: current/next rectangles, two radix buckets, +one line source, two iterates and one local page. Their count is independent +of J_i, the number of lines, rectangles and axes. `tensor.py` creates the pool +once in `TensorWorkspace`, passes the same iterate roles to every line, and +clears every nonreturn role. After the caller consumes and clears the returned +rectangle, the same workspace accepts the next rectangle through the explicit +`rectangle_input(..., tape=...)` and `apply_tensor(..., workspace=...)` interfaces. +The verifier seals all tape constructors across a long/short/long sequence of +complete rectangle calls and checks that the identical eight role objects +return blank. Across such a history, space is the sum of the eight historical +extents, bounded by the largest admitted body for each role; time depends on +the currently occupied lengths, by the invariant in Section 5. +The global tables are concatenated in one protected archive; `pack_tables` +consumes and clears one temporary table before requesting the next from its +generator. Thus a growing number of axes does not require a growing number of +physical tapes. Descriptor tuples in the Python reference represent one +encoded control block. Scan/selection costs on that block are bounded by w +and included in the w^2 allowances; indexed metadata is not free access to +payload or coefficients. + +Let C=product_i d_i and G=sum_i N_i s_i be the total band coefficient count in +the current group's archive. The executable scans the *entire concatenated +archive* once or twice for each axis page, including other axes' coefficients. +If T_ref denotes reference production and quantization, the complete generic +local bill is + + T_ref + O(w^2 [h_axes G + C sum_i (J_i s_i + K + 1)]). (7) + +Input codec, all source/data/page transfers, output copying, sorting, +arithmetic, head returns and erasure are included. T_ref is a separately +amortized group setup if the archive is reused for several rectangles. The +term h_axes G remains present for each rectangle; it is not automatically a +local polynomial merely because d_i is polynomial. + +With eight local roles, their total retained extent is + + O(Cw + max_i d_i s_i q), + +plus O(w) control/scalar storage and the protected archive G(q+2). At most a +constant number of old/new rectangle bodies coexist. The producer's setup +scratch is additional, as quantified next. The code's physical action counts +and full retained extents are evidence for this schedule, not a byte-exact +claim about Python's object allocator or secure memory zeroization. + +## 7. Binding to the actual retained Gaussian entry producer + +The live source is `research/rational-unitary-fft/gaussian_reference.py` at +the exact base in SOURCES.json. Its original geometry and proof are retained +in `RAW-GAUSSIAN-PROOF.md`. `source.py` authenticates all source bytes before +execution. It rebinds the original import dependencies and extracts only the +unchanged `rational`/`load_intervals` helpers from `gaussian.py`, avoiding an +unused full-circuit compiler import. It changes no executed numerical function +body. `Reference.for_cap` is not called by this adapter; its use would require +the larger compiler dependency closure. + +For original source size S, excess K0, target period N=S+K0, and +theta=K0/S, the source fixes + + c_j=floor(theta*j+1/2), q_j=j+c_j, beta_j=theta*j-c_j. + +The narrow reference has identity holes and zero selected/hole cross entries. +For a source halfwidth w0 with 2w0=2w0+2 +therefore contains every nonzero entry of E=I-H. Our table loops over every +canonical target row and every physical offset, calls that exact entry rule, +checks the original row mass and truncates the resulting rational toward zero. +Holes and genuine period crossings use the same rule as all other entries. + +The source's relative-weight construction avoids silently replacing tiny +positive weights by zero. With entry precision b_e its weight precision is + + P_weight=ceil(2 alpha^2/theta)+b_e+7, + +and its kernel precision adds O(alpha^2 w0). Under the retained caller's +theta in [1/(4p^2),1/p^2], alpha^2=O(log p), b_e=O(p), and W= 1/(16p^2), W_i4A, b_i<=A and N_i>=2L. Then every first-face expanded side has +length at most L+2b_i=F_in, max_i u_i, where F_in is the actual incoming grid, and +fund, for a desired local group allowance 2^-Cp, + + q >= Cp + ceil(log2(4 h_axes max_i[(s_i R+2)/delta_i])). (9) + +This makes sum_i nu_i<=2^-Cp/4. Since rho_i^J_i<=exp(-p^2), the tail term in +(5) is also below 2^-Cp/4 eventually for fixed C and polynomial R. The chosen +q is O(p) whenever F_in=O(p) and R is polynomial. No exact incoming bits are +discarded: q is at least F_in. One may choose a_i between delta_i^-1 and +2delta_i^-1, or use the caller's larger existing dyadic p^100 normalization. +The same normalizer must be used by any core route with which these outputs +are spliced. The total outer compensation is O(d log p)=o(p), and must be +paid/restored by the existing caller; it is not canceled for free here. + +For completeness, implement the source's “balanced groups” explicitly. With +d>=g>=2, put m=ceil(d/g) and split the d axes into m groups of sizes +floor(d/m) or ceil(d/m). Every group has at most g axes and at least +floor(g/2) axes. Thus there is no exceptional final one-axis remainder to +which a growing-group amortization has been incorrectly applied. + +The source has ell=Theta(p^(1-epsilon)), axis periods at most 2^ell, +d=Theta(p^epsilon), and g=Theta(p^beta), with beta>1-epsilon. A first-face +rectangle has at least h_axes-1 long sides of length L-2A, so its volume C +satisfies + + log2 C >= (h_axes-1) log2(L-2A). + +Because h_axes=Omega(p^beta), the right side dominates +ell + c log p for every fixed c. Therefore even a complete concatenated +axis archive scan, of size 2^O(ell) poly(p), repeated once or twice per local +axis, is eventually bounded by C. This proves absorption of the repeated +scan term in (7). It is stronger than simply saying local setup is polynomial +in p. For arbitrary fixed h_axes, or any failed finite comparison, retain +the full h_axes G w^2 term. The effective comparison can be made with integer +bit lengths before adopting the asymptotic branch. + +Offline production across all d axes costs +d*2^O(ell)*poly(p)=2^o(p)=o(V), using (8), where V=T_total*p is the source's +full bit volume. This is a different charge from repeated per-rectangle +archive scans. Preparing each group's archive once as it is reached gives +the same summed bound and uses a constant physical tape pool. + +In the actual balanced regime, all control/coordinate fields fit O(p) bits: +h_axes log L=o(p), h_axes ell=o(p), and the source uses beta+1-epsilon<1. +Numerical carriers have O(p) bits by (9). Thus w=O(p), J_i=O(p^4), s_i=O(p), +and K=O(p). Equation (7) gives the deliberately conservative local bound + + O(C h_axes p^7) bit work, plus the explicit offline setup. (10) + +There are O(h_axes A/L) copied records per original full-array record in a +group. Summing (10) over all rectangles and O(d/g) balanced groups gives + + O(V d g A p^6 / L) (11) + +for this numerical consumer, with sparse layout, pages and arithmetic +included. It is inside the older allowance O(V d g A^3/L polylog p). +With A=p^48 and L>=p^400 its exponent is at most +epsilon+beta+54-400<0. The dense gather/return scans remain the separate +O(V d/g) row of the outer ledger; this package does not invoke a dense scan +per numerical axis. The existing first-face copy producer and unique-return +transaction must provide those operations. Formula (11) is not a new kappa +claim; it establishes that this explicit consumer does not exhaust the +already reserved conservative halo budget. + +## 9. Evidence, limits and remaining composition + +The verifier uses exact integers and Fractions for every acceptance decision. +It checks 32 signed nonstationary cyclic-band lines, including identity holes, +negative/positive coefficients and wrapping targets. Its independent dense +polynomial evaluator forms successive powers and their sum. A second global +rounded evaluator checks exact bit equality, while the written proof supplies +the universal quantifiers. + +Two synthetic tensors execute the complete sparse tape schedule in two and +three dimensions. A second history executes three differently shaped rectangles +with the same eight roles and no new tape construction permitted. The actual source fixture is +Reference(32,8,2,1,8,32), with period 40 and eight identity holes. All 1,600 +original entries are checked, including omitted entries and genuine wraps. +Three local lines and a 756-record two-axis saved rectangle are executed; +the latter returns exactly twelve target records. Its source-certified gap, +numerical bound, tail bound, complete products/roundings, page scan count, +radix count and summed retained extents are recorded in RESULT.json. + +These finite source parameters are legal for the retained Reference API but +are not an execution of the eventual outer production regime. The all-size +parameter substitution rests on Sections 7–8 and the explicitly retained +source hypotheses, not on extrapolation from forty rows. + +Controls reject wrong normalization, insufficient source grid, ambiguous band +offsets, missing row gap, oversized actual data, aliased page intervals, +incorrect dependency crops and negative-zero records. Actual consumer code +mutations exercise wrong recurrence sign, wrong neighbor rewind and omitted +erasure, wrong sparse-axis exposure, stale axis pages and shifted return keys; +a dropped actual periodic branch changes the returned source answer. The +long-short-long history and counterfactual high-water tariff guard the +physical reuse obligation that is invisible to a numerical-only comparison. +Normal and optimized replay do not rely on Python assertions. + +Two additional checks were independently developed during adversarial review. +Neither imports verify.py, the dense-power oracle, or its expected outputs. +The first solves four rows of the original forty-by-forty H inverse by exact +rational elimination of H^T. Every computed row satisfies its exact inverse +equations. Tensoring these rows then gives an independent original-inverse +answer at four two-axis targets, against which the physical consumer has +maximum component-l1 error below 5.252e-9, within (5)'s 8.213e-8 allowance. +Its nested target has identical returned bits, all eight tape roles are reused +with constructors sealed, and the reference archive stays unchanged. A shifted +target control has error greater than 0.109. + +The second executes every singleton output of one forty-row input, computes +the original-reference residual r=x/a-Hy, and uses +||H^-1||_infinity<=1/delta to certify ||y-H^-1 x/a||<=||r||/delta. +This gives error below 7.667e-9 without using a polynomial oracle. For a +cyclically shifted returned vector, ||r||/||H||_infinity gives an error lower +bound greater than 0.543. Every acceptance decision is exact rational +arithmetic. Both scripts run normally and with assertions disabled as +registered checks; their decimal output is only a readable summary. +The independent method and implementation provenance concern a separate AI +reviewer in the same research effort, not external mathematical acceptance. + +No arbitrary native implementation, complete finite-core adoption, dense +first-face copy/return protocol, broad Gaussian map, all-depth supplier, +outer tensor/CRT algorithm or exact integer-recovery theorem is established +here. The source H, its certified row gap and ideal-Gaussian comparison remain +named dependencies. #5325 and #4415 already address other error-join/suffix +questions; their results are not duplicated or silently assumed compatible +with a different rounded reference. A complete join must verify that the +core, this consumer, normalizers and the eventual outer recovery use the same +source interface and actual grid/radius contracts. All five selected +framework assumptions remain in force. No new kappa. diff --git a/research/shrinking-reference-halo/README.md b/research/shrinking-reference-halo/README.md new file mode 100644 index 0000000000..d93de03476 --- /dev/null +++ b/research/shrinking-reference-halo/README.md @@ -0,0 +1,198 @@ +# Compute sparse Gaussian inverse halos from the original band + +**Scoped constructive result, with a written all-size proof and exact finite +corroboration. No new κ.** + +This package replaces an unpriced global polynomial-row oracle with an +explicit local numerical consumer. It evaluates the normalized inverse +polynomial from the original rational reference band, shrinking the saved +dependency interval after each step. The full local tensor program includes +sparse axis exposure, absolute-coordinate coefficient pages, actual rounding, +immutable fixed-source lines, physical head returns and cleanup. + +The contribution is the source-bound sequential interface and complete bill. +The Neumann/Horner identities, the direct row-gap locality degree, and generic +rounded core/halo composition were already available. The comparison below +is part of the novelty boundary, not a claim of general literature priority. + +## Technical result + +For real cyclic band matrices `H_i=I-E_i` with row gap `delta_i>0`, bandwidth +`W_i`, and a shared q grid, choose dyadic `a_i` with `a_i delta_i>=1`. The +program uses `J_i` fixed-source updates and a saved halo of +`b_i=(J_i-1)W_i`. It returns the target rectangle with error at most + + sum_i [(2W_i+1)R+2] * 2^-q/delta_i + + R sum_i (1-delta_i)^J_i/(a_i delta_i). + +Every actual intermediate remains on the same grid and within the original +component-l1 radius `R`. Each source line is preserved through its complete +update sequence. The program never forms the dense polynomial coefficient +rows, and it never assumes translation invariance of the reference entries. + +The numerical tensor uses eight reusable local tape roles and one protected +concatenated reference archive. Each local page takes at most two **complete +archive scans per rectangle/axis**, and is reused across all spectator lines. +Sorting touches only the sparse saved rectangle. A live-body/blank-suffix +invariant prevents repeated erasure of old large buffers from introducing an +unfunded `L/A` factor on a later short face. + +For copied volume `C`, key width `K`, arithmetic/control width `w`, and +archive coefficient count `G`, the complete generic bit bill is + + T_reference + O(w^2 [h_axes G + C sum_i(J_i(2W_i+1)+K+1)]). + +The full archive term is explicit. In the exact balanced growing-group regime +of the pinned #4100 route, a rectangle's many long sides absorb the repeated +archive scans. The original source producer has separately charged +`d*2^O(ell)*poly(p)=2^o(p)` setup. The resulting numerical consumer costs +`O(V d g A p^6/L)`, inside the route's older conservative halo allowance. +This substitution does not admit that archived outer proof or change the +selected conditional frontier. + +The complete definitions, no-alias domain, fixed-role implementation, +coefficient producer, scalar arithmetic and production substitution are in +[PROOF.md](PROOF.md). Exact base and source hashes are in +[SOURCES.json](SOURCES.json). + +## What was already proved + +| Source | Existing result | Present distinction | +|---|---|---| +| #1430 and #6490 | Stable fixed-source Horner evaluation and its oracle precision allocation | Original reference entries, local shrinking domains and sequential producer/consumer cost | +| #5159 and #5216 | Complete rounded whole-period service on one rational Gaussian Reference | Sparse local tensor, variable certified gaps, fixed tape roles and production-group substitution | +| #5260 and #5284 | Host-array direct solves and variable-gap cyclic-band precision | Different iterative mechanism; includes the sparse physical page/layout interface | +| #3851 | Physical normalized principal-window compression core | Complements that core; does not reprove its Schur/q-convolution mechanism or use its different gap as this caller's gap | +| #6880 | Direct row-gap polynomial, `J=16p^4`, inward-rounded polynomial rows and nonlinear core/halo composition | Eliminates the polynomial-row oracle using the original band and prices its production/access | +| #4870 | First-face source-copy enumeration | Receives one completed saved rectangle; dense-source copy generation and final unique return remain outside this consumer | + +#5325's tensor error join, #4415's outer suffix accounting, and #4205/#4253's +finite-core circuit theorem are not claimed as new work. A future integration +must check their source/reference versions and actual grids before composing +them with this consumer. + +## Exact evidence and reproduction + +From the repository root, with CPython 3.12 and the standard library: + +```sh +python3 -I -B research/shrinking-reference-halo/verify.py +``` + +Expected marker: `PASS_SHRINKING_REFERENCE_HALO`, with 32 finite lines, +40 Gaussian rows, 1,600 original source entries, 17 rejection controls, +and `no_new_kappa: true`. + +The registered replay runs the author verifier and two separately developed +mathematical checks, each in normal and optimized Python: + +```sh +python3 -B scripts/research_package.py --package research/shrinking-reference-halo +``` + +[RESULT.json](RESULT.json) is generated by the verifier and required by normal +read-only replay. It records: + +- Thirty-two signed, nonstationary cyclic-band lines and ninety-six returned + target coordinates, with exact dense-polynomial and full rounded-period + comparators. +- Complete two- and three-axis synthetic tensor executions, followed by a + long/short/long rectangle history with all tape constructors disabled. +- The actual retained `Reference(32,8,2,1,8,32)`, including every one of its + 1,600 entries, all eight identity holes, and genuine across-period entries. +- Three actual-reference lines and a two-axis, 756-record saved rectangle + returning twelve target records, with the complete product, rounding, + archive-scan, radix, head-action and retained-space counts. +- Seventeen explicit rejection/code-mutation controls. Separate executed + comparisons detect dropping the actual periodic branch and the unfavorable + high-water-clearing tariff, even though the latter leaves numerical answers + unchanged. + +The matrix-power oracle forms successive exact powers and their sum; it does +not import the numerical recurrence's implementation. The global rounded +comparator additionally checks bit-for-bit locality. + +The separately developed [independent_inverse.py](independent_inverse.py) +solves four rows of the **original rational inverse** by exact elimination, +checks their exact matrix residuals, and uses those rows to evaluate the +two-axis inverse independently of the polynomial recurrence. The physical +consumer's four outputs have maximum error below `5.252e-9`, within the +proved `8.213e-8` allowance. A second nested target returns identical bits, +reuses the same eight roles with tape creation disabled, and preserves the +archive. A wrong-target control produces error greater than `0.109`. + +[independent_residual.py](independent_residual.py) runs all forty physical +singleton outputs and bounds their inverse error directly from the original +matrix residual and its exact row gap. The certified error is below +`7.667e-9`, while a cyclically misreturned output has error greater than +`0.543`. Neither check imports the author verifier or its expected output. +Their expected markers are `PASS_LEAD_EXACT_TENSOR_INVERSE` and +`PASS_LEAD_ORIGINAL_REFERENCE_RESIDUAL`. + +These checks were developed by a separate AI reviewer within this contribution, +using different mathematical mechanisms. All acceptance comparisons use +exact rational arithmetic; displayed decimal summaries are diagnostic. The +all-size claims rest on the written proof. No external human or formal-kernel +acceptance is asserted. + +## Scope and limitations + +The source-bound forty-row example is a legal finite Reference fixture, not +an execution of the asymptotic outer production parameters. Its all-input +same-reference numerical error is funded below `2^-20` per axis, while the +source's ideal-Gaussian perturbation and global gap proof remain inherited. +The generic theorem explicitly requires zero outside the stated cyclic band; +checking stored row mass alone does not prove support. + +Binary tape movement is executed. Scalar integer macros are exact in the +reference and are priced by a written ordinary schoolbook arithmetic +implementation. Source cache serialization and its conservative polynomial +setup bound are proved, not claimed as a measured fast Python producer. +Retained blank backing is included in space; Python allocator zeroization +and byte-exact host heap accounting are not claimed. + +The saved rectangle must come from original values before any core mutation. +This package consumes that saved copy and returns its target; it does not +implement the full dense-source first-face gather or final dense unique-key +merge. It supplies no new native supplier, core admission, complete broad +Gaussian map, all-depth compiler, CRT join or exact integer multiplier. All +five selected framework assumptions remain. **No new κ.** + +## Provenance and credit + +Scientific base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. +The selected conditional frontier at that base is +`781451/250000000 = 0.003125804`; it is unchanged. + +The compatible, concurrently published #6880 proof was read at +`e212af981b49c299de515f8c23dfb0e5b73e2e95`. This package is self-contained for +its local theorem and has no executable dependency on that unmerged commit. +The exact retained Gaussian implementation and source proof are pinned at +the canonical base in SOURCES.json; no predecessor file is changed. + +Prepared for **@CubeJerry**, with substantial OpenAI Codex assistance in +mathematics, source analysis, implementation, verification and prose. Credit +Cinna Davis (#4100), Jose Manuel / jmbarrancoml (#3851, #4205/#4253), +JoyboyBrian (#5159/#5216), Hanson Sun / bbMisk (#1430), Ali Romman +(#5260/#5284), @codyw912 (#4870), Nick Petalas (#4217/#5986), and the inherited work of +Vlado Vojdanovski, Jeremy Kothe, Mason Hale and Chafik Boukhalfa. Classical +Neumann iteration, Horner evaluation, diagonal dominance, stable radix +distribution and ordinary binary arithmetic retain their original credit. +The source's Harvey–van der Hoeven, OpenAI manuscript and Douglas Colkitt +lineage and Apache-2.0 notices are retained in the declared sources. + +## Open next questions + +1. **Join this consumer to an actual first-face copy/return transaction.** + The numerical program needs original copied values and must return each + discarded key exactly once. First bind one wrapping/hole rectangle's + encoded payload, normalizer and grid on both sides, then prove the complete + group bill. The dense chronology and output ownership remain the blocker. +2. **Use the same rounded reference at the actual finite core and outer + recovery.** The local result does not permit substituting a similarly named + Gaussian matrix. First pin the core's exact reference/normalizers and its + all-input error, then insert (5) in its existing recovery ledger. Source + compatibility and complete outer admission remain open. + +The quantified questions, overlap coverage and stopping rule are also retained +in [TASK.json](TASK.json). No further optimization is reserved by this package. diff --git a/research/shrinking-reference-halo/RESULT.json b/research/shrinking-reference-halo/RESULT.json new file mode 100644 index 0000000000..2e546fe9ab --- /dev/null +++ b/research/shrinking-reference-halo/RESULT.json @@ -0,0 +1,3662 @@ +{ + "backing_reuse": { + "correct": [ + { + "moves": 61264, + "output": [ + [ + -768, + -393 + ], + [ + -704, + -366 + ], + [ + -640, + -339 + ], + [ + -576, + -312 + ], + [ + -512, + -285 + ], + [ + -448, + -257 + ], + [ + -384, + -230 + ], + [ + -320, + -203 + ], + [ + -257, + -176 + ], + [ + -193, + -149 + ], + [ + -129, + -122 + ], + [ + -65, + -95 + ], + [ + -1, + -68 + ], + [ + 62, + -41 + ], + [ + 125, + -14 + ], + [ + 189, + 13 + ], + [ + 253, + 40 + ], + [ + 317, + 67 + ], + [ + 381, + 94 + ], + [ + 445, + 121 + ], + [ + 509, + 148 + ], + [ + 572, + 175 + ], + [ + 636, + 202 + ], + [ + 700, + 229 + ], + [ + 764, + 257 + ], + [ + 764, + 284 + ], + [ + 572, + 311 + ], + [ + -515, + 338 + ], + [ + -707, + 365 + ], + [ + -707, + 392 + ], + [ + -643, + 387 + ], + [ + -579, + 287 + ], + [ + -516, + -261 + ], + [ + -452, + -362 + ], + [ + -388, + -367 + ], + [ + -324, + -340 + ], + [ + -260, + -313 + ] + ], + "retained_bits": 5110, + "saved_length": 41, + "target_length": 37, + "writes": 12292 + }, + { + "moves": 12880, + "output": [ + [ + 505, + 12 + ] + ], + "retained_bits": 5110, + "saved_length": 5, + "target_length": 1, + "writes": 1204 + }, + { + "moves": 69748, + "output": [ + [ + -8, + -341 + ], + [ + 55, + -313 + ], + [ + 118, + -286 + ], + [ + 182, + -259 + ], + [ + 246, + -232 + ], + [ + 310, + -205 + ], + [ + 374, + -178 + ], + [ + 438, + -151 + ], + [ + 502, + -124 + ], + [ + 565, + -96 + ], + [ + 629, + -69 + ], + [ + 693, + -42 + ], + [ + 757, + -15 + ], + [ + 757, + 11 + ], + [ + 565, + 38 + ], + [ + -522, + 65 + ], + [ + -714, + 92 + ], + [ + -714, + 119 + ], + [ + -650, + 146 + ], + [ + -586, + 173 + ], + [ + -523, + 201 + ], + [ + -459, + 228 + ], + [ + -395, + 255 + ], + [ + -331, + 282 + ], + [ + -267, + 309 + ], + [ + -203, + 336 + ], + [ + -139, + 363 + ], + [ + -75, + 390 + ], + [ + -12, + 386 + ], + [ + 13, + 283 + ], + [ + -76, + -272 + ], + [ + -703, + -406 + ], + [ + -793, + -418 + ], + [ + -768, + -393 + ], + [ + -704, + -366 + ], + [ + -640, + -339 + ], + [ + -576, + -312 + ] + ], + "retained_bits": 5110, + "saved_length": 41, + "target_length": 37, + "writes": 12292 + } + ], + "counterfactual": [ + { + "moves": 61488, + "output": [ + [ + -768, + -393 + ], + [ + -704, + -366 + ], + [ + -640, + -339 + ], + [ + -576, + -312 + ], + [ + -512, + -285 + ], + [ + -448, + -257 + ], + [ + -384, + -230 + ], + [ + -320, + -203 + ], + [ + -257, + -176 + ], + [ + -193, + -149 + ], + [ + -129, + -122 + ], + [ + -65, + -95 + ], + [ + -1, + -68 + ], + [ + 62, + -41 + ], + [ + 125, + -14 + ], + [ + 189, + 13 + ], + [ + 253, + 40 + ], + [ + 317, + 67 + ], + [ + 381, + 94 + ], + [ + 445, + 121 + ], + [ + 509, + 148 + ], + [ + 572, + 175 + ], + [ + 636, + 202 + ], + [ + 700, + 229 + ], + [ + 764, + 257 + ], + [ + 764, + 284 + ], + [ + 572, + 311 + ], + [ + -515, + 338 + ], + [ + -707, + 365 + ], + [ + -707, + 392 + ], + [ + -643, + 387 + ], + [ + -579, + 287 + ], + [ + -516, + -261 + ], + [ + -452, + -362 + ], + [ + -388, + -367 + ], + [ + -324, + -340 + ], + [ + -260, + -313 + ] + ], + "retained_bits": 5110, + "saved_length": 41, + "target_length": 37, + "writes": 12404 + }, + { + "moves": 24192, + "output": [ + [ + 505, + 12 + ] + ], + "retained_bits": 5110, + "saved_length": 5, + "target_length": 1, + "writes": 6860 + }, + { + "moves": 69972, + "output": [ + [ + -8, + -341 + ], + [ + 55, + -313 + ], + [ + 118, + -286 + ], + [ + 182, + -259 + ], + [ + 246, + -232 + ], + [ + 310, + -205 + ], + [ + 374, + -178 + ], + [ + 438, + -151 + ], + [ + 502, + -124 + ], + [ + 565, + -96 + ], + [ + 629, + -69 + ], + [ + 693, + -42 + ], + [ + 757, + -15 + ], + [ + 757, + 11 + ], + [ + 565, + 38 + ], + [ + -522, + 65 + ], + [ + -714, + 92 + ], + [ + -714, + 119 + ], + [ + -650, + 146 + ], + [ + -586, + 173 + ], + [ + -523, + 201 + ], + [ + -459, + 228 + ], + [ + -395, + 255 + ], + [ + -331, + 282 + ], + [ + -267, + 309 + ], + [ + -203, + 336 + ], + [ + -139, + 363 + ], + [ + -75, + 390 + ], + [ + -12, + 386 + ], + [ + 13, + 283 + ], + [ + -76, + -272 + ], + [ + -703, + -406 + ], + [ + -793, + -418 + ], + [ + -768, + -393 + ], + [ + -704, + -366 + ], + [ + -640, + -339 + ], + [ + -576, + -312 + ] + ], + "retained_bits": 5110, + "saved_length": 41, + "target_length": 37, + "writes": 12404 + } + ], + "counterfactual_detected": true, + "retained_extent_ratio": "41/5" + }, + "claim": "scoped written proof and finite tape corroboration", + "control_count": 17, + "controls": [ + "unfunded normalization", + "lost normalized-source precision", + "nonunique cyclic offsets", + "missing contraction gap", + "bad original row gap", + "oversized actual input", + "repeated canonical page coordinate", + "immutable coefficient page", + "immutable fixed source", + "prematurely cropped dependency interval", + "noncanonical negative zero", + "wrong recurrence sign", + "wrong neighbor rewind", + "missing scratch erasure", + "wrong sparse axis exposure", + "stale axis coefficient page", + "shifted returned tensor key" + ], + "finite": [ + { + "bill": { + "additions": 0, + "control_steps": 183, + "maximum_single_tape_extent": 495, + "moves": 3828, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1122, + "roundings": 6, + "setup_divisions": 45, + "setup_entries": 45, + "source_shifts": 6, + "writes": 792 + }, + "bits": 9, + "gap": "1/8", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + -43, + -1 + ], + [ + 15, + 40 + ], + [ + 43, + -17 + ] + ], + "period": 15, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 385, + "maximum_single_tape_extent": 1200, + "moves": 11376, + "page_scans": 2, + "peak_scalar_bits": 19, + "products": 30, + "reads": 3252, + "roundings": 20, + "setup_divisions": 100, + "setup_entries": 100, + "source_shifts": 20, + "writes": 2268 + }, + "bits": 10, + "gap": "1/4", + "length": 3, + "lower": 17, + "nonzero_error": true, + "output": [ + [ + -85, + 93 + ], + [ + -139, + 145 + ], + [ + 166, + -5 + ] + ], + "period": 20, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 207, + "maximum_single_tape_extent": 819, + "moves": 8944, + "page_scans": 1, + "peak_scalar_bits": 22, + "products": 48, + "reads": 2223, + "roundings": 30, + "setup_divisions": 63, + "setup_entries": 63, + "source_shifts": 30, + "writes": 2054 + }, + "bits": 11, + "gap": "3/8", + "length": 3, + "lower": 9, + "nonzero_error": true, + "output": [ + [ + 115, + -111 + ], + [ + 300, + 200 + ], + [ + 337, + 193 + ] + ], + "period": 21, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 681, + "maximum_single_tape_extent": 2100, + "moves": 32928, + "page_scans": 2, + "peak_scalar_bits": 23, + "products": 210, + "reads": 9702, + "roundings": 72, + "setup_divisions": 150, + "setup_entries": 150, + "source_shifts": 72, + "writes": 5586 + }, + "bits": 12, + "gap": "1/8", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + 230, + 6 + ], + [ + 486, + -58 + ], + [ + -385, + -17 + ] + ], + "period": 30, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + }, + { + "bill": { + "additions": 0, + "control_steps": 231, + "maximum_single_tape_extent": 627, + "moves": 4620, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1386, + "roundings": 6, + "setup_divisions": 57, + "setup_entries": 57, + "source_shifts": 6, + "writes": 924 + }, + "bits": 9, + "gap": "1/4", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + -40, + -63 + ], + [ + -90, + -31 + ], + [ + 1, + 122 + ] + ], + "period": 19, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 367, + "maximum_single_tape_extent": 1140, + "moves": 11016, + "page_scans": 2, + "peak_scalar_bits": 19, + "products": 30, + "reads": 3132, + "roundings": 20, + "setup_divisions": 95, + "setup_entries": 95, + "source_shifts": 20, + "writes": 2208 + }, + "bits": 10, + "gap": "3/8", + "length": 3, + "lower": 16, + "nonzero_error": true, + "output": [ + [ + 129, + -2 + ], + [ + -211, + 51 + ], + [ + -206, + 13 + ] + ], + "period": 19, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 199, + "maximum_single_tape_extent": 780, + "moves": 8788, + "page_scans": 1, + "peak_scalar_bits": 21, + "products": 48, + "reads": 2184, + "roundings": 30, + "setup_divisions": 60, + "setup_entries": 60, + "source_shifts": 30, + "writes": 2015 + }, + "bits": 11, + "gap": "1/8", + "length": 3, + "lower": 9, + "nonzero_error": true, + "output": [ + [ + -208, + 165 + ], + [ + 194, + -23 + ], + [ + 327, + -150 + ] + ], + "period": 20, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 663, + "maximum_single_tape_extent": 2030, + "moves": 32508, + "page_scans": 2, + "peak_scalar_bits": 23, + "products": 210, + "reads": 9562, + "roundings": 72, + "setup_divisions": 145, + "setup_entries": 145, + "source_shifts": 72, + "writes": 5516 + }, + "bits": 12, + "gap": "1/4", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + -452, + -551 + ], + [ + 471, + -200 + ], + [ + -718, + -37 + ] + ], + "period": 29, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + }, + { + "bill": { + "additions": 0, + "control_steps": 219, + "maximum_single_tape_extent": 594, + "moves": 4422, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1320, + "roundings": 6, + "setup_divisions": 54, + "setup_entries": 54, + "source_shifts": 6, + "writes": 891 + }, + "bits": 9, + "gap": "3/8", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + 3, + 24 + ], + [ + 22, + -46 + ], + [ + 1, + 118 + ] + ], + "period": 18, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 439, + "maximum_single_tape_extent": 1380, + "moves": 12456, + "page_scans": 2, + "peak_scalar_bits": 17, + "products": 30, + "reads": 3612, + "roundings": 20, + "setup_divisions": 115, + "setup_entries": 115, + "source_shifts": 20, + "writes": 2448 + }, + "bits": 10, + "gap": "1/8", + "length": 3, + "lower": 20, + "nonzero_error": true, + "output": [ + [ + 22, + 5 + ], + [ + 1, + 43 + ], + [ + -11, + -2 + ] + ], + "period": 23, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 191, + "maximum_single_tape_extent": 741, + "moves": 8632, + "page_scans": 1, + "peak_scalar_bits": 22, + "products": 48, + "reads": 2145, + "roundings": 30, + "setup_divisions": 57, + "setup_entries": 57, + "source_shifts": 30, + "writes": 1976 + }, + "bits": 11, + "gap": "1/4", + "length": 3, + "lower": 8, + "nonzero_error": true, + "output": [ + [ + -448, + -86 + ], + [ + 55, + 179 + ], + [ + 673, + -56 + ] + ], + "period": 19, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 645, + "maximum_single_tape_extent": 1960, + "moves": 32088, + "page_scans": 2, + "peak_scalar_bits": 24, + "products": 210, + "reads": 9422, + "roundings": 72, + "setup_divisions": 140, + "setup_entries": 140, + "source_shifts": 72, + "writes": 5446 + }, + "bits": 12, + "gap": "3/8", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + 675, + 430 + ], + [ + -876, + 67 + ], + [ + 205, + 399 + ] + ], + "period": 28, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + }, + { + "bill": { + "additions": 0, + "control_steps": 207, + "maximum_single_tape_extent": 561, + "moves": 4224, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1254, + "roundings": 6, + "setup_divisions": 51, + "setup_entries": 51, + "source_shifts": 6, + "writes": 858 + }, + "bits": 9, + "gap": "1/8", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + 53, + 5 + ], + [ + 56, + 5 + ], + [ + 48, + -1 + ] + ], + "period": 17, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 421, + "maximum_single_tape_extent": 1320, + "moves": 12096, + "page_scans": 2, + "peak_scalar_bits": 20, + "products": 30, + "reads": 3492, + "roundings": 20, + "setup_divisions": 110, + "setup_entries": 110, + "source_shifts": 20, + "writes": 2388 + }, + "bits": 10, + "gap": "1/4", + "length": 3, + "lower": 19, + "nonzero_error": true, + "output": [ + [ + 33, + 288 + ], + [ + -111, + 57 + ], + [ + -143, + -92 + ] + ], + "period": 22, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 223, + "maximum_single_tape_extent": 897, + "moves": 9256, + "page_scans": 1, + "peak_scalar_bits": 22, + "products": 48, + "reads": 2301, + "roundings": 30, + "setup_divisions": 69, + "setup_entries": 69, + "source_shifts": 30, + "writes": 2132 + }, + "bits": 11, + "gap": "3/8", + "length": 3, + "lower": 10, + "nonzero_error": true, + "output": [ + [ + -309, + 183 + ], + [ + 54, + 277 + ], + [ + 570, + -127 + ] + ], + "period": 23, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 627, + "maximum_single_tape_extent": 1890, + "moves": 31668, + "page_scans": 2, + "peak_scalar_bits": 23, + "products": 210, + "reads": 9282, + "roundings": 72, + "setup_divisions": 135, + "setup_entries": 135, + "source_shifts": 72, + "writes": 5376 + }, + "bits": 12, + "gap": "1/8", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + -641, + -19 + ], + [ + 564, + 128 + ], + [ + 110, + 23 + ] + ], + "period": 27, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + }, + { + "bill": { + "additions": 0, + "control_steps": 195, + "maximum_single_tape_extent": 528, + "moves": 4026, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1188, + "roundings": 6, + "setup_divisions": 48, + "setup_entries": 48, + "source_shifts": 6, + "writes": 825 + }, + "bits": 9, + "gap": "1/4", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + -29, + 39 + ], + [ + 52, + 56 + ], + [ + -86, + 7 + ] + ], + "period": 16, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 403, + "maximum_single_tape_extent": 1260, + "moves": 11736, + "page_scans": 2, + "peak_scalar_bits": 19, + "products": 30, + "reads": 3372, + "roundings": 20, + "setup_divisions": 105, + "setup_entries": 105, + "source_shifts": 20, + "writes": 2328 + }, + "bits": 10, + "gap": "3/8", + "length": 3, + "lower": 18, + "nonzero_error": true, + "output": [ + [ + -66, + -131 + ], + [ + 185, + 83 + ], + [ + -52, + 69 + ] + ], + "period": 21, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 215, + "maximum_single_tape_extent": 858, + "moves": 9100, + "page_scans": 1, + "peak_scalar_bits": 20, + "products": 48, + "reads": 2262, + "roundings": 30, + "setup_divisions": 66, + "setup_entries": 66, + "source_shifts": 30, + "writes": 2093 + }, + "bits": 11, + "gap": "1/8", + "length": 3, + "lower": 10, + "nonzero_error": true, + "output": [ + [ + -84, + 0 + ], + [ + -198, + -14 + ], + [ + 104, + -128 + ] + ], + "period": 22, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 699, + "maximum_single_tape_extent": 2170, + "moves": 33348, + "page_scans": 2, + "peak_scalar_bits": 24, + "products": 210, + "reads": 9842, + "roundings": 72, + "setup_divisions": 155, + "setup_entries": 155, + "source_shifts": 72, + "writes": 5656 + }, + "bits": 12, + "gap": "1/4", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + -384, + 105 + ], + [ + 223, + -620 + ], + [ + 486, + 31 + ] + ], + "period": 31, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + }, + { + "bill": { + "additions": 0, + "control_steps": 183, + "maximum_single_tape_extent": 495, + "moves": 3828, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1122, + "roundings": 6, + "setup_divisions": 45, + "setup_entries": 45, + "source_shifts": 6, + "writes": 792 + }, + "bits": 9, + "gap": "3/8", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + 119, + 0 + ], + [ + 79, + 36 + ], + [ + -27, + 58 + ] + ], + "period": 15, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 385, + "maximum_single_tape_extent": 1200, + "moves": 11376, + "page_scans": 2, + "peak_scalar_bits": 18, + "products": 30, + "reads": 3252, + "roundings": 20, + "setup_divisions": 100, + "setup_entries": 100, + "source_shifts": 20, + "writes": 2268 + }, + "bits": 10, + "gap": "1/8", + "length": 3, + "lower": 17, + "nonzero_error": true, + "output": [ + [ + -21, + 42 + ], + [ + -69, + 54 + ], + [ + -39, + -23 + ] + ], + "period": 20, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 207, + "maximum_single_tape_extent": 819, + "moves": 8944, + "page_scans": 1, + "peak_scalar_bits": 22, + "products": 48, + "reads": 2223, + "roundings": 30, + "setup_divisions": 63, + "setup_entries": 63, + "source_shifts": 30, + "writes": 2054 + }, + "bits": 11, + "gap": "1/4", + "length": 3, + "lower": 9, + "nonzero_error": true, + "output": [ + [ + 297, + -225 + ], + [ + -171, + 132 + ], + [ + -13, + -46 + ] + ], + "period": 21, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 681, + "maximum_single_tape_extent": 2100, + "moves": 32928, + "page_scans": 2, + "peak_scalar_bits": 24, + "products": 210, + "reads": 9702, + "roundings": 72, + "setup_divisions": 150, + "setup_entries": 150, + "source_shifts": 72, + "writes": 5586 + }, + "bits": 12, + "gap": "3/8", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + 206, + 445 + ], + [ + 419, + -532 + ], + [ + 300, + -519 + ] + ], + "period": 30, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + }, + { + "bill": { + "additions": 0, + "control_steps": 231, + "maximum_single_tape_extent": 627, + "moves": 4620, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1386, + "roundings": 6, + "setup_divisions": 57, + "setup_entries": 57, + "source_shifts": 6, + "writes": 924 + }, + "bits": 9, + "gap": "1/8", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + -60, + -1 + ], + [ + -63, + 0 + ], + [ + 48, + 8 + ] + ], + "period": 19, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 367, + "maximum_single_tape_extent": 1140, + "moves": 11016, + "page_scans": 2, + "peak_scalar_bits": 20, + "products": 30, + "reads": 3132, + "roundings": 20, + "setup_divisions": 95, + "setup_entries": 95, + "source_shifts": 20, + "writes": 2208 + }, + "bits": 10, + "gap": "1/4", + "length": 3, + "lower": 16, + "nonzero_error": true, + "output": [ + [ + 225, + 22 + ], + [ + 184, + 15 + ], + [ + 198, + 11 + ] + ], + "period": 19, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 199, + "maximum_single_tape_extent": 780, + "moves": 8788, + "page_scans": 1, + "peak_scalar_bits": 22, + "products": 48, + "reads": 2184, + "roundings": 30, + "setup_divisions": 60, + "setup_entries": 60, + "source_shifts": 30, + "writes": 2015 + }, + "bits": 11, + "gap": "3/8", + "length": 3, + "lower": 9, + "nonzero_error": true, + "output": [ + [ + 383, + 172 + ], + [ + 20, + -235 + ], + [ + 323, + -222 + ] + ], + "period": 20, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 663, + "maximum_single_tape_extent": 2030, + "moves": 32508, + "page_scans": 2, + "peak_scalar_bits": 23, + "products": 210, + "reads": 9562, + "roundings": 72, + "setup_divisions": 145, + "setup_entries": 145, + "source_shifts": 72, + "writes": 5516 + }, + "bits": 12, + "gap": "1/8", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + 488, + 4 + ], + [ + 462, + -41 + ], + [ + -136, + 106 + ] + ], + "period": 29, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + }, + { + "bill": { + "additions": 0, + "control_steps": 219, + "maximum_single_tape_extent": 594, + "moves": 4422, + "page_scans": 2, + "peak_scalar_bits": 10, + "products": 0, + "reads": 1320, + "roundings": 6, + "setup_divisions": 54, + "setup_entries": 54, + "source_shifts": 6, + "writes": 891 + }, + "bits": 9, + "gap": "1/4", + "length": 3, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + -25, + -98 + ], + [ + -38, + 37 + ], + [ + 42, + 54 + ] + ], + "period": 18, + "resident_extents": [ + 66, + 99, + 66, + 0 + ], + "terms": 1, + "width": 1 + }, + { + "bill": { + "additions": 30, + "control_steps": 439, + "maximum_single_tape_extent": 1380, + "moves": 12456, + "page_scans": 2, + "peak_scalar_bits": 19, + "products": 30, + "reads": 3612, + "roundings": 20, + "setup_divisions": 115, + "setup_entries": 115, + "source_shifts": 20, + "writes": 2448 + }, + "bits": 10, + "gap": "3/8", + "length": 3, + "lower": 20, + "nonzero_error": true, + "output": [ + [ + -200, + -33 + ], + [ + -39, + 138 + ], + [ + -165, + -32 + ] + ], + "period": 23, + "resident_extents": [ + 168, + 420, + 72, + 168 + ], + "terms": 2, + "width": 2 + }, + { + "bill": { + "additions": 48, + "control_steps": 191, + "maximum_single_tape_extent": 741, + "moves": 8632, + "page_scans": 1, + "peak_scalar_bits": 21, + "products": 48, + "reads": 2145, + "roundings": 30, + "setup_divisions": 57, + "setup_entries": 57, + "source_shifts": 30, + "writes": 1976 + }, + "bits": 11, + "gap": "1/8", + "length": 3, + "lower": 8, + "nonzero_error": true, + "output": [ + [ + -38, + -416 + ], + [ + -142, + -20 + ], + [ + 300, + 45 + ] + ], + "period": 19, + "resident_extents": [ + 182, + 273, + 182, + 130 + ], + "terms": 3, + "width": 1 + }, + { + "bill": { + "additions": 210, + "control_steps": 645, + "maximum_single_tape_extent": 1960, + "moves": 32088, + "page_scans": 2, + "peak_scalar_bits": 23, + "products": 210, + "reads": 9422, + "roundings": 72, + "setup_divisions": 140, + "setup_entries": 140, + "source_shifts": 72, + "writes": 5446 + }, + "bits": 12, + "gap": "1/4", + "length": 3, + "lower": 1, + "nonzero_error": true, + "output": [ + [ + -313, + 436 + ], + [ + -419, + -45 + ], + [ + -133, + 210 + ] + ], + "period": 28, + "resident_extents": [ + 420, + 1050, + 308, + 420 + ], + "terms": 4, + "width": 2 + } + ], + "finite_lines": 32, + "finite_target_outputs": 96, + "gaussian": { + "checked_off_band_entries": 1240, + "dropped_wrap_detected": true, + "gap": "65413/65536", + "holes": [ + 2, + 7, + 12, + 17, + 22, + 27, + 32, + 37 + ], + "lines": [ + { + "bill": { + "additions": 702, + "control_steps": 1219, + "maximum_single_tape_extent": 7830, + "moves": 166440, + "page_scans": 2, + "peak_scalar_bits": 55, + "products": 702, + "reads": 57570, + "roundings": 136, + "setup_divisions": 0, + "setup_entries": 0, + "source_shifts": 136, + "writes": 17730 + }, + "lower": -2, + "nonzero_error": true, + "output": [ + [ + 44823113, + 19209557 + ], + [ + -44739418, + -19173813 + ], + [ + -44739242, + 19173961 + ], + [ + 44739406, + -19174022 + ], + [ + 44739259, + 19173950 + ] + ], + "resident_extents": [ + 1740, + 7830, + 1260, + 1740 + ] + }, + { + "bill": { + "additions": 702, + "control_steps": 1219, + "maximum_single_tape_extent": 7830, + "moves": 166440, + "page_scans": 2, + "peak_scalar_bits": 55, + "products": 702, + "reads": 57570, + "roundings": 136, + "setup_divisions": 0, + "setup_entries": 0, + "source_shifts": 136, + "writes": 17730 + }, + "lower": 5, + "nonzero_error": true, + "output": [ + [ + 44739285, + -19173933 + ], + [ + -44739449, + 19173994 + ], + [ + 44739302, + -19173922 + ], + [ + 44822858, + 19209723 + ], + [ + -44739475, + -19173978 + ] + ], + "resident_extents": [ + 1740, + 7830, + 1260, + 1740 + ] + }, + { + "bill": { + "additions": 702, + "control_steps": 819, + "maximum_single_tape_extent": 7830, + "moves": 144840, + "page_scans": 1, + "peak_scalar_bits": 55, + "products": 702, + "reads": 46770, + "roundings": 136, + "setup_divisions": 0, + "setup_entries": 0, + "source_shifts": 136, + "writes": 17730 + }, + "lower": 18, + "nonzero_error": true, + "output": [ + [ + -44822943, + 19209668 + ], + [ + 44739247, + -19173923 + ], + [ + 44739412, + 19173851 + ], + [ + -44739577, + -19173912 + ], + [ + 44739429, + 19173840 + ] + ], + "resident_extents": [ + 1740, + 7830, + 1260, + 1740 + ] + } + ], + "nonzero_wrap_entries": 2, + "numerical_bound": "11/267931648", + "original_matrix_entries": 1600, + "period": 40, + "setup": { + "band_source_calls": 360, + "kernel_error_bits": 68, + "maximum_rational_height": 175, + "parameters": [ + 32, + 8, + 2, + 1, + 8, + 32 + ], + "production_bill": { + "additions": 0, + "control_steps": 400, + "maximum_single_tape_extent": 10800, + "moves": 21600, + "page_scans": 0, + "peak_scalar_bits": 0, + "products": 0, + "reads": 0, + "roundings": 0, + "setup_divisions": 360, + "setup_entries": 360, + "source_shifts": 0, + "writes": 10800 + }, + "reference_sha256": "1c9678360096d96f71a01153d8ef51ce2b53b5fe2b1f2d35f7b0f6de9d1f9a85", + "stored_coefficient_height": 140, + "stored_entries": 360, + "stored_kernels": 1, + "stored_weights": 32, + "table_bits": 10800, + "weight_precision": 71 + }, + "tail_bound": "228886641/36824245303148281856", + "target_bits": 20, + "tensor": { + "axis_receipts": [ + { + "axis": 0, + "input_lines": 27, + "line_length": 28, + "output_records": 108, + "page_scans": 2, + "products": 17496, + "radix_passes": 10, + "target_length": 4 + }, + { + "axis": 1, + "input_lines": 4, + "line_length": 27, + "output_records": 12, + "page_scans": 2, + "products": 2376, + "radix_passes": 10, + "target_length": 3 + } + ], + "bill": { + "additions": 19872, + "control_steps": 39124, + "maximum_single_tape_extent": 52920, + "moves": 11240280, + "page_scans": 4, + "peak_scalar_bits": 54, + "products": 19872, + "reads": 2398440, + "roundings": 3936, + "setup_divisions": 720, + "setup_entries": 720, + "source_shifts": 3936, + "writes": 2976180 + }, + "copied_records": 756, + "dimensions": 2, + "fixed_local_tape_roles": 8, + "key_width": 10, + "label": "actual-reference-2d", + "nonzero_error": true, + "numerical_bound": "11/133965824", + "output": [ + [ + [ + -1, + 5 + ], + [ + -16563329, + -11064879 + ] + ], + [ + [ + -1, + 6 + ], + [ + -16561022, + -11063579 + ] + ], + [ + [ + -1, + 7 + ], + [ + -16558485, + -11062163 + ] + ], + [ + [ + 0, + 5 + ], + [ + -16770857, + -11181245 + ] + ], + [ + [ + 0, + 6 + ], + [ + -16768550, + -11179945 + ] + ], + [ + [ + 0, + 7 + ], + [ + -16766014, + -11178529 + ] + ], + [ + [ + 1, + 5 + ], + [ + -16770410, + -11180988 + ] + ], + [ + [ + 1, + 6 + ], + [ + -16768103, + -11179688 + ] + ], + [ + [ + 1, + 7 + ], + [ + -16765566, + -11178272 + ] + ], + [ + [ + 2, + 5 + ], + [ + -16769819, + -11180663 + ] + ], + [ + [ + 2, + 6 + ], + [ + -16767512, + -11179363 + ] + ], + [ + [ + 2, + 7 + ], + [ + -16764976, + -11177947 + ] + ] + ], + "protected_archive_bits": 21600, + "role_extents": [ + [ + "rectangle current", + 52920 + ], + [ + "rectangle next", + 7560 + ], + [ + "radix zero", + 31360 + ], + [ + "radix one", + 26460 + ], + [ + "fixed borrowed line", + 1680 + ], + [ + "fixed iterate zero", + 1680 + ], + [ + "fixed iterate one", + 1200 + ], + [ + "fixed local band page", + 7560 + ] + ], + "saved_lengths": [ + 28, + 27 + ], + "source_setup": { + "kernel_error_bits": 68, + "maximum_rational_height": 175, + "parameters": [ + 32, + 8, + 2, + 1, + 8, + 32 + ], + "reference_sha256": "1c9678360096d96f71a01153d8ef51ce2b53b5fe2b1f2d35f7b0f6de9d1f9a85", + "stored_entries": 360, + "stored_kernels": 1, + "stored_weights": 32, + "weight_precision": 71 + }, + "target_records": 12, + "total_retained_local_bits": 130420 + } + }, + "no_new_kappa": true, + "nonzero_rounding_lines": 32, + "program_sha256": { + "engine.py": "38ca22b213a0291cc7ba821baf513db289c1c3e7c24c579c5eff3349280484b2", + "source.py": "20c0fb2e4aa95de976ef6ce74ded4bf1cb9073732eca7eda8f61e45d239afa2c", + "tensor.py": "b3cfe3c18988a89d4a639e8104db7a87f7029d556c74c2e0f60d687ec6be5e80", + "verify.py": "9263a65f31d75f0f53d6acb2219781ee3b48a56fe08963716f104890ea5945f5" + }, + "rectangle_reuse": { + "constructors_sealed_during_calls": true, + "fixed_role_count": 8, + "history": [ + { + "archive_scans": 3, + "copied_records": 81, + "moves": 582456, + "output": [ + [ + [ + -1, + 4 + ], + [ + 12, + -25 + ] + ], + [ + [ + -1, + 5 + ], + [ + 20, + -23 + ] + ], + [ + [ + -1, + 6 + ], + [ + 28, + -20 + ] + ], + [ + [ + -1, + 7 + ], + [ + 39, + -28 + ] + ], + [ + [ + -1, + 8 + ], + [ + 50, + -27 + ] + ], + [ + [ + 0, + 4 + ], + [ + -32, + -27 + ] + ], + [ + [ + 0, + 5 + ], + [ + -24, + -25 + ] + ], + [ + [ + 0, + 6 + ], + [ + -16, + -23 + ] + ], + [ + [ + 0, + 7 + ], + [ + -8, + -22 + ] + ], + [ + [ + 0, + 8 + ], + [ + 0, + -22 + ] + ], + [ + [ + 1, + 4 + ], + [ + -35, + -19 + ] + ], + [ + [ + 1, + 5 + ], + [ + -27, + -17 + ] + ], + [ + [ + 1, + 6 + ], + [ + -19, + -15 + ] + ], + [ + [ + 1, + 7 + ], + [ + -10, + -13 + ] + ], + [ + [ + 1, + 8 + ], + [ + -3, + -12 + ] + ], + [ + [ + 2, + 4 + ], + [ + -31, + -10 + ] + ], + [ + [ + 2, + 5 + ], + [ + -23, + -8 + ] + ], + [ + [ + 2, + 6 + ], + [ + -15, + -6 + ] + ], + [ + [ + 2, + 7 + ], + [ + -7, + -4 + ] + ], + [ + [ + 2, + 8 + ], + [ + 0, + -3 + ] + ], + [ + [ + 3, + 4 + ], + [ + -28, + -1 + ] + ], + [ + [ + 3, + 5 + ], + [ + -19, + 0 + ] + ], + [ + [ + 3, + 6 + ], + [ + -11, + 1 + ] + ], + [ + [ + 3, + 7 + ], + [ + -3, + 3 + ] + ], + [ + [ + 3, + 8 + ], + [ + 4, + 6 + ] + ], + [ + [ + 4, + 4 + ], + [ + -24, + 6 + ] + ], + [ + [ + 4, + 5 + ], + [ + -16, + 8 + ] + ], + [ + [ + 4, + 6 + ], + [ + -8, + 10 + ] + ], + [ + [ + 4, + 7 + ], + [ + 0, + 13 + ] + ], + [ + [ + 4, + 8 + ], + [ + 8, + 16 + ] + ], + [ + [ + 5, + 4 + ], + [ + -20, + 15 + ] + ], + [ + [ + 5, + 5 + ], + [ + -12, + 17 + ] + ], + [ + [ + 5, + 6 + ], + [ + -4, + 19 + ] + ], + [ + [ + 5, + 7 + ], + [ + 3, + 22 + ] + ], + [ + [ + 5, + 8 + ], + [ + 12, + 25 + ] + ] + ], + "retained_bits": 8988, + "saved_lengths": [ + 9, + 9 + ], + "target_records": 35, + "writes": 181088 + }, + { + "archive_scans": 3, + "copied_records": 18, + "moves": 66468, + "output": [ + [ + [ + 8, + -1 + ], + [ + -44, + -7 + ] + ], + [ + [ + 8, + 0 + ], + [ + -33, + 28 + ] + ] + ], + "retained_bits": 8988, + "saved_lengths": [ + 3, + 6 + ], + "target_records": 2, + "writes": 18956 + }, + { + "archive_scans": 3, + "copied_records": 77, + "moves": 472446, + "output": [ + [ + [ + 1, + 9 + ], + [ + 4, + -10 + ] + ], + [ + [ + 1, + 10 + ], + [ + 13, + -7 + ] + ], + [ + [ + 1, + 11 + ], + [ + 21, + -5 + ] + ], + [ + [ + 1, + 12 + ], + [ + 29, + -3 + ] + ], + [ + [ + 1, + 13 + ], + [ + 37, + -1 + ] + ], + [ + [ + 1, + 14 + ], + [ + 45, + 0 + ] + ], + [ + [ + 1, + 15 + ], + [ + 52, + 2 + ] + ], + [ + [ + 2, + 9 + ], + [ + 8, + 0 + ] + ], + [ + [ + 2, + 10 + ], + [ + 16, + 0 + ] + ], + [ + [ + 2, + 11 + ], + [ + 24, + 2 + ] + ], + [ + [ + 2, + 12 + ], + [ + 32, + 5 + ] + ], + [ + [ + 2, + 13 + ], + [ + 40, + 6 + ] + ], + [ + [ + 2, + 14 + ], + [ + 48, + 8 + ] + ], + [ + [ + 2, + 15 + ], + [ + 56, + 10 + ] + ], + [ + [ + 3, + 9 + ], + [ + 12, + 7 + ] + ], + [ + [ + 3, + 10 + ], + [ + 20, + 9 + ] + ], + [ + [ + 3, + 11 + ], + [ + 28, + 11 + ] + ], + [ + [ + 3, + 12 + ], + [ + 36, + 13 + ] + ], + [ + [ + 3, + 13 + ], + [ + 44, + 15 + ] + ], + [ + [ + 3, + 14 + ], + [ + 52, + 17 + ] + ], + [ + [ + 3, + 15 + ], + [ + 61, + 19 + ] + ], + [ + [ + 4, + 9 + ], + [ + 16, + 16 + ] + ], + [ + [ + 4, + 10 + ], + [ + 23, + 18 + ] + ], + [ + [ + 4, + 11 + ], + [ + 31, + 20 + ] + ], + [ + [ + 4, + 12 + ], + [ + 39, + 21 + ] + ], + [ + [ + 4, + 13 + ], + [ + 48, + 24 + ] + ], + [ + [ + 4, + 14 + ], + [ + 55, + 26 + ] + ], + [ + [ + 4, + 15 + ], + [ + 72, + 20 + ] + ], + [ + [ + 5, + 9 + ], + [ + 19, + 26 + ] + ], + [ + [ + 5, + 10 + ], + [ + 27, + 19 + ] + ], + [ + [ + 5, + 11 + ], + [ + 35, + 21 + ] + ], + [ + [ + 5, + 12 + ], + [ + 43, + 23 + ] + ], + [ + [ + 5, + 13 + ], + [ + 51, + 25 + ] + ], + [ + [ + 5, + 14 + ], + [ + 60, + 31 + ] + ], + [ + [ + 5, + 15 + ], + [ + 60, + -30 + ] + ] + ], + "retained_bits": 9204, + "saved_lengths": [ + 7, + 11 + ], + "target_records": 35, + "writes": 145378 + } + ] + }, + "schema_version": 1, + "seed": 72, + "source_sha256": { + "research/certified-gaussian-recovery/NOTICE.md": "10acae9e78402ca70c6afd0e8d6da8fefc0da519c646cf43d93f923aba85b86d", + "research/certified-gaussian-recovery/intervals.py": "159d2a7d32a8cc7c8f56632a8ef127308b984a0a6753c9d6bdccacc6e7d6d4df", + "research/rational-unitary-fft/RAW-GAUSSIAN-PROOF.md": "3f683643a0c0b45d58ec09ebe511e4006cd103e38753f82a4ce21a8570383358", + "research/rational-unitary-fft/exact.py": "c9b89d7357210af69865690ba12e695366961f8b501a8fab9d0fefe3fb30c479", + "research/rational-unitary-fft/gaussian.py": "08155357fd39b5fd7959f51f1d205b6511b8577b51520d793c89f92368b399ab", + "research/rational-unitary-fft/gaussian_reference.py": "ed4d0908646e391d4a0ea32c988a0301a1793a72294ac7058a664ed3283ca3c3", + "research/unconditional-batched-crt/GAUSSIAN.md": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242", + "research/unconditional-batched-crt/HALO.md": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc", + "research/unconditional-batched-crt/PROOF.md": "689fc7b01c5f04f77019ff02d1b79cb4f7020bd98e05b1052020bad295dec060" + }, + "tensors": [ + { + "axis_receipts": [ + { + "axis": 0, + "input_lines": 6, + "line_length": 4, + "output_records": 12, + "page_scans": 2, + "products": 72, + "radix_passes": 5, + "target_length": 2 + }, + { + "axis": 1, + "input_lines": 2, + "line_length": 6, + "output_records": 4, + "page_scans": 2, + "products": 72, + "radix_passes": 5, + "target_length": 2 + } + ], + "bill": { + "additions": 144, + "control_steps": 1226, + "maximum_single_tape_extent": 792, + "moves": 103200, + "page_scans": 4, + "peak_scalar_bits": 18, + "products": 144, + "reads": 19976, + "roundings": 120, + "setup_divisions": 66, + "setup_entries": 66, + "source_shifts": 120, + "writes": 30904 + }, + "copied_records": 24, + "dimensions": 2, + "fixed_local_tape_roles": 8, + "key_width": 5, + "label": "signed-2d", + "nonzero_error": true, + "numerical_bound": "25/768", + "output": [ + [ + [ + -1, + 9 + ], + [ + 23, + -9 + ] + ], + [ + [ + -1, + 10 + ], + [ + -16, + 9 + ] + ], + [ + [ + 0, + 9 + ], + [ + -11, + 8 + ] + ], + [ + [ + 0, + 10 + ], + [ + 1, + 6 + ] + ] + ], + "protected_archive_bits": 792, + "role_extents": [ + [ + "rectangle current", + 696 + ], + [ + "rectangle next", + 348 + ], + [ + "radix zero", + 464 + ], + [ + "radix one", + 348 + ], + [ + "fixed borrowed line", + 144 + ], + [ + "fixed iterate zero", + 144 + ], + [ + "fixed iterate one", + 96 + ], + [ + "fixed local band page", + 216 + ] + ], + "saved_lengths": [ + 4, + 6 + ], + "target_records": 4, + "total_retained_local_bits": 2456 + }, + { + "axis_receipts": [ + { + "axis": 0, + "input_lines": 24, + "line_length": 4, + "output_records": 48, + "page_scans": 2, + "products": 288, + "radix_passes": 7, + "target_length": 2 + }, + { + "axis": 1, + "input_lines": 8, + "line_length": 6, + "output_records": 16, + "page_scans": 2, + "products": 288, + "radix_passes": 7, + "target_length": 2 + }, + { + "axis": 2, + "input_lines": 4, + "line_length": 4, + "output_records": 8, + "page_scans": 2, + "products": 48, + "radix_passes": 7, + "target_length": 2 + } + ], + "bill": { + "additions": 624, + "control_steps": 5151, + "maximum_single_tape_extent": 2976, + "moves": 559200, + "page_scans": 6, + "peak_scalar_bits": 18, + "products": 624, + "reads": 102260, + "roundings": 528, + "setup_divisions": 99, + "setup_entries": 99, + "source_shifts": 528, + "writes": 174220 + }, + "copied_records": 96, + "dimensions": 3, + "fixed_local_tape_roles": 8, + "key_width": 7, + "label": "signed-3d", + "nonzero_error": true, + "numerical_bound": "65/1536", + "output": [ + [ + [ + -1, + 9, + -1 + ], + [ + -3, + 0 + ] + ], + [ + [ + -1, + 9, + 0 + ], + [ + -1, + 0 + ] + ], + [ + [ + -1, + 10, + -1 + ], + [ + -1, + -1 + ] + ], + [ + [ + -1, + 10, + 0 + ], + [ + 3, + 0 + ] + ], + [ + [ + 0, + 9, + -1 + ], + [ + -1, + 2 + ] + ], + [ + [ + 0, + 9, + 0 + ], + [ + 2, + -2 + ] + ], + [ + [ + 0, + 10, + -1 + ], + [ + 6, + 1 + ] + ], + [ + [ + 0, + 10, + 0 + ], + [ + -3, + 1 + ] + ] + ], + "protected_archive_bits": 1188, + "role_extents": [ + [ + "rectangle current", + 2976 + ], + [ + "rectangle next", + 1488 + ], + [ + "radix zero", + 1984 + ], + [ + "radix one", + 1488 + ], + [ + "fixed borrowed line", + 144 + ], + [ + "fixed iterate zero", + 144 + ], + [ + "fixed iterate one", + 96 + ], + [ + "fixed local band page", + 216 + ] + ], + "saved_lengths": [ + 4, + 6, + 4 + ], + "target_records": 8, + "total_retained_local_bits": 8536 + } + ] +} diff --git a/research/shrinking-reference-halo/SOURCES.json b/research/shrinking-reference-halo/SOURCES.json new file mode 100644 index 0000000000..2e7ea79dae --- /dev/null +++ b/research/shrinking-reference-halo/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "research/rational-unitary-fft/exact.py", + "usage": "input", + "git_blob": "aae41e6acfb2e5a4fafdd85727891eb746b57b42", + "sha256": "c9b89d7357210af69865690ba12e695366961f8b501a8fab9d0fefe3fb30c479" + }, + { + "path": "research/rational-unitary-fft/gaussian.py", + "usage": "input", + "git_blob": "52ad2e1d605f5f7d669234567c25bc087306dd44", + "sha256": "08155357fd39b5fd7959f51f1d205b6511b8577b51520d793c89f92368b399ab" + }, + { + "path": "research/rational-unitary-fft/gaussian_reference.py", + "usage": "input", + "git_blob": "92addfabde50655cea7ad5a84cca9cff5457adee", + "sha256": "ed4d0908646e391d4a0ea32c988a0301a1793a72294ac7058a664ed3283ca3c3" + }, + { + "path": "research/rational-unitary-fft/RAW-GAUSSIAN-PROOF.md", + "usage": "input", + "git_blob": "1fb549d24a419abb50f5b772437d87e48c65fe06", + "sha256": "3f683643a0c0b45d58ec09ebe511e4006cd103e38753f82a4ce21a8570383358" + }, + { + "path": "research/certified-gaussian-recovery/intervals.py", + "usage": "input", + "git_blob": "91d458865aa026bdf0d59653a4ecbfe3a178ecbc", + "sha256": "159d2a7d32a8cc7c8f56632a8ef127308b984a0a6753c9d6bdccacc6e7d6d4df" + }, + { + "path": "research/certified-gaussian-recovery/NOTICE.md", + "usage": "input", + "git_blob": "5e3269b5afe5e11f044ffae45216c4731b42c7af", + "sha256": "10acae9e78402ca70c6afd0e8d6da8fefc0da519c646cf43d93f923aba85b86d" + }, + { + "path": "research/unconditional-batched-crt/HALO.md", + "usage": "input", + "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b", + "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc" + }, + { + "path": "research/unconditional-batched-crt/PROOF.md", + "usage": "input", + "git_blob": "406eb561cc8d6041ea3fba1a849653b654f2198c", + "sha256": "689fc7b01c5f04f77019ff02d1b79cb4f7020bd98e05b1052020bad295dec060" + }, + { + "path": "research/unconditional-batched-crt/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + } + ] +} diff --git a/research/shrinking-reference-halo/TASK.json b/research/shrinking-reference-halo/TASK.json new file mode 100644 index 0000000000..5e72703263 --- /dev/null +++ b/research/shrinking-reference-halo/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "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": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "A source-bound local shrinking-domain normalized inverse tensor consumer on fixed sequential tape roles, with coefficient/data error, original reference-band production, full archive access, physical sparse axis exposure and complete generic/production cost.", + "scope_change_reason": "Direct degree specialization and generic Horner stability are already proved. Follow the remaining global coefficient-page and physical local consumer obligation of #6880 and the host-array service boundary of #5159; retain all original Gaussian and outer assumptions.", + "bottleneck_link": "Constructs one analytic_recovery/precision_tape component using the actual rational Gaussian Reference without a global polynomial-row oracle. Does not discharge either complete selected assumption.", + "budget_minutes": 180, + "stop_rule": "Stop at the verified local consumer and its complete cost. No scalar degree retuning, source analytic reproof, independent supplier admission or speculative outer theorem claim.", + "outcome": "completed", + "evidence": "PROOF.md; engine.py/source.py/tensor.py; exact typed RESULT.json; independently developed original-inverse rational elimination and all-row residual certificates; six successful normal and optimized registered replays; predecessor overlap sources.", + "author": "CubeJerry", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, source analysis, implementation, exact verification and separate adversarial AI review.", + "open_questions": [ + { + "question": "Can this local consumer be joined to the actual first-face gather and unique-return transaction?", + "why_it_matters": "Its saved rectangle must contain original values before core mutation, and every returned target key must be consumed exactly once.", + "first_step": "Bind one wrapping/hole rectangle codec and q-grid on both sides, then prove and execute the complete group transaction.", + "blocked_by": "The dense-source copy/return chronology and actual outer ownership interface are outside this package." + }, + { + "question": "Can the same fixed reference and normalizer be admitted at the finite core and outer recovery?", + "why_it_matters": "Similar Gaussian terminology does not make different rounded matrices or all-input error contracts interchangeable.", + "first_step": "Pin the exact core reference and actual-input theorem, then substitute the complete tensor error in the existing recovery ledger.", + "blocked_by": "Finite core adoption, source compatibility and full outer multiplier admission remain unproved here." + } + ] +} diff --git a/research/shrinking-reference-halo/VERIFY.json b/research/shrinking-reference-halo/VERIFY.json new file mode 100644 index 0000000000..1345ca68ab --- /dev/null +++ b/research/shrinking-reference-halo/VERIFY.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/rational-unitary-fft/exact.py", + "research/rational-unitary-fft/gaussian.py", + "research/rational-unitary-fft/gaussian_reference.py", + "research/rational-unitary-fft/RAW-GAUSSIAN-PROOF.md", + "research/certified-gaussian-recovery/intervals.py", + "research/certified-gaussian-recovery/NOTICE.md", + "research/unconditional-batched-crt/HALO.md", + "research/unconditional-batched-crt/PROOF.md", + "research/unconditional-batched-crt/GAUSSIAN.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact source-band line/tensor proof obligations, all forty-row reference entries, fixed-role history, complete physical invoices and negative controls; typed mandatory receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "The identical exact source-bound consumer, ownership histories and rejection controls with assertions disabled." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent_inverse.py" + ], + "timeout_seconds": 180, + "checks": "Separate exact original-matrix inverse-row elimination and physical two-axis tensor execution, sealed fixed-role reuse and wrong-target control. Normal replay." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent_inverse.py" + ], + "timeout_seconds": 180, + "checks": "Separate exact original-matrix inverse-row elimination and physical two-axis tensor execution, sealed fixed-role reuse and wrong-target control. Assertions-disabled replay." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent_residual.py" + ], + "timeout_seconds": 120, + "checks": "Separate all-forty-row original-reference residual certificate and wrong-return-order lower bound, without the author polynomial verifier. Normal replay." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent_residual.py" + ], + "timeout_seconds": 120, + "checks": "Separate all-forty-row original-reference residual certificate and wrong-return-order lower bound, without the author polynomial verifier. Assertions-disabled replay." + } + ] +} diff --git a/research/shrinking-reference-halo/engine.py b/research/shrinking-reference-halo/engine.py new file mode 100644 index 0000000000..984dffee3f --- /dev/null +++ b/research/shrinking-reference-halo/engine.py @@ -0,0 +1,385 @@ +"""Sequential shrinking-domain normalized inverse action. + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +Classical fixed-source Horner iteration is inherited; this file supplies the +local shrinking domains, sequential band-page extraction and ownership trace. +Bit-tape movement is executed. Bounded integer arithmetic is a declared scalar +macro, with its ordinary schoolbook bit cost established in PROOF.md. +""" +from dataclasses import dataclass, field +from fractions import Fraction as Q +from hashlib import sha256 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def trunc(n, denominator): + need(type(n) is int and type(denominator) is int and denominator > 0, + "integer truncation domain") + return (-1 if n < 0 else 1) * (abs(n) // denominator) + + +def inward(value, bits): + value = Q(value) + return trunc(value.numerator << bits, value.denominator) + + +@dataclass +class Bill: + reads: int = 0 + writes: int = 0 + moves: int = 0 + products: int = 0 + additions: int = 0 + roundings: int = 0 + source_shifts: int = 0 + control_steps: int = 0 + peak_scalar_bits: int = 0 + setup_entries: int = 0 + setup_divisions: int = 0 + page_scans: int = 0 + maximum_single_tape_extent: int = 0 + + def scalar(self, *values): + self.peak_scalar_bits = max(self.peak_scalar_bits, + *(abs(x).bit_length() + 1 for x in values)) + + def record(self): + return {name: getattr(self, name) for name in self.__dataclass_fields__} + + +class Tape: + """Binary tape; data may be accessed only at the current head. + + The host list implements tape cells, not a program-visible indexed array. + snapshot() is an independent diagnostic, never a transition primitive. + Blank cells are zero. Every cell beyond live_bits is already blank. Clear + erases the complete current live body; retained blank backing stays paid + in space but need not be erased again for every later shorter line. + """ + def __init__(self, bill, name): + self._cells = [] + self.head = 0 + self.live_bits = 0 + self.bill = bill + self.name = name + self.readonly = False + + @property + def extent(self): + return len(self._cells) + + def read(self): + need(self.head < self.live_bits, "read beyond live encoded body") + self.bill.reads += 1 + return self._cells[self.head] if self.head < self.extent else 0 + + def write(self, bit): + need(not self.readonly, "write to borrowed immutable tape") + need(type(bit) is int and bit in (0, 1), "binary cell") + if self.head >= self.extent: + self._cells.extend([0] * (self.head + 1 - self.extent)) + self._cells[self.head] = bit + self.live_bits = max(self.live_bits, self.head + 1) + self.bill.writes += 1 + self.bill.maximum_single_tape_extent = max(self.bill.maximum_single_tape_extent, self.extent) + + def step(self, direction): + need(type(direction) is int and direction in (-1, 1), "one-cell head move") + need(self.head + direction >= 0, "left tape boundary") + self.head += direction + self.bill.moves += 1 + + def walk(self, distance): + need(type(distance) is int, "encoded head displacement") + direction = -1 if distance < 0 else 1 + for _ in range(abs(distance)): + self.step(direction) + + def rewind(self): + self.walk(-self.head) + + def clear(self): + need(not self.readonly, "clear borrowed immutable tape") + self.rewind() + occupied = self.live_bits + for _ in range(occupied): + self.write(0) + self.step(1) + self.rewind() + self.live_bits = 0 + + def snapshot(self): + return bytes(self._cells) + + +def put_int(tape, value, width): + need(type(value) is int and type(width) is int and width >= 2, + "fixed-width integer") + need(abs(value) < (1 << (width - 1)), "integer carrier overflow") + tape.write(int(value < 0)); tape.step(1) + for shift in range(width - 2, -1, -1): + tape.write((abs(value) >> shift) & 1); tape.step(1) + + +def get_int(tape, width): + sign = tape.read(); tape.step(1) + magnitude = 0 + for _ in range(width - 1): + magnitude = 2 * magnitude + tape.read(); tape.step(1) + need(not (sign and magnitude == 0), "noncanonical negative zero") + return -magnitude if sign else magnitude + + +def put_complex(tape, value, width): + need(type(value) is tuple and len(value) == 2, "signed complex pair") + put_int(tape, value[0], width); put_int(tape, value[1], width) + + +def get_complex(tape, width): + return get_int(tape, width), get_int(tape, width) + + +@dataclass(frozen=True) +class Plan: + period: int + halfwidth: int + bits: int + terms: int + normalizer_shift: int + gap: Q + radius: int = 1 + + def __post_init__(self): + need(all(type(x) is int for x in (self.period, self.halfwidth, self.bits, + self.terms, self.normalizer_shift, self.radius)), "integer plan parameters") + need(self.period > 0 and self.halfwidth >= 0 + and 2 * self.halfwidth < self.period, "unique cyclic band offsets") + need(self.bits >= self.normalizer_shift >= 0 and self.terms >= 1 + and self.radius >= 1, "precision, iteration and radius domain") + need(type(self.gap) in (int, Q) and 0 < self.gap <= 1, "positive rational gap") + need((1 << self.normalizer_shift) * self.gap >= 1, "funded normalization") + + @property + def band(self): + return 2 * self.halfwidth + 1 + + @property + def halo(self): + return (self.terms - 1) * self.halfwidth + + @property + def coefficient_width(self): + return self.bits + 2 + + @property + def data_width(self): + return self.bits + self.radius.bit_length() + 1 + + @property + def numeric_error(self): + return Q(self.band * self.radius + 2, 1 << self.bits) / self.gap + + @property + def tail_error(self): + return self.radius * (1 - self.gap) ** self.terms / ( + (1 << self.normalizer_shift) * self.gap) + + +@dataclass(frozen=True) +class Table: + tape: Tape + plan: Plan + source_id: str + + +@dataclass(frozen=True) +class Page: + tape: Tape + plan: Plan + lower: int + length: int + source_id: str + + +@dataclass(frozen=True) +class Output: + tape: Tape + lower: int + length: int + width: int + blank_scratch: tuple = field(repr=False) + + +def prepare_table(plan, entry, source_id, bill): + """entry(row, column) returns the exact fixed E=I-H coefficient. + + Generic entry-production cost remains explicit; source.py provides the + authenticated Gaussian instantiation and its separately charged setup. + All offsets, including zero entries, are generated and stored. + """ + tape = Tape(bill, "global band table") + largest_height = 0 + for row in range(plan.period): + mass = Q(0) + for offset in range(-plan.halfwidth, plan.halfwidth + 1): + value = Q(entry(row, (row + offset) % plan.period)) + largest_height = max(largest_height, abs(value.numerator).bit_length(), + value.denominator.bit_length()) + mass += abs(value) + coefficient = inward(value, plan.bits) + need(abs(Q(coefficient, 1 << plan.bits)) <= abs(value), "inward coefficient") + need(abs(value - Q(coefficient, 1 << plan.bits)) < Q(1, 1 << plan.bits), + "coefficient error") + put_int(tape, coefficient, plan.coefficient_width) + bill.setup_entries += 1 + bill.setup_divisions += 1 + need(mass <= 1 - plan.gap, "actual source row gap") + bill.control_steps += plan.band + 1 + tape.rewind(); tape.readonly = True + return Table(tape, plan, source_id), largest_height + + +def extract_page(table, lower, length, bill, page_tape=None): + """At most two COMPLETE ordered scans, including all skipped records. + + The lifted interval has length less than the physical period, so each + canonical coordinate appears at most once. A wrapping tail is emitted + before its head. No random seek into the global table is used. + """ + plan = table.plan + need(type(lower) is int and type(length) is int and 0 < length < plan.period, + "nonaliasing lifted page interval") + need(table.tape.head == 0, "global table origin") + # Accounting ownership can change between calls; it is not encoded data. + # Charge the repeated complete scan to THIS call, not to old preparation. + table.tape.bill = bill + start = lower % plan.period + first = min(length, plan.period - start) + spans = [(start, start + first)] + if first < length: + spans.append((0, length - first)) + page = page_tape if page_tape is not None else Tape(bill, "local band page") + need(page.head == 0 and not page.readonly and page.live_bits == 0, + "blank local page role") + page.bill = bill + for begin, end in spans: + for row in range(plan.period): + for _ in range(plan.band): + value = get_int(table.tape, plan.coefficient_width) + if begin <= row < end: + put_int(page, value, plan.coefficient_width) + bill.control_steps += plan.band + 1 + table.tape.rewind() + bill.page_scans += 1 + need(page.head == length * plan.band * plan.coefficient_width, + "complete ordered page") + page.rewind(); page.readonly = True + return Page(page, plan, lower, length, table.source_id) + + +def input_tape(plan, values, bill): + tape = Tape(bill, "borrowed input") + for value in values: + need(type(value) is tuple and len(value) == 2 and + all(type(x) is int for x in value), "integer grid input") + need(abs(value[0]) + abs(value[1]) <= plan.radius * (1 << plan.bits), + "input radius") + put_complex(tape, value, plan.data_width) + tape.rewind(); tape.readonly = True + return tape + + +def apply_line(page, source, target_lower, target_length, bill, workspace=None): + """Return only the target; preserve borrowed input/page and both origins. + + source contains the entire saved dependency interval. All arithmetic is + performed on encoded integer numerators; no Fraction or matrix oracle is + used by the online recurrence. Other tensor coordinates are spectators. + """ + p = page.plan + need(type(target_lower) is int and type(target_length) is int and target_length > 0, + "nonempty target interval") + lower, length = target_lower - p.halo, target_length + 2 * p.halo + need(page.lower == lower and page.length == length, "exact saved dependency domain") + need(length < p.period, "no repeated canonical input coordinate") + need(source.readonly and page.tape.readonly and source.head == page.tape.head == 0, + "immutable origin-aligned input and page") + source.bill = page.tape.bill = bill + record_bits = 2 * p.data_width + need(source.live_bits == length * record_bits, "complete input shape") + if workspace is None: + current, following = Tape(bill, "current iterate"), Tape(bill, "next iterate") + else: + need(type(workspace) is tuple and len(workspace) == 2 + and workspace[0] is not workspace[1], "two distinct fixed iterate roles") + current, following = workspace + need(all(t.head == 0 and not t.readonly and t.live_bits == 0 for t in workspace), + "blank fixed iterate roles") + current.bill = following.bill = bill + scale = 1 << p.bits + # First term z_1=trunc_q(x/a); no E row is needed for this term. + for _ in range(length): + x = get_complex(source, p.data_width) + need(abs(x[0]) + abs(x[1]) <= p.radius * scale, "actual incoming radius") + z = tuple(trunc(v, 1 << p.normalizer_shift) for v in x) + put_complex(current, z, p.data_width) + bill.roundings += 2; bill.source_shifts += 2; bill.control_steps += 1 + bill.scalar(*x, *z) + source.rewind(); current.rewind() + active_lower, active_length = lower, length + for _ in range(1, p.terms): + out_lower, out_length = active_lower + p.halfwidth, active_length - 2 * p.halfwidth + source.walk((out_lower - lower) * record_bits) + page.tape.walk((out_lower - lower) * p.band * p.coefficient_width) + for row in range(out_length): + x = get_complex(source, p.data_width) + real = x[0] << (p.bits - p.normalizer_shift) + imag = x[1] << (p.bits - p.normalizer_shift) + bill.source_shifts += 2 + for _ in range(p.band): + coefficient = get_int(page.tape, p.coefficient_width) + z = get_complex(current, p.data_width) + product_real, product_imag = coefficient * z[0], coefficient * z[1] + real += product_real; imag += product_imag + bill.products += 2; bill.additions += 2; bill.control_steps += 1 + bill.scalar(coefficient, *z, product_real, product_imag, real, imag) + need(abs(real) + abs(imag) <= p.radius * scale * scale, + "partial exact accumulator radius") + result = trunc(real, scale), trunc(imag, scale) + need(abs(result[0]) + abs(result[1]) <= p.radius * scale, + "actual rounded iterate radius") + put_complex(following, result, p.data_width) + bill.roundings += 2; bill.control_steps += 1 + if row + 1 < out_length: + current.walk(-2 * p.halfwidth * record_bits) + need(current.head == active_length * record_bits, "complete neighbor-window traversal") + source.rewind(); page.tape.rewind() + current.clear(); following.rewind() + current, following = following, current + active_lower, active_length = out_lower, out_length + need((active_lower, active_length) == (target_lower, target_length), "target-only return") + need(source.head == page.tape.head == current.head == following.head == 0, + "return origins") + need(following.live_bits == 0, "cleared alternate iterate") + return Output(current, active_lower, active_length, p.data_width, (following,)) + + +def consume(output): + """Caller read, clear and origin restoration; reads only the live prefix. + + An iterate buffer can retain a larger previously occupied blank suffix. + The complete live body is cleared; the suffix is blank by invariant. + """ + need(output.tape.head == 0, "output origin") + result = tuple(get_complex(output.tape, output.width) for _ in range(output.length)) + output.tape.clear() + need(output.tape.head == 0 and output.tape.live_bits == 0, "consumed output cleanup") + return result + + +def tape_digest(tape): + return sha256(tape.snapshot()).hexdigest() diff --git a/research/shrinking-reference-halo/independent_inverse.py b/research/shrinking-reference-halo/independent_inverse.py new file mode 100644 index 0000000000..81f2729b24 --- /dev/null +++ b/research/shrinking-reference-halo/independent_inverse.py @@ -0,0 +1,147 @@ +"""Independent exact inverse-row check of the physical tensor consumer. + +The oracle solves the original rational matrix by Gaussian elimination; +it does not evaluate a Neumann polynomial or a Horner recurrence. +""" +from fractions import Fraction as F +from hashlib import sha256 +import importlib.util +import itertools +import json +from pathlib import Path +import random +import sys + +PACKAGE = Path(__file__).resolve().parent + + +def load(name, file): + spec = importlib.util.spec_from_file_location(name, file) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def inverse_rows(matrix, which): + """Solve H^T v=e_r, with exact rational elimination and residual checks.""" + n = len(matrix) + targets = tuple(sorted(set(which))) + a = [[matrix[j][i] for j in range(n)] + + [F(int(i == r)) for r in targets] for i in range(n)] + for column in range(n): + pivot = next(r for r in range(column, n) if a[r][column]) + a[column], a[pivot] = a[pivot], a[column] + divisor = a[column][column] + a[column] = [v / divisor for v in a[column]] + for row in range(column + 1, n): + factor = a[row][column] + if factor: + a[row] = [x - factor * y for x, y in zip(a[row], a[column])] + result = {} + for index, target in enumerate(targets): + row = [F(0)] * n + for r in range(n - 1, -1, -1): + row[r] = a[r][n + index] - sum(a[r][j] * row[j] for j in range(r + 1, n)) + for c in range(n): + if sum(row[j] * matrix[j][c] for j in range(n)) != int(c == target): + raise AssertionError('exact inverse-row residual') + result[target] = row + return result + + +def main(): + engine = load('shrinking_halo_engine', PACKAGE / 'engine.py') + tensor = load('lead_tensor', PACKAGE / 'tensor.py') + source = load('lead_source', PACKAGE / 'source.py') + raw = source.authenticated_inputs(PACKAGE) + reference = source.make_reference(raw, (32, 8, 2, 1, 8, 32)) + reference.require_narrow_gap() + n = reference.target_size + matrix = [[reference.entry('narrow', r, c).value for c in range(n)] for r in range(n)] + rho = max(sum(abs(F(int(r == c)) - matrix[r][c]) for c in range(n)) for r in range(n)) + gap = F(int((1 - rho) * (1 << 16)), 1 << 16) + shift = 0 + while (1 << shift) * gap < 1: + shift += 1 + plan = engine.Plan(n, 2 * reference.spec.source_halfwidth + 2, 28, 4, shift, gap) + targets = ((-3, 2), (39, 2)) + rows = inverse_rows(matrix, [x % n for lo, count in targets for x in range(lo, lo + count)]) + scale = 1 << plan.bits + rng = random.Random(2026110875) + values = [[(rng.randrange(-8, 9) * (scale // 32), + rng.randrange(-8, 9) * (scale // 32)) for _ in range(n)] for _ in range(n)] + exact = {} + for r, s in itertools.product(*(range(lo, lo + count) for lo, count in targets)): + exact[r, s] = tuple( + sum(rows[r % n][u] * sum(rows[s % n][v] * values[u][v][part] + for v in range(n)) for u in range(n)) / + (scale * (1 << (2 * shift))) for part in (0, 1)) + bill = engine.Bill() + production = source.make_reference(raw, (32, 8, 2, 1, 8, 32)) + + def prepared(): + for _ in range(2): + table, _ = engine.prepare_table( + plan, lambda r, c: source.source_entry(production, r, c), + production.description_hash, bill) + yield table + + archive = tensor.pack_tables(prepared(), bill) + before_archive = engine.tape_digest(archive.tape) + pool = tensor.TensorWorkspace.create(bill) + role_ids = tuple(map(id, pool.roles)) + original_init = engine.Tape.__init__ + + def no_new_tapes(*_args, **_kwargs): + raise AssertionError('new physical role during tensor work or reuse') + + engine.Tape.__init__ = no_new_tapes + observations = [] + outputs = [] + try: + for target in (targets, ((-3, 1), (39, 1))): + layout = tensor.Layout.make(archive.plans, target) + payloads = (values[u % n][v % n] for u, v in itertools.product( + *(range(lo, lo + count) for lo, count in zip(layout.lowers, layout.lengths)))) + incoming = tensor.rectangle_input(layout, payloads, bill, tape=pool.rectangles[0]) + result = tensor.apply_tensor(archive, target, incoming, bill, workspace=pool) + outputs.append(dict(tensor.consume_tensor(result))) + observations.append({'saved_records': layout.volume, 'target_records': result.count, + 'retained_bits': sum(t.extent for t in pool.roles)}) + if tuple(map(id, pool.roles)) != role_ids: + raise AssertionError('workspace roles changed') + if not all(t.head == 0 and t.live_bits == 0 and not any(t.snapshot()) for t in pool.roles): + raise AssertionError('nonblank workspace after return') + if engine.tape_digest(archive.tape) != before_archive or archive.tape.head: + raise AssertionError('borrowed archive changed') + finally: + engine.Tape.__init__ = original_init + bound = 2 * (plan.numeric_error + plan.tail_error) + errors = {} + for key, actual in outputs[0].items(): + error = sum(abs(F(actual[p], scale) - exact[key][p]) for p in (0, 1)) + if error > bound: + raise AssertionError(('exact original tensor inverse', key, str(error), str(bound))) + errors[key] = error + if outputs[1][(-3, 39)] != outputs[0][(-3, 39)]: + raise AssertionError('nested-target or retained-history dependence') + actual = outputs[0][(-3, 39)] + wrong = sum(abs(F(actual[p], scale) - exact[(-2, 40)][p]) for p in (0, 1)) + if wrong <= bound: + raise AssertionError('wrong canonical target key not distinguished') + print('PASS_LEAD_EXACT_TENSOR_INVERSE') + print(json.dumps({'period': n, 'original_entries': n * n, + 'exact_inverse_rows': sorted(rows), 'checked_outputs': len(outputs[0]), + 'maximum_inverse_error': float(max(errors.values())), + 'proved_inverse_error_bound': float(bound), + 'wrong_target_error': float(wrong), + 'fixed_tape_roles': len(pool.roles), 'runs': observations, + 'actual_bit_actions': bill.reads + bill.writes + bill.moves, + 'source_entries': len(production.entries), + 'sha256': {p: sha256((PACKAGE / p).read_bytes()).hexdigest() + for p in ('engine.py', 'tensor.py', 'source.py')}}, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/shrinking-reference-halo/independent_residual.py b/research/shrinking-reference-halo/independent_residual.py new file mode 100644 index 0000000000..e68b361a43 --- /dev/null +++ b/research/shrinking-reference-halo/independent_residual.py @@ -0,0 +1,91 @@ +"""Independent residual certification of the actual Gaussian consumer. + +Uses the author's numerical consumer, but no author's verifier or expected +outputs. The mathematical oracle is an exact original-reference residual. +""" +from fractions import Fraction as F +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import random +import sys + +PACKAGE = Path(__file__).resolve().parent + + +def load(name, file): + spec = importlib.util.spec_from_file_location(name, file) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def main(): + engine = load('lead_halo_engine', PACKAGE/'engine.py') + source = load('lead_halo_source', PACKAGE/'source.py') + raw = source.authenticated_inputs(PACKAGE) + reference = source.make_reference(raw, (32,8,2,1,8,32)) + reference.require_narrow_gap() + n = reference.target_size + H = [[reference.entry('narrow',r,c).value for c in range(n)] for r in range(n)] + E = [[F(int(r==c))-H[r][c] for c in range(n)] for r in range(n)] + rho = max(sum(map(abs,row)) for row in E) + gap = F(int((1-rho)*(1<<16)),1<<16) + shift = 0 + while (1<", + "exec", optimize=0), module.__dict__) + return module + + +def reference_class(raw): + """Rebind only imports, leaving every executed numerical body unchanged. + + gaussian.py also imports a full circuit compiler unused by Reference's + explicit constructor/entry interface. Extract exactly its three named + helpers; no numerical source expression or loop is changed. for_cap is + outside this adapter's domain and is not invoked. + """ + exact_tree = ast.parse(raw[EXACT]) + exact = _module("_shrinking_source_exact", exact_tree.body) + gaussian_tree = ast.parse(raw[GAUSSIAN]) + wanted = {"rational", "load_intervals"} + helpers = [node for node in gaussian_tree.body + if isinstance(node, ast.FunctionDef) and node.name in wanted] + need({node.name for node in helpers} == wanted, "retained Gaussian helper shape") + gaussian = _module("_shrinking_source_gaussian", helpers, + {"Q": Q, "need": need, "sha256": sha256, "sys": sys, + "ModuleType": ModuleType}) + tree = ast.parse(raw[REFERENCE]) + body = [node for node in tree.body if not ( + isinstance(node, ast.ImportFrom) and node.module in ("exact", "gaussian"))] + reference = _module("_shrinking_source_reference", body, + {"Mat": exact.Mat, "ceil_log2": exact.ceil_log2, + "need": exact.need, "INTERVALS": INTERVALS, + "load_intervals": gaussian.load_intervals, + "rational": gaussian.rational}) + return reference.Reference + + +def make_reference(raw, parameters): + return reference_class(raw)(raw, *parameters) + + +def source_entry(reference, row, column): + return Q(int(row == column)) - reference.entry("narrow", row, column).value + + +def source_receipt(reference): + """Diagnostic setup inventory; not an asserted exact Python heap count.""" + values = [entry.value for entry in reference.entries.values()] + weight_values = [value for receipt in reference.weights.values() + for value in receipt.values() if type(value) is Q] + height = max([1] + [max(abs(x.numerator).bit_length(), x.denominator.bit_length()) + for x in values + weight_values]) + return dict(reference_sha256=reference.description_hash, + parameters=list(reference.spec.__dict__.values()), + stored_entries=len(reference.entries), stored_weights=len(reference.weights), + stored_kernels=len(reference.kernel), maximum_rational_height=height, + weight_precision=reference.weight_precision, + kernel_error_bits=reference.kernel_error_bits) + + +def clear_reference(reference): + """Release setup caches; physical erasure is separately charged in proof. + + This does not claim secure zeroization of Python immutable integers. + """ + reference.entries.clear(); reference.weights.clear(); reference.kernel.clear() + for name in ("pi_interval", "root_of_unity"): + function = getattr(reference.exp.oracle, name, None) + if function is not None and hasattr(function, "cache_clear"): + function.cache_clear() diff --git a/research/shrinking-reference-halo/tensor.py b/research/shrinking-reference-halo/tensor.py new file mode 100644 index 0000000000..40e84c41bf --- /dev/null +++ b/research/shrinking-reference-halo/tensor.py @@ -0,0 +1,343 @@ +"""One local sparse rectangle on a fixed pool of sequential tape roles. + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +The full-source gather and the final dense unique-return merge are separate. +""" +from dataclasses import dataclass +import shrinking_halo_engine as M + + +def put_unsigned(tape, value, width): + M.need(type(value) is int and 0 <= value < (1 << width), "unsigned key carrier") + for shift in range(width - 1, -1, -1): + tape.write((value >> shift) & 1); tape.step(1) + + +def get_unsigned(tape, width): + value = 0 + for _ in range(width): + value = 2 * value + tape.read(); tape.step(1) + return value + + +@dataclass(frozen=True) +class Archive: + tape: M.Tape + plans: tuple + source_ids: tuple + + +def pack_tables(tables, bill): + """Consume one prepared axis table at a time into ONE protected archive. + + A generator is sufficient: no simultaneous family of physical axis tapes + is required. Each old table body is erased before advancing the iterator. + The finite tuple of descriptors is charged as an encoded control block. + """ + archive = M.Tape(bill, "global band archive") + plans, source_ids = [], [] + bits = None + for table in tables: + if bits is None: + bits = table.plan.bits + M.need(table.plan.bits == bits and table.tape.head == 0, "common archive grid/origin") + table.tape.bill = bill + for _ in range(table.plan.period * table.plan.band): + coefficient = M.get_int(table.tape, table.plan.coefficient_width) + M.put_int(archive, coefficient, table.plan.coefficient_width) + bill.control_steps += 1 + table.tape.readonly = False; table.tape.clear() + plans.append(table.plan); source_ids.append(table.source_id) + M.need(plans, "nonempty band archive") + archive.rewind(); archive.readonly = True + return Archive(archive, tuple(plans), tuple(source_ids)) + + +def archive_page(archive, axis, lower, length, page_tape, bill): + """One/two full ARCHIVE scans per local axis, never per spectator line.""" + M.need(type(axis) is int and 0 <= axis < len(archive.plans), "archive axis") + p = archive.plans[axis] + M.need(type(lower) is int and type(length) is int and 0 < length < p.period, + "nonaliasing local page") + M.need(archive.tape.head == 0 and archive.tape.readonly, "protected archive origin") + M.need(page_tape.head == 0 and not page_tape.readonly and page_tape.live_bits == 0, + "reusable blank local page") + archive.tape.bill = page_tape.bill = bill + begin = lower % p.period + first = min(length, p.period - begin) + spans = [(begin, begin + first)] + if first < length: + spans.append((0, length - first)) + for begin, end in spans: + for catalog_axis, pp in enumerate(archive.plans): + for row in range(pp.period): + emit = catalog_axis == axis and begin <= row < end + for _ in range(pp.band): + coefficient = M.get_int(archive.tape, pp.coefficient_width) + if emit: + M.put_int(page_tape, coefficient, pp.coefficient_width) + bill.control_steps += pp.band + 1 + archive.tape.rewind(); bill.page_scans += 1 + M.need(page_tape.live_bits == length * p.band * p.coefficient_width, "complete local page") + page_tape.rewind(); page_tape.readonly = True + return M.Page(page_tape, p, lower, length, archive.source_ids[axis]) + + +@dataclass(frozen=True) +class Layout: + targets: tuple + lowers: tuple + lengths: tuple + field_widths: tuple + field_shifts: tuple + key_width: int + data_width: int + bits: int + radius: int + + @classmethod + def make(cls, plans, targets): + M.need(len(plans) == len(targets) and plans, "complete tensor axis metadata") + bits, radius = plans[0].bits, plans[0].radius + M.need(all(p.bits == bits and p.radius == radius for p in plans), + "one incoming/output tensor grid and radius") + lowers, lengths, widths = [], [], [] + for p, target in zip(plans, targets): + M.need(type(target) is tuple and len(target) == 2 and + all(type(x) is int for x in target) and target[1] > 0, "target axis interval") + lo, length = target[0] - p.halo, target[1] + 2 * p.halo + M.need(length < p.period, "each saved axis has unique canonical coordinates") + lowers.append(lo); lengths.append(length); widths.append(max(1, (length - 1).bit_length())) + shifts, total = [0] * len(plans), 0 + for i in range(len(plans) - 1, -1, -1): + shifts[i] = total; total += widths[i] + return cls(tuple(targets), tuple(lowers), tuple(lengths), tuple(widths), tuple(shifts), + total, plans[0].data_width, bits, radius) + + @property + def record_bits(self): + return self.key_width + 2 * self.data_width + + @property + def volume(self): + result = 1 + for length in self.lengths: + result *= length + return result + + def key(self, offsets): + M.need(len(offsets) == len(self.lengths), "complete coordinate tuple") + key = 0 + for offset, length, shift in zip(offsets, self.lengths, self.field_shifts): + M.need(type(offset) is int and 0 <= offset < length, "local coordinate range") + key += offset << shift + return key + + def coordinate(self, key, axis): + return (key >> self.field_shifts[axis]) & ((1 << self.field_widths[axis]) - 1) + + def without_axis(self, key, axis): + mask = ((1 << self.field_widths[axis]) - 1) << self.field_shifts[axis] + return key & ~mask + + +def put_record(tape, key, value, layout): + put_unsigned(tape, key, layout.key_width) + M.put_complex(tape, value, layout.data_width) + + +def get_record(tape, layout): + return get_unsigned(tape, layout.key_width), M.get_complex(tape, layout.data_width) + + +def coordinate_odometer(lengths): + """Metadata convenience; encoded carries are explicitly charged in proof.""" + coordinate = [0] * len(lengths) + while True: + yield tuple(coordinate) + axis = len(lengths) - 1 + while axis >= 0 and coordinate[axis] + 1 == lengths[axis]: + coordinate[axis] = 0; axis -= 1 + if axis < 0: + return + coordinate[axis] += 1 + + +def rectangle_input(layout, values, bill, tape=None): + """Charged codec from lexicographic payload stream, no indexed data lookup.""" + tape = tape if tape is not None else M.Tape(bill, "rectangle current") + M.need(tape.head == 0 and tape.live_bits == 0 and not tape.readonly, "blank reusable rectangle role") + tape.bill = bill + stream = iter(values) + for offsets in coordinate_odometer(layout.lengths): + try: + value = next(stream) + except StopIteration as error: + raise ValueError("incomplete saved rectangle") from error + M.need(type(value) is tuple and len(value) == 2 and all(type(x) is int for x in value) + and abs(value[0]) + abs(value[1]) <= layout.radius * (1 << layout.bits), + "saved rectangle data/radius") + put_record(tape, layout.key(offsets), value, layout) + bill.control_steps += len(layout.lengths) + 1 + try: + next(stream) + except StopIteration: + pass + else: + raise ValueError("extra saved rectangle payload") + tape.rewind() + return tape + + +def expose_axis(current, count, axis, layout, buckets, bill): + """Stable LSD distribution into two fixed buckets, then full concatenation.""" + M.need(current.head == 0 and not current.readonly, "owned rectangle origin") + M.need(current.live_bits == count * layout.record_bits, "complete sparse body") + order = (axis,) + tuple(j for j in range(len(layout.lengths) - 1, -1, -1) if j != axis) + passes = 0 + for field in order: + for bit in range(layout.field_widths[field]): + M.need(all(t.head == 0 and t.live_bits == 0 for t in buckets), + "blank fixed radix buckets") + sizes = [0, 0] + position = layout.field_shifts[field] + bit + for _ in range(count): + key, value = get_record(current, layout) + destination = (key >> position) & 1 + put_record(buckets[destination], key, value, layout) + sizes[destination] += 1 + bill.control_steps += 1 + current.clear() + for bucket, size in zip(buckets, sizes): + bucket.rewind() + for _ in range(size): + key, value = get_record(bucket, layout) + put_record(current, key, value, layout) + bill.control_steps += 1 + bucket.clear() + current.rewind(); passes += 1 + return passes + + +@dataclass(frozen=True) +class TensorOutput: + tape: M.Tape + count: int + layout: Layout + role_extents: tuple + axis_receipts: tuple + blank_roles: tuple + + +@dataclass(frozen=True) +class TensorWorkspace: + rectangles: tuple + buckets: tuple + line_source: M.Tape + iterates: tuple + page: M.Tape + + @classmethod + def create(cls, bill, first_rectangle=None): + first = first_rectangle if first_rectangle is not None else M.Tape(bill, "rectangle current") + return cls((first, M.Tape(bill, "rectangle next")), + (M.Tape(bill, "radix zero"), M.Tape(bill, "radix one")), + M.Tape(bill, "fixed borrowed line"), + (M.Tape(bill, "fixed iterate zero"), M.Tape(bill, "fixed iterate one")), + M.Tape(bill, "fixed local band page")) + + @property + def roles(self): + return self.rectangles + self.buckets + (self.line_source,) + self.iterates + (self.page,) + + +def apply_tensor(archive, targets, source, bill, workspace=None): + """Consume one saved rectangle; return its complete target in lex order. + + There are eight local tape roles, independent of axis count and iteration + count, plus the one protected global archive and bounded scalar/control + tapes. No source/table preparation is repeated inside a spectator line. + """ + layout = Layout.make(archive.plans, targets) + M.need(source.head == 0 and not source.readonly + and source.live_bits == layout.volume * layout.record_bits, "owned complete rectangle") + pool = workspace if workspace is not None else TensorWorkspace.create(bill, source) + roles = pool.roles + M.need(len({id(t) for t in roles}) == 8 and any(t is source for t in pool.rectangles), + "eight distinct fixed roles with designated input") + M.need(all(t is source or (t.head == 0 and t.live_bits == 0 and not t.readonly) for t in roles), + "all noninput fixed roles blank and reusable") + for tape in roles: + tape.bill = bill + current = source + following = pool.rectangles[1] if source is pool.rectangles[0] else pool.rectangles[0] + buckets, line_source, iterates, page_tape = pool.buckets, pool.line_source, pool.iterates, pool.page + count = layout.volume + receipts = [] + for axis, p in enumerate(archive.plans): + start_products, start_scans = bill.products, bill.page_scans + page = archive_page(archive, axis, layout.lowers[axis], layout.lengths[axis], page_tape, bill) + passes = expose_axis(current, count, axis, layout, buckets, bill) + line_length = layout.lengths[axis] + M.need(count % line_length == 0, "complete spectator lines") + lines = count // line_length + target_lower, target_length = layout.targets[axis] + previous_spectator = -1 + for _ in range(lines): + spectator = None + for position in range(line_length): + key, value = get_record(current, layout) + other = layout.without_axis(key, axis) + if spectator is None: + spectator = other + M.need(spectator > previous_spectator, "unique ordered spectator line") + previous_spectator = spectator + M.need(other == spectator and layout.coordinate(key, axis) == position, + "full ordered local dependency line") + M.put_complex(line_source, value, p.data_width) + bill.control_steps += len(layout.lengths) + 1 + line_source.rewind(); line_source.readonly = True + output = M.apply_line(page, line_source, target_lower, target_length, bill, + workspace=iterates) + for offset in range(target_length): + value = M.get_complex(output.tape, p.data_width) + coordinate = target_lower - layout.lowers[axis] + offset + key = spectator | (coordinate << layout.field_shifts[axis]) + put_record(following, key, value, layout) + bill.control_steps += len(layout.lengths) + 1 + output.tape.clear() + line_source.readonly = False; line_source.clear() + current.clear(); following.rewind() + current, following = following, current + page_tape.readonly = False; page_tape.clear() + count = lines * target_length + M.need(current.live_bits == count * layout.record_bits, "exact next tensor rectangle") + receipts.append(dict(axis=axis, input_lines=lines, line_length=line_length, + target_length=target_length, radix_passes=passes, + page_scans=bill.page_scans - start_scans, + products=bill.products - start_products, output_records=count)) + blank = tuple(t for t in roles if t is not current) + M.need(all(t.head == 0 and t.live_bits == 0 for t in blank), + "all nonreturn fixed roles erased") + M.need(current.head == archive.tape.head == 0, "tensor/archive return origins") + return TensorOutput(current, count, layout, + tuple((t.name, t.extent) for t in roles), tuple(receipts), blank) + + +def consume_tensor(output): + """Return lifted coordinates, payloads; consume and clear the live output.""" + layout = output.layout + result = [] + previous = -1 + for _ in range(output.count): + key, value = get_record(output.tape, layout) + M.need(key > previous, "unique lexicographic target key") + previous = key + coordinates = tuple(layout.lowers[i] + layout.coordinate(key, i) + for i in range(len(layout.lengths))) + M.need(all(lo <= x < lo + length for x, (lo, length) in zip(coordinates, layout.targets)), + "target-only tensor output") + result.append((coordinates, value)) + output.tape.clear() + M.need(output.tape.head == 0 and output.tape.live_bits == 0, "tensor return cleanup") + return tuple(result) diff --git a/research/shrinking-reference-halo/verify.py b/research/shrinking-reference-halo/verify.py new file mode 100644 index 0000000000..bde34700a9 --- /dev/null +++ b/research/shrinking-reference-halo/verify.py @@ -0,0 +1,554 @@ +"""Exact, read-only normal/optimized corroboration of the scoped theorem. + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +The dense polynomial oracle forms separate powers, not the online recurrence. +""" +import argparse +from dataclasses import replace +from fractions import Fraction as Q +from hashlib import sha256 +import importlib.util +import itertools +import json +from pathlib import Path +import random +import sys +import types + +PACKAGE = Path(__file__).resolve().parent + + +def load_local(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +M = load_local("shrinking_halo_engine", PACKAGE / "engine.py") +S = load_local("shrinking_halo_source", PACKAGE / "source.py") +T = load_local("shrinking_halo_tensor", PACKAGE / "tensor.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rejected(function, label): + try: + function() + except (ValueError, IndexError): + return label + raise ValueError("negative control accepted: " + label) + + +def pair_norm(value): + return abs(value[0]) + abs(value[1]) + + +def dense_polynomial(matrix, data, terms, normalizer): + """Independent exact mechanism: explicit successive powers and sum.""" + n = len(data) + power = tuple((Q(z[0]), Q(z[1])) for z in data) + total = [list(z) for z in power] + for _ in range(1, terms): + following = [] + for row in range(n): + following.append(tuple(sum((matrix[row][column] * power[column][part] + for column in range(n)), Q(0)) + for part in (0, 1))) + power = tuple(following) + for row in range(n): + for part in (0, 1): + total[row][part] += power[row][part] + return tuple(tuple(value / normalizer for value in z) for z in total) + + +def rounded_global(matrix, data, plan): + """Full-period host comparator, solely to verify exact rounded conformance.""" + n, scale = len(data), 1 << plan.bits + coefficients = [[M.inward(value, plan.bits) for value in row] for row in matrix] + current = [(0, 0)] * n + for _ in range(plan.terms): + current = [tuple(M.trunc((data[row][part] << (plan.bits - plan.normalizer_shift)) + + sum(coefficients[row][column] * current[column][part] + for column in range(n)), scale) + for part in (0, 1)) for row in range(n)] + return tuple(current) + + +def run_line(matrix, data, plan, lower, length, engine=M, table=None, bill=None): + bill = bill or engine.Bill() + table = table or engine.prepare_table(plan, lambda r, c: matrix[r][c], "finite exact E", bill)[0] + before_table = engine.tape_digest(table.tape) + saved_lower, saved_length = lower - plan.halo, length + 2 * plan.halo + page = engine.extract_page(table, saved_lower, saved_length, bill) + values = tuple(data[row % plan.period] for row in range(saved_lower, saved_lower + saved_length)) + source = engine.input_tape(plan, values, bill) + before_source, before_page = engine.tape_digest(source), engine.tape_digest(page.tape) + output = engine.apply_line(page, source, lower, length, bill) + require(output.tape.head == 0 and output.length == length, "owned exact output extent") + physical_extents = (source.extent, page.tape.extent, output.tape.extent, + sum(t.extent for t in output.blank_scratch)) + actual = engine.consume(output) + require(before_source == engine.tape_digest(source) and source.head == 0, + "borrowed input bytes/origin") + require(before_page == engine.tape_digest(page.tape) and page.tape.head == 0, + "borrowed page bytes/origin") + require(before_table == engine.tape_digest(table.tape) and table.tape.head == 0, + "global table bytes/origin") + require(all(t.head == 0 and not any(t.snapshot()) for t in output.blank_scratch), + "alternate backing cleanup") + expected = rounded_global(matrix, data, plan) + require(actual == tuple(expected[row % plan.period] for row in range(lower, lower + length)), + "exact full-period rounded conformance") + rational_data = tuple(tuple(Q(v, 1 << plan.bits) for v in z) for z in data) + exact = dense_polynomial(matrix, rational_data, plan.terms, 1 << plan.normalizer_shift) + error = max(pair_norm(tuple(Q(actual[j][part], 1 << plan.bits) - + exact[(lower + j) % plan.period][part] for part in (0, 1))) + for j in range(length)) + require(error <= plan.numeric_error, "proved coefficient/data bound") + n0 = saved_length + output_counts = [length + 2 * (plan.terms - k) * plan.halfwidth + for k in range(2, plan.terms + 1)] + expected_products = 2 * plan.band * sum(output_counts) + expected_roundings = 2 * (n0 + sum(output_counts)) + require(bill.products == expected_products, "complete multiply invoice") + require(bill.additions == expected_products, "complete accumulation invoice") + require(bill.roundings == expected_roundings, "all completed data roundings") + return actual, error, bill, physical_extents + + +def matrix_cases(): + rng = random.Random(72) + cases = [] + for case in range(32): + width = 1 + case % 2 + terms = 1 + case % 4 + n = 2 * (terms - 1) * width + 15 + case % 5 + gap = Q(1 + case % 3, 8) + bits = 9 + case % 4 + shift = 0 + while (1 << shift) * gap < 1: + shift += 1 + plan = M.Plan(n, width, bits, terms, shift, gap) + matrix = [[Q(0) for _ in range(n)] for _ in range(n)] + holes = {n // 2} + for row in range(n): + if row in holes: + continue + support = [((row + offset) % n, rng.choice((-1, 1)), rng.randint(1, 7)) + for offset in range(-width, width + 1) + if offset and (row + offset) % n not in holes] + denominator = sum(weight for _, _, weight in support) + for column, sign, weight in support: + matrix[row][column] = sign * (1 - gap) * Q(weight, denominator) + data = [] + for _ in range(n): + real = rng.randint(-(1 << bits), 1 << bits) + imag = rng.randint(-((1 << bits) - abs(real)), (1 << bits) - abs(real)) + data.append((real, imag)) + lower = (-2, n - 3, n // 2 - 1, 1)[case % 4] + cases.append((matrix, tuple(data), plan, lower, 3)) + return cases + + +def finite_cases(): + receipts, nonzero_errors = [], 0 + for matrix, data, plan, lower, length in matrix_cases(): + output, error, bill, extents = run_line(matrix, data, plan, lower, length) + nonzero_errors += int(error > 0) + receipts.append(dict(period=plan.period, width=plan.halfwidth, terms=plan.terms, + bits=plan.bits, lower=lower, length=length, gap=str(plan.gap), + output=list(output), nonzero_error=error > 0, + bill=bill.record(), resident_extents=list(extents))) + require(nonzero_errors >= 24, "nontrivial rounding fixtures") + return receipts, nonzero_errors + + +def tensor_oracle(matrices, plans, data, rounded): + """Full canonical tensor, including coordinates outside every local box.""" + sizes = tuple(p.period for p in plans) + current = dict(data) + if not rounded: + current = {key: tuple(Q(v, 1 << plans[0].bits) for v in z) + for key, z in current.items()} + for axis, (matrix, plan) in enumerate(zip(matrices, plans)): + following = {} + others = tuple(i for i in range(len(plans)) if i != axis) + for spectator in itertools.product(*(range(sizes[i]) for i in others)): + keys = [] + for coordinate in range(sizes[axis]): + key, other = [], 0 + for i in range(len(plans)): + if i == axis: + key.append(coordinate) + else: + key.append(spectator[other]); other += 1 + keys.append(tuple(key)) + line = tuple(current[key] for key in keys) + values = rounded_global(matrix, line, plan) if rounded else dense_polynomial( + matrix, line, plan.terms, 1 << plan.normalizer_shift) + following.update(zip(keys, values)) + current = following + return current + + +def tensor_case(matrices, plans, targets, label, tensor_module=T, entry_services=None, source_ids=None): + bill = M.Bill() + def prepared(): + for axis, (matrix, plan) in enumerate(zip(matrices, plans)): + entry = entry_services[axis] if entry_services is not None else ( + lambda r, c, matrix=matrix: matrix[r][c]) + source_id = source_ids[axis] if source_ids is not None else label + "/axis/" + str(axis) + yield M.prepare_table(plan, entry, source_id, bill)[0] + archive = T.pack_tables(prepared(), bill) + archive_before = M.tape_digest(archive.tape) + layout = T.Layout.make(plans, targets) + scale = 1 << plans[0].bits + full_data = {} + for key in itertools.product(*(range(p.period) for p in plans)): + code = sum((i + 3) * (x + 1) ** 2 for i, x in enumerate(key)) + real = (code * 173 % (scale // 2)) - scale // 4 + imag = (code * 97 % (scale // 3)) - scale // 6 + full_data[key] = real, imag + def local_values(): + for offsets in T.coordinate_odometer(layout.lengths): + canonical = tuple((lo + x) % p.period for lo, x, p in zip(layout.lowers, offsets, plans)) + yield full_data[canonical] + source = T.rectangle_input(layout, local_values(), bill) + start_products, start_scans = bill.products, bill.page_scans + output = tensor_module.apply_tensor(archive, targets, source, bill) + values = tensor_module.consume_tensor(output) + require(archive_before == M.tape_digest(archive.tape) and archive.tape.head == 0, + "tensor preserves global source archive") + exact = tensor_oracle(matrices, plans, full_data, rounded=False) + rounded = tensor_oracle(matrices, plans, full_data, rounded=True) + errors = [] + for key, value in values: + canonical = tuple(x % p.period for x, p in zip(key, plans)) + require(value == rounded[canonical], "full rounded tensor equality") + errors.append(pair_norm(tuple(Q(value[part], scale) - exact[canonical][part] + for part in (0, 1)))) + error = max(errors) + require(error <= sum(p.numeric_error for p in plans), "complete normalized tensor bound") + require(error > 0, "nonzero tensor rounding defect") + expected_count = 1 + for _, length in targets: + expected_count *= length + require(len(values) == expected_count, "complete target tensor") + require(len(output.role_extents) == 8, "fixed local physical role count") + products, scans, live_count = 0, 0, layout.volume + for axis, (plan, target, receipt) in enumerate(zip(plans, targets, output.axis_receipts)): + lines = live_count // layout.lengths[axis] + n = target[1] + per_line = 2 * plan.band * ((plan.terms - 1) * n + + plan.halfwidth * (plan.terms - 1) * (plan.terms - 2)) + require(receipt["products"] == lines * per_line, "tensor complete product invoice") + expected_scans = 1 + int((layout.lowers[axis] % plan.period) + layout.lengths[axis] > plan.period) + require(receipt["page_scans"] == expected_scans, "one page production per axis, not per line") + require(receipt["radix_passes"] == layout.key_width, "complete sparse radix exposure") + products += lines * per_line; scans += expected_scans + live_count = lines * n + require(bill.products - start_products == products and bill.page_scans - start_scans == scans, + "complete tensor invoice totals") + return dict(label=label, dimensions=len(plans), saved_lengths=list(layout.lengths), + copied_records=layout.volume, target_records=len(values), + key_width=layout.key_width, fixed_local_tape_roles=8, + role_extents=list(output.role_extents), total_retained_local_bits=sum(n for _, n in output.role_extents), + protected_archive_bits=archive.tape.extent, axis_receipts=list(output.axis_receipts), + output=list(values), numerical_bound=str(sum(p.numeric_error for p in plans)), + nonzero_error=True, bill=bill.record()) + + +def synthetic_tensors(tensor_module=T): + result = [] + for dimensions in (2, 3): + matrices, plans, targets = [], [], [] + for axis in range(dimensions): + n, width, terms = 11, 1, 2 + axis % 2 + gap = Q(axis + 2, 8) + plan = M.Plan(n, width, 10, terms, 2, gap) + matrix = [[Q(0) for _ in range(n)] for _ in range(n)] + for row in range(n): + if row == n // 2: + continue + for offset in (-1, 1): + column = (row + offset) % n + if column != n // 2: + matrix[row][column] = (-1 if (row + axis + offset) % 2 else 1) * (1 - gap) / 2 + matrices.append(matrix); plans.append(plan) + targets.append((-1 if axis % 2 == 0 else n - 2, 2)) + result.append(tensor_case(tuple(matrices), tuple(plans), tuple(targets), + "signed-" + str(dimensions) + "d", tensor_module)) + return result + + +def reuse_history(engine=M): + """Long line, short face, long line on exactly the same physical roles.""" + bill = engine.Bill() + plan = engine.Plan(101, 1, 12, 3, 1, Q(1, 2)) + matrix = [[Q(1, 4) if (c-r) % 101 in (1, 100) else Q(0) + for c in range(101)] for r in range(101)] + data = tuple(((r * 73) % 2048 - 1024, (r * 31) % 1024 - 512) for r in range(101)) + table, _ = engine.prepare_table(plan, lambda r, c: matrix[r][c], "reused source", bill) + page_role = engine.Tape(bill, "reused page") + source_role = engine.Tape(bill, "reused source") + iterates = (engine.Tape(bill, "reused iterate 0"), engine.Tape(bill, "reused iterate 1")) + records = [] + exact = rounded_global(matrix, data, plan) + for lower, length in ((2, 37), (50, 1), (70, 37)): + before = bill.record() + page = engine.extract_page(table, lower-plan.halo, length+2*plan.halo, bill, page_role) + for row in range(lower-plan.halo, lower+length+plan.halo): + engine.put_complex(source_role, data[row % 101], plan.data_width) + source_role.rewind(); source_role.readonly = True + output = engine.apply_line(page, source_role, lower, length, bill, workspace=iterates) + values = engine.consume(output) + require(values == tuple(exact[r % 101] for r in range(lower, lower+length)), + "long-short-long exact returned values") + source_role.readonly = False; source_role.clear() + page_role.readonly = False; page_role.clear() + roles = (source_role, page_role) + iterates + require(all(t.head == 0 and t.live_bits == 0 and not any(t.snapshot()) for t in roles), + "long-short-long retained blank suffix invariant") + after = bill.record() + records.append(dict(target_length=length, saved_length=length+2*plan.halo, + output=list(values), retained_bits=sum(t.extent for t in roles), + writes=after["writes"]-before["writes"], + moves=after["moves"]-before["moves"])) + return records + + +def backing_history_control(): + correct = reuse_history() + text = (PACKAGE / "engine.py").read_text() + require(text.count("occupied = self.live_bits") == 1, "unique historical clear site") + module = types.ModuleType("_shrinking_counterfactual_highwater") + sys.modules[module.__name__] = module + exec(compile(text.replace("occupied = self.live_bits", "occupied = self.extent"), + "", "exec"), module.__dict__) + counterfactual = reuse_history(module) + require([x["output"] for x in correct] == [x["output"] for x in counterfactual], + "counterfactual preserves numerical result") + require(counterfactual[1]["writes"] > 3 * correct[1]["writes"], + "historical backing creates a real short-face tariff") + return dict(correct=correct, counterfactual=counterfactual, + retained_extent_ratio="41/5", counterfactual_detected=True) + + +def rectangle_reuse_history(): + bill = M.Bill() + plans = (M.Plan(17, 1, 10, 2, 1, Q(3, 4)), M.Plan(17, 1, 10, 3, 1, Q(7, 8))) + matrices = tuple([[Q((1 if axis == 0 else -1), 8 << axis) + if (c-r) % 17 in (1, 16) and r != 8 and c != 8 else Q(0) + for c in range(17)] for r in range(17)] for axis in range(2)) + def prepared(): + for axis, plan in enumerate(plans): + yield M.prepare_table(plan, lambda r, c, axis=axis: matrices[axis][r][c], + "rectangle reuse axis " + str(axis), bill)[0] + archive = T.pack_tables(prepared(), bill) + workspace = T.TensorWorkspace.create(bill) + role_ids = {id(t) for t in workspace.roles} + data = {key: ((13*key[0]+29*key[1]) % 512-256, (31*key[0]+7*key[1]) % 256-128) + for key in itertools.product(range(17), repeat=2)} + expected = tensor_oracle(matrices, plans, data, rounded=True) + history = [] + original_constructor = M.Tape.__init__ + def forbidden_constructor(*args, **kwargs): + raise ValueError("new tape role inside rectangle reuse history") + M.Tape.__init__ = forbidden_constructor + try: + for targets in (((-1, 7), (4, 5)), ((8, 1), (-1, 2)), ((1, 5), (9, 7))): + layout = T.Layout.make(plans, targets) + values = (data[tuple((lo+x) % 17 for lo, x in zip(layout.lowers, offsets))] + for offsets in T.coordinate_odometer(layout.lengths)) + before = bill.record() + source = T.rectangle_input(layout, values, bill, workspace.rectangles[0]) + output = T.apply_tensor(archive, targets, source, bill, workspace=workspace) + require({id(output.tape)} | {id(t) for t in output.blank_roles} == role_ids, + "same eight roles across completed rectangles") + answer = T.consume_tensor(output) + require(all(value == expected[tuple(x % 17 for x in key)] for key, value in answer), + "long-short-long rectangle exact output") + require(all(t.head == 0 and t.live_bits == 0 and not any(t.snapshot()) + for t in workspace.roles), "reused rectangle complete restoration") + after = bill.record() + history.append(dict(saved_lengths=list(layout.lengths), copied_records=layout.volume, + target_records=len(answer), output=list(answer), + retained_bits=sum(t.extent for t in workspace.roles), + writes=after["writes"]-before["writes"], + moves=after["moves"]-before["moves"], + archive_scans=after["page_scans"]-before["page_scans"])) + finally: + M.Tape.__init__ = original_constructor + return dict(fixed_role_count=8, constructors_sealed_during_calls=True, history=history) + + +def gaussian_cases(raw): + reference = S.make_reference(raw, (32, 8, 2, 1, 8, 32)) + reference.require_narrow_gap() + gap = Q((reference.narrow_gap * (1 << 16)).numerator // + (reference.narrow_gap * (1 << 16)).denominator, 1 << 16) + shift = 0 + while (1 << shift) * gap < 1: + shift += 1 + plan = M.Plan(reference.target_size, 2 * reference.spec.source_halfwidth + 2, + 28, 4, shift, gap) + require(plan.numeric_error + plan.tail_error < Q(1, 1 << 20), + "uniform same-reference inverse target") + prep_bill = M.Bill() + table, height = M.prepare_table(plan, lambda r, c: S.source_entry(reference, r, c), + reference.description_hash, prep_bill) + setup = S.source_receipt(reference) + setup["band_source_calls"] = prep_bill.setup_entries + setup["stored_coefficient_height"] = height + setup["table_bits"] = table.tape.extent + setup["production_bill"] = prep_bill.record() + # All original source entries, not just the producer's asserted band. + matrix = [[S.source_entry(reference, r, c) for c in range(plan.period)] + for r in range(plan.period)] + omissions, wrap_entries = 0, 0 + holes = tuple(reference.holes) + for r in range(plan.period): + for c in range(plan.period): + distance = min((r - c) % plan.period, (c - r) % plan.period) + if distance > plan.halfwidth: + require(matrix[r][c] == 0, "actual complete off-band support") + omissions += 1 + if abs(r - c) > plan.period // 2 and matrix[r][c]: + wrap_entries += 1 + if r in holes or c in holes: + require(matrix[r][c] == 0, "actual identity holes") + require(wrap_entries > 0 and holes, "actual wrap and holes exercised") + scale = 1 << plan.bits + data = tuple(((1 if r % 3 else -1) * (scale // 3 + 17 * r), + (-1 if r % 2 else 1) * (scale // 7 - 11 * r)) + for r in range(plan.period)) + receipts = [] + for lower in (-2, 5, 18): + output, error, bill, extents = run_line(matrix, data, plan, lower, 5, + table=table, bill=M.Bill()) + require(error > 0, "actual source nonzero numerical error") + receipts.append(dict(lower=lower, output=list(output), bill=bill.record(), + resident_extents=list(extents), nonzero_error=True)) + # An executed wrong branch: suppress genuine across-period E entries. + dropped = [[Q(0) if abs(r - c) > plan.period // 2 else matrix[r][c] + for c in range(plan.period)] for r in range(plan.period)] + wrong, _, _, _ = run_line(dropped, data, plan, -2, 5) + require(wrong != tuple(map(tuple, receipts[0]["output"])), "dropped-wrap control discriminates") + # Fresh retained producers, not the dense checker's indexed matrix, supply + # both actual tensor band tables. They share the same immutable spec. + producer_reference = S.make_reference(raw, (32, 8, 2, 1, 8, 32)) + producer = lambda r, c: S.source_entry(producer_reference, r, c) + tensor = tensor_case((matrix, matrix), (plan, plan), ((-1, 4), (5, 3)), "actual-reference-2d", + entry_services=(producer, producer), + source_ids=(producer_reference.description_hash,) * 2) + tensor["source_setup"] = S.source_receipt(producer_reference) + S.clear_reference(producer_reference) + S.clear_reference(reference) + require(not reference.entries and not reference.weights and not reference.kernel, + "setup cache release") + return dict(setup=setup, period=plan.period, gap=str(gap), holes=list(holes), + original_matrix_entries=plan.period ** 2, checked_off_band_entries=omissions, + nonzero_wrap_entries=wrap_entries, target_bits=20, + numerical_bound=str(plan.numeric_error), tail_bound=str(plan.tail_error), + lines=receipts, tensor=tensor, dropped_wrap_detected=True) + + +def negative_controls(): + controls = [] + p = M.Plan(29, 1, 10, 3, 3, Q(1, 8)) + controls.append(rejected(lambda: replace(p, normalizer_shift=2), "unfunded normalization")) + controls.append(rejected(lambda: replace(p, bits=2), "lost normalized-source precision")) + controls.append(rejected(lambda: replace(p, halfwidth=15), "nonunique cyclic offsets")) + controls.append(rejected(lambda: replace(p, gap=0), "missing contraction gap")) + controls.append(rejected(lambda: M.prepare_table(p, lambda r, c: Q(1, 2), + "invalid row", M.Bill()), "bad original row gap")) + controls.append(rejected(lambda: M.input_tape(p, ((1024, 1),), M.Bill()), "oversized actual input")) + table, _ = M.prepare_table(p, lambda r, c: Q(1, 4) if c == (r + 1) % p.period else Q(0), + "control", M.Bill()) + controls.append(rejected(lambda: M.extract_page(table, 0, p.period, M.Bill()), + "repeated canonical page coordinate")) + page = M.extract_page(table, 0, 7, M.Bill()) + source = M.input_tape(p, ((100, -100),) * 7, M.Bill()) + controls.append(rejected(lambda: page.tape.write(1), "immutable coefficient page")) + controls.append(rejected(lambda: source.write(1), "immutable fixed source")) + controls.append(rejected(lambda: M.apply_line(page, source, 3, 3, M.Bill()), + "prematurely cropped dependency interval")) + bad = M.input_tape(p, ((0, 0),) * 7, M.Bill()) + bad.readonly = False; bad.write(1); bad.rewind(); bad.readonly = True + controls.append(rejected(lambda: M.apply_line(page, bad, 2, 3, M.Bill()), + "noncanonical negative zero")) + # Real source-text changes of the consumer, tested against the independent oracle. + text = (PACKAGE / "engine.py").read_text() + mutations = [ + ("real += product_real; imag += product_imag", "real -= product_real; imag -= product_imag", "wrong recurrence sign"), + ("current.walk(-2 * p.halfwidth * record_bits)", "current.walk(-(2 * p.halfwidth + 1) * record_bits)", "wrong neighbor rewind"), + ("current.clear(); following.rewind()", "current.rewind(); following.rewind()", "missing scratch erasure"), + ] + case = matrix_cases()[3] + for old, new, name in mutations: + require(text.count(old) == 1, "unique mutation site") + module = types.ModuleType("_shrinking_mutation_" + str(len(controls))) + sys.modules[module.__name__] = module + exec(compile(text.replace(old, new), "", "exec"), module.__dict__) + # Reconstruct the plan in the mutated module; other data stay exact. + matrix, data, p0, lower, length = case + pp = module.Plan(**p0.__dict__) + controls.append(rejected(lambda: run_line(matrix, data, pp, lower, length, module), name)) + tensor_text = (PACKAGE / "tensor.py").read_text() + for old, new, name in [ + ("order = (axis,) + tuple(j for j in range(len(layout.lengths) - 1, -1, -1) if j != axis)", + "order = tuple(range(len(layout.lengths)))", "wrong sparse axis exposure"), + ("emit = catalog_axis == axis and begin <= row < end", + "emit = catalog_axis == 0 and begin <= row < end", "stale axis coefficient page"), + ("coordinate = target_lower - layout.lowers[axis] + offset", + "coordinate = target_lower - layout.lowers[axis] + offset + 1", "shifted returned tensor key"), + ]: + require(tensor_text.count(old) == 1, "unique tensor mutation site") + module = types.ModuleType("_shrinking_tensor_mutation_" + str(len(controls))) + sys.modules[module.__name__] = module + exec(compile(tensor_text.replace(old, new), "", "exec"), module.__dict__) + controls.append(rejected(lambda: synthetic_tensors(module), name)) + return controls + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write-receipt", action="store_true") + args = parser.parse_args() + raw = S.authenticated_inputs(PACKAGE) + finite, nonzero = finite_cases() + tensors = synthetic_tensors() + gaussian = gaussian_cases(raw) + controls = negative_controls() + history = backing_history_control() + rectangle_history = rectangle_reuse_history() + result = dict(schema_version=1, seed=72, claim="scoped written proof and finite tape corroboration", + no_new_kappa=True, finite_lines=len(finite), finite_target_outputs=3 * len(finite), + nonzero_rounding_lines=nonzero, finite=finite, tensors=tensors, gaussian=gaussian, + controls=controls, control_count=len(controls), + backing_reuse=history, rectangle_reuse=rectangle_history, + program_sha256={name: sha256((PACKAGE/name).read_bytes()).hexdigest() + for name in ("engine.py", "source.py", "tensor.py", "verify.py")}, + source_sha256={path: sha256(content).hexdigest() for path, content in sorted(raw.items())}) + encoded = json.dumps(result, sort_keys=True, indent=2) + "\n" + receipt = PACKAGE / "RESULT.json" + if args.write_receipt: + receipt.write_text(encoded) + else: + require(receipt.is_file(), "mandatory exact receipt") + # Canonical serialization distinguishes booleans from integers recursively. + require(json.dumps(json.loads(receipt.read_text()), sort_keys=True, separators=(",", ":")) == + json.dumps(result, sort_keys=True, separators=(",", ":")), "exact typed receipt") + print("PASS_SHRINKING_REFERENCE_HALO " + json.dumps( + dict(finite_lines=len(finite), gaussian_rows=gaussian["period"], + controls=len(controls), source_entries=gaussian["original_matrix_entries"], + receipt_sha256=sha256(encoded.encode()).hexdigest(), no_new_kappa=True), sort_keys=True)) + + +if __name__ == "__main__": + main() From 630c9c2a5d6373ca103c55108bb606b4868bc6fd Mon Sep 17 00:00:00 2001 From: CubeJerry <80299683+CubeJerry@users.noreply.github.com> Date: Mon, 9 Nov 2026 00:57:25 +0800 Subject: [PATCH 2/3] Execute sequential first-face halo transport and unique return Prepared for @CubeJerry with substantial OpenAI Codex assistance. No new kappa; independent geometry/radix review and registered checks passed. --- .../EXPECTED.json | 159 +++++ .../sparse-halo-tape-transaction/OVERLAP.json | 33 + .../sparse-halo-tape-transaction/PROOF.md | 427 ++++++++++++ .../sparse-halo-tape-transaction/README.md | 167 +++++ .../sparse-halo-tape-transaction/SOURCES.json | 36 + .../sparse-halo-tape-transaction/TASK.json | 89 +++ .../sparse-halo-tape-transaction/VERIFY.json | 55 ++ .../independent_review.py | 86 +++ .../sparse-halo-tape-transaction/tapes.py | 644 ++++++++++++++++++ .../sparse-halo-tape-transaction/verify.py | 285 ++++++++ 10 files changed, 1981 insertions(+) create mode 100644 research/sparse-halo-tape-transaction/EXPECTED.json create mode 100644 research/sparse-halo-tape-transaction/OVERLAP.json create mode 100644 research/sparse-halo-tape-transaction/PROOF.md create mode 100644 research/sparse-halo-tape-transaction/README.md create mode 100644 research/sparse-halo-tape-transaction/SOURCES.json create mode 100644 research/sparse-halo-tape-transaction/TASK.json create mode 100644 research/sparse-halo-tape-transaction/VERIFY.json create mode 100644 research/sparse-halo-tape-transaction/independent_review.py create mode 100644 research/sparse-halo-tape-transaction/tapes.py create mode 100644 research/sparse-halo-tape-transaction/verify.py diff --git a/research/sparse-halo-tape-transaction/EXPECTED.json b/research/sparse-halo-tape-transaction/EXPECTED.json new file mode 100644 index 0000000000..9b2fe8ab73 --- /dev/null +++ b/research/sparse-halo-tape-transaction/EXPECTED.json @@ -0,0 +1,159 @@ +{ + "arithmetic_pairs": 1364, + "claim": "physical gather/sort/return only; numerical halo consumer is an explicit contract; no new kappa", + "controls": [ + "missing_target", + "duplicate_target", + "kept_row_return", + "core_before_copy", + "return_before_core", + "nonunit_head_jump", + "reversed_bucket_order_detected", + "duplicate_key_stability", + "copy_after_core_detected", + "no_observer_call_in_program" + ], + "fixtures": [ + { + "B": 5, + "C": 16, + "K": 14, + "M": 32, + "Q": 8, + "after_erase": { + "actions": 356848, + "moves": 141644, + "retained_cells": 2077, + "roles": 30 + }, + "before_erase": { + "actions": 350261, + "moves": 138849, + "retained_cells": 2077, + "roles": 30 + }, + "gather": { + "actions": 50995, + "moves": 19768, + "retained_cells": 970, + "roles": 30 + }, + "gather_and_sparse_sort": { + "actions": 296152, + "moves": 117816, + "retained_cells": 1776, + "roles": 30 + }, + "geometry": { + "P": 8, + "a": 2, + "b": 1, + "ell": 4, + "ks": [ + 1 + ], + "spectator_width": 0 + }, + "maximum_fanout": 2, + "output_sha256": "37197df41278fb5df945780e0e7c928ff7e52bb29672b78faeb914ddc44d9339", + "zero_copy_sources": 20 + }, + { + "B": 10, + "C": 1024, + "K": 27, + "M": 1024, + "Q": 448, + "after_erase": { + "actions": 55924621, + "moves": 22322760, + "retained_cells": 124785, + "roles": 30 + }, + "before_erase": { + "actions": 55530902, + "moves": 22154055, + "retained_cells": 124785, + "roles": 30 + }, + "gather": { + "actions": 3764179, + "moves": 1479250, + "retained_cells": 56287, + "roles": 30 + }, + "gather_and_sparse_sort": { + "actions": 50076447, + "moves": 20004132, + "retained_cells": 115551, + "roles": 30 + }, + "geometry": { + "P": 8, + "a": 2, + "b": 1, + "ell": 4, + "ks": [ + 1, + 1 + ], + "spectator_width": 0 + }, + "maximum_fanout": 4, + "output_sha256": "86ee13722bf69bdc41109add08e1df31b8a99afcd81ef1f72bb7039fe8b00c32", + "zero_copy_sources": 400 + }, + { + "B": 10, + "C": 448, + "K": 27, + "M": 1024, + "Q": 448, + "after_erase": { + "actions": 28502162, + "moves": 11345158, + "retained_cells": 70305, + "roles": 30 + }, + "before_erase": { + "actions": 28257705, + "moves": 11240422, + "retained_cells": 70305, + "roles": 30 + }, + "gather": { + "actions": 2597732, + "moves": 1010032, + "retained_cells": 34959, + "roles": 30 + }, + "gather_and_sparse_sort": { + "actions": 22860400, + "moves": 9115074, + "retained_cells": 61071, + "roles": 30 + }, + "geometry": { + "P": 8, + "a": 1, + "b": 0, + "ell": 3, + "ks": [ + 1, + 2 + ], + "spectator_width": 1 + }, + "maximum_fanout": 1, + "output_sha256": "068ca865a3002e52455f2406829f94fbc4c56bf9cae91fc27ba44eb3581739e0", + "zero_copy_sources": 576 + } + ], + "python": "3.12.14", + "source_bindings": [ + "research/halo-copy-enumeration/README.md", + "research/unconditional-batched-crt/HALO.md", + "research/unconditional-batched-crt/GAUSSIAN.md" + ], + "status": "PASS" +} diff --git a/research/sparse-halo-tape-transaction/OVERLAP.json b/research/sparse-halo-tape-transaction/OVERLAP.json new file mode 100644 index 0000000000..8d2268e0fa --- /dev/null +++ b/research/sparse-halo-tape-transaction/OVERLAP.json @@ -0,0 +1,33 @@ +{ + "checked_on": "2026-11-08", + "canonical_base": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "source_scope": "Bounded lead archive synthesis and scoped PR searches; no exhaustive novelty claim. Discussion posting/access limitations retained in README.", + "contextual_sources": [ + { + "path": "research/rounded-core-halo-splice/PROOF.md", + "usage": "provenance", + "pin": "head:e212af981b49c299de515f8c23dfb0e5b73e2e95:research/rounded-core-halo-splice/PROOF.md", + "git_blob": "d9440b8c90f8663057c3266ccbfe348cfcc52140", + "sha256": "dc8b3d58086bbe208320ece31a19080afecd687ac3be554935db3f091b423f24" + } + ], + "contextual_source_policy": "Exact nonexecuted source pins for attribution and compatibility discussion. These are not live runtime inputs or claims of canonical-base ancestry.", + "new_obligation": "#4870 first Open next question: fixed-role physical first-face copy enumeration, full-key radix, paid rewind/erasure and unique return.", + "predecessors": [ + { + "pr": 4100, + "path": "research/unconditional-batched-crt/HALO.md", + "credit": "Cinna Davis; original source-driven halo schedule and tariff." + }, + { + "pr": 4870, + "path": "research/halo-copy-enumeration/README.md", + "credit": "Astra/OpenAI-assisted contribution; exact source membership and volume, physical implementation left open." + }, + { + "pr": 6880, + "head": "e212af981b49c299de515f8c23dfb0e5b73e2e95", + "credit": "CubeJerry/OpenAI-assisted common-reference core/halo splice; pre-copy and unique-return chronology." + } + ] +} diff --git a/research/sparse-halo-tape-transaction/PROOF.md b/research/sparse-halo-tape-transaction/PROOF.md new file mode 100644 index 0000000000..2f69b5b082 --- /dev/null +++ b/research/sparse-halo-tape-transaction/PROOF.md @@ -0,0 +1,427 @@ +# A sequential tape transaction for first-face halo copies + +## 1. Statement, input contract, and contribution boundary + +This note supplies the physical enumeration/sort/return obligation left open +in [the first open question of #4870](../halo-copy-enumeration/README.md). +The first-face partition, its source-membership predicates, and its volume +formula are inherited results. The new object is the fixed-role sequential +program in `tapes.py`, with the complete dense and sparse movement bill below. +It uses no numerical inverse oracle. An independently supplied halo consumer +remains responsible for producing correct returned *values*. + +Fix integers + +\[ + g\ge1,\quad \ell\ge1,\quad k_i\ge1,\quad E\ge0,\quad P\ge1, + \qquad L=2^\ell,\quad S_i=2^{k_i}L, +\] + +and integers \(0\le b4A\). There are \(2^E\) independent +spectator blocks. In a block, a point has coordinates +\(x_i=q_iL+r_i\), with \(0\le q_i<2^{k_i}\), \(0\le r_i