From 4307d3a0cb8921b58ec2f229fdad41db25849932 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 00:51:16 +0000 Subject: [PATCH] feat(research): lower Horner oracle precision volume --- research/horner-increasing-precision/PROOF.md | 142 +++++++++++ .../horner-increasing-precision/README.md | 127 +++++++++ .../horner-increasing-precision/SOURCES.json | 24 ++ .../horner-increasing-precision/TASK.json | 105 ++++++++ .../horner-increasing-precision/VERIFY.json | 34 +++ .../horner-increasing-precision/verify.py | 240 ++++++++++++++++++ 6 files changed, 672 insertions(+) create mode 100644 research/horner-increasing-precision/PROOF.md create mode 100644 research/horner-increasing-precision/README.md create mode 100644 research/horner-increasing-precision/SOURCES.json create mode 100644 research/horner-increasing-precision/TASK.json create mode 100644 research/horner-increasing-precision/VERIFY.json create mode 100644 research/horner-increasing-precision/verify.py diff --git a/research/horner-increasing-precision/PROOF.md b/research/horner-increasing-precision/PROOF.md new file mode 100644 index 0000000000..568741d02e --- /dev/null +++ b/research/horner-increasing-precision/PROOF.md @@ -0,0 +1,142 @@ +# Increasing-precision fixed-source Horner evaluation + +This scoped written theorem and construction were produced by Nick Petalas. +The fixed-source inverse evaluator and disk-grid contract are Hanson Sun's +[PR1430](https://github.com/CrocSwap/integer-mult-bounds/pull/1430). +Variable-precision iteration, Horner evaluation and geometric error damping +are classical. The new step is the explicit schedule and precision-volume +improvement under that rounded-oracle interface. + +## Statement and changed premise + +Use the maximum complex-coordinate norm. Let E be a complex linear map with +norm at most c=21/50. Let D_q consist of complex vectors with coordinates in +2^-q Z[i] and norm at most one. For each integer q>=101, suppose an oracle +T_q:D_q -> D_q satisfies + + ||T_q(z)-Ez|| < (q/3) 2^-q, for every z in D_q. + +No linearity, homogeneity, oddness, consistency between precisions or +correlation of oracle errors is assumed. Supplying this whole oracle family +is an additional premise compared with access to only one fixed T_p. + +For any integer p>=102 and u in D_p, set + + q_j = max(101,j+3), j=0,...,p-1, + v_j = componentwise inward rounding of u/2 to grid 2^-q_j, + y_0 = v_0, + y_j = v_j - T_(q_j)(y_(j-1)), j=1,...,p-1. + w = componentwise inward rounding of y_(p-1) to grid 2^-p. + +Coarser dyadic values embed exactly in every finer grid. The subtraction +is exact on that grid. Every oracle input and every y_j belongs to D_(q_j). +The final output w belongs to D_p and obeys + + ||w - (I+E)^(-1)u/2|| + < [25(2p+13)/96 + 137/58] 2^-p + < p 2^-p. (1) + +The working computation uses two final guard bits; the last inward rounding +returns the original p-bit output format. Its error and work are charged. + +There are exactly p-1 complete oracle calls. The sum of their requested +precision parameters is exactly + + V(p) = sum_(j=1)^(p-1) q_j + = (p^2+5p)/2 + 4750 < p(p-1). (2) + +Thus the same p-term fixed-source evaluation can retain its published +p*2^-p error allowance with a strictly smaller oracle precision volume. +This is a deterministic instruction-parameter count, not a runtime +measurement or a complete bit-cost saving. It approaches half the fixed +p oracle volume as p tends to infinity. Optimality is not claimed. + +## Disk and grid invariants + +Inward componentwise rounding cannot increase the modulus, so ||v_j||<=1/2 +and ||v_j-u/2||=101, + + 1/2 + c + (q/3)2^-q < 1. + +It suffices to check q=101 because q*2^-q decreases. Induction gives +||y_j||<1 and grid membership at every iteration. Oracle outputs belong +to D_(q_j) by the supplied contract. Every subtraction is between two +values on that grid; the norm estimate bounds its result before it is +used again. No uncharged projection is used to repair the invariant. + +## Rounded error and inverse tail + +Set x_0=u/2 and x_j=u/2-E x_(j-1). Then + + x_(p-1) = (1/2) sum_(a=0)^(p-1) (-E)^a u. + +Writing d_j=||y_j-x_j||, the input rounding and oracle contract give + + d_0 < (3/2)2^-q_0, + d_j < c*d_(j-1) + (3/2+q_j/3)2^-q_j. + +Put Q=p+2. For d=p-1-j, q_j>=Q-d and q_j<=Q. Including the initial +error with the same larger coefficient gives + + d_(p-1) + < (3/2+Q/3) 2^-Q sum_(d=0)^(p-1) (2c)^d + < (3/2+Q/3) 2^-Q / (1-2c) + = 25(2p+13) 2^-p / 96. (3) + +This estimate allows arbitrary errors at each precision and every repeated +use of T_101. In particular it assumes no cancellation between calls. + +Since c<1/2, E^p has norm at most c^p<2^-p. The inverse exists by the +convergent Neumann series, and its omitted tail has norm less than + + 2^-p / (2(1-c)) = (25/29)2^-p. + +The final inward projection costs less than (3/2)2^-p and cannot increase +the norm, so w belongs to D_p. Adding (3), the inverse tail and this last +rounding proves the first inequality in (1), since 25/29+3/2=137/58. +The second is equivalent to 1334p>16001, which holds for all p>=102. + +## Exact precision count + +The p-1 calls have indices j=1,...,p-1. Relative to the baseline ramp +j+3, the floor at 101 adds + + sum_(j=1)^97 (98-j) = 97*98/2 = 4753. + +Also sum_(j=1)^(p-1)(j+3)=(p^2+5p)/2-3. This proves the equality in (2). +The baseline difference is + + p(p-1)-V(p) = (p^2-7p-9500)/2. + +It is 95 at p=102 and increases by p-3 on replacing p by p+1. This proves +strict improvement for every p>=102 without a finite extrapolation. +At p=128 the exact volumes are 16256 and 13262. At p=256 they are +65280 and 38158. These count requested precision bits across calls, +excluding the dimension multiplier and all implementation tariffs. + +## Wrapper and scope obligations + +The algorithm retains the original input u, the current state and one oracle +result. It prepares v_j at each iteration, rather than rounding u/2 once. +All those source roundings and source reads are additional explicit work. +Embedding a coarser numerator at a finer grid uses a shift, and subtraction +needs a sign/carry bit before the proved disk bound is applied. The largest +requested grid precision is p+2. In a sequential binary fraction layout, +preparation, embedding, subtraction and head returns use O(s*q_j) bit work +per iteration for s complex coordinates, plus O(sp) initial/final work, +including the charged final projection to the original p-bit grid. +This statement counts these wrapper operations; it does not provide a +source-bound multitape implementation or a favorable complete constant. + +No extra bank is provided free. Read buffers, oracle workspace, cleanup and +arbitrary productive dirty inputs need their actual caller contracts. +The norm proof alone does not authorize replacing precision in an emitted +native word. An actual Gaussian T_q family, its preparation/analytic error, +source streaming, grid conversions, final output use, stock, restoration and +the complete physical bill remain obligations. The five selected framework +assumptions and the selected frontier are unchanged. No new kappa, complete +multiplication theorem, human review or formal-kernel proof is claimed. diff --git a/research/horner-increasing-precision/README.md b/research/horner-increasing-precision/README.md new file mode 100644 index 0000000000..5a7f089a03 --- /dev/null +++ b/research/horner-increasing-precision/README.md @@ -0,0 +1,127 @@ +# Increasing precision lowers the Horner oracle volume + +For every integer p>=102, the fixed-source inverse evaluator can request +strictly fewer total oracle precision bits while retaining p-1 oracle calls, +a p-bit disk-grid output and error less than p*2^-p. This is a scoped written +proof with exact finite corroboration. + +This contribution was produced by Nick Petalas. Apache-2.0. + +Let ||E||<=21/50 in the maximum complex-coordinate norm. Assume access to +the rounded-E oracle of Hanson Sun's +[PR1430](https://github.com/CrocSwap/integer-mult-bounds/pull/1430) at every +integer precision q>=101, with error less than (q/3)2^-q on the whole disk +grid. This family is an explicit additional premise compared with a single +fixed-precision oracle. No consistency between its errors is needed. + +At iteration j=0,...,p-1 use q_j=max(101,j+3). Round the unchanged source +u/2 inward to each working grid and perform the fixed-source Horner update. +The last oracle uses precision p+2. A final charged inward rounding returns +the output to the original p-bit disk grid. [PROOF.md](PROOF.md) proves every +grid/disk invariant, source-rounding charge and inverse-tail bound. + +The exact sum over the p-1 oracle calls is + +```text +fixed precision: p(p-1) +increasing precision: (p^2+5p)/2 + 4750 +strict saving: (p^2-7p-9500)/2 > 0, for every p>=102 +``` + +The ratio approaches one half. At p=128 the counts are 16256 and 13262; +at p=256 they are 65280 and 38158. These are enumerated sums of requested +precision parameters, not runtime measurements, memory bounds, paid recursive +histograms or a complete supplier invoice. The work of repeatedly preparing +the source is explicitly additional. There is no new kappa or selected-frontier +change, and no optimality claim. + +## Evidence and reproduction + +The standalone verifier uses integer dyadic execution and a separate rational +real-block executor. Every reached prefix agrees. Exact rational elimination +of I+E supplies an independent final inverse. Its five rational complex +matrices have dimensions one through three and include a nonnormal case. +Six requested precisions are 102, 103, 128, 192, 256 and 512. Three oracle +modes include input-dependent signed local errors and ordinary inward rounding. + +The generated output reports 684 complete executions and 146718 oracle calls. +It checks the disk and grid conditions and the proved final error bound at +every applicable point. All 1947 integer precisions p=102,...,2048 have their +literal precision sums compared with the closed form and strict-saving test. +Eleven rejecting controls cover bad precision arguments, a frozen coarse +schedule, wrong update sign, missing source halving, decreasing grids, excess +oracle error and an invalid operator bound. All checks use explicit exceptions +and remain enabled under optimization. + +From the worktree root, standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/horner-increasing-precision/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/horner-increasing-precision/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/horner-increasing-precision +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/horner-increasing-precision --check-source-history +``` + +Other machines may substitute their CPython 3.12 path. Direct execution prints +a generated receipt with all six package-file SHA256 hashes and the exact +interpreter version, then PASS_HORNER_INCREASING_PRECISION. It writes no files +and needs neither Git nor external inputs. The registered commands run normal +and optimized checks. Source documents in SOURCES.json are provenance only; +no predecessor executable, scientific verifier or receipt is imported or replayed. +The universal conclusion rests on the written proof, not a finite census. + +## Scope, coordination and credit + +The original formal-interface-lemma card is explicitly changed to a written +precision-interface result. No proof-assistant formalization is claimed. +The selected-source orientation passed at canonical main +7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8, selected PR6030. +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363411) +records the target before substantive work. Live claims and reservations, +recent account PR bodies, open/merged searches and main README searches were +checked. Cached sparse local notes and unpublished work remain coverage limits. + +Hanson Sun / bbMisk's PR1430 supplies the fixed-source evaluator, its oracle +interface and the disk-invariant proof method. Its first Open next question +asks for a corrected actual Gaussian implementation. This is a new precision +schedule for that interface, not the missing backend or an audit of its result. +eumemic / PR5, icekylinx, the Harvey-van der Hoeven resampling lineage, +Artus Krohn-Grimberghe / PR371, Effy Elden / PR684 and Alan Grillo / PR902 +retain their source/interface/analytic credit. Ordinary Horner evaluation, +variable-precision iteration and contraction bounds are classical; global +literature priority is unclaimed. All predecessor files and credit are unchanged. + +The actual multi-precision Gaussian oracle, its preparation, source reads, +head returns, grid conversion, workspace cleanup, dirty restoration, native +legality, stock and complete physical cost remain obligations. The proof +does not discharge any of the five selected framework assumptions. No selected +cold replay, Lean, Docker, physical backend, independent human review or formal +proof-kernel review is claimed. + +## Open next questions + +Can a corrected actual Gaussian E family supply the requested oracles with a +favorable complete invoice? Begin with one implemented family, prove the same +disk/error contract at every q, and price its preparation together with all +repeated source roundings and the final p-bit projection. An actual backend +and source-compatible physical caller are the blockers. TASK.json records +the same question. No further precision optimization is undertaken here. + +## Verifier bounds + +The verifier has no external numeric input. Every matrix has at most three +complex coordinates, each registered execution has a fixed set of 684 cases, +and the independent arithmetic sweep has 1947 iterations with at most 2048 +precision entries each. Functions have at most 44 physical lines. The call +graph is nonrecursive, state is local, file reads are capped at 256 KiB, and +no subprocess, dynamic code generation or callback dispatch is used. + +Python's managed allocation is a deviation from fixed storage. Its scope is +this terminating bounded verifier: at most six scalar coordinates per state, +2048 precision entries, six bounded file reads and fixed-size elimination +matrices. Checks validate input/domain bounds and every disk/grid transition. +A fixed-storage implementation is required before using the verifier in a +runtime that forbids managed allocation. Warning-strict normal/optimized +execution and in-memory source compilation provide the local diagnostics. +External Python linters were unavailable locally; no broader static-analysis +or repository-wide analyzer configuration change is claimed. diff --git a/research/horner-increasing-precision/SOURCES.json b/research/horner-increasing-precision/SOURCES.json new file mode 100644 index 0000000000..5d1bd60e77 --- /dev/null +++ b/research/horner-increasing-precision/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/neumann-rounding-audit/README.md", + "usage": "provenance", + "git_blob": "6c6c0899fc00144c2ba97f1760ecd50a22ba6d57", + "sha256": "332a166718e3671b0db06c8cb73ca7673ee0224ac2645eea61972041d50a110e" + } + ] +} diff --git a/research/horner-increasing-precision/TASK.json b/research/horner-increasing-precision/TASK.json new file mode 100644 index 0000000000..34fb544142 --- /dev/null +++ b/research/horner-increasing-precision/TASK.json @@ -0,0 +1,105 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove an explicit increasing-precision fixed-source Horner schedule with the same p-bit output/error contract and fewer total requested oracle precision bits.", + "scope_change_reason": "The historical formalization card changes to an original written precision-interface theorem, with bounded exact corroboration; no proof assistant or supplier-assumption discharge is claimed.", + "bottleneck_link": "Precision/tape remains a selected framework assumption. This side result reduces an explicit inverse-evaluator oracle precision-volume bound under a changed multi-precision oracle contract, without claiming physical integration or a new kappa.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified schedule giving a strict precision-volume improvement, or post a concrete negative handoff within 60 minutes.", + "outcome": "completed", + "evidence": "PROOF.md supplies the quantified theorem; verify.py checks exact dyadic executions against a separate rational real-block executor and exact inverse, exact schedule arithmetic and rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a corrected actual Gaussian E implementation supply every T_q in this schedule with its full preparation, source-read and cleanup costs?", + "why_it_matters": "Only a complete oracle and wrapper invoice can turn the precision-volume improvement into a physical cost improvement.", + "first_step": "Bind one implemented E family to the PR1430 disk/error contract at every requested q, then price the repeated source roundings and final projection.", + "blocked_by": "The present package supplies an abstract oracle construction and proof, not the corrected physical Gaussian backend." + } + ], + "claim_type": "scoped written proof with exact finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363411", + "source_author": "bbMisk", + "source_pr": 1430, + "predecessor_author": "bbMisk", + "environment": { + "python": "CPython 3.12; exact version is emitted in the generated receipt", + "dependencies": "standard library", + "local_interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + } +} diff --git a/research/horner-increasing-precision/VERIFY.json b/research/horner-increasing-precision/VERIFY.json new file mode 100644 index 0000000000..6c4d90944a --- /dev/null +++ b/research/horner-increasing-precision/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact integer and rational-prefix agreement, inverse error, disk/grid invariants, precision volumes and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same explicit checks with assertions disabled." + } + ] +} diff --git a/research/horner-increasing-precision/verify.py b/research/horner-increasing-precision/verify.py new file mode 100644 index 0000000000..b2356eccf1 --- /dev/null +++ b/research/horner-increasing-precision/verify.py @@ -0,0 +1,240 @@ +"""Exact finite corroboration of the increasing-precision Horner theorem.""" + +from fractions import Fraction as F +from hashlib import sha256 +from pathlib import Path +import json +import platform + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def precisions(p): + require(type(p) is int and 102 <= p <= 2048, "precision domain") + return tuple(max(101, j + 3) for j in range(p)) + + +def trunc(value): + if value >= 0: + return value.numerator // value.denominator + return -((-value).numerator // value.denominator) + + +def rescale(n, old, new): + if new >= old: + return n << (new - old) + return (abs(n) >> (old - new)) * (1 if n >= 0 else -1) + + +def complex_norm_ok(values, bound): + return all(values[i] ** 2 + values[i + 1] ** 2 <= bound ** 2 + for i in range(0, len(values), 2)) + + +def block_matrix(rows): + d = len(rows) + require(1 <= d <= 3 and all(len(row) == d for row in rows), "matrix shape") + require(all(sum(abs(a) + abs(b) for a, b in row) <= F(21, 50) + for row in rows), "operator bound") + result = [[F(0) for _ in range(2 * d)] for _ in range(2 * d)] + for i, row in enumerate(rows): + for j, (a, b) in enumerate(row): + result[2 * i][2 * j] = a + result[2 * i][2 * j + 1] = -b + result[2 * i + 1][2 * j] = b + result[2 * i + 1][2 * j + 1] = a + return result + + +def inverse_shift(matrix): + n = len(matrix) + rows = [[matrix[i][j] + (i == j) for j in range(n)] + + [F(i == j) for j in range(n)] for i in range(n)] + for j in range(n): + pivot = next((i for i in range(j, n) if rows[i][j]), None) + require(pivot is not None, "singular inverse") + rows[j], rows[pivot] = rows[pivot], rows[j] + divisor = rows[j][j] + rows[j] = [x / divisor for x in rows[j]] + for i in range(n): + if i != j: + multiplier = rows[i][j] + rows[i] = [a - multiplier * b for a, b in zip(rows[i], rows[j])] + require(all(rows[i][j] == (i == j) for i in range(n) for j in range(n)), + "inverse left block") + result = [row[n:] for row in rows] + require(all(sum((matrix[i][k] + (i == k)) * result[k][j] for k in range(n)) + == (i == j) for i in range(n) for j in range(n)), "inverse product") + return result + + +def apply(matrix, vector): + return [sum(a * b for a, b in zip(row, vector)) for row in matrix] + + +def integer_oracle(rows, values, q, mode): + exact = [] + for row in rows: + real = sum(a * values[2 * j] - b * values[2 * j + 1] + for j, (a, b) in enumerate(row)) + imag = sum(b * values[2 * j] + a * values[2 * j + 1] + for j, (a, b) in enumerate(row)) + exact.extend((real, imag)) + result = [trunc(x) for x in exact] + for i in range(0, len(values), 2): + sign = (values[i] > 0) - (values[i] < 0) + result[i] += mode * (q // 4 - 2) * sign + errors = [a - b for a, b in zip(result, exact)] + require(all(errors[i] ** 2 + errors[i + 1] ** 2 < F(q, 3) ** 2 + for i in range(0, len(values), 2)), "oracle local error") + return result + + +def run_case(rows, u, p, mode, levels=None, update_sign=-1, halve=True): + levels = precisions(p) if levels is None else levels + require(len(levels) == p and all(101 <= q <= p + 2 for q in levels), + "precision schedule range") + require(all(a <= b for a, b in zip(levels, levels[1:])), "grid nesting") + matrix = block_matrix(rows) + reference = [F(x, 1 << (p + int(halve))) for x in u] + state = [rescale(x, p + int(halve), levels[0]) for x in u] + reference = [F(trunc(x * (1 << levels[0])), 1 << levels[0]) for x in reference] + require(complex_norm_ok(u, 1 << p), "input disk") + require(complex_norm_ok(state, 1 << levels[0]), "initial disk") + for j in range(1, p): + q = levels[j] + embedded = [rescale(x, levels[j - 1], q) for x in state] + require(complex_norm_ok(embedded, 1 << q), "oracle input disk") + image = integer_oracle(rows, embedded, q, mode) + source = [rescale(x, p + int(halve), q) for x in u] + state = [a + update_sign * b for a, b in zip(source, image)] + exact_image = apply(matrix, reference) + rounded = [F(trunc(x * (1 << q)), 1 << q) for x in exact_image] + for i in range(0, len(u), 2): + sign = (reference[i] > 0) - (reference[i] < 0) + rounded[i] += F(mode * (q // 4 - 2) * sign, 1 << q) + source_ref = [F(trunc(F(x, 1 << (p + int(halve))) * (1 << q)), 1 << q) + for x in u] + reference = [a + update_sign * b for a, b in zip(source_ref, rounded)] + require(reference == [F(x, 1 << q) for x in state], "prefix disagreement") + require(complex_norm_ok(state, 1 << q), "output disk") + require(complex_norm_ok(image, 1 << q), "oracle output disk") + final = [rescale(x, levels[-1], p) for x in state] + reference = [F(trunc(x * (1 << p)), 1 << p) for x in reference] + require(reference == [F(x, 1 << p) for x in final], "final projection") + require(complex_norm_ok(final, 1 << p), "final disk") + expected = apply(inverse_shift(matrix), [F(x, 1 << (p + 1)) for x in u]) + error = [a - b for a, b in zip(reference, expected)] + allowance = (F(25 * (2 * p + 13), 96) + F(137, 58)) / (1 << p) + require(allowance < F(p, 1 << p), "claimed allowance") + require(all(error[i] ** 2 + error[i + 1] ** 2 < allowance ** 2 + for i in range(0, len(u), 2)), "final inverse error") + return p - 1 + + +def fixtures(): + z = (F(0), F(0)) + return ( + (((F(21, 50), F(0)),),), + (((F(-21, 50), F(0)),),), + ((z, (F(1, 4), F(0))), ((F(1, 4), F(0)), z)), + ((z, (F(1, 5), F(1, 10))), ((F(-1, 10), F(1, 10)), z)), + (((F(1, 10), F(0)), (F(0), F(1, 5)), z), + (z, (F(-1, 10), F(0)), (F(3, 10), F(0))), + (z, z, (F(1, 5), F(0)))), + ) + + +def input_vectors(d, p): + scale = 1 << p + values = [[0] * (2 * d)] + for j in range(2 * d): + unit = [0] * (2 * d) + unit[j] = scale if j % 2 == 0 else -scale + values.append(unit) + values.append([n for _ in range(d) for n in (3 * scale // 5, 4 * scale // 5)]) + values.append([n for i in range(d) for n in ((-1) ** i * 112, 14)]) + values.append([n for i in range(d) for n in ((-1) ** i * (scale // 2 + 1), scale // 4)]) + return values + + +def proof_arithmetic(): + for p in range(102, 2049): + levels = precisions(p) + actual = sum(levels[1:]) + closed = (p * p + 5 * p) // 2 + 4750 + require(actual == closed < p * (p - 1), "precision volume") + require(F(25 * (2 * p + 13), 96) + F(137, 58) < p, "error allowance") + require(all(q >= p + 2 - (p - 1 - j) for j, q in enumerate(levels)), + "precision damping") + require(F(1, 2) + F(21, 50) + F(101, 3 * (1 << 101)) < 1, + "global disk slack") + require(F(21, 50) < F(1, 2) and 2 * F(21, 50) < 1, "tail and damping") + return 1947 + + +def controls(): + rejected = 0 + for bad in (101, 2049, True, F(102), "102"): + try: + precisions(bad) + except ValueError as error: + require(str(error) == "precision domain", "precision control reason") + rejected += 1 + else: + raise ValueError("bad precision accepted") + row = (((F(1, 4), F(0)),),) + u = [1 << 256, 0] + attempts = ( + ({"levels": (101,) * 256}, "final inverse error"), + ({"update_sign": 1}, "final inverse error"), + ({"halve": False}, "final inverse error"), + ({"levels": (102, 101) + precisions(256)[2:]}, "grid nesting"), + ({"mode": 1000}, "oracle local error"), + ) + for change, reason in attempts: + options = {"mode": 1, **change} + try: + run_case(row, u, 256, **options) + except ValueError as error: + require(str(error) == reason, "semantic control reason") + rejected += 1 + else: + raise ValueError("semantic control accepted") + try: + block_matrix((((F(1, 2), F(0)),),)) + except ValueError as error: + require(str(error) == "operator bound", "operator control reason") + rejected += 1 + else: + raise ValueError("expansive matrix accepted") + return rejected + + +def main(): + cases = calls = 0 + for rows in fixtures(): + for p in (102, 103, 128, 192, 256, 512): + for u in input_vectors(len(rows), p): + for mode in (-1, 0, 1): + calls += run_case(rows, u, p, mode) + cases += 1 + result = {"cases": cases, "oracle_calls": calls, + "precision_arithmetic_cases": proof_arithmetic(), "rejections": controls()} + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + path = package / name + require(path.stat().st_size <= 256 * 1024, "package file capacity") + hashes[name] = sha256(path.read_bytes()).hexdigest() + receipt = {"result": result, "python": platform.python_version(), "sha256": hashes} + print(json.dumps(receipt, sort_keys=True)) + print("PASS_HORNER_INCREASING_PRECISION", json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()