diff --git a/research/p104-stochastic-prefix/PROOF.md b/research/p104-stochastic-prefix/PROOF.md new file mode 100644 index 0000000000..0db4519167 --- /dev/null +++ b/research/p104-stochastic-prefix/PROOF.md @@ -0,0 +1,176 @@ +# Stochastic precision on the first selected scalar block + +This proof and its source-bound certificate were produced by Nick Petalas. +New work is Apache-2.0. The source word and its endpoint theorem are credited +premises. This proof neither re-establishes that endpoint nor changes it. + +## The changed arithmetic contract + +Read `research/p104-helper-subspace-splits/WORD.json.gz` at the base pinned in +SOURCES.json. Take the half-open program interval `[0,9589)`, stopping before +its first MOVE. All 9,589 events are ADD or SCALE at frame 3, the empty frame. +There are 9,358 ADDs and 231 SCALEs, on 748 public roles. The block touches +501 roles. No native frame change, initialization or erasure occurs inside it. +At a fixed stream sample, each real component is consequently a scalar linear +straight-line program with fixed rational coefficients. + +Fix a grid spacing h > 0. All incoming scalar components, including every +dirty helper component, belong to h Z. An ADD computes x_r + q x_s exactly +before rounding once; a SCALE computes q x_r exactly before rounding once. +This is a macro arithmetic contract, not a claim about the source's scalar +bit implementation. There is no overflow or saturation. Integer-coefficient +updates remain exactly on the grid and do not round. For a noninteger dyadic +coefficient, write the exact updated scalar as h(a + theta), with integer a +and 0 <= theta < 1. Return ha with probability 1-theta, or h(a+1) with +probability theta, using a fresh draw conditional on the entire past. Exact +grid values remain exact. Both negative numbers and arbitrary dirty values +are included in this definition. + +The source coefficients have denominator 1, 2 or 4. Since the current values +are on h Z, each noninteger update needs at most one or two fresh fair bits +for exact sampling. There are 7,421 such updates, with total denominator +logarithm 11,713. This bounds random bits per real sample for the literal +fixed-draw sampler. It does not price integer operations, random-bit access, +storage, routing or a full native implementation. + +## Exact output influences + +Let A_t be the exact update matrix for event t, and let d_t be its destination. +Let R be the set of the 7,421 potentially rounded events. Number events from +zero. Define the fixed output vector + + b_t = A_(L-1) ... A_(t+1) e_(d_t), L = 9589, + +where an empty product is the identity. For output j put + + S_j = sum_(t in R) b_t[j]^2, + L_j = sum_(t in R) |b_t[j]|. + +These quantities concern propagation of newly injected errors, independently +of the source's claimed endpoint map. The generated certificate computes +all 748 pairs exactly. Two separate algorithms agree. The reverse engine +starts from identity output columns, records each destination column before +transposing that event, and uses integer vectors with binary denominators. +The forward engine starts from zero formal errors, executes updates in their +original order and injects a new independent formal variable after every +event in R. It uses sparse Fraction dictionaries. Its final coefficients +supply S_j and L_j directly. + +The resulting exact values are + + max S_j = 733/8, attained only at role 217; + max L_j = 90, attained only at role 184; + sum S_j = 32269/4; + #{j : S_j > 0} = 282. + +The complete outputwise list is emitted by verify.py, with source/package +hashes. There are 8,493 nonzero formal error coefficients at exit, with at +most 98 in any output row. These are coefficient occurrences, not distinct +program events. S_j is a sum over possible rounding sites, so it can be +conservative when some sites happen to lie exactly on the grid. No equality +claim for the worst actual stochastic variance is made. + +## Conditional variance and tails + +Let epsilon_t be the additive rounding error after event t. Conditional on +the past, it has mean zero, variance at most h^2/4, and two possible values +in an interval of length h. Set epsilon_t = 0 outside R. Because every +update is linear, the exact difference from the unrounded block is + + E_j = sum_(t in R) b_t[j] epsilon_t. + +The weights are deterministic. Cross terms have zero expectation by +conditioning the later error on its past. Hence, for every allowed input, + + E[E_j] = 0, + E[E_j^2] = sum_t b_t[j]^2 E[epsilon_t^2] + <= h^2 S_j/4, + E[sum_j E_j^2] <= 32269 h^2/16. + +Errors generally are not independent. Their distributions can depend on +previous rounded states. Conditional zero mean is the property used here. + +For completeness, a centered random variable in an interval of length h +satisfies E exp(lambda X) <= exp(lambda^2 h^2/8). Indeed, the second derivative +of its log moment generating function is a variance under exponential tilt. +Every tilted distribution has the same support interval. If a <= Y <= b, +E[(Y-a)(b-Y)] >= 0 gives Var Y <= (b-a)^2/4 after completing the square. +Integrating the derivative bound twice from zero proves the displayed +inequality for positive and negative lambda. Apply it conditionally at each +event, with lambda replaced by lambda b_t[j], then iterate conditional +expectation. Chernoff's bound, optimized at lambda = 4u/(h^2 S_j), gives + + Pr(|E_j| >= u) <= 2 exp(-2u^2/(h^2 S_j)) if S_j > 0. + +An output with S_j = 0 has zero error. A union bound, requiring no independence +between outputs, therefore gives + + Pr(max_j |E_j| >= u) <= 564 exp(-16u^2/(733 h^2)). + +This is an absolute-error statement. It has no input-magnitude factor, +first-order truncation or asymptotic remainder. + +## A one-bit certificate improvement on this block + +For h = 2^-6 and u = 1/2, the preceding failure bound is + + 564 exp(-16384/733) < 2^-23. + +The strict inequality has an exact rational certificate. Put x = 16384/733. +The verifier evaluates P = sum_(k=0)^64 x^k/k! and checks + + P > 564 * 2^23. + +Since exp(x) > P, the claimed probability follows without a floating-point +exponential or logarithm. For complex scalars at one stream sample, apply +the same reasoning to both real and imaginary components. The simultaneous +componentwise failure probability is below 2^-22. At M samples, a union +bound multiplies these bounds by M; there is no all-stream assertion at +fixed failure probability. Independence between samples is not needed for +that union bound, provided each scalar update satisfies its own conditional +rounding contract. + +For deterministic nearest rounding on the same block, the local error is +at most h/2. The exact absolute-influence certificate gives + + max_j |E_j| <= 45h. + +To certify a strict error below 1/2 with h = 2^-g, this bound needs g >= 7. +At g = 6 it gives 45/64; at g = 7 it gives 45/128. Thus the stochastic +certificate uses one fewer fractional bit for a stated failure probability. +This is a comparison of sufficient certificates. It does not prove that +nearest rounding at six bits fails, or that stochastic six-bit precision is +optimal. The allowed initial 2^-6-grid inputs also belong to the 2^-7 grid. +The exact prefix endpoint need not be integral, so this observation does not +by itself imply integer recovery. + +## Essential boundaries and rejection controls + +Fresh conditional randomness is essential. For two updates y += x/2 with +x = 1 and y = 0 on the unit grid, reusing the same fair bit makes the final +error -1 or +1. Its variance is 1, while S_y/4 = 1/2. Each individual rounding +has the right unconditional marginal, which is insufficient. Always rounding +both ties down instead has bias -1. The verifier enumerates the fresh-draw +versions and checks their genuine conditional probabilities. + +A later inverse word with fresh rounding need not restore the dirty inputs +exactly, even if its exact linear endpoint is the identity. For example, +y += x/2 followed by y -= x/2 can leave error -1 or +1 with positive +probability. The finite fixtures include this word. We do not claim exact +restoration from small expected error or a high-probability enclosure. + +No MOVE is rounded or executed here. Initial off-grid conversion, native +frame operators, later scalar blocks, overflow headroom, correlated physical +error, bit-level sampling/costs, exact cleanup, compiler/stock admission, +analytic recovery and whole-multiplier error remain separate obligations. +The full selected source theorem is reused only as provenance, not audited. +The five selected framework assumptions are unchanged. Independent human +and formal proof-kernel review are unclaimed. + +The rounding method and bounded-martingale argument are classical. See +Connolly, Higham and Mary, *Stochastic Rounding and Its Probabilistic Backward +Error Analysis*, SIAM J. Sci. Comput. 43 (2021), A566-A585, +https://doi.org/10.1137/20M1334796, for mean-independent stochastic rounding. +The fixed-grid proof above is self-contained. The contribution is the new +exact selected-block influence certificate and its explicit precision/failure +specialization, not a new general concentration theorem. diff --git a/research/p104-stochastic-prefix/README.md b/research/p104-stochastic-prefix/README.md new file mode 100644 index 0000000000..9c98f2bcdb --- /dev/null +++ b/research/p104-stochastic-prefix/README.md @@ -0,0 +1,141 @@ +# A stochastic precision certificate for the selected P104 prefix + +This contribution was produced by Nick Petalas. Apache-2.0. + +Scoped proof with an exact finite influence certificate. On the selected +#5599 word's first 9,589-event common-frame scalar block, fresh unbiased +fixed-grid stochastic rounding has exact squared influence maximum **733/8**. +For arbitrary incoming grid values, including dirty helpers, six fractional +bits give simultaneous absolute error below 1/2 in every real output at one +stream sample with failure probability below **2^-23**. For both components +of complex outputs the probability is below **2^-22**. + +The deterministic nearest-rounding absolute-influence certificate on this +same block gives error at most 45h and needs seven fractional bits to certify +a strict error below 1/2. This is a one-bit improvement between sufficient +certificates with different guarantees. Neither precision is proved optimal, +and the exact intermediate endpoint need not be integral. + +The stochastic arithmetic contract is new here. Each noninteger dyadic scalar +update is evaluated exactly and rounded once, with fresh conditional randomness. +Integer-grid operations are exact. No predecessor verifier is imported or +replayed, and no predecessor result is audited. [PROOF.md](PROOF.md) derives +the variance and tail inequalities, explains their classical basis and states +the complete boundary. No new kappa, physical supplier or multiplication +theorem is claimed. + +## Evidence and reproduction + +The standalone verifier authenticates the frozen selected word and extracts +its prefix before the first MOVE. A reverse integer-column engine and an +independent chronological formal-error engine agree on all 748 output pairs. +The generated stdout receipt includes every output's squared and absolute +influence, the source/package hashes and the exact tail certificate. + +The block contains 7,421 potentially rounded updates. Its maximum absolute +influence is 90; 282 outputs have nonzero formal noise influence. The forward +engine retains 8,493 nonzero formal coefficients, at most 98 per output. +An exact positive Taylor polynomial proves the exponential comparison. +All 125 tiny-input fixtures are enumerated, with 423 terminal state occurrences. +No random sampling is used. +Controls distinguish chronological order, altered coefficients, fresh draws +from a reused coin and unbiased rounding from biased ties. All checks remain +active with Python optimization. + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -X dev -B research/p104-stochastic-prefix/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -X dev -O -B research/p104-stochastic-prefix/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-stochastic-prefix +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-stochastic-prefix --check-source-history +``` + +Another CPython 3.12 path may replace the displayed interpreter. Expected +markers are `PASS_P104_STOCHASTIC_PREFIX`, `PASS_REGISTERED_RESEARCH_PACKAGE` +and `PASS_RESEARCH_COMMIT_BYTES`. Each registered command has a 120-second +limit. The direct verifier writes no files. The publication preflight needs +committed files and full source history. A Git-free replay needs this package +and the single live word path declared in VERIFY.json. + +## Scope, cost and limitations + +The changed `uniform-transfer-audit` scope concerns the selected +`precision_tape` assumption. Source-binding orientation passes, but no selected +scientific replay is performed. Canonical base is +`19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228531) +records the question. Live open PRs, account history, Discussions, local +reservations, main README contents and distinctive merged-PR terms were +searched. Sparse local cache coverage is incomplete, and these checks cannot +exclude unpublished overlap or establish literature priority. + +The prefix uses one empty common frame and no MOVE. The proof is scalar and +pointwise. All incoming values must already lie on the chosen grid; overflow +and saturation are excluded. At M samples a union bound multiplies the stated +failure probability by M. The literal dyadic sampler needs at most 11,713 +fresh fair bits per real sample, with integer arithmetic and random-bit +movement still unpriced. Native approximation, input conversion, later blocks, +stream-wide precision, physical random sampling, exact dirty restoration, +compiler/stock obligations and analytic recovery remain unproved. All five +selected framework assumptions remain. Independent human and formal +proof-kernel review are unclaimed. Lean, Docker and full multiplier replays +were not run. + +Fresh rounding does not make a rounded inverse restore dirty inputs exactly. +A two-update identity word in the proof can leave a nonzero error. A reused +coin can also violate the variance bound even when its one-step marginals +look unbiased. These limitations prevent interpreting the certificate as an +admitted randomized supplier. + +## Credit + +Ali Romman's #5599 supplies the selected independent-helper word and split +construction. Pierre-Loic Doulcet / hexapode's #5565 supplies its commuting +contacts. Retain Ali Romman's #5580/#5544/#5545, Joel Pulikkan / GamingPuzzled's +#5569, DreamingOfClouds' #5561, thu-nmrc's #5551, Gareth Davidson / bitplane, +David Arias, Cinna Davis, Jacob Alan Sussman, zxv, Cao Yifan and all geometry, +BIT, native, precision, analytic and source predecessors in the unchanged +[selected notice](../p104-helper-subspace-splits/NOTICE). +SOURCES.json pins that notice and the source README as provenance. + +Stochastic rounding and mean-independent error analysis are classical; see +[Connolly, Higham and Mary (2021)](https://doi.org/10.1137/20M1334796). +The proof gives the fixed-grid concentration argument directly. The new +contribution is the exact selected-prefix influence certificate, its explicit +failure bound and the comparison of sufficient precision certificates. + +## Open next questions + +Can one complete native caller use this rounding model while restoring its +dirty state exactly? Start with a round-and-restore ABI that retains and then +erases its random bits, charging every action. A physical reversible sampler +and its complete cost are the present blockers. + +Can a finite sample count and the next actual MOVE preserve a useful total +failure budget? First propagate this block's errors through that native +operator with its own approximation contract. Whole-stream precision and +later blocks are outside this certificate. Structured questions are in +TASK.json. + +## Code constraints + +The verifier is nonrecursive and uses no subprocess, network, dynamic code +or write path. Fixed source bounds are 26,000 full-word events, 9,589 extracted +events, 748 roles, coefficients with denominator at most four and absolute +value at most 16. Reverse vectors have at most 128-bit numerators and exponent +64; forward rational coefficients have matching bit caps, enforced during +replay. Each formal row has at most 10,000 terms. Source +reads are capped at 1 MiB compressed and 4 MiB unpacked, and six receipt reads +at 1 MiB each. Tiny probability trees have at most eight steps, three roles +and 256 states, enforced during enumeration. The Taylor sum has 65 terms. +Functions fit below 60 physical lines. Warning-strict development-mode normal +and optimized runs are the available diagnostics; no external static analyzer +or whole-repository lint configuration is claimed. + +Power of Ten rule 3 has a managed-runtime deviation. Python, Fraction, JSON +and gzip allocate dynamically. The verifier is a finite offline check with +the enforced collection and input caps above, rather than a fixed-allocation +arithmetic implementation. Its matrix and dictionary capacities are finite; +this does not inspect allocator internals or establish a real-time guarantee. +A deployed sampler would need its own storage and random-bit lifetime proof. diff --git a/research/p104-stochastic-prefix/SOURCES.json b/research/p104-stochastic-prefix/SOURCES.json new file mode 100644 index 0000000000..7bb2bf689d --- /dev/null +++ b/research/p104-stochastic-prefix/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper-subspace-splits/NOTICE", + "usage": "provenance", + "git_blob": "f34687ff7eab377d5433f7b0c18274a816d2b73c", + "sha256": "8bbda66537ac761d632603066bdbb568ab5b26545030ea7979e27a85fcbe040c" + }, + { + "path": "research/p104-helper-subspace-splits/README.md", + "usage": "provenance", + "git_blob": "f6303a881379723e1f6512dfe153fafeecbf62dd", + "sha256": "a83c5c3ae7a31a5dfbc3c7c59669ee55cc15f966a0cb4405cb48cb8fa2a94f56" + }, + { + "path": "research/p104-helper-subspace-splits/WORD.json.gz", + "usage": "input", + "git_blob": "e325091e3051afe37a2d9c82f85afe9028510edb", + "sha256": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099" + } + ] +} diff --git a/research/p104-stochastic-prefix/TASK.json b/research/p104-stochastic-prefix/TASK.json new file mode 100644 index 0000000000..3f7924482a --- /dev/null +++ b/research/p104-stochastic-prefix/TASK.json @@ -0,0 +1,111 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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 stochastic-roundoff influence certificate and arbitrary-input tail theorem for the selected P104 first common-frame scalar block.", + "scope_change_reason": "Investigate a changed precision model rather than audit a predecessor: fresh unbiased fixed-grid rounding at scalar macro boundaries, stopping before any MOVE.", + "bottleneck_link": "Scoped precision_tape component on the binding complex supplier. It supplies a local probabilistic enclosure; exact restoration and full randomized cost/admission are not supplied.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact source-bound stochastic precision certificate; do not extend to later blocks or chase a stronger probability.", + "outcome": "completed", + "evidence": "Exact reverse integer-column and independent forward formal-error engines; exhaustive tiny stochastic distributions; rational positive-Taylor tail certificate.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a complete native caller exploit stochastic precision while restoring arbitrary dirty state exactly?", + "why_it_matters": "An intermediate high-probability error bound alone cannot satisfy the selected caller cleanup contract.", + "first_step": "Choose one native round-and-restore interface, expose the retained random bits and price their preparation, reversal and erasure.", + "blocked_by": "No physical reversible randomized arithmetic ABI or whole-call cost is supplied." + }, + { + "question": "What precision and failure budget suffices across every sample and every later native block?", + "why_it_matters": "The present bound covers one common-frame prefix at a fixed sample.", + "first_step": "Specify one finite sample count and propagate its output errors through an actual next MOVE with its own error contract.", + "blocked_by": "Native approximation and stream-wide failure allocation remain unspecified." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228531", + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "priority_revision": 8, + "question_source": "original", + "checks": "Live open PRs, account history, handoffs, active Discussions, reservations, main README and distinctive merged-PR searches. Sparse local cache coverage is incomplete; no global novelty assertion." + }, + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + }, + "local_validation": { + "normal_and_optimized": "passed", + "registered": "passed", + "git_free_optimized": "passed", + "source_corruption": "rejected", + "source_binding_orientation": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "scientific_replay": "not run", + "CI": "pending" + } +} diff --git a/research/p104-stochastic-prefix/VERIFY.json b/research/p104-stochastic-prefix/VERIFY.json new file mode 100644 index 0000000000..6d6db95620 --- /dev/null +++ b/research/p104-stochastic-prefix/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper-subspace-splits/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-X", + "dev", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact full outputwise influence agreement, stochastic distribution enumeration, source authentication, semantic controls and rational tail certificate." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-X", + "dev", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact full outputwise influence agreement, stochastic distribution enumeration, source authentication, semantic controls and rational tail certificate." + } + ] +} diff --git a/research/p104-stochastic-prefix/verify.py b/research/p104-stochastic-prefix/verify.py new file mode 100644 index 0000000000..9d5daac125 --- /dev/null +++ b/research/p104-stochastic-prefix/verify.py @@ -0,0 +1,267 @@ +#!/usr/bin/env python3 +"""Exact stochastic-roundoff certificate, produced by Nick Petalas. Apache-2.0.""" +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import product +from pathlib import Path +import gzip +import io +import json + +HERE = Path(__file__).resolve().parent +SOURCE = 'research/p104-helper-subspace-splits/WORD.json.gz' +FILES = ('README.md', 'PROOF.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', 'verify.py') + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def bounded_read(path, limit): + with path.open('rb') as stream: + raw = stream.read(limit + 1) + need(len(raw) <= limit, 'file capacity') + return raw + + +def prefix(word): + need(type(word) is dict and word.get('schema') == 'p104-productive-source/1', 'schema') + n = word.get('public') + need(type(n) is int and n == 748, 'public dimension') + events = word.get('program') + need(type(events) is list and 0 < len(events) <= 26000, 'program capacity') + cut = next((i for i, e in enumerate(events) if e and e[0] == 'MOVE'), None) + need(cut is not None and cut == 9589, 'first native boundary') + need(word['frames'][3] == [], 'empty common frame') + answer = [] + for e in events[:cut]: + need(type(e) is list and e[0] in ('ADD', 'SCALE'), 'scalar opcode') + need(len(e) == (5 if e[0] == 'ADD' else 4), 'event shape') + need(type(e[1]) is int and 0 <= e[1] < n and e[-1] == 3, 'destination/chart') + if e[0] == 'ADD': + need(type(e[2]) is int and 0 <= e[2] < n and e[1] != e[2], 'source') + need(type(e[-2]) is str, 'exact coefficient text') + q = Q(e[-2]) + need(q and q.denominator in (1, 2, 4) and abs(q) <= 16, 'dyadic coefficient') + answer.append((e[0], e[1], e[2] if e[0] == 'ADD' else None, q)) + return n, answer + + +def source_prefix(): + pins = json.loads(bounded_read(HERE / 'SOURCES.json', 65536))['files'] + pin = [row for row in pins if row['path'] == SOURCE] + need(len(pin) == 1 and pin[0]['usage'] == 'input', 'unique live word pin') + raw = bounded_read(HERE.parents[1] / SOURCE, 1 << 20) + need(sha256(raw).hexdigest() == pin[0]['sha256'], 'source SHA256') + with gzip.GzipFile(fileobj=io.BytesIO(raw)) as stream: + unpacked = stream.read((1 << 22) + 1) + need(len(unpacked) <= 1 << 22, 'unpacked capacity') + n, events = prefix(json.loads(unpacked)) + return n, events, sha256(raw).hexdigest() + + +def normalized(values, exponent): + need(0 <= exponent <= 64, 'dyadic exponent capacity') + for _ in range(exponent): + if any(x & 1 for x in values): + break + values = [x // 2 for x in values] + exponent -= 1 + need(all(abs(x).bit_length() <= 128 for x in values), 'numerator capacity') + return values, exponent + + +def reverse_influences(n, events): + """Propagate output coefficient columns through transposed updates.""" + need(1 <= n <= 748 and len(events) <= 10000, 'reverse capacity') + columns = [[int(i == j) for i in range(n)] for j in range(n)] + powers, squares, absolute = [0] * n, [0] * n, [0] * n + common = 0 + for op, r, s, q in reversed(events): + qe = q.denominator.bit_length() - 1 + if qe: + exponent, v = powers[r], columns[r] + if exponent > common: + squares = [x << (2 * (exponent - common)) for x in squares] + absolute = [x << (exponent - common) for x in absolute] + common = exponent + squares = [x + (y*y << (2*(common-exponent))) for x, y in zip(squares, v)] + absolute = [x + (abs(y) << (common-exponent)) for x, y in zip(absolute, v)] + if op == 'SCALE': + columns[r], powers[r] = normalized([q.numerator*x for x in columns[r]], powers[r]+qe) + else: + level = max(powers[s], powers[r] + qe) + a = 1 << (level - powers[s]) + b = q.numerator << (level - powers[r] - qe) + v = [a*x + b*y for x, y in zip(columns[s], columns[r])] + columns[s], powers[s] = normalized(v, level) + return ([Q(x, 1 << (2*common)) for x in squares], + [Q(x, 1 << common) for x in absolute]) + + +def forward_influences(n, events): + """Independent chronological propagation of formal injected errors.""" + need(1 <= n <= 748 and len(events) <= 10000, 'forward capacity') + rows = [{} for _ in range(n)] + for t, (op, r, s, q) in enumerate(events): + if op == 'SCALE': + rows[r] = {k: q*v for k, v in rows[r].items()} + else: + for k, v in tuple(rows[s].items()): + value = rows[r].get(k, 0) + q*v + if value: + rows[r][k] = value + else: + rows[r].pop(k, None) + if q.denominator > 1: + rows[r][t] = Q(1) + need(len(rows[r]) <= 10000, 'formal error capacity') + need(all(abs(v.numerator).bit_length() <= 128 and + v.denominator.bit_length() <= 65 for v in rows[r].values()), + 'formal coefficient capacity') + squares = [sum((v*v for v in row.values()), Q(0)) for row in rows] + absolute = [sum(map(abs, row.values()), Q(0)) for row in rows] + return squares, absolute, sum(map(len, rows)), max(map(len, rows)) + + +def exact_run(initial, events): + state = list(map(Q, initial)) + for op, r, s, q in events: + state[r] = q*state[r] if op == 'SCALE' else state[r] + q*state[s] + return state + + +def distribution(initial, events): + """Enumerate the genuine conditional probabilities, with fresh draws.""" + need(len(initial) <= 3 and len(events) <= 8, 'enumeration capacity') + states = {tuple(initial): Q(1)} + for op, r, s, q in events: + out = {} + for state, mass in states.items(): + value = q*state[r] if op == 'SCALE' else state[r] + q*state[s] + lo = value.numerator // value.denominator + theta = value - lo + for rounded, probability in ((lo, 1-theta), (lo+1, theta)): + if probability: + target = list(state) + target[r] = rounded + key = tuple(target) + out[key] = out.get(key, 0) + mass*probability + need(len(out) <= 256, 'distribution state capacity') + states = out + need(sum(states.values()) == 1, 'probability conservation') + return states + + +def probability_checks(): + fixtures = [ + [('ADD', 0, 1, Q(1, 2))]*2, + [('SCALE', 0, None, Q(1, 2)), ('ADD', 1, 0, Q(-1, 4)), + ('SCALE', 1, None, Q(-2)), ('ADD', 0, 1, Q(3, 4))], + [('ADD', 0, 1, Q(1, 4)), ('ADD', 1, 0, Q(-1, 2))]*3, + [('ADD', 0, 1, Q(2)), ('SCALE', 1, None, Q(-1))], + [('ADD', 0, 1, Q(1, 2)), ('ADD', 0, 1, Q(-1, 2))], + ] + cases = endpoints = 0 + for events in fixtures: + square, absolute = reverse_influences(2, events) + forward = forward_influences(2, events) + need((square, absolute) == forward[:2], 'small complete influence agreement') + for initial in product(range(-2, 3), repeat=2): + exact = exact_run(initial, events) + states = distribution(initial, events) + endpoints += len(states) + for j in range(2): + mean = sum((mass*state[j] for state, mass in states.items()), Q(0)) + variance = sum((mass*(state[j]-exact[j])**2 for state, mass in states.items()), Q(0)) + need(mean == exact[j] and variance <= square[j]/4, 'unbiasedness/variance') + cases += 1 + return cases, endpoints + + +def controls(events, squares, absolute): + # Exercise actual structural and numeric gates without mutating frozen bytes. + for case in range(5): + rejected = False + try: + if case == 0: + prefix({}) + elif case == 1: + prefix({'schema': 'p104-productive-source/1', 'public': True}) + elif case == 2: + reverse_influences(749, []) + elif case == 3: + normalized([1], 65) + else: + normalized([1 << 129], 0) + except (ValueError, KeyError, TypeError): + rejected = True + need(rejected, 'negative control accepted') + changed = list(events) + index = next(i for i, e in enumerate(changed) if e[3].denominator > 1) + op, r, s, q = changed[index] + changed[index] = (op, r, s, q*2) + need(reverse_influences(748, changed) != (squares, absolute), 'coefficient sensitivity') + need(reverse_influences(748, list(reversed(events))) != (squares, absolute), 'chronology sensitivity') + tiny = [('ADD', 0, 1, Q(1, 2))]*2 + variance_bound = reverse_influences(2, tiny)[0][0]/4 + # A reused coin gives error -1 or +1, violating the fresh-noise bound 1/2. + errors = [Q(2*bit)-exact_run((0, 1), tiny)[0] for bit in range(2)] + variance = sum(e*e for e in errors)/2 + need(sum(errors) == 0 and variance > variance_bound == Q(1, 2), + 'shared randomness rejection witness') + need(exact_run((0, 1), tiny)[0] == 1, 'exact half-add fixture') + # Always rounding both ties down gives output zero, hence bias -1. + need(0 - exact_run((0, 1), tiny)[0] == -1, 'biased tie rejection witness') + return 9 + + +def tail_certificate(maximum, active): + need(maximum == Q(733, 8) and active == 282, 'fixed maximum/domain') + x = Q(2*32**2, 1) / maximum + term = total = Q(1) + for k in range(1, 65): + term *= x/k + total += term + upper = 2*active/total + need(upper < Q(1, 1 << 23), 'rational exponential certificate') + return {'exponent': str(x), 'positive_taylor_terms': 65, + 'failure_bound_strictly_below': '1/8388608', + 'taylor_sum_sha256': sha256(str(total).encode()).hexdigest()} + + +def main(): + n, events, source_hash = source_prefix() + squares, absolute = reverse_influences(n, events) + f_square, f_absolute, entries, support = forward_influences(n, events) + need((squares, absolute) == (f_square, f_absolute), 'all output influence agreement') + need(max(squares) == Q(733, 8) and max(absolute) == 90, 'computed maxima') + active = sum(value > 0 for value in squares) + noisy = sum(q.denominator > 1 for _, _, _, q in events) + bits = sum(q.denominator.bit_length()-1 for _, _, _, q in events) + need(noisy == 7421 and bits == 11713, 'rounded update/random-bit census') + cases, endpoints = probability_checks() + rejects = controls(events, squares, absolute) + receipt = {'status': 'PASS_P104_STOCHASTIC_PREFIX', 'public': n, + 'events': len(events), 'potential_rounds': noisy, 'fresh_bits_upper': bits, + 'add_events': sum(e[0] == 'ADD' for e in events), + 'scale_events': sum(e[0] == 'SCALE' for e in events), + 'touched_roles': len({e[1] for e in events} | {e[2] for e in events if e[0] == 'ADD'}), + 'source_word_sha256': source_hash, + 'active_outputs': active, 'max_squared_influence': str(max(squares)), + 'squared_max_roles': [i for i, x in enumerate(squares) if x == max(squares)], + 'max_absolute_influence': str(max(absolute)), + 'absolute_max_roles': [i for i, x in enumerate(absolute) if x == max(absolute)], + 'total_squared_influence': str(sum(squares)), + 'formal_nonzero_coefficients': entries, 'max_formal_row_support': support, + 'probability_fixtures': cases, 'enumerated_endpoints': endpoints, + 'controls': rejects, 'tail': tail_certificate(max(squares), active), + 'outputwise': [{'squared': str(s), 'absolute': str(a)} for s, a in zip(squares, absolute)], + 'package_sha256': {name: sha256(bounded_read(HERE/name, 1 << 20)).hexdigest() for name in FILES}} + print(json.dumps(receipt, sort_keys=True)) + print('PASS_P104_STOCHASTIC_PREFIX no_new_kappa') + + +if __name__ == '__main__': + main()