feat(sumcheck): add interaction protocol modules - #580
Draft
codygunton wants to merge 146 commits into
Draft
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.
#3) 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 FormalizationFormalizes degree-bounded univariate and multivariate computable polynomials ( Interaction Framework & Oracle SystemEstablishes an interaction-native framework for oracle-based protocols based on interaction trees:
Proof System ImplementationRefactors the Sumcheck protocol to utilize interaction-native reductions:
Warning: Placeholder TheoremsThe file Statistics
Lean Declarations ✏️ **Added:** 306 declaration(s)
📋 **Additional Analysis**Large Contributions
Naming Conventions
Syntax and Formatting
Documentation Standards
API Design and Normal Forms
📄 **Per-File Summaries**
Last updated: 2026-06-11 20:34 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.
Summary
Stack
Depends on #570.
Validation
./scripts/validate.shlake testreportserror: Arklib: no test driver configured