feat: rbrKnowledgeSoundness of BinaryBasefold & ring-switching

[chung-thai-nguyen]

No description provided.

[github-actions]

🤖 Gemini PR Summary

This PR formalizes the Round-by-Round (RBR) knowledge soundness for major components of the Binius proof system, specifically the Binary Basefold and Ring-Switching protocols. It establishes the necessary probability bounds, extraction logic, and simulation infrastructure required for a complete formal security proof in Lean.

Features

• RBR Knowledge Soundness Proofs:
  • Binary Basefold: Implemented round-by-round knowledge soundness for the core interaction phase, query phase, and individual steps (Fold, Commit, Relay, Final).
  • Ring-Switching: Formalized knowledge soundness for the batching phase and sumcheck protocol.
  • FRI-Binius: Completed knowledge soundness and completeness proofs by refactoring sumcheck folding into a logic-step framework.
• Small-Field IOPCS: Instantiated a small-field IOPCS by composing the Ring-Switching protocol with Binary Basefold as the large-field MLIOPCS.
• Mathematical Foundations:
  • Added univariate specializations of the Schwartz-Zippel Lemma and theorems for independent repetitions and union bounds.
  • Added lemmas for MvPolynomial conversions and degree bounds.
  • Introduced the rbrExtractionFailureEvent predicate for a unified framework in soundness proofs.
• Simulation Infrastructure: Introduced reasoning tools for stateful loop simulations and probability notation bridges between VCVio and ArkLib.

Fixes

• Proof Completion: Filled in previously missing proof details for the FRI-Binius core interaction phase and Ring-Switching batching phase.
• Logical Consistency: Resolved gaps in oracle witness-to-statement relations by enforcing strict compatibility and uniqueness properties.
• Probability Bounds: Formally established probability bounds for folding errors and query phase rejections (specifically Lemmas 4.20–4.25).

Refactoring

• Protocol Specification: Refactored the Ring-Switching protocol to reuse Binary Basefold’s final sumcheck step, reducing code duplication.
• Strict Relations: Updated AbstractOStmtIn and MLIOPCS structures to use "strict" initial compatibility relations, which are necessary to distinguish between requirements for perfect completeness vs. knowledge soundness.
• Framework Standardization: Refactored the namespace structure in ReductionLogic and transitioned FRI-Binius steps into a structured "logic-step" framework for better maintainability.
• Oracle Logic: Refactored oracle and folding consistency properties in Binary Basefold to better support preservation lemmas across protocol transitions.

Documentation

No explicit documentation files were modified, but the PR includes significant formalization of protocol specifications and lemmas which serve as the primary technical documentation for the proof system's security properties.

---

Analysis of Changes

Metric	Count
📝 Files Changed	25
✅ Lines Added	10188
❌ Lines Removed	1225

---

sorry Tracking

✅ **Removed:** 9 `sorry`(s)

