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