diff --git a/.github/workflows/pr256-fourier-audit.yml b/.github/workflows/pr256-fourier-audit.yml new file mode 100644 index 0000000000..db5cbe9732 --- /dev/null +++ b/.github/workflows/pr256-fourier-audit.yml @@ -0,0 +1,37 @@ +name: PR256 complex proof audit + +on: + push: + paths: + - 'research/pr256-fourier-audit/**' + - '.github/workflows/pr256-fourier-audit.yml' + pull_request: + paths: + - 'research/pr256-fourier-audit/**' + - '.github/workflows/pr256-fourier-audit.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + finite-audit: + runs-on: ubuntu-24.04 + timeout-minutes: 10 + strategy: + fail-fast: false + matrix: + python-version: ['3.11', '3.13', '3.14'] + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7 + with: + python-version: ${{ matrix.python-version }} + - name: Replay finite program, source bindings, and retained evidence + run: python3 -B research/pr256-fourier-audit/verify.py + - name: Reject corrupted programs, statements, and evidence + run: python3 -B research/pr256-fourier-audit/test_audit.py + - name: Require unchanged tracked artifacts + run: git diff --exit-code diff --git a/research/pr256-fourier-audit/MANIFEST.json b/research/pr256-fourier-audit/MANIFEST.json new file mode 100644 index 0000000000..d5aacb63ef --- /dev/null +++ b/research/pr256-fourier-audit/MANIFEST.json @@ -0,0 +1,29 @@ +{ + "description": "Immutable audit inputs and historical evidence; new audit code is reviewed through the PR diff.", + "files": { + "evidence/five_stage_lean_receipt.json": "195df11c9eb43f56a671bd5f90c96f810bac8ea954cde85dc44c100e04190604", + "evidence/five_stage_openai_origin.json": "ee6e89f2a099324c21da1e7385d2b5c82b64cdbfd225f91e076cd1c8320738c9", + "evidence/five_stage_regeneration_receipt.json": "a47ada8a3095ce1ffc58c43dac9d7dd564069caee184c6f0af4dd830af94a8e4", + "evidence/logs/axioms.log.gz": "c9811ae280c91401bf56660ca3d56fcda28ceee727fb7ab633925278aff0c25d", + "evidence/logs/build.log.gz": "d25a3cf89b770b7a0c7f0ad32adbf2a960d195eb557a3254103e07f39d6326c4", + "evidence/logs/compare_fourier.log.gz": "b379cde884336eb5139bbbd3ab46883e66bc9058390a9223b2c318d61a4c2598", + "evidence/logs/compare_wht.log.gz": "0fc07ebd9dfbaeb4ff419cb4e31a068a69a1075bf3af730d183e9a2e659dfbc1", + "evidence/logs/regenerate_certificate.log.gz": "fe780019ca79162cfcd68e284d73db0d79456715e9c55298e58449cf1954c7e2", + "evidence/logs/regenerate_fourier.log.gz": "6ed176c454f047733b22fed8c76c1f9966b630edd8f9e4c0291b3f0b36ad0a1c", + "evidence/logs/regenerate_program.log.gz": "3f2e7bae2862b423d3bdcf2b00f889763bde77a7aa79a1da14eef83f474adb8e", + "evidence/logs/toolchain.log.gz": "f0d1c3b28558d3555ba5e0322441cbcbcdc20b163d531a1ac14b5e0ace4bcf57", + "evidence/pr256_source_files.json": "3a8341035c7ef0ede3d8d43812aa4bb2ffc78287c8c3424d74b4b98cb8bb7103", + "evidence/proof_source_files.json": "6010ff79f3128533fddc076e223225d58b59d22761746b6119f7ccfd51071ac9", + "expected.json": "295a3f5c0e6843db7fec76b25609d93e0a7aeb60fb79c394e1851ebb6a8789f1", + "inputs/FOURIER_NOTICE": "9419dd03a2f52cf8bdfc4d18216ce29f263ab583b27f01ced8e420985bcb7c81", + "inputs/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "inputs/SOURCE.json": "00f5689fba8d1edc1741376c14a5ad6cdf5e0718dd24af9881949a6bc7cd2cf1", + "inputs/fourier-proof-source.tar.gz": "871f47a16d2571dbcebc2ef61914e85d96b7b44f6d59579da246e13294d5658b", + "inputs/gcert-program-233/NOTICE": "c1c95d22cfb0f455aca64b4bee4cab900829641b8f041280e7aa88034491c87d", + "inputs/gcert-program-233/SOURCE.json": "9ce463476af549c04de4705b1bf0c8f7f18d473dc0817883066ad5e2136d90b5", + "inputs/gcert-program-233/certificate/expected.json": "c0e3d245bf7e458ff86288eb47672491c9efee28181b570f1a3f17c8d915f766", + "inputs/gcert-program-233/certificates/gcert1-p11-pr233-flow.json.gz": "09ceba1c0ea17282da155b937c8463669b913443c20f45fe2a7e6e024cb2d33a", + "inputs/gcert-program-233/gx/gx.py": "6f3dc8bb639933227a8dae181ec4a542e85c7276be9c9e330f49518e7b630b95" + }, + "schema": 1 +} diff --git a/research/pr256-fourier-audit/NOTICE b/research/pr256-fourier-audit/NOTICE new file mode 100644 index 0000000000..124f7f2473 --- /dev/null +++ b/research/pr256-fourier-audit/NOTICE @@ -0,0 +1,28 @@ +PR256 program / Fourier-proof reproduction audit +Copyright 2026 Ryan Shea. New audit code and documentation: Apache-2.0. +Prepared with substantial OpenAI Codex assistance. + +This work adapts the checks and retains the original reproduction evidence from +shea256/fourier-transform-below-nlogn at a101b363b38e6bf7d309042c94ba5fa18a424fad. +It contributes source/program/proof consistency checks and a separate reproduction, +not a new exponent, network, formal framework, or proof of integer multiplication. + +OpenAI supplies the original exact arithmetic model and Fourier reduction. Doug +Colkitt supplies early parameter/network work and the community repository; Rohan +Arun and Swapnil Jain supply earlier community improvements and the research lineage. +Jacob Sussman supplies the five-stage geometry, frame formalization, certificate +format/checker, and formal Fourier framework. Chafik Boukhalfa supplies the PR200/233 +pairing, PR256 explicit program, and the stronger instantiation of that framework. +The circuit retains icekylinx's source-assisted construction, eumemic's v4 modules, +Avi Eisenberg's reconstruction/pairing, an664's sharing work, and the earlier +contributors named in the preserved source notices. The incoming package credits +SovereignSteak and hcg890 for five-stage composition and ledger work. + +inputs/gcert-program-233/NOTICE and inputs/FOURIER_NOTICE are retained byte for byte; +inputs/LICENSE accompanies them. The complete proof archive retains its licenses, +notices and source-specific OpenAI attribution. Do not reinterpret this audit as +authorship of the imported constructions or proofs. + +Metadata clarification: PR209 was contributed by Jacob Sussman and PR237 by Rohan +Arun. The PR256 notice groups those numbers with Rohan Arun; the original notice +is preserved unchanged. This note supplies the checked attribution alongside it. diff --git a/research/pr256-fourier-audit/README.md b/research/pr256-fourier-audit/README.md new file mode 100644 index 0000000000..530c4e05be --- /dev/null +++ b/research/pr256-fourier-audit/README.md @@ -0,0 +1,123 @@ +# PR256 complex program: reproduction and proof consistency audit + +This adds a separate reproduction of Chafik Boukhalfa's PR256 and its instantiation +of Jacob Sussman's Lean framework. **No new multiplication kappa, network, or +Fourier exponent is claimed.** The contribution is a reproducible audit linking +the two source packages, exact arithmetic checks, and retained build evidence. + +## Pinned sources + +| Source | Revision | Role | +| --- | --- | --- | +| [CrocSwap PR256](https://github.com/CrocSwap/integer-mult-bounds/pull/256) | `db3f75cdc5f03f3131d48fb220f6bf1958404ff3` | Explicit complex program and source regeneration | +| [Fourier proof PR2](https://github.com/jacobalansussman/wht-power-saving-lean/pull/2) | `fd19e46b728faa414cbfbf91b01a6a0b7903375d` | Sussman's framework with Boukhalfa's PR233 instantiation | +| [OpenAI formal sources](https://github.com/openai/math/tree/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean) | `fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb` | Original model, Fourier reduction, and challenge | +| [Downstream reproduction](https://github.com/shea256/fourier-transform-below-nlogn/tree/a101b363b38e6bf7d309042c94ba5fa18a424fad) | `a101b363b38e6bf7d309042c94ba5fa18a424fad` | Ryan Shea's checks, source audit, and build receipts | + +The proof extends Sussman revision `f010392c923279e3dd59ef3aa5fedad23affc5fd`. +Lean is 4.34.1; Mathlib is `d13f23b723b8a846827a245b89c10fc7d3f11612`. +The complete 456-file proof source archive is included, without compiled objects. +Only the PR256 inputs needed for the finite audit are copied here; its complete +producer is available at the pinned revision above. Original notices are retained. + +## Offline finite audit + +From the repository root, using Python 3.11 or later and no third-party packages: + +```sh +python3 -B research/pr256-fourier-audit/verify.py +python3 -B research/pr256-fourier-audit/test_audit.py +``` + +The first command: + +1. Checks source pins and runs Sussman's unmodified `gx.check1` on the explicit + PR233 program: 12,052 registers, 18,248 frames, 52,300 gates, and 69,683 + invocation blocks. Exact scalar replay covers all source columns; restoration + of arbitrary dirty scratch is supplied by the Lean invocation theorem. +2. Reconstructs the five-stage histogram and checks `m=110`, `W=14692`, rank + 1613040, deficit 3080, 358975 children and maximum child width 46. +3. Independently bounds the normalized moment using exact rational logarithm and + exponential enclosures at `a=7547361/10^10`. It checks the Lean engine's + finite-fill correction at `s=40`, the positive Fourier gap + `a - delta = 1/10^10`, and failure at `7547365/10^10` for this histogram. +4. Requires the PR256 and Lean programs to agree in every mathematical field + (only the descriptive `derived_from` string differs), then checks the Lean + histogram and exponent literals. It compares the Fourier challenge with the + original after accounting for comments, seven renamed declarations and the + stronger exponent. +5. Checks all 89 imported OpenAI Lean modules, the original challenge and the + toolchain against the 91-file origin ledger. These were fetched separately + from the immutable OpenAI revision during the recorded source audit. +6. Binds the historical reproduction receipts to their compressed logs and all + 456 archived source hashes. Checking a recorded receipt does not rerun Lean. + +Optional full-checkout comparisons require no network: + +```sh +python3 -B research/pr256-fourier-audit/verify.py \ + --program-source /path/to/pr256-checkout \ + --proof-source /path/to/pinned-fourier-checkout \ + --openai-source /path/to/pinned-openai-checkout +``` + +They compare the 20 program-package files, 456 proof-source files and 91 original +OpenAI files with the pinned ledgers, irrespective of the checkout's branch name. The default audit +does not rerun the producer or a full Clifford/DFT computation. + +## Reproducing the Lean build + +Install `leanprover/lean4:v4.34.1`, then run: + +```sh +python3 -B research/pr256-fourier-audit/reproduce_lean.py \ + --work-dir /tmp/pr256-lean-rebuild --lake lake --threads 2 \ + --receipt /tmp/pr256-lean-rebuild-receipt.json +``` + +This extracts the complete pinned source (or checks existing source bytes), +downloads the pinned Mathlib cache, regenerates the 41 certificate and 14 +Fourier-chain files, builds the proof, audits axioms, and runs upstream +`tools/Compare.lean` for WHT, DFT and convolution. The two large scalar reductions +are staged sequentially to reduce peak memory. Allow several GB of storage and +substantial memory; the recorded reproduction used a 32 GiB macOS arm64 machine. + +The original fresh project build passed in 2625.5 seconds, with Mathlib's compiled +cache. The WHT and Fourier comparisons passed in 33.7 and 42.6 seconds. The three +audited final theorems used only `propext`, `Classical.choice`, and `Quot.sound`. +The original combined build temporarily paused one large scalar reduction until +the other completed; it then resumed successfully, without changing source. +The script now stages those targets sequentially. The receipt retains the actual +original commands and is not relabeled as a new run. + +The full PR256 producer regeneration also passed (188.6 seconds), using Python +3.11, NumPy 2.3.5 and SciPy 1.17.0. To rerun that separately: + +```sh +git clone https://github.com/chafreaky/integer-mult-bounds /tmp/pr256-source +git -C /tmp/pr256-source checkout --detach db3f75cdc5f03f3131d48fb220f6bf1958404ff3 +OPENBLAS_NUM_THREADS=1 OMP_NUM_THREADS=1 \ + uv run --python 3.11 --with numpy==2.3.5 --with scipy==1.17.0 \ + python -B /tmp/pr256-source/research/gcert-program-233/verify.py +``` + +## What this establishes for multiplication + +| Evidence | Established scope | Multiplication obligations remaining | +| --- | --- | --- | +| Exact program and histogram checks | The pinned finite complex program and its five-stage accounting agree with the formal input | No bit-side construction or outer multiplication assembly is checked here | +| Lean project and statement comparisons | The upstream WHT and all-length exact DFT/convolution theorems in OpenAI's family-130 RAM model | Finite precision/recovery, bit costs, fixed-tape implementation and the inherited multiplication-specific all-size interfaces are not proved | +| OpenAI source comparison | Imported model/reduction files match the identified OpenAI revision | Human assessment of formal statements and assumptions remains separate | +| Receipt and log hashes | The recorded successful runs are bound to these sources | Hashes alone do not independently attest that an execution occurred | + +The Fourier theorem has `delta=7547360/10^10`. It is an exact-complex-arithmetic +result with supplied roots and unrestricted coefficients, not a multiplication +theorem or practical FFT benchmark. The historical reproduction ran neither the +official Linux comparator nor a second kernel and is not independent human +mathematical review. Boukhalfa later reported official-comparator success in +[`837dc313`](https://github.com/chafreaky/wht-power-saving-lean/commit/837dc3130adc79f7b7ab4ddd56c15576bbd766b0); +that documentation-only update is distinct from this pinned local reproduction. + +See [NOTICE](NOTICE) for attribution and [VALIDATION.md](VALIDATION.md) for the +checks of this contribution. The root selected result and all existing witnesses +remain unchanged. diff --git a/research/pr256-fourier-audit/VALIDATION.md b/research/pr256-fourier-audit/VALIDATION.md new file mode 100644 index 0000000000..21e56afbf7 --- /dev/null +++ b/research/pr256-fourier-audit/VALIDATION.md @@ -0,0 +1,42 @@ +# Validation of this audit contribution + +Prepared against CrocSwap main `3b6b66891c0ac888521cf591fe306c6286601d4f`. +This is a separate AI-assisted reproduction, not independent human mathematical +review. The bound and proof remain the credited upstream authors' results. + +## Audit package + +- Offline finite verifier: passed on Python 3.11, 3.13 and 3.14. +- Eleven audit controls (two positive and nine negative): passed; altered stock/child counts, an unrecorded + exponent, a weakened quantifier, an extra axiom, a missing build, a wrong source + revision and a changed build log are rejected. Optimized Python is refused. +- Full-checkout comparison: all 20 pinned PR256 package files and all 456 proof + source files matched the separate checked-out revisions. +- OpenAI origin: all 91 ledger files were downloaded again from the immutable + OpenAI revision and matched, including all 89 imported OAI modules. +- Ported Lean reproduction wrapper: passed against the existing pinned build, + with `--cache-ready`. Both source generators reproduced their output; staged + scalar targets, combined build, axiom check, WHT comparison and Fourier + comparison all exited 0. This wrapper test reused the project build and is not + a second fresh build. The retained historical receipt records the earlier + successful fresh project compilation. +- Source syntax and whitespace checks passed. + +## Existing repository checks + +`make entrance-bank-verify` passed: selected-record validation, the complete +offline complex/bit construction, all 47 outer constraints, seven margins, +21 assembly controls, and the bank scheduling supplement. + +The full `make verify` regression run was invoked. At submission, its community, +producer, partial-gauge, three-stage-cover and paired-cube groups have passed; +the remaining groups are still pending. This is not a claim that the full suite +has passed. No existing source, certificate, selected-result pointer or root +documentation is changed by the contribution. + +## CI scope + +The added workflow repeats the offline finite audit and audit controls on +Ubuntu with Python 3.11, 3.13 and 3.14. It does not claim to run Lean or a second +kernel; full proof reproduction is the separate documented command. Configuring +the workflow does not itself constitute a successful CI run. diff --git a/research/pr256-fourier-audit/evidence/five_stage_lean_receipt.json b/research/pr256-fourier-audit/evidence/five_stage_lean_receipt.json new file mode 100644 index 0000000000..d5e42fb456 --- /dev/null +++ b/research/pr256-fourier-audit/evidence/five_stage_lean_receipt.json @@ -0,0 +1,135 @@ +{ + "axioms": { + "OAI.PowerSaving.RAM.hillsY_program": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "OAI.PowerSaving.convolution_mainY": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "OAI.PowerSaving.transform_mainY": [ + "Classical.choice", + "Quot.sound", + "propext" + ] + }, + "commands": [ + { + "command": [ + "/tmp/fourier-lean-toolchain/lean-4.34.1-darwin_aarch64/bin/lake", + "--version" + ], + "exit_code": 0, + "label": "toolchain", + "log_sha256": "36526a338068c343bedff5daa38fec328b4f722df1e8f0b5d026d4f0f908f3a3", + "seconds": 0.246 + }, + { + "command": [ + "/opt/homebrew/opt/python@3.14/bin/python3.14", + "-B", + "tools/gx/regen_check.py", + "tools/certificate/gcert1-p11-pr233-flow.json.gz", + "P233", + "B2Gp233" + ], + "exit_code": 0, + "label": "regenerate_certificate", + "log_sha256": "76952939fe619d8f344c0f88579f25929a183bd57b5e58fe974fec990f644d77", + "seconds": 28.829 + }, + { + "command": [ + "/opt/homebrew/opt/python@3.14/bin/python3.14", + "-B", + "tools/fourier/regen_check233.py" + ], + "exit_code": 0, + "label": "regenerate_fourier", + "log_sha256": "eee7ec63261d1ab58a527ada9ee3d47adfabb06385b49925fb831fbb74c0cb4e", + "seconds": 0.107 + }, + { + "command": [ + "/tmp/fourier-lean-toolchain/lean-4.34.1-darwin_aarch64/bin/lake", + "build", + "Work.GCert.Data.ChallengeB2Gp233x", + "Work.GCert.Data.SolutionB2Gp233x", + "Work.Fourier233.UniformFourierChallenge", + "Work.Fourier233.Main", + "Work.Fourier233.Axioms" + ], + "exit_code": 0, + "label": "build", + "log_sha256": "3e3f4b0f0f9a8c95ede2da69d08615bbc5ff763c5a06cc460b9f3f292153d783", + "seconds": 2625.459 + }, + { + "command": [ + "/tmp/fourier-lean-toolchain/lean-4.34.1-darwin_aarch64/bin/lake", + "env", + "lean", + "Work/Fourier233/Axioms.lean" + ], + "exit_code": 0, + "label": "axioms", + "log_sha256": "fd6ef1a75394038e0035b143c1135f4a4d0a6129982ac741bc8c80ebd3c145bd", + "seconds": 6.3 + }, + { + "command": [ + "/tmp/fourier-lean-toolchain/lean-4.34.1-darwin_aarch64/bin/lake", + "env", + "lean", + "--run", + "tools/Compare.lean", + "Work.GCert.Data.ChallengeB2Gp233x", + "Work.GCert.Data.SolutionB2Gp233x", + "OAI.PowerSaving.WHT.wht_main_block_B2Gp233x" + ], + "exit_code": 0, + "label": "compare_wht", + "log_sha256": "a1300346aee4d7a36791f6d5772969e772aa86d7d36ba9777dc521ec94ecc4f8", + "seconds": 33.7 + }, + { + "command": [ + "/tmp/fourier-lean-toolchain/lean-4.34.1-darwin_aarch64/bin/lake", + "env", + "lean", + "--run", + "tools/Compare.lean", + "Work.Fourier233.UniformFourierChallenge", + "Work.Fourier233.Main", + "OAI.PowerSaving.transform_mainY", + "OAI.PowerSaving.convolution_mainY" + ], + "exit_code": 0, + "label": "compare_fourier", + "log_sha256": "48ff3e708c9c38926a39ffd94f761d33245a6abe9aa5749e7233e8f14657fa97", + "seconds": 42.588 + } + ], + "finished_utc": "2026-10-10T03:12:13.637233+00:00", + "fresh_project_build": true, + "independent_human_review": false, + "independent_kernel_run": false, + "machine": "arm64", + "mathlib_commit": "d13f23b723b8a846827a245b89c10fc7d3f11612", + "mathlib_from_cache": true, + "numerical_dft_executed": false, + "official_comparator_run": false, + "platform": "macOS-26.6.2-arm64-arm-64bit-Mach-O", + "schema": 1, + "source_archive_sha256": "871f47a16d2571dbcebc2ef61914e85d96b7b44f6d59579da246e13294d5658b", + "source_commit": "fd19e46b728faa414cbfbf91b01a6a0b7903375d", + "source_files_checked": 456, + "started_utc": "2026-10-10T02:26:36.346772+00:00", + "statement_comparison": "upstream tools/Compare.lean; WHT, all-length DFT and convolution passed", + "success": true, + "threads": 2, + "toolchain": "Lake version 5.0.0-src+5045d00 (Lean version 4.34.1)" +} diff --git a/research/pr256-fourier-audit/evidence/five_stage_openai_origin.json b/research/pr256-fourier-audit/evidence/five_stage_openai_origin.json new file mode 100644 index 0000000000..dd8e3e3a01 --- /dev/null +++ b/research/pr256-fourier-audit/evidence/five_stage_openai_origin.json @@ -0,0 +1,373 @@ +{ + "commit": "fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb", + "files": { + "OAI/Computability/FourierCircuit/Core.lean": { + "sha256": "45fd659a66b3bb93ea9e55ebf0c06fde26a3038e2c7fb369cbd8dada371603a6", + "upstream_path": "lean/OAI/Computability/FourierCircuit/Core.lean" + }, + "OAI/Computability/FourierTransform/AddressTables.lean": { + "sha256": "d833ec98fbf558c2fbea4e7acb608f69cd703eb98ed6257de879d4ff1ef8db0f", + "upstream_path": "lean/OAI/Computability/FourierTransform/AddressTables.lean" + }, + "OAI/Computability/FourierTransform/ArbitraryLength.lean": { + "sha256": "b7be3f6b003cc8beac973ab8aaf410dd6db84b44a7acad66eaac4f40b59cb876", + "upstream_path": "lean/OAI/Computability/FourierTransform/ArbitraryLength.lean" + }, + "OAI/Computability/FourierTransform/Asymptotics.lean": { + "sha256": "a3037d47558d5db18b282fe48b0e0cb302f7efab37ce804caf9b6574c482b2a5", + "upstream_path": "lean/OAI/Computability/FourierTransform/Asymptotics.lean" + }, + "OAI/Computability/FourierTransform/BinaryBasis.lean": { + "sha256": "ab9787433fd1feb0a90557334f0b7409fae080c2ee838adf1c6175a4e0314aa6", + "upstream_path": "lean/OAI/Computability/FourierTransform/BinaryBasis.lean" + }, + "OAI/Computability/FourierTransform/BinaryFFT.lean": { + "sha256": "fa2e7d5f65160fdf98c7208ba1b837aa14da1a306c824afa7065a731036671c8", + "upstream_path": "lean/OAI/Computability/FourierTransform/BinaryFFT.lean" + }, + "OAI/Computability/FourierTransform/BinaryFrames.lean": { + "sha256": "a1a613f0be5be321d16cdfdb6dfe65611cb06bf6693709a143cdf32b41d07245", + "upstream_path": "lean/OAI/Computability/FourierTransform/BinaryFrames.lean" + }, + "OAI/Computability/FourierTransform/BitLayout.lean": { + "sha256": "4cd9c100cd39881060cc4493f544ad85edfb8bfbfefbc1adc5140889c4eb356f", + "upstream_path": "lean/OAI/Computability/FourierTransform/BitLayout.lean" + }, + "OAI/Computability/FourierTransform/ChineseRemainder.lean": { + "sha256": "37d9615b194d34e2ea52cf6de5047bef7814a57608ad2d8959524f62f219e45b", + "upstream_path": "lean/OAI/Computability/FourierTransform/ChineseRemainder.lean" + }, + "OAI/Computability/FourierTransform/ChirpConvolution.lean": { + "sha256": "8b8c951d60beef2fc0f8461ce798295bffcf24b426b457a6c22025516e1e4bbc", + "upstream_path": "lean/OAI/Computability/FourierTransform/ChirpConvolution.lean" + }, + "OAI/Computability/FourierTransform/ChunkCompiler.lean": { + "sha256": "0ca0a87c35b29db93be5f8c5defa638f79d8fd320b0080fd5d911e9bb806b82d", + "upstream_path": "lean/OAI/Computability/FourierTransform/ChunkCompiler.lean" + }, + "OAI/Computability/FourierTransform/ChunkPrograms.lean": { + "sha256": "c7d4dd887cd835c8edb9de82e5c28e9ac4298de6e58f581b3839fe9ba7c549cb", + "upstream_path": "lean/OAI/Computability/FourierTransform/ChunkPrograms.lean" + }, + "OAI/Computability/FourierTransform/CirculantUpdates.lean": { + "sha256": "acee56a87a61938327ef89d6797f13c08e54ca5759c295c4dff2ddd4d5b75f8f", + "upstream_path": "lean/OAI/Computability/FourierTransform/CirculantUpdates.lean" + }, + "OAI/Computability/FourierTransform/ColumnAddresses.lean": { + "sha256": "de7532b3e40c02b44b363e4c13989cbf41fbee0e2ae8d37f59a461084f98bfc3", + "upstream_path": "lean/OAI/Computability/FourierTransform/ColumnAddresses.lean" + }, + "OAI/Computability/FourierTransform/CompilerEnvironment.lean": { + "sha256": "065071798eb7d6b6bb01420a9ef29eb07805ea134305899c7fe9bb1f9a8663e6", + "upstream_path": "lean/OAI/Computability/FourierTransform/CompilerEnvironment.lean" + }, + "OAI/Computability/FourierTransform/ConvolutionProgram.lean": { + "sha256": "a5792081ddb71d2f4813052d65e722b82accbf4ece96d6c69ad3406000c0558c", + "upstream_path": "lean/OAI/Computability/FourierTransform/ConvolutionProgram.lean" + }, + "OAI/Computability/FourierTransform/Cost.lean": { + "sha256": "574eb175d87bcddc323efb4b2227975afd28a52079d3657c058ba9568e539801", + "upstream_path": "lean/OAI/Computability/FourierTransform/Cost.lean" + }, + "OAI/Computability/FourierTransform/DirectionalWords.lean": { + "sha256": "eb9689b4f4e1e6631bb53208afd92b2f2dd612d5ddd85fa8bb40f8596f81d64d", + "upstream_path": "lean/OAI/Computability/FourierTransform/DirectionalWords.lean" + }, + "OAI/Computability/FourierTransform/DisjointIntervals.lean": { + "sha256": "a641f52e1d1e35e462664c783b748942b12bc64b7747eb9c4deeb477a0ba3c9c", + "upstream_path": "lean/OAI/Computability/FourierTransform/DisjointIntervals.lean" + }, + "OAI/Computability/FourierTransform/FourierCompilation.lean": { + "sha256": "f03c9b92c3be39fde0cbd4040bcff850bbd20c436d0cd16f7530073ab9c76fba", + "upstream_path": "lean/OAI/Computability/FourierTransform/FourierCompilation.lean" + }, + "OAI/Computability/FourierTransform/FourierIdentities.lean": { + "sha256": "8a4f93c3f087ddaa55a8463fbe8c150e61f6ac8e41ed8c9c61add0670fe1cad7", + "upstream_path": "lean/OAI/Computability/FourierTransform/FourierIdentities.lean" + }, + "OAI/Computability/FourierTransform/FourierWords.lean": { + "sha256": "8a9e4ba63c2668b7133db1460a13507479598e57fd50243c59e3ac365730d2f0", + "upstream_path": "lean/OAI/Computability/FourierTransform/FourierWords.lean" + }, + "OAI/Computability/FourierTransform/FrameLifting.lean": { + "sha256": "31543b1edc69e19597af8b0035e43c8183c8e9640ed99ee5b8a6b87f77ae0c7b", + "upstream_path": "lean/OAI/Computability/FourierTransform/FrameLifting.lean" + }, + "OAI/Computability/FourierTransform/Goal.lean": { + "sha256": "879a7d19393b7f162e1711fba08e10626444b9e34b5183ead3b7832ba462c344", + "upstream_path": "lean/OAI/Computability/FourierTransform/Goal.lean" + }, + "OAI/Computability/FourierTransform/IntegerPrograms.lean": { + "sha256": "028080a8b977f88300fdb536af94214eb72b117af026518e1c08b84ac50dbb84", + "upstream_path": "lean/OAI/Computability/FourierTransform/IntegerPrograms.lean" + }, + "OAI/Computability/FourierTransform/IntervalEffects.lean": { + "sha256": "a34be872372439cbcfa4a063e360c12ff5b35b5d7fa925a10e49fa20d268fc1c", + "upstream_path": "lean/OAI/Computability/FourierTransform/IntervalEffects.lean" + }, + "OAI/Computability/FourierTransform/IntervalPrograms.lean": { + "sha256": "ecdbfed1b40da9d117170892a0adc207d381f6d2b702868fdb8bc7a0b58e2cc6", + "upstream_path": "lean/OAI/Computability/FourierTransform/IntervalPrograms.lean" + }, + "OAI/Computability/FourierTransform/LayerCompilation.lean": { + "sha256": "23e287c7c7ff066cf662d496d8c8108a80662229354de84abb59fd4da785c927", + "upstream_path": "lean/OAI/Computability/FourierTransform/LayerCompilation.lean" + }, + "OAI/Computability/FourierTransform/LayerPrograms.lean": { + "sha256": "035f13e90785557988a35074ba30babefda81dda352067d5c7b636f3fb82005d", + "upstream_path": "lean/OAI/Computability/FourierTransform/LayerPrograms.lean" + }, + "OAI/Computability/FourierTransform/LayerWords.lean": { + "sha256": "4e42fe8d2807ba5dd10adb7cc64e3c9c95bb1c2f9d5171e91efd37c24f44b01b", + "upstream_path": "lean/OAI/Computability/FourierTransform/LayerWords.lean" + }, + "OAI/Computability/FourierTransform/Layout.lean": { + "sha256": "133ccff630aeb568807bddf3791bf2f9a6fe8f46672ea3dc0f84a3f9df3e9743", + "upstream_path": "lean/OAI/Computability/FourierTransform/Layout.lean" + }, + "OAI/Computability/FourierTransform/LayoutPrograms.lean": { + "sha256": "681d453c33d254b3cec43913ce388fd435f340f7639338f8e67d3d3d28c7cbbd", + "upstream_path": "lean/OAI/Computability/FourierTransform/LayoutPrograms.lean" + }, + "OAI/Computability/FourierTransform/LengthSelection.lean": { + "sha256": "41aa79c7d836733adfecf597f07ab1b020762edd629b2dca49a26f8b03b3b2c2", + "upstream_path": "lean/OAI/Computability/FourierTransform/LengthSelection.lean" + }, + "OAI/Computability/FourierTransform/LocalCompiler.lean": { + "sha256": "ef7ec7017261090b0a798fc6082cda77981fd34d0ff18a5ccfd1f2a1d20a0a50", + "upstream_path": "lean/OAI/Computability/FourierTransform/LocalCompiler.lean" + }, + "OAI/Computability/FourierTransform/LocalPreparation.lean": { + "sha256": "a55545e2a129689bc574a075fccd2ef63c67654011566fc65b0085d453363efc", + "upstream_path": "lean/OAI/Computability/FourierTransform/LocalPreparation.lean" + }, + "OAI/Computability/FourierTransform/LoopBounds.lean": { + "sha256": "8799c6b2539f7b831288b1454a44c8b03912d17f75077362a17983dcd366b351", + "upstream_path": "lean/OAI/Computability/FourierTransform/LoopBounds.lean" + }, + "OAI/Computability/FourierTransform/Main.lean": { + "sha256": "0b2b9f758ff41d4b13b6420451d04fbbd84826a8a2594eb8d5b2311a3861ef55", + "upstream_path": "lean/OAI/Computability/FourierTransform/Main.lean" + }, + "OAI/Computability/FourierTransform/MeasuredFit.lean": { + "sha256": "da9cafbf4d857f759880d9198969cabd8ed31676fb29fa0d22dce2b8dca9c1c2", + "upstream_path": "lean/OAI/Computability/FourierTransform/MeasuredFit.lean" + }, + "OAI/Computability/FourierTransform/MeasuredPrograms.lean": { + "sha256": "03e03bbefec631cec7dec22ee199f97760a3f6d6b4b4f58a76be180a3f767628", + "upstream_path": "lean/OAI/Computability/FourierTransform/MeasuredPrograms.lean" + }, + "OAI/Computability/FourierTransform/NetworkInvocation.lean": { + "sha256": "1f3a4c4b9f30548c76a2c999c239f8ed9f5480b9a14671deba01ed37b092abb7", + "upstream_path": "lean/OAI/Computability/FourierTransform/NetworkInvocation.lean" + }, + "OAI/Computability/FourierTransform/NetworkLabels.lean": { + "sha256": "3c4057cfea65c2305fb2a323feac7ecd49fbd831d84961da6130665e6db09851", + "upstream_path": "lean/OAI/Computability/FourierTransform/NetworkLabels.lean" + }, + "OAI/Computability/FourierTransform/NetworkRoles.lean": { + "sha256": "00c826532d66eece5e7c6b8714a7402d7936f07f7d8a2b8d0fcf8639e0fa2289", + "upstream_path": "lean/OAI/Computability/FourierTransform/NetworkRoles.lean" + }, + "OAI/Computability/FourierTransform/NetworkStages.lean": { + "sha256": "60582947d315fd090f0a5a019b636602c4bb176146843e1c4690ad166c8e16a6", + "upstream_path": "lean/OAI/Computability/FourierTransform/NetworkStages.lean" + }, + "OAI/Computability/FourierTransform/NewtonFactorization.lean": { + "sha256": "264bf2818b36435275fd79281361c5e7d80ba5a7cd7e0e4e6a36a8aae744a15d", + "upstream_path": "lean/OAI/Computability/FourierTransform/NewtonFactorization.lean" + }, + "OAI/Computability/FourierTransform/PackingPrograms.lean": { + "sha256": "4310c0f0bc1c142bb089c2a3d59ed5392f15d25df6fc9c2bca2d4c7674f5c52f", + "upstream_path": "lean/OAI/Computability/FourierTransform/PackingPrograms.lean" + }, + "OAI/Computability/FourierTransform/ParameterPrograms.lean": { + "sha256": "acc759c49833108366684ff9c35f8343c4a3d8976a3d7244be2e40d57c95c686", + "upstream_path": "lean/OAI/Computability/FourierTransform/ParameterPrograms.lean" + }, + "OAI/Computability/FourierTransform/PolynomialBounds.lean": { + "sha256": "904c9e90fd009e0a56a1b35eb4ed54068653e6487a82850ccc1510cb18cf6ab1", + "upstream_path": "lean/OAI/Computability/FourierTransform/PolynomialBounds.lean" + }, + "OAI/Computability/FourierTransform/PolynomialPrograms.lean": { + "sha256": "6dcb0251326a8988b5101ddabbd7b0ff582e0f39646fddc83adae0a07b8a92af", + "upstream_path": "lean/OAI/Computability/FourierTransform/PolynomialPrograms.lean" + }, + "OAI/Computability/FourierTransform/PowerTables.lean": { + "sha256": "372818fd8c12356a5d959286271be0973abab6ecf9521ce1d6b49f922f423d0e", + "upstream_path": "lean/OAI/Computability/FourierTransform/PowerTables.lean" + }, + "OAI/Computability/FourierTransform/PrefixTraversal.lean": { + "sha256": "eb84ca868ca680a66ce14b9a1d27258b733c5dd240f69411ec8b06c9cc84f7d5", + "upstream_path": "lean/OAI/Computability/FourierTransform/PrefixTraversal.lean" + }, + "OAI/Computability/FourierTransform/PrimeSelection.lean": { + "sha256": "c94d8aef61f51b0d658faa64e7323510cf3fa9cb88d6db25542af7287b8c1b76", + "upstream_path": "lean/OAI/Computability/FourierTransform/PrimeSelection.lean" + }, + "OAI/Computability/FourierTransform/ProductMatrix.lean": { + "sha256": "7508fa85fc588567237dc8133e17a26d1883253df72f5e2f1459a16f33434a2e", + "upstream_path": "lean/OAI/Computability/FourierTransform/ProductMatrix.lean" + }, + "OAI/Computability/FourierTransform/ProgramBounds.lean": { + "sha256": "904132230871e8693bafb126ee0fa6147140f83516add46b6e130bb4bdc0334a", + "upstream_path": "lean/OAI/Computability/FourierTransform/ProgramBounds.lean" + }, + "OAI/Computability/FourierTransform/ProgramConstruction.lean": { + "sha256": "b3294e211d08f170e4ca86cd6e4a8be27adae7b538da1d22d7ee03b8f007b4d0", + "upstream_path": "lean/OAI/Computability/FourierTransform/ProgramConstruction.lean" + }, + "OAI/Computability/FourierTransform/RAM.lean": { + "sha256": "4eb8a7cbd1566b9a0537c3423e32528c3d6be691a4780bd549768a96e568fa8d", + "upstream_path": "lean/OAI/Computability/FourierTransform/RAM.lean" + }, + "OAI/Computability/FourierTransform/RecursionBounds.lean": { + "sha256": "eeb1d9752680fdf0c4206ca8fc1369601a45715c7f3d5c91bb9c2d378d212f38", + "upstream_path": "lean/OAI/Computability/FourierTransform/RecursionBounds.lean" + }, + "OAI/Computability/FourierTransform/RecursiveBatches.lean": { + "sha256": "8afd2aed3ad05a145b8ddbca76cdbad6c3fc249c805bc972825b6396248eae97", + "upstream_path": "lean/OAI/Computability/FourierTransform/RecursiveBatches.lean" + }, + "OAI/Computability/FourierTransform/RecursiveContract.lean": { + "sha256": "b0e7deaf0efee6d10ef18efafa4cd5ff3e8513d7c507a23aa16ed39a089c2737", + "upstream_path": "lean/OAI/Computability/FourierTransform/RecursiveContract.lean" + }, + "OAI/Computability/FourierTransform/RegisterBounds.lean": { + "sha256": "5e1a314a8cbdc73cf5247c294f4906fdb205dac34c0be1a22d0bd3e51603c353", + "upstream_path": "lean/OAI/Computability/FourierTransform/RegisterBounds.lean" + }, + "OAI/Computability/FourierTransform/RoleArrays.lean": { + "sha256": "929f8de89d880c898872fb031326ac316f783e61b85ac589f95c5a064f10e6f0", + "upstream_path": "lean/OAI/Computability/FourierTransform/RoleArrays.lean" + }, + "OAI/Computability/FourierTransform/RootPreparation.lean": { + "sha256": "d51bbe713d36fe5dbb2549f2a95d138f346087d68593de446c9ce07f2cc534d9", + "upstream_path": "lean/OAI/Computability/FourierTransform/RootPreparation.lean" + }, + "OAI/Computability/FourierTransform/ScalarNetwork.lean": { + "sha256": "121a5d597f7ae266206d6e113104c98765f30f3ff28f72ccdef64c025c3d0eb5", + "upstream_path": "lean/OAI/Computability/FourierTransform/ScalarNetwork.lean" + }, + "OAI/Computability/FourierTransform/ScalarPreparation.lean": { + "sha256": "1c61342491f4871f8e921c359e74b64c38f3b7c3eccf99ab9b16a399aa635a8e", + "upstream_path": "lean/OAI/Computability/FourierTransform/ScalarPreparation.lean" + }, + "OAI/Computability/FourierTransform/SectorAlgorithm.lean": { + "sha256": "c0ceeb1214d4da1aff3c6b3c4ce6924c1f38f56aa35650d495eb8535d9aa17fe", + "upstream_path": "lean/OAI/Computability/FourierTransform/SectorAlgorithm.lean" + }, + "OAI/Computability/FourierTransform/SectorIdentities.lean": { + "sha256": "9fc0e09ffb02d3fecca284c5314166b95e8fcc211db74f05677573f3eb5acc70", + "upstream_path": "lean/OAI/Computability/FourierTransform/SectorIdentities.lean" + }, + "OAI/Computability/FourierTransform/SectorPacking.lean": { + "sha256": "70c173b66143bc135f6e06ce8d51349b9776f7355d22af39c29c4444c336e80f", + "upstream_path": "lean/OAI/Computability/FourierTransform/SectorPacking.lean" + }, + "OAI/Computability/FourierTransform/SectorPrograms.lean": { + "sha256": "2c099bf7765096db37b982bdac08de7182ce392d254f7f5aba27b66ec7759ab1", + "upstream_path": "lean/OAI/Computability/FourierTransform/SectorPrograms.lean" + }, + "OAI/Computability/FourierTransform/SynchronizedAlgorithm.lean": { + "sha256": "3ed66ac4c06c582b5e6164bda0ceeeab168df42baeddd77d87d711d89df6879e", + "upstream_path": "lean/OAI/Computability/FourierTransform/SynchronizedAlgorithm.lean" + }, + "OAI/Computability/FourierTransform/TensorAlgorithm.lean": { + "sha256": "125a9d16de9655256d1ec348f7e38ef85a226980016b8676341808f891db6a4e", + "upstream_path": "lean/OAI/Computability/FourierTransform/TensorAlgorithm.lean" + }, + "OAI/Computability/FourierTransform/TensorCertificate.lean": { + "sha256": "8e9ef6fb4ef34fde72d53ba4e52668e001452617022f7321a82fb736135e1fd5", + "upstream_path": "lean/OAI/Computability/FourierTransform/TensorCertificate.lean" + }, + "OAI/Computability/FourierTransform/TensorFibers.lean": { + "sha256": "aa8df1a11d4129c7e49ee45ed55414de755c292fbaaa0c28435614e4c7558a30", + "upstream_path": "lean/OAI/Computability/FourierTransform/TensorFibers.lean" + }, + "OAI/Computability/FourierTransform/TensorIndexing.lean": { + "sha256": "a53c88038609e0d28b5dbcc41589a9cb213987787a2efcd7af4a15a98715e94b", + "upstream_path": "lean/OAI/Computability/FourierTransform/TensorIndexing.lean" + }, + "OAI/Computability/FourierTransform/TensorProgram.lean": { + "sha256": "31ae3dc8977ea5e057f74c8a801f571775fe3ff6623dba1b713905b8efd16fcd", + "upstream_path": "lean/OAI/Computability/FourierTransform/TensorProgram.lean" + }, + "OAI/Computability/FourierTransform/TensorRecursion.lean": { + "sha256": "3e291113c770f622049158db8b5cce76483880661f3ab2369870263a4acdbc15", + "upstream_path": "lean/OAI/Computability/FourierTransform/TensorRecursion.lean" + }, + "OAI/Computability/FourierTransform/TensorSaving.lean": { + "sha256": "dd9080d7b64875b4669a6c61c4d5a870d8b00fc8b5efcfc54d7b8be519739882", + "upstream_path": "lean/OAI/Computability/FourierTransform/TensorSaving.lean" + }, + "OAI/Computability/FourierTransform/ToeplitzCompiler.lean": { + "sha256": "b3d2fd466d7a6a232d4ef9307f3e2793d77c6d2058fc301ee7767b8d74f5179f", + "upstream_path": "lean/OAI/Computability/FourierTransform/ToeplitzCompiler.lean" + }, + "OAI/Computability/FourierTransform/ToeplitzIdentities.lean": { + "sha256": "b991e9b8f7f4cb094c243808bc478408b4e94f8fafc45f5384026e94b63224cd", + "upstream_path": "lean/OAI/Computability/FourierTransform/ToeplitzIdentities.lean" + }, + "OAI/Computability/FourierTransform/ToeplitzLayers.lean": { + "sha256": "f9f825cc9bd646b49c4ce657f6bbe9c585bd8d1d80a5fb6d6cfe30e2b05f56e0", + "upstream_path": "lean/OAI/Computability/FourierTransform/ToeplitzLayers.lean" + }, + "OAI/Computability/FourierTransform/ToeplitzPreparation.lean": { + "sha256": "71c4da81502775d89bf82f0bd7bc6bccf1bd631d7bf1e6b4afd55c076a56a28c", + "upstream_path": "lean/OAI/Computability/FourierTransform/ToeplitzPreparation.lean" + }, + "OAI/Computability/FourierTransform/ToeplitzUpdates.lean": { + "sha256": "6d22d3ef4b38cda2d6c944a98a2983d232e3af49dc51f4eb963c0f44373a1830", + "upstream_path": "lean/OAI/Computability/FourierTransform/ToeplitzUpdates.lean" + }, + "OAI/Computability/FourierTransform/TransformProgram.lean": { + "sha256": "91a3339fb5b7ed3d1c1b9c46736d23dc94c6a0e88cb08b2c59135fa74a2d6218", + "upstream_path": "lean/OAI/Computability/FourierTransform/TransformProgram.lean" + }, + "OAI/Computability/FourierTransform/TraversalPrograms.lean": { + "sha256": "9bb540b0da2acff6b2308f52227a6b18a433751da2dfeab7645af0c8831292a3", + "upstream_path": "lean/OAI/Computability/FourierTransform/TraversalPrograms.lean" + }, + "OAI/Computability/FourierTransform/UniformBounds.lean": { + "sha256": "0d284f2ed7125a9446f8985ccef3d06ad3f819472c6ffaf3dc054c359011acbe", + "upstream_path": "lean/OAI/Computability/FourierTransform/UniformBounds.lean" + }, + "OAI/Computability/FourierTransform/WordCompilation.lean": { + "sha256": "d3e30c5465f46cdadb4965222620b926a05e06c8b99a407addcba41bdb2b5923", + "upstream_path": "lean/OAI/Computability/FourierTransform/WordCompilation.lean" + }, + "OAI/Computability/FourierTransform/WordPrograms.lean": { + "sha256": "af6005f9f3e6997228cc85c84ee0b408371608e00a58cc212e8faff9c117734c", + "upstream_path": "lean/OAI/Computability/FourierTransform/WordPrograms.lean" + }, + "OAI/Computability/FourierTransform/WorkBounds.lean": { + "sha256": "f664fde5fcfecfad564c3d42daa8011e3e5f10a745510b265d626e04a5470a97", + "upstream_path": "lean/OAI/Computability/FourierTransform/WorkBounds.lean" + }, + "OAI/Computability/FourierTransform/WorkingCompiler.lean": { + "sha256": "736acaeb5b664ae62e235271ba0316a6eaf9e351639a8b10fe010bf16a811e82", + "upstream_path": "lean/OAI/Computability/FourierTransform/WorkingCompiler.lean" + }, + "OAI/Computability/FourierTransform/WorkingPreparation.lean": { + "sha256": "43fe1a7d39fefc06a20809e3179e293229d61c752a079cff4bbc6772edae698a", + "upstream_path": "lean/OAI/Computability/FourierTransform/WorkingPreparation.lean" + }, + "OAI/Computability/FourierTransform/WorkingTransform.lean": { + "sha256": "cf9342af428783f0ff0eb72ccb497e1ea4b8e2cb4e5ecab3774c00d173a4b473", + "upstream_path": "lean/OAI/Computability/FourierTransform/WorkingTransform.lean" + }, + "lean-toolchain": { + "sha256": "d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b", + "upstream_path": "lean/lean-toolchain" + }, + "third-party/openai-math/lean/ComparatorChallenges/UniformFourier.lean": { + "sha256": "4c571f275bd7506c3ccd1e6d78f2fca77e07112c969c1c62ad8359d61544ec74", + "upstream_path": "lean/ComparatorChallenges/UniformFourier.lean" + } + }, + "repository": "https://github.com/openai/math", + "schema": 1, + "scope": "Byte equality with immutable raw OpenAI sources: 89 OAI modules, toolchain and original Fourier challenge.", + "success": true +} diff --git a/research/pr256-fourier-audit/evidence/five_stage_regeneration_receipt.json b/research/pr256-fourier-audit/evidence/five_stage_regeneration_receipt.json new file mode 100644 index 0000000000..4df30d58e2 --- /dev/null +++ b/research/pr256-fourier-audit/evidence/five_stage_regeneration_receipt.json @@ -0,0 +1,10 @@ +{ + "command": "OPENBLAS_NUM_THREADS=1 OMP_NUM_THREADS=1 uv run --python 3.11 --with numpy==2.3.5 --with scipy==1.17.0 python -B verification/vendor/five_stage/gcert-program-233/verify.py", + "exit_code": 0, + "log": "verification/receipts/five_stage/regenerate_program.log.gz", + "log_sha256": "6f4c1bf53aadf83eb42f6f1d5eb2cbf33defe2a3c93c9d463eb1c260dbcf9a26", + "reported_seconds": 188.6, + "schema": 1, + "source_commit": "db3f75cdc5f03f3131d48fb220f6bf1958404ff3", + "success": true +} diff --git a/research/pr256-fourier-audit/evidence/logs/axioms.log.gz b/research/pr256-fourier-audit/evidence/logs/axioms.log.gz new file mode 100644 index 0000000000..6b07507b65 Binary files /dev/null and b/research/pr256-fourier-audit/evidence/logs/axioms.log.gz differ diff --git a/research/pr256-fourier-audit/evidence/logs/build.log.gz b/research/pr256-fourier-audit/evidence/logs/build.log.gz new file mode 100644 index 0000000000..ec088a9d86 Binary files /dev/null and b/research/pr256-fourier-audit/evidence/logs/build.log.gz differ diff --git a/research/pr256-fourier-audit/evidence/logs/compare_fourier.log.gz b/research/pr256-fourier-audit/evidence/logs/compare_fourier.log.gz new file mode 100644 index 0000000000..8292a80761 Binary files /dev/null and b/research/pr256-fourier-audit/evidence/logs/compare_fourier.log.gz differ diff --git a/research/pr256-fourier-audit/evidence/logs/compare_wht.log.gz b/research/pr256-fourier-audit/evidence/logs/compare_wht.log.gz new file mode 100644 index 0000000000..21280ba719 Binary files /dev/null and b/research/pr256-fourier-audit/evidence/logs/compare_wht.log.gz differ diff --git a/research/pr256-fourier-audit/evidence/logs/regenerate_certificate.log.gz b/research/pr256-fourier-audit/evidence/logs/regenerate_certificate.log.gz new file mode 100644 index 0000000000..b9a514b949 Binary files /dev/null and b/research/pr256-fourier-audit/evidence/logs/regenerate_certificate.log.gz differ diff --git a/research/pr256-fourier-audit/evidence/logs/regenerate_fourier.log.gz b/research/pr256-fourier-audit/evidence/logs/regenerate_fourier.log.gz new file mode 100644 index 0000000000..6a095212fd Binary files /dev/null and b/research/pr256-fourier-audit/evidence/logs/regenerate_fourier.log.gz differ diff --git a/research/pr256-fourier-audit/evidence/logs/regenerate_program.log.gz b/research/pr256-fourier-audit/evidence/logs/regenerate_program.log.gz new file mode 100644 index 0000000000..489f0be489 Binary files /dev/null and b/research/pr256-fourier-audit/evidence/logs/regenerate_program.log.gz differ diff --git a/research/pr256-fourier-audit/evidence/logs/toolchain.log.gz b/research/pr256-fourier-audit/evidence/logs/toolchain.log.gz new file mode 100644 index 0000000000..ae6340df14 Binary files /dev/null and b/research/pr256-fourier-audit/evidence/logs/toolchain.log.gz differ diff --git a/research/pr256-fourier-audit/evidence/pr256_source_files.json b/research/pr256-fourier-audit/evidence/pr256_source_files.json new file mode 100644 index 0000000000..2de8fcf5a0 --- /dev/null +++ b/research/pr256-fourier-audit/evidence/pr256_source_files.json @@ -0,0 +1,22 @@ +{ + "NOTICE": "c1c95d22cfb0f455aca64b4bee4cab900829641b8f041280e7aa88034491c87d", + "PROOF.md": "c878c1a32e9a26bc3965b8843688d6e039094fb9c6b7fa1ea10579d727e70947", + "README.md": "00ab1525204b8130177658dfcb1acc201986c5ee06db27525ba80d57fb8edffe", + "SOURCE.json": "9ce463476af549c04de4705b1bf0c8f7f18d473dc0817883066ad5e2136d90b5", + "certificate/expected.json": "c0e3d245bf7e458ff86288eb47672491c9efee28181b570f1a3f17c8d915f766", + "certificates/gcert1-p11-pr194-flow.json.gz": "27c5b436af4b0683dd161e7f1253661427c45a1493c8dc90fcf0136fbba063ae", + "certificates/gcert1-p11-pr233-flow.json.gz": "09ceba1c0ea17282da155b937c8463669b913443c20f45fe2a7e6e024cb2d33a", + "gcert_emit.py": "10d2fc3f1f3d8cda5f0b07720f51b5a6fd40cfc1490d361939ff93e5470805d3", + "gx/gx.py": "6f3dc8bb639933227a8dae181ec4a542e85c7276be9c9e330f49518e7b630b95", + "references/pr233-layer/NOTICE": "5826b9f155b70d496d729cbaddeadb881abfb68da77f82dfc1746ddfc753313b", + "references/pr233-layer/SOURCE.json": "9ad0549ba2403e8d84d7c0c8e71e5ca952a0604ad626f403426164bd4bc2982c", + "references/pr233-layer/baseline-pr202.tar.gz": "5d08386f71c421d2b83b21020e3b74198e9d0c75884d7d81987307740d98883f", + "references/pr233-layer/certificate.json": "691cb0aaeb0d6b993e1e1e5116ae7a5c57af058a8c413249016347d1b40d3b90", + "references/pr233-layer/verify.py": "cd61a8c61462b4eee95c0858335a9a11bdf1ff8e8e63ebb1e488da29f061ca71", + "references/pr233-layer/witness/kernel-pairs.json": "e33b753fc4519170373207b0527b9cb53e0b552e2a27f48f72381a881c7a227f", + "references/pr233-layer/witness/physical-frames.json": "1a6c215cdc58216f7ec96fb898a471e25d094fd86de085f6c06e86fd8997bfad", + "references/pr233-layer/witness/physical-pairs.json": "e6409fffbf5f3b1ac6434acf2e426503de3a8a18537b8fee761fc4fc931fb896", + "references/sussman/pr193-blocks.json": "4049d066f71119fa72bbc37f7db753ce1e79ae5a69aef9cd2651d618bea5c855", + "scripts/moment.py": "0c7c68122cea18503e973ccf0d244adf8fa0edab95f104393528c6c57f24863a", + "verify.py": "7c4e140a41f9cb1e3bd7ca4eb06e5bb811f583250063ae53a48d39826796261f" +} diff --git a/research/pr256-fourier-audit/evidence/proof_source_files.json b/research/pr256-fourier-audit/evidence/proof_source_files.json new file mode 100644 index 0000000000..63431533b5 --- /dev/null +++ b/research/pr256-fourier-audit/evidence/proof_source_files.json @@ -0,0 +1,458 @@ +{ + ".gitignore": "dedab72bd6025e84a60573f485ac35fe4f2e619f1f5a905d4ed9cd5cd6b79d60", + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "MANIFEST.sha256": "1e8f9dd3b4d9924758e2acd49e10db2d0fdc9e93cb824c7fd1c77d8779d7c0c6", + "NOTICE": "9419dd03a2f52cf8bdfc4d18216ce29f263ab583b27f01ced8e420985bcb7c81", + "OAI/Computability/FourierCircuit/Core.lean": "45fd659a66b3bb93ea9e55ebf0c06fde26a3038e2c7fb369cbd8dada371603a6", + "OAI/Computability/FourierTransform/AddressTables.lean": "d833ec98fbf558c2fbea4e7acb608f69cd703eb98ed6257de879d4ff1ef8db0f", + "OAI/Computability/FourierTransform/ArbitraryLength.lean": "b7be3f6b003cc8beac973ab8aaf410dd6db84b44a7acad66eaac4f40b59cb876", + "OAI/Computability/FourierTransform/Asymptotics.lean": "a3037d47558d5db18b282fe48b0e0cb302f7efab37ce804caf9b6574c482b2a5", + "OAI/Computability/FourierTransform/BinaryBasis.lean": "ab9787433fd1feb0a90557334f0b7409fae080c2ee838adf1c6175a4e0314aa6", + "OAI/Computability/FourierTransform/BinaryFFT.lean": "fa2e7d5f65160fdf98c7208ba1b837aa14da1a306c824afa7065a731036671c8", + "OAI/Computability/FourierTransform/BinaryFrames.lean": "a1a613f0be5be321d16cdfdb6dfe65611cb06bf6693709a143cdf32b41d07245", + "OAI/Computability/FourierTransform/BitLayout.lean": "4cd9c100cd39881060cc4493f544ad85edfb8bfbfefbc1adc5140889c4eb356f", + "OAI/Computability/FourierTransform/ChineseRemainder.lean": "37d9615b194d34e2ea52cf6de5047bef7814a57608ad2d8959524f62f219e45b", + "OAI/Computability/FourierTransform/ChirpConvolution.lean": "8b8c951d60beef2fc0f8461ce798295bffcf24b426b457a6c22025516e1e4bbc", + "OAI/Computability/FourierTransform/ChunkCompiler.lean": "0ca0a87c35b29db93be5f8c5defa638f79d8fd320b0080fd5d911e9bb806b82d", + "OAI/Computability/FourierTransform/ChunkPrograms.lean": "c7d4dd887cd835c8edb9de82e5c28e9ac4298de6e58f581b3839fe9ba7c549cb", + "OAI/Computability/FourierTransform/CirculantUpdates.lean": "acee56a87a61938327ef89d6797f13c08e54ca5759c295c4dff2ddd4d5b75f8f", + "OAI/Computability/FourierTransform/ColumnAddresses.lean": "de7532b3e40c02b44b363e4c13989cbf41fbee0e2ae8d37f59a461084f98bfc3", + "OAI/Computability/FourierTransform/CompilerEnvironment.lean": "065071798eb7d6b6bb01420a9ef29eb07805ea134305899c7fe9bb1f9a8663e6", + "OAI/Computability/FourierTransform/ConvolutionProgram.lean": "a5792081ddb71d2f4813052d65e722b82accbf4ece96d6c69ad3406000c0558c", + "OAI/Computability/FourierTransform/Cost.lean": "574eb175d87bcddc323efb4b2227975afd28a52079d3657c058ba9568e539801", + "OAI/Computability/FourierTransform/DirectionalWords.lean": "eb9689b4f4e1e6631bb53208afd92b2f2dd612d5ddd85fa8bb40f8596f81d64d", + "OAI/Computability/FourierTransform/DisjointIntervals.lean": "a641f52e1d1e35e462664c783b748942b12bc64b7747eb9c4deeb477a0ba3c9c", + "OAI/Computability/FourierTransform/FourierCompilation.lean": "f03c9b92c3be39fde0cbd4040bcff850bbd20c436d0cd16f7530073ab9c76fba", + "OAI/Computability/FourierTransform/FourierIdentities.lean": "8a4f93c3f087ddaa55a8463fbe8c150e61f6ac8e41ed8c9c61add0670fe1cad7", + "OAI/Computability/FourierTransform/FourierWords.lean": "8a9e4ba63c2668b7133db1460a13507479598e57fd50243c59e3ac365730d2f0", + "OAI/Computability/FourierTransform/FrameLifting.lean": "31543b1edc69e19597af8b0035e43c8183c8e9640ed99ee5b8a6b87f77ae0c7b", + "OAI/Computability/FourierTransform/Goal.lean": "879a7d19393b7f162e1711fba08e10626444b9e34b5183ead3b7832ba462c344", + "OAI/Computability/FourierTransform/IntegerPrograms.lean": "028080a8b977f88300fdb536af94214eb72b117af026518e1c08b84ac50dbb84", + "OAI/Computability/FourierTransform/IntervalEffects.lean": "a34be872372439cbcfa4a063e360c12ff5b35b5d7fa925a10e49fa20d268fc1c", + "OAI/Computability/FourierTransform/IntervalPrograms.lean": "ecdbfed1b40da9d117170892a0adc207d381f6d2b702868fdb8bc7a0b58e2cc6", + "OAI/Computability/FourierTransform/LayerCompilation.lean": "23e287c7c7ff066cf662d496d8c8108a80662229354de84abb59fd4da785c927", + "OAI/Computability/FourierTransform/LayerPrograms.lean": "035f13e90785557988a35074ba30babefda81dda352067d5c7b636f3fb82005d", + "OAI/Computability/FourierTransform/LayerWords.lean": "4e42fe8d2807ba5dd10adb7cc64e3c9c95bb1c2f9d5171e91efd37c24f44b01b", + "OAI/Computability/FourierTransform/Layout.lean": "133ccff630aeb568807bddf3791bf2f9a6fe8f46672ea3dc0f84a3f9df3e9743", + "OAI/Computability/FourierTransform/LayoutPrograms.lean": "681d453c33d254b3cec43913ce388fd435f340f7639338f8e67d3d3d28c7cbbd", + "OAI/Computability/FourierTransform/LengthSelection.lean": "41aa79c7d836733adfecf597f07ab1b020762edd629b2dca49a26f8b03b3b2c2", + "OAI/Computability/FourierTransform/LocalCompiler.lean": "ef7ec7017261090b0a798fc6082cda77981fd34d0ff18a5ccfd1f2a1d20a0a50", + "OAI/Computability/FourierTransform/LocalPreparation.lean": "a55545e2a129689bc574a075fccd2ef63c67654011566fc65b0085d453363efc", + "OAI/Computability/FourierTransform/LoopBounds.lean": "8799c6b2539f7b831288b1454a44c8b03912d17f75077362a17983dcd366b351", + "OAI/Computability/FourierTransform/Main.lean": "0b2b9f758ff41d4b13b6420451d04fbbd84826a8a2594eb8d5b2311a3861ef55", + "OAI/Computability/FourierTransform/MeasuredFit.lean": "da9cafbf4d857f759880d9198969cabd8ed31676fb29fa0d22dce2b8dca9c1c2", + "OAI/Computability/FourierTransform/MeasuredPrograms.lean": "03e03bbefec631cec7dec22ee199f97760a3f6d6b4b4f58a76be180a3f767628", + "OAI/Computability/FourierTransform/NetworkInvocation.lean": "1f3a4c4b9f30548c76a2c999c239f8ed9f5480b9a14671deba01ed37b092abb7", + "OAI/Computability/FourierTransform/NetworkLabels.lean": "3c4057cfea65c2305fb2a323feac7ecd49fbd831d84961da6130665e6db09851", + "OAI/Computability/FourierTransform/NetworkRoles.lean": "00c826532d66eece5e7c6b8714a7402d7936f07f7d8a2b8d0fcf8639e0fa2289", + "OAI/Computability/FourierTransform/NetworkStages.lean": "60582947d315fd090f0a5a019b636602c4bb176146843e1c4690ad166c8e16a6", + "OAI/Computability/FourierTransform/NewtonFactorization.lean": "264bf2818b36435275fd79281361c5e7d80ba5a7cd7e0e4e6a36a8aae744a15d", + "OAI/Computability/FourierTransform/PackingPrograms.lean": "4310c0f0bc1c142bb089c2a3d59ed5392f15d25df6fc9c2bca2d4c7674f5c52f", + "OAI/Computability/FourierTransform/ParameterPrograms.lean": "acc759c49833108366684ff9c35f8343c4a3d8976a3d7244be2e40d57c95c686", + "OAI/Computability/FourierTransform/PolynomialBounds.lean": "904c9e90fd009e0a56a1b35eb4ed54068653e6487a82850ccc1510cb18cf6ab1", + "OAI/Computability/FourierTransform/PolynomialPrograms.lean": "6dcb0251326a8988b5101ddabbd7b0ff582e0f39646fddc83adae0a07b8a92af", + "OAI/Computability/FourierTransform/PowerTables.lean": "372818fd8c12356a5d959286271be0973abab6ecf9521ce1d6b49f922f423d0e", + "OAI/Computability/FourierTransform/PrefixTraversal.lean": "eb84ca868ca680a66ce14b9a1d27258b733c5dd240f69411ec8b06c9cc84f7d5", + "OAI/Computability/FourierTransform/PrimeSelection.lean": "c94d8aef61f51b0d658faa64e7323510cf3fa9cb88d6db25542af7287b8c1b76", + "OAI/Computability/FourierTransform/ProductMatrix.lean": "7508fa85fc588567237dc8133e17a26d1883253df72f5e2f1459a16f33434a2e", + "OAI/Computability/FourierTransform/ProgramBounds.lean": "904132230871e8693bafb126ee0fa6147140f83516add46b6e130bb4bdc0334a", + "OAI/Computability/FourierTransform/ProgramConstruction.lean": "b3294e211d08f170e4ca86cd6e4a8be27adae7b538da1d22d7ee03b8f007b4d0", + "OAI/Computability/FourierTransform/RAM.lean": "4eb8a7cbd1566b9a0537c3423e32528c3d6be691a4780bd549768a96e568fa8d", + "OAI/Computability/FourierTransform/RecursionBounds.lean": "eeb1d9752680fdf0c4206ca8fc1369601a45715c7f3d5c91bb9c2d378d212f38", + "OAI/Computability/FourierTransform/RecursiveBatches.lean": "8afd2aed3ad05a145b8ddbca76cdbad6c3fc249c805bc972825b6396248eae97", + "OAI/Computability/FourierTransform/RecursiveContract.lean": "b0e7deaf0efee6d10ef18efafa4cd5ff3e8513d7c507a23aa16ed39a089c2737", + "OAI/Computability/FourierTransform/RegisterBounds.lean": "5e1a314a8cbdc73cf5247c294f4906fdb205dac34c0be1a22d0bd3e51603c353", + "OAI/Computability/FourierTransform/RoleArrays.lean": "929f8de89d880c898872fb031326ac316f783e61b85ac589f95c5a064f10e6f0", + "OAI/Computability/FourierTransform/RootPreparation.lean": "d51bbe713d36fe5dbb2549f2a95d138f346087d68593de446c9ce07f2cc534d9", + "OAI/Computability/FourierTransform/ScalarNetwork.lean": "121a5d597f7ae266206d6e113104c98765f30f3ff28f72ccdef64c025c3d0eb5", + "OAI/Computability/FourierTransform/ScalarPreparation.lean": "1c61342491f4871f8e921c359e74b64c38f3b7c3eccf99ab9b16a399aa635a8e", + "OAI/Computability/FourierTransform/SectorAlgorithm.lean": "c0ceeb1214d4da1aff3c6b3c4ce6924c1f38f56aa35650d495eb8535d9aa17fe", + "OAI/Computability/FourierTransform/SectorIdentities.lean": "9fc0e09ffb02d3fecca284c5314166b95e8fcc211db74f05677573f3eb5acc70", + "OAI/Computability/FourierTransform/SectorPacking.lean": "70c173b66143bc135f6e06ce8d51349b9776f7355d22af39c29c4444c336e80f", + "OAI/Computability/FourierTransform/SectorPrograms.lean": "2c099bf7765096db37b982bdac08de7182ce392d254f7f5aba27b66ec7759ab1", + "OAI/Computability/FourierTransform/SynchronizedAlgorithm.lean": "3ed66ac4c06c582b5e6164bda0ceeeab168df42baeddd77d87d711d89df6879e", + "OAI/Computability/FourierTransform/TensorAlgorithm.lean": "125a9d16de9655256d1ec348f7e38ef85a226980016b8676341808f891db6a4e", + "OAI/Computability/FourierTransform/TensorCertificate.lean": "8e9ef6fb4ef34fde72d53ba4e52668e001452617022f7321a82fb736135e1fd5", + "OAI/Computability/FourierTransform/TensorFibers.lean": "aa8df1a11d4129c7e49ee45ed55414de755c292fbaaa0c28435614e4c7558a30", + "OAI/Computability/FourierTransform/TensorIndexing.lean": "a53c88038609e0d28b5dbcc41589a9cb213987787a2efcd7af4a15a98715e94b", + "OAI/Computability/FourierTransform/TensorProgram.lean": "31ae3dc8977ea5e057f74c8a801f571775fe3ff6623dba1b713905b8efd16fcd", + "OAI/Computability/FourierTransform/TensorRecursion.lean": "3e291113c770f622049158db8b5cce76483880661f3ab2369870263a4acdbc15", + "OAI/Computability/FourierTransform/TensorSaving.lean": "dd9080d7b64875b4669a6c61c4d5a870d8b00fc8b5efcfc54d7b8be519739882", + "OAI/Computability/FourierTransform/ToeplitzCompiler.lean": "b3d2fd466d7a6a232d4ef9307f3e2793d77c6d2058fc301ee7767b8d74f5179f", + "OAI/Computability/FourierTransform/ToeplitzIdentities.lean": "b991e9b8f7f4cb094c243808bc478408b4e94f8fafc45f5384026e94b63224cd", + "OAI/Computability/FourierTransform/ToeplitzLayers.lean": "f9f825cc9bd646b49c4ce657f6bbe9c585bd8d1d80a5fb6d6cfe30e2b05f56e0", + "OAI/Computability/FourierTransform/ToeplitzPreparation.lean": "71c4da81502775d89bf82f0bd7bc6bccf1bd631d7bf1e6b4afd55c076a56a28c", + "OAI/Computability/FourierTransform/ToeplitzUpdates.lean": "6d22d3ef4b38cda2d6c944a98a2983d232e3af49dc51f4eb963c0f44373a1830", + "OAI/Computability/FourierTransform/TransformProgram.lean": "91a3339fb5b7ed3d1c1b9c46736d23dc94c6a0e88cb08b2c59135fa74a2d6218", + "OAI/Computability/FourierTransform/TraversalPrograms.lean": "9bb540b0da2acff6b2308f52227a6b18a433751da2dfeab7645af0c8831292a3", + "OAI/Computability/FourierTransform/UniformBounds.lean": "0d284f2ed7125a9446f8985ccef3d06ad3f819472c6ffaf3dc054c359011acbe", + "OAI/Computability/FourierTransform/WordCompilation.lean": "d3e30c5465f46cdadb4965222620b926a05e06c8b99a407addcba41bdb2b5923", + "OAI/Computability/FourierTransform/WordPrograms.lean": "af6005f9f3e6997228cc85c84ee0b408371608e00a58cc212e8faff9c117734c", + "OAI/Computability/FourierTransform/WorkBounds.lean": "f664fde5fcfecfad564c3d42daa8011e3e5f10a745510b265d626e04a5470a97", + "OAI/Computability/FourierTransform/WorkingCompiler.lean": "736acaeb5b664ae62e235271ba0316a6eaf9e351639a8b10fe010bf16a811e82", + "OAI/Computability/FourierTransform/WorkingPreparation.lean": "43fe1a7d39fefc06a20809e3179e293229d61c752a079cff4bbc6772edae698a", + "OAI/Computability/FourierTransform/WorkingTransform.lean": "cf9342af428783f0ff0eb72ccb497e1ea4b8e2cb4e5ecab3774c00d173a4b473", + "ORIGIN.md": "e8281da1d8188f16c5b2faf34987d77abb0f18c1d164a6f950c6fac3d81c1570", + "README.md": "c3e9b61308eaf9d23f5107bb9d7a13c14a7b947d228022a585a2f8573856f601", + "RELATED-WORK.md": "166a4f4dd6dabb1f6259a249163bc44968a091f04be66c4965ed105fa7b6088c", + "VERIFY.md": "3fd0a022bd6488f348bf2c2be44ebc7236f7e10df58a55cc9d214293e7881e55", + "WHTCheck/Solution.lean": "ce638be547cac9eabc1eb6285b1a5b32b06024ef088c331dc2f585fdb7cdf006", + "Work/Block/Address.lean": "c49dfe44a9f096c2173f17b46c38d4f1d335a0c5a36b45093e6a86755919860b", + "Work/Block/Batches.lean": "95b246e3b7be76957c7f4bf121309c370068a4ce43ffe11f2b8736334be6334e", + "Work/Block/Bridge.lean": "2a8c55b81ca03c2ab2e7704a67fcf306fb3f9a5466b157742d01669aaddc4492", + "Work/Block/Engine.lean": "6722ca54c2736e1ac09abd98183db7784bdf45fcb921a8396053565b0076bf7d", + "Work/Block/Extras.lean": "dd9efe63c99c4116fce301641b87e8886611cbe78dfc971bd93e784fe1ab9842", + "Work/Block/Frames.lean": "6f984c2bb0c9d384891cdbe538e811690bd3e6e97e8f319af47962b1dbd13ad5", + "Work/Block/Majorant.lean": "0af4533c251c2e3488106edbcf936b7372577210e0b496e65c73a76cfd7c6578", + "Work/Block/Paths.lean": "6343c769fa59bf716de2cc52bdc8b583042996dee1dc7fd55e5a27cd0915f157", + "Work/Block/Peel.lean": "76b0f7b28a30abe020846695881662e4857927def7f5ab2c974ee467f34afd3e", + "Work/Block/Port.lean": "9d357b36ed86b2fb2789583d5c113f74d520e6fb6b96c07c2c54c3e9124c309c", + "Work/Block/Recursion.lean": "30566cef90f6304c7229482b98465dbd745a792c2bc284b8559e3d85533eec9b", + "Work/Block/Split.lean": "b868f1a79e1c5a2a958fa85ec976d1ecdfdd80644bfd95c50369c8e17059e193", + "Work/Block/WHT.lean": "e00c1415767b05fd33c0ce9f778f60e96cae61de2bb21b187ec26dc8ff84ee72", + "Work/Block/Word.lean": "7bf08ae84f79761bda635ffc207ef460058cbbe7eb675c7d7cd1af05f600473d", + "Work/BlockAccounting/Moment.lean": "248b3b5705d0ed5c629622119a59ae763f5e1559bd612ac834d1608886c98c99", + "Work/BlockAccounting/Sharp.lean": "07c0cde93babdf789a44fbee1931c3b7128663a9f9371e23da1fda07be07a7cb", + "Work/BlockAccounting/Steps.lean": "b11328b9b43b415fedef5b33c2cba00e489d9de5888873fd5afefa32315399f7", + "Work/BlockApply/Copies.lean": "09de1cba9f2ec2f06ff71c2d4b1f43ba0f71b4d8c8393be137a5d96ff2d97568", + "Work/BlockApply/Exact.lean": "3fa669792878994b1c52c868fae2e28183633f22d300f115c5b57977724af901", + "Work/Bridge/Cert.lean": "5c24746a6330907b9b37d6064095035a58575d64ce793d6d7c9881121fdc3980", + "Work/Bridge/Inv.lean": "f19355fac93ad292296cfd9318d5ffe546ff01f4cadc65b5fba18b00dbf357be", + "Work/Bridge/Net.lean": "cf7d7d330b1bffe2e66712c873e647b13dc32db1ccfc0e0f4cd62ee6caf584f0", + "Work/Bridge/Roles.lean": "3b19269451a10dbfb29e6e081cd492070addf2138d16e69d068a3c7b35a55ca7", + "Work/BridgeGeom/B2.lean": "ea4f37c283b6070577f5b4f644fdc2232ae1114f480b85cd765209dfc863de8d", + "Work/BridgeGeom/Blocks.lean": "3f324b839329080da5c14576427f36428fd1bbd883b1c5d1572551f899f8e84a", + "Work/BridgeGeom/Net.lean": "10aabba2049c837f51c73874cf9cc8bb6afd6f02d6f47ca9de6bb866a4346a67", + "Work/BridgeGeom/Stage.lean": "f3f831c2f36612f54e53f4d60ae2d8f3b44ca7fc83b5445621b3d9839e688941", + "Work/Carrier/Glue.lean": "b409adf582b99e3dcf81ffae1436bc355377355c4131ac298bfdc5e50d481065", + "Work/Carrier/Live.lean": "6d0649eb62589e66057f044e1e2103fc42f3f57a1498f82a26565bd8eb4026d0", + "Work/Carrier/Pack.lean": "7850a957eae315bab3b75a0f2913b03138d3f68e2dcb0aa3242fb222028dee68", + "Work/Carrier/PhasedInv.lean": "d468d6abb733bb5dcabebed73138391be6af7a0aaa7abce0b4f3d3b46e7adca0", + "Work/Carrier/Phases.lean": "71dc3dda23dfe510d5d53cbada3a6c540cd1dc2825503fda618a5bd6cfc3e812", + "Work/Carrier/Ring.lean": "e7e48e9d946a289f0c59dc9a6c8c8e70804951438d111bffdf3297f715af2b15", + "Work/Carrier/Scat.lean": "2ed9811a3b027dcd49517fda99690a070925c6b587b1f45a9ba245c35d133d38", + "Work/Carrier/Sched.lean": "6e7b124deafa91a97d05f095f8644ab35f1650481d9294b718a71058f62c37f3", + "Work/CarrierCheck/B2.lean": "4cdcd3d4940a47aaa5d959ca37f28ddce3b3f40592b754c12a5724ea1c0b3dec", + "Work/CarrierCheck/B2Ke16.lean": "aed0e2b7176234fbea334856b38938f802723db027b93a2764bc18564bdf7bb3", + "Work/CarrierCheck/CCert.lean": "d4f09cee42b04ec4661276c838eacb80015b177111697961ecaffdf2cf574f4b", + "Work/CarrierCheck/ChallengeB2Ke16x.lean": "953578aee4aaf2c8a4b30692406df292445441d3d9ea0a02c5bdc76ee6a15e08", + "Work/CarrierCheck/ChallengeB2Ke16xR.lean": "61d8edf661a316208ae939b42e688a95c237d2a344758069b58f128233fef1d7", + "Work/CarrierCheck/Cr2h16Cert.lean": "49128f7ac960163170c73658f662975bcb7412631c4b58b54d3900b2d216f513", + "Work/CarrierCheck/Gen/Cr2h16.lean": "fae04c990a5a5b915e79e8a012e80536c98ba2d5f5f57a2dd3ba1213577cba70", + "Work/CarrierCheck/Gen/Cr2h16Hist.lean": "4649aa4d566e853ad9fae260801c5724a1a9e16a952fcd69046b27e1451828b8", + "Work/CarrierCheck/Gen/Cr2h16Lab.lean": "fa30579d37d9f2c0f65e58db679eaa65eeedeb11805b5d76ed06c6a3170f2f11", + "Work/CarrierCheck/Gen/Cr2h16Scal.lean": "5796f2f787acd11c89164cf998c6a3ea75cfbcea5eb074cfe946b515fd449ff9", + "Work/CarrierCheck/Gen/Cr2h16Shape.lean": "9564c3b972a1936f9612f30e385deafc52ab892581be5c024cbb02b8f28de3c3", + "Work/CarrierCheck/Hid.lean": "5f813d7024a128e3038b24b28a3396eec9dc9bdf6ac2ebfe292b9257fd98960a", + "Work/CarrierCheck/Inst.lean": "a2fa129a3f2653d8424216d240f6febfc2816e5cdc15aeabdb537da913c619b6", + "Work/CarrierCheck/InstB2Ke16.lean": "2878018696f23639246f63534d44b463af7d1d180928426fbf21e39a89d70406", + "Work/CarrierCheck/Inv.lean": "1edf6cb1a3c69df10e09a525299bdedcdbe12855f679eaceef1a58434d5f7ecb", + "Work/CarrierCheck/Mat.lean": "600b769fafdc83e1c81116dd81be5b213c34b1f3d6a35fc9cec98a62720d1054", + "Work/CarrierCheck/RateB2Ke16.lean": "403a9bd6373c213c86783adc6c47c401f27630897a35fd0a9d9013ed9ef06196", + "Work/CarrierCheck/RateB2Ke16x.lean": "e509cf7439982f2fe241def2f2c2b5178d7aa6ca05a70c40d130636740664305", + "Work/CarrierCheck/Roles.lean": "1ec2135f3628f9ac19cd6c040b5f672c8ab0d242af335acd2f6a7976565f3c1f", + "Work/CarrierCheck/Routes.lean": "9d0b994693a4a950d07335de8f3eadef2bc0e4838b4b9a9ef8cb1faa079b8cc8", + "Work/CarrierCheck/ScalDef.lean": "73e8b7285a23a01302d085e68cef3d27f55654cd78dcd99365d9cef959ea7673", + "Work/CarrierCheck/ScalFin.lean": "5587b03fade33143b17df2860265f9d491e72bab31c2bb58cc2e860b94c7dad4", + "Work/CarrierCheck/ScalId.lean": "930162e0290cc72db9d98e0afad6de099e581176432d5077279aa6582175ecad", + "Work/CarrierCheck/ScalOps.lean": "bce7443d552fc90808efa64f31a8c6f879cd839df652104b06597cf3cdce3245", + "Work/CarrierCheck/ScalRun.lean": "1e33587e7fcffe24955311ae6659fd5273e3adf6f4aef8ef43ca268b58a52ba1", + "Work/CarrierCheck/ScalSound.lean": "592a7e1ea58ab92b7106171be55d1ec423ff99983ea03ce902c869608d20de71", + "Work/CarrierCheck/Scat.lean": "f491e7017b13ada43cdc773b1968e9b40e6e5d22c42aa6420cdd20a5b5a77b15", + "Work/CarrierCheck/SolutionB2Ke16x.lean": "9bc32194807e9f33b370ddc34f94139b31d779395273720bd983a754407ae4de", + "Work/CarrierCheck/SolutionB2Ke16xR.lean": "d444c2074938465e9cf1e528266e38fa4a9b11c52ad64d61631f83cfa376e1e0", + "Work/CarrierCheck/Valid.lean": "6b3635beb4fd74809fca89b04a75054e131b280697833ebed4cffe389632efe2", + "Work/Combine/Chunks.lean": "fc006c1cba37579fe1b0a552a3e0504038b26ed73550503a9a681dc653247977", + "Work/Combine/Hist.lean": "c907c77eac4a3800b4364cc3eedf10e8b34270b6d520ea9b1bbfcc1d0c8b02ac", + "Work/Combine/Ranks.lean": "231d034010b6b5fbac57a6357a2da24def1619cd586797434b8e1a6a215cd93c", + "Work/Combine/Split.lean": "7997fd92374e83f6422dc9debad5b12ec8352e337aa931002c532f3d7d253865", + "Work/Combine/SplitDef.lean": "7d1ad7d57b869b85225fc2f2388be22bb5415c8485049fcfaf92f658f54d82c2", + "Work/Combine/XCirc.lean": "25e38bdce2b1a8b9c03365372e03626ce773dcd009bcf7f1cd01698f4cce7076", + "Work/Combine/XG.lean": "54f62d8173a4e8c306300322b101d9c897ed121cc81ef282fddf0e1bc7594f2f", + "Work/Combine/XInvocation.lean": "dc0da77191875d29cbbd094561fd0844b0b8e414fa755b35176d6ea67859be32", + "Work/Combine/XNetwork.lean": "d44d6275c2ab56d4c06649c05cfa9527ea19874b5d6fe80968bb4c883a93b9e2", + "Work/FoldRate/Arith.lean": "e755364b9d806fa6a4a968c23af1f352d755d7d6be626f99da7962749cd0614f", + "Work/FoldRate/Group.lean": "0e58152681a73a1b1f391de2e6c7264c865a865242736ccbfab99f672cccd4f0", + "Work/FoldRate/RankTools.lean": "1252b2394c952d91e4132ce953d9fca9ce43f4c0d8034f146cca31b90901205d", + "Work/FoldRate/SharpTools.lean": "d0f02c454bb7ca2c8acda96c03d8f876b58cdb0d9574a427b480e093fbb57ecc", + "Work/Fourier/ArbitraryLength.lean": "b7a10aae38da2f0450e362871358fc4fd8b5d59acb46d7b1dffb674d07f6cfb0", + "Work/Fourier/Asymptotics.lean": "7c0e52f6038c29d51ea5a6e747cf88f9db9698b2ecd10d2270c4b0c68302e383", + "Work/Fourier/Axioms.lean": "d37c1f6dae1a8fcf74838870daefcb0123ccf0d7373f44d5412153e287c67c0c", + "Work/Fourier/ConvolutionProgram.lean": "89c0241859c40f8e7ca273c940c34a5364c6c16b1811b23ba14791a27805c9e3", + "Work/Fourier/Goal.lean": "e5c9cb6c61b5d11027d1b4271d693ba45fcf653d154ae790bd4e06e52b6c638c", + "Work/Fourier/Main.lean": "2e8e88efd4dcbdf0b1a6e39ce7eea8c5fd5ffee2faf360a8c0c9cba84c0e4ef3", + "Work/Fourier/Seam.lean": "877511b92663a65662b9f4f58eb3326420bc8e9a300c564051816e336f260f67", + "Work/Fourier/SectorAlgorithm.lean": "79376a18012d493cce3dcdadb6047926985f3aaa2150477acea554f632984957", + "Work/Fourier/SynchronizedAlgorithm.lean": "336c0ad615e5f118ace588ca93d8665c72aa1a1d525274b9f21873ef32dd6541", + "Work/Fourier/TransformProgram.lean": "2ad10882d8f52a9972fb3da23b9dc55514a0c4fa3cecd783e8c59e23c6d34def", + "Work/Fourier/UniformBounds.lean": "28266f5046d537be06cf2de0c4664b91b0d0ab28392561b6011da239aaef6cda", + "Work/Fourier/UniformFourierChallenge.lean": "9592163f84a4c049280b9aaf67c129e09e017d785c88504661320bb8690f0d1a", + "Work/Fourier/WorkingCompiler.lean": "b6529e0c2f30858de41704e3bd12261b540df5785520d28175bd5c9eb68801b8", + "Work/Fourier/WorkingPreparation.lean": "3023bc672d532b493a1e6f652f052f81cd58eafc2b58210e2da16f0b4a769caf", + "Work/Fourier/WorkingTransform.lean": "cd516e41770cdd2c7fe336c130716b70291aa9b608988d2a213d9916b381c1ea", + "Work/Fourier233/ArbitraryLength.lean": "04f7b5ad1f832661139db20926ea212e4a6b3cf62c3493507c3381c397042071", + "Work/Fourier233/Asymptotics.lean": "4e46226649e4236c8dc190249a70071f7d63ed777a2a4f053e4c38bab64ec050", + "Work/Fourier233/Axioms.lean": "5445f37205ee26e4c0cea6295cea4ee822a0d6641ebdb890c95a4ebe67ad4f4b", + "Work/Fourier233/ConvolutionProgram.lean": "49832892ee132448b64fa599dad2981bf9fbab3372b7d9df92d915d2955b1ce7", + "Work/Fourier233/Goal.lean": "a03b206bd60de3d9e09e6493bff5e06ed89e343d76fc5f5ea56f0ab55469f055", + "Work/Fourier233/Main.lean": "34e239ff7322aacd9fef027d160552c5533fc091bdb5d4b781def32479cd66d5", + "Work/Fourier233/Seam.lean": "7b571b9fcb5758047f30d6ab79a76f8c77bbb1c4c75fbbb6579c6704b737549f", + "Work/Fourier233/SectorAlgorithm.lean": "d0d687d5c7f375bcc9dfa267ae1878a64753b5f2e0819a2cd41f3428a3f62f09", + "Work/Fourier233/SynchronizedAlgorithm.lean": "291dd1256ef522d9977f926c6cb544db1a17d8671ac4773332a9c9d91357f12d", + "Work/Fourier233/TransformProgram.lean": "00b16a6d277b3846fd373896484f394d6992a23a79ea089fc21553a9abb5637a", + "Work/Fourier233/UniformBounds.lean": "9d3912fadf66048ce694bf463c12eb98bc795d360afef59e9216b5c4cd225625", + "Work/Fourier233/UniformFourierChallenge.lean": "56b22d76e31df9da0a119e4a04c3d1ba74c8db11740d63b5fcdcdcdbe13bb8fc", + "Work/Fourier233/WorkingCompiler.lean": "e8908662278deeee6c4e4d2b1efb5cda5667881cf44c724b729fd44cbdb0db9e", + "Work/Fourier233/WorkingPreparation.lean": "bbd3263db03d4667b6bff49363c9ae2db81ac59d84547539f0d74cfca703b57e", + "Work/Fourier233/WorkingTransform.lean": "efe058711464305bbf8858ce9337adb514baa55f67adddaee97d3302f5d8e48b", + "Work/GCert/Chain/End.lean": "0fc15a884ff0621edc0fff2cfcd598071be2e9fa57060c0bc453672927e6fb55", + "Work/GCert/Chain/Geom.lean": "c302f5834287421f11f3b0da7112fcde876cbc702896f2af4145b2d72ee393a2", + "Work/GCert/Chain/Inv.lean": "6b4fceb158117a6476366b0360e7f0a00f736fab888c974ecb8b1aabd461c431", + "Work/GCert/Chain/InvThm.lean": "ade7e7873da75ca63a4b5ce2f562dde9c12bfbb69d87d7ae831039ff790e5adb", + "Work/GCert/Chain/NetCert.lean": "22ae34809466b4ac2a2c5cdde526f51ff246f5189f7c142b38aa4c0dcffb04a4", + "Work/GCert/Chain/NetDef.lean": "6e17a68b1e988969f6eb77000028f7ed877e687b8ad3976ec1707fcfe1d2f520", + "Work/GCert/Chain/NetStage.lean": "c122bc01392a6fdcc0bee918fed81804d3c9b1d3e071016dab65a4ed804ef0b6", + "Work/GCert/Chain/Phased.lean": "0de429c80231334f1ce92575c1e8ac382ca2d5e7d956767b547639a8941d9a8c", + "Work/GCert/Chain/Stage.lean": "b80e46b56b75bcb09944e964284f090676f5d644c73da5dc6ac3fcaf99f36db4", + "Work/GCert/Chain/Win.lean": "d63d4a0008141abf2d135617a33e7b10de5aaf0443768341b81ce0761ad92620", + "Work/GCert/Chain/WinB.lean": "c33ec3fce09c0971c32ddcbb86d9383ffbe4c6d05cf36f20460005e6547bb845", + "Work/GCert/Data/B2Gp193.lean": "f65d66e81418753b3b3e184edb8cc4a743a77ae29383e80aaf4bbcdc57da1040", + "Work/GCert/Data/B2Gp193Main.lean": "cb61f304da51f1dd0a2ec25bca4b63eb095eeb2863289e1e2bdee7c82beff48b", + "Work/GCert/Data/B2Gp233.lean": "ec25fbb444efaa9ba4d3a1a5b455705bc13bc7d248309668dd6990fc7f142abf", + "Work/GCert/Data/B2Gp233Main.lean": "689e4881d8e38ff0ab2f6ad702cd60f1b725fc946f9f649a5fabb9a8cdb2da63", + "Work/GCert/Data/ChallengeB2Gp193x.lean": "4566a6595cb3e940b79976a4315a7a7b105c85fea5b667c42712ff03ddb842f4", + "Work/GCert/Data/ChallengeB2Gp233.lean": "f01c1bd10e4de0c7a4d144e25478125df59697112df773dcb26e03d1f493450e", + "Work/GCert/Data/ChallengeB2Gp233x.lean": "14a2596f55510a8b51e04e026a8b1125880d6930bba906cbc85e96eed321fd46", + "Work/GCert/Data/Count.lean": "d8a0928c538fbb28f3b746fe5499d7aca33c9dc1eb9e7f434a959211ec718154", + "Work/GCert/Data/Gen/P193.lean": "2d602004230fda1cc6662db6f5d4463c4b5d956dde859a7530406ddd3723be26", + "Work/GCert/Data/Gen/P193/S0.lean": "bf102c5e0384eb2bb2641e369166fdae13236dd1d9bc8b4207239da2f4f725ef", + "Work/GCert/Data/Gen/P193/S1.lean": "663836a6cf1f97c03692306d1bd321da5a4b637f06b25a30af14c22fabb2cc86", + "Work/GCert/Data/Gen/P193/S2.lean": "d6e9e914789b16ef4c412497fa8be009d0935b352e3702c911d0ecbed5c1e4a3", + "Work/GCert/Data/Gen/P193/S3.lean": "f558c24326df4cf8c7caadb93b35b5071601dc4be17d61ab1e3eeb8e97fa080e", + "Work/GCert/Data/Gen/P193/S4.lean": "2469dd18d5587d7e476a4c69ac79904523eef9a22b57c3b2b4b6f1d531c8ab22", + "Work/GCert/Data/Gen/P193/S5.lean": "823a58ff2382eaa7f18e722d277bd25408f24d7f82b44c9f60b3455c81b388c9", + "Work/GCert/Data/Gen/P193/S6.lean": "f6507ad8e884040230ea440df800b21f16de17f6672073ab33d77e5e1a1c115b", + "Work/GCert/Data/Gen/P193/S7.lean": "b0e14df382b5d3f1f3bc4fca1e0769277c7660f4834f0aaf0067134281a7acf4", + "Work/GCert/Data/Gen/P193End.lean": "1ea2eaa0f3d2f207f63a1a01267ee4c92dfb441495a21b2466332dffdb4d2b70", + "Work/GCert/Data/Gen/P193Hist.lean": "8e7128a9f7e7f7c7efea8d7ef8e15ea29c3e1c727c90cae16b1d9a0c01d7c15d", + "Work/GCert/Data/Gen/P193Par.lean": "b439844169874ede0d44ec2f44a7c2012a781f9f982180eafa8754601797309f", + "Work/GCert/Data/Gen/P193Scal0.lean": "46d9239eddf2d47941249ca3358c682e45e43721c6a0e335cc8866d736576540", + "Work/GCert/Data/Gen/P193Scal1.lean": "c1050c7769d8649949bac1e7e573323d0db777547d16219950fb98891e329519", + "Work/GCert/Data/Gen/P193Seg0.lean": "2cd1b966fe4f3099fe0930960c3bd1f0994b2e16166be8cc53998d43b414a6d4", + "Work/GCert/Data/Gen/P193Seg1.lean": "ea2740d3367bb121923bd9edd11423c4cd1033b7a11fae3eb28daad4c9698446", + "Work/GCert/Data/Gen/P193Seg2.lean": "8e61f9888a1d03b285429443eb5d40c9067e4924d9f39bb108513aa067c14b01", + "Work/GCert/Data/Gen/P193Seg3.lean": "f00b4f2eac6b1513dde2c314bd4c3103539d1fa00cc9b1f6a4630a0b09bc9788", + "Work/GCert/Data/Gen/P193Seg4.lean": "21c89977bdc341220dc62ddb177d6bf510073868a8002fff6437b36ca9c5ba75", + "Work/GCert/Data/Gen/P193SegF.lean": "56cc778db0db3a02965d85456a0124adb9c21081ac805dcdd74f16f1ca6c5771", + "Work/GCert/Data/Gen/P193Tab0.lean": "6316f6007d240d4731f6db877b0d76aafd04da228490167ffeff630791a3f6ac", + "Work/GCert/Data/Gen/P193Tab1.lean": "635aca0625cc06c21796aaae95d465b5b9e849f816ce2ba1a83df59a7f562895", + "Work/GCert/Data/Gen/P193Tab2.lean": "3885ab538ab6bcc890bd704256cec538b88029917e68bb57ce1720ccd9581c16", + "Work/GCert/Data/Gen/P193Tab3.lean": "f6c4cdc134a644de025df9c8e86d2e2ff00a43ed2549f6117816f86f67ac1901", + "Work/GCert/Data/Gen/P193YChk.lean": "3943617b7681a6140cb315953d7b2aa05dcb6640275191574f70c9addfd8d981", + "Work/GCert/Data/Gen/P233.lean": "0fcaf7a9a647b3a0d87a626c2b6a9048b344d8338221dbed35bd637e650f9ce9", + "Work/GCert/Data/Gen/P233/S0.lean": "bdc83eb82a633368e29b1b94bcabb6006fece39c75ab284d1d40d60f6fbaa8b3", + "Work/GCert/Data/Gen/P233/S1.lean": "a422660adf41bd6ab70cb5a6e2c7d1bf84e6a2bd845558c2a784436b9ab77f61", + "Work/GCert/Data/Gen/P233/S2.lean": "2b50fd1a714db88b1c67063269cd71cd3e0783dbd5f67dfb631e1b804432c772", + "Work/GCert/Data/Gen/P233/S3.lean": "e38d01b45716b36feb98bb63f22d87a87755e99936cbd08e1b1bd490f24eaa47", + "Work/GCert/Data/Gen/P233/S4.lean": "f68b912663253168a669b2ffea6f4b7dd2c92aaf1abf38ee6184b3d90a82e236", + "Work/GCert/Data/Gen/P233/S5.lean": "483d3ef75ebc7a4eb37e2dcc649a0e3436265cc5be98dcd4763c1be004555381", + "Work/GCert/Data/Gen/P233/S6.lean": "5164e8093e2a5ccc779c2f064b773398ae1028e050dc2ce97b2be85ccf748fda", + "Work/GCert/Data/Gen/P233/S7.lean": "8b3a670b84c9df745c5cb1fd0a72e6974290b44607d7c88d8d0e37bf58167b77", + "Work/GCert/Data/Gen/P233/S8.lean": "469f63d72742fd685bc2a2b9351aaf2fc37fc98fec7a8130c14005b858b7636b", + "Work/GCert/Data/Gen/P233End.lean": "cb2289f2e4a8f141bbfb24b67963bb6257a26d87f8c85f49c9f12cc549506ac4", + "Work/GCert/Data/Gen/P233Hist.lean": "097c7e7a9ededec13b2ac14b8aa47de2b238db38d23f4633ed07742361371808", + "Work/GCert/Data/Gen/P233Par.lean": "c49a2f6145f077be1442fec6c80f24a1e7677d28c2f4d87250c05818f34c87c6", + "Work/GCert/Data/Gen/P233Scal0.lean": "74c0fa060312c2b725946e4a9cc385acc274c2d3f0d146b8becfa0bc55bc084b", + "Work/GCert/Data/Gen/P233Scal1.lean": "21569ef82221f968c5fa0e2bd6343393c2273e25c580f00b2c02b220fec60f6e", + "Work/GCert/Data/Gen/P233Seg0.lean": "19a0a4b474b9084018d8f53a71f314757e6692a272718df4252dab6c8861d8a5", + "Work/GCert/Data/Gen/P233Seg1.lean": "481f37222d7c761cb04c1b67789f0aa22bb031451e4e9dff4fa774c15a2ac625", + "Work/GCert/Data/Gen/P233Seg2.lean": "66610ffb66898cd8724fabc4adb7cd57fcbd97d11157d0f4ca9934e0ae3d623c", + "Work/GCert/Data/Gen/P233Seg3.lean": "d4bfe286d30327851638d22349728dad642acf280f7524b5e8efba4ea775d086", + "Work/GCert/Data/Gen/P233Seg4.lean": "4a94d8c3a3b92db357e6163059c3ff05c337f529ee9fd7dfb45402494e502a77", + "Work/GCert/Data/Gen/P233Seg5.lean": "a3242a4453967417cc1221f2e291784fa8354cc302e01675ddf7c09e12912e6b", + "Work/GCert/Data/Gen/P233SegF.lean": "ff802a31474d3994d170f9eaf163f5a49b20e86c696a93487570a4172ecd3b1c", + "Work/GCert/Data/Gen/P233Tab0.lean": "a49e8c1b1e6df946572c00e718877dad1eb660892c713d2f92b5a757810d95b9", + "Work/GCert/Data/Gen/P233Tab1.lean": "174e21a9fdef82bc1a3eeef63ce25d40a2e0eedd625e1ff1e229c9a12378df78", + "Work/GCert/Data/Gen/P233Tab2.lean": "4c3334dd4b7314d63b213aa5ce74d94ec008d7f8b9bd21938ea7c94666209dad", + "Work/GCert/Data/Gen/P233Tab3.lean": "945d4121d407dc33c4928fef6513fab0f3f00b0d39c564599f5d02af96319c31", + "Work/GCert/Data/Gen/P233YChk.lean": "cfc3b2f21a761119d4296cff40faedc3116b81d4d971ed3d995a6c0a3ff76dac", + "Work/GCert/Data/Glue.lean": "d5314f2b93a7f0e1c949fb502331825bfc6d9d8762d35f865443e7c95b6c7ef7", + "Work/GCert/Data/InstB2Gp193.lean": "9587ddb9961f44938032b609307ab91c0b0e757e3991f1ad95480dd50fd4f72b", + "Work/GCert/Data/InstB2Gp233.lean": "c542f3212cf662d2b0c4314eb1ca714ba61c15f211fc93f6d517f9ab7d273b6d", + "Work/GCert/Data/P193Cert.lean": "d92ee6889be4753fc99f467bd84039743325123a1165128378b9c906a04f2703", + "Work/GCert/Data/P193Price.lean": "0299bcd0fe255960eec682eef0f045f7e5cb1e4711af2aab4393526eae2caea3", + "Work/GCert/Data/P193ScalOK.lean": "479434815822e98f015e335361089c3788d00dc3dd39c2944f75410aa0c158fe", + "Work/GCert/Data/P233Cert.lean": "c60bdca55b537c097fd7e0414df21b1910d4bb083eb768143241f0de27907d1b", + "Work/GCert/Data/P233Price.lean": "b575833fffb4d10e1f2d9b6e52418b5358b2daab2ce6bbf9a6e607144aeab209", + "Work/GCert/Data/P233ScalOK.lean": "2cbda1fa7174458c8de701921b469cb023cedcd69c587bc1258741f8db0f0395", + "Work/GCert/Data/Price.lean": "fa1b36811c54fd7a996b41e4c1f9418ee77eaea1f5216d4124dc37173560c8c9", + "Work/GCert/Data/RateB2Gp193.lean": "aaee535b0e86bf7443c1dbd96588c45ed648c6edb3d5f253d8fa81b10cedab46", + "Work/GCert/Data/RateB2Gp193x.lean": "6b40cac1481c931d47b1a092e382d04716ede0e785c492a2f2983e886a257c3f", + "Work/GCert/Data/RateB2Gp233.lean": "7c48ab80db14f659562a6178c3c2892cd3a5c1ec8c6962a73bc46bed0eca0f60", + "Work/GCert/Data/RateB2Gp233x.lean": "ae20eb33c14df34121586b49dae0a5a4284bd46e5a4b173eeeafd6d323072cfd", + "Work/GCert/Data/Raw.lean": "aba94a004c94dcae7cf3047c88a6da9561555f4ebe8ab92e299e6ce09ee7aa66", + "Work/GCert/Data/SolutionB2Gp193x.lean": "45c768c9d71a7cc18bd6db74cb036db880d89580ca60557bb4a492280296b169", + "Work/GCert/Data/SolutionB2Gp233.lean": "1f71dae64005f4fab569641f791fdfb8f5542ea621f79148e980408676309341", + "Work/GCert/Data/SolutionB2Gp233x.lean": "b66ea56aa84e84951a53d1ee169fcd72bc86c844fda0d5a45634e2caf1f9c305", + "Work/GCert/Labels/Bits.lean": "f789644886af79704a178aa22176601a73afbb5db945d0dfd6973f2375564d27", + "Work/GCert/Labels/Canon.lean": "bcd2e2dffa0d3dfcd64fa04bc51c9dc426ea8ad19cfacf4b9f84d7cd6e74c2e8", + "Work/GCert/Labels/Def.lean": "9341d2d0ae47b7d997af29858e39693cc8c23bc95e8811b11a2b2bd37e3dfe8f", + "Work/GCert/Labels/Elim.lean": "153ba2a39a3441e8cd5529baddf2286232342cafbea9908aac3839b3a1abb7fb", + "Work/GCert/Labels/EndDef.lean": "8e83ac9f01fafc3c33743405e721d2dc1651b80bcb7587d61a8ca986014fa1ca", + "Work/GCert/Labels/EndSound.lean": "2533d90c95d6eb32665cba6080d27bd975cfa456dfc6fb37f0c76f85b11e7fa1", + "Work/GCert/Labels/Ends.lean": "a27b55dc864addf2c34485dd01aa4cca7a668e617dcb6dcb8b281a9a421aeae1", + "Work/GCert/Labels/Main.lean": "1c564ed3571451b7c9b568d97e9397f4daa77d4220a99ac15a6407995a677796", + "Work/GCert/Labels/Route.lean": "fb8a14b5e46b4d9435ec6a04621689c152c272ae67a470898e357928aa9422f9", + "Work/GCert/Labels/RouteRun.lean": "cb6133e09a209f8cdbf7c96e107506bd6a1588a2ee313e0afe6e48a12c746007", + "Work/GCert/Labels/Sound.lean": "684aade7c7441f57b1e85bee5c64aee00d62cd5e5ff947fcea9cfe5526dd9da2", + "Work/GCert/Labels/Spec.lean": "d2d7c537e801c497b5a87c0f501ad3ad1f42e89d23c7c3a7aacddc786cca9154", + "Work/GCert/Scalar/Bits.lean": "36e76a9bdc4a8cb0124c5998e6853fdceb8cba8c7773d601bf501be308cbd4e5", + "Work/GCert/Scalar/Check.lean": "34122ac94edf27d6b639773a5a6c12ab576b666c1004c3006e2c993671d3e49e", + "Work/GCert/Scalar/Cols.lean": "46635a2794597d7016672022515e2e4d439e21bc8e9f664517d3b1397b8c5800", + "Work/GCert/Scalar/Def.lean": "00432825e66720d4e9c8f217c94b9a1e846b64ae00c5612fc9b7f3b7c1db0b1f", + "Work/GCert/Scalar/End.lean": "68cbdc36c400c8f7151ea6c20afc9f4ae4073df1c2ec6ba0b922bd69f8893f53", + "Work/GCert/Scalar/Fin.lean": "a0e6f6d5a9ec97da809bd4c1013da0f0a6740a40cd08199f30bfbe2d5435d44c", + "Work/GCert/Scalar/Id.lean": "43ace9b4a7637bf369e8f5d0fdfa45b62b1e447938a7db39a149fcca5f571f49", + "Work/GCert/Scalar/Main.lean": "67543f5218392fe289831c9c102241e2b979bdfd4708c6988baba0437d6565ab", + "Work/GCert/Scalar/Mat3.lean": "0180a9acdc4101ac8634fc55123475d8132887208e4f0bb6f9197db1f14cfa20", + "Work/GCert/Scalar/Ops.lean": "63be6e74549092dfa27792f669008a27e0fd74ea7ee2a5a167989b44e34e4551", + "Work/GCert/Scalar/Roles.lean": "fc53e98fe95d1a1b01ec1de618a322ccbf2a46ac7662d24758e8671686fd6fb5", + "Work/GCert/Scalar/Runs.lean": "d8caa9c7454befdff58063535663f17bdc121c961915f9eebba90a464674bf76", + "Work/GCert/Scalar/Scat.lean": "70928cd19a66b7816690492cdbfb37dff5ff652e40ae3791d22b7acf82780888", + "Work/GCert/Scalar/Seg.lean": "988f298ed4bdf728bd1efe518492a2f97bbfffe62856a23b0977fb81d7f4c453", + "Work/GCert/Scalar/Step.lean": "ab682f29ac3ce23dd90ac3d547b0731db37a522505cf59977110074babd8f332", + "Work/GFrame/Clifford/AltBlock.lean": "56f9384c8d2db9df47a3d089d54fcfd6ebd91978893bb9b9df9fbd4c55e14d9d", + "Work/GFrame/Clifford/Base.lean": "766e6b2cb772542294a87e76ae074883c4149c34ebaf9ab30de66b5ab9f01f0d", + "Work/GFrame/Clifford/Basic.lean": "f6873c24735302951429a2a1ab995eb2b6082d38d124a1928e99955ca14041cd", + "Work/GFrame/Clifford/Climb.lean": "a32fa0866eaf81f11c3db2d84c5076876d4a916e0dad87a2a5bb5ea7b1baa6fd", + "Work/GFrame/Clifford/Core.lean": "4aaacd2ab72b5cd627c619f7083595a3c82f781dd24eb92d9c28a9ef424b3285", + "Work/GFrame/Clifford/Cross.lean": "345367b52a8db9157a72c856b5eddcd4328283403bfe0fa508987ae72911b4fb", + "Work/GFrame/Clifford/Entry.lean": "1c6cc8069b3a75561e1be916e106488bcd4801bec911ea41c812c9331b71122a", + "Work/GFrame/Clifford/Fibre.lean": "27fac28943ddd3cea379a5d152e2afbef9a392b039031be0a7e3c9648dde7fa1", + "Work/GFrame/Clifford/FreeLift.lean": "14ed75f64eaa1b77df40b7362caf2ce36ee6562c8047f5e31f1fba95a8a950cc", + "Work/GFrame/Clifford/Old.lean": "8867a97e76db6684be9d669329da1a15c89adb1ae68ba0e2748d0ee0579671bb", + "Work/GFrame/Clifford/Pair.lean": "5709a72f9e107569cea57a7a10a666b408ccae7d2bc9cf849c2e8fd146ea04af", + "Work/GFrame/Clifford/Rep.lean": "a610cc6aec99254c9d42bfd71eed5de6d68acb70490a7b672d697c7c0e282f81", + "Work/GFrame/Clifford/RepFree.lean": "5835e57774c29f6df1492e13bbbb309a7241b75daf4fc86acd565c63eef92a04", + "Work/GFrame/Clifford/Step.lean": "5171af0fcb563d2bc33edc174cd5eb1c34b95ca7795af9aa5ed3fa4c1f934b38", + "Work/GFrame/Engine/Adapt.lean": "feec0a3828867968a5c7c2c30b86ed70449abc3c660a60ada67203a75bae2ef7", + "Work/GFrame/Engine/Cert.lean": "35dac37ae7696ed39d50bc45a7e8e2d36669f0c1e22f85b1c9ae303693211a09", + "Work/GFrame/Engine/Free.lean": "66c0bf81542366af8af6b785760f5519867e38f7f1aeb36603fdd8a282a7bffa", + "Work/GFrame/Engine/FreeLift.lean": "2444500f1b6b5141e116bed0daf8860a5295c05d247eaba124e13dcc27c6395c", + "Work/GFrame/Engine/Group.lean": "d886db1e601a2a5ef9040570958866df48e512077f8181c70d0feda5c4a64c3b", + "Work/GFrame/Engine/Letters.lean": "34906dbf5ae16b5174db00b4881a5cc1d2e583b8c8806db6523a5e2f86565f09", + "Work/GFrame/Engine/Level.lean": "80fb3daa9a45de0ed6da570eb4476b9104734be65d0116f58bcfcbcd67f771d0", + "Work/GFrame/Engine/Main.lean": "dfa6546a16da9acb23adc82db8461b665e9339c7dd375365b9577b44fb035457", + "Work/GFrame/Engine/Over.lean": "b562e53ae56941e796f551d530426417929c1c7fb9dcb31bf0c16609854ec588", + "Work/GFrame/Engine/Recursion.lean": "8652fed961ba0279ea7aef3f079555ba09bf495a538173663594bd6118f06de4", + "Work/GFrame/Engine/Route.lean": "183ba200d92faf67fa41fdaa011980e7674e6f878b3c1f0da028c3f85f4ddc11", + "Work/GFrame/Engine/Sweep.lean": "b0db6efefb2e45b0c21960c9eea07959472c2310ba80ba683df0329d2c245b3a", + "Work/GFrame/Engine/Twisted.lean": "35834d0e8d20e6ea9a507337566b13bfaec45cae5d49afec826db8fb7555bdf8", + "Work/GFrame/Labels/All.lean": "b52d3b7085baed31f474443eaa4f6442e4f8bc76c5bf619d382dca9f81788833", + "Work/GFrame/Labels/BXMap.lean": "3969a0c31038747cabe865de6deb2ee43dc2c6c98c51985e92b01fd0bafd6eb6", + "Work/GFrame/Labels/Calc.lean": "6eff24c202d1215e19bd71d4896ca6cfbdd1f4c30f17b4842fc19e8a864d9f04", + "Work/GFrame/Labels/Conj.lean": "1fa5042338df34ad4fb0323f88af73bf32161b1f4cd73e47b27b3363347a737b", + "Work/GFrame/Labels/ConjB.lean": "01076faaf0d65ae81c9a18ec77ec3c223d127e750d92f22945c93ec69bbd73b9", + "Work/GFrame/Labels/Embed.lean": "567211a16c1d2e3652e1f1d71b2981e3e85a4c4816ece47a2f9094a6a3081d45", + "Work/GFrame/Labels/GCalc.lean": "b2a15fe480347aee457112dc4addb30ac92134f885d45a6c7d72abb6d28f0f19", + "Work/GFrame/Labels/GCarrier.lean": "fd613748598bcf50b9f564abaada1e9869a372b2b32c111487f0d983e54e5044", + "Work/GFrame/Labels/GXMap.lean": "2bd55d1c08e7c18285f6f7580015eb721a2a129d7b53bef2d74d3592bd72944f", + "Work/GFrame/Labels/GeomOld.lean": "c4965008410543ea2213e13fc28190cb2404bfebbb83bda21e32755072a58dc3", + "Work/GFrame/Labels/Maps.lean": "bfd189030c5aaf39313b520ea654851d623525ab6484dac9e6501751632a9856", + "Work/GFrame/Labels/Proj.lean": "28553dd2ed5cdb3a359e60f44997b55a897befae05d7f5aaa2752a5f36bba625", + "Work/GFrame/Labels/Quad.lean": "406533b1663c222d918a59cb8044617040d498a64b3e75075c1eafb4eb5a63b6", + "Work/GFrame/Labels/Sched.lean": "7062ec3650bf18ddc9abf4d4a87c6bb707e46d44e24f19ccd64589fee5fd0cf2", + "Work/GFrame/Labels/SchedR.lean": "8f6b2575c320b316d51c50628fceb9e6c2c4e673e45e59f72f26205694289a5a", + "Work/GFrame/Labels/StageA.lean": "6c901fece3a79a685b17110dee3a863b019a36f703f12548c7f9b8df4c1ea573", + "Work/GFrame/Labels/StageB.lean": "938fb1e62ada9f85177ab41d54983228913dd4801be2db898a5b552a1c469ebf", + "Work/GFrame/Labels/StageBFull.lean": "abdff8a0e10b23484436f6b805f6075847dba28450e9a53894726a91d9aeefd2", + "Work/GFrame/Labels/StageBSem.lean": "d11a8da3738d2f8cfbdf83966be10be1b22187e40038cc1f6a776ca6d1628ed7", + "Work/GFrame/Top/All.lean": "d7e4049aeb4bc3d6ab0780348e1f9bfbd15cbdb413c2c1cbccbbbd5b1b83033e", + "Work/GFrame/Top/Api.lean": "199a2ab07812beb34c205da661618a5e224d46c231ac03eb9fe6d32a7acdcd36", + "Work/GFrame/Top/Assemble.lean": "7f1def0d3d682739103b36c9178706d8f50bde045c66247aa69e26c66c186bdc", + "Work/GFrame/Top/Flag.lean": "74cf41ae9cc07cf63319523588bc1c69fa4d617f04c631ff962fe51b6a9a8269", + "Work/GFrame/Top/Menu.lean": "46e1dd2db8e24535ea74b0c3259589979eb6b58d0f2a7afc9b5061ee9f505fd9", + "Work/GFrame/Top/Regress.lean": "2abb9173dac1bb7a34a64955cad1e74ea6be034fa656fee33f54a812478806ae", + "Work/GFrame/Top/Stage.lean": "79420c95d2c212a911ba479ed7b09f697100942304272745bed937d473522d23", + "Work/GFrame/Top/Stages.lean": "829325a6136ef4d853c59be5fd3dbe1a9a8a61a4a1f9ca75e62ddda308564165", + "Work/Reframe/Basic.lean": "53a495d08b2512a6889a745c6db1a487b9dd288100bf68e4d6d437e814e1abcb", + "Work/Reframe/Erase.lean": "d6acad276ea1531d17cd6609a8440d74748b102e53c149ce364dcc2b0644c8d7", + "Work/Reframe/F3.lean": "2bcef1ed3573e4c30580c0cedee7943f543539569c1f7ec412e382200c440672", + "Work/Reframe/FrameAlg.lean": "404c2bda1235150dcf974154963bcd701a1e494b147ebe3812fed21fa65e8bd9", + "Work/Reframe/Geom3.lean": "52550820c6855b79a6274e5b17a9a4d6614784d09d3644f751518c7da6daa24e", + "Work/Reframe/GeomBase.lean": "f8f007cb2199233db6416e41bbe84aba85d9ccc21b905a1eeac4d847809d4bcf", + "Work/Reframe/GeomNet.lean": "09322559053aeb2e34ca3a653fedba2c17aaf5bcffa3a9f65acf00c40ef77408", + "Work/Reframe/SCert.lean": "4c69fef38100842fdd1b6e058a36c367543b4fa5bd99918ce393004208f07a41", + "Work/Reframe/SNet.lean": "4e7279544845d559e3b6431feade48e139eb994656b6fbad8c7608b34056d698", + "Work/Reframe/Shared.lean": "6d05bfb4afee6473d5d2e5a7db1dfe85e345f16bbf41fb556fb4951025b0739f", + "Work/Scratch/Engine.lean": "61719f5eee7f49b92c1d813153eaa6df6f7830eb7bf2a9b179b880c6615997f9", + "Work/SharedSumChecker/Bits.lean": "7015024d2b4a1074443b4ca10b2ed2366fd00933efb3ef9ed969e099f56dc0a2", + "Work/SharedSumChecker/Check.lean": "e74782bb97b326ad480ce0140a1eec75745d823a9307535200f1b17ca9d81028", + "Work/SharedSumChecker/Circ.lean": "5b955d23d1f8b2a1cb647108d6f8f18535cb2ece6ddc573d9f00b51ad7941e1f", + "Work/SharedSumChecker/Impl.lean": "d30974f060535c379d47d1860d3bdb76c483daaa9466d8b5bc02bb330e7c92e4", + "Work/SharedSumChecker/Mats.lean": "0acda9e50da68a7b2256a9d54613f2280ad577335f9a3bcd5642dd42929fad98", + "Work/SharedSumChecker/Net.lean": "698971523aec89fc9d8395def64c6dd5f19440a1a7675edde2cc0fe610407f78", + "Work/SharedSumChecker/PCert.lean": "97694db183017cb6a13c8a5be9de7fa64cbf50b967fabb4efa8dc696c0f4af06", + "Work/SharedSumChecker/Phase.lean": "5e7bcdfa8947e54c77aeff3078eff66c6a2d83e46dd0764902e8452fde8c6fd2", + "Work/SharedSumChecker/Proj.lean": "473df34ae19c80d9c641f37f6ab0e891d7d342938b85b05a6dbc67a21d46e024", + "Work/SharedSumChecker/Scalar.lean": "a9d50988854bf437ed52fec616d6ccf5671ecfb16d71a3ff47f07d21956144ed", + "Work/SharedSumChecker/ScalarDef.lean": "b35f242d0711c00e5fcc475f86124acc7c6fe9bf9740256fa9db9f895fbc3330", + "Work/SharedSumChecker/Sound.lean": "56b07f3ba590f17ef80e5169dd7f3a7a66e34b5d988484160f34ee736d6a554b", + "Work/SharedSumStructured/Certificate.lean": "25f23138cb8ef251db49c2626d0f9d0caabaf5b0778016449383795ee4457044", + "Work/SharedSumStructured/GPath.lean": "07687321281a337093b892ad30af4cccc0cb854787a77a27aa331d1b54aaa692", + "Work/SharedSumStructured/Invocation.lean": "84e713c917b34f919547d0a9fc652044f5321e7cd97d54f684062e4f04702039", + "Work/SharedSumStructured/Labels.lean": "87177a9ac6a363b015d512d38601c0255310cb18dc285b4808b318751ced46b2", + "Work/SharedSumStructured/Network.lean": "afbbb2cce1090fac4939210879e2e094aa673c54c9d61188a292404f655a29c0", + "comparator/B2Gp193x.json": "b54cb68b5dc0532d31f77e6377fc58471f460d84bd18e29f06ab90382e99e8e8", + "comparator/B2Gp233.json": "3a59da4d51324452243741709d9370a7e96eec615aa3159f7aa65abef8ce94cf", + "comparator/B2Gp233x.json": "228a45dbed862c27b5f3b8445429453d5bf7729f4bec14a681a0dc6a59a33f7b", + "comparator/B2Ke16x.json": "73d2e2eded092ff9f28f7ae6f932d0e7dd4cc6f614795e148ac5f0f8e484e56d", + "comparator/B2Ke16xR.json": "0936bbdf7dcbd39c6b6bd6f5d556f359b855b9169288db734ec0a8b11698b936", + "comparator/UniformFourier.json": "dddd4758b32cf3a7699385a922b9652affa7bdc3e0175c42f1fe24c7ab8a1e64", + "comparator/UniformFourier233.json": "befe2d6bb804aa503130b5dd6399d5d7bb9258d30b54d710868d33ea111168bc", + "lake-manifest.json": "3a7cabde26b0c210cb99f8ad8d523ff7969aea6bc949b6e009a20963802161fa", + "lakefile.lean": "8927b3ee27366af0a026fbaefbc0c5d87fcbfc9138a68ab0938bf71e6cc9f8b5", + "lean-toolchain": "d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b", + "notes/open-directions.md": "d00d17c6b5dafd0432a408cb341ecb80449163c2fd43de9ef225b6ac376acac0", + "notes/scratch-copies.md": "1185fc084c138d4a1e3179b7ba29ff4877598a0d06f059cf7663dcffea124e39", + "third-party/CrocSwap-integer-mult-bounds/NOTICE": "c9850418622aea8d1382a230306c940947b5da818f4854b4b272ed60cf239f6c", + "third-party/openai-math/lean/ComparatorChallenges/UniformFourier.lean": "4c571f275bd7506c3ccd1e6d78f2fca77e07112c969c1c62ad8359d61544ec74", + "tools/Compare.lean": "e48d6d3b5be7f7c84ea949f1dace0a95bd58710c7cd5f3b94c60f4785975dae9", + "tools/ccheck.py": "f4974fc939bb9488604b7d353ed24de7580bfb3bde738a9da98de3bcff2fb772", + "tools/certificate/c2-combine-best-h16.json": "1325bd8a6ccf1bfa2b773d9846c2e7dc8c120c4860c2b4317e109de3e3a20d51", + "tools/certificate/gcert1-p11-pr193.json.gz": "15251deb0c11e0504d7b297c9786818888a93f08b92b03c6c122784b70488633", + "tools/certificate/gcert1-p11-pr233-flow.json.gz": "ab4084bac84aed0982d4dda3e799f2e49effbba7d24c1cc9701a3a870c3415e4", + "tools/emit/ORIGIN.md": "172e208fe80377aeebe1d97fd83eadd1eb923b30432406f29a9b3d45711e30f7", + "tools/emit/gcert_emit.py": "10d2fc3f1f3d8cda5f0b07720f51b5a6fd40cfc1490d361939ff93e5470805d3", + "tools/fourier/mkchain.py": "f1e5d832b98e836a47ff1f85a199f8d9736a18ee48d3a1dc84a01c5ae3570c9c", + "tools/fourier/mkchain233.py": "5712d92772bd9382cd7639c2784382906eca7b42222b6923264532d99e36562c", + "tools/fourier/regen_check.py": "deaff6791fd4198e91559469b54548ab9220ac177a4947a28d5f57aaba04f7f5", + "tools/fourier/regen_check233.py": "cc8c1f085b767ec2e5dd6591c7310c9afa1552b3268819cd90ff5af3ae429ca0", + "tools/gen/b2inst.py": "1a0a717d834333431fdb87ca94a03b89803c5d96621da836feb66e2930de6aac", + "tools/gen/ccgen.py": "31b9c9716d7190cebf95b5a21d7547aa62b2bf70f94a065c6cde6b3ec28d640b", + "tools/gen/crate.py": "a3393d7d7e1a08f5863e0eeafcc6f44c7c98adf8cf890cc25e592118d56de588", + "tools/gen/foldgen.py": "a0f16e2c9e078ffbfb2174281ee93a48c18593aefb880318fc105ec85a205932", + "tools/gen/foldlib.py": "7a3c38a698c129e13a767da75926a1305eb0c031b908450afc6feb185505c59a", + "tools/gen/gen_rates.py": "ef8c869e4cf8da33a4c10b96f7f6faafd46e15d66766238070a60315aa169994", + "tools/gen/gen_sharp.py": "1b5eb3730cb16cf516e760879951fdfb9b065efc55f78c29a5c6404fcca57a78", + "tools/gen/templates/ChallengeB2L16x.lean.txt": "0488b7a2442c795414f103df912d1e6cc66d37b5be270940ea9564b7f2b666be", + "tools/gen/templates/SolutionB2L16x.lean.txt": "d414a890dfe126916374c1afc804b90e5081b7760f894b9ccdcf23d83a12f9ee", + "tools/gx/ORIGIN.md": "f8ab278847b09fc92c4a550bc8b25acb857ac51ab00ae73db02a9e928a74cf7a", + "tools/gx/gsmirror.py": "0e22bbe5924284e2fb916337ccefc8e41f6e54469749986ad15b3b81cfaec534", + "tools/gx/gx.py": "6f3dc8bb639933227a8dae181ec4a542e85c7276be9c9e330f49518e7b630b95", + "tools/gx/gxbind.py": "9c9dcfac47f0535bf3aa8ebf7c662cdef0ebda50a9f0a9282b8f3cf34809f835", + "tools/gx/gxconv.py": "dab7fec9f44c2d368ed334055d7126e202017feb46e41a8d86e2d998720f67c2", + "tools/gx/gxcore.py": "eb972c06fe8c322db2d9a8d9a7d05596e8f40c4ca8e5f42eb6df3c7361b5d517", + "tools/gx/gxdry.py": "e42527388f74437356579cb33efa80d0dc7306c6dc5808fc1e9000afa990661a", + "tools/gx/gxgen.py": "ce9151054370c2210ed08f54c249a19dcb6946d182cdf934dee1a3781b53040f", + "tools/gx/gxmut.py": "13ca344410c4494cb50605c2cc147ad8f4d9e43ce638afaeaa02f2a47a8fd555", + "tools/gx/gxpaths.py": "f00802d48ef3fedb00278f0b1c7bde074cc49dd30f202d7f32a9d2aebb3be443", + "tools/gx/gxrate.py": "514a5719f970fe36b1273cf59df0396db0e042dd7864c2eea53ab2a2fd1e2ad6", + "tools/gx/gxrun.py": "7e61f035c6a2b0c1994913454c98aac394afee168f3ca65d96dd4a5bf47aa393", + "tools/gx/gxunit.py": "3cc09a9c1a2db681c0f2016bc821af5b674d34834dbd6f195b9d482ce7c0ff58", + "tools/gx/refcheck.py": "d352d0f1b5054dad7a89a4d4ac93d2dbf995f866e2fcbeb652432362fed5dc32", + "tools/gx/regen_check.py": "b6172d58749c0b3b9138570c74827bcb23bf5db4ff9643740768cd7782ac4ca6", + "tools/landrun-macos-shim.sh": "3c38ffaf28b9dda4b64a838b62fd318ebe4de736f2afe4d25d89c0c6df3bc13e", + "tools/regen_check.py": "36ccb9b22f0ef6df6b139c4476deb6c51900d0fda8ac4bdc6df3e08772681420", + "tools/whatif_copies.py": "ab66e142da1b4d2411bfe33d7858d8b4b62443ed96534214484d4d7d5dbeeaf0" +} diff --git a/research/pr256-fourier-audit/expected.json b/research/pr256-fourier-audit/expected.json new file mode 100644 index 0000000000..7e9291e92d --- /dev/null +++ b/research/pr256-fourier-audit/expected.json @@ -0,0 +1,81 @@ +{ + "absorption_gap": "1/10000000000", + "bindings": { + "lean_exponents": true, + "lean_histogram": true, + "lean_program": true, + "openai_challenge_modulo_exponent_and_names": true, + "openai_commit": "fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb", + "openai_origin_files": 91 + }, + "finite_fill": { + "gap_lower_bound": "161135866885975440961/200000000000000000000000000000", + "s": 40 + }, + "fourier_saving": "47171/62500000", + "moment_gap_lower_bound": "805679370026745227701/1000000000000000000000000000000", + "negative_control": { + "excess_lower_bound": "205075942678928992113/1000000000000000000000000000000", + "saving": "1509473/2000000000" + }, + "network": { + "calls": 358975, + "child_histogram": { + "1": 145890, + "10": 4025, + "11": 1765, + "12": 5705, + "13": 840, + "14": 3625, + "15": 3025, + "16": 405, + "17": 195, + "18": 13200, + "19": 7205, + "2": 63335, + "20": 110, + "21": 2640, + "3": 49940, + "4": 21835, + "42": 2640, + "46": 2640, + "5": 9880, + "6": 7455, + "7": 3210, + "8": 7390, + "9": 2020 + }, + "deficit": 3080, + "m": 110, + "max_child": 46, + "rank": 1613040, + "roles_per_vertex": 14692 + }, + "program": { + "frames": 18248, + "gates": 52300, + "invocation_blocks": 69683, + "invocation_rank": 262944, + "reference_checker": "Jacob Sussman gx.check1", + "registers": 12052, + "scalar_scope": "all source columns; dirty-scratch restoration is proved by the Lean invocation theorem" + }, + "schema": 1, + "scope": "Finite Python checks only; see five_stage_lean_receipt.json for the separately reproduced Lean build.", + "sources": { + "five_stage": { + "commit": "db3f75cdc5f03f3131d48fb220f6bf1958404ff3", + "repository": "https://github.com/chafreaky/integer-mult-bounds" + }, + "fourier_proof": { + "archive": "fourier-proof-source.tar.gz", + "base_commit": "f010392c923279e3dd59ef3aa5fedad23affc5fd", + "commit": "fd19e46b728faa414cbfbf91b01a6a0b7903375d", + "lean_toolchain": "leanprover/lean4:v4.34.1", + "mathlib_commit": "d13f23b723b8a846827a245b89c10fc7d3f11612", + "pull_request": "https://github.com/jacobalansussman/wht-power-saving-lean/pull/2", + "repository": "https://github.com/chafreaky/wht-power-saving-lean" + } + }, + "tensor_saving": "7547361/10000000000" +} diff --git a/research/pr256-fourier-audit/inputs/FOURIER_NOTICE b/research/pr256-fourier-audit/inputs/FOURIER_NOTICE new file mode 100644 index 0000000000..63aa295646 --- /dev/null +++ b/research/pr256-fourier-audit/inputs/FOURIER_NOTICE @@ -0,0 +1,290 @@ +Walsh-Hadamard power saving (wht-power-saving-lean) +Copyright 2026 Jacob Sussman + +Repository: https://github.com/jacobalansussman/wht-power-saving-lean + +This repository is not a project of OpenAI. OpenAI did not write, review or +endorse it. The package name "OAI" and the namespace "OAI.PowerSaving" are +those of openai/math and are kept only because the new files extend that +development. + +This repository is not a project of CrocSwap/integer-mult-bounds either. Its +authors did not write, review or endorse it. Section 6 says what is taken +from their repository. + +This repository contains files from, and files derived from, the repository +"openai/math" (https://github.com/openai/math), family 130, "Exact Fourier +transforms below n log n", at commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. +That repository is published under the Apache License, Version 2.0. A copy of +the licence is in the file LICENSE. The upstream repository has no NOTICE file +and its licence text names no copyright holder; the files are attributed here +to the authors of openai/math (OpenAI). + +1. Unmodified upstream files. + The 89 files under OAI/Computability/ are byte-for-byte copies of the files + with the same paths under lean/ in openai/math at the commit above. They + have not been changed. Modified copies of some of them are under + Work/Fourier/ and are listed in section 7. + One more file of openai/math is here unchanged, outside the Lean build: + third-party/openai-math/lean/ComparatorChallenges/UniformFourier.lean is a + byte-for-byte copy of lean/ComparatorChallenges/UniformFourier.lean at the + commit above (the statement of OpenAI's Fourier challenge). It is included + so that the modified copy named in section 2 can be compared with it. + +2. Files that contain upstream text. + - Work/CarrierCheck/ChallengeB2Ke16x.lean, + Work/CarrierCheck/ChallengeB2Ke16xR.lean, + Work/GCert/Data/ChallengeB2Gp193x.lean and the text template + tools/gen/templates/ChallengeB2L16x.lean.txt each contain, as their + lines 22-270, lines 9-257 of + lean/ComparatorChallenges/UniformFourier.lean of openai/math (the RAM cost + model), unchanged. Everything else in these files was written for this + repository. + - Work/Fourier/UniformFourierChallenge.lean is a modified copy of + lean/ComparatorChallenges/UniformFourier.lean of openai/math (the + statement of OpenAI's Fourier challenge, 336 lines). Changes: a comment + was added at the top; the exponent 1 - 1/(10^(13:ℕ)) was replaced by + 1 - 7474546/(10^(10:ℕ)); seven names received the suffix "Z" + (decimalExponent, decimalTime, TimeBounds, DFTGoal, ConvGoal, + transform_main, convolution_main). Everything else in the file is the + upstream text, unchanged. See section 7. + - Work/Scratch/Engine.lean and Work/Block/Engine.lean contain copies of + proofs of openai/math, changed for this repository: sections 1, 2 and 5 + of Work/Scratch/Engine.lean are upstream proofs with the batch layout + renamed, and both files contain a copy of the private upstream theorem + "hills_project" (lean/OAI/Computability/FourierTransform/ + TensorProgram.lean) with its envelope generalised. The comments in the + two files mark these places. + - lakefile.lean is adapted from lean/lakefile.lean of openai/math: the same + package name, toolchain, package option and Mathlib pin; every other + dependency was removed and the libraries of this repository were added. + lean-toolchain is a byte-for-byte copy of lean/lean-toolchain. + lake-manifest.json lists Mathlib and its dependencies at the revisions of + lean/lake-manifest.json. + - RELATED-WORK.md reproduces the BibTeX entries of two manuscripts of + openai/math. + +3. New files that build on upstream proofs. + The other files under WHTCheck/ and Work/ were written for this + repository. They import the upstream files, and several of them generalise + or adapt proofs of upstream files (for example Work/Block/Recursion.lean, + which says so in its header). They are changes and additions made for this + repository and are not part of openai/math. + +4. How the new files were made. + Jacob Sussman made the new files on 2026-10-08 and 2026-10-09 by directing + a team of AI agents (Claude). The agents wrote the new Lean files, the + certificate data and the generator scripts. See README.md, section 4. + +5. Ideas taken from other public work. + The network of the first result uses ideas published by others, among them + the helper circuit "NStar3" (Swapnil-jain/integer-mult-kappa, which credits + CrocSwap pull request #36 and Paureel for parts of it), its transfer to + family 130 (shea256/fourier-transform-below-nlogn), and "carrier links" and + "whole-residual batching" (pull requests to CrocSwap/integer-mult-bounds). + No file of Swapnil-jain/integer-mult-kappa or of + shea256/fourier-transform-below-nlogn is included here. One comment in + Work/Scratch/Engine.lean quotes three counts reported in + Swapnil-jain/integer-mult-kappa and names that source. The general frame + lemma that Work/GFrame proves is stated in + notes/general-clifford-frames.tex of CrocSwap/integer-mult-bounds; its Lean + proof was written for this repository. The credits, with links, are in + RELATED-WORK.md. + +6. Data derived from CrocSwap/integer-mult-bounds (second result). + The helper circuit of the second result is the paired-cube circuit of the + repository "CrocSwap/integer-mult-bounds" + (https://github.com/CrocSwap/integer-mult-bounds), in the state of its pull + request #193. It is the design of that community: icekylinx (pull requests + #144 and #184), eumemic (#168, and #117 behind its modules), ikeboy / + Avi Eisenberg (#191 and #193), with an664 (#128) credited there for the + workspace-sharing principle. That repository is published under the Apache + License, Version 2.0 (the same licence text as the file LICENSE). Its + NOTICE file begins "A sharper exponent for integer multiplication / + Copyright 2026 Douglas Colkitt" and says that the community release "is + not solely Douglas Colkitt's work". A complete copy of that NOTICE file, as + it is at the head of pull request #193, is in + third-party/CrocSwap-integer-mult-bounds/NOTICE. + + The data were taken from these files of that repository. They were loaded + as data by programs written for this repository; no program of that + repository was run, and none is included here. + - at the head of pull request #168 (eumemic), + 4a3c769e5c5430e7114c4d3e099ff34664677f17: + references/paired-cube/sources/local_L1.json + references/paired-cube/sources/tmod_TE_TD_TB3_1_1_4_full_6.0617964e-4.json + references/paired-cube/sources/pmod_J0_full_6.0666810e-4.json + references/paired-cube/sources/qmod_climb3u_best.json + references/paired-cube/selected-module/matching-arcs.json + references/paired-cube/physical/frames.json + - at the head of pull request #193 (ikeboy), + 187e1010ac8b259af8e9b5166f68b64bc27b4b47: + research/source-assisted-v4/data/physical-pairs.json + + Files of this repository that contain data derived from them: + tools/certificate/gcert1-p11-pr193.json.gz and the Lean data modules + generated from it, Work/GCert/Data/Gen/P193*.lean and the files they import + from Work/GCert/Data/Gen/P193/; its block counts are also in the generated + modules Work/GCert/Data/P193Price.lean, RateB2Gp193.lean, RateB2Gp193x.lean + and InstB2Gp193.lean. + Changes made: the circuit was rebuilt from those data as one explicit, + renumbered list of additions with a table of frames, in the certificate + format "gcert/1" of this repository; its 1,980 in-place steps were written + as pairs of additions with rescaled coefficients; the Lean data modules + were generated from that list. No file of that repository is included + unchanged, except the copy of its NOTICE file named above. + + Notices of that NOTICE file that pertain to these data, quoted: + + Paired-cube and shared-core extension, 9 October 2026 + Copyright 2026 icekylinx + + Source-assisted common-frame extension (2026-10-09) + Copyright 2026 icekylinx. Apache-2.0. + Substantial dependency: eumemic PR168, + fd25adb7fbaa12ee761d02c733c54d1d2a7687ee + + The full text of both notices, and the notices of the work they build on, + are in the copy named above. The credits, with links and with the words of + pull request #193 about its own sources, are in README.md ("Whose circuit + this is") and in RELATED-WORK.md, section 1. + +7. Modified copies of upstream files (third result). + The files listed below are copies of files of openai/math at the commit + above, changed for this repository. Each begins with a comment that names + the upstream file it is derived from and states what was changed. The + upstream originals under lean/OAI/Computability/ are in this repository + as well, unchanged (section 1), and the copies import them. The upstream + challenge file lean/ComparatorChallenges/UniformFourier.lean is in this + repository in both forms: unchanged under third-party/openai-math/ + (section 1) and modified (section 2). + + - Work/Fourier/ArbitraryLength.lean: modified copy of + lean/OAI/Computability/FourierTransform/ArbitraryLength.lean (224 + lines; 159 of them unchanged in the copy). Changes: identifiers renamed + on 64 lines (18 names: 15 with the suffix Z, 3 with Z inserted); 1 + import line replaced by 1; 15 comment lines added; no other change to + the code. + - Work/Fourier/Asymptotics.lean: modified copy of + lean/OAI/Computability/FourierTransform/Asymptotics.lean (187 lines; + 112 of them unchanged in the copy). Changes: identifiers renamed on 74 + lines (32 names: 26 with the suffix Z, 6 with Z inserted); 1 import + line replaced by 1; 15 comment lines added; no other change to the + code. + - Work/Fourier/Axioms.lean: written for this repository (not a copy of an + upstream file). + - Work/Fourier/ConvolutionProgram.lean: modified copy of + lean/OAI/Computability/FourierTransform/ConvolutionProgram.lean (100 + lines; 77 of them unchanged in the copy). Changes: identifiers renamed + on 22 lines (10 names: 9 with the suffix Z, 1 with Z inserted); 1 + import line replaced by 1; 15 comment lines added; no other change to + the code. + - Work/Fourier/Goal.lean: written for this repository; contains lines of + upstream files: of its 7 code lines, 6 are lines of + lean/OAI/Computability/FourierTransform/Goal.lean (original lines 35, + 75-77, 79, 81): unchanged: its lines 25; with identifiers renamed: its + lines 21, 24, 26, 28, 30. + - Work/Fourier/Main.lean: modified copy of + lean/OAI/Computability/FourierTransform/Main.lean (151 lines; 90 of + them unchanged in the copy). Changes: identifiers renamed on 59 lines + (40 names: 35 with the suffix Z, 5 with Z inserted); 1 import line + replaced by 2; 24 comment lines added; other code lines changed: 1 of + the original, 1 of the copy (copy line 59). + - Work/Fourier/Seam.lean: written for this repository; contains lines of + upstream files: of its 122 code lines, 15 are lines of + lean/OAI/Computability/FourierTransform/TensorProgram.lean (original + lines 36-37, 95-96): unchanged: its lines 93-94, 113-114, 141-142, + 163-164, 185-187, 194-196; with identifiers renamed: its lines 184; 3 + are lines of lean/OAI/Computability/FourierTransform/TensorSaving.lean + (original lines 83-84, 114): with identifiers renamed: its lines 45-46, + 59; 1 is a line of lean/OAI/Computability/FourierTransform/Main.lean + (original line 60): with identifiers renamed: its lines 213. + - Work/Fourier/SectorAlgorithm.lean: modified copy of + lean/OAI/Computability/FourierTransform/SectorAlgorithm.lean (224 + lines; 162 of them unchanged in the copy). Changes: identifiers renamed + on 61 lines (17 names: 13 with the suffix Z, 4 with Z inserted); 1 + import line replaced by 1; 15 comment lines added; no other change to + the code. + - Work/Fourier/SynchronizedAlgorithm.lean: modified copy of + lean/OAI/Computability/FourierTransform/SynchronizedAlgorithm.lean (126 + lines; 94 of them unchanged in the copy). Changes: identifiers renamed + on 31 lines (12 names: 10 with the suffix Z, 1 with Z inserted, 1 + other), the other being "canopy" to "Grove.canopy" (5 lines); 1 import + line replaced by 1; 16 comment lines added; no other change to the + code. + - Work/Fourier/TransformProgram.lean: modified copy of + lean/OAI/Computability/FourierTransform/TransformProgram.lean (146 + lines; 94 of them unchanged in the copy). Changes: identifiers renamed + on 51 lines (21 names: 19 with the suffix Z, 2 with Z inserted); 1 + import line replaced by 1; 15 comment lines added; no other change to + the code. + - Work/Fourier/UniformBounds.lean: modified copy of + lean/OAI/Computability/FourierTransform/UniformBounds.lean (183 lines; + 115 of them unchanged in the copy). Changes: identifiers renamed on 67 + lines (29 names: 25 with the suffix Z, 4 with Z inserted); 1 import + line replaced by 1; 15 comment lines added; no other change to the + code. + - Work/Fourier/UniformFourierChallenge.lean: modified copy of + lean/ComparatorChallenges/UniformFourier.lean (336 lines; 328 of them + unchanged in the copy). Changes: identifiers renamed on 7 lines (7 + names: 7 with the suffix Z); 12 comment lines added; other code lines + changed: 1 of the original, 1 of the copy (copy line 281). + - Work/Fourier/WorkingCompiler.lean: modified copy of + lean/OAI/Computability/FourierTransform/WorkingCompiler.lean (153 + lines; 104 of them unchanged in the copy). Changes: identifiers renamed + on 48 lines (14 names: 14 with the suffix Z); 1 import line replaced by + 1; 15 comment lines added; no other change to the code. + - Work/Fourier/WorkingPreparation.lean: modified copy of + lean/OAI/Computability/FourierTransform/WorkingPreparation.lean (212 + lines; 156 of them unchanged in the copy). Changes: identifiers renamed + on 55 lines (30 names: 28 with the suffix Z, 2 with Z inserted); 1 + import line replaced by 1; 15 comment lines added; no other change to + the code. + - Work/Fourier/WorkingTransform.lean: modified copy of + lean/OAI/Computability/FourierTransform/WorkingTransform.lean (119 + lines; 91 of them unchanged in the copy). Changes: identifiers renamed + on 27 lines (9 names: 8 with the suffix Z, 1 with Z inserted); 1 import + line replaced by 1; 15 comment lines added; no other change to the + code. + + Changes made to the eleven copied proof files: every declaration received + the letter "Z" in its name (as a suffix of its own name, or of the name + of the declaration it belongs to), so that it does not collide with the + upstream declaration of the same name; the upstream exponent "alpha" + (1 - 2/10^11) and the bound "hills" defined from it were replaced by + "alphaZ" (1 - 7474547/10^10) and "hillsZ", which are defined in + Work/Fourier/Seam.lean, and the single use of the upstream theorem + "hills_program" by "hillsZ_program"; the five definitions of the upstream + statement that contain its exponent (decimalExponent, decimalTime, + TimeBounds, DFTGoal, ConvGoal) were replaced by the versions of + Work/Fourier/Goal.lean, whose exponent is 1 - 7474546/(10^(10:ℕ)); + the import lines point to the copies; a header comment was added. + Two further changes: in the copy of Main.lean the same constant stands + once as the literal 2/10^11 and was replaced there too, and the two + final theorems of that copy received a documentation comment; in the + copy of SynchronizedAlgorithm.lean the name "canopy" was written out as + "Grove.canopy" in 5 places, because the short name is shadowed in the + larger environment of the copy. The script also renamed three names + inside upstream comments; the comments are otherwise the upstream ones + and describe the upstream network. + The proofs are those of openai/math. The copies were made by the script + tools/fourier/mkchain.py of this repository. + + Work/Fourier/Goal.lean contains copies of those five definitions of + lean/OAI/Computability/FourierTransform/Goal.lean, with the exponent + replaced and the suffix "Z" on the five names. + + Work/Fourier/Seam.lean was written for this repository. It repeats the + statement of the upstream theorem "hills_program" (TensorProgram.lean) and + the definition of "hills" (TensorSaving.lean) with the two names replaced; + its header says so. + + The work of others that the third result follows (danadran01, shea256, + eumemic) is credited in README.md ("Whose reduction this is") and in + RELATED-WORK.md, section 1. No file of their repositories is included + here. + +Not included in this repository and fetched by the build: Mathlib +(https://github.com/leanprover-community/mathlib4, Apache License 2.0) and its +dependencies. The comparator (https://github.com/leanprover/comparator) is a +separate tool and is not included. diff --git a/research/pr256-fourier-audit/inputs/LICENSE b/research/pr256-fourier-audit/inputs/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/pr256-fourier-audit/inputs/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/pr256-fourier-audit/inputs/SOURCE.json b/research/pr256-fourier-audit/inputs/SOURCE.json new file mode 100644 index 0000000000..ea7960fb5e --- /dev/null +++ b/research/pr256-fourier-audit/inputs/SOURCE.json @@ -0,0 +1,25 @@ +{ + "commit": "db3f75cdc5f03f3131d48fb220f6bf1958404ff3", + "files": { + "FOURIER_NOTICE": "9419dd03a2f52cf8bdfc4d18216ce29f263ab583b27f01ced8e420985bcb7c81", + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "fourier-proof-source.tar.gz": "871f47a16d2571dbcebc2ef61914e85d96b7b44f6d59579da246e13294d5658b", + "gcert-program-233/NOTICE": "c1c95d22cfb0f455aca64b4bee4cab900829641b8f041280e7aa88034491c87d", + "gcert-program-233/SOURCE.json": "9ce463476af549c04de4705b1bf0c8f7f18d473dc0817883066ad5e2136d90b5", + "gcert-program-233/certificate/expected.json": "c0e3d245bf7e458ff86288eb47672491c9efee28181b570f1a3f17c8d915f766", + "gcert-program-233/certificates/gcert1-p11-pr233-flow.json.gz": "09ceba1c0ea17282da155b937c8463669b913443c20f45fe2a7e6e024cb2d33a", + "gcert-program-233/gx/gx.py": "6f3dc8bb639933227a8dae181ec4a542e85c7276be9c9e330f49518e7b630b95" + }, + "fourier_proof": { + "archive": "fourier-proof-source.tar.gz", + "base_commit": "f010392c923279e3dd59ef3aa5fedad23affc5fd", + "commit": "fd19e46b728faa414cbfbf91b01a6a0b7903375d", + "lean_toolchain": "leanprover/lean4:v4.34.1", + "mathlib_commit": "d13f23b723b8a846827a245b89c10fc7d3f11612", + "pull_request": "https://github.com/jacobalansussman/wht-power-saving-lean/pull/2", + "repository": "https://github.com/chafreaky/wht-power-saving-lean" + }, + "path": "research/gcert-program-233", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/256", + "repository": "https://github.com/chafreaky/integer-mult-bounds" +} diff --git a/research/pr256-fourier-audit/inputs/fourier-proof-source.tar.gz b/research/pr256-fourier-audit/inputs/fourier-proof-source.tar.gz new file mode 100644 index 0000000000..a6b5562430 Binary files /dev/null and b/research/pr256-fourier-audit/inputs/fourier-proof-source.tar.gz differ diff --git a/research/pr256-fourier-audit/inputs/gcert-program-233/NOTICE b/research/pr256-fourier-audit/inputs/gcert-program-233/NOTICE new file mode 100644 index 0000000000..bd6b4362aa --- /dev/null +++ b/research/pr256-fourier-audit/inputs/gcert-program-233/NOTICE @@ -0,0 +1,35 @@ +Prepared by Chafik Boukhalfa with substantial Anthropic Claude and OpenAI +Codex assistance. Apache-2.0. Inherited files retain their original notices +and assistance disclosures. This package claims no exclusive priority over +concurrent work and reports no new kappa. + +What this package contributes: gcert_emit.py, the lowering of PR #184's flow +witness and exact lift to Jacob Sussman's certificate format gcert/1, and the +two resulting programs (PR #194's and PR #233's complex words) with their +checks. Everything else is retained and credited: + +- Jacob Sussman (Anthropic Claude assistance): the certificate format gcert/1, + the reference checker gx.py (vendored unchanged in gx/, Apache-2.0, + Copyright 2026 Jacob Sussman, jacobalansussman/wht-power-saving-lean at + f010392c), the Lean-checked bridged five-stage layout and its checks, the + unit convention of gxconv.py reused for scalings, and the published + certificate of #193 whose histogram is the control + (references/sussman/pr193-blocks.json). +- icekylinx (OpenAI GPT-6 Astra and Codex assistance): PR144 paired cubes and + signed decoder (the K blocks and the star scatter replayed here), PR184 + source-assisted construction: frame flow, exact lifts, contract; the flow + DAG and the local completions this package lowers. +- ikeboy: PR191/193/194, the rebuild on the PR168 v4 modules + (source_aligned_local_v4.py, contract_v4.py whose read responses this + package reproduces), and the pairs of #193 (the control's layer). +- eumemic (Anthropic Claude and OpenAI Codex assistance): PR168 modules, + schedules, physical frames (the frames of both programs); PR117/155/157/161. +- hcg890 (PR234), SovereignSteak (PR250: the five-stage ledger statement used + for the price), rohanarun (PR209/237), and the exact-DFT arena of eumemic + (scripts/moment.py adapts eumemic/exact-dft-bounds, Apache-2.0). +- PR202 baseline lineage as credited in references/pr233-layer/NOTICE: + jamesyc / James Chang, DaysSky, GamingPuzzled, gupt1156, Abhinav + Ramachandran/geckods, jacklightChen / Zhihao Chen, Rohan Arun, an664, + Swapnil Jain, hpst3r, Aurel Prosz, dleen, Douglas Colkitt. +- Chafik Boukhalfa (Anthropic Claude and OpenAI Codex assistance): PR200 + maximum-weight reuse pairing, PR233 layer, PR225 exact-DFT transfer. diff --git a/research/pr256-fourier-audit/inputs/gcert-program-233/SOURCE.json b/research/pr256-fourier-audit/inputs/gcert-program-233/SOURCE.json new file mode 100644 index 0000000000..179cf2b1d9 --- /dev/null +++ b/research/pr256-fourier-audit/inputs/gcert-program-233/SOURCE.json @@ -0,0 +1,47 @@ +{ + "description": "Pinned inputs of research/gcert-program-233 (sha256). Vendored byte for byte; nothing is fetched at run time.", + "files": { + "gx/gx.py": "6f3dc8bb639933227a8dae181ec4a542e85c7276be9c9e330f49518e7b630b95", + "references/pr233-layer/NOTICE": "5826b9f155b70d496d729cbaddeadb881abfb68da77f82dfc1746ddfc753313b", + "references/pr233-layer/SOURCE.json": "9ad0549ba2403e8d84d7c0c8e71e5ca952a0604ad626f403426164bd4bc2982c", + "references/pr233-layer/baseline-pr202.tar.gz": "5d08386f71c421d2b83b21020e3b74198e9d0c75884d7d81987307740d98883f", + "references/pr233-layer/certificate.json": "691cb0aaeb0d6b993e1e1e5116ae7a5c57af058a8c413249016347d1b40d3b90", + "references/pr233-layer/verify.py": "cd61a8c61462b4eee95c0858335a9a11bdf1ff8e8e63ebb1e488da29f061ca71", + "references/pr233-layer/witness/kernel-pairs.json": "e33b753fc4519170373207b0527b9cb53e0b552e2a27f48f72381a881c7a227f", + "references/pr233-layer/witness/physical-frames.json": "1a6c215cdc58216f7ec96fb898a471e25d094fd86de085f6c06e86fd8997bfad", + "references/pr233-layer/witness/physical-pairs.json": "e6409fffbf5f3b1ac6434acf2e426503de3a8a18537b8fee761fc4fc931fb896", + "references/sussman/pr193-blocks.json": "4049d066f71119fa72bbc37f7db753ce1e79ae5a69aef9cd2651d618bea5c855", + "scripts/moment.py": "0c7c68122cea18503e973ccf0d244adf8fa0edab95f104393528c6c57f24863a" + }, + "prerequisites": { + "pr202": { + "commit": "8d8d67bcf69c5ea67d3a29dbc64ba588156d6e8d", + "note": "the 308 files rebuilt by references/pr233-layer/verify.py: PR #184 flow/lift (icekylinx), PR #194 v4 scripts (ikeboy), PR #168 modules (eumemic), PR #200 checker (chafreaky)", + "repository": "CrocSwap/integer-mult-bounds" + }, + "pr225": { + "note": "scripts/moment.py: exact rational moment bounds (chafreaky; adapted from eumemic/exact-dft-bounds scripts/verify_moment.py, Apache-2.0)", + "path": "research/exact-dft-transfer/scripts/moment.py", + "pr": 225, + "repository": "CrocSwap/integer-mult-bounds" + }, + "pr233": { + "author": "chafreaky (Anthropic Claude and OpenAI Codex assistance); PR #202 baseline by ikeboy et al., see NOTICE", + "commit": "109a857", + "complex_saving": "3549537/5000000000", + "path": "research/source-assisted-v4-layer", + "pr": 233, + "repository": "CrocSwap/integer-mult-bounds", + "vendored": "references/pr233-layer (baseline-pr202.tar.gz, SOURCE.json, verify.py, certificate.json, NOTICE, witness/)" + }, + "sussman": { + "commit": "f010392c", + "files": { + "tools/certificate/gcert1-p11-pr193.json.gz": "15251deb0c11e0504d7b297c9786818888a93f08b92b03c6c122784b70488633 (its block histogram and counts in references/sussman/pr193-blocks.json)", + "tools/gx/gx.py": "6f3dc8bb639933227a8dae181ec4a542e85c7276be9c9e330f49518e7b630b95 (vendored unchanged as gx/gx.py)" + }, + "licence": "Apache-2.0, Copyright 2026 Jacob Sussman", + "repository": "jacobalansussman/wht-power-saving-lean" + } + } +} diff --git a/research/pr256-fourier-audit/inputs/gcert-program-233/certificate/expected.json b/research/pr256-fourier-audit/inputs/gcert-program-233/certificate/expected.json new file mode 100644 index 0000000000..88181f9c5e --- /dev/null +++ b/research/pr256-fourier-audit/inputs/gcert-program-233/certificate/expected.json @@ -0,0 +1,243 @@ +{ + "pr194": { + "N": 262944, + "R": 9412, + "blocks": { + "c": { + "20": 22 + }, + "s": { + "1": 23898, + "10": 930, + "11": 354, + "12": 1197, + "13": 127, + "14": 742, + "15": 1879, + "16": 88, + "17": 81, + "18": 13, + "19": 167, + "2": 11078, + "3": 9923, + "4": 4209, + "5": 1950, + "6": 1605, + "7": 706, + "8": 1531, + "9": 429 + }, + "x": { + "1": 1320, + "18": 1320, + "2": 1320 + }, + "y": { + "1": 3960, + "18": 1320 + } + }, + "blocks_total": 70169, + "certificate_sha256": "27398a0cfcbe34e5ee97360e69a2d163a417c8ae1b4fdf28ccf89a9eaf4e4cd4", + "cst": 440, + "distinct_frame_steps": 56301, + "five_stage": { + "W": 14692, + "child_histogram": { + "1": 145890, + "10": 4650, + "11": 1770, + "12": 5985, + "13": 635, + "14": 3710, + "15": 9395, + "16": 440, + "17": 405, + "18": 13265, + "19": 835, + "2": 61990, + "20": 110, + "21": 2640, + "3": 49615, + "4": 23685, + "42": 2640, + "46": 2640, + "5": 9750, + "6": 8025, + "7": 3530, + "8": 7655, + "9": 2145 + }, + "deficit": 3080, + "m": 110, + "rank": 1613040 + }, + "frames": 18248, + "gates_A": 13227, + "gates_B": 37997, + "registers": 12052, + "scalar_denominators": { + "s": 2, + "x": 2, + "y": 6 + }, + "scalar_max_abs": { + "s": "3", + "x": "3/2", + "y": "2" + } + }, + "pr233": { + "N": 262944, + "R": 9412, + "blocks": { + "c": { + "20": 22 + }, + "s": { + "1": 23898, + "10": 805, + "11": 353, + "12": 1141, + "13": 168, + "14": 725, + "15": 605, + "16": 81, + "17": 39, + "19": 1441, + "2": 11347, + "3": 9988, + "4": 3839, + "5": 1976, + "6": 1491, + "7": 642, + "8": 1478, + "9": 404 + }, + "x": { + "1": 1320, + "18": 1320, + "2": 1320 + }, + "y": { + "1": 3960, + "18": 1320 + } + }, + "blocks_total": 69683, + "certificate_sha256": "0c026244591a0b6737993aaac5fa8ac4a2bd27aa28e469f2567c698f57ed10a8", + "cst": 440, + "distinct_frame_steps": 56215, + "five_stage": { + "W": 14692, + "a": "7547/10^7", + "child_histogram": { + "1": 145890, + "10": 4025, + "11": 1765, + "12": 5705, + "13": 840, + "14": 3625, + "15": 3025, + "16": 405, + "17": 195, + "18": 13200, + "19": 7205, + "2": 63335, + "20": 110, + "21": 2640, + "3": 49940, + "4": 21835, + "42": 2640, + "46": 2640, + "5": 9880, + "6": 7455, + "7": 3210, + "8": 7390, + "9": 2020 + }, + "deficit": 3080, + "m": 110, + "margin_lower_bound": "1352651747270153812038110502/10^30", + "moment_upper_bound": "14691998647348252729846187961889498/10^30", + "next_grid_point": "7548/10^7", + "next_grid_point_rejected": true, + "rank": 1613040 + }, + "frames": 18248, + "gates_A": 13123, + "gates_B": 39177, + "registers": 12052, + "scalar_denominators": { + "s": 2, + "x": 2, + "y": 6 + }, + "scalar_max_abs": { + "s": "2", + "x": "3/2", + "y": "5/2" + } + }, + "prerequisites": { + "pr202": "8d8d67bcf69c5ea67d3a29dbc64ba588156d6e8d", + "pr233": { + "author": "chafreaky (Anthropic Claude and OpenAI Codex assistance); PR #202 baseline by ikeboy et al., see NOTICE", + "commit": "109a857", + "complex_saving": "3549537/5000000000", + "path": "research/source-assisted-v4-layer", + "pr": 233, + "repository": "CrocSwap/integer-mult-bounds", + "vendored": "references/pr233-layer (baseline-pr202.tar.gz, SOURCE.json, verify.py, certificate.json, NOTICE, witness/)" + }, + "sussman": { + "commit": "f010392c", + "files": { + "tools/certificate/gcert1-p11-pr193.json.gz": "15251deb0c11e0504d7b297c9786818888a93f08b92b03c6c122784b70488633 (its block histogram and counts in references/sussman/pr193-blocks.json)", + "tools/gx/gx.py": "6f3dc8bb639933227a8dae181ec4a542e85c7276be9c9e330f49518e7b630b95 (vendored unchanged as gx/gx.py)" + }, + "licence": "Apache-2.0, Copyright 2026 Jacob Sussman", + "repository": "jacobalansussman/wht-power-saving-lean" + } + }, + "status": "PASS: both flow words exported as gcert/1 programs accepted by gx.check1; PR #233 word priced at 7547/10^7 in the five-stage layout", + "sussman_pr193": { + "N": 262944, + "blocks": { + "c": { + "20": 22 + }, + "s": { + "1": 23898, + "10": 930, + "11": 354, + "12": 1197, + "13": 127, + "14": 742, + "15": 1879, + "16": 88, + "17": 81, + "18": 13, + "19": 167, + "2": 11078, + "3": 9923, + "4": 4209, + "5": 1950, + "6": 1605, + "7": 706, + "8": 1531, + "9": 429 + }, + "x": { + "1": 1320, + "18": 1320, + "2": 1320 + }, + "y": { + "1": 3960, + "18": 1320 + } + }, + "file_sha256": "15251deb0c11e0504d7b297c9786818888a93f08b92b03c6c122784b70488633" + } +} diff --git a/research/pr256-fourier-audit/inputs/gcert-program-233/certificates/gcert1-p11-pr233-flow.json.gz b/research/pr256-fourier-audit/inputs/gcert-program-233/certificates/gcert1-p11-pr233-flow.json.gz new file mode 100644 index 0000000000..d4026e4cbd Binary files /dev/null and b/research/pr256-fourier-audit/inputs/gcert-program-233/certificates/gcert1-p11-pr233-flow.json.gz differ diff --git a/research/pr256-fourier-audit/inputs/gcert-program-233/gx/gx.py b/research/pr256-fourier-audit/inputs/gcert-program-233/gx/gx.py new file mode 100644 index 0000000000..6d14c0a976 --- /dev/null +++ b/research/pr256-fourier-audit/inputs/gcert-program-233/gx/gx.py @@ -0,0 +1,296 @@ +#!/usr/bin/python3 -I +"""gx.py. OWN code (imports nothing of port-producer, nothing outside). +(1) convert(c0): gcert/0 (port-producer's event list) -> gcert/1, the LEAN-FACING NORMAL FORM: + only the main phase (no read0 / undo / uninj: the invocation theorem derives the dirt gate and the undo + gate from the product), every gate an elementary fan-out or fan-in add, the 4x4 K block written as three + such adds plus a sign carried by one register, the star scatter as a table. +(2) check1(c1): the local decidable conditions of EXTENDED-CERT-SPEC.md on a gcert/1 file: + E0 sizes, E1 labels (nested subspaces by containment, equal frame at a gate), E2 scatter cut, + E3 shape (kinds of gates; X1; S1), E4 bracket rule S2, E5 scalar (x-content replay: hid and X3), + E6 price data (block histograms, N), E7 exterior gauges only (Q2). Raises AssertionError(": ..."). +""" +from fractions import Fraction as Fr +from collections import Counter +from math import lcm + + +def need(c, msg): + if not c: + raise AssertionError(msg) + + +def reduce(u, basis): + """basis: reduced echelon, pivot = leading bit, descending. Returns u modulo the span.""" + for b in basis: + if u >> (b.bit_length() - 1) & 1: + u ^= b + return u + + +def echelon_ok(f): + piv = [b.bit_length() - 1 for b in f] + if any(b == 0 for b in f) or piv != sorted(piv, reverse=True) or len(set(piv)) != len(piv): + return False + return all(not (b >> p & 1) for i, b in enumerate(f) for j, p in enumerate(piv) if i != j) + + +def inside(a, b): + return all(reduce(u, b) == 0 for u in a) + + +def par(x): + return bin(x).count("1") & 1 + + +KJ = [[[1, 2] if i == j else [-1, 2] for j in range(4)] for i in range(4)] + + +def convert(c0): + need(c0["format"] == "gcert/0", "input is not gcert/0") + v, h, R = c0["v"], c0["h"], c0["R"] + ev = c0["events"] + cen = [n for n, e in enumerate(ev) if e[0] == "centre"] + need(cen == list(range(cen[0], cen[0] + len(cen))), "centres are not contiguous: no single scatter cut") + A, B, ret = [], [], [] + neg = set() # x registers currently holding MINUS their value (between the two K blocks) + openq = {} + for n, e in enumerate(ev): + k = e[0] + out = A if n < cen[0] else B + if k in ("read0", "undo", "uninj"): + continue + if k == "inj": + need(e[2] not in neg, "inj reads a negated x register") + out.append(["out", e[3], e[2], [[e[1], 1, 1]], []]) + elif k == "op": + if e[3] == -1: + out.append(["neg", e[5], e[1]]) + else: + need(e[3] == 1, "op ca") + out.append(["out", e[5], e[2], [[e[1], e[4], 1]], []]) + elif k == "centre": + ret.append([e[2], e[1], e[3]]) + elif k == "gread": + hit = set(t for t, _, _ in e[3]) + out.append(["out", e[2], e[1], [[v + t, a, b] for t, a, b in e[3]], [v + t for t in e[4] if t not in hit]]) + elif k == "rread": + out.append(["out", e[2], e[1], [[v + t, a, b] for t, a, b in e[3]], []]) + elif k == "ysh": + out.append(["out", e[4], e[2], [[e[1], e[3], 1]], []]) + elif k == "yw": + out.append(["out", e[4], e[2], [[e[1], e[3][0], e[3][1]]], []]) + elif k == "kd": + out.append(["out", e[3], e[2], [[e[1], -1 if e[2] in neg else 1, 1]], []]) + elif k == "ktr": + q = tuple(e[1]) + need(e[2] == KJ, "ktr matrix is not 1 - J/2") + x1, rest = q[0], list(q[1:]) + if q not in openq: # first block: x := M x, register x1 keeps the sign + out.append(["in", e[3], x1, [[r, 1, 1] for r in rest]]) + out.append(["out", e[3], x1, [[r, -1, 2] for r in rest], []]) + out.append(["in", e[3], x1, [[r, 1, 1] for r in rest]]) + openq[q] = n + neg.add(x1) + else: # second block: the three adds undone in reverse order + out.append(["in", e[3], x1, [[r, -1, 1] for r in rest]]) + out.append(["out", e[3], x1, [[r, 1, 2] for r in rest], []]) + out.append(["in", e[3], x1, [[r, -1, 1] for r in rest]]) + del openq[q] + neg.discard(x1) + else: + raise AssertionError("unknown event kind %r" % k) + need(not openq and not neg, "a K block is not closed") + ext = sorted([z[3], z[1]] for z in c0["gauge"] if z[5]) + c1 = dict(format="gcert/1", derived_from=c0["name"] + " (gcert/0)", p=c0["p"], h=h, v=v, R=R, cst=c0["cst"], + N=c0["N"], ports=c0["ports"], frames=c0["frames"], start=c0["start"], final=c0["final"], + ext=ext, ret=sorted(ret), scat=dict(inside=c0["scat"]["inside"], outside=c0["scat"]["outside"]), + A=A, B=B, blocks=c0["blocks"]) + return c1 + + +def scat_row(c, t): + """the scatter of target t: [(k, coefficient)], from the table or from the star rule""" + sc = c["scat"] + if "table" in sc: + return [(k, Fr(a, b)) for k, a, b in sc["table"][t]] + sin, sout = Fr(*sc["inside"]), Fr(*sc["outside"]) + return [(k, sin if c["ports"][t] >> k & 1 else sout) for k in range(c["h"])] + + +def gate_regs(g): + if g[0] == "neg": + return [g[2]], [], [] + if g[0] == "out": + return [g[2]] + [t for t, _, _ in g[3]] + list(g[4]), [(t, g[2], Fr(a, b)) for t, a, b in g[3]], g[4] + if g[0] == "in": + return [g[2]] + [s for s, _, _ in g[3]], [(g[2], s, Fr(a, b)) for s, a, b in g[3]], [] + raise AssertionError("E0: unknown gate kind %r" % (g[0],)) + + +def check1(c, scalar=True, stats=None): + need(c.get("format") == "gcert/1", "E0: format") + h, v, R = c["h"], c["v"], c["R"] + nreg = 2 * v + R + ports, fr = c["ports"], [tuple(f) for f in c["frames"]] + need(len(ports) == v == len(set(ports)) and all(par(q) and 0 < q < 1 << h for q in ports), "E0: ports") + need(fr[0] == () and fr[1] == tuple(1 << i for i in range(h - 1, -1, -1)), "E0: frames 0 and 1") + need(all(echelon_ok(f) for f in fr) and len(set(fr)) == len(fr), "E0: frame table not reduced echelon / repeats") + dim = [len(f) for f in fr] + start, final = c["start"], c["final"] + need(len(start) == len(final) == nreg, "E0: start / final") + ext = {r: f for r, f in c["ext"]} + for t in range(v): + need(fr[start[t]] == (ports[t],) and final[t] == 1, "E1: x start / final") + f = fr[final[v + t]] + need(start[v + t] == 0 and len(f) == h - 1 and all(par(u & ports[t]) == 0 for u in f), "E1: y start / final") + for r in range(2 * v, nreg): + need(start[r] == ext.get(r, 0) and final[r] == 1, "E1: slot start / final") + cls = lambda r: "x" if r < v else "y" if r < 2 * v else "s" + cur = list(start) + H = {"x": Counter(), "y": Counter(), "s": Counter(), "c": Counter()} + steps = set() + + def climb(r, f, where): + o = cur[r] + if o != f: + if (o, f) not in steps: + need(dim[o] < dim[f] and inside(fr[o], fr[f]), "E1: step not nested (%s, register %d)" % (where, r)) + steps.add((o, f)) + H[cls(r)][dim[f] - dim[o]] += 1 + cur[r] = f + okind = {("x", "s"), ("s", "s"), ("s", "y"), ("x", "y"), ("x", "x"), ("y", "y")} + ysum, piv, ytg = Counter(), set(), set() + inc = 0 + for ph, gates in (("A", c["A"]), ("B", c["B"])): + if ph == "B": # ---- E2: the scatter cut + need(sorted(k for k, _, _ in c["ret"]) == list(range(len(c["ret"]))), "E2: retained totals numbered 0..") + if "table" in c["scat"]: + need(len(c["scat"]["table"]) == v and all(0 <= k < len(c["ret"]) for row in c["scat"]["table"] for k, _, _ in row), + "E2: scatter table") + else: + need(len(c["ret"]) == h, "E2: one retained total per coordinate (star rule)") + for k, s, f in c["ret"]: + need(cls(s) == "s" and cur[s] == f, "E2: retained slot %d is not at its frame" % s) + H["c"][dim[f]] += 1 + need(all(cur[v + t] == 0 for t in range(v)), "E2: a y role left frame 0 before the scatter") + for i, g in enumerate(gates): + regs, pairs, _ = gate_regs(g) + need(all(0 <= r < nreg for r in regs) and len(set(regs)) == len(regs), "E3: registers of gate %s%d" % (ph, i)) + inc += len(regs) + for r in regs: + climb(r, g[1], "%s%d" % (ph, i)) + for t, s, co in pairs: + kd = (cls(s), cls(t)) + need(kd in okind, "E3: gate kind %s -> %s (gate %s%d)" % (kd + (ph, i))) + need(ph == "B" or kd in {("x", "s"), ("s", "s")}, "E3: bank gate before the scatter (gate A%d)" % i) + if kd == ("y", "y"): + ysum[s, t] += co + piv.add(s) + ytg.add(t) + need(ph == "B" or all(cls(r) != "y" for r in regs), "E2: y role named in phase A") + for r in range(nreg): + climb(r, final[r], "final") + need(not (piv & ytg), "E4: a pivot is the target of a gate reading y") + need(all(x == 0 for x in ysum.values()), "E4: y-reads of a (pivot, target) pair do not cancel") + Hs = {k: {str(r): n for r, n in sorted(w.items())} for k, w in H.items()} + need(Hs == c["blocks"], "E6: block histograms") + N = sum(r * n for w in H.values() for r, n in w.items()) + tails = sum(dim[f] for f in ext.values()) + need(N == c["N"] and N + tails == R * h + 2 * v * (h - 1) + c["cst"], "E6: N") + if stats is not None: + stats.update(steps=len(steps), incidences=inc, blocks=sum(sum(w.values()) for w in H.values()), + step_work=sum(dim[a] * dim[b] for a, b in steps), ysh_pairs=len(ysum)) + if scalar: + scal(c, stats) + q2(c) + return True + + +def scal(c, stats=None): + """E5: exact replay of the x-content of every register through A, scatter, B.""" + h, v, R = c["h"], c["v"], c["R"] + nreg = 2 * v + R + reg = [({r: Fr(1)} if r < v else {}) for r in range(nreg)] + den = {"x": 1, "y": 1, "s": 1} + mx = {"x": Fr(0), "y": Fr(0), "s": Fr(0)} + cls = lambda r: "x" if r < v else "y" if r < 2 * v else "s" + + def axpy(t, src, co): + d = reg[t] + for k, u in src.items(): + w = d.get(k, 0) + co * u + if w: + d[k] = w + kk = cls(t) + if w.denominator != 1: + den[kk] = lcm(den[kk], w.denominator) + if abs(w) > mx[kk]: + mx[kk] = abs(w) + else: + d.pop(k, None) + + def run(gates): + for g in gates: + if g[0] == "neg": + reg[g[2]] = {k: -u for k, u in reg[g[2]].items()} + elif g[0] == "out": + src = dict(reg[g[2]]) + for t, a, b in g[3]: + axpy(t, src, Fr(a, b)) + else: + for s, a, b in g[3]: + axpy(g[2], reg[s], Fr(a, b)) + run(c["A"]) + tot = {k: dict(reg[s]) for k, s, _ in c["ret"]} + for t in range(v): + for k, co in scat_row(c, t): + axpy(v + t, tot[k], co) + run(c["B"]) + need(all(reg[t] == {t: 1} for t in range(v)), "E5: an x role is not restored (X3)") + need(all(reg[v + t] == {t: 1} for t in range(v)), "E5: a target does not receive exactly its source (hid)") + if stats is not None: + stats.update(den=dict(den), maxabs={k: str(x) for k, x in mx.items()}, + gates_A=len(c["A"]), gates_B=len(c["B"])) + + +def q2(c): + """E7 (only for files with exterior gauges, rule (2)): for every slot q that starts off the zero frame, the + column of q in the y rows of the product is zero (its dirt is removed in line, the derived dirt gate at + frame 0 does not touch it). Replay with the gauged slots as variables, x = 0.""" + h, v, R = c["h"], c["v"], c["R"] + ext = [r for r, _ in c["ext"]] + if not ext: + return True + reg = [dict() for _ in range(2 * v + R)] + for r in ext: + reg[r] = {r: Fr(1)} + + def axpy(t, src, co): + d = reg[t] + for k, u in src.items(): + w = d.get(k, 0) + co * u + if w: + d[k] = w + else: + d.pop(k, None) + + def run(gates): + for g in gates: + if g[0] == "neg": + reg[g[2]] = {k: -u for k, u in reg[g[2]].items()} + elif g[0] == "out": + src = dict(reg[g[2]]) + for t, a, b in g[3]: + axpy(t, src, Fr(a, b)) + else: + for s, a, b in g[3]: + axpy(g[2], reg[s], Fr(a, b)) + run(c["A"]) + tot = {k: dict(reg[s]) for k, s, _ in c["ret"]} + for t in range(v): + for k, co in scat_row(c, t): + if tot[k]: + axpy(v + t, tot[k], co) + run(c["B"]) + need(all(not reg[v + t] for t in range(v)), "E7: the dirt of an exterior-gauged slot reaches a y role (Q2)") + return True diff --git a/research/pr256-fourier-audit/network_contract.py b/research/pr256-fourier-audit/network_contract.py new file mode 100644 index 0000000000..d8cfa5d902 --- /dev/null +++ b/research/pr256-fourier-audit/network_contract.py @@ -0,0 +1,33 @@ +"""Reusable exact arithmetic for finite tensor-network certificates. + +The histogram is an input, not a proof of a realizable network. The written +network contract must separately establish its physical and algorithmic meaning. +""" +from fractions import Fraction as Q +from math import factorial +from rational_bounds import log_bounds + + +def moment_bounds(hist, m, roles, saving): + """Enclose sum n_r (r/m)^(1-saving) / roles using rational arithmetic.""" + if not 0 < saving < 1 or roles <= 0 or m < 2 or not hist: + raise ValueError('invalid network parameters') + lower = upper = Q(0) + grid = 10**60 + for width, count in hist.items(): + if not 0 < width < m or count <= 0: + raise ValueError('children must have positive counts and smaller widths') + lo, hi = log_bounds(Q(m, width)) + lo = Q(lo.numerator * grid // lo.denominator, grid) + hi = Q((hi.numerator * grid + hi.denominator - 1) // hi.denominator, grid) + x, y = saving * lo, saving * hi + if not 0 <= y < 3: + raise ValueError('exponential bound outside its domain') + # Positive Taylor terms give a lower bound; the successive tail ratios + # from the quadratic term onward are at most y/3. + el = sum(x**j / factorial(j) for j in range(7)) + eu = 1 + y + y*y / (2 * (1 - y/3)) + weight = Q(count) * Q(width, m) / roles + lower += weight * el + upper += weight * eu + return lower, upper diff --git a/research/pr256-fourier-audit/rational_bounds.py b/research/pr256-fourier-audit/rational_bounds.py new file mode 100644 index 0000000000..38d72ac976 --- /dev/null +++ b/research/pr256-fourier-audit/rational_bounds.py @@ -0,0 +1,52 @@ +"""Exact rational bounds used by the Fourier extension verifier. + +These helpers enclose logarithms and derived exponent savings with rational +arithmetic. Decimal formatting is for display only. Network counts and proof +obligations are supplied and checked by verify_extension.py. +""" +from __future__ import annotations +from decimal import Decimal, localcontext +from fractions import Fraction as F + +def series_bounds(y: F, terms: int) -> tuple[F, F]: + """Rigorous natural-log enclosure for rational 1 <= y <= 2.""" + if not (1 <= y <= 2) or terms < 1: + raise ValueError('series requires 1 <= y <= 2 and terms >= 1') + z = (y-1)/(y+1) + z2 = z*z + t, s = z, F(0) + for j in range(terms): + s += t/(2*j+1) + t *= z2 + lo = 2*s + tail = 2*t/((2*terms+1)*(1-z2)) + return lo, lo+tail + +def log_bounds(x: F) -> tuple[F, F]: + """Range reduction plus exact atanh series; x is rational and >= 1.""" + if x < 1: + raise ValueError('x must be >= 1') + y, k = x, 0 + while y > 2: + y /= 2 + k += 1 + t = 6 if y < F(1001,1000) else 40 + lo, hi = series_bounds(y, t) + l2, u2 = series_bounds(F(2), 40) + return lo+k*l2, hi+k*u2 + +def saving_bounds(c: dict) -> tuple[F, F]: + eta = c['eta'] + if not (0 < eta < 1): + raise ValueError('positive contraction required') + nl, nu = log_bounds(1/(1-eta)) + dl, du = log_bounds(F(c['m'])) + return nl/du, nu/dl + +def decimal(x: F, precision: int = 36) -> str: + with localcontext() as ctx: + ctx.prec = precision + return str(Decimal(x.numerator)/Decimal(x.denominator)) + +def frac_json(x: F) -> dict: + return {'numerator': str(x.numerator), 'denominator': str(x.denominator)} diff --git a/research/pr256-fourier-audit/reproduce_lean.py b/research/pr256-fourier-audit/reproduce_lean.py new file mode 100644 index 0000000000..ae24620e7d --- /dev/null +++ b/research/pr256-fourier-audit/reproduce_lean.py @@ -0,0 +1,145 @@ +#!/usr/bin/env python3 +"""Reproduce the pinned upstream Lean proof and its statement/axiom comparisons. + +Requires the pinned Lean toolchain on PATH (or --lake). Downloads pinned +Mathlib dependencies/cache unless --cache-ready is set. Extracts the vendored +source archive into --work-dir, or checks every source byte if it already exists. +Does not run the official Linux comparator, an independent kernel, or the DFT. +""" +import argparse +from datetime import datetime, timezone +import hashlib +import json +import os +from pathlib import Path +import platform +import re +import shutil +import subprocess +import sys +import tarfile +import time + +from verify import BASE, VENDOR, require, source_check + + +def prepare(work, archive_path): + work.mkdir(parents=True, exist_ok=True) + with tarfile.open(archive_path) as archive: + members = [m for m in archive.getmembers() if m.isfile()] + hashes = {} + for member in members: + relative = Path(member.name) + require(not relative.is_absolute() and '..' not in relative.parts, + 'unsafe source archive path') + data = archive.extractfile(member).read() + path = work / relative + require(path.resolve().is_relative_to(work.resolve()), 'source path leaves work directory') + if path.exists(): + require(path.read_bytes() == data, 'existing source differs: '+member.name) + else: + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(data) + path.chmod(member.mode & 0o777) + hashes[member.name] = hashlib.sha256(data).hexdigest() + return hashes + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--work-dir', type=Path, required=True) + parser.add_argument('--lake', default='lake') + parser.add_argument('--cache-ready', action='store_true') + parser.add_argument('--threads', type=int, default=2) + parser.add_argument('--receipt', type=Path, default=Path('/tmp/pr256-fourier-audit/lean-receipt.json')) + args = parser.parse_args() + require(args.threads > 0, 'threads must be positive') + source = source_check() + work = args.work_dir.resolve() + hashes = prepare(work, VENDOR/source['fourier_proof']['archive']) + lake = shutil.which(args.lake) + require(lake is not None, 'Lake not found; install leanprover/lean4:v4.34.1 first') + env = dict(os.environ) + env['PATH'] = str(Path(lake).resolve().parent) + os.pathsep + env.get('PATH', '') + env['LEAN_NUM_THREADS'] = str(args.threads) + log_dir = args.receipt.resolve().parent / 'five_stage_lean_logs' + log_dir.mkdir(parents=True, exist_ok=True) + commands = [] + started = datetime.now(timezone.utc).isoformat() + fresh = not (work/'.lake/build/lib/lean/Work').exists() + + def run(label, command): + print('Running '+label+' ...', flush=True) + t0 = time.monotonic() + log_path = log_dir/(label+'.log') + with log_path.open('w') as log: + p = subprocess.run(command, cwd=work, env=env, stdout=log, stderr=subprocess.STDOUT) + output = log_path.read_text() + commands.append({'label': label, 'command': command, 'exit_code': p.returncode, + 'seconds': round(time.monotonic()-t0, 3), + 'log_sha256': hashlib.sha256(log_path.read_bytes()).hexdigest()}) + if p.returncode: + print(output[-6000:]) + raise SystemExit('FAILED '+label+'; log: '+str(log_path)) + print('PASS '+label, flush=True) + return output + + version = run('toolchain', [lake, '--version']).strip() + require('Lean version 4.34.1' in version, 'incorrect Lean toolchain') + if not args.cache_ready: + run('mathlib_cache', [lake, 'exe', 'cache', 'get']) + mathlib = subprocess.check_output(['git', 'rev-parse', 'HEAD'], cwd=work/'.lake/packages/mathlib', text=True).strip() + require(mathlib == source['fourier_proof']['mathlib_commit'], 'Mathlib revision differs') + generated = run('regenerate_certificate', [sys.executable, '-B', 'tools/gx/regen_check.py', + 'tools/certificate/gcert1-p11-pr233-flow.json.gz', 'P233', 'B2Gp233']) + require('41 repository files reproduced byte for byte, 0 different, 0 generated files not in the repository' in generated, + 'Lean certificate generation differs') + transfer = run('regenerate_fourier', [sys.executable, '-B', 'tools/fourier/regen_check233.py']) + require('14 repository files reproduced byte for byte, 0 different, 0 generated files not in the repository' in transfer, + 'Fourier generation differs') + # Each scalar reduction can use several GB. Keep these two independent + # kernel checks sequential, even when other compilation uses two workers. + run('build_scalar0', [lake, 'build', 'Work.GCert.Data.Gen.P233Scal0']) + run('build_scalar1', [lake, 'build', 'Work.GCert.Data.Gen.P233Scal1']) + targets = ['Work.GCert.Data.ChallengeB2Gp233x', 'Work.GCert.Data.SolutionB2Gp233x', + 'Work.Fourier233.UniformFourierChallenge', 'Work.Fourier233.Main', 'Work.Fourier233.Axioms'] + build = run('build', [lake, 'build', *targets]) + axioms = run('axioms', [lake, 'env', 'lean', 'Work/Fourier233/Axioms.lean']) + allowed = {'propext', 'Classical.choice', 'Quot.sound'} + required = ['OAI.PowerSaving.transform_mainY', 'OAI.PowerSaving.convolution_mainY', + 'OAI.PowerSaving.RAM.hillsY_program'] + found = {} + for name in required: + match = re.search(re.escape("'"+name+"' depends on axioms: ")+r'\[([^]]*)\]', axioms) + require(match is not None, 'missing axiom report: '+name) + values = {v.strip() for v in match.group(1).split(',')} + require(values == allowed, 'unexpected axioms: '+name) + found[name] = sorted(values) + comparisons = [ + ('compare_wht', ['Work.GCert.Data.ChallengeB2Gp233x', 'Work.GCert.Data.SolutionB2Gp233x', + 'OAI.PowerSaving.WHT.wht_main_block_B2Gp233x']), + ('compare_fourier', ['Work.Fourier233.UniformFourierChallenge', 'Work.Fourier233.Main', + 'OAI.PowerSaving.transform_mainY', 'OAI.PowerSaving.convolution_mainY'])] + for label, names in comparisons: + output = run(label, [lake, 'env', 'lean', '--run', 'tools/Compare.lean', *names]) + require('RESULT: PASS' in output, 'missing successful statement comparison') + for path, digest in hashes.items(): + require(hashlib.sha256((work/path).read_bytes()).hexdigest() == digest, 'source changed during build: '+path) + receipt = {'schema': 1, 'started_utc': started, 'finished_utc': datetime.now(timezone.utc).isoformat(), + 'source_commit': source['fourier_proof']['commit'], 'source_archive_sha256': + source['files'][source['fourier_proof']['archive']], + 'source_files_checked': len(hashes), 'fresh_project_build': fresh, + 'mathlib_commit': mathlib, 'mathlib_from_cache': True, + 'toolchain': version, 'platform': platform.platform(), 'machine': platform.machine(), + 'threads': args.threads, 'commands': commands, 'axioms': found, + 'statement_comparison': 'upstream tools/Compare.lean; WHT, all-length DFT and convolution passed', + 'official_comparator_run': False, 'independent_kernel_run': False, + 'numerical_dft_executed': False, 'independent_human_review': False, + 'success': True} + args.receipt.parent.mkdir(parents=True, exist_ok=True) + args.receipt.write_text(json.dumps(receipt, indent=2, sort_keys=True)+'\n') + print('PASS: pinned Lean build, standard axioms and theorem/definition comparisons; receipt '+str(args.receipt)) + + +if __name__ == '__main__': + main() diff --git a/research/pr256-fourier-audit/test_audit.py b/research/pr256-fourier-audit/test_audit.py new file mode 100644 index 0000000000..c70a508992 --- /dev/null +++ b/research/pr256-fourier-audit/test_audit.py @@ -0,0 +1,103 @@ +#!/usr/bin/env python3 +"""Mutation controls on the real pinned program, statements and build evidence.""" +import copy +import gzip +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tarfile +import tempfile +import unittest +from unittest.mock import patch + +import verify + + +class AuditControls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.source = verify.source_check() + cls.program = json.loads(gzip.decompress( + (verify.PACKAGE/'certificates/gcert1-p11-pr233-flow.json.gz').read_bytes())) + with tarfile.open(verify.VENDOR/'fourier-proof-source.tar.gz') as archive: + cls.lean_program = json.loads(gzip.decompress(archive.extractfile( + 'tools/certificate/gcert1-p11-pr233-flow.json.gz').read())) + cls.original = archive.extractfile( + 'third-party/openai-math/lean/ComparatorChallenges/UniformFourier.lean').read().decode() + cls.challenge = archive.extractfile( + 'Work/Fourier233/UniformFourierChallenge.lean').read().decode() + + def test_provenance_text_is_not_mathematical_data(self): + self.assertNotEqual(self.program['derived_from'], self.lean_program['derived_from']) + verify.compare_programs(self.program, self.lean_program) + + def test_changed_register_stock_rejects(self): + candidate = dict(self.program, R=self.program['R']-1) + with self.assertRaisesRegex(ValueError, 'Lean input program differs'): + verify.compare_programs(candidate, self.lean_program) + + def test_changed_child_count_rejects(self): + candidate = copy.deepcopy(self.program) + counts = next(iter(candidate['blocks'].values())) + counts[next(iter(counts))] += 1 + with self.assertRaisesRegex(ValueError, 'Lean input program differs'): + verify.compare_programs(candidate, self.lean_program) + + def test_original_challenge_matches(self): + verify.compare_challenges(self.original, self.challenge) + + def test_unrecorded_exponent_rejects(self): + candidate = self.challenge.replace('7547360', '7547362') + self.assertNotEqual(candidate, self.challenge) + with self.assertRaisesRegex(ValueError, 'challenge differs'): + verify.compare_challenges(self.original, candidate) + + def test_weakened_statement_rejects(self): + candidate = self.challenge.replace('∀', '∃', 1) + self.assertNotEqual(candidate, self.challenge) + with self.assertRaisesRegex(ValueError, 'challenge differs'): + verify.compare_challenges(self.original, candidate) + + def check_bad_receipt(self, change, message): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + shutil.copytree(verify.BASE/'evidence', root/'evidence') + path = root/'evidence/five_stage_lean_receipt.json' + receipt = json.loads(path.read_text()) + change(receipt) + path.write_text(json.dumps(receipt)) + with patch.object(verify, 'BASE', root): + with self.assertRaisesRegex(ValueError, message): + verify.check_evidence(self.source) + + def test_extra_axiom_rejects(self): + self.check_bad_receipt(lambda r: r['axioms']['OAI.PowerSaving.transform_mainY'].append('sorryAx'), + 'unexpected recorded axioms') + + def test_missing_build_rejects(self): + self.check_bad_receipt(lambda r: r.update(commands=[c for c in r['commands'] if c['label'] != 'build']), + 'recorded commands differ') + + def test_wrong_source_revision_rejects(self): + self.check_bad_receipt(lambda r: r.update(source_commit='0'*40), 'receipt source differs') + + def test_changed_log_rejects(self): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + shutil.copytree(verify.BASE/'evidence', root/'evidence') + (root/'evidence/logs/build.log.gz').write_bytes(gzip.compress(b'Build completed', mtime=0)) + with patch.object(verify, 'BASE', root): + with self.assertRaisesRegex(ValueError, 'recorded log differs: build'): + verify.check_evidence(self.source) + + def test_optimized_mode_refused(self): + result = subprocess.run([sys.executable, '-B', '-O', str(verify.BASE/'verify.py')], + capture_output=True, text=True) + self.assertNotEqual(result.returncode, 0) + self.assertIn('Run without -O', result.stderr) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/pr256-fourier-audit/verify.py b/research/pr256-fourier-audit/verify.py new file mode 100644 index 0000000000..c0c9846253 --- /dev/null +++ b/research/pr256-fourier-audit/verify.py @@ -0,0 +1,250 @@ +#!/usr/bin/env python3 +"""Check the pinned PR256 program, five-stage ledger and exact Fourier margin. + +Standard library only. This is a finite check, not a Lean build. The separate +reproduce_lean.py reproduces the upstream formal proof. No multiplication +exponent is claimed by this audit. +""" +import argparse +import ast +from collections import Counter +from fractions import Fraction as Q +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import re +import sys +import tarfile + +from network_contract import moment_bounds + +BASE = Path(__file__).resolve().parent +VENDOR = BASE / 'inputs' +PACKAGE = VENDOR / 'gcert-program-233' +REFERENCE = BASE / 'expected.json' +A = Q(7547361, 10**10) +DELTA = Q(7547360, 10**10) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def source_check(): + manifest = json.loads((BASE / 'MANIFEST.json').read_text()) + for path, digest in manifest['files'].items(): + require(hashlib.sha256((BASE / path).read_bytes()).hexdigest() == digest, + 'audit input hash mismatch: ' + path) + source = json.loads((VENDOR / 'SOURCE.json').read_text()) + for path, digest in source['files'].items(): + require(hashlib.sha256((VENDOR / path).read_bytes()).hexdigest() == digest, + 'source hash mismatch: ' + path) + return source + + +def compare_programs(program, lean_program): + left, right = dict(program), dict(lean_program) + # This is the only descriptive field excluded; every mathematical field agrees. + left.pop('derived_from'); right.pop('derived_from') + require(left == right, 'Lean input program differs') + + +def check_evidence(source): + evidence = BASE / 'evidence' + receipt = json.loads((evidence / 'five_stage_lean_receipt.json').read_text()) + require(receipt['success'] is True and receipt['fresh_project_build'] is True, + 'successful fresh Lean reproduction not recorded') + require(receipt['source_commit'] == source['fourier_proof']['commit'], 'receipt source differs') + require(receipt['source_archive_sha256'] == source['files']['fourier-proof-source.tar.gz'], + 'receipt archive differs') + require(receipt['mathlib_commit'] == source['fourier_proof']['mathlib_commit'], 'receipt Mathlib differs') + require('Lean version 4.34.1' in receipt['toolchain'], 'receipt toolchain differs') + allowed = {'propext', 'Classical.choice', 'Quot.sound'} + required = {'OAI.PowerSaving.transform_mainY', 'OAI.PowerSaving.convolution_mainY', + 'OAI.PowerSaving.RAM.hillsY_program'} + require(set(receipt['axioms']) == required, 'receipt theorem set differs') + for name, axioms in receipt['axioms'].items(): + require(set(axioms) == allowed, 'unexpected recorded axioms: ' + name) + commands = receipt['commands'] + require({c['label'] for c in commands} == {'toolchain', 'regenerate_certificate', + 'regenerate_fourier', 'build', 'axioms', 'compare_wht', 'compare_fourier'}, + 'recorded commands differ') + for command in commands: + label = command['label'] + require(command['exit_code'] == 0, 'recorded command failed: ' + label) + data = gzip.decompress((evidence / 'logs' / (label + '.log.gz')).read_bytes()) + require(hashlib.sha256(data).hexdigest() == command['log_sha256'], 'recorded log differs: ' + label) + if label.startswith('compare_'): + require(b'RESULT: PASS' in data, 'recorded comparison did not pass') + if label == 'axioms': + output = data.decode() + for name in required: + match = re.search(re.escape("'"+name+"' depends on axioms: ")+r'\[([^]]*)\]', output) + require(match is not None, 'missing theorem in axiom log: ' + name) + require({a.strip() for a in match.group(1).split(',')} == allowed, + 'unexpected axioms in log: ' + name) + for key in ['official_comparator_run', 'independent_kernel_run', 'independent_human_review', + 'numerical_dft_executed']: + require(receipt[key] is False, 'historical reproduction scope differs: ' + key) + regeneration = json.loads((evidence / 'five_stage_regeneration_receipt.json').read_text()) + require(regeneration['success'] is True and regeneration['exit_code'] == 0, + 'program regeneration did not pass') + require(regeneration['source_commit'] == source['commit'], 'regeneration source differs') + data = gzip.decompress((evidence / 'logs/regenerate_program.log.gz').read_bytes()) + require(hashlib.sha256(data).hexdigest() == regeneration['log_sha256'], 'regeneration log differs') + with tarfile.open(VENDOR / 'fourier-proof-source.tar.gz') as archive: + hashes = {m.name: hashlib.sha256(archive.extractfile(m).read()).hexdigest() + for m in archive.getmembers() if m.isfile()} + require(hashes == json.loads((evidence / 'proof_source_files.json').read_text()), + 'full proof source ledger differs') + require(len(hashes) == receipt['source_files_checked'] == 456, 'proof source count differs') + return hashes + + +def check_checkout(root, hashes, label): + for path, digest in hashes.items(): + require(hashlib.sha256((root / path).read_bytes()).hexdigest() == digest, + label + ' source differs: ' + path) + print('PASS: %d pinned %s source files.' % (len(hashes), label)) + + +def strip_lean_comments(text): + # The two fixed challenge files use non-nested block comments. + text = re.sub(r'/-.*?-/', '', text, flags=re.S) + return ''.join(re.sub(r'--[^\n]*', '', text).split()) + + +def compare_challenges(original, challenge): + for name in ('decimalExponent', 'decimalTime', 'TimeBounds', 'DFTGoal', 'ConvGoal', + 'transform_main', 'convolution_main'): + challenge = challenge.replace(name+'Y', name) + challenge = challenge.replace('1 - 7547360/(10^(10:ℕ))', '1 - 1/(10^(13:ℕ))') + require(strip_lean_comments(original) == strip_lean_comments(challenge), + 'challenge differs beyond comments, names and exponent') + + +def rounded_down(q): + grid = 10**30 + return str(Q(q.numerator * grid // q.denominator, grid)) + + +def verify(): + source = source_check() + spec = importlib.util.spec_from_file_location('five_stage_gx', PACKAGE / 'gx/gx.py') + gx = importlib.util.module_from_spec(spec) + spec.loader.exec_module(gx) + cert = json.loads(gzip.decompress((PACKAGE / 'certificates/gcert1-p11-pr233-flow.json.gz').read_bytes())) + stats = {} + gx.check1(cert, scalar=True, stats=stats) + require((cert['h'], cert['v'], cert['R'], cert['N'], cert['cst']) == (22, 1320, 9412, 262944, 440), + 'unexpected program dimensions') + require(not cert['ext'], 'exterior gauges are outside this selected theorem') + inv = Counter() + for block_class in cert['blocks'].values(): + for width, count in block_class.items(): + inv[int(width)] += count + require(sum(inv.values()) == 69683, 'invocation count differs') + require(sum(r*n for r, n in inv.items()) == cert['N'], 'invocation rank differs') + hist = Counter({r: 5*n for r, n in inv.items()}) + for width in (42, 21, 46, 4): + hist[width] += 2*cert['v'] + m, roles = 5*cert['h'], 4*cert['v'] + cert['R'] + rank = sum(r*n for r, n in hist.items()) + require((m, roles, rank, m*roles-rank, max(hist), sum(hist.values())) == + (110, 14692, 1613040, 3080, 46, 358975), 'five-stage ledger differs') + expected = json.loads((PACKAGE / 'certificate/expected.json').read_text())['pr233']['five_stage'] + require(dict(hist) == {int(r): n for r, n in expected['child_histogram'].items()}, + 'ledger differs from upstream certificate') + lo, hi = moment_bounds(hist, m, roles, A) + require(hi < 1, 'tensor moment does not contract') + require(0 < DELTA < A < 1, 'no Fourier absorption gap') + # Also check the actual finite-fill inequality of the imported Lean engine. + _, endpoint_hi = moment_bounds({m-1: 1, 1: 1}, m, 1, A) + fill = Q(1, 2**40) + folded_hi = (1-fill)*hi + fill*endpoint_hi + require(folded_hi < 1, 'finite-fill engine inequality does not contract') + reject_at = Q(7547365, 10**10) + reject_lo, _ = moment_bounds(hist, m, roles, reject_at) + require(reject_lo > 1, 'negative rate control did not reject') + + with tarfile.open(VENDOR / source['fourier_proof']['archive']) as archive: + def read(path): + return archive.extractfile(path).read() + origin = json.loads((BASE/'evidence/five_stage_openai_origin.json').read_text()) + require(origin['success'] and origin['commit'] == 'fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb', + 'unexpected OpenAI source origin') + oai_paths = {m.name for m in archive.getmembers() + if m.isfile() and m.name.startswith('OAI/') and m.name.endswith('.lean')} + require(oai_paths == {p for p in origin['files'] if p.startswith('OAI/')}, + 'OpenAI source-origin ledger does not cover every imported module') + require(len(origin['files']) == 91, 'unexpected OpenAI source count') + for path, record in origin['files'].items(): + require(hashlib.sha256(read(path)).hexdigest() == record['sha256'], + 'archived source differs from checked OpenAI origin: '+path) + lean_cert = json.loads(gzip.decompress(read('tools/certificate/gcert1-p11-pr233-flow.json.gz'))) + compare_programs(cert, lean_cert) + rate = read('Work/GCert/Data/RateB2Gp233x.lean').decode() + block_list = re.search(r'def blocksB2Gp233x : List \(ℕ × ℕ\) := (\[.*\])', rate).group(1) + require(dict(ast.literal_eval(block_list)) == dict(hist), 'Lean rate ledger differs') + seam = read('Work/Fourier233/Seam.lean').decode() + require('def alphaY : ℝ := 1 - 7547361/(10:ℝ)^10' in seam, 'Lean kernel exponent differs') + require('def targetExponent : ℝ := 1 - 7547360/(10:ℝ)^10' in seam, 'Lean target exponent differs') + goal = read('Work/Fourier233/Goal.lean').decode() + require('def decimalExponentY : ℝ := 1 - 7547360/(10^(10:ℕ))' in goal, 'DFT goal exponent differs') + original = read('third-party/openai-math/lean/ComparatorChallenges/UniformFourier.lean').decode() + challenge = read('Work/Fourier233/UniformFourierChallenge.lean').decode() + compare_challenges(original, challenge) + + return { + 'schema': 1, + 'sources': {'five_stage': {'repository': source['repository'], 'commit': source['commit']}, + 'fourier_proof': source['fourier_proof']}, + 'tensor_saving': str(A), 'fourier_saving': str(DELTA), 'absorption_gap': str(A-DELTA), + 'program': {'registers': 2*cert['v']+cert['R'], 'frames': len(cert['frames']), + 'gates': len(cert['A'])+len(cert['B']), 'invocation_blocks': sum(inv.values()), + 'invocation_rank': cert['N'], 'reference_checker': 'Jacob Sussman gx.check1', + 'scalar_scope': 'all source columns; dirty-scratch restoration is proved by the Lean invocation theorem'}, + 'network': {'m': m, 'roles_per_vertex': roles, 'rank': rank, 'deficit': m*roles-rank, + 'max_child': max(hist), 'calls': sum(hist.values()), + 'child_histogram': {str(r): n for r, n in sorted(hist.items())}}, + 'moment_gap_lower_bound': rounded_down(1-hi), + 'finite_fill': {'s': 40, 'gap_lower_bound': rounded_down(1-folded_hi)}, + 'negative_control': {'saving': str(reject_at), 'excess_lower_bound': rounded_down(reject_lo-1)}, + 'bindings': {'lean_program': True, 'lean_histogram': True, 'lean_exponents': True, + 'openai_challenge_modulo_exponent_and_names': True, + 'openai_origin_files': len(origin['files']), 'openai_commit': origin['commit']}, + 'scope': 'Finite Python checks only; see five_stage_lean_receipt.json for the separately reproduced Lean build.' + } + + +def main(): + if sys.flags.optimize: + raise SystemExit('Run without -O: the imported checker uses assertions.') + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--proof-source', type=Path, help='also compare a full pinned Lean checkout') + parser.add_argument('--program-source', type=Path, help='also compare a full pinned PR256 checkout') + parser.add_argument('--openai-source', type=Path, help='also compare an OpenAI checkout with the origin ledger') + args = parser.parse_args() + source = source_check() + proof_hashes = check_evidence(source) + if args.proof_source: + check_checkout(args.proof_source, proof_hashes, 'Lean') + if args.program_source: + pins = json.loads((BASE / 'evidence/pr256_source_files.json').read_text()) + check_checkout(args.program_source / 'research/gcert-program-233', pins, 'PR256 package') + if args.openai_source: + origin = json.loads((BASE / 'evidence/five_stage_openai_origin.json').read_text()) + pins = {r['upstream_path']: r['sha256'] for r in origin['files'].values()} + check_checkout(args.openai_source, pins, 'OpenAI') + result = verify() + require(json.loads(REFERENCE.read_text()) == result, 'reference certificate differs') + print('PASS: explicit PR256 program, five-stage ledger, exact moment, finite fill, absorption gap and Lean source bindings.') + print('Tensor a = 0.0007547361; Fourier delta = 0.0007547360; gap = 1/10000000000.') + print('PASS: retained reproduction receipts and log hashes. This run does not execute Lean or prove multiplication.') + + +if __name__ == '__main__': + main()