Ring-Switching IOP Prelude

This module contains the core definitions and infrastructure for the ring-switching IOP, including tensor algebra operations, field extension handling, and basic protocol types.

Main Components

1. Tensor Algebra operations: Operations for handling tensor products between small field K and large field L, including embeddings φ₀ : L → L ⊗[K] L, φ₁ : L → L ⊗[K] L, and row/column decompositions with respect to a K-basis β.
2. Protocol Types: Statement and witness types for each phase
3. Security Definitions: Relations & Kstate for security analysis

Enhanced Tensor Algebra Operations

Additional tensor algebra operations for the enhanced protocol specification. Based on the tensor algebra theory from Section 2.1.

@[reducible, inline]

abbrev Binius.RingSwitching.TensorAlgebra (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : Type u_2

Tensor Algebra A = L ⊗_K L. Based on the spec, it's viewed as (2^κ)x(2^κ) arrays of K-elements. The imported TensorAlgebra file provides the leftAlgebra instances.

def Binius.RingSwitching.φ₀ (L : Type u_1) (K : Type u_2) [Field K] [Field L] [Algebra K L] : L →+* TensorAlgebra K L

Column embedding φ₀: L → A as a ring homomorphism. φ₀(α) = α ⊗ 1, operates on columns.

def Binius.RingSwitching.φ₁ (L : Type u_1) (K : Type u_2) [Field K] [Field L] [Algebra K L] : L →+* TensorAlgebra K L

Row embedding φ₁: L → A as a ring homomorphism. φ₁(α) = 1 ⊗ α, operates on rows.

noncomputable def Binius.RingSwitching.decompose_tensor_algebra_rows (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] {σ : Type u_1} (β : Module.Basis σ K L) (s_hat : TensorAlgebra K L) : σ → L

Decompose ŝ into row components (ŝ =: Σ_{u ∈ {0,1}^κ} β_u ⊗ ŝ_u). This views L ⊗ L as a module over L (left action) and finds the coordinates of ŝ with respect to the basis lifted from β.

noncomputable def Binius.RingSwitching.decompose_tensor_algebra_columns (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] {σ : Type u_1} (β : Module.Basis σ K L) (s_hat : TensorProduct K L L) : σ → L

Decompose ŝ into column components (ŝ =: Σ_{v ∈ {0,1}^κ} ŝ_v ⊗ β_v). This views L ⊗ L as a module over L (right action) and finds the coordinates of ŝ with respect to the basis lifted from β.

noncomputable def Binius.RingSwitching.packMLE (κ : ℕ) (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (β : Module.Basis (Fin κ → Fin 2) K L) (t : ↥(BinaryBasefold.MultilinearPoly K ℓ)) : ↥(BinaryBasefold.MultilinearPoly L ℓ')

Definition 2.1 (MLE packing). Packs a small-field multilinear t into a large-field multilinear t' by reinterpreting chunks of 2^κ coefficients as single L-elements. For each w ∈ {0,1}^ℓ', the evaluation t'(w) is defined as: t'(w) := ∑_{v ∈ {0,1}^κ} t(v₀, ..., v_{κ-1}, w₀, ..., w_{ℓ'-1}) ⋅ β_v

noncomputable def Binius.RingSwitching.unpackMLE (κ : ℕ) (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (β : Module.Basis (Fin κ → Fin 2) K L) (t' : ↥(BinaryBasefold.MultilinearPoly L ℓ')) : ↥(BinaryBasefold.MultilinearPoly K ℓ)

Unpacking a Packed Multilinear Polynomial. Reverses the packing defined in packMLE. It reconstructs the small-field multilinear t from the large-field multilinear t'.

The evaluation of t at a point (v, w) is recovered by taking the evaluation of t' at w, which is an element of L, and finding its v-th coordinate with respect to the basis β.

noncomputable def Binius.RingSwitching.componentWise_φ₁_embed_MLE (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (ℓ' : ℕ) (t' : ↥(BinaryBasefold.MultilinearPoly L ℓ')) : ↥(BinaryBasefold.MultilinearPoly (TensorAlgebra K L) ℓ')

Component-wise φ₁ embedding. Takes a polynomial t' with coefficients in L and embeds it into a polynomial with coefficients in the tensor algebra A by applying φ₁ to each coefficient. This is achieved by using MvPolynomial.map.

Enhanced Protocol Type Definitions (Interfaces between phases)

We define the Statement and Witness types at the boundaries of each phase following the enhanced specification.

@[reducible, inline]

abbrev Binius.RingSwitching.MLPEvalStatement (L : Type) (ℓ : ℕ) : Type

structure Binius.RingSwitching.WitMLP (K : Type) [Field K] (ℓ : ℕ) : Type

• t : ↥(BinaryBasefold.MultilinearPoly K ℓ)

structure Binius.RingSwitching.BatchingWitIn (L : Type) [Field L] (K : Type) [Field K] (ℓ ℓ' : ℕ) : Type

• t : ↥(BinaryBasefold.MultilinearPoly K ℓ)
• t' : ↥(BinaryBasefold.MultilinearPoly L ℓ')

structure Binius.RingSwitching.BatchingStmtIn (L : Type) (ℓ : ℕ) : Type

• t_eval_point : Fin ℓ → L
• original_claim : L

structure Binius.RingSwitching.RingSwitchingBaseContext (κ : ℕ) (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (ℓ : ℕ) extends Binius.BinaryBasefold.SumcheckBaseContext L ℓ : Type

• t_eval_point : Fin ℓ → L
• original_claim : L
• s_hat : TensorAlgebra K L
• r_batching : Fin κ → L

structure Binius.RingSwitching.SumcheckWitness (L : Type) [Field L] (ℓ' : ℕ) (i : Fin (ℓ' + 1)) : Type

• t' : ↥(BinaryBasefold.MultilinearPoly L ℓ')
• H : ↥(MvPolynomial.restrictDegree (Fin (ℓ' - ↑i)) L 2)

structure Binius.RingSwitching.MLIOPCSStmt (L : Type) (ℓ' : ℕ) : Type

• point : Fin ℓ' → L
• evaluation : L

def Binius.RingSwitching.MLPEvalRelation (L : Type) [Field L] (ℓ' : ℕ) (ιₛᵢ : Type) (OStmtIn : ιₛᵢ → Type) (input : (MLPEvalStatement L ℓ' × ((j : ιₛᵢ) → OStmtIn j)) × WitMLP L ℓ') : Prop

Standard input relation for MLIOPCS: polynomial evaluation at point equals claimed evaluation

structure Binius.RingSwitching.AbstractOStmtIn (L : Type) [Field L] (ℓ' : ℕ) : Type 1

• ιₛᵢ : Type
• OStmtIn : self.ιₛᵢ → Type
• Oₛᵢ (i : self.ιₛᵢ) : OracleInterface (self.OStmtIn i)
• initialCompatibility : ↥(BinaryBasefold.MultilinearPoly L ℓ') × ((j : self.ιₛᵢ) → self.OStmtIn j) → Prop

def Binius.RingSwitching.AbstractOStmtIn.toRelInput (L : Type) [Field L] (ℓ' : ℕ) (aOStmtIn : AbstractOStmtIn L ℓ') : Set ((MLPEvalStatement L ℓ' × ((j : aOStmtIn.ιₛᵢ) → aOStmtIn.OStmtIn j)) × WitMLP L ℓ')

structure Binius.RingSwitching.MLIOPCS (L : Type) [Field L] (ℓ' : ℕ) extends Binius.RingSwitching.AbstractOStmtIn L ℓ' : Type 1

• ιₛᵢ : Type
• OStmtIn : self.ιₛᵢ → Type
• Oₛᵢ (i : self.ιₛᵢ) : OracleInterface (self.OStmtIn i)
• initialCompatibility : ↥(BinaryBasefold.MultilinearPoly L ℓ') × ((j : self.ιₛᵢ) → self.OStmtIn j) → Prop
• numRounds : ℕ

  Protocol specification

• pSpec : ProtocolSpec self.numRounds
• Oₘ (j : self.pSpec.MessageIdx) : OracleInterface (self.pSpec.Message j)
• O_challenges (i : self.pSpec.ChallengeIdx) : SampleableType (self.pSpec.Challenge i)
• oracleReduction : OracleReduction []ₒ (MLPEvalStatement L ℓ') self.OStmtIn (WitMLP L ℓ') Bool (fun (x : Empty) => Unit) Unit self.pSpec
• perfectCompleteness {σ : Type} {init : ProbComp σ} {impl : QueryImpl []ₒ (StateT σ ProbComp)} : OracleReduction.perfectCompleteness init impl (AbstractOStmtIn.toRelInput L ℓ' self.toAbstractOStmtIn) acceptRejectOracleRel self.oracleReduction
• rbrKnowledgeError : self.pSpec.ChallengeIdx → NNReal
• rbrKnowledgeSoundness {σ : Type} {init : ProbComp σ} {impl : QueryImpl []ₒ (StateT σ ProbComp)} : OracleVerifier.rbrKnowledgeSoundness init impl (AbstractOStmtIn.toRelInput L ℓ' self.toAbstractOStmtIn) acceptRejectOracleRel self.oracleReduction.verifier self.rbrKnowledgeError

@[implicit_reducible]

instance Binius.RingSwitching.instOstmtMLIOPCS (L : Type) [Field L] (ℓ' : ℕ) (aOStmtIn : AbstractOStmtIn L ℓ') (i : aOStmtIn.ιₛᵢ) : OracleInterface (aOStmtIn.OStmtIn i)

noncomputable def Binius.RingSwitching.embedded_MLP_eval (κ : ℕ) (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (t' : ↥(BinaryBasefold.MultilinearPoly L ℓ')) (r : Fin ℓ → L) : TensorAlgebra K L

Compute the tensor value ŝ := φ₁(t')(φ₀(r_κ), ..., φ₀(r_{ℓ-1}))

noncomputable def Binius.RingSwitching.performCheckOriginalEvaluation (κ : ℕ) (L : Type) [Field L] [DecidableEq L] (K : Type) [Field K] [Algebra K L] (β : Module.Basis (Fin κ → Fin 2) K L) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (s : L) (r : Fin ℓ → L) (s_hat : TensorAlgebra K L) : Bool

Step 2 (V): Check 1: s ?= Σ_{v ∈ {0,1}^κ} eqTilde(v, r_{0..κ-1}) ⋅ ŝ_v.

noncomputable def Binius.RingSwitching.compute_A_func (κ : ℕ) (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (β : Module.Basis (Fin κ → Fin 2) K L) (ℓ' : ℕ) (original_r_eval_suffix : Fin ℓ' → L) (r''_batching : Fin κ → L) : (Fin ℓ' → Fin 2) → L

Step 4a: For each w ∈ {0,1}^{ℓ'}, P decompose eq̃(r_κ, ..., r_{ℓ-1}, w_0, ..., w_{ℓ'-1}) =: Σ_{u ∈ {0,1}^κ} A_{w, u} ⋅ β_u. P define the function A: w ↦ Σ_{u ∈ {0,1}^κ} eq̃(u_0, ..., u_{κ-1}, r''_0, ..., r''_{κ-1}) ⋅ A_{w, u} on {0,1}^{ℓ'}.

noncomputable def Binius.RingSwitching.compute_A_MLE (κ : ℕ) (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (β : Module.Basis (Fin κ → Fin 2) K L) (ℓ' : ℕ) (original_r_eval_suffix : Fin ℓ' → L) (r''_batching : Fin κ → L) : ↥(BinaryBasefold.MultilinearPoly L ℓ')

Step 4b: P writes A(X_0, ..., X_{ℓ'-1}) for its multilinear extension of A_func.

def Binius.RingSwitching.getEvaluationPointSuffix (κ : ℕ) (L : Type) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (r : Fin ℓ → L) : Fin ℓ' → L

noncomputable def Binius.RingSwitching.RingSwitching_SumcheckMultParam (κ : ℕ) (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (β : Module.Basis (Fin κ → Fin 2) K L) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) : BinaryBasefold.SumcheckMultiplierParam L ℓ' (RingSwitchingBaseContext κ L K ℓ)

Ring-Switching multiplier parameter for sumcheck, using A_MLE as the multiplier.

noncomputable def Binius.RingSwitching.compute_s0 (κ : ℕ) (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (β : Module.Basis (Fin κ → Fin 2) K L) (s_hat : TensorAlgebra K L) (r''_batching : Fin κ → L) : L

Step 5 (V): Compute s₀ := Σ_{u ∈ {0,1}^κ} eqTilde(u, r'') ⋅ ŝ_u, where ŝ_u is the row components of ŝ.

noncomputable def Binius.RingSwitching.compute_final_eq_tensor (κ : ℕ) (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (r : Fin ℓ → L) (r' : Fin ℓ' → L) : TensorAlgebra K L

Compute the tensor e := eq̃(φ₀(r_κ), ..., φ₀(r_{ℓ-1}), φ₁(r'_0), ..., φ₁(r'_{ℓ'-1}))

noncomputable def Binius.RingSwitching.compute_final_eq_value (κ : ℕ) (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (β : Module.Basis (Fin κ → Fin 2) K L) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (r_eval : Fin ℓ → L) (r'_challenges : Fin ℓ' → L) (r''_batching : Fin κ → L) : L

Decompose the final eq tensor e := Σ_{u ∈ {0,1}^κ} eq̃(u, r'') ⨂ e_u, where e_u is the row components of e. Then compute Σ_{u ∈ {0,1}^κ} eq̃(u_0, ..., u_{κ-1}, r''_0, ..., r''_{κ-1}) ⋅ e_u.

def Binius.RingSwitching.witnessStructuralInvariant (κ : ℕ) (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (β : Module.Basis (Fin κ → Fin 2) K L) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) {i : Fin (ℓ' + 1)} (stmt : BinaryBasefold.Statement (RingSwitchingBaseContext κ L K ℓ) i) (wit : SumcheckWitness L ℓ' i) : Prop

This condition ensures that the witness polynomial H has the correct structure A(...) * t'(...)

def Binius.RingSwitching.masterKStateProp (κ : ℕ) (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (β : Module.Basis (Fin κ → Fin 2) K L) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) {𝓑 : Fin 2 ↪ L} (aOStmtIn : AbstractOStmtIn L ℓ') (stmtIdx : Fin (ℓ' + 1)) (stmt : BinaryBasefold.Statement (RingSwitchingBaseContext κ L K ℓ) stmtIdx) (oStmt : (j : aOStmtIn.ιₛᵢ) → aOStmtIn.OStmtIn j) (wit : SumcheckWitness L ℓ' stmtIdx) (localChecks : Prop := True) : Prop

def Binius.RingSwitching.sumcheckRoundRelationProp (κ : ℕ) (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (β : Module.Basis (Fin κ → Fin 2) K L) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) {𝓑 : Fin 2 ↪ L} (aOStmtIn : AbstractOStmtIn L ℓ') (i : Fin (ℓ' + 1)) (stmt : BinaryBasefold.Statement (RingSwitchingBaseContext κ L K ℓ) i) (oStmt : (j : aOStmtIn.ιₛᵢ) → aOStmtIn.OStmtIn j) (wit : SumcheckWitness L ℓ' i) : Prop

def Binius.RingSwitching.sumcheckRoundRelation (κ : ℕ) (L : Type) [Field L] (K : Type) [Field K] [Algebra K L] (β : Module.Basis (Fin κ → Fin 2) K L) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) {𝓑 : Fin 2 ↪ L} (aOStmtIn : AbstractOStmtIn L ℓ') (i : Fin (ℓ' + 1)) : Set ((BinaryBasefold.Statement (RingSwitchingBaseContext κ L K ℓ) i × ((j : aOStmtIn.ιₛᵢ) → aOStmtIn.OStmtIn j)) × SumcheckWitness L ℓ' i)

Input relation for single round: proper sumcheck statement