diff --git a/research/reservoir-universal-axis-cutoff/PROOF.md b/research/reservoir-universal-axis-cutoff/PROOF.md new file mode 100644 index 0000000000..1517de167c --- /dev/null +++ b/research/reservoir-universal-axis-cutoff/PROOF.md @@ -0,0 +1,172 @@ +# Exact universal axis capacity of the reservoir majorant + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped mathematical proof with exact finite corroboration. +The object optimized here is the inherited conservative factor-3 envelope. +Its failure is not failure of the actual repair algorithm or actual error. + +## Contract + +Use Hiroki KUMAZAKI's PR4174 constructor, at the source pinned in +SOURCES.json. An accepted layout has integers p>=1, c=ceil(log2(p+2)), +ell>=max(2,c), a power of two d>=65536, and d widths in {ell-1,ell}. +If a widths equal ell, its address length and maximum batch are + +```text +L = d(ell-1)+a, 0<=a<=d, +G = 64(ell+c), +r_max = floor(L/(100G)) = floor((d(ell-1)+a)/(6400(ell+c))). +``` + +The minimum allowed d is 65536 because the constructor requires a power +of two at least 51200. Every displayed parameter tuple passes its batch +positivity and volume checks: L/(100G)>=d(ell-1)/(12800ell)>=d/25600>2. +No requirement L<=p is imposed by this constructor. + +James Reed's PR4923 proves the conservative factor 3. PR4924/4925 derive +the printed-envelope ratio. We cite those arithmetic premises, without +replaying their verifiers or claiming their results as new. Relative to +C_E times the printed room, the conservative ratio is + +```text +R = 3 r_max ((p+2)/2^c)^64. +``` + +The question is exactly whether R<=p/6400 for every accepted ell and width +pattern, at fixed p,d. C_E cancels. It is not evaluated or given a value. +This is a different question from R<=1/6400 or from evaluating the real E. + +## The maximum batch is attained + +Put k=floor(d/6400). Then + +```text +max_(ell,a) r_max = k. +``` + +For the upper bound, L<=d ell and ell/(ell+c)<1, so +r_max=k if and only if + +```text +d ell >= 6400k(ell+c), +(delta) ell >= 6400kc. +``` + +Thus the maximum is attained at the finite precision + +```text +ell_* = max(2,c,ceil(6400kc/delta)), a=d. +``` + +This supplies an actual accepted layout, not merely a limiting supremum. +The minimum constructor precision and the open upper limit d/6400 both +matter. Replacing the floor by a rounded or floating-point limit is unsafe. + +## The sharp capacity criterion + +Define the nonnegative integer + +```text +M(p) = floor(p 2^(64c) / (19200 (p+2)^64)). +``` + +The following conditions are equivalent: + +1. Every accepted layout at p,d has R<=p/6400. +2. 19200 floor(d/6400) (p+2)^64 <= p 2^(64c). +3. floor(d/6400)<=M(p). +4. d<=6400(M(p)+1)-1. + +The maximum-batch theorem proves the equivalence of 1 and 2, including +necessity by the attaining all-wide layout. Integer division proves 2 iff +3, and the definition of floor proves 3 iff 4. Equality is accepted. + +Consequently let D(p)=6400(M(p)+1)-1. If D(p)<65536, no allowed dyadic axis +count passes uniformly in precision. Otherwise the largest allowed dyadic +count is 2^floor(log2(D(p))). All smaller allowed dyadic counts pass; every +larger allowed dyadic count has the explicit failure at ell_* above. + +The simple sufficient condition 3d<=p follows as a corollary: then +19200k<3d<=p and ((p+2)/2^c)^64<=1. Unlike L<=p, it does not restrict ell. +It is a sufficient corollary, not the sharp criterion. + +## No cutoff in p alone + +For each fixed p, M(p) is finite. Choose a power of two + +```text +d >= max(65536, 6400(M(p)+1)). +``` + +Then floor(d/6400)>=M(p)+1. The accepted all-wide layout at ell_* fails +the conservative inequality. This works for every p, however large. +Therefore no finite cutoff in p can make this majorant hold on all layouts +accepted by the constructor with unbounded d. A caller must control d or +supply a different bound. This does not assert that actual repair fails. + +## Explicit boundary witnesses + +At p=131070=2^17-2 and d=65536, c=17, M(p)=6, and k=10. For all-wide +layouts the inequality holds exactly when r_max<=6. For arbitrary width +patterns, all-wide maximizes r_max at each precision. The first failing +precision is therefore + +```text +ceil(6400*7*17/(65536-6400*7)) = 37. +``` + +At ell=36, L=2359296, G=3392, r_max=6, and the ratio of the majorant to +the p/6400 allowance is 3840/4369<1. At ell=37, L=2424832, G=3456, +r_max=7, and that ratio is 4480/4369>1. Thus every allowed width pattern +passes for 17<=ell<=36, while the all-wide pattern fails at 37. These +layouts both have L>p. The verifier constructs them with the pinned Layout. + +At p=2^24-2, M(p)=873 and D(p)=5593599. The largest uniformly covered +dyadic axis count is 4194304=2^22; the next count 8388608=2^23 fails at +its attaining precision. This classifies the entire precision/width family +at that p. It does not repeat PR4926's one-layout ratio 12. + +## Verification and limits + +The proof above supplies the unbounded quantifiers. The verifier checks +finite arithmetic boxes, all width-count patterns in its stated boxes, +the attaining precisions and their preceding seam, exact capacity neighbors, +and four actual Layout fixtures. It never executes predecessor verifiers, +the descriptor census, the repair program or the real E polynomial. +RESULT.json gives generated counts, source hashes and all control results. +Normal replay is read-only and rejects a changed receipt under -O. + +Native operations, simultaneous carry correctness, evaluator implementation, +physical repair, memory, routing, restoration, all-size caller integration, +compiler and outer multiplication remain separate obligations. The selected +frontier is unchanged. No kappa, supplier admission or complete multiplication +theorem is claimed. Independent human and formal proof-kernel review are unclaimed. + +## Code constraints + +The new verifier has no recursion. Every enumeration has a fixed finite range +stated in the code and the receipt. Functions stay below 60 physical lines. +Explicit exceptions enforce contracts and receipt comparison under -O. + +Power of Ten rule 3 has a managed-runtime deviation in verify.py: CPython +allocates integers, containers and source Layout prefixes. The finite fixture +has d<=65536; algebraic axis counts up to the stated finite probe exponent +are represented as integers rather than materialized axes. File reads are +capped at 1 MiB. The verifier releases one Layout before constructing the +next. These bounds limit live algorithmic data; runtime internals are not +allocation-instrumented. A native fixed-storage implementation would be +required before allocation-prohibited use. + +Rules 8 and 9 have a source-execution deviation for the four Layout fixtures: +runpy executes exactly one SHA256-authenticated, repository-pinned allocator +and the checker calls its Layout constructor. It imports no predecessor +checker, accepts no user-selected executable, and has no network or Git +runtime dependency. The official read-only Git-free replay exercises this +boundary. The source retains its own implementation and attribution; its +unrelated routines are not changed or claimed compliant here. + +Warning-strict normal and optimized replay provide the local diagnostics. +No static type checker is configured for this standalone package. diff --git a/research/reservoir-universal-axis-cutoff/README.md b/research/reservoir-universal-axis-cutoff/README.md new file mode 100644 index 0000000000..d8a0811980 --- /dev/null +++ b/research/reservoir-universal-axis-cutoff/README.md @@ -0,0 +1,98 @@ +# Exact universal axis cutoff for the CRT reservoir envelope + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped mathematical proof with exact finite corroboration. +For every fixed ambient parameter p and allowed dyadic axis count d, the +largest batch over all accepted precisions and width patterns is exactly +floor(d/6400), and a finite all-wide layout attains it. Consequently the +inherited conservative factor-3 envelope fits the printed repair allowance +for every such layout exactly when + +```text +c = ceil(log2(p+2)), +M = floor(p 2^(64c) / (19200 (p+2)^64)), +d <= 6400(M+1)-1. +``` + +Every larger allowed d has an explicit accepted failure witness. Thus no +cutoff in p alone covers the constructor's unbounded axis counts. This +settles a new uniform capacity question beyond the predecessor's individual +layouts. The proof is in [PROOF.md](PROOF.md), including the exact hypotheses +and an attaining precision. It does not reverify a predecessor theorem. + +For example, at p=131070 and d=65536 every width pattern passes through +precision 36, while the all-wide layout fails at precision 37. The exact +ratios to the allowance are 3840/4369 and 4480/4369, respectively. At +p=2^24-2, the largest axis count covered uniformly in precision is 2^22; +2^23 fails at its explicit attaining precision. + +These are statements about the conservative printed majorant. A failed +majorant is not a counterexample to actual repair, the smaller error bound +or the real E polynomial. No physical supplier, selected-frontier change, +new kappa or complete multiplication theorem is claimed. + +## Reproduce + +From the repository root with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/reservoir-universal-axis-cutoff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/reservoir-universal-axis-cutoff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/reservoir-universal-axis-cutoff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/reservoir-universal-axis-cutoff --check-source-history +``` + +Substitute another CPython 3.12 executable as needed. The direct marker is +PASS_RESERVOIR_UNIVERSAL_AXIS_CUTOFF. Default replay is read-only and compares +the entire generated [receipt](RESULT.json), including package/live-input +SHA256 hashes. `--write NEW_PATH` generates a new receipt and refuses an +existing file. Source pins and provenance are in [SOURCES.json](SOURCES.json). +The checker needs neither Git nor network at runtime. It imports no +predecessor verifier and does not run the descriptor census or repair engine. + +The finite checks cover 74,880 precision rows, 1,152 attainment seams, all +393,222 width-count patterns in six boxes, 1,464 capacity-neighbor probes +at 732 ambient parameters, four actual source Layout fixtures and fourteen +domain/source/receipt controls. The +unbounded quantifiers come from the written floor argument, not from the +finite probes. [VERIFY.json](VERIFY.json) registers normal and optimized +warning-strict commands. Code constraints and bounded runtime deviations +are recorded in the proof. + +## Open next questions + +1. Optimize the exact published window factor instead of the conservative + constant 3. Start with the batch staircase and decreasing correction as + precision varies. Those competing terms are not optimized here. +2. Bind an enclosing physical caller's reached p,d,ell values to this + criterion and the charged E envelope. The real evaluator, repair, + routing, restoration, native and outer obligations remain open. + +Structured first steps and blockers are in [TASK.json](TASK.json). +Independent human and formal proof-kernel review are unclaimed. No Lean, +Docker, selected cold replay or complete multiplier execution was run. + +## Source context and credit + +Base: canonical main 3f0152a32eeebac0df11946dbd50cabe5a7f7839, priority +revision 8. The selected conditional kappa remains .003125804. The +formal-interface-lemma card is changed to this original arithmetic theorem +rather than a formalization or audit. The known-working selected binding +command passed; it was orientation only. + +Credit Hiroki KUMAZAKI for [PR4174's constructor](https://github.com/CrocSwap/integer-mult-bounds/pull/4174), +James Reed for [PR4923's factor 3](https://github.com/CrocSwap/integer-mult-bounds/pull/4923), +[PR4925's ratio](https://github.com/CrocSwap/integer-mult-bounds/pull/4925) +and [PR4926's edge comparison](https://github.com/CrocSwap/integer-mult-bounds/pull/4926). +The compact-switch density/room premises in PR4646 and PR4328, Cinna Davis's +PR4100 CRT framework and their retained predecessor lineage keep their credit. +Integer division and monotonicity are standard. The new step is the exact +unbounded precision optimization, sharp axis-capacity criterion and explicit +failure construction for this envelope. No literature-priority claim is made. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267742). +Overlap covered live open PRs, recent account work, active hub claims, +local reservations, distinctive main README formulas and merged PR bodies. +Unpublished work and historical diffs outside those searches remain limits. +Only this new package is changed; frozen inputs and contributor notices remain. diff --git a/research/reservoir-universal-axis-cutoff/RESULT.json b/research/reservoir-universal-axis-cutoff/RESULT.json new file mode 100644 index 0000000000..235a4769cb --- /dev/null +++ b/research/reservoir-universal-axis-cutoff/RESULT.json @@ -0,0 +1,110 @@ +{ + "actual_layouts": [ + { + "G": 2176, + "L": 1114112, + "d": 65536, + "ell": 17, + "p": 131070, + "r_max": 5, + "wide": 65536 + }, + { + "G": 3392, + "L": 2359296, + "d": 65536, + "ell": 36, + "p": 131070, + "r_max": 6, + "wide": 65536 + }, + { + "G": 3456, + "L": 2359296, + "d": 65536, + "ell": 37, + "p": 131070, + "r_max": 6, + "wide": 0 + }, + { + "G": 3456, + "L": 2424832, + "d": 65536, + "ell": 37, + "p": 131070, + "r_max": 7, + "wide": 65536 + } + ], + "capacities": { + "ambient_parameters": 732, + "dyadic_neighbors": 1464, + "examples": { + "1": { + "axis_limit": 33036799, + "batch_capacity": 5161, + "largest_accepted_dyadic_count": 16777216 + }, + "131070": { + "axis_limit": 44799, + "batch_capacity": 6, + "largest_accepted_dyadic_count": null + }, + "16777214": { + "axis_limit": 5593599, + "batch_capacity": 873, + "largest_accepted_dyadic_count": 4194304 + }, + "2": { + "axis_limit": 6399, + "batch_capacity": 0, + "largest_accepted_dyadic_count": null + }, + "9240576": { + "axis_limit": 116387500828673071187199, + "batch_capacity": 18185547004480167372, + "largest_accepted_dyadic_count": 75557863725914323419136 + } + }, + "no_p_cutoff_witnesses": 732 + }, + "capacity": "d <= 6400*(floor(p*2^(64*c)/(19200*(p+2)^64))+1)-1", + "claim_type": "scoped proof with finite corroboration", + "controls": [ + "invalid_domain_0", + "invalid_domain_1", + "invalid_domain_2", + "invalid_domain_3", + "invalid_domain_4", + "invalid_domain_5", + "invalid_domain_6", + "invalid_domain_7", + "invalid_domain_8", + "allow_one_excess_batch", + "check_only_minimum_precision", + "check_only_narrow_widths", + "changed_source_byte", + "boolean_receipt_count" + ], + "maximum_batch": "floor(d/6400), attained", + "maximum_grid": { + "attaining_seams": 1152, + "precision_rows": 74880 + }, + "no_new_kappa": true, + "schema_version": 1, + "source_sha256": { + "PROOF.md": "cebd3a64f4ba9873d9ea705056e9a39bd13c27b48d6a5d564e17f0c165c32903", + "README.md": "b1c607b19ce68d6e897b626e8cc9fe2e5602aad755df2786a5173775d8b03839", + "SOURCES.json": "e0b6822cb2560c536ca2f2dc1e35199a10c6167ca0ecaf0b7714c1ebb6836d45", + "TASK.json": "fc0a08d6f7d5b70b94643b78a5450e63a404f848abc54a7dfc1db72ad9f6a7fc", + "VERIFY.json": "29e2777e8ad15608068e299a9009e516a0d0fdf0171b19656dff156dd93656b7", + "research/crt-reservoir-placement/allocator.py": "b764195fc6291e3c8fa8297b1f4ceaefc119d5664d8ff348b49eac8a2e79c688", + "verify.py": "79a551ae5991952609fd2dcdc1747958446119d45b948fba3c820e0b641fdb83" + }, + "width_counts": { + "complete_width_count_patterns": 393222, + "layouts": 6 + } +} diff --git a/research/reservoir-universal-axis-cutoff/SOURCES.json b/research/reservoir-universal-axis-cutoff/SOURCES.json new file mode 100644 index 0000000000..e8558485db --- /dev/null +++ b/research/reservoir-universal-axis-cutoff/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "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/crt-reservoir-placement/allocator.py", + "usage": "input", + "git_blob": "4b3ad89652a28f7d142248d1b5747272e696493c", + "sha256": "b764195fc6291e3c8fa8297b1f4ceaefc119d5664d8ff348b49eac8a2e79c688" + }, + { + "path": "research/crt-reservoir-uniform-constant/README.md", + "usage": "provenance", + "git_blob": "275a4c26eab1a800aba7f2a5d1751586815bc23e", + "sha256": "5f1dd9d5e0e67d1901e9fd65207762906c7966e5038609249087cb22dd4c513a" + }, + { + "path": "research/crt-reservoir-production-ratio/README.md", + "usage": "provenance", + "git_blob": "517272145b174f68a8c4f8c997a65bf1bd50eb32", + "sha256": "5fe75f2dc817950fe360f8c78beabe9f32c1420dce6cefe8d381f8356680b70e" + }, + { + "path": "research/crt-reservoir-edge-allowance/README.md", + "usage": "provenance", + "git_blob": "70d8785b448baa8a638ef167a839588bcf1f0e6f", + "sha256": "5be702f2b5e7a51412e17668eda532f71559fe265c50d6dcb878601bcc5ac00a" + }, + { + "path": "research/compact-switch-sharp-density/PROOF.md", + "usage": "provenance", + "git_blob": "f7132bb89ba2dc1153175d400c5baef38a894f3f", + "sha256": "7ef2e48db773013ab4978a1594116c1235110c148081656b6b2c6927b5db6e3f" + } + ] +} diff --git a/research/reservoir-universal-axis-cutoff/TASK.json b/research/reservoir-universal-axis-cutoff/TASK.json new file mode 100644 index 0000000000..6e5f37388f --- /dev/null +++ b/research/reservoir-universal-axis-cutoff/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "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": "Classify exactly when the inherited conservative CRT reservoir 3 r_max envelope fits the printed p/6400 allowance for every precision and width pattern at fixed p and dyadic axis count d; construct attaining failures and exclude a p-only cutoff.", + "scope_change_reason": "This is an original quantified arithmetic question beyond the single-layout comparisons in PR4923/4925/4926. The card is changed from formalization/audit to a written unbounded theorem and exact finite corroboration. No predecessor result is reverified as a deliverable.", + "bottleneck_link": "Separates a sufficient repair-room estimate from the actual L<=p premise. The new sharp axis-capacity criterion can certify arbitrarily long addresses, and proves that increasing p alone does not cover an unconstrained axis count. Actual error, physical repair and complete supplier admission remain separate.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved universal capacity criterion with an attaining source-bound counterexample; package it without optimizing the actual error or changing the envelope.", + "outcome": "completed", + "evidence": "PROOF.md gives the unbounded theorem. The standalone warning-strict normal/optimized verifier checks exact integer inequalities, exhaustive finite width-count patterns, attaining precisions, capacity boundaries, actual Layout fixtures and rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the exact published window factor replace the conservative factor 3 in a sharp universal axis-capacity theorem?", + "why_it_matters": "Failure of the factor-3 majorant is not a lower bound on the actual repair error or its smaller scalar bound.", + "first_step": "Optimize r_max times (2+2^(3-62G)) over all accepted precisions, retaining the floor and the dependence of G on precision.", + "blocked_by": "The batch staircase and decreasing correction must be optimized together; this package fixes the inherited factor-3 majorant." + }, + { + "question": "Does an actual complete CRT caller satisfy the new axis-capacity criterion at every reached parameter?", + "why_it_matters": "A constructor accepts more layouts than a particular multiplier reaches.", + "first_step": "Bind the caller equations for p,d,ell and the charged E envelope, then apply the criterion to those exact reached layouts.", + "blocked_by": "No enclosing physical caller, real E polynomial, source/repair implementation or complete multiplication theorem is established here." + } + ] +} diff --git a/research/reservoir-universal-axis-cutoff/VERIFY.json b/research/reservoir-universal-axis-cutoff/VERIFY.json new file mode 100644 index 0000000000..b375bcdc3a --- /dev/null +++ b/research/reservoir-universal-axis-cutoff/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/crt-reservoir-placement/allocator.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact universal axis-capacity arithmetic; finite width-count and precision boxes; attaining threshold witnesses; four actual source Layout fixtures; all controls; full generated receipt bound to package and live-input SHA256 hashes." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact universal axis-capacity arithmetic; finite width-count and precision boxes; attaining threshold witnesses; four actual source Layout fixtures; all controls; full generated receipt bound to package and live-input SHA256 hashes." + } + ] +} diff --git a/research/reservoir-universal-axis-cutoff/verify.py b/research/reservoir-universal-axis-cutoff/verify.py new file mode 100644 index 0000000000..812f8f3661 --- /dev/null +++ b/research/reservoir-universal-axis-cutoff/verify.py @@ -0,0 +1,235 @@ +#!/usr/bin/env python3 +"""Exact axis capacity of the inherited conservative reservoir envelope.""" + +from __future__ import annotations + +import argparse +import hashlib +import json +import runpy +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +ALLOCATOR = "research/crt-reservoir-placement/allocator.py" +MAX_FILE_BYTES = 1 << 20 + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def read_bytes(path: Path) -> bytes: + with path.open("rb") as handle: + data = handle.read(MAX_FILE_BYTES + 1) + need(len(data) <= MAX_FILE_BYTES, "File exceeds the replay read bound") + return data + + +def canonical(value: object) -> str: + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def parameters(p: int, d: int) -> int: + need(type(p) is int and p >= 1, "p must be a positive integer") + need(type(d) is int and d >= 65536 and d & (d - 1) == 0, + "d must be a power of two at least 65536") + return (p + 1).bit_length() + + +def batch(p: int, d: int, ell: int, wide: int) -> int: + c = parameters(p, d) + need(type(ell) is int and ell >= max(2, c), "Invalid precision") + need(type(wide) is int and 0 <= wide <= d, "Invalid width count") + return (d * (ell - 1) + wide) // (6400 * (ell + c)) + + +def attaining_precision(p: int, d: int) -> int: + c = parameters(p, d) + k, delta = divmod(d, 6400) + need(delta > 0, "A dyadic count has a nonzero remainder modulo 6400") + return max(2, c, (6400 * k * c + delta - 1) // delta) + + +def capacity(p: int) -> tuple[int, int]: + c = parameters(p, 65536) + m = (p << (64 * c)) // (19200 * (p + 2) ** 64) + return m, 6400 * (m + 1) - 1 + + +def envelope_fits(p: int, r: int) -> bool: + c = parameters(p, 65536) + need(type(r) is int and r >= 0, "Invalid batch size") + return 19200 * r * (p + 2) ** 64 <= p << (64 * c) + + +def check_maximum_grid() -> dict[str, int]: + precision_rows = 0 + seams = 0 + for p in range(1, 129): + for exponent in range(16, 25): + d = 1 << exponent + c = parameters(p, d) + k = d // 6400 + ell_star = attaining_precision(p, d) + need(batch(p, d, ell_star, d) == k, "Maximum is not attained") + need(batch(p, d, ell_star + 1, d) == k, "Attained tail changes") + if ell_star > c: + need(batch(p, d, ell_star - 1, d) < k, "Attainment seam") + seams += 1 + for ell in range(c, c + 65): + low = batch(p, d, ell, 0) + high = batch(p, d, ell, d) + need(1 <= low <= high <= k, "Finite precision bound") + length = d * ell + denom = 6400 * (ell + c) + need(high * denom <= length < (high + 1) * denom, + "Integer quotient bounds") + precision_rows += 1 + return dict(precision_rows=precision_rows, attaining_seams=seams) + + +def check_width_counts() -> dict[str, int]: + rows = 0 + d = 65536 + cases = ((1, 2), (1, 100), (2, 2), (2, 84), + (131070, 36), (131070, 37)) + for p, ell in cases: + previous = -1 + k = d // 6400 + for wide in range(d + 1): + r = batch(p, d, ell, wide) + need(previous <= r <= k, "Width-count monotonicity or maximum") + need(r - previous <= 1 or previous == -1, "Unexpected batch jump") + previous = r + rows += 1 + need(previous == batch(p, d, ell, d), "Missing final width count") + return dict(layouts=6, complete_width_count_patterns=rows) + + +def check_capacities() -> dict[str, object]: + values = set(range(1, 513)) + values.update((1 << exponent) + offset + for exponent in range(2, 65) for offset in (-3, -2, -1, 0)) + neighbors = 0 + no_cutoff = 0 + for p in sorted(values): + m, limit = capacity(p) + need(envelope_fits(p, m) and not envelope_fits(p, m + 1), + "Allowance floor seam") + first_failure = max(65536, 1 << limit.bit_length()) + for d in (first_failure, max(65536, first_failure // 2)): + ell_star = attaining_precision(p, d) + r = batch(p, d, ell_star, d) + expected = d <= limit + need(envelope_fits(p, r) == expected, "Sharp axis-capacity boundary") + need((r <= m) == expected, "Batch-capacity equivalence") + neighbors += 1 + ell_star = attaining_precision(p, first_failure) + need(not envelope_fits(p, batch(p, first_failure, ell_star, first_failure)), + "No-p-cutoff witness did not fail") + no_cutoff += 1 + examples = {} + for p in (1, 2, 131070, 16777214, 9240576): + m, limit = capacity(p) + largest = None if limit < 65536 else 1 << (limit.bit_length() - 1) + examples[str(p)] = dict(batch_capacity=m, axis_limit=limit, + largest_accepted_dyadic_count=largest) + need(examples["16777214"]["largest_accepted_dyadic_count"] == 4194304, + "Explicit large capacity") + return dict(ambient_parameters=len(values), dyadic_neighbors=neighbors, + no_p_cutoff_witnesses=no_cutoff, examples=examples) + + +def source_hashes() -> dict[str, str]: + sources = json.loads(read_bytes(PACKAGE / "SOURCES.json")) + rows = [row for row in sources["files"] if row["usage"] == "input"] + need(len(rows) == 1 and rows[0]["path"] == ALLOCATOR, "Unexpected live input") + source = read_bytes(ROOT / ALLOCATOR) + digest = hashlib.sha256(source).hexdigest() + need(digest == rows[0]["sha256"], "Changed allocator source") + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + hashes = {name: hashlib.sha256(read_bytes(PACKAGE / name)).hexdigest() + for name in names} + hashes[ALLOCATOR] = digest + return hashes + + +def actual_layouts() -> list[dict[str, int]]: + constructor = runpy.run_path(str(ROOT / ALLOCATOR))["Layout"] + rows = [] + d, p = 65536, 131070 + for ell, wide in ((17, d), (36, d), (37, 0), (37, d)): + widths = (ell,) * wide + (ell - 1,) * (d - wide) + layout = constructor(p, ell, widths) + expected = batch(p, d, ell, wide) + need(layout.r_max == expected, "Actual Layout batch differs") + need(layout.L == d * (ell - 1) + wide, "Actual Layout length differs") + need(layout.G == 64 * (ell + 17), "Actual Layout guard differs") + rows.append(dict(p=p, d=d, ell=ell, wide=wide, + L=layout.L, G=layout.G, r_max=layout.r_max)) + del layout, widths + need([row["r_max"] for row in rows] == [5, 6, 6, 7], "Boundary fixtures") + need(envelope_fits(p, 6) and not envelope_fits(p, 7), "First failure") + return rows + + +def controls(hashes: dict[str, str]) -> list[str]: + names = [] + bad = ((0, 65536, 2, 0), (True, 65536, 2, 0), (1, 32768, 2, 0), + (1, 102400, 2, 0), (1, 65536, 1, 0), (131070, 65536, 16, 0), + (1, 65536, 2, -1), (1, 65536, 2, 65537), (1, 65536, 2, True)) + for index, args in enumerate(bad): + try: + batch(*args) + except ValueError: + names.append("invalid_domain_" + str(index)) + else: + raise ValueError("An invalid domain fixture was accepted") + p = 131070 + need(envelope_fits(p, 6) and not envelope_fits(p, 7), "Rounded cutoff mutant") + names.append("allow_one_excess_batch") + need(batch(p, 65536, 17, 65536) < 10, "Minimum precision is not maximum") + names.append("check_only_minimum_precision") + need(batch(p, 65536, 37, 0) == 6 < batch(p, 65536, 37, 65536), + "Narrow widths cannot replace the maximum-width pattern") + names.append("check_only_narrow_widths") + changed = hashlib.sha256(read_bytes(ROOT / ALLOCATOR) + b"\n").hexdigest() + need(changed != hashes[ALLOCATOR], "Source corruption was invisible") + names.append("changed_source_byte") + need(canonical({"count": 1}) != canonical({"count": True}), + "Boolean-valued receipt mutation was invisible") + names.append("boolean_receipt_count") + return names + + +def result() -> dict[str, object]: + hashes = source_hashes() + return dict(schema_version=1, claim_type="scoped proof with finite corroboration", + maximum_batch="floor(d/6400), attained", + capacity="d <= 6400*(floor(p*2^(64*c)/(19200*(p+2)^64))+1)-1", + source_sha256=hashes, maximum_grid=check_maximum_grid(), + width_counts=check_width_counts(), capacities=check_capacities(), + actual_layouts=actual_layouts(), controls=controls(hashes), + no_new_kappa=True) + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="Write a new generated receipt") + args = parser.parse_args() + report = result() + if args.write is not None: + with args.write.open("x", encoding="utf-8") as handle: + handle.write(json.dumps(report, indent=2, sort_keys=True) + "\n") + else: + saved = json.loads(read_bytes(PACKAGE / "RESULT.json")) + need(canonical(saved) == canonical(report), "Receipt mismatch") + print("PASS_RESERVOIR_UNIVERSAL_AXIS_CUTOFF " + + hashlib.sha256(canonical(report).encode()).hexdigest()) + + +if __name__ == "__main__": + main()