testudo/src/testudo_snark.rs
src/testudo_snark.rsRaw
1use std::cmp::max;
2
3use crate::errors::ProofVerifyError;
4use crate::r1csinstance::{R1CSCommitmentGens, R1CSEvalProof};
5use crate::r1csproof::R1CSVerifierProof;
6
7use crate::timer::Timer;
8use crate::transcript::TranscriptWriter;
9use crate::{
10 poseidon_transcript::PoseidonTranscript,
11 r1csproof::{R1CSGens, R1CSProof},
12 transcript::Transcript,
13 InputsAssignment, Instance, VarsAssignment,
14};
15use crate::{ComputationCommitment, ComputationDecommitment};
16use ark_crypto_primitives::sponge::poseidon::PoseidonConfig;
17use ark_crypto_primitives::sponge::Absorb;
18use ark_ec::pairing::Pairing;
19
20use ark_serialize::{CanonicalDeserialize, CanonicalSerialize};
21
22#[derive(Debug, CanonicalSerialize, CanonicalDeserialize)]
23
24pub struct TestudoSnark<E: Pairing> {
25 pub r1cs_verifier_proof: R1CSVerifierProof<E>,
26 pub r1cs_eval_proof: R1CSEvalProof<E>,
27 pub inst_evals: (E::ScalarField, E::ScalarField, E::ScalarField),
28 pub r: (Vec<E::ScalarField>, Vec<E::ScalarField>),
29}
30
31pub struct TestudoSnarkGens<E: Pairing> {
32 gens_r1cs_sat: R1CSGens<E>,
33 gens_r1cs_eval: R1CSCommitmentGens<E>,
34}
35
36impl<E: Pairing> TestudoSnarkGens<E> {
37 /// Performs the setups required by the polynomial commitment PST, Groth16
38 /// and the computational commitment given the size of the R1CS statement,
39 /// `num_nz_entries` specifies the maximum number of non-zero entries in
40 /// any of the three R1CS matrices.
41 pub fn setup(
42 num_cons: usize,
43 num_vars: usize,
44 num_inputs: usize,
45 num_nz_entries: usize,
46 poseidon: PoseidonConfig<E::ScalarField>,
47 ) -> Self {
48 // ensure num_vars is a power of 2
49 let num_vars_padded = {
50 let mut num_vars_padded = max(num_vars, num_inputs + 1);
51 if num_vars_padded != num_vars_padded.next_power_of_two() {
52 num_vars_padded = num_vars_padded.next_power_of_two();
53 }
54 num_vars_padded
55 };
56
57 let num_cons_padded = {
58 let mut num_cons_padded = num_cons;
59
60 // ensure that num_cons_padded is at least 2
61 if num_cons_padded == 0 || num_cons_padded == 1 {
62 num_cons_padded = 2;
63 }
64
65 // ensure that num_cons_padded is a power of 2
66 if num_cons.next_power_of_two() != num_cons {
67 num_cons_padded = num_cons.next_power_of_two();
68 }
69 num_cons_padded
70 };
71
72 let gens_r1cs_sat = R1CSGens::setup(
73 b"gens_r1cs_sat",
74 num_cons_padded,
75 num_vars_padded,
76 num_inputs,
77 poseidon,
78 );
79 let gens_r1cs_eval = R1CSCommitmentGens::setup(
80 b"gens_r1cs_eval",
81 num_cons_padded,
82 num_vars_padded,
83 num_inputs,
84 num_nz_entries,
85 );
86 TestudoSnarkGens {
87 gens_r1cs_sat,
88 gens_r1cs_eval,
89 }
90 }
91}
92
93impl<E: Pairing> TestudoSnark<E>
94where
95 E::ScalarField: Absorb,
96{
97 // Constructs the computational commitment, used to prove that the
98 // evaluations of matrices A, B and C sent by the prover to the verifier
99 // are correct.
100 pub fn encode(
101 inst: &Instance<E::ScalarField>,
102 gens: &TestudoSnarkGens<E>,
103 ) -> (
104 ComputationCommitment<E::G1>,
105 ComputationDecommitment<E::ScalarField>,
106 ) {
107 let timer_encode = Timer::new("SNARK::encode");
108 let (comm, decomm) = inst.inst.commit(&gens.gens_r1cs_eval);
109 timer_encode.stop();
110 (
111 ComputationCommitment { comm },
112 ComputationDecommitment { decomm },
113 )
114 }
115
116 // Returns the Testudo SNARK proof which has two components:
117 // * proof that the R1CS instance is satisfiable
118 // * proof that the evlauation of matrices A, B and C on point (x,y)
119 // resulted from the two rounda of sumcheck are correct
120 pub fn prove(
121 inst: &Instance<E::ScalarField>,
122 comm: &ComputationCommitment<E::G1>,
123 decomm: &ComputationDecommitment<E::ScalarField>,
124 vars: VarsAssignment<E::ScalarField>,
125 inputs: &InputsAssignment<E::ScalarField>,
126 gens: &TestudoSnarkGens<E>,
127 transcript: &mut PoseidonTranscript<E::ScalarField>,
128 poseidon: PoseidonConfig<E::ScalarField>,
129 ) -> Result<TestudoSnark<E>, ProofVerifyError> {
130 comm.comm.write_to_transcript(transcript);
131 let c: E::ScalarField = transcript.challenge_scalar(b"");
132 transcript.new_from_state(&c);
133
134 // we might need to pad variables
135 let padded_vars = {
136 let num_padded_vars = inst.inst.get_num_vars();
137 let num_vars = vars.assignment.len();
138 if num_padded_vars > num_vars {
139 vars.pad(num_padded_vars)
140 } else {
141 vars
142 }
143 };
144
145 let (r1cs_sat_proof, rx, ry) = R1CSProof::prove(
146 &inst.inst,
147 padded_vars.assignment,
148 &inputs.assignment,
149 &gens.gens_r1cs_sat,
150 transcript,
151 );
152
153 // We send evaluations of A, B, C at r = (rx, ry) as claims
154 // to enable the verifier complete the first sum-check
155 let timer_eval = Timer::new("eval_sparse_polys");
156 let inst_evals = {
157 let (Ar, Br, Cr) = inst.inst.evaluate(&rx, &ry);
158 transcript.append_scalar(b"", &Ar);
159 transcript.append_scalar(b"", &Br);
160 transcript.append_scalar(b"", &Cr);
161 (Ar, Br, Cr)
162 };
163 timer_eval.stop();
164
165 let timer_eval_proof = Timer::new("r1cs_eval_proof");
166 let r1cs_eval_proof = R1CSEvalProof::prove(
167 &decomm.decomm,
168 &rx,
169 &ry,
170 &inst_evals,
171 &gens.gens_r1cs_eval,
172 transcript,
173 );
174 timer_eval_proof.stop();
175
176 transcript.new_from_state(&c);
177 let timer_sat_circuit_verification = Timer::new("r1cs_sat_circuit_verification");
178 let r1cs_verifier_proof = r1cs_sat_proof
179 .prove_verifier(
180 inst.inst.get_num_vars(),
181 inst.inst.get_num_cons(),
182 &inputs.assignment,
183 &inst_evals,
184 transcript,
185 &gens.gens_r1cs_sat,
186 poseidon,
187 )
188 .unwrap();
189 timer_sat_circuit_verification.stop();
190 Ok(TestudoSnark {
191 r1cs_verifier_proof,
192 r1cs_eval_proof,
193 inst_evals,
194 r: (rx, ry),
195 })
196 }
197
198 pub fn verify(
199 &self,
200 gens: &TestudoSnarkGens<E>,
201 comm: &ComputationCommitment<E::G1>,
202 input: &InputsAssignment<E::ScalarField>,
203 transcript: &mut PoseidonTranscript<E::ScalarField>,
204 _poseidon: PoseidonConfig<E::ScalarField>,
205 ) -> Result<bool, ProofVerifyError> {
206 let (rx, ry) = &self.r;
207
208 let timer_sat_verification = Timer::new("r1cs_sat_verification");
209 let sat_verified = self.r1cs_verifier_proof.verify(
210 (rx.clone(), ry.clone()),
211 &input.assignment,
212 &self.inst_evals,
213 transcript,
214 &gens.gens_r1cs_sat,
215 )?;
216 timer_sat_verification.stop();
217 assert!(sat_verified == true);
218
219 let (Ar, Br, Cr) = &self.inst_evals;
220 transcript.append_scalar(b"", Ar);
221 transcript.append_scalar(b"", Br);
222 transcript.append_scalar(b"", Cr);
223
224 let timer_eval_verification = Timer::new("r1cs_eval_verification");
225 let eval_verified = self.r1cs_eval_proof.verify(
226 &comm.comm,
227 rx,
228 ry,
229 &self.inst_evals,
230 &gens.gens_r1cs_eval,
231 transcript,
232 );
233 timer_eval_verification.stop();
234 Ok(sat_verified && eval_verified.is_ok())
235 }
236}
237
238#[cfg(test)]
239mod tests {
240
241 use crate::ark_std::Zero;
242 use crate::{
243 parameters::poseidon_params,
244 poseidon_transcript::PoseidonTranscript,
245 testudo_snark::{TestudoSnark, TestudoSnarkGens},
246 InputsAssignment, Instance, VarsAssignment,
247 };
248 use ark_ff::{BigInteger, One, PrimeField};
249
250 #[test]
251 pub fn check_testudo_snark() {
252 let num_vars = 256;
253 let num_cons = num_vars;
254 let num_inputs = 10;
255
256 type E = ark_bls12_377::Bls12_377;
257
258 // produce public generators
259 let gens =
260 TestudoSnarkGens::<E>::setup(num_cons, num_vars, num_inputs, num_cons, poseidon_params());
261
262 // produce a synthetic R1CSInstance
263 let (inst, vars, inputs) = Instance::produce_synthetic_r1cs(num_cons, num_vars, num_inputs);
264
265 // create a commitment to R1CSInstance
266 let (comm, decomm) = TestudoSnark::encode(&inst, &gens);
267
268 let params = poseidon_params();
269
270 // produce a proof
271 let mut prover_transcript = PoseidonTranscript::new(¶ms);
272 let proof = TestudoSnark::prove(
273 &inst,
274 &comm,
275 &decomm,
276 vars,
277 &inputs,
278 &gens,
279 &mut prover_transcript,
280 params,
281 )
282 .unwrap();
283
284 // verify the proof
285 let mut verifier_transcript = PoseidonTranscript::new(&poseidon_params());
286 assert!(proof
287 .verify(
288 &gens,
289 &comm,
290 &inputs,
291 &mut verifier_transcript,
292 poseidon_params()
293 )
294 .is_ok());
295 }
296
297 #[test]
298 fn test_padded_constraints() {
299 type F = ark_bls12_377::Fr;
300 type E = ark_bls12_377::Bls12_377;
301 // parameters of the R1CS instance
302 let num_cons = 1;
303 let num_vars = 0;
304 let num_inputs = 3;
305 let num_non_zero_entries = 3;
306
307 // We will encode the above constraints into three matrices, where
308 // the coefficients in the matrix are in the little-endian byte order
309 let mut A: Vec<(usize, usize, Vec<u8>)> = Vec::new();
310 let mut B: Vec<(usize, usize, Vec<u8>)> = Vec::new();
311 let mut C: Vec<(usize, usize, Vec<u8>)> = Vec::new();
312
313 // Create a^2 + b + 13
314 A.push((0, num_vars + 2, (F::one().into_bigint().to_bytes_le()))); // 1*a
315 B.push((0, num_vars + 2, F::one().into_bigint().to_bytes_le())); // 1*a
316 C.push((0, num_vars + 1, F::one().into_bigint().to_bytes_le())); // 1*z
317 C.push((0, num_vars, (-F::from(13u64)).into_bigint().to_bytes_le())); // -13*1
318 C.push((0, num_vars + 3, (-F::one()).into_bigint().to_bytes_le())); // -1*b
319
320 // Var Assignments (Z_0 = 16 is the only output)
321 let vars = vec![F::zero().into_bigint().to_bytes_le(); num_vars];
322
323 // create an InputsAssignment (a = 1, b = 2)
324 let mut inputs = vec![F::zero().into_bigint().to_bytes_le(); num_inputs];
325 inputs[0] = F::from(16u64).into_bigint().to_bytes_le();
326 inputs[1] = F::from(1u64).into_bigint().to_bytes_le();
327 inputs[2] = F::from(2u64).into_bigint().to_bytes_le();
328
329 let assignment_inputs = InputsAssignment::<F>::new(&inputs).unwrap();
330 let assignment_vars = VarsAssignment::new(&vars).unwrap();
331
332 // Check if instance is satisfiable
333 let inst = Instance::new(num_cons, num_vars, num_inputs, &A, &B, &C).unwrap();
334 let res = inst.is_sat(&assignment_vars, &assignment_inputs);
335 assert!(res.unwrap(), "should be satisfied");
336
337 // Testudo public params
338 let gens = TestudoSnarkGens::<E>::setup(
339 num_cons,
340 num_vars,
341 num_inputs,
342 num_non_zero_entries,
343 poseidon_params(),
344 );
345
346 // create a commitment to the R1CS instance
347 let (comm, decomm) = TestudoSnark::encode(&inst, &gens);
348
349 let params = poseidon_params();
350
351 // produce a TestudoSnark
352 let mut prover_transcript = PoseidonTranscript::new(¶ms);
353 let proof = TestudoSnark::prove(
354 &inst,
355 &comm,
356 &decomm,
357 assignment_vars.clone(),
358 &assignment_inputs,
359 &gens,
360 &mut prover_transcript,
361 poseidon_params(),
362 )
363 .unwrap();
364
365 // verify the TestudoSnark
366 let mut verifier_transcript = PoseidonTranscript::new(¶ms);
367 assert!(proof
368 .verify(
369 &gens,
370 &comm,
371 &assignment_inputs,
372 &mut verifier_transcript,
373 poseidon_params()
374 )
375 .is_ok());
376 }
377}