feat: statement for the Binary Basefold protocol

[chung-thai-nguyen]

[x] Full statement for Binary Basefold using Oracle Reduction

---

Note

Introduces a full Binary Basefold protocol framework (specs, verifiers, reductions, core interaction and query phases) and augments AdditiveNTT with domain/fiber, quotient-map, folding, and linearity utilities to support it.

• Binary Basefold Protocol (new):
  • Add scaffold modules: BinaryBasefold.{Prelude,Basic,Steps,CoreInteractionPhase,General,QueryPhase,Spec}.
  • Define protocol specs (pSpec*), oracle statements/interfaces, and per-round verifiers/reductions for fold, relay, commit, and final sumcheck.
  • Implement core interaction (iterated sumcheck + folding) and query phase (proximity tests), with RBR knowledge-soundness and completeness stubs.
• Folding/Domain Utilities (supporting):
  • Define fibers, iterated quotient maps, folding (fold, iterated_fold), and matrix/tensor forms.
  • Add disagreement/distance notions and compliance/bad-event predicates for folding.
• AdditiveNTT Enhancements:
  • Simplify/reshape linearity assumptions; add many lemmas on W, normalizedW, composition, and linear maps.
  • Introduce sDomain basis/size, bijections sDomainFinEquiv, and conversions between indices/points.
  • Provide evaluation polynomial tooling (intermediateEvaluationPoly, refinements) and sumcheck identities.
• Misc:
  • Replace old Binius.Basic import with new Binary Basefold modules.

^{Written by Cursor Bugbot for commit aaa6016. This will update automatically on new commits. Configure here.}

[alexanderlhicks]

/review

External:
https://eprint.iacr.org/2024/504.pdf

Internal:
ArkLib/Data/
ArkLib/OracleReduction/
ArkLib/ProofSystem/Binius/

Comments:

[github-actions]

🤖 AI Review (with external context)\n\nGenerating AI review...

Your pull request has been reviewed. Here is the summary and detailed feedback:

High-level Summary

This pull request introduces a new file to formalize a single round of the Binary Basefold protocol as an interactive oracle reduction. This is a foundational step towards formalizing the complete Binius polynomial commitment scheme. The PR defines the necessary data structures for statements, witnesses, and relations for one round, and outlines the prover and verifier logic within the existing OracleReduction framework.

The overall structure aligns well with the reference paper, and the use of the repository's existing framework is appropriate. However, the implementation is still a work in progress with many key definitions and proofs left as sorry. There are also some correctness concerns, particularly regarding field characteristics and undefined variables.

General Feedback

• Code Organization: The file ArkLib/ProofSystem/Binius/Basic.lean is quite large for a single file. As the implementation grows, it would be beneficial to split it into smaller, more focused files. For example:
  • Binius/BinaryBasefold/Algebra.lean: For algebraic definitions like fold, qMap_fiber, etc.
  • Binius/BinaryBasefold/Round.lean: For the single-round OracleReduction definitions (Statement, Prover, Verifier, etc.).
  • Binius/BinaryBasefold/Protocol.lean: For the sequential composition of rounds to form the full protocol (future work).
• Work-in-Progress State: The extensive use of sorry in both definitions and proofs indicates that this is an initial draft. This is acceptable for an incremental PR, but it's crucial to address the sorrys in key definitions to make the code meaningful. My review will focus on the implemented parts and the overall structure.
• Documentation: The top-level comment describing the protocol is excellent and very helpful for understanding the goal of the formalization.

Specific Feedback & Actionable Suggestions

Here are some specific points that need attention:

1. Missing Characteristic 2 Constraint

Issue: The formalization is for "Binary Basefold", which, as the name and reference paper (Section 4) imply, operates over binary fields (characteristic 2). The current code defines the field L as a generic Field without this constraint. Several algebraic simplifications in the paper rely on this property (e.g., x - y = x + y).

