feat(interaction): add oracle execution and continuation - #570
Draft
codygunton wants to merge 143 commits into
Draft
feat(interaction): add oracle execution and continuation#570codygunton wants to merge 143 commits into
codygunton wants to merge 143 commits into
Conversation
Advance the CompPoly dependency from v4.28.0 (d7b9f98, 58 commits behind) to the latest upstream master tip. The bump is fully backward-compatible with no ArkLib code changes needed. Made-with: Cursor
Replace ~30 duplicated bivariate polynomial declarations (coeff, degrees, weighted degrees, eval, shift, root multiplicity, discriminant) with imports from CompPoly's ToMathlib bridge files. Fix downstream consumers for monomial name disambiguation and the now-unconditional weightedDegree_eq_natWeightedDegree. Net: 597 lines deleted, 47 lines changed across 4 files, zero new sorries. Made-with: Cursor
Bump VCVio from d37e586 to ebea2fa (12 commits). Remove the unused Q_ne_0 field from GuruswamiSudan.Conditions since dvd_property does not require it. Made-with: Cursor
…sors
- Restore `Q_ne_0` field in `GuruswamiSudan.Conditions`: non-zeroness
is integral to the decoder specification (Q=0 trivially satisfies the
algebraic conditions). `dvd_property` still doesn't require it.
- Fix `Conditions` docstring to accurately describe the structure.
- Fix `ne_zero_iff_coeffs_ne_zero` docstring ("all its coefficients" →
"its coefficient function").
- Add `[NoZeroDivisors F]` to `totalDegree_mul` statement — the theorem
is false over semirings with zero divisors.
Made-with: Cursor
Resolve isolated dot, long line, and unnecessary simpa warnings. Made-with: Cursor
New standalone interaction infrastructure built on W-type specs with role decorations, eliminating the old TwoParty/Multiparty inductives and ProtocolSpec/Direction wrappers. - Basic.lean: universe-polymorphic Spec, Transcript, Strategy, Decoration with map, BundledMonad, MonadDecoration, append/comp combinators - TwoParty.lean: Role, RoleDecoration (= Decoration on Spec), Strategy.withRoles, Counterpart, runWithRoles, per-node monad variants - Multiparty.lean: PartyDecoration + toRoles via Decoration.map, three-party knowledge-soundness examples with rfl proofs - Reduction.lean: Prover, Verifier, Reduction, execute parameterized by (pSpec : Spec) (roles : RoleDecoration pSpec) - PORTING.md: tracks core rebuild progress and next steps - Delete old ArkLib/Refactor/ folder (superseded) Made-with: Cursor
- Verifier: add StmtOut, rename decide→verify, m Bool→OptionT m StmtOut - OracleCounterpart: round-by-round challenger with accSpec growing at sender nodes - InteractiveOracleVerifier: unified challenger+verify (= OracleCounterpart at internal nodes, verify fn at .done) - OracleVerifier: batch structure with iov + transcript-dependent simulate + reify - OracleProver, OracleReduction: oracle-aware prover/reduction structures - Decoration.Refine: displayed decoration combinator (cf. displayed algebras, ornaments) - SenderDecoration: Refine specialized to RoleDecoration with role-dependent fiber - Universe polymorphism throughout TwoParty.lean - N-ary composition: replicate, chain, iterate for Spec/Decoration/Strategy/Transcript Made-with: Cursor
…tions Replace SenderDecoration (Decoration.Refine + PUnit junk at receiver nodes) with Role.Refine — a direct recursion on spec + roles that skips receiver nodes cleanly. Prove equivalence with Decoration.Refine for compatibility. Made-with: Cursor
- Add ArkLib/Interaction/Basic/{Spec,Decoration,Strategy,Append,Replicate,Chain,MonadDecoration,BundledMonad}
- Add ArkLib/Interaction/TwoParty/{Role,Decoration,Strategy,Swap,Compose,Refine,Examples}
- Remove monolithic Basic.lean and TwoParty.lean; update Multiparty, Reduction, Oracle imports
- Note Interaction/Basic/ in PORTING.md; add Interaction line to docs/wiki/repo-map.md
Made-with: Cursor
- Define Spec.Decoration.swap so roles.swap elaborates on Decoration (fun _ => Role) - Abbrev RoleDecoration.swap to Spec.Decoration.swap; use roles.swap in Swap/Compose theorems Made-with: Cursor
Add "Authors: Quang Dao" to all Interaction files missing it. Rewrite Spec, Transcript, and ofList docstrings for clarity. Made-with: Cursor
Simplify Prover/Verifier/Reduction types: WitnessIn is plain, VerOutput deleted (verifier returns StatementOut), WitnessOut independent of StatementOut. Add Security.lean with completeness, soundness, knowledge soundness, ClaimTree, KnowledgeClaimTree, and round-by-round definitions. Update Oracle.lean, TwoParty Strategy/Compose, and Multiparty accordingly. Made-with: Cursor
autoImplicit = false is already set globally in lakefile.toml. Remove the duplicate set_option from all Interaction files and document this in AGENTS.md. Made-with: Cursor
…tors, overhaul docstrings Rename `Transcript.appendFamily` -> `liftAppend`, `Transcript.join` -> `append` (freeing `join` for n-ary flattening), and propagate across all files. Reorder Append.lean so `liftAppend` precedes `append`/`split` and `comp` precedes `compFlat`. Add new n-ary chain combinators in Chain.lean: `Transcript.chain` (telescope type), `Transcript.join`/`unjoin` (flatten/unflatten isomorphism with round-trip simp lemmas), `Transcript.liftJoin` (lift telescope-indexed families to chain transcripts). Rename `Spec.chainFamily` -> `Transcript.chainFamily`. Rewrite all docstrings in Append.lean, Chain.lean, and Compose.lean to be intrinsic and intuitive. Add docstring quality rule to CONTRIBUTING.md and AGENTS.md. Made-with: Cursor
…hain Move the continuation-style intrinsic chain (formerly `Spec.Unfolding` in `ChainIntrinsic.lean`) into `Basic/Chain.lean` as the canonical `Spec.Chain` API. Extract the old stage-indexed `Spec.chain` into a new `Basic/StateChain.lean` under the explicit `stateChain` prefix. Chain.lean now provides: - `Spec.Chain` (depth-indexed telescope: round spec + continuation) - `Chain.toSpec` (convert to concrete `Spec` via `Spec.append`) - `Chain.replicate`, `Chain.ofStateMachine` (derived constructors) - `Chain.splitTranscript` / `Chain.appendTranscript` (telescope ops) - `Chain.strategyComp` / `Chain.strategyCompUniform` (composition) StateChain.lean preserves the full legacy API under `stateChain*` names. Made-with: Cursor
…eChain Merge the intrinsic reduction layer (formerly `ReductionIntrinsic.lean`) into `Reduction.lean` as the default `Reduction.ofChain` surface. Rename all stage-threaded chain identifiers to `stateChain*` across TwoParty, Reduction, and Oracle modules. Reduction.lean gains: - `Decoration.ofChain` / `Chain.roles` (role decoration from Chain) - `Strategy.ofChain` / `Counterpart.ofChain` (recursive composition) - `Reduction.ofChain` (stateless chain-based reduction composition) Renames in TwoParty: - `RoleDecoration.chain` → `RoleDecoration.stateChain` - `Counterpart.chainComp*` → `Counterpart.stateChainComp*` - `Strategy.chainCompWithRoles*` → `Strategy.stateChainCompWithRoles*` Renames in Oracle: - `OracleReduction.chainComp` → `OracleReduction.stateChainComp` - `toMonadDecoration_chain` → `toMonadDecoration_stateChain` Made-with: Cursor
Express the sumcheck protocol using the Interaction.Spec framework: - CompPoly.lean: CDegreeLE / CMvDegreeLE types, computable partial evaluation, domain summation, roundPoly, OracleInterface instances - Defs.lean: shared algebraic core (RoundClaim, summation domain, round spec with role decoration) - SingleRound.lean: one-round spec, honest prover step, verifier step - General.lean: n-round stateChain composition, full spec/roles, reduction via stateChainCompUniform - Oracle.lean: oracle decoration, verifier step stub (sorry) Made-with: Cursor
Regenerate the umbrella import file to include new StateChain and Sumcheck/Interaction modules. Update PORTING.md architecture section and phase descriptions to reflect the Chain/StateChain naming, the merged intrinsic reduction layer, and initial Sumcheck progress. Made-with: Cursor
… and theorems Replace every `show ... from by simpa using` cast pattern with named recursive transport functions `Transcript.packAppend` / `unpackAppend`. Rewrite `Reduction.comp` to use non-flat `Strategy.compWithRoles` + `Counterpart.append`, add bridge lemma `Counterpart.append_eq_appendFlat_mapOutput`, and reprove `completeness_comp` / `soundness_comp` against the new structure. Update PORTING.md with Phase 4d progress. Made-with: Cursor
Return the next statement alongside the next witness so composed reductions can enforce prover/verifier statement agreement in completeness and reuse the same transport across the oracle and sumcheck interaction layers. Made-with: Cursor
AI-authored by Codex (GPT-5) on behalf of Quang Dao.
…pen expressions Made-with: Cursor
Made-with: Cursor # Conflicts: # ArkLib/ProofSystem/Fri/RoundConsistency.lean
Move 50 files (Basic/*, TwoParty/*, Concurrent/*, Multiparty/*) from ArkLib/Interaction/ to VCVio/Interaction/. These are pure interaction theory modules with no reduction/oracle-specific dependencies. Kept files (Reduction, Security, Oracle/*, Boundary/*, FiatShamir/*) now import from VCVio.Interaction instead of ArkLib.Interaction. VCVio dependency updated to quang/interaction-migration branch. Made-with: Cursor
Implement the duplex sponge instantiation of the Fiat-Shamir transform for the interaction-native formalization. The basic FS transform is parametric in the ReplayOracle; this constructs a specific ReplayOracle from a duplex sponge with a concrete permutation. New definitions: - SpongeAnnotation: per-node serialization metadata (serialize at sender nodes, squeeze length + deserialize at receiver nodes) - buildSpongeReplayOracle: thread a CanonicalDuplexSponge through the Spec tree to produce a ReplayOracle - spongeReplayOracle / toFSStatement: statement initialization wrappers - Prover/PublicCoinVerifier/PublicCoinReduction.duplexSpongeFiatShamir: the full transform, composing with the existing basic FS machinery Made-with: Cursor
Made-with: Cursor
Commitment scheme cutover to new Interaction.Opening interface, streamline oracle decoration and security theorem infrastructure, and update boundary modules for compatibility. Made-with: Cursor
Introduce HybridSpec (branching + pass-through nodes), partial BCS via CommitDeco, HybridDecoration for mixed plain/oracle senders, PublicQueryVerifier decomposition, and Phase 1/2 infrastructure. Delete the old OracleReduction/BCS/Basic.lean skeleton. Made-with: Cursor
Add blueprint formulation for BCS transformation on hybrid oracle reductions, CDHZ reference, and update wiki with new BCS modules. Made-with: Cursor
Introduce Oracle.Spec, a new inductive type (.done, .public, .oracle) that structurally distinguishes public and oracle messages, giving definitional independence of downstream types from oracle message values. New files: - Spec.lean: core inductive, RoleDeco, OracleDeco, PublicTranscript, QueryHandle, toOracleSpec, restrictLeft/restrictRight - Composition.lean: Reduction.id, comp, freezeSharedToPUnit, pullbackShared - Bridge.lean: conversion from old Interaction.Spec + OracleDecoration - BCS.lean: BCS transform directly on Oracle.Spec (CommitDeco, SharedTranscript, bcsSpec, wrapWithCommitments, PublicQueryVerifier) Modified files: - Core.lean: Oracle.Prover, Oracle.Verifier, Oracle.Reduction structures - Execution.lean: Spec.runWithOracleCounterpart, Reduction.executeConcrete - ArkLib.lean: imports for new modules Made-with: Cursor
- Remove accSpec parameter from Oracle.Verifier.toFun, hardcode to []ₒ - Add liftCounterpartAcc helper to lift counterpart accumulated oracle specs in composition (no sorry) - Rewrite completeness with OutputRealizes conjunct - Rewrite knowledgeSoundness: adversarial prover outputs oStmtOut, extractor sees concrete oracle data - Add oStmtOut parameter to Extractor.Straightline - Remove duplicate Verifier.InputRelation/OutputRelation/Accepts - Inline Accepts into soundness definition - Update blueprint security section to match new definitions Made-with: Cursor
…s hypothesis - Add answerCommittedQueries: compute committed oracle responses from a full transcript (deterministic, pure) - Add bcsPhase2: evaluate PublicQueryVerifier.decide with pre-computed query data - Strengthen hLangOut in knowledgeSoundness_implies_soundness to include OutputRealizes conjunct (required for the proof to go through) - Add detailed proof strategy comment for KS→soundness Made-with: Cursor
- Add OpeningDeco structure to Oracle/BCS.lean: generic opening proof data for committed oracle nodes, parameterized by OpeningProof type - Update PORTING.md with comprehensive Oracle.Spec layer status: file inventory, design decisions, updated TODO list - Update KS→soundness open question to reflect new formulation Made-with: Cursor
- Add N-ary chain composition (Oracle/Chain.lean) with Spec.Chain, Chain.Prover.comp, Chain.Verifier.comp, and Reduction.ofChain - Prove Spec.runWithOracleCounterpart_mapOutputWithRoles in Execution.lean - Prove knowledgeSoundness_implies_soundness in Security.lean (no sorry) - Rename for maximal namespacing: Prover.compAux, Verifier.compAux, Verifier.retargetMonads, Counterpart.liftAcc Made-with: Cursor
The acceptOStmt/acceptWitness approach is circular: it asks the caller to supply concrete oracle realizations, which is the "knowledge" that KS should extract. Revert to sorry with honest existential statement and document the difficulty. Delete the legacy version in OracleSecurity.lean which had the same flaw. Made-with: Cursor
Introduce Counterpart.mapOracles as the structural combinator for oracle-counterpart monad rewriting with a per-receiver reroute. Refactor liftAcc and Verifier.retargetMonads as thin wrappers; adjust Security proofs and statements to match. Made-with: Cursor
Made-with: Cursor
Restore local proofs and explicit query routing after the main merge, while keeping the remaining documented proof gaps isolated. Made-with: Cursor
Made-with: Cursor
Removes every file introduced by the core-rebuild branch outside this slice, so the branch's diff against main is exactly this cumulative slice while preserving the full core-rebuild commit history.
Contributor
🤖 PR SummaryMathematical Formalization - Degree-bounded subtypes for univariate and multivariate polynomials. -
|
| Metric | Count |
|---|---|
| 📝 Files Changed | 12 |
| ✅ Lines Added | 7841 |
| ❌ Lines Removed | 1 |
Lean Declarations
✏️ **Added:** 219 declaration(s)
def Strategy.ofChain {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leantheorem simulate_comp {ι : Type} {oSpec : OracleSpec ι}inArkLib/Interaction/Oracle/Continuation.leandef QueryHandle.routeLeft :inArkLib/Interaction/Oracle/Spec.leantheorem runWithOracleCounterpart_mapOutputWithRolesinArkLib/Interaction/Oracle/Execution.leanabbrev Counterpart (m : Type u → Type u)inArkLib/Interaction/Reduction.leantheorem PublicTranscript.split_append :inArkLib/Interaction/Oracle/Spec.leandef liftAppendLeftQuery :inArkLib/Interaction/Oracle/Core.leandef splitLiftAppendOracleQueryinArkLib/Interaction/Oracle/Execution.leanabbrev wit {StatementOut : Type u} {WitnessOut : Type v}inArkLib/Interaction/Reduction.leantheorem packAppend_unpackAppend (s₁ : Spec) (s₂ : Transcript s₁ → Spec)inArkLib/Interaction/Reduction.leantheorem splitPublicTranscript_appendPublicTranscript (n : Nat) (c : Chain (n + 1))inArkLib/Interaction/Oracle/Chain.leanprivate theorem simulateQ_liftAppendRightContext_withImpl_eqinArkLib/Interaction/Oracle/Continuation.leandef toMonadDecoration {ι : Type} (oSpec : OracleSpec.{0, 0} ι)inArkLib/Interaction/Oracle/Spec.leandef retargetMonadsinArkLib/Interaction/Oracle/Composition.leandef OracleDecoration.QueryHandle :inArkLib/Interaction/Oracle/Core.leanprivate def stateChainCompConcrete {ι : Type} {oSpec : OracleSpec ι}inArkLib/Interaction/Oracle/StateChain.leanabbrev unliftAppend (s₁ : Spec) (s₂ : Transcript s₁ → Spec)inArkLib/Interaction/Reduction.leantheorem Reduction.execute_compinArkLib/Interaction/Reduction.leaninstance instOracleInterfaceCMvDegreeLE :inArkLib/Data/CompPoly/Basic.leanabbrev liftAppendOracleFamilyinArkLib/Interaction/Oracle/Execution.leanabbrev Proof (m : Type u → Type u)inArkLib/Interaction/Reduction.leantheorem mapOutput_doneinArkLib/Interaction/Reduction.leantheorem splitLiftAppendOracleRange_eqinArkLib/Interaction/Oracle/Execution.leandef Reduction.comp {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leandef outputFamilyinArkLib/Interaction/Oracle/Continuation.leanabbrev unpackAppend (s₁ : Spec) (s₂ : Transcript s₁ → Spec)inArkLib/Interaction/Reduction.leandef toOracleDeco : (n : Nat) → (c : Chain n) → OracleDeco (toSpec n c)inArkLib/Interaction/Oracle/Chain.leanprivate def stateChainVerifierinArkLib/Interaction/Oracle/StateChain.leantheorem split_append (s₁ : Spec) (s₂ : Transcript s₁ → Spec)inArkLib/Interaction/Reduction.leanabbrev PublicCoinCounterpart (m : Type u → Type u)inArkLib/Interaction/Reduction.leantheorem runWithOracleCounterpart_mapCounterpartOutputinArkLib/Interaction/Oracle/Execution.leanabbrev stateChainFamilyinArkLib/Interaction/Reduction.leandef promoteStatementToSharedinArkLib/Interaction/Oracle/Continuation.leanprivate def compFlat {ι : Type} {oSpec : OracleSpec ι}inArkLib/Interaction/Oracle/Continuation.leandef Reduction.execute {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leanabbrev OracleProver {ι : Type} (oSpec : OracleSpec.{0, 0} ι)inArkLib/Interaction/Oracle/Core.leandef Decoration.ofChain {S : Type u → Type v}inArkLib/Interaction/Reduction.leanabbrev stmt {StatementOut : Type u} {WitnessOut : Type v}inArkLib/Interaction/Reduction.leantheorem answerSplitLiftAppendQueryAppend_eqinArkLib/Interaction/Oracle/Execution.leandef answerSplitLiftAppendQueryinArkLib/Interaction/Oracle/Execution.leantheorem unpackAppend_packAppend (s₁ : Spec) (s₂ : Transcript s₁ → Spec)inArkLib/Interaction/Reduction.leandef compWithRoles {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leanabbrev stateChainComp {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leandef Reduction.freezeSharedToPUnitinArkLib/Interaction/Oracle/Composition.leandef forgetExecuteWitnessinArkLib/Interaction/Oracle/Execution.leantheorem toSpec_succ {n : Nat} (spec : Oracle.Spec)inArkLib/Interaction/Oracle/Chain.leandef comp {ι : Type} {oSpec : OracleSpec ι}inArkLib/Interaction/Oracle/Continuation.leandef liftAppendRightQuery :inArkLib/Interaction/Oracle/Core.leandef Spec.runWithOracleCounterpartinArkLib/Interaction/Oracle/Execution.leandef appendPublicTranscript (n : Nat) (c : Chain (n + 1))inArkLib/Interaction/Oracle/Chain.leantheorem PublicTranscript.liftAppend_split :inArkLib/Interaction/Oracle/Spec.leandef QueryHandle.routeRight :inArkLib/Interaction/Oracle/Spec.leandef appendRight :inArkLib/Interaction/Oracle/Core.leantheorem simulateQ_extinArkLib/Interaction/Oracle/Core.leantheorem PublicTranscript.append_split :inArkLib/Interaction/Oracle/Spec.leandef toSpec : (n : Nat) → Chain n → Oracle.SpecinArkLib/Interaction/Oracle/Chain.leantheorem Spec.runWithOracleCounterpart_mapOutputWithRolesinArkLib/Interaction/Oracle/Execution.leandef freezeSharedToPUnitinArkLib/Interaction/Oracle/Continuation.leandef PublicTranscript.append :inArkLib/Interaction/Oracle/Spec.leanabbrev LawfulCommMonad (m : Type u → Type u) [Monad m]inArkLib/Interaction/Reduction.leandef idinArkLib/Interaction/Oracle/Continuation.leantheorem simulateQ_cast_depinArkLib/Interaction/Oracle/Core.leantheorem OracleReduction.mapExecuteWitness_eq_execute_mappedOutputinArkLib/Interaction/Oracle/Execution.leandef Chain : Nat → Type 1inArkLib/Interaction/Oracle/Chain.leanprivate def chainStrategyinArkLib/Interaction/Oracle/Continuation.leandef OracleDecoration.answerQuery :inArkLib/Interaction/Oracle/Core.lean@[simp] theorem toSpec_zero (c : Chain 0) : toSpec 0 c = .doneinArkLib/Interaction/Oracle/Chain.leantheorem toInteractionSpec_append :inArkLib/Interaction/Oracle/Spec.leandef restrictLeft {r : Type → Type} [Monad r] :inArkLib/Interaction/Oracle/Spec.leanprivate def liftSimulatedMidOracleContextContinuationinArkLib/Interaction/Oracle/Continuation.leandef restrictRight {r : Type → Type} [Monad r] :inArkLib/Interaction/Oracle/Spec.leantheorem append_split (s₁ : Spec) (s₂ : Transcript s₁ → Spec)inArkLib/Interaction/Reduction.leandef mapOutputWithRoles {m : Type u → Type u} [Functor m] :inArkLib/Interaction/Reduction.leantheorem appendLeft_range :inArkLib/Interaction/Oracle/Core.leandef Reduction.pullbackSharedinArkLib/Interaction/Oracle/Composition.leanprivate def compSimulateinArkLib/Interaction/Oracle/Continuation.leanabbrev mapReceiver {m : Type u → Type u} [Functor m]inArkLib/Interaction/Reduction.leanabbrev withRoles (m : Type u → Type u)inArkLib/Interaction/Reduction.leandef QueryHandle.splitAppend :inArkLib/Interaction/Oracle/Spec.leandef liftOutputinArkLib/Interaction/Oracle/Core.leandef Reduction.stateChainComp {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leandef verifierQueryCMvPolynomial (points : Fin n → R) :inArkLib/Data/CompPoly/Basic.leanabbrev PublicCoinVerifier (m : Type u → Type u)inArkLib/Interaction/Reduction.leaninstance instOracleInterfaceCDegreeLE [Semiring R] :inArkLib/Data/CompPoly/Basic.leandef QueryHandle.appendLeft :inArkLib/Interaction/Oracle/Spec.leandef QueryHandle :inArkLib/Interaction/Oracle/Spec.leandef toVerifier {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leandef OracleDeco.append :inArkLib/Interaction/Oracle/Spec.leandef outputFamilyinArkLib/Interaction/Oracle/Chain.leanabbrev liftAppend (s₁ : Spec) (s₂ : Transcript s₁ → Spec)inArkLib/Interaction/Reduction.leandef Counterpart.ofChain {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leandef runinArkLib/Interaction/Oracle/Continuation.leandef QueryHandle.appendRight :inArkLib/Interaction/Oracle/Spec.leantheorem liftM_cast_query_add_rightinArkLib/Interaction/Oracle/Core.leanabbrev packAppend (s₁ : Spec) (s₂ : Transcript s₁ → Spec)inArkLib/Interaction/Reduction.leanprivate def chainVerifierinArkLib/Interaction/Oracle/Continuation.leandef OracleCounterpart.mapOutput {ι : Type} {oSpec : OracleSpec.{0, 0} ι}inArkLib/Interaction/Oracle/Core.leandef collapseAppendOracleCompinArkLib/Interaction/Oracle/Execution.leandef Reduction.executeConcreteinArkLib/Interaction/Oracle/Execution.leandef transcriptAppend :inArkLib/Interaction/Oracle/Spec.leannoncomputable def ofOracleDecorationinArkLib/Interaction/Oracle/Bridge.leantheorem mapOutputWithRoles_eq_focal_mapOutput {m : Type u → Type u} [Functor m] :inArkLib/Interaction/Reduction.leandef runinArkLib/Interaction/Oracle/Execution.leandef replay {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leandef appendFlat {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leandef compWithRolesFlat {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leanabbrev liftAppendOracleIdxinArkLib/Interaction/Oracle/Execution.leandef append :inArkLib/Interaction/Reduction.leandef compAuxinArkLib/Interaction/Oracle/Composition.leantheorem toOracleSpec_appendRight :inArkLib/Interaction/Oracle/Spec.leandef Reduction.ofChaininArkLib/Interaction/Oracle/Chain.leantheorem toOracleSpec_appendLeft :inArkLib/Interaction/Oracle/Spec.leanabbrev rolesinArkLib/Interaction/Reduction.leandef OracleDecoration.toOracleSpec :inArkLib/Interaction/Oracle/Core.leandef appendLeft :inArkLib/Interaction/Oracle/Core.leanprivate def liftSimulatedMidOracleContextinArkLib/Interaction/Oracle/Continuation.leanabbrev InteractiveOracleVerifier {ι : Type} (oSpec : OracleSpec.{0, 0} ι)inArkLib/Interaction/Oracle/Core.leandef answerQuery :inArkLib/Interaction/Oracle/Spec.leandef toReduction {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leandef toMonadDecoration {ι : Type} (oSpec : OracleSpec.{0, 0} ι)inArkLib/Interaction/Oracle/Core.leandef outputAtEndinArkLib/Interaction/Oracle/Continuation.leanabbrev OracleCounterpart {ι : Type} (oSpec : OracleSpec.{0, 0} ι)inArkLib/Interaction/Oracle/Core.leandef OracleDecoration.oracleContextImplinArkLib/Interaction/Oracle/Core.leandef liftAppendLeftContext :inArkLib/Interaction/Oracle/Core.leandef verifierOutputinArkLib/Interaction/Oracle/Core.leandef mapOutputinArkLib/Interaction/Reduction.leantheorem liftAppendOracleFamily_append_eqinArkLib/Interaction/Oracle/Execution.leandef executeinArkLib/Interaction/Oracle/Continuation.leantheorem toMonadDecoration_appendinArkLib/Interaction/Oracle/Execution.leanabbrev liftAppendProd (s₁ : Spec) (s₂ : Transcript s₁ → Spec)inArkLib/Interaction/Reduction.leaninstance instOracleInterfaceCPolynomial [Nontrivial R] :inArkLib/Data/CompPoly/Basic.leandef mapExecuteWitnessinArkLib/Interaction/Oracle/Execution.leandef runWithRoles {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leandef toOracleSpec :inArkLib/Interaction/Oracle/Spec.leantheorem simulateQ_cast_specinArkLib/Interaction/Oracle/Core.leandef toVerifierinArkLib/Interaction/Oracle/Core.leandef RoleDeco : Oracle.Spec → TypeinArkLib/Interaction/Oracle/Spec.leantheorem PublicTranscript.liftAppend_append :inArkLib/Interaction/Oracle/Spec.leandef accImplAfter :inArkLib/Interaction/Oracle/Execution.leantheorem projectPublic_transcriptAppend :inArkLib/Interaction/Oracle/Spec.leandef PublicTranscript.liftAppend :inArkLib/Interaction/Oracle/Spec.leandef compinArkLib/Interaction/Oracle/Chain.leantheorem answerSplitLiftAppendQueryAppend_simOracle0inArkLib/Interaction/Oracle/Execution.leandef od : {n : Nat} → (c : Chain n) → OracleDecoration (toSpec c) (roles c)inArkLib/Interaction/Oracle/Continuation.leandef RoleDeco.append :inArkLib/Interaction/Oracle/Spec.leantheorem runWithRoles_mapOutputWithRoles_mapOutputinArkLib/Interaction/Reduction.leandef toRoles : (n : Nat) → (c : Chain n) → RoleDeco (toSpec n c)inArkLib/Interaction/Oracle/Chain.leandef liftAppendRightContext :inArkLib/Interaction/Oracle/Core.leandef toSpecRoles : (s : Oracle.Spec) → RoleDeco s → RoleDecoration s.toInteractionSpecinArkLib/Interaction/Oracle/Spec.leanabbrev stateChainCompWithRoles {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leantheorem simulateQ_liftAppendRightContext_eqinArkLib/Interaction/Oracle/Core.leandef mapOraclesinArkLib/Interaction/Oracle/Composition.leantheorem verifierQueryCMvPolynomial_run (poly : CMvPolynomial n R) (points : Fin n → R) :inArkLib/Data/CompPoly/Basic.leanprivate def retargetContinuationVerifierinArkLib/Interaction/Oracle/Continuation.leanprivate theorem simulateQ_liftSimulatedMidOracleContext_eqinArkLib/Interaction/Oracle/Continuation.leandef HonestPubliclyEquivalentinArkLib/Interaction/Oracle/Execution.leanabbrev split (s₁ : Spec) (s₂ : Transcript s₁ → Spec)inArkLib/Interaction/Reduction.leantheorem answerQuery_appendLeft :inArkLib/Interaction/Oracle/Core.leantheorem simulateQ_cast_query_idinArkLib/Interaction/Oracle/Core.leandef toCounterpart {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leandef splitPublicTranscript (n : Nat) (c : Chain (n + 1)) :inArkLib/Interaction/Oracle/Chain.leanprivate def liftPrefixOracleContextinArkLib/Interaction/Oracle/Continuation.leandef PublicTranscript.split :inArkLib/Interaction/Oracle/Spec.leantheorem answerQuery_appendRight :inArkLib/Interaction/Oracle/Core.leandef toInteractionSpec : Oracle.Spec → Interaction.SpecinArkLib/Interaction/Oracle/Spec.leanabbrev OracleDecoration (spec : Spec) (roles : RoleDecoration spec)inArkLib/Interaction/Oracle/Core.leantheorem rel_unliftAppend_append (s₁ : Spec) (s₂ : Transcript s₁ → Spec)inArkLib/Interaction/Reduction.leantheorem OracleReduction.executePublic_eq_map_executeinArkLib/Interaction/Oracle/Execution.leandef projectPublic :inArkLib/Interaction/Oracle/Spec.leandef liftAccinArkLib/Interaction/Oracle/Composition.leanabbrev VerifierOutputinArkLib/Interaction/Oracle/Core.leandef OracleDeco : Oracle.Spec → Type 1inArkLib/Interaction/Oracle/Spec.leannoncomputable def ofInteractionSpecinArkLib/Interaction/Oracle/Bridge.leandef append : (s₁ : Oracle.Spec) → (PublicTranscript s₁ → Oracle.Spec) → Oracle.SpecinArkLib/Interaction/Oracle/Spec.leandef answerSplitLiftAppendQueryAppendinArkLib/Interaction/Oracle/Execution.leanprivate theorem simulateQ_liftSimulatedMidOracleContextContinuation_eqinArkLib/Interaction/Oracle/Continuation.leantheorem simulateQ_castinArkLib/Interaction/Oracle/Core.leandef accSpecAfter :inArkLib/Interaction/Oracle/Execution.leandef Verifier.run {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leantheorem simulateQ_liftAppendRightContext_eq_of_implinArkLib/Interaction/Oracle/Core.leandef executeConcreteinArkLib/Interaction/Oracle/Execution.leanabbrev Verifier (m : Type u → Type u)inArkLib/Interaction/Reduction.leandef CDegreeLE (R : Type) [BEq R] [Semiring R] [LawfulBEq R] (d : ℕ)inArkLib/Data/CompPoly/Basic.leanabbrev verifierMDinArkLib/Interaction/Oracle/Core.leaninstance instOracleInterfaceCMvPolynomial :inArkLib/Data/CompPoly/Basic.leantheorem appendRight_range :inArkLib/Interaction/Oracle/Core.leandef runWithOracleCounterpartinArkLib/Interaction/Oracle/Execution.leandef runConcreteinArkLib/Interaction/Oracle/Execution.leantheorem simulate_compFlat {ι : Type} {oSpec : OracleSpec ι}inArkLib/Interaction/Oracle/Continuation.leandef Reduction.toVerifierinArkLib/Interaction/Oracle/Core.leantheorem mapOutput_id {m : Type u → Type u} [Functor m] [LawfulFunctor m]inArkLib/Interaction/Reduction.leandef Reduction.ofChain {m : Type u → Type u} [Monad m]inArkLib/Interaction/Reduction.leanabbrev OracleStatement {ιₛ : Type v} (OStmt : ιₛ → Type w)inArkLib/Interaction/Oracle/Core.leanabbrev Prover (m : Type u → Type u)inArkLib/Interaction/Reduction.leandef IndividualDegreeLE (deg : ℕ) (p : CMvPolynomial n R) : PropinArkLib/Data/CompPoly/Basic.leandef PublicTranscript : Oracle.Spec → TypeinArkLib/Interaction/Oracle/Spec.leantheorem runWithRoles_compWithRoles_appendinArkLib/Interaction/Reduction.leandef Reduction.idinArkLib/Interaction/Oracle/Composition.leandef toSpec : {n : Nat} → Chain n → SpecinArkLib/Interaction/Oracle/Continuation.leandef HonestExecutionEquivalentinArkLib/Interaction/Oracle/Execution.leantheorem simulateQ_liftAppendLeftContext_eqinArkLib/Interaction/Oracle/Core.leantheorem simulateQ_collapseAppendOracleCompinArkLib/Interaction/Oracle/Execution.leandef roles : {n : Nat} → (c : Chain n) → RoleDecoration (toSpec c)inArkLib/Interaction/Oracle/Continuation.leannoncomputable def ofRoleDecorationinArkLib/Interaction/Oracle/Bridge.leandef PublicTranscript.unliftAppend :inArkLib/Interaction/Oracle/Spec.leandef chainCompinArkLib/Interaction/Oracle/Continuation.leandef executePublicConcreteinArkLib/Interaction/Oracle/Execution.leandef Reduction.compinArkLib/Interaction/Oracle/Composition.leanabbrev Prover {ι : Type} (oSpec : OracleSpec.{0, 0} ι)inArkLib/Interaction/Oracle/Core.leantheorem simulateQ_mapinArkLib/Interaction/Oracle/Execution.leantheorem OracleReduction.HonestExecutionEquivalent.toPublicinArkLib/Interaction/Oracle/Execution.leandef OracleReduction.stateChainComp {ι : Type} {oSpec : OracleSpec ι}inArkLib/Interaction/Oracle/StateChain.leanabbrev HonestProverOutput (StatementOut : Type u) (WitnessOut : Type v)inArkLib/Interaction/Reduction.leandef PublicTranscript.packAppend :inArkLib/Interaction/Oracle/Spec.leandef CMvDegreeLEinArkLib/Data/CompPoly/Basic.leandef Verifier.runinArkLib/Interaction/Oracle/Execution.leantheorem simulateQ_cast_queryinArkLib/Interaction/Oracle/Core.leanabbrev withMonads (spec : Spec) (roles : RoleDecoration spec)inArkLib/Interaction/Reduction.leandef pullbackSharedinArkLib/Interaction/Oracle/Continuation.lean
sorry Tracking
- No
sorrys were added, removed, or affected.
📋 **Additional Analysis**
Style and Naming Guidelines
Naming Conventions
- Acronyms as Words: The definitions
IndividualDegreeLE,CDegreeLE, andCMvDegreeLEinArkLib/Data/CompPoly/Basic.leanviolate the naming convention to treat acronyms as words. They should be renamed toIndividualDegreeLe,CDegreeLe, andCMvDegreeLe(or follow snake_case if intended as theorem-like predicates). - Predicate Naming:
IndividualDegreeLEis adefreturningProp. According to the guidelines, predicates should generally use theIsprefix if they are adjectives (e.g.,IsIndividualDegreeLe). Furthermore, as a term/function, it should uselowerCamelCase(e.g.,individualDegreeLe) unless it is aclass. - Symbol Dictionary: The naming dictionary specifies
lefor the≤symbol. The current implementation uses the all-capsLEvariant in several type names.
Syntax and Formatting
- Function Binders: The guide states a preference for
fun x ↦ ...overλ x, .... The provided diff uses thefun x => ...syntax throughout (e.g., inArkLib/Interaction/Oracle/Bridge.leanandArkLib/Interaction/Oracle/Spec.lean). For consistency with Mathlib style,↦should be used. - Empty Lines: Guidelines prohibit empty lines inside definitions or proofs. Violations occur in:
ArkLib/Interaction/Oracle/Core.lean(e.g., insidetoMonadDecoration,liftOutput, andmapOutput).ArkLib/Interaction/Oracle/Spec.lean(e.g., insidetoOracleSpec).
- Line Length: Several lines exceed the 100-character limit, particularly in
ArkLib/Interaction/Oracle/Execution.leanwithin the definitions ofanswerSplitLiftAppendQueryAppendandsimulateQ_liftAppendRightContext_eq_of_impl.
Documentation Standards
- Missing Docstrings: Several definitions lack the required docstrings:
CDegreeLEandCMvDegreeLEinArkLib/Data/CompPoly/Basic.lean.simulateQ_map,liftAppendOracleIdx,liftAppendOracleFamily,splitLiftAppendOracleQuery, andanswerSplitLiftAppendQueryinArkLib/Interaction/Oracle/Execution.lean.PublicTranscript.unliftAppendandPublicTranscript.packAppendinArkLib/Interaction/Oracle/Spec.lean.
Variable Conventions
- Carrier Types: In
ArkLib/Data/CompPoly/Basic.lean,variable {R : Type}is used. The guidelines recommendvariable {R : Type*} [Semiring R]for algebraic carrier types to allow for universe polymorphism.
Framework Assessment
- Interaction Refactor: The PR successfully implements the transition of the oracle protocol model from a flat representation to one natively built on the W-type interaction tree (
Interaction.Oracle.Spec). - Unification: The code achieves the project goal of unifying
OracleCounterpartwith the genericCounterpart.withMonadsframework by usingtoMonadDecoration.
📄 **Per-File Summaries**
- ArkLib.lean: This update expands the ArkLib library's reach by adding imports for composite polynomials and a new framework for oracle-based interaction and reductions. No
sorryoradmitplaceholders were introduced. - ArkLib/Data/CompPoly/Basic.lean: This file introduces degree-bounded subtypes for computable univariate and multivariate polynomials, along with their corresponding
OracleInterfaceinstances for evaluation. It also defines a predicate for individual monomial degrees in multivariate polynomials and provides a correctness theorem for oracle-based polynomial queries. - ArkLib/Interaction/Oracle/Bridge.lean: This file introduces new definitions to structurally convert W-type-based interaction specifications and their decorations into the newer
Oracle.Specinductive format. It provides functions to map specifications, roles, and oracle interfaces, utilizing a default-element function to handle sender node continuations. - ArkLib/Interaction/Oracle/Chain.lean: This file introduces
Oracle.Spec.Chain, a depth-indexed telescope for defining n-round oracle protocols without explicit external state. It provides utilities to flatten these chains into singleOracle.Specdefinitions and includes composition mechanisms for building full prover strategies, verifier counterparts, andOracle.Reductioninstances from per-round steps. - ArkLib/Interaction/Oracle/Composition.lean: This file introduces infrastructure for composing
Oracle.Reductionobjects, including an identity reduction, shared-input reindexing utilities, and sequential binary composition. The implementation utilizes structural recursion onOracle.Specto ensure that interaction specifications and role decorations reduce definitionally, and the file contains nosorryoradmitplaceholders. - ArkLib/Interaction/Oracle/Continuation.lean: This file introduces infrastructure for sequentially composing and chaining oracle reductions within multi-party interactive protocols. It defines a
Chaininductive type for multi-round continuations and provides robust combinators for executing, simulating, and reindexing these composed structures. Nosorryoradmitplaceholders are introduced in the definitions or proofs. - ArkLib/Interaction/Oracle/Core.lean: This file establishes the core infrastructure for oracle-based interactions, bridging interaction specifications with VCVio's oracle computation model. It introduces key definitions such as
OracleDecoration,OracleVerifier, andOracleReductionto enable path-dependent oracle access and round-by-round challengers. The module also includes supporting theorems for query routing and transcript simulation without anysorryoradmitplaceholders. - ArkLib/Interaction/Oracle/Execution.lean: This file implements the concrete execution engine for oracle-decorated reductions and verifiers, providing infrastructure to run prover-verifier interactions while threading ambient, input, and accumulated oracle interfaces. It introduces core execution definitions such as
executeConcreteandrunWithOracleCounterpart, establishes notions of honest execution equivalence, and provides theorems for distributing monad decorations over appended specifications. The implementation consists of new definitions and theorems with complete proofs and nosorryplaceholders. - ArkLib/Interaction/Oracle/Spec.lean: This file introduces
Oracle.Spec, an inductive type for formalizing oracle reduction protocols by distinguishing between public messages and oracle-accessible messages. It provides comprehensive infrastructure for managing public transcripts, query handling, and verifier monad decorations, along with utilities for the sequential composition of these specifications. - ArkLib/Interaction/Oracle/StateChain.lean: This file introduces machinery for N-ary state chain composition of oracle reductions, defining
stateChainVerifierandOracleReduction.stateChainCompto manage prover and verifier state transitions across multi-stage interactive protocols. These definitions facilitate threading accumulated oracle specifications stage-by-stage and composing complex protocols from simpler steps without anysorryplaceholders. - ArkLib/Interaction/Reduction.lean: This file introduces a framework for interactive protocol participants—including provers, verifiers, and reductions—based on W-type interaction trees rather than flat lists. It provides definitions and theorems for executing and composing these protocols sequentially and through state-indexed chains.
Last updated: 2026-06-11 20:21 UTC.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
mainandmainhas merged into this, the PR should show only the execution/continuation layer over the core oracle protocol surface.Summary
Validation
./scripts/validate.shlake testreportserror: Arklib: no test driver configured