feat: soundness of FRI-Binius protocols

ArkLib.lean

@@ -112,11 +112,13 @@ 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.Soundness
 import ArkLib.ProofSystem.Binius.BinaryBasefold.Spec
 import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps
 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
@@ -160,6 +162,7 @@ import ArkLib.ToMathlib.Data.IndexedBinaryTree.Basic
 import ArkLib.ToMathlib.Data.IndexedBinaryTree.Equiv
 import ArkLib.ToMathlib.Data.IndexedBinaryTree.Lemmas
 import ArkLib.ToMathlib.Finset.Basic
+import ArkLib.ToMathlib.MvPolynomial.Equiv
 import ArkLib.ToVCVio.DistEq
 import ArkLib.ToVCVio.Lemmas
 import ArkLib.ToVCVio.Oracle

ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean

@@ -1159,6 +1159,21 @@ noncomputable def iteratedQuotientMap [NeZero ℓ] (i : Fin r) {destIdx : Fin r}
         _ = (normalizedW 𝔽q β destIdx).eval u := by rw [h_comp_eq]
   exact ⟨y, h_mem⟩
 
+omit [DecidableEq 𝔽q] hF₂ in
+lemma iteratedQuotientMap_congr_k
+    (i : Fin r) {destIdx : Fin r} {k₁ k₂ : ℕ}
+    (hk : k₁ = k₂)
+    (h_destIdx₁ : destIdx.val = i.val + k₁)
+    (h_destIdx₂ : destIdx.val = i.val + k₂)
+    (h_destIdx_le : destIdx.val ≤ ℓ)
+    (x : sDomain 𝔽q β h_ℓ_add_R_rate i) :
+    iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate
+      (i := i) (k := k₁) (h_destIdx := h_destIdx₁) (h_destIdx_le := h_destIdx_le) x
+    =
+    iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate
+      (i := i) (k := k₂) (h_destIdx := h_destIdx₂) (h_destIdx_le := h_destIdx_le) x := by
+  subst hk; rfl
+
 omit [DecidableEq 𝔽q] [NeZero ℓ] hF₂ h_β₀_eq_1 in
 /-- The evaluation of qMap on an element from sDomain i belongs to sDomain (i+1).
 This is a key property that qMap maps between successive domains. -/

ArkLib/Data/Misc/Basic.lean

@@ -28,6 +28,8 @@ def subtypeSumComplEquiv {α : Type*} {p : α → Prop} [DecidablePred p] :
 
 lemma fun_eta_expansion {α β : Type*} (f : α → β) : f = (fun x => f x) := rfl
 
+lemma fun_eta_expansion_apply {α β : Type*} (f : α → β) (x : α) : (f x) = (fun x => f x) x := rfl
+
 /-- Casting a function equals the function that casts its argument. -/
 lemma cast_fun_eq_fun_cast_arg.{u, v} {A B : Type u} {C : Type v} (h : A = B) (f : A → C) :
     cast (congrArg (· → C) h) f = fun x => f (cast h.symm x) := by

ArkLib/OracleReduction/Basic.lean

@@ -772,6 +772,15 @@ end IsSingleRound
 def FullTranscript.mk1 {pSpec : ProtocolSpec 1} (msg0 : pSpec.«Type» 0) :
     FullTranscript pSpec := fun | ⟨0, _⟩ => msg0
 
+@[simp]
+theorem FullTranscript.mk1_eq_snoc {pSpec : ProtocolSpec 1} (msg0 : pSpec.«Type» 0) :
+      FullTranscript.mk1 msg0 = (default : pSpec.Transcript 0).concat msg0 := by
+  unfold FullTranscript.mk1 Transcript.concat
+  simp only [default, Fin.isValue]
+  funext i
+  have hi : i = 0 := by omega
+  subst hi; simp [Fin.snoc]
+
 @[inline, reducible]
 def FullTranscript.mk2 {pSpec : ProtocolSpec 2} (msg0 : pSpec.«Type» 0) (msg1 : pSpec.«Type» 1) :
     FullTranscript pSpec := fun | ⟨0, _⟩ => msg0 | ⟨1, _⟩ => msg1