Theory Polynomial_Commitment_Schemes

theory Polynomial_Commitment_Schemes 
  imports CryptHOL.CryptHOL "HOL-Computational_Algebra.Polynomial" 
    Sigma_Commit_Crypto.Commitment_Schemes
begin

section ‹Polynomial Commitment Schemes›

text ‹This theory captures the notion of Polynomial Commitment Schemes, introduced in
Kate, Zaverucha, and Goldberg's ``Constant-Size Commitments to Polynomials and Their
Applications'' \<^cite>‹KZG10›.

The formalization differs slightly from the early notion of Kate, Zaverucha, and Goldberg, as it
aims to capture, and also draws from, newer approaches to polynomial commitment schemes. 
Examples are WHIR \<^cite>‹WHIR›, BaseFold \<^cite>‹BaseFold›,
Binius \<^cite>‹Binius›, and Dory \<^cite>‹Dory›.

Additionally, the formalization is formulated even more general to be able to capture batching 
schemes as well, which were already introduced by Kate, Zaverucha, and Goldberg.
›

locale abstract_polynomial_commitment_scheme =
  fixes key_gen :: "('ck × 'vk) spmf" ― ‹outputs the keys received by the two parties›
    and commit :: "'ck ⇒ 'r::comm_monoid_add poly  ⇒ ('commit × 'trapdoor) spmf" 
      ― ‹outputs the commitment as well as the secret, which might be used to derive witnesses, 
         and the opening values sent by the committer in the reveal phase›    
    and verify_poly :: "'vk ⇒ 'r poly ⇒ 'commit ⇒ 'trapdoor ⇒ bool"       
      ― ‹checks whether the polynomial corresponds to the commitment›
    and eval :: "'ck ⇒ 'trapdoor ⇒ 'r poly ⇒ 'argument ⇒ ('evaluation × 'witness)"
      ― ‹outputs a point and a witness›
    and verify_eval :: "'vk ⇒ 'commit ⇒ 'argument ⇒ ('evaluation × 'witness) ⇒ bool"
      ― ‹checks whether the point is on the polynomial corresponding to the commitment›
    and valid_poly :: "'r poly ⇒ bool" ― ‹checks whether a polynomial is a valid message e.g. it's 
        degree is bounded›
    and valid_argument :: "'argument ⇒ bool" ― ‹checks whether an argument is a valid message 
      e.g. set size in a batched version›
    and valid_eval :: "('evaluation × 'witness) ⇒ bool" ― ‹checks whether an evaluation is a valid
       message e.g. a valid group element›
begin

text ‹A polynomial commitment scheme is an extension of a standard commitment scheme. 
We reuse the work by Butler, Lochbihler, Aspinall and Gasc\'on, who already formalized commitment
schemes \<^cite>‹BLAG19›.›
sublocale cs: abstract_commitment key_gen commit verify_poly valid_poly .

definition correct_cs_game :: "'r poly ⇒ bool spmf"
  where "correct_cs_game ≡ cs.correct_game"

definition correct_cs 
  where "correct_cs ≡ cs.correct"

text ‹This game captures the correctness property of eval i.e. the results of eval will always 
verify.›
definition correct_eval_game :: "'r poly ⇒ 'argument ⇒ bool spmf"
  where "correct_eval_game p i = do {
  (ck, vk) ← key_gen;
  (c,d) ← commit ck p;
  let w  = eval ck d p i;
  return_spmf (verify_eval vk c i w)
  }"

lemma lossless_correct_eval_game: "⟦lossless_spmf key_gen;
          ⋀ck p. valid_msg p ⟹ lossless_spmf (commit ck p)⟧
              ⟹ valid_msg p ⟹ lossless_spmf (correct_eval_game p i)"  
  by (simp add: correct_eval_game_def split_def Let_def)

text ‹captures the  perfect correctness property of eval›
definition correct_eval
  where "correct_eval ≡ (∀p i. valid_poly p ⟶ valid_argument i ⟶ spmf (correct_eval_game p i) True = 1)"

text ‹We again reuse the previous work on commitment schemes›
definition poly_bind_game
  where "poly_bind_game ≡ cs.bind_game"

definition poly_bind_advantage
  where "poly_bind_advantage ≡ cs.bind_advantage"

type_synonym ('ck', 'commit', 'argument', 'evaluation', 'witness')  eval_bind_adversary = 
  "'ck' ⇒ ('commit' × 'argument'  × 'evaluation' × 'witness'  × 'evaluation' × 'witness') spmf"

