diff --git a/research/gaussian-phase-boundary-count/PROOF.md b/research/gaussian-phase-boundary-count/PROOF.md new file mode 100644 index 0000000000..2bae5211ea --- /dev/null +++ b/research/gaussian-phase-boundary-count/PROOF.md @@ -0,0 +1,147 @@ +# Exact counts for the physical Gaussian carve + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract and source + +Let s,k,w be positive integers, k 4w. (1) + +For each integer x, let j be its residue in [0,s), p=floor(x/s), and + + q_j=floor(tj/s+1/2), h_j=q_j-j=floor(kj/s+1/2). + +A physical cell is a maximal interval on which the pair (p,h_j) is +constant. The source cuts at physical period seams even if the unwrapped +phase does not change there. For a nonempty window [a,a+m), intersect it +with these cells. A piece of length L contributes + + f(L) = L if L<=4w, + 2w if L>4w, (2) + +boundary rows. A piece is called long exactly when L>4w. + +This is the carve in Jose Manuel / jmbarrancoml's PR3851, +`gaussian_axis.py:prepare_weights` and +`gaussian_window.py:prepare_positions,emit_cell`, retained at +`7ab67b4a84d28cd562b9711aa315ca5b47822b37`. Its numerical and physical +correctness are cited premises, not rechecked results. The construction +and credit of its Gaussian, RaD, PR481/486/489 and physical-word predecessors +remain with their sources. Dugongue's PR5566 already uses complete Beatty +runs for another inverse algorithm; the floor identity and general run +viewpoint are credited, rather than claimed as new mathematics. + +The new result is the exact count for this physical-period carve, its +long-piece count and a smaller allowance for the unchanged caller. + +## Every complete cell is long + +In one physical period the phases are 0,...,k. Define their cuts + + A_0=0, A_(k+1)=s, + A_c=ceil(s(2c-1)/(2k)) for 1<=c<=k. + +The phase-c cell is exactly [A_c,A_(c+1)). This follows by solving +c<=kj/s+1/2 4w. + +They imply s/(2k)>d-1/2, hence floor(s/(2k))>=d-1>4w. +Thus (1) follows in that domain. Other production, locality and numerical +hypotheses are not needed for this counting lemma and are not discharged. + +## Exact constant-size formula + +The cell containing x has ordinal + + g(x)=floor(x/s)+floor(kx/s+1/2). (3) + +Indeed, writing x=ps+j gives g(x)=p(k+1)+h_j. Consecutive physical cells +increase this ordinal by one, including negative periods and physical +seams. If c=h_j, its left and right endpoints are + + ell(x)=ps+A_c, r(x)=ps+A_(c+1). (4) + +Set b=a+m and C=g(b-1)-g(a)+1. This is exactly the number of nonempty +pieces meeting the window. If C=1, then + + n_B=f(m), c_long=[m>4w]. (5) + +Otherwise let L=r(a)-a and R=b-ell(b-1). Then + + n_B = 2w(C-2)+f(L)+f(R), + c_long = C-2+[L>4w]+[R>4w]. (6) + +Only the first and last pieces can be clipped. Each of the other C-2 +pieces is a complete long cell, proving both equations. The interior-row +count is exactly m-n_B. The formulas hold for any positive window length, +including multiple periods and arbitrary signed starts. + +The formula uses a fixed number of exact integer operations, independent +of the number of rows or cells. This is an arithmetic-operation statement, +not a constant bit-time claim or an encoded tape implementation. Integer +division and descriptor access still need their physical charges. + +## A smaller source-domain allowance + +For 1<=m<=s, each floor difference in (3) is bounded above by the ceiling +of its argument increment. The period difference is at most one. Hence + + C <= 2+ceil(k(m-1)/s). + +For C>=2, f(L),f(R)<=4w, so (6) gives n_B<=2w(C+2). For C=1, +f(m)<=4w also obeys the following bound. Since n_B<=m in every case, + + n_B <= min(m, 2w ceil(k(m-1)/s)+8w). (7) + +The source's actual window satisfies s-m>w and therefore m=1 and w,m>0. Thus the new untrivialized +allowance is strictly smaller than the published allowance; capping both +allowances by m can make them equal on short windows. No new carve, +word, numerical output or recursive paid profile is asserted. + +## Exact strict example and complete invoice substitution + +Take s=480,t=485,k=5,w=3,d=48 and [a,b)=[0,384). The phase-piece +lengths are + + 48, 96, 96, 96, 48. + +They are all long. Equations (5)-(6) give n_B=30, c_long=5 and n_I=354. +The published allowance is 4*384*3/48+12*3=132. Equation (7) is +6*ceil(5*383/480)+24=48. This is a strict improvement of an upper bound +for the same carve, not a changed execution. The ratio/spacing hypotheses +hold; this small fixture is not an asymptotic production payload. + +The source's word-API count is + + 20 n_I + 16w^2 c_long + 2 n_B(4w+1) + + 2m + 2n_target + 2n_core + 32 c_long. + +Substitute n_I=m-n_B to obtain + + 22m+(8w-18)n_B+(16w^2+32)c_long+2n_target+2n_core. (9) + +At fixed c_long=5, the old n_B allowance gives 10120 plus the last two +terms, (7) gives 9616, and the exact count gives 9508. These totals are +derived solely from the displayed source tariff. They do not claim fewer +calls in the unchanged program. For w>=3 the n_B coefficient is positive, +so an upper bound can be substituted in (9); for w=1,2 it is negative +and that substitution would be invalid. Exact equations (5)-(6) remain +valid for every w. The full tensor/setup/native invoice and all inherited +numerical premises remain separate. diff --git a/research/gaussian-phase-boundary-count/README.md b/research/gaussian-phase-boundary-count/README.md new file mode 100644 index 0000000000..5585f7ec5c --- /dev/null +++ b/research/gaussian-phase-boundary-count/README.md @@ -0,0 +1,121 @@ +# Exact boundary counts for Gaussian phase windows + +This contribution was produced by Nick Petalas. Apache-2.0. + +Scoped counting proof with exact finite corroboration. For the unchanged +physical-period/phase-cell carve in Jose Manuel / jmbarrancoml's +[PR3851](https://github.com/CrocSwap/integer-mult-bounds/pull/3851), the +boundary-row and long-piece counts have a formula requiring only the two +endpoint cells and a fixed number of integer operations. It handles clipped +pieces, negative lifted starts and windows crossing any number of periods. + +For one-period windows in the source production domain, the published +allowance improves from + + n_B <= 4mw/d+12w + +to + + n_B <= min(m, 2w ceil((t-s)(m-1)/s)+8w). + +In the explicit s=480,t=485,w=3,d=48,m=384 window, the old allowance is +132, the new allowance is 48, and the exact count is 30. The execution and +actual number of rows are unchanged. This is a tighter accounting bound, +with no new kappa or selected-frontier change. + +[PROOF.md](PROOF.md) gives the all-size formula and its source-domain +implication. It also substitutes the exact row and long-piece counts in +the complete source word-API tariff. This avoids silently charging saved +boundary rows while forgetting their interior charge. The coefficient of +n_B in that tariff is positive only for w>=3. + +## Evidence and reproduction + +From the repository root, using the CPython 3.12 standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-phase-boundary-count/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gaussian-phase-boundary-count/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-phase-boundary-count +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-phase-boundary-count --check-source-history +``` + +Another CPython 3.12 path may replace the local path. The scientific marker +is `PASS_GAUSSIAN_PHASE_BOUNDARY_COUNT`. Registered replay runs both modes. +All acceptance checks use explicit exceptions and remain active under -O. +Default replay writes nothing. Optional `--receipt PATH` exclusively creates +a generated source-hash receipt outside the checkout; no receipt is handwritten. + +The independent literal checker computes nearest indices from t*j/s and +groups the actual (physical period, nearest-j) keys. It appends one row at +a time and updates the source's threshold rule without calling the closed +form. It checks every s=10..64, w=1..3 and k satisfying the long-cell +hypothesis, every starting residue and every length 1..2s+1. Alternating +residues are shifted into negative periods. All 1,459,710 windows across 319 configurations agree exactly, including +722,570 one-period upper-bound checks. Six semantic and eleven domain controls +pass. Additional fixtures cover +larger periods, translated starts, 4w/4w+1 thresholds and the strict example. +The universal claim comes from the written proof, not these finite cases. + +The verifier authenticates the three source inputs before counting. It +imports and executes no predecessor implementation or scientific suite. +Source-byte hashes bind the scope; they do not certify the numerical or +physical correctness inherited from the source. + +## Scope, credit and overlap + +Source head: `7ab67b4a84d28cd562b9711aa315ca5b47822b37` from PR3851. +Publication base: canonical main `2485805a6d47f36ea83ddde6327d453ac82d44dc`, +priority revision 8. [SOURCES.json](SOURCES.json) pins the retained source +bytes, original card and selected record. [TASK.json](TASK.json) explicitly +changes `uniform-transfer-audit` to this accounting side result for the +analytic/physical caller. No selected assumption is discharged. + +Credit Jose Manuel for the complete physical producer/consumer and its +carve, threshold and word-API tariff. Credit Dugongue's +[PR5566](https://github.com/CrocSwap/integer-mult-bounds/pull/5566) for the +related complete Beatty-run inverse and classical floor/run viewpoint; +Vlado Vojdanovski and the phase-cell contributors, RaD/hipotures, +Chafik Boukhalfa's PR481/486/489, the physical word implementation and the +retained Harvey-van der Hoeven/source lineage. Those results are premises +and context, not audit deliverables. Frozen sources and their credit remain +unchanged. Elementary floor arithmetic is classical; no literature-priority +claim is made for it. + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19292015) +preceded the experiment. Live PRs, recent account work, active Discussions, +local reservations, merged searches and main-tree README formula/object +searches were checked. The card helper had no usable remote cache and +searched only 105 of 8722 local notes; separate live queries and Git-tree +searches supplemented it. Sparse notes, arbitrary diffs and unpublished +work remain outside coverage. These checks are not proof of novelty. + +No changed physical planner, numerical Gaussian replay, native supplier, +retained-backing reduction, full tensor/setup bill, improved multiplication +exponent or complete multiplication theorem is supplied. The fixture does +not satisfy every production locality requirement. The full numerical, +compiler, ownership, precision/tape and analytic assumptions remain. +Independent human and formal proof-kernel review are unclaimed. Lean, +Docker and the selected supplier cold replay were not run. + +## Open next questions + +Can the encoded preparation planner use the exact counts before allocating +boundary banks? Start with one actual Window preparation, charge its encoded +divisions and descriptor access, and compare retained backing and the whole +setup/online bill. A changed physical allocation implementation is missing. +The arithmetic formula alone establishes no storage or runtime reduction. + +## Implementation bounds + +The verifier is nonrecursive. Functions remain below 60 physical lines. +The exhaustive domain fixes s<=64,w<=3 and at most 129 literal rows per +scan; extra literal scans are capped at 1024. Formula inputs are capped at +4096 bits, including a maximum-capacity fixture. The mathematical theorem +has no such bit cap. Source/package reads are capped at 256 KiB per file. +State is local, there is no dynamic code or scientific subprocess, and +failures propagate. Python's integer, dictionary and temporary allocation +are a managed-runtime deviation from fixed steady-state storage; finite +loop, bit and file bounds constrain this command. Warning-strict normal +and optimized execution are registered. An external static analyzer and +fixed-allocation native implementation are not claimed. diff --git a/research/gaussian-phase-boundary-count/SOURCES.json b/research/gaussian-phase-boundary-count/SOURCES.json new file mode 100644 index 0000000000..685ecd3fab --- /dev/null +++ b/research/gaussian-phase-boundary-count/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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/physical-gaussian-core/PROOF.md", + "usage": "input", + "git_blob": "883c8d4a6f0eead888fb3532b60db41596940889", + "sha256": "e909026dd3f455c35ff28210a0c4ffa232ad8d7633174e481094fd09e2469d7a" + }, + { + "path": "research/physical-gaussian-core/gaussian_axis.py", + "usage": "input", + "git_blob": "edc443a7281e83536a00e9f9fa950d7d854705a3", + "sha256": "d416918d7442c5033e43fba94ccc5ed33badc3aebe90ddd479b0b6c020de9724" + }, + { + "path": "research/physical-gaussian-core/gaussian_window.py", + "usage": "input", + "git_blob": "335e0e2d2ee67302a67d1c5ba7c63baecc9b02d8", + "sha256": "d10eb4ac559a5dc3ef4a6178ab4cac7dfdcdb5e84ef8acf372bd22c81ab64996" + }, + { + "path": "research/beatty-run-gaussian-inverse/analysis.md", + "usage": "provenance", + "git_blob": "e5cc397cd0baacd686cb8a075d636b9e595bdfae", + "sha256": "5c015de52b1867b07296c666bbe917c89ce508f6ca45dec909aceea0518b111a" + } + ] +} diff --git a/research/gaussian-phase-boundary-count/TASK.json b/research/gaussian-phase-boundary-count/TASK.json new file mode 100644 index 0000000000..584aa4af1e --- /dev/null +++ b/research/gaussian-phase-boundary-count/TASK.json @@ -0,0 +1,94 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "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": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact physical-period/phase-cell boundary-row and long-piece counts for the unchanged PR3851 Gaussian window carve.", + "scope_change_reason": "A source-relative accounting side result for the analytic/physical caller. It does not discharge any selected framework assumption or audit a predecessor result.", + "bottleneck_link": "Replaces the coarse n_B <= 4mw/d+12w with an exact arithmetic count and a smaller source-domain allowance. The complete outer tensor and supplier remain separate.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified counting improvement; no changed carve, numerical replay or physical implementation expansion.", + "outcome": "completed", + "evidence": "Written all-size counting proof, independent literal phase-key scan, seam/threshold/domain controls and generated hash-bound stdout receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an encoded preparation planner consume the exact count before allocating its boundary banks?", + "why_it_matters": "The arithmetic count alone does not reduce retained backing or pay for encoded divisions and metadata.", + "first_step": "Bind the formula to one actual Window preparation and charge its encoded arithmetic and capacity changes.", + "blocked_by": "No changed physical planner or backing-allocation implementation is supplied." + } + ], + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19292015", + "source_question": "PR #3851 by jmbarrancoml: complete caller accounting and period-cut geometry.", + "verification_scope": "No predecessor scientific verifier is imported or replayed. Numerical/caller correctness is inherited and outside this result.", + "finite_coverage": { + "configurations": 319, + "windows": 1459710, + "one_period_bound_checks": 722570, + "seam_translation_fixtures": 144, + "semantic_controls": 6, + "domain_rejections": 11 + } +} diff --git a/research/gaussian-phase-boundary-count/VERIFY.json b/research/gaussian-phase-boundary-count/VERIFY.json new file mode 100644 index 0000000000..672c9445c4 --- /dev/null +++ b/research/gaussian-phase-boundary-count/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/physical-gaussian-core/PROOF.md", + "research/physical-gaussian-core/gaussian_axis.py", + "research/physical-gaussian-core/gaussian_window.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact closed form versus complete literal phase-key scan; clipped, signed, seam, threshold, strict-improvement and invalid-domain controls; source hashes." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the complete scientific census with every explicit contract active under optimization." + } + ] +} diff --git a/research/gaussian-phase-boundary-count/verify.py b/research/gaussian-phase-boundary-count/verify.py new file mode 100644 index 0000000000..a335223a0a --- /dev/null +++ b/research/gaussian-phase-boundary-count/verify.py @@ -0,0 +1,228 @@ +#!/usr/bin/env python3 +"""Exact phase-window census. Produced by Nick Petalas. Apache-2.0.""" +import argparse +import hashlib +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def ceiling(numerator, denominator): + return -(-numerator // denominator) + + +def validate(s, k, w, start, length): + for value in (s, k, w, start, length): + need(type(value) is int and value.bit_length() <= 4096, + "integer argument with at most 4096 bits") + need(0 < k < s and w > 0 and length > 0, "positive phase/window domain") + need(s // (2 * k) > 4 * w, "every complete physical cell must be long") + + +def cell(s, k, position): + period, residue = divmod(position, s) + phase = (2 * k * residue + s) // (2 * s) + left = 0 if phase == 0 else ceiling(s * (2 * phase - 1), 2 * k) + right = s if phase == k else ceiling(s * (2 * phase + 1), 2 * k) + return period * (k + 1) + phase, period * s + left, period * s + right + + +def piece(length, w): + return (length, 0) if length <= 4 * w else (2 * w, 1) + + +def count(s, k, w, start, length): + """Return boundary rows, long pieces and total pieces, without a row scan.""" + validate(s, k, w, start, length) + first, _, right = cell(s, k, start) + last, left, _ = cell(s, k, start + length - 1) + pieces = last - first + 1 + if pieces == 1: + boundary, long = piece(length, w) + return boundary, long, 1 + first_boundary, first_long = piece(right - start, w) + last_boundary, last_long = piece(start + length - left, w) + boundary = 2 * w * (pieces - 2) + first_boundary + last_boundary + long = pieces - 2 + first_long + last_long + need(0 <= boundary <= length and 0 <= long <= pieces, "count invariants") + return boundary, long, pieces + + +def short_window_bound(s, k, w, length): + need(1 <= length <= s, "bound is for at most one period") + return min(length, 2 * w * ceiling(k * (length - 1), s) + 8 * w) + + +def literal_prefixes(s, k, w, start, limit): + """Independent append-only scan of the source's (period, q_j-j) keys.""" + need(0 < limit <= 1024, "literal scan capacity") + previous, run_length = None, 0 + boundary = long = cells = 0 + for position in range(start, start + limit): + period, residue = divmod(position, s) + nearest = ((s + k) * residue * 2 + s) // (2 * s) + key = period, nearest - residue + if key != previous: + cells += 1 + run_length = 0 + old_boundary = run_length if run_length <= 4 * w else 2 * w + old_long = int(run_length > 4 * w) + run_length += 1 + new_boundary = run_length if run_length <= 4 * w else 2 * w + new_long = int(run_length > 4 * w) + boundary += new_boundary - old_boundary + long += new_long - old_long + previous = key + yield boundary, long, cells + + +def complete_census(): + configurations = windows = bounded = 0 + digest = hashlib.sha256() + for s in range(10, 65): + for w in range(1, 4): + for k in range(1, s // (2 * (4 * w + 1)) + 1): + if s // (2 * k) <= 4 * w: + continue + configurations += 1 + for residue in range(s): + start = residue - (s if residue % 2 else 0) + scans = literal_prefixes(s, k, w, start, 2 * s + 1) + for length, expected in enumerate(scans, 1): + actual = count(s, k, w, start, length) + need(actual == expected, f"literal mismatch {s,k,w,start,length}") + if length <= s: + need(actual[0] <= short_window_bound(s, k, w, length), + "one-period upper bound") + bounded += 1 + digest.update(f"{s},{k},{w},{start},{length}:{actual};".encode()) + windows += 1 + return {"configurations": configurations, "windows": windows, + "bounded_windows": bounded, "transcript_sha256": digest.hexdigest()} + + +def boundary_fixtures(): + checks = 0 + for s, k, w in ((100, 2, 1), (211, 6, 2), (480, 5, 3)): + for start in (-2*s-1, -s, -1, 0, 1, s-1, s, 2*s+1): + for length in (1, 4*w, 4*w+1, s-1, s, 2*s+1): + expected = list(literal_prefixes(s, k, w, start, length)) + need(count(s, k, w, start, length) == expected[-1], "seam fixture") + a = count(s, k, w, start, length) + need(a == count(s, k, w, start + 19*s, length), "translation") + checks += 1 + huge = 1 << 4095 + need(count(huge, 1, 1, -huge, huge) == (4, 2, 2), "capacity boundary") + need(count(480, 5, 3, 0, 384) == (30, 5, 5), "strict witness") + need(short_window_bound(480, 5, 3, 384) == 48, "new witness allowance") + need(4 * 384 * 3 // 48 + 12 * 3 == 132, "old witness allowance") + return {"seam_translation_fixtures": checks, "witness": { + "s": 480, "t": 485, "w": 3, "d": 48, "start": 0, "length": 384, + "piece_lengths": [48, 96, 96, 96, 48], "boundary": 30, + "long_pieces": 5, "new_allowance": 48, "old_allowance": 132}} + + +def controls(): + need(count(100, 2, 1, 90, 20) == (4, 2, 2), "period seam must split") + need(cell(100, 2, -1) == (-1, -25, 0), "signed floor, not truncation") + need(count(100, 2, 1, 0, 25)[2] == 1, "half-open right endpoint") + need(count(100, 2, 1, 0, 4)[0] == 4, "4w is entirely boundary") + need(count(100, 2, 1, 0, 5)[0] == 2, "4w+1 is long") + need(count(480, 5, 3, 0, 9)[0] == 9, "short piece is not capped at 2w") + invalid = ((0, 1, 1, 0, 1), (10, 0, 1, 0, 1), (10, 10, 1, 0, 1), + (100, 2, 0, 0, 1), (100, 2, 1, 0, 0), (100, 2, 1, 0, -1), + (True, 1, 1, 0, 1), (100, 2, 1, 0.0, 1), + (8, 1, 1, 0, 1), (1 << 4096, 1, 1, 0, 1)) + for args in invalid: + try: + count(*args) + except ValueError: + continue + raise ValueError("invalid input was accepted") + try: + short_window_bound(100, 2, 1, 101) + except ValueError: + return {"semantic": 6, "domain_rejections": len(invalid) + 1} + raise ValueError("multi-period bound was accepted") + + +def invoice_fixture(): + lengths, previous = [], None + for position in range(384): + period, residue = divmod(position, 480) + nearest = (2 * 485 * residue + 480) // 960 + key = period, nearest - residue + if key != previous: + lengths.append(0) + lengths[-1] += 1 + previous = key + need(lengths == [48, 96, 96, 96, 48], "literal witness pieces") + w = 3 + units = 0 + for length in lengths: + long = length > 4 * w + for offset in range(length): + boundary = not long or offset < w or offset >= length - w + fee = 2 * (4 * w + 1) if boundary else 20 + units += sum(1 for _ in range(fee)) + units += 2 + if long: + units += sum(1 for _ in range(16 * w * w + 32)) + totals = [22 * 384 + (8*w-18) * b + (16*w*w+32) * 5 for b in (132, 48, 30)] + need(totals[-1] == units == 9508, "complete source tariff substitution") + need(totals == [10120, 9616, 9508], "old, new and exact invoice allowances") + return {"literal_units": units, "allowances": totals, + "common_addend": "2*n_target+2*n_core", "old_to_new_reduction": 504} + + +def source_hashes(package): + root = package.parents[1] + with (package / "SOURCES.json").open("rb") as stream: + metadata = stream.read(262145) + need(len(metadata) <= 262144, "manifest capacity") + sources = json.loads(metadata) + need(len(sources["files"]) <= 16, "source-pin count capacity") + hashes = {} + for entry in sources["files"]: + if entry["usage"] != "input": + continue + path = root / entry["path"] + with path.open("rb") as stream: + data = stream.read(262145) + need(len(data) <= 262144, "source capacity") + digest = hashlib.sha256(data).hexdigest() + need(digest == entry["sha256"], "source byte pin: " + entry["path"]) + hashes[entry["path"]] = digest + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"): + path = package / name + with path.open("rb") as stream: + data = stream.read(262145) + need(len(data) <= 262144, "package capacity") + hashes[name] = hashlib.sha256(data).hexdigest() + return hashes + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + package = Path(__file__).resolve().parent + hashes = source_hashes(package) + result = {"status": "PASS_GAUSSIAN_PHASE_BOUNDARY_COUNT", "claim_type": "scoped-proof", + "census": complete_census(), "fixtures": boundary_fixtures(), + "controls": controls(), "invoice": invoice_fixture(), "sha256": hashes} + output = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.receipt is not None: + need(not args.receipt.resolve().is_relative_to(package.parents[1]), + "receipt must remain outside the checkout") + with args.receipt.open("x") as stream: + stream.write(output) + print(output, end="") + + +if __name__ == "__main__": + main()