feat: completeness and rbrKnowledgeSoundness of FRI-Binius protocols

ArkLib.lean

@@ -51,7 +51,9 @@ import ArkLib.Data.CodingTheory.ProximityGap.Basic
 import ArkLib.Data.CodingTheory.ProximityGap.DG25
 import ArkLib.Data.CodingTheory.ReedSolomon
 import ArkLib.Data.EllipticCurve.BN254
+import ArkLib.Data.FieldTheory.AdditiveNTT.AdditiveNTT
 import ArkLib.Data.Fin.Basic
+import ArkLib.Data.Fin.BigOperators
 import ArkLib.Data.Fin.Fold
 import ArkLib.Data.Fin.Lift
 import ArkLib.Data.Fin.Sigma
@@ -81,6 +83,7 @@ import ArkLib.Data.Probability.Notation
 import ArkLib.OracleReduction.BCS.Basic
 import ArkLib.OracleReduction.Basic
 import ArkLib.OracleReduction.Cast
+import ArkLib.OracleReduction.Completeness
 import ArkLib.OracleReduction.Composition.Parallel.Basic
 import ArkLib.OracleReduction.Composition.Sequential.Append
 import ArkLib.OracleReduction.Composition.Sequential.General
@@ -118,15 +121,32 @@ import ArkLib.ProofSystem.BatchedFri.Security
 import ArkLib.ProofSystem.BatchedFri.Spec.General
 import ArkLib.ProofSystem.BatchedFri.Spec.SingleRound
 import ArkLib.ProofSystem.Binius.BinaryBasefold.Basic
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Code
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Compliance
 import ArkLib.ProofSystem.Binius.BinaryBasefold.CoreInteractionPhase
 import ArkLib.ProofSystem.Binius.BinaryBasefold.General
 import ArkLib.ProofSystem.Binius.BinaryBasefold.Prelude
 import ArkLib.ProofSystem.Binius.BinaryBasefold.QueryPhase
+import ArkLib.ProofSystem.Binius.BinaryBasefold.ReductionLogic
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Relations
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.BadBlocks
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.FoldDistance
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.Incremental
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.Lift
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.Proposition4_21
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.QueryPhasePrelims
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Soundness.QueryPhaseSoundness
 import ArkLib.ProofSystem.Binius.BinaryBasefold.Spec
 import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps.Commit
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps.FinalSumcheck
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps.Fold
+import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps.Relay
 import ArkLib.ProofSystem.Binius.FRIBinius.CoreInteractionPhase
 import ArkLib.ProofSystem.Binius.FRIBinius.General
 import ArkLib.ProofSystem.Binius.FRIBinius.Prelude
+import ArkLib.ProofSystem.Binius.RingSwitching.BBFSmallFieldIOPCS
 import ArkLib.ProofSystem.Binius.RingSwitching.BatchingPhase
 import ArkLib.ProofSystem.Binius.RingSwitching.General
 import ArkLib.ProofSystem.Binius.RingSwitching.Prelude
@@ -171,7 +191,9 @@ import ArkLib.ToMathlib.Data.IndexedBinaryTree.Equiv
 import ArkLib.ToMathlib.Data.IndexedBinaryTree.Lemmas
 import ArkLib.ToMathlib.Finset.Basic
 import ArkLib.ToMathlib.List.Basic
+import ArkLib.ToMathlib.MvPolynomial.Equiv
 import ArkLib.ToVCVio.DistEq
 import ArkLib.ToVCVio.Lemmas
 import ArkLib.ToVCVio.Oracle
 import ArkLib.ToVCVio.SimOracle
+import ArkLib.ToVCVio.Simulation

ArkLib/Data/CodingTheory/DivergenceOfSets.lean

@@ -149,12 +149,12 @@ theorem Pr_uniform_equiv {α β : Type} [Fintype α] [Nonempty α] [Fintype β]
       (PMF.map_comp (p := PMF.uniformOfFintype α) (f := e) (g := P)).symm
   -- Apply both sides to `True`, then use `hmap`.
   -- Finally, recognize the right-hand side as the original `do` block.
-  simpa using congrArg (fun q : PMF Prop => q True) (by
-    calc
-      (PMF.uniformOfFintype α).map (P ∘ e)
-          = ((PMF.uniformOfFintype α).map e).map P := hcomp
-      _ = (PMF.uniformOfFintype β).map P := by simp [hmap]
-    )
+  calc
+    (do let a ← $ᵖ α; pure (P (e a))) True
+      = ((PMF.uniformOfFintype α).map (P ∘ e)) True := rfl
+    _ = (((PMF.uniformOfFintype α).map e).map P) True := by rw [hcomp]
+    _ = ((PMF.uniformOfFintype β).map P) True := by rw [hmap]
+    _ = (do let b ← $ᵖ β; pure (P b)) True := rfl
 
 theorem divergence_attains {ι : Type} [Fintype ι] [Nonempty ι]
   {F : Type} [DecidableEq F]
