feat: even more general ring switch

ArkLib.lean

@@ -141,6 +141,7 @@ import ArkLib.Data.Matrix.Basic
 import ArkLib.Data.Matrix.Sparse
 import ArkLib.Data.Matrix.Vandermonde
 import ArkLib.Data.Misc.Basic
+import ArkLib.Data.Module.Basis
 import ArkLib.Data.MvPolynomial.Degrees
 import ArkLib.Data.MvPolynomial.Interpolation
 import ArkLib.Data.MvPolynomial.LinearMvExtension
@@ -158,6 +159,7 @@ import ArkLib.Data.Polynomial.SplitFold
 import ArkLib.Data.Polynomial.Trivariate
 import ArkLib.Data.Probability.Instances
 import ArkLib.Data.Probability.Notation
+import ArkLib.Data.Probability.OracleCompBridge
 import ArkLib.OracleReduction.BCS.Basic
 import ArkLib.OracleReduction.Basic
 import ArkLib.OracleReduction.Cast
@@ -188,6 +190,7 @@ import ArkLib.OracleReduction.ProtocolSpec.Cast
 import ArkLib.OracleReduction.ProtocolSpec.SeqCompose
 import ArkLib.OracleReduction.Salt
 import ArkLib.OracleReduction.Security.Basic
+import ArkLib.OracleReduction.Security.ChallengeRound
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Basic
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Composition
@@ -230,6 +233,12 @@ import ArkLib.ProofSystem.Fri.Spec.SingleRound
 import ArkLib.ProofSystem.Plonk.Basic
 import ArkLib.ProofSystem.RingSwitching.BatchingPhase
 import ArkLib.ProofSystem.RingSwitching.General
+import ArkLib.ProofSystem.RingSwitching.Generic.Batching
+import ArkLib.ProofSystem.RingSwitching.Generic.Carrier
+import ArkLib.ProofSystem.RingSwitching.Generic.Packing
+import ArkLib.ProofSystem.RingSwitching.Generic.Recombine
+import ArkLib.ProofSystem.RingSwitching.Generic.Reduction
+import ArkLib.ProofSystem.RingSwitching.Generic.Relations
 import ArkLib.ProofSystem.RingSwitching.Prelude
 import ArkLib.ProofSystem.RingSwitching.Profile
 import ArkLib.ProofSystem.RingSwitching.Spec

ArkLib/Data/Module/Basis.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Hicks
+-/
+
+import Mathlib.LinearAlgebra.Basis.Defs
+
+/-!
+# Basis recombination lemmas
+
+The finite `R`-linear recombination along a basis, `s ↦ ∑ i, s i • b i`, is exactly
+`b.equivFun.symm`, hence a bijection (in particular injective: distinct coordinate tuples
+recombine to distinct module elements). Stated once here so both directions of a free-module
+"pack/unpack" argument (e.g. the ring-switching packing- and opening-basis sides) consume the
+same lemma.
+-/
+
+namespace Module.Basis
+
+variable {ι R M : Type*} [Fintype ι] [Semiring R] [AddCommMonoid M] [Module R M]
+
+/-- Recombination along a basis, `s ↦ ∑ i, s i • b i`, is a bijection: it is
+`b.equivFun.symm` in pointful form. -/
+theorem sum_smul_bijective (b : Basis ι R M) :
+    Function.Bijective (fun s : ι → R => ∑ i, s i • b i) := by
+  have h : (fun s : ι → R => ∑ i, s i • b i) = b.equivFun.symm := by
+    funext s
+    rw [Basis.equivFun_symm_apply]
+  rw [h]
+  exact b.equivFun.symm.bijective
+
+/-- Recombination along a basis is injective: distinct coordinate tuples recombine to
+distinct module elements. -/
+theorem sum_smul_injective (b : Basis ι R M) :
+    Function.Injective (fun s : ι → R => ∑ i, s i • b i) :=
+  b.sum_smul_bijective.injective
+
+end Module.Basis

ArkLib/Data/MvPolynomial/Degrees.lean

