feat: List-based IOP model with composition & sumcheck security proofs

ArkLib.lean

@@ -150,6 +150,34 @@ import ArkLib.ProofSystem.Whir.MutualCorrAgreement
 import ArkLib.ProofSystem.Whir.OutofDomainSmpl
 import ArkLib.ProofSystem.Whir.ProximityGen
 import ArkLib.ProofSystem.Whir.RBRSoundness
+import ArkLib.Refactor.FiatShamir
+import ArkLib.Refactor.HVector
+import ArkLib.Refactor.LiftContext
+import ArkLib.Refactor.LiftContext.Lens
+import ArkLib.Refactor.LiftContext.OracleReduction
+import ArkLib.Refactor.LiftContext.Reduction
+import ArkLib.Refactor.OracleVerifier
+import ArkLib.Refactor.ProtocolSpec
+import ArkLib.Refactor.Prover
+import ArkLib.Refactor.Reduction
+import ArkLib.Refactor.Security.Composition
+import ArkLib.Refactor.Security.Composition.Completeness
+import ArkLib.Refactor.Security.Composition.KnowledgeSoundness
+import ArkLib.Refactor.Security.Composition.Soundness
+import ArkLib.Refactor.Security.Composition.Util
+import ArkLib.Refactor.Security.Defs
+import ArkLib.Refactor.Security.StateFunction
+import ArkLib.Refactor.Security.StateRestoration
+import ArkLib.Refactor.Sumcheck.Completeness
+import ArkLib.Refactor.Sumcheck.Defs
+import ArkLib.Refactor.Sumcheck.General
+import ArkLib.Refactor.Sumcheck.PartialEval
+import ArkLib.Refactor.Sumcheck.PolyUtils
+import ArkLib.Refactor.Sumcheck.Security
+import ArkLib.Refactor.Sumcheck.SingleRound
+import ArkLib.Refactor.Sumcheck.Test
+import ArkLib.Refactor.Transcript
+import ArkLib.Refactor.Verifier
 import ArkLib.ToMathlib.BigOperators.Fin
 import ArkLib.ToMathlib.Data.IndexedBinaryTree.Basic
 import ArkLib.ToMathlib.Data.IndexedBinaryTree.Equiv

ArkLib/OracleReduction/OracleInterface.lean

@@ -8,6 +8,7 @@ import VCVio
 import ArkLib.ToVCVio.SimOracle
 import CompPoly.Data.MvPolynomial.Notation
 import Mathlib.Algebra.Polynomial.Roots
+import ArkLib.Data.MvPolynomial.Interpolation
 -- import ArkLib.Data.MlPoly.Basic
 
 /-!
@@ -368,6 +369,59 @@ theorem distanceLE_polynomial_degreeLE :
 theorem distanceLE_mvPolynomial_degreeLE {σ : Type} [Fintype σ] [DecidableEq σ] :
     distanceLE (instMvPolynomialDegreeLE R d σ)
       (Fintype.card σ * d * Fintype.card R ^ (Fintype.card σ - 1)) := by