@@ -862,7 +862,7 @@ theorem concentration_bounds {ι : Type} [Fintype ι] [Nonempty ι] [DecidableEq
       funext u
       apply propext
       simpa using (hiffU u)
-    simp [hfun]
+    exact congr_arg (fun f => (do let u ← $ᵖ U; pure (f u)) True) hfun
   -- Apply proximity gap at parameter δ
   have hδ_bound : (δ : ℝ≥0) ≤ 1 - ReedSolomonCode.sqrtRate deg domain := by
     have hδ_lt_div : (δ : ℝ≥0) < (δ' : ℝ≥0) := by

ArkLib/Data/CodingTheory/Prelims.lean

@@ -7,6 +7,7 @@ Authors: Katerina Hristova, František Silváši, Julian Sutherland, Chung Thai
 import Mathlib.Algebra.Lie.OfAssociative
 import Mathlib.LinearAlgebra.Matrix.Rank
 import Mathlib.LinearAlgebra.AffineSpace.Pointwise
+import CompPoly.Data.Nat.Bitwise
 
 section TensorCombination
 variable {F : Type*} [CommRing F] [Fintype F] [DecidableEq F]
@@ -19,6 +20,72 @@ def multilinearWeight {ϑ : ℕ} (r : Fin ϑ → F) (i : Fin (2 ^ ϑ)) : F :=
   ∏ j : Fin ϑ,
     if i.val.testBit j.val then (r j) else (1 - r j)
 
+omit [Fintype F] [DecidableEq F] in
+lemma multilinearWeight_succ {ϑ : ℕ} (r : Fin (ϑ + 1) → F) (i : Fin (2 ^ (ϑ + 1))) :
+  (multilinearWeight r i) = (multilinearWeight (r := Fin.init r) (i :=
+    ⟨Nat.getLowBits (numLowBits := ϑ) (n := i), by simp [Nat.getLowBits_lt_two_pow]⟩)
+  ) *
+    (if i.val.testBit (ϑ) then (r (Fin.last ϑ)) else (1 - r (Fin.last ϑ))) := by
+  simp only [multilinearWeight, Fin.prod_univ_castSucc]
+  simp_rw [Nat.testBit_eq_getBit, Nat.getBit_of_lowBits]
+  simp only [Fin.coe_castSucc, Fin.val_last, mul_ite, Fin.is_lt, ↓reduceIte]
+  rfl
+
+omit [Fintype F] [DecidableEq F] in
+/-- **Lower Half Weight**:
+If `i < 2^n`, the tensor weight splits into the weight of the lower bits (using the prefix of r)
+multiplied by `(1 - r_n)` (since the n-th bit is 0). -/
+lemma multilinearWeight_succ_lower_half {n : ℕ}
+    (r : Fin (n + 1) → F) (i : Fin (2 ^ (n + 1)))
+    (h_lt : i.val < 2 ^ n) :
+    multilinearWeight r i =
+    multilinearWeight (Fin.init r) ⟨i.val, by exact h_lt⟩ * (1 - r (Fin.last n)) := by
+  -- 1. Apply the generic successor splitting lemma
+  rw [multilinearWeight_succ]
+  -- 2. Simplify the High Bit Term
+  -- Since i < 2^n, the n-th bit is 0
+  have h_bit_zero : i.val.testBit n = false := by
+    rw [Nat.testBit_eq_false_of_lt]
+    exact h_lt
+  simp only [h_bit_zero, Bool.false_eq_true, ↓reduceIte]
+  -- 3. Simplify the Low Bits Term
+  -- Since i < 2^n, getting the low n bits just returns i itself
+  congr 2
+  apply Fin.eq_of_val_eq
+  simp_rw [Nat.getLowBits_eq_mod_two_pow]
+  let i_mod_2_pow_n : i.val % (2 ^ n) = i.val := by
+    rw [Nat.mod_eq_of_lt (h := h_lt)]
+  simp only [i_mod_2_pow_n]
+
+omit [Fintype F] [DecidableEq F] in
+/-- **Upper Half Weight**:
+If `i = j + 2^n` (where `j < 2^n`), the tensor weight splits into the weight of `j`
+(using the prefix of r) multiplied by `r_n` (since the n-th bit is 1).
+-/
+lemma multilinearWeight_succ_upper_half {n : ℕ}
+    (r : Fin (n + 1) → F) (i : Fin (2 ^ (n + 1)))
+    (j : Fin (2 ^ n)) (h_eq : i.val = j.val + 2 ^ n) :
+    multilinearWeight r i =
+    multilinearWeight (Fin.init r) j * (r (Fin.last n)) := by
+  rw [multilinearWeight_succ]
+  -- 2. Simplify the High Bit Term
+  -- i = j + 2^n, so the n-th bit is 1 (since j < 2^n)
+  have h_bit_one : i.val.testBit n = true := by
+    rw [h_eq]; simp_rw [Nat.testBit_eq_getBit]
+    rw [Nat.getBit_1_of_ge_two_pow_and_lt_two_pow_succ (h_ge_two_pow := by omega)
+      (h_lt_two_pow_succ := by omega)]
+  simp only [h_bit_one, if_true]
+  -- 3. Simplify the Low Bits Term
+  -- Low n bits of (j + 2^n) is just j
+  congr 2
+  apply Fin.eq_of_val_eq
+  simp only [h_eq]
+  rw [Nat.getLowBits_eq_mod_two_pow]
+  let j_mod_2_pow_n : j.val % (2 ^ n) = j.val := by
+    rw [Nat.mod_eq_of_lt (h := j.isLt)]
+  simp only [Nat.add_mod_right]
+  simp only [j_mod_2_pow_n]
+
 /-- Linear combination of the rows of `u` according to the tensor product of `r`:
 `[tensor_product r i] ·|u₀|`
                       `|u₁|`

ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean

@@ -164,11 +164,7 @@ theorem exists_basepoint_with_large_line_prob_aux {ι : Type} [Fintype ι] [None
   let P2 : ENNReal := Pr_{let a ←$ᵖ U; let z ←$ᵖ F}[good (a.1 + z • dir)]
   -- Expand the joint probability as an average over basepoints.
   have hP2 : P2 = ∑' a : U, ($ᵖ U) a * lineProb a := by
-    simpa [P2, lineProb] using
-      (prob_tsum_form_split_first (D := ($ᵖ U))
-        (D_rest := fun a : U => (do
-          let z ← $ᵖ F
-          return good (a.1 + z • dir))))
+    simp [P2, lineProb, prob_tsum_form_split_first]
   -- Swap the order of sampling the basepoint and line parameter.
   have hswap :
       (do
@@ -191,11 +187,7 @@ theorem exists_basepoint_with_large_line_prob_aux {ι : Type} [Fintype ι] [None
     have hsplit :
         Pr_{let z ←$ᵖ F; let a ←$ᵖ U}[good (a.1 + z • dir)] =
           ∑' z : F, ($ᵖ F) z * Pr_{let a ←$ᵖ U}[good (a.1 + z • dir)] := by
-      simpa using
-        (prob_tsum_form_split_first (D := ($ᵖ F))
-          (D_rest := fun z : F => (do
-            let a ← $ᵖ U
-            return good (a.1 + z • dir))))
+      simp
     rw [hsplit]
     have hconst :
         ∀ z : F, Pr_{let a ←$ᵖ U}[good (a.1 + z • dir)] = Pr_{let a ←$ᵖ U}[good a.1] := by
@@ -214,14 +206,15 @@ theorem exists_basepoint_with_large_line_prob_aux {ι : Type} [Fintype ι] [None
     simp only [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul]
   -- Rewrite the original hypothesis as a lower bound on `P2`.
   have hP2_gt : P2 > ε := by
-    simpa [hP2_eq] using hprob
+    rw [hP2_eq]
+    exact hprob
   -- Rewrite that lower bound using the weighted-sum formula for `P2`.
   have hsum_gt : (∑' a : U, ($ᵖ U) a * lineProb a) > ε := by
     simpa [hP2] using hP2_gt
   -- Choose a basepoint whose line probability exceeds the threshold.
   rcases exists_of_weighted_avg_gt ($ᵖ U) lineProb (ε : ENNReal) hsum_gt with ⟨a, ha⟩
   refine ⟨a, ?_⟩
-  simpa [lineProb] using ha
+  exact ha
 
 theorem exists_basepoint_with_large_line_prob {ι : Type} [Fintype ι] [Nonempty ι]
     {F : Type} [Field F] [Fintype F] [DecidableEq F]

ArkLib/Data/CodingTheory/ReedSolomon.lean

@@ -440,6 +440,19 @@ lemma constantCode_eq_ofNat_zero_iff [Nonempty ι] :
 lemma wt_constantCode [DecidableEq F] [NeZero x] :
   wt (constantCode x ι) = Fintype.card ι := by unfold constantCode wt; aesop
 
+instance instNontrivial {F ι : Type*} {n : ℕ} [Field F] [Fintype ι] {α : ι ↪ F}
+  [NeZero n] [Nonempty ι] : Nontrivial (ReedSolomon.code α n) := by
+  let c1 := constantCode (1 : F) ι
+  have h_c1_mem : c1 ∈ ReedSolomon.code α n := constantCode_mem_code
+  have h_c1_ne_zero : c1 ≠ 0 := by
+    by_contra h_c1_eq_zero
+    rw [constantCode_eq_ofNat_zero_iff] at h_c1_eq_zero
+    have h_1_ne_0 : (1 : F) ≠ (0 : F) := by exact one_ne_zero (α := F)
+    exact h_1_ne_0 h_c1_eq_zero
+  refine ⟨⟨0, Submodule.zero_mem _⟩, ⟨c1, h_c1_mem⟩, ?_⟩
+  simp only [ne_eq, Subtype.mk_eq_mk]
+  exact h_c1_ne_zero.symm
+
 end
 
 open Finset in