feat: computable FRI-Binius protocols#455
Draft
chung-thai-nguyen wants to merge 5 commits intocompleteness-of-biniusfrom
Draft
feat: computable FRI-Binius protocols#455chung-thai-nguyen wants to merge 5 commits intocompleteness-of-biniusfrom
chung-thai-nguyen wants to merge 5 commits intocompleteness-of-biniusfrom
Conversation
🤖 Gemini PR SummaryRefactors the Binius protocol suite to transition from noncomputable mathematical specifications to computable, executable implementations. This migration focuses on the oracle specifications and protocol structures for FRI-Binius, Binary Basefold, and Ring Switching. Computable Polynomials & Additive NTT
Protocol & Oracle Refactoring
Proof State and Sorries
Infrastructure & Typeclasses
Statistics
Lean Declarations ✏️ **Removed:** 37 declaration(s)
✏️ **Added:** 243 declaration(s)
✏️ **Affected:** 54 declaration(s) (line number changed)
✅ **Removed:** 1 `sorry`(s)
❌ **Added:** 134 `sorry`(s)
🎨 **Style Guide Adherence**This review follows the ArkLib style guide. There are more than 20 violations, so they have been grouped by rule. Naming Conventions
Syntax and Formatting
Documentation Standards
Variable Conventions
📄 **Per-File Summaries**
Last updated: 2026-04-12 14:44 UTC. |
Collaborator
Author
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a12e702613
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+1069
to
+1071
| (pSpec := pSpecCoreInteraction 𝔽q β (ϑ := ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate)) := by | ||
| let _ := 𝓑 | ||
| sorry |
There was a problem hiding this comment.
coreInteractionOracleVerifier is now an opaque placeholder (sorry) instead of the previous OracleVerifier.append composition of sumcheck-fold and final-sumcheck verifiers. This removes the actual verifier control flow from the executable protocol surface, so downstream constructions that rely on this verifier no longer enforce the intended transcript/message sequence at runtime.
Useful? React with 👍 / 👎.
Comment on lines
+86
to
+87
| | some vIdx => vIdx | ||
| | none => 0 |
There was a problem hiding this comment.
The new index-based query verifier path silently defaults to index 0 when queryPointToIndex cannot find a matching preimage. That changes control flow from a decoding failure into querying the first codeword point, which can make verification depend on unrelated oracle values instead of rejecting malformed/unmapped challenges. This branch should return failure (e.g., Option.none) and propagate rejection.
Useful? React with 👍 / 👎.
Collaborator
Author
There was a problem hiding this comment.
@cursor check again whether all oracle defs in Binius and their dependencies have been migrated? No hidden sorrys & no remaining non-computable oracle defs? All security statements are migrated too?
There was a problem hiding this comment.
Here is a fresh pass over ArkLib/ProofSystem/Binius/ (and the thread’s scope).
Oracle definitions: not fully “migrated” in the strong sense
- Across Binius there are
sorry/admitin many.leanfiles (BinaryBasefold, FRIBinius, RingSwitching, plusSoundness/). A single grep run lists well over 100 occurrences spread across those modules. So the story is not “everything is migrated with no gaps.” - A few files under Binius have no
sorry(e.g.Compliance.lean,Relay.lean,FoldDistance.lean,FRIBinius/Prelude.lean,RingSwitching/Spec.lean,RingSwitching/General.lean), but that is not true for the subtree as a whole.
So: oracle specs and many executable definitions are in place, but proofs and some glue are still explicitly incomplete (sorry).
“Hidden” sorrys
- There is no evidence of hidden axioms: gaps are open
sorryin normal source (plus comments like “Original proof sorry’d for migration” in places such asFold.lean/Commit.lean). Nothing suggests concealedsorrybeyond ordinary repo search.
Non-computable pieces
- Main oracle verifiers / reductions are generally computable
defs where that matters. - Remaining
noncomputableitems are mostly not the core protocol gadgets but things like:coreInteractionOracleRbrKnowledgeError(and the FRIBinius copy): ℝ≥0 error bookkeeping (analysis-style).FinalSumcheck.lean:private noncomputable def finalOracleDecoded*(legacy / abstract decoding helpers).Spec.lean: anoncomputable instanceforFintypeon a query type (often unavoidable with classical finiteness).
- So: some noncomputable remains, but it is not “the whole oracle layer is still abstract”; it is localized (errors, some helpers, classical instances).
Security statements
- Not fully migrated. Examples of unfinished security surface:
BinaryBasefold/General.lean,CoreInteractionPhase.lean,Soundness/*.lean,FRIBinius/General.lean,FRIBinius/CoreInteractionPhase.lean, large parts of RingSwitching and Query soundness, etc., still containsorryon completeness / knowledge / soundness theorems.
- That matches the PR checklist: “Spec migration” checked, “Proof migration” unchecked.
Bottom line: No — you cannot honestly claim “all oracle defs and dependencies migrated, no sorrys, no leftover noncomputable oracle defs, and all security statements migrated.” The repo state is explicitly partial: executable protocol structure is largely there; proofs and some analysis/error paths are still admitted or noncomputable where noted above. If you want this tracked for reviewers, the PR Status section is already accurate; the only “action” from an audit is to keep “Proof migration” unchecked until those sorrys are reduced or replaced.
computable-only - rename coreInteractionOracleReductionExec -> coreInteractionOracleReduction - remove noncomputable coreInteractionOracleReduction - define explicit computable core-interaction reduction composition in CoreInteractionPhase - remove threaded coreInteractionProver workaround from FRIBinius/General wrappers/theorem
This comment was marked as low quality.
This comment was marked as low quality.
Sorry, something went wrong.
This comment was marked as low quality.
This comment was marked as low quality.
Sorry, something went wrong.
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.
Summary
Status
Build
Ran targeted builds for migrated surfaces:
ArkLib.ProofSystem.Binius.BinaryBasefold.SpecArkLib.ProofSystem.Binius.BinaryBasefold.GeneralArkLib.ProofSystem.Binius.FRIBinius.GeneralArkLib.ProofSystem.Binius.RingSwitching.GeneralArkLib.ProofSystem.Binius.RingSwitching.BBFSmallFieldIOPCS