-  sorry
+  intro a b hNe
+  set p := a.val - b.val with hp_def
+  have hp : p ≠ 0 := sub_ne_zero.mpr (Subtype.val_injective.ne hNe)
+  have hDeg : ∀ i : σ, p.degreeOf i ≤ d := by
+    intro i
+    refine (MvPolynomial.degreeOf_sub_le i _ _).trans (max_le ?_ ?_)
+    · exact (MvPolynomial.mem_restrictDegree_iff_degreeOf_le _ d).mp a.property i
+    · exact (MvPolynomial.mem_restrictDegree_iff_degreeOf_le _ d).mp b.property i
+  change (Finset.univ.filter fun q =>
+      MvPolynomial.eval q a.val = MvPolynomial.eval q b.val).card ≤ _
+  have hSubset : (Finset.univ.filter fun q =>
+      MvPolynomial.eval q a.val = MvPolynomial.eval q b.val) ⊆
+    (Finset.univ : Finset (σ → R)).filter (fun q => MvPolynomial.eval q p = 0) := by
+    intro q
+    simp only [Finset.mem_filter, Finset.mem_univ, true_and]
+    intro h
+    have : MvPolynomial.eval q (a.val - b.val) = 0 := by
+      rw [map_sub, sub_eq_zero]; exact h
+    rwa [← hp_def] at this
+  have sz := MvPolynomial.schwartz_zippel_of_fintype hp (fun _ : σ => Finset.univ)
+  simp only [Fintype.piFinset_univ, Finset.card_univ, Finset.prod_const] at sz
+  suffices h : ((Finset.univ.filter
+      (fun q => MvPolynomial.eval q p = 0)).card : ℚ≥0) ≤
+      ((Fintype.card σ * d * Fintype.card R ^ (Fintype.card σ - 1) : ℕ) : ℚ≥0) from
+    le_trans (Finset.card_le_card hSubset) (Nat.cast_le.mp h)
+  have hR_pos : (0 : ℚ≥0) < (Fintype.card R : ℚ≥0) ^ Fintype.card σ := by positivity
+  rw [div_le_iff₀ hR_pos] at sz
+  calc ((Finset.univ.filter
+          (fun q => MvPolynomial.eval q p = 0)).card : ℚ≥0)
+      ≤ (∑ i : σ, ((p.degreeOf i : ℚ≥0) / (Fintype.card R : ℚ≥0))) *
+          ((Fintype.card R : ℚ≥0) ^ Fintype.card σ) := sz
+    _ ≤ ((Fintype.card σ : ℚ≥0) * (d : ℚ≥0) / (Fintype.card R : ℚ≥0)) *
+          ((Fintype.card R : ℚ≥0) ^ Fintype.card σ) := by
+        gcongr
+        calc ∑ i : σ, ((p.degreeOf i : ℚ≥0) / (Fintype.card R : ℚ≥0))
+            ≤ ∑ _i : σ, ((d : ℚ≥0) / (Fintype.card R : ℚ≥0)) := by
+              gcongr with i; exact_mod_cast hDeg i
+          _ = (Fintype.card σ : ℚ≥0) * ((d : ℚ≥0) / (Fintype.card R : ℚ≥0)) := by
+              rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
+          _ = (Fintype.card σ : ℚ≥0) * (d : ℚ≥0) / (Fintype.card R : ℚ≥0) :=
+              mul_div_assoc' _ _ _
+    _ ≤ ((Fintype.card σ * d * Fintype.card R ^ (Fintype.card σ - 1) : ℕ) : ℚ≥0) := by
+        rcases Nat.eq_zero_or_pos (Fintype.card σ) with hn | hn
+        · simp [hn]
+        · have hR_ne : (Fintype.card R : ℚ≥0) ≠ 0 :=
+            Nat.cast_ne_zero.mpr Fintype.card_ne_zero
+          have hpow : (Fintype.card R : ℚ≥0) ^ Fintype.card σ =
+              (Fintype.card R : ℚ≥0) *
+              (Fintype.card R : ℚ≥0) ^ (Fintype.card σ - 1) := by
+            conv_lhs =>
+              rw [show Fintype.card σ = (Fintype.card σ - 1) + 1 from by omega]
+            rw [pow_succ']
+          push_cast
+          rw [hpow, ← mul_assoc, div_mul_cancel₀ (h := hR_ne)]
 
 end PolynomialDistance

ArkLib/Refactor/FiatShamir.lean

@@ -0,0 +1,182 @@
+/-
+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.Refactor.Reduction
+
+/-!
+# The Fiat-Shamir Transformation (List-Based Refactored)
+
+The Fiat-Shamir transform converts a public-coin interactive reduction into a
+non-interactive reduction in the random oracle model.
+
+## Design
+
+The FS oracle is defined by structural recursion on `pSpec` with an accumulator
+`acc : List Type` tracking message types seen so far:
+- `P_to_V T` rounds extend `acc` without adding an oracle entry.
+- `V_to_P T` rounds add a challenge oracle: `(StmtIn × HVector id acc) → T`.
+
+The `V_to_P` case uses `Sum.elim` (= `OracleSpec.add`) so VCVio's `SubSpec`
+instances (`subSpec_add_right`) resolve automatically for oracle lifting.
+
+## Main definitions
+
+- `FSIdx` / `fsOracleSpec` / `fsChallengeOracle` — per-round FS challenge oracle
+- `Prover.runFS` — run a prover deriving challenges from the FS oracle
+- `Messages.deriveTranscript` — reconstruct transcript from messages + FS oracle
+- `fsProtocolSpec` — single-message non-interactive protocol spec
+- `Reduction.fiatShamir` — the full Fiat-Shamir transformation
+-/
+
+open OracleComp OracleSpec
+
+namespace ProtocolSpec
+
+/-! ## Fiat-Shamir Oracle Specification -/
+
+/-- Index type for FS oracle queries: nested sum with one entry per `V_to_P` round.
+`P_to_V` rounds simply extend the accumulator without adding a query index. -/
+@[reducible]
+def FSIdx (StmtIn : Type) : List Type → ProtocolSpec → Type
+  | _, [] => PEmpty
+  | acc, (.P_to_V T _) :: tl => FSIdx StmtIn (acc ++ [T]) tl
+  | acc, (.V_to_P _) :: tl => (StmtIn × HVector id acc) ⊕ FSIdx StmtIn acc tl
+
+/-- FS oracle spec: maps each `V_to_P` round's query to its challenge type.
+The `V_to_P` case is `Sum.elim`, which is definitionally `OracleSpec.add`. -/
+@[reducible]
+def fsOracleSpec (StmtIn : Type) : (acc : List Type) → (pSpec : ProtocolSpec) →
+    OracleSpec (FSIdx StmtIn acc pSpec)
+  | _, [] => (PEmpty.elim ·)
+  | acc, (.P_to_V T _) :: tl => fsOracleSpec StmtIn (acc ++ [T]) tl
+  | acc, (.V_to_P T) :: tl =>
+    Sum.elim (fun (_ : StmtIn × HVector id acc) => T) (fsOracleSpec StmtIn acc tl)
+
+/-- Top-level FS challenge oracle (accumulator starts empty). -/
+abbrev fsChallengeOracle (StmtIn : Type) (pSpec : ProtocolSpec) :=
+  fsOracleSpec StmtIn [] pSpec
+
+/-! ## Lifting Helper
+
+In the `V_to_P` recursive case, the tail oracle spec `fsOracleSpec acc tl` must be
+lifted into the full spec `fsOracleSpec acc (.V_to_P T :: tl)`. Since the latter
+unfolds to `Sum.elim (fun _ => T) (fsOracleSpec acc tl)`, the tail spec embeds as
+the right summand. We lift the *combined* `oSpec + fsOracleSpec acc tl` into
+`oSpec + fsOracleSpec acc (.V_to_P T :: tl)` by routing `oSpec` queries to `Sum.inl`
+and `fsOracleSpec acc tl` queries to `Sum.inr ∘ Sum.inr`. -/
+
+def liftFSTail {ι : Type} (oSpec : OracleSpec ι)
+    (StmtIn : Type) (acc : List Type) (T : Type) (tl : ProtocolSpec) :
+    QueryImpl (oSpec + fsOracleSpec StmtIn acc tl)
+      (OracleComp (oSpec + fsOracleSpec StmtIn acc ((.V_to_P T) :: tl))) :=
+  fun
+    | .inl q => liftM (query (.inl q) :
+        OracleQuery (oSpec + fsOracleSpec StmtIn acc ((.V_to_P T) :: tl)) _)
+    | .inr q => liftM (query (.inr (.inr q)) :
+        OracleQuery (oSpec + fsOracleSpec StmtIn acc ((.V_to_P T) :: tl)) _)
+
+/-! ## Prover FS Execution -/
+
+/-- Run a prover with Fiat-Shamir challenge derivation.
+
+At each `P_to_V` round the message is extracted normally and added to the
+accumulator. At each `V_to_P` round the FS oracle is queried with
+`(stmt, accumulated messages)` to derive the challenge. -/
+def Prover.runFS {ι : Type} {oSpec : OracleSpec ι}
+    {Output StmtIn : Type} (stmt : StmtIn) :
+    (acc : List Type) → (pSpec : ProtocolSpec) →
+    Prover (OracleComp oSpec) Output pSpec →
+    HVector id acc →
+    OracleComp (oSpec + fsOracleSpec StmtIn acc pSpec) (Messages pSpec × Output)
+  | _, [], output, _ => pure (HVector.nil, output)
+  | acc, (.P_to_V T _) :: tl, prover, accMsgs => do
+    let (msg, cont) := prover
+    let next ← liftM cont
+    let (msgs, out) ← Prover.runFS stmt (acc ++ [T]) tl next (HVector.snoc accMsgs msg)
+    return (msg ::ₕ msgs, out)
+  | acc, (.V_to_P T) :: tl, prover, accMsgs => do
+    let chal : T ← liftM (query
+      (spec := oSpec + fsOracleSpec StmtIn acc ((.V_to_P T) :: tl))
+      (.inr (.inl (stmt, accMsgs))))
+    let next ← liftM (prover chal)
+    let (msgs, out) ← simulateQ (liftFSTail oSpec StmtIn acc T tl)
+      (Prover.runFS stmt acc tl next accMsgs)
+    return (msgs, out)
+
+/-! ## Transcript Derivation -/
+
+/-- Derive the full transcript from messages by querying the FS oracle for
+each challenge. The verifier-side counterpart to `Prover.runFS`. -/
+def Messages.deriveTranscript {ι : Type} {oSpec : OracleSpec ι}
+    {StmtIn : Type} (stmt : StmtIn) :
+    (acc : List Type) → (pSpec : ProtocolSpec) →
+    HVector id acc → Messages pSpec →
+    OracleComp (oSpec + fsOracleSpec StmtIn acc pSpec) (Transcript pSpec)
+  | _, [], _, _ => pure HVector.nil
+  | acc, (.P_to_V T _) :: tl, accMsgs, msgs => do
+    let msg := msgs.head
+    let rest ← Messages.deriveTranscript stmt (acc ++ [T]) tl
+      (HVector.snoc accMsgs msg) msgs.tail
+    return msg ::ₕ rest
+  | acc, (.V_to_P T) :: tl, accMsgs, msgs => do
+    let chal : T ← liftM (query
+      (spec := oSpec + fsOracleSpec StmtIn acc ((.V_to_P T) :: tl))
+      (.inr (.inl (stmt, accMsgs))))
+    let rest ← simulateQ (liftFSTail oSpec StmtIn acc T tl)
+      (Messages.deriveTranscript stmt acc tl accMsgs msgs)
+    return chal ::ₕ rest
+
+/-! ## Non-Interactive Protocol Spec -/
+
+/-- Trivial `OracleInterface` for the bundled message type (no meaningful queries). -/
+def Messages.trivialOracleInterface (pSpec : ProtocolSpec) :
+    OracleInterface (Messages pSpec) where
+  Query := PEmpty
+  toOC := { spec := (PEmpty.elim ·), impl := (PEmpty.elim ·) }
+
+/-- The FS protocol spec: a single prover-to-verifier message round. -/
+def fsProtocolSpec (pSpec : ProtocolSpec) : ProtocolSpec :=
+  [.P_to_V (Messages pSpec) (Messages.trivialOracleInterface pSpec)]
+
+/-! ## Fiat-Shamir Prover -/
+
+/-- The FS honest prover: runs the original prover with FS challenge derivation,
+then packages all messages into a single non-interactive message. -/
+def HonestProver.fiatShamir {ι : Type} {oSpec : OracleSpec ι}
+    {StmtIn WitIn StmtOut WitOut : Type} {pSpec : ProtocolSpec}
+    (prover : HonestProver (OracleComp oSpec) StmtIn WitIn StmtOut WitOut pSpec) :
+    HonestProver (OracleComp (oSpec + fsChallengeOracle StmtIn pSpec))
+      StmtIn WitIn StmtOut WitOut (fsProtocolSpec pSpec) :=
+  fun (stmt, wit) => do
+    let p ← liftM (prover (stmt, wit))
+    let (msgs, out) ← Prover.runFS stmt [] pSpec p (HVector.nil : HVector id [])
+    return (msgs, pure out)
+
+/-! ## Fiat-Shamir Verifier -/
+
+/-- The FS verifier: receives all messages in one round, derives challenges from
+the FS oracle to reconstruct the full transcript, then runs the original verifier. -/
+def Verifier.fiatShamir {ι : Type} {oSpec : OracleSpec ι}
+    {StmtIn StmtOut : Type} {pSpec : ProtocolSpec}
+    (verifier : Verifier (OracleComp oSpec) StmtIn StmtOut pSpec) :
+    Verifier (OracleComp (oSpec + fsChallengeOracle StmtIn pSpec))
+      StmtIn StmtOut (fsProtocolSpec pSpec) :=
+  fun stmt tr => OptionT.mk do
+    let msgs : Messages pSpec := tr.head
+    let fullTr ← Messages.deriveTranscript stmt [] pSpec (HVector.nil : HVector id []) msgs
+    liftM (verifier stmt fullTr).run
+
+/-! ## Fiat-Shamir Reduction -/
+
+/-- The Fiat-Shamir transformation for an interactive reduction. -/
+def Reduction.fiatShamir {ι : Type} {oSpec : OracleSpec ι}
+    {StmtIn WitIn StmtOut WitOut : Type} {pSpec : ProtocolSpec}
+    (reduction : Reduction (OracleComp oSpec) StmtIn WitIn StmtOut WitOut pSpec) :
+    Reduction (OracleComp (oSpec + fsChallengeOracle StmtIn pSpec))
+      StmtIn WitIn StmtOut WitOut (fsProtocolSpec pSpec) where
+  prover := HonestProver.fiatShamir reduction.prover
+  verifier := Verifier.fiatShamir reduction.verifier
+
+end ProtocolSpec