Suggestion: Add a [CharP L 2] constraint to the BinaryBasefold section or relevant definitions. This will make the formalization more accurate with respect to the reference and simplify some proofs.

-- In ArkLib/ProofSystem/Binius/Basic.lean

-- ...
namespace Binius
namespace BinaryBasefold
noncomputable section Esstentials

universe u
variable {r : ℕ} [NeZero r]
-- Add [CharP L 2] constraint
variable {L : Type u} [Field L] [CharP L 2] [Fintype L] [DecidableEq L]
-- ...

end Esstentials
-- ...
end BinaryBasefold
end Binius

2. Incomplete Key Definitions

Issue: Several critical definitions are incomplete and rely on sorry. This prevents the code from being fully understood or verified.

• qMap_fiber: This function is central to the fold operation but is currently sorry.
• OracleStatement: This type definition has a very complex proof obligation (h_sDomainIdx_lt_ℓ) that is also sorry. Placing complex proofs inside type definitions can make them hard to work with.
• fold and iterated_fold have proof obligations that are sorry.

Suggestion:

• Implement qMap_fiber. The comment correctly describes the linear algebra approach; this should be translated into code.
• For OracleStatement, consider proving h_sDomainIdx_lt_ℓ as a separate helper lemma instead of inside the type definition. This will improve readability and modularity.
• Complete the proofs within fold and iterated_fold.

3. Undefined Variable in Soundness Proof

Issue: In verifier_rbrKnowledgeSoundness, the term (deg : ℝ≥0) is used in the error bound, but deg is not defined in the scope.

-- Problematic code in ArkLib/ProofSystem/Binius/Basic.lean
theorem verifier_rbrKnowledgeSoundness [Fintype L] (i : Fin ℓ) :
    ...
    (rbrKnowledgeError:=fun _ => (deg : ℝ≥0) / (Fintype.card L)) := by
  sorry

Suggestion: This variable likely refers to the degree of the sumcheck polynomial h_i, which is 1. Please define it appropriately or replace it with the correct value. For example:

-- Corrected code
theorem verifier_rbrKnowledgeSoundness [Fintype L] (i : Fin ℓ) :
    let deg := 1 -- The degree of the sumcheck polynomial hᵢ(X)
    (verifier ...).rbrKnowledgeSoundness init impl
    ...
    (rbrKnowledgeError:=fun _ => (deg : ℝ≥0) / (Fintype.card L)) := by
  sorry

4. Ambiguity of 𝓑

Issue: The variable 𝓑 : Fin 2 ↪ L is used in definitions like inputRelation and verifier logic (∑ x ∈ (univ.map 𝓑), ...), but it's not defined or passed as a parameter. It is expected to map to {0, 1} in L.

Suggestion: 𝓑 should be explicitly defined or passed as a parameter to the sections and definitions that use it. For clarity, you could define it as:

def boolEmbedding [OfNat L 0] [OfNat L 1] : Fin 2 ↪ L :=
  ⟨fun b => if b = 0 then 0 else 1,
   by intro x y h; cases x; cases y; simp at h; simp [h]; simp at h; contradiction⟩

And then use 𝓑 := boolEmbedding where needed, ensuring L has OfNat instances for 0 and 1.

5. Incomplete Verifier Implementation

Issue: The verify function in the verifier definition is incomplete and relies on sorry.

Suggestion: Implement the full verifier logic. According to the protocol description, it should:

1. Check that the received polynomial h_i has degree at most 1.
2. Perform the sumcheck: stmt.sumcheck_target = h_i.eval 0 + h_i.eval 1.
3. Construct the output statement for the next round.

Your current implementation correctly uses ∑ x ∈ (univ.map 𝓑), h_i.val.eval x for the sumcheck, which is right if 𝓑 maps to {0, 1} and the field has characteristic 2.

Conclusion

This PR represents significant progress towards formalizing the Binius PCS. The overall structure is sound, but it requires filling in the sorrys and addressing the issues mentioned above to become a complete and correct formalization of a Binary Basefold round. Great work so far, and I look forward to seeing the next iteration

