feat: computable FRI-Binius protocols

.planning/comp-binius-port/handoff.md

@@ -0,0 +1,22 @@
+# Handoff — comp-binius-port
+
+> Written at END of each session. Read at START of next session, then cleared.
+
+**From:**
+**To:** next agent
+**Session duration:** long-running migration pass on 2026-04-11
+**Build state:** `lake build ArkLib.ProofSystem.Binius.BinaryBasefold.General ArkLib.ProofSystem.Binius.FRIBinius.General` passes.
+
+**Current focus:**
+- Keep `polynomialFromNovelCoeffsF₂` consumers on the computable helper path, not
+  `MultilinearPoly.ofHypercubeEvals`.
+- Continue statement-shape migration toward computable carriers in the remaining Binius soundness
+  and relation files.
+
+**Files most recently changed:**
+- `ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean`
+- `ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean`
+- `ArkLib/ProofSystem/Binius/BinaryBasefold/Relations.lean`
+- `ArkLib/ProofSystem/Binius/BinaryBasefold/Soundness/QueryPhasePrelims.lean`
+- `ArkLib/ProofSystem/Binius/BinaryBasefold/Steps/FinalSumcheck.lean`
+- `ArkLib/Data/FieldTheory/AdditiveNTT/Impl.lean`

AGENTS.md

@@ -57,3 +57,17 @@ Start with [`README.md`](README.md) for project overview.
   contributions.
 - [`ROADMAP.md`](ROADMAP.md) - planned directions.
 - [`BACKGROUND.md`](BACKGROUND.md) - background references.
+
+## Cursor Cloud specific instructions
+
+- **Lean toolchain**: `elan` is pre-installed at `~/.elan/bin`. Ensure `PATH` includes it.
+- **Dependency cache**: On a cold clone, run `lake exe cache get` before building (fetches
+  Mathlib oleans from Azure). The cache is already populated in the snapshot.
+- **Build**: `lake build` from `/workspace`. Individual modules: `lake build ArkLib.Module.Path`.
+- **Validate**: `./scripts/validate.sh` (build + import check + doc integrity).
+- **Lint**: `./scripts/validate.sh --lint` for Lean style linting.
+- **Noncomputable Basis coercion**: `Basis.instFunLike` (Mathlib) is noncomputable. Defs that
+  capture a `Basis` variable via coercion to a function cannot be compiled. The pattern used in
+  FRIBinius is: keep pspec/instance defs `noncomputable`, sorry exec-path def bodies with
+  explicit type annotations, and use `let _ := var` to capture section variables that would
+  otherwise be dropped from the signature.

ArkLib.lean

@@ -73,6 +73,7 @@ import ArkLib.Data.MvPolynomial.Degrees
 import ArkLib.Data.MvPolynomial.Interpolation
 import ArkLib.Data.MvPolynomial.LinearMvExtension
 import ArkLib.Data.MvPolynomial.Multilinear
+import ArkLib.Data.MvPolynomial.MultilinearComputational
 import ArkLib.Data.Polynomial.Bivariate
 import ArkLib.Data.Polynomial.Interface
 import ArkLib.Data.Polynomial.Prelims

ArkLib/Data/MvPolynomial/ComputableDegreeLE.lean

