fullcodec_plonk/proof_system/widget/lookup/
proverkey.rs

1// This Source Code Form is subject to the terms of the Mozilla Public
2// License, v. 2.0. If a copy of the MPL was not distributed with this
3// file, You can obtain one at http://mozilla.org/MPL/2.0/.
4//
5// Copyright (c) DUSK NETWORK. All rights reserved.
6
7use super::compress;
8use crate::fft::{Evaluations, Polynomial};
9use crate::plonkup::MultiSet;
10
11use dusk_bls12_381::BlsScalar;
12
13#[derive(Debug, Eq, PartialEq, Clone)]
14pub struct ProverKey {
15    pub(crate) q_lookup: (Polynomial, Evaluations),
16    pub(crate) table_1: (MultiSet, Polynomial, Evaluations),
17    pub(crate) table_2: (MultiSet, Polynomial, Evaluations),
18    pub(crate) table_3: (MultiSet, Polynomial, Evaluations),
19    pub(crate) table_4: (MultiSet, Polynomial, Evaluations),
20}
21
22impl ProverKey {
23    /// Compute identity check for lookup gates
24    pub(crate) fn compute_quotient_i(
25        &self,
26        index: usize,
27        lookup_separation_challenge: &BlsScalar,
28        w_l_i: &BlsScalar,
29        w_r_i: &BlsScalar,
30        w_o_i: &BlsScalar,
31        w_4_i: &BlsScalar,
32        f_i: &BlsScalar,
33        p_i: &BlsScalar,
34        p_i_next: &BlsScalar,
35        t_i: &BlsScalar,
36        t_i_next: &BlsScalar,
37        h_1_i: &BlsScalar,
38        h_1_i_next: &BlsScalar,
39        h_2_i: &BlsScalar,
40        l_first_i: &BlsScalar,
41        (delta, epsilon): (&BlsScalar, &BlsScalar),
42        zeta: &BlsScalar,
43    ) -> BlsScalar {
44        let l_sep_2 = lookup_separation_challenge.square();
45        let l_sep_3 = l_sep_2 * lookup_separation_challenge;
46
47        let one_plus_delta = delta + BlsScalar::one();
48        let epsilon_one_plus_delta = epsilon * one_plus_delta;
49
50        // q_lookup(X) * (a(X) + zeta * b(X) + (zeta^2 * c(X)) + (zeta^3 * d(X)
51        // - f(X))) * α_1
52        let a = {
53            let q_lookup_i = self.q_lookup.1[index];
54            let compressed_tuple =
55                compress(*w_l_i, *w_r_i, *w_o_i, *w_4_i, *zeta);
56
57            q_lookup_i * (compressed_tuple - f_i) * lookup_separation_challenge
58        };
59
60        // L0(X) * (p(X) − 1) * α_1^2
61        let b = { l_first_i * (p_i - BlsScalar::one()) * l_sep_2 };
62
63        // p(X) * (1+δ) * (ε+f(X)) * (ε*(1+δ) + t(X) + δt(Xω)) * α_1^3
64        let c = {
65            let c_1 = epsilon + f_i;
66            let c_2 = epsilon_one_plus_delta + t_i + delta * t_i_next;
67
68            p_i * one_plus_delta * c_1 * c_2 * l_sep_3
69        };
70
71        // − p(Xω) * (ε*(1+δ) + h1(X) + δ*h2(X)) * (ε*(1+δ) + h2(X) + δ*h1(Xω))
72        // * α_1^3
73        let d = {
74            let d_1 = epsilon_one_plus_delta + h_1_i + delta * h_2_i;
75            let d_2 = epsilon_one_plus_delta + h_2_i + delta * h_1_i_next;
76
77            -p_i_next * d_1 * d_2 * l_sep_3
78        };
79
80        a + b + c + d
81    }
82
83    /// Compute linearisation for lookup gates
84    pub(crate) fn compute_linearisation(
85        &self,
86        a_eval: &BlsScalar,
87        b_eval: &BlsScalar,
88        c_eval: &BlsScalar,
89        d_eval: &BlsScalar,
90        f_eval: &BlsScalar,
91        t_eval: &BlsScalar,
92        t_next_eval: &BlsScalar,
93        h_1_eval: &BlsScalar,
94        h_2_eval: &BlsScalar,
95        p_next_eval: &BlsScalar,
96        l1_eval: &BlsScalar,
97        p_poly: &Polynomial,
98        h_2_poly: &Polynomial,
99        (delta, epsilon): (&BlsScalar, &BlsScalar),
100        zeta: &BlsScalar,
101        lookup_separation_challenge: &BlsScalar,
102    ) -> Polynomial {
103        let l_sep_2 = lookup_separation_challenge.square();
104        let l_sep_3 = l_sep_2 * lookup_separation_challenge;
105        let zeta_sq = zeta * zeta;
106        let zeta_cu = zeta * zeta_sq;
107        let one_plus_delta = delta + BlsScalar::one();
108        let epsilon_one_plus_delta = epsilon * one_plus_delta;
109
110        //
111        // - q_lookup(X) * f_eval * lookup_separation_challenge
112        let a = {
113            let a_0 =
114                a_eval + zeta * b_eval + zeta_sq * c_eval + zeta_cu * d_eval;
115
116            &self.q_lookup.0 * &((a_0 - f_eval) * lookup_separation_challenge)
117        };
118
119        // p(X) * L0(z) * α_1^2
120        let b = { p_poly * &(l1_eval * l_sep_2) };
121
122        // p(X) * (1 + δ) * (ε + f_bar) * (ε(1+δ) + t_bar + δ*tω_bar) * α_1^3
123        let c = {
124            let c_0 = epsilon + f_eval;
125            let c_1 = epsilon_one_plus_delta + t_eval + delta * t_next_eval;
126
127            p_poly * &(one_plus_delta * c_0 * c_1 * l_sep_3)
128        };
129
130        // − pω_bar * (ε(1+δ) + h1_bar + δh2_bar) * h2(X) * α_1^3
131        let d = {
132            let d_0 = epsilon_one_plus_delta + h_1_eval + delta * h_2_eval;
133
134            h_2_poly * &(-p_next_eval * d_0 * l_sep_3)
135        };
136
137        let mut r = a;
138        r += &b;
139        r += &c;
140        r += &d;
141
142        r
143    }
144}