feat: even more general ring switch by alexanderlhicks · Pull Request #615 · Verified-zkEVM/ArkLib

alexanderlhicks · 2026-07-07T15:37:46Z

Further generalization of the ring-switching abstraction based on discussion around https://github.com/leanEthereum/leanVM-b/blob/main/misc/ring-switching-generalized.pdf and Flock.
WIP, but should not be a huge PR once the generic layer (mostly in the current draft) is in place, binius and hachi (if the ring switching stage is reached before this is merged) will be ported accordingly.

github-actions · 2026-07-07T15:41:46Z

🤖 PR Summary

This PR generalizes the ring-switching layer to decoupled packing and opening algebras, as documented in Flock (BRW26) and the internal note RSG. The core change is the introduction of the Generic ring-switching subdirectory (ArkLib/ProofSystem/RingSwitching/Generic/) with five new files that define and prove the foundational structures, packing correctness, batching separation, recombination injectivity, a fixed relation chain, and a PCS binding interface. Supporting infrastructure is added under ArkLib/Data/ (module basis lemmas, MvPolynomial degree bounds, probability oracle compiler bridge) and ArkLib/OracleReduction/ (challenge round factoring). A bug fix in the Binius FRI CoreInteractionPhase replaces a silent diagonal evaluation with the corrected witnessNovelCoeffs. The PR is structurally complete with all new files carrying no sorry or admit.

Statistics

Metric	Count
📝 Files Changed	19
✅ Lines Added	2342
❌ Lines Removed	12

Lean Declarations

✏️ Added: 110 declaration(s)

ArkLib/Data/Module/Basis.lean (2)

theorem sum_smul_bijective (b : Basis ι R M) :
theorem sum_smul_injective (b : Basis ι R M) :

ArkLib/Data/MvPolynomial/Degrees.lean (1)

theorem totalDegree_le_card_of_degreeOf_le_one [Fintype σ] (p : MvPolynomial σ R)

ArkLib/Data/MvPolynomial/Multilinear.lean (4)

theorem MLE_eval_eq_sum_eqTilde (evals : (σ → Fin 2) → R) (r : σ → R) :
theorem MLE_totalDegree_le (evals : (σ → Fin 2) → R) :
theorem aeval_multilinear_eq_sum_eqTilde {A : Type*} [CommRing A] [Algebra R A] [IsDomain A]
theorem coe_boolFun_eq_ite [AddMonoidWithOne R] (u : σ → Fin 2) :

ArkLib/Data/Probability/Instances.lean (1)

lemma prob_schwartz_zippel_single_variable {R : Type} [CommRing R] [IsDomain R] [Fintype R]

ArkLib/Data/Probability/OracleCompBridge.lean (2)

theorem probEvent_bind_uniformSample_le {A : Type} (ma : ProbComp A)
theorem probEvent_uniformSample_eq_pr_uniformOfFintype (E : C → Prop) :

ArkLib/OracleReduction/Security/ChallengeRound.lean (2)

theorem probEvent_challengeRound_le
theorem probEvent_rbrGame_le

ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean (2)

def witnessNovelCoeffs (t : L⦃≤ 1⦄[X Fin ℓ]) : Fin (2^ℓ) → L
example :

ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean (2)

def biniusCommitsTo
lemma initialCompatibility_eq_biniusCommitsTo :

ArkLib/ProofSystem/RingSwitching/Generic/Batching.lean (14)

def decoupledFieldCarrier : RingSwitchCarrier (ZMod 2) where
def eqFold (κ : ℕ) : BatchingStrategy P (Fin κ → Fin 2) where
def gammaPowers (e : ℕ) : BatchingStrategy P (Fin e) where
def reindex {P : Type} [CommRing P] {W : Type} [Fintype W] (bat : BatchingStrategy P W)
example (P : Type) [CommRing P] [IsDomain P] [Fintype P] (e : ℕ) :
example (P : Type) [CommRing P] [IsDomain P] [Fintype P] (κ : ℕ) :
example : BatchingStrategy (ZMod 3) (Fin (2 ^ 2))
example : BatchingStrategy (ZMod 3) (Fin 3)
example : Type 1
example : decoupledFieldCarrier.P = GaloisField 2 2
example :
example :
example :
example :

ArkLib/ProofSystem/RingSwitching/Generic/Carrier.lean (15)

