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

AGENTS.md

@@ -27,13 +27,26 @@ Start with [`README.md`](README.md) for project overview.
 
 ## Guardrails
 
-- Lean defaults: `autoImplicit = false`; the long-file linter cap is `1500` unless a file opts
-  out locally.
+- `autoImplicit = false` is set globally in `lakefile.toml`; do **not** add
+  `set_option autoImplicit false` in individual files.
+- The long-file linter cap is `1500` unless a file opts out locally.
 - `ArkLib.lean` is generated; do not hand-edit it.
+- Prefer readable Lean notation when it helps clarity: use notation such as `∑`, `∏`,
+  infix operators, binder notation, and dot notation instead of more verbose combinator
+  forms when the result is clearer and elaborates cleanly.
+- Prefer term-style definitions over tactic-style definitions. Do not start a definition
+  with a `by` block unless there is a strong reason; if a definition seems to require
+  tactics, first reconsider the surrounding API, helper definitions, or expected normal form.
+- Prefer existing library and repo combinators over bespoke helper definitions for simple
+  tuple/index plumbing. If a definition is just snoc/append/update/projection/reindexing and a
+  clear standard combinator already expresses it, use that directly instead of writing or keeping
+  a wrapper definition.
 - Edit source, not derived output such as `.lake/`, `blueprint/web/`, `blueprint/print/`,
   `dependency_graphs/`, or `home_page/docs/`.
 - Pre-existing `sorry` blocks exist in active formalizations; distinguish existing gaps from new
   regressions.
+- Docstrings must be intrinsic and descriptive. Cross-reference *live* sibling definitions, but
+  never reference removed/renamed definitions, change history, or use reactive language.
 - If a PR changes commands, repo structure, generated outputs, or the blueprint/citation
   workflow, update the matching page in [`docs/wiki/`](docs/wiki/README.md) in the same PR.
 - Promote recurring agent learnings into [`docs/wiki/`](docs/wiki/README.md); do not let stable

ArkLib.lean

@@ -53,6 +53,8 @@ import ArkLib.Data.CodingTheory.ProximityGap.DG25.Basic
 import ArkLib.Data.CodingTheory.ProximityGap.DG25.MainResults
 import ArkLib.Data.CodingTheory.ProximityGap.DG25.ReedSolomon
 import ArkLib.Data.CodingTheory.ReedSolomon
+import ArkLib.Data.CompPoly.Basic
+import ArkLib.Data.CompPoly.Fold
 import ArkLib.Data.EllipticCurve.BN254
 import ArkLib.Data.Fin.Basic
 import ArkLib.Data.Fin.Fold
@@ -81,6 +83,23 @@ import ArkLib.Data.Polynomial.RationalFunctions
 import ArkLib.Data.Polynomial.SplitFold
 import ArkLib.Data.Probability.Instances
 import ArkLib.Data.Probability.Notation
+import ArkLib.Interaction.Boundary.Compatibility
+import ArkLib.Interaction.Boundary.Core
+import ArkLib.Interaction.Boundary.Oracle
+import ArkLib.Interaction.Boundary.OracleSecurity
+import ArkLib.Interaction.Boundary.Reification
+import ArkLib.Interaction.Boundary.Security
+import ArkLib.Interaction.FiatShamir.Basic
+import ArkLib.Interaction.FiatShamir.DuplexSponge
+import ArkLib.Interaction.FiatShamir.Transform
+import ArkLib.Interaction.Oracle.Continuation
+import ArkLib.Interaction.Oracle.Core
+import ArkLib.Interaction.Oracle.Execution
+import ArkLib.Interaction.Oracle.StateChain
+import ArkLib.Interaction.OracleReification
+import ArkLib.Interaction.OracleSecurity
+import ArkLib.Interaction.Reduction
+import ArkLib.Interaction.Security
 import ArkLib.OracleReduction.BCS.Basic
 import ArkLib.OracleReduction.Basic
 import ArkLib.OracleReduction.Cast
@@ -147,6 +166,13 @@ import ArkLib.ProofSystem.ConstraintSystem.MemoryChecking
 import ArkLib.ProofSystem.ConstraintSystem.Plonk
 import ArkLib.ProofSystem.ConstraintSystem.R1CS
 import ArkLib.ProofSystem.Fri.Domain
