feat: soundness of FRI-Binius protocols#417
Open
chung-thai-nguyen wants to merge 7 commits intocompleteness-of-biniusfrom
Open
feat: soundness of FRI-Binius protocols#417chung-thai-nguyen wants to merge 7 commits intocompleteness-of-biniusfrom
chung-thai-nguyen wants to merge 7 commits intocompleteness-of-biniusfrom
Conversation
🤖 Gemini PR SummaryMathematical Formalization
Protocol Infrastructure & Refactoring
Proof Status and Critical Gaps
Statistics
Lean Declarations ✏️ **Removed:** 28 declaration(s)
✏️ **Added:** 246 declaration(s)
✏️ **Affected:** 18 declaration(s) (line number changed)
✅ **Removed:** 12 `sorry`(s)
❌ **Added:** 16 `sorry`(s)
🎨 **Style Guide Adherence**This code review is based on the ArkLib style guide. The following violations were identified and grouped by rule: Function SyntaxRule: "Functions: Prefer
Operator and Binder SpacingRule: "Put spaces on both sides of
Tactic Mode and SemicolonsRule: "Avoid using
Line LengthRule: "Line Length: Keep lines under 100 characters."
Documentation StandardsRule: "Every definition and major theorem should have a docstring."
Empty LinesRule: "Avoid empty lines inside definitions or proofs."
Naming ConventionsRule: "Functions and Terms: lowerCamelCase... Prop-valued Classes: Use UpperCamelCase."
📄 **Per-File Summaries**
Last updated: 2026-03-10 05:27 UTC. |
chung-thai-nguyen
force-pushed
the
soundness-of-binius
branch
from
43e8aa7 to
9e0a0ef
Compare
chung-thai-nguyen
requested review from
alexanderlhicks,
dtumad and
quangvdao
and removed request for
quangvdao
🤖 AI Review (with external context)🤖 AI ReviewOverall Summary: 1. TL;DRThe mathematical foundations, protocol abstractions, and probability bounds introduced in this PR are exceptionally robust—particularly the iterated sumcheck phase, Ring-Switching, and Binary Basefold components. However, the PR currently cannot be merged due to multiple compilation-blocking issues (such as the 2. Checklist CoverageNo explicit specification checklist was provided for this PR review. 3. Key Lean 4 / Mathlib Issues
4. Overall VerdictChanges Requested 📄 **Review for `ArkLib.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `ArkLib/Data/Misc/Basic.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `ArkLib/Data/Probability/Instances.lean`**Verdict: Changes Requested Critical Misformalizations: Lean 4 / Mathlib Issues:
Nitpicks:
📄 **Review for `ArkLib/OracleReduction/Basic.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `ArkLib/OracleReduction/Completeness.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks:
📄 **Review for `ArkLib/OracleReduction/Security/RoundByRound.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean`**Verdict: Changes Requested Critical Misformalizations: Lean 4 / Mathlib Issues:
Nitpicks:
📄 **Review for `ArkLib/ProofSystem/Binius/BinaryBasefold/Code.lean`**Verdict: Changes Requested Critical Misformalizations: Lean 4 / Mathlib Issues:
Nitpicks:
📄 **Review for `ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean`**Verdict: Changes Requested Critical Misformalizations: Lean 4 / Mathlib Issues:
Nitpicks: 📄 **Review for `ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean`**Verdict: Changes Requested Critical Misformalizations: Lean 4 / Mathlib Issues:
Nitpicks:
📄 **Review for `ArkLib/ProofSystem/Binius/BinaryBasefold/QueryPhase.lean`**Verdict: Changes Requested Critical Misformalizations: Lean 4 / Mathlib Issues:
have h_point_eq : extractSuffixFromChallenge 𝔽q β v ⟨↑k * ϑ, by omega⟩ (by simp only; omega) =
getFiberPoint 𝔽q β k v (extractMiddleFinMask 𝔽q β v ⟨↑k * ϑ, by omega⟩ ϑ) := by
-- ...
sorryNitpicks:
📄 **Review for `ArkLib/ProofSystem/Binius/BinaryBasefold/ReductionLogic.lean`**Verdict: Needs Minor Revisions Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks:
📄 **Review for `ArkLib/ProofSystem/Binius/BinaryBasefold/Soundness.lean`**Verdict: Changes Requested Critical Misformalizations: Lean 4 / Mathlib Issues:
Nitpicks:
📄 **Review for `ArkLib/ProofSystem/Binius/BinaryBasefold/Spec.lean`**Verdict: Changes Requested Critical Misformalizations: Lean 4 / Mathlib Issues:
Nitpicks: 📄 **Review for `ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean`**Verdict: Changes Requested Critical Misformalizations: Lean 4 / Mathlib Issues:
Nitpicks:
📄 **Review for `ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks:
📄 **Review for `ArkLib/ProofSystem/Binius/FRIBinius/General.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: (aOStmtIn := (BinaryBasefoldAbstractOStmtIn (β := β)
(ϑ := ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate))))This is purely cosmetic, but aligning 📄 **Review for `ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean`**Verdict: Changes Requested Critical Misformalizations: Lean 4 / Mathlib Issues:
Nitpicks:
📄 **Review for `ArkLib/ProofSystem/Binius/RingSwitching/BBFSmallFieldIOPCS.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `ArkLib/ProofSystem/Binius/RingSwitching/BatchingPhase.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks:
📄 **Review for `ArkLib/ProofSystem/Binius/RingSwitching/General.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: (rel₁:=BatchingPhase.batchingInputRelation κ L K β ℓ ℓ'
h_l mlIOPCS.toAbstractOStmtIn)Consider indenting 📄 **Review for `ArkLib/ProofSystem/Binius/RingSwitching/Prelude.lean`**Verdict: Changes Requested Critical Misformalizations: Lean 4 / Mathlib Issues: perfectCompleteness : ∀ {σ : Type} {init : ProbComp σ} {impl : QueryImpl []ₒ (StateT σ ProbComp)},
NeverFail init →
OracleReduction.perfectCompleteness (oSpec:=[]ₒ)
...
(relIn := toAbstractOStmtIn.toStrictRelInput)
(relOut := acceptRejectOracleRel)
(oracleReduction := oracleReduction)
strictPerfectCompleteness : ∀ {σ : Type} {init : ProbComp σ}
{impl : QueryImpl []ₒ (StateT σ ProbComp)},
NeverFail init →
OracleReduction.perfectCompleteness (oSpec:=[]ₒ)
...
(relIn := toAbstractOStmtIn.toStrictRelInput)
(relOut := acceptRejectOracleRel)
(oracleReduction := oracleReduction)This forces users constructing an Nitpicks: 📄 **Review for `ArkLib/ProofSystem/Binius/RingSwitching/Spec.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `ArkLib/ProofSystem/Binius/RingSwitching/SumcheckPhase.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: General Comments:
Great job getting this fully verified! 📄 **Review for `ArkLib/ToMathlib/MvPolynomial/Equiv.lean`**Verdict: Needs Minor Revisions Critical Misformalizations: Lean 4 / Mathlib Issues:
Nitpicks:
📄 **Review for `ArkLib/ToVCVio/Lemmas.lean`**Verdict: Needs Minor Revisions Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks:
📄 **Review for `ArkLib/ToVCVio/Simulation.lean`**Verdict: Changes Requested Critical Misformalizations: Lean 4 / Mathlib Issues:
Nitpicks:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
New version of #296
[x] rbrKnowledgeSoundness of Binary Basefold, Ring-switching, FRI-Binius, simple ring-switching construction (BBFSmallFieldIOPCS), completeness of BBFSmallFieldIOPCS
[x] All soundness lemmas except Lemma 4.25 (Soundness.lean)