Theory Soundness_Proof

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

  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 ‹Soundness Proof for the Sumcheck Protocol›

theory Soundness_Proof
  imports
    Probability_Tools
    Sumcheck_Protocol
begin

context multi_variate_polynomial begin

― ‹Helper lemma: 
   Proves that the probability of two different polynomials evaluating to the same value is small.›
lemma prob_roots:
  assumes "deg q2 ≤ deg p" and "vars q2 ⊆ {x}" 
  shows "measure_pmf.prob (pmf_of_set UNIV) 
        {r. deg q1 ≤ deg p ∧ vars q1 ⊆ {x} ∧ q1 ≠ q2 ∧ eval q1 [x ↦ r] = eval q2 [x ↦ r]} 
        ≤ real (deg p) / real CARD('a)"
proof -
  have "card {r. deg q1 ≤ deg p ∧ vars q1 ⊆ {x} ∧ 
                 q1 ≠ q2 ∧ eval q1 [x ↦ r] = eval q2 [x ↦ r]} = 
         card {r. deg q1 ≤ deg p ∧ vars q1 ⊆ {x} ∧ 
                  deg q2 ≤ deg p ∧ vars q2 ⊆ {x} ∧
                  q1 ≠ q2 ∧ eval q1 [x ↦ r] = eval q2 [x ↦ r]}" using assms by(auto)
   also have "… ≤ deg p"  by(auto simp add: roots)
   finally show ?thesis by(auto simp add: measure_pmf_of_set divide_right_mono) 
qed   


text ‹Soundness proof›