def Bmult {m : ℕ} (r : Fin m → car.E) (weight : car.ιE → car.P) : MultilinearPoly car.P m
def boolToE {m : ℕ} (y : Fin m → Fin 2) : Fin m → car.E
def bridge (weight : car.ιE → car.P) : car.E →ₗ[B] car.P
def decoupledToyCarrier : RingSwitchCarrier (ZMod 2) where
def eqCoord {m : ℕ} (r : Fin m → car.E) (y : Fin m → Fin 2) (u : car.ιE) : B
def packedMLE {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) : MultilinearPoly car.P m
def towerCarrier {K L : Type} [Field K] [Field L] [Algebra K L]
example (Ps : decoupledToyCarrier.ιP → MultilinearPoly (ZMod 2) 3) :
example (r : Fin 3 → decoupledToyCarrier.E) (w : decoupledToyCarrier.ιE → decoupledToyCarrier.P) :
example (r : Fin 3 → decoupledToyCarrier.E) (y : Fin 3 → Fin 2) (u : decoupledToyCarrier.ιE) :
example (r : Fin 3 → decoupledToyCarrier.E) (y : Fin 3 → Fin 2)
example (w : decoupledToyCarrier.ιE → decoupledToyCarrier.P) :
example : RingSwitchCarrier (ZMod 2)
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L) :
theorem bridge_eqTilde {m : ℕ} (r : Fin m → car.E) (y : Fin m → Fin 2)

ArkLib/ProofSystem/RingSwitching/Generic/Packing.lean (14)