[quangvdao]

@chung-thai-nguyen : can you split this PR into multiple parts?

Seems like there are three main protocols: FRI-Binius, Binary-Basefold, and Ring switching (in the binary case)

Each one should be its own PR? Scope the dependencies so there is an ordering to how each PR should be merged.

And what is the difference between FRI-Binius and Binary-Basefold?

[chung-thai-nguyen]

@chung-thai-nguyen : can you split this PR into multiple parts?

Seems like there are three main protocols: FRI-Binius, Binary-Basefold, and Ring switching (in the binary case)

Each one should be its own PR? Scope the dependencies so there is an ordering to how each PR should be merged.

And what is the difference between FRI-Binius and Binary-Basefold?

Yep I will split it into 3 PRs in this order: Binary-Basefold -> Ring switching -> FRI-Binius.
FRI-Binius is a composition of Binary-Basefold and Ring-switching with optimizations.

[alexanderlhicks]

/review

External:
https://eprint.iacr.org/2024/504.pdf

Internal:
ArkLib/Data/
ArkLib/OracleReduction/
ArkLib/ProofSystem/Binius/

Comments:
Please carefully review this PR and identify any issues.

[github-actions]

🤖 AI Review (with external context)\n\nGenerating AI review...

Excellent, this is a substantial pull request that introduces a formalization of the Binius proof system. As an expert code reviewer, I've analyzed the changes in detail, keeping the reference paper, repository context, and best practices in mind. Here is my review:

High-Level Summary

This pull request introduces a large-scale implementation of the Binius proof system, which, according to the reference paper, combines a "ring-switching" technique with a characteristic-2 adaptation of the BaseFold polynomial commitment scheme.

The changes are well-structured, breaking down the protocol into three main components: RingSwitching, BinaryBasefold, and the combined FRIBinius. Each component is further modularized into distinct phases (e.g., BatchingPhase, CoreInteractionPhase, QueryPhase).

The PR also adds foundational utilities to existing files, notably for:

• Additive NTT: Cardinality and bijections for evaluation domains (sDomain).
• Novel Polynomial Basis: A change-of-basis matrix between monomial and novel bases.
• Bitwise Operations: New helper functions for bit manipulation on Nat.

Architecturally, this is a strong foundation for formalizing a complex, state-of-the-art proof system in Lean.

Overall Feedback

This pull request represents a significant and well-thought-out architectural effort. The modular decomposition of the Binius protocol into phases and the use of the OracleReduction framework are excellent design choices that will aid verification and future extensions.

However, the most critical issue is that the implementation is largely a skeleton. A vast majority of the logic and almost all proofs are currently placeholders (sorry). As such, the code is not functional or verifiable in its current state.

Recommendation: I cannot approve this PR for merging in its current state. I recommend breaking this down into a series of smaller, self-contained, and fully proven pull requests. A good approach would be:

1. A PR for the utility functions (Bitwise.lean, AdditiveNTT.lean, NovelPolynomialBasis.lean).
2. Separate PRs for each phase of the RingSwitching and BinaryBasefold protocols, starting from the preludes and moving through the phases.
3. A final PR combining these components into the full FRIBinius system.

This will make the review process more manageable and ensure each component is correct before being built upon.

Specific Issues and Suggestions

Below are specific points of feedback on the code changes.

1. ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean

The additions of sDomain_card and the DomainBijection section are crucial for implementing the protocol. However, they are incomplete.