text ‹captures the evaluation binding game i.e. verifying two contradicting evaluations (‹p(i) ≠ p(i)'›).›
definition eval_bind_game :: "('ck, 'commit, 'argument, 'evaluation, 'witness) eval_bind_adversary ⇒ bool spmf"
  where "eval_bind_game 𝒜 = TRY do {
  (ck, vk) ← key_gen;
  (c, i, v, w, v', w') ← 𝒜 ck;
  _ :: unit ← assert_spmf (v ≠ v' ∧ valid_argument i ∧ valid_eval (v, w) ∧ valid_eval (v', w'));                     
  let b = verify_eval vk c i (v,w);
  let b' = verify_eval vk c i (v',w');
  return_spmf (b ∧ b')} ELSE return_spmf False"

text ‹We capture the advantage of an adversary over winning the evaluation binding game. This has to 
be negligible for evaluation binding to hold.›
definition eval_bind_advantage :: "('ck, 'commit, 'argument, 'evaluation, 'witness) eval_bind_adversary ⇒ real"
  where "eval_bind_advantage 𝒜 ≡ spmf (eval_bind_game 𝒜) True"

type_synonym ('vk', 'argument','state')  eval_hiding_adversary1 = 
  "'vk' ⇒  ('argument' list × 'state') spmf"

type_synonym ('r', 'vk', 'commit', 'argument', 'evaluation', 'witness', 'state')  eval_hiding_adversary2 = 
  "('vk' ⇒ 'state' ⇒ 'commit' ⇒ 'argument' list ⇒ ('evaluation' × 'witness') list ⇒ ('r' poly) spmf)"

text ‹captures the hiding property of the Commit and Eval functions in combination.
Note, this property deviates from the typical indistinguishability games for hiding in general.
Kate, Zaverucha, and Goldberg introduced this notion in their work. ›
definition eval_hiding_game :: "'r poly ⇒ ('vk, 'argument,'state) eval_hiding_adversary1 ⇒ 
  ('r, 'vk, 'commit, 'argument, 'evaluation, 'witness, 'state) eval_hiding_adversary2 ⇒ bool spmf"
  where "eval_hiding_game p 𝒜1 𝒜2 = TRY do {
  (ck, vk) ← key_gen;
  (I,σ) ← 𝒜1 vk;
  (c,d) ← commit ck p;
  let W = map (λi. eval ck d p i) I; 
  p' ← 𝒜2 vk σ c I W;
  return_spmf (p = p')} ELSE return_spmf False"

text ‹We capture the advantage of an adversary over winning the hiding game. This has to be 
negligible for hiding to hold.›
definition eval_hiding_advantage :: "'r poly ⇒ ('vk, 'argument,'state) eval_hiding_adversary1 ⇒ 
  ('r, 'vk, 'commit, 'argument, 'evaluation, 'witness, 'state) eval_hiding_adversary2 ⇒ real"
  where "eval_hiding_advantage p 𝒜1 𝒜2 ≡ spmf (eval_hiding_game p 𝒜1 𝒜2) True"

type_synonym ('ck', 'commit', 'state') knowledge_soundness_adversary1 = "'ck' ⇒ ('commit' × 'state') spmf"

type_synonym ('state', 'ck', 'argument', 'evaluation', 'witness') knowledge_soundness_adversary2 
  = "'ck' ⇒ 'state' ⇒ ('argument' × ('evaluation' × 'witness')) spmf"

type_synonym ('r', 'commit', 'trapdoor') extractor = "'commit' ⇒ ('r' poly × 'trapdoor') spmf"

text ‹captures intuitively the fact that an adversary has to have knowledge of a polynomial in order
to create an evaluation that verifies.    
This property is typically required for succinct non-interactive arguments of knowledge 
(SNARKs) built from polynomial commitment schemes, e.g.\ PLONK \<^cite>‹PLONK›,
Marlin \<^cite>‹Marlin›, and Binius \<^cite>‹Binius›.›
definition knowledge_soundness_game :: "('ck, 'commit, 'state) knowledge_soundness_adversary1 
  ⇒ ('state, 'ck, 'argument, 'evaluation, 'witness) knowledge_soundness_adversary2 
  ⇒ ('r, 'commit, 'trapdoor) extractor ⇒ bool spmf"
  where "knowledge_soundness_game 𝒜1 𝒜2 E = TRY do {
  (ck,vk) ← key_gen;
  (c,σ) ← 𝒜1 ck;
  (p,d) ← E c;
  (i, (p_i,π)) ← 𝒜2 ck σ;
  let w = (p_i, π);
  let (p_i',_) = eval ck d p i;         
  return_spmf (verify_eval vk c i w ∧ p_i ≠ p_i' ∧ valid_argument i ∧ valid_eval w)       
  } ELSE return_spmf False"

text ‹We capture the advantage of an adversary over winning the knowledge soundness game. This has to
be negligible for knowledge soundness to hold.›
definition knowledge_soundness_advantage :: " ('ck, 'commit, 'state) knowledge_soundness_adversary1 
  ⇒ ('state, 'ck, 'argument, 'evaluation, 'witness) knowledge_soundness_adversary2  
  ⇒ ('r, 'commit, 'trapdoor) extractor ⇒ real"
  where "knowledge_soundness_advantage 𝒜1 𝒜2 E ≡ spmf (knowledge_soundness_game 𝒜1 𝒜2 E) True"

end

end