From 99c71d385171480ecc2c43287aa4a04e1027fcd9 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Tue, 13 Oct 2026 11:58:27 -0500 Subject: [PATCH] research: add reversible quadratic phases to dirty stride solver --- .github/workflows/dirty-stride-phases.yml | 27 ++ research/dirty-stride-phases/DERIVATION.diff | 22 + research/dirty-stride-phases/EXPECTED.json | 335 ++++++++++++++ research/dirty-stride-phases/NOTICE.md | 38 ++ research/dirty-stride-phases/PROOF.md | 410 +++++++++++++++++ research/dirty-stride-phases/README.md | 63 +++ research/dirty-stride-phases/SOURCE.json | 123 +++++ research/dirty-stride-phases/VALIDATION.json | 207 +++++++++ research/dirty-stride-phases/chirp.py | 295 ++++++++++++ research/dirty-stride-phases/dirty_stride.py | 409 +++++++++++++++++ research/dirty-stride-phases/oracle.py | 188 ++++++++ research/dirty-stride-phases/test_package.py | 120 +++++ .../dirty-stride-phases/vendor/pr479/PROOF.md | 165 +++++++ .../vendor/pr479/README.md | 40 ++ .../vendor/pr479/SOURCE.json | 10 + .../vendor/pr628/FACTORS.json | 402 ++++++++++++++++ .../vendor/pr628/NOTICE.md | 24 + .../vendor/pr628/SOURCE.json | 18 + .../dirty-stride-phases/vendor/pr628/check.py | 178 ++++++++ .../vendor/pr628/interval_kernel.py | 61 +++ .../dirty-stride-phases/vendor/pr628/scan.py | 123 +++++ .../dirty-stride-phases/vendor/pr985/LICENSE | 201 ++++++++ .../vendor/pr985/NOTICE.md | 39 ++ .../dirty-stride-phases/vendor/pr985/PROOF.md | 428 ++++++++++++++++++ .../vendor/pr985/README.md | 130 ++++++ .../vendor/pr985/dirty_stride.py | 407 +++++++++++++++++ research/dirty-stride-phases/verify.py | 397 ++++++++++++++++ 27 files changed, 4860 insertions(+) create mode 100644 .github/workflows/dirty-stride-phases.yml create mode 100644 research/dirty-stride-phases/DERIVATION.diff create mode 100644 research/dirty-stride-phases/EXPECTED.json create mode 100644 research/dirty-stride-phases/NOTICE.md create mode 100644 research/dirty-stride-phases/PROOF.md create mode 100644 research/dirty-stride-phases/README.md create mode 100644 research/dirty-stride-phases/SOURCE.json create mode 100644 research/dirty-stride-phases/VALIDATION.json create mode 100644 research/dirty-stride-phases/chirp.py create mode 100644 research/dirty-stride-phases/dirty_stride.py create mode 100644 research/dirty-stride-phases/oracle.py create mode 100644 research/dirty-stride-phases/test_package.py create mode 100644 research/dirty-stride-phases/vendor/pr479/PROOF.md create mode 100644 research/dirty-stride-phases/vendor/pr479/README.md create mode 100644 research/dirty-stride-phases/vendor/pr479/SOURCE.json create mode 100644 research/dirty-stride-phases/vendor/pr628/FACTORS.json create mode 100644 research/dirty-stride-phases/vendor/pr628/NOTICE.md create mode 100644 research/dirty-stride-phases/vendor/pr628/SOURCE.json create mode 100644 research/dirty-stride-phases/vendor/pr628/check.py create mode 100644 research/dirty-stride-phases/vendor/pr628/interval_kernel.py create mode 100644 research/dirty-stride-phases/vendor/pr628/scan.py create mode 100644 research/dirty-stride-phases/vendor/pr985/LICENSE create mode 100644 research/dirty-stride-phases/vendor/pr985/NOTICE.md create mode 100644 research/dirty-stride-phases/vendor/pr985/PROOF.md create mode 100644 research/dirty-stride-phases/vendor/pr985/README.md create mode 100644 research/dirty-stride-phases/vendor/pr985/dirty_stride.py create mode 100644 research/dirty-stride-phases/verify.py diff --git a/.github/workflows/dirty-stride-phases.yml b/.github/workflows/dirty-stride-phases.yml new file mode 100644 index 0000000000..b6e9a29dc0 --- /dev/null +++ b/.github/workflows/dirty-stride-phases.yml @@ -0,0 +1,27 @@ +name: Dirty stride quadratic phases +on: + pull_request: + paths: + - 'research/dirty-stride-phases/**' + - '.github/workflows/dirty-stride-phases.yml' + push: + paths: + - 'research/dirty-stride-phases/**' + - '.github/workflows/dirty-stride-phases.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + verify: + runs-on: ubuntu-latest + timeout-minutes: 15 + strategy: + matrix: + python: ['3.11', '3.14'] + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: ${{ matrix.python }} + - run: python -I -O -B research/dirty-stride-phases/verify.py + - run: python -I -O -B research/dirty-stride-phases/test_package.py diff --git a/research/dirty-stride-phases/DERIVATION.diff b/research/dirty-stride-phases/DERIVATION.diff new file mode 100644 index 0000000000..5b1b3c770a --- /dev/null +++ b/research/dirty-stride-phases/DERIVATION.diff @@ -0,0 +1,22 @@ +--- vendor/pr985/dirty_stride.py ++++ dirty_stride.py +@@ -289,7 +289,8 @@ + for i in range(len(data)): + meter.access(data, i) + meter.validation_reads += 1 +- need(rnd(data[i], bits) == data[i], 'fixed grid data') ++ value = data[i] ++ need(rnd(value, bits) == value, 'fixed grid data') + divisor = gcd(len(x), stride) + cycle = len(x)//divisor + inverse = pow((stride//divisor) % cycle, -1, cycle) if cycle > 1 else 0 +@@ -338,7 +339,8 @@ + for i in range(len(data)): + meter.access(data, i) + meter.validation_reads += 1 +- need(rnd(data[i], bits) == data[i], 'fixed grid data') ++ value = data[i] ++ need(rnd(value, bits) == value, 'fixed grid data') + def run(src, dst, lo, hi, level, direction): + if hi-lo == 1: + inside, b, scale = factors[lo] diff --git a/research/dirty-stride-phases/EXPECTED.json b/research/dirty-stride-phases/EXPECTED.json new file mode 100644 index 0000000000..6162624b57 --- /dev/null +++ b/research/dirty-stride-phases/EXPECTED.json @@ -0,0 +1,335 @@ +{ + "controls": { + "nonconstant_witness": { + "length": 8, + "modulus": 16, + "numerator": -3, + "real_separation_lower": "1/8", + "stride": 3 + }, + "rejections": [ + "zero_modulus", + "boolean_numerator", + "aliased_arrays", + "unstable_coefficient", + "unsupported_shift", + "invalid_sign", + "float_coefficient", + "insufficient_precision" + ] + }, + "costs": [ + { + "divisions": 49140, + "length": 70, + "phase_peak_l1_log2_upper": 1, + "phase_terms": 48596, + "products": 98304, + "recursion_depth": 5, + "stride": 29, + "tape_moves": 33906 + }, + { + "divisions": 112500, + "length": 169, + "phase_peak_l1_log2_upper": 2, + "phase_terms": 111252, + "products": 225156, + "recursion_depth": 6, + "stride": 70, + "tape_moves": 92531 + }, + { + "divisions": 285300, + "length": 408, + "phase_peak_l1_log2_upper": 2, + "phase_terms": 282132, + "products": 570744, + "recursion_depth": 7, + "stride": 169, + "tape_moves": 244880 + }, + { + "divisions": 708660, + "length": 985, + "phase_peak_l1_log2_upper": 2, + "phase_terms": 700788, + "products": 1417332, + "recursion_depth": 8, + "stride": 408, + "tape_moves": 634315 + } + ], + "kernels": [ + { + "bits": 78, + "calls": 1, + "count": 1, + "dirt": "7", + "length": 1, + "output_digest": "795d569769d7cf7fa67bcd2773298e96c6f3c2afc983eda024d69302bf4fb056", + "phase_terms": 240, + "stride": 0, + "tape_moves": 17 + }, + { + "bits": 78, + "calls": 1, + "count": 1, + "dirt": "-13", + "length": 5, + "output_digest": "09624cc4b5faf3c305b402677903c698954a5b9f1eaca61b89e9a784df757c61", + "phase_terms": 4048, + "stride": 2, + "tape_moves": 1161 + }, + { + "bits": 114, + "calls": 1, + "count": 1, + "dirt": "1099511627776", + "length": 8, + "output_digest": "17b3c966054848d551486dec54fd642f07cc12b17286412d238f58f991a50984", + "phase_terms": 5340, + "stride": -3, + "tape_moves": 1952 + }, + { + "bits": 154, + "calls": 1, + "count": 1, + "dirt": "1208925819614629174706176", + "length": 17, + "output_digest": "0d2fb4495bf6ffa7e089e1295c6db4322768a89642956c4865412f9cb6a35d75", + "phase_terms": 25612, + "stride": 7, + "tape_moves": 6001 + }, + { + "bits": 91, + "calls": 4, + "count": 2, + "dirt": "7", + "length": 1, + "output_digest": "a519e310179cd9308911399c3093c38f39f2c3509f4ef63a378b9e7cf3179535", + "phase_terms": 270, + "stride": 0, + "tape_moves": 46 + }, + { + "bits": 91, + "calls": 4, + "count": 2, + "dirt": "-13", + "length": 5, + "output_digest": "373fcce23ad8a70119895bf4cbfe509b6365d60c1b91ae08f4d76c49015db1fd", + "phase_terms": 4558, + "stride": 2, + "tape_moves": 4254 + }, + { + "bits": 127, + "calls": 4, + "count": 2, + "dirt": "1099511627776", + "length": 8, + "output_digest": "083c446c693c354b10137da4faecbe739116ba9ebfc0ad83cdedef396d28eb46", + "phase_terms": 5782, + "stride": -3, + "tape_moves": 7098 + }, + { + "bits": 167, + "calls": 4, + "count": 2, + "dirt": "1208925819614629174706176", + "length": 17, + "output_digest": "c9b3d974d9da493433d6108aa12d35c402940f7dd3a4573808b3945c81c6701a", + "phase_terms": 27302, + "stride": 7, + "tape_moves": 22510 + }, + { + "bits": 115, + "calls": 10, + "count": 3, + "dirt": "7", + "length": 1, + "output_digest": "3643a3c327f60464a878ff7573c3a297d3cf6916dd40d150e9260326cfb077e1", + "phase_terms": 318, + "stride": 0, + "tape_moves": 124 + }, + { + "bits": 116, + "calls": 10, + "count": 3, + "dirt": "-13", + "length": 5, + "output_digest": "bd9f7ecd7715055b9cbb71df98093961cb7907a0eded0a54cc09ccbdc303abe8", + "phase_terms": 5408, + "stride": 2, + "tape_moves": 10700 + }, + { + "bits": 151, + "calls": 10, + "count": 3, + "dirt": "1099511627776", + "length": 8, + "output_digest": "583685e75251ce2553b4b1ac958750fa0be1034bfb53e209171cc75ccb364c5b", + "phase_terms": 6598, + "stride": -3, + "tape_moves": 17874 + }, + { + "bits": 191, + "calls": 10, + "count": 3, + "dirt": "1208925819614629174706176", + "length": 17, + "output_digest": "9491e75baed62381ec857e7ac449e371f90da3da80c20a979846bf9e72c275da", + "phase_terms": 30422, + "stride": 7, + "tape_moves": 56508 + }, + { + "bits": 185, + "calls": 28, + "count": 5, + "dirt": "7", + "length": 1, + "output_digest": "9c2398bd38414e474fc51938a2b58bd3d44bd7f0ccbbe1e8e7742e6eb0beb1b2", + "phase_terms": 458, + "stride": 0, + "tape_moves": 420 + }, + { + "bits": 186, + "calls": 28, + "count": 5, + "dirt": "-13", + "length": 5, + "output_digest": "b0d4be356a0c40cf87411a5e13ed3e467f8880c9d65c62698f394e208396ceab", + "phase_terms": 7788, + "stride": 2, + "tape_moves": 30332 + }, + { + "bits": 221, + "calls": 28, + "count": 5, + "dirt": "1099511627776", + "length": 8, + "output_digest": "8060c2bacac5c1330ff8e33ddd843cfd832b34a6181453a9386d40fa075e8380", + "phase_terms": 9046, + "stride": -3, + "tape_moves": 50626 + }, + { + "bits": 261, + "calls": 28, + "count": 5, + "dirt": "1208925819614629174706176", + "length": 17, + "output_digest": "d90d67fdc07061e4a2e0232046fe0e2ff060d1ffd9339558a531b9dfdb696ae5", + "phase_terms": 39782, + "stride": 7, + "tape_moves": 159492 + }, + { + "bits": 323, + "calls": 64, + "count": 8, + "dirt": "7", + "length": 1, + "output_digest": "8ee946687cafa3a56933396a0d88acff66c0c834a4782f6e58d6b530fd3acfaa", + "phase_terms": 738, + "stride": 0, + "tape_moves": 626 + }, + { + "bits": 324, + "calls": 64, + "count": 8, + "dirt": "-13", + "length": 5, + "output_digest": "0ba65205c051c4eef445741868c0e29249410d9c691b91064caebf5a60cb0864", + "phase_terms": 12548, + "stride": 2, + "tape_moves": 66674 + }, + { + "bits": 359, + "calls": 64, + "count": 8, + "dirt": "1099511627776", + "length": 8, + "output_digest": "a4d58b76035655a7ed5f02ff0fa302fae8069c2ba50ca213b77dae1d4711b946", + "phase_terms": 13738, + "stride": -3, + "tape_moves": 111218 + }, + { + "bits": 399, + "calls": 64, + "count": 8, + "dirt": "1208925819614629174706176", + "length": 17, + "output_digest": "14a33fb4e4c45c4d7a769884fe13502823082649b76b5543b6f284918ccb6233", + "phase_terms": 57722, + "stride": 7, + "tape_moves": 354930 + } + ], + "leaves": { + "cases": 263, + "max_squared_error_ratio_log2_upper": -42, + "maximum_bits": 183, + "nonzero_errors": 263, + "output_digest": "f20fcbfddc3341510a297f7c58d1ef687666d23995b4f38ba8eccf58b7f2929a" + }, + "phases": { + "cases": 910, + "coefficient_bits": [ + 10, + 25, + 72, + 104 + ], + "output_digest": "900f8fe4f6c0c79f556d19c4cf6aa0d3f549055d76c9377d45132b42302a463a", + "small_moduli": [ + 1, + 24 + ], + "wide_modulus_bits": 81 + }, + "retained_kernel": { + "cases": [ + { + "bits": 239, + "dirt": "7", + "embedding": 1, + "length": 5, + "output_digest": "ba90948923b8c2d6acb8a06018c2d6744fc0c3a2d0219ecef386e66976727c0e", + "radix": 4, + "stride": 2, + "total_bound_log2_upper": -130 + }, + { + "bits": 275, + "dirt": "1099511627776", + "embedding": 1, + "length": 8, + "output_digest": "0f3c6081e92119c15f165abd7b8a2bb03a7cb8e2dedb1c1443d89a82e627bd2c", + "radix": 4, + "stride": -3, + "total_bound_log2_upper": -129 + } + ], + "factor_residual_log2_upper": -1022, + "inverse_perturbation_log2_upper": -988 + }, + "schema": 1, + "source_pins": 14 +} diff --git a/research/dirty-stride-phases/NOTICE.md b/research/dirty-stride-phases/NOTICE.md new file mode 100644 index 0000000000..ddb3b67bc9 --- /dev/null +++ b/research/dirty-stride-phases/NOTICE.md @@ -0,0 +1,38 @@ +# Attribution and license + +New material is prepared for Ali Romman (@aliromman), with substantial +OpenAI Codex assistance in research, derivation, implementation, checks, +and writing. One assigned AI agent prepared this package. Parent-agent +review is separate from independent human review. + +The new material uses Apache-2.0. Retained files keep their original bytes, +licenses, and notices. `SOURCE.json` records exact Git-blob and SHA256 pins. + +- Ali Romman's PR985 supplies the dirty arbitrary-stride solver, two-tape + transport, source-prefix closure, complete factor word, and inherited + conservative precision proof. The local code reads each validation value + once into a scalar. This makes the literal accesses agree with the meter. + The two edits are shown in `DERIVATION.diff`; the vendor copy is unchanged. +- Rohan Guliani's PR846 supplies the Euclidean decomposition. Charles + Bethin's PR764 supplies the shared-suffix estimate used in that lineage. +- Chafik Boukhalfa's PR479 supplies the retained chirp family and the exact + single-axis finite-difference rule. Its multi-axis stream and faster + scalar cost are not implemented or claimed by this package. +- Ross Richardson's PR948 checks PR479's state transitions by separate + symbolic and integer methods. It was read for scope and prior evidence; + no PR948 code is executed here. +- Chafik Boukhalfa's PR628 supplies the factor fixtures, dirty commutator, + and kernel certificates retained by PR985. The new radix-four check uses + its original root bytes and a separate exact polynomial/dense calculation. +- The retained manuscript supplies the chirp identity and transform context. + The PR621/PR628 kernel lineage credits OpenAI's exact-DFT preprint, + classical Newton and q-Pochhammer factorization, Alexey Kuznetsov, and + the methods listed in the original retained notices. + +Quadratic finite differences, the Machin identity, Taylor error estimates, +and three-shear plane rotations are established methods. No literature +priority is claimed. The contribution is their paid reversible phase +interface around the specific dirty solver and complete factor word. + +No new kappa, selected supplier, measured speedup, full transform, scalar +bit-reversible compiler, or full multiplication theorem is claimed. diff --git a/research/dirty-stride-phases/PROOF.md b/research/dirty-stride-phases/PROOF.md new file mode 100644 index 0000000000..fdbf277a03 --- /dev/null +++ b/research/dirty-stride-phases/PROOF.md @@ -0,0 +1,410 @@ +# Reversible quadratic phases for a dirty cyclic inverse + +## 1. Contract and the changed operator + +Let `Z^w x` have entry `x_((i-w) mod L)`. Let + + D_i = exp(2 pi i a i^2 / m), 0 <= i < L, + +where `a` is an integer and `m` is a positive integer. All phase residues +are reduced modulo `m`. No array of phase values is an input or a temporary. +The arrays are distinct arrays of complex dyadic numbers with grid spacing +`u=2^-W`. The source, target, and borrowed arrays can all contain arbitrary +nonzero data. The implementation measures an upper bound `B` on their +initial complex moduli by a paid scan of their component absolute sums. +Use the maximum complex modulus as the norm of an array, and use its +induced operator norm. + +The main leaf, with no output shift or multiplier, approximates + + y <- y + (I - b D Z^w D^-1)^-1 x, + +where `0 < beta <= 1/2` and `|b| <= 1-beta`. The source is restored exactly. +More generally, the optional constant multiplier `v` and allowed output +shift `s` give the increment + + D v Z^s (I-b Z^w)^-1 D^-1 x, s=0 or s=w modulo L. + +A negative call is the exact inverse instruction word. It approximates the +negative increment. It is not implemented by negating an approximate answer. +The error can depend on the initial dirty target. The precision bound below +includes that dependence. + +The complete factor interface implements `D F D^-1`, where `F` is the +complete PR985 factor word. This needs four phase passes for the whole word, +independent of its leaf count. The borrowed arrays keep the PR985 budget +`h=ceil(log2 n)` for `n` factors. This interface requires exactly `h` arrays. +It restores every borrowed array exactly. Only the source and target pass +through the phase maps; borrowed data can stay arbitrary. + +This changes the site coefficients. Put `U=D Z^w D^-1`. Its entry is + + (Ux)_i = exp(2 pi i a (i^2-j^2)/m) x_j, + j=(i-w) mod L. + +For the retained example `L=8, a=-3, m=16, w=3`, the phase residues on these +edges are `11, 9, 7, 5, 3, 1, 15, 13`. They are not one constant gauge. +The verifier separates its response from the unphased inverse by more than +`1/8` in a real component for a unit source and `b=1/2`. + +## 2. Relation to a retained transform + +PR479 and the retained manuscript use + + a_j = exp(-pi i sum_k s_k j_k^2/t_k). + +The new interface covers each single-axis family exactly: set `L=t`, +`a=-s`, and `m=2t`. For even `t`, this is the retained periodic chirp +`exp(-pi i s j^2/t)`. The sign, including its conjugate, is available by +changing the sign of the integer numerator. Arbitrary positive moduli and +integer numerators also give a well-defined diagonal on a finite array; +periodicity outside that array is not assumed. + +This is an executable dirty realization for that phase family. It is not a +complete transform. It does not implement the multi-axis mixed-radix stream, +arbitrary supplied phase arrays, variable coefficient magnitudes, or a +general variable-coefficient Euclidean solver. It does not replace PR479's +fast scalar interface or its asymptotic scalar row. The slower elementary +phase evaluator used here is fully charged in Section 7. + +## 3. Phase generation and coefficient accuracy + +Each array pass starts with `E=0` and `delta=a mod m`. After it uses index `j`, +it updates + + E <- (E+delta) mod m, + delta <- (delta+2a) mod m. + +Induction gives `E=a j^2 mod m` and `delta=a(2j+1) mod m` before each use. +This is the single-axis finite-difference rule from PR479. The implementation +restarts the rule on every pass. It never reads a stored coefficient table. + +Set `C=W+8`, `P=C+2 bit_length(C+32)+20`, and `e=2^-P`. At each index let + + q = floor(4E/m + 1/2), + h = 4E-q m, + theta = pi h/(2m). + +Then `|h| <= m/2`, `|theta| <= pi/4`, and +`exp(2 pi i E/m) = i^q exp(i theta)`. The code keeps `q modulo 4` after it +forms `h`. A zero `h` has exact zero shear coefficients. + +The remaining cases use the following explicit approximation. These are +error bounds for the executed routine, not assumptions supplied by its +admission guard. + +1. Use `pi = 16 atan(1/5) - 4 atan(1/239)`. Each arctangent uses its first + `P` alternating terms. Round each term separately to spacing `e`. Its + rounding error is at most `e/2`. Its omitted tail is less than `e` by + the alternating-series bound. Both Machin weights are included. Thus + the error in `pi_approx` is at most `(10P+20)e`. +2. Round `pi_approx*h/(2m)` to the same spacing. The resulting angle `X` + differs from `theta` by at most `(3P+6)e`. For the admitted `P` this + also proves `|X|<1`. +3. Start the sine term at `X` and the cosine term at `1`. For `k=1,...,P-1`, + multiply by `-X^2/((2k)(2k+1))` for sine and + `-X^2/((2k-1)(2k))` for cosine, rounding each new term to spacing `e`. + These recurrence factors have modulus at most `1/2`. If the preceding + term error is at most `e`, the next is at most `e/2+e/2=e`. Summing the + `P-1` term errors and the Taylor tail costs at most `Pe`. The tail is + less than `e` since `|X|<1` and `(2P)! > 2^P`. Both sine and cosine + are 1-Lipschitz on the real line. The total error against their values + at `theta` is therefore at most `E0=(4P+8)e`. +4. The exact cosine is at least `sqrt(2)/2`; `E0<1/4`. Thus the computed + `1+cosine` is greater than `1`, as is the exact denominator. Subtract + the two quotients to bound the error in `sine/(1+cosine)` by `2E0`. + The final internal division rounding adds at most `e/2`. The bound + `(8P+17)e` covers this result. +5. Round sine and tangent once more to spacing `2^-C`. The program checks + `(8P+17)2^-P <= 2^(-C-2)`. This holds for the stated `P`; it is also a + fail-closed integer/rational guard. To check all admitted widths, put + `b=bit_length(C+32)`. Then `C>=10`, `b>=6`, and `P<3*2^b`. Thus + `8P+17<2^(b+5)<=2^(2b+18)=2^(P-C-2)`. Each final coefficient is within + `3*2^-C/4 < 2^-C` of its exact value. In particular the rounded + coefficients satisfy `|tangent|<=1/2` and `|sine|<=1`. + +All polynomial sums are sums of dyadic values and are exact. No uncharged +trigonometric library call or supplied approximate root is used. The +independent oracle computes outward rational intervals for the full angle +`2 pi E/m`. It does not use the quadrant reduction, shears, recurrence of +residues, or production term rounding. + +## 4. An exactly reversible grid rotation + +For exact `t=tan(theta/2)` and `s=sin(theta)`, the three real shears + + x1 = x - t y, + y1 = y + s x1, + x2 = x1 - t y1 + +give the rotation by `theta`. This follows from +`1-st=cos(theta)` and `-2t+s t^2=-sin(theta)`. Append the exact quarter-turn +`i^q`. In the implementation each product in a shear is rounded to spacing +`u`, with ties toward positive infinity. Each subtraction or addition is +exact on the grid. + +The inverse first reverses the quarter-turn, then executes + + x1 = x2 + rnd(t y1), + y = y1 - rnd(s x1), + x = x1 + rnd(t y). + +Every rounded value in this inverse is the same rounded value that the +forward instruction used. Thus the inverse restores both components +exactly for every grid input, with no sign-symmetry assumption about the +rounding rule. Different array sites are disjoint, so both directions can +scan in increasing physical index order. + +Let `S_i` be this grid permutation and let `D_i` be the exact unit phase. +A shear with coefficient modulus at most `1` has Euclidean operator norm +at most `2`. The product of the other two shears has norm at most `4`. +The difference caused by the three coefficient errors is at most +`12*2^-C |z|`. The three data-rounding errors contribute at most +`(4+2+1)u/2`. Quarter-turns have norm `1`. The same reasoning applies to the +reverse word. Hence, in both directions, + + |S_i(z)-D_i z| <= 4(|z|+1)u, + |S_i^-1(z)-D_i^-1 z| <= 4(|z|+1)u. (1) + +The sharper coefficient contribution is not needed. The program uses the +same immutable descriptor, precision and deterministic evaluator in both +directions. No coefficient approximation is recovered from modified data. + +## 5. Conjugation, restoration, and the dirty-value error + +Execute, in this order: + + S^-1 on x; S^-1 on y; + the complete pinned dirty word A, with the requested sign; + S on y; S on x. + +The middle word restores its source and every borrowed array exactly. The +outer maps are exact grid inverses. Consequently the whole construction +restores the original source and all borrowed arrays exactly. Replacing +`A` by its complete inverse gives the exact inverse of this whole word. + +Suppose the ideal increment of the middle word is `F x`, with operator norm +at most `K`, and its execution error at initial array bound `D0` is at most + + H(D0+1)u. + +Both signs have the same bound. Require `W>=2`, the inherited PR985 admission, +and `3Hu<=1`. From (1), the transformed arrays have norm at most +`2(B+1)`; the unchanged borrowed arrays also satisfy this bound. Thus the +middle error is at most `3H(B+1)u <= B+1`. If `V` is the target just after +the middle word, then + + |V| <= (3+2K)(B+1). + +The first target transformation contributes at most `4(B+1)u` to final +error. The first source transformation contributes at most `4K(B+1)u`. +The middle word contributes at most `3H(B+1)u`. The final target rotation +contributes at most `(16+8K)(B+1)u`. Their sum is at most + + 32(1+K+H)(B+1)u. (2) + +This proves the stated error against the ideal phased operator, including +large dirty targets. It does not assume that the rounded increment is +independent of those targets. It does not tighten PR985's precision result. + +For a leaf, let `M>=max(1,|v|)`. The program uses the component absolute sum +of the constant multiplier as one such bound. From the pinned leaf theorem, +we can use + + H=68 M/beta^5, K=M/beta. + +For a complete word with `n` factors, let `r>=1` bound every factor scale. +The validated inner multiplier has modulus at most `r`; the outer multiplier +also has modulus at most `r` since `|b|<1`. Put + + N(1)=1, + N(n)=2N(floor(n/2))+2N(ceil(n/2)), + G=2+r/beta, + H=N*68(r+1)*G^(N-1)/beta^5, + K=G^N. + +PR985 supplies the middle execution bound with this `H`. Each ideal factor +has norm at most `r/beta`; `N>=n`, so `K` bounds the product. Exactly `N` +leaves and both signs of every dirty commutator are executed. The generic +kernel tests do not claim that arbitrary input factors are a certified +approximation to a particular retained polynomial. + +To pay execution error to `2^(-p-1)`, `working_bits` takes the maximum of +incoming grid precision, `2`, + + p+1+ceil(log2(32(1+K+H)(B+1))), + ceil(log2(3H)), + ceil(log2(48(depth(L,w)+1)/beta^3)). + +A retained factor certificate must separately pay its approximation error, +scaled by the source norm. Unit diagonal conjugation preserves that norm +bound. The radix-four test does this explicitly in Section 8. + +## 6. Data tapes, magnitude, and storage + +The local `dirty_stride.py` has two small changes from the pinned source. +Each input-validation loop reads `data[i]` once into a scalar before it +compares the rounded value. The predecessor expression read it twice but +charged one access. `DERIVATION.diff` records both changes. No arithmetic +or transport instruction in the inverse solver is changed. A separate array +observer checks literal reads and writes against the reported meter and +also gives a physical-movement lower bound. The original source stays in +`vendor/pr985/` with exact byte pins. + +Use the same two physical data tapes as PR985. A leaf puts one array on each +tape. A complete word puts its last borrowed array on tape B and its source, +target and other borrowed arrays consecutively on tape A. The inherited +routing swaps a leaf target onto B when necessary and restores that carrier. +No tape head is assigned separately to each array. + +Every array read and write, including phase scans and input validation, +charges the distance from the previous physical head position plus one. +The wrapper returns both heads to their origins before the middle word and +after the final phase passes. The middle word also pays its own returns. +The phase generator uses constant scalar registers beside the parked data +head. Reading or writing a complex record costs its complete record width. + +For a leaf, input validation costs at most `4L` record moves. The four phase +scans cost at most `16L` together. Their head returns cost at most `4L`. +Adding this to PR985's `4096L` bound gives the conservative bound `4160L`. +For a complete word, input validation, phase scans, travel between the +source and target slots, and returns cost at most `64(h+2)L`. Add this to +PR985's `8192(N+1)(h+2)L` bound. The result is at most + + 8256(N+1)(h+2)L. + +No control counter or coefficient tape is counted as a free data tape; their +bit costs are stated in Section 7. + +A leaf uses no borrowed data array. A word uses exactly `h` arbitrary +borrowed arrays. The implementation holds only a constant number of clean +arithmetic registers in phase preparation, rotation, or one leaf. A phase +object contains scalar descriptors and one scalar pi approximation. There +is no list or cache of arithmetic values indexed by `L` or `W`. The array +list in the word contains references to existing arrays only. The `n` +factor descriptors are immutable input records, with `O(nS)` input bits +for descriptor width `S`. Their sequential access is paid below. This +input storage is distinct from clean arithmetic workspace. + +The inherited leaf index stack occupies `O(log^2 L)` metadata bits. The word +also uses `O(log n (log n+log L))` metadata bits. The phase stream adds +`O(log m+log L+log P)` control bits and a constant number of `O(P)` scalar +values. Scalar arithmetic scratch is additional and is included below. +This is not a bit-reversible implementation of its scalar arithmetic. + +An explicit data-magnitude bound is + + 16384(M+1)(B+1)/beta^7 for a leaf, + 16384(r+1)(B+1)G^N/beta^7 for a word. + +PR985 bounds the middle values with transformed input bound `2(B+1)`. +The additional factor covers all three shear intermediates, whose norms +are at most eight times the input plus `4u`. The bound also covers the +untransformed initial arrays. The integer reserve is the ceiling of the +base-two logarithm of this bound, plus two sign/rounding bits. There is no +silent fixed-width overflow assumption. The finite replay measures array +writes and each transient real/imaginary pair inside the phase shears. It +does not measure the internal Machin integer widths; those use the +analytical bound in Section 7. + +## 7. Complete phase and bit cost + +Let `V=bit_length(m)`, and include the original numerator's full input width +when its descriptor is read and reduced. The phase stream uses `O(V)` bit +additions and reductions at each site. Its exact quadratic residue needs +no large square. Initial descriptor normalization and all precision-control +arithmetic are paid setup operations. + +One invocation prepares pi once, with `2P` rounded terms. It then evaluates +exactly `4L` phase coefficients. Each nontrivial evaluation has `2(P-1)` +Taylor terms. With the counters used by the reference, the phase layer has +at most + + 2P(4L+1) Taylor/Machin terms, + 4P(4L+1) counted scalar products, + 2P(4L+1) counted scalar divisions. + +The product total includes the three data shears per phase use. Integer +loop expressions and grid rounding are not extra unit-cost oracles: they +are included in the bit cost below. The scalar-operation count is +`O((L+1)P)`, not `O(L)`. The phase setup is not repeated at each inner leaf +of a complete factor word. + +The largest Machin power is below `239^(2P+1)`, so it has fewer than +`16P+8` bits. Every term is rounded before it is added to an accumulator. +The Taylor products and denominators have `O(P+V+log P)` bits. Include the +fractional precision, integer data reserve, original immutable coefficient +and phase-descriptor widths, and these phase temporaries in a scalar size +`T`. The exact rational budget constants `H` and `K` must also fit. If `S` +bounds the bit widths of each input scalar descriptor, their numerators and +denominators can have `O((N+1)S)` bits even when their magnitudes are small. +A constant multiple of `(N+1)S+P+V+2W+I+log L` suffices for `T`, where `I` +is the integer data reserve. This pays the rational control values as well +as the data arithmetic. It gives `O(T)` scalar storage, with a fixed number +of arithmetic work tapes. + +Let `C(T)` pay a scalar product or quotient, including rounding, on that +workspace. Schoolbook fixed-width arithmetic gives the sufficient choice +`C(T)=O(T^2)` on a fixed number of tapes. The exact-rational Python program +is a reference for the instructions and rounding. It is not a timing +implementation of that tape bound. + +For the complete `n`-factor word, a conservative paid bill is + + external factor production + + O((N L + (L+1)P + n+N+1) C(T)) + + O(N(h+2)L T + n N T) + + O((L+1)V + L log L). + +The API takes the factor descriptors as inputs; their production is an +inherited external cost and is not improved here. The `n+N+1` term pays +descriptor normalization, factor-margin validation, and the exact rational +precision-control computation, including binary powers and leaf counting. +The `n N T` term pays worst-case sequential factor-descriptor access for +every leaf. Validation of factor margins, source reads, all copies and +swaps, inverse calls, rounding, Euclidean children, and both head returns +are included. The elementary phase setup and term counters fit the displayed +phase cost. Oversized input descriptors and computing the precision bound +are included in setup; their lengths are not inferred from their magnitudes. +For a leaf use `N=1`, `h=0` and its constant descriptor cost. + +This construction does not inherit PR479's fast exponential complexity. +It supplies an explicit, slower complete phase interface. Fast phase +preparation can replace it only with a separate workspace and error proof. +No new supplier constant or kappa follows from this bill. + +## 8. Independent checks and a retained kernel + +The checker uses an outward rational interval oracle for full-angle sine +and cosine. It computes residues by direct integer squares. It evaluates +cyclic inverses by finite geometric sums. Thus it does not repeat the +production finite differences, shear rotation, or Euclidean recursion. +All error comparisons include the oracle interval width. + +For the retained `r=4, k=1` polynomial, set `zeta=i`. Its coefficients are +`(1/r) product_(s=j+1)^(r-1)(1-zeta^s)`, hence + + Q(X)=1+(1+i)X/2+(1+i)X^2/4+X^3/4. + +The unchanged PR628 root fixture, retained by PR985, gives a rational +factor polynomial `Qhat`. The checker expands its roots exactly and bounds +`epsilon=sum_j |Q_j-Qhat_j|` by component absolute sums. It checks each +stable factor margin. Therefore `A=4/beta^3` bounds `Qhat(U)^-1` for every +unitary weighted cyclic shift `U` in this family. If `A epsilon<1`, the +resolvent identity gives + + ||Q(U)^-1-Qhat(U)^-1|| <= A^2 epsilon/(1-A epsilon). + +The checker adds this bound times the source norm to (2). It separately +uses exact rational Gaussian elimination on the matrix for `Q(tau Z^w)`, +with interval right-hand sides after the ideal chirp. Two executions use +nonconstant quadratic chirps, dirty borrowed arrays, and the 128-bit total +budget. The length-eight case is in the retained periodic phase family. +Both the dense ideal comparison and exact complete-word inverse +are checked. This validates these cases and their stated uniform analytic +bound. It is not a complete-transform or multiplication verification. + +The finite replay is evidence for the written statements. It is not a Lean +proof, an independent human review, or a proof that the inherited PR985, +all-size compiler, common-label, physical supplier, analytic-transfer, and +multiplication assumptions hold. diff --git a/research/dirty-stride-phases/README.md b/research/dirty-stride-phases/README.md new file mode 100644 index 0000000000..2a4091ff32 --- /dev/null +++ b/research/dirty-stride-phases/README.md @@ -0,0 +1,63 @@ +# A nonconstant chirp for the dirty cyclic inverse + +This research construction adds the quadratic diagonal +`D_j=exp(2 pi i a j^2/m)` to PR985's dirty arbitrary-stride solver. The leaf +adds an approximation to `(I-b D Z^w D^-1)^-1 x` to a dirty target. It +restores the source exactly, needs no extra data array, and uses a constant +number of clean arithmetic registers. A negative call is its exact grid +inverse. The complete factor interface uses the original logarithmic +borrowed-array budget and pays only four phase passes for the whole word. + +The site coefficients are nonconstant. For `L=8, a=-3, m=16, w=3`, the +shift-edge phase residues are `11,9,7,5,3,1,15,13`. The family includes the +retained single-axis transform chirp `exp(-pi i s j^2/t)` by taking even +`L=t`, `a=-s`, and `m=2t`. + +`chirp.py` generates each coefficient from exact integer residues with a +rounded Machin/Taylor evaluator. It implements each rotation with three +reversible real shears and an exact quarter-turn. There is no clean phase +array, cached table, or free phase lookup. Both forward and inverse maps +have a conservative error bound that includes the initial dirty values. +See [PROOF.md](PROOF.md) for the full coefficient, precision, workspace, +restoration, and tape bill. + +The phase layer costs `O((L+1)P)` scalar steps, where `P=W+O(log W)` and `W` +is the complete working precision. It does not retain an `O(L)` scalar +count or PR479's fast exponential bound. The data movement stays linear: +`4160L` record moves per leaf is a conservative bound on the two physical +data tapes. A complete word uses its charged PR985 routing plus four phase +passes. Scalar work tapes and descriptor access are also paid in the proof. + +Run with Python 3.11 or later and the standard library: + +```sh +python3 -I -O -B research/dirty-stride-phases/verify.py +python3 -I -O -B research/dirty-stride-phases/test_package.py +``` + +The first command checks 910 phase cases, 263 rounded leaf executions, +20 complete generic factor words, two retained radix-four kernel cases, +four larger movement fixtures, and invalid-input controls. All 263 leaf +cases have a nonzero error against the independent ideal interval oracle. +The inputs include odd lowest grid bits and dirty values through `2^80`. +The two retained kernels pay both factor error and execution error to the +128-bit target. The second command checks source mutations and package +relocation. `VALIDATION.json` records the completed checks and their limits. + +The oracle uses full-angle rational intervals, direct quadratic residues, +finite geometric sums, and exact dense polynomial elimination. It does +not call the production phase or inverse solver. These are separate +computational paths, not independent human review or a formal theorem. +The exact deterministic receipt is [EXPECTED.json](EXPECTED.json). +`--write /absolute/new/receipt.json` writes a new receipt without overwrite. + +Base: `8bddbee377e2f3ce1f1247196c4b290d55767d20`. +PR985 dependency: `9df42a99dd8497b6e7d46cd2507bb89071372640`. +[Source pins](SOURCE.json) and [attribution](NOTICE.md) keep the predecessor +sources and substantial AI-assistance disclosure explicit. + +No new kappa is claimed. The selected frontier and `upstream/` are unchanged. +Arbitrary supplied phase arrays, multi-axis tensor streams, variable +coefficient magnitudes, full-transform composition, fast phase evaluation, +common-label compilation, physical supplier hosting, and the multiplication +reduction remain outside this construction. diff --git a/research/dirty-stride-phases/SOURCE.json b/research/dirty-stride-phases/SOURCE.json new file mode 100644 index 0000000000..3fc9cd2d0a --- /dev/null +++ b/research/dirty-stride-phases/SOURCE.json @@ -0,0 +1,123 @@ +{ + "base": "8bddbee377e2f3ce1f1247196c4b290d55767d20", + "sources": [ + { + "pr": 985, + "commit": "9df42a99dd8497b6e7d46cd2507bb89071372640", + "path": "research/dirty-stride-source-reuse/dirty_stride.py", + "local": "vendor/pr985/dirty_stride.py", + "sha256": "129b2bc8cf89159aae0a810fad4703caefefccf1c5f4805dd3c9b5e8d967354b", + "blob": "f469930b8b7d79cbc05a884dc2e224e32db7fc4a" + }, + { + "pr": 985, + "commit": "9df42a99dd8497b6e7d46cd2507bb89071372640", + "path": "research/dirty-stride-source-reuse/PROOF.md", + "local": "vendor/pr985/PROOF.md", + "sha256": "af6560b048b20649aebd31d68815948a104d2c87efcdf556c85a10f48bbc0489", + "blob": "01a3da73470dc773a33948ee5f8cfc8848798411" + }, + { + "pr": 985, + "commit": "9df42a99dd8497b6e7d46cd2507bb89071372640", + "path": "research/dirty-stride-source-reuse/NOTICE.md", + "local": "vendor/pr985/NOTICE.md", + "sha256": "759fd9ada0c70e657a0b903089b32c84239b05b1f214cb01e81e9ca61b0d87f4", + "blob": "a96d0c7fea342d1e6990b4d16d731038ba983511" + }, + { + "pr": 985, + "commit": "9df42a99dd8497b6e7d46cd2507bb89071372640", + "path": "research/dirty-stride-source-reuse/README.md", + "local": "vendor/pr985/README.md", + "sha256": "96527e5f166ab8223e5c652975f32b4ba1b6b1d7fd41667a46bf515571fdaf13", + "blob": "451ac2bac0cc263d03f3a489fc5dabd653e9a4c5" + }, + { + "pr": 985, + "commit": "9df42a99dd8497b6e7d46cd2507bb89071372640", + "path": "research/dirty-stride-source-reuse/LICENSE", + "local": "vendor/pr985/LICENSE", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64" + }, + { + "pr": 479, + "commit": "40dd01058439cdffae3e3b41c4fe52edaccf5f91", + "path": "research/streamed-chirp-phases/README.md", + "local": "vendor/pr479/README.md", + "sha256": "ce0750869369141e7f1e70f8f5872a0b8d0a72b33bd0aad163798f64ee0ed442", + "blob": "b75ad5c75b6ab221e362771f2a788e54700806a8" + }, + { + "pr": 479, + "commit": "40dd01058439cdffae3e3b41c4fe52edaccf5f91", + "path": "research/streamed-chirp-phases/PROOF.md", + "local": "vendor/pr479/PROOF.md", + "sha256": "0c4438e09ec34ec8208dff90851fbc05bee0cbbefcac4d90208cfc63facc0207", + "blob": "fd05f84d603a509db594122c723d19cdf1cb029a" + }, + { + "pr": 479, + "commit": "40dd01058439cdffae3e3b41c4fe52edaccf5f91", + "path": "research/streamed-chirp-phases/SOURCE.json", + "local": "vendor/pr479/SOURCE.json", + "sha256": "a90653f2ab1a1ac32880e2b3818c13b8b7a6c3972b67f0f769ecb6641d8170ab", + "blob": "53657bfc2985f8cf4038347e5f577238ee2cac46" + }, + { + "pr": 628, + "retained_by_pr": 985, + "commit": "9df42a99dd8497b6e7d46cd2507bb89071372640", + "path": "research/dirty-stride-source-reuse/vendor/pr628/FACTORS.json", + "local": "vendor/pr628/FACTORS.json", + "sha256": "643d60ac24d5e67f6c9305175bd1c99bf5e42edfef6d1995c051e0b98ba446a7", + "blob": "d3894bd2a1660229f1a7ed16c9d982689effc96f" + }, + { + "pr": 628, + "retained_by_pr": 985, + "commit": "9df42a99dd8497b6e7d46cd2507bb89071372640", + "path": "research/dirty-stride-source-reuse/vendor/pr628/NOTICE.md", + "local": "vendor/pr628/NOTICE.md", + "sha256": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68", + "blob": "22fbeb8ef0a28dd6b3feea718492091319ceb96e" + }, + { + "pr": 628, + "retained_by_pr": 985, + "commit": "9df42a99dd8497b6e7d46cd2507bb89071372640", + "path": "research/dirty-stride-source-reuse/vendor/pr628/SOURCE.json", + "local": "vendor/pr628/SOURCE.json", + "sha256": "38a425e2d3a72a5e39b18b54c728e40407e121d481a1c6423edd5c18e9b68a04", + "blob": "59bddaea4d66725bf675a67b6d2cf85a061b1fae" + }, + { + "pr": 628, + "retained_by_pr": 985, + "commit": "9df42a99dd8497b6e7d46cd2507bb89071372640", + "path": "research/dirty-stride-source-reuse/vendor/pr628/check.py", + "local": "vendor/pr628/check.py", + "sha256": "a3e46b556894d71a1c83bbbac01c50c1a541285fc9422a3567d5eb1d1ee86e7d", + "blob": "5ef6dd67b6c6cf949fedf16c0cd7b34ca4ccafc2" + }, + { + "pr": 628, + "retained_by_pr": 985, + "commit": "9df42a99dd8497b6e7d46cd2507bb89071372640", + "path": "research/dirty-stride-source-reuse/vendor/pr628/interval_kernel.py", + "local": "vendor/pr628/interval_kernel.py", + "sha256": "9b7bb24640a9a7d3f83c7951dfef483ec933db4c50de6c0130b85f450eeddfbe", + "blob": "1182175a55cb871481de0f56ea9ae56e474705fe" + }, + { + "pr": 628, + "retained_by_pr": 985, + "commit": "9df42a99dd8497b6e7d46cd2507bb89071372640", + "path": "research/dirty-stride-source-reuse/vendor/pr628/scan.py", + "local": "vendor/pr628/scan.py", + "sha256": "1a9c01ca1a29a9be1e756858161202621db29d5d332a4266b4017a9502a50d7e", + "blob": "d620e493596f12578c1ce47f216c44c79b65de08" + } + ] +} diff --git a/research/dirty-stride-phases/VALIDATION.json b/research/dirty-stride-phases/VALIDATION.json new file mode 100644 index 0000000000..a4db243e56 --- /dev/null +++ b/research/dirty-stride-phases/VALIDATION.json @@ -0,0 +1,207 @@ +{ + "base": "8bddbee377e2f3ce1f1247196c4b290d55767d20", + "completed": [ + { + "check": "Primary isolated optimized replay and receipt generation", + "command_template": "python3 -I -O -B research/dirty-stride-phases/verify.py --write /absolute/new/receipt.json", + "max_resident_bytes": 28360704, + "real_seconds": 65.2, + "result": "PASS_DIRTY_STRIDE_PHASES phases=910 leaves=263 kernels=20 retained=2 costs=4 input_controls=8", + "system_seconds": 0.6, + "user_seconds": 59.25 + }, + { + "check": "Semantic controls, source binding, type-sensitive receipt and read-only relocation", + "command": "python3 -I -O -B research/dirty-stride-phases/test_package.py", + "max_resident_bytes": 30392320, + "real_seconds": 63.62, + "result": "PASS_DIRTY_PHASE_PACKAGE controls=12 relocation=1 regeneration=1", + "system_seconds": 0.71, + "user_seconds": 57.32 + }, + { + "check": "Selected publication record", + "command": "make selected-record-check", + "result": "PASS selected record, exact kappa, original source inventory and proof supplement: 1661960547713947/1000000000000000000" + }, + { + "check": "Selected-result tests", + "command": "python3 -I -B -m unittest discover -s tests -p 'test_selected*.py'", + "result": "25 tests passed in 1.331 seconds" + }, + { + "check": "Exact inherited derivative", + "result": "DERIVATION.diff is the complete diff from the byte-exact PR985 original. It contains only two read-once validation changes." + }, + { + "check": "Protected source comparison", + "command": "git diff --exit-code 8bddbee377e2f3ce1f1247196c4b290d55767d20 -- certificates upstream docs/research", + "result": "Exit 0; no changes." + }, + { + "check": "Python 3.11 grammar and final source freeze", + "result": "PASS syntax_3_11_and_final_freeze files=25; grammar only, not a Python 3.11 execution." + }, + { + "check": "Staged whitespace", + "command": "git diff --cached --check", + "result": "Exit 0." + } + ], + "date_utc": "2026-10-13", + "development_findings": [ + "Independent literal access observations found two PR985 validation expressions that each read a value twice but charge one read. The local derived file reads each value once. The exact original remains pinned and unchanged.", + "The first relocation attempt after adding phase peak fields rejected an older receipt. A new full execution generated the final receipt; the subsequent complete package replay passed." + ], + "environment": { + "experiment_workers": 1, + "libraries": "Python standard library only", + "platform": "macOS-26.6.1-arm64-arm-64bit-Mach-O", + "python": "3.14.7 (main, Aug 5 2026, 10:29:49) [Clang 21.0.0 (clang-2100.1.1.101)]" + }, + "limits": [ + "Finite exact replay supports the written proof. It is not a formal proof or independent human review.", + "No complete transform, arbitrary supplied phase array, multi-axis stream, variable coefficient magnitude, or fast phase evaluator is implemented.", + "The Python rational reference is not a fast-bit compiler, scalar bit-reversible machine, or runtime speedup.", + "Only the retained radix-four polynomial is checked here; the full set of inherited kernel fixtures is not replayed by this package.", + "The full repository suite and selected cold replay were not run for this isolated addition.", + "Local checks used Python 3.14.7 on macOS arm64. Python 3.11 and Linux hosted CI were not run locally.", + "No selected bound, upstream file, physical supplier, common-label compiler, or multiplication reduction is changed.", + "The reported durations describe local verification runs, not performance benchmarks." + ], + "mathematical_scope": { + "cost": "Four phase passes per whole word; O((L+1)P) phase scalar operations, P=W+O(log W). Descriptor access, scalar workspace, all data access, and two physical data-tape returns are charged.", + "operator": "D (I-b Z^w)^-1 D^-1, with D_j=exp(2 pi i a j^2/m), and conjugation of the complete inherited factor word.", + "peak_observation": "The verifier checks stored array peaks and every transient real/imaginary pair inside the phase shears. Internal Machin integer widths use the analytical bound, not a measured peak.", + "precision": "Conservative coefficient and dirty-conjugation error bound. The two retained radix-four kernel cases also pay their exact factor residual.", + "restoration": "Exact source and borrowed-array restoration and complete-word grid inversion.", + "retained_phase_case": "L=8, a=-3, m=16; the single-axis periodic retained chirp." + }, + "negative_controls": { + "byte_identical_receipt": true, + "controls": [ + { + "name": "wrong_machin_weight", + "rejected": "phase coefficient accuracy" + }, + { + "name": "short_shear_precision", + "rejected": "phase coefficient accuracy" + }, + { + "name": "wrong_forward_shear", + "rejected": "rotation accuracy" + }, + { + "name": "wrong_reverse_shear", + "rejected": "rotation exact inverse" + }, + { + "name": "linear_phase_stream", + "rejected": "phased leaf accuracy" + }, + { + "name": "unrestored_source", + "rejected": "leaf source restoration" + }, + { + "name": "wrong_target_phase", + "rejected": "phased leaf accuracy" + }, + { + "name": "unpaid_phase_read", + "rejected": "paid data accesses" + }, + { + "name": "lost_quadratic_sign", + "rejected": "phased leaf accuracy" + }, + { + "name": "wrong_child_inverse", + "rejected": "kernel source and scratch restoration" + }, + { + "name": "source_bytes", + "rejected": "source SHA256: vendor/pr985/dirty_stride.py" + }, + { + "name": "boolean_receipt", + "rejected": "typed receipt mismatch" + } + ], + "relocated_read_only_replay": true + }, + "read_accounting_audit": [ + { + "kind": "leaf", + "length": 8, + "missing_reads": 16, + "observed_reads": 572, + "observed_writes": 458, + "reported_reads": 556, + "reported_writes": 458, + "source": "original" + }, + { + "kind": "compose", + "length": 8, + "missing_reads": 88, + "observed_reads": 2336, + "observed_writes": 1832, + "reported_reads": 2248, + "reported_writes": 1832, + "source": "original" + }, + { + "kind": "leaf", + "length": 8, + "missing_reads": 0, + "observed_reads": 556, + "observed_writes": 458, + "reported_reads": 556, + "reported_writes": 458, + "source": "derived" + }, + { + "kind": "compose", + "length": 8, + "missing_reads": 0, + "observed_reads": 2248, + "observed_writes": 1832, + "reported_reads": 2248, + "reported_writes": 1832, + "source": "derived" + } + ], + "receipt_sha256": "3305f81e9befe11133e85e0e38b5f0824c7a520d02e1799d5bf703e0bd1df740", + "schema": 1, + "source_freeze": { + "DERIVATION.diff": "07b2cf978a268d365d7e150aa2e1c0f0bc5f574a372433607c6f24d25afb7679", + "EXPECTED.json": "3305f81e9befe11133e85e0e38b5f0824c7a520d02e1799d5bf703e0bd1df740", + "NOTICE.md": "4e56d5e2d74653e96bdbc4da631613593b24e5518d73738a8845829b632cfcad", + "PROOF.md": "bf1dc6ca7f2cb5cdfb95c5f2c773a0840d1f75d7b448382469a963cd442d1c76", + "README.md": "d36497f94f5eab67779b9cdc70f5a257e9ddc87bf38ee0d374a1d49f53b3da21", + "SOURCE.json": "11a5404401e160502ce30e396bc3313e9bd5833de83862308c0c08c9dc19ea6e", + "chirp.py": "63631c48a2578a19962cc41caac7513a83ee3c0cd28d6140a789c8ec78310edd", + "dirty_stride.py": "941b8499a290bd08199c1ac4a6f90ef0e031be0f6249a60db2b6604900f2255a", + "oracle.py": "861eeb9c53b19e893766a517819735cbad1a510deff07b4de938802dc3e16daa", + "test_package.py": "cb26e1e6c3dd4cb5d076ce9805776bf62fadf73842bc15c650ea24283efc90ab", + "vendor/pr479/PROOF.md": "0c4438e09ec34ec8208dff90851fbc05bee0cbbefcac4d90208cfc63facc0207", + "vendor/pr479/README.md": "ce0750869369141e7f1e70f8f5872a0b8d0a72b33bd0aad163798f64ee0ed442", + "vendor/pr479/SOURCE.json": "a90653f2ab1a1ac32880e2b3818c13b8b7a6c3972b67f0f769ecb6641d8170ab", + "vendor/pr628/FACTORS.json": "643d60ac24d5e67f6c9305175bd1c99bf5e42edfef6d1995c051e0b98ba446a7", + "vendor/pr628/NOTICE.md": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68", + "vendor/pr628/SOURCE.json": "38a425e2d3a72a5e39b18b54c728e40407e121d481a1c6423edd5c18e9b68a04", + "vendor/pr628/check.py": "a3e46b556894d71a1c83bbbac01c50c1a541285fc9422a3567d5eb1d1ee86e7d", + "vendor/pr628/interval_kernel.py": "9b7bb24640a9a7d3f83c7951dfef483ec933db4c50de6c0130b85f450eeddfbe", + "vendor/pr628/scan.py": "1a9c01ca1a29a9be1e756858161202621db29d5d332a4266b4017a9502a50d7e", + "vendor/pr985/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "vendor/pr985/NOTICE.md": "759fd9ada0c70e657a0b903089b32c84239b05b1f214cb01e81e9ca61b0d87f4", + "vendor/pr985/PROOF.md": "af6560b048b20649aebd31d68815948a104d2c87efcdf556c85a10f48bbc0489", + "vendor/pr985/README.md": "96527e5f166ab8223e5c652975f32b4ba1b6b1d7fd41667a46bf515571fdaf13", + "vendor/pr985/dirty_stride.py": "129b2bc8cf89159aae0a810fad4703caefefccf1c5f4805dd3c9b5e8d967354b", + "verify.py": "06ff4d614c51433d499cc11fe0df3ee4dd7a63cf98877473c41a4b36804884e5" + }, + "status": "Verified local research construction; no new kappa.", + "workflow_sha256": "91fb9e25d439cb8181542ef8639b2d94b1ed46785c30e585045c5e41a7d351ea" +} diff --git a/research/dirty-stride-phases/chirp.py b/research/dirty-stride-phases/chirp.py new file mode 100644 index 0000000000..8a5c397148 --- /dev/null +++ b/research/dirty-stride-phases/chirp.py @@ -0,0 +1,295 @@ +"""Use reversible quadratic phases around the pinned dirty-array solver.""" +from dataclasses import dataclass +from fractions import Fraction as F +import importlib.util +from pathlib import Path +import sys + +_SPEC = importlib.util.spec_from_file_location( + 'dirty_phase_predecessor', Path(__file__).resolve().parent/'dirty_stride.py') +d = importlib.util.module_from_spec(_SPEC) +sys.modules[_SPEC.name] = d +_SPEC.loader.exec_module(d) + + +def real_round(value, bits): + scale = 1 << bits + value = value*scale + F(1, 2) + return F(value.numerator//value.denominator, scale) + + +@dataclass +class Meter(d.Meter): + phase_evaluations: int = 0 + phase_passes: int = 0 + phase_terms: int = 0 + phase_products: int = 0 + phase_divisions: int = 0 + phase_record_moves: int = 0 + phase_recurrence_steps: int = 0 + input_reads: int = 0 + descriptor_bits: int = 0 + coefficient_bits: int = 0 + internal_bits: int = 0 + error_bound: F = F(0) + initial_bound: F = F(0) + phase_peak_l1: F = F(0) + + +def pi_approx(bits, meter): + """Use the Machin identity and round each arctangent term.""" + value = F(0) + for denominator, scale in ((5, 16), (239, -4)): + power = denominator + for k in range(bits): + term = real_round(F(1, (2*k+1)*power), bits) + value += scale*term if k % 2 == 0 else -scale*term + power *= denominator*denominator + meter.phase_terms += 1 + meter.phase_divisions += 1 + meter.phase_products += 2 + return value + + +@dataclass(frozen=True) +class Phase: + numerator: int + modulus: int + bits: int + internal: int + pi: F + meter: Meter + + @classmethod + def prepare(cls, numerator, modulus, bits, meter): + d.need(type(numerator) is int and type(modulus) is int and modulus > 0, + 'integer phase descriptor') + d.need(type(bits) is int and bits >= 2, 'phase precision') + coefficient_bits = bits+8 + internal = coefficient_bits + 2*(coefficient_bits+32).bit_length()+20 + d.need((8*internal+17)*F(1, 1 << internal) + <= F(1, 1 << (coefficient_bits+2)), 'phase coefficient budget') + meter.descriptor_bits += abs(numerator).bit_length()+modulus.bit_length()+2 + meter.coefficient_bits = coefficient_bits + meter.internal_bits = internal + return cls(numerator % modulus, modulus, bits, internal, + pi_approx(internal, meter), meter) + + def coefficients(self, residue): + """Return a quarter-turn and two dyadic shear coefficients.""" + d.need(type(residue) is int and 0 <= residue < self.modulus, 'phase residue') + self.meter.phase_evaluations += 1 + quadrant = (8*residue+self.modulus)//(2*self.modulus) + remainder = 4*residue-quadrant*self.modulus + if remainder == 0: + return quadrant % 4, F(0), F(0) + angle = real_round(self.pi*remainder/(2*self.modulus), self.internal) + self.meter.phase_products += 1 + self.meter.phase_divisions += 1 + d.need(abs(angle) <= 1, 'reduced angle') + sine = sine_term = angle + cosine = cosine_term = F(1) + for k in range(1, self.internal): + sine_term = real_round(-sine_term*angle*angle/((2*k)*(2*k+1)), self.internal) + cosine_term = real_round(-cosine_term*angle*angle/((2*k-1)*(2*k)), self.internal) + sine += sine_term + cosine += cosine_term + self.meter.phase_terms += 2 + self.meter.phase_products += 4 + self.meter.phase_divisions += 2 + tangent = real_round(sine/(1+cosine), self.internal) + self.meter.phase_divisions += 1 + tangent = real_round(tangent, self.bits+8) + sine = real_round(sine, self.bits+8) + d.need(abs(tangent) <= F(1, 2) and abs(sine) <= 1, 'bounded phase shears') + return quadrant % 4, tangent, sine + + +def quarter_turn(value, quadrant): + real, imag = value + if quadrant == 0: + return value + if quadrant == 1: + return -imag, real + if quadrant == 2: + return -real, -imag + return imag, -real + + +def observe_phase(value, meter): + if meter is not None: + meter.phase_peak_l1 = max(meter.phase_peak_l1, abs(value[0])+abs(value[1])) + + +def rotate(value, coefficients, bits, inverse=False, meter=None): + """Apply three grid shears. The inverse uses the reverse instruction order.""" + quadrant, tangent, sine = coefficients + observe_phase(value, meter) + if inverse: + real, imag = quarter_turn(value, (-quadrant) % 4) + real += real_round(tangent*imag, bits) + observe_phase((real, imag), meter) + imag -= real_round(sine*real, bits) + observe_phase((real, imag), meter) + real += real_round(tangent*imag, bits) + observe_phase((real, imag), meter) + result = real, imag + else: + real, imag = value + real -= real_round(tangent*imag, bits) + observe_phase((real, imag), meter) + imag += real_round(sine*real, bits) + observe_phase((real, imag), meter) + real -= real_round(tangent*imag, bits) + observe_phase((real, imag), meter) + result = quarter_turn((real, imag), quadrant) + if meter is not None: + meter.phase_products += 3 + return result + + +def phase_pass(data, phase, inverse): + """Scan one array. Use quadratic finite differences and no phase table.""" + meter = phase.meter + before = meter.tape_moves + residue = 0 + difference = phase.numerator + for i in range(len(data)): + coefficients = phase.coefficients(residue) + meter.access(data, i) + value = rotate(data[i], coefficients, phase.bits, inverse, meter) + meter.access(data, i, True) + data[i] = value + residue = (residue+difference) % phase.modulus + difference = (difference+2*phase.numerator) % phase.modulus + meter.phase_recurrence_steps += 1 + meter.phase_passes += 1 + meter.phase_record_moves += meter.tape_moves-before + + +def _validate_arrays(arrays, bits, meter): + d.need(type(bits) is int and bits >= 2, 'working precision') + d.need(arrays and len(arrays[0]) > 0, 'nonempty arrays') + d.need(len({id(a) for a in arrays}) == len(arrays), 'distinct arrays') + length = len(arrays[0]) + d.need(all(len(a) == length for a in arrays), 'equal array lengths') + bound = F(0) + for data in arrays: + for i in range(length): + meter.access(data, i) + meter.input_reads += 1 + value = data[i] + d.need(isinstance(value, tuple) and len(value) == 2 + and all(type(v) in (int, F) for v in value), 'rational complex data') + d.need(d.rnd(value, bits) == value, 'fixed grid data') + bound = max(bound, abs(value[0])+abs(value[1])) + meter.initial_bound = bound + return bound + + +def _word_budget(bits, beta, length, stride, base_error, operator_norm, bound): + d.need(d.admitted(beta, bits, d.depth(length, stride)), 'inherited precision admission') + unit = F(1, 1 << bits) + d.need(3*base_error*unit <= 1, 'conjugation precision admission') + return 32*(1+operator_norm+base_error)*(bound+1)*unit + + +def _phase_descriptor(numerator, modulus): + d.need(type(numerator) is int and type(modulus) is int and modulus > 0, + 'integer phase descriptor') + + +def _coefficient(value): + return isinstance(value, tuple) and len(value) == 2 and all(type(v) in (int, F) for v in value) + + +def lift(x, y, b, beta, bits, stride, numerator, modulus, + sign=1, multiplier=d.ONE, shift=0): + """Add D times the pinned cyclic inverse times D inverse to a dirty target.""" + _phase_descriptor(numerator, modulus) + d.need(type(stride) is int and type(shift) is int + and type(sign) is int and sign in (-1, 1), 'integer stride and sign') + d.need(type(beta) in (int, F) and 0 < beta <= F(1, 2), 'stable margin') + d.need(_coefficient(b) and d.norm2(b) <= (1-beta)**2, 'stable coefficient') + d.need(_coefficient(multiplier), 'constant multiplier') + d.need(len(x) > 0 and shift % len(x) in (0, stride % len(x)), 'supported output shift') + meter = Meter() + meter.layout = {id(x): (0, 0), id(y): (1, 0)} + bound = _validate_arrays((x, y), bits, meter) + multiplier_bound = max(F(1), abs(multiplier[0])+abs(multiplier[1])) + base_error = 68*multiplier_bound/beta**5 + operator_norm = multiplier_bound/beta + meter.error_bound = _word_budget(bits, beta, len(x), stride, base_error, operator_norm, bound) + phase = Phase.prepare(numerator, modulus, bits, meter) + phase_pass(x, phase, True) + phase_pass(y, phase, True) + meter.rewind() + d.lift(x, y, b, beta, bits, stride, sign, multiplier, shift, meter) + phase_pass(y, phase, False) + phase_pass(x, phase, False) + meter.rewind() + return meter + + +def compose(x, y, factors, scratch, tau, beta, bits, stride, numerator, modulus, sign=1): + """Conjugate a complete PR985 factor word. Restore all borrowed arrays.""" + _phase_descriptor(numerator, modulus) + d.need(type(sign) is int and sign in (-1, 1) and type(stride) is int, 'integer stride and sign') + d.need(type(beta) in (int, F) and 0 < beta <= F(1, 2), 'stable margin') + d.need(factors and len(scratch) == (len(factors)-1).bit_length(), 'exact borrowed-array budget') + d.need(_coefficient(tau) and d.norm2(tau) == 1, 'unit gauge') + scale_bound = F(1) + for factor in factors: + d.need(isinstance(factor, tuple) and len(factor) == 3, 'factor descriptor') + inside, b, scale = factor + d.need(type(inside) is bool and _coefficient(b) and d.norm2(b) <= (1-beta)**2 + and type(scale) in (int, F), 'stable factor descriptor') + scale_bound = max(scale_bound, abs(scale)) + scratch = list(scratch) + arrays = [x, y]+scratch + meter = Meter() + if scratch: + meter.layout = {id(a): (0, i*len(x)) for i, a in enumerate(arrays[:-1])} + meter.layout[id(scratch[-1])] = (1, 0) + else: + meter.layout = {id(x): (0, 0), id(y): (1, 0)} + bound = _validate_arrays(arrays, bits, meter) + calls = d.leaf_calls(len(factors)) + growth = 2+scale_bound/beta + base_error = calls*68*(scale_bound+1)/beta**5*growth**(calls-1) + operator_norm = growth**calls + meter.error_bound = _word_budget(bits, beta, len(x), stride, base_error, operator_norm, bound) + phase = Phase.prepare(numerator, modulus, bits, meter) + phase_pass(x, phase, True) + phase_pass(y, phase, True) + meter.rewind() + d.compose(x, y, factors, scratch, tau, beta, bits, stride, sign, meter) + phase_pass(y, phase, False) + phase_pass(x, phase, False) + meter.rewind() + return meter + + +def working_bits(target_bits, incoming_bits, bound, beta, length, stride, + multiplier_bound=1, count=1, scale_bound=None): + """Choose a conservative precision for the complete conjugated word.""" + d.need(type(target_bits) is int and target_bits >= 0 + and type(incoming_bits) is int and incoming_bits >= 0 + and type(bound) in (int, F) and type(beta) in (int, F) + and bound >= 0 and 0 < beta <= F(1, 2) + and type(length) is int and length > 0 and type(stride) is int + and type(multiplier_bound) in (int, F) and multiplier_bound >= 1, 'working budget domain') + if scale_bound is None: + d.need(count == 1, 'leaf count') + base_error = 68*multiplier_bound/beta**5 + operator_norm = multiplier_bound/beta + else: + d.need(type(scale_bound) in (int, F) and scale_bound >= 1, 'factor scale bound') + calls = d.leaf_calls(count) + growth = 2+F(scale_bound)/beta + base_error = calls*68*(scale_bound+1)/beta**5*growth**(calls-1) + operator_norm = growth**calls + return max(2, incoming_bits, + target_bits+1+d.ceil_log2(32*(1+operator_norm+base_error)*(bound+1)), + d.ceil_log2(3*base_error), + d.ceil_log2(48*(d.depth(length, stride)+1)/beta**3)) diff --git a/research/dirty-stride-phases/dirty_stride.py b/research/dirty-stride-phases/dirty_stride.py new file mode 100644 index 0000000000..027108871d --- /dev/null +++ b/research/dirty-stride-phases/dirty_stride.py @@ -0,0 +1,409 @@ +"""Add a cyclic inverse to a target and restore the source exactly. + +This is a fixed-grid arithmetic model with two data tapes. Every data access +pays its head movement. See PROOF.md for the complete bill. +""" +from dataclasses import dataclass, field +from fractions import Fraction as F +from math import gcd + +ZERO = (F(0), F(0)) +ONE = (F(1), F(0)) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def add(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def sub(a, b): + return (a[0] - b[0], a[1] - b[1]) + + +def mul(a, b): + return (a[0]*b[0] - a[1]*b[1], a[0]*b[1] + a[1]*b[0]) + + +def norm2(a): + return a[0]*a[0] + a[1]*a[1] + + +def div(a, b): + d = norm2(b) + need(d != 0, 'zero divisor') + v = mul(a, (b[0], -b[1])) + return (v[0]/d, v[1]/d) + + +def rnd(a, bits): + """Use nearest dyadic rounding, with ties toward positive infinity.""" + scale = 1 << bits + def component(v): + t = v*scale + F(1, 2) + return F(t.numerator // t.denominator, scale) + return (component(a[0]), component(a[1])) + + +def trunc(a, bits): + """Truncate each component toward zero. This cannot increase the norm.""" + scale = 1 << bits + return tuple(F(int(v*scale), scale) for v in a) + + +@dataclass +class Meter: + reads: int = 0 + writes: int = 0 + tape_moves: int = 0 + products: int = 0 + power_products: int = 0 + divisions: int = 0 + nodes: int = 0 + leaves: int = 0 + validation_reads: int = 0 + max_depth: int = 0 + heads: dict = field(default_factory=dict) + layout: dict = field(default_factory=dict) + + def access(self, data, index, write=False): + tape, start = self.layout[id(data)] + position = start+index + self.tape_moves += abs(position - self.heads.get(tape, 0)) + 1 + self.heads[tape] = position + if write: + self.writes += 1 + else: + self.reads += 1 + + def rewind(self): + for tape, position in self.heads.items(): + self.tape_moves += position + self.heads[tape] = 0 + + +@dataclass(frozen=True) +class View: + data: list + start: int + step: int + length: int + meter: Meter + + def index(self, i): + need(0 <= i < self.length, 'view index') + return (self.start + self.step*i) % len(self.data) + + def get(self, i): + j = self.index(i) + self.meter.access(self.data, j) + return self.data[j] + + def put(self, i, value): + j = self.index(i) + self.meter.access(self.data, j, True) + self.data[j] = value + + def part(self, first, length): + need(0 <= first and first + length <= self.length, 'view interval') + return View(self.data, self.start + self.step*first, self.step, length, self.meter) + + def reverse(self): + return View(self.data, self.start + self.step*(self.length-1), + -self.step, self.length, self.meter) + + +def depth(length, stride): + count = 0 + while True: + stride %= length + stride = min(stride, length-stride) + if stride == 0: + return count + length, stride = stride, (-length) % stride + count += 1 + + +def admitted(beta, bits, levels): + return (type(bits) is int and bits >= 0 and 0 < beta <= F(1, 2) + and 48*(levels+1)*F(1, 1 << bits) <= beta**3) + + +def power(b, exponent, bits, meter): + """Use a left-to-right binary product and scalar working storage.""" + need(exponent >= 1, 'positive exponent') + result = b + for k in range(exponent.bit_length()-2, -1, -1): + result = trunc(mul(result, result), bits) + meter.power_products += 1 + if (exponent >> k) & 1: + result = trunc(mul(result, b), bits) + meter.power_products += 1 + return result + + +@dataclass(frozen=True) +class Geometry: + root: tuple + divisor: int + cycle: int + inverse: int + bits: int + meter: Meter + + def exponents(self, length, stride, orientation): + if stride == 0: + return (self.cycle, self.cycle) + def exponent(displacement): + need(displacement % self.divisor == 0, 'cycle lattice') + return ((displacement // self.divisor)*self.inverse) % self.cycle or self.cycle + return (exponent(orientation*stride), exponent(orientation*(stride-length))) + + def coefficients(self, length, stride, orientation): + a, b = self.exponents(length, stride, orientation) + left = power(self.root, a, self.bits, self.meter) + right = left if a == b else power(self.root, b, self.bits, self.meter) + return (left, right) + + +def emit(target, i, value, multiplier, sign, bits): + if multiplier != ONE: + target.meter.products += 1 + value = rnd(mul(multiplier, value), bits) + old = target.get(i) + target.put(i, add(old, value) if sign == 1 else sub(old, value)) + + +def swap(source, target): + for i in range(source.length): + left, right = source.get(i), target.get(i) + source.put(i, right) + target.put(i, left) + + +def causal(source, carrier, stride, geometry, undo=False): + """Apply the causal lifts with block swaps; restore the dirty carrier.""" + a, _ = geometry.coefficients(source.length, stride, source.step) + n = source.length + if undo: + swap(source, carrier) + for first in range(((n-1)//stride)*stride, -1, -stride): + size = min(stride, n-first) + swap(source.part(first, size), carrier.part(first, size)) + if first: + for i in range(first+size-1, first-1, -1): + value = rnd(mul(a, carrier.get(i-stride)), geometry.bits) + geometry.meter.products += 1 + source.put(i, sub(source.get(i), value)) + else: + for first in range(0, n, stride): + size = min(stride, n-first) + if first: + for i in range(first, first+size): + value = rnd(mul(a, carrier.get(i-stride)), geometry.bits) + geometry.meter.products += 1 + source.put(i, add(source.get(i), value)) + swap(source.part(first, size), carrier.part(first, size)) + swap(source, carrier) + + +def expand(source, target, stride, geometry, multiplier, sign): + """Conjugate the seed injection by exact inverse causal grid maps.""" + causal(target, source, stride, geometry, undo=True) + _, b = geometry.coefficients(source.length, stride, source.step) + coefficient = mul(multiplier, b) + geometry.meter.products += 1 + for i in range(stride): + value = rnd(mul(coefficient, source.get(i)), geometry.bits) + geometry.meter.products += 1 + emit(target, i, value, ONE, sign, geometry.bits) + causal(target, source, stride, geometry) + + +def closure(source, target, stride, geometry, sign, level): + """Move the child target to the other tape and restore the carrier.""" + borrowed = source.part(0, stride) + carrier = target.part(0, stride) + ends = source.part(source.length-stride, stride) + swap(borrowed, carrier) + solve(ends, carrier, (-source.length) % stride, geometry, sign=sign, level=level+1) + swap(borrowed, carrier) + + +def diagonal(source, target, geometry, multiplier, sign): + coefficient = power(geometry.root, geometry.cycle, geometry.bits, geometry.meter) + denominator = sub(ONE, coefficient) + for i in range(source.length): + value = rnd(div(source.get(i), denominator), geometry.bits) + geometry.meter.divisions += 1 + emit(target, i, value, multiplier, sign, geometry.bits) + + +def solve(source, target, stride, geometry, multiplier=ONE, sign=1, level=0): + """Use integer metadata at each level; scalar temporaries stay in helpers.""" + length = source.length + stride %= length + if 2*stride > length: + source, target, stride = source.reverse(), target.reverse(), length-stride + geometry.meter.nodes += 1 + geometry.meter.max_depth = max(geometry.meter.max_depth, level) + if stride == 0: + diagonal(source, target, geometry, multiplier, sign) + return + causal(source, target, stride, geometry) + if sign == 1: + for i in range(length): + emit(target, i, source.get(i), multiplier, 1, geometry.bits) + closure(source, target, stride, geometry, 1, level) + expand(source, target, stride, geometry, multiplier, 1) + closure(source, target, stride, geometry, -1, level) + expand(source, target, stride, geometry, multiplier, -1) + else: + expand(source, target, stride, geometry, multiplier, 1) + closure(source, target, stride, geometry, 1, level) + expand(source, target, stride, geometry, multiplier, -1) + closure(source, target, stride, geometry, -1, level) + for i in range(length): + emit(target, i, source.get(i), multiplier, -1, geometry.bits) + causal(source, target, stride, geometry, undo=True) + + +def lift(x, y, b, beta, bits, stride, sign=1, multiplier=ONE, shift=0, meter=None): + """Add multiplier*(I-b Z^stride)^-1 x at output indices i+shift.""" + need(type(stride) is int and type(shift) is int and type(sign) is int + and sign in (-1, 1), 'integer stride and sign') + need(x is not y and len(x) == len(y) and len(x) > 0, 'distinct equal arrays') + need(shift % len(x) in (0, stride % len(x)), 'output shift must be zero or the leaf stride') + need(isinstance(b, tuple) and len(b) == 2 and norm2(b) <= (1-beta)**2, 'stable constant coefficient') + need(isinstance(multiplier, tuple) and len(multiplier) == 2, 'constant multiplier') + need(admitted(beta, bits, depth(len(x), stride)), 'precision admission') + meter = meter if meter is not None else Meter() + if not meter.layout: + meter.layout = {id(x): (0, 0), id(y): (1, 0)} + need(id(x) in meter.layout and id(y) in meter.layout + and {meter.layout[id(x)][0], meter.layout[id(y)][0]} == {0, 1}, 'two distinct data tapes') + for data in (x, y): + for i in range(len(data)): + meter.access(data, i) + meter.validation_reads += 1 + value = data[i] + need(rnd(value, bits) == value, 'fixed grid data') + divisor = gcd(len(x), stride) + cycle = len(x)//divisor + inverse = pow((stride//divisor) % cycle, -1, cycle) if cycle > 1 else 0 + geometry = Geometry(b, divisor, cycle, inverse, bits, meter) + solve(View(x, 0, 1, len(x), meter), View(y, shift, 1, len(y), meter), + stride, geometry, multiplier, sign) + meter.leaves += 1 + meter.rewind() + return meter + + +def leaf_bound(bound, beta, bits, multiplier_bound=1): + return (64*multiplier_bound*(bound+1)/beta**5 + 3)*F(1, 1 << bits) + + +def leaf_calls(count): + need(type(count) is int and count >= 1, 'positive factor count') + if count == 1: + return 1 + return 2*leaf_calls(count//2) + 2*leaf_calls(count-count//2) + + +def compose(x, y, factors, scratch, tau, beta, bits, stride, sign=1, meter=None): + """Use PR628's balanced dirty commutator with the new arbitrary-stride leaf.""" + need(factors and len(scratch) >= (len(factors)-1).bit_length(), 'dirty depth') + arrays = [x, y] + scratch + need(len({id(a) for a in arrays}) == len(arrays), 'all arrays distinct') + need(len(x) > 0 and all(len(a) == len(x) for a in arrays), 'array lengths') + need(isinstance(tau, tuple) and norm2(tau) == 1, 'immutable unit gauge') + need(type(sign) is int and sign in (-1, 1) and type(stride) is int, 'integer stride and sign') + need(admitted(beta, bits, depth(len(x), stride)), 'precision admission') + for factor in factors: + need(isinstance(factor, tuple) and len(factor) == 3, 'factor descriptor') + inside, b, scale = factor + need(type(inside) is bool and isinstance(b, tuple) and len(b) == 2 + and norm2(b) <= (1-beta)**2 and isinstance(scale, (int, F)), 'stable factor descriptor') + meter = meter if meter is not None else Meter() + if scratch: + layout = {id(a): (0, i*len(x)) for i, a in enumerate(arrays[:-1])} + layout[id(scratch[-1])] = (1, 0) + else: + layout = {id(x): (0, 0), id(y): (1, 0)} + need(not meter.layout or meter.layout == layout, 'kernel tape layout') + meter.layout = layout + for data in arrays: + for i in range(len(data)): + meter.access(data, i) + meter.validation_reads += 1 + value = data[i] + need(rnd(value, bits) == value, 'fixed grid data') + def run(src, dst, lo, hi, level, direction): + if hi-lo == 1: + inside, b, scale = factors[lo] + phase = (tau[0], -tau[1]) if inside else tau + coefficient = mul(b, phase) + m = phase if inside else (-b[0], -b[1]) + m = (m[0]*scale, m[1]*scale) + if meter.layout[id(src)][0] == meter.layout[id(dst)][0]: + spare = scratch[-1] + destination = View(dst, 0, 1, len(dst), meter) + carrier = View(spare, 0, 1, len(spare), meter) + swap(destination, carrier) + lift(src, spare, coefficient, beta, bits, -stride if inside else stride, + direction, m, -stride if inside else 0, meter) + swap(destination, carrier) + else: + lift(src, dst, coefficient, beta, bits, -stride if inside else stride, + direction, m, -stride if inside else 0, meter) + return + mid = (lo+hi)//2 + z = scratch[level] + if direction == 1: + run(src, z, lo, mid, level+1, 1) + run(z, dst, mid, hi, level+1, 1) + run(src, z, lo, mid, level+1, -1) + run(z, dst, mid, hi, level+1, -1) + else: + run(z, dst, mid, hi, level+1, 1) + run(src, z, lo, mid, level+1, 1) + run(z, dst, mid, hi, level+1, -1) + run(src, z, lo, mid, level+1, -1) + run(x, y, 0, len(factors), 0, sign) + meter.rewind() + return meter + + +def ceil_log2(value): + value = F(value) + need(value > 0, 'positive logarithm') + k = value.numerator.bit_length() - value.denominator.bit_length() + power_of_two = F(2)**k + return k if value <= power_of_two else k+1 + + +def execution_bound(count, r, beta, initial_bound, bits): + need(r >= 1 and initial_bound >= 0 and 0 < beta <= F(1, 2) + and type(bits) is int and bits >= 0, 'execution budget domain') + calls = leaf_calls(count) + a = 68*(r+1)/beta**5 + growth = 2+F(r)/beta + need(a*F(1, 1 << bits) <= 1, 'execution precision') + return calls*a*(initial_bound+1)*F(1, 1 << bits)*growth**(calls-1) + + +def working_bits(count, r, beta, initial_bound, target_bits, incoming_bits, length, stride): + need(r >= 1 and initial_bound >= 0 and 0 < beta <= F(1, 2) + and type(target_bits) is int and target_bits >= 0 + and type(incoming_bits) is int and incoming_bits >= 0 + and type(length) is int and length > 0 and type(stride) is int, 'working budget domain') + calls = leaf_calls(count) + a = 68*(r+1)/beta**5 + growth = 2+F(r)/beta + levels = depth(length, stride) + return max(incoming_bits, target_bits+1+ceil_log2(calls*a*(initial_bound+1)) + +(calls-1)*ceil_log2(growth), ceil_log2(a), + ceil_log2(48*(levels+1)/beta**3)) diff --git a/research/dirty-stride-phases/oracle.py b/research/dirty-stride-phases/oracle.py new file mode 100644 index 0000000000..2851b219ad --- /dev/null +++ b/research/dirty-stride-phases/oracle.py @@ -0,0 +1,188 @@ +"""Enclose the ideal phases and operators with rational intervals. + +This checker does not use the production phase reduction, grid rotation, +finite differences, or Euclidean inverse program. +""" +from fractions import Fraction as F +from functools import lru_cache +from math import gcd + + +def outward(lo, hi, bits): + scale = 1 << bits + return F((lo*scale).__floor__(), scale), F((hi*scale).__ceil__(), scale) + + +def point(value): + return F(value), F(value) + + +def plus(a, b, bits): + return outward(a[0]+b[0], a[1]+b[1], bits) + + +def neg(a): + return -a[1], -a[0] + + +def times(a, b, bits): + values = (a[0]*b[0], a[0]*b[1], a[1]*b[0], a[1]*b[1]) + return outward(min(values), max(values), bits) + + +def scale(a, value, bits): + return times(a, point(value), bits) + + +@lru_cache(maxsize=32) +def pi_interval(bits): + def arctangent(denominator): + total = F(0) + power = denominator + k = 0 + while True: + total += (-1 if k % 2 else 1)*F(1, (2*k+1)*power) + k += 1 + power *= denominator*denominator + remainder = F(1, (2*k+1)*power) + if remainder < F(1, 1 << (bits+8)): + other = total+(-1 if k % 2 else 1)*remainder + return min(total, other), max(total, other) + a, b = arctangent(5), arctangent(239) + return outward(16*a[0]-4*b[1], 16*a[1]-4*b[0], bits) + + +@lru_cache(maxsize=4096) +def phase(numerator, modulus, index, bits): + residue = numerator*index*index % modulus + if residue == 0: + return point(1), point(0) + angle = scale(pi_interval(bits), F(2*residue, modulus), bits) + squared = times(angle, angle, bits) + sine = sine_term = angle + cosine = cosine_term = point(1) + tail = F(7*7, 2) + k = 1 + unit = F(1, 1 << bits) + while True: + sine_term = scale(times(sine_term, squared, bits), -F(1, 2*k*(2*k+1)), bits) + cosine_term = scale(times(cosine_term, squared, bits), -F(1, (2*k-1)*2*k), bits) + sine = plus(sine, sine_term, bits) + cosine = plus(cosine, cosine_term, bits) + tail *= F(49, (2*k+1)*(2*k+2)) + k += 1 + if tail < unit and k >= 4: + sine_tail = tail*F(7, 2*k+1) + return (outward(cosine[0]-tail, cosine[1]+tail, bits), + outward(sine[0]-sine_tail, sine[1]+sine_tail, bits)) + + +def complex_point(value): + return point(value[0]), point(value[1]) + + +def complex_add(a, b, bits): + return plus(a[0], b[0], bits), plus(a[1], b[1], bits) + + +def complex_mul(a, b, bits): + return (plus(times(a[0], b[0], bits), neg(times(a[1], b[1], bits)), bits), + plus(times(a[0], b[1], bits), times(a[1], b[0], bits), bits)) + + +def rational_mul(a, b): + return a[0]*b[0]-a[1]*b[1], a[0]*b[1]+a[1]*b[0] + + +def inverse(value): + norm = value[0]*value[0]+value[1]*value[1] + return value[0]/norm, -value[1]/norm + + +def cyclic(source, coefficient, stride, bits): + length = len(source) + cycle = length//gcd(length, stride) + power = (F(1), F(0)) + for _ in range(cycle): + power = rational_mul(power, coefficient) + denominator_inverse = complex_point(inverse((1-power[0], -power[1]))) + result = [] + for i in range(length): + total = complex_point((0, 0)) + power = (F(1), F(0)) + for j in range(cycle): + total = complex_add(total, complex_mul(complex_point(power), source[(i-j*stride) % length], bits), bits) + power = rational_mul(power, coefficient) + result.append(complex_mul(total, denominator_inverse, bits)) + return result + + +def conjugate_input(source, numerator, modulus, bits): + return [complex_mul((phase(numerator, modulus, i, bits)[0], + neg(phase(numerator, modulus, i, bits)[1])), complex_point(value), bits) + for i, value in enumerate(source)] + + +def conjugate_output(source, numerator, modulus, bits): + return [complex_mul(phase(numerator, modulus, i, bits), value, bits) + for i, value in enumerate(source)] + + +def leaf(source, coefficient, stride, numerator, modulus, bits, multiplier=(F(1), F(0)), shift=0): + transformed = conjugate_input(source, numerator, modulus, bits) + solved = cyclic(transformed, coefficient, stride, bits) + shifted = [complex_mul(complex_point(multiplier), solved[(i-shift) % len(source)], bits) + for i in range(len(source))] + return conjugate_output(shifted, numerator, modulus, bits) + + +def kernel(source, factors, tau, stride, numerator, modulus, bits): + out = conjugate_input(source, numerator, modulus, bits) + for inside, coefficient, factor_scale in factors: + if inside: + gauge = tau[0], -tau[1] + b = rational_mul(coefficient, gauge) + multiplier = gauge[0]*factor_scale, gauge[1]*factor_scale + solved = cyclic(out, b, -stride, bits) + out = [complex_mul(complex_point(multiplier), solved[(i+stride) % len(source)], bits) + for i in range(len(source))] + else: + b = rational_mul(coefficient, tau) + multiplier = -coefficient[0]*factor_scale, -coefficient[1]*factor_scale + out = [complex_mul(complex_point(multiplier), value, bits) + for value in cyclic(out, b, stride, bits)] + return conjugate_output(out, numerator, modulus, bits) + + +def squared_distance_bound(actual, expected): + return sum(max(abs(actual[i]-expected[i][0]), abs(actual[i]-expected[i][1]))**2 for i in range(2)) + + +def polynomial(source, coefficients, stride, numerator, modulus, bits, tau): + """Use exact Gaussian elimination for the polynomial matrix.""" + length = len(source) + matrix = [[(F(0), F(0)) for _ in range(length)] for _ in range(length)] + power = F(1), F(0) + for j, coefficient in enumerate(coefficients): + weight = rational_mul(coefficient, power) + for i in range(length): + column = (i-stride*j) % length + old = matrix[i][column] + matrix[i][column] = old[0]+weight[0], old[1]+weight[1] + power = rational_mul(power, tau) + rhs = conjugate_input(source, numerator, modulus, bits) + for k in range(length): + pivot = next(i for i in range(k, length) if matrix[i][k] != (0, 0)) + matrix[k], matrix[pivot] = matrix[pivot], matrix[k] + rhs[k], rhs[pivot] = rhs[pivot], rhs[k] + divisor = inverse(matrix[k][k]) + matrix[k] = [rational_mul(divisor, v) for v in matrix[k]] + rhs[k] = complex_mul(complex_point(divisor), rhs[k], bits) + for i in range(length): + if i == k: + continue + weight = matrix[i][k] + subtrahend = [rational_mul(weight, v) for v in matrix[k]] + matrix[i] = [(v[0]-w[0], v[1]-w[1]) for v, w in zip(matrix[i], subtrahend)] + rhs[i] = complex_add(rhs[i], complex_mul(complex_point((-weight[0], -weight[1])), rhs[k], bits), bits) + return conjugate_output(rhs, numerator, modulus, bits) diff --git a/research/dirty-stride-phases/test_package.py b/research/dirty-stride-phases/test_package.py new file mode 100644 index 0000000000..f16e79082f --- /dev/null +++ b/research/dirty-stride-phases/test_package.py @@ -0,0 +1,120 @@ +"""Reject concrete source faults and replay the package after relocation.""" +import hashlib +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +from fractions import Fraction as F + +HERE = Path(__file__).resolve().parent + + +def load(path, name): + 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 + + +v = load(HERE/'verify.py', 'package_verifier') + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def reject(name, action, expected): + try: + action() + except ValueError as error: + need(str(error) in expected, name+': wrong rejection: '+str(error)) + return dict(name=name, rejected=str(error)) + raise ValueError(name+': mutation was accepted') + + +def main(): + source = (HERE/'chirp.py').read_text() + phase_case = lambda module: v.check_phase_case(module, 7, 1, 64, (F(17, 4), F(-33, 8))) + leaf_case = lambda module: v.check_leaf_case(module, 8, 3, -3, 16, 2**40) + faults = [ + ('wrong_machin_weight', '((5, 16), (239, -4))', '((5, 15), (239, -4))', + phase_case, {'phase coefficient accuracy'}), + ('short_shear_precision', 'real_round(tangent, self.bits+8)', 'real_round(tangent, 8)', + phase_case, {'phase coefficient accuracy'}), + ('wrong_forward_shear', 'imag += real_round(sine*real, bits)', 'imag -= real_round(sine*real, bits)', + phase_case, {'rotation accuracy'}), + ('wrong_reverse_shear', 'imag -= real_round(sine*real, bits)', 'imag += real_round(sine*real, bits)', + phase_case, {'rotation exact inverse'}), + ('linear_phase_stream', 'difference = (difference+2*phase.numerator) % phase.modulus', + 'difference = (difference+phase.numerator) % phase.modulus', + leaf_case, {'phased leaf accuracy'}), + ('unrestored_source', ' phase_pass(x, phase, False)', ' phase_pass(x, phase, True)', + leaf_case, {'leaf source restoration'}), + ('wrong_target_phase', ' phase_pass(y, phase, False)', ' phase_pass(y, phase, True)', + leaf_case, {'phased leaf accuracy'}), + ('unpaid_phase_read', ' meter.access(data, i)\n value = rotate', + ' value = rotate', leaf_case, {'paid data accesses'}), + ('lost_quadratic_sign', 'return cls(numerator % modulus,', 'return cls((-numerator) % modulus,', + leaf_case, {'phased leaf accuracy'}), + ] + controls = [] + with tempfile.TemporaryDirectory(prefix='dirty-phase-controls-') as temporary: + root = Path(temporary) + for index, (name, old, new, check, errors) in enumerate(faults): + need(old in source, 'mutation anchor: '+name) + package = root/name + (package/'vendor/pr985').mkdir(parents=True) + shutil.copyfile(HERE/'dirty_stride.py', package/'dirty_stride.py') + (package/'chirp.py').write_text(source.replace(old, new, 1)) + module = load(package/'chirp.py', 'fault_'+str(index)) + controls.append(reject(name, lambda: check(module), errors)) + # The mathematical verifier must reject an incorrect borrowed-array inverse. + package = root/'wrong_child_inverse' + (package/'vendor/pr985').mkdir(parents=True) + (package/'chirp.py').write_text(source) + prior = (HERE/'dirty_stride.py').read_text() + old = 'run(src, z, lo, mid, level+1, -1)' + need(old in prior, 'child inverse anchor') + (package/'dirty_stride.py').write_text(prior.replace(old, 'run(src, z, lo, mid, level+1, 1)', 1)) + module = load(package/'chirp.py', 'fault_child') + controls.append(reject('wrong_child_inverse', lambda: v.check_kernel_case(module, 2, 5, 2, 13), + {'kernel source and scratch restoration', 'phased kernel accuracy'})) + # Check content binding separately from all semantic fault checks above. + package = root/'binding' + shutil.copytree(HERE, package) + pin = package/'vendor/pr985/dirty_stride.py' + pin.write_bytes(pin.read_bytes()+b'\n') + relocated = load(package/'verify.py', 'binding_verifier') + controls.append(reject('source_bytes', relocated.pins, + {'source SHA256: vendor/pr985/dirty_stride.py'})) + # A noninteger schema value must not compare equal to its integer value. + receipt = json.loads((HERE/'EXPECTED.json').read_text()) + altered = dict(receipt, schema=True) + need(v.canonical(receipt) != v.canonical(altered), 'typed receipt comparison') + controls.append(dict(name='boolean_receipt', rejected='typed receipt mismatch')) + clean = root/'standalone' + shutil.copytree(HERE, clean) + before = {str(path.relative_to(clean)): hashlib.sha256(path.read_bytes()).hexdigest() + for path in clean.rglob('*') if path.is_file()} + for path in clean.rglob('*'): + if path.is_file(): + path.chmod(0o444) + output = root/'regenerated.json' + completed = subprocess.run([sys.executable, '-I', '-O', '-B', str(clean/'verify.py'), '--write', str(output)], + cwd=root, text=True, capture_output=True, timeout=600) + need(completed.returncode == 0, 'relocated replay: '+completed.stdout+completed.stderr) + need(output.read_bytes() == (HERE/'EXPECTED.json').read_bytes(), 'relocated full receipt') + after = {str(path.relative_to(clean)): hashlib.sha256(path.read_bytes()).hexdigest() + for path in clean.rglob('*') if path.is_file()} + need(before == after, 'read-only package changed') + print(json.dumps(dict(controls=controls, relocated_read_only_replay=True, byte_identical_receipt=True), sort_keys=True)) + print('PASS_DIRTY_PHASE_PACKAGE controls='+str(len(controls))+' relocation=1 regeneration=1') + + +if __name__ == '__main__': + main() diff --git a/research/dirty-stride-phases/vendor/pr479/PROOF.md b/research/dirty-stride-phases/vendor/pr479/PROOF.md new file mode 100644 index 0000000000..fd05f84d60 --- /dev/null +++ b/research/dirty-stride-phases/vendor/pr479/PROOF.md @@ -0,0 +1,165 @@ +# Exact streamed chirp phases and the scalar cost row + +## Changed cost, unchanged numerical map + +The retained chirp array, in the original padded tensor order, is + +``` +a(j) = exp(-pi*i*sum_i s_i*j_i^2/t_i), +E(j) = -sum_i s_i*j_i^2*(r/t_i) mod 2r, +a(j) = exp(2*pi*i*E(j)/(2r)). +``` + +Here r=2^ell, t_i is r or r/2, t_i>=2, and 00. Twist products, coefficientwise scalar products and +format adapters already fit this bound. Polynomial-ring products on O(rp)-bit +packed records are a separate cost and are **not** included in this change. +Thus this **scalar cost row** has normalized +exponent delta and saving `1-delta`, instead of `1-epsilon-delta`. + +Every generated residue E is the original exact residue. Call the same +retained disk-grid exponential routine with the same E, denominator 2r and +precision p. Its output and error guarantee are unchanged. There is no new +transcendental approximation, normalization, phase convention or input order. + +## Direct width-sensitive computation + +An index j_i and source s_i each have at most ell bits. The square has at +most 2ell bits, its product with s_i at most 3ell bits, and multiplication +by r/t_i is a shift by zero or one bit. Reduce every term modulo 2r before +adding it to the running residue. Only O(ell)-bit arithmetic is required +for each term, including the modular accumulator. + +Using the already retained unconditional multiplier on these short integers +costs `O(ell*log(2ell))` per term. Descriptors s_i,t_i and coordinates j_i +are serialized as O(ell)-bit fields, not padded to p bits individually. +One scan through all d fields costs O(d*ell). Consequently the phase cost +per coefficient is + +``` +O(d*ell*log(2ell)) = O(p*log(2p)). +``` + +Coordinate extraction and resetting those short fields are also charged to +the O(d*ell) scan. The one precision-p exponential then costs +`O(max(p,log(2r))^(1+delta)) = O(p^(1+delta))`, using the unchanged cited +scalar interface in the source. The descriptor scan no longer contributes +a factor d to that cost. No improved multiplier is called on its own input +size; these control records and coefficient products are strictly short. + +## An additive generator with an explicit tape schedule + +Put Q=2r and `A_i=-s_i*(r/t_i) mod Q`. For each axis store its radix, +current index j_i, value `v_i=A_i*j_i^2 mod Q`, and forward difference +`Delta_i=A_i*(2j_i+1) mod Q`, together with A_i. Keep the global residue +`E=sum_i v_i mod Q` on a separate work tape. Initially j_i=v_i=E=0 and +Delta_i=A_i. + +Emit E, then advance the last axis, carrying left in lexicographic order. +At an axis whose index is not last: + +``` +E <- E + Delta_i mod Q +v_i <- v_i + Delta_i mod Q +Delta_i <- Delta_i + 2*A_i mod Q +j_i <- j_i + 1 +``` + +At a wrapped axis: + +``` +E <- E - v_i mod Q +j_i,v_i <- 0,0 +Delta_i <- A_i +``` + +Then carry to its left neighbor. When every axis wraps, stop; no full-width +remaining-output counter is required. The identities +`(j+1)^2-j^2=2j+1` and `2(j+1)+1=(2j+1)+2` prove the invariant at every +ordinary increment. Subtraction of the old v_i proves it across every +carry, including simultaneous carries. Thus the emitted sequence is exactly +the original E(j), and the final complete rollover restores E=0 and all +initial axis states. There is no precomputed table of T phases. + +Store the d axis records consecutively on one tape, fastest axis last. +Each record has O(ell) bits; each visit scans a fixed number of its fields. +The carry head only walks to adjacent records and then returns across the +records just visited. The global E tape uses O(ell) bits and is restored to +its starting head position after each update. The coefficient and phase +output tapes advance sequentially. The retained exponential subroutine uses +its fixed work tapes between visits; the axis tape can remain parked. +This is a fixed tape count, with O(d*ell)=O(p) persistent phase state. + +Over a complete T-entry stream, the exact number of axis visits is + +``` +V_axis = sum_i T / product_(j>i) t_j < 2T, +``` + +because all radices are at least two. Returning the head adds at most the +same number of record traversals. Modular arithmetic costs O(ell) per +visit, so phase generation costs `O(T*ell+d*ell)` bit operations. Reading +the source descriptors and forming A_i use only shifts and modular +negations on O(ell)-bit words. Intermediate signed sums fit a constant +multiple of ell bits. The precision-p exponential and coefficient output +dominate this cost. Verifier statistics and materialized coordinate tuples +are not required by the generator or this tape schedule. + +## Numerical and operator interfaces + +The scalar routine already returns a disk-grid approximation with error +less than `2*2^-p`. We pass the same exact integer residue and denominator, +so no new precision loss is introduced. Retain the original exact dyadic +endpoint products and their component truncations. The chirp convolution +identity and its error proof therefore apply without a change. + +For every pair of tensor addresses j,k, periodicity of the even t_i gives + +``` +E(j-k mod t) - E(j) - E(k) + = 2*sum_i s_i*j_i*k_i*(r/t_i) mod 2r. +``` + +This checks the coefficient identity underlying the retained permuted +Fourier transform, including wrapped differences and the sign of the phase. +Conjugation uses the same generated array as before. The FFT layouts from +#475 are internal to the convolution; the chirp interface remains in the +original tensor order. No source or frequency permutation has been dropped. + +The executable generator is an exact reference implementation and the finite +checks test its residues, carries, widths, period and operator exponents. +They do not execute the cited high-precision exponential or a full multiplier. +Equality of its exact inputs is the transfer argument for that unchanged +routine. Nor is the Python runtime a measurement of the fixed-tape bound. + +## Remaining barriers + +Only `scalar_work` improves from `1-epsilon-delta` to `1-delta`. +The Gaussian arithmetic margin is still +`min(1-epsilon-delta,r-delta)`, so it was already no larger than the old +scalar margin. Changing this row alone cannot improve the current minimum. +The source-bound arithmetic control verifies this fact with #472's exact +parameters and leaves every other constraint intact. It is not a new finite +supplier invoice or a higher-kappa certificate. + +Together with #475, this removes reserved-axis, exceptional top-bit and +scalar-chirp costs from the list of independent bottlenecks. Gaussian line +application, normalization `epsilon+r<1`, and the separate small-field +exposure condition remain, as does the separate polynomial-product dimension +margin. Those require actual constructions or tighter +justified bounds of their own. Kappa=1 is not established. + +Prepared by chafreaky with OpenAI Codex assistance. The chirp formula, +permuted Fourier identity, scalar exponential interface and asymptotic size +bands are retained from the source-pinned integer-mult-bounds manuscript and +its credited authors. Exact quadratic differences are elementary; no claim +of literature priority is made. Apache-2.0. diff --git a/research/dirty-stride-phases/vendor/pr479/README.md b/research/dirty-stride-phases/vendor/pr479/README.md new file mode 100644 index 0000000000..b75ad5c75b --- /dev/null +++ b/research/dirty-stride-phases/vendor/pr479/README.md @@ -0,0 +1,40 @@ +# Streamed chirp phases + +The retained chirp generator computes one exponential per coefficient, but +charges d index calculations at full p-bit width. The indices have only +ell-bit width, with d*ell=O(p). Accounting for those widths removes a factor +d. The accompanying additive generator independently obtains the exact same +phase residues with fewer than 2T axis-record visits over a T-entry stream. + +The chirp/scalar row becomes `O(T*p^(1+delta))`, with normalized saving +`1-delta` rather than `1-epsilon-delta`. The scalar exponential, phase sign, +denominator, disk-grid error, pointwise products and tensor order are retained. +Polynomial-ring products are separate and unchanged. + +**No new kappa is claimed.** The Gaussian margin is no larger than the old +scalar margin, so the current overall minimum is unchanged. This follows +#475's removal of two FFT costs by removing a further independent scalar cost. + +Run with Python 3.11+ and the standard library: + +```sh +python -B research/streamed-chirp-phases/verify.py /absolute/new/output +``` + +Finite controls cover 319 complete streams and 587,020 phase entries; +191,592 exact chirp/Fourier coefficient identities; 60 bounded distant-state +probes with control words up to 522 bits; exact complete-period restoration; +adjacent-record traversal counts; narrow arithmetic widths; six mutations; +and the unchanged outer minimum. Distant probes do not claim execution of +their enormous prefixes. + +The verifier does not execute the retained high-precision exponential or a +full multiplication machine. It proves equality of the integer arguments +passed to that unchanged routine. The all-size fixed-tape bound is the +written transfer in [PROOF.md](PROOF.md), not a Python runtime measurement. + +SOURCE.json pins the manuscript and inherited arithmetic. Original files +are unchanged. New implementation and accounting by chafreaky with OpenAI +Codex assistance. The chirp formula and scalar interfaces belong to the +source authors; no literature priority for elementary finite differences is +claimed. Apache-2.0. diff --git a/research/dirty-stride-phases/vendor/pr479/SOURCE.json b/research/dirty-stride-phases/vendor/pr479/SOURCE.json new file mode 100644 index 0000000000..53657bfc29 --- /dev/null +++ b/research/dirty-stride-phases/vendor/pr479/SOURCE.json @@ -0,0 +1,10 @@ +{ + "commit": "5996e33ecad6a0ccd578aec58831457829d75575", + "files": { + "upstream/build/sections/07-resampling.tex": "8a6b91670f9163afb54892489fa2210c77fe1b058f0325ec7d18b44b94be6e2c", + "upstream/build/sections/08-assembly.tex": "763d7945b1e1ec4ebae9b799bcefcc45fa9bae6e2ffad799868a9c3d513dbd4a", + "research/e8-r740-replica32/code/engines/outer.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c", + "research/e8-r715-whole-hosted/EXPECTED.json": "9e91920c50fa72d81916faa17feb19d57568a7bb107a55e0ba3af1025e42e062", + "research/complementary-fft-reservoirs/PROOF.md": "708adab0cd71f06d0827006cf244bf7f586a2b6c0b1eab6de8256a6c59b9df13" + } +} diff --git a/research/dirty-stride-phases/vendor/pr628/FACTORS.json b/research/dirty-stride-phases/vendor/pr628/FACTORS.json new file mode 100644 index 0000000000..d3894bd2a1 --- /dev/null +++ b/research/dirty-stride-phases/vendor/pr628/FACTORS.json @@ -0,0 +1,402 @@ +[ + { + "radix": 3, + "embedding": 1, + "roots": [ + [ + "-49530798732358771146118901080958076273052470912342260266258914227109710325121387637640669783171544976658235453737966492290535102314016775076196131137253281608605845416954368911072190053165368500463077348683479820730223655747230034954087192637416985282711781569366341015472238222901103154593890125768068166111/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "13475305001181955152635744113343228941870362999235845156852762789867665164197346764233250937361286208084929252607275859697194884125876348244811537318304219573113812813781235059890295167053180994008138010725194287959555680271101985158640265590661977057048524039192974778963502923615772560082862029626247356915/11235582092889474423308157442431404585112356118389416079589380072358292237843810195794279832650471001320007117491962084853674360550901038905802964414967132773610493339054092829768888725077880882465817684505312860552384417646403930092119569408801702322709406917786643639996702871154982269052209770601514008576" + ], + [ + "-170592372764629843867157976456437557496591605016661465377627293282379593058008669423781376417268214078363699912331157051907114448593591383586878883684704623349440149303389490092308949295538404178253469730760549011796778712019234252302695280536406885179602202888146765328976392461917368148065254242900199873601/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-46411209039859540974176647362240554857493432165837745376222291831822369430116719300153189465225800706342648078500395279868781491155333745970178758722507111433403998868313736485156740909917748907461424289090884948593897673112150836753179290605396652366677201787911857343898640266500768045571317618646184981515/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152" + ] + ], + "beta": "1/32", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 4, + "embedding": 1, + "roots": [ + [ + "18839227606306460928750436776825014273496077882053237212856774153163841259423959845929808348046828320902424357370784726029073309579224150022196016795678227966011136545266483378669974662335269472502528125472018535885295396863622929964034462260120294171947340433492325221872688727385544533583048885326400903597/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "12796926340379968523293584046788682991068081520875261248350397459182248423294625032260126325308015563095435234200881380927938236702421262255195096551267084999719624023209458696352316971284756123109784206671973205284974765619111294724890379061690528176512207203087118838657451331182211930074180553022205037717/11235582092889474423308157442431404585112356118389416079589380072358292237843810195794279832650471001320007117491962084853674360550901038905802964414967132773610493339054092829768888725077880882465817684505312860552384417646403930092119569408801702322709406917786643639996702871154982269052209770601514008576" + ], + [ + "-67937135992698413485848028692002309503217002121030373236286063853851112002834956545147982981350737462809662177353146777437281023159349478379475061510263643694108201092716816673971478633600166383954345966000686009575573734331558302198133439150275018280298091260360209316562436177361876091474717502741308380027/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304", + "5835616822424528393018276731807351617575339522981934688817604363901147520344005371600541622764811103253229296878826668528234697818556822582094397306602957922127281544555831623274134108430066605792876461395490781682749981003075479237572505884700169238753265724966398880489058963937223602091905317904711941499/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ], + [ + "73140002878255602241711158912281750377574232707837598458857400104507930946414903201953646254948585509216110472170409026061261014243757141002856798605902222432653774400735298040913720270819301943861772786445719733578848858120147397354586183800152541785894513923362213804429810043582243527480464796014608479295/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-101965650555502300179425242688687701922297090080040644000576714490063310164897746283818166254598757360914998703650200531654685086831846027226086641171539829015447750993610037727758956893880614628095284026104635045032186714065136378505612299766669091235639722208461448795105675773286000398597466612399588126671/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ] + ], + "beta": "1/32", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 5, + "embedding": 1, + "roots": [ + [ + "18410399432434593285169076294769602275894540638275295419244544381879773242101229303192661033873560946309710294140171891893900372823577853227464636318197065166893737578492060390055766605671671799743745029504200984650324085253453636489088551766233790345264477955593735634726155875498225455897152145422527110857/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304", + "88926944313291886897540182389959275756316664511795052113045934836868436387626350644157761509746590523735127289561482706452011713192888368531757723983026280383546034048812998372260884484021077768824721106874944498264700931287184901932524740060871613024772296891180592599727648764929046216006068462246504374811/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-167545453603640477774873977068820521490816283320967799058419418306745166535530698475752796883467944874062781699503482002031721106189111733803133269028126037337336557647540282023493990675410251006273872459992624200925878916492155324954465535073616098706096481035319289799489810569175272312690818408702357774707/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "154556349957963769064367096421348364953192572923709918873780464142362058554060160862470338328380796109257170485631887393041866922712420579126848130118663444268007905141768967672162702816973919207497792878550271826416467017062585388767141690359055369161984340591026398951036705551282299373389928249065466957777/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-246025941110189748337782398645962696281966535596390989644134716992878047915802819087254020031137007742552596547220618828803263741659091725736455982888598484589330876923271022291321628747736395867996706991862080909718783945688678933156172363230796038024619721716767295126085355526352538295019215908632644428645/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-80017827675325207808535539612151904575968566998857213977754346138586638701168117409273474539675100516306047838318004762335480802433891996015633286597935493715465198565408881501720917279311214162172063959383782684101469915657487668687514739767345963311117394934914437584673901163128059865890829000565376585079/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "215712256432223249791838888842272962081449782057642246390000600800148072180501294511436300947360881829332748816482640829932179778301978229874156851415522923858548828681148808544326153700577210577826268148302190110772732181100719565734873230271520263077404047413202169567004576671193383551882477838906429979943/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-343345360254883912964398674422494284929201599795775129858953529504351638375339699421889616865554200011416676596545392950323715795619267003477668104686330984199520110843844773329958643601792506764296355657817381043552933491542452533905205092594361844214785757345776857492089057313413558295951124845050277505639/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ] + ], + "beta": "1/64", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 7, + "embedding": 1, + "roots": [ + [ + "120836177722361423700961200616746340939117621826067821546283999942075497210076949759460370715678904626969473270870038244427213482017330996532718477962097048482765518680096123147561488619800104812093083654163138766755667970537231472653449243809561047362543545086368385980168510507433365046715788937161703716085/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "68125532188584294286663341974472312621216872199921619246009406654878430278942492383247031997235044995684216361049673718348715972217344544049530857813500428243332162775155119877092074201530144921889140264057120091137424453307505120185335081880162914431352955991832950471916200413514695655590549673800742347681/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-23352251484866588814984102757151938020295470378892869474143458720257279649755690100107547794252764950418419952156812046731260229125257633674879904341802608588717478148648944135150233501962993159400202815681865439334171539946279604850805926161998688918951893236128852170350420117380648887992523528703050194783/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "12132115037519896013585104434007386698287966150528447173769745653094849377705471451533571302407701987585405260939215552836593163546110098278844478687559077536413118639791236269008047600329470759689721901333721666143586701098282693338033702985076136987291514686849805451278368411427725280317893977203863584583/11235582092889474423308157442431404585112356118389416079589380072358292237843810195794279832650471001320007117491962084853674360550901038905802964414967132773610493339054092829768888725077880882465817684505312860552384417646403930092119569408801702322709406917786643639996702871154982269052209770601514008576" + ], + [ + "-92291382711014775221380021171202817794657125260699000287682436525116249639100986456003288102293593362503506340776371812568234629218022304094954295338321708547490187028615230917002633870289187269289797994714342072570440381702763361962356356505306507682202967183538465154964375441642931008189553934230981931559/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "119712689918657651145189233762925546457090337327810229148877839636675818166345698397220337691661044465436596246450977563970023691296540621113539611731979073364553791157261962787179002477238112224575127636003783615332436194461854998451162028079761177278027679849503098212639903585808693056859631675024978403655/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-241550214101542094297167535638151897507830585201411331736006717246868123702109366984690181768784545848116906421886000314994526788327659530751761942604584557795696877540130891932133377552105984741145270626005788962709578395270874088233819746015884483414705471639012552028950063730900626438412769308246134412423/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-44636521770478560155358654717184927568066750073373513015128082461673476496822166780757639936727928123676721979818426533919863914831246651250724819329685161786373417321779253128206274251444083819402120012005681947845516990805594334226921578412078056649090375828519802643691118444466847932595531100425230751867/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-30203061381136258809439665112684149466527548721381460346906377733218206927673101886508360525270680857362678859262610296498976901610754244593890353821856268232116927740493603349537265139809747876075016798077935946460243881062966294672661437770702005876180419387161259974619074523496342984580783717368906963491/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "-305110068800135848497848181573777483300901124284310624770759696080464881064477659631992063113691884421747360163819890589058455217115247182223505704124808283746309249249359889226760626023333388774388559141421503453637601946482828567415910388069454422041311561341290600832629150554612317238895704865818852456303/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "321370196207928824720915204711075455015246912340098126751032311594524033112453537345445629309422537818066392684089031234715114932786141935425039670921672922753033036803089443416637226862726853593951312786044577899391357952048006221305816041423551248138900234992740786667031784280806046850529260976098348049203/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-24530473927531504467392407392323938052443883461832126187972943992643983667419063708657378422819680820353364287646948211385092126125885316040368239976682069981937416789728921378575979136146542456286295719081463657034678512460199743093437741946258402070242087927157968777687527815825283515074190769218475070497/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152" + ] + ], + "beta": "1/512", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 8, + "embedding": 1, + "roots": [ + [ + "8676521756510435418408946804461767324891306204862417174847745121263025946650658922911780062841899310292089809846830833767424385518217195893825119278967539421517248349379935548836275419185719990536047729374806106190931483190985689626709113976582272252929209174868395094303365494483709135736692733466731317795/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "46927175506395187795687931561127127492542914401987186784106756230323458946080644106593751363160127877209084537223858819579870206674713563202937305209536930043680869885123270522345465099010053820092378973496193748874813123926250211050432217802376301722910925291572156201602782436939032617502745379314433603689/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ], + [ + "66202580992830939447277596770820976547224187818360015042315917699790056190563629777404288554237323292216596605503553003282188641500233854198283302909676455062335042428271478810798541736972692302397024682764300702362971680590029381246736867638520196791172922404288387541122616211813091943463685403402194819637/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "121765996413538109244722158430733772946581021648295379494316178425975201830123378250127037871022862140665047768946333869871635524590445958253367982270652171353818448747755198251644533171986927552011666923832137891571028711514868831622149886611924577771659219065857057020727239216653669500246218019089692681775/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-63004972185514719302016938882476801018029290150894658797428428794872008178224844068489106570343956469890320581237050176572657244106576400241496924996645905145525690133237596136064437406720491787085549650786601720713499367232077045311041089715211178346785441054922158278590254819899949862505839484404422514173/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "162089912107789904580698670024539381013319877304490279642065801647607770297007606234339566380838505368774389327096714260667996331814249381137709093996072587356720324791880511287815302447216666542808264118488552050522502999610415668210833042811542567219354932850746955158614010677677778588862432609198364889609/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-114541150781975074659493858700499576773418741657487570824179357865241951223155018561684267907712799100922762526706741412523928902105409038951683693424204620570355075936652546398681787931145609090635335092259268023627437543404884939870413071359280803563668076790897925194743799223677433801998275248938099138653/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "28536383328959703993730430075303364190020911254551649423945663982045094704274492977093462377686393175454598424578736919668575596341930388955047068633656361481992620692814813327812876623975978375572536423322145652113828759035405388077251778997084312380853597717028602612494470837499099867849196700594746333193/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-201517388249894989478411032097072751718656423446768498708508564928448662660651229648295542554051448907899318156973678948290345776073447986354173204606393763408869392055271224486081374851034619526102418795206963640221560398265963426462213308991975932816594775660953319668579841424702426262528857537080463794965/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-174513042277315163849266924439208792551210027773319873062117112212107791949617487997311514602133978721591638988373550045126013490861600577744660221983293741489328994487990284644844821816190752936317045684025385986252691736431523152528005392504331486525860129092504396317973074372934850065698391093382548690683/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "20853952201633312877387277508463847055126394746254519899742972932555894208910866792849243688527659586695779456772099102381103863965624564255350878448532450809472846089800434934408081189773222964612807975923115727341248896300480297539550915338524351483735093086771402116129065052573895987568833471894650866121/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-312641081391502269606656250395689464714521237121044730843195101985540858918629890694914712449559446202158312842962672451031785756934401273144496289056535368585556084621907933962326641902682587075123817870096547428328478755021925309233810847720403976729205559662801376490464233034499544774061638742784145893525/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "166672131806845776192896885973661042124973372869940345006468266318743480528703466414015865739675637832291806442497067063319157094307655919219743641987468037062277740025664176448810213542701871758655081692776525610517996057224630655703118199190067622390022656134231632552577778502578893106037108271941930607565/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "-4376967838200489497250994948825473623872235696381225795629850903139948925947408138790254476399212615558494266176816561458243901205759824715627651584088611054101239737165343081922176424447484738906847833188948761892037696110205922052863065492314158621446222809067390965832669530284377833079714832042153910245/5617791046444737211654078721215702292556178059194708039794690036179146118921905097897139916325235500660003558745981042426837180275450519452901482207483566386805246669527046414884444362538940441232908842252656430276192208823201965046059784704400851161354703458893321819998351435577491134526104885300757004288" + ] + ], + "beta": "1/8192", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 9, + "embedding": 1, + "roots": [ + [ + "333910482659483459438655528550746003905249000982454975806894848438737707753764976869561366054330641369183833856032301628669487010009234742939505872476695122089942073608783197493524773122513229557328670182714416409970596568787760524274687406159411184511162472265702547672362929076759614595740589264277517789373/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-47752137171466876261593994891268639759720371836251849522631883826242730835462895269072450253303956251409642499713362915697132486294075863280378249136595798406260146271799670133428231669418934780402000503782168565275986637683350570973550359499708480182227099344116449794282936783930506661431843381346792007145/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "180857061429154340683796569249229633634282740219290917942321763794161703285567755908320831766805092839199995120635992701965884419377793868614453316178802274842846369150241658175248894374357637462187419868434067659967756992677108864166432671147587357826434832424046949718532074646758771501650950393504125313/702223880805592151456759840151962786569522257399338504974336254522393264865238137237142489540654437582500444843247630303354647534431314931612685275935445798350655833690880801860555545317367555154113605281582053784524026102900245630757473088050106395169337932361665227499793929447186391815763110662594625536", + "89031252177887495190665762976190738719635134333314194291508015840329805457255816648024444476560108063934040996807695532427466053700897943316995019084184510458211965571902286576252834532496294909472140013944090159918770767649059087712467909540838463240479671623720707864757601071992191516521915069518033316617/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-77570549831923552874388989142731030044682007042905840083400846000380141528891579777851595702752702328774473303959132662315889278783543232097424451580806347987068043391866782113060657867967927073555566291117612044119958405987268589066112630178066419315079209294063775976558795584459682150886660045413954013769/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "179897435173147029214413437523250288359207247872041518170502120727641382930349650875642891171666569302908673314657961466832174273548337212606432197485311335192890539535613453859826823968059826198019685012450454506061510186429992789952527736462387221084655053453668251388987921959301870000019796834301705370287/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-190010959094347690462269137172070133553459071158786598796602362999138607180514755593009011514443911574926856975116553278070950196565545016104446202259984121956425990468540175254088981798543541253103375431235218242689895049528330746625788021572824829150972581783014458284949616718799691063891716331606263765491/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "99030770506346274571412767249597026710488468973300656614141769044065104917082032751052659130642873032747152401206156730746432904390655127956658220469005080826426402974997601139897941906522466353259384287497934337081931282143875656631456401729850661272991846764776573277336890519241664182121666563815825108741/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-233081207055107292068614793986538528139321828237103534257403268711362307316433680696116996201453280211587720811602707281081949546040375748910078559633641468576989928431965548210945788819468022114946692214502141994372721141673746177085180557226353646152761400166555794272666489885938550232614191513505184437909/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-55943527093538648994131853774327760706423292404958516460832453352530715831038895988364294084379075527404154738093222713072803156085772412806543739693673201174982311509658713101771928709767111169834072902328747368130517026338521314072319621096339894710376582330134409800137590938355592424671582274968784888015/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-73674816051867153651072739874884099639564752966078427342019842615755828513593612394516445502429253037266855084255963456491511864584968452239949356574902784890872662314770973795626380106098390700582613148829779523841278267045301960823172752044249996830463280555136131109752238430106594324223891786255349386507/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "-229807430732849177117110644126555193643659835289545136715286801956254443227030503648670842696618870987609340139528277927495657195520865722750609252335913869508408276603724155327353030563572875987772902902949206596449124196495306939290344827467222870442728695524546121120411264232478377181674795998646854090937/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "21321939274995178538221961206791871382984274797017580984543305003879576871583449027897925288200755917559935688963418115740792809342472296149539253956569356996997885510566587640382490543578910073936695660519193238722044786613345993169911490333550849222184308269478701581148338439803843307487853418615205531513/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304", + "-150737439183938417466026541943664853780573301677390200716773762546802420416786746939455291356847900573293657693272612561521417054798588970409780434875913176859075028648525952666660665297532915477471545641607412073362848129142966744244476665807658602486321803579387819475245914693110974696229125922432406831735/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "35114167688248708489705226725520322239757602458420567049561448419515293002391419875052402245031950661384666638645168035176238701372703027255979313802828205032500024750897988872631333460681293263507451895457087663973744113306278768660451880594853026913028478026418649968409550880245338037923086078312777680791/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304", + "27546478297781289342951459913655862154150871859653605939980547557514582388613385010841997426553751173842745619847075795184069081850799605852120546322776304239444231584968459156764651674979961647993059971657017151034383284332304041936961882154160895082836934427447719866692376787959364467530446014008721598863/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ] + ], + "beta": "1/1024", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 9, + "embedding": 2, + "roots": [ + [ + "36627579605007658966659778461203634251371697379108157264801251842963340495317878340007270952160418991100126967216105106719737629728806468143838917422932843178173126209184087556635317452073232467886327807084905993395510516160589404741476340166934455525421308327705599519861799297110888754524674156034983913189/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "91213904696706307172757488630720409637634441273504301106383789102894171902182804905443189017899008504696948838212829861096814223539148482614848676923111790231266756795679293509188920363735763072749479237417340538439822705330283204140328446148978965322292213168306231351893475906153300657761895447665575697199/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "84035680545684351602473661021561463081168863906638834415994052385965625479101474846868259017791131826318727391437910192088726625481437554020823348149067175314300228396308280676735847981399985641700401470915484644497581666130585473688371033657369860576189725447930344844832440162634723948823836250202417994515/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "8148013099263468190653788738472861941241579884501632117571698363380494060372231299699288233780855988276576215383902261263316045847213105572379987687627519561818982137927974561918890474195006623065707914273566644830852081228319342987631236139162161704438123829472498354324469835175859687317768243701014103519/11235582092889474423308157442431404585112356118389416079589380072358292237843810195794279832650471001320007117491962084853674360550901038905802964414967132773610493339054092829768888725077880882465817684505312860552384417646403930092119569408801702322709406917786643639996702871154982269052209770601514008576" + ], + [ + "-100078953961497513827019582958503948692313436745489773412119737617020533859319405373115780371895107700252180090915260674831636736234959936041881253145088199481284819872914984423224863245178613426667354296068721645475017118632587754300463918861969486842414948740548757053004934043822785610986714760398365599679/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "3398809930139403861148899090261015484845408816967426658162601582201664636905280230206674173374829015640972007851858863447180055375534479268107072312487849563160091306886763149122921123989532906823269948436995082554330272656634564774170850622113683532802699002449190529818559937755553698477368426140195610501/2808895523222368605827039360607851146278089029597354019897345018089573059460952548948569958162617750330001779372990521213418590137725259726450741103741783193402623334763523207442222181269470220616454421126328215138096104411600982523029892352200425580677351729446660909999175717788745567263052442650378502144" + ], + [ + "-183338193122679443380740560128812455004059475231783258422114826847995734608876245819348478430541727370982727757486771145154226239259518782402684145929956021883455556122678489997638290182053381073341880321623966722662080562479192139016173619844654784754986657599090969957280567175733144107276191731039944767793/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "69544043884892615520046310400849713710736128335193355114162837516266036707296210585162307101033581669414559740283356404136662487557992456157952373635087040782218145130401822170858673477542223017483990259128019803079762888726928377309670948765232529247230492706760919274284002471550667971352710783976141811759/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-286271387236816925280241522879228420963755468856311152978521691079419985629370744590058055558139090150368540678259547716089060942385350516235204508672078069739575899105386310373908278914441421362759756269445058265422389064137253935790453915270461746334070802354549224387950778330302172659661620800950476186749/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-82918958338806825753830833680976263062074588869905593699233198939242160296448906481827055827641905389023514571488788279137339639543608846689251136263565750412573086750041060060195606898601160434500732786154396471493243930049913562346718453598705146259982726005531537274756750753151714066487137785910761431947/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-49807632985904636056327801309165668569949679703177249904015612774568110724009981257491882061879367530463687202275856313301341867893146717453038446249068471976860842053788497157502426856271448101222353866671376525212460060433231010076669364400926876741344107657680474212816727791674300296404422336397687738749/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "-177362022940644076757392587993194089526114195004881930778497281946886928035272836044916000656700084837927346549061559295412976727004631522383668857538236746314783697433474028860696915143971089197553031019918950340000537004506529613569767212474004309695951498140271896557248889203205304701749822638973665710421/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "151726435005196152503621229407512430240201194430624150994328999718615893705101127231153874291153282523199899481986566943279721987880106907314573029521495326835809641098557389722103622116104726637641894632029695112812573695921454951502415653852282073265566820064948245713045069992446951560447509654860385758977/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-384822354883360534431812042911405387725218348666290124845083009057711843252196160570381320302098793490714437674025650657316209395944001060980319931861297115592823638687839794408498221389027544281560445374349368840423996714188312856799321242909238654232390908052313482832343212428064897303568712693638467285975/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "41081431198079572611558466625440658048255168639522243169055624589826066923314664776521434977008446938486253681718692790654307094043265416041383699295454020975360572161215700150415363540172271447445087225207715238810462166560904016969936740545340760747113041037652787910341644753600676564529962945902837220001/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304", + "-4118711747111065465143117971635801376758138406433752164082253287354658505291179385338879623132445718177109921503638931942611426340975801223027948444391682221345950298080184044770827371312364405460096337648485815254515555637274146065727250436766509743948076237782619108756462233723207660043495600271274827343/5617791046444737211654078721215702292556178059194708039794690036179146118921905097897139916325235500660003558745981042426837180275450519452901482207483566386805246669527046414884444362538940441232908842252656430276192208823201965046059784704400851161354703458893321819998351435577491134526104885300757004288" + ] + ], + "beta": "1/128", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 11, + "embedding": 1, + "roots": [ + [ + "19987067627228188344629069299179400482723624880399215433823291767545287429199097189201872739530866475858846834340571882225835111913315556842511345498467666815253246841468908666504463346483028254245326381190693095283853100267355904488055841487849491381199845949444150700195520393828374821557134768600767466237/11235582092889474423308157442431404585112356118389416079589380072358292237843810195794279832650471001320007117491962084853674360550901038905802964414967132773610493339054092829768888725077880882465817684505312860552384417646403930092119569408801702322709406917786643639996702871154982269052209770601514008576", + "-16371177452751777825563018362473384628992592467063145384041920070193938502884230358731455517486303546488422975735506625293320144959392098974784869852824091878513232785682339953450977565251051966045793101131935501779170807314388776610230256291440229867741336996952861254445223349520745729923222550176564288491/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "18856846747548568697588208088342677025973301317628666942362894682533954455666322781604686688583386331954228030929273184779113235417601784513933283718249884792714800236464676089878514996628927413059992636963593921322785923317037817194703770654332326501994334024022987493666601426630817081203976984338145763405/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152", + "92987134558769461110036206867296860043881621638534166853641725913226172224366088756826381486275497978147294133585381794639930001435905110892538226145300666954747499650465654558096450639522609112222032585019033582960779504653453557208357386268301504380446208517791958035784800586179182112037390042935466531117/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-8755627176049049991226664047137245698863739906064153437347452970558147035098726451283760392997679178295614102787623006912674241102405755920868082634752574119386112664741472162925566921061850884242496676415467646079844403140934545444691802820099406918031463518136566579394224020189874248767924449767942783925/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "184869178819451977603611176386928738242876901648101569688171783567941034492292441694469196166591126057251772941746470171157037212752090292935695497021766339398687078438294125034073412980357691297887600434603353395394298477189459158524716423700412207205879422399971470449045719677938588065634394716581191836817/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-54478583300645253822831870111416997505140953588934025523583341251965664154365796078024298205741864555549713807076133144301802106929744713687687990384993502959532496048549753489310281500438525352868503316582822328826656480517864695496618221362284012857411443021555596782792697074220181225526863918268300639411/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "20286205262628437605254043475721537150966571526564811549532640552204714056754728803364947802459551692869353686447919641018139868478560640763273306515452613049046891837083267506195031814938252858003236870013002284111289860505997396859958206617069856782707127987927582577818632717973254483287992421656734652759/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152" + ], + [ + "-95898183509014184241500254592800463383859036505354131097291586846162888704186664657955359052988941231121132518651068021267889402827792190056019212109768207300155797496969688201128119018149578616452527735438289364195597833846776297049494445152908588057194749724385825905412784224692093180207921450384112242461/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "42778814428655042090098870059327487099864258445354926673871694836725119840952203199861360259612720795076463940032853087688047118369165810858094712277252996243488507752097503657331562950399220905133886815882248888535031166708361760343306732503522179656046809130881476963896662304795263022774723587080694995587/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-225921504279610020642388278131970798218208536978767361355204927337288732255627291982651523854880824990070444198973400989148467743303745890374317986738214990201636073279077380395278347044974050305694703888747355737926977743906487115905900433985192373300492134362778507994126188996113276482333293522946874166163/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-18512006630388580492498585919316792146843256940712140321718354870283077911759945301636725256521424427374811915420777847665766697831971631267719642616122994338671795328699256187096082707061323572720759145517912510241431847044219321767359552211168619158510793131072148281713269420146872738380344999839805482673/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-180384503040408332969274788910647993002194348933408627006352614755504198801432827860872973900664892565262188160970148757056307523990146812970216425530483920281444046886004414828488834832305952363622670602928505922661923912562146105294903808098488454307366830380059864074416998974794846587590490652864169574297/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-176646969751708359448147936704547232946199217170499539675033536510376224673878639512761397186205834591084970427821916955369563206972314869103885725048066220048023304706002429705664922747797907812155061260294680552052160516977538525542207321666484952876348281560646346378263539923187144743564731897674171100239/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-38861837212388384976420529976991509417115833041275628837436068047549600060280382176786322036369939502791851622004559175908329336385610877310085063200757697917251570206071466998822689139170709736990644246151849501271239337143095479406182219416332143451639476774213058321348321744184322700650862375330310963823/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-277565260286031004677878130054188583191705289863934684844268782639173497999273973903587616669187872134632967542328894598608374892255412381085758974558621898023147837402060395658900058771526410416451986547731710938161234642213649079303903522523174051553608817790842230009020182395206171132818408527279761433361/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "21488211622826500960553162925976956012202845211007392491489641798267308432671711630040098232679466316650764179735598419427366676486749904192558644332299235921421144714023516384651586190355271133895433014816047193327744219762731373547159612179053454955452144677625900088969121688703953521421817439565637653255/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152", + "-128511894661549286531404877158872813325425204854650114042374504318410629316789283103583139449251533177702910299315398368686906037165442415057629373076402635077289348627984153358667785498500978795932314288919594386024513282286275663286707605543358820950021120445081138909212973329449308021598533550888061275955/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "83585712907819930372525737678387002726043373066088394654745598301106562580077687197093984735045193590830082209556833412016347775904780083057550263000319559749883171904511683435215084292917686994094634613938974636571702338378693688527807890580242888639214849494751714712417179164070115873698326690655414974855/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "39527043648482950010229499119972439999724135181397298119791477377378696955872414923351111484626654042810194997537223158576386497412597956774521165982556008744194574609655834444282255397016231889321227196472166056329130778270908426382465705876154201534793629442915901015100724328325125021229484333621969864103/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ] + ], + "beta": "1/1024", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 13, + "embedding": 1, + "roots": [ + [ + "18692326237161478268382893815511145026088685648190526628486457135249558896952920917514467617130261745382206732573150104474804362843637309165023312885970700945843085407379411136466208630482730176116475442280579227987505293153616103902239142645063037996256214288997875546400775697052054140996875722199535144377/11235582092889474423308157442431404585112356118389416079589380072358292237843810195794279832650471001320007117491962084853674360550901038905802964414967132773610493339054092829768888725077880882465817684505312860552384417646403930092119569408801702322709406917786643639996702871154982269052209770601514008576", + "6486859248533430000780273205701654512173970909417755732036832012643583151844496919483104176207017793400666110165169957902541959012070998111285223760348081928328199544477282093388192150307015875863662558373792923793254558604148460967249276341192795957495960108311024542088237938103987924150576546911604521261/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "157323348664187956666822829330189664661635426810358914253796127992247865612061106690649235990527526045899298682970108967127473022845446753514004123946631683036181536536551113663594714055940804627834938973774495105472785669307840365432825878956659739101252967010629991460289857031165177301889783427611928177035/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "40452681226070075570072472344401074944712003983589808887925600577667159697646220867905051803615621855045591166578947446549771630680539405755136473452812017494827925564012739248547906421181216869880258586492201563801160785331284811700400735399327336162196251093715630564873576011674857714278044254516933544179/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "34899392812722428966123339680611544816703491872217428378010116691058846226498126253227436478273425414652638211700583485046158136663268894227982165278243907434398134769506468269248093633129553630375056939180388351514797408409815225914896580843925098996214002147635347069013543757886234918338529369491958625833/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "88011579740709610420551536777095471880520733731329804909182057295159138856658844441946791253952523971367978325361906101288855444899057938251340285018035035161867960959529967697490808156919827046584265520088861647898766523277648589169329276572810161414081405603460615665641982272371797657744614418548585824559/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-23632344362636047103245294315793142313888805211632242345277872394180256512662942947584023084035033218243173110811282908595282258284332226870800162079433188907613058231842037992245668397834548268318570993706111537983389312729510092584842380438077530588177371098312347383358971591168761951695032633273140864129/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "179549417839364571074172991064461500088264697781045040638237379539937742850790852186678832881823049512825498163936194969819369072795634141188946475578546985346143228307209114122988494462198458310511930360221307110264021454197646686772971727200632632260525068224424641531327341793787119527322865955849707710265/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-64171504828073803152954152937711567711542666684035601356646712378688470076580612870475769092135067000533842853688036144897397023533079657883641351971704778429165978068814538057468601770310658772323207554597087096804145799486637998411913965567996425496787598923735682562388421874636442133233905377559485353157/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "73251115769149306473345828646266294966486765451643471177403942814435204983959223865491318323457407052192740413543012493039306909122000661827522200300183854470520931139463523567192277441532807875169028627798601616463280909274217382738236473252288608372738895951142823317852525506369814133883275719630758807137/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-96104599738951769633676493389601285253005282559510584694569816846333257502863917660923538247139087495252208921646849092614916922614604316843162321832456288793741483649147875280476706456286703917113215728033231503625203893643516836727765185675495923663427569333306934484123850806643288701454825729811953604323/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "9516631030430603547304258413179041787814767345466107116984577378638068226215235344637777767447480019230821635109605408066669055840851972438579815757178810228708736258218847736218387748283693992362423328654952423382366630325601232318115927373324378897688359132242894713899973429384583590542101150580140274839/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152" + ], + [ + "-55062228354540215497376005863565840475664320925484203015301893653352734911931366500499734179862501376983233255651835114951841126300871292416409994938947913247339808265695383764522624850188675657931604747407328681915351414694957246542297547449812418192888195444651234827845753423977115916824720713929628153581/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304", + "-12496569895905601754496446211252110954226257293968968523070001442676531897713204634587293165700868423273240811744498014947415054071256992206134858336956107724864774886993506222731936628197452918495709094251331874681454069575341628004137867852588704373449128871488326320348282721855230926986775081427488534319/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-97236621922926488171753094952475321839966850867104708437058094218576032195216305246450562921641655245078955900922369570464505990156267416121818652856643194067118861143473065056879134133679172250527578434553971705148706518072819842042031704168804575722945478691295867602666460085505768296696878111825723393123/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "-139974366379725222238941562299015165007954582856054307766040303104694071987798318784342412584103837521837750166553176969910384907399840762917340723142586181202439284159762153726030716323608885065258852362112003980666178559063919724073261539914546317386542228981943211320210328234291676368809663605528890583427/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-12916153817227395308964320333307521693172637922378933961237847141531974139138197199274579477201858620610500507563920459598428400153777012639967564196276145126945301605944903521853118392469464413956941118844472993633600262566258024731392397410303362620852019080248276163503519613363724636522615542062596291175/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152", + "-238994272365838385358698151204558291126185120423482408759980968611149377358699437412307564621248256757262516810026759206258728546995344843798934973819120821031754741483239472065190876326354096946934497360840975069467809446930323282385605750700824263085431792466905140472727845592124191127039452483105619360915/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "6013043937133886929785992231257511969627667249481246735439580322562221982328578577554836403334984733439034934735034117774148354364364987263562214790340175882986670622045334794157783337444852881404655139096629253059946504379613666594193738691315078072319789952637941430021364779329441507323583528933381210005/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152", + "-278679923529189704360039255534940158059487346553817563199472560610069982490137529352759281333079523373930862003820159709004193000121849875645389874369158065539387537232566451095140876980715405549825629533527920059018461562814145916859044343901996440993708624557401126980979858868823094800991662382134844602877/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "109989007535808651476018626898092526943022773744744817418914845584436965704556653332778848051969834606627072091810750458326495050646220897112757542708660487042684367750689381549049479775617896373974012758542109149431726669145658671611746929890662655791701705849605871346529807065359253700271713756945440448383/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "-51882011778821188484364240793453110774348786484062001914177257798483135937985388930919631365603190565770832669699636056548063889192925119116887789197614808884804148831874399739412809224443826013793004508047851389354227654919416055982643722487389332768423157423587133671627261738239235292352438537394793285609/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ], + [ + "105894466188666824637797522379481298816044382741836996193011641682857452110816736028928950018833122381771371198703803457128745525851017334778410249826879397875759195534689495859965994904874626346162905042038177007336006951294064455526202243127641508935278616124494878183999313811884724475030368145374684989523/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "70513352389598145213663477133635023707890899921823566159207226270576916995395924683079445594271942693838367850660040457845959093720558038483352469338574636265642119180155548293660979873985809604194360555360145016038237726142654627699688283243073137486408739406691752226458425337231524766414622661143826464579/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ] + ], + "beta": "1/4096", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 16, + "embedding": 1, + "roots": [ + [ + "134039650432496433101295605159145494804947147618859989214825957778126813783946265379824234530653079795983300535220081531974499830210731306488624875267801121995052729438299927149721093666927526785655754801147235486784301827065913383198135946696241002975265831017168785200446019385215181318777012203053206775435/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "10043776175087489111857420427705466089122018604250422834704851221257606484042652956267827527042103582138401817998484317090147751084140645935922861891946502301969712627060390112286498548692413675638854082746767615556998261778873625372575511704320589333963130560858950109780981665146820923938000446283595843981/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ], + [ + "163698198267763187271175317732354162942142798991132287897605537834861074139898973926663170112137318749861087075458509497866923709014367775583409379820255381037822285641799332965596998682187512678394888610812074850883841645394925104103931217581714852536893012837648469034763538149987146660169793180318525683963/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "34154907814115855601778002615718880203068084565931904547779687937911408288344869439590995495717368706638636414617448243280929199776252293685154663952500722290615662112290390816093868694604275838431637064859423302174318393837094657848778434379080583038727143019868879816065247203874832557642095346180510541817/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "125972697409629971610668644095806954773026269483836139794069300342348858033512225247311677027781101220433900638850299785029618718841248714192496025858197851778421685409754264599923508300047622246726630559684778235132368096407527643305232066166954976575730325609055979040383084148029612053926198944646591312277/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "15167790659874947924589060300057100404989113576637779018845337397852208471948163165837442910874732484685189549202575299032263922362242746686661085009319025178790114153139930066286476936454793858408781296809315075998603335912470151363640101092646280120351957483245267415973808462131927199015047640649421685169/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152" + ], + [ + "13853536865015261579911150032049872304272006558508656999350196565098776518334784731805531655741656799427586114638867558728051351302042284720128353136488689847220369858233808059733505486343038607449224336533854935610047845464572670709769013819513710914519750342782309697087053886069773135656466958608061541769/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "177545851147179895490196191648273709559870852473948635168982933050035672511543664292889660396400875012049726711091359491491643948309945736293014186853449971590825791166882789030071391843162221062181697202769315484013800917514554939433749527198631298084673567294376435632058165815416832640235572073617726120941/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-52210378056113995222526794456200026551550434350267615704607002484161409961625123864247636241912256583356359184500954597575895892110205892926433892520877857803012652172002684435938465544783335544671181399418477865628149454975798200306362483024809010252305140774988065045567446320437361416053738363358747644443/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "87648308710707093471187039917458706451472578491021738770540393300719242093206053400276097328660396266053722682800563211432811793974391639650142917556304518681178604701687327846402527191048522814812999729648713916842250073122954579935163661634587626288322854319550536493507991774193503157659239580292987842157/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-116664073824034912718051835779935450320038013857443941308097484208019490686854521720422334021093095268154662714097019061138743852755115144088228123078315232346900394049166264273018455963049040513237001187564736700035245183063339192035351382225907798789582613795974065118752512750692942562782534375193614661861/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "149449269678260753521945326074791968079519019469792743136375292271466248404832296872514640066703937306939051683043529915596390678603913779661604066173180108039752595884583226240160259044735240089986116711339120429442816430176353855415258845446067522565220002881930958366647672375789662340506634532555558066251/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-85610957404387028634243322426648242688663257839375635069698465559559419377521551982033761821736612609921595358004172251326835155119996617686944093557730406618580170261786725657706867217353963671009491290423195732204000640025294244393939752267572032643929785491689258684316664163295188812404572449637311320451/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "99615833663101054301816080147826293655285718447019552564330413357835145945778960092597289825973787281964918942430276502793281215764935713502351704443126657759517272838966727793208748184206115834330960302736430555573552466912693730743584134891685941797179902285300308856534717258649051539716231977831990434935/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-206470925126790414958903095327931072696188278347167769164325237872418927430185815104414777620540205015448274164195641352218542457975169039791010753378777708716944076446597350330115681723054142766603880278838717720575430103778172708862328494065918713903827091679242299103863352097855468435963485647011288487845/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "28326730094049526360308020645864856724598891128838513609367588904514833835204347361667185978800994436970191543152173345365891935121884286237303162650500563575271973969509154285033455092089962932786873166080400502570268738193931444116625301385853996639117280974700258567439169279262226550039720244993440086577/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-212793201622109962448330100692808593439645159644577548679667883054110536914612983822159045347472254754395342771708966598767283083523909873556284381276124835470115664134649247694090104295004718385271153849431718533152316853933967919972046963990390480364949318130626453951329110678301062337081449200475601735875/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-57964249005932469131896837719919287256295100537523457777437606447238450243954529094264672294496860934864424519386491456408615251057823684209861120741434670159618673936343232127524840096572869938406481577342691505214852241781904532730223280532007263456890157126325151281429988053858853115810915974956182248013/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-181906514405143036384357434995971625275836390798303598349017616251000415282024441569357952686816616444878672327665448828051994214624348737805868406889846662816154885625310561267277397135353478192043756460106331313083421328902239020972755544322708347048855909898995764083966273823919667161396109476550719848725/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-147945663340461763698212430143771286414026284146309945071685010721085537380641268203814890803383015075422455405339014135542776026293391412163500686456905034790428849048670266153134094858649998069511486106390629359568273414843847740088984032890568291491121209596476991217967574780912075401622245788540973317237/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-109295650712632922954470152700014140962344687784228817505917409852933900860213282982253187319663670767937851495649957296830456277490544817826798947725684889752695688092754004821393186285277520453649669774004548684876352062161227459330029625465970767406457202300678613241928430071212855440266575276167464763807/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-56200741848002868079111868432724886507129621548125121648642474266599250489673841691778046881437449293933434722648357280706913445930283045991236908716738562916199191451345481529063774448710946467551285759609323141571550416355308596877200595274065373565280076263027603986562578831336689401091825392816459762247/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ], + [ + "15968822176892792285891476438139425317687583108455281192008770761103687215213981897594608046751009662616135817210933151016991807601573680585709456982599855455736137633949541869722566316681492518193528500018722529515726386747292338115274696063766393314538517893691137581991598848479112650484943606294759671/1404447761611184302913519680303925573139044514798677009948672509044786529730476274474284979081308875165000889686495260606709295068862629863225370551870891596701311667381761603721111090634735110308227210563164107569048052205800491261514946176100212790338675864723330454999587858894372783631526221325189251072", + "-266324790638046954468748086815326096854011998014910958879637384810491281671701735342579622902906841022217262017537242815542832447116697353634706329017518582629343845840130883918382746688279956080610789278337184153491906948023245930590272626869013417164765399270940382908317755754807962553226947387458433481969/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "1060865642031292630770255648031651464303955219241748845301061404301449150107131123877033982501236564870546734157170738071205142825981730629211934466958373310795930234883644313113012070731987912222503770737372313560840648279391481374684780737322726034313967342539259478356716096981485614792922808816297076935/1404447761611184302913519680303925573139044514798677009948672509044786529730476274474284979081308875165000889686495260606709295068862629863225370551870891596701311667381761603721111090634735110308227210563164107569048052205800491261514946176100212790338675864723330454999587858894372783631526221325189251072", + "-246799233700152837800565619104070457222176842192478672102595825359550055541867252492449227477274629665694532828700249246838030620913792598556947021011742874894999694125075108903854687975235844168506798118891370394456073402356817011957930168970746212902758217822556747842079095849448037149783703853881509351465/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "74864797941206513281047175374406371423373655545874336711328481273747977974984455616940936075339467433634151221026156653070150698647294564580345247390350645817572015177013890581338145235391049860293804890641833349803840457797326162410138640935908664989180260619163393823243511563841284652103776498758852275761/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "158507016237416030279508951176317259509379692049347194102510424353036380843727700204504205980624447511489013333078714007658126019484831026660454241743943509290714726174111157436372813963025263036212831092360360315950519574485871493725846468575071813444421951074798721371147434849601216160281721594412331444679/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "126287595802823388378145790573347116516250877023657551588569070335106577368621778092749228800089231992059072999369812292461321688715048725080489109408634374024142218044000898630952519239661477382516567361587110636505950019813691734756152201601098996057298499115007197346303456331071237494888612444968034206643/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "-143526397691224128056251209454968080411106577138808675995376721394908697117978740021220231248704896684803444156609685788793425078524968774144075750535259582404256698559171991950020896681595928832179228331976729295065837037698098662420392076528307364731612360503267270299597486337931330781272500922478650324859/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ] + ], + "beta": "1/512", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + } +] diff --git a/research/dirty-stride-phases/vendor/pr628/NOTICE.md b/research/dirty-stride-phases/vendor/pr628/NOTICE.md new file mode 100644 index 0000000000..22fbeb8ef0 --- /dev/null +++ b/research/dirty-stride-phases/vendor/pr628/NOTICE.md @@ -0,0 +1,24 @@ +# Attribution and scope + +Ali Romman's PR621, exact head 520774462b19b29af41554b74def31f9d01e997e, +supplies the prime-power kernel circle bound. Its kernel attribution is +OpenAI's exact-DFT preprint at adc7f1241b42e322a6451854ab7e4b4c146bf78a +(`loc:newton`, `loc:fourier-factorization`) and classical q-Pochhammer/Newton +factorization, including Alexey Kuznetsov's cited q-calculus work. This +package does not claim to originate those constructions. + +Pan's approximate-factorization theorem is used in the form stated by +Mehlhorn, Sagraloff and Wang; Brent's work supplies fast elementary-function +evaluation. Causal/anticausal recursive filtering is standard, as illustrated +by the Briand-Davy source listed in SOURCE.json. Sources are cited for these +specific tools, not as proofs of this package's complete claim. + +The scan rounding analysis, explicit budget composition, interval and +factor certificates, routed reference execution, and packaging were +prepared with substantial OpenAI Codex assistance for chafreaky. The dense +matrix solver and algebraic coefficient crosschecks provide independent +computational paths, not human peer review or formal Lean verification. + +No new multiplication exponent, literature priority, maintainer acceptance, +physical tape execution, or production performance result is claimed. +The code and documents use the repository's Apache-2.0 license. diff --git a/research/dirty-stride-phases/vendor/pr628/SOURCE.json b/research/dirty-stride-phases/vendor/pr628/SOURCE.json new file mode 100644 index 0000000000..59bddaea4d --- /dev/null +++ b/research/dirty-stride-phases/vendor/pr628/SOURCE.json @@ -0,0 +1,18 @@ +{ + "upstream_kernel_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/621", + "upstream_kernel_head": "520774462b19b29af41554b74def31f9d01e997e", + "upstream_proof_url": "https://github.com/CrocSwap/integer-mult-bounds/blob/520774462b19b29af41554b74def31f9d01e997e/research/prime-power-cyclic-inverse/PROOF.md", + "upstream_proof_sha256": "2b8056c88e66f692f407450fff0414d41bcd09db8597be22e274a6c3dc20eb9e", + "factorization_primary": "https://arxiv.org/pdf/1301.4870", + "factorization_result": "Theorem 2 and Corollary 1, PDF page 8, crediting Pan", + "elementary_functions_primary": "https://maths-people.anu.edu.au/~brent/pub/pub034.html", + "recursive_filter_primary": "https://www.ipol.im/pub/art/2019/257/article_lr.pdf", + "local_provenance": { + "stable-cyclic-scan": "bc36a9d44893f9cd25225b64b08f1f3e938a248f39c16fa50d71e84eb0a1b0ef", + "stable-cyclic-mixed": "df063d9ec36d95a65119af4518137f78935ac6fac0e88de11e6a7212492afe4a", + "uniform-neighbor-cyclic-inverse": "1f8fc021a466d03d62ccf708ef6cc83d2b38b340b50893fbcceb39c704922a71" + }, + "base_commit": "ed49217ad6244f1d3bfe4588f122fa861849739c", + "reference_runtime": "Python standard library; no external packages or historical workspace files required.", + "unimplemented": "Pan worst-case factorizer, fast elementary-function implementation, literal tape simulator, dirty-scratch restoration, complete multiplication reduction." +} diff --git a/research/dirty-stride-phases/vendor/pr628/check.py b/research/dirty-stride-phases/vendor/pr628/check.py new file mode 100644 index 0000000000..5ef6dd67b6 --- /dev/null +++ b/research/dirty-stride-phases/vendor/pr628/check.py @@ -0,0 +1,178 @@ +"""Rational proof of mixed inside/outside cyclic factor inversion.""" +from pathlib import Path +from fractions import Fraction as F +import argparse,importlib.util,json,math,sys +sys.set_int_max_str_digits(100000) +P=Path(__file__).resolve().parent +def module(name): + s=importlib.util.spec_from_file_location(name,P/(name+'.py'));m=importlib.util.module_from_spec(s);s.loader.exec_module(m);return m +c=module('scan');ik=module('interval_kernel') + +def prime_power(r): + if type(r)!=int or r<3:return False + p=next((d for d in range(2,math.isqrt(r)+1) if r%d==0),r) + while r%p==0:r//=p + return r==1 + +def certify(data): + r,k=data['radix'],data['embedding'] + c.need(prime_power(r) and type(k)==int and 00 and type(target)==int and target>0,'precision budget') + c.need(type(fb)==int and 0=F(1,2),'gauge chart') + parameters=[im/(1+re) for im in v[1] for re in v[0]] + mid=(min(parameters)+max(parameters))/2 + t=c.rounded((mid,F(0)),1024)[0] + sigma=c.mul(center,((1-t*t)/(1+t*t),2*t/(1+t*t))) + c.need(c.norm2(sigma)==1,'exact rational unit phase') + error=sum(max(abs(endpoint-coordinate) for endpoint in iv) for iv,coordinate in zip(box,sigma)) + c.need(error0) + for name in ('unit_root','missing_root','wrong_embedding','low_precision','bad_margin'): + row=json.loads(json.dumps(mixed)) + if name=='unit_root':row['roots'][0]=['1','0'] + if name=='missing_root':row['roots'].pop() + if name=='wrong_embedding':row['embedding']=row['radix'] + if name=='low_precision':row['working_bits']=8 + if name=='bad_margin':row['beta']='1' + try:certify(row) + except ValueError as error:controls.append(dict(name=name,rejected=str(error))) + else:raise ValueError('bad control accepted '+name) + state=certify(mixed);x=[c.ONE,c.ZERO,(F(1,2),F(1,4))] + bad=apply(x,state,1,omit_inner_shift=True) + try:residual_check(x,bad,state,1) + except ValueError as error:controls.append(dict(name='omitted_inner_shift',rejected=str(error))) + else:raise ValueError('inner-shift mutation accepted') + try:apply(x,state,1,(F(1),F(1))) + except ValueError as error:controls.append(dict(name='nonunit_gauge',rejected=str(error))) + else:raise ValueError('nonunit gauge accepted') + args.out.write_text(json.dumps(dict(status='passed',kernel_crosschecks=crosschecks,irrational_gauge=gauge_record,certificates=certificates,cases=cases,controls=controls),indent=2)+'\n') + print(json.dumps(dict(status='passed',certificates=len(certificates),cases=len(cases),dense_cases=sum(row['dense_comparison'] for row in cases),controls=len(controls)))) + +if __name__=='__main__':main() diff --git a/research/dirty-stride-phases/vendor/pr628/interval_kernel.py b/research/dirty-stride-phases/vendor/pr628/interval_kernel.py new file mode 100644 index 0000000000..1182175a55 --- /dev/null +++ b/research/dirty-stride-phases/vendor/pr628/interval_kernel.py @@ -0,0 +1,61 @@ +"""Outward-rounded rational enclosures for prime-power cyclic kernels.""" +from fractions import Fraction as F +import math +from functools import lru_cache + +BITS=1536 +SCALE=1<4:raise ValueError('angle bound') + itheta=(point(0),theta) + total=term=ONE + # Taylor remainder for complex exp: <=exp(4)*4^(N+1)/(N+1)! <128*... + n=0 + while True: + n+=1;term=cmul(term,itheta);term=(scale(term[0],F(1,n)),scale(term[1],F(1,n)));total=cadd(total,term) + remainder=F(128*4**(n+1),math.factorial(n+1)) + if remainder 0, 'empty cycle') + need(direction in (-1, 1), 'invalid direction') + need(0 < beta <= 1, 'invalid margin') + need(norm2(b) <= (1-beta)**2, 'uncertified stable factor') + u = F(1, 1 << bits) + need(u <= beta*beta/2, 'precision too low for closure') + order = list(range(len(x))) if direction == 1 else list(reversed(range(len(x)))) + z, power = ZERO, ONE + for i in order: + z = rounded(add(x[i], mul(b, z)), bits) + power = rounded(mul(b, power), bits) + den = sub(ONE, power) + need(norm2(den) >= (beta/2)**2, 'closure lower bound failed') + seed = rounded(div(z, den), bits) + y, previous = [ZERO]*len(x), seed + for i in order: + previous = rounded(add(x[i], mul(b, previous)), bits) + y[i] = previous + return y + +def dense_solve(x, b, direction): + """Independent exact Gaussian elimination on the cyclic matrix.""" + n = len(x) + a = [[ZERO for _ in range(n)] + [x[i]] for i in range(n)] + for i in range(n): + a[i][i] = add(a[i][i], ONE) + j = (i-direction) % n + a[i][j] = sub(a[i][j], b) + for k in range(n): + pivot = next(i for i in range(k, n) if a[i][k] != ZERO) + a[k], a[pivot] = a[pivot], a[k] + p = a[k][k] + a[k] = [div(v, p) for v in a[k]] + for i in range(n): + if i == k: continue + p = a[i][k] + a[i] = [sub(v, mul(p, w)) for v, w in zip(a[i], a[k])] + return [row[-1] for row in a] + +def residual_bound(x, y, b, beta, direction, bound): + # Neumann inverse norm <= 1/beta converts residual to forward error. + for i in range(len(x)): + residual = sub(sub(y[i], mul(b, y[(i-direction) % len(x)])), x[i]) + need(norm2(residual) <= (beta*bound)**2, 'residual error bound failed') + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--out', type=Path, required=True) + args = parser.parse_args() + cases = [] + for beta in (F(1, 2), F(1, 16), F(1, 4096)): + for unit in (ONE, (F(-1), F(0)), (F(3, 5), F(4, 5))): + b = mul((1-beta, F(0)), unit) + for n in (1, 2, 3, 8, 17, 64): + x = [(F((i*7)%13-6, 8), F((i*11)%17-8, 16)) for i in range(n)] + B = max(abs(v[0])+abs(v[1]) for v in x) + for direction in (-1, 1): + bits = 64 + bound = 6*(B+1)*F(1, 1 << bits)/beta**3 + y = scan(x, b, beta, bits, direction) + residual_bound(x, y, b, beta, direction, bound) + if n <= 8: + exact = dense_solve(x, b, direction) + need(all(norm2(sub(v,w)) <= bound**2 for v,w in zip(y,exact)), 'dense comparison failed') + cases.append(dict(beta=str(beta), b=[str(v) for v in b], length=n, + direction=direction, bits=bits, forward_error_bound=str(bound), + dense_crosscheck=n<=8, residual_check=True)) + controls = [] + for name, x, b, beta, bits, direction in ( + ('unstable', [ONE], ONE, F(1,2), 64, 1), + ('underprecision', [ONE], (F(15,16),F(0)), F(1,16), 3, 1), + ('empty', [], ZERO, F(1,2), 64, 1), + ('bad_direction', [ONE], ZERO, F(1,2), 64, 0), + ): + try: scan(x,b,beta,bits,direction) + except ValueError as error: controls.append(dict(name=name,rejected=str(error))) + else: raise ValueError('negative control accepted: '+name) + x = [ONE, ZERO, ONE] + b, beta = (F(1,2),F(0)), F(1,2) + y = scan(x,b,beta,64,1) + y[0] = add(y[0],ONE) + try: residual_bound(x,y,b,beta,1,F(1,1<<40)) + except ValueError as error: controls.append(dict(name='corrupt_output',rejected=str(error))) + else: raise ValueError('corrupt output accepted') + args.out.write_text(json.dumps(dict(status='passed',cases=cases,controls=controls),indent=2)+'\n') + print(json.dumps(dict(status='passed',cases=len(cases),dense_cases=sum(c['dense_crosscheck'] for c in cases),controls=len(controls)))) + +if __name__ == '__main__': main() diff --git a/research/dirty-stride-phases/vendor/pr985/LICENSE b/research/dirty-stride-phases/vendor/pr985/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/dirty-stride-phases/vendor/pr985/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/dirty-stride-phases/vendor/pr985/NOTICE.md b/research/dirty-stride-phases/vendor/pr985/NOTICE.md new file mode 100644 index 0000000000..a96d0c7fea --- /dev/null +++ b/research/dirty-stride-phases/vendor/pr985/NOTICE.md @@ -0,0 +1,39 @@ +# Attribution and license + +New material is prepared for Ali Romman (@aliromman), with substantial +OpenAI Codex assistance in the derivation, implementation, tests, and text. +One AI agent performed this work. The separate exact arithmetic paths are +not independent human review or a formal proof of the full theorem. + +The new files use Apache-2.0. The retained predecessor files keep their +original notices and source pins in `SOURCE.json`. + +- Rohan Guliani (@Rohansguliani), PR846, supplies the Euclidean chain and + closure decomposition and its linear-tape clean-storage solver. This + submission uses that decomposition and supplies a separate dirty transport + proof. It does not reuse the clean queue or its traffic constant. +- Chafik Boukhalfa (@chafreaky), PR628, supplies certified factor data, + paid coefficient and phase preparation, rounded integer lifts, and the + balanced dirty commutator. Its unchanged checker and dense solver check + the original kernels here. Its original dirty proof supplies the + conservative full-word perturbation argument. +- Charles Bethin (@cbethin), PR764, supplies the shared-suffix estimate used + in the weighted error argument, also used by PR846. No PR764 code is used. +- Ali Romman, PR621, supplies the uniform cyclic inverse bound and retained + kernel lineage. PR628's notice credits the pinned OpenAI exact-DFT + preprint, classical Newton and q-Pochhammer factorization, Alexey + Kuznetsov, and the cited preparation and filtering methods. Those credits + remain applicable. No priority claim is made for those methods. +- 0xkilgore's PR663 independently audits exact restoration and the binary + leaf count. PR673, PR689, PR730, PR744, and later echo work study other + tree and scratch contracts. The present source reuse acts inside a leaf. + +The overlap check also read Chafik Boukhalfa's PR862, PR905, PR929, and PR951, +Gareth Davidson's PR877, Wentao Li's PR805, and Chafik Boukhalfa's new +PR977. PR977 improves the precision of the clean solver. Ross Richardson's +PR982 borrows outputs for a different fanout interface. These results supply different +precision or storage results. They are not implemented, benchmarked, or +combined by this package. Their inspected heads are recorded in CLAIM.json. + +No literature-priority, new kappa, selected-supplier, production-speed, +bit-reversible compiler, or complete multiplication theorem claim is made. diff --git a/research/dirty-stride-phases/vendor/pr985/PROOF.md b/research/dirty-stride-phases/vendor/pr985/PROOF.md new file mode 100644 index 0000000000..01a3da7347 --- /dev/null +++ b/research/dirty-stride-phases/vendor/pr985/PROOF.md @@ -0,0 +1,428 @@ +# A dirty source for the arbitrary-stride closure + +## Contract and limits + +Let `Z_L^w x` have entry `x_((i-w) mod L)`. Let `0 < beta <= 1/2`, +`|b| <= 1-beta`, and `u=2^-W`. The source `x` and target `y` are distinct +length-`L` arrays on the complex dyadic grid of spacing `u`. They can contain +arbitrary data. The coefficient `b` is one immutable rational complex number. Reduce the +stride modulo `L`. The bounds below use a residue with `O(log L)` bits; +reading an oversized stride descriptor is additional input work. + +The function `lift` adds an approximation to + + m (I-b Z_L^w)^-1 x + +to a cyclic shift of `y`. It restores `x` exactly. It needs no other data +array, no reserved zero bits, and only a constant number of clean complex +arithmetic registers. The recursion keeps integer indices and array views. +It does not keep a clean array of coefficients or closure values. + +Reversible block swaps implement the data operations on two sequential +tapes. No blank data array or coefficient table is used. The source and +target occupy one tape each during a leaf. The complete kernel routes its +borrowed arrays over the same two tapes, with all movement charged below. +The optional output shift is zero or the leaf stride; these are the two +cases required by the kernel factors. The construction does not implement +the variable-coefficient case of PR846's Theorem 1. + +Let `K` be the number of non-base Euclidean levels. Assume + + 48 (K+1) u <= beta^3. + +If `|x_i| <= B`, the unscaled target increment differs from the inverse by +at most + + 64 (B+1) u / beta^5. + +A multiplier of modulus at most `M`, with `M>=1`, changes this bound to + + (64 M (B+1) / beta^5 + 3) u. + +The rounded increment can depend on the target's initial value within this +error bound. A negative call executes the exact inverse word. It restores +the completed positive call, including all source and target data. + +## Source reuse + +As in Rohan Guliani's PR846, normalize the stride and reverse the index views +when necessary. Then `0 < w <= L/2`. Split the source into chains with +indices `c, c+w, c+2w, ...`. Apply the causal integer lifts + + x_i += rnd(a_i x_(i-w)), i=w,...,L-1. + +Call the resulting source `z`. Each lift has an exact inverse on the grid: +subtract the same rounded product in reverse order. Add `z` to the target +before using any source entries as temporary storage. + +The last `w` source entries contain the closure right-hand side. The first +`w` source entries are disjoint from that tail. Use this prefix as a dirty +target for the recursive closure. It contains arbitrary values; it is not +cleared. Let `F` be the completed rounded closure call. Let `H` be the +linear chain expansion. A reversible rounded conjugation implements the +additive `H` call, as specified below. +Execute + + F(tail, prefix) + H_add(prefix, y) + F_inverse(tail, prefix) + H_add_inverse(prefix, y) + +Then undo the original causal lifts. There are two recursive calls. + +The recursive call restores its input tail. The expansion preserves the +whole source, including the changed prefix and the tail. Thus `F_inverse` +sees precisely the state left by `F` and restores the prefix exactly. +Target independence and rounded linearity are not required. The two +expansion errors are charged separately. At every depth the prefix and +tail are disjoint because `2w <= L`. This proves restoration by induction. + +The negative leaf reverses the complete middle word: first the positive +expansion, then `F`, then the inverse expansion, then `F_inverse`, then the +negative baseline addition. It is not the positive word with all signs +changed in place. + +In exact arithmetic the source lifts give the chain decomposition +`S x = z + H S_child z_tail`. The four instructions above add precisely the +second term. This is the usual dirty commutator, with its connector taken +from the source prefix. PR628 supplies the dirty commutator and exact grid +lift methods; PR846 supplies the chain/closure decomposition. + +## Reversible transport on two dirty tapes + +Write `C` for the causal map whose non-start coefficient is `a`. Split the +source and carrier views into consecutive blocks of at most `w` records. +The carrier has arbitrary contents. For each block in forward order: + +1. For each position after the first block, add the rounded product of `a` + and the preceding block's value on the carrier tape to the source. +2. Swap this whole source block with its corresponding carrier block. + +At this point the source tape holds the original carrier, and the carrier +tape holds `C_round(source)`. Swap the two complete views. The causal map +has been applied, and the carrier has been restored exactly. Each block +scan and each rewind costs its block length. There is no length-`w` clean +queue. The old carrier data remains in the other tape throughout. + +For the inverse, first swap the complete views. Visit the blocks in reverse +order. Swap the current block back, then subtract its rounded predecessor +products. The predecessor block is still on the carrier tape. Reverse the +order within each block as well. This is the exact inverse grid word. +Each map costs at most `64n` data-record moves on views of length `n`, +including read/write charges, block rewinds and full-view swaps. This loose +bound also covers a cyclic view that crosses the root tape boundary once. + +An expansion uses this causal map on the **target**, with the source as +its dirty carrier. Apply `C_round_inverse` to the target, add +`rnd(m*b_start*prefix_i)` to its first `w` entries, then apply `C_round`. +The source is restored by each transport pass and is unchanged at the +injection. The negative expansion changes only the injection sign. It is +the exact inverse of the positive expansion. + +The closure source and its dirty prefix initially lie on the same tape. +Swap the source prefix with the first `w` records of the other tape. Run +the child on the source tail and this moved prefix, then swap back. The +outer target's displaced data is never read by the child and is restored +exactly. Both child views are now on distinct tapes. Their physical spans +are contiguous. At the root an output shift of zero or the leaf stride +ensures that the moved prefix does not cross the tape boundary. All later +views are reversals or subintervals of these contiguous views. + +## Two coefficients per level + +No length-dependent clean coefficient table is required. Put + + g = gcd(L0,w0), M = L0/g, v = (w0/g)^-1 modulo M. + +For `M=1`, all cycles have length one and no modular inverse is required. +At a recursive level the remaining original indices form an interval, +with orientation `s` equal to `+1` or `-1`. Its length and stride are `n,d`. +The displacement to a predecessor is `s*d` when `i>=d`, and `s*(d-n)` +otherwise. The number of original edges is the unique integer in `[1,M]` +congruent to + + (displacement/g) v modulo M. + +The induced edge stops at the first remaining vertex. It cannot complete +an extra original cycle first. Thus these residues are the actual return +times, not only congruence classes. At a base level each vertex has returned +to itself, so its exponent is `M`. There are only two possible coefficients +per level, both powers of the original `b`. + +The checker independently forms each new exponent by summing the old chain +exponents. It compares all resulting entries with this modular formula. +That finite comparison supports the all-length argument above. + +The implementation recomputes these two powers before each pass. Scalar +temporaries are held only inside `causal`, `expand`, and `diagonal`; they +are discarded before a recursive call. The recursion retains only views, +integer metadata, and references to the immutable root descriptor. + +## Rounded coefficient preparation + +`power` uses binary powering from the most significant bit. After each +product it truncates both components toward zero. A truncation has complex +error at most `2u` and cannot increase the norm. Hence the value prepared +for exponent `e` has norm at most `q^e`, where `q=|b|`. + +Expand the repeated squaring into a binary multiplication tree with `e` +leaves. A local error propagates through sibling products whose combined +norm is at most `q^(e-t)`, where that node contains `t` leaves. At most two +nodes have more than `floor(e/2)` leaves. All other internal nodes have at +least `ceil(e/2)` leaves outside them. Therefore the error is at most + + 2u [2 + e q^ceil(e/2)] <= 2u [2 + 2/beta] <= 8u/beta. + +Here `k q^k <= sum_(j=0)^(k-1) q^j <= 1/beta`. Exponents one and two +satisfy the same bound directly. The tree counts repeated operands with +their multiplicity; reuse of a scalar result does not remove its error. + +Let a chain contain `t` prepared coefficients. Each coefficient and its +exact counterpart has norm at most `q`. A telescoping product comparison +gives error at most + + (8u/beta) t q^(t-1) <= 8u/beta^2. + +Compare this chain product `pi` with the freshly prepared child coefficient. +They approximate the same original power. Their difference is at most + + eta = 12u/beta^2, + +since `8u/beta^2 + 8u/beta <= 12u/beta^2`. Every prepared coefficient has +margin at least `beta`. These statements include complex coefficients. + +## Error recurrence + +Consider the exact solution of the system with the prepared coefficients +at each level. Suppose its right-hand side satisfies + + |x_i| <= A (1-|a_i|). + +The shared-suffix identity used by Charles Bethin in PR764 bounds the exact +zero-seed chain value by `A(1-|pi|)`. The rounded causal pass adds at most +`u/beta`. Because the child coefficient differs from `pi` by at most `eta`, +the next weighted bound is + + A_next <= (1 + 12u/beta^3) A + u/beta^2. + +Start with `A0=B/beta`. The admission condition gives +`K*12u/beta^3 <= 1/4`. Thus `(1+12u/beta^3)^K < 2`, and at every level + + A <= Astar = 2(B/beta+1). + +The inverse of a system with coefficients of modulus at most `1-beta` +has infinity norm at most `1/beta`. Its stronger weighted estimate is: +if `|v_i| <= C(1-|a_i|)`, its solution has norm at most `C`. Both follow +from the absolutely convergent Neumann series and telescoping weights. + +Compare the exact child solution with the exact Schur solution. Their +right-hand sides differ by at most `u/beta`, and their coefficients differ +by at most `eta`. The Schur solution is a restriction of the parent solution +and has norm at most `Astar`. Their solution difference is at most + + Dstar = u/beta^2 + 12 Astar u/beta^3. + +The rounded inverse causal map differs from `C^-1` by at most `u` per +entry: each non-start entry subtracts one rounded product. The forward map +differs from `C` by at most `u/beta`. The seed injection adds at most `u` +error. Since `||C||<=1/beta`, the conjugated expansion differs from its +linear additive map by at most `3u/beta`, independently of both dirty +arrays. There are two expansions. The source pass contributes another +`u/beta`. Each chain prefix contains at +least one coefficient, so it contracts a child error by at most `1-beta`. +For the unscaled leaf error, + + e_k <= (1-beta) e_(k+1) + Dstar + 7u/beta, + e_K <= u. + +Summing the geometric series gives + + e_0 <= u + u/beta^3 + 12 Astar u/beta^4 + 7u/beta^2 + <= 64(B+1)u/beta^5. + +The root multiplier scales the baseline and each seed injection. The +injection rounding was already charged above. The baseline adds at most +one further `u`; a diagonal root adds at most one. Taking `M>=1` gives the +stated conservative bound with an additional `3u` allowance. + +## Complete arithmetic and storage recurrence + +Let `n_k` be the level lengths after orientation changes. Then + + n_k >= 2 n_(k+1) + n_(k+2). + +Indeed the next length is the normalized remainder, which is at most the +ordinary Euclidean remainder. Let `S(n,d)` be the sum of lengths over the +full binary recursion tree. It satisfies + + S(n,0)=n, + S(n,d)=n+2 S(d,(-n) mod d) <= 5n+2d <= 6n. + +The potential `5n+2d` proves the inequality directly using +`n>=2d+d_next`. Each non-base visit pays for six complete causal maps, +two seed injections, the baseline output, four closure transport swaps, +and both complete children. Each base visit pays for all divisions and +target additions. Validation scans and final head returns are also paid. +Reversal and slicing create index views; their physical accesses still pay +for every movement. + +Each visit prepares at most sixteen powers, each with `O(log M)` products. +This cost is also `O(L)`, although the constant is not optimized. From +`n_k>=5n_(k+2)`, a tree of depth `K` has `O(2^K)` nodes and +`2^K=O(L^log_5(4))`. Since `log_5(4)<1`, +`2^K log L=O(L)`. The Euclidean and modular-inverse setup uses integer +arithmetic on `O(log L)` bits. The implementation retains `O(log L)` +integer metadata words, or `O(log^2 L)` bits, with no data-sized values +on the recursion stack. Index arithmetic can be charged conservatively +with sequential counter updates. A block counter costs `O(w)` bit changes +over a block, including its `O(log(w+1))` reset. Integer setup costs +`O(log^3 L)` per visit, using a conservative schoolbook division bound. +The bound on `2^K` also gives `2^K log^3 L=O(L)`, so the total control cost +is `O(L)` bit operations in +the stated tape implementation. The rational reference uses Python +indices; it is not a timing implementation of this control bound. + +An explicit loose count is at most `1280L` scalar products and divisions, +including power preparation and a root multiplier. To see this, let `J` +be the number of tree visits. The direct count is at most +`9S + 32J bit_length(M) + 3L`. Since `4^8 <= 5^7`, the depth bound gives +`J <= 4 L^(7/8)`. Also `log2 L <= 8 L^(1/8)` for `L>=1`. It follows that +`J bit_length(M) <= 36L`, which proves the stated count. Mutable data +accesses are at most `71S+2L < 512L`, including both validation scans. +These constants are arithmetic bounds, not measured runtime claims. + +Thus one leaf uses `O(L)` rounded scalar operations, two data arrays, and +`O(1)` clean arithmetic registers, apart from scalar arithmetic workspace. +If both incoming arrays have norm at most `D`, internal values have +magnitude bounded by a polynomial in `(D+1)/beta`, independent of `L`. +The weighted bound gives `H=3(D+1)/beta` for causal source values at every +level. Under `a*u<=1` below, a completed child changes a prefix of this +size by at most `H/beta+(H+1)/2`. Thus the changed seed has norm at most +`10(D+1)/beta^2`. Each expansion target adds at most `M` times that seed +norm plus `3u/beta`. Inside its causal conjugation, the inverse pass has +norm at most twice its input plus `u`; the injection adds its seed term; +the forward pass divides this combined bound by at most `beta` and adds +`u/beta`. Apply these inequalities to both expansion calls and the baseline. +The loose bound `512(M+1)(D+1)/beta^7` covers every intermediate value, +including the displaced carrier data. At each recursive call its initial +target is a source prefix or the completed change to that prefix; no +unbounded sequence of target magnifications is assumed. The implementation +is an exact-rational reference with explicit +rounding; it is not a fast fixed-precision arithmetic compiler. + +## Products and paid precision + +For a certified kernel `Q(U)=r^-1 product_j(U-rho_j)`, use the same factor +maps as PR628 and PR846, with `U=tau Z_L^w` and constant `|tau|=1`. +For an outer root use coefficient `tau/rho` and multiplier `-1/rho`. +For an inner root use coefficient `rho*conj(tau)`, stride `-w`, multiplier +`conj(tau)`, and output shift `-w`. Include `r` in one multiplier. + +The implementation uses PR628's balanced four-call dirty commutator. +It requires `h=ceil(log2(r-1))` distinct arbitrary dirty arrays. The new +leaf needs no additional array. For `n` factors, the complete leaf count is + + N(1)=1, N(n)=2N(floor(n/2))+2N(ceil(n/2)) <= 4n^2. + +A negative composition reverses the order and signs of the four child +calls. Ancestor inputs and targets cannot be used as deeper scratch. +All source and borrowed data restore exactly. The final rounded increment +of a composition can depend on the initial borrowed values, as in PR628. + +For a simple sufficient bound retain PR628's full-word perturbation proof. +Put `a=68(r+1)/beta^5`, `G=2+r/beta`, and let every initial array have norm +at most `D`. If `a*u<=1`, then the execution error is at most + + N a (D+1) u G^(N-1). + +Choose `W` at least the incoming grid precision, the admission budget, and + + p+1 + ceil(log2(N a (D+1))) + (N-1) ceil(log2 G). + +This pays the execution error to `2^(-p-1)`. The pinned factor certificate +pays the remaining error to `2^(-p-1)` after scaling by the source norm. +For general input norm `X`, coefficient preparation must use target +`p+ceil(log2(max(1,X)))`. The supplied fixtures have ample certified margin; +their scaled perturbation is checked exactly, not assumed. + +With PR628's inherited `log2(1/beta)=O(r^3)`, this conservative choice is +`O(p+incoming_bits+log(D+1)+r^5+log(log L+2))` fractional bits. Integer +magnitude bits have the same order. An explicit safe integer reserve is + + ceil(log2(D+1)) + N ceil(log2 G) + + ceil(log2(512(r+1)/beta^7)) + 3. + +This note does not claim a precision improvement. Gareth Davidson's PR877 +and Chafik Boukhalfa's PR905 give stronger prefix bounds for the predecessor +dispatcher. Their cubic or quartic conclusions are not imported without a +separate check of the new leaf contract. + +## Complete tape and preparation bill + +The meter maps every mutable array to one of **two** physical tapes and +an absolute tape offset. It charges the distance from the previous head +position plus one unit for each read or write. It counts transport swaps, +validation, source restoration, and explicit final head returns. It does +not give each borrowed array a free tape head. + +One non-base visit costs at most `640n` record moves, apart from its two +children. Six causal maps cost at most `384n`. Baseline and seed scans cost +at most `24n`. The closure swaps and travel into and out of the child spans +cost at most `32n`. These total less than `640n`. The loose allowance also +covers the root cyclic view and entry positioning. A base visit costs at +most `8n`. Since `S<=6L`, validation and head returns leave the complete +leaf below **`4096L` data-record moves**. This is a proof bound, not a claim +that its constant is sharp. + +For a full kernel with `h>=1`, place the last borrowed array on tape B. +Place the source, target, and other borrowed arrays consecutively on tape +A. If a leaf's two arrays are both on A, swap its target with the array on +B, execute the leaf, and swap back. The B array is distinct from both +operands in this case. Its contents never enter the leaf calculation and +are restored exactly. If a leaf already uses both tapes, no such routing +is needed. For `h=0`, put the two arrays on separate tapes directly. + +This routing adds `O((h+2)L)` moves per leaf, including the distance between +array slots and returns to the tape origins. The full bound used by the +checker is `8192(N+1)(h+2)L` moves. It includes the initial validation scan. +No extra data array is allocated for transport. + +Let `W_total` include the fractional bits, integer reserve, and the bit +lengths of the immutable coefficient, gauge, and margin descriptors. The generic +rational API does not bound descriptor length from coefficient magnitude. +Let `M(W_total)` include the chosen rounded scalar multiplication and +division cost. With this complete scalar word size, the resulting bill is + + preparation + O(N L) M(W_total) + O(N(h+2)L W_total). + +Locating a factor on a sequential read-only descriptor tape costs at most +`O(r W_total)` per leaf, hence `O(r^3 W_total)` over the word. The original +factor and phase preparation charges remain inherited from PR628; this +descriptor access is included, not treated as free. Temporary powers, +source reads, multipliers, divisions, copies, inverse calls, and children +are all charged. The two data tapes, scalar arithmetic tapes, and metadata +stack use a fixed number of tapes. Borrowed data storage remains `hL` +complex words. Scalar arithmetic workspace has the declared word size; +the leaf index stack has `O(log^2 L)` bits. The balanced composition and +array routing retain another `O(log r (log r + log L))` metadata bits. +Their control cost is absorbed by the routing and descriptor terms, since +`log L=O(L)` and `log^2 r=O(r)`. These are metadata bits, not arithmetic +registers or data arrays. + +This is a constant-coefficient kernel construction. Variable site phases, +complete-transform composition and normalization, common-label/Clifford +compilation, physical supplier hosting, and the multiplication reduction +remain open. There is no new kappa, complex b, or BIT c claim. Finite replay +is not a formal proof of the full theorem or independent human review. + +Chafik Boukhalfa's concurrent PR951 gives two grouped additive calls with +no dirty connector in a neighboring-cycle layout. It uses a larger clean +scalar workspace. This note instead uses constant clean arithmetic storage +per first-order leaf, the original logarithmic dirty array budget, and +arbitrary-stride transport. It makes no claim to improve PR951's arithmetic +count or cubic precision. + +Chafik Boukhalfa's PR977 removes the length admission and proves cubic +precision for PR846 in its original clean scratch model. This construction +retains its stated admission and conservative precision. Combining those +precision arguments with the new dirty leaf requires a separate proof. diff --git a/research/dirty-stride-phases/vendor/pr985/README.md b/research/dirty-stride-phases/vendor/pr985/README.md new file mode 100644 index 0000000000..451ac2bac0 --- /dev/null +++ b/research/dirty-stride-phases/vendor/pr985/README.md @@ -0,0 +1,130 @@ +# Dirty cyclic inverse with source reuse + +**Status: research construction. No new kappa.** + +This is a follow-up to [PR846](https://github.com/CrocSwap/integer-mult-bounds/pull/846). +It implements an arbitrary-stride inverse for a **constant** stable complex +coefficient. It adds the inverse to a dirty target and restores the source +exactly, with no extra data array inside the leaf. The implementation also +composes the leaves into the certified kernels from PR628, with the same +`ceil(log2(r-1))` borrowed arrays as its original dirty dispatcher. + +The source prefix holds the recursive closure result temporarily. Two +opposite closure calls restore that prefix. Each closure input is the +disjoint source tail. The resulting recurrence has two children and total +weighted length at most `6L`. Coefficients at each level have only two +possible exponents, so they can be prepared in scalar storage. + +Reversible block swaps use the existing dirty target as a carrier. A +causal conjugation expands the closure values without a clean queue. +The construction uses `O(L)` rounded scalar operations, `O(L)` data-record +movement on **two tapes**, and `O(1)` clean arithmetic registers per leaf. +The leaf index stack uses `O(log^2 L)` bits. The full kernel retains the original +logarithmic number of borrowed arrays and routes all of them over the same +two tapes. Every swap, child, inverse call, and head return is charged. + +## Reproduce + +Use standard-library Python 3.11 or later from any working directory: + +```sh +python3 -I -O -B research/dirty-stride-source-reuse/verify.py +python3 -I -O -B research/dirty-stride-source-reuse/test_package.py +``` + +The first command compares every field with `EXPECTED.json`. It checks +8,256 stride geometries, 3,456 rounded generic leaves, and 80 original +kernel executions. All 3,456 leaf and 80 kernel executions have nonzero +rounding error. +The inputs, targets, and borrowed arrays all include an odd lowest working +bit. No clean low-bit storage is reserved. The second command checks +standalone use, exact regeneration, source and certificate corruption, and +faults in the arithmetic word. It runs two complete replays; the scoped CI +job uses this command on Python 3.11 and 3.14. + +Expected primary marker: + +```text +PASS_DIRTY_STRIDE_SOURCE_REUSE geometry=8256 generic=3456 kernels=80 controls=12 +``` + +To write a new receipt, use an output path that does not exist: + +```sh +python3 -I -O -B research/dirty-stride-source-reuse/verify.py --write /tmp/dirty-stride-replay.json +``` + +`PROOF.md` gives the all-length restoration, rounding, preparation, memory, +arithmetic, and tape arguments. `EXPECTED.json` is finite supporting evidence. +`VALIDATION.json` records the checks actually run. The exact-rational Python +implementation does not establish a measured fast-arithmetic runtime. + +## Evidence and scope + +- All lengths `1..128` and all residues `0..L-1` compare the return-time + formula with explicit chain elimination: 8,256 cases and 29,642 levels. +- 2,322 rounded powers check the norm and the uniform error bound through + exponent 129. This includes 2,178 cases with nonzero preparation error. +- Generic leaves cover lengths `1..24`, every integer stride in `[-L,L)`, + both allowed output shifts, and margins `1/2`, `1/16`, and `1/4096`. + A separate finite geometric sum + supplies the exact result. All source restoration and inverse checks pass. +- All ten pinned PR628 fixtures through radix 16 run at both unit gauges, + with zero, positive, and negative strides. A dense rational solve of the + expanded polynomial is the numerical oracle. Scaled factor perturbation, + 128-bit target accuracy, the full leaf count, dirty restoration, and exact + inverse cancellation are checked. +- An indexed bank rejects iteration and slicing inside the solver. The + arithmetic and data-access counters check the written complete recurrence. + The tape counter uses two physical heads, including when the kernel has + several borrowed arrays. It includes validation, transport, reads, writes, + restoration, and returns to the tape origins. + +For one leaf the sufficient error is `64(B+1) 2^-W / beta^5`, with admission +`48(K+1) 2^-W <= beta^3`. The complete kernel uses the conservative PR628 +perturbation argument with the new leaf constant. It does not claim the +stronger precision results of PR877 or PR905. + +The proof gives loose bounds of `1280L` counted products/divisions and +`4096L` data-record moves per leaf. The complete kernel pays +`O(NL) M(W_total) + O(N(h+2)L W_total)`, plus coefficient/phase preparation +and descriptor access, where `N<=4(r-1)^2` and `h=ceil(log2(r-1))`. +These are proved operation bounds, not measured runtime speedups. + +The rounded increment can depend on the initial target. The package has +a concrete length-three example. Inverse calls therefore reverse the +complete word; changing signs in the original order is not sufficient. +Variable site phases, complete-transform accounting, physical supplier +realization, and the multiplication reduction remain open. + +## Pins, selection, and credit + +Base: `47481c89fd30a43f8f882eb4b391e89c29273fd0`. +The selected conditional result at that base is PR890, +`kappa=1661957774647029/1000000000000000000`. At submission refresh, main +`407d52ff15b2217b6e22bce44728b4c3907b6515` selects PR942 at +`kappa=1661960547713947/1000000000000000000`. This package changes neither +certificate. `CLAIM.json` records both contexts. + +The exact source heads, paths, Git blobs, and SHA256 values are in +`SOURCE.json`. Retained files are unchanged; some are context documents, +not standalone copies of their original packages. The baseline PR846 +replay passed separately at head `4bdb3e755ea7118170a7a34764df955880dec282`. +No selected frontier or file under `upstream/` is changed. + +OS assignment seed **36** selected the complex supplier track. The user +then selected the remaining dirty-array solver in PR846 explicitly. +`CLAIM.json` records the three scoped candidates, the chosen mechanism, +the local claim, and the overlap check. This is a construction, not a search +for a better kappa or an optimal algorithm. + +Credit Rohan Guliani for PR846, Chafik Boukhalfa for PR628, Charles Bethin +for PR764, and the original PR621 and kernel lineage. The later PR862, +PR877, PR905, PR929, and concurrent PR951 results have different precision, +scalar storage, or neighboring-stride contracts. PR951 has two grouped +calls and no dirty connector, with larger clean scalar workspace. This +contribution makes no claim to improve that arithmetic count or its cubic +precision. PR977 improves PR846 to cubic precision and removes its length +admission, with the original clean scratch model. Its precision result is +not imported here. See `NOTICE.md` for attribution and the AI assistance +disclosure. diff --git a/research/dirty-stride-phases/vendor/pr985/dirty_stride.py b/research/dirty-stride-phases/vendor/pr985/dirty_stride.py new file mode 100644 index 0000000000..f469930b8b --- /dev/null +++ b/research/dirty-stride-phases/vendor/pr985/dirty_stride.py @@ -0,0 +1,407 @@ +"""Add a cyclic inverse to a target and restore the source exactly. + +This is a fixed-grid arithmetic model with two data tapes. Every data access +pays its head movement. See PROOF.md for the complete bill. +""" +from dataclasses import dataclass, field +from fractions import Fraction as F +from math import gcd + +ZERO = (F(0), F(0)) +ONE = (F(1), F(0)) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def add(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def sub(a, b): + return (a[0] - b[0], a[1] - b[1]) + + +def mul(a, b): + return (a[0]*b[0] - a[1]*b[1], a[0]*b[1] + a[1]*b[0]) + + +def norm2(a): + return a[0]*a[0] + a[1]*a[1] + + +def div(a, b): + d = norm2(b) + need(d != 0, 'zero divisor') + v = mul(a, (b[0], -b[1])) + return (v[0]/d, v[1]/d) + + +def rnd(a, bits): + """Use nearest dyadic rounding, with ties toward positive infinity.""" + scale = 1 << bits + def component(v): + t = v*scale + F(1, 2) + return F(t.numerator // t.denominator, scale) + return (component(a[0]), component(a[1])) + + +def trunc(a, bits): + """Truncate each component toward zero. This cannot increase the norm.""" + scale = 1 << bits + return tuple(F(int(v*scale), scale) for v in a) + + +@dataclass +class Meter: + reads: int = 0 + writes: int = 0 + tape_moves: int = 0 + products: int = 0 + power_products: int = 0 + divisions: int = 0 + nodes: int = 0 + leaves: int = 0 + validation_reads: int = 0 + max_depth: int = 0 + heads: dict = field(default_factory=dict) + layout: dict = field(default_factory=dict) + + def access(self, data, index, write=False): + tape, start = self.layout[id(data)] + position = start+index + self.tape_moves += abs(position - self.heads.get(tape, 0)) + 1 + self.heads[tape] = position + if write: + self.writes += 1 + else: + self.reads += 1 + + def rewind(self): + for tape, position in self.heads.items(): + self.tape_moves += position + self.heads[tape] = 0 + + +@dataclass(frozen=True) +class View: + data: list + start: int + step: int + length: int + meter: Meter + + def index(self, i): + need(0 <= i < self.length, 'view index') + return (self.start + self.step*i) % len(self.data) + + def get(self, i): + j = self.index(i) + self.meter.access(self.data, j) + return self.data[j] + + def put(self, i, value): + j = self.index(i) + self.meter.access(self.data, j, True) + self.data[j] = value + + def part(self, first, length): + need(0 <= first and first + length <= self.length, 'view interval') + return View(self.data, self.start + self.step*first, self.step, length, self.meter) + + def reverse(self): + return View(self.data, self.start + self.step*(self.length-1), + -self.step, self.length, self.meter) + + +def depth(length, stride): + count = 0 + while True: + stride %= length + stride = min(stride, length-stride) + if stride == 0: + return count + length, stride = stride, (-length) % stride + count += 1 + + +def admitted(beta, bits, levels): + return (type(bits) is int and bits >= 0 and 0 < beta <= F(1, 2) + and 48*(levels+1)*F(1, 1 << bits) <= beta**3) + + +def power(b, exponent, bits, meter): + """Use a left-to-right binary product and scalar working storage.""" + need(exponent >= 1, 'positive exponent') + result = b + for k in range(exponent.bit_length()-2, -1, -1): + result = trunc(mul(result, result), bits) + meter.power_products += 1 + if (exponent >> k) & 1: + result = trunc(mul(result, b), bits) + meter.power_products += 1 + return result + + +@dataclass(frozen=True) +class Geometry: + root: tuple + divisor: int + cycle: int + inverse: int + bits: int + meter: Meter + + def exponents(self, length, stride, orientation): + if stride == 0: + return (self.cycle, self.cycle) + def exponent(displacement): + need(displacement % self.divisor == 0, 'cycle lattice') + return ((displacement // self.divisor)*self.inverse) % self.cycle or self.cycle + return (exponent(orientation*stride), exponent(orientation*(stride-length))) + + def coefficients(self, length, stride, orientation): + a, b = self.exponents(length, stride, orientation) + left = power(self.root, a, self.bits, self.meter) + right = left if a == b else power(self.root, b, self.bits, self.meter) + return (left, right) + + +def emit(target, i, value, multiplier, sign, bits): + if multiplier != ONE: + target.meter.products += 1 + value = rnd(mul(multiplier, value), bits) + old = target.get(i) + target.put(i, add(old, value) if sign == 1 else sub(old, value)) + + +def swap(source, target): + for i in range(source.length): + left, right = source.get(i), target.get(i) + source.put(i, right) + target.put(i, left) + + +def causal(source, carrier, stride, geometry, undo=False): + """Apply the causal lifts with block swaps; restore the dirty carrier.""" + a, _ = geometry.coefficients(source.length, stride, source.step) + n = source.length + if undo: + swap(source, carrier) + for first in range(((n-1)//stride)*stride, -1, -stride): + size = min(stride, n-first) + swap(source.part(first, size), carrier.part(first, size)) + if first: + for i in range(first+size-1, first-1, -1): + value = rnd(mul(a, carrier.get(i-stride)), geometry.bits) + geometry.meter.products += 1 + source.put(i, sub(source.get(i), value)) + else: + for first in range(0, n, stride): + size = min(stride, n-first) + if first: + for i in range(first, first+size): + value = rnd(mul(a, carrier.get(i-stride)), geometry.bits) + geometry.meter.products += 1 + source.put(i, add(source.get(i), value)) + swap(source.part(first, size), carrier.part(first, size)) + swap(source, carrier) + + +def expand(source, target, stride, geometry, multiplier, sign): + """Conjugate the seed injection by exact inverse causal grid maps.""" + causal(target, source, stride, geometry, undo=True) + _, b = geometry.coefficients(source.length, stride, source.step) + coefficient = mul(multiplier, b) + geometry.meter.products += 1 + for i in range(stride): + value = rnd(mul(coefficient, source.get(i)), geometry.bits) + geometry.meter.products += 1 + emit(target, i, value, ONE, sign, geometry.bits) + causal(target, source, stride, geometry) + + +def closure(source, target, stride, geometry, sign, level): + """Move the child target to the other tape and restore the carrier.""" + borrowed = source.part(0, stride) + carrier = target.part(0, stride) + ends = source.part(source.length-stride, stride) + swap(borrowed, carrier) + solve(ends, carrier, (-source.length) % stride, geometry, sign=sign, level=level+1) + swap(borrowed, carrier) + + +def diagonal(source, target, geometry, multiplier, sign): + coefficient = power(geometry.root, geometry.cycle, geometry.bits, geometry.meter) + denominator = sub(ONE, coefficient) + for i in range(source.length): + value = rnd(div(source.get(i), denominator), geometry.bits) + geometry.meter.divisions += 1 + emit(target, i, value, multiplier, sign, geometry.bits) + + +def solve(source, target, stride, geometry, multiplier=ONE, sign=1, level=0): + """Use integer metadata at each level; scalar temporaries stay in helpers.""" + length = source.length + stride %= length + if 2*stride > length: + source, target, stride = source.reverse(), target.reverse(), length-stride + geometry.meter.nodes += 1 + geometry.meter.max_depth = max(geometry.meter.max_depth, level) + if stride == 0: + diagonal(source, target, geometry, multiplier, sign) + return + causal(source, target, stride, geometry) + if sign == 1: + for i in range(length): + emit(target, i, source.get(i), multiplier, 1, geometry.bits) + closure(source, target, stride, geometry, 1, level) + expand(source, target, stride, geometry, multiplier, 1) + closure(source, target, stride, geometry, -1, level) + expand(source, target, stride, geometry, multiplier, -1) + else: + expand(source, target, stride, geometry, multiplier, 1) + closure(source, target, stride, geometry, 1, level) + expand(source, target, stride, geometry, multiplier, -1) + closure(source, target, stride, geometry, -1, level) + for i in range(length): + emit(target, i, source.get(i), multiplier, -1, geometry.bits) + causal(source, target, stride, geometry, undo=True) + + +def lift(x, y, b, beta, bits, stride, sign=1, multiplier=ONE, shift=0, meter=None): + """Add multiplier*(I-b Z^stride)^-1 x at output indices i+shift.""" + need(type(stride) is int and type(shift) is int and type(sign) is int + and sign in (-1, 1), 'integer stride and sign') + need(x is not y and len(x) == len(y) and len(x) > 0, 'distinct equal arrays') + need(shift % len(x) in (0, stride % len(x)), 'output shift must be zero or the leaf stride') + need(isinstance(b, tuple) and len(b) == 2 and norm2(b) <= (1-beta)**2, 'stable constant coefficient') + need(isinstance(multiplier, tuple) and len(multiplier) == 2, 'constant multiplier') + need(admitted(beta, bits, depth(len(x), stride)), 'precision admission') + meter = meter if meter is not None else Meter() + if not meter.layout: + meter.layout = {id(x): (0, 0), id(y): (1, 0)} + need(id(x) in meter.layout and id(y) in meter.layout + and {meter.layout[id(x)][0], meter.layout[id(y)][0]} == {0, 1}, 'two distinct data tapes') + for data in (x, y): + for i in range(len(data)): + meter.access(data, i) + meter.validation_reads += 1 + need(rnd(data[i], bits) == data[i], 'fixed grid data') + divisor = gcd(len(x), stride) + cycle = len(x)//divisor + inverse = pow((stride//divisor) % cycle, -1, cycle) if cycle > 1 else 0 + geometry = Geometry(b, divisor, cycle, inverse, bits, meter) + solve(View(x, 0, 1, len(x), meter), View(y, shift, 1, len(y), meter), + stride, geometry, multiplier, sign) + meter.leaves += 1 + meter.rewind() + return meter + + +def leaf_bound(bound, beta, bits, multiplier_bound=1): + return (64*multiplier_bound*(bound+1)/beta**5 + 3)*F(1, 1 << bits) + + +def leaf_calls(count): + need(type(count) is int and count >= 1, 'positive factor count') + if count == 1: + return 1 + return 2*leaf_calls(count//2) + 2*leaf_calls(count-count//2) + + +def compose(x, y, factors, scratch, tau, beta, bits, stride, sign=1, meter=None): + """Use PR628's balanced dirty commutator with the new arbitrary-stride leaf.""" + need(factors and len(scratch) >= (len(factors)-1).bit_length(), 'dirty depth') + arrays = [x, y] + scratch + need(len({id(a) for a in arrays}) == len(arrays), 'all arrays distinct') + need(len(x) > 0 and all(len(a) == len(x) for a in arrays), 'array lengths') + need(isinstance(tau, tuple) and norm2(tau) == 1, 'immutable unit gauge') + need(type(sign) is int and sign in (-1, 1) and type(stride) is int, 'integer stride and sign') + need(admitted(beta, bits, depth(len(x), stride)), 'precision admission') + for factor in factors: + need(isinstance(factor, tuple) and len(factor) == 3, 'factor descriptor') + inside, b, scale = factor + need(type(inside) is bool and isinstance(b, tuple) and len(b) == 2 + and norm2(b) <= (1-beta)**2 and isinstance(scale, (int, F)), 'stable factor descriptor') + meter = meter if meter is not None else Meter() + if scratch: + layout = {id(a): (0, i*len(x)) for i, a in enumerate(arrays[:-1])} + layout[id(scratch[-1])] = (1, 0) + else: + layout = {id(x): (0, 0), id(y): (1, 0)} + need(not meter.layout or meter.layout == layout, 'kernel tape layout') + meter.layout = layout + for data in arrays: + for i in range(len(data)): + meter.access(data, i) + meter.validation_reads += 1 + need(rnd(data[i], bits) == data[i], 'fixed grid data') + def run(src, dst, lo, hi, level, direction): + if hi-lo == 1: + inside, b, scale = factors[lo] + phase = (tau[0], -tau[1]) if inside else tau + coefficient = mul(b, phase) + m = phase if inside else (-b[0], -b[1]) + m = (m[0]*scale, m[1]*scale) + if meter.layout[id(src)][0] == meter.layout[id(dst)][0]: + spare = scratch[-1] + destination = View(dst, 0, 1, len(dst), meter) + carrier = View(spare, 0, 1, len(spare), meter) + swap(destination, carrier) + lift(src, spare, coefficient, beta, bits, -stride if inside else stride, + direction, m, -stride if inside else 0, meter) + swap(destination, carrier) + else: + lift(src, dst, coefficient, beta, bits, -stride if inside else stride, + direction, m, -stride if inside else 0, meter) + return + mid = (lo+hi)//2 + z = scratch[level] + if direction == 1: + run(src, z, lo, mid, level+1, 1) + run(z, dst, mid, hi, level+1, 1) + run(src, z, lo, mid, level+1, -1) + run(z, dst, mid, hi, level+1, -1) + else: + run(z, dst, mid, hi, level+1, 1) + run(src, z, lo, mid, level+1, 1) + run(z, dst, mid, hi, level+1, -1) + run(src, z, lo, mid, level+1, -1) + run(x, y, 0, len(factors), 0, sign) + meter.rewind() + return meter + + +def ceil_log2(value): + value = F(value) + need(value > 0, 'positive logarithm') + k = value.numerator.bit_length() - value.denominator.bit_length() + power_of_two = F(2)**k + return k if value <= power_of_two else k+1 + + +def execution_bound(count, r, beta, initial_bound, bits): + need(r >= 1 and initial_bound >= 0 and 0 < beta <= F(1, 2) + and type(bits) is int and bits >= 0, 'execution budget domain') + calls = leaf_calls(count) + a = 68*(r+1)/beta**5 + growth = 2+F(r)/beta + need(a*F(1, 1 << bits) <= 1, 'execution precision') + return calls*a*(initial_bound+1)*F(1, 1 << bits)*growth**(calls-1) + + +def working_bits(count, r, beta, initial_bound, target_bits, incoming_bits, length, stride): + need(r >= 1 and initial_bound >= 0 and 0 < beta <= F(1, 2) + and type(target_bits) is int and target_bits >= 0 + and type(incoming_bits) is int and incoming_bits >= 0 + and type(length) is int and length > 0 and type(stride) is int, 'working budget domain') + calls = leaf_calls(count) + a = 68*(r+1)/beta**5 + growth = 2+F(r)/beta + levels = depth(length, stride) + return max(incoming_bits, target_bits+1+ceil_log2(calls*a*(initial_bound+1)) + +(calls-1)*ceil_log2(growth), ceil_log2(a), + ceil_log2(48*(levels+1)/beta**3)) diff --git a/research/dirty-stride-phases/verify.py b/research/dirty-stride-phases/verify.py new file mode 100644 index 0000000000..a3ed2ebf4d --- /dev/null +++ b/research/dirty-stride-phases/verify.py @@ -0,0 +1,397 @@ +"""Check the phased dirty operator against independent rational intervals.""" +import argparse +from fractions import Fraction as F +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent + + +def load(path, name): + 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 + + +c = load(HERE/'chirp.py', 'checked_chirp') +o = load(HERE/'oracle.py', 'phase_oracle') + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')) + + +class Bus: + def __init__(self): + self.heads = {0: 0, 1: 0} + self.minimum_moves = 0 + self.reads = self.writes = 0 + + def access(self, tape, position, write): + self.minimum_moves += abs(position-self.heads[tape])+1 + self.heads[tape] = position + if write: + self.writes += 1 + else: + self.reads += 1 + + +class Bank: + """Refuse data copies and slices. Measure the largest stored value.""" + def __init__(self, values, bus=None, tape=0, offset=0): + self.bus, self.tape, self.offset = bus, tape, offset + self.values = list(values) + self.peak = max(abs(a)+abs(b) for a, b in self.values) + + def __len__(self): + return len(self.values) + + def __getitem__(self, index): + need(type(index) is int, 'array slices are not allowed') + if self.bus is not None: + self.bus.access(self.tape, self.offset+index, False) + return self.values[index] + + def __setitem__(self, index, value): + need(type(index) is int, 'array slices are not allowed') + if self.bus is not None: + self.bus.access(self.tape, self.offset+index, True) + self.values[index] = value + self.peak = max(self.peak, abs(value[0])+abs(value[1])) + + def __iter__(self): + raise ValueError('array copies are not allowed') + + +def data(length, bits, salt=0, dirt=0): + unit = F(1, 1 << bits) + return [(F((7*i+salt) % 19-9, 8)+dirt+unit, + F((11*i+salt) % 17-8, 16)-dirt+3*unit) for i in range(length)] + + +def digest(arrays): + return hashlib.sha256(canonical([[[str(a), str(b)] for a, b in array] for array in arrays]).encode()).hexdigest() + + +def pins(): + sources = json.loads((HERE/'SOURCE.json').read_text()) + for row in sources['sources']: + value = (HERE/row['local']).read_bytes() + need(hashlib.sha256(value).hexdigest() == row['sha256'], 'source SHA256: '+row['local']) + need(hashlib.sha1(b'blob '+str(len(value)).encode()+b'\0'+value).hexdigest() + == row['blob'], 'source Git blob: '+row['local']) + return len(sources['sources']) + + +def check_phase_case(module, modulus, residue, bits, value): + meter = module.Meter() + plan = module.Phase.prepare(1, modulus, bits, meter) + coefficients = plan.coefficients(residue) + quadrant, tangent, sine = coefficients + ideal = o.phase(residue, modulus, 1, bits+96) + real, imag = ideal + reduced = ((real, imag), (imag, o.neg(real)), + (o.neg(real), o.neg(imag)), (o.neg(imag), real))[quadrant] + need(reduced[0][0] >= F(1, 2), 'phase quadrant') + denominator = o.plus(o.point(1), reduced[0], bits+96) + ratio = [v/w for v in reduced[1] for w in denominator] + tangent_error = max(abs(tangent-min(ratio)), abs(tangent-max(ratio))) + sine_error = max(abs(sine-reduced[1][0]), abs(sine-reduced[1][1])) + need(tangent_error <= F(1, 1 << (bits+8)) and sine_error <= F(1, 1 << (bits+8)), + 'phase coefficient accuracy') + rotated = module.rotate(value, coefficients, bits) + exact = o.complex_mul(ideal, o.complex_point(value), bits+96) + bound = 4*(abs(value[0])+abs(value[1])+1)*F(1, 1 << bits) + need(o.squared_distance_bound(rotated, exact) <= bound*bound, 'rotation accuracy') + need(module.rotate(rotated, coefficients, bits, True) == value, 'rotation exact inverse') + inverse_rotated = module.rotate(value, coefficients, bits, True) + exact_inverse = o.complex_mul((ideal[0], o.neg(ideal[1])), o.complex_point(value), bits+96) + need(o.squared_distance_bound(inverse_rotated, exact_inverse) <= bound*bound, 'inverse rotation accuracy') + need(module.rotate(inverse_rotated, coefficients, bits) == value, 'rotation reverse cancellation') + return digest([[rotated, inverse_rotated]]) + + +def phase_check(module=c): + cases = 0 + result = hashlib.sha256() + for bits in (2, 17, 64): + unit = F(1, 1 << bits) + for modulus in range(1, 25): + for residue in range(modulus): + value = (F(17, 4)+unit, -F(33, 8)+3*unit) + if residue % 3 == 1: + value = (2**60+unit, -2**48+3*unit) + result.update(check_phase_case(module, modulus, residue, bits, value).encode()) + cases += 1 + for modulus in (2**80, 2**80+7): + for residue in (1, modulus//8, modulus//4-1, modulus//2+1, modulus-1): + result.update(check_phase_case(module, modulus, residue, 96, (F(1, 8), F(-11, 16))).encode()) + cases += 1 + return dict(cases=cases, small_moduli=[1, 24], coefficient_bits=[10, 25, 72, 104], + wide_modulus_bits=81, output_digest=result.hexdigest()) + + +def check_leaf_case(module, length, stride, numerator, modulus, dirt=0, shift=0, + sign=1, beta=F(1, 4), target_bits=32): + multiplier = (F(3, 5), F(-4, 5)) + bits = module.working_bits(target_bits, 4, 2*abs(dirt)+8, beta, length, stride, + multiplier_bound=F(7, 5)) + x0 = data(length, bits, 2) + y0 = data(length, bits, 9, dirt) + bus = Bus() + x, y = Bank(x0, bus, 0), Bank(y0, bus, 1) + result = module.lift(x, y, (F(3, 10), F(2, 5)), beta, bits, stride, numerator, modulus, + sign, multiplier, shift) + need(x.values == x0, 'leaf source restoration') + need(result.reads == bus.reads and result.writes == bus.writes, 'paid data accesses') + need(result.tape_moves >= bus.minimum_moves, 'minimum physical tape movement') + need(result.phase_passes == 4 and result.phase_evaluations == 4*length + and result.phase_recurrence_steps == 4*length, 'four complete phase passes') + need(result.input_reads == 2*length, 'paid input scan') + need(result.tape_moves <= 4160*length and result.phase_record_moves <= 16*length, + 'phased leaf tape bill') + need(all(position == 0 for position in result.heads.values()) + and set(result.heads) == {0, 1}, 'two returned data heads') + need(result.phase_terms <= 2*result.internal_bits*(4*length+1) + and result.phase_products <= 4*result.internal_bits*(4*length+1) + and result.phase_divisions <= 2*result.internal_bits*(4*length+1), 'phase arithmetic bill') + need(result.error_bound <= F(1, 1 << (target_bits+1)), 'leaf precision choice') + ideal = o.leaf(x0, (F(3, 10), F(2, 5)), stride, numerator, modulus, bits+96, + multiplier, shift) + error = F(0) + nonzero = False + for i in range(length): + increment = (sign*(y.values[i][0]-y0[i][0]), sign*(y.values[i][1]-y0[i][1])) + error = max(error, o.squared_distance_bound(increment, ideal[i])) + nonzero |= not (ideal[i][0][0] <= increment[0] <= ideal[i][0][1] + and ideal[i][1][0] <= increment[1] <= ideal[i][1][1]) + need(error <= result.error_bound**2, 'phased leaf accuracy') + integer_bound = 16384*(F(7, 5)+1)*(result.initial_bound+1)/beta**7 + need(max(x.peak, y.peak, result.phase_peak_l1) <= 2*integer_bound, 'leaf integer reserve') + output = digest([y.values]) + module.lift(x, y, (F(3, 10), F(2, 5)), beta, bits, stride, numerator, modulus, + -sign, multiplier, shift) + need(x.values == x0 and y.values == y0, 'leaf complete-word inverse') + return dict(output=output, nonzero=nonzero, ratio=error/result.error_bound**2, + bits=bits, phase_terms=result.phase_terms, tape_moves=result.tape_moves) + + +def leaf_check(module=c): + count = nonzero = 0 + worst = F(0) + width = 0 + output = hashlib.sha256() + for length in range(1, 13): + for stride in sorted({0, 1, length//2, length-1, -1, -length//2}): + for numerator, modulus in ((-3, 2*length), (5, 2*length+1)): + for dirt in (0, 2**40): + shift = stride if dirt else 0 + result = check_leaf_case(module, length, stride, numerator, modulus, + dirt, shift, -1 if stride < 0 else 1) + count += 1 + nonzero += result['nonzero'] + worst = max(worst, result['ratio']) + width = max(width, result['bits']) + output.update(result['output'].encode()) + for length, stride, numerator, modulus in ((17, 7, -3, 34), (29, 12, -5, 58), + (11, -7, 2**96+9, 2**80+7)): + result = check_leaf_case(module, length, stride, numerator, modulus, 2**80, stride, + beta=F(1, 32), target_bits=64) + count += 1 + nonzero += result['nonzero'] + worst = max(worst, result['ratio']) + width = max(width, result['bits']) + output.update(result['output'].encode()) + need(nonzero == count, 'nonzero rounded leaf errors') + return dict(cases=count, nonzero_errors=nonzero, maximum_bits=width, + max_squared_error_ratio_log2_upper=c.d.ceil_log2(worst), output_digest=output.hexdigest()) + + +def check_kernel_case(module, count, length, stride, dirt=0): + beta = F(1, 4) + factors = [(i % 2 == 0, (F(1, 4), F((-1)**i, 8)), F(3 if i == 0 else 1)) for i in range(count)] + numerator, modulus = -3, 2*length + tau = F(3, 5), F(4, 5) + bits = module.working_bits(48, 4, 2*abs(dirt)+16, beta, length, stride, count=count, scale_bound=3) + x0, y0 = data(length, bits, 2), data(length, bits, 8, dirt) + scratch0 = [data(length, bits, 15+j, (-1)**j*dirt) for j in range((count-1).bit_length())] + bus = Bus() + originals = [x0, y0]+scratch0 + banks = [Bank(a, bus, 1 if i == len(originals)-1 else 0, + 0 if i == len(originals)-1 else i*length) for i, a in enumerate(originals)] + x, y, scratch = banks[0], banks[1], banks[2:] + result = module.compose(x, y, factors, scratch, tau, beta, bits, stride, numerator, modulus) + need(x.values == x0 and [a.values for a in scratch] == scratch0, 'kernel source and scratch restoration') + need(result.reads == bus.reads and result.writes == bus.writes, 'kernel paid data accesses') + need(result.tape_moves >= bus.minimum_moves, 'kernel minimum physical tape movement') + calls = c.d.leaf_calls(count) + need(result.leaves == calls, 'complete factor word') + need(result.phase_passes == 4 and result.phase_evaluations == 4*length, + 'four phase passes around the complete kernel') + need(set(result.heads) == {0, 1} and all(p == 0 for p in result.heads.values()), 'kernel data heads') + need(result.tape_moves <= 8256*(calls+1)*(len(scratch)+2)*length, 'kernel tape bill') + need(result.phase_terms <= 2*result.internal_bits*(4*length+1), 'kernel phase generation bill') + need(result.error_bound <= F(1, 1 << 49), 'kernel precision choice') + integer_bound = 16384*4*(result.initial_bound+1)*14**calls/beta**7 + need(max(result.phase_peak_l1, *(bank.peak for bank in banks)) <= 2*integer_bound, + 'kernel integer reserve including phase transients') + exact = o.kernel(x0, factors, tau, stride, numerator, modulus, bits+96) + error = max(o.squared_distance_bound((y.values[i][0]-y0[i][0], y.values[i][1]-y0[i][1]), exact[i]) + for i in range(length)) + need(error <= result.error_bound**2, 'phased kernel accuracy') + output = digest([y.values]) + module.compose(x, y, factors, scratch, tau, beta, bits, stride, numerator, modulus, -1) + need(x.values == x0 and y.values == y0 and [a.values for a in scratch] == scratch0, + 'kernel complete-word inverse') + return dict(count=count, length=length, stride=stride, dirt=str(dirt), bits=bits, + calls=calls, tape_moves=result.tape_moves, phase_terms=result.phase_terms, + output_digest=output) + + +def kernel_check(module=c): + return [check_kernel_case(module, count, length, stride, dirt) + for count in (1, 2, 3, 5, 8) + for length, stride, dirt in ((1, 0, 7), (5, 2, -13), (8, -3, 2**40), (17, 7, 2**80))] + + +def cost_check(module=c): + rows = [] + for length, stride in ((70, 29), (169, 70), (408, 169), (985, 408)): + bits = 48 + x0, y0 = data(length, bits, 4), data(length, bits, 15) + bus = Bus() + x, y = Bank(x0, bus, 0), Bank(y0, bus, 1) + result = module.lift(x, y, (F(0), F(0)), F(1, 2), bits, stride, -3, 2*length) + need(x.values == x0, 'large leaf source restoration') + need(result.reads == bus.reads and result.writes == bus.writes, 'large paid data accesses') + need(result.tape_moves >= bus.minimum_moves, 'large minimum physical tape movement') + need(result.tape_moves <= 4160*length, 'large leaf tape bound') + need(result.phase_evaluations == 4*length and result.phase_passes == 4, 'large leaf phase access') + module.lift(x, y, (F(0), F(0)), F(1, 2), bits, stride, -3, 2*length, -1) + need(x.values == x0 and y.values == y0, 'large leaf exact inverse') + rows.append(dict(length=length, stride=stride, tape_moves=result.tape_moves, + phase_terms=result.phase_terms, phase_peak_l1_log2_upper=c.d.ceil_log2(result.phase_peak_l1), + products=result.phase_products, + divisions=result.phase_divisions, recursion_depth=result.max_depth)) + return rows + + +def controls(module=c): + cases = [] + def rejected(name, call, arrays, original): + try: + call() + except ValueError as error: + expected = dict(zero_modulus='integer phase descriptor', boolean_numerator='integer phase descriptor', + aliased_arrays='distinct arrays', insufficient_precision='conjugation precision admission', + unstable_coefficient='stable coefficient', unsupported_shift='supported output shift', + invalid_sign='integer stride and sign', float_coefficient='stable coefficient') + need(str(error) == expected[name], 'wrong rejection: '+name+'; '+str(error)) + need(arrays == original, 'rejection changed data: '+name) + cases.append(name) + else: + raise ValueError('accepted invalid input: '+name) + x, y = data(5, 80), data(5, 80, 7) + original = [x[:], y[:]] + defaults = dict(x=x, y=y, b=(F(1, 4), F(0)), beta=F(1, 4), bits=80, stride=2, + numerator=-3, modulus=10) + for name, patch in (('zero_modulus', {'modulus':0}), ('boolean_numerator', {'numerator':True}), + ('aliased_arrays', {'y':x}), + ('unstable_coefficient', {'b':(F(1), F(0))}), ('unsupported_shift', {'shift':1}), + ('invalid_sign', {'sign':0}), ('float_coefficient', {'b':(0.25,0.0)})): + args = defaults | patch + rejected(name, lambda args=args: module.lift(**args), [x, y], original) + coarse_x = [(F(1), F(0))]*5 + coarse_y = [(F(2), F(0))]*5 + rejected('insufficient_precision', lambda: module.lift(coarse_x, coarse_y, (F(1, 4), F(0)), + F(1, 4), 14, 2, -3, 10), [coarse_x, coarse_y], [coarse_x[:], coarse_y[:]]) + # A unit source has a nonconstant response under the retained length-eight chirp. + source = [(F(i == 0), F(0)) for i in range(8)] + phased = o.leaf(source, (F(1, 2), F(0)), 3, -3, 16, 160) + plain = o.leaf(source, (F(1, 2), F(0)), 3, 0, 16, 160) + separation = max(max(F(0), phased[i][0][0]-plain[i][0][1], + plain[i][0][0]-phased[i][0][1]) for i in range(8)) + need(separation > F(1, 8), 'nonconstant phase witness') + return dict(rejections=cases, nonconstant_witness=dict(length=8, stride=3, numerator=-3, modulus=16, + real_separation_lower='1/8')) + + +def retained_kernel_check(module=c): + fixture = next(row for row in json.loads((HERE/'vendor/pr628/FACTORS.json').read_text()) + if row['radix'] == 4 and row['embedding'] == 1) + beta = F(fixture['beta']) + roots = [tuple(F(v) for v in z) for z in fixture['roots']] + factors = [] + approximate = [(F(1), F(0))] + for i, root in enumerate(roots): + inside = root[0]**2+root[1]**2 < 1 + b = root if inside else o.inverse(root) + need(b[0]**2+b[1]**2 <= (1-beta)**2, 'retained stable factor') + factors.append((inside, b, F(4 if i == 0 else 1))) + following = [(F(0), F(0)) for _ in range(len(approximate)+1)] + for j, value in enumerate(approximate): + v = o.rational_mul(root, value) + following[j] = following[j][0]-v[0], following[j][1]-v[1] + following[j+1] = following[j+1][0]+value[0], following[j+1][1]+value[1] + approximate = following + approximate = [(a/4, b/4) for a, b in approximate] + exact = [(F(1), F(0)), (F(1, 2), F(1, 2)), (F(1, 4), F(1, 4)), (F(1, 4), F(0))] + residual = sum(abs(a-c)+abs(b-d) for (a, b), (c, d) in zip(approximate, exact)) + inverse_bound = 4/beta**3 + need(inverse_bound*residual < 1, 'retained factor residual') + perturbation = inverse_bound**2*residual/(1-inverse_bound*residual) + rows = [] + for length, stride, dirt in ((5, 2, 7), (8, -3, 2**40)): + bits = module.working_bits(128, 4, 2*dirt+8, beta, length, stride, count=3, scale_bound=4) + initial = [data(length, bits, 3+7*j, dirt if j else 0) for j in range(4)] + banks = [Bank(a) for a in initial] + tau = F(3, 5), F(4, 5) + result = module.compose(banks[0], banks[1], factors, banks[2:], tau, beta, bits, stride, -3, 2*length) + need(banks[0].values == initial[0] and [a.values for a in banks[2:]] == initial[2:], + 'retained kernel restoration') + source_bound = max(abs(a)+abs(b) for a, b in initial[0]) + total = result.error_bound+perturbation*source_bound + need(total <= F(1, 1 << 128), 'retained kernel 128-bit budget') + ideal = o.polynomial(initial[0], exact, stride, -3, 2*length, bits+96, tau) + error = max(o.squared_distance_bound((banks[1].values[i][0]-initial[1][i][0], + banks[1].values[i][1]-initial[1][i][1]), ideal[i]) + for i in range(length)) + need(error <= total**2, 'retained dense polynomial accuracy') + output = digest([a.values for a in banks]) + module.compose(banks[0], banks[1], factors, banks[2:], tau, beta, bits, stride, -3, 2*length, -1) + need([a.values for a in banks] == initial, 'retained complete-word inverse') + rows.append(dict(radix=4, embedding=1, length=length, stride=stride, dirt=str(dirt), bits=bits, + total_bound_log2_upper=c.d.ceil_log2(total), output_digest=output)) + return dict(factor_residual_log2_upper=c.d.ceil_log2(residual), + inverse_perturbation_log2_upper=c.d.ceil_log2(perturbation), cases=rows) + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--write', type=Path) + args = parser.parse_args() + result = dict(schema=1, source_pins=pins(), phases=phase_check(), leaves=leaf_check(), + kernels=kernel_check(), retained_kernel=retained_kernel_check(), costs=cost_check(), controls=controls()) + encoded = json.dumps(result, indent=2, sort_keys=True)+'\n' + if args.write: + with args.write.open('x') as output: + output.write(encoded) + else: + need(canonical(result) == canonical(json.loads((HERE/'EXPECTED.json').read_text())), 'full typed receipt') + print('PASS_DIRTY_STRIDE_PHASES phases='+str(result['phases']['cases']) + +' leaves='+str(result['leaves']['cases'])+' kernels='+str(len(result['kernels'])) + +' retained='+str(len(result['retained_kernel']['cases']))+' costs='+str(len(result['costs']))+' input_controls='+str(len(result['controls']['rejections']))) + + +if __name__ == '__main__': + main()