+import ArkLib.ProofSystem.Fri.Interaction.Core
+import ArkLib.ProofSystem.Fri.Interaction.FinalFold
+import ArkLib.ProofSystem.Fri.Interaction.FoldPhase
+import ArkLib.ProofSystem.Fri.Interaction.FoldRound
+import ArkLib.ProofSystem.Fri.Interaction.General
+import ArkLib.ProofSystem.Fri.Interaction.Protocol
+import ArkLib.ProofSystem.Fri.Interaction.QueryRound
 import ArkLib.ProofSystem.Fri.RoundConsistency
 import ArkLib.ProofSystem.Fri.Spec.General
 import ArkLib.ProofSystem.Fri.Spec.SingleRound
@@ -160,6 +186,11 @@ import ArkLib.ProofSystem.Stir.ProximityBound
 import ArkLib.ProofSystem.Stir.ProximityGap
 import ArkLib.ProofSystem.Stir.Quotienting
 import ArkLib.ProofSystem.Sumcheck.Impl.Basic
+import ArkLib.ProofSystem.Sumcheck.Interaction.CompPoly
+import ArkLib.ProofSystem.Sumcheck.Interaction.Defs
+import ArkLib.ProofSystem.Sumcheck.Interaction.General
+import ArkLib.ProofSystem.Sumcheck.Interaction.Oracle
+import ArkLib.ProofSystem.Sumcheck.Interaction.SingleRound
 import ArkLib.ProofSystem.Sumcheck.Spec.General
 import ArkLib.ProofSystem.Sumcheck.Spec.SingleRound
 import ArkLib.ProofSystem.Whir.BlockRelDistance

ArkLib/Data/CompPoly/Basic.lean

@@ -0,0 +1,81 @@
+/-
+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
+
+attribute [local instance] instDecidableEqOfLawfulBEq
+
+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 :=
+  ∀ 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
+   }
+
+end OracleInterface

ArkLib/Data/CompPoly/Fold.lean

@@ -0,0 +1,63 @@
+/-
+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 ArkLib.Data.CompPoly.Basic
+import ArkLib.Data.Polynomial.SplitFold
+
+/-!
+# Computable Split/Fold for `CPolynomial`
+
+Native computable `CPolynomial` versions of the split/fold operations used by
+FRI. The definitions operate directly on CompPoly coefficients and do not route
+through Mathlib polynomials.
+-/
+
+open CompPoly CPoly
+open scoped BigOperators
+
+namespace CompPoly.CPolynomial
+
+variable {R : Type} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R]
+
+/-- The `i`-th component of the `n`-way split of a computable polynomial. -/
+def splitNth (n : ℕ) [NeZero n] (p : CPolynomial R) : Fin n → CPolynomial R :=
+  fun i => ∑ j ∈ p.support,
+    if j % n = (i : ℕ) then
+      monomial (j / n) (p.coeff j)
+    else
+      0
+
+/-- Recombine the `n`-way split of `p` using powers of `α`. -/
+def foldNth (n : ℕ) [NeZero n] (p : CPolynomial R) (α : R) :
+    CPolynomial R :=
+  ∑ i : Fin n, C (α ^ (i : ℕ)) * splitNth n p i
+
+end CompPoly.CPolynomial
+
+section ToPoly
+
+open Polynomial
+
+namespace CompPoly.CPolynomial
+
+variable {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] [DecidableEq R]
+
+theorem splitNth_toPoly (n : ℕ) [NeZero n] (p : CPolynomial R) (i : Fin n) :
+    (splitNth n p i).toPoly = p.toPoly.splitNth n i := by
+  sorry
+
+theorem foldNth_toPoly (n : ℕ) [NeZero n] (p : CPolynomial R) (α : R) :
+    (foldNth n p α).toPoly = p.toPoly.foldNth n α := by
+  sorry
+
+theorem foldNth_natDegree_le_of_le
+    (n d : ℕ) [NeZero n] (p : CPolynomial R) (α : R)
+    (hdeg : p.natDegree ≤ n * d) :
+    (foldNth n p α).natDegree ≤ d := by
+  sorry
+
+end CompPoly.CPolynomial
+
+end ToPoly