feat(Interaction): full interaction framework with concurrent semantics, open composition, and protocol frontends

[quangvdao]

Summary

This PR introduces the Interaction framework: a complete, sorry-free formalization of interactive protocol semantics in Lean 4, replacing the old flat ProtocolSpec model with a dependent-type-native design where later protocol rounds can depend on earlier moves.

The framework is organized in clean, acyclic layers, from sequential two-party protocols up to concurrent open-system composition. It also includes interaction-native frontends for Sumcheck and FRI, plus supporting computable polynomial infrastructure.

Scale: 126 commits, 211 files changed, ~41K lines added across 66 Interaction modules, 12 proof-system modules, 2 CompPoly modules, 7 blueprint chapters, 5 design documents, and CI/tooling updates.

What's in this PR

1. Core sequential interaction (Interaction/Basic/)

• Spec: W-type interaction trees with dependent branching (move types at later rounds depend on earlier moves)
• Transcript: complete plays through a Spec
• Decoration: per-node metadata with functorial mapping
• Node: realized node contexts, schemas, and telescope-style descriptions
• Syntax / Shape / Interaction: generic local participant syntax, functorial refinements, and local execution laws
• Strategy: one-player strategies with monadic effects
• Append / Replicate / Chain / StateChain: sequential composition, iteration, continuation-style telescopes, and stage-indexed state chains
• BundledMonad / MonadDecoration: per-node monadic effects
• Ownership: owner-based interaction model for building SyntaxOver objects

2. Two-party protocols (Interaction/TwoParty/)

• Role: sender/receiver roles with Action / Dual / interact
• Decoration: RoleDecoration plus RoleMonadContext / RolePairedMonadContext
• Strategy: Strategy.withRoles, Counterpart, PublicCoinCounterpart with transcript replay, runWithRoles execution, runWithRolesAndMonads for per-node monads
• Compose: append, replicate, stateChain composition for strategies and counterparts
• Refine: Role.Refine for role-aware data refinement (sender-specific data, no receiver padding)
• Swap: involutive role swap with composition lemmas
• Examples: concrete rfl proofs showing computed strategy types

3. Multiparty local views (Interaction/Multiparty/)

• Core: LocalView inductive (active / observe / hidden / quotient) for partial observability, localSyntax, multiparty Strategy via SyntaxOver.comap
• Profile: per-party ViewProfile for heterogeneous observation across parties
• Broadcast: public-transcript specialization (one acts, all observe)
• Directed: point-to-point sender/receiver edge decorations
• Examples: three-party knowledge-soundness, adversarial delivery, adaptive corruption scenarios
• Multiparty.lean (root): N-party as Spec + PartyDecoration, with MPST-style projection to roles via toRoles

4. Concurrent semantics (Interaction/Concurrent/)

Structural layer:

• Spec: structural concurrent syntax via binary par
• Frontier / Trace: enabled events and scheduler linearizations
• Independence / Interleaving: true-concurrency diamond lemma and trace equivalence

Dynamic process layer:

• Process: StepOver / ProcessOver (context-parametric) and closed-world Step / Process specializations with NodeSemantics (controllers + LocalView)
• Machine: state-indexed transition system frontend
• Tree: structural-tree frontend bridging to Process
• Control / Profile / Current: scheduler ownership, per-party profiles, and current local views

Verification layer:

• Execution / Run: finite prefixes and infinite runs with metadata extraction
• Observation: transcript matching relations (by controller, event, ticket, observation)
• Refinement: forward simulation with behavior preservation
• Bisimulation / Equivalence: symmetric refinement and packaged equivalence notions
• Policy: executable step policies with trace compliance
• Fairness: weak/strong fairness via stable tickets
• Liveness: temporal predicates, system-level safety/liveness under fairness

Open composition layer:

• Interface: Interface := PFunctor, Packet, Hom (chart), QueryHom (lens), Equiv, sum with composition laws
• OpenTheory: boundary-indexed algebra of open systems (map / par / wire / plug) with IsLawful typeclasses (functoriality, naturality)
• OpenSyntax: tagless-final free lawful model (Expr), proving OpenTheory coherence

Examples: in-flight delivery, looping processes, ticket bisimulation, observation simulation

5. Reductions and security (Interaction/Reduction.lean, Security.lean)

• Prover / Verifier / Reduction: interactive protocol participants over Spec + RoleDecoration
• PublicCoinVerifier: public-coin specialization
• Reduction.comp / stateChainComp / ofChain: sequential and chain-based composition
• Completeness / Soundness / Knowledge soundness: round-by-round analysis via claim trees
• ClaimTree / KnowledgeClaimTree: per-round security decomposition

6. Oracle layer (Interaction/Oracle/)

• Core: OracleDecoration attaching path-dependent oracle interfaces to interaction nodes, OracleCounterpart, OracleProver, OracleReduction, query routing
• Execution: runWithOracleCounterpart, accumulated oracle specs, honest public/execution equivalence
• Continuation: sequential and multi-round oracle reduction composition (Chain, comp)
• StateChain: oracle-aware state-chain verifier and reduction composition

7. Oracle security and reification (OracleSecurity.lean, OracleReification.lean)

• Behavior-first security: completeness, soundness, knowledge soundness for oracle reductions
• Reification bridge between abstract behaviors and concrete oracle statements
• Proof that reified knowledge soundness implies reified soundness

8. Boundaries (Interaction/Boundary/)

• Core: Statement / Witness / Context for same-transcript interface adaptation
• Oracle: OracleStatementAccess, pullbackCounterpart for oracle boundary transport
• Reification: OracleStatementReification, Realizes coherence predicate
• Security / OracleSecurity / Compatibility: transport of soundness, completeness, and simulation across boundaries

9. Fiat-Shamir (Interaction/FiatShamir/)

• Basic: ReplayOracle, MessagesOnly, deriveTranscript
• Transform: full Fiat-Shamir transform for provers, verifiers, and reductions

10. Proof system frontends

Sumcheck (ProofSystem/Sumcheck/Interaction/):

• Algebraic core: RoundClaim, domain summation, round specs with role decorations
• Single-round oracle reduction with proved execution equivalences
• N-round composition via stateChainComp (security proofs are scaffolding)
• Computable polynomial operations for sum-check (CompPoly.lean)

FRI (ProofSystem/Fri/Interaction/):

• Domain geometry, degree bounds, evaluation indexing
• Fold round / fold phase / final fold as oracle continuations
• Query round with consistency checks
• Full protocol composition via OracleReduction.comp

CompPoly (Data/CompPoly/):

• CDegreeLE / CMvDegreeLE degree-bounded types with OracleInterface instances
• splitNth / foldNth for computable polynomial splitting/folding

11. Documentation and infrastructure

Design documents:

• PORTING.md: core rebuild progress tracker
• INTERACTION_BOUNDARIES.md: boundary framework specification
• INTERACTION_CONCURRENT_SPEC.md: concurrent extension design reference
• INTERACTION_PROTOCOL_ROADMAP.md: literature-grounded protocol roadmap
• INTERACTION_BRACHA_VERIFICATION.md: Bracha RBC as benchmark target

Blueprint: New "Interaction Framework" chapter with 7 sections (foundations, composition, two-party, Fiat-Shamir, oracle, security, boundary)

Tooling:

• scripts/check-warning-log.py: new CI warning budget enforcement
• scripts/validate.sh: updated to run warning checks on Interaction/ and Data/ subtrees (excluding sorry warnings)
• Dependency bumps: CompPoly to fe33688, VCVio to 2fec633

Wiki: docs/wiki/repo-map.md updated with Interaction module map

Sorry status

• ArkLib/Interaction/ (66 files): 0 sorries (the entire abstract framework is sorry-free)
• Data/CompPoly/Fold.lean: 3 sorries (bridge lemmas to Mathlib toPoly)
• ProofSystem/Fri/Interaction/Core.lean: 2 sorries (honest fold degree bounds)
• ProofSystem/Sumcheck/Interaction/CompPoly.lean: 14 sorries (evaluation, degree, and ring hom lemmas)
• ProofSystem/Fri/RoundConsistency.lean: 1 sorry (Lagrange completeness)
• All sorries are in new code (not regressions); the canonical Sumcheck General.lean security proofs use trivial as explicit placeholders

Test plan

• lake build ArkLib succeeds
• ./scripts/validate.sh passes (warning budget, import check, docs integrity)
• No new non-sorry warnings in Interaction/ or Data/ subtrees
• Review sorry obligations in CompPoly and proof-system frontends (tracked, not blocking)
• Clean up untracked duplicate files (General (1).lean, SingleRound (1).lean)

---

Posted by Cursor assistant (model: claude-4.6-opus-high-thinking) on behalf of the user (Quang Dao) with approval.

[chatgpt-codex-connector]

Codex usage limits have been reached for code reviews. Please check with the admins of this repo to increase the limits by adding credits.
Credits must be used to enable repository wide code reviews.

[github-actions]

🤖 Gemini PR Summary

Formalizes a modular, dependently typed interaction framework in Lean 4, replacing the legacy ProtocolSpec with a native W-type-based system (Spec) where move types at later rounds depend on earlier moves. The framework spans from sequential two-party protocols to concurrent open-system composition, providing the infrastructure for modern interactive proof systems.

Core Interaction & Concurrency