def curryFamily {κ ℓ ℓ' : ℕ} {K : Type} [CommRing K] (h_l : ℓ = ℓ' + κ)
def unpack {m : ℕ} (t' : MultilinearPoly car.P m) : car.ιP → MultilinearPoly B m
example (Ps : decoupledToyCarrier.ιP → MultilinearPoly (ZMod 2) 3) (pt : Fin 3 → ZMod 2) :
example (Ps : decoupledToyCarrier.ιP → MultilinearPoly (ZMod 2) 3) :
example (t' : MultilinearPoly decoupledToyCarrier.P 3) :
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L) (m : ℕ) :
theorem packMLE_eq_packedMLE_curry {κ : ℕ} [NeZero κ] {K L : Type} [Field K] [Field L] [Algebra K L]
theorem packedMLE_eval {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) (pt : Fin m → B) :
theorem packedMLE_surjective {m : ℕ} :
theorem packedMLE_unpack {m : ℕ} (t' : MultilinearPoly car.P m) :
theorem packedMLE_val {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) :
theorem unpack_coeff {m : ℕ} (t' : MultilinearPoly car.P m) (i : car.ιP) (d : Fin m →₀ ℕ) :
theorem unpack_eval_zeroOne {m : ℕ} (t' : MultilinearPoly car.P m) (i : car.ιP)
theorem unpack_packedMLE {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) :

ArkLib/ProofSystem/RingSwitching/Generic/Recombine.lean (7)

example : Function.Injective
example : Function.Injective
example : Function.Injective
example {K L : Type} [Field K] [Field L] [Algebra K L] {ι : Type} [Fintype ι]
theorem openingDecomposition_injective :
theorem recombine_bijective :
theorem recombine_injective :

ArkLib/ProofSystem/RingSwitching/Generic/Reduction.lean (22)

def PhasePrvState : Fin (2 + 1) → Type
def honestSlices {m : ℕ} (r : Fin m → car.E) (t' : MultilinearPoly car.P m) :
def pSpecRingSwitchPhase : ProtocolSpec 2
def phaseRBRError : (pSpecRingSwitchPhase car bat).ChallengeIdx → ℝ≥0
def phaseRelIn :
def phaseRelOut :
def phaseWitMid : Fin (2 + 1) → Type
def ringSwitchPhase :
def ringSwitchPhaseProver :
def ringSwitchPhaseRBRKnowledgeSound {σ : Type} (init : ProbComp σ)
def ringSwitchPhaseVerifier :
example (i : (pSpecRingSwitchPhase car bat).ChallengeIdx) (h : i.1 = 1) :
example (r : Fin 3 → decoupledToyCarrier.E)
example :
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L)
example {σ : Type} (init : ProbComp σ) (impl : QueryImpl []ₒ (StateT σ ProbComp)) :
noncomputable def phaseKnowledgeStateFunction [IsDomain car.E] :
noncomputable def phaseRbrExtractor :
private lemma pr_eq_zero_of_forall_not {α : Type} (D : PMF α) (P : α → Prop)
private theorem phase_badEvent_le
theorem honestSlices_mem_sliceRel {m : ℕ} (r : Fin m → car.E)
theorem ringSwitchPhase_rbrKnowledgeSound [IsDomain car.E] {σ : Type} (init : ProbComp σ)

ArkLib/ProofSystem/RingSwitching/Generic/Relations.lean (22)

def claimConsistent (α : car.ιP → car.E) (s : car.ιE → car.P) : Prop
def evalRel (pc : PackedCommitment P m) :
def openingClaimRel (m : ℕ) :
def sliceRel (m : ℕ) (r : Fin m → car.E) :
def sumcheckClaimRel (m : ℕ) (r : Fin m → car.E) (w : car.ιE → car.P) :
def trivial (P : Type) [CommRing P] (m : ℕ) : PackedCommitment P m where
example (r : Fin 3 → decoupledToyCarrier.E) (w : decoupledToyCarrier.ιE → decoupledToyCarrier.P) :
example (r : Fin 3 → decoupledToyCarrier.E) :
example (α : decoupledToyCarrier.ιP → decoupledToyCarrier.E)
example : PackedCommitment decoupledToyCarrier.P 3
example : Type 1
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L) :
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L)
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L)
example {m : ℕ} {r : Fin m → decoupledFieldCarrier.E}
example {m : ℕ} {r : Fin m → decoupledFieldCarrier.E}
theorem aeval_unpack_of_slices [IsDomain car.E] {m : ℕ} {r : Fin m → car.E}
theorem claimConsistent_of_slices [IsDomain car.E] {m : ℕ} {r : Fin m → car.E}
theorem commitsTo_ne_top [Nontrivial P] (pc : PackedCommitment P m) :
theorem commitsTo_not_top [Nontrivial P] (pc : PackedCommitment P m) (c : ∀ j, pc.OStmt j) :
theorem openingClaimRel_of_claimConsistent [IsDomain car.E] {m : ℕ} {r : Fin m → car.E}
theorem sumcheckClaim_of_slices {m : ℕ} {r : Fin m → car.E}

sorry Tracking

No sorrys were added, removed, or affected.

📋 **Additional Analysis**

The diff introduces a large new generic ring-switching layer, fixes a bug in BinaryBasefold, and updates documentation. Overall it follows the ArkLib style guide closely, but a few minor violations were found.

📄 **Per-File Summaries**

ArkLib.lean: Added 9 new imports to ArkLib.lean: ArkLib.Data.Module.Basis, ArkLib.Data.Probability.OracleCompBridge, ArkLib.OracleReduction.Security.ChallengeRound, and six modules under ArkLib.ProofSystem.RingSwitching.Generic (Batching, Carrier, Packing, Recombine, Reduction, Relations). These imports extend the project's support for module bases, a probability oracle compiler bridge, a challenge round in oracle reduction security, and generic ring-switching components in the proof system.
ArkLib/Data/Module/Basis.lean: This new file ArkLib/Data/Module/Basis.lean adds two lemmas to the Module.Basis namespace (for Fintype index types) that characterize the finite R-linear recombination map s ↦ ∑ i, s i • b i associated to a basis b. sum_smul_bijective proves this map is bijective by identifying it with b.equivFun.symm (whose bijectivity follows from equivFun being an isomorphism). sum_smul_injective then derives the corollary that distinct coordinate tuples recombine to distinct module elements. Introducing these lemmas provides a common, reusable reference for both directions of a free-module "pack/unpack" argument, such as those arising in ring-switching proofs.
ArkLib/Data/MvPolynomial/Degrees.lean: Added theorem totalDegree_le_card_of_degreeOf_le_one (in the DegreeOf section) which states that if p : MvPolynomial σ R with Fintype σ satisfies degreeOf i p ≤ 1 for all i, then totalDegree p ≤ Fintype.card σ. This provides a bound on total degree for polynomials that are degree‑at‑most‑1 in each variable, e.g. multilinear polynomials.
ArkLib/Data/MvPolynomial/Multilinear.lean: Added coe_boolFun_eq_ite to relate the Fin 2 → R coercion to an if‑then‑else representation. Added MLE_eval_eq_sum_eqTilde expressing evaluation of the multilinear extension at an arbitrary point as a sum over the hypercube with the eq‑indicator. Added MLE_totalDegree_le bounding the total degree of the multilinear extension by the number of variables. Added aeval_multilinear_eq_sum_eqTilde (with a [IsDomain A] hypothesis) giving an expansion of the aeval of a multilinear polynomial over an R‑algebra in terms of its evaluations on the hypercube.
ArkLib/Data/Probability/Instances.lean: The Schwartz-Zippel lemma prob_schwartz_zippel_mv_polynomial is generalized: its hypothesis now requires a degree bound d : ℕ (renamed from n) and its conclusion gives probability ≤ d / |R| rather than n / |R|. A new lemma prob_schwartz_zippel_single_variable is added: for a non-zero one-variable polynomial f (as an MvPolynomial (Fin 1) R) with total degree ≤ d, the probability it vanishes at a uniformly random point of R is ≤ d / |R|; it is proved by reducing to the multivariate form via prob_uniform_singleton_finFun_eq and Pr_congr.
ArkLib/Data/Probability/OracleCompBridge.lean: This new file ArkLib/Data/Probability/OracleCompBridge.lean introduces two theorems that connect probability statements over VCVio's OracleComp to those over PMF sampling notation, enabling translation between round-by-round security games and per-round error analyses. probEvent_uniformSample_eq_pr_uniformOfFintype equates the event probability of a uniform query $ᵗ C to the PMF-level probability under PMF.uniformOfFintype C. probEvent_bind_uniformSample_le provides a bound for the OracleComp bind of a transcript prefix ma followed by a uniform challenge $ᵗ C, given a per-prefix PMF-level bound, which is the probability core of factoring an RBR (round-by-round) game. The file also establishes the imports VCVio and ArkLib.Data.Probability.Instances with a comment noting the layering precedent.
ArkLib/OracleReduction/Security/ChallengeRound.lean: This new file (ArkLib/OracleReduction/Security/ChallengeRound.lean) introduces two theorems in the Verifier namespace that factor the probability analysis of a single challenge round in round-by-round (RBR) games. probEvent_challengeRound_le proves that if for every fixed prefix outcome a, the PMF-level probability of a bad event q under a uniform challenge is bounded by ε, then the entire game (prefix computation, uniform challenge draw via challengeQueryImpl, and post-processing) also has probability at most ε. probEvent_rbrGame_le is a specialized variant that directly matches the let-bind shape used in Verifier.rbrKnowledgeSoundness (with Prover.runWithLogToRound), providing the same bound without requiring the destructuring bind to be unfolded by whnf. Both theorems are stated over an arbitrary oSpec implementation impl, range over an arbitrary A and β, and use simulateQ with impl.addLift challengeQueryImpl to represent the game's execution.
ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean: Added witnessNovelCoeffs to correctly encode a multilinear witness's Boolean-hypercube table using LSB-first bit ordering (Nat.getBit), replacing the previous inline fun ω => t.val.eval ω which, due to a silent coercion, evaluated at a constant point, making the encoding non‑injective and the consistency predicates vacuously loose. This fix is applied in getMidCodewords and firstOracleWitnessConsistencyProp, both of which now use witnessNovelCoeffs. A regression check (example) verifies that X 0 and X 1 are now distinguished at index 1.
ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean: This commit fixes an incorrect call in the sumcheckFoldLens definition inside CoreInteractionPhase.lean. Previously, the lambda fun ω => t.val.eval ω incorrectly used the diagonal evaluations of t; it has been replaced with BinaryBasefold.witnessNovelCoeffs (L := L) t, which correctly reads t's cube table (LSB-first) as required. A comment block explains the reasoning and references a prior fix ("R7 fix"). No sorry or admit were added.
ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean: Added the biniusCommitsTo definition, which re-expresses BinaryBasefoldAbstractOStmtIn.initialCompatibility as a commitsTo-oriented predicate for the generic PCS interface, along with the lemma initialCompatibility_eq_biniusCommitsTo proving definitional equality. The docstring notes that the underlying predicate now correctly reads t's cube table via witnessNovelCoeffs (fixing a non-injective encoding issue from the S5 close-review).
ArkLib/ProofSystem/RingSwitching/Generic/Batching.lean: This new file introduces the generic batching separation framework for ring-switching, defining the BatchingStrategy structure (with fields Challenge, weight, error, and a separates theorem) and two proven instances: gammaPowers (γ-power random linear combination, error e/|P|, universal claim count) and eqFold (eq-indicator folding, error κ/|P|, power-of-two claim counts). It provides a reindex method to transport a strategy along a claim-index equivalence, enabling S6 to land instances onto a carrier's opening index. The file also defines decoupledFieldCarrier (P = 𝔽₄, E = 𝔽₈) over ZMod 2 to exercise the [IsDomain P]-gated results, and includes a sanity block with rfl error-bound pins and instantiation examples verifying that the framework applies to concrete fields and the decoupled carrier. No sorry or admit appear.
ArkLib/ProofSystem/RingSwitching/Generic/Carrier.lean: This new file introduces RingSwitchCarrier, a structure parameterized by two unrelated B-algebras P and E (each with a B-basis), which serves as the definitional core of the generic ring-switch layer. It defines the packing primitive packedMLE, the eq-decomposition coordinate function eqCoord, the linear bridge map bridge, the auxiliary Bmult multilinear, and proves the key identity bridge_eqTilde linking them via openBasis.repr. Two concrete instances are provided: towerCarrier (where P = E) and decoupledToyCarrier (where P ≠ E over ZMod 2), accompanied by sanity checks that exercise all definitions on both carriers, ensuring the layer does not inadvertently assume P = E.
ArkLib/ProofSystem/RingSwitching/Generic/Packing.lean: This new file introduces the generic packing correctness for ring-switching, proving the semantic content of packing via packedMLE_eval (evaluation at base-embedded points reassembles base evaluations against the packing basis). It also provides the generic unpacking section with unpack, packedMLE_unpack, unpack_packedMLE, packedMLE_surjective, and unpack_eval_zeroOne, establishing a round-trip bijection over any CommRing. Additionally, it proves the Binius-stability bridge packMLE_eq_packedMLE_curry (label 'R2') identifying the DP24 rank-2^κ variable-splitting packMLE with the generic packedMLE applied to the curried family curryFamily.
ArkLib/ProofSystem/RingSwitching/Generic/Recombine.lean: This new file adds the generic ring-switching recombination injectivity theorems recombine_bijective, recombine_injective, and openingDecomposition_injective. The first two establish that the packing-basis recombination (step 4, safe-core (iii)) is bijective—hence injective—as required for soundness per Remark 5 of [BRW26], while the third proves injectivity of the opening-basis decomposition, pinning uniqueness of B-coordinates. The file also includes concrete sanity tests exercising these results on both the tower carrier and the decoupled toy carrier, demonstrating that no domain or field hypotheses are needed (pure CommRing + Basis theory).
ArkLib/ProofSystem/RingSwitching/Generic/Reduction.lean: This commit introduces ArkLib/ProofSystem/RingSwitching/Generic/Reduction.lean, a new file that implements the concrete hand-written ring-switch phase (ProtocolSpec 2) for the generic ring-switching construction. It defines the protocol specification (pSpecRingSwitchPhase), the honest prover's slices (honestSlices) and its prover (ringSwitchPhaseProver), the verifier with a critical claim-consistency check against the input claims (ringSwitchPhaseVerifier), and the combined oracle reduction (ringSwitchPhase). The file establishes the phase's input and output relations (phaseRelIn, phaseRelOut), the round-by-round knowledge error vector (phaseRBRError), and provides the full RBR knowledge-soundness infrastructure: intermediate witness types (phaseWitMid), an extractor (phaseRbrExtractor), a knowledge state function (phaseKnowledgeStateFunction), a bounding lemma for the challenge round's bad event (phase_badEvent_le), and the main theorem ringSwitchPhase_rbrKnowledgeSound (conditioned on [IsDomain car.E]). The module also includes a Sanity section with testable examples instantiating the phase on concrete carriers (tower and decoupled-field) and a pin verifying that the error vector equals the batching strategy's separation error at the challenge round. No sorry or admit is present in this file.
ArkLib/ProofSystem/RingSwitching/Generic/Relations.lean: This new file ArkLib/ProofSystem/RingSwitching/Generic/Relations.lean defines the framework-fixed relation chain (safety pillar 4) and the PCS binding interface (safety pillar 2) for the generic ring-switching layer, adding 450 lines of Lean code. Under RingSwitchCarrier it introduces the anchor relation openingClaimRel (evaluation claims at point r), the intermediate sliceRel (eq-weighted hypercube sums), the batched sumcheckClaimRel, and the chain-coherence theorem sumcheckClaim_of_slices. It also defines the Remark-5 consistency check claimConsistent (comparing claims against slices via both bases), the core theorem aeval_unpack_of_slices (with [IsDomain car.E]), and the completeness/soundness theorems claimConsistent_of_slices and openingClaimRel_of_claimConsistent. The PCS interface is provided by the structure PackedCommitment with the binding predicate commitsTo, its functionality law commitsTo_functional, and the enforcement theorems commitsTo_not_top and commitsTo_ne_top (closing design Hole A). evalRel combines MLPEvalRelation with commitsTo as the anchored input relation. The structure DenseMLPCS extends PackedCommitment with a protocol specification, perfect completeness, and round-by-round knowledge soundness, all stated against the fixed evalRel. A Sanity section includes non-vacuity examples and type‑checking instances on the decoupled and tower carriers, verifying that the relation chain and PCS interface instantiate correctly. The diff contains no sorry or admit.
blueprint/src/references.bib: The blueprint/src/references.bib file is updated to include three new bibliographic entries: BRW26 (Bünz, Rothblum, and Wang's 2026 ePrint paper "Flock: Fast Proving for Batch Boolean Computations"), HJRRR25 (Hemo, Jue, Rabinovich, Roh, and Rothblum's 2025 ePrint paper "Jagged Polynomial Commitments (or: How to Stack Multilinears)"), and RSG (the informal note "Ring switching, generalized" from the leanEthereum/leanVM-b repository, which describes transforming a polynomial commitment scheme for 𝔽₂^f into one for 𝔽₂^e, decoupling packing/opening fields, and γ-power batching). These additions provide the formal citation data for sources that are presumably referenced in the blueprint text.
docs/kb/concepts/ring-switching.md: The documentation file docs/kb/concepts/ring-switching.md was significantly expanded to introduce a new second-generation abstraction called "The Generic layer" (located in ProofSystem/RingSwitching/Generic/), which generalizes from the tower case to decoupled packing and opening algebras P and E (following Flock's Appendix B and the "Ring switching, generalized" note), with tower switching becoming a special case P = E = L.

The addition details the seven-step spine every ring switch shares, the four safety pillars (coordinate maps derived from a bundled Basis, commitment binding through the PCS's own commitsTo, generically proven packing correctness, and no free Prop in the relation chain), and provides a status report for specific files within the Generic layer, each described with its key definitions and proven lemmas.

Newly described files and theorems include:

Carrier.lean: RingSwitchCarrier, bridge_eqTilde (Flock Claim 6's expansion)
Packing.lean: packedMLE_eval, packMLE_eq_packedMLE_curry (the "Binius-stability bridge")
Batching.lean: BatchingStrategy with proven instances gammaPowers and eqFold, plus reindex for transport and the decoupled field carrier label "R5"
Recombine.lean: recombine_bijective / recombine_injective, openingDecomposition_injective (via Module.Basis.sum_smul_bijective)
Relations.lean: The fixed relation chain (openingClaimRel, sliceRel, sumcheckClaimRel), the chain-coherence proof sumcheckClaim_of_slices, plus PCS interface (PackedCommitment, DenseMLPCS) and re-expressed Binius.FRIBinius.biniusCommitsTo

The documentation also notes that Carrier.lean, Packing.lean, Batching.lean, Recombine.lean, and Relations.lean are all proven, sorry-free, and axiom-clean, and clarifies what is not yet built (the assembled ringSwitch reduction, Binius migration, and the MBP-B̂ efficiency layer). Additionally, three new references were added to the Core References section: [BRW26], [RSG], and [HJRRR25].

docs/wiki/repo-map.md: Added documentation for a second-generation ring switching layer under ProofSystem/RingSwitching/Generic/, detailing Carrier.lean (RingSwitchCarrier with decoupled packing/opening algebras), Packing.lean (packing correctness and DP24 bridge), Batching.lean (BatchingStrategy, gammaPowers, eqFold, Schwartz–Zippel under [IsDomain]), Recombine.lean (injectivity on both bases, citing Flock Remark 5 and Data/Module/Basis.lean:sum_smul_bijective), and Relations.lean (relation chain with openingClaimRel, middle relations, PackedCommitment/DenseMLPCS with commitsTo). The new layer is noted as intended to eventually subsume the existing Profile.lean path while leaving it untouched during migration.

Last updated: 2026-07-11 23:48 UTC.

alexanderlhicks · 2026-07-07T15:45:08Z

big next step will be the reduction & soundness.

…rface - Generic/Relations.lean: framework-fixed relation chain — openingClaimRel anchor (+ non-vacuity witness), sliceRel, sumcheckClaimRel, and the proven chain coherence sumcheckClaim_of_slices (via bridge_eqTilde); PackedCommitment (commitsTo + functionality law + Nonempty guard; the legacy True-hook is unstatable: commitsTo_not_top / commitsTo_ne_top); DenseMLPCS mirroring MLIOPCS with relIn fixed to evalRel (= MLPEvalRelation AND commitsTo), so the PCS's own completeness/RBR fields consume the binding predicate - Data/Module/Basis.lean (new): reusable Basis.sum_smul_{bijective,injective}; Recombine.lean refactored onto it + openingDecomposition_injective (the opening half of Flock Remark 5) - Binius/FRIBinius/Prelude.lean: biniusCommitsTo (commitsTo orientation of the legacy initialCompatibility, rfl-pinned); documents the pre-existing upstream diagonal-coercion bug in firstOracleWitnessConsistencyProp (encoding reads t's diagonal evaluations, so commitsTo functionality is unprovable until the upstream spelling is fixed — recorded S7 gate) - KB ring-switching page + repo-map updated; ArkLib.lean regenerated All new declarations sorry-free and axiom-clean; RingSwitching sorry count unchanged at 14; binaryTowerProfile untouched. Hardened via a 4-pass independent adversarial close-review (structural Nonempty guard, precision fixes, upstream bug confirmed by compiled probe and logged). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

firstOracleWitnessConsistencyProp, getMidCodewords, and the honest-witness lens in FRIBinius/CoreInteractionPhase built P0 from `fun w => t.val.eval w`, where the silent coercion Fin (2^l) -> (Fin l -> L) is the pointwise Nat-cast CONSTANT function — the "novel coefficients" were t's evaluations at diagonal points, not its hypercube table, making the encoding non-injective (X 0 and X 1 collapsed definitionally; compiled counterexample) and the predicate unusable as binding semantics (functionality provably false). Fix: new named encoder BinaryBasefold.witnessNovelCoeffs — t's cube table in the LSB-first Nat.getBit order, the exact inverse of the decoder's Nat.binaryFinMapToNat mapping (roundtrip: getBit_of_binaryFinMapToNat) — used at all three sites; a repo-wide sweep found no further instances. Compiled regression probe: witnessNovelCoeffs now separates X 0 / X 1. The biniusCommitsTo functionality proof (S7) is provable-as-sketched again. Pre-existing bug (predates this PR); all consumers are sorry-gated statements, so nothing proven was invalidated. Found by the S5 close-review adversarial passes. Docstrings and the KB page updated accordingly. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Review finding: the R7 regression probe was verified in-session but never committed, so nothing in-tree would catch the diagonal-encoding bug regressing. Adds a generic-field example separating witnessNovelCoeffs (X 0) from (X 1) at omega = 1 - unprovable under the pre-fix diagonal spelling. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Two plumbing lemmas for RBR-game factoring (generic ring-switch S6): - probEvent_uniformSample_eq_pr_uniformOfFintype: Pr[E | $t C] equals the PMF-level Pr_{c <-$p C}[E c] - probEvent_bind_uniformSample_le: a per-prefix PMF bound transfers to the bind (prefix; uniform challenge; pair) - the challenge-round shape Both sorry-free and axiom-clean ([propext, Classical.choice, Quot.sound]). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Verifier.probEvent_challengeRound_le: bounds the RBR-game shape (prefix; uniformly sampled challenge i; post-map) by any epsilon that bounds the PMF-level bad-event probability for every fixed prefix outcome - the bridge from simulateQ (impl.addLift challengeQueryImpl) games to Pr_{c <- $p _} per-round analyses (BatchingStrategy.separates). The prefix is an arbitrary OracleComp (no prover unfolding); the post-map covers the games' (transcript, challenge, queryLog) triple. Sorry-free, axiom-clean. Closes the bootstrapped 'medium' plumbing item; the feared erw-chain reduced to one erw [simulateQ_query]. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

… check (S6/F2) The design-review F2 algebra, all sorry-free and axiom-clean: - Packing.lean: generic unpack (coefficient-wise packBasis.repr) with the round-trip PROVEN both directions (packedMLE_unpack / unpack_packedMLE; packedMLE_surjective constructive) - CommRing-only, honoring the file's no-assumed-round-trip disclaimer - Relations.lean: claimConsistent (DP24 Check 1 in family form, the [BRW26] Remark-5 read-back equation) + both directions: openingClaimRel_of_claimConsistent (soundness read-back, [IsDomain E] - the logged S6 deviation) and claimConsistent_of_slices (completeness) - Data/MvPolynomial/Multilinear.lean: aeval_multilinear_eq_sum_eqTilde (eq-expansion of a multilinear at an algebra point; reusable) INV-2: exercised on tower, decoupled-toy (CommRing-only parts) and decoupled-field (domain-gated parts) carriers. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…uction Generic/Reduction.lean: the ProtocolSpec 2 phase (prover sends slices, verifier sends batching challenge) written WITHOUT the composition operators, so every definition is sorry-free and axiom-clean (verified: standard 3 axioms on all 8 public decls) despite upstream OracleVerifier.append.verify being sorried. - Verifier performs the soundness-critical claim-consistency check (design review F1: without it the phase RBR statement is false), and fails via OptionT failure, not a dummy statement - phaseRelIn = openingClaimRel AND commitsTo (packedMLE wit) - the oracle-extended anchor promised at S5; phaseRelOut carries commitsTo through to the sumcheck claim - Per-round error VECTOR (bat.error at the single challenge round) - WitMid/extractor via unpack; RBR knowledge soundness recorded as a Prop-valued def (roadmap section 8, F3) pending the stretch proof - W := car.iE pinned; INV-2 examples on tower + decoupled-field carriers Also folds ChallengeRound.lean + Reduction.lean into the ArkLib.lean umbrella (283 imports). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…o first) ringSwitchPhase_rbrKnowledgeSound: the ring-switch phase is round-by-round knowledge sound with error bat.error at the batching-challenge round - the FIRST non-vacuous RBR probability bound completed in ArkLib (the three prior real ones are all sorried). - phaseKnowledgeStateFunction [IsDomain car.E]: round 1 tracks the Remark-5 check + binding + slice relation; round 2 re-tracks the check (the verifier fails without it), binding, and the batched claim; toFun_full cases on the verifier's definitional if and kills the failure branch by empty support - phase_badEvent_le: commitsTo_functional collapses the existential to the committed t'0; the surviving event is exactly BatchingStrategy.separates on the sent slices vs the honest slices of t'0 (via sumcheckClaim_of_slices); no-commitment branch has probability zero - Verifier.probEvent_rbrGame_le (Security/ChallengeRound.lean): the factoring lemma restated at the literal game shape - unifying the game's destructuring bind against the plain-bind lemma diverges in whnf (structure-eta through the prover term), so the same proof script is replayed with the matcher fired by one constructor-level obtain All axiom-clean ([propext, Classical.choice, Quot.sound]); zero sorry tokens; no maxHeartbeats override needed; whole library green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Independent adversarial close-review verdict: theorem holds up, 'repo first' claim accurate, no blockers. Adds its two suggested witnesses: phaseRelIn nonemptiness (true claims + trivial commitment - the RBR obligation is not discharged by an empty input relation) and an end-to-end application of ringSwitchPhase_rbrKnowledgeSound at decoupledFieldCarrier with the PROVEN gamma-powers strategy (real separation error 3/4). Honest caveats recorded in roadmap section 8: phase completeness deferred (next session), and the repo-wide RBR->knowledge-soundness implication remains sorried upstream. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

start generalizing

af91401

alexanderlhicks changed the title ~~start generalizing~~ feat: even more general ring switch Jul 7, 2026

alexanderlhicks and others added 10 commits July 7, 2026 23:54

style(Data/MvPolynomial): show -> change (Data zero-warning budget)

86f9f0f

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat: even more general ring switch#615

feat: even more general ring switch#615
alexanderlhicks wants to merge 11 commits into
mainfrom
feat/generic-ring-switch

alexanderlhicks commented Jul 7, 2026

Uh oh!

github-actions Bot commented Jul 7, 2026 •

edited

Loading

Uh oh!

alexanderlhicks commented Jul 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

alexanderlhicks commented Jul 7, 2026

Uh oh!

github-actions Bot commented Jul 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

alexanderlhicks commented Jul 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

github-actions Bot commented Jul 7, 2026 •

edited

Loading