Nova/src/gadgets/r1cs.rs
src/gadgets/r1cs.rsRaw
1//! This module implements various gadgets necessary for folding R1CS types.
2use crate::{
3 gadgets::{
4 ecc::AllocatedPoint,
5 utils::{
6 alloc_bignat_constant, alloc_one, alloc_scalar_as_base, conditionally_select,
7 conditionally_select_bignat, le_bits_to_num,
8 },
9 },
10 poseidon::{NovaPoseidonConstants, PoseidonROGadget},
11 r1cs::{R1CSInstance, RelaxedR1CSInstance},
12 traits::Group,
13};
14use bellperson::{
15 gadgets::{boolean::Boolean, num::AllocatedNum, Assignment},
16 ConstraintSystem, SynthesisError,
17};
18use bellperson_nonnative::{
19 mp::bignat::BigNat,
20 util::{convert::f_to_nat, num::Num},
21};
22use ff::Field;
23
24/// An Allocated R1CS Instance
25#[derive(Clone)]
26pub struct AllocatedR1CSInstance<G>
27where
28 G: Group,
29{
30 pub(crate) W: AllocatedPoint<G::Base>,
31 pub(crate) X0: AllocatedNum<G::Base>,
32 pub(crate) X1: AllocatedNum<G::Base>,
33}
34
35impl<G> AllocatedR1CSInstance<G>
36where
37 G: Group,
38{
39 /// Takes the r1cs instance and creates a new allocated r1cs instance
40 pub fn alloc<CS: ConstraintSystem<<G as Group>::Base>>(
41 mut cs: CS,
42 u: Option<R1CSInstance<G>>,
43 ) -> Result<Self, SynthesisError> {
44 // Check that the incoming instance has exactly 2 io
45 let W = AllocatedPoint::alloc(
46 cs.namespace(|| "allocate W"),
47 u.get()
48 .map_or(None, |u| Some(u.comm_W.comm.to_coordinates())),
49 )?;
50
51 let X0 = alloc_scalar_as_base::<G, _>(
52 cs.namespace(|| "allocate X[0]"),
53 u.get().map_or(None, |u| Some(u.X[0])),
54 )?;
55 let X1 = alloc_scalar_as_base::<G, _>(
56 cs.namespace(|| "allocate X[1]"),
57 u.get().map_or(None, |u| Some(u.X[1])),
58 )?;
59
60 Ok(AllocatedR1CSInstance { W, X0, X1 })
61 }
62
63 /// Absorb the provided instance in the RO
64 pub fn absorb_in_ro(&self, ro: &mut PoseidonROGadget<G::Base>) {
65 ro.absorb(self.W.x.clone());
66 ro.absorb(self.W.y.clone());
67 ro.absorb(self.W.is_infinity.clone());
68 ro.absorb(self.X0.clone());
69 ro.absorb(self.X1.clone());
70 }
71}
72
73/// An Allocated Relaxed R1CS Instance
74pub struct AllocatedRelaxedR1CSInstance<G>
75where
76 G: Group,
77{
78 pub(crate) W: AllocatedPoint<G::Base>,
79 pub(crate) E: AllocatedPoint<G::Base>,
80 pub(crate) u: AllocatedNum<G::Base>,
81 pub(crate) X0: BigNat<G::Base>,
82 pub(crate) X1: BigNat<G::Base>,
83}
84
85impl<G> AllocatedRelaxedR1CSInstance<G>
86where
87 G: Group,
88{
89 /// Allocates the given RelaxedR1CSInstance as a witness of the circuit
90 pub fn alloc<CS: ConstraintSystem<<G as Group>::Base>>(
91 mut cs: CS,
92 inst: Option<RelaxedR1CSInstance<G>>,
93 limb_width: usize,
94 n_limbs: usize,
95 ) -> Result<Self, SynthesisError> {
96 let W = AllocatedPoint::alloc(
97 cs.namespace(|| "allocate W"),
98 inst
99 .get()
100 .map_or(None, |inst| Some(inst.comm_W.comm.to_coordinates())),
101 )?;
102
103 let E = AllocatedPoint::alloc(
104 cs.namespace(|| "allocate E"),
105 inst
106 .get()
107 .map_or(None, |inst| Some(inst.comm_E.comm.to_coordinates())),
108 )?;
109
110 // u << |G::Base| despite the fact that u is a scalar.
111 // So we parse all of its bytes as a G::Base element
112 let u = alloc_scalar_as_base::<G, _>(
113 cs.namespace(|| "allocate u"),
114 inst.get().map_or(None, |inst| Some(inst.u)),
115 )?;
116
117 // Allocate X0 and X1. If the input instance is None, then allocate default values 0.
118 let X0 = BigNat::alloc_from_nat(
119 cs.namespace(|| "allocate X[0]"),
120 || {
121 Ok(f_to_nat(
122 &inst.clone().map_or(G::Scalar::zero(), |inst| inst.X[0]),
123 ))
124 },
125 limb_width,
126 n_limbs,
127 )?;
128
129 let X1 = BigNat::alloc_from_nat(
130 cs.namespace(|| "allocate X[1]"),
131 || {
132 Ok(f_to_nat(
133 &inst.clone().map_or(G::Scalar::zero(), |inst| inst.X[1]),
134 ))
135 },
136 limb_width,
137 n_limbs,
138 )?;
139
140 Ok(AllocatedRelaxedR1CSInstance { W, E, u, X0, X1 })
141 }
142
143 /// Allocates the hardcoded default RelaxedR1CSInstance in the circuit.
144 /// W = E = 0, u = 1, X0 = X1 = 0
145 pub fn default<CS: ConstraintSystem<<G as Group>::Base>>(
146 mut cs: CS,
147 limb_width: usize,
148 n_limbs: usize,
149 ) -> Result<Self, SynthesisError> {
150 let W = AllocatedPoint::default(cs.namespace(|| "allocate W"))?;
151 let E = W.clone();
152
153 let u = W.x.clone(); // In the default case, W.x = u = 0
154
155 let X0 = BigNat::alloc_from_nat(
156 cs.namespace(|| "allocate x_default[0]"),
157 || Ok(f_to_nat(&G::Scalar::zero())),
158 limb_width,
159 n_limbs,
160 )?;
161
162 let X1 = BigNat::alloc_from_nat(
163 cs.namespace(|| "allocate x_default[1]"),
164 || Ok(f_to_nat(&G::Scalar::zero())),
165 limb_width,
166 n_limbs,
167 )?;
168
169 Ok(AllocatedRelaxedR1CSInstance { W, E, u, X0, X1 })
170 }
171
172 /// Allocates the R1CS Instance as a RelaxedR1CSInstance in the circuit.
173 /// E = 0, u = 1
174 pub fn from_r1cs_instance<CS: ConstraintSystem<<G as Group>::Base>>(
175 mut cs: CS,
176 inst: AllocatedR1CSInstance<G>,
177 limb_width: usize,
178 n_limbs: usize,
179 ) -> Result<Self, SynthesisError> {
180 let E = AllocatedPoint::default(cs.namespace(|| "allocate W"))?;
181
182 let u = alloc_one(cs.namespace(|| "one"))?;
183
184 let X0 = BigNat::from_num(
185 cs.namespace(|| "allocate X0 from relaxed r1cs"),
186 Num::from(inst.X0.clone()),
187 limb_width,
188 n_limbs,
189 )?;
190
191 let X1 = BigNat::from_num(
192 cs.namespace(|| "allocate X1 from relaxed r1cs"),
193 Num::from(inst.X1.clone()),
194 limb_width,
195 n_limbs,
196 )?;
197
198 Ok(AllocatedRelaxedR1CSInstance {
199 W: inst.W,
200 E,
201 u,
202 X0,
203 X1,
204 })
205 }
206
207 /// Absorb the provided instance in the RO
208 pub fn absorb_in_ro<CS: ConstraintSystem<<G as Group>::Base>>(
209 &self,
210 mut cs: CS,
211 ro: &mut PoseidonROGadget<G::Base>,
212 ) -> Result<(), SynthesisError> {
213 ro.absorb(self.W.x.clone());
214 ro.absorb(self.W.y.clone());
215 ro.absorb(self.W.is_infinity.clone());
216 ro.absorb(self.E.x.clone());
217 ro.absorb(self.E.y.clone());
218 ro.absorb(self.E.is_infinity.clone());
219 ro.absorb(self.u.clone());
220
221 // Analyze X0 as limbs
222 let X0_bn = self
223 .X0
224 .as_limbs::<CS>()
225 .iter()
226 .enumerate()
227 .map(|(i, limb)| {
228 limb
229 .as_sapling_allocated_num(cs.namespace(|| format!("convert limb {} of X_r[0] to num", i)))
230 })
231 .collect::<Result<Vec<AllocatedNum<G::Base>>, _>>()?;
232
233 // absorb each of the limbs of X[0]
234 for limb in X0_bn.into_iter() {
235 ro.absorb(limb);
236 }
237
238 // Analyze X1 as limbs
239 let X1_bn = self
240 .X1
241 .as_limbs::<CS>()
242 .iter()
243 .enumerate()
244 .map(|(i, limb)| {
245 limb
246 .as_sapling_allocated_num(cs.namespace(|| format!("convert limb {} of X_r[1] to num", i)))
247 })
248 .collect::<Result<Vec<AllocatedNum<G::Base>>, _>>()?;
249
250 // absorb each of the limbs of X[1]
251 for limb in X1_bn.into_iter() {
252 ro.absorb(limb);
253 }
254
255 Ok(())
256 }
257
258 /// Folds self with a relaxed r1cs instance and returns the result
259 #[allow(clippy::too_many_arguments)]
260 pub fn fold_with_r1cs<CS: ConstraintSystem<<G as Group>::Base>>(
261 &self,
262 mut cs: CS,
263 params: AllocatedNum<G::Base>, // hash of R1CSShape of F'
264 u: AllocatedR1CSInstance<G>,
265 T: AllocatedPoint<G::Base>,
266 poseidon_constants: NovaPoseidonConstants<G::Base>,
267 limb_width: usize,
268 n_limbs: usize,
269 ) -> Result<AllocatedRelaxedR1CSInstance<G>, SynthesisError> {
270 // Compute r:
271 let mut ro: PoseidonROGadget<G::Base> = PoseidonROGadget::new(poseidon_constants);
272 ro.absorb(params);
273 self.absorb_in_ro(cs.namespace(|| "absorb running instance"), &mut ro)?;
274 u.absorb_in_ro(&mut ro);
275 ro.absorb(T.x.clone());
276 ro.absorb(T.y.clone());
277 ro.absorb(T.is_infinity.clone());
278 let r_bits = ro.get_challenge(cs.namespace(|| "r bits"))?;
279 let r = le_bits_to_num(cs.namespace(|| "r"), r_bits.clone())?;
280
281 // W_fold = self.W + r * u.W
282 let rW = u.W.scalar_mul(cs.namespace(|| "r * u.W"), r_bits.clone())?;
283 let W_fold = self.W.add(cs.namespace(|| "self.W + r * u.W"), &rW)?;
284
285 // E_fold = self.E + r * T
286 let rT = T.scalar_mul(cs.namespace(|| "r * T"), r_bits)?;
287 let E_fold = self.E.add(cs.namespace(|| "self.E + r * T"), &rT)?;
288
289 // u_fold = u_r + r
290 let u_fold = AllocatedNum::alloc(cs.namespace(|| "u_fold"), || {
291 Ok(*self.u.get_value().get()? + r.get_value().get()?)
292 })?;
293 cs.enforce(
294 || "Check u_fold",
295 |lc| lc,
296 |lc| lc,
297 |lc| lc + u_fold.get_variable() - self.u.get_variable() - r.get_variable(),
298 );
299
300 // Fold the IO:
301 // Analyze r into limbs
302 let r_bn = BigNat::from_num(
303 cs.namespace(|| "allocate r_bn"),
304 Num::from(r.clone()),
305 limb_width,
306 n_limbs,
307 )?;
308
309 // Allocate the order of the non-native field as a constant
310 let m_bn = alloc_bignat_constant(
311 cs.namespace(|| "alloc m"),
312 &G::get_order(),
313 limb_width,
314 n_limbs,
315 )?;
316
317 // Analyze X0 to bignat
318 let X0_bn = BigNat::from_num(
319 cs.namespace(|| "allocate X0_bn"),
320 Num::from(u.X0.clone()),
321 limb_width,
322 n_limbs,
323 )?;
324
325 // Fold self.X[0] + r * X[0]
326 let (_, r_0) = X0_bn.mult_mod(cs.namespace(|| "r*X[0]"), &r_bn, &m_bn)?;
327 // add X_r[0]
328 let r_new_0 = self.X0.add::<CS>(&r_0)?;
329 // Now reduce
330 let X0_fold = r_new_0.red_mod(cs.namespace(|| "reduce folded X[0]"), &m_bn)?;
331
332 // Analyze X1 to bignat
333 let X1_bn = BigNat::from_num(
334 cs.namespace(|| "allocate X1_bn"),
335 Num::from(u.X1.clone()),
336 limb_width,
337 n_limbs,
338 )?;
339
340 // Fold self.X[1] + r * X[1]
341 let (_, r_1) = X1_bn.mult_mod(cs.namespace(|| "r*X[1]"), &r_bn, &m_bn)?;
342 // add X_r[1]
343 let r_new_1 = self.X1.add::<CS>(&r_1)?;
344 // Now reduce
345 let X1_fold = r_new_1.red_mod(cs.namespace(|| "reduce folded X[1]"), &m_bn)?;
346
347 Ok(Self {
348 W: W_fold,
349 E: E_fold,
350 u: u_fold,
351 X0: X0_fold,
352 X1: X1_fold,
353 })
354 }
355
356 /// If the condition is true then returns this otherwise it returns the other
357 pub fn conditionally_select<CS: ConstraintSystem<<G as Group>::Base>>(
358 &self,
359 mut cs: CS,
360 other: AllocatedRelaxedR1CSInstance<G>,
361 condition: &Boolean,
362 ) -> Result<AllocatedRelaxedR1CSInstance<G>, SynthesisError> {
363 let W = AllocatedPoint::conditionally_select(
364 cs.namespace(|| "W = cond ? self.W : other.W"),
365 &self.W,
366 &other.W,
367 condition,
368 )?;
369
370 let E = AllocatedPoint::conditionally_select(
371 cs.namespace(|| "E = cond ? self.E : other.E"),
372 &self.E,
373 &other.E,
374 condition,
375 )?;
376
377 let u = conditionally_select(
378 cs.namespace(|| "u = cond ? self.u : other.u"),
379 &self.u,
380 &other.u,
381 condition,
382 )?;
383
384 let X0 = conditionally_select_bignat(
385 cs.namespace(|| "X[0] = cond ? self.X[0] : other.X[0]"),
386 &self.X0,
387 &other.X0,
388 condition,
389 )?;
390
391 let X1 = conditionally_select_bignat(
392 cs.namespace(|| "X[1] = cond ? self.X[1] : other.X[1]"),
393 &self.X1,
394 &other.X1,
395 condition,
396 )?;
397
398 Ok(AllocatedRelaxedR1CSInstance { W, E, u, X0, X1 })
399 }
400}