Theory KZG_def

theory KZG_def

imports Polynomial_Commitment_Schemes Primitives
begin

text ‹In this theory we formalize the KZG polynomial commitment scheme as introduced in Kate,
Zaverucha, and Goldberg's ``Constant-Size Commitments to Polynomials and Their Applications''
\<^cite>‹KZG10›.›

section ‹KZG function definitions›

text ‹Define the KZG with functions that match the abstract polynomial commitment scheme and 
instantiate the KZG as a polynomial commitment scheme.›

locale KZG = math_primitives
begin

type_synonym trapdoor = unit
type_synonym 'a' ck = "'a' list"
type_synonym 'a' vk = "'a' list"
type_synonym 'a' commit = "'a'"
type_synonym 'e' argument = "'e' mod_ring"
type_synonym 'e' evaluation = "'e' mod_ring"
type_synonym 'a' witness = "'a'"

subsection ‹Setup›

text ‹We do not compute the Groups for the bilinear pairing but assume them and compute 
a uniformly random secret key ‹α› and from that the structured reference string (srs)/public key 
‹PK = (g, g^α, ... , g^(α^t))›. Setup is a trusted Setup function, which generates the shared public 
key for both parties (prover and verifier).›
definition Setup :: "('e mod_ring × 'a list) spmf"
where 
  "Setup = do {
    x :: nat ← sample_uniform (order G⇩p);
    let α::'e mod_ring = of_int_mod_ring (int x) in
    return_spmf (α, map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1]) 
  }"

text‹This function computes ‹g^φ(α)›, given the by Setup generated public key. 
(‹α› being the from Setup generated private key)

The function is basically a Prod of ‹public key!i ^ coeff φ i›, which computes ‹g^φ(a)›, given the 
public key:
‹∏[0...degree φ]. PK!i^coeff φ i› 
= ‹∏[0...degree φ]. g^(α^i)^coeff φ i›
= ‹∏[0...degree φ]. g^(coeff φ i * α^i)›
= ‹g^(∑[0...degree φ]. coeff φ i * α^i)›
= ‹g^φ(α)›
›
fun g_pow_PK_Prod :: "'a list ⇒'e mod_ring poly ⇒ 'a" where
  "g_pow_PK_Prod PK φ = fold (λi acc. acc ⊗⇘G⇩p⇙ PK!i ^⇘G⇩p⇙ (poly.coeff φ i)) [0..<Suc (degree φ)] 𝟭⇘G⇩p⇙"

text ‹q\_coeffs is a accumulator for the fold function.
fold coeffs\_n creates a vertical summation by going through the power\_diff\_sumr2 and instead of 
adding the horizontal row, mapping it into a list, which is added onto the previous list of 
coefficients, hence summing the coefficients vertical in a list. Illustration:

0: [0                     ]  
=> map (+)
1: [f1                    ]
=> map(+)
2: [f1 + f2*u             , f2*x        ] 
=> map(+)
3: [f1 + f2*u + f3*u\textasciicircum{}2    , f2*x+f3*u*x , f3*x\textasciicircum{}2]
...
n: [f1 + ... + fn*u\textasciicircum{}(n-1) , ... , f(i-1)*x\textasciicircum{}i +...+fn*u\textasciicircum{}((n-1)-i)*x\textasciicircum{}i , ... , fn*x\textasciicircum{}(n-1)]

Hence the resulting list represents the vertical sum with coefficient i at position (i-1).
The correctness proof is to be found in the correctness theory KZG\_correct.
›
definition coeffs_n :: "'e mod_ring poly ⇒ 'e mod_ring ⇒ 'e mod_ring list ⇒ nat ⇒ 'e mod_ring list"
  where "coeffs_n φ u = (λq_coeffs. λn. map (λ(i::nat). (nth_default 0 q_coeffs i + poly.coeff φ n * u ^ (n - Suc i))) [0..<n])"