• Issue: The functions sDomainToFin and finToSDomain, which are supposed to create a bijection between the evaluation domain and Fin _, are filled with sorry. The correctness of the FRI-Binius implementation will heavily depend on these conversions.

  -- ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean:694:8
  noncomputable def sDomainToFin (i : Fin r) (h_i : i < ℓ + R_rate)
    (x : sDomain 𝔽q h_Fq_char_prime h_Fq_card_gt_1 β hβ_lin_indep ℓ R_rate h_ℓ_add_R_rate i) :
    Fin (2^(ℓ + R_rate - i.val)) := by
    -- Get the basis representation of x
    let basis := sDomain_basis 𝔽q h_Fq_char_prime h_Fq_card_gt_1 β hβ_lin_indep ℓ R_rate h_ℓ_add_R_rate i h_i
    let coeffs := basis.repr x
    -- Convert the coefficients to a natural number (binary interpretation)
    let nat_val: ℕ := Finsupp.sum coeffs (fun j c =>
      sorry -- if c = 0 then 0 else 2^j.val
    )
    -- ...

• Suggestion: The sorry within the Finsupp.sum needs to be implemented. This logic should convert the coefficients (which are elements of 𝔽q) into bits to form a natural number. If 𝔽q is GF(2), this is straightforward. For larger 𝔽q, a canonical mapping from field elements to bitstrings is required. The proofs for left_inv and right_inv in sDomainFinEquiv must also be completed.

2. ArkLib/Data/FieldTheory/AdditiveNTT/NovelPolynomialBasis.lean

The new definitions related to the changeOfBasisMatrix are well-structured and correctly identify key properties like being lower-triangular and having a non-zero determinant, which are essential for its invertibility.

• Positive Feedback: The proofs for changeOfBasisMatrix_lower_triangular and changeOfBasisMatrix_diag_ne_zero correctly use the degree properties of the novel polynomial basis, aligning with the theory in the reference paper. The addition of monomialToNovelCoeffs and novelToMonomialCoeffs using this matrix is the correct approach.

3. ArkLib/Data/Nat/Bitwise.lean

New bit manipulation utilities have been added, which appear useful. However, their proofs are missing.

• Issue: The proofs for the properties of joinBits and other new lemmas are sorry. For instance, the proof that joinBits produces a value within the correct range is essential for type safety.

  -- ArkLib/Data/Nat/Bitwise.lean:153:45
  def joinBits {n m : ℕ} (low : Fin (2 ^ n)) (high : Fin (2 ^ m)) : Fin (2 ^ (m+n)) :=
    ⟨(high.val <<< n) ||| low.val, by sorry⟩

• Suggestion: The proof can be completed by showing high.val * 2^n + low.val < 2^(m+n). Given high.val < 2^m and low.val < 2^n, this is provable:
  high.val * 2^n + low.val ≤ (2^m - 1) * 2^n + (2^n - 1) = 2^(m+n) - 2^n + 2^n - 1 = 2^(m+n) - 1.
  Please complete this and all other sorry'd proofs in this file.

4. ArkLib/ProofSystem/Binius/... (New Files)

This is a massive addition of new files, laying out the architecture for the entire Binius system. The structure is logical, but the implementation is almost entirely placeholders.

• Issue: Across all new protocol files (e.g., BatchingPhase.lean, CoreInteractionPhase.lean), key logic is stubbed out. For example, in FRIBinius/BatchingPhase.lean, the central oracleReduction is built by lifting RingSwitching.BatchingPhase.batchingOracleReduction, but the lenses (batchingOracleStmtLens, batchingWitLens) that define this lifting are themselves incomplete.

  -- ArkLib/ProofSystem/Binius/FRIBinius/BatchingPhase.lean:71:4
  def batchingOracleStmtLens : OracleStatement.Lens.{0, 0, 0, 0, 0, 0, 0, 0}
    ... :=
    ⟨fun ⟨stmt, _⟩ => ({
      ...
    }, fun (_ : mlIOPCS.ιₛᵢ) => sorry),
    fun ⟨stmt, ostmt⟩ ⟨inner_out_stmt, _⟩ => ⟨sorry, sorry⟩⟩

• Suggestion: Prioritize implementing the core logic within these sorry blocks. For batchingOracleStmtLens, the projection function needs to correctly construct the input statement for the inner protocol (RingSwitching.BatchingPhase.StmtIn) from the outer one (FRIBinius.InitialStatement). The sorry for the oracle statements also needs to be filled, likely involving a simulation argument.

