sonobe/src/decider/circuit.rs
src/decider/circuit.rsRaw
1use ark_ec::CurveGroup;
2use ark_ff::{Field, PrimeField};
3use ark_r1cs_std::{
4 alloc::{AllocVar, AllocationMode},
5 fields::FieldVar,
6};
7use ark_relations::r1cs::{Namespace, SynthesisError};
8use core::{borrow::Borrow, marker::PhantomData};
9
10use crate::ccs::r1cs::RelaxedR1CS;
11use crate::utils::vec::SparseMatrix;
12use crate::Error;
13
14pub type ConstraintF<C> = <<C as CurveGroup>::BaseField as Field>::BasePrimeField;
15
16#[derive(Debug, Clone)]
17pub struct RelaxedR1CSGadget<F: PrimeField, CF: PrimeField, FV: FieldVar<F, CF>> {
18 _f: PhantomData<F>,
19 _cf: PhantomData<CF>,
20 _fv: PhantomData<FV>,
21}
22impl<F: PrimeField, CF: PrimeField, FV: FieldVar<F, CF>> RelaxedR1CSGadget<F, CF, FV> {
23 /// performs the RelaxedR1CS check (Az∘Bz==uCz+E)
24 pub fn check(rel_r1cs: RelaxedR1CSVar<F, CF, FV>, z: Vec<FV>) -> Result<(), Error> {
25 let Az = mat_vec_mul_sparse(rel_r1cs.A, z.clone());
26 let Bz = mat_vec_mul_sparse(rel_r1cs.B, z.clone());
27 let Cz = mat_vec_mul_sparse(rel_r1cs.C, z.clone());
28 let uCz = vec_scalar_mul(&Cz, &rel_r1cs.u);
29 let uCzE = vec_add(&uCz, &rel_r1cs.E)?;
30 let AzBz = hadamard(&Az, &Bz)?;
31 for i in 0..AzBz.len() {
32 AzBz[i].enforce_equal(&uCzE[i].clone())?;
33 }
34 Ok(())
35 }
36}
37
38fn mat_vec_mul_sparse<F: PrimeField, CF: PrimeField, FV: FieldVar<F, CF>>(
39 m: SparseMatrixVar<F, CF, FV>,
40 v: Vec<FV>,
41) -> Vec<FV> {
42 let mut res = vec![FV::zero(); m.n_rows];
43 for (row_i, row) in m.coeffs.iter().enumerate() {
44 for (value, col_i) in row.iter() {
45 res[row_i] += value.clone().mul(&v[*col_i].clone());
46 }
47 }
48 res
49}
50pub fn vec_add<F: PrimeField, CF: PrimeField, FV: FieldVar<F, CF>>(
51 a: &Vec<FV>,
52 b: &Vec<FV>,
53) -> Result<Vec<FV>, Error> {
54 if a.len() != b.len() {
55 return Err(Error::NotSameLength(
56 "a.len()".to_string(),
57 a.len(),
58 "b.len()".to_string(),
59 b.len(),
60 ));
61 }
62 let mut r: Vec<FV> = vec![FV::zero(); a.len()];
63 for i in 0..a.len() {
64 r[i] = a[i].clone() + b[i].clone();
65 }
66 Ok(r)
67}
68pub fn vec_scalar_mul<F: PrimeField, CF: PrimeField, FV: FieldVar<F, CF>>(
69 vec: &Vec<FV>,
70 c: &FV,
71) -> Vec<FV> {
72 let mut result = vec![FV::zero(); vec.len()];
73 for (i, a) in vec.iter().enumerate() {
74 result[i] = a.clone() * c;
75 }
76 result
77}
78pub fn hadamard<F: PrimeField, CF: PrimeField, FV: FieldVar<F, CF>>(
79 a: &Vec<FV>,
80 b: &Vec<FV>,
81) -> Result<Vec<FV>, Error> {
82 if a.len() != b.len() {
83 return Err(Error::NotSameLength(
84 "a.len()".to_string(),
85 a.len(),
86 "b.len()".to_string(),
87 b.len(),
88 ));
89 }
90 let mut r: Vec<FV> = vec![FV::zero(); a.len()];
91 for i in 0..a.len() {
92 r[i] = a[i].clone() * b[i].clone();
93 }
94 Ok(r)
95}
96
97#[derive(Debug, Clone)]
98pub struct SparseMatrixVar<F: PrimeField, CF: PrimeField, FV: FieldVar<F, CF>> {
99 _f: PhantomData<F>,
100 _cf: PhantomData<CF>,
101 _fv: PhantomData<FV>,
102 pub n_rows: usize,
103 pub n_cols: usize,
104 // same format as the native SparseMatrix (which follows ark_relations::r1cs::Matrix format
105 pub coeffs: Vec<Vec<(FV, usize)>>,
106}
107
108impl<F, CF, FV> AllocVar<SparseMatrix<F>, CF> for SparseMatrixVar<F, CF, FV>
109where
110 F: PrimeField,
111 CF: PrimeField,
112 FV: FieldVar<F, CF>,
113{
114 fn new_variable<T: Borrow<SparseMatrix<F>>>(
115 cs: impl Into<Namespace<CF>>,
116 f: impl FnOnce() -> Result<T, SynthesisError>,
117 mode: AllocationMode,
118 ) -> Result<Self, SynthesisError> {
119 f().and_then(|val| {
120 let cs = cs.into();
121
122 let mut coeffs: Vec<Vec<(FV, usize)>> = Vec::new();
123 for row in val.borrow().coeffs.iter() {
124 let mut rowVar: Vec<(FV, usize)> = Vec::new();
125 for &(value, col_i) in row.iter() {
126 let coeffVar = FV::new_variable(cs.clone(), || Ok(value), mode)?;
127 rowVar.push((coeffVar, col_i));
128 }
129 coeffs.push(rowVar);
130 }
131
132 Ok(Self {
133 _f: PhantomData,
134 _cf: PhantomData,
135 _fv: PhantomData,
136 n_rows: val.borrow().n_rows,
137 n_cols: val.borrow().n_cols,
138 coeffs,
139 })
140 })
141 }
142}
143
144#[derive(Debug, Clone)]
145pub struct RelaxedR1CSVar<F: PrimeField, CF: PrimeField, FV: FieldVar<F, CF>> {
146 _f: PhantomData<F>,
147 _cf: PhantomData<CF>,
148 _fv: PhantomData<FV>,
149 pub A: SparseMatrixVar<F, CF, FV>,
150 pub B: SparseMatrixVar<F, CF, FV>,
151 pub C: SparseMatrixVar<F, CF, FV>,
152 pub u: FV,
153 pub E: Vec<FV>,
154}
155
156impl<F, CF, FV> AllocVar<RelaxedR1CS<F>, CF> for RelaxedR1CSVar<F, CF, FV>
157where
158 F: PrimeField,
159 CF: PrimeField,
160 FV: FieldVar<F, CF>,
161{
162 fn new_variable<T: Borrow<RelaxedR1CS<F>>>(
163 cs: impl Into<Namespace<CF>>,
164 f: impl FnOnce() -> Result<T, SynthesisError>,
165 mode: AllocationMode,
166 ) -> Result<Self, SynthesisError> {
167 f().and_then(|val| {
168 let cs = cs.into();
169
170 let A = SparseMatrixVar::<F, CF, FV>::new_constant(cs.clone(), &val.borrow().A)?;
171 let B = SparseMatrixVar::<F, CF, FV>::new_constant(cs.clone(), &val.borrow().B)?;
172 let C = SparseMatrixVar::<F, CF, FV>::new_constant(cs.clone(), &val.borrow().C)?;
173 let E = Vec::<FV>::new_variable(cs.clone(), || Ok(val.borrow().E.clone()), mode)?;
174 let u = FV::new_variable(cs.clone(), || Ok(val.borrow().u), mode)?;
175
176 Ok(Self {
177 _f: PhantomData,
178 _cf: PhantomData,
179 _fv: PhantomData,
180 A,
181 B,
182 C,
183 E,
184 u,
185 })
186 })
187 }
188}
189
190#[cfg(test)]
191mod tests {
192 use super::*;
193 use ark_crypto_primitives::crh::{
194 sha256::{
195 constraints::{Sha256Gadget, UnitVar},
196 Sha256,
197 },
198 CRHScheme, CRHSchemeGadget,
199 };
200 use ark_ff::BigInteger;
201 use ark_pallas::{Fq, Fr};
202 use ark_r1cs_std::{
203 alloc::AllocVar,
204 bits::uint8::UInt8,
205 eq::EqGadget,
206 fields::{fp::FpVar, nonnative::NonNativeFieldVar},
207 };
208 use ark_relations::r1cs::{
209 ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, SynthesisError,
210 };
211 use ark_std::One;
212
213 use crate::ccs::r1cs::{
214 tests::{get_test_r1cs, get_test_z},
215 R1CS,
216 };
217 use crate::frontend::arkworks::{extract_r1cs_and_z, tests::TestCircuit};
218
219 #[test]
220 fn test_relaxed_r1cs_small_gadget_handcrafted() {
221 let r1cs: R1CS<Fr> = get_test_r1cs();
222 let rel_r1cs = r1cs.relax();
223 let z = get_test_z(3);
224
225 let cs = ConstraintSystem::<Fr>::new_ref();
226
227 let zVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z)).unwrap();
228 let rel_r1csVar =
229 RelaxedR1CSVar::<Fr, Fr, FpVar<Fr>>::new_witness(cs.clone(), || Ok(rel_r1cs)).unwrap();
230
231 RelaxedR1CSGadget::<Fr, Fr, FpVar<Fr>>::check(rel_r1csVar, zVar).unwrap();
232 assert!(cs.is_satisfied().unwrap());
233 }
234
235 // gets as input a circuit that implements the ConstraintSynthesizer trait, and that has been
236 // initialized.
237 fn test_relaxed_r1cs_gadget<CS: ConstraintSynthesizer<Fr>>(circuit: CS) {
238 let cs = ConstraintSystem::<Fr>::new_ref();
239
240 circuit.generate_constraints(cs.clone()).unwrap();
241 cs.finalize();
242 assert!(cs.is_satisfied().unwrap());
243
244 let cs = cs.into_inner().unwrap();
245
246 let (r1cs, z) = extract_r1cs_and_z::<Fr>(&cs);
247 r1cs.check_relation(&z).unwrap();
248
249 let relaxed_r1cs = r1cs.relax();
250 relaxed_r1cs.check_relation(&z).unwrap();
251
252 // set new CS for the circuit that checks the RelaxedR1CS of our original circuit
253 let cs = ConstraintSystem::<Fr>::new_ref();
254 // prepare the inputs for our circuit
255 let zVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z)).unwrap();
256 let rel_r1csVar =
257 RelaxedR1CSVar::<Fr, Fr, FpVar<Fr>>::new_witness(cs.clone(), || Ok(relaxed_r1cs))
258 .unwrap();
259
260 RelaxedR1CSGadget::<Fr, Fr, FpVar<Fr>>::check(rel_r1csVar, zVar).unwrap();
261 assert!(cs.is_satisfied().unwrap());
262 }
263
264 #[test]
265 fn test_relaxed_r1cs_small_gadget_arkworks() {
266 let x = Fr::from(5_u32);
267 let y = x * x * x + x + Fr::from(5_u32);
268 let circuit = TestCircuit::<Fr> { x, y };
269 test_relaxed_r1cs_gadget(circuit);
270 }
271
272 struct Sha256TestCircuit<F: PrimeField> {
273 _f: PhantomData<F>,
274 pub x: Vec<u8>,
275 pub y: Vec<u8>,
276 }
277 impl<F: PrimeField> ConstraintSynthesizer<F> for Sha256TestCircuit<F> {
278 fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
279 let x = Vec::<UInt8<F>>::new_witness(cs.clone(), || Ok(self.x))?;
280 let y = Vec::<UInt8<F>>::new_input(cs.clone(), || Ok(self.y))?;
281
282 let unitVar = UnitVar::default();
283 let comp_y = <Sha256Gadget<F> as CRHSchemeGadget<Sha256, F>>::evaluate(&unitVar, &x)?;
284 comp_y.0.enforce_equal(&y)?;
285 Ok(())
286 }
287 }
288 #[test]
289 fn test_relaxed_r1cs_medium_gadget_arkworks() {
290 let x = Fr::from(5_u32).into_bigint().to_bytes_le();
291 let y = <Sha256 as CRHScheme>::evaluate(&(), x.clone()).unwrap();
292
293 let circuit = Sha256TestCircuit::<Fr> {
294 _f: PhantomData,
295 x,
296 y,
297 };
298 test_relaxed_r1cs_gadget(circuit);
299 }
300
301 // circuit that has the number of constraints specified in the `n_constraints` parameter. Note
302 // that the generated circuit will have very sparse matrices, so the resulting constraints
303 // number of the RelaxedR1CS gadget must take that into account.
304 struct CustomTestCircuit<F: PrimeField> {
305 _f: PhantomData<F>,
306 pub n_constraints: usize,
307 pub x: F,
308 pub y: F,
309 }
310 impl<F: PrimeField> CustomTestCircuit<F> {
311 fn new(n_constraints: usize) -> Self {
312 let x = F::from(5_u32);
313 let mut y = F::one();
314 for _ in 0..n_constraints - 1 {
315 y *= x;
316 }
317 Self {
318 _f: PhantomData,
319 n_constraints,
320 x,
321 y,
322 }
323 }
324 }
325 impl<F: PrimeField> ConstraintSynthesizer<F> for CustomTestCircuit<F> {
326 fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
327 let x = FpVar::<F>::new_witness(cs.clone(), || Ok(self.x))?;
328 let y = FpVar::<F>::new_input(cs.clone(), || Ok(self.y))?;
329
330 let mut comp_y = FpVar::<F>::new_witness(cs.clone(), || Ok(F::one()))?;
331 for _ in 0..self.n_constraints - 1 {
332 comp_y *= x.clone();
333 }
334
335 comp_y.enforce_equal(&y)?;
336 Ok(())
337 }
338 }
339
340 #[test]
341 fn test_relaxed_r1cs_custom_circuit() {
342 let n_constraints = 10_000;
343 let x = Fr::from(5_u32);
344 let mut y = Fr::one();
345 for _ in 0..n_constraints - 1 {
346 y *= x;
347 }
348
349 let circuit = CustomTestCircuit::<Fr> {
350 _f: PhantomData,
351 n_constraints,
352 x,
353 y,
354 };
355 test_relaxed_r1cs_gadget(circuit);
356 }
357
358 #[test]
359 fn test_relaxed_r1cs_nonnative_circuit() {
360 let cs = ConstraintSystem::<Fq>::new_ref();
361 // in practice we would use CycleFoldCircuit, but is a very big circuit (when computed
362 // non-natively inside the RelaxedR1CS circuit), so in order to have a short test we use a
363 // custom circuit.
364 let circuit = CustomTestCircuit::<Fq>::new(10);
365 circuit.generate_constraints(cs.clone()).unwrap();
366 cs.finalize();
367 let cs = cs.into_inner().unwrap();
368 let (r1cs, z) = extract_r1cs_and_z::<Fq>(&cs);
369
370 let relaxed_r1cs = r1cs.relax();
371
372 // natively
373 let cs = ConstraintSystem::<Fq>::new_ref();
374 let zVar = Vec::<FpVar<Fq>>::new_witness(cs.clone(), || Ok(z.clone())).unwrap();
375 let rel_r1csVar = RelaxedR1CSVar::<Fq, Fq, FpVar<Fq>>::new_witness(cs.clone(), || {
376 Ok(relaxed_r1cs.clone())
377 })
378 .unwrap();
379 RelaxedR1CSGadget::<Fq, Fq, FpVar<Fq>>::check(rel_r1csVar, zVar).unwrap();
380
381 // non-natively
382 let cs = ConstraintSystem::<Fr>::new_ref();
383 let zVar = Vec::<NonNativeFieldVar<Fq, Fr>>::new_witness(cs.clone(), || Ok(z)).unwrap();
384 let rel_r1csVar =
385 RelaxedR1CSVar::<Fq, Fr, NonNativeFieldVar<Fq, Fr>>::new_witness(cs.clone(), || {
386 Ok(relaxed_r1cs)
387 })
388 .unwrap();
389 RelaxedR1CSGadget::<Fq, Fr, NonNativeFieldVar<Fq, Fr>>::check(rel_r1csVar, zVar).unwrap();
390 }
391}