feat(interaction): add core oracle protocol surface - #532
Draft
codygunton wants to merge 147 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.
- 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
Structural Changes
Infrastructure
Proof Status
Statistics
Lean Declarations ✏️ **Added:** 148 declaration(s)
📋 **Additional Analysis**Style and Naming Violations
Documentation and Citations
📄 **Per-File Summaries**
Last updated: 2026-06-16 04:22 UTC. |
lalalune
referenced
this pull request
in lalalune/ArkLib
Jun 5, 2026
# Conflicts: # ArkLib.lean # ArkLib/CommitmentScheme/Basic.lean # ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean # ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean # ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean # ArkLib/Data/CodingTheory/ReedSolomon/FftDomain.lean # ArkLib/Data/MvPolynomial/LinearMvExtension.lean # ArkLib/Data/Polynomial/RationalFunctions.lean # ArkLib/OracleReduction/Execution.lean # ArkLib/ProofSystem/BatchedFri/Spec/General.lean # ArkLib/ProofSystem/Fri/Spec/SingleRound.lean # docs/wiki/README.md # docs/wiki/generated-files.md
lalalune
referenced
this pull request
in lalalune/ArkLib
Jun 5, 2026
… CompPoly) These 4 self-contained modules (0 sorries) were absent from main despite the PR #532 merge commit — the live rebase automation had reverted their content. Restores ArkLib/Interaction/Oracle/{Core,Spec}.lean, Interaction/Reduction.lean, Data/CompPoly/Basic.lean and registers them in the generated root. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This was referenced Jun 6, 2026
lalalune
referenced
this pull request
in lalalune/ArkLib
Jun 7, 2026
…oParty Reduces the Interaction/Reduction error count 55 -> 30. The remainder is an API-redesign gap, not name resolution: the file targets Spec.Strategy.withRoles / Spec.Counterpart / Spec.PublicCoinCounterpart which no longer exist in the pinned PolyFun - the API moved to the SyntaxOver/ShapeOver/StrategyOver.TwoParty forms (PolyFun 5d3a160). Migrating needs the PR #532 owner's design intent. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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
Extracts the core Interaction/oracle protocol surface from ArkLib PR #433 and rebases it onto current
mainas the first reviewable slice of a minimized Interaction stack.These files are taken directly from PR #433 without modification:
ArkLib/Interaction/Oracle/Core.leanArkLib/Interaction/Oracle/Spec.leanArkLib/Interaction/Reduction.leanIt also includes the CompPoly oracle-interface pieces in
ArkLib/Data/CompPoly/Basic.leanneeded by the later Sumcheck integration.This is the smallest useful first slice: the interaction-native reduction and oracle protocol surface plus the CompPoly oracle bridge, without execution/composition, Sumcheck, FRI, BCS, Fiat-Shamir, boundary, or security modules.
Dependency: CompPoly
ArkLib/Data/CompPoly/Basic.leanimportsCompPoly.Multivariate.DegreeBound, which does not yet exist inVerified-zkEVM/CompPoly. That module is added in:feat(multivariate): add degree-bounded sumcheck primitives.Until #241 lands,
lakefile.toml/lake-manifest.jsontemporarily pincodygunton/CompPoly @ 36c32f00(one commit ahead of upstream, carrying exactly that module). Once #241 merges, the pin will move back toVerified-zkEVM/CompPolyat the merged revision and the lakefile/manifest diff in this PR drops to zero.New Completion Work In This PR
None. The substantive Lean content is from PR #433; this PR rebases, isolates, and validates the core slice.
Commit history
The branch carries the full
core-rebuildhistory (Quang Dao's commits) followed by a single commit that pares the tree down to this slice, so authorship of the underlying work is preserved.Validation
./scripts/validate.shpassed on the branch (with the CompPoly pin above).🤖 Generated with Claude Code