KBFold

Post-Quantum Multilinear Polynomial Commitments from FRI Folding in the Boolean-Kernel Basis.

This repository contains three things that describe one object:

	What	Where
📄	A self-contained paper (55 pages): definitions, theorems and full proofs	paper/ · PDF
✅	A Lean 4 formalisation of the paper's mathematics (17 modules, ~7,200 lines, no sorry)	lean/
⚙️	A Rust reference implementation of the commitment scheme, with benchmarks	rust/

The idea in one paragraph

BaseFold-style polynomial commitments fold a Reed–Solomon codeword while running a sumcheck. Over smooth multiplicative domains, the classical FRI fold acts on monomial coefficients, so a prover holding a multilinear polynomial as a table of values must first change representation. We introduce the Boolean-kernel basis

$$K_b(X) = \prod_{k=1}^{n} \bigl(X^{2^{k-1}} + b_k\bigr), \qquad b \in {0,1}^n,$$

of the polynomials of degree $< 2^n$. In this basis a normalised FRI fold is exactly the restriction of one variable of the multilinear extension of the coordinate table (the fold dictionary). Folding the codeword of $\sum_b f(b) K_b$ therefore evaluates $\tilde f$ directly: the committed word, the sumcheck table and the folds are three views of one object.

Main results

• Basis theorem. ${K_b}$ is a basis of $\mathbb{F}[X]_{<2^n}$; the change of basis to monomials is a Kronecker power of a $2\times2$ matrix and costs $\tfrac{n}{2}2^n$ additions.

• Fold dictionary. $\mathrm{pfold}r\bigl(\sum_b \lambda(b) K_b\bigr) = \sum{b'} \mathrm{res}r(\lambda)(b'), K{b'}$.

• Low degree and evaluation. A sign-condition characterisation of low degree in kernel coordinates; univariate evaluation as a scaled multilinear evaluation.

• Commitment scheme. A transparent, hash-based multilinear PCS (BaseFold paradigm, kernel encoding), with proofs of:

  • completeness;
  • soundness and evaluation binding in the unique-decoding regime;
  • round-by-round knowledge soundness with an explicit decoding extractor.

  The only external ingredient about codes is the correlated-agreement theorem of BCIKS.

• Post-quantum security. From round-by-round knowledge soundness we derive the relaxed round-by-round knowledge soundness of Chiesa–Di–Hu–Zheng (ePrint 2025/2166).

  • By their BCS theorem for interactive oracle reductions, the non-interactive scheme is knowledge sound against quantum adversaries in the QROM, with explicit concrete bounds.
  • This holds even though the adversary chooses the Merkle-committed commitment.
  • Example parameters: $2^{64}$ queries, error $< 2^{-31.8}$, with κ = 248 queries and a 256-bit hash.

Verification status

Part	Paper	Lean	Other checks
Multilinear toolkit, smooth domains, RS codes (§2)	proved	✅ formalised	—
IOPs, round-by-round soundness, sumcheck (§3.1–3.4)	proved	✅ formalised	—
Kernel basis, low degree, evaluation (§4)	proved	✅ formalised	paper_checks, $n \le 6$
Fold dictionary, word folds, classical fold (§5)	proved	✅ formalised	paper_checks, $n \le 6$
Completeness (§6)	proved	✅ formalised	Rust tests, paper_checks
Soundness, binding, RBR knowledge (§7.1–7.6)	proved	✅ formalised, axiom BCIKS	exhaustive checks over $\mathbb{F}_{17}$ in paper_checks
Relaxed RBR knowledge, erasures (§7.7)	proved	✅ formalised, axiom BCIKS	two independent reviews
Post-quantum corollary (Thm 3.16, Cor 7.26)	theorem quoted from CDHZ25, specialisation proved	— (quantum model)	exact parameter computation (pq_params)
Correlated agreement (BCIKS Thm 4.1)	quoted	the single axiom bciks_unique	—

Details: docs/VERIFICATION.md · paper ↔ Lean map: docs/LEAN_MAP.md.

Repository layout

paper/     LaTeX sources, bibliography, compiled PDF
lean/      Lake project KBFold (Lean 4.23.0 + Mathlib v4.23.0)
rust/      kbfold crate: field (Goldilocks + quadratic extension), NTT, Merkle, PCS; tests, benchmarks, checks
checks/    Python reference for the post-quantum parameter computation
docs/      verification report, paper↔Lean map, roadmap

Quick start

Lean (checks every formalised theorem; downloads the Mathlib cache):

cd lean
lake exe cache get
lake build
lake env lean KBFold/Audit.lean    # prints the axioms used by the main theorems

Rust (Rust ≥ 1.85; the library is published on crates.io as kbfold):

cd rust
cargo test --release                          # completeness, tampering, robustness, field facts
cargo test --release --features insecure-test-vectors  # test vectors (vectors/)
cargo run --release --example paper_checks    # numerical checks of the paper's lemmas
cargo run --release --example pq_params       # exact post-quantum bound (Remark 7.28)
cargo run --release --example bench -- scaling   # one benchmark of Section 9 (modes: scaling pq salt stop rate breakdown)
bench/run_all.sh mymachine 22 [path/to/whir]    # all benchmarks of Section 9, CSV in results/mymachine/

Paper:

cd paper && latexmk -pdf main.tex

Scope

• Unique decoding only. The soundness analysis stays in the unique-decoding regime. List-decoding analyses need fewer queries; extending to them is planned for version 2 (see the roadmap).
• One opening per proof. The analysis covers one commitment opened at one point per proof; batched and multiple openings are planned for version 2.
• Post-quantum parameters. The corollary applies to the compiler of CDHZ25 (Construction 11.7). The Rust code follows its structure: salted Merkle trees, one round salt per round, challenges from all previous roots and salts. Use Params::post_quantum(m) with challenges in Fp4; Params::classical(m) with Fp2 gives about 100 bits of classical security.
• Performance. With 20 variables at 100 bits of security (rate 1/4, one committed word in four, merged paths): prover 0.84 s single-threaded, proof 237 KiB, verifier 1.2 ms on a 2-vCPU cloud machine; the paper (Section 9) compares with WHIR on the same machine.
• Reference implementation. Single-threaded and not audited; the verifier returns Result and never panics on malformed proofs.

Citation

@misc{Mkhida2026KBFold,
  author = {Abdelali Mkhida},
  title  = {Post-Quantum Multilinear Polynomial Commitments from {FRI} Folding
            in the {Boolean}-Kernel Basis},
  year   = {2026},
  note   = {Paper, Lean 4 formalisation and Rust implementation},
  howpublished = {\url{https://github.com/qoosmo/kbfold}}
}

See also CITATION.cff.

Author

Abdelali Mkhida — independent researcher, Algorizk Labs · ORCID 0009-0009-2101-9070 · ali.mkhida@algorizk.xyz

License

Code: dual-licensed under MIT or Apache-2.0, at your option. Paper (paper/): Creative Commons Attribution 4.0 International (CC BY 4.0).