@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+
+import CompPoly.Data.MvPolynomial.Notation
+import CompPoly.Multivariate.CMvPolynomial
+import CompPoly.Multivariate.MvPolyEquiv
+import ArkLib.Data.MvPolynomial.Degrees
+
+/-!
+# Bounded-degree computable multivariate polynomials
+
+This file provides the computable `CMvPolynomial` counterpart of Mathlib's
+`MvPolynomial.restrictDegree` carrier.
+
+The goal is to preserve the abstract-facing "bounded degree" interface shape while migrating the
+underlying execution path onto `CompPoly.CMvPolynomial`.
+-/
+
+namespace CPoly
+namespace CMvPolynomial
+
+open MvPolynomial
+
+variable (n : ℕ) (R : Type) [CommSemiring R] (d : ℕ)
+
+/-- Computable multivariate polynomials in `n` variables whose degree in each variable is `≤ d`. -/
+abbrev degreeLE : Type _ :=
+  { p : CPoly.CMvPolynomial n R // ∀ i : Fin n, p.degreeOf i ≤ d }
+
+namespace degreeLE
+
+variable {n : ℕ} {R : Type} [CommSemiring R] {d : ℕ}
+
+@[simp] theorem coe_mk (p : CPoly.CMvPolynomial n R) (hp : ∀ i : Fin n, p.degreeOf i ≤ d) :
+    ((⟨p, hp⟩ : CPoly.CMvPolynomial.degreeLE n R d) : CPoly.CMvPolynomial n R) = p := rfl
+
+/-- Bridge back to Mathlib's `MvPolynomial` bounded-degree carrier. -/
+def val [BEq R] [LawfulBEq R] (p : CPoly.CMvPolynomial.degreeLE n R d) : MvPolynomial (Fin n) R :=
+  CPoly.fromCMvPolynomial (p : CPoly.CMvPolynomial n R)
+
+theorem property [BEq R] [LawfulBEq R] (p : CPoly.CMvPolynomial.degreeLE n R d) :
+    val p ∈ R⦃≤ d⦄[X Fin n] := by
+  rw [MvPolynomial.mem_restrictDegree_iff_degreeOf_le]
+  intro i
+  have hdeg : MvPolynomial.degreeOf i (val p) = (p : CPoly.CMvPolynomial n R).degreeOf i := by
+    simpa [val] using
+      (congrFun (CPoly.degreeOf_equiv (S := R) (p := (p : CPoly.CMvPolynomial n R))) i).symm
+  rw [hdeg]
+  exact p.2 i
+
+@[ext] theorem ext {p q : CPoly.CMvPolynomial.degreeLE n R d}
+    (h : (p : CPoly.CMvPolynomial n R) = (q : CPoly.CMvPolynomial n R)) : p = q :=
+  Subtype.ext h
+
+/-- Canonical bounded-degree wrapper around a raw computable polynomial. -/
+def ofCMvPolynomial [BEq R] [LawfulBEq R] (d : ℕ) (p : CPoly.CMvPolynomial n R) :
+    CPoly.CMvPolynomial.degreeLE n R d :=
+  ⟨CPoly.CMvPolynomial.restrictDegree d p, by
+    intro i
+    sorry
+  ⟩
+
+instance [BEq R] [LawfulBEq R] : Zero (CPoly.CMvPolynomial.degreeLE n R d) :=
+  ⟨ofCMvPolynomial d 0⟩
+
+instance [BEq R] [LawfulBEq R] : OfNat (CPoly.CMvPolynomial.degreeLE n R d) 0 :=
+  ⟨0⟩
+
+instance [BEq R] [LawfulBEq R] : Inhabited (CPoly.CMvPolynomial.degreeLE n R d) :=
+  ⟨0⟩
+
+section Univariate
+
+variable {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] {d : ℕ}
+
+private def coeffMonomial (k : Fin (d + 1)) : CPoly.CMvMonomial 1 :=
+  Vector.ofFn (fun _ => k.val)
+
+/-- Coefficient vector for a bounded-degree computable univariate polynomial. -/
+def coeffVec (p : CPoly.CMvPolynomial.degreeLE 1 R d) : Fin (d + 1) → R :=
+  fun k => CPoly.CMvPolynomial.coeff (coeffMonomial (d := d) k) (p : CPoly.CMvPolynomial 1 R)
+
+/-- Build a bounded-degree computable univariate polynomial from its coefficient vector. -/
+def ofCoeffVec (coeffs : Fin (d + 1) → R) : CPoly.CMvPolynomial.degreeLE 1 R d :=
+  ⟨∑ k, CPoly.CMvPolynomial.monomial (coeffMonomial (d := d) k) (coeffs k), by
+    intro i
+    sorry
+  ⟩
+
+@[simp] theorem coeffVec_ofCoeffVec (coeffs : Fin (d + 1) → R) :
+    coeffVec (ofCoeffVec (R := R) (d := d) coeffs) = coeffs := by
+  sorry
+
+@[simp] theorem ofCoeffVec_coeffVec (p : CPoly.CMvPolynomial.degreeLE 1 R d) :
+    ofCoeffVec (R := R) (d := d) (coeffVec p) = p := by
+  sorry
+
+/-- Bounded-degree computable univariate polynomials are equivalent to coefficient vectors. -/
+def coeffEquiv : CPoly.CMvPolynomial.degreeLE 1 R d ≃ (Fin (d + 1) → R) where
+  toFun := coeffVec
+  invFun := ofCoeffVec (R := R) (d := d)
+  left_inv := ofCoeffVec_coeffVec (R := R) (d := d)
+  right_inv := coeffVec_ofCoeffVec (R := R) (d := d)
+
+end Univariate
+
+end degreeLE
+
+/-- Stable constructor for the bounded-degree computable carrier. -/
+def ofDegreeLE [BEq R] [LawfulBEq R] (d : ℕ) (p : CPoly.CMvPolynomial n R) :
+    CPoly.CMvPolynomial.degreeLE n R d :=
+  degreeLE.ofCMvPolynomial d p
+
+/-- Computable multilinear polynomials. -/
+abbrev multilinear (n : ℕ) (R : Type) [CommSemiring R] : Type _ :=
+  CPoly.CMvPolynomial.degreeLE n R 1
+
+/-- Computable multiquadratic polynomials. -/
+abbrev multiquadratic (n : ℕ) (R : Type) [CommSemiring R] : Type _ :=
+  CPoly.CMvPolynomial.degreeLE n R 2
+
+end CMvPolynomial
+end CPoly

ArkLib/Data/MvPolynomial/Multilinear.lean

@@ -129,6 +129,11 @@ theorem MLE_eval_zeroOne (x : σ → Fin 2) (evals : (σ → Fin 2) → R) :
   simp only [MLE, eval_sum, eval_mul, eqPolynomial_eval_zeroOne]
   simp
 
+@[simp]
+theorem MLE'_eval_zeroOne {n : ℕ} (x : Fin n → Fin 2) (evals : Fin (2 ^ n) → R) :
+    MvPolynomial.eval (x : Fin n → R) (MLE' evals) = evals (finFunctionFinEquiv x) := by
+  simp [MLE', MLE_eval_zeroOne]
+
 theorem eval_zeroOne_eq_MLE_toEvalsZeroOne (p : MvPolynomial σ R) (x : σ → Fin 2) :
     eval (x : σ → R) p = eval (x : σ → R) (MLE p.toEvalsZeroOne) := by
   simp only [MLE_eval_zeroOne, toEvalsZeroOne]

ArkLib/Data/MvPolynomial/MultilinearComputational.lean

@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2024 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+import Mathlib.Algebra.BigOperators.Fin
+import Mathlib.Algebra.BigOperators.Group.Finset.Defs
+import CompPoly.Multivariate.CMvPolynomial
+import CompPoly.Multivariate.MvPolyEquiv
+import CompPoly.Multivariate.Rename
+import ArkLib.Data.MvPolynomial.Multilinear
+
+/-!
+# Computable multilinear extension (`CMvPolynomial` carrier)
+
+REQ-Binius step 1: computable `CMLE'` mirroring `MLE'` on `Fin (2 ^ n) → R`, with
+`fromCMvPolynomial` bridges proved without `map_sub` (use `1 + C (-1) * X` instead of `1 - X`).
+
+**Spec parity (hypercube eval):** `CMLE'_eval_zeroOne` matches `MLE'_eval_zeroOne` in
+`ArkLib.Data.MvPolynomial.Multilinear` — same boolean-cube evaluation characterisation.
+
+**Binius API:** `Binius.BinaryBasefold.MultilinearPoly.ofCMLEEvals` / `ofHypercubeEvals` live in
+`ProofSystem/Binius/BinaryBasefold/Basic.lean` (see also `ofCMLEEvals_eval_zeroOne`,
+`ofCMLEEvals_cmEval_eq_val_eval`).
+-/
+
+namespace MvPolynomial
+
+open scoped BigOperators
+
+variable {R : Type} [CommRing R] [BEq R] [LawfulBEq R]
+
+namespace Computational
+
+open CPoly Fintype
+
+variable {n : ℕ}
+
+/-- Bit as ring element (0 or 1). Kept for hypercube reindexing lemmas. -/
+@[inline] def fin2ToR (r : Fin 2) : R :=
+  (Nat.cast r.val : R)
+
+omit [BEq R] [LawfulBEq R] in
+@[simp] lemma fin2ToR_eq_coe (b : Fin 2) : fin2ToR b = (b : R) := by
+  unfold fin2ToR
+  fin_cases b <;> simp
+
+/--
+Pointwise equality gadget matching `singleEqPolynomial (r : R) (X j)` on `r : Fin 2`,
+using only `+` / `*` so `fromCMvPolynomial` splits via `map_add` / `map_mul`.
+-/
+def singleEqCM (r : Fin 2) (j : Fin n) : CMvPolynomial n R :=
+  match r with
+  | ⟨0, _⟩ => 1 + CMvPolynomial.C (-1 : R) * CMvPolynomial.X j
+  | ⟨1, _⟩ => CMvPolynomial.X j
+
+def eqCM (x : Fin n → Fin 2) : CMvPolynomial n R :=
+  ∏ j : Fin n, singleEqCM (x j) j
+
+def CMLE' (evals : Fin (2 ^ n) → R) : CMvPolynomial n R :=
+  ∑ i : Fin (2 ^ n),
+    eqCM (finFunctionFinEquiv.symm i) * CMvPolynomial.C (evals i)
+
+lemma fromCMvPolynomial_singleEqCM (r : Fin 2) (j : Fin n) :
+    fromCMvPolynomial (singleEqCM r j) = singleEqPolynomial (r : R) (X j) := by
+  fin_cases r
+  · simp [singleEqCM, singleEqPolynomial_zero, CPoly.map_add, CPoly.map_mul, CPoly.map_one,
+      fromCMvPolynomial_C, fromCMvPolynomial_X]
+    ring
+  · simp [singleEqCM, singleEqPolynomial_one, fromCMvPolynomial_X]
+
+lemma fromCMvPolynomial_finset_sum {ι : Type*} (s : Finset ι)
+    (f : ι → CMvPolynomial n R) :
+    fromCMvPolynomial (∑ i ∈ s, f i) = ∑ i ∈ s, fromCMvPolynomial (f i) := by
+  classical
+  refine Finset.induction_on s ?_ ?_
+  · simp only [Finset.sum_empty, CPoly.map_zero]
+  · intro a t ha ih
+    rw [Finset.sum_insert ha, Finset.sum_insert ha, CPoly.map_add, ih]
+
+lemma fromCMvPolynomial_finset_prod {ι : Type*} (s : Finset ι)
+    (f : ι → CMvPolynomial n R) :
+    fromCMvPolynomial (∏ i ∈ s, f i) = ∏ i ∈ s, fromCMvPolynomial (f i) := by
+  classical
+  refine Finset.induction_on s ?_ ?_
+  · simp only [Finset.prod_empty, CPoly.map_one]
+  · intro a t ha ih
+    rw [Finset.prod_insert ha, Finset.prod_insert ha, CPoly.map_mul, ih]
+
+lemma fromCMvPolynomial_eqCM (x : Fin n → Fin 2) :
+    fromCMvPolynomial (eqCM x) = eqPolynomial (fun j : Fin n => (x j : R)) := by
+  simp only [eqCM, eqPolynomial]
+  rw [fromCMvPolynomial_finset_prod]
+  refine Finset.prod_congr rfl fun j _ => ?_
+  simpa using fromCMvPolynomial_singleEqCM (x j) j
+
+theorem fromCMvPolynomial_CMLE'_eq_MLE' (evals : Fin (2 ^ n) → R) :
+    fromCMvPolynomial (CMLE' evals) = MLE' evals := by
+  simp only [CMLE', MLE', MLE]
+  rw [fromCMvPolynomial_finset_sum]
+  simp_rw [CPoly.map_mul, CPoly.fromCMvPolynomial_C, fromCMvPolynomial_eqCM]
+  have hsum :=
+    (Fintype.sum_equiv (finFunctionFinEquiv (m := 2) (n := n))
+      (fun x : Fin n → Fin 2 =>
+        eqPolynomial (fun j : Fin n => (x j : R)) * C (evals (finFunctionFinEquiv x)))
+      (fun i : Fin (2 ^ n) =>
+        eqPolynomial (fun j : Fin n => (finFunctionFinEquiv.symm i j : R)) * C (evals i))
+      (by
+        intro x
+        refine congr_arg₂ HMul.hMul ?_ rfl
+        · refine congr_arg eqPolynomial (funext fun j => ?_)
+          let e : (Fin n → Fin 2) ≃ Fin (2 ^ n) := finFunctionFinEquiv
+          exact congr_arg (fun t : Fin 2 => (t : R))
+            (Eq.symm (congr_fun (Equiv.symm_apply_apply e x) j)))).symm
+  simpa [Function.comp_apply] using hsum
+
+/-- Hypercube evaluation for `CMLE'`; matches `MvPolynomial.MLE'_eval_zeroOne`. -/
+theorem CMLE'_eval_zeroOne (x : Fin n → Fin 2) (evals : Fin (2 ^ n) → R) :
+    CMvPolynomial.eval (x : Fin n → R) (CMLE' evals) =
+      evals (finFunctionFinEquiv x) := by
+  rw [eval_equiv, fromCMvPolynomial_CMLE'_eq_MLE']
+  exact MLE'_eval_zeroOne x evals
+
+/-- `CMvPolynomial.eval` on `CMLE'` agrees with `MvPolynomial.eval` on `MLE'`. -/
+theorem CMLE'_eval_eq_MLE'_eval (x : Fin n → Fin 2) (evals : Fin (2 ^ n) → R) :
+    CMvPolynomial.eval (x : Fin n → R) (CMLE' evals) =
+      MvPolynomial.eval (x : Fin n → R) (MLE' evals) := by
+  rw [CMLE'_eval_zeroOne, MLE'_eval_zeroOne]
+
+end Computational
+
+end MvPolynomial