• Sequential Foundations: Models protocols as interaction trees with dependent branching. Includes Transcript for execution plays, Decoration for per-node metadata, and a dual-role algebra (Role) for sender/receiver actions and strategies.
• Concurrent Semantics: Introduces structural concurrency via a binary parallelism operator (par). Includes a dynamic process layer (StepOver, ProcessOver), scheduler ownership, and formal verification tools for fairness, liveness, and trace equivalence (including a "True Concurrency" diamond lemma).
• Open System Composition: Implements an OpenTheory layer using a tagless-final approach. This allows algebraic composition of protocols using map, par, wire, and plug operators, governed by lawfulness typeclasses for functoriality and naturality.
• Multiparty Local Views: Provides a LocalView model for partial observability, enabling formalization of heterogeneous observation across parties, adaptive corruption, and adversarial delivery.

Oracle Security & Boundaries

• Oracle Layer: Integrates path-dependent oracle interfaces (OracleDecoration) and reductions (OracleReduction) with the VCVio library.
• Boundary Framework: Facilitates protocol interface adaptation (statements, witnesses, oracles) through pullback operations that preserve soundness and completeness across semantic layers.
• Reification: Establishes a bridge between abstract oracle behaviors and concrete data, proving that behavior-level knowledge soundness implies soundness in concrete executions.

Proof System Frontends & Computable Polynomials

• Sumcheck: Implemented as an N-round recursive oracle reduction. Supported by CompPoly, a new library for computable, degree-bounded multivariate polynomials tailored for partial evaluation and domain summation.
• FRI (Fast Reed-Solomon Interactive IOP): Formalized as a composition of folding rounds and query phases using the oracle continuation framework.
• Fiat-Shamir: Provides a generic transform to convert public-coin interactive protocols into non-interactive forms using sponge-based transcript hashing.

Critical Technical Details: sorry Placeholders

The core ArkLib/Interaction/ framework (66 files) is entirely sorry-free. However, placeholders remain in the following peripheral or higher-level modules:

• Data/CompPoly/Fold.lean: 3 sorries regarding bridge lemmas to Mathlib toPoly and degree bounds.
• ProofSystem/Fri/Interaction/Core.lean: 2 sorries concerning honest fold degree bounds.
• ProofSystem/Sumcheck/Interaction/CompPoly.lean: 14 sorries for algebraic properties (evaluation, degree, ring homomorphisms).
• ProofSystem/Fri/RoundConsistency.lean: 1 sorry for Lagrange completeness.
• ProofSystem/Sumcheck/Interaction/General.lean: Security proofs are currently scaffolded with trivial placeholders.

Infrastructure & Documentation

• Blueprint: Adds a new "Interaction Framework" chapter with seven sections covering foundations, composition, security, and boundaries.
• Design Docs: Includes specifications for concurrency (INTERACTION_CONCURRENT_SPEC.md), boundaries (INTERACTION_BOUNDARIES.md), and the protocol roadmap.
• Tooling: Updates validate.sh and introduces a Python-based CI script to enforce warning budgets in the Interaction/ and Data/ subtrees.

---

Statistics

Metric	Count
📝 Files Changed	67
✅ Lines Added	21489
❌ Lines Removed	110

---

Lean Declarations

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

