Theory Public_Coin_Proofs

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

  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 ‹Generic Public-coin Interactive Proofs›

theory Public_Coin_Proofs
  imports Probability_Tools 
begin

subsection ‹Generic definition›

type_synonym ('i, 'r, 'a, 'resp, 'ps) prv = "'i ⇒ 'a ⇒ 'a list ⇒ 'r ⇒ 'ps ⇒ 'resp × 'ps" 

locale public_coin_proof =
  fixes ver0 :: "'i ⇒ 'vs ⇒ bool"
    and ver1 :: "'i ⇒ 'resp ⇒ 'r ⇒ 'a ⇒ 'a list ⇒ 'vs ⇒ bool × 'i × 'vs"
begin

fun prove :: "'vs ⇒ ('i, 'r, 'a, 'resp, 'ps) prv ⇒ 'ps ⇒ 'i ⇒ 'r ⇒ ('a × 'r) list ⇒ bool" where
  "prove vs prv ps I r [] ⟷ ver0 I vs" |
  "prove vs prv ps I r ((x, r')#rm) ⟷ 
     (let (resp, ps') = prv I x (map fst rm) r ps in 
      let (ok, I', vs') = ver1 I resp r' x (map fst rm) vs in 
        ok ∧ prove vs' prv ps' I' r' rm)"

text ‹
The parameters are
\begin{itemize}
\item @{term "(ver0, ver1)"} and @{term "vs"} are the verifier and its current state,
\item @{term "prv"} and @{term "ps"} are the prover and its current state,
\item @{term "I ∈ S"} is the problem instance,
\item @{term "r"} is the verifier's randomness for the current round.
\item @{term "rs"} is the (list of) randomness for the remaining rounds, and
\item @{term "xs"} is a list of public per-round information/
\end{itemize}
We assume that @{term "rs"} and @{term "xs"} have the same length.
›

end


subsection ‹Generic soundness and completeness›

locale public_coin_proof_security = 
  public_coin_proof ver0 ver1
  for ver0 :: "'i ⇒ 'vs ⇒ bool" 
  and ver1 :: "'i ⇒ 'resp ⇒ 'r ⇒ 'a ⇒ 'a list ⇒ 'vs ⇒ bool × 'i × 'vs" + 
  fixes S :: "'i set"            ― ‹problem specification›
    and honest_pr :: "('i, 'r, 'a, 'resp, 'ps) prv"
    and compl_err :: "'i ⇒ real"
    and sound_err :: "'i ⇒ real"
    and compl_assm :: "'vs ⇒ 'ps ⇒ 'i ⇒ 'a list ⇒ bool"
    and sound_assm :: "'vs ⇒ 'ps ⇒ 'i ⇒ 'a list ⇒ bool"
  assumes
    completeness:  
       "⟦ I ∈ S; compl_assm vs ps I xs ⟧ ⟹
          measure_pmf.prob 
            (pmf_of_set (tuples UNIV (length xs)))
            {rs. prove vs honest_pr ps I r (zip xs rs)} ≥ 1 - compl_err I" and

    soundness:
       "⟦ I ∉ S; sound_assm vs ps I xs ⟧ ⟹ 
          measure_pmf.prob 
            (pmf_of_set (tuples UNIV (length xs)))
            {rs. prove vs pr ps I r (zip xs rs)} ≤ sound_err I" 


locale public_coin_proof_strong_props = 
  public_coin_proof ver0 ver1 
  for ver0 :: "'i ⇒ 'vs ⇒ bool" 
  and ver1 :: "'i ⇒ 'resp ⇒ 'r::finite ⇒ 'a ⇒ 'a list ⇒ 'vs ⇒ bool × 'i × 'vs" + 
  fixes S :: "'i set"            ― ‹problem specification›
    and honest_pr :: "('i, 'r, 'a, 'resp, 'ps) prv"
    and sound_err :: "'i ⇒ real"
    and compl_assm :: "'vs ⇒ 'ps ⇒ 'i ⇒ 'a list ⇒ bool"
    and sound_assm :: "'vs ⇒ 'ps ⇒ 'i ⇒ 'a list ⇒ bool"
  assumes
    completeness:  
       "⟦ I ∈ S; compl_assm vs ps I (map fst rm) ⟧ ⟹ prove vs honest_pr ps I r rm" and

    soundness:
       "⟦ I ∉ S; sound_assm vs ps I xs ⟧ ⟹ 
          measure_pmf.prob 
            (pmf_of_set (tuples UNIV (length xs)))
            {rs. prove vs pr ps I r (zip xs rs)} ≤ sound_err I" 
begin


text ‹Show that this locale satisfies the weaker assumptions of @{locale public_coin_proof_security}.›

sublocale pc_props: 
  public_coin_proof_security ver0 ver1 S honest_pr "λ_. 0" sound_err compl_assm sound_assm
  by (unfold_locales)
     (fastforce simp add: prob_pmf_of_set_geq_1 tuples_Suc completeness, 
      clarsimp simp add: soundness)

end


end