diff --git a/research/crt-evaluator-layout-binding/PROOF.md b/research/crt-evaluator-layout-binding/PROOF.md new file mode 100644 index 0000000000..cc93cf1630 --- /dev/null +++ b/research/crt-evaluator-layout-binding/PROOF.md @@ -0,0 +1,156 @@ +# The constant-1 evaluator on accepted reservoir layouts + +This is a counting proof for one binding step inside Cinna Davis's PR #4100, +`CRT.md` §2–§4. It connects two merged packages. It is not an acceptance of +that construction, and it does not change κ. + +- PR #4377 (`research/crt-uniform-evaluator`) proves that the control + evaluator costs at most `E(p, ell) = 2^{4 ell} (p+2)^{16}` bit-steps, + so `C_E = 1`. Its domain is `p >= 2`, `ell >= 1`, a CRT group of bit + length `W <= p`, and a batch of at most `A <= 8(p+2)` target axes. +- PR #4174 (`research/crt-reservoir-placement`) constructs the layouts + and the reservoir batches of `CRT.md` §3. + +PR #4377 left the use of `C = 1` inside §3–§4 open, first at the `H >= G` +comparison, because placement geometry was not yet an input. PRs +#4921 and #4923–#4926 then carried the coefficient `C_E` through the product line +without evaluating it. This note supplies that binding. + +## Setting + +The #4174 constructor `Layout(p, ell, widths)` accepts exactly when + +```text +p >= 1, ell >= 2, ell >= λ := ceil(log2(p+2)), +d = len(widths) is a power of two at least 51200, +every width is ell-1 or ell, +r_max = floor(L / (100 G)) >= 1, +``` + +where `L` is the sum of the widths and `G = 64 (ell + λ)`. It sets +`H = r_max G`. Every plan has at most `r_max` active axes. Every control +group is the complete left child of a tree node, which is a set of logical +axes. + +The extra hypothesis is + +```text +(A) L <= p. +``` + +PR #4328 introduced (A) for the absorption step, and #4646 uses it. At the +actual #4100 caller it holds: #4377's size paragraph shows that the dyadic +length satisfies `log2 T <= b + 1 <= p` with `p = 6b`, and `log2 T` is the +sum of the axis widths. The #4174 production plan has `p = 6L`. + +## Theorem + +Let `Layout(p, ell, widths)` be accepted, and assume (A). Then: + +1. `ell >= 21`, `λ >= 21`, `p >= 1310720`, and `G >= 2688`. All four + bounds are attained together by `p = 1310720`, `ell = 21`, + `d = 2^16` and every width 20. +2. Every #4377 hypothesis holds: `p >= 2`, `ell >= 1`, every control + group has `W <= L <= p`, every batch has at most + `r_max <= floor(p / 268800)` axes, and the layout has at most + `d <= floor(p / 20)` axes. The last two are below `8(p+2)`. So one + evaluation costs at most `E(p, ell) = 2^{4 ell} (p+2)^{16}` bit-steps, + with `C_E = 1`. This holds whether #4377's batch is read as one + reservoir batch or as all axes. +3. `H >= G`, and + + ```text + 2^{-H} E <= 2^{-G} E <= 2^{-60 ell - 48 λ} <= 2^{-2268}. + ``` + + The maximum `2^{-2268}` of `2^{-G} E` over these layouts is attained + at `p = 2^{21} - 2`, `ell = 21`, `d = 2^16` and every width 20. +4. For `r <= r_max` targets with digit failures `2/B` and either window + term, `β = 2 (2^G - 2) 2^{-64G}` or the published `8B/2^K`, the + bad-key evaluation charge per record satisfies + + ```text + r (2/B + window) E < (p / 89600) 2^{-G} E < 2^{-2263}. + ``` + + With `C_E = 1`, this replaces #4646's printed + `(C_E p / 6400) 2^{-60 ell} (p+2)^{-48}`. + +Without (A), part 2 fails for an accepted layout. `p = 2`, `ell = 2`, +`d = 2^19` and every width 2 is accepted with `L = 2^20`, `G = 256` and +`r_max = 40 > 32 = 8(p+2)`. Its root control group has `W = 2^19 > p`. + +## Proof + +**Part 1.** `d` is a power of two at least 51200, so `d >= 2^16`. Every +width is at least `ell - 1`, so `L >= 2^16 (ell - 1)`. By the definition +of `λ`, `2^λ >= p + 2 > p`. With (A) and `ell >= λ`, + +```text +2^16 (ell - 1) <= L <= p < 2^λ <= 2^ell, +``` + +so `ell - 1 < 2^{ell - 16}`. For `2 <= ell <= 16` the right side is at +most 1, and `ell - 1 >= 1`. For `17 <= ell <= 20` the right side is at +most 16, and `ell - 1 >= 16`. Both cases are contradictions, so +`ell >= 21`. Then `p >= L >= 2^16 · 20 = 1310720`. Since +`p + 2 >= 1310722 > 2^20`, `λ >= 21` and `G = 64(ell + λ) >= 2688`. + +For the witness, `λ = ceil(log2 1310722) = 21 = ell`. Also +`L = 1310720 = p`, `G = 2688`, and `r_max = floor(1310720 / 268800) = 4`. + +*Remark.* The actual caller gives the stronger `L <= b + 1` with +`p = 6b`. Then `6 (2^16 (ell - 1) - 1) <= p <= 2^ell - 2`. This fails for +`ell = 23` (`8650746 > 8388606`) and for every smaller `ell`, so +`ell >= 24` there. The #4174 production plan `p = 9240576`, `ell = 24` +attains it. The theorem below uses only (A). + +**Part 2.** By part 1, `p >= 2` and `ell >= 1`. A control group is a set +of axes, so `W <= L <= p`. By part 1, `100 G >= 268800`, so +`r_max = floor(L / (100G)) <= floor(p / 268800)`. Also +`d <= L / (ell - 1) <= p / 20`. Both are below `p < 8(p+2)`. Thus +#4377's proposition applies with `C = 1`. + +**Part 3.** The constructor requires `r_max >= 1`, so `H = r_max G >= G`. +#4174's PROOF.md derives the same fact from `d >= 51200`. Then +`2^{-H} E <= 2^{-G} E`. Using `G = 64 ell + 64 λ` and `p + 2 <= 2^λ`, + +```text +2^{-G} E = 2^{-60 ell - 64 λ} (p+2)^{16} <= 2^{-60 ell - 48 λ}. +``` + +This is at most #4100's display `2^{-60 ell} (p+2)^{-48}`, since +`(p+2)^{-48} >= 2^{-48 λ}`. With `ell, λ >= 21` it is at most +`2^{-2268}`. Equality needs `ell = λ = 21` and `p + 2 = 2^{21}`. The +witness `p = 2097150` is accepted with `L = 1310720 <= p`, `G = 2688` and +`r_max = 4`. + +**Part 4.** `2/B = 2^{1-G}`. The sharp window is `β < 2^{1-63G}`. +The published window is `8B/2^K = 2^{3-63G}`, with `K = 64G`. Either way, + +```text +2/B + window <= 2^{-G} (2 + 2^{3-62G}) < 3 · 2^{-G}. +``` + +By (A) and part 1, `r <= r_max <= p / (100G) <= p / 268800`. So +`r (2/B + window) < 3p 2^{-G} / 268800 = p 2^{-G} / 89600`. Multiply by +`E`. By part 3, `2^{-G} E <= 2^{-60 ell - 48 λ}`. Since `p < 2^λ`, + +```text +(p / 89600) 2^{-G} E < 2^{-60 ell - 47 λ} / 89600 <= 2^{-2247} / 2^{16} + = 2^{-2263}. +``` + +**Counterexample without (A).** `p = 2` gives `λ = 2`, so `ell = 2` is +allowed and `G = 256`. Here `d = 2^19 >= 51200`. With every width 2, +`L = 2^20`, so `r_max = floor(2^20 / 25600) = 40 >= 1`. The constructor +accepts it. `8(p+2) = 32 < 40`. The root left child has `2^18` axes and +`W = 2^19`. ∎ + +## What this does not prove + +- The ordinary H-bit interchange callee and its `O(V H^{1-a} + V)` bill. +- Sparse repair sorting, reinsertion or fixed-tape radix passes. +- The finite range that falls back to elementary multiplication. +- The #4377 bit-step model itself. It is used as stated, not replayed. +- Any statement about layouts that violate (A). diff --git a/research/crt-evaluator-layout-binding/README.md b/research/crt-evaluator-layout-binding/README.md new file mode 100644 index 0000000000..e5b8140194 --- /dev/null +++ b/research/crt-evaluator-layout-binding/README.md @@ -0,0 +1,101 @@ +# Constant-1 CRT evaluator on accepted reservoir layouts + +**Scoped counting proof. No new κ.** The selected conditional exponent stays +60403/20000000. This does not accept PR #4100. + +## Result + +PR #4377 proves that #4100's control evaluator costs at most +`E(p, ell) = 2^{4 ell} (p+2)^{16}` bit-steps, so `C_E = 1`, when the CRT +group has bit length `W <= p` and the batch has at most `8(p+2)` axes. Its +open question 2 asked to use `C = 1` inside §3–§4, starting with `H >= G`. +That was blocked on placement geometry. PR #4174 has since been merged. +PRs #4646, #4921 and #4923–#4926 kept `C_E` as an unevaluated factor. + +[PROOF.md](PROOF.md) shows the following for every layout accepted by the +#4174 constructor with `L <= p`. That hypothesis is #4328's, and it holds +at the actual #4100 caller. + +| Part | Statement | Sharp at | +|---|---|---| +| 1 | `ell >= 21`, `p >= 1310720`, `G >= 2688` | `p = 1310720`, `ell = 21`, `d = 2^16`, widths 20 | +| 2 | `W <= p`, `r_max <= p/268800`, `d <= p/20`, all below `8(p+2)`, so `C_E = 1` applies | — | +| 3 | `H >= G` and `2^{-H} E <= 2^{-G} E <= 2^{-60 ell - 48 λ} <= 2^{-2268}` | `p = 2^{21} - 2`, `ell = 21` | +| 4 | per-record bad-key charge `r (2/B + window) E < (p/89600) 2^{-G} E < 2^{-2263}` | not sharp | + +Part 4 holds for both the sharp window `β` and the published `8B/2^K`. It +replaces #4646's printed `(C_E p / 6400) 2^{-60 ell} (p+2)^{-48}`. + +**The hypothesis `L <= p` is needed.** The constructor also accepts `p = 2`, +`ell = 2`, `d = 2^19`, widths 2. There `L = 2^20`, `r_max = 40 > 32 = 8(p+2)`, +and the root control group has `W = 2^19 > p`. So `C = 1` does not transfer to +that layout. Also, #4845's two `p = 2` exceptions are outside `L <= p`. With +`L <= p` we have `p >= 1310720`, so #4845's full-batch fit for `p >= 3` applies. + +With the actual caller's stronger `L <= b + 1` and `p = 6b`, the same argument +gives `ell >= 24`. The #4174 production plan `p = 9240576`, `ell = 24` attains it. + +Not proved here: the ordinary H-bit interchange callee, sparse sorting and +reinsertion, the elementary finite range, and #4377's bit-step model. The +last is used as stated and not replayed. + +## Evidence + +[verify.py](verify.py) loads the #4174 allocator on main. It checks the +following: + +- the thresholds `ell >= 21` and `ell >= 24` for every `ell <= 256`; +- the minimal, `2^{21} - 2`, production and #4926 edge layouts, including + the first 64 plans on the bottom and root levels; +- equality `2^{-G} E = 2^{-2268}` at `p = 2^{21} - 2`, with exact + rational part-4 bounds for both windows; +- the accepted counterexample; +- four rejection controls. These are an `ell = 20` layout, the sharper + bound `2^{-2269}`, the cap off `L <= p` and the coefficient `1/268800`. + +Input pins and quoted source phrases are checked first. The finite checks +corroborate the written proof; they do not replace it. + +## Scope + +Card `uniform-transfer-audit`, scope **refined** to the evaluator-to-layout +binding. Canonical main fetched 2026-10-23 at +`cef4b52f2a59009865bf8eabde1be3f159063703`, priority revision 7. Source +pins are in [SOURCES.json](SOURCES.json). + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3 scripts/research_package.py --package research/crt-evaluator-layout-binding --check-only +python3.12 -B scripts/research_package.py --package research/crt-evaluator-layout-binding +``` + +The direct command `python3.12 -B research/crt-evaluator-layout-binding/verify.py` +prints `PASS_CRT_EVALUATOR_LAYOUT_BINDING` in well under a second. + +## Open next questions + +1. **Does one ordinary H-bit interchange of `CRT.md` §3–§4 fit its stated + `O(V H^{1-a} + V)` bill at the actual #4174 width `H = r_max G`?** + - *Why it matters:* it is the reservoir-side remainder of #4377 and #4650 + open question 2. Under `L <= p`, the evaluator side is closed here. + - *First step:* write one #4174 three-field exchange as ordinary + interchange calls. Count its placement and restoration actions against + `V H^{1-a}` on `p = 1310720`, `ell = 21`. + - *Blocked by:* nothing. + +## Credit + +Cinna Davis, PR #4100, for the CRT construction, `E(p, ell)` and the +reservoir parameters. unpaidmoon, PR #4377, for the constant-1 evaluator and +the open question. PR #4646 (unpaidmoon) for the absorption and the printed +product line. PR #4328 for the `L <= p` hypothesis. Hiroki KUMAZAKI +(@kumagi), PR #4174, for the constructor and the production plan. PR #4650 +and PR #4845 for the shared-arena bills. James Reed, PRs #4921 and #4923–#4926, for +the reservoir-constant chain that left `C_E` open. + +Prepared by JoyboyBrian with substantial Anthropic Claude (Claude Code) +assistance. Apache-2.0. No independent human review and no formal-kernel +acceptance are claimed. diff --git a/research/crt-evaluator-layout-binding/SOURCES.json b/research/crt-evaluator-layout-binding/SOURCES.json new file mode 100644 index 0000000000..2e89286f4b --- /dev/null +++ b/research/crt-evaluator-layout-binding/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/compact-switch-sharp-density/PROOF.md", + "usage": "input", + "git_blob": "f7132bb89ba2dc1153175d400c5baef38a894f3f", + "sha256": "7ef2e48db773013ab4978a1594116c1235110c148081656b6b2c6927b5db6e3f" + }, + { + "path": "research/crt-reservoir-placement/PROOF.md", + "usage": "input", + "git_blob": "087ab4462282fc68d6f5b8b1f17167383e77df7c", + "sha256": "cea5eec3d4ec1008293e98213f519bdbf88dcd9aa801bff516eaee24340efa68" + }, + { + "path": "research/crt-reservoir-placement/allocator.py", + "usage": "input", + "git_blob": "4b3ad89652a28f7d142248d1b5747272e696493c", + "sha256": "b764195fc6291e3c8fa8297b1f4ceaefc119d5664d8ff348b49eac8a2e79c688" + }, + { + "path": "research/crt-uniform-evaluator/PROOF.md", + "usage": "input", + "git_blob": "7175c780b63378963c00ea29d76a9d1d7f86bbf0", + "sha256": "a67dce487dfaf0f1748458cf052b85203654d63f84c4e362ae78fe1bae1a3d42" + }, + { + "path": "research/unconditional-batched-crt/CRT.md", + "usage": "input", + "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6", + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b" + } + ] +} diff --git a/research/crt-evaluator-layout-binding/TASK.json b/research/crt-evaluator-layout-binding/TASK.json new file mode 100644 index 0000000000..9ee8f415e1 --- /dev/null +++ b/research/crt-evaluator-layout-binding/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "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": "Bind PR #4377's constant-1 evaluator E(p,ell)=2^{4ell}(p+2)^{16} to every PR #4174 accepted reservoir layout with L <= p: verify the evaluator's W <= p and 8(p+2) batch caps, H >= G, the dense amortization 2^{-H}E and the sparse per-record charge with C_E = 1, and show the caps fail on an accepted layout without L <= p.", + "scope_change_reason": "The card asks for one quantified #4100 step at its actual caller. This narrows it to the binding that #4377 open question 2 left blocked on placement geometry, now merged as #4174, and that #4646, #4921 and #4923-#4926 carried as an unevaluated C_E.", + "bottleneck_link": "Side result for the #4100 all-size audit: it removes the unevaluated constant C_E from the CRT repair amortization at the actual caller. The selected conditional exponent and frontier are unchanged.", + "budget_minutes": 60, + "stop_rule": "Stop after the binding at the evaluator interface. Do not price the ordinary H-bit interchange callee, sparse sorting or reinsertion, and do not replay #4377's bit-step model.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/crt-evaluator-layout-binding", + "author": "JoyboyBrian", + "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5) for the derivation, verifier and text.", + "open_questions": [ + { + "question": "With C_E = 1 bound here, does one ordinary H-bit interchange of CRT.md §3-§4 fit its stated O(V H^{1-a} + V) bill at the actual #4174 field width H = r_max G?", + "why_it_matters": "It is the remaining reservoir-side half of #4377 open question 2 and #4650 open question 2; the evaluator side is now closed under L <= p.", + "first_step": "Express one #4174 three-field exchange as ordinary interchange calls and count its placement and restoration tape actions against V H^{1-a} on the minimal layout p = 1310720, ell = 21.", + "blocked_by": "nothing" + } + ] +} diff --git a/research/crt-evaluator-layout-binding/VERIFY.json b/research/crt-evaluator-layout-binding/VERIFY.json new file mode 100644 index 0000000000..9063346801 --- /dev/null +++ b/research/crt-evaluator-layout-binding/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/compact-switch-sharp-density/PROOF.md", + "research/crt-reservoir-placement/PROOF.md", + "research/crt-reservoir-placement/allocator.py", + "research/crt-uniform-evaluator/PROOF.md", + "research/unconditional-batched-crt/CRT.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Under L <= p on #4174 layouts: ell >= 21 exactly (all ell <= 256), the minimal and 2^21-2 witnesses, the production plan and the #4926 edge satisfy the #4377 batch/group caps, H >= G, 2^{-G}E <= 2^{-2268} with equality at p=2^21-2, and the per-record charge below 2^{-2263}; the accepted p=2, d=2^19 layout breaks the cap; four mutated claims are rejected." + } + ] +} diff --git a/research/crt-evaluator-layout-binding/verify.py b/research/crt-evaluator-layout-binding/verify.py new file mode 100644 index 0000000000..6dc68c3d61 --- /dev/null +++ b/research/crt-evaluator-layout-binding/verify.py @@ -0,0 +1,177 @@ +#!/usr/bin/env python3 +"""Bind the constant-1 CRT evaluator to accepted reservoir layouts. + +PR #4377 proves E(p, ell) = 2^{4 ell} (p+2)^{16} on W <= p and at most +8(p+2) axes. PR #4174 constructs the reservoir layouts. Under L <= p this +checks the written proof's integer facts on exact witnesses, the threshold +ell >= 21 for every ell up to 256, and rejection controls. The universal +statement is PROOF.md, not this finite check. No new kappa is claimed. +""" + +from __future__ import annotations + +import hashlib +import importlib.util +import json +import sys +from fractions import Fraction +from itertools import islice +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "crt-evaluator-layout-binding" +ALLOCATOR = ROOT / "research/crt-reservoir-placement/allocator.py" + +PHRASES = { + "research/crt-uniform-evaluator/PROOF.md": ( + "`A <= 8(p+2)` target axes", + "E(p, ell) = 2^{4 ell} (p+2)^{16}", + "may be taken to be `C = 1` on this domain", + ), + "research/compact-switch-sharp-density/PROOF.md": ( + "r (2/B + β) E ≤ (C_E p / 6400) 2^{−60 ell} (p+2)^{−48}.", + "Assume `L ≤ p` and `r ≤ floor(L/(100G))`.", + ), + "research/unconditional-batched-crt/CRT.md": ( + "E(p,ell) <= C 2^(4 ell) (p+2)^16.", + "2^-G E(p,ell) <= C 2^(-60 ell) (p+2)^(-48),", + "H>=G eventually", + ), + "research/crt-reservoir-placement/PROOF.md": ( + "r_max >= d/51200 >= 1, H>=G, H<=L/100.", + ), +} + + +def need(condition: bool, message: str) -> None: + if not condition: + raise SystemExit("FAIL: " + message) + + +def pins_and_phrases() -> None: + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + for row in sources["files"]: + if row["usage"] == "input": + digest = hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() + need(digest == row["sha256"], row["path"]) + for path, phrases in PHRASES.items(): + text = (ROOT / path).read_text(encoding="utf-8") + for phrase in phrases: + need(phrase in text, f"{path}: {phrase}") + + +def load_allocator(): + spec = importlib.util.spec_from_file_location("crt_reservoir_allocator", ALLOCATOR) + module = importlib.util.module_from_spec(spec) + sys.modules[spec.name] = module + spec.loader.exec_module(module) + return module + + +def lam(p: int) -> int: + return (p + 1).bit_length() # ceil(log2(p+2)) + + +def scaled_charge(p: int, ell: int, G: int) -> Fraction: + """2^{-G} E with C_E = 1.""" + return Fraction(2 ** (4 * ell) * (p + 2) ** 16, 2 ** G) + + +def threshold() -> None: + """Part 1: with minimal L = 2^16 (ell-1), some p satisfies L <= p and + ceil(log2(p+2)) <= ell exactly when ell >= 21.""" + feasible = [ell for ell in range(2, 257) if (1 << 16) * (ell - 1) <= (1 << ell) - 2] + need(feasible == list(range(21, 257)), "ell >= 21 threshold") + # Remark: actual caller L <= b + 1 with p = 6b. + caller = [ell for ell in range(2, 257) + if 6 * ((1 << 16) * (ell - 1) - 1) <= (1 << ell) - 2] + need(caller == list(range(24, 257)), "ell >= 24 at the actual caller") + need(lam(1310720) == 21 and lam((1 << 20) - 2) == 20, "lambda helper") + + +def check_layout(allocator, p: int, ell: int, widths: tuple[int, ...]): + """Parts 2-4 on one accepted L <= p layout.""" + layout = allocator.Layout(p, ell, widths) + L, G, r_max, H, d = layout.L, layout.G, layout.r_max, layout.H, layout.d + need(L <= p and ell >= 21 and lam(p) >= 21 and p >= 1310720 and G >= 2688, "part 1") + need(G == 64 * (ell + lam(p)) and H == r_max * G and H >= G, "H >= G") + need(r_max <= p // 268800 < 8 * (p + 2), "batch cap") + need(d <= p // 20 < 8 * (p + 2), "axis cap") + # Every batch and control group of the top and bottom levels. + for level in (1, layout.levels): + for plan in iter_plans_sample(allocator, layout, level): + need(len(plan.active_axes) <= r_max, "plan batch size") + for dep in plan.dependencies: + lo, hi = dep.left_interval + need(hi - lo <= L <= p, "control group W <= p") + charge = scaled_charge(p, ell, G) + bound = Fraction(1, 2 ** (60 * ell + 48 * lam(p))) + need(charge <= bound <= Fraction(1, 2 ** 2268), "part 3") + need(bound <= Fraction(1, 2 ** (60 * ell) * (p + 2) ** 48), "#4100 display") + B, K = 2 ** G, 64 * G + sharp = Fraction(2 * (B - 2), 2 ** (64 * G)) + published = Fraction(8 * B, 2 ** K) + for window in (sharp, published): + density = r_max * (Fraction(2, B) + window) + need(density < Fraction(p, 89600 * B), "part 4 density") + need(density * 2 ** (4 * ell) * (p + 2) ** 16 < Fraction(1, 2 ** 2263), "part 4") + return layout, charge + + +def iter_plans_sample(allocator, layout, level): + # ponytail: first 64 batches of a level; the universal claim is PROOF.md. + return islice(allocator.iter_plans(layout, level), 64) + + +def witnesses(allocator) -> None: + twenty = (20,) * 65536 + minimal, charge = check_layout(allocator, 1310720, 21, twenty) + need((minimal.L, minimal.G, minimal.r_max, minimal.H) == (1310720, 2688, 4, 10752), + "minimal witness") + need(charge < Fraction(1, 2 ** 2268), "minimal witness is not the maximum") + peak, charge = check_layout(allocator, (1 << 21) - 2, 21, twenty) + need(peak.r_max == 4 and charge == Fraction(1, 2 ** 2268), "2^{-2268} attained") + production = tuple(24 - (i % 2) for i in range(65536)) + layout, _ = check_layout(allocator, 6 * sum(production), 24, production) + need(layout.p == 9240576 and layout.r_max == 5, "#4174 production plan") + layout, _ = check_layout(allocator, (1 << 24) - 2, 24, (23,) * 65536) + need(layout.r_max == 4, "#4926 edge layout") + + +def without_length_hypothesis(allocator) -> None: + layout = allocator.Layout(2, 2, (2,) * (1 << 19)) + need(layout.L == 1 << 20 and layout.L > layout.p and layout.G == 256, "counterexample") + need(layout.r_max == 40 and layout.r_max > 8 * (layout.p + 2), "batch cap fails") + root = next(allocator.iter_plans(layout, layout.levels)) + lo, hi = root.dependencies[0].left_interval + need(hi - lo == 1 << 19 and hi - lo > layout.p, "root W exceeds p") + + +def controls(allocator) -> None: + """Each mutated claim must be rejected.""" + rejected = 0 + try: # ell = 20 has lambda = 21 once p >= L = 2^16 * 19 + allocator.Layout(65536 * 19, 20, (19,) * 65536) + except ValueError: + rejected += 1 + peak = scaled_charge((1 << 21) - 2, 21, 2688) + rejected += peak > Fraction(1, 2 ** 2269) # a sharper universal bound fails + rejected += 40 > 8 * (2 + 2) # the cap fails off L <= p + density = 4 * (Fraction(2, 2 ** 2688) + Fraction(8, 2 ** (63 * 2688))) + rejected += density >= Fraction(1310720, 268800 * 2 ** 2688) # 1/268800 is too small + need(rejected == 4, "rejection controls") + + +def main() -> None: + pins_and_phrases() + threshold() + allocator = load_allocator() + witnesses(allocator) + without_length_hypothesis(allocator) + controls(allocator) + print("PASS_CRT_EVALUATOR_LAYOUT_BINDING ell_min=21 p_min=1310720 " + "max_scaled_charge=2^-2268 record_charge<2^-2263 controls=4") + + +if __name__ == "__main__": + main()