Full Binary Basefold Protocol

Sequential composition of:

1. Core Interaction Phase (ℓ rounds of sumcheck + folding, and a final sumcheck)
2. Query Phase (final non-interactive proximity testing)

References

• [DP24] Diamond, Benjamin E., and Jim Posen. "Polylogarithmic Proofs for Multilinears over Binary Towers." Cryptology ePrint Archive (2024).

instance Binius.BinaryBasefold.FullBinaryBasefold.instOracleInterfaceUnitOfEmpty : {x : Empty} → OracleInterface Unit

@[reducible]

noncomputable def Binius.BinaryBasefold.FullBinaryBasefold.fullOracleVerifier {r : ℕ} [NeZero r] {L : Type} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type) [Field 𝔽q] [Fintype 𝔽q] [DecidableEq 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] [h_β₀_eq_1 : Fact (β 0 = 1)] {ℓ 𝓡 ϑ : ℕ} (γ_repetitions : ℕ) [NeZero ℓ] [NeZero 𝓡] [NeZero ϑ] {h_ℓ_add_R_rate : ℓ + 𝓡 < r} [hdiv : Fact (ϑ ∣ ℓ)] : OracleVerifier []ₒ (Statement (SumcheckBaseContext L ℓ) 0) (OracleStatement 𝔽q β ϑ 0) Bool (fun (x : Empty) => Unit) (fullPSpec 𝔽q β γ_repetitions)

The oracle verifier for the full Binary Basefold protocol

@[reducible]

noncomputable def Binius.BinaryBasefold.FullBinaryBasefold.fullOracleReduction {r : ℕ} [NeZero r] {L : Type} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type) [Field 𝔽q] [Fintype 𝔽q] [DecidableEq 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] [h_β₀_eq_1 : Fact (β 0 = 1)] {ℓ 𝓡 ϑ : ℕ} (γ_repetitions : ℕ) [NeZero ℓ] [NeZero 𝓡] [NeZero ϑ] {h_ℓ_add_R_rate : ℓ + 𝓡 < r} {𝓑 : Fin 2 ↪ L} [hdiv : Fact (ϑ ∣ ℓ)] : OracleReduction []ₒ (Statement (SumcheckBaseContext L ℓ) 0) (OracleStatement 𝔽q β ϑ 0) (Witness 𝔽q β 0) Bool (fun (x : Empty) => Unit) Unit (fullPSpec 𝔽q β γ_repetitions)

The reduction for the full Binary Basefold protocol

@[reducible]

noncomputable def Binius.BinaryBasefold.FullBinaryBasefold.fullOracleProof {r : ℕ} [NeZero r] {L : Type} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type) [Field 𝔽q] [Fintype 𝔽q] [DecidableEq 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] [h_β₀_eq_1 : Fact (β 0 = 1)] {ℓ 𝓡 ϑ : ℕ} (γ_repetitions : ℕ) [NeZero ℓ] [NeZero 𝓡] [NeZero ϑ] {h_ℓ_add_R_rate : ℓ + 𝓡 < r} {𝓑 : Fin 2 ↪ L} [hdiv : Fact (ϑ ∣ ℓ)] : OracleProof []ₒ (Statement (SumcheckBaseContext L ℓ) 0) (OracleStatement 𝔽q β ϑ 0) (Witness 𝔽q β 0) (fullPSpec 𝔽q β γ_repetitions)

The full Binary Basefold protocol as a Proof

Security Properties

theorem Binius.BinaryBasefold.FullBinaryBasefold.fullOracleReduction_perfectCompleteness {r : ℕ} [NeZero r] {L : Type} [Field L] [Fintype L] [DecidableEq L] [CharP L 2] [OracleComp.SelectableType L] (𝔽q : Type) [Field 𝔽q] [Fintype 𝔽q] [DecidableEq 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] [h_β₀_eq_1 : Fact (β 0 = 1)] {ℓ 𝓡 ϑ : ℕ} (γ_repetitions : ℕ) [NeZero ℓ] [NeZero 𝓡] [NeZero ϑ] {h_ℓ_add_R_rate : ℓ + 𝓡 < r} {𝓑 : Fin 2 ↪ L} [hdiv : Fact (ϑ ∣ ℓ)] {σ : Type} {init : ProbComp σ} {impl : QueryImpl []ₒ (StateT σ ProbComp)} (hInit : OracleComp.neverFails init) : OracleReduction.perfectCompleteness init impl (roundRelation 𝔽q β 0) acceptRejectOracleRel (fullOracleReduction 𝔽q β γ_repetitions)

Perfect completeness for the full Binary Basefold protocol (reduction)

noncomputable def Binius.BinaryBasefold.FullBinaryBasefold.fullRbrKnowledgeError {r : ℕ} [NeZero r] {L : Type} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ 𝓡 ϑ : ℕ} (γ_repetitions : ℕ) [NeZero ℓ] [NeZero ϑ] {h_ℓ_add_R_rate : ℓ + 𝓡 < r} [hdiv : Fact (ϑ ∣ ℓ)] (i : (fullPSpec 𝔽q β γ_repetitions).ChallengeIdx) : NNReal

Combined RBR knowledge soundness error for the full protocol

theorem Binius.BinaryBasefold.FullBinaryBasefold.fullOracleVerifier_rbrKnowledgeSoundness {r : ℕ} [NeZero r] {L : Type} [Field L] [Fintype L] [DecidableEq L] [CharP L 2] [OracleComp.SelectableType L] (𝔽q : Type) [Field 𝔽q] [Fintype 𝔽q] [DecidableEq 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] [h_β₀_eq_1 : Fact (β 0 = 1)] {ℓ 𝓡 ϑ : ℕ} (γ_repetitions : ℕ) [NeZero ℓ] [NeZero 𝓡] [NeZero ϑ] {h_ℓ_add_R_rate : ℓ + 𝓡 < r} {𝓑 : Fin 2 ↪ L} [hdiv : Fact (ϑ ∣ ℓ)] {σ : Type} {init : ProbComp σ} {impl : QueryImpl []ₒ (StateT σ ProbComp)} : OracleVerifier.rbrKnowledgeSoundness init impl (roundRelation 𝔽q β 0) acceptRejectOracleRel (fullOracleVerifier 𝔽q β γ_repetitions) (fullRbrKnowledgeError 𝔽q β γ_repetitions)

Round-by-round knowledge soundness for the full Binary Basefold oracle verifier