• theorem foldCommitOracleVerifier_rbrKnowledgeSoundness in ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean
• theorem iteratedSumcheckOracleVerifier_rbrKnowledgeSoundness (i : Fin ℓ') : in ArkLib/ProofSystem/Binius/RingSwitching/SumcheckPhase.lean
• theorem foldRelayOracleVerifier_rbrKnowledgeSoundness in ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean
• theorem finalSumcheckOracleVerifier_rbrKnowledgeSoundness {σ : Type} in ArkLib/ProofSystem/Binius/RingSwitching/SumcheckPhase.lean
• instance : ∀ j, OracleInterface ((pSpecSumcheckRound (L in ArkLib/ProofSystem/Binius/RingSwitching/Spec.lean
• theorem finalSumcheckOracleVerifier_rbrKnowledgeSoundness [Fintype L] {σ : Type} in ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean
• def finalSumcheckKStateProp {m : Fin (1 + 1)} (tr : Transcript m (pSpecFinalSumcheckStep (L in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
• theorem fullOracleVerifier_rbrKnowledgeSoundness {𝓑 : Fin 2 ↪ L} : in ArkLib/ProofSystem/Binius/RingSwitching/General.lean
• def sumcheckFoldKnowledgeError in ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean

❌ **Added:** 19 `sorry`(s)

• lemma oracleWitnessConsistency_commit_step_backward (i : Fin ℓ) (hCR : isCommitmentRound ℓ ϑ i) in ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean
• lemma logical_checkSingleRepetition_of_mem_support_forIn_body {σ : Type} in ArkLib/ProofSystem/Binius/BinaryBasefold/QueryPhase.lean
• lemma sumcheckConsistency_witMLPToWitness0_of_eval in ArkLib/ProofSystem/Binius/RingSwitching/BBFSmallFieldIOPCS.lean
• def bbfMLIOPCS : MLIOPCS L ℓ' where in ArkLib/ProofSystem/Binius/RingSwitching/BBFSmallFieldIOPCS.lean
• lemma foldStep_rbrExtractionFailureEvent_imply_sumcheck_or_badEvent (i : Fin ℓ) in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
• lemma extracted_t_poly_eval_eq_final_constant in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
• def BinaryBasefoldAbstractOStmtIn : (RingSwitching.AbstractOStmtIn (L in ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean
• lemma exists_path_of_mem_support_forIn_unit {σ α : Type} [spec.FiniteRange] in ArkLib/ToVCVio/SimulationInfrastructure.lean
• theorem lemma_4_25_reject_if_suffix_in_disagreement in ArkLib/ProofSystem/Binius/BinaryBasefold/Soundness.lean
• lemma ENNReal.coe_div_of_NNReal {a b : NNReal} : in ArkLib/Data/Nat/Bitwise.lean
• lemma extractMLP_some_of_oracleFoldingConsistency in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
• theorem prop_4_22_bad_event_exists_bound in ArkLib/ProofSystem/Binius/BinaryBasefold/Soundness.lean
• lemma badEventExistsProp_commit_step_backward (i : Fin ℓ) (hCR : isCommitmentRound ℓ ϑ i) in ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean
• theorem soundness_unroll_runToRound_2_pSpec_2 in ArkLib/OracleReduction/Completeness.lean
• lemma mapOStmtOut_eq_mkVerifierOStmtOut_relayStep in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
• lemma badEventExistsProp_relay_preserved (i : Fin ℓ) (hNCR : ¬ isCommitmentRound ℓ ϑ i) in ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean
• lemma oracleWitnessConsistency_relay_preserved' (i : Fin ℓ) (hNCR : ¬ isCommitmentRound ℓ ϑ i) in ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean
• lemma exists_rel_path_of_mem_support_forIn_stateful {ι : Type} {spec : OracleSpec ι} [spec.FiniteRange] in ArkLib/ToVCVio/SimulationInfrastructure.lean
• lemma extractMLP_eq_some_iff_pair_UDRClose (f : (sDomain 𝔽q β h_ℓ_add_R_rate) ⟨0, by omega⟩ → L) in ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean

---

🎨 **Style Guide Adherence**

This review is based on the provided ArkLib Style Guide. Several lines violate naming conventions, formatting rules, and documentation standards.

Naming Convention Violations

• ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean:
  • Line 1858: def strictfinalSumcheckStepFoldingStateProp
    • Violation: "Types and Structures: UpperCamelCase" (also violates lowerCamelCase for terms if intended as a function). It should likely be StrictFinalSumcheck....
• ArkLib/ProofSystem/Binius/BinaryBasefold/Soundness.lean:
  • Line 164: def queryRbrKnowledgeError_singleRepetition
    • Violation: "Functions and Terms: lowerCamelCase".
  • Line 281: def logical_proximityChecksSpec
    • Violation: "Functions and Terms: lowerCamelCase".
• ArkLib/ProofSystem/Binius/RingSwitching/BatchingPhase.lean:
  • Line 443: def batchingRBRKnowledgeError
    • Violation: "Acronyms: Treat as words (HtmlParser not HTMLParser)". Should be batchingRbrKnowledgeError.

Syntax and Formatting Violations

• ArkLib/Data/Misc/Basic.lean:
  • Line 31: lemma fun_eta_expansion {α β : Type*} (f : α → β) : f = (fun x => f x)
    • Violation: "Functions: Prefer fun x ↦ ... over λ x, ..." (The guide follows Lean community standards where ↦ is preferred over =>).
• ArkLib/Data/Nat/Bitwise.lean:
  • Line 84: ... = (((a / b) : NNReal): ENNReal) := by
    • Violation: "Operators: Put spaces on both sides of :".
• ArkLib/Data/Probability/Instances.lean:
  • Line 394: ... [ENNReal.tsum_add];
    • Violation: "Delimiters: Avoid using ; to separate tactics unless writing short, single-line tactic sequences." (Redundant trailing semicolon).
  • Line 512: calc Pr_{ let f ← $ᵖ (Fin (n + 1) → A) }[ P (f (Fin.last n)) ∧ ∀ (i : Fin n), P (f i.castSucc) ]
    • Violation: "Line Length: Keep lines under 100 characters."
  • Line 534: (Finset.filter (fun (p : A × (Fin n → A)) => P p.1 ∧ ∀ (i : Fin n), P (p.2 i)) Finset.univ).card =
    • Violation: "Line Length: Keep lines under 100 characters."
  • Line 550: rw [mul_assoc (a := ((Fintype.card A):ENNReal)⁻¹ * ...)]
    • Violation: "Operators: Put spaces on both sides of :" and "Line Length: Keep lines under 100 characters."
  • Line 615: Pr_{ let r ←$ᵖ (Fin 1 → R) }
    • Violation: "Operators: Put spaces on both sides of ... infix operators" (Missing space around ←).
  • Line 708: _ = Pr_{ let r ←$ᵖ R }[ ... ] := by apply Pr_congr; simp [sub_eq_zero]
    • Violation: "Tactic Mode: Place by at the end of the line preceding the tactic block. Indent the tactic block."
• ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean:
  • Line 760: rw [MvPolynomial.eq_C_of_isEmpty ...]
    • Violation: "Line Length: Keep lines under 100 characters."
• ArkLib/ProofSystem/Binius/BinaryBasefold/QueryPhase.lean:
  • Line 1836: rcases probEvent_relOut_gt_0 with ⟨stmtOut, oStmtOut, h_output_mem_V_run_support, h_relOut⟩
    • Violation: "Line Length: Keep lines under 100 characters."
  • Line 1840: (Empty line)
    • Violation: "Empty Lines: Avoid empty lines inside definitions or proofs."
  • Line 1940: apply OracleReduction.unroll_rbrKnowledgeSoundness (kSF := queryKnowledgeStateFunction ...)
    • Violation: "Line Length: Keep lines under 100 characters."

Documentation and Header Violations

• ArkLib/ProofSystem/Binius/BinaryBasefold/Soundness.lean:
  • Line 1: (Missing Header)
    • Violation: "Headers: Use standard file headers including copyright, license (Apache 2.0), and authors."
• ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean:
  • Line 69: ... captures |Λ| = 1 ...
    • Violation: "Syntax: Use LaTeX for math: $ f(x) = y $ (inline)". Should be $ |\Lambda| = 1 $.

---

📄 **Per-File Summaries**

• ArkLib.lean: This change adds imports for Binary Basefold soundness and multivariate polynomial conversions to the main library file.
• ArkLib/Data/Misc/Basic.lean: Added the fun_eta_expansion_apply lemma to provide an applied version of the function eta expansion identity.
• ArkLib/Data/Nat/Bitwise.lean: Added the lemma ENNReal.coe_div_of_NNReal, which states that the quotient of two NNReal values coerced to ENNReal equals the coercion of their quotient.
• ArkLib/Data/Probability/Instances.lean: This PR adds the union bound, theorems for the probability of independent repetitions, and specific univariate specializations of the Schwartz-Zippel lemma for low-degree polynomials.
• ArkLib/OracleReduction/Completeness.lean: Introduces unroll lemmas and probability simplification theorems for round-by-round knowledge soundness to facilitate reasoning about probabilistic bounds in protocol security proofs.
• ArkLib/OracleReduction/Security/RoundByRound.lean: Added theorems to facilitate the substitution of pointwise-equivalent error terms in round-by-round knowledge soundness definitions.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean: This change refactors oracle and folding consistency properties and introduces preservation lemmas for witness and bad-event predicates across protocol transitions in the Binius Binary Basefold proof system.
• ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean: This change establishes the round-by-round knowledge soundness for the Binius Binary Basefold core interaction phase by composing the soundness proofs of individual protocol rounds and blocks.
• ArkLib/ProofSystem/Binius/BinaryBasefold/QueryPhase.lean: This update refactors the query phase logic to incorporate logical proximity check specifications and completes the formal proof of round-by-round knowledge soundness for the binary Basefold protocol.
• ArkLib/ProofSystem/Binius/BinaryBasefold/ReductionLogic.lean: Refactored the namespace structure and introduced the rbrExtractionFailureEvent predicate to provide a generic framework for round-by-round knowledge soundness proofs.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Soundness.lean: This file formalizes the soundness proof for the Binius Binary Basefold protocol, establishing the probability bounds for folding errors and query phase rejections through Lemmas 4.20–4.25.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Spec.lean: Defined and refactored missing typeclass instances for the Binary Basefold protocol's messages, challenges, and domains.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean: This change implements the round-by-round knowledge soundness proofs for the Binary Basefold protocol's components—including Fold, Commit, Relay, and Final steps—by defining the necessary extractors, knowledge state properties, and extraction failure probability bounds.
• ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean: This update implements the completeness and knowledge soundness proofs for the Binius FRI core interaction phase by refactoring the sumcheck folding and final sumcheck steps into a more structured logic-step framework and filling in previously missing proof details.
• ArkLib/ProofSystem/Binius/FRIBinius/General.lean: This change formalizes the round-by-round knowledge soundness of the FRI-Binius protocol and refactors associated oracle definitions and relations to support this proof.
• ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean: Updated BinaryBasefoldAbstractOStmtIn by adding strict compatibility and uniqueness properties to formally relate oracle witnesses and statements in the Binius FRI protocol.
• ArkLib/ProofSystem/Binius/RingSwitching/BBFSmallFieldIOPCS.lean: Instantiates a small-field IOPCS by composing the Ring-Switching protocol with Binary Basefold as the underlying large-field MLIOPCS, providing a reference implementation with formal proofs for perfect completeness and knowledge soundness.
• ArkLib/ProofSystem/Binius/RingSwitching/BatchingPhase.lean: Formalizes the completeness and knowledge soundness proofs for the Binius ring-switching batching phase by introducing strict relations and completing the extraction logic.
• ArkLib/ProofSystem/Binius/RingSwitching/General.lean: Updates the ring-switching protocol's security properties by adopting strict input relations and completing the round-by-round knowledge soundness proof.
• ArkLib/ProofSystem/Binius/RingSwitching/Prelude.lean: This change introduces strict initial compatibility relations and uniqueness constraints to the AbstractOStmtIn and MLIOPCS structures to distinguish between the requirements for perfect completeness and knowledge-soundness proofs.
• ArkLib/ProofSystem/Binius/RingSwitching/Spec.lean: Refactor the Ring-Switching protocol specification to reuse the Binary Basefold final sumcheck step and simplify associated oracle and typeclass instances.
• ArkLib/ProofSystem/Binius/RingSwitching/SumcheckPhase.lean: This change implements the round-by-round knowledge soundness proofs for the Ring Switching sumcheck protocol by defining the necessary extractors and knowledge state properties.
• ArkLib/ToMathlib/MvPolynomial/Equiv.lean: Adds lemmas proving that Polynomial.toMvPolynomial preserves non-zero values and that its total degree is bounded by the original polynomial's natural degree.
• ArkLib/ToVCVio/Lemmas.lean: Adds lemmas characterizing the support and mapping behavior of StateT computations within OracleComp.
• ArkLib/ToVCVio/SimulationInfrastructure.lean: Adds reasoning infrastructure for stateful loop simulations and bridges probability notations between VCVio and ArkLib.

---

Last updated: 2026-02-12 17:05 UTC.

[alexanderlhicks]

FYI I'll merge the 4.26 PR first, so keep an eye out for any proofs breaking when that happens.

[chung-thai-nguyen]

@alexanderlhicks Sure I will take a look.