@@ -186,6 +186,22 @@ theorem mem_restrictDegree_iff_degreeOf_le (p : MvPolynomial σ R) (n : ℕ) :
   apply Iff.trans (mem_restrictDegree_iff_sup σ p n)
   simp only [degreeOf]
 
+/-- A polynomial with degree at most `1` in each of finitely many variables (e.g. a multilinear
+polynomial) has total degree at most the number of variables. -/
+theorem totalDegree_le_card_of_degreeOf_le_one [Fintype σ] (p : MvPolynomial σ R)
+    (h : ∀ i, p.degreeOf i ≤ 1) : p.totalDegree ≤ Fintype.card σ := by
+  rw [MvPolynomial.totalDegree]
+  refine Finset.sup_le fun m hm => ?_
+  have hsum : (m.sum fun _ e => e) = ∑ i, m i := by
+    rw [Finsupp.sum_fintype]
+    intro i; rfl
+  rw [hsum]
+  calc ∑ i, m i ≤ ∑ _i : σ, 1 :=
+        Finset.sum_le_sum fun i _ =>
+          le_trans (Finset.le_sup (f := fun m => m i) hm)
+            (by rw [← MvPolynomial.degreeOf_eq_sup]; exact h i)
+    _ = Fintype.card σ := by simp
+
 end DegreeOf
 
 section Equiv

ArkLib/Data/MvPolynomial/Multilinear.lean

@@ -27,6 +27,15 @@ variable {σ : Type*} {R : Type*}
 instance coeFunctionFin2 [NatCast R] : Coe (σ → Fin 2) (σ → R) where
   coe := fun vec i => vec i
 
+/-- The Boolean-point coercion above agrees with the if-then-else spellings used elsewhere
+(`if · = 1 then 1 else 0` as in `RingSwitchCarrier.boolToE`, or the propositionally identical
+`if · == 1` as in `RingSwitching.compute_s0`); this is the bridge between them. -/
+theorem coe_boolFun_eq_ite [AddMonoidWithOne R] (u : σ → Fin 2) :
+    (u : σ → R) = fun i => if u i = 1 then 1 else 0 := by
+  funext i
+  have h : u i = 0 ∨ u i = 1 := by fin_omega
+  rcases h with h | h <;> simp [h]
+
 variable [CommRing R]
 
 def toEvalsZeroOne (p : MvPolynomial σ R) : (σ → Fin 2) → R :=
