feat: List-based IOP model with composition & sumcheck security proofs by quangvdao · Pull Request #392 · Verified-zkEVM/ArkLib

quangvdao · 2026-03-07T09:13:01Z

Summary

This PR introduces a complete rewrite of the IOP (Interactive Oracle Proof) model using list-based protocol specifications, replacing the Fin n-indexed approach. The new model eliminates pervasive casting overhead and makes composition definitional.

Motivation

The existing ProtocolSpec n (indexed by Fin n) creates significant friction:

Casting overhead: composing ProtocolSpec n and ProtocolSpec m requires Fin.castSucc/Fin.castAdd everywhere
Rigid prover structure: stateful provers with Fin (n+1) → Type are painful to define and compose
Oracle index accumulation: chains of Function.Embedding.trans/Equiv.sumAssoc are hard to work with
Incomplete proofs: many composition lemmas have sorrys due to indexing complexity, not mathematical difficulty

Architecture

The refactored model lives entirely under ArkLib/Refactor/ (27 new files, ~10,400 lines) and is strictly additive — no existing functionality is removed.

Core modules:

ProtocolSpec — List (Direction × Type) with definitional append
HVector — heterogeneous vectors as the backbone for transcripts
Transcript — messages, challenges, and full transcripts over HVector
Prover / Verifier / OracleVerifier — participants defined by structural recursion
Reduction — reductions between protocol specs with composition (comp, compNth)

Security framework:

Security.Defs — completeness, soundness, knowledge soundness with outside challenge sampling
Security.StateFunction / StateRestoration — state-function and state-restoration soundness
Security.Composition.{Util, Completeness, Soundness, KnowledgeSoundness} — modular composition theorems

Sumcheck case study (validation target):

Sumcheck.Defs / SingleRound — single-round protocol definition
Sumcheck.PolyUtils / PartialEval — polynomial utilities and partial evaluation lemmas
Sumcheck.Completeness — perfect completeness proof
Sumcheck.Security — round-by-round (RBR) soundness via composition
Sumcheck.General — multi-round composition via compNth
Sumcheck.Test — end-to-end computable test (#eval)

Additional infrastructure:

FiatShamir — Fiat-Shamir transformation for list-based specs
LiftContext / LiftContext.Lens — context lifting via lenses for embedding reductions

Other changes

OracleInterface.lean: Proved distanceLE_mvPolynomial_degreeLE (Schwartz-Zippel bound for multivariate polynomials), filling a sorry
VCVio dependency: bumped from v4.28.0 to master (required by new API surface)
Blueprint: added iop_refactor_security_composition.tex chapter
Design doc: docs/design/iop-refactor.md with full rationale and API reference

Remaining `sorry`s (22 total)

Module	Count	Nature
`LiftContext/OracleReduction`	8	Oracle query routing through lifted contexts
`LiftContext/Reduction`	7	Reduction lifting through lenses
`StateRestoration`	6	State-restoration soundness (WIP)
`Sumcheck/Test`	1	Decidable instance placeholder for `#eval`

All core security composition theorems (completeness, soundness, knowledge soundness) and sumcheck security proofs are sorry-free.

Test plan

lake build ArkLibRefactor compiles successfully
lake build ArkLib (existing library) still compiles
#eval Sumcheck.test in Sumcheck/Test.lean runs the end-to-end sumcheck test
Verify no non-sorry warnings via lake build output

Made with Cursor

Comprehensive design doc covering the list-based ProtocolSpec refactor, including bundled OracleInterface, coinductive Prover, dual-track Verifier/OracleVerifier, outside challenge sampling, BCS analysis, and FIOP+FC pipeline from eprint 2025/902. Co-authored-by: Cursor <cursoragent@cursor.com>

- HVector: heterogeneous vector ported from lean-mlir with snoc, splitAt, take, drop, and simp lemmas - ProtocolSpec: list-based protocol spec with Round inductive (P_to_V T oi, V_to_P T) bundling OracleInterface; smart constructors .msg/.chal; messageTypes/challengeTypes with append and take lemmas - Transcript: full and partial transcripts as HVector Round.type; Messages/Challenges extraction; PartialTranscript.concat by structural recursion (no casts) Co-authored-by: Cursor <cursoragent@cursor.com>

- Prover: coinductive type with run (outside challenges) and comp (sequential composition via list append); HonestProver wrapper - Verifier: plain verifier seeing messages via full transcript; comp splits transcript at boundary - OracleVerifier: MessageOracleIdx and oracleSpecOfMessages from bundled OracleInterface; oracleImplOfMessages for pure oracle implementation; OracleVerifier structure with verify/simulate/reify; toVerifier bridge (sorry — requires VCVio simulation machinery) - Reduction: plain Reduction and OracleReduction (dual-track); OracleProver with oracle statement data; Proof specialization; Reduction.run; OracleReduction.toReduction (sorry) Co-authored-by: Cursor <cursoragent@cursor.com>

…anup Add security definition files (Defs.lean, StateFunction.lean) with completeness, soundness, knowledge soundness, and round-by-round soundness. Fix build errors across Phase 0/1 files (HVector refactor to recursive def, explicit args for autoImplicit=false, Prover destructuring). Remove all linter warnings (unused simp args, flexible simp tactics). Co-authored-by: Cursor <cursoragent@cursor.com>

…ition) Add sequential composition and n-fold composition for all core types: Prover.iterate, HonestProver.compNth, Verifier.compNth, OracleVerifier.comp/ compNth, Reduction.comp/compNth, OracleReduction.comp/compNth. Add challenge sampling for composed protocols (ofAppend, ofReplicate). Add security composition theorems: completeness composes, perfect completeness composes, RBR soundness implies soundness, n-fold soundness/knowledge soundness. Probability proofs deferred (sorry) pending VCVio infrastructure. Co-authored-by: Cursor <cursoragent@cursor.com>

- Add Prover.mapOutput for mapping prover output types - Add SubSpec instances for oracleSpecOfMessages over append (left/right) - Implement OracleVerifier.toVerifier via answerMsgQuery + simulateQ - Implement OracleVerifier.compNth base case simulate - Implement OracleReduction.toReduction using toVerifier + mapOutput - Fix OracleReduction.compNth base case simulate Remaining sorries: OracleVerifier.comp.verify/simulate (complex cross-spec oracle routing) and 8 composition theorem proofs (need VCVio probability lemmas). Co-authored-by: Cursor <cursoragent@cursor.com>

…Verifier.comp - Rewrite Challenges.split/join and Messages.split/join using structural recursion on pSpec₁, eliminating all rw/simp casts (Eq.mpr) that poisoned downstream definitional equality - Fully implement OracleVerifier.comp verify and simulate fields (were sorry): route queries via SubSpec coercions with continuation mapping (q'.2 <$> liftM (query ...)) to preserve range types - Update callers to pass explicit pSpec₁/pSpec₂ arguments Co-authored-by: Cursor <cursoragent@cursor.com>

Annotate OracleVerifier.comp (query routing strategy, SubSpec continuation pattern), toVerifier (three oracle layers), SubSpec embeddings (left/right index wrapping), Prover.comp, OracleReduction.toReduction, and Challenges/Messages split/join (structural recursion rationale). Co-authored-by: Cursor <cursoragent@cursor.com>

…lSpec Define the Fiat-Shamir transform using structural recursion on the new list-based ProtocolSpec with an accumulator tracking message types. Uses Sum.elim for V_to_P challenge oracle entries so VCVio's SubSpec instances resolve automatically. Includes Prover.runFS, Messages.deriveTranscript, fsProtocolSpec, and the full Reduction.fiatShamir. Made-with: Cursor

- Run prover/verifier/extractor under one shared init per Pr-sample - Tie knowledge-soundness acceptance to the prover's StmtOut - Make FS Messages trivial OracleInterface non-global (avoid instance hazards) - Add OracleVerifier reify/simulate consistency predicate and clarify HVector universes Made-with: Cursor

Introduce a generic oracle-state invariant API and refactor completeness + RBR soundness/KS notions to quantify over initial states satisfying Inv. Update composition theorem statements and the blueprint writeup accordingly. Made-with: Cursor

Switch VCVio to track master and update the Lake manifest lock to 0e91cb33e47b92c41fc1ef0052ca58b0870cedd5. Made-with: Cursor

…ty theorems Define the full general sumcheck protocol in the refactored IOP framework using CompPoly's computable polynomial types (CMvPolynomial for oracle statements, CPolynomial for round messages). New files under ArkLib/Refactor/Sumcheck/: - PolyUtils.lean: OracleInterface instances, CDegreeLE type, CPolynomial bridge lemmas, Lagrange interpolation - Defs.lean: statement types, per-round protocol spec, input relations, computeRoundPoly (evaluate-and-interpolate) - SingleRound.lean: single-round prover, verifier, oracle verifier, reduction - General.lean: multi-round composition via replicate/compNth, multiRoundProver, generalReduction - Security.lean: perfect completeness, single-round soundness (Schwartz-Zippel), multi-round soundness theorem statements (sorry'd proofs) Supporting changes: - HVector: pin PUnit universe to prevent metavariable leaks in compNth - ProtocolSpec: change msg/chal from def to abbrev for instance synthesis - OracleVerifier: add compNth infrastructure Made-with: Cursor

Remove unnecessary `noncomputable` from `computeRoundPoly`, `prover`, `singleRoundReduction`, `multiRoundProver`, and `generalReduction` — all CompPoly operations (eval, lagrange interpolation, field arithmetic) are fully computable. Upgrade Security.lean to use framework-native `rbrSoundness` / `Verifier.soundness` via empty-oracle embedding. Add Test.lean with `native_decide` and `#eval!` tests running the full honest prover + verifier end-to-end over ZMod 7. Made-with: Cursor

Move general-purpose helper lemmas out of the Completeness section and into their proper namespaces following VCVio convention: - probEvent_bind_bind_swap, probEvent_compl_le_of_ge, probEvent_ge_of_compl_le → root-level section ProbEvent - HVector.splitAt_append → root-level namespace HVector - Transcript.split_join → ProtocolSpec.Transcript (before section) - Prover.run_comp_join, run_comp_join_bind → ProtocolSpec.Prover (before section) These lemmas are candidates for upstreaming to VCVio. Made-with: Cursor

Make the multi-round verifier/prover return the sampled challenge vector alongside the final value, so the remaining obligation can live in the reduction output language. Made-with: Cursor

- Invariant.lean: replace unnecessary `simpa` with `simp` at four sites - PolyUtils.lean: replace `show` tactic with `change` to satisfy style linter - Test.lean: suppress `native_decide` linter (intentional for ZMod 7 checks), fix pre-existing parse errors from `|>.value`/`|>.challenges` syntax (wrap in parens), and fix `proverOut.1.value` → `proverOut.value` (`.1` is `.challenges : Vector`, not `.value`) - Composition.lean: add Verifier.StatePreserving / Verifier.OutputIndependent wrappers and oracleFree_* implication lemmas; remove unused _hV₂ parameter from completeness_comp and corollaries Made-with: Cursor

