diff --git a/ArkLib.lean b/ArkLib.lean index 8f5e8c4c9..ce15fe61b 100644 --- a/ArkLib.lean +++ b/ArkLib.lean @@ -140,6 +140,7 @@ import ArkLib.OracleReduction.Security.RoundByRound import ArkLib.OracleReduction.Security.SpecialSoundness import ArkLib.OracleReduction.Security.StateRestoration import ArkLib.OracleReduction.VectorIOR +import ArkLib.ProofSystem.BatchedFri.Security import ArkLib.ProofSystem.BatchedFri.Spec.General import ArkLib.ProofSystem.BatchedFri.Spec.SingleRound import ArkLib.ProofSystem.Binius.BinaryBasefold.Basic @@ -191,6 +192,7 @@ import ArkLib.ToMathlib.Data.IndexedBinaryTree.Equiv import ArkLib.ToMathlib.Data.IndexedBinaryTree.Lemmas import ArkLib.ToMathlib.Finset.Basic import ArkLib.ToMathlib.Finsupp.Fin +import ArkLib.ToMathlib.List.Basic import ArkLib.ToMathlib.MvPolynomial.Equiv import ArkLib.ToMathlib.NumberTheory.PrattCertificate import ArkLib.ToMathlib.UInt.Equiv diff --git a/ArkLib/Data/CodingTheory/ProximityGap.lean b/ArkLib/Data/CodingTheory/ProximityGap.lean index c29be9b73..04565a3e4 100644 --- a/ArkLib/Data/CodingTheory/ProximityGap.lean +++ b/ArkLib/Data/CodingTheory/ProximityGap.lean @@ -117,8 +117,8 @@ noncomputable def δ_ε_proximityGap {α : Type} [DecidableEq α] [Nonempty α] (P : Finset (ι → α)) (C : Set (Finset (ι → α))) (δ ε : ℝ≥0) : Prop := ∀ S ∈ C, ∀ [Nonempty S], Xor' - ( Pr_{let x ← $ᵖ S}[Code.relHammingDistToCode x.1 P ≤ δ] = 1 ) - ( Pr_{let x ← $ᵖ S}[Code.relHammingDistToCode x.1 P ≤ δ] ≤ ε ) + ( Pr_{let x ←$ᵖ S}[Code.relHammingDistToCode x.1 P ≤ δ] = 1 ) + ( Pr_{let x ←$ᵖ S}[Code.relHammingDistToCode x.1 P ≤ δ] ≤ ε ) end section @@ -299,7 +299,7 @@ section open Polynomial open Polynomial.Bivariate -/-- Following the Proximity Gap paper this the Y-degree of +/-- Following the Proximity Gap paper this the Y-degree of a trivariate polynomial `Q`. -/ def D_Y (Q : F[Z][X][Y]) : ℕ := Bivariate.natDegreeY Q @@ -352,7 +352,7 @@ structure ModifiedGuruswami D_YZ Q ≤ n * (m + 1/(2 : ℚ))^3 / (6 * Real.sqrt ((k + 1) / n)) /-- The claim 5.4 from the proximity gap paper. - It essentially claims that there exists + It essentially claims that there exists a soultion to the Guruswami-Sudan constraints above. -/ lemma modified_guruswami_has_a_solution @@ -376,7 +376,7 @@ noncomputable def coeffs_of_close_proximity (ωs : Fin n ↪ F) (δ : ℚ) (u₀ open Polynomial omit [DecidableEq (RatFunc F)] in -/-- There exists a `δ`-close polynomial `P_z` for each `z` +/-- There exists a `δ`-close polynomial `P_z` for each `z` from the set `S`. -/ lemma exists_Pz_of_coeffs_of_close_proximity @@ -397,7 +397,7 @@ lemma exists_Pz_of_coeffs_of_close_proximity by convert dist; rw [←hS.2]; rfl ⟩⟩ -/-- The `δ`-close polynomial `Pz` for each `z` +/-- The `δ`-close polynomial `Pz` for each `z` from the set `S` (`coeffs_of_close_proximity`). -/ noncomputable def Pz @@ -411,7 +411,7 @@ noncomputable def Pz /-- Proposition 5.5 from the proximity gap paper. There exists a subset `S'` of the set `S` and a bivariate polynomial `P(X, Z)` that matches - `Pz` on that set. + `Pz` on that set. -/ lemma exists_a_set_and_a_matching_polynomial (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) @@ -492,14 +492,14 @@ noncomputable def H : F[Z][X] := (exists_factors_with_large_common_root_set k δ x₀ h_gs).choose_spec.choose /-- An important property of the polynomial - `H` extracted from claim 5.7 is that it is + `H` extracted from claim 5.7 is that it is irreducible. -/ lemma irreducible_H (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) : Irreducible (H k δ x₀ h_gs) := by - have h := Classical.choose_spec <| Classical.choose_spec + have h := Classical.choose_spec <| Classical.choose_spec (exists_factors_with_large_common_root_set (δ := δ) (x₀ := x₀) k h_gs) simp [H] rcases h with ⟨_, h, _⟩ @@ -507,7 +507,7 @@ lemma irreducible_H open AppendixA.ClaimA2 in /-- The claim 5.8 from the proximity gap paper. - States that the approximate solution is + States that the approximate solution is actually a solution. This version of the claim is stated in terms of coefficients. @@ -515,18 +515,18 @@ open AppendixA.ClaimA2 in lemma approximate_solution_is_exact_solution_coeffs (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) : ∀ t ≥ k, - α' - x₀ - (R k δ x₀ h_gs) - (irreducible_H k h_gs) - t - = + α' + x₀ + (R k δ x₀ h_gs) + (irreducible_H k h_gs) + t + = (0 : AppendixA.𝕃 (H k δ x₀ h_gs)) := by sorry open AppendixA.ClaimA2 in /-- The claim 5.8 from the proximity gap paper. - States that the approximate solution is + States that the approximate solution is actually a solution. This version is in terms of polynomials. -/ @@ -538,7 +538,7 @@ lemma approximate_solution_is_exact_solution_coeffs' if t ≥ k then (0 : AppendixA.𝕃 (H k δ x₀ h_gs)) else PowerSeries.coeff _ t - (γ' + (γ' x₀ (R k (x₀ := x₀) (δ := δ) h_gs) (irreducible_H k h_gs))) := by @@ -546,7 +546,7 @@ lemma approximate_solution_is_exact_solution_coeffs' open AppendixA.ClaimA2 in /-- Claim 5.9 from the proximity gap paper. - States that the solution `γ` is linear in + States that the solution `γ` is linear in the variable `Z`. -/ lemma solution_gamma_is_linear_in_Z @@ -560,7 +560,7 @@ lemma solution_gamma_is_linear_in_Z (Polynomial.C Polynomial.X) * (Polynomial.map Polynomial.C v₁) ) := by sorry -/-- The linear represenation of the solution `γ` +/-- The linear represenation of the solution `γ` extracted from the claim 5.9. -/ noncomputable def P @@ -569,7 +569,7 @@ noncomputable def P : F[Z][X] := let v₀ := Classical.choose (solution_gamma_is_linear_in_Z k (δ := δ) (x₀ := x₀) h_gs) - let v₁ := Classical.choose + let v₁ := Classical.choose (Classical.choose_spec <| solution_gamma_is_linear_in_Z k (δ := δ) (x₀ := x₀) h_gs) ( (Polynomial.map Polynomial.C v₀) + @@ -583,7 +583,7 @@ lemma gamma_eq_P (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) : γ' x₀ (R k δ x₀ h_gs) (irreducible_H k (x₀ := x₀) (δ := δ) h_gs) = - AppendixA.polyToPowerSeries𝕃 _ + AppendixA.polyToPowerSeries𝕃 _ (P k δ x₀ h_gs) := by sorry /-- The set `S'_x` from the proximity gap paper (just before claim 5.10). @@ -594,7 +594,7 @@ noncomputable def matching_set_at_x (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) (x : Fin n) : Finset F := @Set.toFinset _ {z : F | ∃ h : z ∈ matching_set k ωs δ u₀ u₁ h_gs, - u₀ x + z * u₁ x = + u₀ x + z * u₁ x = (Pz (matching_set_is_a_sub_of_coeffs_of_close_proximity k h_gs h)).eval (ωs x)} sorry /-- Claim 5.10 of the proximity gap paper. @@ -618,7 +618,7 @@ lemma solution_gamma_matches_word_if_subset_large := by sorry /-- Claim 5.11 from the proximity gap paper. - There exists a set of points `{x₀,...,x_{k+1}}` + There exists a set of points `{x₀,...,x_{k+1}}` such that the sets S_{x_j} satisfy the condition in the claim 5.10. -/ @@ -641,4 +641,377 @@ lemma exists_points_with_large_matching_subset end ProximityGapSection5 end +section ProximityGapSection6 +variable {F : Type} [Field F] [Fintype F] [DecidableEq F] [DecidableEq (RatFunc F)] +variable {n k m : ℕ} [NeZero n] + +/-- An affine curve parameterized by the field + and whose defining vectors are the vectors + `u 0, ..., u (n - 1)`. +-/ +def curve {l : ℕ} (u : Fin l → Fin n → F) (z : F) : Fin n → F := + ∑ i, z ^ i.1 • u i + +/-- The parameters for which the curve points are + `δ`-close to a set `V` (typically, a linear code). + The set `S` from the proximity gap paper. +-/ +noncomputable def coeffs_of_close_proximity_curve {l : ℕ} + (δ : ℚ) (u : Fin l → Fin n → F) (V : Finset (Fin n → F)) : Finset F := + have : Fintype { z | δᵣ(curve u z, V) ≤ δ} := by infer_instance + @Set.toFinset _ { z | δᵣ(curve u z, V) ≤ δ} this + +/-- If the set of points `δ`-close to the code `V` has + at least `n * l + 1` points then + there exists a curve defined by vectors `v` from `V` + such that the points of `curve u` and `curve v` + are `δ`-close with the same parameters. + Moreover, `u` and `v` differ at at most `δ * n` + positions. +-/ +theorem large_agreement_set_on_curve_implies_correlated_agreement {l : ℕ} + {rho : ℚ} + {δ : ℚ} + {V : Finset (Fin n → F)} + (hδ : δ ≤ (1 - rho) / 2) + {u : Fin l → Fin n → F} + (hS : n * l < (coeffs_of_close_proximity_curve δ u V).card) + : + coeffs_of_close_proximity_curve δ u V = F ∧ + ∃ (v : Fin l → Fin n → F), + ∀ z, δᵣ(curve u z, curve v z) ≤ δ ∧ + ({ x : Fin n | Finset.image u ≠ Finset.image v } : Finset _).card ≤ δ * n := by + sorry + +/-- The distance bound from the proximity gap paper. +-/ +noncomputable def δ₀ (rho : ℚ) (m : ℕ) : ℝ := + 1 - Real.sqrt rho - Real.sqrt rho / (2 * m) + +/-- If the set of points on the curve defined by `u` + close to `V` has at least + `((1 + 1 / (2 * m)) ^ 7 * m ^ 7) / (3 * (Real.rpow rho (3 / 2 : ℚ))) + * n ^ 2 * l + 1` points then + there exist vectors `v` from `V` that + `(1 - δ) * n` close to vectors `u`. +-/ +theorem large_agreement_set_on_curve_implies_correlated_agreement' {l : ℕ} + [Finite F] + {m : ℕ} + {rho : ℚ} + {δ : ℚ} + (hm : 3 ≤ m) + {V : Finset (Fin n → F)} + (hδ : δ ≤ δ₀ rho m) + {u : Fin l → Fin n → F} + (hS : ((1 + 1 / (2 * m)) ^ 7 * m ^ 7) / (3 * (Real.rpow rho (3 / 2 : ℚ))) + * n ^ 2 * l < (coeffs_of_close_proximity_curve δ u V).card) + : + ∃ (v : Fin l → Fin n → F), + ∀ i, v i ∈ V ∧ + (1 - δ) * n ≤ ({x : Fin n | ∀ i, u i x = v i x} : Finset _).card := sorry + +section +open NNReal Finset Function + +open scoped BigOperators +open scoped ReedSolomonCode + +variable {l : ℕ} [NeZero l] + {ι : Type} [Fintype ι] [Nonempty ι] + {F : Type} [Field F] [Fintype F] [DecidableEq F] + + +open scoped Pointwise in +open scoped ProbabilityTheory in +open Uniform in +/-- +Lemma 6.3 in [BCIKS20]. + +Let `V` be a Reed–Solomon code of rate `ρ`, and let `U` be an affine subspace obtained by +translating a linear subspace `U'`. For a proximity parameter `δ` below the Johnson/Guruswami–Sudan +list-decoding bound (`0 < δ < 1 - √ρ`), suppose that a random point `u` sampled uniformly from `U` +is `δ`-close to `V` with probability strictly larger than the proximity-gap error bound `ε`. Then +every point of the underlying linear subspace `U'` is also `δ`-close to `V`. +-/ +theorem average_proximity_implies_proximity_of_linear_subspace [DecidableEq ι] [DecidableEq F] + {u : Fin (l + 2) → ι → F} {k : ℕ} {domain : ι ↪ F} {δ : ℝ≥0} + (hδ : δ ∈ Set.Ioo 0 (1 - (ReedSolomonCode.sqrtRate (k + 1) domain))) : + letI U' : Finset (ι → F) := + SetLike.coe (affineSpan F (Finset.univ.image (Fin.tail u))) |>.toFinset + letI U : Finset (ι → F) := u 0 +ᵥ U' + haveI : Nonempty U := sorry + letI ε : ℝ≥0 := ProximityGap.errorBound δ (k + 1) domain + letI V := ReedSolomon.code domain (k + 1) + Pr_{let u ←$ᵖ U}[δᵣ(u.1, V) ≤ δ] > ε → ∀ u' ∈ U', δᵣ(u', V) ≤ δ := by + sorry + +end + +end ProximityGapSection6 + +section ProximityGapSection7 + +variable {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] +variable {n k m : ℕ} + +namespace WeightedAgreement + +open NNReal Finset Function + +open scoped BigOperators + +section + +variable {n : Type} [Fintype n] [DecidableEq n] + +variable {ι : Type} [Fintype ι] [Nonempty ι] +variable {F : Type} [Field F] [Fintype F] [DecidableEq F] + +variable (C : Submodule F (n → F)) [DecidablePred (· ∈ C)] + (μ : ι → Set.Icc (0 : ℚ) 1) + +/-- Relative μ-agreement between words `u` and `v`. -/ +noncomputable def agree (u v : ι → F) : ℝ := + 1 / (Fintype.card ι) * ∑ i ∈ { i | u i = v i }, (μ i).1 + +/-- `μ`-agreement between a word and a set `V`. -/ +noncomputable def agree_set (u : ι → F) (V : Finset (ι → F)) [Nonempty V] : ℝ := + (Finset.image (agree μ u) V).max' (nonempty_coe_sort.1 (by aesop)) + +/-- Weighted size of a subdomain. -/ +noncomputable def mu_set (ι' : Finset ι) : ℝ := + 1/(Fintype.card ι) * ∑ i ∈ ι', (μ i).1 + +/-- `μ`-weighted correlated agreement. -/ +noncomputable def weightedCorrelatedAgreement + (C : Set (ι → F)) [Nonempty C] {k : ℕ} (U : Fin k → ι → F) : ℝ := + sSup {x | + ∃ D' ⊆ (Finset.univ (α := ι)), + x = mu_set μ D' ∧ + ∃ v : Fin k → ι → F, ∀ i, v i ∈ C ∧ ∀ j ∈ D', v i j = U i j + } + +open ReedSolomonCode + +instance {domain : ι ↪ F} {deg : ℕ} : Nonempty (finCarrier domain deg) := by + unfold finCarrier + apply Nonempty.to_subtype + simp [ReedSolomon.code] + exact Submodule.nonempty (Polynomial.degreeLT F deg) + +open ProbabilityTheory in +/-- Weighted correlated agreement over curves. + Take a Reed-Solomon code of length `ι` and degree `deg`, a proximity-error parameter +pair `(δ, ε)` and a curve generated by vectors `u`, such that the probability that a random +point on the curve is `δ`-close to Reed-Solomon code is at most `ε`. +Then, the words `u` have weighted correlated agreement. +-/ +theorem weighted_correlated_agreement_for_parameterized_curves + [DecidableEq ι] [Fintype ι] [DecidableEq F] [Fintype F] + {l : ℕ} + {k : ℕ} {u : Fin (l + 2) → ι → F} + {deg : ℕ} {domain : ι ↪ F} {δ : ℝ≥0} + {μ : ι → Set.Icc (0 : ℚ) 1} + {M : ℕ} + {α : ℝ≥0} + (hμ : ∀ i, ∃ n : ℤ, (μ i).1 = (n : ℚ) / (M : ℚ)) : + letI sqrtRate := ReedSolomonCode.sqrtRate deg domain + (hα : sqrtRate < α) → + (hα₁ : α < 1) → + letI ε := ProximityGap.errorBound δ deg domain + letI pr := + let curve := Curve.parametrisedCurveFinite u + Pr_{let u ←$ᵖ curve}[agree_set μ u (finCarrier domain deg) ≥ α] + (hproximity : pr > (l + 1 : NNReal) * ε) → + (h_additionally : pr ≥ + ENNReal.ofReal ( + ((l + 1) * (M * Fintype.card ι + 1) : ℝ) / (Fintype.card F : ℝ) + * + (1 / min (α - sqrtRate) (sqrtRate / 20) + 3 / sqrtRate) + ) + ) → + ∃ ι' : Finset ι, ∃ v : Fin (l + 2) → ι → F, + (∀ i, v i ∈ ReedSolomon.code domain deg) ∧ + mu_set μ ι' ≥ α ∧ + ∀ i, ∀ x ∈ ι', u i x = v i x := sorry + +/-- Weighted correlated agreement over curves. +Take a Reed-Solomon code of length `ι` and degree `deg`, a proximity-error parameter +pair `(δ, ε)` and a curve generated by vectors `u`, such that the probability that a random +point on the curve is `δ`-close to Reed-Solomon code is at most `ε`. +Then, the words `u` have weighted correlated agreement. + +Version with different bounds. +-/ +theorem weighted_correlated_agreement_for_parameterized_curves' + [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} + {deg : ℕ} {domain : ι ↪ F} {δ : ℝ≥0} + {μ : ι → Set.Icc (0 : ℚ) 1} + {M m : ℕ} + (hm : 3 ≤ m) + (hμ : ∀ i, ∃ n : ℤ, (μ i).1 = (n : ℚ) / (M : ℚ)) + {α : ℝ≥0} : + letI sqrtRate := ReedSolomonCode.sqrtRate deg domain + letI S : Finset F := { + z : F | agree_set μ (fun i ↦ ∑ j, z ^ j.1 * u j i) (finCarrier domain deg) ≥ α + } + (hα : sqrtRate * (1 + 1 / (2 * m : ℝ)) ≤ α) → + (hS : + Finset.card S > + max ((1 + 1 / (2 * m : ℝ))^7 * m^7 * (Fintype.card ι)^2 * (l + 1) / (3 * sqrtRate^3)) + ((2 * m + 1) * (M * Fintype.card ι + 1) * (l + 1) / sqrtRate.toReal) + ) → + ∃ v : Fin (l + 2) → ι → F, + (∀ i, v i ∈ ReedSolomon.code domain deg) ∧ + mu_set μ {i : ι | ∀ j, u j i = v j i} ≥ α := sorry + +open Uniform in +open scoped Pointwise in +open ProbabilityTheory in +/-- Weighted correlated agreement over affine spaces. +Take a Reed-Solomon code of length `ι` and degree `deg`, a proximity-error parameter +pair `(δ, ε)` and an affine space generated by vectors `u`, such that the probability that a random +point from the space is `δ`-close to Reed-Solomon code is at most `ε`. +Then, the words `u` have weighted correlated agreement. +-/ +theorem weighted_correlated_agreement_over_affine_spaces + [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} + {deg : ℕ} {domain : ι ↪ F} + {μ : ι → Set.Icc (0 : ℚ) 1} + {M : ℕ} + {α : ℝ≥0} : + letI sqrtRate := ReedSolomonCode.sqrtRate deg domain + (hα : sqrtRate < α) → + (hα₁ : α < 1) → + (hμ : ∀ i, ∃ n : ℤ, (μ i).1 = (n : ℚ) / (M : ℚ)) → + letI ε := ProximityGap.errorBound α deg domain + letI pr := + Pr_{let u ←$ᵖ (u 0 +ᵥ affineSpan F (Finset.univ.image (Fin.tail u)).toSet) + }[agree_set μ u (finCarrier domain deg) ≥ α] + pr > ε → + pr ≥ ENNReal.ofReal ( + ((M * Fintype.card ι + 1) : ℝ) / (Fintype.card F : ℝ) + * + (1 / min (α - sqrtRate) (sqrtRate / 20) + 3 / sqrtRate) + ) → + ∃ ι' : Finset ι, ∃ v : Fin (l + 2) → ι → F, + (∀ i, v i ∈ ReedSolomon.code domain deg) ∧ + mu_set μ ι' ≥ α ∧ + ∀ i, ∀ x ∈ ι', u i x = v i x := by sorry + +open scoped ProbabilityTheory in +open scoped Pointwise in +open Uniform in +/-- Weighted correlated agreement over affine spaces. +Take a Reed-Solomon code of length `ι` and degree `deg`, a proximity-error parameter +pair `(δ, ε)` and an affine space generated by vectors `u`, such that the probability that a random +point from the space is `δ`-close to Reed-Solomon code is at most `ε`. +Then, the words `u` have weighted correlated agreement. + +Version with different bounds. +-/ +theorem weighted_correlated_agreement_over_affine_spaces' + [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} + {deg : ℕ} {domain : ι ↪ F} + {μ : ι → Set.Icc (0 : ℚ) 1} + {α : ℝ≥0} + {M m : ℕ} + (hm : 3 ≤ m) + (hμ : ∀ i, ∃ n : ℤ, (μ i).1 = (n : ℚ) / (M : ℚ)) : + letI sqrtRate := ReedSolomonCode.sqrtRate deg domain + letI pr := + Pr_{let u ←$ᵖ (u 0 +ᵥ affineSpan F (Finset.univ.image (Fin.tail u)).toSet) + }[agree_set μ u (finCarrier domain deg) ≥ α] + (hα : sqrtRate * (1 + 1 / (2 * m : ℝ)) ≤ α) → + letI numeratorl : ℝ := (1 + 1 / (2 * m : ℝ))^7 * m^7 * (Fintype.card ι)^2 + letI denominatorl : ℝ := (3 * sqrtRate^3) * Fintype.card F + letI numeratorr : ℝ := (2 * m + 1) * (M * Fintype.card ι + 1) + letI denominatorr : ℝ := sqrtRate * Fintype.card F + pr > ENNReal.ofReal (max (numeratorl / denominatorl) (numeratorr / denominatorr)) → + ∃ v : Fin (l + 2) → ι → F, + (∀ i, v i ∈ ReedSolomon.code domain deg) ∧ + mu_set μ {i : ι | ∀ j, u j i = v j i} ≥ α := by sorry + +/-- +Lemma 7.5 in [BCIKS20]. + +This is the “list agreement on a curve implies correlated agreement” lemma. + +We are given two lists of functions `u, v : Fin (l + 2) → ι → F`, where each `v i` is a +Reed–Solomon codeword of degree `deg` over the evaluation domain `domain`. From these +lists we form the bivariate “curves” + +* `w x z = ∑ i, z^(i.1) * u i x`, +* `wtilde x z = ∑ i, z^(i.1) * v i x`. + +Fix a finite set `S' ⊆ F` with `S'.card > l + 1`, and a (product) measure `μ` on the +evaluation domain `ι`. Assume that for every `z ∈ S'` the one-dimensional functions +`w · z` and `wtilde · z` have agreement at least `α` with respect to `μ`. Then the set +of points `x` on which *all* coordinates agree, i.e. `u i x = v i x` for every `i`, +has μ-measure strictly larger than + +`α - (l + 1) / (S'.card - (l + 1))`. +-/ +lemma list_agreement_on_curve_implies_correlated_agreement_bound + [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} + {deg : ℕ} {domain : ι ↪ F} + {μ : ι → Set.Icc (0 : ℚ) 1} + {α : ℝ≥0} + {v : Fin (l + 2) → ι → F} + (hv : ∀ i, v i ∈ (ReedSolomon.code domain deg)) + {S' : Finset F} + (hS'_card : S'.card > l + 1) : + letI w (x : ι) (z : F) : F := ∑ i, z ^ i.1 * u i x + letI wtilde (x : ι) (z : F) : F := ∑ i, z ^ i.1 * v i x + (hS'_agree : ∀ z ∈ S', agree μ (w · z) (wtilde · z) ≥ α) → + mu_set μ {x : ι | ∀ i, u i x = v i x} > + α - ((l + 1) : ℝ) / (S'.card - (l + 1)) := by sorry + +/-- +Lemma 7.6 in [BCIKS20]. + +This is the “integral-weight” strengthening of the list-agreement-on-a-curve ⇒ +correlated-agreement bound. + +We have two lists of functions `u, v : Fin (l + 2) → ι → F`, where each `v i` is a +Reed–Solomon codeword of degree `deg` over the evaluation domain `domain`. From +these lists we form the bivariate “curves” +* `w x z = ∑ i, z^(i.1) * u i x`, +* `wtilde x z = ∑ i, z^(i.1) * v i x`. + +The domain `ι` is finite and is equipped with a weighted measure `μ`, where each +weight `μ i` is a rational with common denominator `M`. Let `S' ⊆ F` be a set of +field points with +* `S'.card > l + 1`, and +* `S'.card ≥ (M * Fintype.card ι + 1) * (l + 1)`. + +Assume that for every `z ∈ S'` the µ-weighted agreement between `w · z` and +`wtilde · z` is at least `α`. Then the µ-measure of the set of points where *all* +coordinates agree, i.e. where `u i x = v i x` for every `i`, is at least `α`: + +`mu_set μ {x | ∀ i, u i x = v i x} ≥ α`. +-/ +lemma sufficiently_large_list_agreement_on_curve_implies_correlated_agreement + [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} + {deg : ℕ} {domain : ι ↪ F} + {μ : ι → Set.Icc (0 : ℚ) 1} + {α : ℝ≥0} + {M : ℕ} + (hμ : ∀ i, ∃ n : ℤ, (μ i).1 = (n : ℚ) / (M : ℚ)) + {v : Fin (l + 2) → ι → F} + (hv : ∀ i, v i ∈ ReedSolomon.code domain deg) + {S' : Finset F} + (hS'_card : S'.card > l + 1) + (hS'_card₁ : S'.card ≥ (M * Fintype.card ι + 1) * (l + 1)) : + letI w (x : ι) (z : F) : F := ∑ i, z ^ i.1 * u i x + letI wtilde (x : ι) (z : F) : F := ∑ i, z ^ i.1 * v i x + (hS'_agree : ∀ z ∈ S', agree μ (w · z) (wtilde · z) ≥ α) → + mu_set μ {x : ι | ∀ i, u i x = v i x} ≥ α := by sorry +end + +end WeightedAgreement + +end ProximityGapSection7 + end ProximityGap diff --git a/ArkLib/Data/CodingTheory/ReedSolomon.lean b/ArkLib/Data/CodingTheory/ReedSolomon.lean index c177c8c9b..27e0e7e75 100644 --- a/ArkLib/Data/CodingTheory/ReedSolomon.lean +++ b/ArkLib/Data/CodingTheory/ReedSolomon.lean @@ -346,6 +346,15 @@ theorem minDist [Field F] [DecidableEq F] (inj : Function.Injective α) [NeZero end +noncomputable scoped instance {α : Type} (s : Set α) [inst : Finite s] : Fintype s + := Fintype.ofFinite _ + +open NNReal Finset Function Finset in +def finCarrier {ι : Type} [Fintype ι] + {F : Type} [Field F] [Fintype F] + (domain : ι ↪ F) (deg : ℕ) : Finset (ι → F) := + (ReedSolomon.code domain deg).carrier.toFinset + end ReedSolomonCode end diff --git a/ArkLib/ProofSystem/BatchedFri/Security.lean b/ArkLib/ProofSystem/BatchedFri/Security.lean new file mode 100644 index 000000000..1053da74c --- /dev/null +++ b/ArkLib/ProofSystem/BatchedFri/Security.lean @@ -0,0 +1,459 @@ +/- + Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. + Released under Apache 2.0 license as described in the file LICENSE. + Authors: František Silváši, Julian Sutherland, Ilia Vlasov + + [BCIKS20] refers to the paper "Proximity Gaps for Reed-Solomon Codes" by Eli Ben-Sasson, + Dan Carmon, Yuval Ishai, Swastik Kopparty, and Shubhangi Saraf. + + Using {https://eprint.iacr.org/2020/654}, version 20210703:203025. +-/ + +import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs + +import ArkLib.Data.CodingTheory.Basic +import ArkLib.Data.CodingTheory.Prelims +import ArkLib.Data.CodingTheory.ProximityGap +import ArkLib.Data.CodingTheory.ReedSolomon +import ArkLib.Data.Probability.Notation +import ArkLib.ProofSystem.BatchedFri.Spec.General +import ArkLib.ProofSystem.Fri.Domain +import ArkLib.ProofSystem.Fri.Spec.General +import ArkLib.ProofSystem.Fri.Spec.SingleRound +import ArkLib.OracleReduction.Security.Basic +import ToMathlib.Control.OptionT +import ArkLib.ToMathlib.List.Basic +import Mathlib.Algebra.Ring.NonZeroDivisors + +namespace Fri +section Fri + +open OracleComp OracleSpec ProtocolSpec CosetDomain +open NNReal Finset Function ProbabilityTheory + +variable {𝔽 : Type} [NonBinaryField 𝔽] [Finite 𝔽] [DecidableEq 𝔽] [Nontrivial 𝔽] +variable (D : Subgroup 𝔽ˣ) (n : ℕ) [DIsCyclicC : IsCyclicWithGen D] [DSmooth : SmoothPowerOfTwo n D] +variable (g : 𝔽ˣ) {k : ℕ} +variable (s : Fin (k + 1) → ℕ+) (d : ℕ+) +variable {i : Fin (k + 1)} + +noncomputable local instance : Fintype 𝔽 := Fintype.ofFinite _ + +instance {F : Type} [Field F] {a : F} [inst : NeZero a] : Invertible a where + invOf := a⁻¹ + invOf_mul_self := by field_simp [inst.out] + mul_invOf_self := by field_simp [inst.out] + +section Completeness + +def cosetEnum (s₀ : evalDomainSigma D g s i) (k_le_n : ∑ j', (s j').1 ≤ n) + (j : Fin (2 ^ (s i).1)) : { x // x ∈ evalDomainSigma D g s ↑i } := + let r : Domain.evalDomain D (n - ↑(s i)) := + Domain.domainEnum D + ⟨n - (s i).1, show n - (s i).1 < n + 1 by omega⟩ + ⟨j.1, + by + simp only + rw [Nat.sub_sub_eq_min] + apply lt_of_lt_of_le j.2 + rw [Nat.pow_le_pow_iff_right Nat.le.refl, Nat.le_min] + apply And.intro + · refine le_trans ?_ k_le_n + apply Finset.single_le_sum (f := fun i ↦ (s i).1) <;> simp + · exact Nat.le_refl _ + ⟩ + ⟨ + _, + CosetDomain.mul_root_of_unity D (sum_finRangeTo_le_sub_of_le k_le_n) s₀.2 r.2 + ⟩ + +def cosetG (s₀ : evalDomainSigma D g s i) : Finset (evalDomainSigma D g s i) := + if k_le_n : ∑ j', (s j').1 ≤ n + then + (Finset.univ).image (cosetEnum D n g s s₀ k_le_n) + else ∅ + +def pows (z : 𝔽) (ℓ : ℕ) : Matrix Unit (Fin ℓ) 𝔽 := + Matrix.of <| fun _ j => z ^ j.val + +def VDM (s₀ : evalDomainSigma D g s i) : + Matrix (Fin (2 ^ (s i : ℕ))) (Fin (2 ^ (s i : ℕ))) 𝔽 := + if k_le_n : (∑ j', (s j').1) ≤ n + then Matrix.vandermonde (fun j => (cosetEnum D n g s s₀ k_le_n j).1.1) + else 1 + +def cosetEnum' (s₀ : evalDomainSigma D g s i) (k_le_n : ∑ j', (s j').1 ≤ n) + (j : Fin (2 ^ (s i).1)) : cosetG D n g s s₀ := + ⟨ + cosetEnum D n g s s₀ k_le_n j, + by simp [cosetG, k_le_n] + ⟩ + +noncomputable def fin_equiv_coset (s₀ : evalDomainSigma D g s i) (k_le_n : ∑ j', (s j').1 ≤ n) : + (Fin (2 ^ (s i).1)) ≃ { x // x ∈ cosetG D n g s s₀ } := by + apply Equiv.ofBijective (cosetEnum' D n g s s₀ k_le_n) + unfold cosetEnum' cosetEnum + unfold Function.Bijective + apply And.intro + · intros a b + aesop + · rintro ⟨⟨y, h'⟩, h⟩ + simp only [evalDomain.eq_1, finRangeTo.eq_1, Domain.evalDomain.eq_1, Subtype.mk.injEq] + simp only [evalDomain.eq_1, finRangeTo.eq_1, Domain.evalDomain.eq_1, cosetG, k_le_n, + ↓reduceDIte, mem_image, mem_univ, cosetEnum, Subtype.mk.injEq, true_and] at h + exact h + +def invertibleDomain (s₀ : evalDomainSigma D g s i) : Invertible (VDM D n g s s₀) := by + haveI : NeZero (VDM D n g s s₀).det := by + constructor + unfold VDM + split_ifs with cond + · simp only [Matrix.det_vandermonde] + rw [Finset.prod_ne_zero_iff] + intros i' _ + rw [Finset.prod_ne_zero_iff] + intros j' h' + have : i' ≠ j' := by + rename_i a + simp_all only [mem_univ, mem_Ioi, ne_eq] + obtain ⟨val, property⟩ := s₀ + simp_all only [evalDomain, finRangeTo, Domain.evalDomain] + apply Aesop.BuiltinRules.not_intro + intro a + subst a + simp_all only [lt_self_iff_false] + intros contra + apply this + rw [sub_eq_zero, cosetEnum, cosetEnum] at contra + norm_cast at contra + rw [mul_left_cancel_iff] at contra + norm_cast at contra + rw [Function.Embedding.apply_eq_iff_eq, Fin.mk.injEq] at contra + exact Fin.eq_of_val_eq (id (Eq.symm contra)) + · simp + apply @Matrix.invertibleOfDetInvertible + +noncomputable def VDMInv (s₀ : evalDomainSigma D g s i) (k_le_n : ∑ j', (s j').1 ≤ n) : + Matrix (Fin (2 ^ (s i).1)) (cosetG D n g s s₀) 𝔽 := + Matrix.reindex (Equiv.refl _) (fin_equiv_coset D n g s s₀ k_le_n) + (invertibleDomain D n g s s₀).invOf + +lemma g_elem_zpower_iff_exists_nat {G : Type} [Group G] [Finite G] {gen g : G} : + g ∈ Subgroup.zpowers gen ↔ ∃ n : ℕ, g = gen ^ n ∧ n < orderOf gen := by + have := isOfFinOrder_of_finite gen + refine ⟨fun h ↦ ?p₁, ?p₂⟩ + · obtain ⟨k, h⟩ := Subgroup.mem_zpowers_iff.1 h + let k' := k % orderOf gen + have pow_pos : 0 ≤ k' := by apply Int.emod_nonneg; simp [*] + obtain ⟨n, h'⟩ : ∃ n : ℕ, n = k' := by rcases k' with k' | k' <;> [(use k'; grind); aesop] + use n + have : gen ^ n = gen ^ k := by have := zpow_mod_orderOf gen k; grind [zpow_natCast] + have : n < orderOf gen := by zify; rw [h']; apply Int.emod_lt; simp [isOfFinOrder_of_finite gen] + grind + · grind [Subgroup.npow_mem_zpowers] + + +open Matrix in +noncomputable def f_succ' + (f : evalDomainSigma D g s i → 𝔽) (z : 𝔽) (k_le_n : ∑ j', ↑(s j') ≤ n) + (s₀' : evalDomainSigma D g s (i.1 + 1)) : 𝔽 := + have : + ∃ s₀ : evalDomain D g (∑ j' ∈ finRangeTo (i.1), ↑(s j')), + s₀.1 ^ (2 ^ (s i).1) = s₀'.1 := by + have h := s₀'.2 + simp only [evalDomain] at h + have : + ((g ^ 2 ^ ∑ j' ∈ finRangeTo (↑i + 1), (s j').1))⁻¹ * s₀'.1 ∈ + Domain.evalDomain D (∑ j' ∈ finRangeTo (↑i + 1), ↑(s j')) + := by + aesop_reconcile + simp only [Domain.evalDomain] at this + rw [g_elem_zpower_iff_exists_nat] at this + rcases this with ⟨m, this⟩ + have m_lt := this.2 + have := eq_mul_of_inv_mul_eq this.1 + iterate 2 rw [sum_finRangeTo_add_one, Nat.pow_add, pow_mul] at this + rw [pow_right_comm _ _ m] at this + use + ⟨ + (g ^ 2 ^ ∑ j' ∈ finRangeTo ↑i, (s j').1) * + ((DIsCyclicC.gen ^ 2 ^ ∑ j' ∈ finRangeTo ↑i, (s j').1) ^ m), + by + have := fun X₁ X₂ X₃ ↦ @mem_leftCoset_iff.{0} 𝔽ˣ _ X₁ X₂ X₃ + reconcile + erw + [ + evalDomain, this, ←mul_assoc, inv_mul_cancel, + one_mul, Domain.evalDomain, SetLike.mem_coe + ] + exact Subgroup.npow_mem_zpowers _ _ + ⟩ + simp only [this, mul_pow] + rfl + let s₀ := Classical.choose this + (pows z _ *ᵥ VDMInv D n g s s₀ k_le_n *ᵥ Finset.restrict (cosetG D n g s s₀) f) () + +/-- This theorem asserts that given an appropriate codeword, + `f` of an appropriate Reed-Solomon code, the result of honestly folding the corresponding + polynomial is then itself a member of the next Reed-Solomon code. + + Corresponds to Claim 8.1 of [BCIKS20] -/ +lemma fri_round_consistency_completeness + {f : ReedSolomon.code (domainEmb D g (i := ∑ j' ∈ finRangeTo i, s j')) + (2 ^ (n - (∑ j' ∈ finRangeTo i, (s j' : ℕ))))} + {z : 𝔽} + (k_le_n : ∑ j', ↑(s j') ≤ n) + : + f_succ' D n g s f.val z k_le_n ∈ + (ReedSolomon.code + (CosetDomain.domainEmb D g) + (2 ^ (n - (∑ j' ∈ finRangeTo (i.1 + 1), (s j' : ℕ)))) + ).carrier + := by sorry + +end Completeness + +section Soundness + +variable (domain_size_cond : (2 ^ (∑ i, (s i : ℕ))) * d ≤ 2 ^ n) + +/-- Affine space: {g | ∃ x : Fin t.succ → 𝔽, x 0 = 1 ∧ g = ∑ i, x i • f i } +-/ +def Fₛ {ι : Type} [Fintype ι] {t : ℕ} (f : Fin t.succ → (ι → 𝔽)) : AffineSubspace 𝔽 (ι → 𝔽) := + f 0 +ᵥ affineSpan 𝔽 (Finset.univ.image (f ∘ Fin.succ)) + +noncomputable def correlated_agreement_density {ι : Type} [Fintype ι] + (Fₛ : AffineSubspace 𝔽 (ι → 𝔽)) (V : Submodule 𝔽 (ι → 𝔽)) : ℝ := + let Fc := Fₛ.carrier.toFinset + let Vc := V.carrier.toFinset + (Fc ∩ Vc).card / Fc.card + +open Polynomial + +noncomputable def oracleImpl + (l : ℕ) (z : Fin (k + 1) → 𝔽) (f : (CosetDomain.evalDomain D g 0) → 𝔽) : + QueryImpl + ([]ₒ ++ₒ ([Spec.FinalOracleStatement D g s]ₒ ++ₒ [(Spec.QueryRound.pSpec D g l).Message]ₒ)) + (OracleComp [(Spec.QueryRound.pSpec D g l).Message]ₒ) where + impl := + fun q ↦ + match q with + | query (.inl i) _ => PEmpty.elim i + | query (.inr (.inl i)) dom => + let f0 := Lagrange.interpolate Finset.univ (fun v => v.1.1) f + let chals : List (Fin (k + 1) × 𝔽) := + ((List.finRange (k + 1)).map (fun i => (i, z i))).take i.1 + let fi : 𝔽[X] := List.foldl (fun f (i, α) => Polynomial.foldNth (s i) f α) f0 chals + if h : i.1 = k + 1 + then pure <| by + simp only + [ + OracleSpec.range, OracleSpec.append, + OracleInterface.toOracleSpec, Spec.FinalOracleStatement + ] + unfold OracleInterface.Response Spec.instOracleInterfaceFinalOracleStatement + simp [h] + unfold OracleInterface.instDefault Spec.FinalOracleStatement + rw [h] + simp + exact fi + else pure <| by + simp only + [ + OracleSpec.range, OracleSpec.append, + OracleInterface.toOracleSpec, Spec.FinalOracleStatement + ] + unfold OracleInterface.Response Spec.instOracleInterfaceFinalOracleStatement + simp [h] + simp only + [ + OracleSpec.domain, OracleSpec.append, + OracleInterface.toOracleSpec, Spec.FinalOracleStatement + ] at dom + unfold OracleInterface.Query Spec.instOracleInterfaceFinalOracleStatement at dom + simp only [h, ↓reduceDIte] at dom + exact fi.eval dom.1.1 + | query (.inr (.inr i)) t => OracleComp.lift (query i t) + +instance {g : 𝔽ˣ} {l : ℕ} : [(Spec.QueryRound.pSpec D g l).Message]ₒ.FiniteRange where + range_inhabited' := by + intros i + unfold Spec.QueryRound.pSpec MessageIdx at i + have : i.1 = 0 := by omega + have h := this ▸ i.2 + simp at h + range_fintype' := by + intros i + unfold Spec.QueryRound.pSpec MessageIdx at i + have : i.1 = 0 := by omega + have h := this ▸ i.2 + simp at h + +open ENNReal in +noncomputable def εC + (𝔽 : Type) [Finite 𝔽] (n : ℕ) {k : ℕ} (s : Fin (k + 1) → ℕ+) (m : ℕ) (ρ_sqrt : ℝ≥0) : ℝ≥0∞ := + ENNReal.ofReal <| + (m + (1 : ℚ)/2)^7 * (2^n)^2 + / ((2 * ρ_sqrt ^ 3) * (Fintype.card 𝔽)) + + (∑ i, 2 ^ (s i).1) * (2 * m + 1) * (2 ^ n + 1) / (Fintype.card 𝔽 * ρ_sqrt) + +open ENNReal in +/-- Corresponds to Claim 8.2 of [BCIKS20] -/ +lemma fri_query_soundness + {t : ℕ} + {α : ℝ} + (f : Fin t.succ → (CosetDomain.evalDomain D g 0 → 𝔽)) + (h_agreement : + correlated_agreement_density + (Fₛ f) + (ReedSolomon.code (CosetDomain.domainEmb (i := 0) D g) (2 ^ n)) + ≤ α) + {m : ℕ} + (m_ge_3 : m ≥ 3) + : + let ρ_sqrt := + ReedSolomonCode.sqrtRate + (2 ^ n) + (CosetDomain.domainEmb (i := 0) D g) + let α0 : ℝ≥0∞ := ENNReal.ofReal (max α (ρ_sqrt * (1 + 1 / (2 * (m : ℝ≥0))))) + let εQ (x : Fin t → 𝔽) + (z : Fin (k + 1) → 𝔽) := + Pr_{let samp ←$ᵖ (CosetDomain.evalDomain D g 0)}[ + [ + fun _ => True | + ( + (do + simulateQ + (oracleImpl D g s 1 z (fun v ↦ f 0 v + ∑ i, x i * f i.succ v)) + ( + ( + Fri.Spec.QueryRound.queryVerifier D g + (n := n) s + (by + apply Spec.round_bound (d := d) + transitivity + · exact domain_size_cond + · apply pow_le_pow (by decide) (by decide) + simp + ) + 1 + ).verify + z + (fun i => + by + simpa only + [ + Spec.QueryRound.pSpec, Challenge, + show i.1 = 0 by omega, Fin.isValue, + Fin.vcons_zero + ] using fun _ => samp + ) + ) + ) + ) + ] = 1 + ] + Pr_{let x ←$ᵖ (Fin t → 𝔽); let z ←$ᵖ (Fin (k + 1) → 𝔽)}[ εQ x z > α0 ] ≤ εC 𝔽 n s m ρ_sqrt + := by sorry + +instance instFinRangeOfAppend {m n : ℕ} {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} + [FiniteRange [pSpec₁.Challenge]ₒ] [FiniteRange [pSpec₂.Challenge]ₒ] : + FiniteRange [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ := sorry + +-- set_option diagnostics true +instance {t l : ℕ} : + ([]ₒ ++ₒ + [((BatchedFri.Spec.BatchingRound.batchSpec 𝔽 t) ++ₚ + (Spec.pSpecFold D g k s ++ₚ Spec.FinalFoldPhase.pSpec 𝔽 ++ₚ + Spec.QueryRound.pSpec D g l)).Challenge]ₒ).FiniteRange := sorry + -- refine @OracleSpec.instFiniteRangeSumAppend (h₁ := inferInstance) (h₂ := ?_) .. + -- refine @instFinRangeOfAppend _ _ _ _ ?_ ?_ + -- · unfold BatchedFri.Spec.BatchingRound.batchSpec Challenge OracleInterface.toOracleSpec + -- simp only [Fin.vcons_fin_zero, Nat.reduceAdd, ChallengeIdx] + -- constructor + -- · intros i + -- unfold OracleSpec.range + -- simp only + -- rcases i with ⟨i, h⟩ + -- have : i = 0 := by omega + -- subst this + -- simp + -- unfold OracleInterface.Response challengeOracleInterface + -- simp only + -- unfold Challenge + -- simp + -- haveI : Inhabited 𝔽 := ⟨0⟩ + -- infer_instance + -- · intros i + -- unfold OracleSpec.range + -- simp only + -- rcases i with ⟨i, h⟩ + -- have : i = 0 := by omega + -- subst this + -- simp + -- unfold OracleInterface.Response challengeOracleInterface + -- simp only + -- unfold Challenge + -- simp + -- haveI : Inhabited 𝔽 := ⟨0⟩ + -- infer_instance + -- · refine @instFinRangeOfAppend _ _ _ _ ?_ ?_ + -- · refine @instFinRangeOfAppend _ _ _ _ ?_ ?_ + -- unfold Spec.pSpecFold Challenge OracleInterface.toOracleSpec + -- constructor + -- · intros i + -- unfold OracleSpec.range + -- simp only + -- rcases i with ⟨i, h⟩ + -- have : i = 0 := by omega + -- subst this + -- simp + -- unfold OracleInterface.Response challengeOracleInterface + -- simp only + -- unfold Challenge + -- simp + -- haveI : Inhabited 𝔽 := ⟨0⟩ + -- infer_instance + + + + + + + + + -- refine { range_inhabited' := ?_, range_fintype' := ?_ } + -- refine fun i ↦ ?_ + -- rcases i with i | i + -- · rcases i + -- · + +open ENNReal in +/-- Corresponds to Claim 8.3 of [BCIKS20] -/ +lemma fri_soundness + {t l m : ℕ} + (f : Fin t.succ → (CosetDomain.evalDomain D g 0 → 𝔽)) + (m_ge_3 : m ≥ 3) + : + let ρ_sqrt := + ReedSolomonCode.sqrtRate + (2 ^ n) + (CosetDomain.domainEmb (i := 0) D g) + let α : ℝ≥0 := (ρ_sqrt * (1 + 1 / (2 * (m : ℝ≥0)))) + (∃ prov : OracleProver (WitOut := Unit) .., + [fun _ => True | + OracleReduction.run () f () + ⟨ + prov, + (BatchedFri.Spec.batchedFRIreduction (n := n) D g k s d domain_size_cond l t).verifier + ⟩ + ] > εC 𝔽 n s m ρ_sqrt + α ^ l) → + ProximityGap.correlatedAgreement + (ReedSolomon.code (CosetDomain.domainEmb (i := 0) D g) (2 ^ n)).carrier + (1 - α) f := by + sorry + +end Soundness + +end Fri +end Fri diff --git a/ArkLib/ProofSystem/BatchedFri/Spec/General.lean b/ArkLib/ProofSystem/BatchedFri/Spec/General.lean index f87a8f861..802554e64 100644 --- a/ArkLib/ProofSystem/BatchedFri/Spec/General.lean +++ b/ArkLib/ProofSystem/BatchedFri/Spec/General.lean @@ -82,9 +82,33 @@ noncomputable def liftedFRI [DecidableEq F] : (liftingLens D x k s d m) (Fri.Spec.reduction D x k s d dom_size_cond l) +instance instBatchFRIreductionMessageOI : ∀ j, + OracleInterface + ((batchSpec F m ++ₚ + ( + Fri.Spec.pSpecFold D x k s ++ₚ + Fri.Spec.FinalFoldPhase.pSpec F ++ₚ + Fri.Spec.QueryRound.pSpec D x l + ) + ).Message j) := fun j ↦ by + apply instOracleInterfaceMessageAppend + +instance instBatchFRIreductionChallengeOI : ∀ j, + OracleInterface + ((batchSpec F m ++ₚ + ( + Fri.Spec.pSpecFold D x k s ++ₚ + Fri.Spec.FinalFoldPhase.pSpec F ++ₚ + Fri.Spec.QueryRound.pSpec D x l + ) + ).Challenge j) := + ProtocolSpec.challengeOracleInterface + + /- Oracle reduction of the batched FRI protocol. -/ @[reducible] -noncomputable def batchedFRIreduction [DecidableEq F] := +noncomputable def batchedFRIreduction [DecidableEq F] + := OracleReduction.append (BatchingRound.batchOracleReduction D x s d m) (liftedFRI D x k s d dom_size_cond l m) diff --git a/ArkLib/ProofSystem/BatchedFri/Spec/SingleRound.lean b/ArkLib/ProofSystem/BatchedFri/Spec/SingleRound.lean index cb4bdaa9c..60c16e251 100644 --- a/ArkLib/ProofSystem/BatchedFri/Spec/SingleRound.lean +++ b/ArkLib/ProofSystem/BatchedFri/Spec/SingleRound.lean @@ -74,6 +74,9 @@ def batchSpec (F : Type) (m : ℕ) : ProtocolSpec 1 := ⟨!v[.V_to_P], !v[Fin m instance : ∀ j, OracleInterface ((batchSpec F m).Message j) | ⟨0, h⟩ => nomatch h +instance : ∀ j, OracleInterface ((batchSpec F m).Challenge j) := + ProtocolSpec.challengeOracleInterface + /-- The batching round oracle prover. -/ noncomputable def batchProver : OracleProver []ₒ @@ -98,8 +101,7 @@ noncomputable def batchProver : ps 0 + ∑ i, Polynomial.C (cs i) * (ps i.succ).1, by unfold Fri.Spec.Witness - simp only [List.toFinset_finRange, Fin.coe_ofNat_eq_mod, Nat.zero_mod, List.take_zero, - List.toFinset_nil, sum_empty, tsub_zero] + simp only [Fin.coe_ofNat_eq_mod, Nat.zero_mod] apply mem_degreeLT.mpr by_cases h : ↑(ps 0) + ∑ i, Polynomial.C (cs i) * ↑(ps i.succ) = 0 · rw [h] diff --git a/ArkLib/ProofSystem/Fri/Domain.lean b/ArkLib/ProofSystem/Fri/Domain.lean index ef44c655f..7035dffc2 100644 --- a/ArkLib/ProofSystem/Fri/Domain.lean +++ b/ArkLib/ProofSystem/Fri/Domain.lean @@ -1,15 +1,80 @@ import Mathlib.GroupTheory.Coset.Basic import Mathlib.GroupTheory.GroupAction.Basic import Mathlib.GroupTheory.SpecificGroups.Cyclic +import Mathlib.MeasureTheory.MeasurableSpace.Defs import ArkLib.Data.FieldTheory.NonBinaryField.Basic import ArkLib.Data.GroupTheory.Smooth +import ArkLib.ToMathlib.Finset.Basic + +import Mathlib.Data.FinEnum variable {F : Type} [NonBinaryField F] [Finite F] variable (D : Subgroup Fˣ) {n : ℕ} [DIsCyclicC : IsCyclicWithGen D] [DSmooth : SmoothPowerOfTwo n D] namespace Fri +section + +/- +For `[CommMonoid K], (Monoid.toMulAction _ : MulAction Kˣ Kˣ) = Units.mulAction'` is not defeq. +This leads to some typeclass friction that is ameliorated, albeit not resolved, by some automation. + +Viz. the discussion here: +https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/class.2Flemmas.20for.20smul.20distributing.20over.20smul +-/ + +omit [Finite F] in +@[simp, grind _=_] +private lemma op_der_eq : Monoid.toMulAction Fˣ = Units.mulAction' := by ext; rfl + +open Lean Elab in +/-- +A variation on `rw [op_der_eq] at *`. + +Ensures that once `Fˣ` is fixed, we use `Monoid.toMulAction Fˣ`, not `Units.mulAction'`. +-/ +private def reconcile (goal : MVarId) : MetaM (Option MVarId) := goal.withContext do + let mut goal ← go goal + for const in ←getLCtx do + if const.isImplementationDetail then continue + goal ← go goal (mkIdent const.userName) + pure (.some goal) + where go (goal : MVarId) (loc : Option Ident := .none) : MetaM MVarId := do + let tac : MetaM _ := + match loc with + | .none => `(tactic|try rewrite [op_der_eq]) + | .some loc => `(tactic|try rewrite [op_der_eq] at $loc:ident) + let ([goal'], _) ← runTactic goal (←tac) + | throwError "Failed to reconcile `Monoid.toMulAction` and `Units.mulAction`." + return goal' + +open Lean Elab Tactic in +/-- +Reconciles `Monoid.toMulAction Fˣ = Units.mulAction'` across the goal. +-/ +scoped elab "reconcile" : tactic => liftMetaTactic1 reconcile + +/-- +`reconcile`-aware `aesop` that deals with coset membership. + +Can be trivially extended to recognise more than just `mem_leftCoset_iff`. +-/ +syntax (name := reconcileStx) "aesop_reconcile" : tactic + +set_option hygiene false in +open Lean Elab Tactic PrettyPrinter Delaborator in +@[tactic reconcileStx, inherit_doc reconcileStx] +private def elabReconcileStx : Tactic := fun stx => withMainContext do + match stx with + | `(tactic|aesop_reconcile) => + evalTactic (← + `(tactic|(have := fun A A₁ X₁ X₂ X₃ ↦ @mem_leftCoset_iff.{0} A A₁ X₁ X₂ X₃ + reconcile + specialize this (Units ‹_›) inferInstance + aesop))) + | _ => throwError "Unsupported syntax." + namespace Domain /-- Constructs the subgroups of `Fˣ` which we will use to construct @@ -27,169 +92,95 @@ def domain (n : ℕ) (i : ℕ) : Fin (2 ^ (n - i)) → evalDomain D i := fun j => ⟨(DIsCyclicC.gen ^ (2 ^ i)) ^ j.1, by simp⟩ omit [Finite F] in -lemma domain_surjective (i : ℕ) : i ≤ n → Function.Surjective (domain D n i) := by - intros h - unfold Function.Surjective - intros b - have := b.2 - simp only [evalDomain] at this - have : ∃ j, b.1 = (DIsCyclicC.gen ^ (2 ^ i)) ^ j ∧ j < 2 ^ (n - i) := by - rw [Subgroup.mem_zpowers_iff] at this - rcases this with ⟨k, b_def⟩ - have : ∃ k : ℕ, (DIsCyclicC.gen ^ 2 ^ i) ^ k = b.1 := by - exists Int.toNat (k % (2 ^ (n - i))) - have k_rel : ∃ m, k = k % (2 ^ (n - i)) + m * (2 ^ (n - i)) := by - exists (k / (2 ^ (n - i))) - exact Eq.symm (Int.emod_add_ediv' k (2 ^ (n - i))) - rcases k_rel with ⟨m, k_rel⟩ - rw [k_rel] at b_def - have cast_rw {a : Fˣ} {n : ℕ} : a ^ n = a ^ (n : ℤ) := by - exact rfl - rw [cast_rw] - have : 0 ≤ k % 2 ^ (n - i) := by - apply Int.emod_nonneg k - exact Ne.symm (NeZero.ne' (2 ^ (n - i))) - simp only [Int.ofNat_toNat, this, sup_of_le_left, evalDomain] - rw [←b_def, zpow_add, mul_comm m, zpow_mul] - norm_cast - rw - [ - (pow_mul DIsCyclicC.gen (2 ^ i) (2 ^ (n - i))).symm, - ←pow_add, Nat.add_sub_of_le h, ←DSmooth.smooth, pow_orderOf_eq_one - ] - simp - rcases this with ⟨k, b_def⟩ - exists (k % (2 ^ (n - i))) - apply And.intro - · rw [←b_def] - have k_rel : ∃ m, k = k % (2 ^ (n - i)) + m * (2 ^ (n - i)) := by - exists (k / (2 ^ (n - i))) - exact Eq.symm (Nat.mod_add_div' k (2 ^ (n - i))) - rcases k_rel with ⟨m, k_rel⟩ - rw (occs := .pos [1]) [k_rel] - rw [pow_add, mul_comm m, pow_mul] - norm_cast - rw - [ - (pow_mul DIsCyclicC.gen (2 ^ i) (2 ^ (n - i))).symm, - ←pow_add, Nat.add_sub_of_le h, ←DSmooth.smooth, pow_orderOf_eq_one - ] +lemma domain_surjective {i : ℕ} : Function.Surjective (domain D n i) := by + by_cases h : i ≤ n + · intros b + have := b.2 + simp only [evalDomain] at this + have : ∃ j, b.1 = (DIsCyclicC.gen ^ (2 ^ i)) ^ j ∧ j < 2 ^ (n - i) := by + rw [Subgroup.mem_zpowers_iff] at this + rcases this with ⟨k, b_def⟩ + have : ∃ k : ℕ, (DIsCyclicC.gen ^ 2 ^ i) ^ k = b.1 := by + exists Int.toNat (k % (2 ^ (n - i))) + have k_rel : ∃ m, k = k % (2 ^ (n - i)) + m * (2 ^ (n - i)) := by + exists (k / (2 ^ (n - i))) + exact Eq.symm (Int.emod_add_ediv' k (2 ^ (n - i))) + rcases k_rel with ⟨m, k_rel⟩ + rw [k_rel] at b_def + have cast_rw {a : Fˣ} {n : ℕ} : a ^ n = a ^ (n : ℤ) := by + exact rfl + rw [cast_rw] + have : 0 ≤ k % 2 ^ (n - i) := by + apply Int.emod_nonneg k + exact Ne.symm (NeZero.ne' (2 ^ (n - i))) + simp only [Int.ofNat_toNat, this, sup_of_le_left, evalDomain] + rw [←b_def, zpow_add, mul_comm m, zpow_mul] + norm_cast + rw + [ + (pow_mul DIsCyclicC.gen (2 ^ i) (2 ^ (n - i))).symm, + ←pow_add, Nat.add_sub_of_le h, ←DSmooth.smooth, pow_orderOf_eq_one + ] + simp + rcases this with ⟨k, b_def⟩ + exists (k % (2 ^ (n - i))) + apply And.intro + · rw [←b_def] + have k_rel : ∃ m, k = k % (2 ^ (n - i)) + m * (2 ^ (n - i)) := by + exists (k / (2 ^ (n - i))) + exact Eq.symm (Nat.mod_add_div' k (2 ^ (n - i))) + rcases k_rel with ⟨m, k_rel⟩ + rw (occs := .pos [1]) [k_rel] + rw [pow_add, mul_comm m, pow_mul] + norm_cast + rw + [ + (pow_mul DIsCyclicC.gen (2 ^ i) (2 ^ (n - i))).symm, + ←pow_add, Nat.add_sub_of_le h, ←DSmooth.smooth, pow_orderOf_eq_one + ] + simp + · apply Nat.mod_lt _ + exact Nat.two_pow_pos _ + rcases this with ⟨j, h⟩ + exists ⟨j, h.2⟩ + unfold domain + rcases b with ⟨b, hb⟩ + simp only at h + simp [h] + · intros b + simp only [not_le] at h + have : n - i = 0 := by omega + use ⟨0, by rw [this]; decide⟩ + unfold domain + simp + have h : DIsCyclicC.gen.1 ^ (2 ^ i) = 1 := by + have h : ∃ j : ℕ, i = n + j := by + apply Nat.exists_eq_add_of_le + exact Nat.le_of_succ_le h + rcases h with ⟨j, h⟩ + rw [h, Nat.pow_add, pow_mul] + have : DIsCyclicC.gen.1 ^ (2 ^ n) = 1 := by + apply orderOf_dvd_iff_pow_eq_one.mp + norm_cast + rw [DSmooth.smooth] + rw [this] simp - · apply Nat.mod_lt _ - exact Nat.two_pow_pos _ - rcases this with ⟨j, h⟩ - exists ⟨j, h.2⟩ - unfold domain - rcases b with ⟨b, hb⟩ - simp only at h - simp [h] + rcases b with ⟨b, h'⟩ + rw [evalDomain, h, Subgroup.zpowers_one_eq_bot, Subgroup.mem_bot] at h' + simp [h'] lemma pow_inj {i : ℕ} {a b : Fin (2 ^ (n - i))} : i ≤ n → (DIsCyclicC.gen.1 ^ 2 ^ i) ^ a.1 = (DIsCyclicC.gen.1 ^ 2 ^ i) ^ b.1 → a = b := by - intros h h' - have ha := a.2 - have hb := b.2 - by_contra a_neq_b - rcases Fin.lt_or_lt_of_ne a_neq_b with a_le_b | a_gt_b - · have h' := h'.symm - rw [←mul_inv_eq_one] at h' - have cast_eq {a : Fˣ} (n : ℕ) : a ^ n = a ^ (Int.ofNat n) := by - exact rfl - rw [cast_eq a.1, cast_eq b.1, ←zpow_neg, ←zpow_add] at h' - have h₁ : 0 < (Int.ofNat b.1 + -Int.ofNat a.1) := by - apply Int.lt_add_of_neg_add_lt - rw [add_zero] - simp only [Int.ofNat_eq_coe, neg_lt_neg_iff, Nat.cast_lt, Fin.val_fin_lt] - exact a_le_b - have h₂ : (Int.ofNat b.1 + -Int.ofNat a.1) < 2 ^ (n - i) := by - simp only [Int.ofNat_eq_coe, add_neg_lt_iff_lt_add] - apply lt_add_of_lt_of_nonneg - · norm_cast - · simp - have : Int.ofNat b.1 + -Int.ofNat a.1 = Int.ofNat (b.1 - a.1) := by - simp - have : Int.ofNat b.1 + - Int.ofNat a.1 = Int.ofNat b.1 - Int.ofNat a.1 := by - ring - rw [Int.ofNat_eq_coe, Int.ofNat_eq_coe] at this - rw [this, Int.sub_eq_iff_eq_add'] - norm_cast - refine Eq.symm (Nat.add_sub_of_le ?_) - exact Nat.le_of_succ_le a_le_b - rw [this] at h' h₁ h₂ - rw [Int.ofNat_eq_coe, zpow_natCast] at h' - have h' := orderOf_dvd_of_pow_eq_one h' - have : orderOf (DIsCyclicC.gen.1 ^ 2 ^ i) = 2 ^ (n - i) := by - rw [orderOf_pow] - norm_cast - rw [DSmooth.smooth] - have : n = (n - i) + i := by - exact (Nat.sub_eq_iff_eq_add h).mp rfl - rw (occs := .pos [2]) [this] - rw [pow_add, Nat.gcd_mul_left_left] - exact Nat.pow_div h (by decide) - rw [this] at h' - have : 2 ^ (n - i) ≤ b.1 - a.1 := by - rcases h' with ⟨m, h'⟩ - rw [Int.ofNat_eq_coe, Int.natCast_pos] at h₁ - have : m > 0 := by - by_contra h - simp at h - rw [h, mul_zero] at h' - rw [h', lt_self_iff_false] at h₁ - exact h₁ - nlinarith - have : b.1 - a.1 < 2 ^ (n - i) := by - exact Nat.sub_lt_of_lt hb - linarith - · rw [←mul_inv_eq_one] at h' - have cast_eq {a : Fˣ} (n : ℕ) : a ^ n = a ^ (Int.ofNat n) := by - exact rfl - rw [cast_eq a.1, cast_eq b.1, ←zpow_neg, ←zpow_add] at h' - have h₁ : 0 < (Int.ofNat a.1 + -Int.ofNat b.1) := by - apply Int.lt_add_of_neg_add_lt - rw [add_zero] - simp only [Int.ofNat_eq_coe, neg_lt_neg_iff, Nat.cast_lt, Fin.val_fin_lt] - exact a_gt_b - have h₂ : (Int.ofNat a.1 + -Int.ofNat b.1) < 2 ^ (n - i) := by - simp only [Int.ofNat_eq_coe, add_neg_lt_iff_lt_add] - apply lt_add_of_lt_of_nonneg - · norm_cast - · simp - have : Int.ofNat a.1 + -Int.ofNat b.1 = Int.ofNat (a.1 - b.1) := by - simp - have : Int.ofNat a.1 + - Int.ofNat b.1 = Int.ofNat a.1 - Int.ofNat b.1 := by - ring - rw [Int.ofNat_eq_coe, Int.ofNat_eq_coe] at this - rw [this, Int.sub_eq_iff_eq_add'] - norm_cast - refine Eq.symm (Nat.add_sub_of_le ?_) - exact Nat.le_of_succ_le a_gt_b - rw [this] at h' h₁ h₂ - rw [Int.ofNat_eq_coe, zpow_natCast] at h' - have h' := orderOf_dvd_of_pow_eq_one h' - have : orderOf (DIsCyclicC.gen.1 ^ 2 ^ i) = 2 ^ (n - i) := by - rw [orderOf_pow] - norm_cast - rw [DSmooth.smooth] - have : n = (n - i) + i := by - exact (Nat.sub_eq_iff_eq_add h).mp rfl - rw (occs := .pos [2]) [this] - rw [pow_add, Nat.gcd_mul_left_left] - exact Nat.pow_div h (by decide) - rw [this] at h' - have : 2 ^ (n - i) ≤ a.1 - b.1 := by - rcases h' with ⟨m, h'⟩ - rw [Int.ofNat_eq_coe, Int.natCast_pos] at h₁ - have : m > 0 := by - by_contra h - simp at h - rw [h, mul_zero] at h' - rw [h', lt_self_iff_false] at h₁ - exact h₁ - nlinarith - have : a.1 - b.1 < 2 ^ (n - i) := by - exact Nat.sub_lt_of_lt ha - linarith + intros h₁ h₂ + rw [pow_inj_mod] at h₂ + have : orderOf (DIsCyclicC.gen.1 ^ 2 ^ i) = 2 ^ (n - i) := by + calc orderOf (DIsCyclicC.gen.1 ^ 2 ^ i) + _ = 2 ^ n / (2 ^ n).gcd (2 ^ i) := by simp [orderOf_pow, DSmooth.smooth] + _ = 2 ^ n / (2 ^ (n - i + i)).gcd (2 ^ i) := by aesop + _ = 2 ^ n / (2 ^ (n - i) * 2 ^ i).gcd (2 ^ i) := by grind + _ = 2 ^ n / 2 ^ i := by rw [Nat.gcd_mul_left_left _ _] + _ = 2 ^ (n - i) := Nat.pow_div h₁ (by decide) + grind [Fin.val_inj, Nat.mod_eq_of_lt, cases Fin] lemma domain_injective (i : ℕ) : i ≤ n → Function.Injective (domain D n i) := by intros h a b h' @@ -215,49 +206,30 @@ def domainEmb {i : ℕ} : evalDomain D i ↪ F := /- Proof the first subgroup is `D`, the cyclic group generated by `DIsCyclicC.gen : Fˣ` -/ omit [Finite F] in -lemma D_def : D = evalDomain D 0 := by +@[simp] +lemma D_def : evalDomain D 0 = D := by unfold evalDomain - simp only [pow_zero, pow_one] - have := DIsCyclicC.zpow_surjective - unfold Function.Surjective at this + symm ext x - apply Iff.intro - · intros h - rcases this ⟨x, h⟩ with ⟨a, h⟩ - simp only at h - refine Subgroup.mem_zpowers_iff.mpr ?_ - exists a - have : x = (DIsCyclicC.gen ^ a) := by - norm_cast - rw [h] - rw [this] - · intros h - rw [Subgroup.mem_zpowers_iff] at h - rcases h with ⟨k, h⟩ - norm_cast at h - rw [←h] - exact (DIsCyclicC.gen ^ k).2 + rw [Subgroup.mem_zpowers_iff] + simp only [pow_zero, pow_one] + norm_cast + refine ⟨fun h ↦ ?p₁, fun h ↦ h.choose_spec ▸ (DIsCyclicC.gen ^ h.choose).2⟩ + have := DIsCyclicC.zpow_surjective ⟨x, h⟩ + grind /- Proof each on of these groups is cyclic (with a computable generator) -/ -instance {i : ℕ} : IsCyclicWithGen (evalDomain D i) := by - unfold evalDomain - constructor - swap - · refine ⟨DIsCyclicC.gen.1 ^ 2 ^ i, ?_⟩ - simp - · unfold Function.Surjective - rintro ⟨b, h⟩ - have : ∃ n : ℤ, b = (DIsCyclicC.gen.1 ^ 2 ^ i) ^ n := by - refine Subgroup.exists_mem_zpowers.mp ?_ - exists b - rcases this with ⟨a, h'⟩ - exists a - simp only [h'] - rfl +instance {i : ℕ} : IsCyclicWithGen (evalDomain D i) := + ⟨ + ⟨DIsCyclicC.gen.1 ^ 2 ^ i, by simp⟩, + by rintro ⟨b, h⟩ + have := Subgroup.exists_mem_zpowers.1 ⟨b, ⟨h, rfl⟩⟩ + aesop + ⟩ omit [Finite F] in lemma pow_2_pow_i_mem_Di_of_mem_D : - ∀ {x : Fˣ} (i : ℕ), + ∀ {x : Fˣ} {i : ℕ}, x ∈ D → x ^ (2 ^ i) ∈ evalDomain D i := by intros x i h simp only [evalDomain] @@ -342,44 +314,30 @@ lemma minus_one_in_doms {i : ℕ} (h : i < n) : exists ((2 ^ (n - (i + 1)))) norm_cast rw [←pow_mul, ←pow_add] - have : (i + (n - (i + 1))) = n - 1 := by - refine Eq.symm ((fun {b a c} h ↦ (Nat.sub_eq_iff_eq_add' h).mp) (Nat.le_sub_one_of_lt h) ?_) - exact Eq.symm (Nat.Simproc.sub_add_eq_comm n i 1) - rw [this] - have : ((DIsCyclicC.gen.1 ^ 2 ^ (n - 1)) ^ 2) = 1 := by - rw [←pow_mul] - have : 2 ^ (n - 1) * 2 = 2 ^ n := by - apply Nat.two_pow_pred_mul_two - linarith - rw [this, ←DSmooth.smooth] + rw [show i + (n - (i + 1)) = n - 1 by omega] + have : (DIsCyclicC.gen.1 ^ 2 ^ (n - 1)) ^ 2 = 1 := by + rw [ + ←pow_mul, + show 2 ^ (n - 1) * 2 = 2 ^ n by grind [Nat.two_pow_pred_mul_two], + ←DSmooth.smooth + ] norm_cast rw [pow_orderOf_eq_one] have alg {x : Fˣ} : x^2 = 1 → x = 1 ∨ x = -1 := by - intros h - refine (Units.inv_eq_self_iff x).mp ?_ - have {a b : Fˣ} (c : Fˣ) : c * a = c * b → a = b := by - intros h - have : c⁻¹ * (c * a) = c⁻¹ * (c * a) := by rfl - rw (occs := .pos [2]) [h] at this - rw [←mul_assoc, ←mul_assoc, inv_mul_cancel, one_mul, one_mul] at this - exact this - apply this x - simp only [mul_inv_cancel, h.symm, pow_two] - have cast : (DIsCyclicC.gen ^ 2 ^ (n - 1)).1 = (DIsCyclicC.gen.1 ^ 2 ^ (n - 1)) := by rfl - rw [cast] + intros h₁ + have := sq_eq_one_iff (a := (x : F)) + norm_cast at this + aesop specialize alg this - rcases alg with alg | alg - · have gen_ord := DSmooth.smooth - rw [orderOf_eq_iff (by simp)] at gen_ord - have gen_ord := - gen_ord.2 - (2 ^ (n - 1)) - (by apply Nat.two_pow_pred_lt_two_pow; linarith) - (by simp) - exfalso - apply gen_ord - norm_cast at alg - · assumption + have gen_ord := DSmooth.smooth + rw [orderOf_eq_iff (by simp)] at gen_ord + norm_cast at alg + have gen_ord := + gen_ord.2 + (2 ^ (n - 1)) + (by apply Nat.two_pow_pred_lt_two_pow; linarith) + (by simp) + tauto omit [Finite F] in lemma dom_n_eq_triv : evalDomain D n = ⊥ := by @@ -395,62 +353,44 @@ instance {i : Fin (n + 1)} : OfNat (evalDomain D i) 1 where instance domain_neg_inst {i : Fin n} : Neg (evalDomain D i.1) where neg := fun x => ⟨_, minus_one_in_doms D i.2⟩ * x -/- Enumerates the `2^s` roots of unity of `Fˣ`, which corresponds to the - elemens of the `(n - s)`th subgroup (for `s ≤ n`). -/ -def rootsOfUnity (n s : ℕ) : List (Domain.evalDomain D (n - s)) := - List.map - (fun i => - ⟨ - (DIsCyclicC.gen.1 ^ (2 ^ (n - s))) ^ i, - by - unfold evalDomain - apply Subgroup.mem_zpowers_iff.mpr - exists i - ⟩ - ) - (List.range (2 ^ s)) - end Domain namespace CosetDomain open Pointwise -omit [Finite F] in -private lemma op_der_eq : Monoid.toMulAction Fˣ = Units.mulAction' := by - unfold Units.mulAction' Monoid.toMulAction - congr - ext g m - simp only [Units.val_mul] - unfold_projs - rfl - /- Element of `Fˣ` we will use to define our coset -/ variable (x : Fˣ) /- Cosets that will form domains of evaluation for the FRI codewords. -/ @[simp] def evalDomain (i : ℕ) : Set Fˣ := - (x ^ (2 ^ i)) • (Domain.evalDomain D i) + x ^ (2 ^ i) • Domain.evalDomain D i + +abbrev evalDomainSigma (s : Fin (n + 1) → ℕ+) (i : ℕ) := + evalDomain D x (∑ j' ∈ finRangeTo i, s j') /- Enumeration of the elements of the `i`th coset. -/ def domain (n : ℕ) (i : ℕ) : Fin (2 ^ (n - i)) → evalDomain D x i := fun j => ⟨ x ^ 2 ^ i * (DIsCyclicC.gen ^ (2 ^ i)) ^ j.1, - by - simp - rw [←Domain.evalDomain] - have h : - (x ^ 2 ^ i)⁻¹ * (x ^ 2 ^ i * (DIsCyclicC.gen.1 ^ 2 ^ i) ^ j.1) ∈ - Domain.evalDomain D i := by - rw [←mul_assoc] - simp - convert (mem_leftCoset_iff _).mpr h - expose_names - exact (@op_der_eq F inst).symm + by aesop_reconcile ⟩ +omit [Finite F] in +lemma domain_surjective {i : ℕ} : Function.Surjective (domain D x n i) := by + rintro ⟨b, hb⟩ + unfold evalDomain at hb + unfold domain + have h' : (x ^ (2 ^ i))⁻¹ * b ∈ Domain.evalDomain D i := by + aesop_reconcile + rcases Domain.domain_surjective (n := n) _ ⟨_, h'⟩ with ⟨a, h''⟩ + use a + unfold Domain.domain at h'' + simp only [Domain.evalDomain, Subtype.mk.injEq] at h'' + simp only [mul_eq_of_eq_inv_mul h''] + lemma domain_injective {i : ℕ} : i ≤ n → Function.Injective (domain D x n i) := by intros h intros a b @@ -477,39 +417,81 @@ def domainEmb {i : ℕ} : evalDomain D x i ↪ F := simp only [h] ⟩ +noncomputable def domainToFin {i : Fin (n + 1)} : evalDomain D x i → Fin (2 ^ (n - i)) := + fun g => + have : ∃ ind : Fin (2 ^ (n - i)), + g.1.1 = x.1 ^ (2 ^ i.1) * ((DIsCyclicC.gen.1 ^ (2 ^ i.1)) ^ ind.1) := by + have h := g.2 + unfold evalDomain at h + have h' : (x ^ 2 ^ i.1)⁻¹ * ↑g ∈ ↑(Domain.evalDomain D ↑i) := by aesop_reconcile + unfold Domain.evalDomain at h' + rw [Subgroup.mem_zpowers_iff] at h' + rcases h' with ⟨ind, h'⟩ + have h' : + ∃ ind : ℕ, + (DIsCyclicC.gen.1 ^ 2 ^ i.1) ^ ind = (x ^ 2 ^ i.1)⁻¹ * ↑g ∧ ind < 2 ^ (n - i) := by + exists Int.toNat (ind % (2 ^ (n - i))) + have k_rel : ∃ m, ind = ind % (2 ^ (n - i)) + m * (2 ^ (n - i)) := by + exists (ind / (2 ^ (n - i))) + exact Eq.symm (Int.emod_add_ediv' ind (2 ^ (n - i))) + rcases k_rel with ⟨m, k_rel⟩ + rw [k_rel] at h' + have cast_rw {a : Fˣ} {n : ℕ} : a ^ n = a ^ (n : ℤ) := by + exact rfl + rw [cast_rw] + have : 0 ≤ ind % 2 ^ (n - i) := by + apply Int.emod_nonneg ind + exact Ne.symm (NeZero.ne' (2 ^ (n - i))) + simp only [Int.ofNat_toNat, this, sup_of_le_left, evalDomain] + rw [←h', zpow_add, mul_comm m, zpow_mul] + norm_cast + rw + [ + (pow_mul DIsCyclicC.gen (2 ^ i.1) (2 ^ (n - i.1))).symm, + ←pow_add, Nat.add_sub_of_le (by omega), ←DSmooth.smooth, pow_orderOf_eq_one + ] + simp only [Nat.cast_pow, Nat.cast_ofNat, one_zpow, mul_one, Nat.ofNat_pos, pow_pos, + Int.toNat_lt', true_and, gt_iff_lt] + have h' := @Int.emod_lt ind (2 ^ (n - i.1)) (by simp) + simp only [Int.natAbs_pow, Int.reduceAbs, Nat.cast_pow, Nat.cast_ofNat] at h' + exact h' + rcases h' with ⟨ind, h', cond⟩ + exists ⟨ind, cond⟩ + have h' : g.1 = (x ^ 2 ^ i.1) * (DIsCyclicC.gen ^ 2 ^ i.1) ^ ind := by + apply Eq.symm + rw [h'] + simp + rw [h'] + rfl + Classical.choose this + /- Helper lemmas for constructing operations on/lifting between domains. -/ omit [Finite F] in -lemma D_def : evalDomain D x 0 = x • D := by simp [Domain.D_def D] +@[simp] +lemma D_def : evalDomain D x 0 = x • D := by + unfold evalDomain + rw [Domain.D_def] + simp lemma pow_2_pow_i_mem_Di_of_mem_D {F : Type} [NonBinaryField F] [Finite F] {D : Subgroup Fˣ} [DIsCyclicC : IsCyclicWithGen ↥D] {x : Fˣ} : - ∀ {a : Fˣ} (i : ℕ), + ∀ {a : Fˣ} {i : ℕ}, a ∈ evalDomain D x 0 → a ^ (2 ^ i) ∈ evalDomain D x i := by unfold evalDomain intros a i h - have h : x⁻¹ * a ∈ Domain.evalDomain D 0 := by - simp only [pow_zero, pow_one] at h - apply (mem_leftCoset_iff _).mp - convert h - exact op_der_eq - rw [←Domain.D_def] at h - have h := Domain.pow_2_pow_i_mem_Di_of_mem_D D i h + have h : x⁻¹ * a ∈ Domain.evalDomain D 0 := by aesop_reconcile have : (x⁻¹ * a) ^ 2 ^ i = (x ^ (2 ^ i))⁻¹ * (a ^ (2 ^ i)) := by field_simp - rw [this] at h - convert (mem_leftCoset_iff _).mpr h - exact op_der_eq.symm + simp only [Domain.D_def] at h + have := Domain.pow_2_pow_i_mem_Di_of_mem_D D (i := i) h + aesop_reconcile omit [Finite F] in lemma sqr_mem_D_succ_i_of_mem_D_i : ∀ {a : Fˣ} {i : ℕ}, a ∈ evalDomain D x i → a ^ 2 ∈ evalDomain D x (i + 1) := by unfold evalDomain intros a i h - have h : (x ^ 2 ^ i)⁻¹ * a ∈ Domain.evalDomain D i := by - apply (mem_leftCoset_iff _).mp - convert h - exact op_der_eq - have h := Domain.sqr_mem_D_succ_i_of_mem_D_i D h + have h : (x ^ 2 ^ i)⁻¹ * a ∈ Domain.evalDomain D i := by aesop_reconcile have : ((x ^ 2 ^ i)⁻¹ * a) ^ 2 = (x ^ 2 ^ (i + 1))⁻¹ * (a ^ 2) := by have : ((x ^ 2 ^ i)⁻¹ * a) ^ 2 = ((x ^ 2 ^ i) ^ 2)⁻¹ * (a ^ 2) := by field_simp rw [this] @@ -518,9 +500,8 @@ lemma sqr_mem_D_succ_i_of_mem_D_i : ∀ {a : Fˣ} {i : ℕ}, congr 1 grind rw [this] - rw [this] at h - convert (mem_leftCoset_iff _).mpr h - exact op_der_eq.symm + have h := Domain.sqr_mem_D_succ_i_of_mem_D_i D h + aesop_reconcile omit [Finite F] in lemma pow_lift : ∀ {a : Fˣ} {i : ℕ} (s : ℕ), @@ -542,21 +523,17 @@ lemma neg_mem_dom_of_mem_dom : ∀ {a : Fˣ} (i : Fin n), unfold evalDomain rintro a ⟨i, i_prop⟩ h have mem : (x ^ 2 ^ i)⁻¹ * a ∈ Domain.evalDomain D i := by - apply (mem_leftCoset_iff _).mp - convert h - exact op_der_eq - + aesop_reconcile have : (x ^ 2 ^ i)⁻¹ * -a ∈ ↑(Domain.evalDomain D i) := by have : (x ^ 2 ^ i)⁻¹ * -a = ((x ^ 2 ^ i)⁻¹ * a) * (- 1) := by field_simp rw [this] exact ( Subgroup.mul_mem_cancel_right - (Domain.evalDomain D i) + _ (Domain.minus_one_in_doms D i_prop) ).mpr mem - convert (mem_leftCoset_iff _).mpr this - exact op_der_eq.symm + aesop_reconcile omit [Finite F] in lemma mul_root_of_unity {x : Fˣ} : @@ -566,9 +543,7 @@ lemma mul_root_of_unity {x : Fˣ} : intros a b i j i_le_j a_in b_in unfold evalDomain Domain.evalDomain at * have : (x ^ 2 ^ i)⁻¹ * a ∈ (Subgroup.zpowers (DIsCyclicC.gen.1 ^ 2 ^ i)) := by - apply (mem_leftCoset_iff _).mp - convert a_in - exact op_der_eq + aesop_reconcile have : (x ^ 2 ^ i)⁻¹ * (a * b) ∈ (Subgroup.zpowers (DIsCyclicC.gen.1 ^ 2 ^ i)) := by rw [Subgroup.mem_zpowers_iff] at b_in this rcases this with ⟨ka, a_in⟩ @@ -576,13 +551,11 @@ lemma mul_root_of_unity {x : Fˣ} : apply Subgroup.mem_zpowers_iff.mpr exists (ka + (2 ^ (j - i)) * kb) rw [ - ←@mul_assoc Fˣ _ _ a b, ←a_in, ←b_in, zpow_add, - Eq.symm (pow_mul_pow_sub 2 i_le_j), pow_mul, zpow_mul + ←@mul_assoc _ _ _ a b, ←a_in, ←b_in, zpow_add, + (pow_mul_pow_sub 2 i_le_j).symm, pow_mul, zpow_mul ] norm_cast - have := (mem_leftCoset_iff (x ^ 2 ^ i)).mpr this - convert this - exact op_der_eq.symm + aesop_reconcile omit [Finite F] in lemma dom_n_eq_triv : evalDomain D x n = {x ^ (2 ^ n)} := by @@ -590,11 +563,31 @@ lemma dom_n_eq_triv : evalDomain D x n = {x ^ (2 ^ n)} := by rw [Domain.dom_n_eq_triv] simp +noncomputable local instance : Fintype F := Fintype.ofFinite _ + +noncomputable instance : Nonempty ↑(CosetDomain.evalDomain D x 0) := + ⟨x, by aesop_reconcile⟩ + +noncomputable instance : Fintype ↑(CosetDomain.evalDomain D x 0) := inferInstance + instance domain_neg_inst {F : Type} [NonBinaryField F] [Finite F] {D : Subgroup Fˣ} {n : ℕ} [DIsCyclicC : IsCyclicWithGen ↥D] [DSmooth : SmoothPowerOfTwo n ↥D] {x : Fˣ} (i : Fin n) : Neg (evalDomain D x i) where neg := fun a => ⟨_, neg_mem_dom_of_mem_dom D x i a.2⟩ +instance {i : Fin (n + 1)} : Fintype (evalDomain D x i) where + elems := Finset.univ.map (domainEnum D x (i := i)) + complete := by + intros y + apply Finset.mem_map.mpr + simp only [domainEnum] + rcases @domain_surjective (n := n) _ _ D _ _ _ _ y with ⟨a, h⟩ + use a + rw [←h] + simp + end CosetDomain +end + end Fri diff --git a/ArkLib/ProofSystem/Fri/Spec/General.lean b/ArkLib/ProofSystem/Fri/Spec/General.lean index 17013c300..627a0503a 100644 --- a/ArkLib/ProofSystem/Fri/Spec/General.lean +++ b/ArkLib/ProofSystem/Fri/Spec/General.lean @@ -37,7 +37,7 @@ variable (l : ℕ) def inputRelation [DecidableEq F] (δ : ℝ≥0) : Set ( - (Statement (k := k) F 0 × (∀ j, OracleStatement (k := k) D x s 0 j)) × + (Statement F (0 : Fin (k + 1)) × (∀ j, OracleStatement D x s 0 j)) × Witness F s d (0 : Fin (k + 2)) ) := match k with @@ -62,14 +62,26 @@ def pSpecFold : ProtocolSpec (Fin.vsum fun (_ : Fin k) ↦ 2) := instance : ∀ j, OracleInterface ((pSpecFold D x k s).Message j) := instOracleInterfaceMessageSeqCompose +instance : ∀ j, OracleInterface ((pSpecFold D x k s).Challenge j) := + ProtocolSpec.challengeOracleInterface + instance : ∀ j, OracleInterface (((pSpecFold D x k s ++ₚ FinalFoldPhase.pSpec F)).Message j) := instOracleInterfaceMessageAppend +instance : ∀ j, OracleInterface (((pSpecFold D x k s ++ₚ FinalFoldPhase.pSpec F)).Challenge j) := + ProtocolSpec.challengeOracleInterface + instance : ∀ i, OracleInterface ((pSpecFold D x k s ++ₚ FinalFoldPhase.pSpec F ++ₚ QueryRound.pSpec D x l).Message i) := instOracleInterfaceMessageAppend +instance : + ∀ j, + OracleInterface + (((pSpecFold D x k s ++ₚ FinalFoldPhase.pSpec F ++ₚ QueryRound.pSpec D x l)).Challenge j) := + ProtocolSpec.challengeOracleInterface + /- Oracle reduction for all folding rounds of the FRI protocol -/ @[reducible] noncomputable def reductionFold : @@ -82,7 +94,7 @@ noncomputable def reductionFold : := OracleReduction.append (OracleReduction.seqCompose _ _ (fun (i : Fin (k + 1)) => Witness F s d i.castSucc) (FoldPhase.foldOracleReduction D x s d)) - (FinalFoldPhase.finalFoldOracleReduction D x (k := k) s d) + (FinalFoldPhase.finalFoldOracleReduction D x s d) /- Oracle reduction of the FRI protocol. -/ @[reducible] @@ -93,7 +105,7 @@ noncomputable def reduction [DecidableEq F] : (FinalStatement F k) (FinalOracleStatement D x s) (Witness F s d (Fin.last (k + 1))) (pSpecFold D x k s ++ₚ FinalFoldPhase.pSpec F ++ₚ QueryRound.pSpec D x l) := OracleReduction.append (reductionFold D x k s d) - (QueryRound.queryOracleReduction (k := k) D x s d dom_size_cond l) + (QueryRound.queryOracleReduction D x s d dom_size_cond l) end Spec diff --git a/ArkLib/ProofSystem/Fri/Spec/SingleRound.lean b/ArkLib/ProofSystem/Fri/Spec/SingleRound.lean index 9902f06e2..01e2f271f 100644 --- a/ArkLib/ProofSystem/Fri/Spec/SingleRound.lean +++ b/ArkLib/ProofSystem/Fri/Spec/SingleRound.lean @@ -82,7 +82,7 @@ def OracleStatement (i : Fin (k + 1)) : Fin (i.val + 1) → Type := def FinalOracleStatement : Fin (k + 2) → Type := fun j => if j.1 = k + 1 - then (Unit → F[X]) + then F[X] else (evalDomain D x (∑ j' ∈ finRangeTo j.1, s j') → F) /-- The FRI protocol has as witness the polynomial that is supposed to correspond to the codeword in @@ -92,7 +92,7 @@ def Witness (F : Type) [NonBinaryField F] {k : ℕ} (s : Fin (k + 1) → ℕ+) (d : ℕ+) (i : Fin (k + 2)) := F⦃< 2^((∑ j', (s j').1) - (∑ j' ∈ finRangeTo i.1, (s j').1)) * d⦄[X] -private lemma sum_add_one {i : Fin (k + 1)} : +private lemma sum_finRangeTo_add_one {i : Fin (k + 1)} : ∑ j' ∈ finRangeTo (i.1 + 1), (s j').1 = (∑ j' ∈ finRangeTo i.1, (s j').1) + (s i).1 := by rw [finRangeTo, List.take_add, List.toFinset_append] rw @@ -169,7 +169,7 @@ private lemma witness_lift {F : Type} [NonBinaryField F] rw [Nat.sub_sub_right b h', Nat.sub_add_comm h, Nat.add_comm] rw [←mul_assoc, ←pow_add, arith] · convert deg_bound - rw [sum_add_one] + rw [sum_finRangeTo_add_one] simp · simp only [ge_iff_le] apply sum_le_univ_sum_of_nonneg @@ -200,12 +200,7 @@ instance {i : Fin (k + 1)} : ∀ j, OracleInterface (OracleStatement D x s i j) instance : ∀ j, OracleInterface (FinalOracleStatement D x s j) := fun j => if h : j = k + 1 - then { - Query := Unit - Response := F[X] - answer := cast (by simp [h, FinalOracleStatement]) - (id (α := Unit → F[X])) - } + then OracleInterface.instDefault else { Query := ↑( @@ -242,7 +237,7 @@ lemma range_lem₂ : [FinalOracleStatement D x s]ₒ.range (Fin.last (k + 1)) = unfold OracleSpec.range FinalOracleStatement OracleInterface.toOracleSpec unfold OracleInterface.Query unfold instOracleInterfaceFinalOracleStatement - simp + aesop (add simp OracleInterface.instDefault) omit [Finite F] in @[simp] @@ -251,7 +246,7 @@ lemma domain_lem₂ : unfold OracleSpec.domain FinalOracleStatement OracleInterface.toOracleSpec unfold OracleInterface.Query unfold instOracleInterfaceFinalOracleStatement - simp + aesop (add simp OracleInterface.instDefault) namespace FoldPhase @@ -337,6 +332,9 @@ instance {i : Fin k} : ∀ j, OracleInterface ((pSpec D x s i).Message j) simp only [Fin.vcons_fin_zero, Nat.reduceAdd, Fin.isValue, Fin.vcons_one] infer_instance +instance {i : Fin k} : ∀ j, OracleInterface ((pSpec D x s i).Challenge j) := + ProtocolSpec.challengeOracleInterface + /-- The prover for the `i`-th round of the FRI protocol. It first receives the challenge, then does an `s` degree split of this polynomial. Finally, it returns the evaluation of this polynomial on the next evaluation domain. -/ @@ -491,15 +489,16 @@ def outputRelation (cond : ∑ i, (s i).1 ≤ n) [DecidableEq F] (δ : ℝ≥0) element as the challenge to the prover, then in contrast to the previous folding rounds simply sends the folded polynomial to the verifier. -/ @[reducible] -def pSpec (F : Type) [Semiring F] : ProtocolSpec 2 := ⟨!v[.V_to_P, .P_to_V], !v[F, Unit → F[X]]⟩ +def pSpec (F : Type) [Semiring F] : ProtocolSpec 2 := + ⟨!v[.V_to_P, .P_to_V], !v[F, F[X]]⟩ /- `OracleInterface` instance for the `pSpec` of the final folding round of the FRI protocol. -/ instance : ∀ j, OracleInterface ((pSpec F).Message j) | ⟨0, h⟩ => nomatch h - | ⟨1, _⟩ => by - unfold pSpec Message - simp only [Fin.vcons_fin_zero, Nat.reduceAdd, Fin.isValue, Fin.vcons_one] - exact OracleInterface.instFunction + | ⟨1, _⟩ => OracleInterface.instDefault + +/- `OracleInterface` instance for the `pSpec` of the final folding round of the FRI protocol. -/ +instance : ∀ j, OracleInterface ((pSpec F).Challenge j) := ProtocolSpec.challengeOracleInterface /- Prover for the final folding round of the FRI protocol. -/ noncomputable def finalFoldProver : @@ -522,7 +521,7 @@ noncomputable def finalFoldProver : sendMessage | ⟨0, h⟩ => nomatch h | ⟨1, _⟩ => fun ⟨⟨chals, o⟩, p⟩ => - pure ⟨fun x => p.1, ⟨⟨chals, o⟩, p⟩⟩ + pure ⟨p.1, ⟨⟨chals, o⟩, p⟩⟩ receiveChallenge | ⟨0, _⟩ => fun ⟨⟨chals, o⟩, p⟩ => pure <| @@ -546,7 +545,7 @@ noncomputable def finalFoldProver : unfold FinalOracleStatement if h : j.1 = k + 1 then - simpa [h] using fun x => p.1 + simpa [h] using p.1 else simpa [h, ↓reduceIte, OracleStatement, evalDomain] using o ⟨j.1, Nat.lt_of_le_of_ne (Fin.is_le j) h⟩ @@ -613,7 +612,7 @@ namespace QueryRound /- Parameter for the number of round consistency checks to be run by the query round. -/ -variable (l : ℕ) +variable (l : ℕ) [NeZero l] /- Input/Output relations for the query round of the FRI protocol -/ def inputRelation (cond : ∑ i, (s i).1 ≤ n) [DecidableEq F] (δ : ℝ≥0) : @@ -641,10 +640,13 @@ def pSpec : ProtocolSpec 1 := ⟨!v[.V_to_P], !v[Fin l → evalDomain D x 0]⟩ /- `OracleInterface` instances for the query round `pSpec`. -/ -instance : ∀ j, OracleInterface ((pSpec D x l).Message j) := fun j => +instance (priority := high) : ∀ j, OracleInterface ((pSpec D x l).Message j) := fun j => match j with | ⟨0, h⟩ => nomatch h +instance (priority := high) : ∀ j, OracleInterface ((pSpec D x l).Challenge j) := + ProtocolSpec.challengeOracleInterface + instance : ∀ j, OracleInterface ((pSpec D x l).Challenge j) := fun j => by unfold Challenge @@ -698,15 +700,16 @@ def getConst (k : ℕ) (s : Fin (k + 1) → ℕ+) : OracleComp [FinalOracleState (by simpa using ()) ) -private lemma roots_of_unity_lem {s : Fin (k + 1) → ℕ+} {i : Fin (k + 1)} +private lemma sum_finRangeTo_le_sub_of_le {s : Fin (k + 1) → ℕ+} {i : Fin (k + 1)} (k_le_n : (∑ j', (s j').1) ≤ n) : (∑ j' ∈ finRangeTo i.1, (s j').1) ≤ n - (s i).1 := by apply Nat.le_sub_of_add_le - rw [←sum_add_one] + rw [←sum_finRangeTo_add_one] transitivity · exact sum_le_univ_sum_of_nonneg (by simp) · exact k_le_n + /- Verifier for query round of the FRI protocol. Runs `l` checks on uniformly sampled points in the first evaluation domain against the oracles sent during every folding round. -/ @@ -727,20 +730,32 @@ noncomputable def queryVerifier (k_le_n : (∑ j', (s j').1) ≤ n) (l : ℕ) [D let s₀ : evalDomain D x (∑ j' ∈ finRangeTo i.1, (s j').1) := - ⟨_, pow_2_pow_i_mem_Di_of_mem_D _ s₀.2⟩ + ⟨_, pow_2_pow_i_mem_Di_of_mem_D s₀.2⟩ let queries : List ( evalDomain D x (∑ j' ∈ finRangeTo i.1, (s j').1) ) := List.map - (fun r => + (fun ind => + let r := + Domain.domainEnum D (⟨n - (s i).1, by grind⟩ : Fin (n + 1)) + ⟨ + ind.1, + by + have : (s i).1 ≤ n := by + refine le_trans ?_ k_le_n + apply Finset.single_le_sum + (f := fun j => (s j).1) (by aesop) (mem_univ _) + simp_all only [Nat.sub_sub_eq_min, inf_of_le_right, Fin.is_lt] + ⟩ ⟨ _, - CosetDomain.mul_root_of_unity D (roots_of_unity_lem k_le_n) s₀.2 r.2 + CosetDomain.mul_root_of_unity D + (sum_finRangeTo_le_sub_of_le k_le_n) s₀.2 r.2 ⟩ ) - (Domain.rootsOfUnity D n (s i)) + (List.finRange (2 ^ (s i).1)) let (pts : List (F × F)) ← List.mapM (fun q => queryCodeword D x k s q >>= fun v => pure (q.1.1, v)) @@ -750,7 +765,7 @@ noncomputable def queryVerifier (k_le_n : (∑ j', (s j').1) ≤ n) (l : ℕ) [D then have := CosetDomain.pow_lift D x (s i).1 s₀.2 queryCodeword D x k s (i := ⟨i.1.succ, Order.lt_add_one_iff.mpr h⟩) - ⟨_, by rw [←sum_add_one] at this; exact this⟩ + ⟨_, by rw [←sum_finRangeTo_add_one] at this; exact this⟩ else pure (p.eval (s₀.1.1 ^ (2 ^ (s (Fin.last k)).1))) guard (RoundConsistency.roundConsistencyCheck x₀ pts β) diff --git a/ArkLib/ToMathlib/Finset/Basic.lean b/ArkLib/ToMathlib/Finset/Basic.lean index 85fbdcb05..f9554dad2 100644 --- a/ArkLib/ToMathlib/Finset/Basic.lean +++ b/ArkLib/ToMathlib/Finset/Basic.lean @@ -6,6 +6,11 @@ Authors: František Silváši, Julian Sutherland, Ilia Vlasov import Mathlib.Algebra.Order.Ring.Nat import Mathlib.Algebra.Ring.Regular import Mathlib.Data.Finset.Image +import Mathlib.Algebra.BigOperators.Group.Finset.Defs +import ArkLib.ToMathlib.List.Basic +import Mathlib.Algebra.BigOperators.Group.Finset.Basic +import Mathlib.Data.PNat.Notation +import Mathlib.Algebra.Order.BigOperators.Group.Finset /-! # Definitions and lemmas related to `Finset`. @@ -108,3 +113,23 @@ theorem shift_left_mem {s : Finset ℕ} {d : ℕ} : d ∈ shift_left s ↔ (d + @[simp] def finRangeTo {k : ℕ} (i : ℕ) : Finset (Fin k) := (List.take i (List.finRange k)).toFinset + +@[simp] +lemma sum_finRangeTo_add_one {n} {i : Fin (n + 1)} {f : Fin (n + 1) → ℕ} : + ∑ j' ∈ finRangeTo (i + 1), f j' = (∑ j' ∈ finRangeTo i, f j') + f i := by + unfold finRangeTo + suffices ∑ x ∈ insert i (List.take i (List.finRange (n + 1))).toFinset, f x = + ∑ x ∈ (List.take i (List.finRange (n + 1))).toFinset, f x + f i by + simpa [List.take_add] + have : i ∉ (List.take i (List.finRange (n + 1))).toFinset := by + aesop (add simp List.mem_iff_getElem) (add safe (by grind [cases Fin])) + simp +arith [Finset.sum_insert this] + +lemma sum_finRangeTo_le_sub_of_le {n k : ℕ} {s : Fin (k + 1) → ℕ+} {i : Fin (k + 1)} + (k_le_n : ∑ j', (s j' : ℕ) ≤ n) : + ∑ j' ∈ finRangeTo i, (s j' : ℕ) ≤ n - (s i : ℕ) := by + apply Nat.le_sub_of_add_le + rw [←sum_finRangeTo_add_one] + transitivity + · exact Finset.sum_le_univ_sum_of_nonneg (by simp) + · exact k_le_n diff --git a/ArkLib/ToMathlib/List/Basic.lean b/ArkLib/ToMathlib/List/Basic.lean new file mode 100644 index 000000000..2c0283acf --- /dev/null +++ b/ArkLib/ToMathlib/List/Basic.lean @@ -0,0 +1,9 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: František Silváši, Julian Sutherland, Ilia Vlasov +-/ + +@[simp, grind =] +theorem List.take_one_eq_head.{u} {α : Type u} {l : List α} (h : l ≠ []) : + l.take 1 = [l.head h] := by grind [cases List]