diff --git a/ArkLib.lean b/ArkLib.lean index 17b094706a..6d0e2f3f45 100644 --- a/ArkLib.lean +++ b/ArkLib.lean @@ -205,12 +205,10 @@ import ArkLib.ProofSystem.ConstraintSystem.R1CS import ArkLib.ProofSystem.Fri.RoundConsistency import ArkLib.ProofSystem.Fri.Spec.General import ArkLib.ProofSystem.Fri.Spec.SingleRound -import ArkLib.ProofSystem.Logup.Common +import ArkLib.ProofSystem.Logup.Algebra import ArkLib.ProofSystem.Logup.Protocol import ArkLib.ProofSystem.Logup.Security.Completeness import ArkLib.ProofSystem.Logup.Security.Soundness -import ArkLib.ProofSystem.Logup.Sumcheck.SumcheckBridge -import ArkLib.ProofSystem.Logup.Sumcheck.SumcheckPolynomial import ArkLib.ProofSystem.Plonk.Basic import ArkLib.ProofSystem.Spartan.Basic import ArkLib.ProofSystem.Stir.Combine diff --git a/ArkLib/ProofSystem/Logup/Algebra.lean b/ArkLib/ProofSystem/Logup/Algebra.lean new file mode 100644 index 0000000000..d625e76d59 --- /dev/null +++ b/ArkLib/ProofSystem/Logup/Algebra.lean @@ -0,0 +1,873 @@ +import ArkLib.Data.MvPolynomial.Multilinear +import Mathlib.Algebra.Order.Floor.Div + +/-! +# LogUp algebra and sumcheck polynomial + +This file contains the algebra used to express LogUp as a sumcheck claim and tries to be decoupled +from the protocol types. It works with plain hypercube functions `(Fin n → Fin 2) → F`, polynomial +inputs `MvPolynomial (Fin n) F`, challenges, and partial-sum groups. + +The main output is `logupQPolynomial`, the polynomial `Q` that the protocol sends to sumcheck, plus +`logupQPolynomial_degreeOf`, the individual-degree bound needed by sumcheck. The row-level and +point-level definitions in this file are the semantic versions used to connect `Q` back to honest +LogUp data and to the verifier's final point check. + +## Sections + +* **Generic batched polynomial** is the abstract polynomial shape used by the sumcheck claim, with + its generic individual-degree bound. The later LogUp proof only has to show its ingredients are + multilinear. +* **Term indexing** names the `M + 1` fractional terms and relates the table/column oracle labels to + paper indices `0, …, M`. +* **Fractional decompositions in `F[X]`** are the protocol-independent, paper-shaped statements over + the polynomial ring (cleared-denominator form): uniqueness of fractional decompositions + (Lemma 4), the collecting bridge, and the set-inclusion criterion (Lemma 5). +* **Fractional-identity algebra** builds the row-wise LogUp quantities on the Boolean hypercube: + normalized multiplicities, logarithmic-derivative terms, helper groups, and the row value + `qOnHypercube`. +* **Final-point reconstructions** rebuilds the same value from the verifier's scalar oracle answers + at sumcheck's final point `r`. +* **The LogUp polynomial** assembles the concrete polynomial `Q` from the input polynomials and + proves the individual-degree bound required by ArkLib's generic sumcheck protocol. +* **Polynomial evaluation agreement** shows `Q` agrees on Boolean rows with the row-wise expression + built from its inputs' Boolean evaluations. +-/ + +namespace Logup + +open scoped BigOperators + +/-! ## Generic batched polynomial -/ + +section BatchedPolynomial + +variable {F : Type} [Field F] {n T K : ℕ} +variable (groups : Fin K → Finset (Fin T)) +variable (phiPoly numerPoly : Fin T → MvPolynomial (Fin n) F) +variable (helperPoly : Fin K → MvPolynomial (Fin n) F) + +/-- One group's cleared-denominator identity, as a polynomial in abstract per-term denominator +(`phiPoly`) and numerator (`numerPoly`) polynomials and per-group helper polynomials. -/ +noncomputable def batchedDomainIdentity (k : Fin K) : MvPolynomial (Fin n) F := + helperPoly k * (∏ i ∈ groups k, phiPoly i) - + ∑ i ∈ groups k, numerPoly i * ∏ j ∈ (groups k).erase i, phiPoly j + +/-- The generic batched sumcheck polynomial: a `λ`-batched sum of per-group cleared-denominator +identities, weighted by an equality kernel. Independent of any particular protocol. -/ +noncomputable def batchedSumcheckPolynomial + (zChallenge : Fin n → F) (batchingScalars : Fin K → F) : MvPolynomial (Fin n) F := + ∑ k : Fin K, (helperPoly k + + MvPolynomial.eqPolynomial zChallenge * MvPolynomial.C (batchingScalars k) * + batchedDomainIdentity groups phiPoly numerPoly helperPoly k) + +private theorem prod_phiPoly_degreeOf + (hphi : ∀ i v, MvPolynomial.degreeOf v (phiPoly i) ≤ 1) + (s : Finset (Fin T)) (v : Fin n) : + MvPolynomial.degreeOf v (∏ i ∈ s, phiPoly i) ≤ T := by + calc + _ ≤ ∑ i ∈ s, MvPolynomial.degreeOf v (phiPoly i) := MvPolynomial.degreeOf_prod_le v _ _ + _ ≤ ∑ _i ∈ s, 1 := Finset.sum_le_sum (fun i _ => hphi i v) + _ = s.card := by simp + _ ≤ T := le_trans (Finset.card_le_univ s) (by simp) + +/-- Each group identity has individual degree at most `T + 1`. -/ +theorem batchedDomainIdentity_degreeOf + (hphi : ∀ i v, MvPolynomial.degreeOf v (phiPoly i) ≤ 1) + (hnumer : ∀ i v, MvPolynomial.degreeOf v (numerPoly i) ≤ 1) + (hhelper : ∀ k v, MvPolynomial.degreeOf v (helperPoly k) ≤ 1) + (k : Fin K) (v : Fin n) : + MvPolynomial.degreeOf v (batchedDomainIdentity groups phiPoly numerPoly helperPoly k) + ≤ T + 1 := by + unfold batchedDomainIdentity + have hLeft : + MvPolynomial.degreeOf v (helperPoly k * (∏ i ∈ groups k, phiPoly i)) ≤ T + 1 := by + calc + _ ≤ MvPolynomial.degreeOf v (helperPoly k) + + MvPolynomial.degreeOf v (∏ i ∈ groups k, phiPoly i) := MvPolynomial.degreeOf_mul_le v _ _ + _ ≤ 1 + T := by + gcongr + · exact hhelper k v + · exact prod_phiPoly_degreeOf phiPoly hphi (groups k) v + _ = T + 1 := by omega + have hRight : + MvPolynomial.degreeOf v + (∑ i ∈ groups k, numerPoly i * ∏ j ∈ (groups k).erase i, phiPoly j) ≤ T + 1 := by + calc + _ ≤ (groups k).sup fun i => + MvPolynomial.degreeOf v (numerPoly i * ∏ j ∈ (groups k).erase i, phiPoly j) := + MvPolynomial.degreeOf_sum_le v _ _ + _ ≤ T + 1 := by + apply Finset.sup_le + intro i _ + calc + _ ≤ MvPolynomial.degreeOf v (numerPoly i) + + MvPolynomial.degreeOf v (∏ j ∈ (groups k).erase i, phiPoly j) := + MvPolynomial.degreeOf_mul_le v _ _ + _ ≤ 1 + T := by + gcongr + · exact hnumer i v + · exact prod_phiPoly_degreeOf phiPoly hphi ((groups k).erase i) v + _ = T + 1 := by omega + exact (MvPolynomial.degreeOf_sub_le v _ _).trans (max_le hLeft hRight) + +/-- The batched polynomial has individual degree at most `T + 2`. -/ +theorem batchedSumcheckPolynomial_degreeOf + (zChallenge : Fin n → F) (batchingScalars : Fin K → F) + (hphi : ∀ i v, MvPolynomial.degreeOf v (phiPoly i) ≤ 1) + (hnumer : ∀ i v, MvPolynomial.degreeOf v (numerPoly i) ≤ 1) + (hhelper : ∀ k v, MvPolynomial.degreeOf v (helperPoly k) ≤ 1) + (v : Fin n) : + MvPolynomial.degreeOf v + (batchedSumcheckPolynomial groups phiPoly numerPoly helperPoly zChallenge batchingScalars) + ≤ T + 2 := by + unfold batchedSumcheckPolynomial + calc + _ ≤ (Finset.univ : Finset (Fin K)).sup fun k => + MvPolynomial.degreeOf v + (helperPoly k + + MvPolynomial.eqPolynomial zChallenge * MvPolynomial.C (batchingScalars k) * + batchedDomainIdentity groups phiPoly numerPoly helperPoly k) := + MvPolynomial.degreeOf_sum_le v _ _ + _ ≤ T + 2 := by + apply Finset.sup_le + intro k _ + have hHelper : + MvPolynomial.degreeOf v (helperPoly k) ≤ T + 2 := (hhelper k v).trans (by omega) + have hProduct : + MvPolynomial.degreeOf v + (MvPolynomial.eqPolynomial zChallenge * MvPolynomial.C (batchingScalars k) * + batchedDomainIdentity groups phiPoly numerPoly helperPoly k) ≤ T + 2 := by + calc + _ ≤ MvPolynomial.degreeOf v + (MvPolynomial.eqPolynomial zChallenge * MvPolynomial.C (batchingScalars k)) + + MvPolynomial.degreeOf v + (batchedDomainIdentity groups phiPoly numerPoly helperPoly k) := + MvPolynomial.degreeOf_mul_le v _ _ + _ ≤ (MvPolynomial.degreeOf v (MvPolynomial.eqPolynomial zChallenge) + + MvPolynomial.degreeOf v (MvPolynomial.C (batchingScalars k))) + + MvPolynomial.degreeOf v + (batchedDomainIdentity groups phiPoly numerPoly helperPoly k) := by + gcongr + exact MvPolynomial.degreeOf_mul_le v _ _ + _ ≤ (1 + 0) + (T + 1) := by + gcongr + · exact MvPolynomial.eqPolynomial_degreeOf (R := F) zChallenge v + · exact (MvPolynomial.degreeOf_C (R := F) (batchingScalars k) v).le + · exact batchedDomainIdentity_degreeOf groups phiPoly numerPoly helperPoly + hphi hnumer hhelper k v + _ = T + 2 := by omega + exact (MvPolynomial.degreeOf_add_le v _ _).trans (max_le hHelper hProduct) + +end BatchedPolynomial + +/-! ## Term indexing + +LogUp has `M + 1` terms: term `0` is the table, terms `1, …, M` are the lookup columns. -/ + +/-- Labels for the `M + 1` LogUp terms: the table and the `M` lookup columns. -/ +inductive InputIdx (M : ℕ) where + | table : InputIdx M + | column : Fin M → InputIdx M +deriving DecidableEq + +/-- Term labels `0, ..., M` from the paper, with `0` denoting the table term. -/ +@[reducible] +def TermIdx (M : ℕ) : Type := + Fin (M + 1) + +/-- Interpret term index `0` as the table and term indices `1, ..., M` as lookup columns. -/ +def termToInput {M : ℕ} (i : TermIdx M) : InputIdx M := + if h : i.val = 0 then .table else .column ⟨i.val - 1, by omega⟩ + +/-- Interpret a table/column label as its term index `0, ..., M`. -/ +def inputToTerm {M : ℕ} : InputIdx M → TermIdx M + | .table => ⟨0, by omega⟩ + | .column i => ⟨i.val + 1, by omega⟩ + +@[simp] +theorem termToInput_inputToTerm {M : ℕ} (i : InputIdx M) : + termToInput (inputToTerm i) = i := by + cases i <;> simp [termToInput, inputToTerm] + +@[simp] +theorem inputToTerm_termToInput {M : ℕ} (i : TermIdx M) : + inputToTerm (termToInput i) = i := by + unfold termToInput + split + · next h => exact Fin.ext h.symm + · next h => apply Fin.ext; simp only [inputToTerm]; omega + +/-! ## Fractional decompositions in `F[X]` (paper Section 2.3) + +Paper-shaped statements over the polynomial ring `F[X]`, in cleared-denominator form: +`clearedDecomp` is the numerator left after multiplying the formal `∑_z m(z)/(X + z)` by the common +denominator `∏_{w∈F}(X + w)`. Working in `F[X]` (rather than `RatFunc F`) keeps these formal and +dependency-light. We prove `clearedDecomp`'s uniqueness (Lemma 4), the "collecting" bridge +`clearedSum_eq_clearedDecomp`, and the set-inclusion criterion (Lemma 5). -/ + +section FractionalDecomposition + +open Polynomial + +variable {F : Type} [Field F] [Fintype F] [DecidableEq F] + +/-- The cleared-denominator decomposition `∑_{z ∈ F} m(z) · ∏_{w ≠ z}(X + w)` in `F[X]`: the +numerator left after multiplying the formal `∑_z m(z)/(X + z)` by `∏_{w∈F}(X + w)`. -/ +noncomputable def clearedDecomp (m : F → F) : F[X] := + ∑ z : F, C (m z) * ∏ w ∈ Finset.univ.erase z, (X + C w) + +/-- **Lemma 4** (uniqueness of fractional decompositions). Over a finite field the coefficient map +`m ↦ clearedDecomp m` is injective: two cleared decompositions coincide in `F[X]` iff their +coefficient functions agree everywhere. -/ +theorem clearedDecomp_injective {m₁ m₂ : F → F} : + clearedDecomp m₁ = clearedDecomp m₂ ↔ m₁ = m₂ := by + refine ⟨fun H => ?_, fun H => by rw [H]⟩ + funext w + -- The coefficient-difference decomposition is the zero polynomial. + have hp0 : (∑ z : F, C (m₁ z - m₂ z) * ∏ u ∈ Finset.univ.erase z, (X + C u)) = 0 := by + have hsub : clearedDecomp m₁ - clearedDecomp m₂ = 0 := by rw [H, sub_self] + rw [clearedDecomp, clearedDecomp, ← Finset.sum_sub_distrib] at hsub + rw [← hsub] + exact Finset.sum_congr rfl (fun z _ => by rw [map_sub, sub_mul]) + -- Evaluating at `-w` isolates the `w`-th coefficient. + have heval := congrArg (Polynomial.eval (-w)) hp0 + simp only [Polynomial.eval_finsetSum, Polynomial.eval_mul, Polynomial.eval_C, + Polynomial.eval_prod, Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_zero] at heval + have hsingle : (∑ z : F, (m₁ z - m₂ z) * ∏ u ∈ Finset.univ.erase z, (-w + u)) + = (m₁ w - m₂ w) * ∏ u ∈ Finset.univ.erase w, (-w + u) := by + refine Finset.sum_eq_single w (fun z _ hzw => ?_) + (fun h => absurd (Finset.mem_univ w) h) + have hwmem : w ∈ Finset.univ.erase z := + Finset.mem_erase.mpr ⟨fun hwz => hzw hwz.symm, Finset.mem_univ w⟩ + exact mul_eq_zero_of_right _ (Finset.prod_eq_zero hwmem (neg_add_cancel w)) + rw [hsingle] at heval + have hprodne : (∏ u ∈ Finset.univ.erase w, (-w + u)) ≠ 0 := by + rw [Finset.prod_ne_zero_iff] + intro u hu hzero + rw [Finset.mem_erase] at hu + exact hu.1 (neg_injective (add_eq_zero_iff_eq_neg.mp hzero)).symm + exact sub_eq_zero.mp ((mul_eq_zero.mp heval).resolve_right hprodne) + +/-- "Collecting": an indexed sum of cleared single terms `∑ i, c i · ∏_{w ≠ a i}(X + w)` equals the +cleared decomposition whose coefficient at `z` is the total weight `∑_{a i = z} c i`. This is the +bridge between sequence-indexed sums (the protocol side) and `clearedDecomp` (Lemmas 4/5). -/ +theorem clearedSum_eq_clearedDecomp {ι : Type*} [Fintype ι] (a c : ι → F) : + (∑ i, C (c i) * ∏ w ∈ Finset.univ.erase (a i), (X + C w)) + = clearedDecomp (fun z => ∑ i ∈ Finset.univ.filter (fun i => a i = z), c i) := by + unfold clearedDecomp + rw [← Finset.sum_fiberwise (Finset.univ : Finset ι) a + (fun i => C (c i) * ∏ w ∈ Finset.univ.erase (a i), (X + C w))] + refine Finset.sum_congr rfl (fun z _ => ?_) + rw [map_sum, Finset.sum_mul] + refine Finset.sum_congr rfl (fun i hi => ?_) + rw [Finset.mem_filter] at hi + rw [hi.2] + +/-- The multiplicity of a value `z` in a finite sequence `a : ι → F`. -/ +def seqMultiplicity {ι : Type*} [Fintype ι] (a : ι → F) (z : F) : ℕ := + (Finset.univ.filter fun i => a i = z).card + +/-- **Lemma 5** (set inclusion), cleared-denominator form. When the field characteristic exceeds the +sizes of the index types, the set underlying `a` is contained in that of `b` iff there exist +multiplicities `m` making the cleared logarithmic-derivative identity hold in `F[X]` (the cleared +form of `∑_i 1/(X + a i) = ∑_j m j/(X + b j)`). The honest witness is the normalized multiplicity +`m j = ma(b j)/mb(b j)`. Generalizes the paper's equal-length sequences to arbitrary index types. -/ +theorem setInclusion_iff_cleared {ι κ : Type*} [Fintype ι] [Fintype κ] + (hNa : Fintype.card ι < ringChar F) (hNb : Fintype.card κ < ringChar F) + (a : ι → F) (b : κ → F) : + (∀ i, ∃ j, a i = b j) ↔ + ∃ m : κ → F, + (∑ i, ∏ w ∈ Finset.univ.erase (a i), (X + C w)) + = ∑ j, C (m j) * ∏ w ∈ Finset.univ.erase (b j), (X + C w) := by + -- Nonzero-cast of multiplicities: any count below `ringChar F` survives. + have hcastne : ∀ k : ℕ, 0 < k → k < ringChar F → (k : F) ≠ 0 := by + intro k hk hkr hzero + exact (Nat.not_dvd_of_pos_of_lt hk hkr) ((ringChar.spec F k).1 hzero) + have hleA : ∀ w : F, seqMultiplicity a w ≤ Fintype.card ι := by + intro w + calc seqMultiplicity a w ≤ (Finset.univ : Finset ι).card := Finset.card_filter_le _ _ + _ = Fintype.card ι := Finset.card_univ + have hleB : ∀ w : F, seqMultiplicity b w ≤ Fintype.card κ := by + intro w + calc seqMultiplicity b w ≤ (Finset.univ : Finset κ).card := Finset.card_filter_le _ _ + _ = Fintype.card κ := Finset.card_univ + have hcast : ∀ z : F, (∑ _i ∈ Finset.univ.filter (fun i => a i = z), (1 : F)) + = (seqMultiplicity a z : F) := by + intro z; rw [Finset.sum_const, nsmul_eq_mul, mul_one]; rfl + -- Collecting turns each side into a `clearedDecomp`. + have hL : (∑ i, ∏ w ∈ Finset.univ.erase (a i), (X + C w)) + = clearedDecomp (fun z => (seqMultiplicity a z : F)) := by + have h1 : (∑ i, ∏ w ∈ Finset.univ.erase (a i), (X + C w)) + = ∑ i, C (1 : F) * ∏ w ∈ Finset.univ.erase (a i), (X + C w) := by simp + rw [h1, clearedSum_eq_clearedDecomp a (fun _ => 1)] + exact congrArg clearedDecomp (funext (fun z => hcast z)) + have hR : ∀ m : κ → F, (∑ j, C (m j) * ∏ w ∈ Finset.univ.erase (b j), (X + C w)) + = clearedDecomp (fun z => ∑ j ∈ Finset.univ.filter (fun j => b j = z), m j) := + fun m => clearedSum_eq_clearedDecomp b m + -- By Lemma 4 the identity is exactly fiberwise equality of total weights. + have key : ∀ m : κ → F, + ((∑ i, ∏ w ∈ Finset.univ.erase (a i), (X + C w)) + = ∑ j, C (m j) * ∏ w ∈ Finset.univ.erase (b j), (X + C w)) + ↔ ∀ z : F, (seqMultiplicity a z : F) + = ∑ j ∈ Finset.univ.filter (fun j => b j = z), m j := by + intro m + rw [hL, hR m, clearedDecomp_injective] + exact funext_iff + constructor + · -- Forward: the normalized multiplicity is a valid witness. + intro hinc + refine ⟨fun j => (seqMultiplicity a (b j) : F) / (seqMultiplicity b (b j) : F), (key _).2 ?_⟩ + intro z + by_cases hz : seqMultiplicity a z = 0 + · rw [hz, Nat.cast_zero] + symm + refine Finset.sum_eq_zero (fun j hj => ?_) + rw [Finset.mem_filter] at hj + rw [hj.2, hz, Nat.cast_zero, zero_div] + · obtain ⟨i₀, hi₀⟩ := + Finset.card_ne_zero.mp (show (Finset.univ.filter (fun i => a i = z)).card ≠ 0 from hz) + rw [Finset.mem_filter] at hi₀ + obtain ⟨j₀, hj₀⟩ := hinc i₀ + have hbz_ne : seqMultiplicity b z ≠ 0 := by + refine Finset.card_ne_zero.mpr ⟨j₀, Finset.mem_filter.mpr ⟨Finset.mem_univ j₀, ?_⟩⟩ + rw [hj₀.symm.trans hi₀.2] + have hconst : ∀ j ∈ Finset.univ.filter (fun j => b j = z), + (seqMultiplicity a (b j) : F) / (seqMultiplicity b (b j) : F) + = (seqMultiplicity a z : F) / (seqMultiplicity b z : F) := by + intro j hj; rw [Finset.mem_filter] at hj; rw [hj.2] + have hcard : ((Finset.univ.filter (fun j => b j = z)).card : F) = (seqMultiplicity b z : F) := + rfl + rw [Finset.sum_congr rfl hconst, Finset.sum_const, nsmul_eq_mul, hcard] + have hbzF : (seqMultiplicity b z : F) ≠ 0 := + hcastne _ (Nat.pos_of_ne_zero hbz_ne) (lt_of_le_of_lt (hleB z) hNb) + field_simp + · -- Converse: a value of `a` has nonzero multiplicity, so its fiber in `b` is nonempty. + rintro ⟨m, hm⟩ i + have hcoef := (key m).1 hm (a i) + by_contra hcon + simp only [not_exists] at hcon + have hempty : Finset.univ.filter (fun j => b j = a i) = ∅ := by + rw [Finset.filter_eq_empty_iff] + exact fun j _ hbj => hcon j hbj.symm + rw [hempty, Finset.sum_empty] at hcoef + have hpos : 0 < seqMultiplicity a (a i) := + Finset.card_pos.mpr ⟨i, Finset.mem_filter.mpr ⟨Finset.mem_univ i, rfl⟩⟩ + exact hcastne _ hpos (lt_of_le_of_lt (hleA (a i)) hNa) hcoef + +set_option linter.unusedFintypeInType false in +/-- **Lemma 5**, forward direction evaluated at a point `x` (paper eq. (15)). If every value of `a` +occurs among the values of `b`, then the logarithmic-derivative identity holds at `x` with the +normalized multiplicity `seqMultiplicity a (b j) / seqMultiplicity b (b j)` as witness. This is the +evaluated specialization that the completeness proof consumes; the formal `F[X]` statement is +`setInclusion_iff_cleared`. The hypothesis `hchar` (that a nonzero `a`-multiplicity forces a nonzero +`b`-multiplicity in `F`) packages set inclusion together with the characteristic bound, exactly as +in the protocol. Lean's `_ / 0 = 0` convention makes pole hypotheses unnecessary. -/ +theorem setInclusion_eval_forward {ι κ : Type*} [Fintype ι] [Fintype κ] + (a : ι → F) (b : κ → F) (x : F) + (hchar : ∀ z : F, seqMultiplicity a z ≠ 0 → (seqMultiplicity b z : F) ≠ 0) : + (∑ i, (1 : F) / (x + a i)) + = ∑ j, (seqMultiplicity a (b j) : F) / (seqMultiplicity b (b j) : F) / (x + b j) := by + have key : ∀ z : F, + seqMultiplicity b z • ((seqMultiplicity a z : F) / (seqMultiplicity b z : F) / (x + z)) + = seqMultiplicity a z • ((1 : F) / (x + z)) := by + intro z + by_cases ha : seqMultiplicity a z = 0 + · simp [ha] + · rw [nsmul_eq_mul, nsmul_eq_mul] + have hbF : (seqMultiplicity b z : F) ≠ 0 := hchar z ha + field_simp + have hLHS : (∑ i, (1 : F) / (x + a i)) + = ∑ z : F, seqMultiplicity a z • ((1 : F) / (x + z)) := by + rw [← Finset.sum_fiberwise (Finset.univ : Finset ι) a] + refine Finset.sum_congr rfl (fun z _ => ?_) + have h : ∀ i ∈ Finset.univ.filter (fun i => a i = z), + (1 : F) / (x + a i) = (1 : F) / (x + z) := + fun i hi => by rw [Finset.mem_filter] at hi; rw [hi.2] + rw [Finset.sum_congr rfl h, Finset.sum_const] + rfl + have hRHS : (∑ j, (seqMultiplicity a (b j) : F) / (seqMultiplicity b (b j) : F) / (x + b j)) + = ∑ z : F, seqMultiplicity b z • + ((seqMultiplicity a z : F) / (seqMultiplicity b z : F) / (x + z)) := by + rw [← Finset.sum_fiberwise (Finset.univ : Finset κ) b] + refine Finset.sum_congr rfl (fun z _ => ?_) + have h : ∀ j ∈ Finset.univ.filter (fun j => b j = z), + (seqMultiplicity a (b j) : F) / (seqMultiplicity b (b j) : F) / (x + b j) + = (seqMultiplicity a z : F) / (seqMultiplicity b z : F) / (x + z) := + fun j hj => by rw [Finset.mem_filter] at hj; rw [hj.2] + rw [Finset.sum_congr rfl h, Finset.sum_const] + rfl + rw [hLHS, hRHS] + exact Finset.sum_congr rfl (fun z _ => (key z).symm) + +end FractionalDecomposition + +/-! ## Fractional-identity algebra + +LogUp's logarithmic-derivative construction, evaluated on hypercube rows. The table, columns, +multiplicity, and helper functions are bare hypercube functions `(Fin n → Fin 2) → F`. -/ + +section Algebra + +variable {F : Type} [Field F] {n M K : ℕ} + +/-- Number of table rows with value `a`. -/ +def tableMultiplicityCount [Fintype F] [DecidableEq F] (table : (Fin n → Fin 2) → F) (a : F) : ℕ := + ((Finset.univ : Finset (Fin n → Fin 2)).filter fun u => table u = a).card + +/-- Total number of lookup-column entries with value `a`. -/ +def lookupMultiplicityCount [Fintype F] [DecidableEq F] + (columns : Fin M → (Fin n → Fin 2) → F) (a : F) : ℕ := + ((Finset.univ : Finset (Fin M × (Fin n → Fin 2))).filter fun ix => columns ix.1 ix.2 = a).card + +/-- The normalized multiplicity from paper equation (14), evaluated at one table row. -/ +noncomputable def normalizedMultiplicityValue [Fintype F] [DecidableEq F] + (table : (Fin n → Fin 2) → F) (columns : Fin M → (Fin n → Fin 2) → F) (u : Fin n → Fin 2) : F := + let a := table u + (lookupMultiplicityCount columns a : F) / (tableMultiplicityCount table a : F) + +/-- The denominator term `φᵢ(u)` from Protocol 2. -/ +noncomputable def phi (table : (Fin n → Fin 2) → F) (columns : Fin M → (Fin n → Fin 2) → F) + (xChallenge : F) : InputIdx M → (Fin n → Fin 2) → F + | .table => fun u => xChallenge + table u + | .column i => fun u => xChallenge + columns i u + +/-- The numerator term `mᵢ(u)`, with `m₀ = m` and `mᵢ = -1` for columns. -/ +noncomputable def numerator (multiplicity : (Fin n → Fin 2) → F) : + InputIdx M → (Fin n → Fin 2) → F + | .table => multiplicity + | .column _ => fun _ => -1 + +/-- The denominator term, indexed as `0, ..., M` as in the paper. -/ +noncomputable def termPhi (table : (Fin n → Fin 2) → F) (columns : Fin M → (Fin n → Fin 2) → F) + (xChallenge : F) (i : TermIdx M) (u : Fin n → Fin 2) : F := + phi table columns xChallenge (termToInput i) u + +/-- The numerator term, indexed as `0, ..., M` as in the paper. -/ +noncomputable def termNumerator (multiplicity : (Fin n → Fin 2) → F) + (i : TermIdx M) (u : Fin n → Fin 2) : F := + numerator multiplicity (termToInput i) u + +/-- The domain-identity expression for one helper function `hₖ`. -/ +noncomputable def domainIdentityTerm (groups : Fin K → Finset (TermIdx M)) + (table : (Fin n → Fin 2) → F) (columns : Fin M → (Fin n → Fin 2) → F) + (multiplicity : (Fin n → Fin 2) → F) (helpers : Fin K → (Fin n → Fin 2) → F) + (xChallenge : F) (k : Fin K) (u : Fin n → Fin 2) : F := + helpers k u * (∏ i ∈ groups k, termPhi table columns xChallenge i u) - + ∑ i ∈ groups k, termNumerator multiplicity i u * ∏ j + ∈ (groups k).erase i, termPhi table columns xChallenge j u + +/-- The helper value `hₖ(u) = Σᵢ mᵢ(u)/φᵢ(u)` from paper equation (16). -/ +noncomputable def helperValue (groups : Fin K → Finset (TermIdx M)) + (table : (Fin n → Fin 2) → F) (columns : Fin M → (Fin n → Fin 2) → F) + (multiplicity : (Fin n → Fin 2) → F) (xChallenge : F) (k : Fin K) (u : Fin n → Fin 2) : F := + ∑ i ∈ groups k, termNumerator multiplicity i u / termPhi table columns xChallenge i u + +/-- The batched polynomial expression `Q` from paper equation (18), evaluated on a row `u ∈ H`. -/ +noncomputable def qOnHypercube (groups : Fin K → Finset (TermIdx M)) + (table : (Fin n → Fin 2) → F) (columns : Fin M → (Fin n → Fin 2) → F) + (multiplicity : (Fin n → Fin 2) → F) (helpers : Fin K → (Fin n → Fin 2) → F) + (xChallenge : F) (zChallenge : Fin n → F) (batchingScalars : Fin K → F) + (u : Fin n → Fin 2) : F := + ∑ k : Fin K, ( + helpers k u + + MvPolynomial.eval (u : Fin n → F) (MvPolynomial.eqPolynomial zChallenge) * + batchingScalars k * + domainIdentityTerm groups table columns multiplicity helpers xChallenge k u) + +/-- Honest helper values make the cleared-denominator identity vanish pointwise, away from poles. -/ +theorem domainIdentityTerm_eq_zero (groups : Fin K → Finset (TermIdx M)) + (table : (Fin n → Fin 2) → F) (columns : Fin M → (Fin n → Fin 2) → F) + (multiplicity : (Fin n → Fin 2) → F) (helpers : Fin K → (Fin n → Fin 2) → F) + (xChallenge : F) (k : Fin K) (u : Fin n → Fin 2) + (hh : helpers k u = helperValue groups table columns multiplicity xChallenge k u) + (hφ : ∀ i ∈ groups k, termPhi table columns xChallenge i u ≠ 0) : + domainIdentityTerm groups table columns multiplicity helpers xChallenge k u = 0 := by + rw [domainIdentityTerm, hh, helperValue, Finset.sum_mul, sub_eq_zero] + refine Finset.sum_congr rfl (fun i hi => ?_) + rw [← Finset.mul_prod_erase _ _ hi] + field_simp [hφ i hi] + +/-- If a lookup value appears in a column and every lookup value appears in the table, then the +corresponding table multiplicity is nonzero as a field element under the LogUp characteristic +bound. -/ +theorem tableMultiplicityCount_cast_ne_zero_of_lookupMultiplicityCount_ne_zero [Fintype F] + [DecidableEq F] (hcharLarge : M * 2 ^ n < ringChar F) + (table : (Fin n → Fin 2) → F) (columns : Fin M → (Fin n → Fin 2) → F) + (hcols : ∀ j : Fin M, ∀ u : Fin n → Fin 2, ∃ v : Fin n → Fin 2, + columns j u = table v) + {a : F} (hlookup : lookupMultiplicityCount columns a ≠ 0) : + (tableMultiplicityCount table a : F) ≠ 0 := by + classical + have hlookupCard : + ((Finset.univ : Finset (Fin M × (Fin n → Fin 2))).filter fun ix => + columns ix.1 ix.2 = a).card ≠ 0 := by + simpa [lookupMultiplicityCount] using hlookup + obtain ⟨⟨j, u⟩, hju⟩ := Finset.card_ne_zero.mp hlookupCard + simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hju + obtain ⟨v, hv⟩ := hcols j u + have hvTable : table v = a := hv.symm.trans hju + have htablePos : 0 < tableMultiplicityCount table a := by + rw [tableMultiplicityCount, Finset.card_pos] + exact ⟨v, by simp [hvTable]⟩ + have hMpos : 0 < M := lt_of_le_of_lt (Nat.zero_le j.val) j.isLt + have htable_le_card : + tableMultiplicityCount table a ≤ Fintype.card (Fin n → Fin 2) := by + rw [tableMultiplicityCount, ← Finset.card_univ] + exact Finset.card_filter_le _ _ + have hcard_hypercube : Fintype.card (Fin n → Fin 2) = 2 ^ n := by + simp + have hpow_le : 2 ^ n ≤ M * 2 ^ n := by + have hMone : 1 ≤ M := Nat.succ_le_of_lt hMpos + nth_rewrite 1 [← Nat.one_mul (2 ^ n)] + exact Nat.mul_le_mul_right (2 ^ n) hMone + have htable_lt_char : tableMultiplicityCount table a < ringChar F := by + calc + tableMultiplicityCount table a ≤ Fintype.card (Fin n → Fin 2) := htable_le_card + _ = 2 ^ n := hcard_hypercube + _ ≤ M * 2 ^ n := hpow_le + _ < ringChar F := hcharLarge + intro hzero + have hdvd : ringChar F ∣ tableMultiplicityCount table a := + (ringChar.spec F (tableMultiplicityCount table a)).1 hzero + exact (Nat.not_dvd_of_pos_of_lt htablePos htable_lt_char) hdvd + +/-- If `x` avoids the table poles, then it avoids all table and lookup-column denominator poles +under lookup containment. -/ +theorem termPhi_ne_zero_of_table_poles + (table : (Fin n → Fin 2) → F) (columns : Fin M → (Fin n → Fin 2) → F) (xChallenge : F) + (hcols : ∀ j : Fin M, ∀ u : Fin n → Fin 2, ∃ v : Fin n → Fin 2, + columns j u = table v) + (hNoTablePoles : ∀ u : Fin n → Fin 2, xChallenge + table u ≠ 0) : + ∀ (i : TermIdx M) (u : Fin n → Fin 2), termPhi table columns xChallenge i u ≠ 0 := by + intro i u + cases hti : termToInput i with + | table => + rw [termPhi, hti] + simpa [phi] using hNoTablePoles u + | column j => + obtain ⟨v, hv⟩ := hcols j u + rw [termPhi, hti, phi] + simpa [hv] using hNoTablePoles v + +/-- The table-pole set has size at most the Boolean hypercube. -/ +theorem pole_card_le [Fintype F] [DecidableEq F] (table : (Fin n → Fin 2) → F) : + (Finset.univ.filter (fun x : F => ∃ u : Fin n → Fin 2, x + table u = 0)).card + ≤ Fintype.card (Fin n → Fin 2) := by + classical + calc + (Finset.univ.filter (fun x : F => ∃ u : Fin n → Fin 2, x + table u = 0)).card + ≤ (Finset.univ.image (fun u : Fin n → Fin 2 => -table u)).card := by + apply Finset.card_le_card + intro x hx + simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hx + obtain ⟨u, hu⟩ := hx + exact Finset.mem_image.mpr + ⟨u, Finset.mem_univ u, (eq_neg_of_add_eq_zero_left hu).symm⟩ + _ ≤ Fintype.card (Fin n → Fin 2) := by + rw [← Finset.card_univ] + exact Finset.card_image_le + +/-- The honest row-wise LogUp claim sums to zero away from denominator poles. -/ +theorem logupOuterClaim_zero [Fintype F] [DecidableEq F] + (groups : Fin K → Finset (TermIdx M)) + (hgroups : ∀ g : TermIdx M → F, (∑ k : Fin K, ∑ i ∈ groups k, g i) = ∑ i : TermIdx M, g i) + (table : (Fin n → Fin 2) → F) (columns : Fin M → (Fin n → Fin 2) → F) + (xChallenge : F) (zChallenge : Fin n → F) (batchingScalars : Fin K → F) + (hchar : ∀ a : F, lookupMultiplicityCount columns a ≠ 0 → + (tableMultiplicityCount table a : F) ≠ 0) + (hpoles : ∀ (i : TermIdx M) (u : Fin n → Fin 2), + termPhi table columns xChallenge i u ≠ 0) : + (∑ u : Fin n → Fin 2, + qOnHypercube groups table columns (normalizedMultiplicityValue table columns) + (fun k u => helperValue groups table columns + (normalizedMultiplicityValue table columns) xChallenge k u) + xChallenge zChallenge batchingScalars u) = 0 := by + have hq : ∀ u : Fin n → Fin 2, + qOnHypercube groups table columns (normalizedMultiplicityValue table columns) + (fun k u => helperValue groups table columns + (normalizedMultiplicityValue table columns) xChallenge k u) + xChallenge zChallenge batchingScalars u + = ∑ k : Fin K, + helperValue groups table columns + (normalizedMultiplicityValue table columns) xChallenge k u := by + intro u + simp only [qOnHypercube] + refine Finset.sum_congr rfl (fun k _ => ?_) + rw [domainIdentityTerm_eq_zero groups table columns (normalizedMultiplicityValue table columns) + (fun k u => helperValue groups table columns + (normalizedMultiplicityValue table columns) xChallenge k u) + xChallenge k u rfl (fun i _ => hpoles i u), mul_zero, add_zero] + have hsum : ∀ u : Fin n → Fin 2, + (∑ k : Fin K, + helperValue groups table columns + (normalizedMultiplicityValue table columns) xChallenge k u) + = ∑ i : TermIdx M, + termNumerator (normalizedMultiplicityValue table columns) i u / + termPhi table columns xChallenge i u := by + intro u + simp only [helperValue] + exact hgroups + (fun i => termNumerator (normalizedMultiplicityValue table columns) i u / + termPhi table columns xChallenge i u) + have hterm : ∀ u : Fin n → Fin 2, + (∑ i : TermIdx M, + termNumerator (normalizedMultiplicityValue table columns) i u / + termPhi table columns xChallenge i u) + = normalizedMultiplicityValue table columns u / (xChallenge + table u) + + ∑ j : Fin M, (-1 : F) / (xChallenge + columns j u) := by + intro u + have hcol : ∀ j : Fin M, + termNumerator (normalizedMultiplicityValue table columns) (Fin.succ j) u / + termPhi table columns xChallenge (Fin.succ j) u + = (-1 : F) / (xChallenge + columns j u) := by + intro j + have htt : termToInput (Fin.succ j : TermIdx M) = InputIdx.column j := by + simp [termToInput] + simp only [termNumerator, termPhi, htt, numerator, phi] + rw [Fin.sum_univ_succ] + refine congrArg₂ (· + ·) rfl ?_ + exact Finset.sum_congr rfl (fun j _ => hcol j) + -- Paper eq. (15): the honest identity at `xChallenge`, as the evaluated forward of Lemma 5 + -- (`setInclusion_eval_forward`) with the lookup columns as `a` and the table as `b`. + have hmi : (∑ u : Fin n → Fin 2, + normalizedMultiplicityValue table columns u / (xChallenge + table u)) + = ∑ j : Fin M, ∑ u : Fin n → Fin 2, (1 : F) / (xChallenge + columns j u) := by + have h := setInclusion_eval_forward (fun p : Fin M × (Fin n → Fin 2) => columns p.1 p.2) + table xChallenge hchar + rw [Fintype.sum_prod_type] at h + exact h.symm + simp_rw [hq, hsum, hterm] + rw [Finset.sum_add_distrib, hmi, + Finset.sum_comm (f := fun u j => (-1 : F) / (xChallenge + columns j u)), + ← Finset.sum_add_distrib] + refine Finset.sum_eq_zero (fun j _ => ?_) + rw [← Finset.sum_add_distrib] + exact Finset.sum_eq_zero (fun u _ => by ring) + +end Algebra + +/-! ## Final-point reconstructions + +The verifier's reconstruction of `Q` at the sumcheck point `r` from the claimed evaluation values +`mVal = m(r)`, `tVal = t(r)`, `colVals i = fᵢ(r)`, `helperVals k = hₖ(r)`. -/ + +section AtPoint + +variable {F : Type} [Field F] {n M K : ℕ} + +/-- Denominator term at the final sumcheck point, from the claimed evaluation values. -/ +def phiAtPoint (xChallenge tVal : F) (colVals : Fin M → F) : InputIdx M → F + | .table => xChallenge + tVal + | .column i => xChallenge + colVals i + +/-- Numerator term at the final sumcheck point, from the claimed multiplicity value. -/ +def numeratorAtPoint (mVal : F) : InputIdx M → F + | .table => mVal + | .column _ => -1 + +/-- Term denominator at the final sumcheck point, indexed by `0, ..., M`. -/ +def termPhiAtPoint (xChallenge tVal : F) (colVals : Fin M → F) (i : TermIdx M) : F := + phiAtPoint xChallenge tVal colVals (termToInput i) + +/-- Term numerator at the final sumcheck point, indexed by `0, ..., M`. -/ +def termNumeratorAtPoint (mVal : F) (i : TermIdx M) : F := + numeratorAtPoint mVal (termToInput i) + +/-- The domain-identity expression at the final sumcheck point `r`. -/ +noncomputable def domainIdentityAtPoint (groups : Fin K → Finset (TermIdx M)) + (xChallenge mVal tVal : F) (colVals : Fin M → F) (helperVals : Fin K → F) (k : Fin K) : F := + helperVals k * (∏ i ∈ groups k, termPhiAtPoint xChallenge tVal colVals i) - + ∑ i ∈ groups k, + termNumeratorAtPoint mVal i * + ∏ j ∈ (groups k).erase i, termPhiAtPoint xChallenge tVal colVals j + +/-- The verifier's final check value `Q(eq(r,z), m(r), φᵢ(r), hₖ(r))` from paper (19). -/ +noncomputable def qAtPoint (groups : Fin K → Finset (TermIdx M)) + (xChallenge : F) (zChallenge rChallenge : Fin n → F) (batchingScalars : Fin K → F) + (mVal tVal : F) (colVals : Fin M → F) (helperVals : Fin K → F) : F := + ∑ k : Fin K, ( + helperVals k + + MvPolynomial.eval rChallenge (MvPolynomial.eqPolynomial zChallenge) * batchingScalars k * + domainIdentityAtPoint groups xChallenge mVal tVal colVals helperVals k) + +end AtPoint + +/-! ## The LogUp polynomial + +The input polynomials (table, columns, multiplicity, helpers) combined into LogUp's instantiation of +the generic batched polynomial. -/ + +section Polynomial + +variable {F : Type} [Field F] {n M K : ℕ} + +/-- Denominator polynomial `φ` for one term: `x + (its oracle polynomial)`. -/ +noncomputable def termPhiPolynomial (table : MvPolynomial (Fin n) F) + (columns : Fin M → MvPolynomial (Fin n) F) (xChallenge : F) (i : TermIdx M) : + MvPolynomial (Fin n) F := + MvPolynomial.C xChallenge + + match termToInput i with + | .table => table + | .column j => columns j + +/-- Numerator polynomial for one term: the multiplicity polynomial for the table term, `-1` else. -/ +noncomputable def termNumeratorPolynomial (multiplicity : MvPolynomial (Fin n) F) (i : TermIdx M) : + MvPolynomial (Fin n) F := + match termToInput i with + | .table => multiplicity + | .column _ => MvPolynomial.C (-1) + +theorem termPhiPolynomial_degreeOf {table : MvPolynomial (Fin n) F} + {columns : Fin M → MvPolynomial (Fin n) F} + (htable : ∀ v, MvPolynomial.degreeOf v table ≤ 1) + (hcolumns : ∀ j v, MvPolynomial.degreeOf v (columns j) ≤ 1) + (xChallenge : F) (j : TermIdx M) (i : Fin n) : + MvPolynomial.degreeOf i (termPhiPolynomial table columns xChallenge j) ≤ 1 := by + unfold termPhiPolynomial + calc + _ ≤ max (MvPolynomial.degreeOf i (MvPolynomial.C xChallenge)) + (MvPolynomial.degreeOf i + (match termToInput j with + | .table => table + | .column c => columns c)) := + MvPolynomial.degreeOf_add_le i _ _ + _ ≤ max 0 1 := by + gcongr + · exact (MvPolynomial.degreeOf_C (R := F) xChallenge i).le + · cases termToInput j with + | table => exact htable i + | column c => exact hcolumns c i + _ = 1 := by omega + +theorem termNumeratorPolynomial_degreeOf {multiplicity : MvPolynomial (Fin n) F} + (hmult : ∀ v, MvPolynomial.degreeOf v multiplicity ≤ 1) (j : TermIdx M) (i : Fin n) : + MvPolynomial.degreeOf i (termNumeratorPolynomial multiplicity j) ≤ 1 := by + unfold termNumeratorPolynomial + cases termToInput j with + | table => exact hmult i + | column c => exact (MvPolynomial.degreeOf_C (R := F) (-1 : F) i).le.trans (by omega) + +/-- The concrete multivariate LogUp sumcheck polynomial `Q`: the generic batched polynomial +instantiated with the oracle polynomials. -/ +noncomputable def logupQPolynomial (groups : Fin K → Finset (TermIdx M)) + (table : MvPolynomial (Fin n) F) (columns : Fin M → MvPolynomial (Fin n) F) + (multiplicity : MvPolynomial (Fin n) F) (helpers : Fin K → MvPolynomial (Fin n) F) + (xChallenge : F) (zChallenge : Fin n → F) (batchingScalars : Fin K → F) : + MvPolynomial (Fin n) F := + batchedSumcheckPolynomial groups (termPhiPolynomial table columns xChallenge) + (termNumeratorPolynomial multiplicity) helpers zChallenge batchingScalars + +/-- `Q` has individual degree at most `M + 3`, given that the oracle polynomials are multilinear. -/ +theorem logupQPolynomial_degreeOf (groups : Fin K → Finset (TermIdx M)) + {table : MvPolynomial (Fin n) F} {columns : Fin M → MvPolynomial (Fin n) F} + {multiplicity : MvPolynomial (Fin n) F} {helpers : Fin K → MvPolynomial (Fin n) F} + (htable : ∀ v, MvPolynomial.degreeOf v table ≤ 1) + (hcolumns : ∀ j v, MvPolynomial.degreeOf v (columns j) ≤ 1) + (hmult : ∀ v, MvPolynomial.degreeOf v multiplicity ≤ 1) + (hhelper : ∀ k v, MvPolynomial.degreeOf v (helpers k) ≤ 1) + (xChallenge : F) (zChallenge : Fin n → F) (batchingScalars : Fin K → F) (i : Fin n) : + MvPolynomial.degreeOf i + (logupQPolynomial groups table columns multiplicity helpers + xChallenge zChallenge batchingScalars) ≤ M + 3 := by + refine le_trans (batchedSumcheckPolynomial_degreeOf groups + (termPhiPolynomial table columns xChallenge) (termNumeratorPolynomial multiplicity) + helpers zChallenge batchingScalars + (fun j v => termPhiPolynomial_degreeOf htable hcolumns xChallenge j v) + (fun j v => termNumeratorPolynomial_degreeOf hmult j v) + hhelper i) (by omega) + +end Polynomial + +/-! ## Polynomial evaluation agreement -/ + +section PolynomialEval + +variable {F : Type} [Field F] {n M K : ℕ} + +/-- On Boolean rows, the concrete polynomial `Q` agrees with the row-wise LogUp expression built +from the Boolean evaluations of its input polynomials. -/ +theorem logupQPolynomial_eval_hypercube (groups : Fin K → Finset (TermIdx M)) + (table : MvPolynomial (Fin n) F) (columns : Fin M → MvPolynomial (Fin n) F) + (multiplicity : MvPolynomial (Fin n) F) (helpers : Fin K → MvPolynomial (Fin n) F) + (xChallenge : F) (zChallenge : Fin n → F) (batchingScalars : Fin K → F) + (u : Fin n → Fin 2) : + MvPolynomial.eval (u : Fin n → F) + (logupQPolynomial groups table columns multiplicity helpers + xChallenge zChallenge batchingScalars) + = + qOnHypercube groups (MvPolynomial.toEvalsZeroOne table) + (fun i => MvPolynomial.toEvalsZeroOne (columns i)) + (MvPolynomial.toEvalsZeroOne multiplicity) + (fun k => MvPolynomial.toEvalsZeroOne (helpers k)) + xChallenge zChallenge batchingScalars u := by + have hphi : ∀ i : TermIdx M, + MvPolynomial.eval (u : Fin n → F) (termPhiPolynomial table columns xChallenge i) = + termPhi (MvPolynomial.toEvalsZeroOne table) + (fun j => MvPolynomial.toEvalsZeroOne (columns j)) xChallenge i u := by + intro i + unfold termPhiPolynomial termPhi phi + cases termToInput i <;> simp [MvPolynomial.toEvalsZeroOne] + have hnum : ∀ i : TermIdx M, + MvPolynomial.eval (u : Fin n → F) (termNumeratorPolynomial multiplicity i) = + termNumerator (MvPolynomial.toEvalsZeroOne multiplicity) i u := by + intro i + unfold termNumeratorPolynomial termNumerator numerator + cases termToInput i <;> simp [MvPolynomial.toEvalsZeroOne] + rw [logupQPolynomial, batchedSumcheckPolynomial, qOnHypercube, map_sum] + refine Finset.sum_congr rfl (fun k _ => ?_) + rw [map_add, map_mul, map_mul, MvPolynomial.eval_C] + congr 2 + rw [batchedDomainIdentity, domainIdentityTerm, map_sub, map_mul, map_prod, map_sum] + congr 1 + · congr 1 + exact Finset.prod_congr rfl (fun i _ => hphi i) + · refine Finset.sum_congr rfl (fun i _ => ?_) + rw [map_mul, map_prod, hnum i] + congr 1 + exact Finset.prod_congr rfl (fun j _ => hphi j) + +/-- At an arbitrary point, the concrete polynomial `Q` agrees with the value reconstructed from +the scalar evaluations of its input polynomials. -/ +theorem logupQPolynomial_eval_point (groups : Fin K → Finset (TermIdx M)) + (table : MvPolynomial (Fin n) F) (columns : Fin M → MvPolynomial (Fin n) F) + (multiplicity : MvPolynomial (Fin n) F) (helpers : Fin K → MvPolynomial (Fin n) F) + (xChallenge : F) (zChallenge rChallenge : Fin n → F) (batchingScalars : Fin K → F) : + MvPolynomial.eval rChallenge + (logupQPolynomial groups table columns multiplicity helpers + xChallenge zChallenge batchingScalars) + = + qAtPoint groups xChallenge zChallenge rChallenge batchingScalars + (MvPolynomial.eval rChallenge multiplicity) + (MvPolynomial.eval rChallenge table) + (fun i => MvPolynomial.eval rChallenge (columns i)) + (fun k => MvPolynomial.eval rChallenge (helpers k)) := by + have hphi : ∀ i : TermIdx M, + MvPolynomial.eval rChallenge (termPhiPolynomial table columns xChallenge i) = + termPhiAtPoint xChallenge (MvPolynomial.eval rChallenge table) + (fun j => MvPolynomial.eval rChallenge (columns j)) i := by + intro i + unfold termPhiPolynomial termPhiAtPoint phiAtPoint + cases termToInput i <;> simp + have hnum : ∀ i : TermIdx M, + MvPolynomial.eval rChallenge (termNumeratorPolynomial multiplicity i) = + termNumeratorAtPoint (MvPolynomial.eval rChallenge multiplicity) i := by + intro i + unfold termNumeratorPolynomial termNumeratorAtPoint numeratorAtPoint + cases termToInput i <;> simp + rw [logupQPolynomial, batchedSumcheckPolynomial, qAtPoint, map_sum] + refine Finset.sum_congr rfl (fun k _ => ?_) + rw [map_add, map_mul, map_mul, MvPolynomial.eval_C] + congr 2 + rw [batchedDomainIdentity, domainIdentityAtPoint, map_sub, map_mul, map_prod, map_sum] + congr 1 + · congr 1 + exact Finset.prod_congr rfl (fun i _ => hphi i) + · refine Finset.sum_congr rfl (fun i _ => ?_) + rw [map_mul, map_prod, hnum i] + congr 1 + exact Finset.prod_congr rfl (fun j _ => hphi j) + +end PolynomialEval + +end Logup diff --git a/ArkLib/ProofSystem/Logup/Common.lean b/ArkLib/ProofSystem/Logup/Common.lean deleted file mode 100644 index c270a6615e..0000000000 --- a/ArkLib/ProofSystem/Logup/Common.lean +++ /dev/null @@ -1,421 +0,0 @@ -import Mathlib.Algebra.BigOperators.Fin -import Mathlib.Algebra.CharP.Defs -import Mathlib.Data.Fin.Basic -import Mathlib.Data.Finset.Basic -import Mathlib.Data.Fintype.Basic -import Mathlib.Tactic -import ArkLib.OracleReduction.Composition.Sequential.Append -import ArkLib.OracleReduction.Basic - -/-! -# LogUp Common Definitions - -Domain types, protocol statements, and the outer-round algebra shared across all LogUp modules. --/ - -namespace Logup - -universe u - -open scoped BigOperators - -/-- The boolean hypercube with `2^n` points. - -The paper writes this domain as `H = {±1}^n`; we use bit vectors as row indices and embed -them into a field by `bitToSign`. --/ -@[reducible] -def Hypercube (n : ℕ) : Type := - Fin n → Fin 2 - -/-- Embed a hypercube bit as a `{±1}` field element. -/ -def bitToSign (F : Type u) [One F] [Neg F] (b : Fin 2) : F := - if b = 0 then -1 else 1 - -/-- Embed a hypercube row as a point of `{±1}^n ⊂ Fⁿ`. -/ -def signPoint (F : Type u) [One F] [Neg F] {n : ℕ} (u : Hypercube n) : Fin n → F := - fun j => bitToSign F (u j) - -/-- The Lagrange kernel `L_H(x, z) = 2^{-n} * ∏ᵢ (1 + xᵢ zᵢ)` for `H = {±1}^n`. -/ -noncomputable def lagrangeKernelAtPoint (F : Type u) [Field F] {n : ℕ} - (x z : Fin n → F) : F := - ((2 : F) ^ n)⁻¹ * ∏ j : Fin n, (1 + x j * z j) - -/-- The Lagrange kernel with the first argument restricted to a hypercube row. -/ -noncomputable def lagrangeKernel (F : Type u) [Field F] {n : ℕ} - (u : Hypercube n) (z : Fin n → F) : F := - lagrangeKernelAtPoint F (signPoint F u) z - -/-- A Lagrange oracle is a function on `H`; queries ask for inner products with `L_H(., z)`. -/ -structure LagrangeOracle (F : Type u) (n : ℕ) where - values : Hypercube n → F - -instance {F : Type u} {n : ℕ} : CoeFun (LagrangeOracle F n) (fun _ => Hypercube n → F) where - coe oracle := oracle.values - -/-- A multilinear oracle over the row variables of `H = {±1}^n`, represented in Lagrange form. -/ -@[reducible] -def MultilinearOracle (F : Type u) (n : ℕ) : Type u := - LagrangeOracle F n - -/-- Evaluate a multilinear oracle on a Boolean-hypercube row. -/ -def evalOnHypercube {F : Type u} {n : ℕ} - (p : MultilinearOracle F n) (u : Hypercube n) : F := - p u - -/-- Lagrange-oracle queries are exactly the paper's inner products with `L_H(., z)`. -/ -noncomputable instance instLagrangeOracleInterface {F : Type u} [Field F] {n : ℕ} : - OracleInterface (LagrangeOracle F n) where - Query := Fin n → F - toOC.spec := (Fin n → F) →ₒ F - toOC.impl z := do - let oracle ← read - return ∑ u : Hypercube n, oracle u * lagrangeKernel F u z - -/-- The semantic value returned by querying a Lagrange-form multilinear oracle at `z`. -/ -noncomputable def lagrangeOracleEval {F : Type u} [Field F] {n : ℕ} - (oracle : MultilinearOracle F n) (z : Fin n → F) : F := - ∑ u : Hypercube n, oracle u * lagrangeKernel F u z - -/-- Input oracle labels for Protocol 2: one table oracle and `M` lookup-column oracles. -/ -inductive InputOracleIdx (M : ℕ) where - | table : InputOracleIdx M - | column : Fin M → InputOracleIdx M -deriving DecidableEq - -/-- Term labels `0, ..., M` from the paper, with `0` denoting the table term. -/ -@[reducible] -def TermIdx (M : ℕ) : Type := - Fin (M + 1) - -/-- Interpret term index `0` as the table and term indices `1, ..., M` as lookup columns. -/ -def termToInput {M : ℕ} (i : TermIdx M) : InputOracleIdx M := - if h : i.val = 0 then - .table - else - .column ⟨i.val - 1, by omega⟩ - -/-- Interpret input-oracle labels as term indices `0, ..., M`. -/ -def inputToTerm {M : ℕ} : InputOracleIdx M → TermIdx M - | .table => ⟨0, by omega⟩ - | .column i => ⟨i.val + 1, by omega⟩ - -/-- Protocol parameter `ℓ`, the chosen partial-sum size from Protocol 2. -/ -structure ProtocolParams (M : ℕ) where - /-- The partial-sum size `ℓ`. -/ - sumSize : ℕ - /-- Protocol 2 requires `1 ≤ ℓ`. -/ - sumSize_pos : 0 < sumSize - /-- Protocol 2 requires `ℓ ≤ M + 1`. -/ - sumSize_le : sumSize ≤ M + 1 - -namespace ProtocolParams - -/-- The number of partial-sum groups `K = ceil((M + 1) / ℓ)`. -/ -def numGroups {M : ℕ} (params : ProtocolParams M) : ℕ := - (M + params.sumSize) / params.sumSize - -/-- The consecutive interval `Iₖ = [(k - 1)ℓ, kℓ) ∩ [0, M]`, zero-indexed. -/ -def group {M : ℕ} (params : ProtocolParams M) (k : Fin params.numGroups) : - Finset (TermIdx M) := - Finset.univ.filter fun i : TermIdx M => - k.val * params.sumSize ≤ i.val ∧ i.val < (k.val + 1) * params.sumSize - -end ProtocolParams - -/-- Public parameter assumptions for Protocol 2. - -The paper fixes a finite field with characteristic larger than `M * 2^n`; we also record that -`-1` and `1` are distinct so that `{±1}^n` is genuinely a Boolean hypercube in the field. --/ -structure StmtIn (F : Type u) [Field F] [Fintype F] (n M : ℕ) : Type u where - /-- The paper's characteristic condition `char(F) > M * 2^n`. -/ - charLarge : M * 2 ^ n < ringChar F - /-- The two signs used for the hypercube are distinct. -/ - signsDistinct : (-1 : F) ≠ 1 - -/-- Input oracle statements: the table `t` and lookup columns `fᵢ`, as multilinear oracles. -/ -@[reducible, simp] -def OStmtIn (F : Type u) (n M : ℕ) : InputOracleIdx M → Type u - | .table => MultilinearOracle F n - | .column _ => MultilinearOracle F n - -/-- Input LogUp oracles are accessed by evaluating their multilinear polynomial extensions. -/ -noncomputable instance instOStmtInOracleInterface {F : Type u} [Field F] {n M : ℕ} : - ∀ i, OracleInterface (OStmtIn F n M i) - | .table => inferInstance - | .column _ => inferInstance - -/-- Accessor for the input table oracle `t`. -/ -@[reducible, simp] -def tableOracle {F : Type u} {n M : ℕ} - (oStmt : ∀ i, OStmtIn F n M i) : MultilinearOracle F n := - oStmt .table - -/-- Accessor for the `i`-th lookup-column oracle `fᵢ`. -/ -@[reducible, simp] -def columnOracle {F : Type u} {n M : ℕ} - (oStmt : ∀ i, OStmtIn F n M i) (i : Fin M) : MultilinearOracle F n := - oStmt (.column i) - -/-- Semantic input relation for Protocol 2: every lookup-column value occurs in the table range. -/ -def inputRelation (F : Type u) [Field F] [Fintype F] (n M : ℕ) : - Set ((StmtIn F n M × (∀ i, OStmtIn F n M i)) × Unit) := - { ⟨⟨_, oStmt⟩, _⟩ | - ∀ i : Fin M, ∀ x : Hypercube n, ∃ y : Hypercube n, - evalOnHypercube (columnOracle oStmt i) x = evalOnHypercube (tableOracle oStmt) y } - -/-- The full LogUp protocol returns no additional public data on success. -/ -@[reducible, simp] -def StmtOut : Type := - Unit - -/-- The full LogUp protocol leaves no output oracle statements. -/ -@[reducible, simp] -def OutputOracleIdx : Type := - Fin 0 - -/-- Output oracle statements for the full LogUp protocol. -/ -@[reducible, simp] -def OStmtOut : OutputOracleIdx → Type := - fun i => Fin.elim0 i - -/-- The full LogUp protocol has no output oracle interfaces to provide. -/ -instance instOStmtOutOracleInterface : - ∀ i, OracleInterface (OStmtOut i) := - fun i => Fin.elim0 i - -/-- The full protocol has a trivial final relation: successful verification returns `Unit`. -/ -def outputRelation : Set ((StmtOut × (∀ i, OStmtOut i)) × Unit) := - Set.univ - -section ProtocolSpec - -/-- The prover's first Protocol 2 message: the multiplicity function `m : H → F`. -/ -@[reducible, simp] -def MultiplicityMessage (F : Type) (n : ℕ) : Type := - MultilinearOracle F n - -/-- The prover's second Protocol 2 message: helper functions `h₁, ..., h_K : H → F`. -/ -@[reducible, simp] -def HelperMessages (F : Type) (n K : ℕ) : Type := - Fin K → MultilinearOracle F n - -/-- The verifier's second outer challenge: `z ∈ Fⁿ` and batching scalars `λ₁, ..., λ_K`. -/ -@[reducible, simp] -def BatchingChallenge (F : Type) (n K : ℕ) : Type := - (Fin n → F) × (Fin K → F) - -end ProtocolSpec - -section OuterIO - -variable (F : Type) [Field F] [Fintype F] (n M : ℕ) (params : ProtocolParams M) - -/-- The outer LogUp statement after the verifier has sampled `x`, `z`, and `λ`. -/ -structure StmtAfterOuter where - /-- The logarithmic-derivative challenge `x`. -/ - xChallenge : F - /-- The Lagrange-kernel point `z ∈ Fⁿ`. -/ - zChallenge : Fin n → F - /-- The batching scalars `λ₁, ..., λ_K`. -/ - batchingScalars : Fin params.numGroups → F - -/-- Oracle labels retained after the outer LogUp phase. -/ -inductive OuterOracleIdx (M : ℕ) where - | input : InputOracleIdx M → OuterOracleIdx M - | multiplicity : OuterOracleIdx M - | helpers : OuterOracleIdx M -deriving DecidableEq - -/-- Oracle statements retained after the outer LogUp phase. -/ -@[reducible, simp] -def OStmtAfterOuter (F : Type) [Field F] (n M : ℕ) (params : ProtocolParams M) : - OuterOracleIdx M → Type - | .input i => OStmtIn F n M i - | .multiplicity => MultiplicityMessage F n - | .helpers => HelperMessages F n params.numGroups - -/-- Oracle interfaces for all oracle statements retained after the outer LogUp phase. -/ -noncomputable instance instOStmtAfterOuterOracleInterface - {F : Type} [Field F] {n M : ℕ} {params : ProtocolParams M} : - ∀ i, OracleInterface (OStmtAfterOuter F n M params i) - | .input i => inferInstanceAs (OracleInterface (OStmtIn F n M i)) - | .multiplicity => inferInstanceAs (OracleInterface (MultiplicityMessage F n)) - | .helpers => inferInstanceAs (OracleInterface (HelperMessages F n params.numGroups)) - -/-- Protocol 2 has no private witness beyond the input oracles at this layer. -/ -@[reducible, simp] -def WitIn (F : Type u) [Field F] [Fintype F] (_n M : ℕ) (_params : ProtocolParams M) : Type := - Unit - -end OuterIO - -section ProtocolAlgebra - -variable {F : Type} [Field F] [Fintype F] [DecidableEq F] {n M K : ℕ} -variable (params : ProtocolParams M) - -/-- A decomposition of the term indices `{0, ..., M}` into the partial-sum groups `Iₖ`. -/ -@[reducible] -def PartialSumGroups (M K : ℕ) : Type := - Fin K → Finset (TermIdx M) - -/-- The paper's canonical consecutive groups `Iₖ`, derived from the parameter `ℓ`. -/ -def canonicalGroups : PartialSumGroups M params.numGroups := - fun k => params.group k - -/-- Outer transcript data produced before entering the embedded sumcheck. -/ -structure OuterTranscriptData (F : Type) [Field F] [Fintype F] (n M : ℕ) - (params : ProtocolParams M) where - /-- The multiplicity function `m : H → F`. -/ - multiplicity : MultiplicityMessage F n - /-- The verifier challenge `x : F`. -/ - xChallenge : F - /-- The helper functions `h₁, ..., h_K : H → F`. -/ - helpers : HelperMessages F n params.numGroups - /-- The Lagrange-kernel point `z ∈ Fⁿ`. -/ - zChallenge : Fin n → F - /-- The batching scalars `λ₁, ..., λ_K`. -/ - batchingScalars : Fin params.numGroups → F - -/-- Number of table rows with value `a`. -/ -def tableMultiplicityCount (oStmt : ∀ i, OStmtIn F n M i) (a : F) : ℕ := - ((Finset.univ : Finset (Hypercube n)).filter fun u => - evalOnHypercube (tableOracle oStmt) u = a).card - -/-- Total number of lookup-column entries with value `a`. -/ -def lookupMultiplicityCount (oStmt : ∀ i, OStmtIn F n M i) (a : F) : ℕ := - ((Finset.univ : Finset (Fin M × Hypercube n)).filter fun ix => - evalOnHypercube (columnOracle oStmt ix.1) ix.2 = a).card - -/-- The normalized multiplicity from paper equation (14), evaluated at one table row. -/ -noncomputable def normalizedMultiplicityValue (oStmt : ∀ i, OStmtIn F n M i) - (u : Hypercube n) : F := - let a := evalOnHypercube (tableOracle oStmt) u - (lookupMultiplicityCount oStmt a : F) / (tableMultiplicityCount oStmt a : F) - -/-- The honest multiplicity oracle `m : H → F` from paper equation (14). -/ -noncomputable def honestMultiplicity (oStmt : ∀ i, OStmtIn F n M i) : - MultiplicityMessage F n := - ⟨fun u => normalizedMultiplicityValue oStmt u⟩ - -/-- The denominator term `φᵢ(u)` from Protocol 2. -/ -noncomputable def phi (oStmt : ∀ i, OStmtIn F n M i) (xChallenge : F) : - InputOracleIdx M → Hypercube n → F - | .table => fun u => xChallenge + evalOnHypercube (tableOracle oStmt) u - | .column i => fun u => xChallenge + evalOnHypercube (columnOracle oStmt i) u - -/-- The numerator term `mᵢ(u)` from Protocol 2, with `m₀ = m` and `mᵢ = -1` for columns. -/ -noncomputable def numerator (multiplicity : MultilinearOracle F n) : - InputOracleIdx M → Hypercube n → F - | .table => evalOnHypercube multiplicity - | .column _ => fun _ => -1 - -/-- The denominator term, indexed as `0, ..., M` as in the paper. -/ -noncomputable def termPhi (oStmt : ∀ i, OStmtIn F n M i) (xChallenge : F) - (i : TermIdx M) (u : Hypercube n) : F := - phi oStmt xChallenge (termToInput i) u - -/-- The numerator term, indexed as `0, ..., M` as in the paper. -/ -noncomputable def termNumerator (multiplicity : MultilinearOracle F n) - (i : TermIdx M) (u : Hypercube n) : F := - numerator multiplicity (termToInput i) u - -/-- Product of the denominator terms in one partial-sum group. -/ -noncomputable def denominatorProduct (groups : PartialSumGroups M K) - (oStmt : ∀ i, OStmtIn F n M i) (xChallenge : F) (k : Fin K) (u : Hypercube n) : F := - ∏ i ∈ groups k, termPhi oStmt xChallenge i u - -/-- The domain-identity expression for one helper function `hₖ`. -/ -noncomputable def domainIdentityTerm (groups : PartialSumGroups M K) - (oStmt : ∀ i, OStmtIn F n M i) (multiplicity : MultilinearOracle F n) - (helpers : HelperMessages F n K) (xChallenge : F) (k : Fin K) (u : Hypercube n) : F := - evalOnHypercube (helpers k) u * denominatorProduct groups oStmt xChallenge k u - - ∑ i ∈ groups k, - termNumerator multiplicity i u * ∏ j ∈ (groups k).erase i, termPhi oStmt xChallenge j u - -/-- The helper value `hₖ(u) = Σᵢ mᵢ(u)/φᵢ(u)` from paper equation (16). -/ -noncomputable def helperValue (groups : PartialSumGroups M K) - (oStmt : ∀ i, OStmtIn F n M i) (multiplicity : MultilinearOracle F n) - (xChallenge : F) (k : Fin K) (u : Hypercube n) : F := - ∑ i ∈ groups k, termNumerator multiplicity i u / termPhi oStmt xChallenge i u - -/-- The honest helper oracle `hₖ : H → F` for one partial-sum group. -/ -noncomputable def helperOracle (groups : PartialSumGroups M K) - (oStmt : ∀ i, OStmtIn F n M i) (multiplicity : MultilinearOracle F n) - (xChallenge : F) (k : Fin K) : MultilinearOracle F n := - ⟨fun u => helperValue groups oStmt multiplicity xChallenge k u⟩ - -/-- The honest helper-oracle bundle `h₁, ..., h_K` from paper equation (16). -/ -noncomputable def honestHelpers (oStmt : ∀ i, OStmtIn F n M i) (xChallenge : F) : - HelperMessages F n params.numGroups := - let multiplicity := honestMultiplicity oStmt - fun k => helperOracle (canonicalGroups params) oStmt multiplicity xChallenge k - -/-- The batched polynomial expression `Q` from paper equation (18), evaluated on a row `u ∈ H`. -/ -noncomputable def qOnHypercube (groups : PartialSumGroups M K) - (oStmt : ∀ i, OStmtIn F n M i) (multiplicity : MultilinearOracle F n) - (helpers : HelperMessages F n K) (xChallenge : F) (zChallenge : Fin n → F) - (batchingScalars : Fin K → F) (u : Hypercube n) : F := - ∑ k : Fin K, ( - evalOnHypercube (helpers k) u + - lagrangeKernel F u zChallenge * batchingScalars k * - domainIdentityTerm groups oStmt multiplicity helpers xChallenge k u) - -/-- Point evaluations queried by the verifier at the final sumcheck point `r`. -/ -structure PointEvaluations (F : Type) (M K : ℕ) where - /-- Claimed value `m(r)`. -/ - multiplicity : F - /-- Claimed value `t(r)`. -/ - table : F - /-- Claimed values `fᵢ(r)`. -/ - columns : Fin M → F - /-- Claimed values `hₖ(r)`. -/ - helpers : Fin K → F - -/-- Denominator term at the final sumcheck point, reconstructed from oracle query answers. -/ -def phiAtPoint (xChallenge : F) (evals : PointEvaluations F M K) : - InputOracleIdx M → F - | .table => xChallenge + evals.table - | .column i => xChallenge + evals.columns i - -/-- Numerator term at the final sumcheck point, reconstructed from oracle query answers. -/ -def numeratorAtPoint (evals : PointEvaluations F M K) : InputOracleIdx M → F - | .table => evals.multiplicity - | .column _ => -1 - -/-- Term denominator at the final sumcheck point, indexed by `0, ..., M`. -/ -def termPhiAtPoint (xChallenge : F) (evals : PointEvaluations F M K) (i : TermIdx M) : F := - phiAtPoint xChallenge evals (termToInput i) - -/-- Term numerator at the final sumcheck point, indexed by `0, ..., M`. -/ -def termNumeratorAtPoint (evals : PointEvaluations F M K) (i : TermIdx M) : F := - numeratorAtPoint evals (termToInput i) - -/-- The domain-identity expression at the final sumcheck point `r`. -/ -noncomputable def domainIdentityAtPoint (groups : PartialSumGroups M K) - (xChallenge : F) (evals : PointEvaluations F M K) (k : Fin K) : F := - evals.helpers k * (∏ i ∈ groups k, termPhiAtPoint xChallenge evals i) - - ∑ i ∈ groups k, - termNumeratorAtPoint evals i * - ∏ j ∈ (groups k).erase i, termPhiAtPoint xChallenge evals j - -/-- The verifier's final check value `Q(L_H(r,z), m(r), φᵢ(r), hₖ(r))` from paper (19). -/ -noncomputable def qAtPoint (groups : PartialSumGroups M K) (xChallenge : F) - (zChallenge rChallenge : Fin n → F) (batchingScalars : Fin K → F) - (evals : PointEvaluations F M K) : F := - ∑ k : Fin K, ( - evals.helpers k + - lagrangeKernelAtPoint F rChallenge zChallenge * batchingScalars k * - domainIdentityAtPoint groups xChallenge evals k) - -/-- Predicate for paper step 4: final oracle-query answers match the sumcheck's expected value. -/ -noncomputable def finalQueryCheck (groups : PartialSumGroups M K) (xChallenge : F) - (zChallenge rChallenge : Fin n → F) (batchingScalars : Fin K → F) - (evals : PointEvaluations F M K) (expectedValue : F) : Prop := - qAtPoint groups xChallenge zChallenge rChallenge batchingScalars evals = expectedValue - -end ProtocolAlgebra - -end Logup diff --git a/ArkLib/ProofSystem/Logup/Protocol.lean b/ArkLib/ProofSystem/Logup/Protocol.lean index 8716086d14..3df8e07c87 100644 --- a/ArkLib/ProofSystem/Logup/Protocol.lean +++ b/ArkLib/ProofSystem/Logup/Protocol.lean @@ -1,17 +1,252 @@ -import ArkLib.ProofSystem.Logup.Common -import ArkLib.ProofSystem.Logup.Sumcheck.SumcheckBridge +import Mathlib.Algebra.Order.Floor.Div +import ArkLib.Data.MvPolynomial.Multilinear +import ArkLib.OracleReduction.OracleInterface +import ArkLib.ProofSystem.Logup.Algebra +import ArkLib.ProofSystem.Sumcheck.Spec.General /-! # LogUp Protocol -Outer and full protocol specs, prover, verifier, and oracle reductions for LogUp Protocol 2. +Protocol specs, honest prover, verifier, and oracle reductions for Protocol 2 of Haböck's LogUp +lookup argument (Cryptology ePrint Archive, Paper 2022/1530, +). + +The protocol checks that every value in the `M` lookup-column oracles occurs somewhere in the table +oracle. + +## Protocol Specification + +The LogUp protocol is parameterized by: +- a field `F`; +- a row dimension `n`, with rows indexed by the Boolean hypercube `H = {±1}ⁿ`; +- `M` lookup-column oracles `fᵢ : H → F` and one table oracle `t : H → F`; +- a partial-sum size `ℓ` (`1 ≤ ℓ ≤ M + 1`), stored in `ProtocolParams`, which determines the number + `K = ⌈(M + 1) / ℓ⌉` of helper oracles; and +- the characteristic condition `char(F) > M * 2^n`. + +### The relation and its logarithmic-derivative reformulation + +The input relation is the set inclusion `⋃ᵢ {fᵢ(u) : u ∈ H} ⊆ {t(u) : u ∈ H}`: every value +appearing in any lookup column also appears somewhere in the table. Under the characteristic +condition, Lemma 5 of the paper makes this equivalent to the existence of a multiplicity function +`m : H → F` satisfying the rational identity (paper eq. (13)) + + `∑ u ∈ H, ∑ i ∈ [1, M], 1 / (X + fᵢ(u)) = ∑ u ∈ H, m(u) / (X + t(u))` in `F(X)`. + +The canonical witness is the normalized multiplicity (paper eq. (14)), +`m(u) = (∑ᵢ #{y ∈ H : fᵢ(y) = t(u)}) / #{y ∈ H : t(y) = t(u)}`, which counts how often the table +value `t(u)` is used across the lookup columns (and equals the plain count when `t` is injective). + +### The protocol + +1. The prover sends the multiplicity oracle `m`. The verifier samples the logarithmic-derivative + challenge `x ←$ F`. The paper draws `x ∉ {-t(u) : u ∈ H}` by rejection sampling so that every + denominator is nonzero; following Remark 3, this formalization instead samples `x` uniformly from + all of `F` and absorbs the rare bad event (a vanishing denominator) into the completeness error, + avoiding the rejection-sampling constraint. Specializing the identity above at `X = x` and + clearing it to one side gives the scalar claim (paper eq. (15)) + + `∑ u ∈ H, (∑ i ∈ [1, M], 1 / (x + fᵢ(u))) - m(u) / (x + t(u)) = 0`. + + It is convenient to fold the table and columns into `M + 1` indexed terms (paper notation): + `m₀ = m`, `ϕ₀(u) = x + t(u)`, and `mᵢ = -1`, `ϕᵢ(u) = x + fᵢ(u)` for `i = 1, ..., M`, so the + summand is `∑ i ∈ [0, M], mᵢ(u) / ϕᵢ(u)`. + +2. The denominator index set `[0, M]` is partitioned into the `K` consecutive groups + `Iₖ = [(k-1)ℓ, kℓ) ∩ [0, M]`. For each group the prover forms the partial sum (paper eq. (16)) + `hₖ(u) = ∑ i ∈ Iₖ, mᵢ(u) / ϕᵢ(u)` and sends the helper oracles `h₁, ..., h_K`. By construction + the helpers sum to zero, `∑ u ∈ H, (h₁(u) + ... + h_K(u)) = 0`, and each obeys the + cleared-denominator *domain identity* (paper eq. (17)) + + `hₖ(u) * (∏ i ∈ Iₖ, ϕᵢ(u)) = ∑ i ∈ Iₖ, mᵢ(u) * (∏ j ∈ Iₖ \ {i}, ϕⱼ(u))` for all `u ∈ H`. + +3. The verifier samples a point `z : Fin n → F` and batching scalars `λ₁, ..., λ_K`. Multiplying the + domain identities by the Lagrange kernel `L_H(·, z)` turns each "for all `u ∈ H`" identity into a + zero-sum over `H`, and the `λ`-batching collapses the `K` domain identities together with the + helper zero-sum into the single batched polynomial `Q` (paper eq. (18)) + + `Q = ∑ k ∈ [1, K], (hₖ + L * λₖ * (hₖ * ∏ i ∈ Iₖ, ϕᵢ - ∑ i ∈ Iₖ, mᵢ * ∏ j ∈ Iₖ \ {i}, ϕⱼ))`, + + where `L = L_H(u, z)`. Prover and verifier then run generic sumcheck (Protocol 1) on the claim + `∑ u ∈ H, Q(L_H(u, z), m(u), ϕ₀(u), ..., ϕ_M(u), h₁(u), ..., h_K(u)) = 0`. + +4. Sumcheck leaves a final point `r : Fin n → F` and a claimed value `v` for the polynomial of + paper eq. (19) at `r`. The verifier queries the retained LogUp oracles `m, t, f₁, ..., f_M`, + `h₁, ..., h_K` at `r`, computes the kernel value `L_H(r, z)` itself, reconstructs `Q(r)` from + these answers, and accepts only if this reconstructed value equals `v`. + +### Formalization + +The LogUp paper writes the row domain as `{±1}^n`; this formalization uses the affine-equivalent +Boolean hypercube together with ArkLib's existing equality polynomial and +[`MLE`](ArkLib/Data/MvPolynomial/Multilinear.lean) definitions. + +The formalization is split into three ArkLib reductions. + +* The outer LogUp phase sends the multiplicity oracle `m`, samples the challenge `x`, sends the + helper oracles, and samples the batching challenge `(z, lambda)`. At the end of this phase, the + verifier has the data needed to state a single zero-sum claim about the LogUp polynomial `Q`. +* The sumcheck phase runs ArkLib's generic sumcheck on the claim that `Q` sums to zero. The + *polynomial and all of LogUp's fractional-identity algebra* are protocol-agnostic and live in + [`Algebra`](ArkLib/ProofSystem/Logup/Algebra.lean), parameterized on bare oracle functions. This + file supplies the oracle data from the retained LogUp oracles and connects the two worlds through + the context lens `logupSumcheckContextLens`. +* The final zero-round phase queries the retained LogUp oracles at sumcheck's final point and checks + that those oracle values really give the value claimed by sumcheck. + +This file holds the LogUp *interactive oracle reduction* itself: the oracle representation types, +the input/output statements and relations, the sumcheck bridge and context lens, the transcript +shapes, the prover/verifier objects, and the oracle reductions for each phase and the composed +protocol. + +The main artefacts that define the protocol are `pSpec`, `logupProver`, `logupVerifier`, +and `logupOracleReduction`. + -/ namespace Logup -open scoped BigOperators +universe u + +open scoped BigOperators MvPolynomial + +/-! # Phase 1 — Outer LogUp -section ProtocolSpec +The input boundary, outer transcript, honest multiplicity/helper messages, outer prover/verifier, +and first oracle reduction. -/ + +section Phase1 + +/-- Protocol parameter `ℓ`, the chosen partial-sum size from Protocol 2. -/ +structure ProtocolParams (M : ℕ) where + /-- The partial-sum size `ℓ`. -/ + sumSize : ℕ + /-- Protocol 2 requires `1 ≤ ℓ`. -/ + sumSize_pos : 0 < sumSize + /-- Protocol 2 requires `ℓ ≤ M + 1`. -/ + sumSize_le : sumSize ≤ M + 1 + +namespace ProtocolParams + +/-- The number of partial-sum groups `K = ceil((M + 1) / ℓ)`. -/ +def numGroups {M : ℕ} (params : ProtocolParams M) : ℕ := + (M + params.sumSize) / params.sumSize + +/-- `numGroups` really is the ceiling `⌈(M + 1) / ℓ⌉`: the floor-division formula +`(M + ℓ) / ℓ` agrees with `Nat.ceilDiv` because `ℓ ≥ 1` (`sumSize_pos`). -/ +theorem numGroups_eq_ceilDiv {M : ℕ} (params : ProtocolParams M) : + params.numGroups = (M + 1) ⌈/⌉ params.sumSize := by + have h := params.sumSize_pos + rw [Nat.ceilDiv_eq_add_pred_div] + unfold numGroups + congr 1 + omega + +/-- The consecutive interval `Iₖ = [(k - 1)ℓ, kℓ) ∩ [0, M]`, zero-indexed. -/ +def group {M : ℕ} (params : ProtocolParams M) (k : Fin params.numGroups) : + Finset (TermIdx M) := + Finset.univ.filter fun i : TermIdx M => + k.val * params.sumSize ≤ i.val ∧ i.val < (k.val + 1) * params.sumSize + +end ProtocolParams + +/-- Input oracle statements: the table `t` and lookup columns `fᵢ`, as multilinear polynomials +(reusing ArkLib's bounded-degree polynomial oracle, queried by evaluation). -/ +@[reducible, simp] +def OStmtIn (F : Type u) [CommSemiring F] (n M : ℕ) : InputIdx M → Type u + | .table => F⦃≤ 1⦄[X (Fin n)] + | .column _ => F⦃≤ 1⦄[X (Fin n)] + +/-- Input LogUp oracles are accessed by evaluating their multilinear polynomial extensions. -/ +noncomputable instance instOStmtInOracleInterface {F : Type u} [Field F] {n M : ℕ} : + ∀ i, OracleInterface (OStmtIn F n M i) + | .table => inferInstance + | .column _ => inferInstance + +/-- The prover's first Protocol 2 message: the multiplicity function `m : H → F`, as a +multilinear polynomial. -/ +@[reducible, simp] +def MultiplicityMessage (F : Type) [CommSemiring F] (n : ℕ) : Type := + F⦃≤ 1⦄[X (Fin n)] + +/-- The prover's second Protocol 2 message: helper functions `h₁, ..., h_K : H → F`, as +multilinear polynomials. -/ +@[reducible, simp] +def HelperMessages (F : Type) [CommSemiring F] (n K : ℕ) : Type := + Fin K → F⦃≤ 1⦄[X (Fin n)] + +/-- The verifier's second outer challenge: `z ∈ Fⁿ` and batching scalars `λ₁, ..., λ_K`. -/ +@[reducible, simp] +def BatchingChallenge (F : Type) (n K : ℕ) : Type := + (Fin n → F) × (Fin K → F) + +variable (F : Type) [Field F] [Fintype F] (n M : ℕ) (params : ProtocolParams M) + +/-- The outer LogUp statement after the verifier has sampled `x`, `z`, and `λ`. -/ +structure StmtAfterOuter where + /-- The logarithmic-derivative challenge `x`. -/ + xChallenge : F + /-- The equality-kernel point `z ∈ Fⁿ`. -/ + zChallenge : Fin n → F + /-- The batching scalars `λ₁, ..., λ_K`. -/ + batchingScalars : Fin params.numGroups → F + +/-- Oracle labels retained after the outer LogUp phase. -/ +inductive OuterOracleIdx (M : ℕ) where + | input : InputIdx M → OuterOracleIdx M + | multiplicity : OuterOracleIdx M + | helpers : OuterOracleIdx M +deriving DecidableEq + +/-- Oracle statements retained after the outer LogUp phase. -/ +@[reducible, simp] +def OStmtAfterOuter (F : Type) [Field F] (n M : ℕ) (params : ProtocolParams M) : + OuterOracleIdx M → Type + | .input i => OStmtIn F n M i + | .multiplicity => MultiplicityMessage F n + | .helpers => HelperMessages F n params.numGroups + +/-- Oracle interfaces for all oracle statements retained after the outer LogUp phase. -/ +noncomputable instance instOStmtAfterOuterOracleInterface + {F : Type} [Field F] {n M : ℕ} {params : ProtocolParams M} : + ∀ i, OracleInterface (OStmtAfterOuter F n M params i) + | .input i => inferInstanceAs (OracleInterface (OStmtIn F n M i)) + | .multiplicity => inferInstanceAs (OracleInterface (MultiplicityMessage F n)) + | .helpers => inferInstanceAs (OracleInterface (HelperMessages F n params.numGroups)) + + +variable {F : Type} [Field F] [Fintype F] [DecidableEq F] {n M : ℕ} +variable (params : ProtocolParams M) + + +/-- The honest multiplicity oracle `m : H → F` from paper equation (14), as the multilinear +extension of the normalized-multiplicity table. -/ +noncomputable def honestMultiplicity (oStmt : ∀ i, OStmtIn F n M i) : MultiplicityMessage F n := + (MvPolynomial.MLEEquiv (R := F) (σ := Fin n)).symm + (normalizedMultiplicityValue (MvPolynomial.toEvalsZeroOne (oStmt .table).1) + (fun i => MvPolynomial.toEvalsZeroOne (oStmt (.column i)).1)) + +/-- The honest helper-oracle bundle `h₁, ..., h_K` from paper equation (16). -/ +noncomputable def honestHelpers (oStmt : ∀ i, OStmtIn F n M i) (xChallenge : F) : + HelperMessages F n params.numGroups := + fun k => + (MvPolynomial.MLEEquiv (R := F) (σ := Fin n)).symm + (helperValue (params.group) (MvPolynomial.toEvalsZeroOne (oStmt .table).1) + (fun i => MvPolynomial.toEvalsZeroOne (oStmt (.column i)).1) + (MvPolynomial.toEvalsZeroOne (honestMultiplicity oStmt).1) xChallenge k) + +/-- Public parameter assumptions for Protocol 2. -/ +structure StmtIn (F : Type u) [Field F] [Fintype F] (n M : ℕ) : Type u where + /-- The paper's characteristic condition `char(F) > M * 2^n`. -/ + charLarge : M * 2 ^ n < ringChar F + +/-- Semantic input relation for Protocol 2: every lookup-column value occurs in the table range. -/ +def inputRelation (F : Type u) [Field F] [Fintype F] (n M : ℕ) : + Set ((StmtIn F n M × (∀ i, OStmtIn F n M i)) × Unit) := + { ⟨⟨_, oStmt⟩, _⟩ | + ∀ i : Fin M, ∀ x : (Fin n → Fin 2), ∃ y : (Fin n → Fin 2), + MvPolynomial.toEvalsZeroOne (oStmt (.column i)).1 x + = MvPolynomial.toEvalsZeroOne (oStmt .table).1 y } open ProtocolSpec @@ -24,7 +259,7 @@ The transcript shape is: 4. `V → P`: challenge `(z, λ)`. -/ @[reducible] -def outerPSpec (F : Type) (n : ℕ) {M : ℕ} (params : ProtocolParams M) : ProtocolSpec 4 := +def outerPSpec (F : Type) [Field F] (n : ℕ) {M : ℕ} (params : ProtocolParams M) : ProtocolSpec 4 := ⟨!v[.P_to_V], !v[MultiplicityMessage F n]⟩ ++ₚ ⟨!v[.V_to_P], !v[F]⟩ ++ₚ ⟨!v[.P_to_V], !v[HelperMessages F n params.numGroups]⟩ ++ₚ @@ -48,7 +283,7 @@ noncomputable instance instOuterPSpecMessageOracleInterface /-- The verifier challenges in the outer LogUp transcript are sampled uniformly from their types. -/ instance instOuterPSpecChallengeSampleable - {F : Type} [Fintype F] [Inhabited F] [SampleableType F] {n M : ℕ} + {F : Type} [Field F] [Fintype F] [SampleableType F] {n M : ℕ} {params : ProtocolParams M} : ∀ i, SampleableType ((outerPSpec F n params).Challenge i) | ⟨0, h0⟩ => by @@ -61,48 +296,12 @@ instance instOuterPSpecChallengeSampleable change Direction.P_to_V = Direction.V_to_P at h2 cases h2 | ⟨3, _⟩ => by + -- `BatchingChallenge` is a product type, and VCVio's `SampleableType (α × β)` instance + -- requires `Inhabited` on each factor; supply it from the field's zero. + letI : Inhabited F := ⟨0⟩ change SampleableType (BatchingChallenge F n params.numGroups) infer_instance -end ProtocolSpec - -section FullProtocolSpec - -open ProtocolSpec - -/-- Protocol 2 transcript shape: the outer LogUp messages followed by ArkLib's generic sumcheck. -/ -@[reducible] -noncomputable def pSpec (F : Type) [Field F] [Fintype F] [DecidableEq F] - (n M : ℕ) (params : ProtocolParams M) : - ProtocolSpec (4 + Fin.vsum (fun _ : Fin n => 2)) := - outerPSpec F n params ++ₚ logupSumcheckPSpec F n M params - -/-- The full LogUp prover messages are oracle-accessible: outer LogUp messages followed by the -embedded sumcheck messages. -/ -noncomputable instance instPSpecMessageOracleInterface - {F : Type} [Field F] [Fintype F] [DecidableEq F] {n M : ℕ} - {params : ProtocolParams M} : - ∀ i, OracleInterface ((pSpec F n M params).Message i) := by - change ∀ i, - OracleInterface (((outerPSpec F n params) ++ₚ logupSumcheckPSpec F n M params).Message i) - exact ProtocolSpec.instOracleInterfaceMessageAppend - -/-- The full LogUp verifier challenges are sampleable: outer LogUp challenges followed by the -embedded sumcheck challenges. -/ -noncomputable instance instPSpecChallengeSampleable - {F : Type} [Field F] [Fintype F] [DecidableEq F] [SampleableType F] {n M : ℕ} - {params : ProtocolParams M} : - ∀ i, SampleableType ((pSpec F n M params).Challenge i) := by - letI : Inhabited F := ⟨0⟩ - change ∀ i, - SampleableType (((outerPSpec F n params) ++ₚ - logupSumcheckPSpec F n M params).Challenge i) - exact ProtocolSpec.instSampleableTypeChallengeAppend - -end FullProtocolSpec - -section OuterProver - variable {ι : Type} (oSpec : OracleSpec ι) variable (F : Type) [Field F] [Fintype F] [DecidableEq F] (n M : ℕ) variable (params : ProtocolParams M) @@ -117,7 +316,7 @@ def outerProverState : Fin 5 → Type /-- The honest prover for the outer LogUp phase. -/ noncomputable def outerProver : - OracleProver oSpec (StmtIn F n M) (OStmtIn F n M) (WitIn F n M params) + OracleProver oSpec (StmtIn F n M) (OStmtIn F n M) (Unit) (StmtAfterOuter F n M params) (OStmtAfterOuter F n M params) Unit (outerPSpec F n params) where PrvState := outerProverState F n M params @@ -147,60 +346,24 @@ noncomputable def outerProver : | .helpers => honestHelpers params oStmt x), ()) -end OuterProver - -section SumcheckProver - -variable {ι : Type} (oSpec : OracleSpec ι) -variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [Fact ((-1 : F) ≠ 1)] - [SampleableType F] (n M : ℕ) -variable (params : ProtocolParams M) - -/-- The prover for the embedded sumcheck phase of LogUp Protocol 2. -/ -noncomputable def sumcheckProver [SampleableType F] : - OracleProver oSpec (StmtAfterOuter F n M params) (OStmtAfterOuter F n M params) Unit - (StmtOut) (OStmtOut) Unit - (logupSumcheckPSpec F n M params) := - (sumcheckOracleReduction oSpec F n M params).prover - -end SumcheckProver - -section FullProver - -variable {ι : Type} (oSpec : OracleSpec ι) -variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [Fact ((-1 : F) ≠ 1)] - [SampleableType F] (n M : ℕ) -variable (params : ProtocolParams M) - -/-- The full LogUp prover, composed from the outer prover and embedded sumcheck prover. -/ -noncomputable def logupProver : - OracleProver oSpec (StmtIn F n M) (OStmtIn F n M) (WitIn F n M params) - (StmtOut) (OStmtOut) Unit - (pSpec F n M params) := - Prover.append (outerProver oSpec F n M params) (sumcheckProver oSpec F n M params) - -end FullProver - -section OuterVerifier - variable {ι : Type} (oSpec : OracleSpec ι) variable (F : Type) [Field F] [Fintype F] [DecidableEq F] (n M : ℕ) variable (params : ProtocolParams M) @[grind] -private def outerChallengeXIdx : (outerPSpec F n params).ChallengeIdx := +def outerChallengeXIdx : (outerPSpec F n params).ChallengeIdx := ⟨1, rfl⟩ @[grind] -private def outerChallengeBatchIdx : (outerPSpec F n params).ChallengeIdx := +def outerChallengeBatchIdx : (outerPSpec F n params).ChallengeIdx := ⟨3, rfl⟩ @[grind] -private def outerMultiplicityMessageIdx : (outerPSpec F n params).MessageIdx := +def outerMultiplicityMessageIdx : (outerPSpec F n params).MessageIdx := ⟨0, rfl⟩ @[grind] -private def outerHelpersMessageIdx : (outerPSpec F n params).MessageIdx := +def outerHelpersMessageIdx : (outerPSpec F n params).MessageIdx := ⟨2, rfl⟩ /-- The verifier for the outer LogUp phase. -/ @@ -210,11 +373,9 @@ noncomputable def outerVerifier : (outerPSpec F n params) where verify := fun _ challenges => do let x : F := challenges (outerChallengeXIdx F n M params) - -- TODO: Replace the current table-scan rejection check with a faithful sampler - -- for x ∉ { -t(u) : u ∈ H }. - for u in (Finset.univ : Finset (Hypercube n)).toList do - let tAtU : F ← query (spec := [OStmtIn F n M]ₒ) ⟨InputOracleIdx.table, signPoint F u⟩ - guard (x + tAtU ≠ 0) + -- Following Remark 3 of the LogUp paper, the verifier samples `x` uniformly and does not + -- scan the table to reject poles. Pole challenges are treated as bad/failing inputs for the + -- honest handoff, and `Completeness.lean` accounts for that event. let batch : BatchingChallenge F n params.numGroups := challenges (outerChallengeBatchIdx F n M params) pure { xChallenge := x, zChallenge := batch.1, batchingScalars := batch.2 } @@ -236,71 +397,414 @@ noncomputable def outerVerifier : | multiplicity => rfl | helpers => rfl -end OuterVerifier +variable {ι : Type} (oSpec : OracleSpec ι) +variable (F : Type) [Field F] [Fintype F] [DecidableEq F] (n M : ℕ) +variable (params : ProtocolParams M) + +/-- The outer LogUp phase as an ArkLib oracle reduction. -/ +noncomputable def outerOracleReduction : + OracleReduction oSpec (StmtIn F n M) (OStmtIn F n M) (Unit) + (StmtAfterOuter F n M params) (OStmtAfterOuter F n M params) Unit + (outerPSpec F n params) where + prover := outerProver oSpec F n M params + verifier := outerVerifier oSpec F n M params + +end Phase1 + + +/-! # Phase 2 — Sumcheck + +Runs ArkLib's generic sumcheck on the zero-sum claim for LogUp's polynomial `Q`. Contains the +bridge packaging `Q` for generic sumcheck, the context lens, the lifted prover/verifier, and +the assembled oracle reduction. -/ + +section Phase2 + +variable (F : Type) [Field F] [Fintype F] [DecidableEq F] (n M : ℕ) +variable (params : ProtocolParams M) + +/-- Individual-degree bound for LogUp's embedded sumcheck polynomial. -/ +def logupSumcheckDegree (_params : ProtocolParams M) : ℕ := + M + 3 + +/-- LogUp state after the embedded sumcheck, before the final oracle-query check. -/ +structure StmtAfterSumcheck where + /-- The outer transcript data retained for reconstructing `Q(r)`. -/ + outer : StmtAfterOuter F n M params + /-- Sumcheck's final point claim `Q(r) = v`. -/ + finalClaim : (Sumcheck.Spec.StatementRound F n (.last n)) + + +/-- LogUp enters the embedded sumcheck with the zero-sum claim. -/ +def logupInitialSumcheckStatement : (Sumcheck.Spec.StatementRound F n 0) where + target := 0 + challenges := fun i => Fin.elim0 i + +/-- Package `logupQPolynomial` with its degree certificate into ArkLib's oracle statement type. -/ +noncomputable def logupSumcheckPolynomial + (stmt : StmtAfterOuter F n M params) + (oStmt : ∀ i, OStmtAfterOuter F n M params i) : + (Sumcheck.Spec.OracleStatement F n (logupSumcheckDegree M params)) () := by + classical + refine ⟨logupQPolynomial (params.group) (oStmt (.input .table)).1 + (fun i => (oStmt (.input (.column i))).1) (oStmt .multiplicity).1 + (fun k => (oStmt .helpers k).1) stmt.xChallenge stmt.zChallenge stmt.batchingScalars, ?_⟩ + rw [MvPolynomial.mem_restrictDegree_iff_degreeOf_le] + intro i + exact logupQPolynomial_degreeOf (params.group) + ((MvPolynomial.mem_restrictDegree_iff_degreeOf_le _ _).mp (oStmt (.input .table)).2) + (fun j => (MvPolynomial.mem_restrictDegree_iff_degreeOf_le _ _).mp + (oStmt (.input (.column j))).2) ((MvPolynomial.mem_restrictDegree_iff_degreeOf_le _ _).mp + (oStmt .multiplicity).2) (fun k => (MvPolynomial.mem_restrictDegree_iff_degreeOf_le _ _).mp + (oStmt .helpers k).2) stmt.xChallenge stmt.zChallenge stmt.batchingScalars i + +/-- Package the LogUp `Q` polynomial as the single oracle statement expected by Sumcheck. -/ +noncomputable def logupSumcheckOracleStmt + (stmt : StmtAfterOuter F n M params) + (oStmt : ∀ i, OStmtAfterOuter F n M params i) : + ∀ i, Sumcheck.Spec.OracleStatement F n (logupSumcheckDegree M params) i := + fun _ => logupSumcheckPolynomial F n M params stmt oStmt + +/-- The LogUp zero-sum claim that is fed to the generic sumcheck. -/ +noncomputable def logupOuterSumcheckClaim + (stmt : StmtAfterOuter F n M params) + (oStmt : ∀ i, OStmtAfterOuter F n M params i) : F := + ∑ u : (Fin n → Fin 2), + MvPolynomial.eval (u : Fin n → F) + (logupQPolynomial (params.group) (oStmt (.input .table)).1 + (fun i => (oStmt (.input (.column i))).1) (oStmt .multiplicity).1 + (fun k => (oStmt .helpers k).1) stmt.xChallenge stmt.zChallenge stmt.batchingScalars) + +/-- Relation handed from the outer LogUp phase to the embedded sumcheck: the outer algebra produced +a genuine zero-sum claim. -/ +def logupMidRelation : + Set ((StmtAfterOuter F n M params × (∀ i, OStmtAfterOuter F n M params i)) × Unit) := + { x | logupOuterSumcheckClaim F n M params x.1.1 x.1.2 = 0 } + +variable (F : Type) [Field F] (n M : ℕ) +variable (params : ProtocolParams M) + +/-- The Boolean sumcheck domain, packaged in the form expected by `Sumcheck.Spec`. -/ +def booleanDomain : Fin 2 ↪ F where + toFun := fun b => (b : F) + inj' := by + intro a b h + fin_cases a <;> fin_cases b + · rfl + · simp at h + · simp at h + · rfl + +/-- Relation after embedded sumcheck: the final sumcheck point claim is valid for the retained +LogUp polynomial. The final LogUp phase consumes this by querying the retained oracles at that +point and recomputing `Q(r)`. -/ +def logupAfterSumcheckRelation : + Set ((StmtAfterSumcheck F n M params × (∀ i, OStmtAfterOuter F n M params i)) × Unit) := + { x | + ((x.1.1.finalClaim, + logupSumcheckOracleStmt F n M params x.1.1.outer x.1.2), ()) ∈ + Sumcheck.Spec.relationRound F n (logupSumcheckDegree M params) (booleanDomain F) + (Fin.last n) } + +/-- The initial generic Sumcheck relation induced by a LogUp outer transcript. -/ +def logupSumcheckRelationInput + (stmt : StmtAfterOuter F n M params) + (oStmt : ∀ i, OStmtAfterOuter F n M params i) : Prop := + ((logupInitialSumcheckStatement F n, logupSumcheckOracleStmt F n M params stmt oStmt), + ()) ∈ + Sumcheck.Spec.relationRound F n (logupSumcheckDegree M params) (booleanDomain F) 0 + +variable {ι : Type} (oSpec : OracleSpec ι) +variable (F : Type) [Field F] [Fintype F] [DecidableEq F] (n M : ℕ) +variable (params : ProtocolParams M) + +/-- Context lens from LogUp's retained outer state to ArkLib's generic Sumcheck state. + +The projection builds the generic zero-sum claim and its single polynomial oracle. The lift keeps +the outer LogUp data and retained oracles together with Sumcheck's final point claim, so the next +LogUp phase can perform the paper's final oracle-query check. +-/ +noncomputable def logupSumcheckContextLens : + OracleContext.Lens + (StmtAfterOuter F n M params) (StmtAfterSumcheck F n M params) + ((Sumcheck.Spec.StatementRound F n 0)) ((Sumcheck.Spec.StatementRound F n (.last n))) + (OStmtAfterOuter F n M params) (OStmtAfterOuter F n M params) + (Sumcheck.Spec.OracleStatement F n (logupSumcheckDegree M params)) + (Sumcheck.Spec.OracleStatement F n (logupSumcheckDegree M params)) + Unit Unit Unit Unit where + stmt := + ⟨fun ctx => + (logupInitialSumcheckStatement F n, + logupSumcheckOracleStmt F n M params ctx.1 ctx.2), + fun ctx inner => + ({ outer := ctx.1, finalClaim := inner.1 }, ctx.2)⟩ + wit := + ⟨fun _ => (), + fun _ _ => ()⟩ + +variable {ι : Type} (oSpec : OracleSpec ι) +variable (F : Type) [Field F] [Fintype F] [DecidableEq F] (n M : ℕ) +variable (params : ProtocolParams M) + +/-- ArkLib's generic sumcheck reduction specialized to LogUp's Boolean domain and degree bound. -/ +noncomputable def logupConcreteSumcheckOracleReduction [SampleableType F] : + OracleReduction oSpec ((Sumcheck.Spec.StatementRound F n 0)) + (Sumcheck.Spec.OracleStatement F n (logupSumcheckDegree M params)) Unit + ((Sumcheck.Spec.StatementRound F n (.last n))) + (Sumcheck.Spec.OracleStatement F n (logupSumcheckDegree M params)) Unit + ((Sumcheck.Spec.pSpec F (logupSumcheckDegree M params) n)) := + Sumcheck.Spec.oracleReduction F (logupSumcheckDegree M params) + (booleanDomain F) n oSpec -section SumcheckVerifier +variable {ι : Type} (oSpec : OracleSpec ι) +variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [SampleableType F] (n M : ℕ) +variable (params : ProtocolParams M) + +/-- The prover for the embedded sumcheck phase of LogUp Protocol 2. -/ +noncomputable def sumcheckProver : + OracleProver oSpec (StmtAfterOuter F n M params) (OStmtAfterOuter F n M params) Unit + (StmtAfterSumcheck F n M params) (OStmtAfterOuter F n M params) Unit + ((Sumcheck.Spec.pSpec F (logupSumcheckDegree M params) n)) := + (logupConcreteSumcheckOracleReduction oSpec F n M params).prover.liftContext + (logupSumcheckContextLens F n M params) variable {ι : Type} (oSpec : OracleSpec ι) -variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [Fact ((-1 : F) ≠ 1)] (n M : ℕ) +variable (F : Type) [Field F] [Fintype F] [DecidableEq F] (n M : ℕ) variable (params : ProtocolParams M) /-- The verifier for the embedded sumcheck phase of LogUp Protocol 2. -/ noncomputable def sumcheckVerifier [SampleableType F] : OracleVerifier oSpec (StmtAfterOuter F n M params) (OStmtAfterOuter F n M params) - (StmtOut) (OStmtOut) - (logupSumcheckPSpec F n M params) := - (sumcheckOracleReduction oSpec F n M params).verifier + (StmtAfterSumcheck F n M params) (OStmtAfterOuter F n M params) + ((Sumcheck.Spec.pSpec F (logupSumcheckDegree M params) n)) := + (logupConcreteSumcheckOracleReduction oSpec F n M params).verifier.liftContext + (logupSumcheckContextLens F n M params).stmt + +variable {ι : Type} (oSpec : OracleSpec ι) +variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [SampleableType F] (n M : ℕ) +variable (params : ProtocolParams M) + +/-- The embedded LogUp sumcheck phase, obtained by lifting ArkLib's generic Sumcheck reduction +through the LogUp-to-Sumcheck context lens with the generic `OracleReduction.liftContext`. Its +prover and verifier are defeq to `sumcheckProver`/`sumcheckVerifier`, which the full-protocol +appends consume directly. -/ +noncomputable def sumcheckOracleReduction : + OracleReduction oSpec (StmtAfterOuter F n M params) (OStmtAfterOuter F n M params) Unit + (StmtAfterSumcheck F n M params) (OStmtAfterOuter F n M params) Unit + ((Sumcheck.Spec.pSpec F (logupSumcheckDegree M params) n)) := + (logupConcreteSumcheckOracleReduction oSpec F n M params).liftContext + (logupSumcheckContextLens F n M params) + +end Phase2 + -end SumcheckVerifier +/-! # Phase 3 — Final point check -section FullVerifier +The verifier queries the retained LogUp oracles at sumcheck's final +point and checks that they reproduce the claimed value. -/ + +section Phase3 + +/-- The final LogUp point check has no transcript messages; it only queries retained oracles. -/ +@[reducible] +def finalCheckPSpec : ProtocolSpec 0 := + !p[] + +/-- The full LogUp protocol returns no additional public data on success. -/ +@[reducible, simp] +def StmtOut : Type := + Unit + +/-- The full LogUp protocol leaves no output oracle statements. -/ +@[reducible, simp] +def OutputOracleIdx : Type := + Fin 0 + +/-- Output oracle statements for the full LogUp protocol. -/ +@[reducible, simp] +def OStmtOut : OutputOracleIdx → Type := + fun i => Fin.elim0 i + +/-- The full LogUp protocol has no output oracle interfaces to provide. -/ +instance instOStmtOutOracleInterface : + ∀ i, OracleInterface (OStmtOut i) := + fun i => Fin.elim0 i + +/-- The final relation after the point check: accepted executions return `Unit`. -/ +def outputRelation : Set ((StmtOut × (∀ i, OStmtOut i)) × Unit) := + Set.univ variable {ι : Type} (oSpec : OracleSpec ι) -variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [Fact ((-1 : F) ≠ 1)] - [SampleableType F] (n M : ℕ) +variable (F : Type) [Field F] [Fintype F] [DecidableEq F] (n M : ℕ) variable (params : ProtocolParams M) -/-- The full LogUp verifier, obtained by composing the outer verifier with the embedded sumcheck -verifier. -/ -noncomputable def logupVerifier : - OracleVerifier oSpec (StmtIn F n M) (OStmtIn F n M) - (StmtOut) (OStmtOut) - (pSpec F n M params) := - OracleVerifier.append (outerVerifier oSpec F n M params) (sumcheckVerifier oSpec F n M params) +/-- The prover for the final LogUp point check; there are no messages in this phase. -/ +noncomputable def finalCheckProver : + OracleProver oSpec (StmtAfterSumcheck F n M params) (OStmtAfterOuter F n M params) Unit + StmtOut OStmtOut Unit + finalCheckPSpec where + PrvState := fun _ => StmtAfterSumcheck F n M params × + (∀ i, OStmtAfterOuter F n M params i) + input := fun ⟨ctx, _⟩ => ctx + sendMessage := fun i => Fin.elim0 i + receiveChallenge := fun i => Fin.elim0 i + output := fun _ => pure ((((), fun i => Fin.elim0 i), ())) -end FullVerifier +variable {ι : Type} (oSpec : OracleSpec ι) +variable (F : Type) [Field F] [Fintype F] [DecidableEq F] (n M : ℕ) +variable (params : ProtocolParams M) + +/-- Query one retained LogUp oracle during the final point check. -/ +def finalCheckQuery + (i : OuterOracleIdx M) + (q : (instOStmtAfterOuterOracleInterface (F := F) (n := n) (params := params) i).Query) : + OptionT + (OracleComp (oSpec + ([OStmtAfterOuter F n M params]ₒ + [finalCheckPSpec.Message]ₒ))) + ((instOStmtAfterOuterOracleInterface (F := F) (n := n) (params := params) i).Response q) := + OptionT.mk <| some <$> OracleComp.lift + (OracleSpec.query + (show (oSpec + ([OStmtAfterOuter F n M params]ₒ + + [finalCheckPSpec.Message]ₒ)).Domain from Sum.inr (Sum.inl ⟨i, q⟩))) + +/-- The verifier's final Protocol 2 check: reconstruct `Q(r)` from retained LogUp oracle +evaluations and compare it with the expected value output by sumcheck. -/ +noncomputable def finalCheckVerifier : + OracleVerifier oSpec (StmtAfterSumcheck F n M params) (OStmtAfterOuter F n M params) + StmtOut OStmtOut + finalCheckPSpec where + verify := fun stmt _ => do + let r : Fin n → F := stmt.finalClaim.challenges + let expectedValue : F := stmt.finalClaim.target + let multiplicity ← finalCheckQuery oSpec F n M params .multiplicity r + let table ← finalCheckQuery oSpec F n M params (.input .table) r + let columnValues ← (Vector.finRange M).mapM + (fun i => finalCheckQuery oSpec F n M params (.input (.column i)) r) + let helperValues ← (Vector.finRange params.numGroups).mapM + (fun k => finalCheckQuery oSpec F n M params .helpers ⟨k, r⟩) + guard (qAtPoint (params.group) stmt.outer.xChallenge stmt.outer.zChallenge r + stmt.outer.batchingScalars multiplicity table (fun i => columnValues[i]) + (fun k => helperValues[k]) = expectedValue) + pure () + + embed := + { toFun := fun i => Fin.elim0 i + inj' := fun i => Fin.elim0 i } -section OuterReduction + hEq := fun i => Fin.elim0 i variable {ι : Type} (oSpec : OracleSpec ι) variable (F : Type) [Field F] [Fintype F] [DecidableEq F] (n M : ℕ) variable (params : ProtocolParams M) -/-- The outer LogUp phase as an ArkLib oracle reduction. -/ -noncomputable def outerOracleReduction : - OracleReduction oSpec (StmtIn F n M) (OStmtIn F n M) (WitIn F n M params) - (StmtAfterOuter F n M params) (OStmtAfterOuter F n M params) Unit - (outerPSpec F n params) where - prover := outerProver oSpec F n M params - verifier := outerVerifier oSpec F n M params +/-- The final LogUp point check as an ArkLib oracle reduction. -/ +noncomputable def finalCheckOracleReduction : + OracleReduction oSpec (StmtAfterSumcheck F n M params) (OStmtAfterOuter F n M params) Unit + (StmtOut) (OStmtOut) Unit + finalCheckPSpec where + prover := finalCheckProver oSpec F n M params + verifier := finalCheckVerifier oSpec F n M params + +end Phase3 + + +/-! # Full protocol + +The three phase reductions composed into the full LogUp transcript, prover, verifier, and oracle +reduction. -/ + +section FullProtocol + +open ProtocolSpec + +/-- Protocol 2 before the final point check: outer LogUp followed by generic sumcheck. -/ +@[reducible] +noncomputable def pSpecBeforeFinal (F : Type) [Field F] [Fintype F] [DecidableEq F] + (n M : ℕ) (params : ProtocolParams M) := + outerPSpec F n params ++ₚ (Sumcheck.Spec.pSpec F (logupSumcheckDegree M params) n) + +/-- Protocol 2 transcript shape: outer LogUp, ArkLib's generic sumcheck, and the final point check. +-/ +@[reducible] +noncomputable def pSpec (F : Type) [Field F] [Fintype F] [DecidableEq F] + (n M : ℕ) (params : ProtocolParams M) := + pSpecBeforeFinal F n M params ++ₚ finalCheckPSpec + +/-- The prover messages before the final check are oracle-accessible: outer LogUp followed by the +embedded sumcheck messages. -/ +noncomputable instance instPSpecBeforeFinalMessageOracleInterface + {F : Type} [Field F] [Fintype F] [DecidableEq F] {n M : ℕ} + {params : ProtocolParams M} : + ∀ i, OracleInterface ((pSpecBeforeFinal F n M params).Message i) := by + unfold pSpecBeforeFinal + exact ProtocolSpec.instOracleInterfaceMessageAppend + +/-- The full LogUp prover messages are oracle-accessible: outer LogUp and sumcheck messages; the +final point check has no messages. -/ +noncomputable instance instPSpecMessageOracleInterface + {F : Type} [Field F] [Fintype F] [DecidableEq F] {n M : ℕ} + {params : ProtocolParams M} : + ∀ i, OracleInterface ((pSpec F n M params).Message i) := by + unfold pSpec + exact ProtocolSpec.instOracleInterfaceMessageAppend + +/-- The verifier challenges before the final check are sampleable: outer LogUp followed by the +embedded sumcheck challenges. -/ +noncomputable instance instPSpecBeforeFinalChallengeSampleable + {F : Type} [Field F] [Fintype F] [DecidableEq F] [SampleableType F] {n M : ℕ} + {params : ProtocolParams M} : + ∀ i, SampleableType ((pSpecBeforeFinal F n M params).Challenge i) := by + unfold pSpecBeforeFinal + exact ProtocolSpec.instSampleableTypeChallengeAppend + +/-- The full LogUp verifier challenges are sampleable: the final point check has no challenges. -/ +noncomputable instance instPSpecChallengeSampleable + {F : Type} [Field F] [Fintype F] [DecidableEq F] [SampleableType F] {n M : ℕ} + {params : ProtocolParams M} : + ∀ i, SampleableType ((pSpec F n M params).Challenge i) := by + unfold pSpec + exact ProtocolSpec.instSampleableTypeChallengeAppend + +variable {ι : Type} (oSpec : OracleSpec ι) +variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [SampleableType F] (n M : ℕ) +variable (params : ProtocolParams M) -end OuterReduction +/-- The full LogUp prover, composed from the outer prover and embedded sumcheck prover. -/ +noncomputable def logupProver : + OracleProver oSpec (StmtIn F n M) (OStmtIn F n M) (Unit) + (StmtOut) (OStmtOut) Unit + (pSpec F n M params) := + Prover.append + (Prover.append (outerProver oSpec F n M params) (sumcheckProver oSpec F n M params)) + (finalCheckProver oSpec F n M params) -section FullReduction +variable {ι : Type} (oSpec : OracleSpec ι) +variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [SampleableType F] (n M : ℕ) +variable (params : ProtocolParams M) + +/-- The full LogUp verifier, obtained by composing the outer verifier with the embedded sumcheck +verifier and final point check. -/ +noncomputable def logupVerifier : + OracleVerifier oSpec (StmtIn F n M) (OStmtIn F n M) + (StmtOut) (OStmtOut) + (pSpec F n M params) := + OracleVerifier.append + (OracleVerifier.append (outerVerifier oSpec F n M params) + (sumcheckVerifier oSpec F n M params)) + (finalCheckVerifier oSpec F n M params) variable {ι : Type} (oSpec : OracleSpec ι) -variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [Fact ((-1 : F) ≠ 1)] - [SampleableType F] (n M : ℕ) +variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [SampleableType F] (n M : ℕ) variable (params : ProtocolParams M) /-- The full LogUp Protocol as an ArkLib oracle reduction. -/ noncomputable def logupOracleReduction : - OracleReduction oSpec (StmtIn F n M) (OStmtIn F n M) (WitIn F n M params) + OracleReduction oSpec (StmtIn F n M) (OStmtIn F n M) (Unit) (StmtOut) (OStmtOut) Unit (pSpec F n M params) where prover := logupProver oSpec F n M params verifier := logupVerifier oSpec F n M params -end FullReduction +end FullProtocol + end Logup diff --git a/ArkLib/ProofSystem/Logup/Security/Completeness.lean b/ArkLib/ProofSystem/Logup/Security/Completeness.lean index c6cea978d6..564d210859 100644 --- a/ArkLib/ProofSystem/Logup/Security/Completeness.lean +++ b/ArkLib/ProofSystem/Logup/Security/Completeness.lean @@ -1,40 +1,963 @@ import ArkLib.OracleReduction.Security.Basic +import ArkLib.OracleReduction.Composition.Sequential.Append +import ArkLib.ProofSystem.Sumcheck.Spec.General import ArkLib.ProofSystem.Logup.Protocol +import ArkLib.ToVCVio.OracleComp.Coercions.SubSpec /-! # LogUp Completeness -Main completeness statement for Protocol 2 of `paper.txt`. +Completeness statements for Protocol 2 of Haböck's LogUp lookup argument (Cryptology ePrint +Archive, Paper 2022/1530, ). -/ open scoped NNReal namespace Logup +section ProtocolAlgebra + +variable {F : Type} [Field F] {M : ℕ} + +/-- The protocol's concrete partial-sum groups partition the term indices `{0, …, M}`. -/ +theorem sum_protocolGroups (params : ProtocolParams M) (g : TermIdx M → F) : + (∑ k : Fin params.numGroups, ∑ i ∈ params.group k, g i) = ∑ i : TermIdx M, g i := by + classical + have hℓ := params.sumSize_pos + have hidx : ∀ i : TermIdx M, i.val / params.sumSize < params.numGroups := by + intro i + have hiM : i.val ≤ M := Nat.lt_succ_iff.mp i.isLt + have hle : i.val / params.sumSize ≤ M / params.sumSize := Nat.div_le_div_right hiM + rw [ProtocolParams.numGroups, Nat.add_div_right _ hℓ] + omega + rw [← Finset.sum_fiberwise Finset.univ + (fun i : TermIdx M => (⟨i.val / params.sumSize, hidx i⟩ : Fin params.numGroups)) g] + refine Finset.sum_congr rfl (fun k _ => ?_) + congr 1 + ext i + simp only [ProtocolParams.group, Finset.mem_filter, Finset.mem_univ, true_and, Fin.ext_iff] + constructor + · rintro ⟨h1, h2⟩ + have ha : k.val ≤ i.val / params.sumSize := (Nat.le_div_iff_mul_le hℓ).mpr h1 + have hb : i.val / params.sumSize < k.val + 1 := (Nat.div_lt_iff_lt_mul hℓ).mpr h2 + omega + · intro h + exact ⟨(Nat.le_div_iff_mul_le hℓ).mp (by omega), (Nat.div_lt_iff_lt_mul hℓ).mp (by omega)⟩ + +end ProtocolAlgebra + section Completeness variable {ι : Type} (oSpec : OracleSpec ι) -variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [Fact ((-1 : F) ≠ 1)] - [SampleableType F] +variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [SampleableType F] variable (n M : ℕ) variable (params : ProtocolParams M) variable {σ : Type} (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) -/-- Completeness error forced by the current rejection-based model of the `x` challenge. +local instance instOracleCompLawfulMonad' {τ : Type} (spec : OracleSpec τ) : + LawfulMonad (OracleComp spec) := + OracleComp.instLawfulMonad spec -Protocol 2 samples `x` from the complement of the table poles. The current verifier samples from -all of `F` and rejects poles, so the intended completeness statement carries this explicit bad-`x` -probability. Once the challenge sampler is modeled as the complement distribution, this should -collapse to perfect completeness. --/ +local instance instOuterChallengeOracleInterface' : + (i : (outerPSpec F n params).ChallengeIdx) → + OracleInterface ((outerPSpec F n params).Challenge i) := + ProtocolSpec.challengeOracleInterface + +omit [Fintype F] [DecidableEq F] [SampleableType F] in +private theorem sum_piFinset_map_univ_eq_sum_hypercube + (D : Fin 2 ↪ F) (f : (Fin n → F) → F) : + (∑ x ∈ Fintype.piFinset fun _ : Fin n => Finset.univ.map D, f x) = + ∑ u : (Fin n → Fin 2), f (fun j => D (u j)) := by + let e : (Fin n → Fin 2) ↪ (Fin n → F) := Function.Embedding.arrowCongrRight D + change (∑ x ∈ Fintype.piFinset fun _ : Fin n => Finset.univ.map D, f x) = + ∑ u : (Fin n → Fin 2), f (e u) + rw [← Finset.sum_map] + congr 1 + ext x + constructor + · intro hx + rw [Fintype.mem_piFinset] at hx + have hx_coord : ∀ j : Fin n, ∃ b : Fin 2, D b = x j := by + intro j + rcases Finset.mem_map.mp (hx j) with ⟨b, _, hb⟩ + exact ⟨b, hb⟩ + let u : (Fin n → Fin 2) := fun j => Classical.choose (hx_coord j) + exact Finset.mem_map.mpr ⟨u, Finset.mem_univ _, by + funext j + exact Classical.choose_spec (hx_coord j)⟩ + · intro hx + rw [Fintype.mem_piFinset] + intro j + rcases Finset.mem_map.mp hx with ⟨u, _, rfl⟩ + exact Finset.mem_map.mpr ⟨u j, Finset.mem_univ _, rfl⟩ + +omit [Fintype F] [DecidableEq F] [SampleableType F] in +/-- If LogUp's outer algebra proves a zero sum, then the generic Sumcheck input relation is exactly +the claim sent to Sumcheck. -/ +theorem logupSumcheckRelationInput_of_zero + {stmt : StmtAfterOuter F n M params} + {oStmt : ∀ i, OStmtAfterOuter F n M params i} + (hZero : logupOuterSumcheckClaim F n M params stmt oStmt = 0) : + logupSumcheckRelationInput F n M params stmt oStmt := by + unfold logupSumcheckRelationInput Sumcheck.Spec.relationRound + simp only [Fin.coe_ofNat_eq_mod, Nat.zero_mod, Nat.sub_zero, logupInitialSumcheckStatement, + Set.mem_setOf_eq, Fin.elim0_append, logupSumcheckOracleStmt] + change + (∑ x ∈ Fintype.piFinset fun _ : Fin n => Finset.univ.map (booleanDomain F), + MvPolynomial.eval ((x ∘ Fin.cast (by omega)) ∘ Fin.cast (by omega)) + (logupSumcheckPolynomial F n M params stmt oStmt).val) = 0 + rw [sum_piFinset_map_univ_eq_sum_hypercube + (F := F) (n := n) (D := booleanDomain F) + (f := fun x => + MvPolynomial.eval ((x ∘ Fin.cast (by omega)) ∘ Fin.cast (by omega)) + (logupSumcheckPolynomial F n M params stmt oStmt).val)] + calc + (∑ u : (Fin n → Fin 2), + MvPolynomial.eval + ((((fun j => (booleanDomain F) (u j)) ∘ Fin.cast (by omega)) ∘ + Fin.cast (by omega))) + (logupSumcheckPolynomial F n M params stmt oStmt).val) + = + logupOuterSumcheckClaim F n M params stmt oStmt := by + rw [logupOuterSumcheckClaim] + apply Finset.sum_congr rfl + intro u _ + simp only [booleanDomain, logupSumcheckPolynomial] + congr 1 + _ = 0 := hZero + +/-- Completeness error from the current `x`-sampling model: the verifier samples `x` from all of +`F`. Following Remark 3 of the LogUp paper, table-pole challenges are treated as bad inputs for +the honest handoff rather than rejected by an exponential verifier scan. -/ noncomputable def logupCompletenessError (F : Type) [Fintype F] (n : ℕ) : ℝ≥0 := - (Fintype.card (Hypercube n) : ℝ≥0) / (Fintype.card F) + (Fintype.card (Fin n → Fin 2) : ℝ≥0) / (Fintype.card F) + +omit [DecidableEq F] in +private theorem uniform_avoids_table_poles_prob [Inhabited F] + (oStmt : ∀ i, OStmtIn F n M i) : + (1 : ENNReal) - (logupCompletenessError F n : ENNReal) ≤ + Pr[fun x : F => ∀ u : (Fin n → Fin 2), + x + MvPolynomial.toEvalsZeroOne (oStmt .table).1 u ≠ 0 | $ᵗ F] := by + classical + letI : DecidableEq F := Classical.decEq F + let bad : F → Prop := + fun x => ∃ u : (Fin n → Fin 2), x + MvPolynomial.toEvalsZeroOne (oStmt .table).1 u = 0 + have hbad : + Pr[bad | $ᵗ F] ≤ (logupCompletenessError F n : ENNReal) := by + rw [probEvent_uniformSample] + unfold logupCompletenessError + have hcard : + ((Finset.univ.filter bad).card : ENNReal) ≤ + (Fintype.card (Fin n → Fin 2) : ENNReal) := by + exact_mod_cast (by + simpa [bad] using + pole_card_le (F := F) (n := n) (table := MvPolynomial.toEvalsZeroOne (oStmt .table).1)) + convert ENNReal.div_le_div_right hcard (Fintype.card F : ENNReal) using 1; norm_num + have hcompl : + Pr[fun x : F => ¬ bad x | $ᵗ F] + Pr[bad | $ᵗ F] = (1 : ENNReal) := by + have h := probEvent_compl ($ᵗ F) (fun x : F => ¬ bad x) + simpa [bad, probFailure_uniformSample, not_not] using h + rw [tsub_le_iff_right] + calc + (1 : ENNReal) = Pr[fun x : F => ¬ bad x | $ᵗ F] + Pr[bad | $ᵗ F] := hcompl.symm + _ ≤ Pr[fun x : F => ¬ bad x | $ᵗ F] + (logupCompletenessError F n : ENNReal) := + add_le_add le_rfl hbad + · apply le_of_eq + congr + funext x + simp [bad] + +private theorem le_probEvent_bind_of_forall_le {m : Type → Type*} [Monad m] [LawfulMonad m] + [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [MonadLiftT m SetM] + [LawfulMonadLiftT m SetM] [EvalDistCompatible m] + {α β : Type} {mx : m α} {my : α → m β} {q : β → Prop} {r : ENNReal} + (hfail : Pr[⊥ | mx] = 0) (h : ∀ x ∈ support mx, r ≤ Pr[ q | my x]) : + r ≤ Pr[ q | mx >>= my] := by + have htrue : Pr[fun _ : α => True | mx] = (1 : ENNReal) := by + exact probEvent_eq_one (mx := mx) (p := fun _ : α => True) ⟨hfail, by simp⟩ + have hmul := mul_le_probEvent_bind (mx := mx) (my := my) + (p := fun _ : α => True) (q := q) (r := 1) (r' := r) + (by simp [htrue]) (fun x hx _ => h x hx) + simpa using hmul + +private theorem support_pure_eq {m : Type → Type*} [Monad m] [LawfulMonad m] + [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] + {α : Type} {x y : α} (h : y ∈ support (pure x : m α)) : y = x := by + simpa [mem_support_pure_iff] using h + +private theorem support_simulateQ_run_fst_subset {ι : Type} {spec : OracleSpec ι} + {m : Type → Type*} [Monad m] [LawfulMonad m] [MonadLiftT m SetM] + [LawfulMonadLiftT m SetM] {σ α : Type} + (impl : QueryImpl spec (StateT σ m)) {oa : OracleComp spec α} {s s' : σ} {y : α} + (h : (y, s') ∈ support ((simulateQ impl oa).run s)) : + y ∈ support oa := + OracleComp.support_simulateQ_run'_subset impl oa s (by + rw [StateT.run'_eq, support_map, Set.mem_image] + exact ⟨(y, s'), h, rfl⟩) + +private theorem mem_support_liftM_oracleComp {ι τ : Type} {spec : OracleSpec ι} + {superSpec : OracleSpec τ} {α : Type} + [MonadLift (OracleQuery spec) (OracleQuery superSpec)] + {oa : OracleComp spec α} {x : α} + (h : x ∈ support (liftM oa : OracleComp superSpec α)) : x ∈ support oa := by + rw [← OracleComp.liftComp_eq_liftM (superSpec := superSpec) oa] at h + exact OracleComp.mem_support_of_mem_support_liftComp oa x h + + +private theorem reduction_run_prover_mem {ι : Type} {oSpec : OracleSpec ι} + {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} + (R : Reduction oSpec StmtIn WitIn StmtOut WitOut pSpec) + (stmt : StmtIn) (wit : WitIn) + (tr : pSpec.FullTranscript) (out : StmtOut) (witOut : WitOut) (verOut : StmtOut) + (h : some ((tr, out, witOut), verOut) ∈ support (R.run stmt wit).run) : + (tr, out, witOut) ∈ support (Prover.run stmt wit R.prover) := by + simp only [ProtocolSpec.ChallengeIdx, ProtocolSpec.Challenge, Reduction.run, bind_pure_comp, + OptionT.run_bind, OptionT.run_monadLift, monadLift_self, + OracleSpec.ProgrammingPolicy.empty_apply, OptionT.run_map, Option.elimM_map, Option.elim_some, + support_bind, Set.mem_iUnion, exists_prop, Prod.exists] at h + rcases h with ⟨a, a_1, b, hp, hv⟩ + suffices hEq : (a, a_1, b) = (tr, out, witOut) by + simpa [hEq] using hp + simp only [Option.elimM, support_bind, Set.mem_iUnion, exists_prop] at hv + rcases hv with ⟨i, _hi, hv⟩ + cases i with + | none => simp at hv + | some verCandidate => + simp only [Option.elim_some, support_map, Set.mem_image, Option.map_eq_some_iff, + Prod.mk.injEq, exists_eq_right_right, ↓existsAndEq, true_and] at hv + rcases hv with ⟨_, rfl, rfl, rfl⟩ + rfl + +private theorem seqCompose_prover_preserves {ι : Type} {oSpec : OracleSpec ι} (m : ℕ) : + ∀ {Stmt : Fin (m + 1) → Type} {O : Type} + {rounds : Fin m → ℕ} {pSpec : ∀ i, ProtocolSpec (rounds i)} + (P : (i : Fin m) → Prover oSpec (Stmt i.castSucc) Unit (Stmt i.succ) Unit (pSpec i)) + (proj : (i : Fin (m + 1)) → Stmt i → O), + (∀ (i : Fin m) (stmt : Stmt i.castSucc) (out : Stmt i.succ) + (tr : (pSpec i).FullTranscript), + (tr, out, ()) ∈ support (Prover.run stmt () (P i)) → + proj i.succ out = proj i.castSucc stmt) → + ∀ (stmt : Stmt 0) (out : Stmt (Fin.last m)) + (tr : (ProtocolSpec.seqCompose pSpec).FullTranscript), + (tr, out, ()) ∈ support (Prover.run stmt () (Prover.seqCompose Stmt (fun _ => Unit) P)) → + proj (Fin.last m) out = proj 0 stmt := by + induction m with + | zero => + intro Stmt O rounds pSpec P proj hP stmt out tr h + rw [Prover.seqCompose_zero] at h + simp only [Fin.vsum_zero, Fin.reduceLast, Nat.reduceAdd, ProtocolSpec.ChallengeIdx, + ProtocolSpec.Challenge, Prover.run, Fin.isValue, Prover.id, ProtocolSpec.MessageIdx, + ProtocolSpec.Message, Prover.runToRound, id_eq, Fin.induction_zero] at h + cases h + rfl + | succ m ih => + intro Stmt O rounds pSpec P proj hP stmt out tr h + let tailSpec : ProtocolSpec (Fin.vsum fun i : Fin m => rounds (Fin.succ i)) := + ProtocolSpec.seqCompose (fun i : Fin m => pSpec (Fin.succ i)) + let tail : Prover oSpec (Stmt (Fin.succ 0)) Unit (Stmt (Fin.last (m + 1))) Unit + tailSpec := + Prover.seqCompose (fun i => Stmt i.succ) (fun _ => Unit) + (fun i => P (Fin.succ i)) + let trApp : ((pSpec 0) ++ₚ tailSpec).FullTranscript := tr + have h' : (trApp, out, ()) ∈ support (((do + let ⟨tr₁, stmt₂, wit₂⟩ ← liftM (Prover.run stmt () (P 0)) + let ⟨tr₂, stmt₃, wit₃⟩ ← liftM (Prover.run stmt₂ wit₂ tail) + pure (tr₁ ++ₜ tr₂, stmt₃, wit₃)) : + OracleComp (oSpec + [((pSpec 0) ++ₚ tailSpec).Challenge]ₒ) + (((pSpec 0) ++ₚ tailSpec).FullTranscript × Stmt (Fin.last (m + 1)) × Unit))) := by + rw [← @Prover.append_run ι oSpec (Stmt 0) Unit (Stmt (Fin.succ 0)) Unit + (Stmt (Fin.last (m + 1))) Unit (rounds 0) + (Fin.vsum fun i : Fin m => rounds (Fin.succ i)) + (pSpec 0) tailSpec (P 0) tail stmt ()] + simpa [trApp, tail, tailSpec, Prover.seqCompose_succ] using h + rw [mem_support_bind_iff] at h' + rcases h' with ⟨⟨tr₁, stmt₂, wit₂⟩, h₁, hrest⟩ + cases wit₂ + rw [mem_support_bind_iff] at hrest + rcases hrest with ⟨⟨tr₂, stmt₃, wit₃⟩, h₂, hpure⟩ + cases wit₃ + rw [support_pure, Set.mem_singleton_iff] at hpure + injection hpure with htr hout + have h₁' : (tr₁, stmt₂, ()) ∈ support (Prover.run stmt () (P 0)) := + mem_support_liftM_oracleComp + (superSpec := oSpec + [((pSpec 0) ++ₚ tailSpec).Challenge]ₒ) h₁ + have h₂' : (tr₂, out, ()) ∈ support + (Prover.run stmt₂ () + (Prover.seqCompose (fun i => Stmt i.succ) (fun _ => Unit) + (fun i => P (Fin.succ i)))) := by + cases hout + exact mem_support_liftM_oracleComp + (superSpec := oSpec + [((pSpec 0) ++ₚ tailSpec).Challenge]ₒ) h₂ + calc + proj (Fin.last (m + 1)) out = proj (Fin.succ (Fin.last m)) out := rfl + _ = proj (Fin.succ (0 : Fin (m + 1))) stmt₂ := by + exact ih + (P := fun i => P (Fin.succ i)) + (proj := fun i => proj (Fin.succ i)) + (fun i stmt out tr h => hP (Fin.succ i) stmt out tr h) + stmt₂ out tr₂ h₂' + _ = proj 0 stmt := hP 0 stmt stmt₂ tr₁ h₁' + +private theorem sumcheckSingleRound_prover_preserves_oracleStmt + {R : Type} [CommSemiring R] [DecidableEq R] [SampleableType R] + {n deg : ℕ} {m : ℕ} (D : Fin m ↪ R) {ι : Type} (oSpec : OracleSpec ι) (i : Fin n) + (stmt : Sumcheck.Spec.StatementRound R n i.castSucc × + (∀ j, Sumcheck.Spec.OracleStatement R n deg j)) + (out : Sumcheck.Spec.StatementRound R n i.succ × + (∀ j, Sumcheck.Spec.OracleStatement R n deg j)) + (tr : (Sumcheck.Spec.SingleRound.pSpec R deg).FullTranscript) + (h : (tr, out, ()) ∈ support + (Prover.run stmt () + ((Sumcheck.Spec.SingleRound.oracleReduction R n deg D oSpec i).toReduction.prover))) : + out.2 = stmt.2 := by + rw [Sumcheck.Spec.SingleRound.oracleReduction, OracleReduction.toReduction, + OracleReduction.liftContext, OracleProver.liftContext, Prover.liftContext_run] at h + rw [mem_support_bind_iff] at h + rcases h with ⟨⟨trInner, innerOut, innerWit⟩, _, hout⟩ + rw [support_pure, Set.mem_singleton_iff] at hout + cases hout + rcases stmt with ⟨⟨oldTarget, challenges⟩, oStmt⟩ + rcases innerOut with ⟨⟨newTarget, chal⟩, oStmt'⟩ + rfl + +private theorem sumcheckProver_preserves_oracleStmt + {R : Type} [CommSemiring R] [DecidableEq R] [SampleableType R] + {deg : ℕ} {m : ℕ} (D : Fin m ↪ R) {ι : Type} (oSpec : OracleSpec ι) (n : ℕ) + (stmt : Sumcheck.Spec.StatementRound R n 0 × + (∀ j, Sumcheck.Spec.OracleStatement R n deg j)) + (out : Sumcheck.Spec.StatementRound R n (Fin.last n) × + (∀ j, Sumcheck.Spec.OracleStatement R n deg j)) + (tr : (Sumcheck.Spec.pSpec R deg n).FullTranscript) + (h : (tr, out, ()) ∈ support + (Prover.run stmt () ((Sumcheck.Spec.oracleReduction R deg D n oSpec).toReduction.prover))) : + out.2 = stmt.2 := by + refine @seqCompose_prover_preserves ι oSpec n + (Stmt := fun i => Sumcheck.Spec.StatementRound R n i × + (∀ j, Sumcheck.Spec.OracleStatement R n deg j)) + (O := ∀ j, Sumcheck.Spec.OracleStatement R n deg j) + (rounds := fun _ => 2) + (pSpec := fun _ => Sumcheck.Spec.SingleRound.pSpec R deg) + (P := fun i => (Sumcheck.Spec.SingleRound.oracleReduction R n deg D oSpec i).toReduction.prover) + (proj := fun _ stmt => stmt.2) ?_ stmt out tr ?_ + · intro i stmt out tr h + exact sumcheckSingleRound_prover_preserves_oracleStmt D oSpec i stmt out tr h + · simpa [Sumcheck.Spec.oracleReduction, OracleReduction.seqCompose, OracleProver.seqCompose, + OracleReduction.toReduction] using h + +local macro "peel_sim_map " h:ident " with " pat:rcasesPat : tactic => + `(tactic| + (erw [simulateQ_map, StateT.run_map] at $h:ident + rw [support_map, Set.mem_image] at $h:ident + obtain $pat := $h)) + +local macro "peel_sim_bind " h:ident " with " pat:rcasesPat : tactic => + `(tactic| + (erw [simulateQ_bind, StateT.run_bind] at $h:ident + rw [mem_support_bind_iff] at $h:ident + obtain $pat := $h)) + +open OracleComp OracleSpec in +omit σ init impl [DecidableEq F] [SampleableType F] in +/-- Simulating the scan-free outer verifier against the honest oracles leaves only the public +challenge data packaged as the outer statement. -/ +theorem outerVerify_simulateQ_eq (stmt : StmtIn F n M) (oStmt : ∀ i, OStmtIn F n M i) + (messages : ∀ i, (outerPSpec F n params).Message i) + (challenges : ∀ i, (outerPSpec F n params).Challenge i) : + simulateQ (OracleInterface.simOracle2 oSpec oStmt messages) + ((outerVerifier oSpec F n M params).verify stmt challenges) + = (do + let x : F := challenges (outerChallengeXIdx F n M params) + let batch : BatchingChallenge F n params.numGroups := + challenges (outerChallengeBatchIdx F n M params) + pure { xChallenge := x, zChallenge := batch.1, batchingScalars := batch.2 } + : OptionT (OracleComp oSpec) (StmtAfterOuter F n M params)) := by + simp [outerVerifier, outerChallengeXIdx, outerChallengeBatchIdx] + rfl + +/-- Four-round unfolding of `Fin.induction` (the analog of `Fin.induction_two`), for the outer +LogUp prover's `runToRound`. -/ +private theorem Fin.induction_four {motive : Fin 5 → Sort*} {zero : motive 0} + {succ : ∀ i : Fin 4, motive i.castSucc → motive i.succ} : + Fin.induction (motive := motive) zero succ (Fin.last 4) + = succ 3 (succ 2 (succ 1 (succ 0 zero))) := rfl + +set_option maxHeartbeats 1000000 in +-- The proof peels the whole four-round outer transcript and reconstructs the handoff relation; +-- the generated support terms are large even though the reasoning is deterministic. + +/-- Completeness of the outer LogUp phase: the honest outer prover reaches the zero-sum handoff +relation, except with the pole-sampling error. -/ +theorem logup_outer_completeness [Inhabited F] : + (outerOracleReduction oSpec F n M params).completeness init impl + (inputRelation F n M) (logupMidRelation F n M params) (logupCompletenessError F n) := by + unfold OracleReduction.completeness Reduction.completeness + rintro ⟨stmt, oStmt⟩ ⟨⟩ hIn + simp only [outerOracleReduction, OracleReduction.toReduction, Reduction.run, Prover.run, + Verifier.run, Prover.runToRound, outerProver, Fin.induction_four, + Prover.processRound, outerPSpec] + repeat' split <;> rename_i hd <;> first | exact absurd hd (by decide) | skip + simp only [ProtocolSpec.getChallenge, liftM, monadLift, MonadLift.monadLift, + MonadLiftT.monadLift, OracleComp.liftComp_pure, bind_pure_comp, map_pure, + QueryImpl.addLift_def] + refine ge_trans (probEvent_mono + (p := fun out => ∀ u : (Fin n → Fin 2), + out.2.1.xChallenge + MvPolynomial.toEvalsZeroOne (oStmt .table).1 u ≠ 0) + ?goodOutputs) ?goodProb + · -- every output with a non-pole outer challenge satisfies the success predicate + intro out hout hGood + rw [OptionT.mem_support_iff] at hout + simp only [OptionT.run_mk, support_bind, Set.mem_iUnion] at hout + obtain ⟨s, -, hout⟩ := hout + simp only [StateT.run'_eq, support_map, Set.mem_image] at hout + obtain ⟨⟨_, s'⟩, hout, rfl⟩ := hout + peel_sim_bind hout with ⟨⟨pres, s2⟩, hpres, hver⟩ + simp only [OptionT.lift, OptionT.mk] at hpres + peel_sim_map hpres with ⟨⟨pval, sp⟩, hpval, hpeq⟩ + peel_sim_map hpval with ⟨⟨a, sa⟩, ha, hpval_eq⟩ + peel_sim_bind ha with ⟨⟨b, sb⟩, hb, ha3⟩ + peel_sim_map ha3 with ⟨⟨zlam, szlam⟩, hzlam, ha3eq⟩ + -- round 1: peel `hb` to reach the `x` challenge query + peel_sim_map hb with ⟨⟨c, sc⟩, hc, hbeq⟩ + peel_sim_bind hc with ⟨⟨d, sd⟩, hd, hc2⟩ + peel_sim_map hc2 with ⟨⟨xval, sx⟩, hx, hc2eq⟩ + -- round 0 is deterministic (a pure `honestMultiplicity` send) + peel_sim_map hd with ⟨⟨e, se⟩, he, hdeq⟩ + erw [simulateQ_pure, StateT.run_pure] at he + rw [support_pure, Set.mem_singleton_iff] at he + obtain ⟨rfl, rfl⟩ := Prod.mk.inj he + -- substitute the prover-side equation chain to make `pval`/`pres` concrete + obtain ⟨rfl, rfl⟩ := Prod.mk.inj hdeq + obtain ⟨rfl, rfl⟩ := Prod.mk.inj hc2eq + obtain ⟨rfl, rfl⟩ := Prod.mk.inj hbeq + obtain ⟨rfl, rfl⟩ := Prod.mk.inj ha3eq + obtain ⟨rfl, rfl⟩ := Prod.mk.inj hpval_eq + obtain ⟨rfl, rfl⟩ := Prod.mk.inj hpeq + change F at xval + change BatchingChallenge F n params.numGroups at zlam + -- peel the verifier (match on `some pval` resolves; then its bind) + simp only at hver + erw [simulateQ_bind, StateT.run_bind] at hver + rw [mem_support_bind_iff] at hver + obtain ⟨⟨vstmt, sv⟩, hverify, hvout⟩ := hver + -- The scan-free verifier packages the sampled challenges; the non-pole assumption comes from + -- the good-challenge event above. + simp only [OracleVerifier.toVerifier] at hverify + rw [outerVerify_simulateQ_eq] at hverify + -- The verifier accepted: `vstmt = some _` (the `none` branch of `hvout` yields `none ≠ some`). + rcases vstmt with _ | vAccepted + · simp only [simulateQ_pure, StateT.run_pure, support_pure, Set.mem_singleton_iff] at hvout + simp at hvout + · rcases vAccepted with _ | vAccepted + · simp only [OStmtAfterOuter, OStmtIn, MultiplicityMessage, HelperMessages, + Nat.reduceAdd, Fin.vcons_fin_zero, BatchingChallenge] at hvout + have hvoutBase := support_simulateQ_run_fst_subset + (impl + QueryImpl.liftTarget (StateT σ ProbComp) + (ProtocolSpec.challengeQueryImpl (pSpec := outerPSpec F n params))) hvout + letI : + (i : (outerPSpec F n params).ChallengeIdx) → + OracleInterface ((outerPSpec F n params).Challenge i) := + ProtocolSpec.challengeOracleInterface + letI : LawfulMonad (OracleComp (oSpec + [(outerPSpec F n params).Challenge]ₒ)) := + OracleComp.instLawfulMonad _ + change some out ∈ support + ((_ <$> + (failure : + OptionT (OracleComp (oSpec + [(outerPSpec F n params).Challenge]ₒ)) _)).run) + at hvoutBase + rw [OptionT.run_map, OptionT.run_failure] at hvoutBase + rw [support_map, support_pure, Set.mem_image] at hvoutBase + obtain ⟨a, ha, hmap⟩ := hvoutBase + rw [Set.mem_singleton_iff] at ha + subst a + simp at hmap + · -- The honest output: `out` pairs the prover view with the verifier's accepted statement. + rw [show (some (some vAccepted), sv).1 = some (some vAccepted) by rfl] at hvout + simp only [Option.getM_some, map_pure] at hvout + obtain ⟨rfl, rfl⟩ := hvout + simp only [OStmtAfterOuter, OStmtIn, MultiplicityMessage, HelperMessages] at hverify + have hverifyBase := support_simulateQ_run_fst_subset + (impl + QueryImpl.liftTarget (StateT σ ProbComp) + (ProtocolSpec.challengeQueryImpl (pSpec := outerPSpec F n params))) hverify + letI : + (i : (outerPSpec F n params).ChallengeIdx) → + OracleInterface ((outerPSpec F n params).Challenge i) := + ProtocolSpec.challengeOracleInterface + letI : LawfulMonad (OracleComp (oSpec + [(outerPSpec F n params).Challenge]ₒ)) := + OracleComp.instLawfulMonad _ + have hverifyEq := support_pure_eq + (m := OracleComp (oSpec + [(outerPSpec F n params).Challenge]ₒ)) hverifyBase + simp only [Option.some.injEq] at hverifyEq + subst vAccepted + have hNoTablePoles : + ∀ u : (Fin n → Fin 2), + xval + MvPolynomial.toEvalsZeroOne (oStmt .table).1 u ≠ 0 := by + intro u + simpa [outerVerifier, outerChallengeXIdx, outerChallengeBatchIdx, + ProtocolSpec.FullTranscript.challenges, ProtocolSpec.Transcript.concat, Fin.snoc] + using hGood u + have hcols : ∀ j : Fin M, ∀ u : (Fin n → Fin 2), ∃ v : (Fin n → Fin 2), + MvPolynomial.toEvalsZeroOne (oStmt (.column j)).1 u = + MvPolynomial.toEvalsZeroOne (oStmt .table).1 v := by + simpa [inputRelation] using hIn + have hchar : ∀ a : F, + lookupMultiplicityCount + (fun j => MvPolynomial.toEvalsZeroOne (oStmt (.column j)).1) a ≠ 0 → + (tableMultiplicityCount (MvPolynomial.toEvalsZeroOne (oStmt .table).1) a : F) ≠ 0 := + fun _ hlookup => + tableMultiplicityCount_cast_ne_zero_of_lookupMultiplicityCount_ne_zero + stmt.charLarge (MvPolynomial.toEvalsZeroOne (oStmt .table).1) + (fun j => MvPolynomial.toEvalsZeroOne (oStmt (.column j)).1) hcols hlookup + have hpoles : ∀ (i : TermIdx M) (u : (Fin n → Fin 2)), + termPhi (MvPolynomial.toEvalsZeroOne (oStmt .table).1) + (fun j => MvPolynomial.toEvalsZeroOne (oStmt (.column j)).1) xval i u ≠ 0 := + termPhi_ne_zero_of_table_poles (MvPolynomial.toEvalsZeroOne (oStmt .table).1) + (fun j => MvPolynomial.toEvalsZeroOne (oStmt (.column j)).1) xval hcols + hNoTablePoles + let stmtAfter : StmtAfterOuter F n M params := + { xChallenge := xval, zChallenge := zlam.1, batchingScalars := zlam.2 } + let oStmtAfter : ∀ i, OStmtAfterOuter F n M params i := + fun + | .input i => oStmt i + | .multiplicity => honestMultiplicity oStmt + | .helpers => honestHelpers params oStmt xval + have hMultiplicity : + MvPolynomial.toEvalsZeroOne (honestMultiplicity oStmt).1 = + normalizedMultiplicityValue (MvPolynomial.toEvalsZeroOne (oStmt .table).1) + (fun i => MvPolynomial.toEvalsZeroOne (oStmt (.column i)).1) := by + change (MvPolynomial.MLEEquiv (R := F) (σ := Fin n)) (honestMultiplicity oStmt) = _ + simp [honestMultiplicity] + have hHelpers : + (fun k => MvPolynomial.toEvalsZeroOne (honestHelpers params oStmt xval k).1) = + fun k u => + helperValue params.group (MvPolynomial.toEvalsZeroOne (oStmt .table).1) + (fun i => MvPolynomial.toEvalsZeroOne (oStmt (.column i)).1) + (normalizedMultiplicityValue (MvPolynomial.toEvalsZeroOne (oStmt .table).1) + (fun i => MvPolynomial.toEvalsZeroOne (oStmt (.column i)).1)) + xval k u := by + funext k + change (MvPolynomial.MLEEquiv (R := F) (σ := Fin n)) + (honestHelpers params oStmt xval k) = _ + simp [honestHelpers, hMultiplicity] + have hmid : ((stmtAfter, oStmtAfter), ()) ∈ logupMidRelation F n M params := by + unfold logupMidRelation logupOuterSumcheckClaim + rw [← logupOuterClaim_zero + (groups := params.group) (hgroups := sum_protocolGroups (F := F) params) + (table := MvPolynomial.toEvalsZeroOne (oStmt .table).1) + (columns := fun j => MvPolynomial.toEvalsZeroOne (oStmt (.column j)).1) + (xChallenge := xval) (zChallenge := zlam.1) (batchingScalars := zlam.2) + hchar hpoles] + apply Finset.sum_congr rfl + intro u _ + rw [logupQPolynomial_eval_hypercube] + simp [stmtAfter, oStmtAfter, hMultiplicity, hHelpers] + simp? [outerVerifier, outerChallengeXIdx, outerChallengeBatchIdx, + ProtocolSpec.FullTranscript.challenges, ProtocolSpec.FullTranscript.messages, + ProtocolSpec.Transcript.concat, Fin.snoc] + constructor + · convert hmid using 2 + apply Prod.ext + · rfl + · funext i + cases i <;> simp [oStmtAfter, outerMultiplicityMessageIdx, + outerHelpersMessageIdx] + · funext i + cases i <;> simp [outerMultiplicityMessageIdx, + outerHelpersMessageIdx] + · -- pole-probability bound `Pr[x avoids all table poles] ≥ 1 - |H|/|F|` + refine le_trans (uniform_avoids_table_poles_prob (F := F) (n := n) (M := M) oStmt) ?_ + rw [OptionT.mk_bind] + apply le_probEvent_bind_of_forall_le + · simp + · intro s hs + clear hs + simp only [OptionT.run_mk, OptionT.run_bind, OptionT.run_lift, Option.elimM, + map_eq_bind_pure_comp, bind_assoc, pure_bind, bind_pure_comp, simulateQ_bind, + StateT.run'_eq, StateT.run_bind, Function.comp_apply] + erw [simulateQ_bind] + erw [simulateQ_bind] + erw [simulateQ_bind] + erw [simulateQ_bind] + erw [simulateQ_pure] + simp only [pure_bind] + erw [simulateQ_pure] + simp only [pure_bind] + erw [simulateQ_bind] + rw [QueryImpl.simulateQ_add_liftComp_right, simulateQ_liftTarget] + erw [simulateQ_query] + simp only [OracleSpec.query_def, OracleQuery.input_apply, ProtocolSpec.challengeQueryImpl, + OracleQuery.cont_apply, outerPSpec] + simp + · simpa [probEvent_uniformSample] using + (mul_le_probEvent_bind + (mx := (liftM ($ᵗ F : ProbComp F) : OptionT ProbComp F)) + (p := fun x : F => ∀ u : (Fin n → Fin 2), + x + MvPolynomial.toEvalsZeroOne (oStmt .table).1 u ≠ 0) + (r := Pr[fun x : F => ∀ u : (Fin n → Fin 2), + x + MvPolynomial.toEvalsZeroOne (oStmt .table).1 u ≠ 0 | $ᵗ F]) + (r' := 1) (by simp) (by + intro x hx hGood + erw [simulateQ_pure] + simp only [StateT.run_pure, liftM_pure, pure_bind] + erw [simulateQ_pure] + simp only [StateT.run_pure, liftM_pure, pure_bind] + rw [one_le_probEvent_iff, probEvent_eq_one_iff] + constructor + · rw [probFailure_bind_eq_zero_iff] + constructor + · simp [OptionT.probFailure_liftM] + · intro batchState hbatch + rw [probFailure_bind_eq_zero_iff] + constructor + · simp [OptionT.probFailure_liftM] + · intro verifiedState hverified + have hSome : ∃ accepted, verifiedState.1 = some accepted := by + cases hfirst : verifiedState.1 with + | none => + exfalso + have hv := hverified + rw [OptionT.support_liftM] at hv + simp only [OracleVerifier.toVerifier] at hv + erw [outerVerify_simulateQ_eq] at hv + erw [simulateQ_bind, StateT.run_bind] at hv + rw [mem_support_bind_iff] at hv + obtain ⟨⟨ver, sver⟩, hverPure, hverRest⟩ := hv + erw [simulateQ_pure, StateT.run_pure] at hverPure + rw [support_pure, Set.mem_singleton_iff] at hverPure + obtain ⟨rfl, rfl⟩ := Prod.mk.inj hverPure + erw [simulateQ_pure, StateT.run_pure] at hverRest + rw [support_pure, Set.mem_singleton_iff] at hverRest + cases hverRest + simp at hfirst + | some accepted => + exact ⟨accepted, rfl⟩ + rcases hSome with ⟨accepted, haccepted⟩ + rw [OptionT.probFailure_eq, OptionT.run_mk, haccepted] + simp + · intro out hout + rw [mem_support_bind_iff] at hout + obtain ⟨batchState, hbatch, hout⟩ := hout + rw [OptionT.support_liftM] at hbatch + erw [simulateQ_bind, StateT.run_bind] at hbatch + rw [mem_support_bind_iff] at hbatch + obtain ⟨⟨batch, sbatch⟩, hbatchSample, hbatchPure⟩ := hbatch + erw [simulateQ_pure, StateT.run_pure] at hbatchPure + rw [support_pure, Set.mem_singleton_iff] at hbatchPure + subst batchState + rw [mem_support_bind_iff] at hout + obtain ⟨verifiedState, hverified, hout⟩ := hout + rw [OptionT.mem_support_iff] at hout + simp only [OptionT.run_mk, support_pure, Set.mem_singleton_iff] at hout + have hverified' := hverified + rw [OptionT.support_liftM] at hverified' + simp only [OracleVerifier.toVerifier] at hverified' + erw [outerVerify_simulateQ_eq] at hverified' + simp [outerChallengeXIdx, outerChallengeBatchIdx, + ProtocolSpec.FullTranscript.challenges, ProtocolSpec.Transcript.concat, + Fin.snoc] at hverified' + erw [simulateQ_bind, StateT.run_bind] at hverified' + rw [mem_support_bind_iff] at hverified' + obtain ⟨⟨verOpt, sver⟩, hverOpt, hverified''⟩ := hverified' + erw [simulateQ_pure, StateT.run_pure] at hverOpt + rw [support_pure, Set.mem_singleton_iff] at hverOpt + obtain ⟨rfl, rfl⟩ := Prod.mk.inj hverOpt + erw [simulateQ_pure, StateT.run_pure] at hverified'' + rw [support_pure, Set.mem_singleton_iff] at hverified'' + subst verifiedState + cases hout + exact hGood)) + +/-- Lens-completeness for the LogUp→Sumcheck lens: `proj` builds the zero-sum instance, and `lift` +retains the outer LogUp data together with sumcheck's final valid point claim. -/ +instance logupSumcheckLensComplete : + (logupSumcheckContextLens F n M params).toContext.IsComplete + (logupMidRelation F n M params) + (Sumcheck.Spec.relationRound F n (logupSumcheckDegree M params) (booleanDomain F) 0) + (logupAfterSumcheckRelation F n M params) + (Sumcheck.Spec.relationRound F n (logupSumcheckDegree M params) (booleanDomain F) + (Fin.last n)) + ((logupConcreteSumcheckOracleReduction oSpec F n M params).toReduction.compatContext + (logupSumcheckContextLens F n M params).toContext) where + proj_complete := by + rintro ⟨stmt, oStmt⟩ ⟨⟩ h + exact logupSumcheckRelationInput_of_zero F n M params h + lift_complete := by + intro outerStmt outerWit innerStmtOut innerWitOut hCompat _ hRelOut + have hOStmt : + innerStmtOut.2 = logupSumcheckOracleStmt F n M params outerStmt.1 outerStmt.2 := by + simp only [Reduction.compatContext, Function.comp_apply, ProtocolSpec.ChallengeIdx, + ProtocolSpec.Challenge, OStmtAfterOuter, OStmtIn, MultiplicityMessage, HelperMessages, + Set.mem_image, OptionT.mem_support_iff, Prod.exists, exists_and_right, + exists_eq_right] at hCompat + rcases hCompat with ⟨td, vOut, verOStmt, hRun⟩ + have hProver := reduction_run_prover_mem + ((logupConcreteSumcheckOracleReduction oSpec F n M params).toReduction) + ((logupSumcheckContextLens F n M params).toContext.proj (outerStmt, outerWit)).1 + ((logupSumcheckContextLens F n M params).toContext.proj (outerStmt, outerWit)).2 + td innerStmtOut innerWitOut (vOut, verOStmt) hRun + have hPres := sumcheckProver_preserves_oracleStmt (booleanDomain F) oSpec n + ((logupSumcheckContextLens F n M params).toContext.proj (outerStmt, outerWit)).1 + innerStmtOut td hProver + simpa [logupSumcheckContextLens] using hPres + cases innerWitOut + have hPair : + (innerStmtOut.1, logupSumcheckOracleStmt F n M params outerStmt.1 outerStmt.2) = + innerStmtOut := by + cases innerStmtOut + simpa using hOStmt.symm + simpa [logupSumcheckContextLens, logupAfterSumcheckRelation, hPair] using hRelOut + +omit [Fintype F] in +/-- Completeness of the embedded sumcheck phase: it carries `logupMidRelation` to the retained +final sumcheck claim with no extra error, by reusing the generic sumcheck's perfect completeness +through the LogUp-to-Sumcheck context lens. -/ +theorem logupSumcheckPhaseCompleteness : + (sumcheckOracleReduction oSpec F n M params).completeness init impl + (logupMidRelation F n M params) (logupAfterSumcheckRelation F n M params) 0 := + OracleReduction.liftContext_perfectCompleteness + (lens := logupSumcheckContextLens F n M params) + (lensComplete := logupSumcheckLensComplete oSpec F n M params) + (Sumcheck.Spec.oracleReduction_perfectCompleteness + F (logupSumcheckDegree M params) (booleanDomain F) n oSpec) + + +omit [Fintype F] [SampleableType F] in +/-- Completeness of the final LogUp point check: once sumcheck's final claim is valid for the +retained LogUp polynomial, the verifier's oracle queries reconstruct the same value. -/ +theorem finalCheckCompleteness : + (finalCheckOracleReduction oSpec F n M params).completeness init impl + (logupAfterSumcheckRelation F n M params) outputRelation 0 := by + unfold OracleReduction.completeness Reduction.completeness + rintro ⟨stmt, oStmt⟩ ⟨⟩ hRel + have hExpected : + MvPolynomial.eval stmt.finalClaim.challenges + (logupQPolynomial (params.group) (oStmt (.input .table)).1 + (fun i => (oStmt (.input (.column i))).1) (oStmt .multiplicity).1 + (fun k => (oStmt .helpers k).1) stmt.outer.xChallenge stmt.outer.zChallenge + stmt.outer.batchingScalars) = + stmt.finalClaim.target := by + unfold logupAfterSumcheckRelation Sumcheck.Spec.relationRound at hRel + simp only [Set.mem_setOf_eq, logupSumcheckOracleStmt, logupSumcheckPolynomial] at hRel + have tailSize_zero : n - (Fin.last n : Fin (n + 1)) = 0 := by simp + let tail0 : Fin (n - (Fin.last n : Fin (n + 1))) → F := + fun i => Fin.elim0 (Fin.cast (by simp) i) + have hfinalPoint : + Fin.append stmt.finalClaim.challenges tail0 ∘ + Fin.cast (Sumcheck.Spec.relationRound._proof_1 n (Fin.last n)) = + stmt.finalClaim.challenges := by + funext i + change Fin.append stmt.finalClaim.challenges tail0 + (Fin.cast (Sumcheck.Spec.relationRound._proof_1 n (Fin.last n)) i) = + stmt.finalClaim.challenges i + rw [Fin.append_right_nil stmt.finalClaim.challenges tail0 tailSize_zero] + congr 1 + have hsum : + (∑ x ∈ Fintype.piFinset fun _ : Fin (n - (Fin.last n : Fin (n + 1))) => + Finset.univ.map (booleanDomain F), + MvPolynomial.eval + (Fin.append stmt.finalClaim.challenges x ∘ + Fin.cast (Sumcheck.Spec.relationRound._proof_1 n (Fin.last n))) + (logupQPolynomial (params.group) (oStmt (.input .table)).1 + (fun i => (oStmt (.input (.column i))).1) (oStmt .multiplicity).1 + (fun k => (oStmt .helpers k).1) stmt.outer.xChallenge stmt.outer.zChallenge + stmt.outer.batchingScalars)) = + MvPolynomial.eval stmt.finalClaim.challenges + (logupQPolynomial (params.group) (oStmt (.input .table)).1 + (fun i => (oStmt (.input (.column i))).1) (oStmt .multiplicity).1 + (fun k => (oStmt .helpers k).1) stmt.outer.xChallenge stmt.outer.zChallenge + stmt.outer.batchingScalars) := by + rw [Finset.sum_eq_single tail0] + · rw [hfinalPoint] + rfl + · intro b _ hb + exact False.elim (hb (funext fun i => Fin.elim0 (Fin.cast (by simp) i))) + · intro hnot + exact False.elim (hnot (by + rw [Fintype.mem_piFinset] + intro i + exact Fin.elim0 (Fin.cast tailSize_zero i))) + exact hsum ▸ hRel + have hGuard : + qAtPoint (params.group) stmt.outer.xChallenge stmt.outer.zChallenge + stmt.finalClaim.challenges stmt.outer.batchingScalars + (MvPolynomial.eval stmt.finalClaim.challenges (oStmt .multiplicity).1) + (MvPolynomial.eval stmt.finalClaim.challenges (oStmt (.input .table)).1) + (fun i => MvPolynomial.eval stmt.finalClaim.challenges (oStmt (.input (.column i))).1) + (fun k => MvPolynomial.eval stmt.finalClaim.challenges (oStmt .helpers k).1) = + stmt.finalClaim.target := by + rw [← hExpected] + exact (logupQPolynomial_eval_point (params.group) (oStmt (.input .table)).1 + (fun i => (oStmt (.input (.column i))).1) (oStmt .multiplicity).1 + (fun k => (oStmt .helpers k).1) stmt.outer.xChallenge stmt.outer.zChallenge + stmt.finalClaim.challenges stmt.outer.batchingScalars).symm + let qImpl : + QueryImpl + (oSpec + ([OStmtAfterOuter F n M params]ₒ + [finalCheckPSpec.Message]ₒ)) + (OracleComp oSpec) := + OracleInterface.simOracle2 (T₁ := OStmtAfterOuter F n M params) + (T₂ := finalCheckPSpec.Message) oSpec oStmt + (fun i : finalCheckPSpec.MessageIdx => Fin.elim0 i) + have hquery : + ∀ (i : OuterOracleIdx M) + (q : (instOStmtAfterOuterOracleInterface (F := F) (n := n) (params := params) i).Query), + simulateQ qImpl ((finalCheckQuery oSpec F n M params i q).run) = + (pure (some ((instOStmtAfterOuterOracleInterface + (F := F) (n := n) (params := params) i).answer (oStmt i) q)) : + OracleComp oSpec _) := by + intro i q + simp only [finalCheckQuery, OptionT.run_mk, simulateQ_map, qImpl, + OracleInterface.simOracle2, QueryImpl.addLift_def, simulateQ_query, + QueryImpl.add_apply_inr, QueryImpl.liftTarget_apply, QueryImpl.add, + OracleInterface.simOracle0, OracleInterface.answer, OracleQuery.cont_query, + OracleQuery.input_query] + change some <$> id <$> + (pure (ReaderT.run (OracleInterface.toOC.impl q) (oStmt i)) : + OracleComp oSpec _) = + (pure (some (ReaderT.run (OracleInterface.toOC.impl q) (oStmt i))) : + OracleComp oSpec _) + simp + have hVerify : + simulateQ qImpl + ((finalCheckVerifier oSpec F n M params).verify stmt (fun i => Fin.elim0 i)).run = + (pure (some ()) : OracleComp oSpec (Option StmtOut)) := by + simp only [finalCheckVerifier, OptionT.run_bind, OptionT.run_pure] + erw [simulateQ_bind] + rw [hquery .multiplicity stmt.finalClaim.challenges] + simp only [pure_bind, Option.elim_some] + erw [simulateQ_bind] + rw [hquery (.input .table) stmt.finalClaim.challenges] + simp only [pure_bind, Option.elim_some] + let colValue := fun i : Fin M => + MvPolynomial.eval stmt.finalClaim.challenges (oStmt (.input (.column i))).1 + have hcols := simulateQ_optionT_mapM_pure qImpl + (fun i : Fin M => + finalCheckQuery oSpec F n M params (.input (.column i)) stmt.finalClaim.challenges) + colValue (Vector.finRange M) (by + intro i + simpa [colValue, OracleInterface.answer] using + hquery (.input (.column i)) stmt.finalClaim.challenges) + erw [simulateQ_option_elimM] + erw [hcols] + simp only [pure_bind, Option.elimM, Option.elim_some] + let helperValue := fun k : Fin params.numGroups => + MvPolynomial.eval stmt.finalClaim.challenges (oStmt .helpers k).1 + have hhelpers := simulateQ_optionT_mapM_pure qImpl + (fun k : Fin params.numGroups => + finalCheckQuery oSpec F n M params .helpers ⟨k, stmt.finalClaim.challenges⟩) + helperValue (Vector.finRange params.numGroups) (by + intro k + simpa [helperValue, OracleInterface.answer] using + hquery .helpers ⟨k, stmt.finalClaim.challenges⟩) + erw [simulateQ_option_elimM] + erw [hhelpers] + simp only [pure_bind, Option.elimM, Option.elim_some] + have hGuard' : + qAtPoint (params.group) stmt.outer.xChallenge stmt.outer.zChallenge + stmt.finalClaim.challenges stmt.outer.batchingScalars + (OracleInterface.answer (oStmt .multiplicity) stmt.finalClaim.challenges) + (OracleInterface.answer (oStmt (.input .table)) stmt.finalClaim.challenges) + colValue + helperValue = + stmt.finalClaim.target := by + simpa [OracleInterface.answer, colValue, helperValue] using hGuard + erw [simulateQ_option_elimM] + simp [guard, hGuard', OptionT.run_pure, Option.elimM] + have hVerifyDefault : + simulateQ + (OracleInterface.simOracle2 oSpec oStmt + (ProtocolSpec.FullTranscript.messages (default : finalCheckPSpec.FullTranscript))) + (((finalCheckVerifier oSpec F n M params).verify stmt + (ProtocolSpec.FullTranscript.challenges + (default : finalCheckPSpec.FullTranscript))).run) = + (pure (some ()) : OracleComp oSpec (Option StmtOut)) := by + simpa [qImpl, finalCheckPSpec] using hVerify + have hVerifyDefaultT : + OptionT.run + (simulateQ + (OracleInterface.simOracle2 oSpec oStmt + (ProtocolSpec.FullTranscript.messages (default : finalCheckPSpec.FullTranscript))) + ((finalCheckVerifier oSpec F n M params).verify stmt + (ProtocolSpec.FullTranscript.challenges + (default : finalCheckPSpec.FullTranscript)))) = + (pure (some ()) : OracleComp oSpec (Option StmtOut)) := by + simpa [OptionT.run] using hVerifyDefault + have hVerifyDefaultT' : + OptionT.run + (simulateQ + (OracleInterface.simOracle2 oSpec oStmt + (ProtocolSpec.FullTranscript.messages default)) + ((finalCheckVerifier oSpec F n M params).verify stmt + (ProtocolSpec.FullTranscript.challenges default))) = + (pure (some ()) : OracleComp oSpec (Option StmtOut)) := by + simpa [finalCheckPSpec] using hVerifyDefaultT + have hrun : + (finalCheckOracleReduction oSpec F n M params).toReduction.run (stmt, oStmt) () = + (pure ((default, ((), fun i => Fin.elim0 i), ()), ((), fun i => Fin.elim0 i)) : + OptionT (OracleComp _) _) := by + simp [finalCheckOracleReduction, OracleReduction.toReduction, Reduction.run, + finalCheckProver, Prover.run, Verifier.run, Prover.runToRound, + finalCheckPSpec, OracleVerifier.toVerifier] + erw [hVerifyDefaultT'] + simp + congr + funext i + exact Fin.elim0 i + simp only [ENNReal.coe_zero, tsub_zero] + rw [hrun] + rw [ge_iff_le, one_le_probEvent_iff, probEvent_eq_one_iff] + refine ⟨?_, ?_⟩ + · rw [OptionT.probFailure_eq, OptionT.run_mk] + simp only [probFailure_eq_zero, zero_add] + apply probOutput_eq_zero_of_not_mem_support + simp only [support_bind, Set.mem_iUnion, not_exists] + intro s _ hmem + change none ∈ _root_.support + (StateT.run' (simulateQ _ + (pure (some + ((default, ((), fun i => Fin.elim0 i), ()), ((), fun i => Fin.elim0 i))) : + OracleComp _ _)) s) at hmem + rw [simulateQ_pure] at hmem + change none ∈ _root_.support + (Prod.fst <$> (pure (some + ((default, ((), fun i => Fin.elim0 i), ()), ((), fun i => Fin.elim0 i))) : + StateT σ ProbComp _).run s) at hmem + rw [StateT.run_pure] at hmem + simp [map_pure] at hmem + · intro out hout + rw [OptionT.mem_support_iff] at hout + simp only [OptionT.run_mk, support_bind, Set.mem_iUnion] at hout + obtain ⟨s, -, hout⟩ := hout + change some out ∈ _root_.support + (StateT.run' (simulateQ _ + (pure (some + ((default, ((), fun i => Fin.elim0 i), ()), ((), fun i => Fin.elim0 i))) : + OracleComp _ _)) s) at hout + rw [simulateQ_pure] at hout + change some out ∈ _root_.support + (Prod.fst <$> (pure (some + ((default, ((), fun i => Fin.elim0 i), ()), ((), fun i => Fin.elim0 i))) : + StateT σ ProbComp _).run s) at hout + rw [StateT.run_pure] at hout + simp [map_pure, support_pure] at hout + cases hout + exact ⟨Set.mem_univ _, rfl⟩ /-- Main ArkLib completeness theorem for LogUp Protocol 2. -/ theorem logup_completeness : (logupOracleReduction oSpec F n M params).completeness init impl (inputRelation F n M) outputRelation (logupCompletenessError F n) := by - sorry + letI : Inhabited F := ⟨0⟩ + have hOuterSumcheck := OracleReduction.append_completeness.{0, 0, 0, 0} + (outerOracleReduction oSpec F n M params) + (sumcheckOracleReduction oSpec F n M params) + (logup_outer_completeness oSpec F n M params init impl) + (logupSumcheckPhaseCompleteness oSpec F n M params init impl) + have hFull := OracleReduction.append_completeness.{0, 0, 0, 0} + ((outerOracleReduction oSpec F n M params).append + (sumcheckOracleReduction oSpec F n M params)) + (finalCheckOracleReduction oSpec F n M params) + hOuterSumcheck + (finalCheckCompleteness oSpec F n M params init impl) + simpa only [add_zero] using hFull end Completeness diff --git a/ArkLib/ProofSystem/Logup/Security/Soundness.lean b/ArkLib/ProofSystem/Logup/Security/Soundness.lean index 2c13f9e5dc..0193010dd8 100644 --- a/ArkLib/ProofSystem/Logup/Security/Soundness.lean +++ b/ArkLib/ProofSystem/Logup/Security/Soundness.lean @@ -4,7 +4,8 @@ import ArkLib.ProofSystem.Logup.Protocol /-! # LogUp Soundness -Main soundness statement for Protocol 2 of `paper.txt`. +Soundness target for Protocol 2 of Haböck's LogUp lookup argument (Cryptology ePrint Archive, +Paper 2022/1530, ). -/ open scoped NNReal @@ -14,22 +15,30 @@ namespace Logup section Soundness variable {ι : Type} (oSpec : OracleSpec ι) -variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [Fact ((-1 : F) ≠ 1)] - [SampleableType F] +variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [SampleableType F] variable (n M : ℕ) variable (params : ProtocolParams M) variable {σ : Type} (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp)) -/-- Paper-shaped soundness error for the LogUp outer checks plus the embedded sumcheck error. -/ +/-- Paper-shaped soundness error for the LogUp outer checks plus the embedded sumcheck error. + +The first term divides by `|F| - |H|`, the number of non-pole field elements a good challenge can +be sampled from. This expression is only meaningful when `|H| < |F|` (see `logup_soundness`); +otherwise the natural-number subtraction truncates to `0` and the term silently vanishes. -/ noncomputable def logupSoundnessError (F : Type) [Fintype F] (n M : ℕ) (params : ProtocolParams M) (sumcheckSoundnessError : ℝ≥0) : ℝ≥0 := - ((((M + 1) * Fintype.card (Hypercube n) - 1 : ℕ) : ℝ≥0) / - ((Fintype.card F - Fintype.card (Hypercube n) : ℕ) : ℝ≥0)) + + ((((M + 1) * Fintype.card (Fin n → Fin 2) - 1 : ℕ) : ℝ≥0) / + ((Fintype.card F - Fintype.card (Fin n → Fin 2) : ℕ) : ℝ≥0)) + (((params.numGroups + 1 : ℕ) : ℝ≥0) / (Fintype.card F : ℝ≥0)) + sumcheckSoundnessError -/-- Main ArkLib soundness theorem for LogUp Protocol 2. -/ -theorem logup_soundness (sumcheckSoundnessError : ℝ≥0) : +/-- Main ArkLib soundness theorem for LogUp Protocol 2. + +The hypothesis `hcard : |H| < |F|` guarantees there exist non-pole field elements to sample a +challenge from, and makes the `|F| - |H|` denominator of `logupSoundnessError` positive (so the +natural-number subtraction equals the true difference rather than truncating to `0`). -/ +theorem logup_soundness (sumcheckSoundnessError : ℝ≥0) + (hcard : Fintype.card (Fin n → Fin 2) < Fintype.card F) : (logupVerifier oSpec F n M params).soundness init impl (inputRelation F n M).language outputRelation.language (logupSoundnessError F n M params sumcheckSoundnessError) := by diff --git a/ArkLib/ProofSystem/Logup/Sumcheck/SumcheckBridge.lean b/ArkLib/ProofSystem/Logup/Sumcheck/SumcheckBridge.lean deleted file mode 100644 index 1d7638b86a..0000000000 --- a/ArkLib/ProofSystem/Logup/Sumcheck/SumcheckBridge.lean +++ /dev/null @@ -1,278 +0,0 @@ -import ArkLib.ProofSystem.Logup.Sumcheck.SumcheckPolynomial -import ArkLib.ProofSystem.Sumcheck.Spec.General - -/-! -# LogUp Sumcheck Bridge - -Packages `logupQPolynomial` from `SumcheckPolynomial.lean` into ArkLib's Sumcheck interface -types, then connects it to the generic Sumcheck relation, verifier, reduction, and context lift. --/ - -namespace Logup - -open scoped BigOperators - -section SumcheckInterface - -variable (F : Type) [Field F] [Fintype F] [DecidableEq F] (n M : ℕ) -variable (params : ProtocolParams M) - -/-- Individual-degree bound for LogUp's embedded sumcheck polynomial. -/ -def logupSumcheckDegree (_params : ProtocolParams M) : ℕ := - M + 3 - -/-- The concrete ArkLib Sumcheck transcript shape for LogUp's embedded sumcheck. -/ -abbrev logupSumcheckPSpec : ProtocolSpec (Fin.vsum (fun _ : Fin n => 2)) := - Sumcheck.Spec.pSpec F (logupSumcheckDegree M params) n - -/-- The generic sumcheck input statement used by LogUp: target `0`, no prior challenges. -/ -abbrev LogupSumcheckStmtIn (_params : ProtocolParams M) : Type := - Sumcheck.Spec.StatementRound F n 0 - -/-- The generic sumcheck output statement: the final claim at verifier point `r`. -/ -abbrev LogupSumcheckStmtOut (_params : ProtocolParams M) : Type := - Sumcheck.Spec.StatementRound F n (.last n) - -/-- The generic sumcheck oracle statement: LogUp's bounded-degree `Q` polynomial. -/ -abbrev LogupSumcheckOracleStatement : Unit → Type := - Sumcheck.Spec.OracleStatement F n (logupSumcheckDegree M params) - -/-- LogUp enters the embedded sumcheck with the zero-sum claim. -/ -def logupInitialSumcheckStatement : LogupSumcheckStmtIn F n M params where - target := 0 - challenges := fun i => Fin.elim0 i - -/-- Package `logupQPolynomial` with its degree certificate into ArkLib's oracle statement type. -/ -noncomputable def logupSumcheckPolynomial - (stmt : StmtAfterOuter F n M params) - (oStmt : ∀ i, OStmtAfterOuter F n M params i) : - LogupSumcheckOracleStatement F n M params () := by - classical - exact ⟨logupQPolynomial F n M params stmt oStmt, by - rw [MvPolynomial.mem_restrictDegree_iff_degreeOf_le] - intro i - exact logupQPolynomial_degreeOf F n M params stmt oStmt i⟩ - -/-- Package the LogUp `Q` polynomial as the single oracle statement expected by Sumcheck. -/ -noncomputable def logupSumcheckOracleStmt - (stmt : StmtAfterOuter F n M params) - (oStmt : ∀ i, OStmtAfterOuter F n M params i) : - ∀ i, LogupSumcheckOracleStatement F n M params i := - fun _ => logupSumcheckPolynomial F n M params stmt oStmt - -/-- The row-wise claim that `logupQPolynomial` agrees with `qOnHypercube` on `H`. -/ -def logupSumcheckPolynomialRowsAgree - (stmt : StmtAfterOuter F n M params) - (oStmt : ∀ i, OStmtAfterOuter F n M params i) : Prop := - ∀ u : Hypercube n, - MvPolynomial.eval (signPoint F u) (logupSumcheckPolynomial F n M params stmt oStmt).1 = - qOnHypercube (canonicalGroups params) (fun i => oStmt (.input i)) (oStmt .multiplicity) - (oStmt .helpers) stmt.xChallenge stmt.zChallenge stmt.batchingScalars u - -/-- The LogUp zero-sum claim that is fed to the generic sumcheck. -/ -noncomputable def logupOuterSumcheckClaim - (stmt : StmtAfterOuter F n M params) - (oStmt : ∀ i, OStmtAfterOuter F n M params i) : F := - ∑ u : Hypercube n, - qOnHypercube (canonicalGroups params) (fun i => oStmt (.input i)) (oStmt .multiplicity) - (oStmt .helpers) stmt.xChallenge stmt.zChallenge stmt.batchingScalars u - -/-- Semantic agreement between final oracle-query answers and the retained LogUp oracles. -/ -def logupPointEvaluationsAgree - (r : Fin n → F) - (oStmt : ∀ i, OStmtAfterOuter F n M params i) - (evals : PointEvaluations F M params.numGroups) : Prop := - evals.multiplicity = lagrangeOracleEval (oStmt .multiplicity) r ∧ - evals.table = lagrangeOracleEval (oStmt (.input .table)) r ∧ - (∀ i : Fin M, evals.columns i = lagrangeOracleEval (oStmt (.input (.column i))) r) ∧ - ∀ k : Fin params.numGroups, evals.helpers k = lagrangeOracleEval ((oStmt .helpers) k) r - -end SumcheckInterface - -section SumcheckBridge - -variable (F : Type) [Field F] (n M : ℕ) -variable (params : ProtocolParams M) - -/-- The `{±1}` sumcheck domain, packaged in the form expected by `Sumcheck.Spec`. -/ -def signDomain (hSigns : (-1 : F) ≠ 1) : Fin 2 ↪ F where - toFun := bitToSign F - inj' := by - intro a b h - fin_cases a <;> fin_cases b - · rfl - · exact absurd h hSigns - · exact absurd h.symm hSigns - · rfl - -private theorem sum_piFinset_map_univ_eq_sum_hypercube - (D : Fin 2 ↪ F) (f : (Fin n → F) → F) : - (∑ x ∈ Fintype.piFinset fun _ : Fin n => Finset.univ.map D, f x) = - ∑ u : Hypercube n, f (fun j => D (u j)) := by - classical - symm - refine Finset.sum_nbij (s := (Finset.univ : Finset (Hypercube n))) - (t := Fintype.piFinset fun _ : Fin n => Finset.univ.map D) - (i := fun u j => D (u j)) ?hi ?hinj ?hsurj ?hfg - · intro u _ - rw [Fintype.mem_piFinset] - intro j - exact Finset.mem_map.mpr ⟨u j, Finset.mem_univ _, rfl⟩ - · intro u _ v _ huv - funext j - exact D.injective (congr_fun huv j) - · intro x hx - have hx_coord : ∀ j : Fin n, ∃ b : Fin 2, D b = x j := by - intro j - have hxj := (Fintype.mem_piFinset.mp hx) j - rcases Finset.mem_map.mp hxj with ⟨b, _, hb⟩ - exact ⟨b, hb⟩ - let u : Hypercube n := fun j => Classical.choose (hx_coord j) - refine ⟨u, Finset.mem_univ _, ?_⟩ - funext j - exact Classical.choose_spec (hx_coord j) - · intro u _ - rfl - - -/-- The initial generic Sumcheck relation induced by a LogUp outer transcript. -/ -def logupSumcheckRelationInput (hSigns : (-1 : F) ≠ 1) - (stmt : StmtAfterOuter F n M params) - (oStmt : ∀ i, OStmtAfterOuter F n M params i) : Prop := - ((logupInitialSumcheckStatement F n M params, logupSumcheckOracleStmt F n M params stmt oStmt), - ()) ∈ - Sumcheck.Spec.relationRound F n (logupSumcheckDegree M params) (signDomain F hSigns) 0 - -/-- If the polynomial bridge agrees on the hypercube and LogUp's outer algebra proves a zero sum, -then the generic Sumcheck input relation is exactly the claim sent to Sumcheck. -/ -theorem logupSumcheckRelationInput_of_rowsAgree - {hSigns : (-1 : F) ≠ 1} - {stmt : StmtAfterOuter F n M params} - {oStmt : ∀ i, OStmtAfterOuter F n M params i} - (hRows : logupSumcheckPolynomialRowsAgree F n M params stmt oStmt) - (hZero : logupOuterSumcheckClaim F n M params stmt oStmt = 0) : - logupSumcheckRelationInput F n M params hSigns stmt oStmt := by - unfold logupSumcheckRelationInput Sumcheck.Spec.relationRound - simp only [Fin.coe_ofNat_eq_mod, Nat.zero_mod, Nat.sub_zero, logupInitialSumcheckStatement, - Set.mem_setOf_eq, Fin.elim0_append, logupSumcheckOracleStmt] - change - (∑ x ∈ Fintype.piFinset fun _ : Fin n => Finset.univ.map (signDomain F hSigns), - MvPolynomial.eval ((x ∘ Fin.cast (by omega)) ∘ Fin.cast (by omega)) - (logupSumcheckPolynomial F n M params stmt oStmt).val) = 0 - rw [sum_piFinset_map_univ_eq_sum_hypercube - (F := F) (n := n) (D := signDomain F hSigns) - (f := fun x => - MvPolynomial.eval ((x ∘ Fin.cast (by omega)) ∘ Fin.cast (by omega)) - (logupSumcheckPolynomial F n M params stmt oStmt).val)] - calc - (∑ u : Hypercube n, - MvPolynomial.eval - ((((fun j => (signDomain F hSigns) (u j)) ∘ Fin.cast (by omega)) ∘ - Fin.cast (by omega))) - (logupSumcheckPolynomial F n M params stmt oStmt).val) - = - logupOuterSumcheckClaim F n M params stmt oStmt := by - rw [logupOuterSumcheckClaim] - apply Finset.sum_congr rfl - intro u _ - simpa [signDomain, signPoint] using hRows u - _ = 0 := hZero - -/-- The obligations needed to replace the current abstract embedded sumcheck by ArkLib's generic -sumcheck plus LogUp's final oracle-query check. -/ -structure LogupSumcheckBridge - (stmt : StmtAfterOuter F n M params) - (oStmt : ∀ i, OStmtAfterOuter F n M params i) where - rowsAgree : logupSumcheckPolynomialRowsAgree F n M params stmt oStmt - claimZero : logupOuterSumcheckClaim F n M params stmt oStmt = 0 - finalEval : - ∀ (r : Fin n → F) (evals : PointEvaluations F M params.numGroups), - logupPointEvaluationsAgree F n M params r oStmt evals → - MvPolynomial.eval r (logupSumcheckPolynomial F n M params stmt oStmt).1 = - qAtPoint (canonicalGroups params) stmt.xChallenge stmt.zChallenge r - stmt.batchingScalars evals - - -end SumcheckBridge - -section ConcreteSumcheckReduction - -variable {ι : Type} (oSpec : OracleSpec ι) -variable (F : Type) [Field F] [Fintype F] [DecidableEq F] (n M : ℕ) -variable (params : ProtocolParams M) - -/-- The existing generic Sumcheck oracle verifier specialized to LogUp's domain and degree bound. -/ -noncomputable def logupConcreteSumcheckOracleVerifier [SampleableType F] - (hSigns : (-1 : F) ≠ 1) : - OracleVerifier oSpec (LogupSumcheckStmtIn F n M params) - (LogupSumcheckOracleStatement F n M params) - (LogupSumcheckStmtOut F n M params) - (LogupSumcheckOracleStatement F n M params) - (logupSumcheckPSpec F n M params) := - Sumcheck.Spec.oracleVerifier F (logupSumcheckDegree M params) - (signDomain F hSigns) n oSpec - -/-- The existing generic Sumcheck oracle reduction specialized to LogUp's domain and degree -bound. -/ -noncomputable def logupConcreteSumcheckOracleReduction [SampleableType F] - (hSigns : (-1 : F) ≠ 1) : - OracleReduction oSpec (LogupSumcheckStmtIn F n M params) - (LogupSumcheckOracleStatement F n M params) Unit - (LogupSumcheckStmtOut F n M params) - (LogupSumcheckOracleStatement F n M params) Unit - (logupSumcheckPSpec F n M params) := - Sumcheck.Spec.oracleReduction F (logupSumcheckDegree M params) - (signDomain F hSigns) n oSpec - -end ConcreteSumcheckReduction - -section SumcheckLift - -variable {ι : Type} (oSpec : OracleSpec ι) -variable (F : Type) [Field F] [Fintype F] [DecidableEq F] [Fact ((-1 : F) ≠ 1)] (n M : ℕ) -variable (params : ProtocolParams M) - -/-- Context lens from LogUp's retained outer state to ArkLib's generic Sumcheck state. - -The projection builds the generic zero-sum claim and its single polynomial oracle. The lift drops -the generic Sumcheck output because the top-level LogUp protocol returns only success/failure. --/ -noncomputable def logupSumcheckContextLens : - OracleContext.Lens - (StmtAfterOuter F n M params) StmtOut - (LogupSumcheckStmtIn F n M params) (LogupSumcheckStmtOut F n M params) - (OStmtAfterOuter F n M params) OStmtOut - (LogupSumcheckOracleStatement F n M params) - (LogupSumcheckOracleStatement F n M params) - Unit Unit Unit Unit where - stmt := - ⟨fun ctx => - (logupInitialSumcheckStatement F n M params, - logupSumcheckOracleStmt F n M params ctx.1 ctx.2), - fun _ _ => ((), fun i => Fin.elim0 i)⟩ - wit := - ⟨fun _ => (), - fun _ _ => ()⟩ - -/-- The embedded LogUp sumcheck phase, obtained by lifting ArkLib's generic Sumcheck reduction -through the LogUp-to-Sumcheck context lens. -/ -noncomputable def sumcheckOracleReduction [SampleableType F] : - OracleReduction oSpec (StmtAfterOuter F n M params) (OStmtAfterOuter F n M params) Unit - (StmtOut) (OStmtOut) Unit - (logupSumcheckPSpec F n M params) := - let lens : - OracleContext.Lens.{0, 0, 0, 0} - (StmtAfterOuter F n M params) StmtOut - (LogupSumcheckStmtIn F n M params) (LogupSumcheckStmtOut F n M params) - (OStmtAfterOuter F n M params) OStmtOut - (LogupSumcheckOracleStatement F n M params) - (LogupSumcheckOracleStatement F n M params) - Unit Unit Unit Unit := - logupSumcheckContextLens F n M params - (logupConcreteSumcheckOracleReduction oSpec F n M params - (Fact.out : (-1 : F) ≠ 1)).liftContext - lens - -end SumcheckLift - -end Logup diff --git a/ArkLib/ProofSystem/Logup/Sumcheck/SumcheckPolynomial.lean b/ArkLib/ProofSystem/Logup/Sumcheck/SumcheckPolynomial.lean deleted file mode 100644 index cd1d634616..0000000000 --- a/ArkLib/ProofSystem/Logup/Sumcheck/SumcheckPolynomial.lean +++ /dev/null @@ -1,416 +0,0 @@ -import ArkLib.Data.MvPolynomial.Degrees -import ArkLib.ProofSystem.Logup.Common - -/-! -# LogUp Sumcheck Polynomial - -Constructs `logupQPolynomial`, an `MvPolynomial (Fin n) F` whose restriction to the signed -hypercube agrees with `qOnHypercube` from `Common.lean`, and proves its individual degree is -at most `M + 3`. Depends only on `Common.lean` and Mathlib — no ArkLib Sumcheck types. --/ - -namespace Logup - -open scoped BigOperators - -section SumcheckPolynomial - -variable (F : Type) [Field F] (n M : ℕ) -variable (params : ProtocolParams M) - -/-- The `{±1}` Lagrange basis polynomial for one hypercube row. -/ -private noncomputable def signedBasisPolynomial (u : Hypercube n) : - MvPolynomial (Fin n) F := - MvPolynomial.C (((2 : F) ^ n)⁻¹) * - ∏ j : Fin n, (1 + MvPolynomial.C (bitToSign F (u j)) * MvPolynomial.X j) - -/-- Multilinear extension of a function on the signed hypercube `{±1}ⁿ`. -/ -private noncomputable def signedMLEPolynomial (values : Hypercube n → F) : - MvPolynomial (Fin n) F := - ∑ u : Hypercube n, MvPolynomial.C (values u) * signedBasisPolynomial F n u - -/-- The polynomial whose value at `r` is `L_H(r, z)`. -/ -private noncomputable def lagrangeKernelPolynomial (z : Fin n → F) : - MvPolynomial (Fin n) F := - MvPolynomial.C (((2 : F) ^ n)⁻¹) * - ∏ j : Fin n, (1 + MvPolynomial.C (z j) * MvPolynomial.X j) - -private theorem signedBasisPolynomial_eval (u : Hypercube n) (r : Fin n → F) : - MvPolynomial.eval r (signedBasisPolynomial F n u) = lagrangeKernel F u r := by - simp [signedBasisPolynomial, lagrangeKernel, lagrangeKernelAtPoint, signPoint] - -private theorem signedMLEPolynomial_eval (values : Hypercube n → F) (r : Fin n → F) : - MvPolynomial.eval r (signedMLEPolynomial F n values) = - ∑ u : Hypercube n, values u * lagrangeKernel F u r := by - simp [signedMLEPolynomial, signedBasisPolynomial_eval] - -private theorem lagrangeKernelPolynomial_eval (z r : Fin n → F) : - MvPolynomial.eval r (lagrangeKernelPolynomial F n z) = - lagrangeKernelAtPoint F r z := by - simp [lagrangeKernelPolynomial, lagrangeKernelAtPoint, mul_comm] - -private theorem signedLinearFactor_degreeOf (a : F) (i j : Fin n) : - MvPolynomial.degreeOf i (1 + MvPolynomial.C a * MvPolynomial.X j) ≤ - if i = j then 1 else 0 := by - by_cases hij : i = j - · subst i - simp only [↓reduceIte] - have hone : - MvPolynomial.degreeOf j (1 : MvPolynomial (Fin n) F) ≤ 1 := by - simp - have hmul : - MvPolynomial.degreeOf j (MvPolynomial.C a * MvPolynomial.X j) ≤ 1 := by - calc - _ ≤ MvPolynomial.degreeOf j (MvPolynomial.C a) + - MvPolynomial.degreeOf j (MvPolynomial.X j) := by - exact MvPolynomial.degreeOf_mul_le j _ _ - _ ≤ 0 + 1 := by - gcongr - · exact (MvPolynomial.degreeOf_C (R := F) a j).le - · exact MvPolynomial.degreeOf_X_le (R := F) j j - _ = 1 := by omega - exact (MvPolynomial.degreeOf_add_le j _ _).trans (max_le hone hmul) - · simp only [hij, ↓reduceIte] - have hone : - MvPolynomial.degreeOf i (1 : MvPolynomial (Fin n) F) ≤ 0 := by - simp - have hmul : - MvPolynomial.degreeOf i (MvPolynomial.C a * MvPolynomial.X j) ≤ 0 := by - calc - _ ≤ MvPolynomial.degreeOf i (MvPolynomial.C a) + - MvPolynomial.degreeOf i (MvPolynomial.X j) := by - exact MvPolynomial.degreeOf_mul_le i _ _ - _ ≤ 0 + 0 := by - gcongr - · exact (MvPolynomial.degreeOf_C (R := F) a i).le - · exact (MvPolynomial.degreeOf_X_of_ne (R := F) i j hij).le - _ = 0 := by omega - exact (MvPolynomial.degreeOf_add_le i _ _).trans (max_le hone hmul) - -private theorem signedBasisPolynomial_degreeOf (u : Hypercube n) (i : Fin n) : - MvPolynomial.degreeOf i (signedBasisPolynomial F n u) ≤ 1 := by - calc - _ ≤ MvPolynomial.degreeOf i (MvPolynomial.C (((2 : F) ^ n)⁻¹)) + - MvPolynomial.degreeOf i - (∏ j : Fin n, (1 + MvPolynomial.C (bitToSign F (u j)) * MvPolynomial.X j)) := by - exact MvPolynomial.degreeOf_mul_le i _ _ - _ ≤ 0 + - MvPolynomial.degreeOf i - (∏ j : Fin n, (1 + MvPolynomial.C (bitToSign F (u j)) * MvPolynomial.X j)) := by - gcongr - exact (MvPolynomial.degreeOf_C (R := F) (((2 : F) ^ n)⁻¹) i).le - _ = - MvPolynomial.degreeOf i - (∏ j : Fin n, (1 + MvPolynomial.C (bitToSign F (u j)) * MvPolynomial.X j)) := by - simp - _ ≤ ∑ j : Fin n, - MvPolynomial.degreeOf i (1 + MvPolynomial.C (bitToSign F (u j)) * MvPolynomial.X j) := by - exact MvPolynomial.degreeOf_prod_le i _ _ - _ ≤ ∑ j : Fin n, if i = j then 1 else 0 := by - apply Finset.sum_le_sum - intro j _ - exact signedLinearFactor_degreeOf F n (bitToSign F (u j)) i j - _ = 1 := by - norm_num - -private theorem signedMLEPolynomial_degreeOf (values : Hypercube n → F) (i : Fin n) : - MvPolynomial.degreeOf i (signedMLEPolynomial F n values) ≤ 1 := by - classical - calc - _ ≤ (Finset.univ : Finset (Hypercube n)).sup - fun u => MvPolynomial.degreeOf i - (MvPolynomial.C (values u) * signedBasisPolynomial F n u) := by - exact MvPolynomial.degreeOf_sum_le i _ _ - _ ≤ 1 := by - apply Finset.sup_le - intro u _ - calc - MvPolynomial.degreeOf i (MvPolynomial.C (values u) * signedBasisPolynomial F n u) - ≤ MvPolynomial.degreeOf i (MvPolynomial.C (values u)) + - MvPolynomial.degreeOf i (signedBasisPolynomial F n u) := by - exact MvPolynomial.degreeOf_mul_le i _ _ - _ ≤ 0 + 1 := by - gcongr - · exact (MvPolynomial.degreeOf_C (R := F) (values u) i).le - · exact signedBasisPolynomial_degreeOf F n u i - _ = 1 := by omega - -private theorem lagrangeKernelPolynomial_degreeOf (z : Fin n → F) (i : Fin n) : - MvPolynomial.degreeOf i (lagrangeKernelPolynomial F n z) ≤ 1 := by - calc - _ ≤ MvPolynomial.degreeOf i (MvPolynomial.C (((2 : F) ^ n)⁻¹)) + - MvPolynomial.degreeOf i - (∏ j : Fin n, (1 + MvPolynomial.C (z j) * MvPolynomial.X j)) := by - exact MvPolynomial.degreeOf_mul_le i _ _ - _ ≤ 0 + - MvPolynomial.degreeOf i - (∏ j : Fin n, (1 + MvPolynomial.C (z j) * MvPolynomial.X j)) := by - gcongr - exact (MvPolynomial.degreeOf_C (R := F) (((2 : F) ^ n)⁻¹) i).le - _ = - MvPolynomial.degreeOf i - (∏ j : Fin n, (1 + MvPolynomial.C (z j) * MvPolynomial.X j)) := by - simp - _ ≤ ∑ j : Fin n, - MvPolynomial.degreeOf i (1 + MvPolynomial.C (z j) * MvPolynomial.X j) := by - exact MvPolynomial.degreeOf_prod_le i _ _ - _ ≤ ∑ j : Fin n, if i = j then 1 else 0 := by - apply Finset.sum_le_sum - intro j _ - exact signedLinearFactor_degreeOf F n (z j) i j - _ = 1 := by - norm_num - -/-- Polynomial extension of one retained Lagrange-form multilinear oracle. -/ -private noncomputable def multilinearOraclePolynomial (oracle : MultilinearOracle F n) : - MvPolynomial (Fin n) F := - signedMLEPolynomial F n fun u => evalOnHypercube oracle u - -private theorem multilinearOraclePolynomial_eval (oracle : MultilinearOracle F n) - (r : Fin n → F) : - MvPolynomial.eval r (multilinearOraclePolynomial F n oracle) = - lagrangeOracleEval oracle r := by - simp [multilinearOraclePolynomial, signedMLEPolynomial_eval, lagrangeOracleEval, - evalOnHypercube] - -private noncomputable def inputOraclePolynomial - (oStmt : ∀ i, OStmtAfterOuter F n M params i) (idx : InputOracleIdx M) : - MvPolynomial (Fin n) F := - match idx with - | .table => multilinearOraclePolynomial F n (oStmt (.input .table)) - | .column i => multilinearOraclePolynomial F n (oStmt (.input (.column i))) - -private noncomputable def multiplicityPolynomial - (oStmt : ∀ i, OStmtAfterOuter F n M params i) : - MvPolynomial (Fin n) F := - multilinearOraclePolynomial F n (oStmt .multiplicity) - -private noncomputable def helperPolynomial - (oStmt : ∀ i, OStmtAfterOuter F n M params i) (k : Fin params.numGroups) : - MvPolynomial (Fin n) F := - multilinearOraclePolynomial F n ((oStmt .helpers) k) - -private noncomputable def termPhiPolynomial - (stmt : StmtAfterOuter F n M params) - (oStmt : ∀ i, OStmtAfterOuter F n M params i) (i : TermIdx M) : - MvPolynomial (Fin n) F := - MvPolynomial.C stmt.xChallenge + inputOraclePolynomial F n M params oStmt (termToInput i) - -private noncomputable def termNumeratorPolynomial - (oStmt : ∀ i, OStmtAfterOuter F n M params i) (i : TermIdx M) : - MvPolynomial (Fin n) F := - match termToInput i with - | .table => multiplicityPolynomial F n M params oStmt - | .column _ => MvPolynomial.C (-1) - -private noncomputable def domainIdentityPolynomial - (stmt : StmtAfterOuter F n M params) - (oStmt : ∀ i, OStmtAfterOuter F n M params i) (k : Fin params.numGroups) : - MvPolynomial (Fin n) F := - helperPolynomial F n M params oStmt k * - (∏ i ∈ canonicalGroups params k, termPhiPolynomial F n M params stmt oStmt i) - - ∑ i ∈ canonicalGroups params k, - termNumeratorPolynomial F n M params oStmt i * - ∏ j ∈ (canonicalGroups params k).erase i, - termPhiPolynomial F n M params stmt oStmt j - -private theorem multilinearOraclePolynomial_degreeOf (oracle : MultilinearOracle F n) - (i : Fin n) : - MvPolynomial.degreeOf i (multilinearOraclePolynomial F n oracle) ≤ 1 := by - simpa [multilinearOraclePolynomial] using - signedMLEPolynomial_degreeOf F n (fun u => evalOnHypercube oracle u) i - -private theorem inputOraclePolynomial_degreeOf - (oStmt : ∀ i, OStmtAfterOuter F n M params i) (idx : InputOracleIdx M) - (i : Fin n) : - MvPolynomial.degreeOf i (inputOraclePolynomial F n M params oStmt idx) ≤ 1 := by - cases idx with - | table => - simpa [inputOraclePolynomial] using - multilinearOraclePolynomial_degreeOf F n (oStmt (.input .table)) i - | column j => - simpa [inputOraclePolynomial] using - multilinearOraclePolynomial_degreeOf F n (oStmt (.input (.column j))) i - -private theorem multiplicityPolynomial_degreeOf - (oStmt : ∀ i, OStmtAfterOuter F n M params i) (i : Fin n) : - MvPolynomial.degreeOf i (multiplicityPolynomial F n M params oStmt) ≤ 1 := - multilinearOraclePolynomial_degreeOf F n (oStmt .multiplicity) i - -private theorem helperPolynomial_degreeOf - (oStmt : ∀ i, OStmtAfterOuter F n M params i) (k : Fin params.numGroups) - (i : Fin n) : - MvPolynomial.degreeOf i (helperPolynomial F n M params oStmt k) ≤ 1 := - multilinearOraclePolynomial_degreeOf F n ((oStmt .helpers) k) i - -private theorem termPhiPolynomial_degreeOf - (stmt : StmtAfterOuter F n M params) - (oStmt : ∀ i, OStmtAfterOuter F n M params i) (j : TermIdx M) (i : Fin n) : - MvPolynomial.degreeOf i (termPhiPolynomial F n M params stmt oStmt j) ≤ 1 := by - calc - _ ≤ max (MvPolynomial.degreeOf i (MvPolynomial.C stmt.xChallenge)) - (MvPolynomial.degreeOf i (inputOraclePolynomial F n M params oStmt (termToInput j))) := by - exact MvPolynomial.degreeOf_add_le i _ _ - _ ≤ max 0 1 := by - gcongr - · exact (MvPolynomial.degreeOf_C (R := F) stmt.xChallenge i).le - · exact inputOraclePolynomial_degreeOf F n M params oStmt (termToInput j) i - _ = 1 := by - omega - -private theorem termNumeratorPolynomial_degreeOf - (oStmt : ∀ i, OStmtAfterOuter F n M params i) (j : TermIdx M) (i : Fin n) : - MvPolynomial.degreeOf i (termNumeratorPolynomial F n M params oStmt j) ≤ 1 := by - unfold termNumeratorPolynomial - cases h : termToInput j with - | table => - simpa [h, multiplicityPolynomial] using - multiplicityPolynomial_degreeOf F n M params oStmt i - | column c => - exact (MvPolynomial.degreeOf_C (R := F) (-1 : F) i).le.trans (by omega) - -private theorem finset_card_termIdx_le (s : Finset (TermIdx M)) : - s.card ≤ M + 1 := by - simpa [TermIdx] using Finset.card_le_univ (s := s) - -private theorem termPhiPolynomial_prod_degreeOf - (stmt : StmtAfterOuter F n M params) - (oStmt : ∀ i, OStmtAfterOuter F n M params i) (s : Finset (TermIdx M)) - (i : Fin n) : - MvPolynomial.degreeOf i - (∏ j ∈ s, termPhiPolynomial F n M params stmt oStmt j) ≤ M + 1 := by - calc - _ ≤ ∑ j ∈ s, - MvPolynomial.degreeOf i (termPhiPolynomial F n M params stmt oStmt j) := by - exact MvPolynomial.degreeOf_prod_le i _ _ - _ ≤ ∑ _j ∈ s, 1 := by - apply Finset.sum_le_sum - intro j _ - exact termPhiPolynomial_degreeOf F n M params stmt oStmt j i - _ = s.card := by - simp - _ ≤ M + 1 := finset_card_termIdx_le M s - -private theorem domainIdentityPolynomial_degreeOf - (stmt : StmtAfterOuter F n M params) - (oStmt : ∀ i, OStmtAfterOuter F n M params i) (k : Fin params.numGroups) - (i : Fin n) : - MvPolynomial.degreeOf i (domainIdentityPolynomial F n M params stmt oStmt k) ≤ M + 2 := by - unfold domainIdentityPolynomial - have hProd : - MvPolynomial.degreeOf i - (∏ j ∈ canonicalGroups params k, termPhiPolynomial F n M params stmt oStmt j) ≤ - M + 1 := - termPhiPolynomial_prod_degreeOf F n M params stmt oStmt (canonicalGroups params k) i - have hLeft : - MvPolynomial.degreeOf i - (helperPolynomial F n M params oStmt k * - (∏ j ∈ canonicalGroups params k, termPhiPolynomial F n M params stmt oStmt j)) ≤ - M + 2 := by - calc - _ ≤ MvPolynomial.degreeOf i (helperPolynomial F n M params oStmt k) + - MvPolynomial.degreeOf i - (∏ j ∈ canonicalGroups params k, - termPhiPolynomial F n M params stmt oStmt j) := by - exact MvPolynomial.degreeOf_mul_le i _ _ - _ ≤ 1 + (M + 1) := by - gcongr - exact helperPolynomial_degreeOf F n M params oStmt k i - _ = M + 2 := by - omega - have hRight : - MvPolynomial.degreeOf i - (∑ j ∈ canonicalGroups params k, - termNumeratorPolynomial F n M params oStmt j * - ∏ l ∈ (canonicalGroups params k).erase j, - termPhiPolynomial F n M params stmt oStmt l) ≤ - M + 2 := by - calc - _ ≤ (canonicalGroups params k).sup fun j => - MvPolynomial.degreeOf i - (termNumeratorPolynomial F n M params oStmt j * - ∏ l ∈ (canonicalGroups params k).erase j, - termPhiPolynomial F n M params stmt oStmt l) := by - exact MvPolynomial.degreeOf_sum_le i _ _ - _ ≤ M + 2 := by - apply Finset.sup_le - intro j _ - have hEraseProd : - MvPolynomial.degreeOf i - (∏ l ∈ (canonicalGroups params k).erase j, - termPhiPolynomial F n M params stmt oStmt l) ≤ M + 1 := - termPhiPolynomial_prod_degreeOf F n M params stmt oStmt - ((canonicalGroups params k).erase j) i - calc - _ ≤ MvPolynomial.degreeOf i (termNumeratorPolynomial F n M params oStmt j) + - MvPolynomial.degreeOf i - (∏ l ∈ (canonicalGroups params k).erase j, - termPhiPolynomial F n M params stmt oStmt l) := by - exact MvPolynomial.degreeOf_mul_le i _ _ - _ ≤ 1 + (M + 1) := by - gcongr - exact termNumeratorPolynomial_degreeOf F n M params oStmt j i - _ = M + 2 := by - omega - exact (MvPolynomial.degreeOf_sub_le i _ _).trans (max_le hLeft hRight) - -/-- The concrete multivariate LogUp sumcheck polynomial before packaging with its degree proof. -/ -noncomputable def logupQPolynomial - (stmt : StmtAfterOuter F n M params) - (oStmt : ∀ i, OStmtAfterOuter F n M params i) : - MvPolynomial (Fin n) F := - ∑ k : Fin params.numGroups, ( - helperPolynomial F n M params oStmt k + - lagrangeKernelPolynomial F n stmt.zChallenge * - MvPolynomial.C (stmt.batchingScalars k) * - domainIdentityPolynomial F n M params stmt oStmt k) - -theorem logupQPolynomial_degreeOf - (stmt : StmtAfterOuter F n M params) - (oStmt : ∀ i, OStmtAfterOuter F n M params i) (i : Fin n) : - MvPolynomial.degreeOf i (logupQPolynomial F n M params stmt oStmt) ≤ M + 3 := by - classical - unfold logupQPolynomial - calc - _ ≤ (Finset.univ : Finset (Fin params.numGroups)).sup fun k => - MvPolynomial.degreeOf i - (helperPolynomial F n M params oStmt k + - lagrangeKernelPolynomial F n stmt.zChallenge * - MvPolynomial.C (stmt.batchingScalars k) * - domainIdentityPolynomial F n M params stmt oStmt k) := by - exact MvPolynomial.degreeOf_sum_le i _ _ - _ ≤ M + 3 := by - apply Finset.sup_le - intro k _ - have hHelper : MvPolynomial.degreeOf i (helperPolynomial F n M params oStmt k) ≤ M + 3 := - (helperPolynomial_degreeOf F n M params oStmt k i).trans (by omega) - have hProduct : - MvPolynomial.degreeOf i - (lagrangeKernelPolynomial F n stmt.zChallenge * - MvPolynomial.C (stmt.batchingScalars k) * - domainIdentityPolynomial F n M params stmt oStmt k) ≤ M + 3 := by - calc - _ ≤ MvPolynomial.degreeOf i - (lagrangeKernelPolynomial F n stmt.zChallenge * - MvPolynomial.C (stmt.batchingScalars k)) + - MvPolynomial.degreeOf i - (domainIdentityPolynomial F n M params stmt oStmt k) := by - exact MvPolynomial.degreeOf_mul_le i _ _ - _ ≤ (MvPolynomial.degreeOf i (lagrangeKernelPolynomial F n stmt.zChallenge) + - MvPolynomial.degreeOf i (MvPolynomial.C (stmt.batchingScalars k))) + - MvPolynomial.degreeOf i - (domainIdentityPolynomial F n M params stmt oStmt k) := by - gcongr - exact MvPolynomial.degreeOf_mul_le i _ _ - _ ≤ (1 + 0) + (M + 2) := by - gcongr - · exact lagrangeKernelPolynomial_degreeOf F n stmt.zChallenge i - · exact (MvPolynomial.degreeOf_C (R := F) (stmt.batchingScalars k) i).le - · exact domainIdentityPolynomial_degreeOf F n M params stmt oStmt k i - _ = M + 3 := by - omega - exact (MvPolynomial.degreeOf_add_le i _ _).trans (max_le hHelper hProduct) - -end SumcheckPolynomial - -end Logup diff --git a/ArkLib/ProofSystem/Sumcheck/Spec/General.lean b/ArkLib/ProofSystem/Sumcheck/Spec/General.lean index 7fa223905a..71143438c1 100644 --- a/ArkLib/ProofSystem/Sumcheck/Spec/General.lean +++ b/ArkLib/ProofSystem/Sumcheck/Spec/General.lean @@ -213,6 +213,15 @@ theorem reduction_perfectCompleteness : (R := SingleRound.reduction R n deg D oSpec) (h := fun i => SingleRound.reduction_perfectCompleteness i) +/-- Perfect completeness for the (full) sum-check oracle reduction. -/ +theorem oracleReduction_perfectCompleteness : + (oracleReduction R deg D n oSpec).perfectCompleteness init impl + (relationRound R n deg D 0) (relationRound R n deg D (.last n)) := + OracleReduction.seqCompose_perfectCompleteness + (rel := relationRound R n deg D) + (R := SingleRound.oracleReduction R n deg D oSpec) + (h := fun i => SingleRound.oracleReduction_perfectCompleteness i) + /-- Round-by-round knowledge soundness with error `deg / |R|` per challenge for the (full) sum-check protocol -/ theorem oracleVerifier_rbrKnowledgeSoundness [Fintype R] :