From 52c8749f08e90498b3b6661b7de3ddfc1b98aeaf Mon Sep 17 00:00:00 2001 From: qoosmo Date: Thu, 27 Aug 2026 20:17:23 +0300 Subject: [PATCH] chore: professionalize kernel basis research artifact --- .github/workflows/ci.yml | 66 +++++++++ CONTRIBUTING.md | 40 ++++++ KernelBasisFiltration.lean | 10 +- LICENSE-APACHE | 201 +++++++++++++++++++++++++++ LICENSE-MIT | 21 +++ README.md | 198 ++++++++++++++++++++++++-- SECURITY.md | 11 ++ docs/VERIFICATION.md | 61 ++++++++ lake-manifest.json | 96 +++++++++++++ lakefile.toml | 1 + rust/Cargo.lock | 4 +- rust/Cargo.toml | 13 +- rust/src/bin/bench.rs | 42 ++++-- rust/src/lib.rs | 277 ++++++++++++++++++++++++++++++------- 14 files changed, 963 insertions(+), 78 deletions(-) create mode 100644 .github/workflows/ci.yml create mode 100644 CONTRIBUTING.md create mode 100644 LICENSE-APACHE create mode 100644 LICENSE-MIT create mode 100644 SECURITY.md create mode 100644 docs/VERIFICATION.md create mode 100644 lake-manifest.json diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 0000000..e4d18ff --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,66 @@ +name: CI + +on: + push: + branches: ["master"] + pull_request: + branches: ["master"] + workflow_dispatch: + +permissions: + contents: read + +jobs: + rust: + name: Rust + runs-on: ubuntu-latest + defaults: + run: + shell: bash + + steps: + - name: Checkout + uses: actions/checkout@v4 + + - name: Install Rust + uses: dtolnay/rust-toolchain@stable + with: + components: rustfmt, clippy + + - name: Formatting + run: cargo fmt --manifest-path rust/Cargo.toml --all -- --check + + - name: Check all targets + run: cargo check --manifest-path rust/Cargo.toml --all-targets --all-features + + - name: Tests + run: cargo test --manifest-path rust/Cargo.toml --all-features + + - name: Clippy + run: cargo clippy --manifest-path rust/Cargo.toml --all-targets --all-features -- -D warnings + + - name: Compile benchmark harness + run: cargo build --release --manifest-path rust/Cargo.toml --bin kernel-basis-bench + + lean: + name: Lean + runs-on: ubuntu-latest + + steps: + - name: Checkout + uses: actions/checkout@v4 + + - name: Build pinned Lean/Mathlib development + uses: leanprover/lean-action@v1 + with: + auto-config: false + build: true + test: false + use-mathlib-cache: true + + - name: Report admitted proof obligations + shell: bash + run: | + count="$(grep -cE '^[[:space:]]*sorry[[:space:]]*$' KernelBasisFiltration.lean || true)" + echo "Lean formalization currently contains ${count} explicit sorry placeholder(s)." + echo "A green build is not a completed machine-checked proof while these remain." diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 0000000..b9aebc0 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,40 @@ +# Contributing + +This repository is a research artifact. Changes should preserve the distinction between the mathematical manuscript, executable cross-checks, and incomplete formal verification. + +## Before opening a pull request + +Run the Rust quality gates: + +```sh +cargo fmt --manifest-path rust/Cargo.toml --all -- --check +cargo check --manifest-path rust/Cargo.toml --all-targets --all-features +cargo test --manifest-path rust/Cargo.toml --all-features +cargo clippy --manifest-path rust/Cargo.toml --all-targets --all-features -- -D warnings +cargo build --release --manifest-path rust/Cargo.toml --bin kernel-basis-bench +``` + +Run the Lean build: + +```sh +lake update +lake exe cache get +lake build +``` + +## Research claims + +When changing a theorem statement, transform convention, index ordering, or benchmark claim: + +1. update the manuscript/source of truth if appropriate; +2. update the Rust checks that exercise the same statement; +3. update the Lean statement when it has a corresponding declaration; +4. state clearly when a result is experimentally checked rather than proved; +5. do not describe admitted Lean declarations as machine-checked proofs. + +## Style + +- Rust must pass `rustfmt` and Clippy with `-D warnings`. +- Prefer deterministic tests. +- Keep asymptotic claims separate from machine-specific timings. +- Avoid introducing proving-system claims outside the scope of this artifact. diff --git a/KernelBasisFiltration.lean b/KernelBasisFiltration.lean index 869d672..0d8a08a 100644 --- a/KernelBasisFiltration.lean +++ b/KernelBasisFiltration.lean @@ -11,7 +11,7 @@ machine-checked proof of the paper. -/ import Mathlib.Algebra.Polynomial.Basic -import Mathlib.Algebra.Polynomial.Degree.Definitions +import Mathlib.Algebra.Polynomial.Degree.Defs import Mathlib.Algebra.Polynomial.Monic import Mathlib.Data.Fin.Basic import Mathlib.Data.Finset.Basic @@ -20,6 +20,8 @@ import Mathlib.LinearAlgebra.LinearIndependent.Defs open Polynomial open BigOperators +noncomputable section + variable {F : Type*} [Field F] /-- A Boolean vector of length `m`, i.e. an element of `{0,1}^m`, @@ -41,6 +43,12 @@ def comp {m : ℕ} (y : BVec m) : BVec m := def dom {m : ℕ} (y a : BVec m) : Prop := ∀ i, a i = true → y i = true +/-- Boolean domination is decidable because it is a proposition over a finite +Boolean index set. This explicit instance keeps coefficient statements +self-contained under the pinned Lean/Mathlib environment. -/ +instance instDecidableDom {m : ℕ} (y a : BVec m) : Decidable (dom y a) := + Classical.propDecidable _ + /-- Binary value `|a|_2`, Section 3.1. -/ def val {m : ℕ} (a : BVec m) : ℕ := ∑ i : Fin m, if a i then 2 ^ (i : ℕ) else 0 diff --git a/LICENSE-APACHE b/LICENSE-APACHE new file mode 100644 index 0000000..aee82c3 --- /dev/null +++ b/LICENSE-APACHE @@ -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 2026 Ali Mkhida, Algorizk Labs + + 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/LICENSE-MIT b/LICENSE-MIT new file mode 100644 index 0000000..c6ff7d3 --- /dev/null +++ b/LICENSE-MIT @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2026 Ali Mkhida, Algorizk Labs + +Permission is hereby granted, free of charge, to any person obtaining a copy +of the software and associated software documentation files (the "Software"), +to deal in the Software without restriction, including without limitation the +rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is furnished +to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/README.md b/README.md index 523d22a..c41deb4 100644 --- a/README.md +++ b/README.md @@ -1,39 +1,157 @@ -# kernel-basis-filtration +# Boolean Kernel Basis Filtration -Public research artifact for **\"The Boolean Kernel Basis and Its Low-Degree Filtration over Arbitrary Fields\"** by Ali Mkhida (Algorizk Labs). +[![CI](https://github.com/qoosmo/kernel-basis-filtration/actions/workflows/ci.yml/badge.svg)](https://github.com/qoosmo/kernel-basis-filtration/actions/workflows/ci.yml) +[![Lean 4](https://img.shields.io/badge/formalization-Lean%204-blue.svg)](KernelBasisFiltration.lean) +[![Rust](https://img.shields.io/badge/computational%20checks-Rust-orange.svg)](rust/) +[![License: MIT OR Apache-2.0](https://img.shields.io/badge/software%20license-MIT%20OR%20Apache--2.0-blue.svg)](#license) -The paper studies a Boolean-indexed polynomial basis over arbitrary fields and gives an exact characterization of the ordinary degree filtration in that basis. +**Research artifact for _“The Boolean Kernel Basis and Its Low-Degree Filtration over Arbitrary Fields”_ by Ali Mkhida (Algorizk Labs).** + +This repository studies a Boolean-indexed polynomial basis in which every basis element has maximal ordinary degree, then characterizes exactly how low-degree polynomials appear in those coordinates. - **Paper:** [`docs/paper.pdf`](docs/paper.pdf) -- **Source:** [`docs/paper.tex`](docs/paper.tex) -- **Rust implementation and tests:** [`rust/`](rust/) -- **Lean 4 formalization (in progress):** [`KernelBasisFiltration.lean`](KernelBasisFiltration.lean) +- **LaTeX source:** [`docs/paper.tex`](docs/paper.tex) +- **Rust computational checks:** [`rust/`](rust/) +- **Lean 4 formalization:** [`KernelBasisFiltration.lean`](KernelBasisFiltration.lean) +- **Verification notes:** [`docs/VERIFICATION.md`](docs/VERIFICATION.md) -## Verification status +## Main result + +Let \(N = 2^m\), let \(F\) be an arbitrary field, and index Boolean vectors by +\(y=(y_0,\ldots,y_{m-1}) \in \{0,1\}^m\). Define + +\[ +K_y(X)=\prod_{i=0}^{m-1}\left(X^{2^i}+y_i\right). +\] + +The paper proves three structural facts. + +### 1. Boolean kernel basis + +The family + +\[ +\{K_y : y\in\{0,1\}^m\} +\] + +is a basis of \(F[X]_{ Vec { let mut state = seed ^ 0x9E3779B97F4A7C15; (0..n) .map(|_| { - state = state.wrapping_mul(6364136223846793005).wrapping_add(1442695040888963407); + state = state + .wrapping_mul(6364136223846793005) + .wrapping_add(1442695040888963407); F::new((state >> 1) as i128, p) }) .collect() @@ -20,8 +22,13 @@ fn time_it(f: impl FnOnce() -> T) -> (T, f64) { fn main() { let p = GOLDILOCKS_P; - println!("Zeta transform: naive O(N^2) vs fast O(N log N), field = Goldilocks (2^64 - 2^32 + 1)"); - println!("{:>3} {:>10} {:>14} {:>14} {:>10}", "m", "N", "naive (s)", "fast (s)", "speedup"); + println!( + "Zeta transform: naive O(N^2) vs fast O(N log N), field = Goldilocks (2^64 - 2^32 + 1)" + ); + println!( + "{:>3} {:>10} {:>14} {:>14} {:>10}", + "m", "N", "naive (s)", "fast (s)", "speedup" + ); println!("{}", "-".repeat(56)); // Naive is O(N^2); keep it to sizes that finish in reasonable time. @@ -37,19 +44,29 @@ fn main() { if m <= naive_max_m { let (u_naive, t_naive) = time_it(|| zeta_naive(&lambda, m, p)); assert_eq!(u_naive, u_fast, "naive/fast disagreement at m={m}"); - let speedup = if t_fast > 0.0 { t_naive / t_fast } else { f64::INFINITY }; + let speedup = if t_fast > 0.0 { + t_naive / t_fast + } else { + f64::INFINITY + }; println!( "{:>3} {:>10} {:>14.6} {:>14.6} {:>9.1}x", m, n, t_naive, t_fast, speedup ); } else { - println!("{:>3} {:>10} {:>14} {:>14.6} {:>10}", m, n, "(skipped)", t_fast, "-"); + println!( + "{:>3} {:>10} {:>14} {:>14.6} {:>10}", + m, n, "(skipped)", t_fast, "-" + ); } } println!(); println!("Mobius inversion: naive O(N^2) vs fast O(N log N)"); - println!("{:>3} {:>10} {:>14} {:>14} {:>10}", "m", "N", "naive (s)", "fast (s)", "speedup"); + println!( + "{:>3} {:>10} {:>14} {:>14} {:>10}", + "m", "N", "naive (s)", "fast (s)", "speedup" + ); println!("{}", "-".repeat(56)); for m in 1..=fast_max_m { @@ -61,13 +78,20 @@ fn main() { if m <= naive_max_m { let (lam_naive, t_naive) = time_it(|| mobius_naive(&u, m, p)); assert_eq!(lam_naive, lam_fast, "naive/fast disagreement at m={m}"); - let speedup = if t_fast > 0.0 { t_naive / t_fast } else { f64::INFINITY }; + let speedup = if t_fast > 0.0 { + t_naive / t_fast + } else { + f64::INFINITY + }; println!( "{:>3} {:>10} {:>14.6} {:>14.6} {:>9.1}x", m, n, t_naive, t_fast, speedup ); } else { - println!("{:>3} {:>10} {:>14} {:>14.6} {:>10}", m, n, "(skipped)", t_fast, "-"); + println!( + "{:>3} {:>10} {:>14} {:>14.6} {:>10}", + m, n, "(skipped)", t_fast, "-" + ); } } diff --git a/rust/src/lib.rs b/rust/src/lib.rs index c3a4842..26f47fd 100644 --- a/rust/src/lib.rs +++ b/rust/src/lib.rs @@ -12,6 +12,13 @@ //! integer in 0..N (N = 2^m) via bit i <-> coordinate y_i, exactly //! matching |a|_2 = sum_i a_i 2^i from the paper. Complement is the //! bitwise NOT restricted to m bits, `(N - 1) ^ a`. +//! +//! This crate is a research reference implementation, not a constant-time +//! or audited finite-field library. + +#![forbid(unsafe_code)] + +use std::ops::{Add, Mul, Neg, Sub}; /// The Goldilocks prime, 2^64 - 2^32 + 1. pub const GOLDILOCKS_P: u64 = 0xFFFF_FFFF_0000_0001; @@ -21,60 +28,147 @@ pub const GOLDILOCKS_P: u64 = 0xFFFF_FFFF_0000_0001; /// prime that fits in a u64. #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub struct F { - pub v: u64, - pub p: u64, + v: u64, + p: u64, } impl F { + /// Construct a canonical residue modulo `p`. + /// + /// The caller is responsible for choosing a prime modulus when field + /// semantics are required. pub fn new(v: i128, p: u64) -> Self { - let m = p as i128; - let r = ((v % m) + m) % m; - F { v: r as u64, p } + assert!(p >= 2, "modulus must be at least 2"); + let modulus = p as i128; + let r = ((v % modulus) + modulus) % modulus; + Self { v: r as u64, p } } + pub fn zero(p: u64) -> Self { - F { v: 0, p } + assert!(p >= 2, "modulus must be at least 2"); + Self { v: 0, p } } + pub fn one(p: u64) -> Self { - F { v: 1 % p, p } + assert!(p >= 2, "modulus must be at least 2"); + Self { v: 1, p } + } + + #[inline] + pub fn value(self) -> u64 { + self.v + } + + #[inline] + pub fn modulus(self) -> u64 { + self.p } - pub fn add(self, o: F) -> F { - debug_assert_eq!(self.p, o.p); - let s = self.v as u128 + o.v as u128; - F { v: (s % self.p as u128) as u64, p: self.p } + + #[inline] + pub fn is_zero(self) -> bool { + self.v == 0 + } + + #[inline] + fn assert_same_modulus(self, other: Self) { + assert_eq!( + self.p, other.p, + "field modulus mismatch: {} != {}", + self.p, other.p + ); + } +} + +impl Add for F { + type Output = Self; + + fn add(self, rhs: Self) -> Self::Output { + self.assert_same_modulus(rhs); + let sum = self.v as u128 + rhs.v as u128; + Self { + v: (sum % self.p as u128) as u64, + p: self.p, + } } - pub fn sub(self, o: F) -> F { - debug_assert_eq!(self.p, o.p); - let s = (self.v as i128 - o.v as i128 + self.p as i128) % self.p as i128; - F { v: s as u64, p: self.p } +} + +impl Sub for F { + type Output = Self; + + fn sub(self, rhs: Self) -> Self::Output { + self.assert_same_modulus(rhs); + let v = if self.v >= rhs.v { + self.v - rhs.v + } else { + self.p - (rhs.v - self.v) + }; + Self { v, p: self.p } } - pub fn mul(self, o: F) -> F { - debug_assert_eq!(self.p, o.p); - let s = self.v as u128 * o.v as u128; - F { v: (s % self.p as u128) as u64, p: self.p } +} + +impl Mul for F { + type Output = Self; + + fn mul(self, rhs: Self) -> Self::Output { + self.assert_same_modulus(rhs); + let product = self.v as u128 * rhs.v as u128; + Self { + v: (product % self.p as u128) as u64, + p: self.p, + } } - pub fn neg(self) -> F { +} + +impl Neg for F { + type Output = Self; + + fn neg(self) -> Self::Output { if self.v == 0 { self } else { - F { v: self.p - self.v, p: self.p } + Self { + v: self.p - self.v, + p: self.p, + } } } - pub fn is_zero(self) -> bool { - self.v == 0 - } +} + +#[inline] +fn domain_size(m: u32) -> usize { + assert!( + m < usize::BITS, + "m must be smaller than usize::BITS ({})", + usize::BITS + ); + 1usize << m +} + +fn validate_table(values: &[F], m: u32, p: u64, name: &str) { + let expected = domain_size(m); + assert_eq!( + values.len(), + expected, + "{name} must have length 2^m = {expected}" + ); + assert!( + values.iter().all(|value| value.modulus() == p), + "{name} contains an element with a different modulus" + ); } /// Hamming weight of an m-bit integer (only the low `m` bits are meant to /// be set, but this just counts whatever bits are present). #[inline] pub fn wt(y: usize) -> u32 { - (y as u64).count_ones() + y.count_ones() } /// Boolean complement of `a` within `m` bits. #[inline] pub fn comp(a: usize, m: u32) -> usize { - let n = 1usize << m; + let n = domain_size(m); + assert!(a < n, "Boolean index a={a} is outside 0..{n}"); (n - 1) ^ a } @@ -82,7 +176,8 @@ pub fn comp(a: usize, m: u32) -> usize { /// K_y(X) = prod_i (X^{2^i} + y_i), built via the recursive even/odd /// construction of Section 4.3: O(N log N) time. pub fn kernel_poly_coeffs(y: usize, m: u32, p: u64) -> Vec { - let n = 1usize << m; + let n = domain_size(m); + assert!(y < n, "Boolean index y={y} is outside 0..{n}"); let mut c = vec![F::zero(p); n]; c[0] = F::one(p); let mut deg = 1usize; @@ -91,9 +186,9 @@ pub fn kernel_poly_coeffs(y: usize, m: u32, p: u64) -> Vec { let mut new_c = vec![F::zero(p); n]; for j in 0..deg { if yi == 1 { - new_c[j] = new_c[j].add(c[j]); + new_c[j] = new_c[j] + c[j]; } - new_c[j + (1 << i)] = new_c[j + (1 << i)].add(c[j]); + new_c[j + (1 << i)] = new_c[j + (1 << i)] + c[j]; } c = new_c; deg <<= 1; @@ -104,6 +199,9 @@ pub fn kernel_poly_coeffs(y: usize, m: u32, p: u64) -> Vec { /// Exact coefficient formula, Proposition 4.3/2.2 (complement-corrected): /// [K_y]_a = 1 iff y >= comp(a), else 0. pub fn kernel_coeff_formula(y: usize, a: usize, m: u32, p: u64) -> F { + let n = domain_size(m); + assert!(y < n, "Boolean index y={y} is outside 0..{n}"); + assert!(a < n, "Boolean index a={a} is outside 0..{n}"); let ab = comp(a, m); if (y & ab) == ab { F::one(p) @@ -116,17 +214,18 @@ pub fn kernel_coeff_formula(y: usize, a: usize, m: u32, p: u64) -> F { /// u[a] = sum_{y >= comp(a)} lambda[y]. Reference implementation, and the /// slow half of the benchmark. pub fn zeta_naive(lambda: &[F], m: u32, p: u64) -> Vec { - let n = 1usize << m; + validate_table(lambda, m, p, "lambda"); + let n = domain_size(m); let mut u = vec![F::zero(p); n]; - for a in 0..n { + for (a, ua) in u.iter_mut().enumerate() { let ab = comp(a, m); let mut s = F::zero(p); for (y, &ly) in lambda.iter().enumerate() { if (y & ab) == ab { - s = s.add(ly); + s = s + ly; } } - u[a] = s; + *ua = s; } u } @@ -134,14 +233,15 @@ pub fn zeta_naive(lambda: &[F], m: u32, p: u64) -> Vec { /// Fast O(N log N) zeta transform composed with the complement /// permutation, via the standard "sum over supersets" butterfly schedule. pub fn zeta_fast(lambda: &[F], m: u32, p: u64) -> Vec { - let n = 1usize << m; + validate_table(lambda, m, p, "lambda"); + let n = domain_size(m); let mut f = lambda.to_vec(); for i in 0..m { let bit = 1usize << i; for mask in 0..n { if mask & bit == 0 { let hi = f[mask | bit]; - f[mask] = f[mask].add(hi); + f[mask] = f[mask] + hi; } } } @@ -155,24 +255,30 @@ pub fn zeta_fast(lambda: &[F], m: u32, p: u64) -> Vec { /// Naive O(N^2) Moebius inversion: /// lambda[y] = sum_{b>=y} (-1)^{wt(b)-wt(y)} u[comp(b)]. pub fn mobius_naive(u: &[F], m: u32, p: u64) -> Vec { - let n = 1usize << m; + validate_table(u, m, p, "u"); + let n = domain_size(m); let mut lambda = vec![F::zero(p); n]; - for y in 0..n { + for (y, lambda_y) in lambda.iter_mut().enumerate() { let mut s = F::zero(p); for b in 0..n { if (b & y) == y { let term = u[comp(b, m)]; - s = if (wt(b) - wt(y)) % 2 == 0 { s.add(term) } else { s.sub(term) }; + s = if (wt(b) - wt(y)).is_multiple_of(2) { + s + term + } else { + s - term + }; } } - lambda[y] = s; + *lambda_y = s; } lambda } /// Fast O(N log N) Moebius inversion via the inverse butterfly schedule. pub fn mobius_fast(u: &[F], m: u32, p: u64) -> Vec { - let n = 1usize << m; + validate_table(u, m, p, "u"); + let n = domain_size(m); let mut h = vec![F::zero(p); n]; for (b, hb) in h.iter_mut().enumerate() { *hb = u[comp(b, m)]; @@ -182,7 +288,7 @@ pub fn mobius_fast(u: &[F], m: u32, p: u64) -> Vec { for mask in 0..n { if mask & bit == 0 { let hi = h[mask | bit]; - h[mask] = h[mask].sub(hi); + h[mask] = h[mask] - hi; } } } @@ -199,7 +305,8 @@ pub fn degree(u: &[F]) -> Option { /// 2^m entries, low `k` bits = x, high `m-k` bits = h) satisfy the /// character condition for this k? pub fn satisfies_character_condition(lambda: &[F], m: u32, k: u32, p: u64) -> bool { - let _ = p; + assert!(k <= m, "k must satisfy k <= m"); + validate_table(lambda, m, p, "lambda"); let q = m - k; let low_n = 1usize << k; let high_n = 1usize << q; @@ -207,7 +314,7 @@ pub fn satisfies_character_condition(lambda: &[F], m: u32, k: u32, p: u64) -> bo let mu_x = lambda[x | ((high_n - 1) << k)]; // h = all-ones (1_q) for h in 0..high_n { let y = x | (h << k); - let expected = if (q - wt(h as usize)) % 2 == 1 { mu_x.neg() } else { mu_x }; + let expected = if (q - wt(h)) % 2 == 1 { -mu_x } else { mu_x }; if lambda[y] != expected { return false; } @@ -220,14 +327,21 @@ pub fn satisfies_character_condition(lambda: &[F], m: u32, k: u32, p: u64) -> bo /// for the given `mu : {0,1}^k -> F` (i.e. the forward direction of /// Theorem 5.2: lambda[(x,h)] = (-1)^{q-wt(h)} mu[x]). pub fn character_table_from_mu(mu: &[F], m: u32, k: u32, p: u64) -> Vec { + assert!(k <= m, "k must satisfy k <= m"); let q = m - k; - let n = 1usize << m; - let high_n = 1usize << q; + let n = domain_size(m); + let low_n = domain_size(k); + let high_n = domain_size(q); + assert_eq!(mu.len(), low_n, "mu must have length 2^k = {low_n}"); + assert!( + mu.iter().all(|value| value.modulus() == p), + "mu contains an element with a different modulus" + ); let mut lambda = vec![F::zero(p); n]; for (x, &mux) in mu.iter().enumerate() { for h in 0..high_n { let y = x | (h << k); - lambda[y] = if (q - wt(h)) % 2 == 1 { mux.neg() } else { mux }; + lambda[y] = if (q - wt(h)) % 2 == 1 { -mux } else { mux }; } } lambda @@ -244,7 +358,9 @@ mod tests { let mut state = seed ^ 0x9E3779B97F4A7C15; (0..n) .map(|_| { - state = state.wrapping_mul(6364136223846793005).wrapping_add(1442695040888963407); + state = state + .wrapping_mul(6364136223846793005) + .wrapping_add(1442695040888963407); F::new((state >> 1) as i128, P) }) .collect() @@ -256,9 +372,9 @@ mod tests { let n = 1usize << m; for y in 0..n { let coeffs = kernel_poly_coeffs(y, m, P); - for a in 0..n { + for (a, &coeff) in coeffs.iter().enumerate() { assert_eq!( - coeffs[a], + coeff, kernel_coeff_formula(y, a, m, P), "mismatch at y={y}, a={a}" ); @@ -366,4 +482,67 @@ mod tests { } } } + + #[test] + fn zero_dimension_transforms_are_identity() { + let lambda = vec![F::new(7, P)]; + assert_eq!(zeta_fast(&lambda, 0, P), lambda); + assert_eq!(mobius_fast(&lambda, 0, P), lambda); + assert_eq!(kernel_poly_coeffs(0, 0, P), vec![F::one(P)]); + } + + #[test] + fn characteristic_two_condition_is_constant_on_high_fibers() { + let p = 2; + let m = 3; + let k = 1; + let mu = vec![F::zero(p), F::one(p)]; + let lambda = character_table_from_mu(&mu, m, k, p); + + for x in 0..(1usize << k) { + for h in 0..(1usize << (m - k)) { + assert_eq!(lambda[x | (h << k)], mu[x]); + } + } + + assert!(satisfies_character_condition(&lambda, m, k, p)); + let u = zeta_fast(&lambda, m, p); + if let Some(d) = degree(&u) { + assert!(d < (1usize << k)); + } + } + + #[test] + fn k_equals_m_accepts_an_arbitrary_kernel_table() { + let m = 5; + let lambda = rand_field_vec(1usize << m, 2026); + assert!(satisfies_character_condition(&lambda, m, m, P)); + } + + #[test] + #[should_panic(expected = "k must satisfy k <= m")] + fn rejects_k_larger_than_m() { + let lambda = vec![F::zero(P); 4]; + let _ = satisfies_character_condition(&lambda, 2, 3, P); + } + + #[test] + #[should_panic(expected = "lambda must have length")] + fn rejects_wrong_transform_table_length() { + let lambda = vec![F::zero(P); 3]; + let _ = zeta_fast(&lambda, 2, P); + } + + #[test] + #[should_panic(expected = "different modulus")] + fn rejects_mixed_modulus_table() { + let lambda = vec![F::zero(P), F::zero(17)]; + let _ = zeta_fast(&lambda, 1, P); + } + + #[test] + #[should_panic(expected = "field modulus mismatch")] + fn arithmetic_rejects_cross_modulus_operands() { + let _ = F::one(17) + F::one(19); + } }