• abbrev IsComplete in ArkLib/Interaction/Boundary/Compatibility.lean
• def OracleCounterpart.mapOutput {ι : Type} {oSpec : OracleSpec.{0, 0} ι} in ArkLib/Interaction/Oracle/Core.lean
• theorem plain_oracleSenderIndependent : in ArkLib/Interaction/BCS/HybridDecoration.lean
• def queryRoundContinuation in ArkLib/ProofSystem/Fri/Interaction/QueryRound.lean
• theorem perfectCompleteness_pullback in ArkLib/Interaction/Boundary/Security.lean
• abbrev afterMessage in ArkLib/Interaction/FiatShamir/DuplexSponge.lean
• def appendRight : in ArkLib/Interaction/Oracle/Core.lean
• def pullbackSimulate in ArkLib/Interaction/Boundary/Oracle.lean
• abbrev afterChallenge in ArkLib/Interaction/FiatShamir/DuplexSponge.lean
• def residualDegreeBound (i : ℕ) : ℕ in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def Strategy.ofChain {m : Type u → Type u} [Monad m] in ArkLib/Interaction/Reduction.lean
• theorem simulateQ_cast_spec in ArkLib/Interaction/Oracle/Core.lean
• theorem simulateQ_cast in ArkLib/Interaction/Oracle/Core.lean
• def evalPointVal (i : ℕ) (idx : EvalIdx (n in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def pullback in ArkLib/Interaction/Boundary/Reification.lean
• theorem Reduction.completeness_comp in ArkLib/Interaction/Security.lean
• def reifiedPerfectCompleteness in ArkLib/Interaction/OracleReification.lean
• def Prover.fiatShamir in ArkLib/Interaction/FiatShamir/Transform.lean
• def completeness in ArkLib/Interaction/OracleSecurity.lean
• abbrev VerifierOutput in ArkLib/Interaction/Oracle/Core.lean
• abbrev OracleStatement {ιₛ : Type v} (OStmt : ιₛ → Type w) in ArkLib/Interaction/Oracle/Core.lean
• def toFSStatement in ArkLib/Interaction/FiatShamir/DuplexSponge.lean
• def od : {n : Nat} → (c : Chain n) → OracleDecoration (toSpec c) (roles c) in ArkLib/Interaction/Oracle/Continuation.lean
• def answerSplitLiftAppendQuery in ArkLib/Interaction/OracleReification.lean
• theorem partialEvalFirst_eval (a : R) (p : CMvPolynomial (n + 1) R) (v : Fin n → R) : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• def run in ArkLib/Interaction/Oracle/Continuation.lean
• abbrev Prover (m : Type u → Type u) in ArkLib/Interaction/Reduction.lean
• theorem foldNth_natDegree_le_of_le in ArkLib/Data/CompPoly/Fold.lean
• theorem roundOracleReduction_execute_eq_stateful in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• def IndividualDegreeLE (deg : ℕ) (p : CMvPolynomial n R) : Prop in ArkLib/Data/CompPoly/Basic.lean
• abbrev InputStatement : Type in ArkLib/ProofSystem/Fri/Interaction/Protocol.lean
• def finalFoldRoles : RoleDecoration (finalFoldSpec (F in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def finalFoldOD : in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def outputRelationOfRelation in ArkLib/Interaction/OracleReification.lean
• abbrev squeezeLen in ArkLib/Interaction/FiatShamir/DuplexSponge.lean
• def OracleDecoration.QueryHandle : in ArkLib/Interaction/Oracle/Core.lean
• theorem simulateQ_add_liftComp_left in ArkLib/Interaction/Boundary/Oracle.lean
• abbrev PolyStmt (R : Type) [BEq R] [CommSemiring R] [LawfulBEq R] in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• def fsContext (Context : StatementIn → Spec.{u}) in ArkLib/Interaction/FiatShamir/Transform.lean
• def inputRelationOfReifiedRelation in ArkLib/Interaction/OracleReification.lean
• theorem pullbackSimulate_eval in ArkLib/Interaction/Boundary/Oracle.lean
• abbrev foldRoundCodeword in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def honestCodeword (i : ℕ) (p : HonestPoly (F in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• abbrev serialize in ArkLib/Interaction/FiatShamir/DuplexSponge.lean
• def liftOutput in ArkLib/Interaction/Oracle/Core.lean
• theorem honestFinalPolynomial_natDegree_le in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• theorem roundOracleReduction_honestExecutionEquivalentStateful in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• abbrev FoldChallenges : Type in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def foldPhaseContinuation {ι : Type} {oSpec : OracleSpec ι} in ArkLib/ProofSystem/Fri/Interaction/FoldPhase.lean
• def splitNth (n : ℕ) [NeZero n] (p : CPolynomial R) : Fin n → CPolynomial R in ArkLib/Data/CompPoly/Fold.lean
• def Verifier.run {m : Type u → Type u} [Monad m] in ArkLib/Interaction/Reduction.lean
• def currentRoundResidual {n prefixLen : Nat} (h : prefixLen < n) in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• def fsStatementOut in ArkLib/Interaction/FiatShamir/Transform.lean
• def roles : {n : Nat} → (c : Chain n) → RoleDecoration (toSpec c) in ArkLib/Interaction/Oracle/Continuation.lean
• abbrev PolyFamily (R : Type) [BEq R] [CommSemiring R] [LawfulBEq R] in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• theorem realizes_materializeOut in ArkLib/Interaction/Boundary/Reification.lean
• instance of interpreter lifting (cf. Xia et al., *Interaction Trees*): the inner in ArkLib/Interaction/Boundary/Oracle.lean
• abbrev FinalStatement : Type in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def routeInnerOutputQueries in ArkLib/Interaction/Boundary/Oracle.lean
• def foldRoundRoles in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• theorem realizes_simOracle0 in ArkLib/Interaction/OracleSecurity.lean
• abbrev roles in ArkLib/Interaction/Reduction.lean
• def fsWitnessOut in ArkLib/Interaction/FiatShamir/Transform.lean
• def chainComp in ArkLib/Interaction/Oracle/Continuation.lean
• theorem simulateQ_map in ArkLib/Interaction/Boundary/Oracle.lean
• theorem sumAllButFirst_eval (D : Fin m → R) : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• def liftAppendLeftQueries : in ArkLib/Interaction/Oracle/Core.lean
• theorem isKnowledgeSound_implies_isSound in ArkLib/Interaction/Security.lean
• def randomChallenger (sample : (T : Type) → ProbComp T) : in ArkLib/Interaction/Security.lean
• def OracleDecoration.oracleContextImpl in ArkLib/Interaction/Oracle/Core.lean
• theorem toUnivariate_natDegree_le {deg : ℕ} in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• def PublicCoinVerifier.fiatShamir in ArkLib/Interaction/FiatShamir/Transform.lean
• theorem toUnivariate_eval (p : CMvPolynomial 1 R) (x : R) : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• theorem routeInnerOutputQueries_materialize in ArkLib/Interaction/Boundary/Reification.lean
• abbrev InputImpl in ArkLib/Interaction/OracleSecurity.lean
• def evalSize (i : ℕ) : ℕ in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• theorem toMonadDecoration_append in ArkLib/Interaction/Oracle/Execution.lean
• theorem partialEvalLast_eval (a : R) (p : CMvPolynomial (n + 1) R) (v : Fin n → R) : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• def IsKnowledgeSound {m : Type u → Type u} [Monad m] [HasEvalSPMF m] in ArkLib/Interaction/Security.lean
• def stepResidual (chal : R) in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• def Reduction.stateChainComp {m : Type u → Type u} [Monad m] in ArkLib/Interaction/Reduction.lean
• abbrev ReifiedOutputRelation in ArkLib/Interaction/OracleReification.lean
• def inputLanguageOfReifiedLanguage in ArkLib/Interaction/OracleReification.lean
• def currentResidual {n prefixLen : Nat} (h : prefixLen ≤ n) in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• theorem answerSplitLiftAppendQueryAppend_simOracle0 in ArkLib/Interaction/Oracle/Execution.lean
• theorem runWithOracleCounterpart_mapCounterpartOutput in ArkLib/Interaction/Oracle/Execution.lean
• def SimulatesConcrete in ArkLib/Interaction/OracleReification.lean
• abbrev OutputLanguage in ArkLib/Interaction/OracleSecurity.lean
• def mapExecuteWitness in ArkLib/Interaction/Oracle/Execution.lean
• def runConcrete in ArkLib/Interaction/Oracle/Execution.lean
• def Prover.duplexSpongeFiatShamir in ArkLib/Interaction/FiatShamir/DuplexSponge.lean
• def terminalGood {spec : Spec} {roles : RoleDecoration spec} {Claim : Type u} in ArkLib/Interaction/Security.lean
• def pullbackCounterpart in ArkLib/Interaction/Boundary/Oracle.lean
• def liftAppendRightQueries : in ArkLib/Interaction/Oracle/Core.lean
• theorem routeInnerOutputQueries_eval in ArkLib/Interaction/Boundary/Oracle.lean
• def CMvDegreeLE in ArkLib/Data/CompPoly/Basic.lean
• def OracleReduction.stateChainComp {ι : Type} {oSpec : OracleSpec ι} in ArkLib/Interaction/Oracle/StateChain.lean
• abbrev HonestProverOutput (StatementOut : Type u) (WitnessOut : Type v) in ArkLib/Interaction/Reduction.lean
• def foldNth (n : ℕ) [NeZero n] (p : CPolynomial R) (α : R) : in ArkLib/Data/CompPoly/Fold.lean
• abbrev foldPhaseOD : in ArkLib/ProofSystem/Fri/Interaction/FoldPhase.lean
• theorem simulateQ_compose in ArkLib/Interaction/Boundary/Oracle.lean
• abbrev OracleDecoration (spec : Spec) (roles : RoleDecoration spec) in ArkLib/Interaction/Oracle/Core.lean
• abbrev PublicCoinVerifier (m : Type u → Type u) in ArkLib/Interaction/Reduction.lean
• def reifiedKnowledgeSoundness in ArkLib/Interaction/OracleReification.lean
• abbrev afterMessage {X : Type u} {rest : X → Spec} {rRest : ∀ x, RoleDecoration (rest x)} in ArkLib/Interaction/FiatShamir/Basic.lean
• theorem simulateQ_compConcrete in ArkLib/Interaction/OracleReification.lean
• theorem simulateQ_liftAppendRightContext_eq in ArkLib/Interaction/Oracle/Core.lean
• theorem simulateQ_liftAppendLeftContext_eq in ArkLib/Interaction/Oracle/Core.lean
• def replay {m : Type u → Type u} [Monad m] in ArkLib/Interaction/Reduction.lean
• theorem soundness_of_rbrSoundness in ArkLib/Interaction/Security.lean
• def finalFoldContinuation {SharedIn : Type} {ι : Type} {oSpec : OracleSpec ι} in ArkLib/ProofSystem/Fri/Interaction/FinalFold.lean
• def pullbackVerifier in ArkLib/Interaction/Boundary/Oracle.lean
• def comp {ι : Type} {oSpec : OracleSpec ι} in ArkLib/Interaction/Oracle/Continuation.lean
• def Reduction.ofChain {m : Type u → Type u} [Monad m] in ArkLib/Interaction/Reduction.lean
• def liftAppendRightContext : in ArkLib/Interaction/Oracle/Core.lean
• abbrev ReifiedInputLanguage in ArkLib/Interaction/OracleReification.lean
• def roundRoles : RoleDecoration (roundSpec R deg) in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• def executeConcrete in ArkLib/Interaction/Oracle/Execution.lean
• abbrev RoundClaim in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• def routeInputQueriesOuterEval in ArkLib/Interaction/Boundary/Oracle.lean
• def fullSum {n : ℕ} {m_dom : ℕ} (D : Fin m_dom → R) (poly : PolyStmt R deg n) : R in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• theorem knowledgeSoundness_implies_soundness in ArkLib/Interaction/OracleSecurity.lean
• theorem simulateQ_collapseAppendOracleComp in ArkLib/Interaction/Oracle/Execution.lean
• def partialEvalPrefix : {i k : ℕ} → (Fin i → R) → CMvPolynomial (i + k) R → CMvPolynomial k R in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• theorem pullbackSimulate_materialize in ArkLib/Interaction/Boundary/Reification.lean
• def SpongeAnnotation (U : Type) : in ArkLib/Interaction/FiatShamir/DuplexSponge.lean
• def OracleDecoration.toOracleSpec : in ArkLib/Interaction/Oracle/Core.lean
• theorem completeness_pullback in ArkLib/Interaction/Boundary/Security.lean
• abbrev OutputImpl in ArkLib/Interaction/OracleSecurity.lean
• abbrev fullOD (n : Nat) : in ArkLib/ProofSystem/Sumcheck/Interaction/General.lean
• theorem runWithOracleCounterpart_pullbackCounterpart_raw in ArkLib/Interaction/Boundary/Oracle.lean
• def soundness in ArkLib/Interaction/OracleSecurity.lean
• theorem simulateQ_cast_dep in ArkLib/Interaction/Oracle/Core.lean
• def Realizes in ArkLib/Interaction/Boundary/Reification.lean
• def accSpecAfter : in ArkLib/Interaction/Oracle/Execution.lean
• theorem evalSize_pos (i : ℕ) : 0 < evalSize (n in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• theorem appendRight_range : in ArkLib/Interaction/Oracle/Core.lean
• theorem splitLiftAppendOracleRange_eq in ArkLib/Interaction/Oracle/Execution.lean
• def Terminal {spec : Spec} {roles : RoleDecoration spec} {Claim : Type u} in ArkLib/Interaction/Security.lean
• theorem appendLeft_range : in ArkLib/Interaction/Oracle/Core.lean
• abbrev EmptyOracleFamily : PEmpty → Type in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def Counterpart.ofChain {m : Type u → Type u} [Monad m] in ArkLib/Interaction/Reduction.lean
• abbrev foldRoundChallenge in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• abbrev fullSpec (n : Nat) : Spec in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• theorem answerQuery_appendRight : in ArkLib/Interaction/Oracle/Core.lean
• def roundPoly (D : Fin m → R) (k : ℕ) (p : CMvPolynomial (k + 1) R) : CPolynomial R in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• abbrev liftAppendOracleFamily in ArkLib/Interaction/Oracle/Execution.lean
• theorem sumcheckReduction_completeness in ArkLib/ProofSystem/Sumcheck/Interaction/General.lean
• def OutputRealizes in ArkLib/Interaction/OracleSecurity.lean
• theorem realizes_materializeIn in ArkLib/Interaction/Boundary/Reification.lean
• theorem Reduction.execute_comp in ArkLib/Interaction/Reduction.lean
• def PublicCoinVerifier.duplexSpongeFiatShamir in ArkLib/Interaction/FiatShamir/DuplexSponge.lean
• theorem knowledgeSoundness_implies_soundness in ArkLib/Interaction/Security.lean
• theorem simulateQ_compose_lambda in ArkLib/Interaction/Oracle/Core.lean
• def appendLeft : in ArkLib/Interaction/Oracle/Core.lean
• def id in ArkLib/Interaction/Oracle/Continuation.lean
• abbrev finalFoldChallenge in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def collapseAppendOracleComp in ArkLib/Interaction/Oracle/Execution.lean
• theorem answerQuery_appendLeft : in ArkLib/Interaction/Oracle/Core.lean
• def Reduction.execute {m : Type u → Type u} [Monad m] in ArkLib/Interaction/Reduction.lean
• abbrev Output in ArkLib/Interaction/OracleReification.lean
• abbrev foldPhaseContext : Spec in ArkLib/ProofSystem/Fri/Interaction/FoldPhase.lean
• abbrev InputRelation in ArkLib/Interaction/OracleSecurity.lean
• def rbrSoundness in ArkLib/Interaction/Security.lean
• abbrev roundChallenge (tr : Spec.Transcript (roundSpec R deg)) : in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• theorem roundProverStepStateful_fromResidual in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• def queryRoundSpec : Spec in ArkLib/ProofSystem/Fri/Interaction/QueryRound.lean
• def routeInputQueries in ArkLib/Interaction/Boundary/Oracle.lean
• def deriveTranscript : in ArkLib/Interaction/FiatShamir/Basic.lean
• def advance in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• def Reduction.completeness in ArkLib/Interaction/Security.lean
• def queryBatchConsistent in ArkLib/ProofSystem/Fri/Interaction/QueryRound.lean
• def pullbackShared in ArkLib/Interaction/Oracle/Continuation.lean
• def liftAppendLeftQuery : in ArkLib/Interaction/Oracle/Core.lean
• def partialEvalFirst (a : R) (p : CMvPolynomial (n + 1) R) : CMvPolynomial n R in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• def maxPathError {spec : Spec} {roles : RoleDecoration spec} {Claim : Type u} in ArkLib/Interaction/Security.lean
• theorem roundProverStep_map_fst in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• def pullback {m : Type _ → Type _} [Monad m] [Functor m] in ArkLib/Interaction/Boundary/Core.lean
• def roundFiberIdx in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def challengePrefix (n : Nat) (tr : Spec.Transcript (fullSpec R deg n)) : in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• def initialCodewords (codeword : Codeword (F in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def roundArity (i : Fin (k + 1)) : ℕ in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def queryRoundRoles : RoleDecoration (queryRoundSpec (n in ArkLib/ProofSystem/Fri/Interaction/QueryRound.lean
• def runWithOracleCounterpart in ArkLib/Interaction/Oracle/Execution.lean
• def honestFoldPoly {i : Fin k} in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• theorem simulateQ_add_liftComp_right in ArkLib/Interaction/Boundary/Oracle.lean
• abbrev EvalIdx (i : ℕ) in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def sumOverLast (D : Fin m → R) (p : CMvPolynomial (n + 1) R) : CMvPolynomial n R in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• def toUnivariate (p : CMvPolynomial 1 R) : CPolynomial R in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• abbrev liftAppendOracleIdx in ArkLib/Interaction/Oracle/Execution.lean
• def finalFoldSpec : Spec in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• abbrev FoldCodewordOracleFamily in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• abbrev OracleProver {ι : Type} (oSpec : OracleSpec.{0, 0} ι) in ArkLib/Interaction/Oracle/Core.lean
• theorem Reduction.perfectCompleteness_comp in ArkLib/Interaction/Security.lean
• def liftAppendRightQuery : in ArkLib/Interaction/Oracle/Core.lean
• abbrev QueryResult : Type in ArkLib/ProofSystem/Fri/Interaction/QueryRound.lean
• theorem roundProverStep_map_residualWitness in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• def statementResult {m_dom : Nat} (D : Fin m_dom → R) : in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• theorem roundProverStep_map_honestProverOutputWitness in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• theorem sumOverLast_eval (D : Fin m → R) (p : CMvPolynomial (n + 1) R) (v : Fin n → R) : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• def perfectCompleteness in ArkLib/Interaction/OracleSecurity.lean
• def forgetExecuteWitness in ArkLib/Interaction/Oracle/Execution.lean
• def nextRoundIdx in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def RoundCheckProp {m_dom : ℕ} (D : Fin m_dom → R) (target : RoundClaim R) in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• abbrev FSStatement (StatementIn : Type u) (Context : StatementIn → Spec.{u}) in ArkLib/Interaction/FiatShamir/Transform.lean
• def good {spec : Spec} {roles : RoleDecoration spec} {Claim : Type u} in ArkLib/Interaction/Security.lean
• abbrev Proof (m : Type u → Type u) in ArkLib/Interaction/Reduction.lean
• def toVerifier in ArkLib/Interaction/Oracle/Core.lean
• def pullback in ArkLib/Interaction/Boundary/Oracle.lean
• def initialChallenges : FoldChallengePrefix (F in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• theorem rbrKnowledgeSoundness_implies_knowledgeSoundness in ArkLib/Interaction/Security.lean
• def spongeReplayOracle in ArkLib/Interaction/FiatShamir/DuplexSponge.lean
• theorem IsSound.bound_terminalProb in ArkLib/Interaction/Security.lean
• theorem foldNth_toPoly (n : ℕ) [NeZero n] (p : CPolynomial R) (α : R) : in ArkLib/Data/CompPoly/Fold.lean
• def roundSpec : Spec in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• def accImplAfter : in ArkLib/Interaction/Oracle/Execution.lean
• theorem honestFoldPoly_natDegree_le {i : Fin k} in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• abbrev InteractiveOracleVerifier {ι : Type} (oSpec : OracleSpec.{0, 0} ι) in ArkLib/Interaction/Oracle/Core.lean
• def outputRelationOfReifiedRelation in ArkLib/Interaction/OracleReification.lean
• theorem execute_pullback in ArkLib/Interaction/Boundary/Security.lean
• theorem simulateQ_map in ArkLib/Interaction/Oracle/Execution.lean
• abbrev Codeword (_s : Fin (k + 1) → ℕ+) (_n : ℕ) (i : ℕ) : Type in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def verifierOutput in ArkLib/Interaction/Oracle/Core.lean
• abbrev fullRoles (n : Nat) : RoleDecoration (fullSpec R deg n) in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• def toVerifier {m : Type u → Type u} [Monad m] in ArkLib/Interaction/Reduction.lean
• abbrev Verifier (m : Type u → Type u) in ArkLib/Interaction/Reduction.lean
• def CDegreeLE (R : Type) [BEq R] [Semiring R] [LawfulBEq R] (d : ℕ) in ArkLib/Data/CompPoly/Basic.lean
• abbrev roundPoly (tr : Spec.Transcript (roundSpec R deg)) : in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• def honestRoundPoly {m_dom : ℕ} (D : Fin m_dom → R) in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• theorem partialEvalFirst_individualDegreeLE {deg : ℕ} (a : R) in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• theorem liftM_cast_query_add_right in ArkLib/Interaction/Oracle/Core.lean
• def routeInputQueriesInnerEval in ArkLib/Interaction/Boundary/Oracle.lean
• def Reduction.comp {m : Type u → Type u} [Monad m] in ArkLib/Interaction/Reduction.lean
• abbrev ReplayOracle (spec : Spec.{u}) (roles : RoleDecoration spec) : Type u in ArkLib/Interaction/FiatShamir/Basic.lean
• def remainingShift (i : ℕ) : ℕ in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• theorem run_pullback in ArkLib/Interaction/Boundary/Security.lean
• abbrev InputOracleFamily in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def prefixShift (i : ℕ) : ℕ in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• theorem simulateQ_cast_query in ArkLib/Interaction/Oracle/Core.lean
• abbrev InputLanguage in ArkLib/Interaction/OracleSecurity.lean
• theorem rbrKnowledgeSoundness_implies_rbrSoundness in ArkLib/Interaction/Security.lean
• theorem routeInputQueries_eval in ArkLib/Interaction/Boundary/Oracle.lean
• def HonestPubliclyEquivalent in ArkLib/Interaction/Oracle/Execution.lean
• theorem splitNth_toPoly (n : ℕ) [NeZero n] (p : CPolynomial R) (i : Fin n) : in ArkLib/Data/CompPoly/Fold.lean
• def outputAtEnd in ArkLib/Interaction/Oracle/Continuation.lean
• def Strategy.runWithReplayOracle {m : Type u → Type u} [Monad m] : in ArkLib/Interaction/FiatShamir/Transform.lean
• theorem OracleReduction.HonestExecutionEquivalent.toPublic in ArkLib/Interaction/Oracle/Execution.lean
• abbrev FoldChallengePrefix (i : ℕ) : Type in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def OracleSenderIndependent : in ArkLib/Interaction/BCS/HybridDecoration.lean
• abbrev challenge {X : Type u} {rest : X → Spec} {rRest : ∀ x, RoleDecoration (rest x)} in ArkLib/Interaction/FiatShamir/Basic.lean
• def CommitmentDecoration {ι : Type} (oSpec : OracleSpec.{0, 0} ι) : in ArkLib/Interaction/BCS/HybridDecoration.lean
• def evalPoint (i : ℕ) (idx : EvalIdx (n in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• abbrev roundTranscript (n : Nat) in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• def answerQuery : in ArkLib/Interaction/BCS/HybridDecoration.lean
• abbrev wit {StatementOut : Type u} {WitnessOut : Type v} in ArkLib/Interaction/Reduction.lean
• instance instOracleInterfaceCDegreeLE [Semiring R] : in ArkLib/Data/CompPoly/Basic.lean
• def outputLanguageOfReifiedLanguage in ArkLib/Interaction/OracleReification.lean
• instance instOracleInterfaceCMvDegreeLE : in ArkLib/Data/CompPoly/Basic.lean
• abbrev deserialize in ArkLib/Interaction/FiatShamir/DuplexSponge.lean
• def reifiedSoundness in ArkLib/Interaction/OracleReification.lean
• def MessagesOnly : in ArkLib/Interaction/FiatShamir/Basic.lean
• def PublicCoinReduction.fiatShamir in ArkLib/Interaction/FiatShamir/Transform.lean
• def honestRoundPolyAtPrefix {m_dom : ℕ} (D : Fin m_dom → R) in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• def honestFinalPolynomial in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def partialEvalLast (a : R) (p : CMvPolynomial (n + 1) R) : CMvPolynomial n R in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• def queryRoundOD : in ArkLib/ProofSystem/Fri/Interaction/QueryRound.lean
• def roundProverStep (m : Type → Type) [Monad m] in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• def toSpec : {n : Nat} → Chain n → Spec in ArkLib/Interaction/Oracle/Continuation.lean
• theorem reifiedKnowledgeSoundness_implies_reifiedSoundness in ArkLib/Interaction/OracleReification.lean
• theorem roundPoly_natDegree_le {deg : ℕ} (D : Fin m → R) {k : ℕ} in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• def freezeSharedToPUnit in ArkLib/Interaction/Oracle/Continuation.lean
• def roundOracleDecoration : in ArkLib/ProofSystem/Sumcheck/Interaction/Oracle.lean
• theorem roundOracleReduction_honestPubliclyEquivalentStateful in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• def PublicCoinReduction.duplexSpongeFiatShamir in ArkLib/Interaction/FiatShamir/DuplexSponge.lean
• theorem liftAppendOracleFamily_append_eq in ArkLib/Interaction/Oracle/Execution.lean
• def knowledgeSoundness in ArkLib/Interaction/OracleSecurity.lean
• abbrev OutputRelation in ArkLib/Interaction/OracleSecurity.lean
• theorem evalSize_factor in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• theorem simulate_comp {ι : Type} {oSpec : OracleSpec ι} in ArkLib/Interaction/Oracle/Continuation.lean
• def IsSound {m : Type u → Type u} [Monad m] [HasEvalSPMF m] in ArkLib/Interaction/Security.lean
• theorem simulateQ_ext in ArkLib/Interaction/Boundary/Oracle.lean
• theorem soundness_comp in ArkLib/Interaction/Security.lean
• theorem roundContinuationOption_proverEq_stateful in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• def soundness in ArkLib/Interaction/Security.lean
• def ofOracleDecoration : in ArkLib/Interaction/BCS/HybridDecoration.lean
• theorem IsKnowledgeSound.bound_terminalProb in ArkLib/Interaction/Security.lean
• def plain : in ArkLib/Interaction/BCS/HybridDecoration.lean
• abbrev FoldCodewordPrefix in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def QueryHandle : in ArkLib/Interaction/BCS/HybridDecoration.lean
• def OracleDecoration.answerQuery : in ArkLib/Interaction/Oracle/Core.lean
• theorem roundOracleReduction_executePublic_eq_stateful in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• def queryBatchConsistentQ in ArkLib/ProofSystem/Fri/Interaction/QueryRound.lean
• theorem sumcheckReduction_soundness in ArkLib/ProofSystem/Sumcheck/Interaction/General.lean
• abbrev ReifiedInputRelation in ArkLib/Interaction/OracleReification.lean
• instance instOracleInterfaceCPolynomial [Nontrivial R] : in ArkLib/Data/CompPoly/Basic.lean
• def answerSplitLiftAppendQueryAppend in ArkLib/Interaction/Oracle/Execution.lean
• instance instOracleInterfaceCMvPolynomial : in ArkLib/Data/CompPoly/Basic.lean
• def output in ArkLib/Interaction/OracleReification.lean
• instance instOracleInterfaceEmptyOracleFamily : in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def foldRoundContinuation {SharedIn : Type} {ι : Type} {oSpec : OracleSpec ι} in ArkLib/ProofSystem/Fri/Interaction/FoldRound.lean
• def run in ArkLib/Interaction/Oracle/Execution.lean
• abbrev afterChallenge {X : Type u} {rest : X → Spec} {rRest : ∀ x, RoleDecoration (rest x)} in ArkLib/Interaction/FiatShamir/Basic.lean
• theorem probAccept_pullback_le in ArkLib/Interaction/Boundary/Security.lean
• abbrev IsSound in ArkLib/Interaction/Boundary/Compatibility.lean
• abbrev QueryBatch : Type in ArkLib/ProofSystem/Fri/Interaction/QueryRound.lean
• def splitLiftAppendOracleQuery in ArkLib/Interaction/Oracle/Execution.lean
• theorem roundPoly_eval (D : Fin m → R) (k : ℕ) (p : CMvPolynomial (k + 1) R) (x : R) : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• def foldRoundSpec in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def answerSplitLiftAppendQuery in ArkLib/Interaction/Oracle/Execution.lean
• abbrev HonestPoly (i : ℕ) in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• theorem partialEvalPrefix_individualDegreeLE {deg : ℕ} : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• def buildSpongeReplayOracle : in ArkLib/Interaction/FiatShamir/DuplexSponge.lean
• def rbrKnowledgeSoundness in ArkLib/Interaction/Security.lean
• def roundProverStepStateful (m : Type → Type) [Monad m] in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• def toOracleSpec : in ArkLib/Interaction/BCS/HybridDecoration.lean
• def foldRoundOD in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• abbrev stmt {StatementOut : Type u} {WitnessOut : Type v} in ArkLib/Interaction/Reduction.lean
• def outputFamily in ArkLib/Interaction/Oracle/Continuation.lean
• theorem prefixShift_le_sub_round in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def toClaimTree {spec : Spec} {roles : RoleDecoration spec} {Claim : Type u} in ArkLib/Interaction/Security.lean
• theorem prefixShift_succ (i : Fin (k + 1)) : in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def Decoration.ofChain {S : Type u → Type v} in ArkLib/Interaction/Reduction.lean
• theorem simulates_pullback in ArkLib/Interaction/Boundary/OracleSecurity.lean
• theorem runWithOracleCounterpart_mapOutputWithRoles in ArkLib/Interaction/Oracle/Execution.lean
• def toMonadDecoration {ι : Type} (oSpec : OracleSpec.{0, 0} ι) in ArkLib/Interaction/BCS/HybridReduction.lean
• def HonestExecutionEquivalent in ArkLib/Interaction/Oracle/Execution.lean
• abbrev verifierMD in ArkLib/Interaction/Oracle/Core.lean
• abbrev finalFoldPolynomial in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• theorem roundContinuation_publicEq_stateful in ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean
• theorem simulateQ_ext in ArkLib/Interaction/Oracle/Core.lean
• def toReduction {m : Type u → Type u} [Monad m] in ArkLib/Interaction/Reduction.lean
• def Realizes in ArkLib/Interaction/OracleSecurity.lean
• def knowledgeSoundness in ArkLib/Interaction/Security.lean
• theorem answerSplitLiftAppendQueryAppend_eq in ArkLib/Interaction/Oracle/Execution.lean
• def evalAtIdx (p : CPolynomial F) {i : ℕ} (idx : EvalIdx (n in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def roundCheck {m_dom : ℕ} (D : Fin m_dom → R) (target : RoundClaim R) in ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean
• abbrev HybridDecoration (spec : Spec) (roles : RoleDecoration spec) in ArkLib/Interaction/BCS/HybridDecoration.lean
• def execute in ArkLib/Interaction/Oracle/Continuation.lean
• def follow {spec : Spec} {roles : RoleDecoration spec} {Claim : Type u} in ArkLib/Interaction/Security.lean
• def reifiedCompleteness in ArkLib/Interaction/OracleReification.lean
• abbrev ReifiedOutputLanguage in ArkLib/Interaction/OracleReification.lean
• def totalShift : ℕ in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• abbrev foldPhaseRoles : in ArkLib/ProofSystem/Fri/Interaction/FoldPhase.lean
• def executePublicConcrete in ArkLib/Interaction/Oracle/Execution.lean
• theorem runWithOracleCounterpart_pullbackCounterpart in ArkLib/Interaction/Boundary/Oracle.lean
• abbrev OracleCounterpart {ι : Type} (oSpec : OracleSpec.{0, 0} ι) in ArkLib/Interaction/Oracle/Core.lean
• def roundAnchorIdx in ArkLib/ProofSystem/Fri/Interaction/Core.lean
• def liftAppendLeftContext : in ArkLib/Interaction/Oracle/Core.lean
• def Reduction.perfectCompleteness in ArkLib/Interaction/Security.lean
• theorem OracleReduction.mapExecuteWitness_eq_execute_mappedOutput in ArkLib/Interaction/Oracle/Execution.lean
• def inputRelationOfRelation in ArkLib/Interaction/OracleReification.lean
• abbrev InputWitness : Type in ArkLib/ProofSystem/Fri/Interaction/Protocol.lean
• def promoteStatementToShared in ArkLib/Interaction/Oracle/Continuation.lean
• def fsRoles (Context : StatementIn → Spec.{u}) in ArkLib/Interaction/FiatShamir/Transform.lean
• theorem OracleReduction.executePublic_eq_map_execute in ArkLib/Interaction/Oracle/Execution.lean
• def sumAllButFirst (D : Fin m → R) : (k : ℕ) → CMvPolynomial (k + 1) R → CMvPolynomial 1 R in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean
• theorem simulate_compFlat {ι : Type} {oSpec : OracleSpec ι} in ArkLib/Interaction/Oracle/Continuation.lean
• theorem simulateQ_liftId in ArkLib/Interaction/Boundary/Oracle.lean
• def Accepts in ArkLib/Interaction/OracleSecurity.lean
• def toMonadDecoration {ι : Type} (oSpec : OracleSpec.{0, 0} ι) in ArkLib/Interaction/Oracle/Core.lean

---

sorry Tracking

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

• theorem sumAllButFirst_eval (D : Fin m → R) : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean (L125)
• theorem partialEvalPrefix_individualDegreeLE {deg : ℕ} : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean (L144)
• theorem partialEvalPrefix_individualDegreeLE {deg : ℕ} : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean (L149)
• theorem partialEvalPrefix_individualDegreeLE {deg : ℕ} : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean (L170)
• theorem partialEvalPrefix_individualDegreeLE {deg : ℕ} : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean (L171)
• theorem partialEvalPrefix_individualDegreeLE {deg : ℕ} : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean (L172)
• theorem partialEvalPrefix_individualDegreeLE {deg : ℕ} : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean (L173)
• theorem honestFinalPolynomial_natDegree_le in ArkLib/ProofSystem/Fri/Interaction/Core.lean (L322)
• theorem partialEvalLast_eval (a : R) (p : CMvPolynomial (n + 1) R) (v : Fin n → R) : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean (L109)
• theorem partialEvalFirst_eval (a : R) (p : CMvPolynomial (n + 1) R) (v : Fin n → R) : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean (L102)
• theorem roundPoly_natDegree_le {deg : ℕ} (D : Fin m → R) {k : ℕ} in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean (L221)
• theorem toUnivariate_natDegree_le {deg : ℕ} in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean (L213)
• theorem toUnivariate_eval (p : CMvPolynomial 1 R) (x : R) : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean (L194)
• theorem sumOverLast_eval (D : Fin m → R) (p : CMvPolynomial (n + 1) R) (v : Fin n → R) : in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean (L116)
• theorem foldNth_toPoly (n : ℕ) [NeZero n] (p : CPolynomial R) (α : R) : in ArkLib/Data/CompPoly/Fold.lean (L53)
• theorem splitNth_toPoly (n : ℕ) [NeZero n] (p : CPolynomial R) (i : Fin n) : in ArkLib/Data/CompPoly/Fold.lean (L49)
• theorem foldNth_natDegree_le_of_le in ArkLib/Data/CompPoly/Fold.lean (L59)
• theorem honestFoldPoly_natDegree_le {i : Fin k} in ArkLib/ProofSystem/Fri/Interaction/Core.lean (L306)
• theorem partialEvalFirst_individualDegreeLE {deg : ℕ} (a : R) in ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean (L136)

---

🎨 **Style Guide Adherence**

This code review is based on the provided ArkLib style guide.

Documentation and Citation Violations

• Docstring Syntax (Backticks): The guide requires using backticks for Lean names (e.g., `List.map`). There are over 40 instances where Lean names are used in docstrings as plain text.
  • ArkLib/Interaction/BCS/HybridDecoration.lean:18: "HybridDecoration — assigns an optional OracleInterface at each sender..." (Should be `HybridDecoration` and `OracleInterface`).
  • ArkLib/Interaction/BCS/HybridDecoration.lean:21: "Defined as Role.Refine..." (Should be `Role.Refine`).
  • ArkLib/Interaction/Boundary/Core.lean:25: "...FRIBinius witness reinterpretation, BatchedFRI batching boundary)."
• Docstring Quality: Docstrings must describe what a definition is or what a theorem states, and references to "TODO", design history, or reactive language are prohibited.
  • ArkLib/Interaction/BCS/HybridDecoration.lean:44: "...aligning with the OracleInterfaces TODO in ProtocolSpec/Basic.lean and the functional BCS literature (eprint 2025/902)."
• Citation Standards: All cited papers must use citation keys (e.g., [ACFY24]) and include a ## References section in the file header.
  • ArkLib/Interaction/BCS/HybridDecoration.lean:45: References "eprint 2025/902" directly and lacks a ## References section.
• Missing Docstrings: "Every definition and major theorem should have a docstring."
  • ArkLib/Data/CompPoly/Basic.lean:34: def CDegreeLE lacks a docstring.
  • ArkLib/Data/CompPoly/Basic.lean:39: def CMvDegreeLE lacks a docstring.
  • ArkLib/Data/CompPoly/Fold.lean:47: theorem splitNth_toPoly lacks a docstring.
  • ArkLib/Data/CompPoly/Fold.lean:51: theorem foldNth_toPoly lacks a docstring.
  • ArkLib/Data/CompPoly/Fold.lean:55: theorem foldNth_natDegree_le_of_le lacks a docstring.

Syntax and Formatting Violations

• Line Length: "Keep lines under 100 characters." There are over 30 violations of this rule.
  • ArkLib/Interaction/BCS/HybridDecoration.lean:159: Length 104.
  • ArkLib/Interaction/Boundary/Oracle.lean:108: Length 104.
  • ArkLib/Interaction/Boundary/Oracle.lean:405: Length 110.
• Indentation: "Use 2 spaces for indentation." There are over 100 violations where 3, 4, 5, or 6 spaces are used instead of consistent 2-space increments.
  • ArkLib/Data/CompPoly/Basic.lean:50: Query := Fin n → R (3 spaces).
  • ArkLib/Data/CompPoly/Basic.lean:52: spec := (Fin n → R) →ₒ R (5 spaces).
  • ArkLib/Interaction/Boundary/Oracle.lean:66: simp (6 spaces).
• Function Notation: "Prefer fun x ↦ ... over λ x, ...." While the diff avoids λ, it uses fun x => exclusively. The guide specifically requests the ↦ symbol for function terms. (Pervasive across all new files).
  • ArkLib/Data/CompPoly/Basic.lean:53: impl := fun points => do ... (Should use ↦).
  • ArkLib/Interaction/BCS/HybridDecoration.lean:61: abbrev HybridDecoration ... := Interaction.Role.Refine (fun X => ...)
• File Headers (Copyright Year): "Use standard file headers including copyright... (c) 2024".
  • ArkLib/Interaction/BCS/HybridDecoration.lean:2: Copyright (c) 2026 (Incorrect year).
  • ArkLib/Interaction/BCS/HybridReduction.lean:2: Copyright (c) 2026 (Incorrect year).

Naming Convention Violations

• Theorem Naming Logic: "Hypotheses: Use _of_ to separate hypotheses, listed in the order they appear."
  • ArkLib/Interaction/BCS/HybridDecoration.lean:163: plain_oracleSenderIndependent (Should be oracleSenderIndependent_plain or oracleSenderIndependent_of_plain to indicate that the property follows from being 'plain').

---

📄 **Per-File Summaries**

• AGENTS.md: This update refines the project's guardrails by introducing stylistic preferences for readable notation, term-style definitions, and the use of existing library combinators over bespoke helpers. It also clarifies global configuration settings for autoImplicit and establishes stricter quality and maintenance standards for docstrings and wiki documentation.
• ArkLib.lean: This update expands the ArkLib library by importing several new modules related to interactive proof systems, oracle interactions, and Fiat-Shamir transformations. Specifically, it integrates new components for composition polynomials and the interactive protocols for FRI and Sumcheck.
• ArkLib/Data/CompPoly/Basic.lean: This file introduces definitions for degree-bounded univariate and multivariate computable polynomials, including a predicate for individual variable degrees. It also provides several OracleInterface instances to enable evaluation queries on these polynomial types within the library's oracle framework.
• ArkLib/Data/CompPoly/Fold.lean: This new file introduces native computable splitNth and foldNth operations for CPolynomial to support FRI protocols without routing through Mathlib polynomials. It includes theorems relating these definitions to standard polynomial operations and degree bounds, though splitNth_toPoly, foldNth_toPoly, and foldNth_natDegree_le_of_le currently contain sorry placeholders.
• ArkLib/Interaction/Boundary/Compatibility.lean: This file introduces the Statement.IsSound and Context.IsComplete classes to formalize semantic soundness and completeness predicates across interaction boundaries. It also provides definitions to flatten oracle-aware boundaries into concrete plain boundaries, allowing the base predicates to be applied to oracle statements and contexts without any sorry or admit placeholders.
• ArkLib/Interaction/Boundary/Core.lean: This file introduces the core framework for "interaction boundaries," providing definitions like Statement, Witness, and Context to reinterpret protocol interfaces without altering their underlying transcript or round structure. It includes pullback functions that adapt verifiers, provers, and reductions to these new interfaces through input projection and output lifting. No sorry or admit placeholders are introduced.
• ArkLib/Interaction/Boundary/Oracle.lean: This file introduces an oracle access layer for interaction boundaries, providing a framework for verifier-side oracle simulation. It defines the OracleStatementAccess structure and the pullbackCounterpart combinator to translate queries between inner and outer oracle specifications. The implementation includes several new definitions and theorems verifying that rerouted simulations maintain behavioral equivalence with their original counterparts.
• ArkLib/Interaction/Boundary/OracleSecurity.lean: This file defines the infrastructure for transporting oracle-based security properties across interaction boundaries, focusing on verifier simulation and honest execution views. It introduces several new definitions and theorems, most notably simulates_pullback, which proves that boundary pullbacks preserve the correspondence between concrete oracle materialization and simulated oracle behavior for both verifiers and reductions. No sorry or admit placeholders are included.
• ArkLib/Interaction/Boundary/Reification.lean: This file introduces the reification layer for interaction-native oracle boundaries, defining OracleStatementReification for concrete data mapping and a Realizes predicate to ensure coherence between materialization and simulation views. It provides bundled structures for oracle statements and contexts along with several theorems relating simulation to materialization. These components are used to implement a pullback operation that lifts oracle reductions across context boundaries.
• ArkLib/Interaction/Boundary/Security.lean: This file establishes the operational and security properties of verifiers and reductions when "pulled back" across interaction boundaries. It introduces theorems for soundness and completeness transport—such as Verifier.probAccept_pullback_le and Reduction.completeness_pullback—to prove that security guarantees are preserved when lifting executions from inner to outer statement types. No sorry or admit placeholders are used in the proofs.
• ArkLib/Interaction/FiatShamir/Basic.lean: This file introduces the foundational definitions for the Fiat-Shamir transform, defining ReplayOracle as a deterministic counterpart and MessagesOnly as the data type for non-interactive proofs. It includes the deriveTranscript function to reconstruct interactive transcripts from messages-only proofs and contains no sorry placeholders.
• ArkLib/Interaction/FiatShamir/DuplexSponge.lean: This file introduces a concrete duplex sponge instantiation of the Fiat-Shamir transform, defining the SpongeAnnotation structure for node-specific serialization and the buildSpongeReplayOracle function to generate deterministic challenges. It provides high-level definitions, such as PublicCoinReduction.duplexSpongeFiatShamir, to convert interactive public-coin protocols into non-interactive ones without the use of sorry or admit placeholders.
• ArkLib/Interaction/FiatShamir/Transform.lean: This file implements the Fiat-Shamir transform for public-coin interactive protocols by replacing random verifiers with deterministic replay oracles. It introduces definitions for transforming interactive provers, verifiers, and reductions into their non-interactive counterparts, allowing for the generation and verification of "messages-only" proofs. No sorry or admit placeholders are included.
• ArkLib/Interaction/Oracle/Continuation.lean: This file introduces new definitions and theorems for the sequential and multi-round composition of oracle reductions in interactive protocols. It defines an inductive Chain type to represent intrinsic round structures and a comp operator for binary composition, supported by theorems that establish the equivalence of composed simulators. The implementation contains no sorry or admit placeholders.
• ArkLib/Interaction/Oracle/Core.lean: This file establishes the core framework for oracle-based interactions by bridging the generic Interaction.Spec layer with VCVio's oracle computation model. It introduces OracleDecoration for path-dependent oracle access and provides the foundational definitions and theorems for OracleProver, OracleVerifier, and OracleReduction. No sorry or admit placeholders are present in the implementation.
• ArkLib/Interaction/Oracle/Execution.lean: This file introduces the operational framework for executing oracle-based interactions, providing the infrastructure to compose reductions via transcript appending and manage accumulated oracle states. It defines the core runWithOracleCounterpart execution engine and high-level APIs for running concrete reductions and verifiers, supported by theorems for distributing monad decorations over specification compositions. Additionally, the file establishes formal notions of honest public and execution equivalence for relating different oracle reductions; no sorry or admit placeholders are used.
• ArkLib/Interaction/Oracle/StateChain.lean: This file introduces infrastructure for composing oracle interactions into state chains, providing a mechanism to thread prover/verifier state and accumulated oracle specifications across multiple protocol stages. It defines stateChainVerifier and OracleReduction.stateChainComp to construct complex multi-stage oracle reductions from simpler individual steps. No sorry or admit placeholders are present in the implementation.
• ArkLib/Interaction/OracleReification.lean: This file establishes a bridge between abstract oracle behaviors and concrete oracle statements, introducing the Reification structure and derived security definitions such as reifiedSoundness and reifiedCompleteness. It includes several new definitions and theorems, notably proving that reified knowledge soundness implies reified soundness and providing query-level simulation results for oracle composition. The proofs are complete and contain no sorry or admit placeholders.
• ArkLib/Interaction/OracleSecurity.lean: This file introduces a "behavior-first" framework for defining the security of oracle-based interaction protocols, shifting focus from concrete oracle implementations to transcript-indexed oracle behaviors. It provides formal definitions for relative completeness, soundness, and knowledge soundness for oracle reductions and verifiers, and includes a theorem proving that knowledge soundness implies standard soundness.
• ArkLib/Interaction/Reduction.lean: This file introduces a new framework for interactive protocols by defining Prover, Verifier, and Reduction types based on W-type interaction trees (Spec). It provides support for public-coin protocols, sequential composition of reductions, and execution over stateful or stateless chains, including a theorem characterizing the output of composed reductions. No sorry or admit placeholders are used.
• ArkLib/Interaction/Security.lean: This file introduces foundational definitions and composition theorems for the completeness, soundness, and knowledge soundness of interactive reductions. It features a round-by-round analysis framework based on "claim trees" to derive global security bounds from local round properties, with all proofs provided and no sorry placeholders.
• ArkLib/ProofSystem/Fri/Interaction/Core.lean: This new file establishes the core executable definitions and interaction specifications for an interaction-native implementation of the FRI protocol. It introduces structural definitions for domain indexing, protocol round specifications (using the Interaction framework), and honest prover logic, while including sorry placeholders for two theorems regarding polynomial degree bounds after folding.
• ArkLib/ProofSystem/Fri/Interaction/FinalFold.lean: This file introduces the finalFoldContinuation definition, which implements the terminal fold round of the FRI protocol within an interactive oracle reduction framework. It defines the prover and verifier logic for sampling a final challenge and computing the final degree-bounded polynomial and its associated statement.
• ArkLib/ProofSystem/Fri/Interaction/FoldPhase.lean: This file introduces the definitions and logic necessary to chain $k$ non-final FRI folding rounds into a single interaction continuation. It defines the protocol's state transitions, transcript reconstruction, and the core foldPhaseContinuation using a modular oracle-reduction framework, without the use of any sorry placeholders.
• ArkLib/ProofSystem/Fri/Interaction/FoldRound.lean: This file introduces the foldRoundContinuation definition to model a single non-final FRI folding round as a modular oracle reduction. It implements the logic for the honest prover's polynomial folding, the verifier's challenge sampling, and oracle simulation for the resulting folded codewords without any sorry placeholders.
• ArkLib/ProofSystem/Fri/Interaction/General.lean: This new file serves as an umbrella module for the interaction-native FRI (Fast Reed-Solomon Interactive Oracle Proof of Proximity) protocol development. It provides documentation for the protocol's architectural components, such as folding rounds and query phases, while currently acting as an organizational entry point with no new theorems or definitions.
• ArkLib/ProofSystem/Fri/Interaction/Protocol.lean: This file defines the full interaction-native FRI (Fast Reed-Solomon Interactive Oracle Proof of Proximity) protocol by composing the folding and query phases using OracleReduction.comp. It introduces new definitions for the terminal phase and the complete protocol reduction logic, and it contains no sorry placeholders.
• ArkLib/ProofSystem/Fri/Interaction/QueryRound.lean: This new file formalizes the FRI query phase by introducing definitions and logic for sampling query batches and performing consistency checks across FRI rounds. It provides both direct and oracle-based functions to verify that sampled base-domain indices remain consistent with folded codewords and the terminal polynomial. No sorry or admit placeholders are used in the implementation.
• ArkLib/ProofSystem/Sumcheck/Interaction/CompPoly.lean: This file introduces computable, cast-free operations for CMvPolynomial and CPolynomial tailored for the Sum-check protocol, including partial evaluation, domain summation, and a bridge to univariate polynomials. It establishes the ResidualPoly structure for tracking prover state, though most correctness and degree-preservation proofs are currently marked with sorry placeholders.
• ArkLib/ProofSystem/Sumcheck/Interaction/Defs.lean: This file introduces the core definitions for an interaction-native sum-check protocol, including interaction specifications (roundSpec, fullSpec), state transition logic (advance), and per-round verification functions (roundCheck). It defines the algebraic structure for representing polynomials and sum-claims across multi-round interactions using the VCVio framework. No sorry or admit placeholders are present.
• ArkLib/ProofSystem/Sumcheck/Interaction/General.lean: This new file implements the general $n$-round oracle-native sum-check protocol by recursively composing single-round interactions within the VCVio framework. It introduces definitions for both stateless and stateful prover strategies—sumcheckReduction and sumcheckReductionStateful—alongside placeholder completeness and soundness theorems. While the file contains no sorry or admit placeholders, the security proofs are currently trivial and intended for future implementation.
• ArkLib/ProofSystem/Sumcheck/Interaction/Oracle.lean: This file introduces new definitions for an oracle-native sum-check protocol, specifically providing roundOracleDecoration and oracleVerifierStep to handle single-round verifier logic and polynomial oracle queries. These components support a continuation-based refactor where the prover's univariate messages are treated as queryable oracles. No sorry or admit placeholders are included.
• ArkLib/ProofSystem/Sumcheck/Interaction/SingleRound.lean: This file formalizes a single round of the sum-check protocol as an oracle reduction, providing definitions for computing residual polynomials, univariate round polynomials, and honest prover steps. It introduces both stateless and stateful implementations of the round continuation and provides theorems proving their public and execution equivalence in honest settings. No sorry or admit placeholders are included in the code.
• CONTRIBUTING.md: This update expands the style guide to emphasize code readability through the use of standard Lean notation, existing library combinators, and term-style definitions over tactics. Additionally, it establishes stricter quality standards for docstrings, requiring they focus on mathematical descriptions while prohibiting historical commentary or references to renamed or removed definitions.
• INTERACTION_BOUNDARIES.md: This document provides the design specification for the ArkLib.Interaction.Boundary framework, which enables protocol interface adaptation (statement, witness, and oracle reinterpretation) while preserving the underlying transcript and round structure. It establishes a three-layer architecture—Core, Access, and Reification—to formalize how verifier simulations and prover materializations are "pulled back" across boundaries, explicitly decoupling these interface mappings from sequential protocol composition.
• INTERACTION_BRACHA_VERIFICATION.md: This document identifies Bracha Reliable Broadcast (RBC) as a primary benchmark for the Interaction library, noting its suitability for testing the framework’s concurrency, multiparty, and liveness features. It maps the landscape of existing protocol formalizations, such as Bythos and Veil, to position Interaction as an interaction-centric alternative that prioritizes Lean-native verification over external SMT solvers.
• INTERACTION_CONCURRENT_SPEC.md: This design reference outlines a concurrent extension for the ArkLib.Interaction library, proposing a minimal continuation-based kernel centered on binary structural parallelism. It establishes a frontier-residual operational semantics to support adversarial scheduling and provides a comprehensive roadmap for integrating diverse concurrency mental models, such as state machines and partial-order semantics.
• INTERACTION_PROTOCOL_ROADMAP.md: This new documentation file outlines a strategic roadmap for evolving the Interaction module into a generalized semantic framework for modeling and verifying concurrent protocols. It details a six-phase development plan covering core concurrency foundations, choreography frontends, knowledge-based security, and causal models. The proposed architecture prioritizes first-class support for partial observability, scheduler control, and causal equivalence across diverse protocol families.
• PORTING.md: This documentation tracks the architectural overhaul of the library's core interaction and oracle layers, detailing the transition from a flat protocol model to a universe-polymorphic system based on Interaction.Spec (W-type game trees). It provides a comprehensive roadmap of the rebuild, outlining completed phases for foundational interactions and oracle verifiers, current progress on security definitions, and planned migrations for downstream cryptographic protocols.
• blueprint/src/coding_theory/defs.tex: This update refines the mapping between blueprint definitions and the Lean formalization by providing more precise, namespaced paths for interleaved codes and proximity measures. It also improves the formatting of references for generator matrices.
• blueprint/src/content.tex: This change introduces the "Interaction Framework" chapter to the project blueprint, establishing the formal structure for foundational concepts like protocol composition, the Fiat-Shamir transformation, and security definitions. It serves to organize the theoretical groundwork necessary for modeling interactive proofs and oracle-based protocols.
• blueprint/src/interaction/boundary.tex: This file introduces the concept of protocol "Boundaries," providing a dependent-type-native framework for reinterpreting statement, witness, and oracle interfaces without altering transcript structures. It defines a layered architecture for query simulation and concrete data reification, establishing the necessary pullback operations and coherence predicates (such as Realizes) to transport soundness and completeness properties across protocol layers.
• blueprint/src/interaction/composition.tex: This file documents the formalization of sequential composition and iteration mechanisms for interaction specifications and strategies. It introduces the liftAppend combinator to manage dependent types without explicit casts and defines various iteration patterns, including state-indexed chains and continuation-based telescopes.
• blueprint/src/interaction/fiat_shamir.tex: This document specifies a Fiat-Shamir transform for dependent interaction trees, where the protocol's future shape can depend on earlier verifier challenges. It introduces a PublicCoinCounterpart structure to enable verifier-side transcript replay and defines a method for reconstructing full transcripts from sender-only message sequences using a deterministic replay oracle.
• blueprint/src/interaction/foundations.tex: This file introduces the foundational theory for modeling interactive protocols as dependently-typed trees (Spec), allowing for protocols where message spaces and round counts depend on previous moves. It defines core abstractions including Transcript, metadata Decoration, and monadic Strategy, prioritizing structural recursion over index-based arithmetic to simplify protocol composition and reasoning.
• blueprint/src/interaction/oracle.tex: This file adds a new section to the blueprint defining the formal framework for path-dependent oracle access in interactive oracle proofs. It introduces definitions for OracleDecoration and QueryHandle to model queryable transcript messages and provides a bridge to the generic Counterpart.withMonads framework to enable compositional OracleReduction and OracleVerifier structures.
• blueprint/src/interaction/security.tex: This file defines formal security properties—including completeness, soundness, and knowledge soundness—within the Spec + RoleDecoration interaction framework. It introduces claim trees for round-by-round soundness analysis and specifies oracle-level security definitions that rely on the existence of concrete data to satisfy the verifier's simulation.
• blueprint/src/interaction/two_party.tex: This file adds the formal specification for two-party and multi-party interactions by decorating existing interaction trees with sender and receiver roles. It defines the duality between choosing moves ($\Sigma$-types) and responding to them ($\Pi$-types) to formalize strategies, counterparts, and role-aware refinements for oracle-based verification.
• blueprint/src/macros/common.tex: This update introduces a set of LaTeX macros to support the formal documentation of a Spec-based interaction framework built on W-types. The new commands cover core concepts such as strategies, roles, decorations, and oracles.
• blueprint/src/oracle_reductions/defs.tex: This update reformats the Lean declaration tags in the blueprint to use individual \lean{} commands for each term instead of comma-separated lists. This change likely improves the granularity of the mapping between the formal LaTeX definitions and their corresponding Lean 4 implementations.
• blueprint/src/polynomials/defs.tex: This update removes the explicit Lean implementation tags UniPoly and MlPoly from the blueprint definitions for computable univariate and multilinear polynomials. This effectively decouples these high-level definitions from their specific Lean identifiers in the documentation.
• blueprint/src/proof_systems/binius.tex: The changes remove \lean command references that linked mathematical definitions and theorems for binary tower fields to specific Lean identifiers. This decouples the high-level documentation in the blueprint from the underlying formal implementation names.
• blueprint/src/proof_systems/simple_protocols.tex: The changes refine the mapping between the blueprint and the Lean implementation by splitting combined \lean tags into individual commands for the DoNothing reduction. Additionally, the reference to CheckClaim.oracleReduction_completeness was removed, likely to reflect changes in the underlying formalization.
• blueprint/src/proof_systems/stir.tex: This update refines the LaTeX blueprint by splitting grouped Lean declaration links into individual \lean commands. This change ensures each formal theorem and definition is explicitly and separately mapped to its corresponding mathematical lemma.
• blueprint/src/proof_systems/whir.tex: This documentation update refines the Lean tags in the blueprint by splitting multi-item \lean commands into separate entries. These changes improve the mapping between the LaTeX definitions and their corresponding Lean declarations for the WHIR proof system.
• blueprint/src/references.bib: This change expands the bibliography by adding several references related to dependent type theory (ornamental algebras and interactive programs) and modern cryptography. Key additions include works on SNARK protocols (Zinc, Jolt) and the formalization/standardization of the Fiat-Shamir transformation.
• blueprint/src/vcv/defs.tex: This PR updates the Lean 4 cross-reference tags in the blueprint to accurately match the namespaces and naming conventions used in the formal library. These refinements ensure that definitions such as OracleSpec, evalDist, and various simulation oracles are correctly linked to their corresponding Lean implementations.
• docs/wiki/README.md: This update expands the documentation index by adding references to new design specifications and roadmaps concerning interaction boundaries, concurrency, protocol families, and formal verification benchmarks.
• docs/wiki/repo-map.md: This update to the repository map documents the reorganization of the ArkLib/Interaction/Concurrent/ directory into specialized modules for structural concurrency, dynamic process semantics, and open-interface primitives. It clarifies the layout of recent additions, including open-boundary definitions and the OpenTheory composition interface.
• scripts/README.md: This update corrects the documentation for validate.sh to reflect that the script now enforces a zero-warning policy (excluding sorry placeholders) for the ArkLib/Interaction/ directory. This expands the existing linting requirements previously only noted for ArkLib/Data/.
• scripts/check-docs-integrity.py: The script now uses git ls-files to identify markdown files within the documentation and script directories. This change ensures that integrity checks are performed only on files tracked by Git, preventing the processing of untracked or local-only files.
• scripts/validate.sh: This update extends the validation script to enforce a zero-warning policy (excluding sorry placeholders) for the ArkLib/Interaction/ directory. This ensures that any new code in this section of the library must be free of warnings before passing the CI check.
• ArkLib/Interaction/BCS/HybridReduction.lean: This file introduces the HybridOracleReduction structure and the toMonadDecoration function to support protocols where only select sender nodes carry oracle interfaces. These definitions generalize standard oracle reductions to facilitate the BCS transformation, and the file contains no sorry or admit placeholders.
• ArkLib/Interaction/BCS/HybridDecoration.lean: This file introduces HybridDecoration, an infrastructure for the BCS transformation that allows prover messages to be either plain metadata or committed oracle messages. It defines several new structures and predicates for managing oracle queries and commitment metadata, including a theorem proving the well-formedness of the trivial plain decoration. No sorry or admit placeholders are used.

---

Last updated: 2026-04-11 13:46 UTC.

[github-actions]

Build Timing Report

• Commit: f4bd76d
• Message: Merge 5861161 into b5d5002
• Ref: quang/core-rebuild
• Comparison baseline: 20428b1 from the previous successful PR update.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; validation wrapper ./scripts/validate.sh.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	693.83	1025.92	+332.09	exit 1
Warm rebuild	2.00	-	-	-
Validation wrapper	2.05	-	-	-

Incremental Rebuild Signal

• Clean:warm comparison is unavailable because one of the build measurements is missing.

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
144.00	201.00	-57.00	ArkLib/ProofSystem/Component/RandomQuery.lean
70.00	66.00	+4.00	ArkLib/ProofSystem/Fri/Spec/SingleRound.lean
65.00	62.00	+3.00	ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean
59.00	48.00	+11.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean
58.00	59.00	-1.00	ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean
56.00	56.00	+0.00	ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
41.00	34.00	+7.00	ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean
38.00	21.00	+17.00	ArkLib/Data/CodingTheory/PolishchukSpielman/Existence.lean
36.00	37.00	-1.00	ArkLib/Data/CodingTheory/DivergenceOfSets.lean
36.00	33.00	+3.00	ArkLib/ProofSystem/Fri/Domain.lean
36.00	43.00	-7.00	ArkLib/OracleReduction/LiftContext/Reduction.lean
33.00	29.00	+4.00	ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
31.00	34.00	-3.00	ArkLib/OracleReduction/Security/RoundByRound.lean
29.00	30.00	-1.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/GoodCoeffs.lean
25.00	22.00	+3.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/JointAgreement.lean
23.00	15.00	+8.00	ArkLib/Data/Polynomial/SplitFold.lean
22.00	36.00	-14.00	ArkLib/ProofSystem/BatchedFri/Security.lean
20.00	18.00	+2.00	ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean
19.00	17.00	+2.00	ArkLib/Data/CodingTheory/Basic/Distance.lean
19.00	17.00	+2.00	ArkLib/Data/CodingTheory/PolishchukSpielman/Degrees.lean