• Positive Feedback: The use of liftContext to compose protocol phases is an excellent example of compositional design. Once the lenses and base protocols are fully implemented, this structure will be very powerful.

Conclusion

This PR lays down an impressive and well-designed skeleton for the Binius proof system. The modular approach is commendable. However, due to the extensive use of sorry, the code is currently a blueprint rather than a functional implementation. I recommend rejecting this PR in its current form and resubmitting the changes in smaller, complete, and verifiable increments. This will ensure the correctness of the foundational components before the full protocol is assembled.

I look forward to reviewing the subsequent, more focused PRs

[chung-thai-nguyen]

/review

External:
https://eprint.iacr.org/2024/504.pdf

Internal:
ArkLib/Data/
ArkLib/OracleReduction/
ArkLib/ProofSystem/Binius/

Comments:
Please carefully review this PR and identify any issues.

[github-actions]

🤖 AI Review (with external context)\n\nGenerating AI review...

Thank you for the opportunity to review this pull request. Here is my detailed analysis:

High-Level Summary

This pull request introduces a substantial and well-structured implementation of the Binary Basefold polynomial commitment scheme, as described in the reference paper "Polylogarithmic Proofs for Multilinears over Binary Towers". The changes span new protocol specifications, interactive oracle reductions for each protocol step, and their composition into a full protocol. The PR also includes necessary modifications to supporting libraries, particularly for Additive NTT, bitwise operations, and polynomial properties.

The modular design, breaking the complex protocol into smaller, composable OracleReductions, is excellent and will aid in future verification and maintenance.

However, a major concern is that all security proofs (completeness and knowledgeSoundness) for the newly introduced protocol components are currently marked as sorry. While the structure is in place, the core security claims of the implementation are not yet verified.

General Feedback

Correctness and Completeness

1. Missing Security Proofs: The most critical issue is the absence of security proofs for the protocol components. All new OracleReduction and OracleVerifier definitions in Steps.lean, CoreInteractionPhase.lean, and QueryPhase.lean are accompanied by perfectCompleteness and rbrKnowledgeSoundness theorems, but their proofs are sorry. Merging this PR as-is would leave the security of this critical component unverified.

   Recommendation: These sorry proofs must be completed before this PR can be considered for merging. This is a blocker.

2. Potentially Incorrect Type Signature Change in Additive NTT: There is a change to the signature of intermediateNormVpoly in ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean that seems questionable.

   -noncomputable def intermediateNormVpoly (i: Fin (ℓ+1)) (k : Fin (ℓ - i)) : L[X] :=
   +noncomputable def intermediateNormVpoly (i: Fin (ℓ+1)) (k : Fin (ℓ - i + 1)) : L[X] :=

   The index k for the i-th order subspace vanishing polynomials Ŵₖ⁽ⁱ⁾ is expected to range from 0 to ℓ - i - 1, which corresponds to the type Fin (ℓ - i). The change to Fin (ℓ - i + 1) allows k to go up to ℓ - i, which seems inconsistent with its usage in intermediateNovelBasisX and the underlying theory from the reference paper. This discrepancy is also visible in the base_intermediateNormVpoly lemma.

   Recommendation: Please verify the correctness of this type change. If it is intentional, please add comments explaining the reasoning. Otherwise, it should be reverted to Fin (ℓ - i).

Code Style and Readability

1. Monolithic Proofs: Some proofs, particularly in ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean, are very long and complex (e.g., NTTStage_correctness, evenRefinement_eq_novel_poly_of_0_leading_suffix).

   Recommendation: Break down these large proofs into smaller, well-named helper lemmas. This will improve readability, maintainability, and make the proofs easier to verify.

2. Clarity of Bitwise Operations: The file ArkLib/Data/Nat/Bitwise.lean introduces several new bitwise manipulation helpers like joinBits.

   Recommendation: Add docstrings to these new functions to clarify their purpose and, importantly, the endianness convention they assume. This is crucial for anyone trying to understand or use these low-level functions.

