feat(interaction): add oracle execution and continuation

ArkLib.lean

@@ -80,6 +80,7 @@ import ArkLib.Data.CodingTheory.ProximityGap.MCAGenerator
 import ArkLib.Data.CodingTheory.ProximityGap.ProximityGenerators
 import ArkLib.Data.CodingTheory.ReedSolomon
 import ArkLib.Data.CodingTheory.ReedSolomon.Multilinear
+import ArkLib.Data.CompPoly.Basic
 import ArkLib.Data.Domain.CosetFftDomain.Defs
 import ArkLib.Data.Domain.CosetFftDomain.Log
 import ArkLib.Data.Domain.CosetFftDomain.Mem
@@ -136,6 +137,15 @@ import ArkLib.Data.Polynomial.SplitFold
 import ArkLib.Data.Polynomial.Trivariate
 import ArkLib.Data.Probability.Instances
 import ArkLib.Data.Probability.Notation
+import ArkLib.Interaction.Oracle.Bridge
+import ArkLib.Interaction.Oracle.Chain
+import ArkLib.Interaction.Oracle.Composition
+import ArkLib.Interaction.Oracle.Continuation
+import ArkLib.Interaction.Oracle.Core
+import ArkLib.Interaction.Oracle.Execution
+import ArkLib.Interaction.Oracle.Spec
+import ArkLib.Interaction.Oracle.StateChain
+import ArkLib.Interaction.Reduction
 import ArkLib.OracleReduction.BCS.Basic
 import ArkLib.OracleReduction.Basic
 import ArkLib.OracleReduction.Cast

