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