File-Specific Feedback

ArkLib/ProofSystem/Binius/BinaryBasefold/QueryPhase.lean

The logic in queryOracleVerifier seems to correctly follow the query phase described in the paper. However, the connection between the declarative proximityChecksSpec and the imperative implementation in queryOracleVerifier is not formally established.

Recommendation: Add a helper lemma or theorem showing that the loop inside queryOracleVerifier correctly implements the logic of proximityChecksSpec. This would strengthen the correctness argument for the verifier.

ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean

In addition to the type signature issue mentioned above, some hypotheses have been removed from function signatures. For example, prod_X_sub_C_eq_X_pow_card_sub_X no longer requires h_Fq_card_gt_1. This simplification is correct because for any Fintype that is a Field, the cardinality is greater than 1. This is a good improvement. Similar changes making instance arguments implicit are also good for usability.

ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean

The definitions for foldOracleProver, foldOracleVerifier, and other step-wise reductions are well-structured. However, as noted before, the security proofs are missing.

For example, in foldOracleReduction_perfectCompleteness:

theorem foldOracleReduction_perfectCompleteness (hInit : init.neverFails) (i : Fin ℓ) :
    OracleReduction.perfectCompleteness
      ... := by
  unfold OracleReduction.perfectCompleteness
  intro stmtIn witIn h_relIn
  simp only
  sorry

Recommendation: Completing this proof would involve showing that an honest prover, starting in a valid state (h_relIn), produces messages that cause the verifier to accept and transition to a valid output state. This is a non-trivial proof that needs to be provided.

Conclusion

This is an impressive piece of work that lays down a solid and detailed foundation for the Binary Basefold protocol. The structure is logical and follows modern software engineering principles by breaking down complexity.

However, the PR cannot be merged in its current state due to the complete absence of security proofs for the protocol itself. The sorrys in all completeness and soundness theorems are critical blockers. Additionally, the potential type signature issue in AdditiveNTT.lean should be addressed.

I recommend the author prioritize filling in the sorry proofs, starting from the smallest components in Steps.lean and building up through composition. Once these are complete, this will be a very valuable contribution to the library.

[github-actions]

🤖 Gemini PR Summary

This diff introduces a comprehensive implementation of the Binary Basefold protocol, a core component of the Binius proof system.

The key changes are:

• New Binary Basefold Protocol Implementation: A large new module, ArkLib/ProofSystem/Binius/BinaryBasefold, has been added. It provides a structured implementation of the protocol, broken down into its constituent parts:

  • Preliminaries and basic definitions (Prelude.lean, Basic.lean).
  • Protocol specifications (Spec.lean).
  • Individual steps like folding and committing (Steps.lean).
  • The main interactive phases (CoreInteractionPhase.lean, QueryPhase.lean).
  • Composition of all parts into the full protocol (General.lean).

• Specialization for Binary Fields (𝔽₂): The underlying libraries for Additive NTT and Novel Polynomial Bases have been specialized to operate over the binary field 𝔽₂, a requirement for Binary Basefold. This involved adding Fintype.card 𝔽q = 2 as a standing assumption.

• New Foundational Tools: To support the protocol's implementation, several new tools and mathematical formalizations were added:

  • A crucial bijection between the abstract algebraic evaluation domains (sDomain) and concrete integer indices (Fin (2^k)) was defined in the AdditiveNTT library.
  • New helper lemmas for bitwise operations (e.g., getMiddleBits, joinBits) were added to support index manipulation.
  • Functions for converting between monomial and novel polynomial basis coefficients have been introduced.

• Code Refactoring and Cleanup: Throughout the modified files, hypotheses were refactored into Lean's Fact typeclass, simplifying function signatures and making proofs cleaner and more idiomatic.

---

Analysis of Changes

Metric	Count
📝 Files Changed	13
✅ Lines Added	6790
❌ Lines Removed	569

