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