theorem soundness_inductive:
  assumes 
    "vars p ⊆ set vs" and
    "deg p ≤ d" and 
    "distinct vs" and 
    "H ≠ {}"
  shows 
    "measure_pmf.prob 
       (pmf_of_set (tuples UNIV (length vs)))
       {rs. 
          sumcheck pr s (H, p, v) r (zip vs rs) ∧ 
          v ≠ (∑σ ∈ substs (set vs) H. eval p σ)} 
     ≤ real (length vs) * real d / real (CARD('a))"
  using assms
proof(induction vs arbitrary: s p v r)
  case Nil
  show ?case
    by(simp)
next
  case (Cons x vs)

  ― ‹abbreviations›
  let ?prob = "measure_pmf.prob (pmf_of_set (tuples UNIV (Suc (length vs))))"
  let ?reduced_prob = "measure_pmf.prob (pmf_of_set (tuples UNIV (length vs)))"

  let ?q = "∑σ ∈ substs (set vs) H. inst p σ"      ― ‹honest polynomial q›

  let ?pr_q = "fst (pr (H, p, v) x vs r s)"      ― ‹polynomial q from prover›
  let ?pr_s' = "snd (pr (H, p, v) x vs r s)"     ― ‹prover's next state›

  ― ‹some useful derived facts› 
  have ‹vars (p) ⊆ insert x (set vs)› ‹x ∉ set vs› ‹distinct vs› 
    using ‹vars (p) ≤ set (x # vs)› ‹distinct (x # vs)› by auto

  have P0: 
    ‹?prob {r1#rs | r1 rs.                
               deg (?pr_q) ≤ deg (p) ∧ vars (?pr_q) ⊆ {x} ∧      
               v = (∑a∈H. eval (?pr_q) [x ↦ a]) ∧
               sumcheck pr (?pr_s') (H, inst (p) [x ↦ r1], eval (?pr_q) [x ↦ r1]) r1 (zip vs rs) ∧ 
               v ≠ (∑σ ∈ substs (insert x (set vs)) H. eval (p) σ) ∧ ?pr_q = ?q} = 0›
  proof -
    have "(∑a∈H. eval (?q) [x ↦ a]) = 
          (∑a∈H. ∑σ ∈ substs (set vs) H. eval (p) ([x ↦ a] ++ σ))"
      using ‹vars (p) ⊆ insert x (set vs)› ‹x ∉ set vs›  
      by(auto simp add: eval_sum_inst)
    moreover 
    have "(∑a∈H. ∑σ ∈ substs (set vs) H. eval (p) ([x ↦ a] ++ σ)) =
          (∑σ ∈ substs (insert x (set vs)) H. eval (p) σ)" using ‹x ∉ set vs›
      by(auto simp add: sum_merge) 
    ultimately
    have "{r1#rs | r1 rs.                      
                 v = (∑a∈H. eval (?pr_q) [x ↦ a]) ∧
                 v ≠ (∑σ ∈ substs (insert x (set vs)) H. eval (p) σ) ∧ ?pr_q = ?q} = {}" 
      by(auto)    
    then show "?thesis" 
      by (intro prob_empty) (auto 4 4)
  qed

  { ― ‹left-hand-side case where we use the roots assumption›
    have ‹?prob {r1#rs | r1 rs. 
                       deg (?pr_q) ≤ deg (p) ∧ vars (?pr_q) ⊆ {x} ∧
                       v = (∑a∈H. eval (?pr_q) [x ↦ a]) ∧
                       sumcheck pr (?pr_s') (H, inst (p) [x ↦ r1], eval (?pr_q) [x ↦ r1]) r1 (zip vs rs) ∧
                       ?pr_q ≠ ?q ∧ eval (?pr_q) [x ↦ r1] = eval (?q) [x ↦ r1]} ≤
          ?prob {r1#rs | r1 rs. 
                       deg (?pr_q) ≤ deg (p) ∧ vars (?pr_q) ⊆ {x} ∧
                       ?pr_q ≠ ?q ∧ eval (?pr_q) [x ↦ r1] = eval (?q) [x ↦ r1]}›
      by (intro prob_mono) (auto 4 4) 

    also have ‹... =
          measure_pmf.prob (pmf_of_set UNIV) {r1. 
              deg (?pr_q) ≤ deg (p) ∧ vars (?pr_q) ⊆ {x} ∧
              ?pr_q ≠ ?q ∧ eval (?pr_q) [x ↦ r1] = eval (?q) [x ↦ r1]}›
      by (auto simp add: prob_tuples_hd_tl_indep[where Q = "λrs. True", simplified]) 

    also have ‹... ≤ real (deg (p)) / real CARD('a)› 
      using ‹vars (p) ⊆ insert x (set vs)› ‹H ≠ {}› 
      by(auto simp add: prob_roots honest_prover_deg honest_prover_vars)

    also have ‹... ≤ real d / real CARD('a)› using ‹deg (p) ≤ d›
      by (simp add: divide_right_mono) 

    finally
    have ‹?prob {r1#rs | r1 rs. 
                       deg (?pr_q) ≤ deg (p) ∧ vars (?pr_q) ⊆ {x} ∧
                       v = (∑a∈H. eval (?pr_q) [x ↦ a]) ∧
                       sumcheck pr (?pr_s') (H, inst (p) [x ↦ r1], eval (?pr_q) [x ↦ r1]) r1 (zip vs rs) ∧
                       ?pr_q ≠ ?q ∧ eval (?pr_q) [x ↦ r1] = eval (?q) [x ↦ r1]}
           ≤ real d / real CARD('a)› .
  }
  note RP_left = this

  {
    have *: ‹⋀α. eval (?q) [x ↦ α] = (∑σ ∈ substs (set vs) H. eval (inst (p) [x ↦ α]) σ)›
      using ‹vars (p) ⊆ insert x (set vs)› ‹x ∉ set vs›
      by(auto simp add: eval_sum_inst_commute)

    have ‹⋀α. vars (inst (p) [x ↦ α]) ⊆ set vs› using vars_inst ‹vars (p) ⊆ insert x (set vs)› 
      by fastforce
    have ‹⋀α. deg (inst (p) [x ↦ α]) ≤ d› using deg_inst ‹deg (p) ≤ d›
      using le_trans by blast

    ― ‹right-hand-side case where we apply the induction hypothesis›
    have ‹?prob {r1#rs | r1 rs.
                       deg (?pr_q) ≤ deg (p) ∧ vars (?pr_q) ⊆ {x} ∧
                       v = (∑a∈H. eval (?pr_q) [x ↦ a]) ∧
                       sumcheck pr (?pr_s') (H, inst (p) [x ↦ r1], eval (?pr_q) [x ↦ r1]) r1 (zip vs rs) ∧
                       ?pr_q ≠ ?q ∧ eval (?pr_q) [x ↦ r1] ≠ eval (?q) [x ↦ r1]}
         ≤ ?prob {r1#rs | r1 rs. 
                       sumcheck pr (?pr_s') (H, inst (p) [x ↦ r1], eval (?pr_q) [x ↦ r1]) r1 (zip vs rs) ∧
                       eval (?pr_q) [x ↦ r1] ≠ (∑σ ∈ substs (set vs) H. eval (inst (p) [x ↦ r1]) σ)}›
      by(intro prob_mono) (auto simp add: *)

    ― ‹fix @{text "r1"}›
    also have ‹… = (∑α ∈ UNIV.
                     ?reduced_prob {rs. 
                       sumcheck pr (?pr_s') (H, inst (p) [x ↦ α], eval (?pr_q) [x ↦ α]) α (zip vs rs) ∧
                       eval (?pr_q) [x ↦ α] ≠ (∑σ ∈ substs (set vs) H. eval (inst (p) [x ↦ α]) σ)})
                  / real(CARD('a))›
      by(auto simp add: prob_tuples_fixed_hd)

    ― ‹apply the induction hypothesis›
    also have ‹… ≤ (∑α ∈ (UNIV::'a set). real (length vs) * real d / real CARD('a)) 
                    / real(CARD('a))›
      using ‹⋀α. vars (inst (p) [x ↦ α]) ⊆ set vs› 
            ‹⋀α. deg (inst (p) [x ↦ α]) ≤ d› 
            ‹distinct vs› ‹H ≠ {}›
      by (intro divide_right_mono sum_mono Cons.IH) (auto)

    also have ‹… = real (length vs) * real d / real CARD('a)›
      by fastforce  

    finally
    have ‹?prob {r1#rs | r1 rs. 
                       deg (?pr_q) ≤ deg (p) ∧ vars (?pr_q) ⊆ {x} ∧
                       v = (∑a∈H. eval (?pr_q) [x ↦ a]) ∧
                       sumcheck pr (?pr_s') (H, inst (p) [x ↦ r1], eval (?pr_q) [x ↦ r1]) r1 (zip vs rs) ∧
                       ?pr_q ≠ ?q ∧ eval (?pr_q) [x ↦ r1] ≠ eval (?q) [x ↦ r1]}
         ≤ real (length vs) * real d / real CARD('a)› .
  }
  note RP_right = this 
  
  ― ‹main equational reasoning proof›
  have ‹?prob {rs. 
          sumcheck pr s (H, p, v) r (zip (x # vs) rs) ∧ 
          v ≠ (∑σ ∈ substs (insert x (set vs)) H. eval p σ)} 
      = ?prob {r1#rs | r1 rs. sumcheck pr s (H, p, v) r (zip (x # vs) (r1#rs))
                               ∧ v ≠ (∑σ ∈ substs (insert x (set vs)) H. eval p σ)}›
   by(intro prob_cong) (auto simp add: tuples_Suc) 

  ― ‹unfold sumcheck›
  also have ‹… = ?prob {r1#rs | r1 rs. 
                  (let (q, s') = pr (H, p, v) x vs r s in
                  deg q ≤ deg p ∧ vars q ⊆ {x} ∧
                  v = (∑a ∈ H. eval q [x ↦ a])  ∧ 
                  sumcheck pr s' (H, inst p [x ↦ r1], eval q [x ↦ r1]) r1 (zip vs rs)) ∧ 
                  v ≠ (∑σ ∈ substs (insert x (set vs)) H. eval p σ)}›
    by(intro prob_cong) (auto del: subsetI)

  also have ‹… = ?prob {r1#rs | r1 rs . 
                  deg ?pr_q ≤ deg p ∧ vars ?pr_q ⊆ {x} ∧
                  v = (∑a∈H. eval ?pr_q [x ↦ a]) ∧
                  sumcheck pr ?pr_s' (H, inst p [x ↦ r1], eval ?pr_q [x ↦ r1]) r1 (zip vs rs) ∧ 
                  v ≠ (∑σ ∈ substs (insert x (set vs)) H. eval p σ)}›
    by (intro prob_cong) (auto del: subsetI)

  ― ‹case split on whether prover's polynomial q equals honest one›
   also have ‹… = ?prob {r1#rs | r1 rs.                
                     deg (?pr_q) ≤ deg (p) ∧ vars (?pr_q) ⊆ {x} ∧      
                     v = (∑a∈H. eval (?pr_q) [x ↦ a]) ∧
                     sumcheck pr (?pr_s') (H, inst (p) [x ↦ r1], eval (?pr_q) [x ↦ r1]) r1 (zip vs rs) ∧ 
                     v ≠ (∑σ ∈ substs (insert x (set vs)) H. eval (p) σ) ∧ ?pr_q = ?q} 
                + ?prob {r1#rs | r1 rs. 
                     deg (?pr_q) ≤ deg (p) ∧ vars (?pr_q) ⊆ {x} ∧
                     v = (∑a∈H. eval (?pr_q) [x ↦ a]) ∧
                     sumcheck pr (?pr_s') (H, inst (p) [x ↦ r1], eval (?pr_q) [x ↦ r1]) r1 (zip vs rs) ∧
                     v ≠ (∑σ ∈ substs (insert x (set vs)) H. eval (p) σ) ∧ ?pr_q ≠ ?q}›
     by(intro prob_disjoint_cases) auto
 
  ― ‹first probability is 0›
  also have ‹… = ?prob {r1#rs | r1 rs. 
                     deg (?pr_q) ≤ deg (p) ∧ vars (?pr_q) ⊆ {x} ∧
                     v = (∑a∈H. eval (?pr_q) [x ↦ a]) ∧
                     sumcheck pr (?pr_s') (H, inst (p) [x ↦ r1], eval (?pr_q) [x ↦ r1]) r1 (zip vs rs) ∧
                     v ≠ (∑σ ∈ substs (insert x (set vs)) H. eval (p) σ) ∧ ?pr_q ≠ ?q}› 
    by (simp add: P0)

  ― ‹dropped condition›
  also have ‹… ≤ ?prob {r1#rs | r1 rs. 
                     deg (?pr_q) ≤ deg (p) ∧ vars (?pr_q) ⊆ {x} ∧
                     v = (∑a∈H. eval (?pr_q) [x ↦ a]) ∧
                     sumcheck pr (?pr_s') (H, inst (p) [x ↦ r1], eval (?pr_q) [x ↦ r1]) r1 (zip vs rs) ∧
                     ?pr_q ≠ ?q}›
    by(intro prob_mono) (auto)

  also have ‹… =
          ?prob {r1#rs | r1 rs.  
                       deg (?pr_q) ≤ deg (p) ∧ vars (?pr_q) ⊆ {x} ∧
                       v = (∑a∈H. eval (?pr_q) [x ↦ a]) ∧
                       sumcheck pr (?pr_s') (H, inst (p) [x ↦ r1], eval (?pr_q) [x ↦ r1]) r1 (zip vs rs) ∧
                       ?pr_q ≠ ?q ∧ eval (?pr_q) [x ↦ r1] = eval (?q) [x ↦ r1]} + 
          ?prob {r1#rs | r1 rs.  
                       deg (?pr_q) ≤ deg (p) ∧ vars (?pr_q) ⊆ {x} ∧
                       v = (∑a∈H. eval (?pr_q) [x ↦ a])  ∧
                       sumcheck pr (?pr_s') (H, inst (p) [x ↦ r1], eval (?pr_q) [x ↦ r1]) r1 (zip vs rs) ∧
                       ?pr_q ≠ ?q ∧ eval (?pr_q) [x ↦ r1] ≠ eval (?q) [x ↦ r1]}›
    by(intro prob_disjoint_cases) (auto)

  also have ‹… ≤ real d / real CARD('a) + 
                  (real (length vs) * real d) / real CARD('a)›
    by (intro add_mono RP_left RP_right)

  also have ‹… = (1 + real (length vs)) * real d / real CARD('a)›
    by (metis add_divide_distrib mult_Suc of_nat_Suc of_nat_add of_nat_mult)

  finally show ?case by simp
qed


corollary soundness:
  assumes 
    "(H, p, v) ∉ Sumcheck"
    "vars p = set vs" and  
    "distinct vs" and 
    "H ≠ {}"
  shows 
    "measure_pmf.prob 
       (pmf_of_set (tuples UNIV (arity p)))
       {rs. sumcheck pr s (H, p, v) r (zip vs rs)} 
     ≤ real (arity p) * real (deg p) / real (CARD('a))"
  using assms
proof - 
  have *: ‹arity p = length vs› using ‹vars p = set vs› ‹distinct vs› 
    by (simp add: arity_def distinct_card)

  have "measure_pmf.prob (pmf_of_set (tuples UNIV (arity p)))
          {rs. sumcheck pr s (H, p, v) r (zip vs rs)} =
        measure_pmf.prob (pmf_of_set (tuples UNIV (arity p)))
          {rs. sumcheck pr s (H, p, v) r (zip vs rs) ∧ (H, p, v) ∉ Sumcheck}"
  using ‹(H, p, v) ∉ Sumcheck›
    by (intro prob_cong) (auto)
  also have "… ≤ real (arity p) * real (deg p) / real (CARD('a))" using assms(2-) *
    by (auto simp add: Sumcheck_def intro!: soundness_inductive)
  finally show ?thesis by simp
qed


end 

end