arrabbiata/
setup.rs

1//! This module defines methods and structures for setting up the circuit, or in
2//! a more theoretical language, the "NP relation" that the circuit will be
3//! related to.
4//! Note that when mentioning "circuit" in this context, we are referring to
5//! a specific user application in addition to the circuit used to encode the
6//! verifier.
7//!
8//! The setup phase defines the constraints that the computation/the app must
9//! satisfy, the evaluation domains, and the SRS for the polynomial commitment
10//! scheme. Generally, the setup phase is an agreement between the prover and
11//! the verifier on the language and the protocol parameters (cryptographic
12//! primitives, security level, etc). The setup phase will also contain some
13//! pre-computed values to ease both the prover's and the verifier's work.
14//!
15//! As part of the setup phase, the parties will also agree on a set of
16//! predefined values that will shape the selectors and the computation.
17//!
18//! A prover will be providing a proof of a particular [IndexedRelation] created
19//! during the setup phase, by encapsulating a value of this type in its
20//! [crate::witness::Env] structure. The prover will then refer to the values
21//! saved in the type [IndexedRelation].
22//!
23//! On the other side, a verifier will be instantiated with the relevant indexed
24//! relation.
25//!
26use ark_ff::PrimeField;
27use kimchi::circuits::domains::EvaluationDomains;
28use log::{debug, info};
29use mina_poseidon::constants::SpongeConstants;
30use mvpoly::{monomials::Sparse, MVPoly};
31use num_bigint::{BigInt, BigUint};
32use num_integer::Integer;
33use o1_utils::FieldHelpers;
34use poly_commitment::{ipa::SRS, PolyComm, SRS as _};
35use std::{collections::HashMap, time::Instant};
36
37use crate::{
38    column::Gadget,
39    constraint,
40    curve::{ArrabbiataCurve, PlonkSpongeConstants},
41    interpreter::{self, VERIFIER_STARTING_INSTRUCTION},
42    MAXIMUM_FIELD_SIZE_IN_BITS, MAX_DEGREE, MV_POLYNOMIAL_ARITY, NUMBER_OF_COLUMNS,
43    NUMBER_OF_GADGETS, VERIFIER_CIRCUIT_SIZE,
44};
45
46/// An indexed relation is a structure that contains all the information needed
47/// describing a specialised sub-class of the NP relation. It includes some
48/// (protocol) parameters like the SRS, the evaluation domains, and the
49/// constraints describing the computation.
50///
51/// The prover will be instantiated for a particular indexed relation, and the
52/// verifier will be instantiated with (relatively) the same indexed relation.
53pub struct IndexedRelation<
54    Fp: PrimeField,
55    Fq: PrimeField,
56    E1: ArrabbiataCurve<ScalarField = Fp, BaseField = Fq>,
57    E2: ArrabbiataCurve<ScalarField = Fq, BaseField = Fp>,
58> where
59    E1::BaseField: PrimeField,
60    E2::BaseField: PrimeField,
61{
62    /// Domain for Fp
63    pub domain_fp: EvaluationDomains<E1::ScalarField>,
64
65    /// Domain for Fq
66    pub domain_fq: EvaluationDomains<E2::ScalarField>,
67
68    /// SRS for the first curve
69    pub srs_e1: SRS<E1>,
70
71    /// SRS for the second curve
72    pub srs_e2: SRS<E2>,
73
74    /// The application size, i.e. the number of rows per accumulation an
75    /// application can use.
76    ///
77    /// Note that the value is the same for both circuits. We do suppose both
78    /// SRS are of the same sizes and the verifier circuits are the same.
79    pub app_size: usize,
80
81    /// The description of the program, in terms of gadgets.
82    /// For now, the program is the same for both curves.
83    ///
84    /// The number of elements is exactly the size of the SRS.
85    pub circuit_gates: Vec<Gadget>,
86
87    /// Commitments to the selectors used by both circuits
88    pub selectors_comm: (
89        [PolyComm<E1>; NUMBER_OF_GADGETS],
90        [PolyComm<E2>; NUMBER_OF_GADGETS],
91    ),
92
93    /// The constraints given as multivariate polynomials using the [mvpoly]
94    /// library, indexed by the gadget to ease the selection of the constraints
95    /// while computing the cross-terms during the accumulation process.
96    ///
97    /// When the accumulation scheme is implemented, this structure will
98    /// probably be subject to changes as the SNARK used for the accumulation
99    /// scheme will probably work over expressions used in
100    /// [kimchi::circuits::expr]. We leave that for the future, and focus
101    /// on the accumulation scheme implementation.
102    ///
103    /// We keep two sets of constraints for the time being as we might want in
104    /// the future to have different circuits for one of the curves, as inspired
105    /// by [CycleFold](https://eprint.iacr.org/2023/1192).
106    /// In the current design, both circuits are the same and the prover will do
107    /// the same job over both curves.
108    pub constraints_fp: HashMap<Gadget, Vec<Sparse<Fp, { MV_POLYNOMIAL_ARITY }, { MAX_DEGREE }>>>,
109    pub constraints_fq: HashMap<Gadget, Vec<Sparse<Fq, { MV_POLYNOMIAL_ARITY }, { MAX_DEGREE }>>>,
110
111    /// Initial state of the sponge, containing circuit specific
112    /// information.
113    // FIXME: setup correctly with the initial transcript.
114    // The sponge must be initialized correctly with all the information
115    // related to the actual relation being accumulated/proved.
116    // Note that it must include the information of both circuits!
117    pub initial_sponge: [BigInt; PlonkSpongeConstants::SPONGE_WIDTH],
118}
119
120impl<
121        Fp: PrimeField,
122        Fq: PrimeField,
123        E1: ArrabbiataCurve<ScalarField = Fp, BaseField = Fq>,
124        E2: ArrabbiataCurve<ScalarField = Fq, BaseField = Fp>,
125    > IndexedRelation<Fp, Fq, E1, E2>
126where
127    E1::BaseField: PrimeField,
128    E2::BaseField: PrimeField,
129{
130    pub fn new(srs_log2_size: usize) -> Self {
131        assert!(E1::ScalarField::MODULUS_BIT_SIZE <= MAXIMUM_FIELD_SIZE_IN_BITS.try_into().unwrap(), "The size of the field Fp is too large, it should be less than {MAXIMUM_FIELD_SIZE_IN_BITS}");
132        assert!(Fq::MODULUS_BIT_SIZE <= MAXIMUM_FIELD_SIZE_IN_BITS.try_into().unwrap(), "The size of the field Fq is too large, it should be less than {MAXIMUM_FIELD_SIZE_IN_BITS}");
133        let modulus_fp = E1::ScalarField::modulus_biguint();
134        let alpha = PlonkSpongeConstants::PERM_SBOX;
135        assert!(
136            (modulus_fp - BigUint::from(1_u64)).gcd(&BigUint::from(alpha)) == BigUint::from(1_u64),
137            "The modulus of Fp should be coprime with {alpha}"
138        );
139        let modulus_fq = E2::ScalarField::modulus_biguint();
140        let alpha = PlonkSpongeConstants::PERM_SBOX;
141        assert!(
142            (modulus_fq - BigUint::from(1_u64)).gcd(&BigUint::from(alpha)) == BigUint::from(1_u64),
143            "The modulus of Fq should be coprime with {alpha}"
144        );
145
146        let srs_size = 1 << srs_log2_size;
147        let domain_fp = EvaluationDomains::<E1::ScalarField>::create(srs_size).unwrap();
148        let domain_fq = EvaluationDomains::<E2::ScalarField>::create(srs_size).unwrap();
149
150        info!("Create an SRS of size {srs_log2_size} for the first curve");
151        let srs_e1: SRS<E1> = {
152            let start = Instant::now();
153            let srs = SRS::create(srs_size);
154            debug!("SRS for E1 created in {:?}", start.elapsed());
155            let start = Instant::now();
156            srs.get_lagrange_basis(domain_fp.d1);
157            debug!("Lagrange basis for E1 added in {:?}", start.elapsed());
158            srs
159        };
160        info!("Create an SRS of size {srs_log2_size} for the second curve");
161        let srs_e2: SRS<E2> = {
162            let start = Instant::now();
163            let srs = SRS::create(srs_size);
164            debug!("SRS for E2 created in {:?}", start.elapsed());
165            let start = Instant::now();
166            srs.get_lagrange_basis(domain_fq.d1);
167            debug!("Lagrange basis for E2 added in {:?}", start.elapsed());
168            srs
169        };
170
171        let constraints_fp: HashMap<
172            Gadget,
173            Vec<Sparse<E1::ScalarField, { MV_POLYNOMIAL_ARITY }, { MAX_DEGREE }>>,
174        > = {
175            let env: constraint::Env<E1> = constraint::Env::new();
176            let constraints = env.get_all_constraints_indexed_by_gadget();
177            constraints
178                .into_iter()
179                .map(|(k, polynomials)| {
180                    (
181                        k,
182                        polynomials
183                            .into_iter()
184                            .map(|p| Sparse::from_expr(p, Some(NUMBER_OF_COLUMNS)))
185                            .collect(),
186                    )
187                })
188                .collect()
189        };
190
191        let constraints_fq: HashMap<
192            Gadget,
193            Vec<Sparse<E2::ScalarField, { MV_POLYNOMIAL_ARITY }, { MAX_DEGREE }>>,
194        > = {
195            let env: constraint::Env<E2> = constraint::Env::new();
196            let constraints = env.get_all_constraints_indexed_by_gadget();
197            constraints
198                .into_iter()
199                .map(|(k, polynomials)| {
200                    (
201                        k,
202                        polynomials
203                            .into_iter()
204                            .map(|p| Sparse::from_expr(p, Some(NUMBER_OF_COLUMNS)))
205                            .collect(),
206                    )
207                })
208                .collect()
209        };
210
211        // FIXME: note that the app size can be different for both curves. We
212        // suppose we have the same circuit on both curves for now.
213        let app_size = srs_size - VERIFIER_CIRCUIT_SIZE;
214
215        // Build the selectors for both circuits.
216        // FIXME: we suppose we have the same circuit on both curve for now.
217        let circuit_gates: Vec<Gadget> = {
218            let mut v: Vec<Gadget> = Vec::with_capacity(srs_size);
219            // The first [app_size] rows are for the application
220            v.extend([Gadget::App].repeat(app_size));
221
222            // Verifier circuit structure
223            {
224                let mut curr_instruction = VERIFIER_STARTING_INSTRUCTION;
225                for _i in 0..VERIFIER_CIRCUIT_SIZE - 1 {
226                    v.push(Gadget::from(curr_instruction));
227                    curr_instruction = interpreter::fetch_next_instruction(curr_instruction);
228                }
229                // Additional row for the Poseidon hash
230                v.push(Gadget::NoOp);
231            }
232            assert_eq!(v.len(), srs_size);
233            v
234        };
235
236        let selectors_comm: (
237            [PolyComm<E1>; NUMBER_OF_GADGETS],
238            [PolyComm<E2>; NUMBER_OF_GADGETS],
239        ) = {
240            // We initialize to the blinder to avoid the identity element.
241            let init: (
242                [PolyComm<E1>; NUMBER_OF_GADGETS],
243                [PolyComm<E2>; NUMBER_OF_GADGETS],
244            ) = (
245                core::array::from_fn(|_| PolyComm::new(vec![srs_e1.h])),
246                core::array::from_fn(|_| PolyComm::new(vec![srs_e2.h])),
247            );
248            // We commit to the selectors using evaluations.
249            // As they are supposed to be one or zero, each row adds a small
250            // contribution to the commitment.
251            // We explicity commit to all gadgets, even if they are not used in
252            // this indexed relation.
253            circuit_gates
254                .iter()
255                .enumerate()
256                .fold(init, |mut acc, (row, g)| {
257                    let i = usize::from(*g);
258                    acc.0[i] = &acc.0[i] + &srs_e1.get_lagrange_basis(domain_fp.d1)[row];
259                    acc.1[i] = &acc.1[i] + &srs_e2.get_lagrange_basis(domain_fq.d1)[row];
260                    acc
261                })
262        };
263
264        // FIXME: setup correctly the initial sponge state
265        let sponge_e1: [BigInt; PlonkSpongeConstants::SPONGE_WIDTH] =
266            core::array::from_fn(|_i| BigInt::from(42u64));
267
268        Self {
269            domain_fp,
270            domain_fq,
271            srs_e1,
272            srs_e2,
273            app_size,
274            circuit_gates,
275            selectors_comm,
276            constraints_fp,
277            constraints_fq,
278            initial_sponge: sponge_e1,
279        }
280    }
281
282    pub fn get_srs_size(&self) -> usize {
283        self.domain_fp.d1.size as usize
284    }
285
286    pub fn get_srs_blinders(&self) -> (E1, E2) {
287        (self.srs_e1.h, self.srs_e2.h)
288    }
289}