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}