Theory Sumcheck_Protocol

(*******************************************************************************

  Project: Sumcheck Protocol

  Authors: Azucena Garvia Bosshard <zucegb@gmail.com>
           Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
           Jonathan Bootle, IBM Research Europe <jbt@zurich.ibm.com>

*******************************************************************************)

section ‹Sumcheck Protocol›

theory Sumcheck_Protocol
  imports 
    Public_Coin_Proofs
    Abstract_Multivariate_Polynomials
begin

subsection ‹The sumcheck problem›

text ‹Type of sumcheck instances›
type_synonym ('p, 'a, 'b) sc_inst = "'a set × 'p × 'b"

definition (in multi_variate_polynomial) 
  Sumcheck :: "('p, 'a, 'b) sc_inst set" where
  "Sumcheck = {(H, p, v) | H p v. v = (∑σ∈substs (vars p) H. eval p σ)}"


subsection ‹The sumcheck protocol›

text ‹Type of the prover› 
type_synonym ('p, 'a, 'b, 'v, 's) prover = "(('p, 'a, 'b) sc_inst, 'a, 'v, 'p, 's) prv"

text ‹Here is how the expanded type lools like @{typ [display] "('p, 'a, 'b, 'v, 's) prover"}.›


context multi_variate_polynomial begin

text ‹Sumcheck function›
fun sumcheck :: "('p, 'a, 'b, 'v, 's) prover ⇒ 's ⇒ ('p, 'a, 'b) sc_inst ⇒ 'a ⇒ ('v × 'a) list ⇒ bool" where
  "sumcheck pr s (H, p, v) r_prev [] ⟷ v = eval p Map.empty"
| "sumcheck pr s (H, p, v) r_prev ((x, r) # rm) ⟷ 
     (let (q, s') = pr (H, p, v) x (map fst rm) r_prev s in
        vars q ⊆ {x} ∧ deg q ≤ deg p ∧
        v = (∑y ∈ H. eval q [x ↦ y]) ∧ 
        sumcheck pr s' (H, inst p [x ↦ r], eval q [x ↦ r]) r rm)"

text ‹Honest prover definition›
fun honest_prover :: "('p, 'a, 'b, 'v, unit) prover" where
  "honest_prover (H, p, _) x xs _ _ = (∑σ ∈ substs (set xs) H. inst p σ, ())"

declare honest_prover.simps [simp del]
lemmas honest_prover_def = honest_prover.simps 

text ‹Lemmas on variables and degree of the honest prover.›

lemma honest_prover_vars:
  assumes "vars p ⊆ insert x V" "finite V" "H ≠ {}" "finite H" 
  shows "vars (∑σ∈substs V H. inst p σ) ⊆ {x}" 
proof -
  have *: "⋀σ. σ ∈ substs V H ⟹ vars (inst p σ) ⊆ {x}" using assms
    by (metis (no_types, lifting) Diff_eq_empty_iff Diff_insert subset_iff substE vars_inst)

  have "vars (sum (inst p) (substs V H)) ⊆ (⋃σ∈substs V H. vars (inst p σ))" 
    using ‹finite V› ‹finite H›
    by (auto simp add: vars_sum substs_finite)
  also have "… ⊆ {x}" using ‹H ≠ {}› *
    by (auto simp add: substs_nonempty vars_finite substs_finite)
  finally show ?thesis .
qed

lemma honest_prover_deg:
  assumes "H ≠ {}" "finite V"
  shows "deg (∑σ∈substs V H. inst p σ) ≤ deg p"
proof - 
  have "deg (∑σ∈substs V H. inst p σ) ≤ Max {deg (inst p σ) |σ. σ ∈ substs V H}"
    by(auto simp add: substs_finite substs_nonempty deg_sum assms)
  also have "… ≤ deg p" 
    by(auto simp add: substs_finite substs_nonempty deg_inst assms)
  finally show ?thesis .
qed


subsection ‹The sumcheck protocol as a public-coin proof instance›

text ‹Define verifier functions›

fun sc_ver0 :: "('p, 'a, 'b) sc_inst ⇒ unit ⇒ bool" where
   "sc_ver0 (H, p, v) () ⟷ v = eval p Map.empty"

fun sc_ver1 :: 
  "('p, 'a, 'b) sc_inst ⇒ 'p ⇒ 'a ⇒ 'v ⇒ 'v list ⇒ unit ⇒ bool × ('p, 'a, 'b) sc_inst × unit" 
where
   "sc_ver1 (H, p, v) q r x _ () = (
      vars q ⊆ {x} ∧ deg q ≤ deg p ∧ v = (∑y ∈ H. eval q [x ↦ y]), 
      (H, inst p [x ↦ r], eval q [x ↦ r]), 
      ()
   )"

sublocale sc: public_coin_proof sc_ver0 sc_ver1 .


text ‹Equivalence of @{term sumcheck} with public-coin proofs instance›

lemma prove_sc_eq_sumcheck:
  ‹sc.prove () pr ps (H, p, v) r rm = sumcheck pr ps (H, p, v) r rm›
proof (induction "()" pr ps "(H, p, v)" r rm arbitrary: p v rule: sc.prove.induct)
  case (1 vs prv ps r)
  then show ?case by (simp)
next
  case (2 vs prv ps r r' rs x xs)
  then show ?case by (simp split:prod.split)
qed


end
end