text ‹The objective of this function is to extract ‹ψ› in ‹φ x - φ u = (x-u) * ψ x›
Idea:
the polynomial ‹φ› can be represented as a sum, hence:
‹φ x - φ u›
= ‹(∑i≤degree φ. coeff φ i * x^i) - (∑i≤degree φ. coeff φ i * x^i)›
= ‹(x-u)(∑i≤degree φ. coeff φ i * (∑j<i. u^(i - Suc j)*x^j))›
(for the last step see the lemma power\_diff\_sumr2)
Hence: ‹ψ x = (∑i≤degree φ. coeff φ i * (∑j<i. u^(i - Suc j)*x^j))›
However, to build a polynomial ‹ψ› in Isabelle, we need the individual coefficients for every power 
of x (i.e. bring the sum into a form of ‹(∑i≤degree φ. coeff_i*x^i)› where coeff\_i is the individual
coefficients for every power i of x. This translation is the main-purpose of the extractor function. 
The key idea is reordering the summation obtained from the power\_diff\_sumr2 lemma:

One can imagine the summation of power\_diff\_sumr2 to be horizontal, in the sense that it computes 
the coefficients from 0 to degree ‹φ› = n, and adds (or could add) to each coefficient in every iteration:
0: 0 +
1: f1 +
2: f2*u + f2*x +
3: f3*u\textasciicircum{}2 + f3*u*x + f3*x\textasciicircum{}2
...
n: fn*u\textasciicircum{}(n-1) + ... fn*u\textasciicircum{}((n-1)-i)*x\textasciicircum{}i ...  + fn*x\textasciicircum{}(n-1)
we order it to compute the coefficients one by one (to compute vertical)
1: 0 + f1          + ... + fn*u\textasciicircum{}(n-1)         +
2: 0 + f2 * x      + ... + fn*u\textasciicircum{}((n-1)-1) * x +
...
n: 0 + fn * x\textasciicircum{}(n-1)

In formulas:
‹(∑i≤degree φ. coeff φ i * (∑j<i. u^(i - Suc j)*x^j))› =
‹(∑i≤degree φ. (∑j∈{i<..<Suc (degree φ)}. coeff φ j * u^(j-Suc i)) * x^i)›
›
definition ψ_of :: "'e mod_ring poly ⇒ 'e mod_ring ⇒ 'e mod_ring poly" 
  where "ψ_of φ u = (let 
     ψ_coeffs = foldl (coeffs_n φ u) [] [0..<Suc (degree φ)] ―‹coefficients of ‹ψ››
    in Poly ψ_coeffs) ―‹‹ψ››"

text ‹a wrapper around Setup that hands the srs to both parties›
definition key_gen :: "('a ck × 'a vk) spmf"
  where "key_gen =  do {
    (α, PK) ← Setup;
    return_spmf (PK,PK) 
  }"

text ‹the KZG functions follow the description in section 3.2 of the KZG paper, but mirror the 
structure and naming of the abstract polynomial commitment scheme.›

definition commit :: "'a ck ⇒ 'e mod_ring poly ⇒ ('a commit × trapdoor) spmf"
  where "commit PK φ = return_spmf (g_pow_PK_Prod PK φ, ()) ―‹‹g^φ(α)››"

definition verify_poly :: "'a vk ⇒ 'e mod_ring poly ⇒ 'a commit ⇒ trapdoor ⇒ bool"
  where "verify_poly PK φ C td = (C = g_pow_PK_Prod PK φ)  ―‹‹C = g^φ(α)››"

text ‹This is the createWitness function in the KZG paper›
definition Eval :: "'a ck ⇒ trapdoor ⇒ 'e mod_ring poly ⇒ 'e mod_ring ⇒ ('e mod_ring × 'a witness)"
  where "Eval PK td φ i = (let ψ = ψ_of φ i ―‹‹ψ› in ‹φ(x) - φ(i) = (x-i) * ψ(x)››
    in (poly φ i, g_pow_PK_Prod PK ψ) ―‹‹(φ(i),g^ψ(α))››)"

definition verify_eval :: "'a vk ⇒ 'a commit ⇒ 'e mod_ring ⇒ ('e mod_ring × 'a witness) ⇒ bool"
  where "verify_eval PK C i val = (let (eval,w) = val 
  in  (e w (PK!1  ÷⇘G⇩p⇙ (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ i)) ⊗⇘G⇩T⇙ ((e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙) ^⇘G⇩T⇙ eval) = e C ❙g⇘G⇩p⇙)) 
    ―‹‹e(g^ψ(α), g^α / g^i) ⊗ e(g,g)^φ(i) = e(C, g)››"

definition valid_poly::"'e mod_ring poly ⇒ bool"
  where "valid_poly φ = (degree φ ≤ max_deg)"

definition valid_argument :: "'e argument ⇒ bool"
  where "valid_argument _ = True"

definition valid_eval::"('e mod_ring × 'a witness) ⇒ bool"
  where "valid_eval val = (let (_,w) = val in w ∈ carrier G⇩p)"

text ‹the KZG is a polynomial commitment scheme›
sublocale abstract_polynomial_commitment_scheme key_gen commit verify_poly Eval verify_eval 
  valid_poly valid_argument valid_eval .

end

end