halo2_axiom/poly/ipa/commitment/
verifier.rs

Help
1use group::ff::{BatchInvert, Field};
2
3use super::ParamsIPA;
4use crate::{arithmetic::CurveAffine, poly::ipa::strategy::GuardIPA};
5use crate::{
6    poly::{commitment::MSM, ipa::msm::MSMIPA, Error},
7    transcript::{EncodedChallenge, TranscriptRead},
8};
9
10/// Checks to see if the proof represented within `transcript` is valid, and a
11/// point `x` that the polynomial commitment `P` opens purportedly to the value
12/// `v`. The provided `msm` should evaluate to the commitment `P` being opened.
13pub fn verify_proof<'params, C: CurveAffine, E: EncodedChallenge<C>, T: TranscriptRead<C, E>>(
14    params: &'params ParamsIPA<C>,
15    mut msm: MSMIPA<'params, C>,
16    transcript: &mut T,
17    x: C::Scalar,
18    v: C::Scalar,
19) -> Result<GuardIPA<'params, C>, Error> {
20    let k = params.k as usize;
21
22    // P' = P - [v] G_0 + [ξ] S
23    msm.add_constant_term(-v); // add [-v] G_0
24    let s_poly_commitment = transcript.read_point().map_err(|_| Error::OpeningError)?;
25    let xi = *transcript.squeeze_challenge_scalar::<()>();
26    msm.append_term(xi, s_poly_commitment.into());
27
28    let z = *transcript.squeeze_challenge_scalar::<()>();
29
30    let mut rounds = vec![];
31    for _ in 0..k {
32        // Read L and R from the proof and write them to the transcript
33        let l = transcript.read_point().map_err(|_| Error::OpeningError)?;
34        let r = transcript.read_point().map_err(|_| Error::OpeningError)?;
35
36        let u_j_packed = transcript.squeeze_challenge();
37        let u_j = *u_j_packed.as_challenge_scalar::<()>();
38
39        rounds.push((l, r, u_j, /* to be inverted */ u_j, u_j_packed));
40    }
41
42    rounds
43        .iter_mut()
44        .map(|&mut (_, _, _, ref mut u_j, _)| u_j)
45        .batch_invert();
46
47    // This is the left-hand side of the verifier equation.
48    // P' + \sum([u_j^{-1}] L_j) + \sum([u_j] R_j)
49    let mut u = Vec::with_capacity(k);
50    let mut u_packed: Vec<C::Scalar> = Vec::with_capacity(k);
51    for (l, r, u_j, u_j_inv, u_j_packed) in rounds {
52        msm.append_term(u_j_inv, l.into());
53        msm.append_term(u_j, r.into());
54
55        u.push(u_j);
56        u_packed.push(u_j_packed.get_scalar());
57    }
58
59    // Our goal is to check that the left hand side of the verifier
60    // equation
61    //     P' + \sum([u_j^{-1}] L_j) + \sum([u_j] R_j)
62    // equals (given b = \mathbf{b}_0, and the prover's values c, f),
63    // the right-hand side
64    //   = [c] (G'_0 + [b * z] U) + [f] W
65    // Subtracting the right-hand side from both sides we get
66    //   P' + \sum([u_j^{-1}] L_j) + \sum([u_j] R_j)
67    //   + [-c] G'_0 + [-cbz] U + [-f] W
68    //   = 0
69    //
70    // Note that the guard returned from this function does not include
71    // the [-c]G'_0 term.
72
73    let c = transcript.read_scalar().map_err(|_| Error::SamplingError)?;
74    let neg_c = -c;
75    let f = transcript.read_scalar().map_err(|_| Error::SamplingError)?;
76    let b = compute_b(x, &u);
77
78    msm.add_to_u_scalar(neg_c * &b * &z);
79    msm.add_to_w_scalar(-f);
80
81    let guard = GuardIPA {
82        msm,
83        neg_c,
84        u,
85        u_packed,
86    };
87
88    Ok(guard)
89}
90
91/// Computes $\prod\limits_{i=0}^{k-1} (1 + u_{k - 1 - i} x^{2^i})$.
92fn compute_b<F: Field>(x: F, u: &[F]) -> F {
93    let mut tmp = F::ONE;
94    let mut cur = x;
95    for u_j in u.iter().rev() {
96        tmp *= F::ONE + &(*u_j * &cur);
97        cur *= cur;
98    }
99    tmp
100}
halo2_axiom/poly/ipa/commitment/verifier.rs

halo2_axiom/poly/ipa/commitment/
verifier.rs
