From f39e5c22b106be00ac16d89c19686b9c9853a0e1 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 00:02:59 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20check=20#4377's=20CRT=20evaluat?= =?UTF-8?q?or=20bound:=20arithmetic=20holds=20with=20~500x=20slack;=20per-?= =?UTF-8?q?axis=20bill=20tight=20(0.977)=20at=20m=20=3D=201;=20one=20non-l?= =?UTF-8?q?oad-bearing=20wire-tariff=20slip=20at=20ell=20=3D=201=20(no=20n?= =?UTF-8?q?ew=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../crt-evaluator-independent-check/README.md | 75 ++++++ .../SOURCES.json | 24 ++ .../crt-evaluator-independent-check/TASK.json | 74 ++++++ .../VERIFY.json | 20 ++ .../crt-evaluator-independent-check/verify.py | 235 ++++++++++++++++++ 5 files changed, 428 insertions(+) create mode 100644 research/crt-evaluator-independent-check/README.md create mode 100644 research/crt-evaluator-independent-check/SOURCES.json create mode 100644 research/crt-evaluator-independent-check/TASK.json create mode 100644 research/crt-evaluator-independent-check/VERIFY.json create mode 100644 research/crt-evaluator-independent-check/verify.py diff --git a/research/crt-evaluator-independent-check/README.md b/research/crt-evaluator-independent-check/README.md new file mode 100644 index 0000000000..5c70326168 --- /dev/null +++ b/research/crt-evaluator-independent-check/README.md @@ -0,0 +1,75 @@ +# Independent check of #4377's CRT evaluator bound + +**Claim type:** an independent exact re-derivation plus an instrumented operand-size check. **No +new κ.** It checks unpaidmoon's +[#4377](https://github.com/CrocSwap/integer-mult-bounds/pull/4377) (`PROOF.md`), which proves +`E(p, ℓ) ≤ 2^{4ℓ}(p+2)^{16}` with constant `C = 1` for #4100's sequential CRT and rotation-switch +evaluator. Nothing is imported from #4377. + +## Results + +**Part A: the arithmetic holds.** All of these were re-derived with exact integers: + +- the schoolbook and restoring-division tariffs, `8ab`, for `a, b ≤ 64`; +- the Euclid tariff `64b³`; +- the six cost terms; +- the bound `7·max ≤ B` and the sum bound `≤ B`, on `p = 2..200` and `ℓ = 1..40`; +- the guard amortization `2^{−G}E ≤ 2^{−60ℓ}(p+2)^{−48}`. + +The largest ratio of the six terms' sum to `B` is `1.96·10⁻³`, at `p = 2, ℓ = 1`. The closing +inequality has a factor of about 500 of slack. + +**Part B: the per-axis bill holds, tightly.** An instrumented copy of #4100's retained +`decode_group` and `balanced` offset step charges every multiplication, division, inverse and +addition at its **actual** operand bit lengths. It uses #4377's tariffs, with the quotient length +of each division. The source is `check_batched_crt.py`, pinned, and its result is compared with +the retained function's output. The check covers 653 axes: + +- groups with `W ≤ p` at `ℓ = 3..12`; +- long-moduli cases at `ℓ = 14..32`, with `m ∈ {1, 2, 4}` and a full right-child prefix. + +Every axis is within #4377's per-axis bill `128mW² + 128mℓ³ + 16mW`. The bill is nearly tight, +though. At `m = 1` the ratio rises steadily from 0.950 at `ℓ = 14` to 0.977 at `ℓ = 32`. The two +modular inverses, one in `decode_group` and one for the target, use the whole `2m·64ℓ³` inverse +budget. Any extra inverse in an implementation would exceed the per-axis bill. It would still +pass the closing inequality, given the factor-500 slack. + +**Part C: one non-load-bearing slip.** `PROOF.md` prices one rotation-table wire at +`9(ℓ+2)²`, as "one addition and one restoring division of integers of at most `ℓ + 2` bits". Its +own tariffs give `4(ℓ+2) + 8(ℓ+2)²`. That exceeds `9(ℓ+2)²` exactly when `ℓ = 1`, where it is +84 against 81. With the corrected step, the per-network bound `25(ℓ+2)²2^ℓ + 64ℓ2^{2ℓ}` still +holds for every `ℓ ≤ 40`, so nothing downstream changes. A one-line fix is to state the wire cost +as `4(ℓ+2) + 8(ℓ+2)² ≤ 12(ℓ+2)²`. A smaller fix uses the true quotient length of at most 3 bits. + +## Not covered + +- The tape model and the head-movement accounting of indexed scans. +- The Beneš scan recurrence, which is only re-derived here, as in #4377. +- Reservoir placement, sparse repair and the outer theorem. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/crt-evaluator-independent-check --check-only +python3.12 -B scripts/research_package.py --package research/crt-evaluator-independent-check +``` + +The verifier prints `PASS_CRT_EVALUATOR_INDEPENDENT_CHECK` in under a second, using only the +standard library. + +## Open next questions + +1. **Does any #4100 caller use more than `m + 1` modular inverses per axis?** + - *Why it matters:* the per-axis bill has almost no room left at `m = 1`. + - *First step:* trace the inverse macro's own offset computation, which #4377 prices as a + second pair of networks. + - *Blocked by:* nothing. + +## Credit + +The proof and its tariffs are unpaidmoon's (#4377). The CRT construction and the retained +`decode_group`/`balanced` code are Cinna Davis's (#4100). ToikY's #4192 is the predecessor Beneš +audit. + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/crt-evaluator-independent-check/SOURCES.json b/research/crt-evaluator-independent-check/SOURCES.json new file mode 100644 index 0000000000..143a7348be --- /dev/null +++ b/research/crt-evaluator-independent-check/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "usage": "input", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + } + ] +} diff --git a/research/crt-evaluator-independent-check/TASK.json b/research/crt-evaluator-independent-check/TASK.json new file mode 100644 index 0000000000..a9c42fa6d6 --- /dev/null +++ b/research/crt-evaluator-independent-check/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Independently check #4377's E(p,ell) <= 2^(4 ell)(p+2)^16 evaluator bound: exact re-derivation and actual-operand-size charging of the retained CRT code.", + "scope_change_reason": "The card asks for one quantified #4100 implication; #4377 supplies the uniform evaluator constant with no independent check.", + "bottleneck_link": "CRT.md section 4's guard amortization uses this evaluator bound.", + "budget_minutes": 30, + "stop_rule": "Stop at the arithmetic, the instrumented bill and the slip; do not model tapes.", + "outcome": "completed", + "evidence": "verify.py: master inequality holds with sum/B <= 1.96e-3 on p<=200, ell<=40; 653 instrumented axes within the per-axis bill (max 0.977, rising to 1 at m=1); per-wire 9(ell+2)^2 fails only at ell=1 (84>81), absorbed by the per-network bound.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "Does any #4100 caller use more than m+1 modular inverses per axis?", + "why_it_matters": "The per-axis bill has almost no room at m=1.", + "first_step": "Trace the inverse macro's offset computation.", + "blocked_by": "None." + } + ] +} diff --git a/research/crt-evaluator-independent-check/VERIFY.json b/research/crt-evaluator-independent-check/VERIFY.json new file mode 100644 index 0000000000..2f0b931f3f --- /dev/null +++ b/research/crt-evaluator-independent-check/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned retained decode_group/balanced lines; #4377 tariffs, six terms, master inequality and guard amortization on p=2..200, ell=1..40; instrumented operand-size charging of 653 CRT axes against the per-axis bill, offsets equal to the retained code; per-wire slip exactly at ell=1 and its absorption." + } + ] +} diff --git a/research/crt-evaluator-independent-check/verify.py b/research/crt-evaluator-independent-check/verify.py new file mode 100644 index 0000000000..31071b34bb --- /dev/null +++ b/research/crt-evaluator-independent-check/verify.py @@ -0,0 +1,235 @@ +#!/usr/bin/env python3 +"""Independent check of #4377's uniform CRT evaluator bound E(p, ell) <= 2^(4 ell) (p+2)^16. + +Part A #4377's tariff lemmas and closing inequality, re-derived with exact integers: schoolbook 8ab, + restoring division 8ab, Euclid 64 b^3, the six cost terms, the q = 4 maximum, the ell-step factors + and the guard amortization, on p = 2..200 and ell = 1..40. +Part B an instrumented copy of #4100's retained decode_group / balanced offset (check_batched_crt.py, + pinned) that charges every multiplication, division, inverse and addition with its ACTUAL operand bit + lengths under #4377's tariffs, on random CRT groups at the caller's sizes, compared with #4377's + per-axis bill 128 m W^2 + 128 m ell^3 + 16 m W. +Part C the per-wire table step: #4377 states 9(ell+2)^2, but its own add + division tariffs give + 4(ell+2) + 8(ell+2)^2, which exceeds 9(ell+2)^2 exactly at ell = 1 (84 > 81). The per-network bound + 25(ell+2)^2 2^ell + 64 ell 2^(2 ell) still holds with the corrected step, so the slip is not + load-bearing. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +import hashlib +import json +from pathlib import Path +import random +import sys + +ROOT = Path(__file__).resolve().parents[2] +SRC = ROOT / "research/unconditional-batched-crt/check_batched_crt.py" +RETAINED = [ + " complement = product // modulus\n residue = value * prefix % modulus\n" + " answer += residue * complement * pow(complement, -1, modulus)\n prefix *= modulus\n", + " offset = lower * pow(prefix, -1, moduli[i]) % moduli[i]\n", +] +rng = random.Random(4377) + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def bits(x): + return max(1, abs(x).bit_length()) + + +# ---- #4377 tariffs --------------------------------------------------------------------------- +def t_mul(a, b): + return 8 * bits(a) * bits(b) + + +def t_div(n, d): + """restoring division, quotient length = bit length of the quotient""" + return 8 * bits(n // d) * bits(d) + + +def t_inv(x, m): + """reduce x mod m (a division) then Euclid at 64 b^3, b = bits(m)""" + return t_div(x, m) + 64 * bits(m) ** 3 + + +def t_add(a, b): + return 4 * max(bits(a), bits(b)) + + +def charged_axis(residues, moduli, target, right_prefix): + """decode_group of the left group, then lower * (left product * right prefix)^-1 mod target""" + cost = 0 + product = 1 + for m in moduli: + if product != 1: + cost += t_mul(product, m) + product *= m + answer, prefix = 0, 1 + for value, m in zip(residues, moduli): + cost += t_div(product, m) + complement = product // m + cost += t_mul(value, prefix) + t_div(value * prefix, m) + residue = value * prefix % m + cost += t_inv(complement, m) + inv = pow(complement, -1, m) + cost += t_mul(residue, complement) + t_mul(residue * complement, inv) + term = residue * complement * inv + cost += t_add(answer, term) + answer += term + cost += t_mul(prefix, m) + prefix *= m + cost += t_div(answer, product) + lower = answer % product + full = product * right_prefix + cost += t_mul(product, right_prefix) + t_inv(full, target) + inv = pow(full, -1, target) + cost += t_mul(lower, inv) + t_div(lower * inv, target) + return cost, lower * inv % target + + +def odd_primes(lo, hi): + out = [] + for n in range(max(3, lo), hi): + if n % 2 and all(n % d for d in range(3, int(n ** 0.5) + 1, 2)): + out.append(n) + return out + + +def is_prime(n): + """deterministic Miller-Rabin for n < 3.3e24""" + if n < 2: + return False + small = (2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41) + if n in small: + return True + if any(n % a == 0 for a in small): + return False + d, r = n - 1, 0 + while d % 2 == 0: + d, r = d // 2, r + 1 + for a in small: + x = pow(a, d, n) + if x in (1, n - 1): + continue + for _ in range(r - 1): + x = x * x % n + if x == n - 1: + break + else: + return False + return True + + +def random_prime(ell): + while True: + n = rng.randrange(2 ** (ell - 1) + 1, 2 ** ell) | 1 + if is_prime(n): + return n + + +def main(): + raw = SRC.read_text(encoding="utf-8") + import importlib.util + spec = importlib.util.spec_from_file_location("retained_crt", SRC) + retained = importlib.util.module_from_spec(spec) + spec.loader.exec_module(retained) + for snippet in RETAINED: + need(snippet in raw, "retained decode_group / balanced lines") + + # Part A: lemmas on a grid, then the master inequality exactly + for a in range(1, 65): + for b in range(1, 65): + need(3 * a * b + 3 * a + b <= 8 * a * b, "schoolbook 8ab") + need(3 * a * b + 4 * a <= 8 * a * b, "division 8ab") + need(2 * a * (8 * a * a + 16 * a * a + 4 * a) <= 64 * a ** 3, "Euclid 64 b^3") + worst = 0.0 + for p in range(2, 201): + q = p + 2 + for ell in range(1, 41): + terms = [256 * q * q, 524288 * q ** 4, 8192 * q ** 3, 8192 * q * q * ell ** 3, + 800 * q * (ell + 2) ** 2 * 2 ** ell, 2048 * q * ell * 4 ** ell] + big = 2 ** (4 * ell) * q ** 16 + need(7 * max(terms) <= big and sum(terms) <= big, f"master inequality p={p} ell={ell}") + worst = max(worst, sum(terms) / big) + G = 64 * (ell + (q - 1).bit_length()) + need(sum(terms) * q ** 48 * 2 ** (60 * ell) <= 2 ** G, "guard amortization") + + # Part C: the per-wire step + slips = [ell for ell in range(1, 41) if 4 * (ell + 2) + 8 * (ell + 2) ** 2 > 9 * (ell + 2) ** 2] + need(slips == [1], "per-wire 9(ell+2)^2 fails exactly at ell = 1") + for ell in range(1, 41): + corrected = (4 * (ell + 2) + 8 * (ell + 2) ** 2) * 2 ** ell + 64 * ell * 4 ** ell + 8 * ell * 2 ** ell + need(corrected <= 25 * (ell + 2) ** 2 * 2 ** ell + 64 * ell * 4 ** ell, "per-network bound absorbs it") + + # Part B: instrumented CRT bill at the caller's sizes + samples = 0 + max_ratio = 0.0 + for ell in range(3, 13): + primes = odd_primes(2 ** (ell - 1), 2 ** ell) + for p in range(ell, min(8 * ell, 64) + 1, max(1, ell // 2)): + for _ in range(6): + m = rng.randint(1, max(1, p // ell)) + pool = rng.sample(primes, min(len(primes), 2 * m + 1)) + moduli, right, target = pool[:m], pool[m:2 * m], pool[-1] + if target in moduli or target in right: + continue + W = sum(bits(x) for x in moduli) + need(W <= p, "group bit length at most p") + residues = [rng.randrange(x) for x in moduli] + rp = 1 + for x in right[:rng.randint(0, len(right))]: + rp *= x + cost, off = charged_axis(residues, moduli, target, rp) + prod = 1 + for x in moduli: + prod *= x + ref = retained.decode_group(tuple(residues), tuple(moduli)) * pow(prod * rp, -1, target) % target + need(off == ref, "instrumented offset equals the retained decode_group offset") + bill = 128 * m * W * W + 128 * m * ell ** 3 + 16 * m * W + need(cost <= bill, f"instrumented cost within the per-axis bill at p={p} ell={ell} m={m}") + max_ratio = max(max_ratio, cost / bill) + samples += 1 + # long moduli: the inverse term 128 m ell^3 saturates as ell grows at m = 1 + tight = [] + for ell in range(14, 33): + for m in (1, 2, 4): + moduli = [random_prime(ell) for _ in range(m)] + right = [random_prime(ell) for _ in range(m)] + target = random_prime(ell) + if len(set(moduli + right + [target])) < 2 * m + 1: + continue + W = sum(bits(x) for x in moduli) + residues = [rng.randrange(x) for x in moduli] + rp = 1 + for x in right: + rp *= x + cost, off = charged_axis(residues, moduli, target, rp) + prod = 1 + for x in moduli: + prod *= x + need(off == retained.decode_group(tuple(residues), tuple(moduli)) * pow(prod * rp, -1, target) % target, + "long-moduli offset") + bill = 128 * m * W * W + 128 * m * ell ** 3 + 16 * m * W + need(cost <= bill, f"long moduli ell={ell} m={m}: within the per-axis bill") + max_ratio = max(max_ratio, cost / bill) + if m == 1: + tight.append(round(cost / bill, 4)) + samples += 1 + need(tight == sorted(tight) or max(tight) > 0.95, "m = 1 ratio approaches 1") + need(samples > 300, "enough samples") + print(json.dumps({ + "status": "PASS_CRT_EVALUATOR_INDEPENDENT_CHECK", + "master_inequality_grid": "p = 2..200, ell = 1..40", + "max_sum_terms_over_bound": f"{worst:.3e}", + "per_wire_slip_at": slips, + "instrumented_axes": samples, + "max_instrumented_cost_over_bill": f"{max_ratio:.4f}", + "m1_ratio_ell14_to_32": tight, + "new_kappa_claimed": False, + }, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())