Theory Completeness_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 ‹Completeness Proof for the Sumcheck Protocol›

theory Completeness_Proof
  imports
    Sumcheck_Protocol
begin

context multi_variate_polynomial begin

text ‹Completeness proof›

theorem completeness_inductive:  
  assumes 
    ‹v = (∑σ ∈ substs (set (map fst rm)) H. eval p σ)›
    ‹vars p ⊆ set (map fst rm)›
    ‹distinct (map fst rm)›
    ‹H ≠ {}›
  shows 
    "sumcheck honest_prover u (H, p, v) r_prev rm"
  using assms
proof(induction honest_prover u "(H, p, v)" r_prev rm arbitrary: H p v rule: sumcheck.induct)
  case (1 s H p v r_prev)
  then show ?case by(simp)
next
  case (2 s H p v r_prev x r rm)

  note IH = 2(1)    ― ‹induction hypothesis›

  let ?V = "set (map fst rm)"
  let ?q = "(∑σ ∈ substs ?V H. inst p σ)"

  have ‹vars p ⊆ insert x ?V› ‹x ∉ ?V› ‹distinct (map fst rm)›
    using 2(3-4) by(auto)

  ― ‹evaluation check›
  have ‹(∑σ ∈ substs (insert x ?V) H. eval p σ) = (∑h∈H. eval ?q [x ↦ h])›
  proof - 
    have "(∑σ∈substs (insert x ?V) H. eval p σ) = 
          (∑h∈H. (∑σ ∈ substs ?V H. eval p ([x ↦ h] ++ σ)))" 
      using ‹x ∉ ?V› 
      by(auto simp add: sum_merge)
    also have "… = (∑h∈H. eval ?q [x ↦ h])"
      using ‹vars p ⊆ insert x ?V›
      by(auto simp add: eval_sum_inst)
    finally show ?thesis .
  qed
  moreover 
  ― ‹recursive check›
  have ‹sumcheck honest_prover () (H, inst p [x ↦ r], eval ?q [x ↦ r]) r rm›
  proof -
    have ‹vars (inst p [x ↦ r]) ⊆ ?V› 
      using ‹vars p ⊆ insert x ?V› vars_inst by fastforce
    moreover
    have "eval ?q [x ↦ r] = (∑σ ∈ substs ?V H. eval (inst p [x ↦ r]) σ)" 
      using ‹vars p ⊆ insert x ?V› ‹x ∉ set (map fst rm)›
      by (auto simp add: eval_sum_inst_commute)
    ultimately
    show ?thesis using IH ‹distinct (map fst rm)› ‹H ≠ {}› 
      by (simp add: honest_prover_def)
  qed
  ultimately show ?case using 2(2-3,5)
    by (simp add: honest_prover_def honest_prover_vars honest_prover_deg)
qed


corollary completeness:  
  assumes 
    ‹(H, p, v) ∈ Sumcheck›
    ‹vars p = set (map fst rm)›   
    ‹distinct (map fst rm)›
    ‹H ≠ {}›
  shows 
    "sumcheck honest_prover u (H, p, v) r rm"
  using assms
  by (auto simp add: Sumcheck_def intro: completeness_inductive)

end

end