ArkLib/Data/CompPoly/Basic.lean

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+import CompPoly.Multivariate.CMvPolynomial
+import CompPoly.Multivariate.Operations
+import CompPoly.Multivariate.Rename
+import CompPoly.Univariate.ToPoly.Impl
+import ArkLib.OracleReduction.OracleInterface
+
+/-!
+# Shared CompPoly Wrappers and Oracle Interfaces
+
+Shared degree-bounded computable polynomial types used across protocols, together
+with reusable `OracleInterface` instances.
+-/
+
+open CompPoly CPoly Std
+
+namespace CPoly.CMvPolynomial
+
+variable {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
+
+/-- `p` has individual degree at most `deg` when every monomial exponent is
+bounded by `deg` in every coordinate. -/
+def IndividualDegreeLE (deg : ℕ) (p : CMvPolynomial n R) : Prop :=
+  letI := Classical.decEq R
+  ∀ i : Fin n, ∀ mono ∈ Lawful.monomials p, mono.degreeOf i ≤ deg
+
+end CPoly.CMvPolynomial
+
+/-- A computable univariate polynomial with `natDegree ≤ d`. -/
+def CDegreeLE (R : Type) [BEq R] [Semiring R] [LawfulBEq R] (d : ℕ) :=
+  { p : CPolynomial R // p.natDegree ≤ d }
+
+/-- A computable multivariate polynomial with individual degree at most `d` in
+every coordinate. -/
+def CMvDegreeLE
+    (R : Type) [BEq R] [CommSemiring R] [LawfulBEq R] (n d : ℕ) :=
+  { p : CMvPolynomial n R // CMvPolynomial.IndividualDegreeLE (R := R) d p }
+
+section OracleInterface
+
+open OracleComp OracleSpec
+
+variable {n : ℕ} {deg : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
+
+instance instOracleInterfaceCMvPolynomial :
+    OracleInterface (CMvPolynomial n R) where
+   Query := Fin n → R
+   toOC := {
+     spec := (Fin n → R) →ₒ R
+     impl := fun points => do return CMvPolynomial.eval points (← read)
+   }
+
+instance instOracleInterfaceCPolynomial [Nontrivial R] :
+    OracleInterface (CPolynomial R) where
+   Query := R
+   toOC := {
+     spec := R →ₒ R
+     impl := fun point => do return CPolynomial.eval point (← read)
+   }
+
+instance instOracleInterfaceCDegreeLE [Semiring R] :
+    OracleInterface (CDegreeLE R deg) where
+   Query := R
+   toOC := {
+     spec := R →ₒ R
+     impl := fun point => do return CPolynomial.eval point (← read).1
+   }
+
+instance instOracleInterfaceCMvDegreeLE :
+    OracleInterface (CMvDegreeLE R n deg) where
+   Query := Fin n → R
+   toOC := {
+     spec := (Fin n → R) →ₒ R
+     impl := fun points => do return CMvPolynomial.eval points (← read).1
+   }
+
+namespace Examples
+
+/-- A verifier-side query against a multivariate polynomial oracle.
+
+The verifier supplies only an evaluation point. The polynomial itself is supplied
+later as the read-only oracle environment. -/
+def verifierQueryCMvPolynomial (points : Fin n → R) :
+    ReaderM (CMvPolynomial n R) R :=
+  (instOracleInterfaceCMvPolynomial (n := n) (R := R)).toOC.impl points
+
+set_option linter.unusedSectionVars false
+
+/-- Running the verifier-side query against a concrete polynomial agrees with
+ordinary polynomial evaluation. -/
+theorem verifierQueryCMvPolynomial_run (poly : CMvPolynomial n R) (points : Fin n → R) :
+    (verifierQueryCMvPolynomial (R := R) points).run poly =
+      CMvPolynomial.eval points poly := by
+  unfold verifierQueryCMvPolynomial
+  rfl
+
+end Examples
+
+end OracleInterface

ArkLib/Interaction/Oracle/Bridge.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+import ArkLib.Interaction.Oracle.Core
+
+/-!
+# Bridge: Interaction.Spec + OracleDecoration → Oracle.Spec
+
+Structural conversion from the W-type-based
+`Interaction.Spec + RoleDecoration + OracleDecoration` to the new
+`Interaction.Oracle.Spec` inductive.
+
+## Main definitions
+
+- `Interaction.Oracle.Spec.ofInteractionSpec` — convert an `Interaction.Spec`
+  with `RoleDecoration` and `OracleDecoration` into an `Oracle.Spec`.
+  At sender nodes the continuation is treated as constant (picking a
+  representative via a provided default-element function).
+- `Interaction.Oracle.Spec.ofRoleDecoration` — convert a `RoleDecoration`
+  to `Spec.RoleDeco`.
+- `Interaction.Oracle.Spec.ofOracleDecoration` — convert an
+  `OracleDecoration` to `Spec.OracleDeco`.
+
+## Implementation notes
+
+The bridge requires a `senderDefault` function to pick a representative
+element at each sender node (since oracle message types may not have
+`Inhabited` instances). In practice, all oracle message types are nonempty,
+so any such function suffices.
+
+Verifier and reduction conversions (from `OracleVerifier`/`OracleReduction`
+to `Oracle.Verifier`/`Oracle.Reduction`) are deferred. The output types need
+to be re-indexed from `Interaction.Spec.Transcript` to
+`Oracle.Spec.PublicTranscript`, which requires careful coherence proofs. In
+practice, consumers should construct `Oracle.Spec`-based reductions natively
+rather than converting from the old representation.
+-/
+
+open OracleComp OracleSpec
+open Interaction.TwoParty
+
+namespace Interaction.Oracle.Spec
+
+/-- Convert an `Interaction.Spec + RoleDecoration + OracleDecoration` into an
+`Oracle.Spec`.
+
+At sender nodes, the continuation `rest x` is structurally required to be
+constant by `OracleDecoration` (oracle messages don't branch). We pick the
+representative using the `senderDefault` function.
+
+At receiver nodes, the continuation genuinely depends on the message, so
+`.public` is used. -/
+noncomputable def ofInteractionSpec
+    (senderDefault : ∀ (X : Type), OracleInterface X → X) :
+    (spec : Interaction.Spec) → (roles : RoleDecoration spec) →
+    OracleDecoration spec roles → Oracle.Spec
+  | .done, _, _ => .done
+  | .node X rest, ⟨.sender, rRest⟩, ⟨oi, odRest⟩ =>
+      let x₀ := senderDefault X oi
+      .oracle X (ofInteractionSpec senderDefault (rest x₀) (rRest x₀) (odRest x₀))
+  | .node X rest, ⟨.receiver, rRest⟩, odFn =>
+      .«public» X (fun x =>
+        ofInteractionSpec senderDefault (rest x) (rRest x) (odFn x))
+
+/-- Convert a `RoleDecoration` to `RoleDeco` on the resulting `Oracle.Spec`.
+Only receiver nodes carry role information in `Oracle.Spec`; sender nodes
+are structurally `.sender` by construction. -/
+noncomputable def ofRoleDecoration
+    (senderDefault : ∀ (X : Type), OracleInterface X → X) :
+    (spec : Interaction.Spec) → (roles : RoleDecoration spec) →
+    (od : OracleDecoration spec roles) →
+    RoleDeco (ofInteractionSpec senderDefault spec roles od)
+  | .done, _, _ => ⟨⟩
+  | .node _ rest, ⟨.sender, rRest⟩, ⟨oi, odRest⟩ =>
+      let x₀ := senderDefault _ oi
+      ofRoleDecoration senderDefault (rest x₀) (rRest x₀) (odRest x₀)
+  | .node _ rest, ⟨.receiver, rRest⟩, odFn =>
+      ⟨.receiver, fun x =>
+        ofRoleDecoration senderDefault (rest x) (rRest x) (odFn x)⟩
+
+/-- Convert an `OracleDecoration` to `OracleDeco` on the resulting
+`Oracle.Spec`. The `OracleInterface` at each sender node becomes the
+`.oracle` node's interface. -/
+noncomputable def ofOracleDecoration
+    (senderDefault : ∀ (X : Type), OracleInterface X → X) :
+    (spec : Interaction.Spec) → (roles : RoleDecoration spec) →
+    (od : OracleDecoration spec roles) →
+    OracleDeco (ofInteractionSpec senderDefault spec roles od)
+  | .done, _, _ => ⟨⟩
+  | .node _ rest, ⟨.sender, rRest⟩, ⟨oi, odRest⟩ =>
+      let x₀ := senderDefault _ oi
+      ⟨oi, ofOracleDecoration senderDefault (rest x₀) (rRest x₀) (odRest x₀)⟩
+  | .node _ rest, ⟨.receiver, rRest⟩, odFn =>
+      fun x => ofOracleDecoration senderDefault (rest x) (rRest x) (odFn x)
+
+end Interaction.Oracle.Spec