---

sorry Tracking

• ❌ Added: 30 sorry(s)
  • def foldKnowledgeStateFunction (i : Fin ℓ) : in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
  • theorem foldCommitOracleReduction_perfectCompleteness in ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean
  • lemma oracleWitnessConsistency_relay_preserved in ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean
  • instance : ∀ i, SelectableType ((pSpecQuery 𝔽q β γ_repetitions in ArkLib/ProofSystem/Binius/BinaryBasefold/Spec.lean
  • theorem commitOracleReduction_perfectCompleteness (hInit : init.neverFails) (i : Fin ℓ) in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
  • def foldMatrix (i : Fin r) (steps : Fin (ℓ + 1)) (h_i_add_steps : i.val + steps < ℓ + 𝓡) in ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean
  • theorem finalSumcheckOracleReduction_perfectCompleteness {σ : Type} in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
  • theorem sumcheckFoldOracleReduction_perfectCompleteness (hInit : init.neverFails) : in ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean
  • theorem foldOracleReduction_perfectCompleteness (hInit : init.neverFails) (i : Fin ℓ) : in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
  • def finalSumcheckKStateProp {m : Fin (1 + 1)} (tr : Transcript m (pSpecFinalSumcheckStep (L in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
  • def commitKState (i : Fin ℓ) (hCR : isCommitmentRound ℓ ϑ i) : in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
  • def queryKStateProp {m : Fin (1 + 1)} in ArkLib/ProofSystem/Binius/BinaryBasefold/QueryPhase.lean
  • theorem foldRelayOracleVerifier_rbrKnowledgeSoundness in ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean
  • theorem sumcheckFoldOracleVerifier_rbrKnowledgeSoundness : in ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean
  • theorem commitOracleVerifier_rbrKnowledgeSoundness (i : Fin ℓ) in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
  • theorem queryOracleProof_perfectCompleteness {σ : Type} in ArkLib/ProofSystem/Binius/BinaryBasefold/QueryPhase.lean
  • theorem finalSumcheckOracleVerifier_rbrKnowledgeSoundness [Fintype L] {σ : Type} in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
  • lemma iterated_fold_transitivity in ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean
  • def relayKnowledgeStateFunction (i : Fin ℓ) (hNCR : ¬ isCommitmentRound ℓ ϑ i) : in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
  • theorem foldOracleVerifier_rbrKnowledgeSoundness (i : Fin ℓ) : in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
  • theorem queryOracleVerifier_rbrKnowledgeSoundness [Fintype L] {σ : Type} (init : ProbComp σ) in ArkLib/ProofSystem/Binius/BinaryBasefold/QueryPhase.lean
  • theorem foldCommitOracleVerifier_rbrKnowledgeSoundness in ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean
  • theorem relayOracleVerifier_rbrKnowledgeSoundness (i : Fin ℓ) in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
  • def sumcheckFoldKnowledgeError in ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean
  • theorem foldRelayOracleReduction_perfectCompleteness in ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean
  • theorem relayOracleReduction_perfectCompleteness (hInit : init.neverFails) (i : Fin ℓ) in ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
  • lemma nonDoomedFoldingProp_relay_preserved (i : Fin ℓ) (hNCR : ¬ isCommitmentRound ℓ ϑ i) in ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean
  • theorem fixFirstVariablesOfMQP_degreeLE {deg : ℕ} (v : Fin (ℓ + 1)) {challenges : Fin v → L} in ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean
  • theorem iterated_fold_eq_matrix_form (i : Fin ℓ) (steps : ℕ) (h_i_add_steps : i + steps ≤ ℓ) in ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean
  • def queryCodeword (j : Fin (toOutCodewordsCount ℓ ϑ (Fin.last ℓ))) in ArkLib/ProofSystem/Binius/BinaryBasefold/QueryPhase.lean

---

Last updated: 2025-10-31 02:10 UTC. See the main CI run for build status.