- Add \oSpec macro and remark on sequential composition / non-interference, explaining why P₂ can mutate oracle state before V₁ runs - Rename composition notation from R₂ ∘ R₁ to R₁ comp R₂ to match Lean - Add Definition: oracle-free verifier (sufficient non-interference condition) - Add Lemma: decomposing a composed run under OracleFree assumption (mirrors Lean's run_comp_join_eq_bind) - Rewrite Theorem proof (completeness composes with additive error) to follow the Lean proof structure: stage predicates, challenge re-sampling swap, conditional stage-2 bound, union bound - Add Remark discussing potential weakenings of OracleFree (StatePreserving, OutputIndependent, read-only oracles, commutation hypotheses) - Update n-fold completeness corollary to assume OracleFree and PreservesInv Made-with: Cursor

Remove unnecessary simp/simpa patterns and unused assumptions in Sumcheck security/completeness proofs so `ArkLib/Refactor` is warning-clean except for remaining `sorry` declarations. Made-with: Cursor

Apply the remaining Refactor proof cleanups across composition and sumcheck modules, including style/linter polish and aligned theorem updates, while keeping the workspace warning-clean apart from intentional sorrys. Made-with: Cursor

…ntrypoints Update Refactor security modules to use VCVio's invariant/simulation lemmas, remove local duplicate invariant definitions, and split aggregate imports by introducing ArkLibRefactor as the dedicated Refactor umbrella. Made-with: Cursor

Clean up lints in the composition security file by removing style and unused-argument warnings while preserving the existing theorem placeholders. Made-with: Cursor

…ess, KnowledgeSoundness Split the large Composition.lean into four sub-modules under Composition/ and turn the original file into a re-export hub. Broken proofs are preserved as sorry + block comments for future work. Made-with: Cursor

Progress composition proofs by adding StateT run/map lemmas, wiring RBR knowledge-to-soundness bridge, and restructuring key proof blocks for ongoing completion. Made-with: Cursor

Replace unnecessary `simpa` with `simp`, remove unused simp arguments (`hmid`, `bind_assoc`), and convert non-terminal `simp` to `simp only` in Soundness.lean. Also includes proof fill-ins for StateFunction and KnowledgeSoundness. Made-with: Cursor

…ion and prove single-round sumcheck RBR soundness Refactor knowledge soundness definitions and proofs: - Simplify prover output type from (StmtOut × WitOut) to WitOut in knowledgeSoundness - Project RBR soundness/knowledge soundness distributions to transcript only - Universally quantify rbrKnowledgeSoundness over prover output type - Replace ~400-line direct knowledge soundness proof with short composition (RBR k.s. → RBR soundness → soundness → knowledge soundness) - Drop Inhabited constraints from rbrKnowledgeSoundness_implies_rbrSoundness Add Newton-form fast interpolation with precompiled inverse deltas and prove roundVerifierState_rbrSoundness for single-round sumcheck. Made-with: Cursor

- Add QueryImpl.ofSubSpec: generic SubSpec-to-QueryImpl constructor - Add comp.liftOStmtMsg: shared helper for OStmt+message lifting - Add comp.liftVerify₁, comp.liftVerify₂, comp.liftSimulate as named definitions replacing inline let-bindings in comp - Rewrite comp body using named helpers + OptionT do-notation - Remove duplicate SubSpec.trans (already in VCVio) - Add docstrings to HVector snoc, splitAt, take, drop - Mark probEvent_exists_finset_le_sum for removal after VCVio update Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…ration - Add OracleAwareStateFunction and OracleAwareKnowledgeStateFunction with bridge theorems from legacy variants; remove problematic trace variants (OracleAwareTraceStateFunction and friends) whose toFun_next axiom was too restrictive - Add simp lemmas for Transcript.ofMessagesChallenges roundtrips - Make liftFSTail public (needed by StateRestoration) - Add LiftContext module with lens-based lifting for reductions and oracle reductions (WIP, contains sorries) - Add StateRestoration security definitions and bridge theorems (WIP) Made-with: Cursor

… casts Nat.sub uses brecOn internally, so (k+1) - (n+1) is NOT definitionally equal to k - n. This caused all rightOfAppend_concat proofs to require painful casts. Fix by parameterizing rightOfAppend with an explicit local index j and proof j + |pSpec₁| = k, eliminating subtraction from the return type entirely. Key changes: - rightOfAppend now takes (h_eq : j + pSpec₁.length = k) instead of (hk : pSpec₁.length ≤ k), returning PartialTranscript pSpec₂ j - rightOfAppend_concat proven sorry-free with no outer cast - leftFullOfAppend_concat and leftOfAppend_concat proven sorry-free - Added oracleFree_compNth, InLangAtChallenges, roundVerifierStateAsOracle_oracleFree, generalVerifierStateAsOracle_oracleFree, rbrSoundnessError_eq_errorReplicate - Scaffolded generalVerifierStateAsOracle_rbrSoundness (3 sorry's remain) Made-with: Cursor

…t warnings Replace manual inductive state-function construction for n-round soundness with the generic `rbrSoundness_compNth` composition lemma. Add `toFun_challenge_of_mem` fields, omit unused section variables. Made-with: Cursor

…on lemmas Add SymbolicPoly witness type and symbolic round/multi-round reductions via compNth. Fill in rbrSoundness_comp proof skeleton with state function construction. Add HVector.take bridge lemmas for transcript split projections. Made-with: Cursor

…undness proof - PartialEval: derive DecidableEq from LawfulBEq via local instance, removing redundant variable and omit annotations; decompose roundPoly_natDegree_le into per-operation degree lemmas - Soundness: extend rbrSoundness_comp proof with case split on Nonempty Inv - Security: add #print axioms for generalVerifier_rbrSoundness Made-with: Cursor

Extract StateFunction construction into `rbrSoundness_comp_sf` and zero-round base case into `rbrSoundness_replicate_zero`. Fix omega linter warnings by replacing with explicit proof terms. Lower all maxHeartbeats from 800K-4M to 300K or default. Made-with: Cursor

…mmas Thread IndividualDegreeLE witness through SymbolicPoly so the symbolic prover preserves degree bounds across rounds. Add partialEvalFirst and roundPoly degree preservation lemmas in PartialEval. Made-with: Cursor

Move foundational definitions and proofs out of Security.lean into their logical homes to improve modularity and reduce file size (~1578 → ~970 lines): - Completeness.lean: trueTarget/trueRoundValue relation lemmas - PartialEval.lean: prefixPoint_spec characterization theorem - General.lean: outputLang, roundStateLang, TrueRoundPolyExists, trueRoundPolyExists_of_ostmt, and language helper lemmas Fix all linter warnings (unused section variables, simpa/simp, unused simp args, empty lines within commands, long lines, file-too-long). Made-with: Cursor

Replace the sorry in distanceLE_mvPolynomial_degreeLE with a complete proof using the Schwartz-Zippel lemma. The bound shows that for two distinct multivariate polynomials with individual degree ≤ d, the number of agreeing evaluation queries is at most |σ| * d * |R|^(|σ| - 1). Also add #print axioms for generalVerifier_rbrSoundness in Security.lean. Made-with: Cursor

github-actions · 2026-03-07T09:14:38Z

🤖 Gemini PR Summary

Refactors the Interactive Oracle Proof (IOP) model within ArkLib by transitioning from Fin n-indexed protocol specifications to a List-based architecture. This change eliminates casting overhead (e.g., Fin.castSucc) and enables definitional composition of protocols. All new logic is located in ArkLib/Refactor/ and is strictly additive.

Core Formalization

List-Based Protocol Specifications: Replaces indexing with List (Direction × Type). Uses heterogeneous vectors (HVector) for transcripts, facilitating seamless concatenation and nesting.
Security Framework: Formalizes definitions for completeness, soundness, and knowledge soundness (straight-line extractors) within a unified probabilistic formulation.
Composition Theorems: Provides formal proofs for sequential and $n$-fold protocol composition. Establishes that completeness and soundness errors accumulate linearly/additively, while perfect completeness is preserved definitionally.
Schwartz-Zippel Lemma: Proves distanceLE_mvPolynomial_degreeLE in OracleInterface.lean, completing the multivariate polynomial degree bounds required for IOP soundness.
Oracle Verifier Architecture: Defines OracleVerifier using the OracleComp monad, enabling verifiers to interact with prover messages and input statements as queryable oracles.

Sumcheck Implementation

Verified Protocol: Implements the Sumcheck protocol from first principles, including polynomial utilities for partial evaluation and Lagrange interpolation.
Formal Proofs: Includes full, sorry-free proofs for the Sumcheck protocol’s perfect completeness and round-by-round (RBR) soundness.
Validation: Provides a computable test suite over ZMod 7 using #eval and native_decide to verify honest prover and verifier logic.

Infrastructure & Tooling

Fiat-Shamir Transformation: Generic implementation to convert public-coin interactive reductions into non-interactive versions using a random oracle.
Context Lifting (Lenses): Introduces a "Lens" mechanism to transport statements, witnesses, and oracles between protocol layers, facilitating sub-protocol embedding.
Dependency Update: Bumps VCVio from v4.28.0 to master.
Documentation: Adds a design document (docs/design/iop-refactor.md) and a new chapter to the formal blueprint (iop_refactor_security_composition.tex).

Proof Status & `sorry` Placeholders

Note: There is a discrepancy between the PR body and the draft summary regarding protocol dependency. The PR body defines ProtocolSpec as a simple List (Direction × Type), whereas the draft summary describes a "Telescope Framework" (ProtocolCtx) using W-types to support rounds where future types depend on previous message values.

This PR contains 22 sorry placeholders:

LiftContext/OracleReduction.lean (8) & LiftContext/Reduction.lean (7): Proofs regarding the preservation of completeness and soundness when lifting reductions through lenses.
StateRestoration.lean (6): Core lemmas and implication theorems for state-restoration soundness.
Sumcheck/Test.lean (1): Decidable instance placeholder for end-to-end evaluation.

The core Sumcheck security proofs and general composition theorems are complete and sorry-free.

Statistics

Metric	Count
📝 Files Changed	46
✅ Lines Added	14802
❌ Lines Removed	4

Lean Declarations

✏️ **Added:** 388 declaration(s)

def emptyPrefix : Vector R 0 in ArkLib/Refactor/Telescope/Sumcheck.lean
theorem challengeTypes_cons_V_to_P {T : Type} {tl : ProtocolSpec} : in ArkLib/Refactor/ProtocolSpec.lean
def OracleVerifier {ι : Type} (oSpec : OracleSpec ι) in ArkLib/Refactor/Telescope/OracleVerifier.lean
lemma PartialTranscript.rightOfAppend_hvector_take_aux {pSpec₁ pSpec₂ : ProtocolSpec} in ArkLib/Refactor/Transcript.lean
def ofList : ProtocolSpec → ProtocolCtx in ArkLib/Refactor/Telescope/Basic.lean
def generalVerifier (D : Fin m → R) : in ArkLib/Refactor/Sumcheck/General.lean
theorem Verifier.soundness_compNth in ArkLib/Refactor/Security/Composition/Soundness.lean
instance instMessageDataOracleInterface : in ArkLib/Refactor/Telescope/OracleVerifier.lean
def pullback {ctx : ProtocolCtx} {Claim : Type} (tree : ClaimTree ctx Claim) : in ArkLib/Refactor/Telescope/Basic.lean
lemma Reduction.id_perfectCompleteness in ArkLib/Refactor/Security/Composition/Completeness.lean
def rbrSoundnessError : ChallengeIndex (generalPSpec R deg n) → ℝ≥0 in ArkLib/Refactor/Sumcheck/Security.lean
abbrev chal (T : Type) (bm : BundledMonad) (rest : ProtocolCtxM) : ProtocolCtxM in ArkLib/Refactor/Telescope/Basic.lean
def PartialTranscript.ofTranscript {pSpec : ProtocolSpec} (tr : Transcript pSpec) : in ArkLib/Refactor/Transcript.lean
def prefixPoint : ∀ {i n : ℕ}, Vector R i → (Fin n → R) → Fin (n + i) → R in ArkLib/Refactor/Sumcheck/PartialEval.lean
def lagrangeInterpolate (pts vals : Vector R (n + 1)) : CPolynomial R in ArkLib/Refactor/Sumcheck/PolyUtils.lean
lemma split_join {pSpec₁ pSpec₂ : ProtocolSpec} in ArkLib/Refactor/Transcript.lean
def get {α : Type*} {A : α → Type*} : in ArkLib/Refactor/HVector.lean
def sampleChallenges (pSpec : ProtocolSpec) [ChallengesSampleable pSpec] : in ArkLib/Refactor/Security/Defs.lean
def subSpec_oracleSpecOfMessages_right : in ArkLib/Refactor/OracleVerifier.lean
def runWithTranscript in ArkLib/Refactor/Telescope/Reduction.lean
def toVerifier in ArkLib/Refactor/OracleVerifier.lean
theorem sumAllButFirst_monomials_get0_le {deg : ℕ} (D : Fin m → R) (k : ℕ) in ArkLib/Refactor/Sumcheck/PartialEval.lean
def split : in ArkLib/Refactor/Transcript.lean
theorem partialEvalFirst_individualDegreeLE {deg : ℕ} (a : R) in ArkLib/Refactor/Sumcheck/PartialEval.lean
def oracleImplOfMessages : in ArkLib/Refactor/OracleVerifier.lean
def Prover (m : Type → Type) (Output : Type) : ProtocolSpec → Type in ArkLib/Refactor/Prover.lean
theorem trueTarget_push_eq_trueRoundValue in ArkLib/Refactor/Sumcheck/Completeness.lean
def verifierFrom : in ArkLib/Refactor/Telescope/Sumcheck.lean
def StateRestoration in ArkLib/Refactor/Security/StateRestoration.lean
def type : Round → Type in ArkLib/Refactor/ProtocolSpec.lean
def verifier (D : Fin m → R) : in ArkLib/Refactor/Telescope/Sumcheck.lean
def Transcript.truncate : (n : Nat) → (ctx : ProtocolCtx) → in ArkLib/Refactor/Telescope/Basic.lean
def liftFSTail {ι : Type} (oSpec : OracleSpec ι) in ArkLib/Refactor/FiatShamir.lean
def PartialTranscript.empty (pSpec : ProtocolSpec) : PartialTranscript pSpec 0 in ArkLib/Refactor/Transcript.lean
theorem messageTypes_nil : messageTypes ([] : ProtocolSpec) = [] in ArkLib/Refactor/ProtocolSpec.lean
def prover {i : ℕ} in ArkLib/Refactor/Sumcheck/SingleRound.lean
theorem lagrangeInterpolateWithPlan_natDegree (plan : InterpPlan R n) in ArkLib/Refactor/Sumcheck/PolyUtils.lean
theorem roundPoly_natDegree_le {deg : ℕ} (D : Fin m → R) {k : ℕ} in ArkLib/Refactor/Sumcheck/PartialEval.lean
def tail {α : Type*} {A : α → Type*} {a : α} {as : List α} in ArkLib/Refactor/HVector.lean
def IndividualDegreeLE (deg : ℕ) (p : CMvPolynomial n R) : Prop in ArkLib/Refactor/Sumcheck/PolyUtils.lean
lemma run_comp_join_eq_bind in ArkLib/Refactor/Security/Composition/Completeness.lean
def Verifier.knowledgeSoundness (relIn : Set (StmtIn × WitIn)) in ArkLib/Refactor/Security/Defs.lean
theorem oracleFree_compNth {ι : Type} {oSpec : OracleSpec ι} in ArkLib/Refactor/Security/Composition/Util.lean
def roundSoundnessError : ℝ≥0 in ArkLib/Refactor/Sumcheck/Security.lean
abbrev Proof (m : Type → Type) (StmtIn WitIn : Type) (pSpec : ProtocolSpec) in ArkLib/Refactor/Reduction.lean
def map {α : Type*} {A B : α → Type*} (f : ∀ (a : α), A a → B a) : in ArkLib/Refactor/HVector.lean
def OracleVerifier.liftContext in ArkLib/Refactor/LiftContext/OracleReduction.lean
def srReplayChallengeAux in ArkLib/Refactor/Security/StateRestoration.lean
def id {m : Type → Type} [Monad m] {S W : Type} : in ArkLib/Refactor/Reduction.lean
def TrueRoundPolyExists (poly : OStmt R deg n) (D : Fin m → R) : Prop in ArkLib/Refactor/Sumcheck/General.lean
def runToRound {m : Type → Type} [Monad m] {Output : Type} : in ArkLib/Refactor/Prover.lean
def roundVerifierState (D : Fin m → R) : in ArkLib/Refactor/Sumcheck/General.lean
def messageData : {ctx : ProtocolCtx} → (tr : Transcript ctx) → MessageData tr in ArkLib/Refactor/Telescope/OracleVerifier.lean
theorem roundVerifierState_rbrSoundness in ArkLib/Refactor/Sumcheck/Security.lean
def Verifier.liftContext {m : Type → Type} [Monad m] in ArkLib/Refactor/LiftContext/Reduction.lean
theorem splitAt_append (l₁ l₂ : List α) (v₁ : HVector A l₁) (v₂ : HVector A l₂) : in ArkLib/Refactor/HVector.lean
theorem liftContext_perfectCompleteness in ArkLib/Refactor/LiftContext/Reduction.lean
theorem natDegree_add_le' (p q : CPolynomial R) : in ArkLib/Refactor/Sumcheck/PolyUtils.lean
theorem rbrSoundness_implies_oracleAwareRbrSoundness in ArkLib/Refactor/Security/StateFunction.lean
instance instOracleInterfaceCPolynomial : in ArkLib/Refactor/Sumcheck/PolyUtils.lean
def Transcript.join : in ArkLib/Refactor/Telescope/Basic.lean
def Verifier.compNth {m : Type → Type} [Monad m] {S : Type} in ArkLib/Refactor/Telescope/Basic.lean
def appendLeft (i : ChallengeIndex pSpec₁) : ChallengeIndex (pSpec₁ ++ pSpec₂) in ArkLib/Refactor/ProtocolSpec.lean
def iterate {m : Type → Type} [Monad m] {S : Type} : in ArkLib/Refactor/Prover.lean
def join : in ArkLib/Refactor/Transcript.lean
def StateRestoration.Soundness in ArkLib/Refactor/Security/StateRestoration.lean
def trueRoundValue (poly : OStmt R deg n) {i : ℕ} in ArkLib/Refactor/Sumcheck/Completeness.lean
theorem PartialTranscript.leftFullOfAppend_hvector_take {pSpec₁ pSpec₂ : ProtocolSpec} in ArkLib/Refactor/Transcript.lean
def HonestProver.liftContext {m : Type → Type} [Monad m] in ArkLib/Refactor/LiftContext/Reduction.lean
theorem oracleAwareRbrKnowledgeSoundness_implies_knowledgeSoundness in ArkLib/Refactor/Security/Composition/KnowledgeSoundness.lean
theorem challengeTypes_cons_P_to_V {T : Type} {oi : OracleInterface T} {tl : ProtocolSpec} : in ArkLib/Refactor/ProtocolSpec.lean
theorem pullback_isSound {ctx : ProtocolCtx} {Claim : Type} in ArkLib/Refactor/Telescope/Basic.lean
theorem replicate_succ (n : Nat) (pSpec : ProtocolSpec) : in ArkLib/Refactor/ProtocolSpec.lean
theorem claimTreeFrom_isSound in ArkLib/Refactor/Telescope/Sumcheck.lean
def Reduction.fiatShamir {ι : Type} {oSpec : OracleSpec ι} in ArkLib/Refactor/FiatShamir.lean
def partialEvalLast (a : R) (p : CMvPolynomial (n + 1) R) : CMvPolynomial n R in ArkLib/Refactor/Sumcheck/PartialEval.lean
theorem rbrSoundnessError_eq_errorReplicate : in ArkLib/Refactor/Sumcheck/Security.lean
theorem comp_not_good_of_not_good : in ArkLib/Refactor/Telescope/Basic.lean
theorem Verifier.oracleAwareRbrSoundness_compNth in ArkLib/Refactor/Security/Composition/Soundness.lean
theorem stateRestorationSoundness_implies_soundness in ArkLib/Refactor/Security/StateRestoration.lean
def mapOutput {m : Type → Type} [Functor m] {A B : Type} (f : A → B) : in ArkLib/Refactor/Prover.lean
def reifySimulateCorrect in ArkLib/Refactor/OracleVerifier.lean
def toRight (i : ChallengeIndex (pSpec₁ ++ pSpec₂)) (h : pSpec₁.length ≤ i.1) : in ArkLib/Refactor/ProtocolSpec.lean
def replicate (ctx : ProtocolCtxM) : Nat → ProtocolCtxM in ArkLib/Refactor/Telescope/Basic.lean
def soundness in ArkLib/Refactor/Telescope/Security/Defs.lean
theorem liftContext_toReduction_comm in ArkLib/Refactor/LiftContext/OracleReduction.lean
def PartialTranscript.rightOfAppend in ArkLib/Refactor/Transcript.lean
def snoc {α : Type*} {A : α → Type*} {a : α} {as : List α} in ArkLib/Refactor/HVector.lean
abbrev msg (T : Type) [oi : OracleInterface T] : Round in ArkLib/Refactor/ProtocolSpec.lean
def trueTarget (poly : OStmt R deg n) {i : ℕ} (fixed : Vector R i) (D : Fin m → R) : R in ArkLib/Refactor/Sumcheck/Completeness.lean
theorem rbrSoundness_comp in ArkLib/Refactor/Security/Composition/Soundness.lean
def splitReplicate {pSpec : ProtocolSpec} (n : Nat) in ArkLib/Refactor/ProtocolSpec.lean
def run {m : Type → Type} [Monad m] {Output : Type} : in ArkLib/Refactor/Prover.lean
def run in ArkLib/Refactor/Telescope/Reduction.lean
def Reduction.compatContext in ArkLib/Refactor/LiftContext/Reduction.lean
def lagrangeBasis (pts : Vector R (n + 1)) (i : Fin (n + 1)) : CPolynomial R in ArkLib/Refactor/Sumcheck/PolyUtils.lean
def good {ctx : ProtocolCtx} {Claim : Type} : ClaimTree ctx Claim → Claim → Prop in ArkLib/Refactor/Telescope/Basic.lean
theorem PartialTranscript.leftFullOfAppend_concat in ArkLib/Refactor/Transcript.lean
theorem rbrKnowledgeSoundness_implies_oracleAwareRbrKnowledgeSoundness in ArkLib/Refactor/Security/StateFunction.lean
theorem lagrangeInterpolate_natDegree (pts vals : Vector R (n + 1)) : in ArkLib/Refactor/Sumcheck/PolyUtils.lean
theorem messageTypes_append (p₁ p₂ : ProtocolSpec) : in ArkLib/Refactor/ProtocolSpec.lean
theorem MessageOracleIdx_cons_P_to_V {T : Type} {oi : OracleInterface T} in ArkLib/Refactor/OracleVerifier.lean
abbrev F in ArkLib/Refactor/Sumcheck/Test.lean
def isChallenge : Round → Bool in ArkLib/Refactor/ProtocolSpec.lean
def isChallenge : ProtocolCtx → Bool in ArkLib/Refactor/Telescope/Basic.lean
def StateRestoration.KnowledgeSoundness in ArkLib/Refactor/Security/StateRestoration.lean
theorem generalVerifier_rbrSoundness in ArkLib/Refactor/Sumcheck/Security.lean
theorem MessageOracleIdx_nil : MessageOracleIdx [] = PEmpty in ArkLib/Refactor/OracleVerifier.lean
theorem liftContext_toVerifier_comm in ArkLib/Refactor/LiftContext/OracleReduction.lean
def challengeCount : ProtocolSpec → Nat in ArkLib/Refactor/ProtocolSpec.lean
def splitPrefix : in ArkLib/Refactor/Telescope/Basic.lean
theorem outputLang_subset_roundStateLang in ArkLib/Refactor/Sumcheck/General.lean
def terminalGood {ctx : ProtocolCtx} {Claim : Type} : in ArkLib/Refactor/Telescope/Basic.lean
def ofCtx (bm : BundledMonad) : ProtocolCtx → ProtocolCtxM in ArkLib/Refactor/Telescope/Basic.lean
def D : Fin 2 → F in ArkLib/Refactor/Sumcheck/Test.lean
theorem Verifier.oracleAwareRbrKnowledgeSoundness_compNth in ArkLib/Refactor/Security/Composition/KnowledgeSoundness.lean
def run {m : Type → Type} [Monad m] in ArkLib/Refactor/Telescope/Basic.lean
def prover in ArkLib/Refactor/Telescope/Sumcheck.lean
lemma oracleFree_comp {ι : Type} {oSpec : OracleSpec ι} in ArkLib/Refactor/Security/Composition/Util.lean
def PartialTranscript.take {pSpec : ProtocolSpec} {n : Nat} in ArkLib/Refactor/Transcript.lean
theorem Reduction.completeness_compNth in ArkLib/Refactor/Security/Composition/Completeness.lean
abbrev PartialTranscript (ctx : ProtocolCtx) (n : Nat) : Type in ArkLib/Refactor/Telescope/Basic.lean
theorem liftContext_rbrKnowledgeSoundness in ArkLib/Refactor/LiftContext/OracleReduction.lean
theorem sumOverLast_eval (D : Fin m → R) (p : CMvPolynomial (n + 1) R) (v : Fin n → R) : in ArkLib/Refactor/Sumcheck/PartialEval.lean
def Transcript.ofMessagesChallenges : in ArkLib/Refactor/Transcript.lean
def FSIdx (StmtIn : Type) : List Type → ProtocolSpec → Type in ArkLib/Refactor/FiatShamir.lean
theorem inputLang_iff_initState_mem_roundStateLang in ArkLib/Refactor/Sumcheck/General.lean
def Challenger.comp {m : Type → Type} [Monad m] : in ArkLib/Refactor/Telescope/Basic.lean
def singleChallenge (T : Type) : ProtocolSpec in ArkLib/Refactor/ProtocolSpec.lean
lemma get_eq_right (i : Fin (pSpec₁ ++ pSpec₂).length) (h : pSpec₁.length ≤ i.1) : in ArkLib/Refactor/ProtocolSpec.lean
def lagrangeInterpolateRawFast (pts vals : Vector R (n + 1)) : CPolynomial.Raw R in ArkLib/Refactor/Sumcheck/PolyUtils.lean
abbrev StmtIn in ArkLib/Refactor/Sumcheck/Defs.lean
def stateRestorationSoundness in ArkLib/Refactor/Security/StateRestoration.lean
def oracleImpl in ArkLib/Refactor/Telescope/OracleVerifier.lean
theorem soundness_mono in ArkLib/Refactor/Telescope/Security/Composition/Soundness.lean
def PartialTranscript.toFull {pSpec : ProtocolSpec} in ArkLib/Refactor/Transcript.lean
def Proof.completeness (Inv : σ → Prop) (langIn : Set (StmtIn × WitIn)) in ArkLib/Refactor/Security/Defs.lean
lemma run_comp_join_bind {m : Type → Type} [Monad m] [LawfulMonad m] in ArkLib/Refactor/Prover.lean
def roundPoly (D : Fin m → R) (k : ℕ) (p : CMvPolynomial (k + 1) R) : CPolynomial R in ArkLib/Refactor/Sumcheck/PartialEval.lean
def toUnivariate (p : CMvPolynomial 1 R) : CPolynomial R in ArkLib/Refactor/Sumcheck/PartialEval.lean
def comp : in ArkLib/Refactor/Telescope/Basic.lean
lemma get_eq_left (i : Fin (pSpec₁ ++ pSpec₂).length) (h : i.1 < pSpec₁.length) : in ArkLib/Refactor/ProtocolSpec.lean
def HonestProver.fiatShamir {ι : Type} {oSpec : OracleSpec ι} in ArkLib/Refactor/FiatShamir.lean
lemma probEvent_exists_finset_le_sum in ArkLib/Refactor/Security/Composition/Util.lean
theorem messageTypes_cons_V_to_P {T : Type} {tl : ProtocolSpec} : in ArkLib/Refactor/ProtocolSpec.lean
theorem soundness_of_comp_isSound in ArkLib/Refactor/Telescope/Security/Composition/Soundness.lean
theorem PartialTranscript.leftOfAppend_eq_ofTranscript_leftFullOfAppend in ArkLib/Refactor/Transcript.lean
def partialEvalPrefix : ∀ {i n : ℕ}, Vector R i → CMvPolynomial (n + i) R → CMvPolynomial n R in ArkLib/Refactor/Sumcheck/PartialEval.lean
theorem roundVerifierStateAsOracle_oracleFree (D : Fin m → R) : in ArkLib/Refactor/Sumcheck/Security.lean
theorem liftContext_rbrSoundness in ArkLib/Refactor/LiftContext/Reduction.lean
def roundStateLang (poly : OStmt R deg n) (D : Fin m → R) : in ArkLib/Refactor/Sumcheck/General.lean
def toReduction in ArkLib/Refactor/Reduction.lean
def Verifier.comp {m : Type → Type} [Monad m] {S₁ : Type} : in ArkLib/Refactor/Telescope/Basic.lean
def StatePreserving {ι : Type} {oSpec : OracleSpec ι} {σ : Type} in ArkLib/Refactor/Security/Composition/Util.lean
def eval (x : Fin n → R) (p : CMvDegreeLE R n d) : R in ArkLib/Refactor/Sumcheck/PolyUtils.lean
theorem Reduction.perfectCompleteness_compNth in ArkLib/Refactor/Security/Composition/Completeness.lean
theorem generalVerifier_soundness in ArkLib/Refactor/Sumcheck/Security.lean
def Transcript.split : in ArkLib/Refactor/Telescope/Basic.lean
def messageTypes : ProtocolSpec → List Type in ArkLib/Refactor/ProtocolSpec.lean
theorem PartialTranscript.rightOfAppend_ofTranscript_eq_split_snd in ArkLib/Refactor/Transcript.lean
def foldl {α : Type*} {A : α → Type*} {β : Type*} (f : ∀ (a : α), β → A a → β) : in ArkLib/Refactor/HVector.lean
def answerMsgQuery : in ArkLib/Refactor/OracleVerifier.lean
theorem rbrSoundness_implies_soundness in ArkLib/Refactor/Security/Composition/Soundness.lean
def initState (target : R) : RoundState (R in ArkLib/Refactor/Sumcheck/General.lean
def challengeTypes : ProtocolSpec → List Type in ArkLib/Refactor/ProtocolSpec.lean
theorem prefixPoint_spec {i n : ℕ} (fixed : Vector R i) (v : Fin n → R) (x : Fin (n + i)) : in ArkLib/Refactor/Sumcheck/PartialEval.lean
def MessageData : {ctx : ProtocolCtx} → Transcript ctx → Type in ArkLib/Refactor/Telescope/OracleVerifier.lean
def HonestProver (m : Type → Type) (StmtIn WitIn StmtOut WitOut : Type) in ArkLib/Refactor/Prover.lean
def inputRelation {n m : ℕ} (poly : OStmt R deg n) (D : Fin m → R) : Set (R × Unit) in ArkLib/Refactor/Sumcheck/Defs.lean
theorem toPoly_add' (p q : CPolynomial R) : in ArkLib/Refactor/Sumcheck/PolyUtils.lean
theorem PartialTranscript.leftOfAppend_concat in ArkLib/Refactor/Transcript.lean
def Verifier (m : Type → Type) (StmtIn : Type) (ctx : ProtocolCtxM) in ArkLib/Refactor/Telescope/Basic.lean
def symbolicGeneralReduction (poly : OStmt R deg n) (D : Fin m → R) : in ArkLib/Refactor/Sumcheck/General.lean
def ChallengeIndex (pSpec : ProtocolSpec) : Type in ArkLib/Refactor/ProtocolSpec.lean
def Terminal : {ctx : ProtocolCtx} → {Claim : Type} → in ArkLib/Refactor/Telescope/Basic.lean
def outputLang (poly : OStmt R deg n) : Set (RoundState (R in ArkLib/Refactor/Sumcheck/General.lean
def symbolicRoundHonestProver (D : Fin m → R) : in ArkLib/Refactor/Sumcheck/General.lean
def transcript : Transcript (generalPSpec F 1 2) in ArkLib/Refactor/Sumcheck/Test.lean
lemma rightIndexLt (i : Fin (pSpec₁ ++ pSpec₂).length) (h : pSpec₁.length ≤ i.1) : in ArkLib/Refactor/ProtocolSpec.lean
def take {α : Type*} {A : α → Type*} : in ArkLib/Refactor/HVector.lean
def id {m : Type → Type} [Monad m] in ArkLib/Refactor/Telescope/Reduction.lean
theorem toUnivariate_eval (p : CMvPolynomial 1 R) (x : R) : in ArkLib/Refactor/Sumcheck/PartialEval.lean
def replicate : Nat → ProtocolSpec → ProtocolSpec in ArkLib/Refactor/ProtocolSpec.lean
def PartialTranscript.concat : (n : Nat) → (ctx : ProtocolCtx) → in ArkLib/Refactor/Telescope/Basic.lean
def goodTargetFrom in ArkLib/Refactor/Telescope/Sumcheck.lean
theorem lagrangeInterpolate_eval (pts vals : Vector R (n + 1)) in ArkLib/Refactor/Sumcheck/PolyUtils.lean
def append {α : Type*} {A : α → Type*} : in ArkLib/Refactor/HVector.lean
def roundPoly₁ : CDegreeLE F 1 in ArkLib/Refactor/Sumcheck/Test.lean
theorem trueRoundPolyExists_of_ostmt in ArkLib/Refactor/Sumcheck/General.lean
def Transcript.toChallenges : in ArkLib/Refactor/Transcript.lean
def proverFrom : in ArkLib/Refactor/Telescope/Sumcheck.lean
theorem liftContext_perfectCompleteness in ArkLib/Refactor/LiftContext/OracleReduction.lean
def lagrangeBasisWithPlan (plan : InterpPlan R n) (i : Fin (n + 1)) : CPolynomial R in ArkLib/Refactor/Sumcheck/PolyUtils.lean
theorem MessageOracleIdx_cons_V_to_P {T : Type} {tl : ProtocolSpec} : in ArkLib/Refactor/OracleVerifier.lean
def OracleProver.liftContext in ArkLib/Refactor/LiftContext/OracleReduction.lean
def toReduction in ArkLib/Refactor/Telescope/Reduction.lean
def Messages.trivialOracleInterface (pSpec : ProtocolSpec) : in ArkLib/Refactor/FiatShamir.lean
theorem liftContext_rbrKnowledgeSoundness in ArkLib/Refactor/LiftContext/Reduction.lean
def srReplayChallenge in ArkLib/Refactor/Security/StateRestoration.lean
def symbolicRoundReduction (D : Fin m → R) : in ArkLib/Refactor/Sumcheck/General.lean
def FirstStageVerifierStep in ArkLib/Refactor/Security/Composition/Util.lean
def headType : ProtocolCtx → Type in ArkLib/Refactor/Telescope/Basic.lean
theorem liftContext_soundness in ArkLib/Refactor/LiftContext/OracleReduction.lean
def myPoly : CMvPolynomial 2 F in ArkLib/Refactor/Sumcheck/Test.lean
theorem liftContext_completeness in ArkLib/Refactor/LiftContext/Reduction.lean
theorem eval_add' (x : R) (p q : CPolynomial R) : in ArkLib/Refactor/Sumcheck/PolyUtils.lean
theorem IsSound.bound_terminalProb in ArkLib/Refactor/Telescope/Security/Defs.lean
def compNth {m : Type → Type} [Monad m] {S W : Type} in ArkLib/Refactor/Prover.lean
def subSpec_oracleSpecOfMessages_left : in ArkLib/Refactor/OracleVerifier.lean
def Prover.runFS {ι : Type} {oSpec : OracleSpec ι} in ArkLib/Refactor/FiatShamir.lean
theorem singleRoundVerifier_accept_of_backend in ArkLib/Refactor/Sumcheck/Completeness.lean
def Prover : (ctx : ProtocolCtxM) → (Transcript ctx → Type) → Type in ArkLib/Refactor/Telescope/Basic.lean
def OracleReduction.liftContext in ArkLib/Refactor/LiftContext/OracleReduction.lean
theorem messageTypes_take_succ (pSpec : ProtocolSpec) (n : Nat) : in ArkLib/Refactor/ProtocolSpec.lean
def follow : {ctx : ProtocolCtx} → {Claim : Type} → (tree : ClaimTree ctx Claim) → in ArkLib/Refactor/Telescope/Basic.lean
def Extractor.Straightline.liftContext in ArkLib/Refactor/LiftContext/Reduction.lean
def comp in ArkLib/Refactor/OracleVerifier.lean
def CMvDegreeLE (R : Type) [BEq R] [CommSemiring R] [LawfulBEq R] (n d : ℕ) in ArkLib/Refactor/Sumcheck/PolyUtils.lean
theorem challengeTypes_take_zero (pSpec : ProtocolSpec) : in ArkLib/Refactor/ProtocolSpec.lean
def toVerifier in ArkLib/Refactor/Telescope/OracleVerifier.lean
def g₁ : CompPoly.CPolynomial F in ArkLib/Refactor/Sumcheck/Test.lean
instance instOracleInterfaceCMvPolynomial : in ArkLib/Refactor/Sumcheck/PolyUtils.lean
def claimTreeFrom in ArkLib/Refactor/Telescope/Sumcheck.lean
def acceptsFrom in ArkLib/Refactor/Telescope/Sumcheck.lean
def Verifier.compatStatement in ArkLib/Refactor/LiftContext/Reduction.lean
theorem Transcript.truncate_succ' {T : Type} in ArkLib/Refactor/Telescope/Basic.lean
theorem PartialTranscript.rightOfAppend_hvector_take {pSpec₁ pSpec₂ : ProtocolSpec} in ArkLib/Refactor/Transcript.lean
theorem CPolynomial.natDegree_zero_le (d : ℕ) : in ArkLib/Refactor/Sumcheck/PartialEval.lean
def append (ctx₁ : ProtocolCtxM) (ctx₂ : Transcript ctx₁ → ProtocolCtxM) : in ArkLib/Refactor/Telescope/Basic.lean
theorem liftContext_knowledgeSoundness in ArkLib/Refactor/LiftContext/OracleReduction.lean
theorem generalReduction_perfectCompleteness_of_backend [DecidableEq R] in ArkLib/Refactor/Sumcheck/Security.lean
def srKnowledgeSoundnessGame in ArkLib/Refactor/Security/StateRestoration.lean
def Verifier (m : Type → Type) (StmtIn StmtOut : Type) (pSpec : ProtocolSpec) in ArkLib/Refactor/Verifier.lean
lemma oracleFree_statePreserving {ι : Type} {oSpec : OracleSpec ι} {σ : Type} in ArkLib/Refactor/Security/Composition/Util.lean
def ProtocolSpec in ArkLib/Refactor/ProtocolSpec.lean
def evalPoint {i : ℕ} (fixed : Vector R i) (D : Fin m → R) in ArkLib/Refactor/Sumcheck/Completeness.lean
def oracleAwareRbrSoundness (langIn : Set StmtIn) (langOut : Set StmtOut) in ArkLib/Refactor/Security/StateFunction.lean
theorem Verifier.knowledgeSoundness_compNth in ArkLib/Refactor/Security/Composition/KnowledgeSoundness.lean
def getType (pSpec : ProtocolSpec) (i : Fin pSpec.length) : Type in ArkLib/Refactor/ProtocolSpec.lean
abbrev chal (T : Type) : Round in ArkLib/Refactor/ProtocolSpec.lean
theorem maxPathError_comp : in ArkLib/Refactor/Telescope/Basic.lean
theorem Reduction.completeness_comp in ArkLib/Refactor/Security/Composition/Completeness.lean
theorem PartialTranscript.rightOfAppend_concat in ArkLib/Refactor/Transcript.lean
def simOracleSingle {T : Type} [OracleInterface T] (t : T) : in ArkLib/Refactor/Telescope/OracleVerifier.lean
abbrev OStmt (deg n : ℕ) in ArkLib/Refactor/Sumcheck/Defs.lean
def errorReplicate in ArkLib/Refactor/Security/Composition/Util.lean
theorem stateRestorationKnowledgeSoundness_implies_knowledgeSoundness in ArkLib/Refactor/Security/StateRestoration.lean
theorem eval_sum' {ι : Type} (x : R) (s : Finset ι) (f : ι → CPolynomial R) : in ArkLib/Refactor/Sumcheck/PolyUtils.lean
def lagrangeInterpolateWithPlan (plan : InterpPlan R n) (vals : Vector R (n + 1)) : in ArkLib/Refactor/Sumcheck/PolyUtils.lean
def Verifier.fiatShamir {ι : Type} {oSpec : OracleSpec ι} in ArkLib/Refactor/FiatShamir.lean
def roundPoly₂ : CDegreeLE F 1 in ArkLib/Refactor/Sumcheck/Test.lean
abbrev srChallengeOracle (StmtIn : Type) (pSpec : ProtocolSpec) in ArkLib/Refactor/Security/StateRestoration.lean
theorem claimTree_isSound in ArkLib/Refactor/Telescope/Sumcheck.lean
theorem PartialTranscript.leftFullOfAppend_ofTranscript_eq_split_fst in ArkLib/Refactor/Transcript.lean
lemma hvector_take_succ_eq_concat {pSpec : ProtocolSpec} in ArkLib/Refactor/Transcript.lean
def Transcript : ProtocolCtxM → Type in ArkLib/Refactor/Telescope/Basic.lean
def splitAt {α : Type*} {A : α → Type*} : in ArkLib/Refactor/HVector.lean
def HonestProver (m : Type → Type) in ArkLib/Refactor/Telescope/Reduction.lean
def nil : Messages ([] : ProtocolSpec) in ArkLib/Refactor/Transcript.lean
def Transcript.toMessages : in ArkLib/Refactor/Transcript.lean
def mapOutput : in ArkLib/Refactor/Telescope/Basic.lean
def errorAppend in ArkLib/Refactor/Security/Composition/Util.lean
def OracleFree {ι : Type} {oSpec : OracleSpec ι} {SIn SOut : Type} {pSpec : ProtocolSpec} in ArkLib/Refactor/Security/Composition/Util.lean
def verifier (D : Fin m → R) : in ArkLib/Refactor/Sumcheck/SingleRound.lean
lemma rightIndexLt' (i : Fin pSpec₂.length) : in ArkLib/Refactor/ProtocolSpec.lean
def PartialTranscript.leftOfAppend in ArkLib/Refactor/Transcript.lean
def toStateRestorationKnowledgeSoundness in ArkLib/Refactor/Security/StateRestoration.lean
theorem verifierFrom_soundness in ArkLib/Refactor/Telescope/Sumcheck.lean
def g₂ : CompPoly.CPolynomial F in ArkLib/Refactor/Sumcheck/Test.lean
def PartialTranscript.leftFullOfAppend in ArkLib/Refactor/Transcript.lean
def CDegreeLE (R : Type) [BEq R] [Semiring R] [LawfulBEq R] (d : ℕ) in ArkLib/Refactor/Sumcheck/PolyUtils.lean
theorem liftContext_completeness in ArkLib/Refactor/LiftContext/OracleReduction.lean
theorem partialEvalPrefix_individualDegreeLE {deg : ℕ} : in ArkLib/Refactor/Sumcheck/PartialEval.lean
def splitPrefix {m : Type → Type} [Monad m] {Output : Type} : in ArkLib/Refactor/Prover.lean
theorem sumAllButFirst_eval (D : Fin m → R) : in ArkLib/Refactor/Sumcheck/PartialEval.lean
theorem run_mapOutput {m : Type → Type} [Monad m] [LawfulMonad m] {A B : Type} (f : A → B) : in ArkLib/Refactor/Prover.lean
theorem liftContext_soundness in ArkLib/Refactor/LiftContext/Reduction.lean
theorem trueTarget_at_n in ArkLib/Refactor/Sumcheck/Completeness.lean
def sumAllButFirst (D : Fin m → R) : (k : ℕ) → CMvPolynomial (k + 1) R → CMvPolynomial 1 R in ArkLib/Refactor/Sumcheck/PartialEval.lean
def appendRight (i : ChallengeIndex pSpec₂) : ChallengeIndex (pSpec₁ ++ pSpec₂) in ArkLib/Refactor/ProtocolSpec.lean
theorem liftContext_run in ArkLib/Refactor/LiftContext/Reduction.lean
theorem challengeTypes_take_succ (pSpec : ProtocolSpec) (n : Nat) : in ArkLib/Refactor/ProtocolSpec.lean
def soundnessError : ℝ≥0 in ArkLib/Refactor/Sumcheck/Security.lean
theorem soundness_of_isSound in ArkLib/Refactor/Telescope/Security/Defs.lean
def srImplFromBasicAux in ArkLib/Refactor/Security/StateRestoration.lean
def Reduction.perfectCompleteness (Inv : σ → Prop) (relIn : Set (StmtIn × WitIn)) in ArkLib/Refactor/Security/Defs.lean
def rbrKnowledgeSoundness in ArkLib/Refactor/Security/StateFunction.lean
def Proof.soundness (langIn : Set StmtIn) in ArkLib/Refactor/Security/Defs.lean
def comp {m : Type → Type} [Monad m] in ArkLib/Refactor/Telescope/Reduction.lean
theorem rbrSoundness_compNth in ArkLib/Refactor/Security/Composition/Soundness.lean
def Reduction.liftContext {m : Type → Type} [Monad m] in ArkLib/Refactor/LiftContext/Reduction.lean
def singleRoundReduction {i : ℕ} in ArkLib/Refactor/Sumcheck/SingleRound.lean
theorem bound_terminalProb_comp in ArkLib/Refactor/Telescope/Security/Composition/Soundness.lean
def liftContext : in ArkLib/Refactor/LiftContext/Reduction.lean
def fsProtocolSpec (pSpec : ProtocolSpec) : ProtocolSpec in ArkLib/Refactor/FiatShamir.lean
def partialEvalFirst (a : R) (p : CMvPolynomial (n + 1) R) : CMvPolynomial n R in ArkLib/Refactor/Sumcheck/PartialEval.lean
def computeRoundPoly {n : ℕ} {m : ℕ} {i : ℕ} in ArkLib/Refactor/Sumcheck/Defs.lean
def comp {m : Type → Type} [Monad m] {S₁ S₂ S₃ : Type} in ArkLib/Refactor/Verifier.lean
def isMessage : ProtocolCtx → Bool in ArkLib/Refactor/Telescope/Basic.lean
def compNth in ArkLib/Refactor/OracleVerifier.lean
lemma run_comp_join {m : Type → Type} [Monad m] [LawfulMonad m] in ArkLib/Refactor/Prover.lean
def messageCount : ProtocolSpec → Nat in ArkLib/Refactor/ProtocolSpec.lean
theorem generalVerifierStateAsOracle_oracleFree (D : Fin m → R) : in ArkLib/Refactor/Sumcheck/Security.lean
def oracleAwareRbrKnowledgeSoundness in ArkLib/Refactor/Security/StateFunction.lean
def lagrangeInterpolateWithPlanRawFast (plan : InterpPlan R n) (vals : Vector R (n + 1)) : in ArkLib/Refactor/Sumcheck/PolyUtils.lean
def drop {α : Type*} {A : α → Type*} : in ArkLib/Refactor/HVector.lean
lemma run_splitPrefix_join in ArkLib/Refactor/Prover.lean
def Verifier.soundness (langIn : Set StmtIn) (langOut : Set StmtOut) in ArkLib/Refactor/Security/Defs.lean
theorem trueTarget_at_zero in ArkLib/Refactor/Sumcheck/Completeness.lean
theorem verifier_soundness in ArkLib/Refactor/Telescope/Sumcheck.lean
theorem Transcript.truncate_succ {T : Type} {oi : OracleInterface T} in ArkLib/Refactor/Telescope/Basic.lean
def comp in ArkLib/Refactor/Reduction.lean
def MessageOracleIdx : ProtocolSpec → Type in ArkLib/Refactor/OracleVerifier.lean
theorem rbrKnowledgeSoundness_implies_rbrSoundness in ArkLib/Refactor/Security/StateFunction.lean
theorem replicate_zero (pSpec : ProtocolSpec) : replicate 0 pSpec = [] in ArkLib/Refactor/ProtocolSpec.lean
theorem toUnivariate_natDegree_le {deg : ℕ} in ArkLib/Refactor/Sumcheck/PartialEval.lean
def Transcript.suffix : (n : Nat) → (ctx : ProtocolCtx) → in ArkLib/Refactor/Telescope/Basic.lean
def sumOverLast (D : Fin m → R) (p : CMvPolynomial (n + 1) R) : CMvPolynomial n R in ArkLib/Refactor/Sumcheck/PartialEval.lean
theorem oracleAwareRbrSoundness_implies_soundness in ArkLib/Refactor/Security/Composition/Soundness.lean
def roundProverStep in ArkLib/Refactor/Sumcheck/General.lean
lemma oracleFree_outputIndependent {ι : Type} {oSpec : OracleSpec ι} {σ : Type} in ArkLib/Refactor/Security/Composition/Util.lean
def nil {α : Type*} {A : α → Type*} : HVector A ([] : List α) in ArkLib/Refactor/HVector.lean
def srSoundnessGame in ArkLib/Refactor/Security/StateRestoration.lean
def toStateRestorationSoundness in ArkLib/Refactor/Security/StateRestoration.lean
theorem partialEvalPrefix_eval : in ArkLib/Refactor/Sumcheck/PartialEval.lean
theorem liftContext_knowledgeSoundness in ArkLib/Refactor/LiftContext/Reduction.lean
def runWithLog in ArkLib/Refactor/Telescope/Reduction.lean
def stateRestorationKnowledgeSoundness in ArkLib/Refactor/Security/StateRestoration.lean
def rbrSoundness (langIn : Set StmtIn) (langOut : Set StmtOut) in ArkLib/Refactor/Security/StateFunction.lean
def srInitFromBasic in ArkLib/Refactor/Security/StateRestoration.lean
theorem PartialTranscript.leftOfAppend_hvector_take {pSpec₁ pSpec₂ : ProtocolSpec} in ArkLib/Refactor/Transcript.lean
def Challenger : ProtocolCtxM → Type in ArkLib/Refactor/Telescope/Basic.lean
theorem Reduction.perfectCompleteness_comp in ArkLib/Refactor/Security/Composition/Completeness.lean
def cons {α : Type*} {A : α → Type*} {a : α} {as : List α} in ArkLib/Refactor/HVector.lean
theorem liftContext_rbrSoundness in ArkLib/Refactor/LiftContext/OracleReduction.lean
def PartialTranscript.aux : Nat → ProtocolCtx → Type in ArkLib/Refactor/Telescope/Basic.lean
def comp {m : Type → Type} [Monad m] {S₁ W₁ S₂ W₂ S₃ W₃ : Type} in ArkLib/Refactor/Prover.lean
theorem sumOverLast_monomials_get0_le {deg : ℕ} (D : Fin m → R) in ArkLib/Refactor/Sumcheck/PartialEval.lean
def OracleProver {ι : Type} (oSpec : OracleSpec ι) in ArkLib/Refactor/Reduction.lean
abbrev fsChallengeOracle (StmtIn : Type) (pSpec : ProtocolSpec) in ArkLib/Refactor/FiatShamir.lean
theorem Transcript.split_join : in ArkLib/Refactor/Telescope/Basic.lean
def empty : ProtocolSpec in ArkLib/Refactor/ProtocolSpec.lean
def cons {tl : ProtocolSpec} {r : Round} (val : r.type) (tr : Transcript tl) : in ArkLib/Refactor/Transcript.lean
def symbolicReductionState (D : Fin m → R) : in ArkLib/Refactor/Sumcheck/General.lean
theorem IsSound.comp in ArkLib/Refactor/Telescope/Security/Composition/Soundness.lean
def compNth in ArkLib/Refactor/Reduction.lean
theorem length_challengeTypes (pSpec : ProtocolSpec) : in ArkLib/Refactor/ProtocolSpec.lean
def Reduction.completeness (Inv : σ → Prop) (relIn : Set (StmtIn × WitIn)) in ArkLib/Refactor/Security/Defs.lean
def fsOracleSpec (StmtIn : Type) : (acc : List Type) → (pSpec : ProtocolSpec) → in ArkLib/Refactor/FiatShamir.lean
def toOracleAware in ArkLib/Refactor/Security/StateFunction.lean
def evalPts : Vector F 2 in ArkLib/Refactor/Sumcheck/Test.lean
def generalReduction in ArkLib/Refactor/Sumcheck/General.lean
def OracleProver {ι : Type} (oSpec : OracleSpec ι) in ArkLib/Refactor/Telescope/Reduction.lean
def run {m : Type → Type} [Monad m] in ArkLib/Refactor/Reduction.lean
def Extractor.Straightline (oSpec : OracleSpec ι) (StmtIn WitIn WitOut : Type) in ArkLib/Refactor/Security/Defs.lean
def inputLang {n m : ℕ} (poly : OStmt R deg n) (D : Fin m → R) : Set R in ArkLib/Refactor/Sumcheck/Defs.lean
def oracleImplOfOStmtInMessages {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} in ArkLib/Refactor/OracleVerifier.lean
def compileInterpPlan (pts : Vector R (n + 1)) : InterpPlan R n where in ArkLib/Refactor/Sumcheck/PolyUtils.lean
def singleRoundRbrError : ChallengeIndex (pSpec (R in ArkLib/Refactor/Sumcheck/Security.lean
def toLeft (i : ChallengeIndex (pSpec₁ ++ pSpec₂)) (h : i.1 < pSpec₁.length) : in ArkLib/Refactor/ProtocolSpec.lean
theorem partialEvalLast_eval (a : R) (p : CMvPolynomial (n + 1) R) (v : Fin n → R) : in ArkLib/Refactor/Sumcheck/PartialEval.lean
def singleMessage (T : Type) [oi : OracleInterface T] : ProtocolSpec in ArkLib/Refactor/ProtocolSpec.lean
def srImplFromBasic in ArkLib/Refactor/Security/StateRestoration.lean
lemma hvector_take_length_eq {pSpec : ProtocolSpec} (tr : Transcript pSpec) : in ArkLib/Refactor/Transcript.lean
theorem challengeTypes_nil : challengeTypes ([] : ProtocolSpec) = [] in ArkLib/Refactor/ProtocolSpec.lean
def PartialTranscript.remaining : (n : Nat) → (ctx : ProtocolCtx) → in ArkLib/Refactor/Telescope/Basic.lean
theorem roundPoly_eval (D : Fin m → R) (k : ℕ) (p : CMvPolynomial (k + 1) R) (x : R) : in ArkLib/Refactor/Sumcheck/PartialEval.lean
abbrev msg (T : Type) [oi : OracleInterface T] (bm : BundledMonad) (rest : ProtocolCtxM) : in ArkLib/Refactor/Telescope/Basic.lean
theorem messageTypes_cons_P_to_V {T : Type} {oi : OracleInterface T} {tl : ProtocolSpec} : in ArkLib/Refactor/ProtocolSpec.lean
theorem messageTypes_take_zero (pSpec : ProtocolSpec) : in ArkLib/Refactor/ProtocolSpec.lean
lemma leftIndexLt (i : Fin pSpec₁.length) : in ArkLib/Refactor/ProtocolSpec.lean
lemma oracleFree_compNth_verifier {ι : Type} {oSpec : OracleSpec ι} in ArkLib/Refactor/Security/Composition/Util.lean
theorem eval_mul' (x : R) (p q : CPolynomial R) : in ArkLib/Refactor/Sumcheck/PolyUtils.lean
def Messages.deriveTranscript {ι : Type} {oSpec : OracleSpec ι} in ArkLib/Refactor/FiatShamir.lean
def compNth {m : Type → Type} [Monad m] {S : Type} in ArkLib/Refactor/Verifier.lean
theorem oracleAwareRbrKnowledgeSoundness_implies_oracleAwareRbrSoundness in ArkLib/Refactor/Security/StateFunction.lean
theorem rbrSoundness_replicate_zero in ArkLib/Refactor/Security/Composition/Soundness.lean
def head {α : Type*} {A : α → Type*} {a : α} {as : List α} in ArkLib/Refactor/HVector.lean
def split (i : ChallengeIndex (pSpec₁ ++ pSpec₂)) : in ArkLib/Refactor/ProtocolSpec.lean
def ofSubSpec {ι₁ ι₂ : Type} {spec₁ : OracleSpec ι₁} {superSpec : OracleSpec ι₂} in ArkLib/Refactor/OracleVerifier.lean
def oracleSpecOfMessages : (pSpec : ProtocolSpec) → OracleSpec (MessageOracleIdx pSpec) in ArkLib/Refactor/OracleVerifier.lean
theorem partialEvalFirst_eval (a : R) (p : CMvPolynomial (n + 1) R) (v : Fin n → R) : in ArkLib/Refactor/Sumcheck/PartialEval.lean
theorem challengeTypes_append (p₁ p₂ : ProtocolSpec) : in ArkLib/Refactor/ProtocolSpec.lean
def OutputIndependent {ι : Type} {oSpec : OracleSpec ι} {σ : Type} in ArkLib/Refactor/Security/Composition/Util.lean
theorem length_messageTypes (pSpec : ProtocolSpec) : in ArkLib/Refactor/ProtocolSpec.lean
def Transcript.toPartial {pSpec : ProtocolSpec} in ArkLib/Refactor/Transcript.lean
theorem rbrKnowledgeSoundness_implies_knowledgeSoundness in ArkLib/Refactor/Security/Composition/KnowledgeSoundness.lean
def PartialTranscript.concat : in ArkLib/Refactor/Transcript.lean

sorry Tracking

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

theorem distanceLE_mvPolynomial_degreeLE {σ : Type} [Fintype σ] [DecidableEq σ] : in ArkLib/OracleReduction/OracleInterface.lean (L371)

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

theorem liftContext_toVerifier_comm in ArkLib/Refactor/LiftContext/OracleReduction.lean (L83)
theorem stateRestorationSoundness_implies_soundness in ArkLib/Refactor/Security/StateRestoration.lean (L380)
theorem liftContext_run in ArkLib/Refactor/LiftContext/Reduction.lean (L126)
theorem liftContext_knowledgeSoundness in ArkLib/Refactor/LiftContext/Reduction.lean (L210)
theorem stateRestorationKnowledgeSoundness_implies_knowledgeSoundness in ArkLib/Refactor/Security/StateRestoration.lean (L396)
theorem liftContext_rbrKnowledgeSoundness in ArkLib/Refactor/LiftContext/OracleReduction.lean (L202)
theorem liftContext_rbrSoundness in ArkLib/Refactor/LiftContext/OracleReduction.lean (L182)
def liftContext : in ArkLib/Refactor/LiftContext/Reduction.lean (L147)
theorem liftContext_rbrKnowledgeSoundness in ArkLib/Refactor/LiftContext/Reduction.lean (L231)
def OracleVerifier.liftContext in ArkLib/Refactor/LiftContext/OracleReduction.lean (L49)
def OracleVerifier.liftContext in ArkLib/Refactor/LiftContext/OracleReduction.lean (L52)
theorem liftContext_rbrSoundness in ArkLib/Refactor/LiftContext/Reduction.lean (L218)
theorem liftContext_knowledgeSoundness in ArkLib/Refactor/LiftContext/OracleReduction.lean (L174)
def srKnowledgeSoundnessGame in ArkLib/Refactor/Security/StateRestoration.lean (L237)
def srKnowledgeSoundnessGame in ArkLib/Refactor/Security/StateRestoration.lean (L277)
def srKnowledgeSoundnessGame in ArkLib/Refactor/Security/StateRestoration.lean (L293)
def srKnowledgeSoundnessGame in ArkLib/Refactor/Security/StateRestoration.lean (L309)
theorem liftContext_soundness in ArkLib/Refactor/LiftContext/OracleReduction.lean (L160)
theorem liftContext_completeness in ArkLib/Refactor/LiftContext/OracleReduction.lean (L129)
theorem liftContext_completeness in ArkLib/Refactor/LiftContext/Reduction.lean (L171)
theorem liftContext_soundness in ArkLib/Refactor/LiftContext/Reduction.lean (L197)

🎨 **Style Guide Adherence**

The following code changes violate the ArkLib style guide. Since there are more than 20 violations, they are grouped by rule below.

Grouped Violations

Rule: "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)."
- Violation Count: ~45
- Representative Examples:
  - def FSIdx in ArkLib/Refactor/FiatShamir.lean:41 (should be FsIdx)
  - def liftFSTail in ArkLib/Refactor/FiatShamir.lean:69 (should be liftFsTail)
  - abbrev OStmt in ArkLib/Refactor/Sumcheck/Defs.lean:60 (should be Ostmt)
  - class IsRBRSound in ArkLib/Refactor/Security/StateFunction.lean:79 (should be IsRbrSound)
Rule: "Every definition and major theorem should have a docstring."
- Violation Count: >100
- Representative Examples:
  - def HVector.nil in ArkLib/Refactor/HVector.lean:39 (lacks docstring)
  - theorem Reduction.completeness_comp in ArkLib/Refactor/Security/Composition/Completeness.lean:118 (lacks docstring)
  - def roundVerifierState in ArkLib/Refactor/Sumcheck/General.lean:41 (lacks docstring)
  - structure Witness.Lens in ArkLib/Refactor/LiftContext/Lens.lean:26 (lacks docstring)
Rule: "Variable Conventions: ... h, h₁, ... : Assumptions/Hypotheses" and "Functions and Terms: lowerCamelCase"
- Violation Count: >80
- Representative Examples:
  - hNe in ArkLib/OracleReduction/OracleInterface.lean:372 (uses CamelCase for a hypothesis; should be h_ne or h)
  - hDeg in ArkLib/OracleReduction/OracleInterface.lean:375 (uses CamelCase for a hypothesis; should be h_deg or h)
  - hPres in ArkLib/Refactor/Security/Composition/Completeness.lean:130 (uses CamelCase for a hypothesis; should be h_pres or h)
  - sz in ArkLib/OracleReduction/OracleInterface.lean:389 (non-standard variable name for a theorem result)
Rule: "Symbol Naming Dictionary: ≤ | le"
- Violation Count: ~15
- Representative Examples:
  - theorem distanceLE_mvPolynomial_degreeLE in ArkLib/OracleReduction/OracleInterface.lean:369 (should use le instead of LE)
  - structure CDegreeLE in ArkLib/Refactor/Sumcheck/PolyUtils.lean:71 (should use Le or le)

Specific Violations

Rule: "Functions and Terms: lowerCamelCase"
- is_complete in ArkLib/Refactor/Security/Defs.lean:126 (Class field uses snake_case)
- is_perfect_complete in ArkLib/Refactor/Security/Defs.lean:131 (Class field uses snake_case)
- is_sound in ArkLib/Refactor/Security/Defs.lean:159 (Class field uses snake_case)
- is_knowledge_sound in ArkLib/Refactor/Security/Defs.lean:192 (Class field uses snake_case)
- is_rbr_sound in ArkLib/Refactor/Security/StateFunction.lean:80 (Class field uses snake_case)
Rule: "Hypotheses: Prefer placing hypotheses to the left of the colon... rather than using arrows."
- ArkLib/Refactor/Security/StateRestoration.lean:186: OracleComp oSpec α) : ∀ (σ0 : σ) (ch : Challenges pSpec), ... := by (Should move σ0 and ch to the left of the colon as (σ0 : σ) (ch : Challenges pSpec) : ...)
- ArkLib/Refactor/Sumcheck/Security.lean:612: ∀ (k : Nat), rbrSoundness ... := by (Should move k to the left of the colon)

📄 **Per-File Summaries**

ArkLib.lean: This update expands the library's main entry point by importing a suite of new modules from the ArkLib.Refactor directory. These imports introduce refactored definitions and proofs for cryptographic components, including Fiat-Shamir transforms, Sumcheck protocols, and a general framework for security composition and soundness.
ArkLib/OracleReduction/OracleInterface.lean: This change provides a formal proof for the theorem distanceLE_mvPolynomial_degreeLE, which establishes a bound on the distance between multivariate polynomials with restricted degrees. The proof leverages the Schwartz-Zippel lemma and removes a previously existing sorry placeholder.
ArkLib/Refactor/FiatShamir.lean: This file introduces the definitions and infrastructure for the Fiat-Shamir transformation, which converts public-coin interactive reductions into non-interactive ones using a random oracle. It defines the FS oracle specification, logic for FS-compatible prover and verifier execution, and the final Reduction.fiatShamir transformation. The implementation is complete and contains no sorry placeholders.
ArkLib/Refactor/HVector.lean: This file introduces a heterogeneous vector type, HVector, implemented as a nested product of types to ensure universe stability across type families. It provides standard list-like operations such as map, append, splitAt, and get, along with custom notation and several structural theorems; no sorry placeholders are used.
ArkLib/Refactor/LiftContext.lean: This new file serves as a central entry point for the LiftContext module, aggregating imports for its lens, reduction, and oracle reduction submodules. It contains no new definitions, theorems, or sorry placeholders.
ArkLib/Refactor/LiftContext/Lens.lean: This file introduces several new definitions for "lenses" (such as Statement.Lens, Witness.Lens, and OracleContext.Lens) designed to transport statements, witnesses, and oracles between different protocol interface layers. It also establishes type classes to define and verify side-conditions for these lenses, including soundness, completeness, and knowledge soundness. No sorry or admit placeholders are included in the changes.
ArkLib/Refactor/LiftContext/OracleReduction.lean: This file introduces definitions and a framework for lifting oracle-based provers, verifiers, and reductions into larger contexts using lenses. It includes several theorem statements for the preservation of completeness and various forms of soundness under these lifts, though many definitions and nearly all proofs currently contain sorry placeholders.
ArkLib/Refactor/LiftContext/Reduction.lean: This file introduces infrastructure for lifting cryptographic reductions, honest provers, and verifiers into different contexts using a "lens" mechanism. It provides definitions for lifted components and establishes a theorem surface for proving the preservation of properties such as completeness and soundness, though most major preservation proofs currently contain sorry placeholders.
ArkLib/Refactor/OracleVerifier.lean: Introduces the OracleVerifier structure and supporting infrastructure for protocols requiring oracle access to prover messages and input statements via the OracleComp monad. Key additions include definitions for message-based oracle specifications, sequential verifier composition, and a conversion utility to standard Verifier types. No sorry or admit placeholders are present in the file.
ArkLib/Refactor/ProtocolSpec.lean: This file introduces a new list-based ProtocolSpec definition to replace the previous indexed version, simplifying protocol composition and oracle interface synthesis. It provides core definitions for prover and verifier rounds, extraction functions for message and challenge types, and several supporting theorems for indexing and replication without any sorry placeholders.
ArkLib/Refactor/Prover.lean: This file introduces the Prover and HonestProver types, providing a recursive framework for modeling interactive cryptographic protocols based on a ProtocolSpec. It includes definitions for running, composing, and splitting provers, supported by formal proofs (such as run_comp_join and run_splitPrefix_join) that verify the consistency of these operations. No sorry or admit placeholders are present in the implementation.
ArkLib/Refactor/Reduction.lean: This file introduces the Reduction and OracleReduction structures, which pair provers and verifiers as primary units for interactive proof composition. It provides definitions for sequential and $n$-fold composition of these reductions, along with a mechanism to convert oracle-based reductions into plain reductions.
ArkLib/Refactor/Security/Composition.lean: This file serves as a central entry point for security composition by re-exporting submodules related to completeness, soundness, and knowledge soundness. It introduces no new definitions or theorems directly, acting solely as a module aggregator for the composition framework.
ArkLib/Refactor/Security/Composition/Completeness.lean: This file establishes the formal foundation for completeness composition in protocol reductions, proving that completeness errors add linearly under reduction composition and $n$-fold iteration. It introduces several key theorems, including Reduction.completeness_comp and Reduction.completeness_compNth, and demonstrates that perfect completeness is preserved through these operations; no sorry placeholders are used.
ArkLib/Refactor/Security/Composition/KnowledgeSoundness.lean: This new file establishes the formal relationship between round-by-round (RBR) knowledge soundness and standard knowledge soundness within a cryptographic protocol framework. It introduces several key theorems, most notably proving that RBR knowledge soundness implies global knowledge soundness and providing a bounded error for the $n$-fold composition of protocols (knowledgeSoundness_compNth). No sorry or admit placeholders are present in the proofs.
ArkLib/Refactor/Security/Composition/Soundness.lean: This file establishes the mathematical foundation for the composition of Round-By-Round (RBR) soundness in cryptographic protocols, proving that RBR soundness implies standard protocol soundness with a summed error bound. It introduces new definitions and theorems for the sequential and $n$-fold composition of sound verifiers, demonstrating that soundness is preserved with additive error using state invariants and state functions. No sorry or admit placeholders are introduced in the proofs.
ArkLib/Refactor/Security/Composition/Util.lean: This file introduces utility definitions and lemmas for protocol composition, including error-map combinators for appended and replicated protocols and predicates for "oracle-free" verifiers. It establishes that oracle-freedom is preserved under sequential composition and replication, and provides a probabilistic union-bound lemma for existential statements. The file contains no sorry or admit placeholders.
ArkLib/Refactor/Security/Defs.lean: This file introduces new formal definitions for cryptographic security notions within a refactored IOP model, including challenge sampling infrastructure, completeness, and soundness. It establishes a framework for knowledge soundness using straight-line extractors and provides specialized definitions for proof systems, utilizing a unified probability formulation over challenge and oracle randomness. No sorry or admit placeholders are included.
ArkLib/Refactor/Security/StateFunction.lean: This new file introduces formal definitions and theorems for round-by-round (RBR) soundness and knowledge soundness in cryptographic protocols. It defines StateFunction and KnowledgeStateFunction structures, establishes probabilistic RBR security properties, and provides theorems bridging knowledge soundness to standard soundness in both basic and oracle-aware settings.
ArkLib/Refactor/Security/StateRestoration.lean: This file introduces a refactored framework for state-restoration (SR) security, including infrastructure for challenge replay and formal definitions for SR soundness and knowledge soundness. It establishes a constructive bridge between SR notions and basic outside-sampling security definitions, although several core lemmas and implication theorems currently contain sorry placeholders.
ArkLib/Refactor/Sumcheck/Completeness.lean: This file defines the "true" intermediate targets and round values for the Sumcheck protocol and provides a backend-agnostic proof of single-round perfect completeness. It introduces a RoundPolyBackend structure to specify honest prover behavior and proves several theorems relating partial sums to the verifier's acceptance criteria without using any sorry placeholders.
ArkLib/Refactor/Sumcheck/Defs.lean: This file introduces the core definitions and protocol specifications for a refactored sumcheck protocol, including structures for round states, oracle statements, and the evaluation-interpolation strategy for round polynomials. It consists entirely of new definitions and types without theorems or proofs, and contains no sorry placeholders.
ArkLib/Refactor/Sumcheck/General.lean: This file implements the multi-round Sumcheck protocol by modularly composing $n$ single-round steps using the compNth construction. It introduces definitions for the multi-round protocol specification, verifiers (plain and oracle), and provers (standard and symbolic), while proving the existence of valid round polynomials to support the protocol's completeness. No sorry or admit placeholders are present.
ArkLib/Refactor/Sumcheck/PartialEval.lean: This file introduces new definitions and theorems for computable partial evaluation and domain summation of multivariate polynomials, providing the core symbolic operations required for the Sumcheck protocol. It includes semantic correctness lemmas relating these operations to standard polynomial evaluation and provides proofs for bounding the degree of the resulting "round polynomials." No sorry or admit placeholders are present in the code.
ArkLib/Refactor/Sumcheck/PolyUtils.lean: This new file provides utility definitions and theorems for computable polynomials, introducing degree-bounded subtypes (CDegreeLE, CMvDegreeLE) and OracleInterface instances to support the sumcheck protocol. It establishes bridge lemmas between the library’s polynomial types and Mathlib's Polynomial and includes a verified, performance-optimized implementation of Lagrange interpolation. No sorry or admit placeholders are present.
ArkLib/Refactor/Sumcheck/Security.lean: This new file establishes the security properties of the general sumcheck protocol by introducing formal proofs for perfect completeness and round-by-round soundness. It derives the protocol's overall soundness error bound using a modular framework for composing interactive proofs and contains no sorry or admit placeholders.
ArkLib/Refactor/Sumcheck/SingleRound.lean: This new file introduces definitions for the core components of a single round of the sumcheck protocol, including the honest prover, a plain verifier, and an oracleVerifier. It also provides a singleRoundReduction to formalize the interaction between the prover and verifier, and contains no sorry placeholders.
ArkLib/Refactor/Sumcheck/Test.lean: This file introduces a concrete test suite for the sumcheck protocol implementation over ZMod 7, using native_decide to verify round-by-round computations and verifier acceptance. It also includes an end-to-end execution of the honest prover and verifier reduction via #eval!.
ArkLib/Refactor/Transcript.lean: This file introduces definitions and theorems for protocol transcripts, messages, and challenges, providing a framework for managing full and partial interactive protocol data. It implements operations for splitting and joining these structures using structural recursion to ensure definitional equalities necessary for protocol composition proofs. The file includes numerous lemmas relating partial transcript projections to HVector operations and contains no sorry or admit placeholders.
ArkLib/Refactor/Verifier.lean: This file introduces the Verifier definition, representing a "plain" verifier that processes full message transcripts directly without oracle access. It also provides foundational operations for modular protocol design, specifically sequential (comp) and iterated (compNth) composition of verifiers.
ArkLibRefactor.lean: This file serves as a top-level aggregator for the refactored ArkLib library, importing core modules related to cryptographic protocols, the Sumcheck protocol, and security definitions. It provides a centralized entry point for components such as Fiat-Shamir transformations, transcript handling, and proofs for completeness and soundness.
blueprint/src/content.tex: This change integrates a new section into the blueprint documenting a list-based refactor for Interactive Oracle Proofs (IOPs). It specifically introduces draft content for self-contained security and composition proofs within the oracle reductions framework.
blueprint/src/oracle_reductions/iop_refactor_security_composition.tex: This section formalizes the theoretical framework for a list-based IOP refactor, defining security notions such as round-by-round (RBR) soundness and knowledge soundness. It provides paper-style proofs for composing these local, per-round properties into global security bounds via union bounds and establishes the requirements for completeness under sequential composition in the presence of shared stateful oracles.
docs/design/iop-refactor.md: This design document proposes a major refactor of the Interactive Oracle Proof (IOP) framework, transitioning from Fin-indexed protocol specifications to a more flexible List-based model. The change aims to eliminate pervasive friction from index casting and rigid prover states, facilitating easier protocol composition and more robust proofs for round-by-round soundness. Key architectural updates include the use of heterogeneous vectors (HVector) for transcripts and a coinductive InteractOutputProver to simplify state management.
ArkLib/Refactor/Telescope/Security/Composition.lean: This new file establishes a composition layer for telescope-native security statements by re-exporting the path-sensitive soundness composition development. It currently serves as an umbrella module and introduces no new definitions, theorems, or sorry placeholders.
ArkLib/Refactor/Telescope/Security.lean: This new file establishes an umbrella module for the telescope security layer by aggregating definitions and composition theorems. It serves as a central entry point for the library's security substrate, focusing on semantic soundness and path-sensitive state functions.
ArkLib/Refactor/Telescope.lean: This new file serves as a central umbrella module for the "Telescopic Protocol Specifications" refactor, aggregating core definitions, oracle-aware runtime interfaces, and security properties. It establishes a structured entry point for the telescope-native refactor substrate, including its application to the Sumcheck protocol.
ArkLib/Refactor/Telescope/Reduction.lean: This file introduces a framework for statement-indexed "Telescope Reductions," defining core structures like HonestProver and OracleReduction to support challenger-driven protocol execution. It provides new definitions for the sequential composition and execution of these reductions, including utilities for logging oracle queries, and contains no sorry or admit placeholders.
ArkLib/Refactor/Telescope/Security/Composition/Soundness.lean: This file introduces new theorems establishing the soundness of staged protocol compositions within the Telescope framework, primarily proving that structural soundness is closed under composition (IsSound.comp) and providing associated error bounds. It culminates in a statement-indexed verifier soundness theorem for composed protocols and contains no sorry or admit placeholders.
ArkLib/Refactor/Telescope/OracleVerifier.lean: This file introduces a statement-indexed oracle verifier infrastructure that allows verifiers to query both statement-specific input oracles and prior prover messages extracted from a protocol transcript. It provides new definitions to reify transcript data into a queryable oracle interface and includes a utility to convert these indexed verifiers into concrete verifiers. No sorry placeholders are present in the new definitions.
ArkLib/Refactor/Telescope/Security/Defs.lean: This file introduces formal definitions and theorems for telescope protocol security, establishing the link between structural claim trees and verifier soundness. It provides the core theorem IsSound.bound_terminalProb to bound the probability of reaching a good terminal state from a bad root claim, and bridges this to a statement-indexed soundness definition via soundness_of_isSound. The implementation is complete and contains no sorry or admit placeholders.
ArkLib/Refactor/Telescope/Sumcheck.lean: This file implements a refactored version of the sumcheck protocol using the ProtocolCtx framework, threading the verifier's challenge prefix recursively through the protocol's state. It introduces new definitions for the telescope-native prover and verifier, along with comprehensive soundness theorems that establish probabilistic error bounds for the protocol. No sorry or admit placeholders are used in the implementation or proofs.
ArkLib/Refactor/Telescope/Basic.lean: This file introduces ProtocolCtx, a W-type for telescopic protocol specifications where round types and challenges depend on values exchanged in earlier rounds. It provides core definitions for transcripts, provers, and verifiers, implements sequential composition and prefix splitting, and defines a recursive ClaimTree structure for soundness analysis. The file introduces new definitions and theorems without any sorry or admit placeholders.

Last updated: 2026-03-10 01:41 UTC.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: b5ea17d64b

ℹ️ 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".

chatgpt-codex-connector · 2026-03-07T09:20:32Z

lakefile.toml

 name = "VCVio"
 git = "https://github.com/Verified-zkEVM/VCV-io"
-rev = "v4.28.0"
+rev = "master"


Pin VCVio dependency to an immutable revision

Setting VCVio to rev = "master" makes builds drift over time, because the dependency reference is a moving branch rather than a fixed commit/tag; a fresh dependency resolution can pull a newer VCVio state than the one this change was validated against and break ArkLib without any change in this repository. Pinning lakefile.toml to a concrete revision preserves reproducibility while still allowing intentional upgrades.

Useful? React with 👍 / 👎.

Introduce a telescope-native `ProtocolCtx` surface so runtime wrappers, soundness composition, and sumcheck share one maximally dependent cutover path. Keep the telescope slice warning-clean and buildable as an isolated migration target. Made-with: Cursor

quangvdao and others added 30 commits February 24, 2026 19:30

chore(Deps): update VCVio to master

5b305c2

Switch VCVio to track master and update the Lake manifest lock to 0e91cb33e47b92c41fc1ef0052ca58b0870cedd5. Made-with: Cursor

feat(Sumcheck): output evaluation claim in reduction

7ff29d1

Make the multi-round verifier/prover return the sampled challenge vector alongside the final value, so the remaining obligation can live in the reduction output language. Made-with: Cursor

fix(Sumcheck): clear non-sorry warnings in security proofs

b60c2c8

Remove unnecessary simp/simpa patterns and unused assumptions in Sumcheck security/completeness proofs so `ArkLib/Refactor` is warning-clean except for remaining `sorry` declarations. Made-with: Cursor

fix(Composition): clear non-sorry warnings in security composition

a818aef

Clean up lints in the composition security file by removing style and unused-argument warnings while preserving the existing theorem placeholders. Made-with: Cursor

refactor(Composition): advance soundness and knowledge-soundness cutover

ef7291c

Progress composition proofs by adding StateT run/map lemmas, wiring RBR knowledge-to-soundness bridge, and restructuring key proof blocks for ongoing completion. Made-with: Cursor

Fix compNth knowledge soundness Case 2 proof

fb87b9d

added new lagrange interpolation with proofs

5dcd59c

security: add oracle-aware trace defs and sumcheck language bridges

98830de

Refactor composition utilities into core modules

e045530

quangvdao and others added 16 commits March 1, 2026 13:06

Update VCVio dependency to latest master

42a05a0

sumcheck: factor RBR state-input bridge for general verifier

07b5356

sumcheck: refine single-round RBR state and append transcript helpers

bd5095e

refactor: improve transcript append projections and add RBR error maps

ea551b2

Merge remote-tracking branch 'origin/main' into quang/iop-refactor

59e47ec

Merge remote-tracking branch 'origin/main' into quang/iop-refactor

b5ea17d

quangvdao requested review from alexanderlhicks and dtumad and removed request for dtumad March 7, 2026 09:13

chatgpt-codex-connector bot reviewed Mar 7, 2026

View reviewed changes

quangvdao marked this pull request as draft March 8, 2026 06:09

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: List-based IOP model with composition & sumcheck security proofs#392

feat: List-based IOP model with composition & sumcheck security proofs#392
quangvdao wants to merge 47 commits intomainfrom
quang/iop-refactor

quangvdao commented Mar 7, 2026

Uh oh!

github-actions bot commented Mar 7, 2026 •

edited

Loading

Grouped Violations

Specific Violations

Uh oh!

chatgpt-codex-connector bot left a comment

Uh oh!

chatgpt-codex-connector bot Mar 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

quangvdao commented Mar 7, 2026

Summary

Motivation

Architecture

Other changes

Remaining sorrys (22 total)

Test plan

Uh oh!

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

Uh oh!

🤖 Gemini PR Summary

Core Formalization

Sumcheck Implementation

Infrastructure & Tooling

Proof Status & sorry Placeholders

Grouped Violations

Specific Violations

Uh oh!

chatgpt-codex-connector bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector bot Mar 7, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Remaining `sorry`s (22 total)

github-actions bot commented Mar 7, 2026 •

edited

Loading

Proof Status & `sorry` Placeholders