@@ -143,6 +152,12 @@ theorem eval_zeroOne_eq_MLE_toEvalsZeroOne (p : MvPolynomial σ R) (x : σ → F
     eval (x : σ → R) p = eval (x : σ → R) (MLE p.toEvalsZeroOne) := by
   simp only [MLE_eval_zeroOne, toEvalsZeroOne]
 
+/-- Evaluating a multilinear extension at an **arbitrary** point expands over the hypercube
+against the eq-indicator: `(MLE g)(r) = ∑_x eq̃(x, r) · g(x)`. -/
+theorem MLE_eval_eq_sum_eqTilde (evals : (σ → Fin 2) → R) (r : σ → R) :
+    MvPolynomial.eval r (MLE evals) = ∑ x : σ → Fin 2, eqTilde (x : σ → R) r * evals x := by
+  simp only [MLE, map_sum, map_mul, eval_C, eqTilde]
+
 section DegreeOf
 
 omit [Fintype σ] in
@@ -210,6 +225,11 @@ theorem MLE_degreeOf (evals : (σ → Fin 2) → R) (i : σ) : degreeOf i (MLE e
   apply (mem_restrictDegree_iff_degreeOf_le _ _).mp
   exact MLE_mem_restrictDegree evals
 
+/-- A multilinear extension over `σ` variables has total degree at most `|σ|`. -/
+theorem MLE_totalDegree_le (evals : (σ → Fin 2) → R) :
+    (MLE evals).totalDegree ≤ Fintype.card σ :=
+  totalDegree_le_card_of_degreeOf_le_one _ (fun i => MLE_degreeOf evals i)
+
 end DegreeOf
 
 -- TODO: add lemmas about the uniqueness of multilinear polynomials up to evaluations on hypercube
@@ -272,6 +292,34 @@ def MLEEquiv : R⦃≤ 1⦄[X σ] ≃ ((σ → Fin 2) → R) where
 def MLEEquivFin {n : ℕ} : R⦃≤ 1⦄[X (Fin n)] ≃ (Fin (2 ^ n) → R) :=
   Equiv.trans MLEEquiv (Equiv.piCongr finFunctionFinEquiv (fun _ => Equiv.refl _))
 
+omit [DecidableEq R] [IsDomain R] in
+/-- **Multilinear `aeval` hypercube expansion**: evaluating a multilinear polynomial over `R` at a
+point `r` of an `R`-algebra `A` expands over the Boolean hypercube against the eq-indicator,
+`aeval r p = ∑ y, eq̃(y, r) · algebraMap R A (p(y))`. The proof self-interpolates the
+coefficient-mapped polynomial over `A` (`is_multilinear_iff_eq_evals_zeroOne`, a root-counting
+argument), whence the `[IsDomain A]` hypothesis; the identity itself holds over any commutative
+ring, and dropping the domain hypothesis is future work. -/
+theorem aeval_multilinear_eq_sum_eqTilde {A : Type*} [CommRing A] [Algebra R A] [IsDomain A]
+    {p : MvPolynomial σ R} (hp : p ∈ R⦃≤ 1⦄[X σ]) (r : σ → A) :
+    aeval r p
+      = ∑ y : σ → Fin 2, eqTilde (y : σ → A) r * algebraMap R A (eval (y : σ → R) p) := by
+  have hq : map (algebraMap R A) p ∈ A⦃≤ 1⦄[X σ] := by
+    rw [mem_restrictDegree] at hp ⊢
+    exact fun s hs i => hp s (support_map_subset _ _ hs) i
+  calc aeval r p = eval r (map (algebraMap R A) p) := by
+        rw [eval_map, aeval_def]
+    _ = ∑ y : σ → Fin 2, eqTilde (y : σ → A) r * (map (algebraMap R A) p).toEvalsZeroOne y := by
+        conv_lhs => rw [← is_multilinear_iff_eq_evals_zeroOne.mp hq]
+        exact MLE_eval_eq_sum_eqTilde _ r
+    _ = ∑ y : σ → Fin 2, eqTilde (y : σ → A) r * algebraMap R A (eval (y : σ → R) p) := by
+        refine Finset.sum_congr rfl fun y _ => ?_
+        congr 1
+        change eval (y : σ → A) (map (algebraMap R A) p) = algebraMap R A (eval (y : σ → R) p)
+        have hpt : (y : σ → A) = fun i => algebraMap R A ((y : σ → R) i) :=
+          funext fun i => (map_natCast (algebraMap R A) _).symm
+        rw [hpt, eval_map]
+        exact (eval₂_comp (algebraMap R A) (y : σ → R) p).symm
+
 end MvPolynomial
 
 end

ArkLib/Data/Probability/Instances.lean

@@ -452,32 +452,33 @@ lemma Pr_congr {α : Type} {D : PMF α} {P Q : α → Prop}
   congr 1; exact propext (h x)
 
 /-- **Schwartz-Zippel Lemma** (Probability Form):
-For a non-zero multivariate polynomial `P` of total degree at most `d` over a finite field `L`,
-the probability that `P(r)` evaluates to 0 for a uniformly random `r` is at most `d / |L|`. -/
+For a non-zero multivariate polynomial `P` of total degree at most `d` over a finite integral
+domain `R`, the probability that `P(r)` evaluates to 0 for a uniformly random `r` is at most
+`d / |R|`. -/
 lemma prob_schwartz_zippel_mv_polynomial {R : Type} [CommRing R] [IsDomain R] [Fintype R]
     {n : ℕ}
-    (P : MvPolynomial (Fin n) R) (h_nonzero : P ≠ 0) (h_deg : P.totalDegree ≤ n) :
+    (P : MvPolynomial (Fin n) R) (d : ℕ) (h_nonzero : P ≠ 0) (h_deg : P.totalDegree ≤ d) :
     Pr_{ let r ←$ᵖ (Fin n → R) }[ MvPolynomial.eval r P = 0 ] ≤
-      (n : ℝ≥0) / (Fintype.card R : ℝ≥0) := by
+      (d : ℝ≥0) / (Fintype.card R : ℝ≥0) := by
   classical
   rw [prob_uniform_eq_card_filter_div_card]
   push_cast
   have sz_bound := MvPolynomial.schwartz_zippel_totalDegree (R := R) (n := n)
     (p := P) (hp := h_nonzero) (S := Finset.univ)
   simp only [Fintype.piFinset_univ, card_univ] at sz_bound
-  have sz_bound_le_n_div_card_R : ((#{f | (MvPolynomial.eval f) P = 0}) : ℚ≥0)
-    / ((Fintype.card R ^ n)) ≤ (n : ℚ≥0) / ((#(Finset.univ : Finset R)) : ℚ≥0) := by
+  have sz_bound_le_d_div_card_R : ((#{f | (MvPolynomial.eval f) P = 0}) : ℚ≥0)
+    / ((Fintype.card R ^ n)) ≤ (d : ℚ≥0) / ((#(Finset.univ : Finset R)) : ℚ≥0) := by
     calc
       _ ≤ (P.totalDegree : ℚ≥0) / ((#(Finset.univ : Finset R)) : ℚ≥0) := sz_bound
       _ ≤ _ := by
         simp only [card_univ]
         apply div_le_of_le_mul₀ (hb := by simp only [zero_le]) (hc := by simp only [zero_le])
-        -- ⊢ ↑P.totalDegree ≤ ↑n / ↑(Fintype.card R) * ↑(Fintype.card R)
+        -- ⊢ ↑P.totalDegree ≤ ↑d / ↑(Fintype.card R) * ↑(Fintype.card R)
         rw [div_mul_cancel₀ (h := by simp only [ne_eq, Nat.cast_eq_zero, Fintype.card_ne_zero,
           not_false_eq_true])]
         exact Nat.cast_le.mpr h_deg
   have sz_bound_ENNReal : ((#{f | (MvPolynomial.eval f) P = 0}) : ENNReal)
-    / ((Fintype.card R ^ n) : ℕ) ≤ (n : ENNReal) / (Fintype.card R : ENNReal) := by
+    / ((Fintype.card R ^ n) : ℕ) ≤ (d : ENNReal) / (Fintype.card R : ENNReal) := by
     simp_rw [ENNReal.coe_Nat_coe_NNRat]
     conv_lhs => rw [ENNReal.coe_div_of_NNRat (hb := by
       simp only [Nat.cast_pow, ne_eq, pow_eq_zero_iff', Nat.cast_eq_zero, Fintype.card_ne_zero,
@@ -486,11 +487,27 @@ lemma prob_schwartz_zippel_mv_polynomial {R : Type} [CommRing R] [IsDomain R] [F
       Fintype.card_ne_zero, not_false_eq_true])]
     rw [ENNReal.coe_le_of_NNRat]
     simp only [Nat.cast_pow]
-    exact sz_bound_le_n_div_card_R
+    exact sz_bound_le_d_div_card_R
   simp only [Fintype.card_pi, prod_const, card_univ, Fintype.card_fin, Nat.cast_pow, ge_iff_le]
   rw [Nat.cast_pow] at sz_bound_ENNReal
   exact sz_bound_ENNReal
 
+/-- **Schwartz-Zippel**, single-variable sampling form: for a non-zero polynomial in one variable
+(as an `MvPolynomial (Fin 1)`) of total degree at most `d`, the probability that it vanishes at a
+uniformly random point of `R` (sampled directly, not as `Fin 1 → R`) is at most `d / |R|`. -/
+lemma prob_schwartz_zippel_single_variable {R : Type} [CommRing R] [IsDomain R] [Fintype R]
+    (f : MvPolynomial (Fin 1) R) (d : ℕ) (h_nonzero : f ≠ 0) (h_deg : f.totalDegree ≤ d) :
+    Pr_{ let γ ←$ᵖ R }[ MvPolynomial.eval (fun _ : Fin 1 => γ) f = 0 ] ≤
+      (d : ℝ≥0) / (Fintype.card R : ℝ≥0) := by
+  rw [← prob_uniform_singleton_finFun_eq
+    (P := fun γ => MvPolynomial.eval (fun _ : Fin 1 => γ) f = 0)]
+  calc Pr_{ let r ←$ᵖ (Fin 1 → R) }[ MvPolynomial.eval (fun _ : Fin 1 => r 0) f = 0 ]
+      = Pr_{ let r ←$ᵖ (Fin 1 → R) }[ MvPolynomial.eval r f = 0 ] := by
+        refine Pr_congr fun r => ?_
+        have hr : (fun _ : Fin 1 => r 0) = r := funext fun i => congrArg r (Subsingleton.elim 0 i)
+        rw [hr]
+    _ ≤ _ := prob_schwartz_zippel_mv_polynomial f d h_nonzero h_deg
+
 /-- Pushforward of `PMF.uniformOfFintype α` under a map `f : α → β` whose fibers
 over the image all have the same cardinality `k > 0` is the uniform distribution
 on the image of `f`.

ArkLib/Data/Probability/OracleCompBridge.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Hicks
+-/
+
+import VCVio
+import ArkLib.Data.Probability.Instances
+
+/-!
+# Bridge: VCVio `OracleComp` events ↔ `PMF` sampling notation
+
+Round-by-round security games in ArkLib live on the VCVio side (`Pr[E | oa]` over
+`OracleComp`/`ProbComp`), while per-round error analyses are naturally stated against the
+`PMF`-level sampling notation `Pr_{ let c ←$ᵖ C }[ E c ]` (`ArkLib.Data.Probability.Notation`).
+This file provides the bridge:
+
+* `probEvent_uniformSample_eq_pr_uniformOfFintype`: the event probability of a uniform query
+  `$ᵗ C` is exactly that of `PMF.uniformOfFintype C`.
+* `probEvent_bind_uniformSample_le`: a per-prefix `PMF`-level bound transfers to the bind
+  `do let a ← ma; let c ← $ᵗ C; return (a, c)` — the shape of an RBR game whose final
+  round is a uniformly sampled challenge.
+
+Layering: `Data` files may import VCVio (precedent: `ArkLib.Data.Hash.DuplexSponge`).
+-/
+
+open OracleComp ProbabilityTheory NNReal
+
+open scoped ENNReal
+
+section OracleCompBridge
+
+variable {C : Type} [SampleableType C] [Fintype C] [Nonempty C]
+
+/-- The event probability of a uniform query `$ᵗ C` agrees with the `PMF`-level probability
+under `PMF.uniformOfFintype C`: both are `#{c | E c} / #C`. -/
+theorem probEvent_uniformSample_eq_pr_uniformOfFintype (E : C → Prop) :
+    Pr[E | $ᵗ C] = Pr_{ let c ← $ᵖ C}[E c] := by
+  classical
+  rw [probEvent_uniformSample, prob_uniform_eq_card_filter_div_card]
+  simp
+
+/-- A per-prefix `PMF`-level bound on a uniformly sampled challenge transfers to the
+`OracleComp` bind `do let a ← ma; let c ← $ᵗ C; return (a, c)`.
+
+This is the probability core of factoring an RBR game: `ma` is the (already simulated)
+transcript prefix, `c` the fresh challenge, and `E` the bad event. -/
+theorem probEvent_bind_uniformSample_le {A : Type} (ma : ProbComp A)
+    (E : A → C → Prop) {ε : ℝ≥0∞}
+    (h : ∀ a, Pr_{ let c ← $ᵖ C}[E a c] ≤ ε) :
+    Pr[fun x => E x.1 x.2 | do let a ← ma; let c ← $ᵗ C; return (a, c)] ≤ ε := by
+  refine probEvent_bind_le_of_forall_le fun a _ => ?_
+  calc Pr[fun x => E x.1 x.2 | do let c ← $ᵗ C; return (a, c)]
+      = Pr[fun c => E a c | $ᵗ C] := by
+        rw [bind_pure_comp, probEvent_map]
+        rfl
+    _ = Pr_{ let c ← $ᵖ C}[E a c] := probEvent_uniformSample_eq_pr_uniformOfFintype _
+    _ ≤ ε := h a
+
+end OracleCompBridge