diff --git a/research/physical-fft-word/EVIDENCE.md b/research/physical-fft-word/EVIDENCE.md new file mode 100644 index 0000000000..cefb9b6159 --- /dev/null +++ b/research/physical-fft-word/EVIDENCE.md @@ -0,0 +1,93 @@ +# FFT word verification scope + +Jose Manuel (`jmbarrancoml`), with substantial OpenAI Codex assistance. +I ran the seven suites below on Darwin arm64 with Python 3.12.13. I use +exact Python integers only in separate checking models. During physical +execution I disable payload decoding and retain the encoded tape +operations, fixed pools and protected-output protocol. I record final +committed-export and hosted receipts in the public PR and Discussion3664. + +| Suite | Author checks | +|---|---| +| `sources` | Complete corrected PR3709 export, 26 retained files, one shared physical type cohort, actual RingProduct/Karatsuba child identities, two Gaussian source hashes, changed-archive and duplicate-runtime rejection. | +| `budget` | 8,190 finite geometry cases, strict coefficient headroom, no wrap, linear packet volume, full setup charges and exact arithmetic-power comparison. PROOF.md supplies the universal argument. | +| `plan` | 13 encoded geometries from width 2 through `2^257+7`; exact fields, preserved width port, rejection of widths 0 and 1. These are metadata-only cases. | +| `base` | 18 complete products at widths 1, 2, 3, 8, 15 and 16: zero, one and maximum operands, on one owner. | +| `codec` | 10 complete packing/carry cases through 1,024 bits, including partial digits and canonical-short zero/one inputs. I supply the normalized-product boundary with an independent integer convolution fixture. | +| `failures` | 13 malformed-input, output and allocation controls, followed by a positive packet on the same owner. | +| `fft` | Actual default FFT call at width 17, base call at 16, then the retained signed Arithmetic consumer at width 19 on the same word owner. | + +## Complete FFT sequence + +For width 17 I multiply `(2^17-1)*(2^17-33)`. I compare all 34 returned +bits with the exact integer product, preserve all three borrowed ports, +inspect complete owned restoration and consume the protected result. +The physical ring arithmetic executes 896 word products and 11,648 +Karatsuba nodes; the new owner's peak pool use is 27 roles. The raw +bit-byte SHA256 is: + +```text +62e37795a75598907558cf9780e449d61e9d704b7efa07f470a4491332b832d8 +``` + +I then multiply `65535*65533` through the base branch on the same owner. +The 32-bit raw return has SHA256: + +```text +2a68f44e8a83fa88e55b83f6db4186448898a41e06f0af18c706269bc4049ea2 +``` + +Finally, the retained `Arithmetic.multiply` caller multiplies signed +`-1` by `2^19-15`, declaring width 19. This exercises canonical-short +input, negative sign handling, caller scope suspension, the actual +default FFT branch and complete raw-return consumption. The ring +executes another 896 word products. The caller's pool peaks at three +roles. The 38-bit magnitude representation has SHA256: + +```text +ec30665633fa9c08dcbcf86d79f4049ffc76dcaf2699be106cdf6a7a2c7fad91 +``` + +I use no reduced test cutoff or FFT-result substitution in this suite. +The ring's internal word owner remains the original Karatsuba engine. + +## Separate codec and rejection coverage + +The codec suite uses widths 2, 3, 5, 17, 21, 65, 257 and 1,024 with +maximum-times-near-maximum inputs, plus canonical-short one and zero +cases at widths 65 and 257. I execute physical packing and carrying, +using a separate integer convolution at the ring-return boundary. +For the 1,024-bit case the 2,048-bit result has SHA256: + +```text +9b953c0abf693e0525b98a66ad337c93217d4eb7845fc6a1a2d91fc7f0d5dead +``` + +I reject zero width, each oversized operand, unconsumed protected output, +and dynamic physical-tape allocation during a completed macro. At the +unpack boundary I reject a nonzero imaginary component, a negative real +coefficient, excess coefficient headroom, a nonzero dummy record, +short/extra returns, a shortened output extent and nonzero final carry. +Those malformed-return fixtures check the carry consumer without +claiming another complete FFT execution. + +The positive width-7 call after owner rejection tests returns SHA256 +`6ef12bc0bf346df6d3fb05ce169e60013adc3ca15d1692a7c724e7f0f1f3fd5d`. +I require explicit exceptions, preserve borrowed values and inspect +scratch cleanup. The source suite also rejects a changed archive digest +and a second runtime cohort. + +## Proof and remaining obligations + +I prove the exact-grid identity, no-wrap condition, carry invariant, +time and space bounds in PROOF.md. The finite budget suite checks the +same inequalities over widths 3 through 8,192 and authenticates the +inherited Fourier-power calculation. It records the Gaussian arithmetic +power `9981/10000`, Fourier power `99827619697/100000000000`, and positive +gap `17619697/100000000000`. + +I retain PR3709's numerical precision/recovery premises. I have not +executed a large production FFT word, implemented the Gaussian caller, +or completed the CRT/integer theorem. A reviewer must assess the +all-size proof and inherited premises apart from these finite author +checks. I leave the selected frontier unchanged. diff --git a/research/physical-fft-word/PROOF.md b/research/physical-fft-word/PROOF.md new file mode 100644 index 0000000000..b066548b77 --- /dev/null +++ b/research/physical-fft-word/PROOF.md @@ -0,0 +1,216 @@ +# Exact FFT word multiplication + +Jose Manuel (`jmbarrancoml`), with substantial OpenAI Codex assistance. +I give a fixed-tape implementation of the classical radix-digit/FFT +reduction, using the complete normalized product from corrected PR3709. +I retain its numerical proof and source notices. I distinguish the +all-size argument below from the finite checks in EVIDENCE.md. + +## Contract and dependency + +The caller supplies two canonical nonnegative Count magnitudes a and b, +at their origin heads, and a canonical positive width n. I require +`0<=a,b<2^n`. The borrowed tapes must lie outside the owner's scratch and +child roles. The two magnitude ports may alias each other. I return +exactly 2n raw LSB-first bits for ab, including high zero bits, and +restore the borrowed values and origin heads. + +The caller must consume the protected output before reuse. I expose the +`closed`, `pool`, `output` and `canonical` ownership interface used by +the retained signed arithmetic consumer. I erase owned scratch and +consume child returns before completing a legal call. + +I use a fixed small-word cutoff of 16 by default. The constructor can +compile another fixed cutoff at least two; it is a program constant, +not an input-dependent parameter. Below that cutoff I call the retained +WordProduct. Above it I call RingProduct, whose internal multiplier +remains the original Karatsuba WordProduct. The dependency is acyclic. +In particular, I do not install FftWord inside its own RingProduct child. + +The word theorem uses PR3709's normalized-product proof and the elementary +tape codecs. I make no call to a T74 supplier, a full synthetic Fourier +transform or an HH integer-multiplication oracle in this word algorithm. + +## Encoded geometry and packing + +For the FFT branch, let + + beta=ceil(log2 n), B=2^beta, q=ceil(n/beta), + r=2^ell, ell=ceil(log2(2q)), p0=2beta+ell. + +The default branch has n>16, so beta>=1 and the divisions are defined. +The same formulas work above any fixed cutoff at least two. I have +`2q<=r<4q`, `r*beta>=2n` and `1<=ell=2n`, the remaining padding bits +are zero; I check them rather than discarding them unchecked. I require +both a finished output counter and zero final carry. + +The returned word is therefore exactly ab with the declared 2n-bit +extent. The carry and output passes cost O(r*p0)=O(n). The small-word +branch has the same endpoint by the retained WordProduct proof. + +I include encoded loop control in that linear charge. The retained +Counter stores `finished` as a boolean and decrements only its trailing +zero prefix before rewinding that prefix. Across a countdown from N, +the ripple lengths sum to `2N-popcount(N)`. Construction and cleanup +add O(log(N+1)). The retained `indices(N)` also increments one mutable +index by its low-bit ripple; I neither retain nor close that yielded +index. Repeating `indices(beta)` across r digits costs +`O(r*(beta+log(beta+1)))=O(n)`. Each local addition and right shift +uses O(p0+beta) work. I perform no full-width count copy or comparison +per emitted bit. + +## Complete time and space + +For n above the fixed cutoff, beta=Theta(log(n+2)), +`q=O(n/beta)`, `r=O(n/beta)`, and `p0=O(beta)`. +I use the general PR3709 product invoice with A=C=1, retaining its +unamortized setup: + + O(r(ell+1)p0^(8/5) + r*p0^3 + p0^3). + +The first term is O(n*beta^(8/5)). The twiddle term is O(n*beta^2), +and the global metadata term is O(beta^3). Packing, validation, exact +carries, copying the protected result and cleanup add O(n). +I obtain + + time = O(n log2(n+2)^2), space = O(n). + +This estimate does not assume A=Theta(p0). I pay the setup term directly +in the scalar call. For an elementary bound, n>=3 gives +`r<8n/beta`, `ell+1<=2beta`, `p0<=4beta` and beta<=n. Replacing the +8/5 scalar power by the larger quadratic power bounds the three terms +by `256n beta^2`, `512n beta^2` and `64n beta^2`, respectively, up to +the retained implementation constants. The finitely many small widths +fit the same asymptotic bound with a constant depending on the fixed +cutoff. + +I keep two packed operands, the protected result, a constant number of +inherited packet buffers and O(log n)-bit carry/geometry records. Since +`r*(p0+2)=O(n)`, these occupy O(n) cells. I include the retained word +stack and twiddle workspace in that bound. The number of tape roles is +fixed. During reuse the host backing arrays retain their largest prior +blank extent; their high-water storage is O(max n over those calls). +I clear bodies and restore heads before each return. Diagnostic host +counters do not select operations and can be omitted from the program. + +## Consequence for the Gaussian arithmetic allowance + +For any fixed delta>0, `log2(n+2)^2=O(n^delta)`. One explicit argument +for 0=1/2`, `n+2<=3n` and +`exp(u)>=u^2/2`. It gives + + log2(n+2)^2 <= 24 delta^(-2) n^delta, n>=1. + +Thus this concrete word primitive supplies an O(n^(1+delta)) +allowance for each fixed delta, including the retained delta=.0001. + +The pinned bulk Gaussian reports use scalar p-bit products and four +packed Toeplitz convolutions per local inverse application. Their cell +length is at most 4d+1<=5p in the intended range, so the packed integer +width is O(L_cell*p). I can charge such a product at +`O(L_cell*p*log2(p+2)^2)` with this adapter. I preserve the report's +separate coefficient, layout, factor-page and restoration obligations. + +The w^2 scalar boundary term alone, with direct p^(8/5) multiplication, +would have normalized power `8/5-rho=1.598` at rho=.002. I use that +term as a failure screen; direct multiplication of the larger packed +cells can cost more. With the new word primitive, the report's arithmetic +schedule has powers epsilon and 1-rho, up to logarithms. Absorbing those +logs with delta=.0001 gives + + max(epsilon+delta,1-rho+delta)=.9981 + < Phi=.99827619697. + +I retain the positive gap .00017619697 as an arithmetic feasibility +result. I have not implemented the Gaussian caller in this package or +verified its complete physical invoice. The selected frontier remains +unchanged. + +## Verification and attribution + +I execute the default FFT branch at widths 17 and 19, including the +retained signed Arithmetic consumer and a base call between them. I +check codecs separately through 1,024 bits using independent integer +convolution as a boundary fixture; I do not relabel that as a full FFT +execution. I also check large encoded geometry without materializing its +payload, and execute malformed-return and ownership controls. + +I credit the standard radix/FFT reduction and Karatsuba algorithm, +corrected PR3709's normalized-product implementation, Mason Hale's +certified interval reference, Dugongue's scalar-ABI precedent and the +retained source notices. The numerical predecessor remains subject to +its separate precision/recovery audit. These are AI-assisted author +checks and an algorithmic proof, not independent human or formal-kernel +verification of the complete multiplication project. diff --git a/research/physical-fft-word/README.md b/research/physical-fft-word/README.md new file mode 100644 index 0000000000..d149d6c20f --- /dev/null +++ b/research/physical-fft-word/README.md @@ -0,0 +1,96 @@ +# Physical FFT word multiplication + +Jose Manuel (`jmbarrancoml`), with substantial OpenAI Codex assistance. +Apache-2.0; I retain the predecessor archives and their notices. + +I implement exact unsigned n-bit multiplication in the retained fixed-tape +model, with `O(n log2(n+2)^2)` time and `O(n)` space. I use the classical +radix-digit/FFT reduction through corrected [PR3709](https://github.com/CrocSwap/integer-mult-bounds/pull/3709), +head `62264289adb01f3ba4930cd0154c75887f96203c`. Its internal Karatsuba +multiplier remains unchanged, so the dependency is acyclic. I give the +all-size argument in [PROOF.md](PROOF.md) and separate finite execution +coverage in [EVIDENCE.md](EVIDENCE.md). + +The caller supplies two canonical nonnegative Count magnitudes and a +positive width n, with both magnitudes below `2^n`. I return exactly 2n +raw LSB-first bits, preserve borrowed values and heads, and restore owned +scratch. The caller must consume the protected output before reuse. +`FftWord()` uses the retained word engine through 16 bits and the actual +FFT path above that fixed cutoff. I also exercise the retained signed +`Arithmetic.multiply` consumer with this new word owner. + +For the FFT branch I choose `b=ceil(log2 n)`, `q=ceil(n/b)`, minimal +`r=2^ell>=2q`, and `p0=2b+ell`. I pack each digit as `a_i/2^b` and +call the complete normalized product with A=C=1, including its second +zero record. Since `2^p0=r*2^(2b)` and the degree is below r, I recover +ordinary integer convolution coefficients as the returned real +numerators. Sequential radix carries give the exact word. I include +unamortized twiddle setup in the cost bound. + +This closes a scalar-arithmetic implementation gap for the retained +Gaussian resampling schedule. With delta=.0001, I can charge its +arithmetic at power .9981, below the inherited full Fourier power +.99827619697. I have not implemented that Gaussian caller here. The +Gaussian coefficient producer, guarded convolutions, factor-page access, +window restoration and complete CRT/integer join remain open. I retain +PR3709's numerical proof obligations and the selected frontier. + +## Reproduction + +Use Python 3.12 and the standard library from the repository root: + +```sh +python3.12 scripts/research_package.py --package research/physical-fft-word --check-only +python3.12 scripts/research_package.py --package research/physical-fft-word +python3.12 scripts/check_research_commit.py --package research/physical-fft-word --check-source-history +``` + +I register seven suites in [VERIFY.json](VERIFY.json), with a 600-second +maximum for the full FFT sequence and a 960-second sum of command +timeouts. The tests check actual FFT products at widths 17 and 19, +base calls through 16, isolated codecs through 1,024, encoded geometry +through width `2^257+7`, and malformed packet/ownership controls. +The codec and metadata cases do not claim full FFT execution at those +larger widths. The checks use explicit failures under optimized Python. + +I retain the complete corrected product export in `inputs/ring-export.tar`. +The loader checks its SHA256, complete member inventory and nested source +bindings before importing one shared physical runtime. I declare the two +Gaussian cost reports as live inputs in [SOURCES.json](SOURCES.json). +The official committed export also includes them for replay outside Git. + +## Coordination and attribution + +I recorded the five-point expansion decision before implementation in +[Discussion3664](https://github.com/CrocSwap/integer-mult-bounds/discussions/3664). +I started from main `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority +revision 6, and retained the `uniform-transfer-audit` card. [TASK.json](TASK.json) +records scope, overlap coverage and remaining questions. I follow the +arithmetic handoff from [PR3763](https://github.com/CrocSwap/integer-mult-bounds/pull/3763); +this word algorithm does not invoke its chirp caller or a T74 supplier. + +I credit the standard FFT/radix reduction and Karatsuba algorithm, +PR3709's numerical implementation and exact recovery proof, Mason Hale's +[PR2313](https://github.com/CrocSwap/integer-mult-bounds/pull/2313) certified +interval reference, Dugongue's [PR2790](https://github.com/CrocSwap/integer-mult-bounds/pull/2790) +scalar-ABI precedent, the retained rad20 Gaussian reports and the nested +source notices. Codex assisted the mathematics, implementation, source +analysis, checks and prose. I claim author verification of this package; +I do not claim independent human or formal-kernel review. + +## Open next questions + +- Can a physical Gaussian expansion/compression pair use this scalar API + within its complete cost allowance? First implement one guarded + Toeplitz convolution and its coefficient producer from the pinned + phase-cell source. A complete caller still needs factor-page access, + layout, normalization and window restoration. +- Can a reviewer validate the normalized-product precision and exact + recovery proof on which this adapter depends? First check PR3709 + Sections 3–4 against the retained implementation and its recovery + controls. A finite successful product does not discharge that all-size + numerical argument. +- Can the mixed-radix CRT entrance and return preserve the valid interval + and padding through the full Gaussian/chirp caller? First specify an + actual field conversion and check its interval endpoints. The complete + CRT/Gaussian/integer join remains outside this package. diff --git a/research/physical-fft-word/SOURCES.json b/research/physical-fft-word/SOURCES.json new file mode 100644 index 0000000000..5b5f9add7c --- /dev/null +++ b/research/physical-fft-word/SOURCES.json @@ -0,0 +1,11 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + {"path":"docs/research/agent-task-catalog.json","usage":"provenance","git_blob":"67f085acd86acd7d4e03922d9cf4b26bca66fed5","sha256":"47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"}, + {"path":"certificates/selected-result.json","usage":"provenance","git_blob":"b1fea0c94436b236cc2b7d41a7be032811b94c81","sha256":"bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"}, + {"path":"research/physical-fft-word/inputs/ring-export.tar","usage":"input","pin":"head:d24ceb50e2d06c421c61f40e4e14445fed61c952:research/physical-fft-word/inputs/ring-export.tar","git_blob":"004c660f786cee08b07fd74af80c9c91146b89f4","sha256":"c03d4b056ccd3db860c93579f6525e0bb1baea31cff879eb07135c99432ef159"}, + {"path":"references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md","usage":"input","git_blob":"d72345a0aa748443c4efcddf87aa10d524664841","sha256":"3cdf492bcb719db4295658604dc202d6a2c5a008b87de43ec54f0107c64db730"}, + {"path":"references/semantic-bulk/rad20/reports/downstream-microbox-resampling.md","usage":"input","git_blob":"27f962de34b6943aee33cc0d40b8c7883ccf56f2","sha256":"9598c236eed7e44ac5eb41cc20f7c23249829e195247d15e2857a34e14222c49"} + ] +} diff --git a/research/physical-fft-word/TASK.json b/research/physical-fft-word/TASK.json new file mode 100644 index 0000000000..b3abbb14cc --- /dev/null +++ b/research/physical-fft-word/TASK.json @@ -0,0 +1,56 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": ["certificates/selected-result.json", "docs/audit.md"], + "methods": ["Prove one missing implication with explicit quantified hypotheses.", "Find an exact counterexample at the claimed interface boundary."], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": ["python3", "-B", "scripts/research_baseline.py"], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": ["Choose one tape, precision, hosting or restoration lemma."], + "scope_change_triggers": ["Replacing a quantified obligation with another finite smoke test."], + "overlap_terms": ["uniform transfer", "all-size", "precision"] + }, + "scope_status": "refined", + "scope_change_reason": "I take the concrete scalar-arithmetic handoff after PR3763. I implement the classical radix-digit reduction through corrected PR3709, retaining its internal Karatsuba owner to avoid a circular multiplier dependency. I recorded the complete invoice and five-point expansion decision in Discussion3664 before implementation.", + "actual_scope": "Exact physical unsigned word multiplication in O(n log2(n+2)^2) time and O(n) space: encoded radix geometry, sequential packing, normalized-product execution, exact carries, fixed output extent and restored tape ownership.", + "bottleneck_link": "Direct p^(8/5) scalar multiplication already makes the Gaussian boundary arithmetic exceed the inherited Fourier allowance. This concrete word primitive supplies each fixed p^(1+delta) arithmetic allowance; a full Gaussian implementation remains separate.", + "budget_minutes": 60, + "stop_rule": "Complete the acyclic scalar adapter and its full setup/carry bill, or report an exact cost or restoration obstruction. Reject growing-root scans, lost low bits, circular multiplication and unpaid twiddle setup. The donor requested continued research beyond the default session budget; registered checks remain within repository limits.", + "outcome": "completed", + "evidence": "I implemented the adapter and supplied the all-size exact-grid, carry, time and space argument. Seven suites cover actual default FFT products17/19, retained signed-consumer integration, base reuse, separate codec fixtures through1024 bits, large encoded metadata,13 failure controls and exact cost arithmetic. EVIDENCE.md separates full execution, fixtures and inherited premises; the public receipt records committed-export and hosted verification.", + "author": "Jose Manuel (jmbarrancoml)", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, implementation, source-analysis agents, verification and prose. No independent human or formal-kernel review claimed.", + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3664", + "overlap": "I started from canonical main20ecf2891d80b5acf18d980b2164fb44ea7faa90, priority revision6, and refreshed it before publication; it remains unchanged. The full search through2026-10-18 20:56:35UTC covered491 open PRs and2509 Discussion records with complete pagination and zero warnings. Targeted checks through20:52:32UTC covered100 recent PRs,30 hub comments with replies, all of3664, exact3709/3763/3765 heads and feedback, and complete FFT-word/unsigned-multiplication/near-linear searches. I found no competing physical near-linear word adapter or new source objection in that coverage. I retain Dugongue's quadratic ABI precedent and jwr's adjacent PR3765 chirp-budget check, which leaves its consumer unrun. Arham Tahir's separate3664#19022515 audit of3709 Sections3-4 has no published outcome; I claim no acceptance from it. I posted the expansion decision before implementation, with22:15UTC claim expiry.", + "open_questions": [ + { + "question": "Can a physical Gaussian expansion/compression pair use this scalar API within its complete allowance?", + "why_it_matters": "The word primitive closes scalar arithmetic but does not produce Gaussian coefficients or execute the surrounding resampling caller.", + "first_step": "Implement one guarded Toeplitz convolution and its coefficient producer from the pinned phase-cell source, with complete scaling and precision.", + "blocked_by": "Factor-page access, layout, normalization, window restoration and the full Gaussian caller remain open." + }, + { + "question": "Can a reviewer validate the inherited normalized-product precision and exact recovery argument?", + "why_it_matters": "The all-size word proof depends on PR3709's numerical endpoint, beyond finite product checks.", + "first_step": "Check PR3709 Sections3-4 against the retained implementation and recovery controls.", + "blocked_by": "The separate numerical review remains an inherited obligation; no independent human or formal-kernel review is claimed here." + }, + { + "question": "Can the mixed-radix CRT entrance and return preserve the valid interval and padding through the complete caller?", + "why_it_matters": "A scalar multiplier does not implement the field conversions or final coefficient recovery.", + "first_step": "Specify one actual source/target field conversion and test interval endpoints while retaining both S factors in final integer recovery.", + "blocked_by": "The full CRT/Gaussian/integer join remains outside this package." + } + ] +} diff --git a/research/physical-fft-word/VERIFY.json b/research/physical-fft-word/VERIFY.json new file mode 100644 index 0000000000..6eda5c2836 --- /dev/null +++ b/research/physical-fft-word/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/physical-fft-word/inputs/ring-export.tar", + "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md", + "references/semantic-bulk/rad20/reports/downstream-microbox-resampling.md" + ], + "commands": [ + {"argv":["{python}","-I","-O","-Werror","-B","{package}/verify.py","--suite","sources"],"timeout_seconds":30,"checks":"Whole corrected product export, source hashes, one physical type cohort, acyclic actual child owners and changed-source/runtime rejection."}, + {"argv":["{python}","-I","-O","-Werror","-B","{package}/verify.py","--suite","budget"],"timeout_seconds":30,"checks":"8190 finite geometry and cost controls, complete twiddle setup and exact Gaussian arithmetic comparison; PROOF.md supplies the universal argument."}, + {"argv":["{python}","-I","-O","-Werror","-B","{package}/verify.py","--suite","plan"],"timeout_seconds":60,"checks":"Encoded geometry through width 2^257+7, preserved metadata port and invalid-width rejection; large cases are metadata-only."}, + {"argv":["{python}","-I","-O","-Werror","-B","{package}/verify.py","--suite","base"],"timeout_seconds":60,"checks":"18 actual base products through width16 on one owner, exact raw extent, preservation and cleanup."}, + {"argv":["{python}","-I","-O","-Werror","-B","{package}/verify.py","--suite","codec"],"timeout_seconds":90,"checks":"Physical packing and carry passes through1024 bits, using a separate exact convolution boundary fixture; not full FFT execution at those larger widths."}, + {"argv":["{python}","-I","-O","-Werror","-B","{package}/verify.py","--suite","failures"],"timeout_seconds":90,"checks":"13 malformed-input, return, protected-output and allocation controls, followed by a positive same-owner packet."}, + {"argv":["{python}","-I","-O","-Werror","-B","{package}/verify.py","--suite","fft"],"timeout_seconds":600,"checks":"Complete default FFT product17, base reuse16 and retained signed Arithmetic consumer19, with exact integer oracles, protected-return consumption and actual child execution."} + ] +} diff --git a/research/physical-fft-word/fft_word_check_base.py b/research/physical-fft-word/fft_word_check_base.py new file mode 100644 index 0000000000..b16e335ef4 --- /dev/null +++ b/research/physical-fft-word/fft_word_check_base.py @@ -0,0 +1,16 @@ +"""Small-word boundary and repeated use of the exact base owner.""" +from fft_word_sources import require + + +def run(): + from fft_word_engine import FftWord + from fft_word_check_fft import packet + owner = FftWord() + cases = [] + for width in (1, 2, 3, 8, 15, 16): + maximum = (1 << width)-1 + for a, b in ((0, maximum), (1, maximum), (maximum, maximum)): + cases.append(packet(owner, a, b, width)) + require(owner.calls == dict(base=len(cases), fft=0), "complete small-word branch coverage") + return {"packets": len(cases), "widths": [1, 2, 3, 8, 15, 16], + "last": cases[-1], "calls": owner.calls} diff --git a/research/physical-fft-word/fft_word_check_budget.py b/research/physical-fft-word/fft_word_check_budget.py new file mode 100644 index 0000000000..1a57e6d083 --- /dev/null +++ b/research/physical-fft-word/fft_word_check_budget.py @@ -0,0 +1,36 @@ +"""Exact finite controls for the all-size word and Gaussian arithmetic bills.""" +from fractions import Fraction +import importlib.util +from fft_word_sources import active, require + + +def run(): + cases = 0 + for n in range(3, 8193): + b = (n-1).bit_length() + q = (n+b-1)//b + ell = (2*q-1).bit_length() + r, p = 1 << ell, 2*b+ell + require(2*q <= r < 4*q and 2*q-2 < r and r*b >= 2*n, "complete padded digit geometry") + require(q*((1 << b)-1)**2 < 1 << (p-1), "strict real coefficient headroom") + require(r*(p+2) <= 40*n, "linear complete packet volume") + require(r*(ell+1)*p*p <= 256*n*b*b, "FFT arithmetic inside n log-squared allowance") + require(r*p**3 <= 512*n*b*b and p**3 <= 64*n*b*b, "unamortized twiddle and metadata setup") + cases += 1 + path = active().ring_package / "ring_check_budget.py" + spec = importlib.util.spec_from_file_location("fft_word_inherited_budget", path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + source = module.run() + phi = Fraction(source["fourier_power"]) + epsilon, rho, delta = Fraction(997, 1000), Fraction(2, 1000), Fraction(1, 10000) + old_power = Fraction(8, 5)-rho + gaussian_arithmetic = max(epsilon+delta, 1-rho+delta) + require(old_power > phi and gaussian_arithmetic == Fraction(9981, 10000) < phi, + "changed Gaussian scalar arithmetic feasibility") + require(phi-gaussian_arithmetic == Fraction(17619697, 100000000000), "strict arithmetic margin") + return {"finite_geometry_cases": cases, "packet_bound": "r*(p0+2)<=40*n", + "full_word_time": "O(n*log2(n+2)^2)", "word_space": "O(n)", + "old_gaussian_power": str(old_power), "new_gaussian_arithmetic_power": str(gaussian_arithmetic), + "fourier_power": str(phi), "arithmetic_gap": str(phi-gaussian_arithmetic), + "scope": "PROOF.md supplies the universal argument; Gaussian coefficient, layout and restoration work remains separate."} diff --git a/research/physical-fft-word/fft_word_check_codec.py b/research/physical-fft-word/fft_word_check_codec.py new file mode 100644 index 0000000000..21bb602fe8 --- /dev/null +++ b/research/physical-fft-word/fft_word_check_codec.py @@ -0,0 +1,89 @@ +"""Codec checks using independent integer convolution as a boundary fixture.""" +from hashlib import sha256 +from fft_word_sources import require + + +def geometry(width): + b = (width-1).bit_length() + q = (width+b-1)//b + ell = (2*q-1).bit_length() + return b, q, ell, 1 << ell, 2*b+ell + + +def fixtures(a, b, width): + from check_composed import encode + digit_bits, q, ell, r, p = geometry(width) + mask = (1 << digit_bits)-1 + left = [(a >> (i*digit_bits)) & mask for i in range(q)] + right = [(b >> (i*digit_bits)) & mask for i in range(q)] + packets = [encode([(v << (p-digit_bits), 0) for v in digits] + + [(0, 0)]*(2*r-q), p+2) for digits in (left, right)] + coefficients = [0]*r + for i, x in enumerate(left): + for j, y in enumerate(right): + coefficients[i+j] += x*y + require(max(coefficients) < 1 << (p-1), "independent coefficient headroom") + returned = encode([(v, 0) for v in coefficients]+[(0, 0)]*r, p+2) + return packets, returned, (digit_bits, q, ell, r, p) + + +def packet(a, b, width): + from cardinal_counts import Count + from check_support import no_decode + from fft_word_codec import pack, unpack + from fft_word_plan import WordPlan + from records import Tape + from ring_check_words import body, tape, word_bits + from scratch_pool import ScratchPool + from session import OuterScope, borrowed_tape, erase_marker, sealed_constructors + from words import BLANK + expected, raw, shape = fixtures(a, b, width) + counts = tuple(Count.literal(v) for v in (a, b, width)) + saved = tuple((bytes(v.tape.cells), v.tape.head) for v in counts) + source, output = tape(raw), Tape() + pool = ScratchPool(128) + scope = OuterScope(pool) + plan = WordPlan(counts[2]) + try: + with sealed_constructors(), scope.installed(): + try: + with no_decode(): + plan.compile() + for value, wanted in zip(counts[:2], expected): + with no_decode(): + packed = pack(value, plan, pool) + try: + require(body(borrowed_tape(packed)) == wanted, "sequential radix-grid packing") + finally: + packed.clear() + with no_decode(): + unpack(source, output, plan) + require(body(output) == word_bits(a*b, 2*width), "sequential exact carries and output padding") + finally: + plan.close() + pool.empty() + require(saved == tuple((bytes(v.tape.cells), v.tape.head) for v in counts) + and body(source) == raw, "codec preserves borrowed inputs") + require(all(t.head == 1 and all(v == BLANK for v in t.cells[1:]) for t in pool.tapes), + "codec scratch restoration") + return {"width": width, "operand_bits": [a.bit_length(), b.bit_length()], + "digit_bits": shape[0], "digits": shape[1], "ell": shape[2], "p": shape[4], + "output_sha256": sha256(body(output)).hexdigest(), "pool_peak": pool.peak, + "scope": "codec only; the ring return comes from independent integer convolution"} + finally: + output.clear() + erase_marker(output) + for value in counts: + value.close() + for value in pool.tapes: + erase_marker(value) + + +def run(): + records = [] + for width in (2, 3, 5, 17, 21, 65, 257, 1024): + maximum = (1 << width)-1 + records.append(packet(maximum, maximum-2, width)) + records.append(packet(1, (1 << 65)-7, 65)) + records.append(packet(0, (1 << 257)-1, 257)) + return {"packets": records} diff --git a/research/physical-fft-word/fft_word_check_failures.py b/research/physical-fft-word/fft_word_check_failures.py new file mode 100644 index 0000000000..b50b380818 --- /dev/null +++ b/research/physical-fft-word/fft_word_check_failures.py @@ -0,0 +1,138 @@ +"""Boundary, ownership and corrupted coefficient-return controls.""" +from unittest.mock import patch +from fft_word_sources import require + + +def rejected_return(raw, width, message, short_output=False): + from cardinal_counts import Count + from check_support import no_decode + from fft_word_codec import unpack + from fft_word_plan import WordPlan + from records import Tape + from ring_check_words import body, tape + from scratch_pool import ScratchPool + from session import OuterScope, erase_marker, sealed_constructors + source, output = tape(raw), Tape() + n = Count.literal(width) + plan = WordPlan(n) + pool = ScratchPool(128) + scope = OuterScope(pool) + try: + with sealed_constructors(), scope.installed(): + try: + plan.compile() + if short_output: + plan.output_bits.close() + plan.fields["output_bits"] = Count.literal(1) + try: + with no_decode(): + unpack(source, output, plan) + except ValueError as error: + require(message in str(error), "intended coefficient-return rejection: " + str(error)) + else: + raise ValueError("missing coefficient-return rejection") + finally: + plan.close() + pool.empty() + require(body(source) == raw, "rejected coefficient return remains borrowed") + finally: + output.clear() + erase_marker(output) + n.close() + for value in pool.tapes: + erase_marker(value) + + +def run(): + from cardinal_counts import Count + from check_composed import encode + from check_support import no_decode + from fft_word_check_codec import fixtures + from fft_word_check_fft import packet + from fft_word_engine import FftWord + from records import Tape + from ring_check_words import body + from session import erase_marker + from words import BLANK + owner = FftWord() + controls = [] + for name, a, b, width, message in ( + ("zero_width", 0, 0, 0, "positive cardinality"), + ("left_magnitude_too_wide", 8, 1, 3, "fits declared word width"), + ("right_magnitude_too_wide", 1, 8, 3, "fits declared word width"), + ): + values = tuple(Count.literal(v) for v in (a, b, width)) + saved = tuple((bytes(v.tape.cells), v.tape.head) for v in values) + try: + try: + with no_decode(): + owner.run(*values) + except ValueError as error: + require(message in str(error), "intended word admission failure") + controls.append(name) + else: + raise ValueError("missing word admission rejection") + require(saved == tuple((bytes(v.tape.cells), v.tape.head) for v in values), + "rejected word call preserves inputs") + require(owner.closed and not owner.pool.live and owner.output.read() == BLANK, + "rejected word call restores its owner") + owner.idle() + finally: + for value in values: + value.close() + packet(owner, 3, 5, 4, consume=False) + retained = body(owner.output) + values = tuple(Count.literal(v) for v in (1, 1, 2)) + try: + try: + owner.run(*values) + except ValueError as error: + require("consume prior FFT-word output" in str(error) and body(owner.output) == retained, + "protected word return stays intact") + controls.append("protected_output") + else: + raise ValueError("missing protected word rejection") + finally: + for value in values: + value.close() + owner.output.clear() + erase_marker(owner.output) + values = tuple(Count.literal(v) for v in (1, 1, 17)) + try: + with patch("fft_word_engine.pack", lambda *_: Tape()): + try: + owner.run(*values) + except ValueError as error: + require("physical Tape allocation inside" in str(error), "fixed tape inventory guard") + controls.append("dynamic_physical_tape") + else: + raise ValueError("missing dynamic tape rejection") + owner.idle() + require(owner.closed and not owner.pool.live and owner.output.read() == BLANK, + "allocation rejection restores the word owner") + finally: + for value in values: + value.close() + _, raw, (_, _, _, r, p) = fixtures(31, 29, 5) + component = p+2 + for name, position, message in ( + ("nonzero_imaginary", component, "nonnegative real"), + ("negative_coefficient", component-1, "nonnegative real"), + ("coefficient_headroom", p-1, "coefficient headroom"), + ("nonzero_dummy_record", 2*r*component, "zero second product record"), + ): + changed = bytearray(raw) + changed[position] = 1 + rejected_return(bytes(changed), 5, message) + controls.append(name) + rejected_return(raw[:-1], 5, "zero second product record") + controls.append("short_return") + rejected_return(raw+b"\x00", 5, "complete normalized word-product packet") + controls.append("extra_return") + rejected_return(raw, 5, "zero high product padding", short_output=True) + controls.append("shortened_output_extent") + coefficients = [(0, 0)]*(2*r) + coefficients[r-1] = (64, 0) + rejected_return(encode(coefficients, component), 5, "zero final carry") + controls.append("nonzero_final_carry") + return {"controls": controls, "positive_after_rejections": packet(owner, 127, 125, 7)} diff --git a/research/physical-fft-word/fft_word_check_fft.py b/research/physical-fft-word/fft_word_check_fft.py new file mode 100644 index 0000000000..0b2bbbde60 --- /dev/null +++ b/research/physical-fft-word/fft_word_check_fft.py @@ -0,0 +1,102 @@ +"""Complete default-crossover FFT multiplication against exact integers.""" +from hashlib import sha256 +from fft_word_sources import require + + +def packet(owner, a, b, width, consume=True): + from cardinal_counts import Count + from check_support import no_decode + from ring_check_words import body, word_bits + from session import erase_marker + from word_product import WordProduct + from words import BLANK + values = tuple(Count.literal(v) for v in (a, b, width)) + saved = tuple((bytes(v.tape.cells), v.tape.head) for v in values) + calls = dict(owner.calls) + products = owner.product.arithmetic.products + nodes = owner.product.word.calls["nodes"] + try: + with no_decode(): + output = owner.run(*values) + actual = body(output) + require(actual == word_bits(a*b, 2*width), "complete exact FFT-word product") + require(saved == tuple((bytes(v.tape.cells), v.tape.head) for v in values), + "FFT-word preserves all borrowed numerical ports") + owner.idle() + require(owner.closed and not owner.pool.live and owner.a is owner.b is None, + "closed FFT-word owner") + require(type(owner.product.word) is WordProduct and type(owner.base) is WordProduct, + "acyclic retained Karatsuba dependencies") + require(all(t.head == 1 and all(bit == BLANK for bit in t.cells) + for t in (*owner.pool.tapes, *owner.canonical)), "FFT-word owned restoration") + delta = {key: owner.calls[key]-calls[key] for key in calls} + require(delta == (dict(base=1, fft=0) if width <= owner.base_bits else dict(base=0, fft=1)), + "actual default word crossover") + result = {"width": width, "bits": len(actual), "calls": delta, + "sha256": sha256(actual).hexdigest(), "pool_peak": owner.pool.peak, + "ring_word_products": owner.product.arithmetic.products-products, + "ring_word_nodes": owner.product.word.calls["nodes"]-nodes} + if consume: + output.clear() + erase_marker(output) + return result + finally: + for value in values: + value.close() + + +def signed_consumer(owner): + from cardinal_counts import Count + from check_support import no_decode + from fft_arithmetic import Arithmetic + from ring_check_words import decode, word_bits + from ring_words import Signed + from scratch_pool import ScratchPool + from session import OuterScope, erase_marker, sealed_constructors + from words import BLANK + width, a, b = 19, 1, (1 << 19)-15 + values = tuple(Count.literal(v) for v in (a, b, width)) + left, right = Signed(values[0], True), Signed(values[1]) + saved = tuple((bytes(v.tape.cells), v.tape.head) for v in values) + pool = ScratchPool(32) + scope = OuterScope(pool) + arithmetic = Arithmetic(owner, scope) + before = dict(owner.calls) + products = owner.product.arithmetic.products + result = None + try: + with sealed_constructors(), scope.installed(): + try: + with no_decode(): + result = arithmetic.multiply(left, right, values[2]) + magnitude = decode(result.magnitude) + require(result.negative and magnitude == a*b, "retained signed consumer with actual FFT word") + require(owner.output.read() == BLANK and arithmetic.products == 1, + "signed consumer consumes the complete protected raw word") + owner.idle() + finally: + if result is not None: + result.close() + pool.empty() + require(saved == tuple((bytes(v.tape.cells), v.tape.head) for v in values), + "signed integration preserves borrowed magnitudes and width") + delta = {key: owner.calls[key]-before[key] for key in before} + require(delta == dict(base=0, fft=1), "signed integration executes the default FFT branch") + return {"consumer": "retained Arithmetic.multiply", "width": width, "negative": True, + "canonical_short_operand": a, "calls": delta, + "raw_product_sha256": sha256(word_bits(magnitude, 2*width)).hexdigest(), + "ring_word_products": owner.product.arithmetic.products-products, + "caller_pool_peak": pool.peak} + finally: + for value in values: + value.close() + for value in pool.tapes: + erase_marker(value) + + +def run(): + from fft_word_engine import FftWord + owner = FftWord() + return {"packets": [packet(owner, (1 << 17)-1, (1 << 17)-33, 17), + packet(owner, (1 << 16)-1, (1 << 16)-3, 16), + signed_consumer(owner)]} diff --git a/research/physical-fft-word/fft_word_check_plan.py b/research/physical-fft-word/fft_word_check_plan.py new file mode 100644 index 0000000000..3b5691dd82 --- /dev/null +++ b/research/physical-fft-word/fft_word_check_plan.py @@ -0,0 +1,49 @@ +"""Encoded geometry, including large metadata-only widths.""" +from fft_word_sources import require + + +def run(): + from cardinal_counts import Count + from check_support import no_decode + from fft_word_plan import WordPlan + from ring_check_words import decode + records = [] + for width in (2, 3, 5, 16, 17, 19, 21, 33, 65, 257, 1024, (1 << 33)+7, (1 << 257)+7): + n = Count.literal(width) + saved = bytes(n.tape.cells), n.tape.head + plan = WordPlan(n) + try: + with no_decode(): + plan.compile() + b = (width-1).bit_length() + q = (width+b-1)//b + ell = (2*q-1).bit_length() + r, p = 1 << ell, 2*b+ell + expected = dict(one=1, b=b, q=q, ell=ell, r=r, p=p, component=p+2, + shift=p-b, output_bits=2*width, + padding_bits=2*(2*r-q)*(p+2), dummy_bits=2*r*(p+2), + coefficient_limit=1 << (p-1)) + require({key: decode(value) for key, value in plan.fields.items()} == expected, + "exact encoded radix geometry") + require(2*q <= r < 4*q and r*b >= 2*width and ell < p + and p == 2*b+ell, "no-wrap and exact-grid invariants") + require((bytes(n.tape.cells), n.tape.head) == saved, "preserved width descriptor") + records.append({"width": str(width), "b": b, "q": str(q), "ell": ell, + "p": p, "metadata_only": True}) + finally: + plan.close() + n.close() + for width in (0, 1): + n = Count.literal(width) + plan = WordPlan(n) + try: + try: + plan.compile() + except ValueError as error: + require("extent at least two" in str(error), "FFT geometry excludes width zero or one") + else: + raise ValueError("missing FFT geometry admission rejection") + finally: + plan.close() + n.close() + return {"plans": records, "rejected_widths": [0, 1]} diff --git a/research/physical-fft-word/fft_word_check_sources.py b/research/physical-fft-word/fft_word_check_sources.py new file mode 100644 index 0000000000..8eb350e1ef --- /dev/null +++ b/research/physical-fft-word/fft_word_check_sources.py @@ -0,0 +1,52 @@ +"""Whole predecessor binding, shared types and acyclic multiplier ownership.""" +from hashlib import sha256 +import importlib +from pathlib import Path +from unittest.mock import patch +import fft_word_sources +from fft_word_sources import HERE, active, require + + +def run(): + from cardinal_counts import Count + from records import Tape + from fft_word_engine import FftWord + from word_product import WordProduct + fft_word_sources.authenticate() + state = active() + modules = ("fft_word_plan", "fft_word_codec", "fft_word_engine") + for name in modules: + module = importlib.import_module(name) + require(Path(module.__file__).resolve() == HERE / (name + ".py"), "local FFT-word module") + for key, canonical in (("Count", Count), ("Tape", Tape)): + if hasattr(module, key): + require(getattr(module, key) is canonical, "one FFT-word physical class") + owner = FftWord() + require(type(owner.product) is state.ring.RingProduct and type(owner.base) is WordProduct + and type(owner.product.word) is WordProduct and owner.product.arithmetic.word is owner.product.word, + "acyclic actual normalized-product and Karatsuba children") + owner.idle() + inputs = { + "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md": + "3cdf492bcb719db4295658604dc202d6a2c5a008b87de43ec54f0107c64db730", + "references/semantic-bulk/rad20/reports/downstream-microbox-resampling.md": + "9598c236eed7e44ac5eb41cc20f7c23249829e195247d15e2857a34e14222c49", + } + for path, digest in inputs.items(): + require(sha256((HERE.parents[1] / path).read_bytes()).hexdigest() == digest, + "pinned Gaussian arithmetic source") + with patch.object(fft_word_sources, "DIGEST", "0"*64): + try: + fft_word_sources.authenticate() + except ValueError as error: + require("pinned FFT-word source bytes" in str(error), "changed source binding rejection") + else: + raise ValueError("missing source binding rejection") + try: + with fft_word_sources.opened(): + raise ValueError("second FFT-word runtime opened") + except ValueError as error: + require("cold FFT-word namespace" in str(error), "second runtime rejection") + return {"predecessor_head": fft_word_sources.HEAD, "export_sha256": fft_word_sources.DIGEST, + "predecessor_files": 26, "runtime_modules": list(modules), "inputs": inputs, + "controls": ["changed_archive_binding", "second_runtime"], "acyclic_children": True} diff --git a/research/physical-fft-word/fft_word_codec.py b/research/physical-fft-word/fft_word_codec.py new file mode 100644 index 0000000000..9444abc96a --- /dev/null +++ b/research/physical-fft-word/fft_word_codec.py @@ -0,0 +1,78 @@ +"""Sequential magnitude packing and exact radix carries on encoded tapes.""" +from fft_word_sources import active +active() +from cardinal_counts import Count +from encoded import compare +from ring_words import read_signed, right_shift +from router_metadata import indices, owned +from stream import Counter +from words import BLANK, RIGHT, need + + +def pack(source, plan, pool): + output = pool.acquire() + source.rewind() + try: + for _ in indices(plan.q): + for _ in indices(plan.shift): + output.append(0) + for _ in indices(plan.b): + ended = source.read() == RIGHT + bit = 0 if ended else source.read() + need(bit in (0, 1), "canonical packed word digit") + output.append(bit) + if not ended: + source.step(1) + for _ in range(2): + output.append(0) + for _ in indices(plan.component): + output.append(0) + need(source.read() == RIGHT, "complete declared-width word packing") + for _ in indices(plan.padding_bits): + output.append(0) + output.rewind() + return output + except BaseException: + output.clear() + raise + finally: + source.rewind() + + +def unpack(source, output, plan): + source.rewind() + carry = Count.literal(0) + try: + with owned(Counter(plan.output_bits)) as (remaining,): + for _ in indices(plan.r): + with owned(read_signed(source, plan.component)) as (real,): + with owned(read_signed(source, plan.component)) as (imaginary,): + need(not real.negative and imaginary.magnitude.zero(), + "nonnegative real digit-convolution coefficient") + need(compare(real.magnitude, plan.coefficient_limit) < 0, + "digit-convolution coefficient headroom") + total = real.magnitude + total.add(carry) + total.rewind() + for _ in indices(plan.b): + ended = total.read() == RIGHT + bit = 0 if ended else total.read() + need(bit in (0, 1), "canonical carried word digit") + if remaining.finished: + need(bit == 0, "zero high product padding") + else: + output.append(bit) + remaining.decrement() + if not ended: + total.step(1) + following = right_shift(total, plan.b) + carry.close() + carry = following + need(remaining.finished and carry.zero(), "complete exact word output and zero final carry") + for _ in indices(plan.dummy_bits): + need(source.read() == 0, "zero second product record") + source.step(1) + need(source.read() == BLANK, "complete normalized word-product packet") + finally: + carry.close() + source.rewind() diff --git a/research/physical-fft-word/fft_word_engine.py b/research/physical-fft-word/fft_word_engine.py new file mode 100644 index 0000000000..a9e00dd0b5 --- /dev/null +++ b/research/physical-fft-word/fft_word_engine.py @@ -0,0 +1,108 @@ +"""Exact O(n log²(n+2)) word multiplication with an acyclic FFT dependency.""" +from fft_word_sources import active +active() +from cardinal_counts import Count, positive +from compact_counts import append_bits +from encoded import compare +from fft_word_codec import pack, unpack +from fft_word_plan import WordPlan +from records import Tape +from ring_engine import RingProduct +from ring_words import fits +from router_metadata import owned +from scratch_pool import ScratchPool +from session import (OuterScope, borrowed_count, borrowed_tape, erase_marker, + initialize_marker, sealed_constructors) +from word_product import WordProduct +from words import BLANK, need + + +class FftWord: + def __init__(self, base_bits=16): + need(type(base_bits) is int and base_bits >= 2, "fixed FFT-word base cutoff") + self.base_bits = base_bits + self.base, self.product = WordProduct(), RingProduct() + self.pool = ScratchPool(256) + self.scope = OuterScope(self.pool) + self.output = Tape() + self.a = self.b = None + self.closed = True + self.calls = dict(base=0, fft=0) + # Inspection-only canonical roles; each child manages its own markers. + self.canonical = (*self.base.canonical, self.base.output, self.product.output, + *self.product.word.canonical, self.product.word.output, + self.product.twiddles.output) + for value in (*self.pool.tapes, self.output): + erase_marker(value) + + def idle(self): + self.product.idle() + need(self.base.closed and not self.base.pool.live + and self.product.closed and not self.product.pool.live + and all(value.read() == BLANK for value in self.canonical), + "consumed FFT-word children") + + def run(self, first, second, width): + first, second, width = (borrowed_count(v) for v in (first, second, width)) + need(all(v.tape not in (*self.canonical, *self.pool.tapes, self.output) + for v in (first, second, width)), "borrowed external FFT-word ports") + need(self.closed and not self.pool.live and self.output.read() == BLANK + and self.a is self.b is None, "consume prior FFT-word output") + positive(width) + self.idle() + for value in (*self.pool.tapes, self.output): + initialize_marker(value) + self.closed = False + plan = None + succeeded = False + try: + with sealed_constructors(), self.scope.installed(): + try: + fits(first, width) + fits(second, width) + with owned(Count.literal(self.base_bits)) as (cutoff,): + small = compare(width, cutoff) <= 0 + if small: + with self.scope.suspended(): + returned = self.base.run(first, second, width) + try: + append_bits(returned, self.output) + finally: + returned.clear() + erase_marker(returned) + self.calls["base"] += 1 + else: + plan = WordPlan(width) + plan.compile() + self.a = pack(first, plan, self.pool) + self.b = pack(second, plan, self.pool) + with self.scope.suspended(): + returned = self.product.run(borrowed_tape(self.a), borrowed_tape(self.b), + *(borrowed_count(v) for v in (plan.one, plan.p, plan.ell, plan.one))) + try: + unpack(returned, self.output, plan) + finally: + returned.clear() + erase_marker(returned) + self.calls["fft"] += 1 + self.idle() + succeeded = True + finally: + for value in (first, second, width): + value.rewind() + for value in (self.a, self.b): + if value is not None: + value.clear() + self.a = self.b = None + if plan is not None: + plan.close() + self.pool.empty() + finally: + for value in self.pool.tapes: + erase_marker(value) + self.output.rewind() + if not succeeded: + self.output.clear() + erase_marker(self.output) + self.closed = True + return self.output diff --git a/research/physical-fft-word/fft_word_plan.py b/research/physical-fft-word/fft_word_plan.py new file mode 100644 index 0000000000..a3914e8e06 --- /dev/null +++ b/research/physical-fft-word/fft_word_plan.py @@ -0,0 +1,69 @@ +"""Encoded radix geometry for exact recovery through Q_p(fg/r).""" +from fft_word_sources import active +active() +from cardinal_counts import Count +from encoded import compare, divide, subtract +from ring_words import power_two +from router_metadata import ceiling_log, owned +from words import need + + +def ceiling_divide(numerator, denominator): + result, remainder = divide(numerator, denominator) + try: + if not remainder.zero(): + result.increment() + return result + except BaseException: + result.close() + raise + finally: + remainder.close() + + +class WordPlan: + def __init__(self, width): + self.n = width + self.fields = {} + + def keep(self, name, value): + need(name not in self.fields, "one FFT-word numerical role") + self.fields[name] = value + return value + + def __getattr__(self, name): + return self.fields[name] + + def compile(self): + with owned(Count.literal(2)) as (two,): + need(compare(self.n, two) >= 0, "FFT-word extent at least two") + self.keep("one", Count.literal(1)) + self.keep("b", ceiling_log(self.n)) + self.keep("q", ceiling_divide(self.n, self.b)) + with owned(Count(self.q)) as (twice,): + twice.multiply_small(2) + self.keep("ell", ceiling_log(twice)) + self.keep("r", power_two(self.ell)) + self.keep("p", Count(self.b)) + self.p.multiply_small(2) + self.p.add(self.ell) + self.keep("component", Count(self.p)) + self.component.increment() + self.component.increment() + self.keep("shift", subtract(self.p, self.b)) + self.keep("output_bits", Count(self.n)) + self.output_bits.multiply_small(2) + with owned(Count(self.r)) as (records,): + records.multiply_small(2) + with owned(subtract(records, self.q)) as (zeros,): + self.keep("padding_bits", Count.product(zeros, self.component)) + self.padding_bits.multiply_small(2) + self.keep("dummy_bits", Count.product(self.r, self.component)) + self.dummy_bits.multiply_small(2) + with owned(subtract(self.p, self.one)) as (exponent,): + self.keep("coefficient_limit", power_two(exponent)) + + def close(self): + for value in reversed(tuple(self.fields.values())): + value.close() + self.fields.clear() diff --git a/research/physical-fft-word/fft_word_sources.py b/research/physical-fft-word/fft_word_sources.py new file mode 100644 index 0000000000..77662c1454 --- /dev/null +++ b/research/physical-fft-word/fft_word_sources.py @@ -0,0 +1,84 @@ +"""Open the corrected normalized product and its single physical cohort.""" +from contextlib import contextmanager +from hashlib import sha256 +import importlib +import importlib.util +import json +from pathlib import Path, PurePosixPath +import sys +import tarfile +import tempfile + +HERE = Path(__file__).resolve().parent +PACKAGE = "research/physical-ring-product" +HEAD = "62264289adb01f3ba4930cd0154c75887f96203c" +DIGEST = "c03d4b056ccd3db860c93579f6525e0bb1baea31cff879eb07135c99432ef159" +MANIFEST = "39c6eb4f1c2d38fdf8e44ae5c6b16bfe5315ff796ac60f1f6e48161ad3e2bab4" +_active = None + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(path=None): + path = HERE / "inputs/ring-export.tar" if path is None else Path(path) + require(path.is_file() and not path.is_symlink(), "regular FFT-word source export") + require(sha256(path.read_bytes()).hexdigest() == DIGEST, "pinned FFT-word source bytes") + with tarfile.open(path, "r:") as archive: + members = archive.getmembers() + names = [item.name for item in members] + require(len(names) == 27 and len(set(names)) == 27, "complete unique FFT-word source export") + for item in members: + part = PurePosixPath(item.name) + require(item.isfile() and not part.is_absolute() and ".." not in part.parts + and "\\" not in item.name and part.as_posix() == item.name + and item.size <= 2**27, "bounded regular FFT-word source member") + raw = archive.extractfile(".research-export.json").read() + require(sha256(raw).hexdigest() == MANIFEST, "pinned FFT-word source receipt") + receipt = json.loads(raw) + require((receipt["commit"], receipt["package"], len(receipt["files"])) + == (HEAD, PACKAGE, 26), "FFT-word source identity") + require(set(names) == {row["path"] for row in receipt["files"]} | {".research-export.json"}, + "exact FFT-word source member set") + for row in receipt["files"]: + data = archive.extractfile(row["path"]).read() + require(len(data) == row["size"] and sha256(data).hexdigest() == row["sha256"], + "FFT-word source member: " + row["path"]) + return path + + +def active(): + require(_active is not None, "authenticated FFT-word cohort") + return _active + + +@contextmanager +def opened(): + global _active + require(_active is None and "ring_sources" not in sys.modules, "cold FFT-word namespace") + path = authenticate() + old_path = sys.path[:] + with tempfile.TemporaryDirectory(prefix="fft-word-source-") as directory: + with tarfile.open(path, "r:") as archive: + archive.extractall(directory, filter="data") + package = Path(directory) / PACKAGE + spec = importlib.util.spec_from_file_location("ring_sources", package / "ring_sources.py") + source = importlib.util.module_from_spec(spec) + sys.modules["ring_sources"] = source + try: + spec.loader.exec_module(source) + sys.path.insert(0, str(package)) + with source.opened() as state: + _active = state + state.ring_package = package + state.ring = importlib.import_module("ring_engine") + require(Path(state.ring.__file__).resolve() == (package / "ring_engine.py").resolve(), + "actual authenticated normalized-product code") + yield state + finally: + _active = None + sys.path[:] = old_path + if sys.modules.get("ring_sources") is source: + del sys.modules["ring_sources"] diff --git a/research/physical-fft-word/inputs/ring-export.tar b/research/physical-fft-word/inputs/ring-export.tar new file mode 100644 index 0000000000..004c660f78 Binary files /dev/null and b/research/physical-fft-word/inputs/ring-export.tar differ diff --git a/research/physical-fft-word/verify.py b/research/physical-fft-word/verify.py new file mode 100644 index 0000000000..6df2a92bef --- /dev/null +++ b/research/physical-fft-word/verify.py @@ -0,0 +1,29 @@ +"""Cold entry point for exact FFT-word checks.""" +import argparse +import importlib +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from fft_word_sources import opened, require + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--suite", required=True) + args = parser.parse_args() + require(args.suite in ("fft", "base", "codec", "plan", "failures", "sources", "budget"), + "registered FFT-word suite") + with opened(): + name = "fft_word_check_" + args.suite + module = importlib.import_module(name) + require(Path(module.__file__).resolve() == Path(__file__).resolve().parent / (name + ".py"), + "package-local FFT-word checker") + result = module.run() + print(json.dumps({"status": "PASS_PHYSICAL_FFT_WORD", "suite": args.suite, + "evidence": result}, sort_keys=True)) + + +if __name__ == "__main__": + main()