From 08f0609cc997da02944cf5517eba1aa954665050 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 22:24:38 +0000 Subject: [PATCH] feat(research): bound once-rounded rational gate temporaries --- research/integer-rounded-gate/PROOF.md | 152 ++++++++++++++ research/integer-rounded-gate/README.md | 131 ++++++++++++ research/integer-rounded-gate/SOURCES.json | 48 +++++ research/integer-rounded-gate/TASK.json | 110 ++++++++++ research/integer-rounded-gate/VERIFY.json | 40 ++++ research/integer-rounded-gate/kernel.py | 112 +++++++++++ research/integer-rounded-gate/verify.py | 224 +++++++++++++++++++++ 7 files changed, 817 insertions(+) create mode 100644 research/integer-rounded-gate/PROOF.md create mode 100644 research/integer-rounded-gate/README.md create mode 100644 research/integer-rounded-gate/SOURCES.json create mode 100644 research/integer-rounded-gate/TASK.json create mode 100644 research/integer-rounded-gate/VERIFY.json create mode 100644 research/integer-rounded-gate/kernel.py create mode 100644 research/integer-rounded-gate/verify.py diff --git a/research/integer-rounded-gate/PROOF.md b/research/integer-rounded-gate/PROOF.md new file mode 100644 index 0000000000..6909bff0ab --- /dev/null +++ b/research/integer-rounded-gate/PROOF.md @@ -0,0 +1,152 @@ +# A smaller arithmetic width for once-rounded rational gates + +This scoped construction and proof were produced by Nick Petalas. Apache-2.0. + +## Statement + +Let B>=2 and C>=1 be integers. Four signed input grid numerators X_j satisfy + + -2^(B-1) <= X_j < 2^(B-1), 0<=j<4. + +A rational row has coefficients p_j/d_j, with integer p_j and d_j such that + + |p_j| < 2^C, 1 <= d_j < 2^C. + +The coefficients need not be reduced. There is a constant-word arithmetic +program that computes + + floor(sum_j (p_j/d_j) X_j + 1/2) + +with every signed data-arithmetic temporary fitting + + W = B + 4C + 2 bits. (1) + +The program uses shifts, bit tests, addition, subtraction and comparisons. +Multiplication and division below are implemented by bounded binary loops. +They are not assumed machine instructions. Four applications to saved inputs +implement any two-coordinate Gaussian rational matrix gate, rounding each +real and imaginary output once with ties toward positive infinity. + +This is an upper bound, not a minimum-width theorem. It concerns arithmetic +words after coefficients and input data are supplied. No reversible circuit, +bit-tape running time, memory layout or coefficient-preparation bound follows. + +## Common-denominator accumulation + +Set + + D = product_j d_j, + N_j = p_j X_j product_(k!=j) d_k, + S = sum_j N_j. + +Compute D by four successive products starting from one. Compute each N_j +from p_j X_j and then the three other denominators. Accumulate its exact +integer value before proceeding to the next term. No product is rounded. + +We have + + 1 <= D < 2^(4C), + |N_j| < 2^(B+4C-1), + |sum_(j in J) N_j| < 4 * 2^(B+4C-1) = 2^(W-1) (2) + +for every partial sum occurring in this fixed four-term order. The bound +uses |X_j|<=2^(B-1), including the most negative B-bit input. Strictness +comes from the four coefficient numerator/denominator factors, each strictly +below 2^C. Signs and cancellation are unrestricted. + +Each nonzero partial product has magnitude at most the corresponding full +product: every remaining denominator is at least one. A zero numerator +remains zero. All these intermediate values fit (1), by (2). D and its +partial products fit as well. The exact rational row value is S/D. + +For signed multiplication, retain the result sign and use unsigned +magnitudes. Scan the multiplier's binary digits from low to high, adding +the shifted multiplicand when a digit is one. Every shifted multiplicand +and every partial sum is at most the full magnitude product. Hence the +same word bound applies to the shift/add implementation, including its +positive magnitude words. None of these constructed products is the most +negative W-bit integer, so taking its absolute value is safe. + +## Division and signed ties + +Put t=|S|. Binary long division scans exactly W-1 positions of t, from +most significant to least significant. Maintain a quotient prefix q and +remainder r. At each position with digit b, replace + + r by 2r+b, + q by 2q, + if r>=D, subtract D from r and add one to q. + +The ordinary prefix-division induction proves that the final pair satisfies +t=qD+r and 0<=r=2, this is below 2^(W-1). +Each quotient prefix is at most the final quotient, which is at most t. +The shifted quotient prefix before its next digit is no larger than the +next completed quotient prefix. Thus every quotient and remainder word +fits (1). The Python helper enforces the sufficient additional contract +D<2^(W-2), which holds here by the stronger D<2^(4C). + +The final rounded integer is + + q + [2r>=D], if S>=0, + -q - [2r>D], if S<0. (3) + +For S>=0, this is floor(q+r/D+1/2). For S<0, it is +floor(-q-r/D+1/2). The strict inequality in the negative branch is +essential: -1/2 rounds to zero. The positive halfway value 1/2 rounds to +one. The word 2r is below 2D, so its comparison is also safe. + +If D=1, r=0 and rounding changes nothing. If D>=2 and t>=1, the rounded +result's magnitude is at most q+1<=t. At t=0 it is zero. Therefore the +final result also fits W signed bits. Equations (2) and (3), rather than +finite extrapolation, prove the all-B, all-C construction. + +## Complex gates, input snapshots and the cited allowance + +For a complex row a_0 z_0+a_1 z_1, expand its real and imaginary parts +using the four real input coordinates. Each real row has exactly four +rational coefficients, with signs but no increased component height. +If the inputs are 2^-F X_j, multiplying a rounded output by 2^F gives +exactly the integer expression above. The arithmetic bound depends on +B=F+I, not separately on F. The input grid cancels before arithmetic. + +Save all four inputs, compute all four output integers, then overwrite +the four stored coordinates. This gives the same saved-input, +exact-local-sum, once-per-output rounding contract as Jose Manuel's +`rational-unitary-fft/exact.py:apply`. Armin Pourshafeie's PR5240 asks for +such a concrete arithmetic implementation. Its layer and stored-state +theorems are cited premises, not re-proved or audited here. + +The same source's `engine.py:certificate` and FULL-PROOF.md use the +conservative temporary allowance + + 2F + 8C + 2I + 32 = 2B + 8C + 32. + +The new arithmetic construction uses + + B + 4C + 2 = (2B + 8C + 32)/2 - 14. (4) + +This reduces a sufficient maximum arithmetic-word width. It does not +establish a reduction in total live bits, elapsed time or a complete +caller's allocation. Output data still need that caller's independent +amplitude bound before they can be stored back in B bits. The kernel +permits W-bit outputs and makes no unconditional B-bit output claim. + +## One source-produced butterfly + +The verifier calls the retained `Phases(4, source)` and +`Builder.butterfly` with the exact phase i. They produce + + [ 13575/19193, 13568 i/19193 ] + [ 13568/19193, -13575 i/19193 ]. + +The maximum component height is C=15. For B=18, the new bound is 80 bits. +Evaluating the cited allowance at these same parameters gives 188 bits. +This comparison does not assert that a complete source caller selected +C=15 or allocated an 188-bit word. It is a same-parameter comparison of +two sufficient formulas. Actual coefficient production is used to supply +this finite fixture; its approximation theorem is not an audit target. + +The independent Fraction oracle, source executor comparisons, large-height +fixtures and controls corroborate the implementation. They do not replace +the proof or establish any physical supplier or multiplication theorem. diff --git a/research/integer-rounded-gate/README.md b/research/integer-rounded-gate/README.md new file mode 100644 index 0000000000..80e8ae627e --- /dev/null +++ b/research/integer-rounded-gate/README.md @@ -0,0 +1,131 @@ +# Once-rounded rational gates with smaller arithmetic words + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped arithmetic construction and written proof with exact +finite corroboration. A two-coordinate Gaussian rational gate can compute +each output with one final nearest rounding, using signed arithmetic words +of width B+4C+2. Here B is the signed input-numerator width, and C bounds +the bit length of every coefficient component's numerator magnitude and +positive denominator. B>=2 and C>=1; the input fractional grid is arbitrary. + +The cited rational FFT/Full allowance is 2B+8C+32. The new sufficient width +is half that allowance minus fourteen bits. [PROOF.md](PROOF.md) proves the +all-width bound by four-term common-denominator accumulation and bounded +binary multiplication/division. [kernel.py](kernel.py) implements it with +integer shifts, tests, additions, subtraction and comparisons. It uses no +machine multiplication/division instruction or intermediate rounding. +All four real inputs are saved before output writes. + +This answers the arithmetic question left open by Armin Pourshafeie in +[PR5240](https://github.com/CrocSwap/integer-mult-bounds/pull/5240). +The result is a new implementation and resource bound, not an audit of the +predecessor's rounded-layer theorem. No new kappa or selected-frontier +change is claimed. The bound is sufficient, not proved minimal. + +## Evidence and reproduction + +The exact finite checks cover 50,625 four-term rows, 3,600 two-term rows, +31,744 binary divisions, 50 large-height rows and 768 complete complex-gate +cases. Eight semantic checks distinguish signed ties, product rounding and +input overwrite. Seventeen invalid-domain/overflow requests reject. +The largest tested data/coefficient widths are 2048 and 256 bits. +The word observer checks arithmetic intermediates at each operation. + +The retained phase factory at precision four supplies an actual butterfly +with component height fifteen. For B=18, our construction uses 80-bit +temporaries; the cited formula evaluated at those same parameters gives +188 bits. This does not assert a particular full caller allocated 188 bits. +The verifier compares all four rounded output components with the retained +saved-input executor, on three grids and all 256 stated input combinations. + +From the repository root, standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/integer-rounded-gate/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/integer-rounded-gate/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/integer-rounded-gate +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/integer-rounded-gate --check-source-history --check-modes +``` + +Other machines can substitute their CPython 3.12 path. Both registered +commands have a 120-second cap. The direct marker is +`PASS_INTEGER_ROUNDED_GATE`. Its generated stdout receipt binds every +package file by SHA256. Verification writes no package files. No receipt +is handwritten or committed. Source pins and the complete originating +card are in [SOURCES.json](SOURCES.json) and [TASK.json](TASK.json). + +## Scope and credit + +The theorem concerns arithmetic data words, given supplied coefficients. +The executable accepts 2<=B<=2048 and 1<=C<=256. Its word observer uses +host arithmetic to detect overflow; it is not a physical machine emitter. +Output values fit W=B+4C+2 bits. Returning them to B-bit data storage still +requires the caller's separate amplitude contract. No total-live-storage, +runtime or bit-tape improvement is claimed. + +Coefficient preparation, its local temporaries, reversible cleanup, actual +instruction encoding, tape movement, all-size compiler funding and supplier +admission remain open. All five selected framework assumptions remain. +No selected scientific replay, native/Lean/Docker build, independent human +review or proof-kernel acceptance is claimed. + +Credit Armin Pourshafeie / apoursh for PR5240's explicit arithmetic seam; +Jose Manuel / jmbarrancoml for the rational executor, phase producer and +coefficient/temporary contracts; Vlado Vojdanovski for the schedule; +Chafik Boukhalfa for phases; Brian / JoyboyBrian and James Reed for the +retained cut/allocator work; Cinna Davis and the numerical/compiler lineage. +Common-denominator arithmetic, long multiplication/division and nearest +rounding are classical. Nick Petalas's PR5940 concerns conditioned operator +interpolation; that theorem and its follow-up question are not extended. +Predecessor files and their credit lines remain unchanged. + +Base is canonical main 7c49fe32c55de02c2c873655c804b16e4c3fef0a, +priority revision eight, selected PR6030. The source-binding baseline passed. +The supplier-boundary-audit card explicitly changes to this constructive +arithmetic side result, because a missing local kernel separates stored-state +bounds from an implementation. This does not change a supplier family or +admit a new one. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361639) +reserves the same scope. + +Live claims, local reservations, open/account PRs, main formula/object +searches, merged searches and the cached card report were checked. The +cache covered 370 open PRs and 6,284 Discussion records, with complete +remote pagination. Its sparse local corpus covered 115 of 8,917 notes; +relevant packages were materialized and main README searches supplemented +it. Arbitrary historical diffs and unpublished work remain coverage limits. + +## Open next questions + +Bind this kernel to one complete Full allocation and charge its exact live +word count, source snapshots, output staging, bit operations, cleanup and +tape movement. Start from one emitted two-wire call and its proved input +and output amplitude bounds. A physical arithmetic/ownership contract and +the complete caller invoice remain missing. The present maximum word width +does not settle those costs. No further optimization is reserved. + +## Code constraints + +Foundational Thinking fixes grid numerators and coefficient pairs before +arithmetic. Build the Lever supplies the retained kernel and independent +Fraction oracle. Prove It Works requires actual source-produced gate +conformance, overflow checks and rejection controls. + +All new functions fit sixty lines. There is no recursion or generated code +in the new kernel. Each multiplication scans at most W-1 multiplier bits; +each division scans exactly W-1 positions; W<=3074. Gate loops have four +iterations. Fixed finite verification domains bound all other loops. +Explicit exceptions retain checks under optimized Python. + +Power of Ten rule 3 deviation: CPython allocates integers and containers +during this bounded reference execution. Fixed B,C limits, four-coordinate +state and one current row bound the kernel's live collections. A static +memory backend is needed before a fixed-allocation claim. The width +observer's capacity and operation counters are verification metadata outside the +claimed data-word program. Rule 8/9 fixture deviation: the unchanged phase +factory executes its authenticated interval source; imports and dispatch +are limited to the five declared inputs and their standard-library imports. +Its preparation is outside the arithmetic-width theorem. The 120-second +registered timeout also bounds this finite fixture. Warning-strict normal +and optimized replay and AST/function-size checks supply local diagnostics; +no separate type analyzer or linter is claimed. diff --git a/research/integer-rounded-gate/SOURCES.json b/research/integer-rounded-gate/SOURCES.json new file mode 100644 index 0000000000..d32aacea72 --- /dev/null +++ b/research/integer-rounded-gate/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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/cubic-cyclic-inverse/vendor/interval_kernel.py", + "usage": "input", + "git_blob": "1182175a55cb871481de0f56ea9ae56e474705fe", + "sha256": "9b7bb24640a9a7d3f83c7951dfef483ec933db4c50de6c0130b85f450eeddfbe" + }, + { + "path": "research/matching-layer-rounding/README.md", + "usage": "input", + "git_blob": "99f648abd626c91312ae03dffc41bf307a33176a", + "sha256": "ba0225a7af7aa7547d719831f3122c02af09bd56ae32eb45aecccb2e66d8cbdb" + }, + { + "path": "research/rational-unitary-fft/FULL-PROOF.md", + "usage": "input", + "git_blob": "e650f46863115f810e27b403f916dd7f79b37786", + "sha256": "acf8c596d91b5efd35a286735d6867ff8afce64354a13f680c2fae3dab824410" + }, + { + "path": "research/rational-unitary-fft/engine.py", + "usage": "input", + "git_blob": "e9f2f2b08dc2bc4c646e47dca92059351ca89384", + "sha256": "9e36aee0835e6b1b62997433581f88b5a434ccab8ae43e5c25d1deaaf1ebf653" + }, + { + "path": "research/rational-unitary-fft/exact.py", + "usage": "input", + "git_blob": "aae41e6acfb2e5a4fafdd85727891eb746b57b42", + "sha256": "c9b89d7357210af69865690ba12e695366961f8b501a8fab9d0fefe3fb30c479" + } + ] +} diff --git a/research/integer-rounded-gate/TASK.json b/research/integer-rounded-gate/TASK.json new file mode 100644 index 0000000000..3bddd95b97 --- /dev/null +++ b/research/integer-rounded-gate/TASK.json @@ -0,0 +1,110 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one changed supplier have complete source-bound native, caller, ordinary and outer admission coverage?", + "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": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "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 latest uncovered candidate and build a delta coverage map against the selected review. For P104, #5717 changes owned-lifetime assumptions and #5719 covers exact #5713 causal premises; neither automatically transfers to #5718. For BIT, #5679/#5708 need component admission and compatible outer use. Check controls and exact source identity before reuse; stop with one resolved gap or explicit remaining obligation. A heavy full replay requires a separate serial resource budget.", + "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": [ + "supplier admission", + "5717", + "5719", + "5708", + "owned lifetime" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "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": "Construct a once-rounded two-coordinate Gaussian rational gate using B+4C+2-bit signed integer arithmetic temporaries, including a concrete retained butterfly.", + "scope_change_reason": "Answer PR5240 arithmetic Open next question with an original implementation and width theorem. This is a constructive precision-boundary side result, not an audit or supplier-admission decision.", + "bottleneck_link": "The source stored-grid theorem assumes exact local products/sums and bounded temporaries. This supplies a smaller sufficient arithmetic width, while physical implementation, preparation and complete supplier costs remain open.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved width improvement with exact conformance and rejection evidence; do not optimize the bound or extend to a full caller.", + "outcome": "completed", + "evidence": "PROOF.md proves the all-B,C construction. kernel.py uses checked binary arithmetic; verify.py supplies Fraction and source-produced butterfly conformance, signed ties, input-snapshot and domain/overflow controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one complete Full allocation use this kernel with a fully priced physical arithmetic and ownership contract?", + "why_it_matters": "A smaller maximum arithmetic-word width alone does not reduce a complete supplier invoice.", + "first_step": "Select one emitted two-wire call; derive its input/output amplitude bounds and count live snapshots, output staging, bit operations, cleanup and movement.", + "blocked_by": "Physical backend, exact live-word and tape costs, and the complete caller invoice." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361639", + "source_question": { + "pr": 5240, + "author": "apoursh", + "head": "6d0a6043120880c696d0850e9242a16e6fb980a5", + "scope": "Open next question on bounded-word two-coordinate multiply/add/round arithmetic." + }, + "claim_type": "scoped arithmetic construction and proof with exact finite corroboration", + "environment": { + "python": "CPython 3.12.15", + "dependencies": "standard library", + "platform": "Darwin 27.0.0 arm64" + }, + "limitations": [ + "No optimality, total-storage, runtime or bit-tape improvement claim.", + "No physical instruction emitter, reversible cleanup or coefficient-preparation proof.", + "No complete Full allocation, supplier admission, new kappa or selected-frontier change.", + "All five framework assumptions remain; no independent human or formal proof-kernel acceptance." + ] +} diff --git a/research/integer-rounded-gate/VERIFY.json b/research/integer-rounded-gate/VERIFY.json new file mode 100644 index 0000000000..1c7b65b6dd --- /dev/null +++ b/research/integer-rounded-gate/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/cubic-cyclic-inverse/vendor/interval_kernel.py", + "research/matching-layer-rounding/README.md", + "research/rational-unitary-fft/FULL-PROOF.md", + "research/rational-unitary-fft/engine.py", + "research/rational-unitary-fft/exact.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New width/rounding construction, exact rational oracle, actual source butterfly conformance and semantic/domain/overflow controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New width/rounding construction, exact rational oracle, actual source butterfly conformance and semantic/domain/overflow controls." + } + ] +} diff --git a/research/integer-rounded-gate/kernel.py b/research/integer-rounded-gate/kernel.py new file mode 100644 index 0000000000..45ffe0f280 --- /dev/null +++ b/research/integer-rounded-gate/kernel.py @@ -0,0 +1,112 @@ +"""Once-rounded four-term rows with bounded signed integer arithmetic. + +Produced by Nick Petalas. Apache-2.0. +""" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +class Words: + """A width observer; its capacity constants are outside the data program.""" + + def __init__(self, width): + require(type(width) is int and 8 <= width <= 3074, "word capacity") + self.width = width + self.peak = 0 + self.operations = 0 + + def check(self, value): + require(type(value) is int, "integer word") + limit = 1 << (self.width - 1) + if not -limit <= value < limit: + raise OverflowError("signed word overflow") + self.peak = max(self.peak, abs(value).bit_length() + 1) + self.operations += 1 + return value + + def multiply(self, left, right): + """Shift/add multiplication; no integer multiplication instruction.""" + self.check(left) + self.check(right) + negative = (left < 0) != (right < 0) + term, digits = self.check(abs(left)), self.check(abs(right)) + result = 0 + for bit in range(digits.bit_length()): + if (digits >> bit) & 1: + result = self.check(result + term) + if bit + 1 < digits.bit_length(): + term = self.check(term << 1) + return self.check(-result if negative else result) + + def divide(self, numerator, denominator): + """Unsigned binary division, using a fixed number of bit positions.""" + require(numerator >= 0 and denominator > 0, "division domain") + require(denominator < (1 << (self.width - 2)), "division remainder capacity") + self.check(numerator) + self.check(denominator) + quotient = remainder = 0 + for bit in range(self.width - 2, -1, -1): + remainder = self.check((remainder << 1) + ((numerator >> bit) & 1)) + quotient = self.check(quotient << 1) + if remainder >= denominator: + remainder = self.check(remainder - denominator) + quotient = self.check(quotient + 1) + require(0 <= remainder < denominator, "division remainder invariant") + return quotient, remainder + + +def validate(rows, state, data_bits, coefficient_bits): + require(type(data_bits) is int and 2 <= data_bits <= 2048, "data width") + require(type(coefficient_bits) is int and 1 <= coefficient_bits <= 256, + "coefficient width") + require(type(rows) in (tuple, list), "row collection") + require(len(state) == 4 and len(rows) == 4, "four real coordinates") + limit = 1 << (data_bits - 1) + require(all(type(x) is int and -limit <= x < limit for x in state), + "signed input numerators") + for row in rows: + require(type(row) in (tuple, list), "row representation") + require(len(row) == 4, "four terms per row") + for pair in row: + require(type(pair) is tuple and len(pair) == 2, "rational pair") + numerator, denominator = pair + require(type(numerator) is int and type(denominator) is int, + "integer rational components") + require(abs(numerator).bit_length() <= coefficient_bits + and 0 < denominator < (1 << coefficient_bits), + "coefficient height") + + +def rounded_row(row, state, words): + denominator = 1 + for _, divisor in row: + denominator = words.multiply(denominator, divisor) + accumulator = 0 + for term_index in range(4): + numerator = words.multiply(row[term_index][0], state[term_index]) + for divisor_index in range(4): + if divisor_index != term_index: + numerator = words.multiply(numerator, row[divisor_index][1]) + accumulator = words.check(accumulator + numerator) + quotient, remainder = words.divide(words.check(abs(accumulator)), denominator) + twice_remainder = words.check(remainder << 1) + if accumulator < 0: + result = -quotient - int(twice_remainder > denominator) + else: + result = quotient + int(twice_remainder >= denominator) + return words.check(result) + + +def apply_gate(rows, state, data_bits, coefficient_bits): + """Overwrite four grid numerators after all outputs have been computed.""" + require(type(state) is list, "mutable four-coordinate state") + validate(rows, state, data_bits, coefficient_bits) + words = Words(data_bits + 4 * coefficient_bits + 2) + before = tuple(state) + outputs = [rounded_row(row, before, words) for row in rows] + for index in range(4): + state[index] = outputs[index] + return words diff --git a/research/integer-rounded-gate/verify.py b/research/integer-rounded-gate/verify.py new file mode 100644 index 0000000000..6da494b004 --- /dev/null +++ b/research/integer-rounded-gate/verify.py @@ -0,0 +1,224 @@ +"""Exact finite evidence for the new bounded arithmetic kernel. + +Produced by Nick Petalas. Apache-2.0. +""" + +import ast +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +sys.path.insert(0, str(PACKAGE)) +from kernel import Words, apply_gate, require, rounded_row + + +def authenticate(): + source_manifest = PACKAGE / "SOURCES.json" + require(source_manifest.stat().st_size <= 1048576, "source manifest capacity") + manifest = json.loads(source_manifest.read_text()) + require(len(manifest["files"]) == 7, "source inventory capacity") + inputs = [item for item in manifest["files"] if item["usage"] == "input"] + require(len(inputs) == 5, "declared source closure") + for item in inputs: + path = ROOT / item["path"] + require(path.stat().st_size <= 1048576, "source file capacity") + require(sha256(path.read_bytes()).hexdigest() == item["sha256"], + "source digest: " + item["path"]) + return len(inputs) + + +def literal_round(value): + shifted = value + Fraction(1, 2) + return shifted.numerator // shifted.denominator + + +def oracle(row, state): + return literal_round(sum((Fraction(*pair) * x for pair, x in zip(row, state)), + Fraction(0))) + + +def row_cases(): + alphabet = [(-1, 1), (-1, 2), (0, 1), (1, 2), (1, 1)] + cases = 0 + max_peak = 0 + for row in product(alphabet, repeat=4): + for state in product((-2, 0, 1), repeat=4): + words = Words(12) + actual = rounded_row(row, state, words) + require(actual == oracle(row, state), "four-term exact rounding") + require(words.peak <= 12, "four-term width") + max_peak = max(max_peak, words.peak) + cases += 1 + return cases, max_peak + + +def two_term_cases(): + alphabet = sorted({Fraction(a, d) for a in range(-3, 4) for d in range(1, 4)}) + cases = 0 + for first, second in product(alphabet, repeat=2): + row = ((first.numerator, first.denominator), + (second.numerator, second.denominator), (0, 1), (0, 1)) + for x, y in product(range(-2, 2), repeat=2): + state = (x, y, 0, 0) + require(rounded_row(row, state, Words(12)) == oracle(row, state), + "complete signed two-term domain") + cases += 1 + return cases + + +def division_cases(): + cases = 0 + for numerator in range(1024): + for denominator in range(1, 32): + actual = Words(13).divide(numerator, denominator) + require(actual == divmod(numerator, denominator), "binary division") + cases += 1 + return cases + + +def extreme_cases(): + cases = 0 + max_peak = 0 + for data_bits, coefficient_bits in product((2, 18, 128, 512, 2048), + (1, 2, 15, 64, 256)): + high = (1 << coefficient_bits) - 1 + row = tuple((sign * high, high) for sign in (1, -1, 1, -1)) + state = tuple(sign * ((1 << (data_bits - 1)) - 1) for sign in (1, -1, 1, -1)) + width = data_bits + 4 * coefficient_bits + 2 + for current in (state, tuple(-x - 1 for x in state)): + words = Words(width) + require(rounded_row(row, current, words) == oracle(row, current), + "extreme products and cancellation") + require(words.peak <= width, "extreme temporary width") + max_peak = max(max_peak, words.peak) + cases += 1 + return cases, max_peak + + +def real_rows(gate): + rows = [] + for row in gate: + real = [part for value in row for part in (value.re, -value.im)] + imag = [part for value in row for part in (value.im, value.re)] + rows.extend(tuple((x.numerator, x.denominator) for x in parts) + for parts in (real, imag)) + return tuple(rows) + + +def actual_gate_cases(): + sys.path.insert(0, str(ROOT / "research/rational-unitary-fft")) + import engine + import exact + source = (ROOT / "research/cubic-cyclic-inverse/vendor/interval_kernel.py").read_text() + phases = engine.Phases(4, source) + builder = object.__new__(engine.Builder) + builder.phases = phases + gate = builder.butterfly(phases.phase(4, 1)) + rows = real_rows(gate) + height = max(max(abs(a).bit_length(), d.bit_length()) for row in rows for a, d in row) + require(height == 15, "concrete source-produced gate height") + cases = 0 + for bits, state in product((1, 12, 128), product((-131072, -1, 0, 131071), repeat=4)): + scale = 1 << bits + vector = exact.Vec([exact.C(Fraction(state[0], scale), Fraction(state[1], scale)), + exact.C(Fraction(state[2], scale), Fraction(state[3], scale))]) + expected, _ = exact.apply([[(tuple(range(2)), gate)]], vector, bits) + expected = tuple(int(part * scale) for value in expected for part in (value.re, value.im)) + current = list(state) + words = apply_gate(rows, current, 18, height) + require(tuple(current) == expected, "source once-rounded butterfly contract") + require(words.width == 80 and words.peak <= 80, "concrete arithmetic width") + cases += 1 + require(2 * 18 + 8 * height + 32 == 188, "same-parameter cited allowance") + return cases, [[value.record() for value in row] for row in gate] + + +def controls(): + checks = 0 + row = ((1, 2), (1, 2), (0, 1), (0, 1)) + require(rounded_row(row, (1, 1, 0, 0), Words(12)) == 1, + "sum before rounding") + checks += 1 + require(sum(literal_round(Fraction(*pair) * x) for pair, x in zip(row, (1, 1, 0, 0))) == 2, + "per-product rounding differs") + checks += 1 + for value, expected in ((1, 1), (-1, 0), (3, 2), (-3, -1)): + require(rounded_row(((1, 2), (0, 1), (0, 1), (0, 1)), + (value, 0, 0, 0), Words(12)) == expected, "signed halfway ties") + checks += 1 + swap = tuple(tuple((int(j == (i ^ 2)), 1) for j in range(4)) for i in range(4)) + state = [1, 2, 3, 4] + apply_gate(swap, state, 4, 1) + require(state == [3, 4, 1, 2], "saved source coordinates") + checks += 1 + broken = [1, 2, 3, 4] + for i in range(4): + broken[i] = oracle(swap[i], broken) + require(broken != state, "overwrite-before-read differs") + checks += 1 + return checks + + +def rejection_controls(): + identity = tuple(tuple((int(i == j), 1) for j in range(4)) for i in range(4)) + cases = [(identity, [0] * 4, 1, 2), (identity, [0] * 4, 2049, 2), + (identity, [0] * 4, 4, 0), (identity, [0] * 4, 4, 257), + (identity, [0] * 3, 4, 2), (identity[:3], [0] * 4, 4, 2), + (identity, [True, 0, 0, 0], 4, 2), (identity, [8, 0, 0, 0], 4, 2), + (identity, [-9, 0, 0, 0], 4, 2), (identity, (0, 0, 0, 0), 4, 2)] + for pair in ((1, 0), (1, -1), (4, 1), (1, 4), (True, 1)): + cases.append((((pair,) + identity[0][1:],) + identity[1:], [0] * 4, 4, 2)) + for rows, state, data_bits, coefficient_bits in cases: + before = tuple(state) + try: + apply_gate(rows, state, data_bits, coefficient_bits) + except ValueError: + require(tuple(state) == before, "invalid request leaves state unchanged") + else: + raise ValueError("invalid request accepted") + for value in (128, -129): + try: + Words(8).check(value) + except OverflowError: + continue + raise ValueError("overflow accepted") + return len(cases) + 2 + + +def main(): + source_count = authenticate() + rows, row_peak = row_cases() + two_terms = two_term_cases() + divisions = division_cases() + extremes, extreme_peak = extreme_cases() + actual, gate = actual_gate_cases() + semantic = controls() + rejected = rejection_controls() + hashes = {} + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "kernel.py", "verify.py") + for name in names: + path = PACKAGE / name + require(path.stat().st_size <= 1048576, "package file capacity") + hashes[name] = sha256(path.read_bytes()).hexdigest() + if path.suffix == ".py": + tree = ast.parse(path.read_text()) + for node in ast.walk(tree): + if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef)): + require(node.end_lineno - node.lineno + 1 <= 60, "function size") + receipt = dict(marker="PASS_INTEGER_ROUNDED_GATE", sources=source_count, + four_term_rows=rows, two_term_rows=two_terms, divisions=divisions, + extreme_rows=extremes, actual_gate_cases=actual, + row_peak_bits=row_peak, extreme_peak_bits=extreme_peak, + semantic_controls=semantic, rejection_controls=rejected, + source_gate=gate, package_sha256=hashes) + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()