kimchi_stubs/
pasta_fp_plonk_proof.rs

1use crate::{
2    arkworks::{CamlFp, CamlGVesta},
3    field_vector::fp::CamlFpVector,
4    pasta_fp_plonk_index::{CamlPastaFpPlonkIndex, CamlPastaFpPlonkIndexPtr},
5    pasta_fp_plonk_verifier_index::CamlPastaFpPlonkVerifierIndex,
6    srs::fp::CamlFpSrs,
7    WithLagrangeBasis,
8};
9use ark_ec::AffineRepr;
10use ark_ff::One;
11use core::array;
12use groupmap::GroupMap;
13use kimchi::{
14    circuits::{
15        lookup::runtime_tables::{caml::CamlRuntimeTable, RuntimeTable},
16        polynomial::COLUMNS,
17    },
18    proof::{
19        PointEvaluations, ProofEvaluations, ProverCommitments, ProverProof, RecursionChallenge,
20    },
21    prover::caml::CamlProofWithPublic,
22    prover_index::ProverIndex,
23    verifier::{batch_verify, verify, Context},
24    verifier_index::VerifierIndex,
25};
26use mina_curves::pasta::{Fp, Fq, Pallas, Vesta, VestaParameters};
27use mina_poseidon::{
28    constants::PlonkSpongeConstantsKimchi,
29    sponge::{DefaultFqSponge, DefaultFrSponge},
30};
31use poly_commitment::{
32    commitment::{CommitmentCurve, PolyComm},
33    ipa::OpeningProof,
34};
35use std::convert::TryInto;
36
37type EFqSponge = DefaultFqSponge<VestaParameters, PlonkSpongeConstantsKimchi>;
38type EFrSponge = DefaultFrSponge<Fp, PlonkSpongeConstantsKimchi>;
39
40#[ocaml_gen::func]
41#[ocaml::func]
42pub fn caml_pasta_fp_plonk_proof_create(
43    index: CamlPastaFpPlonkIndexPtr<'static>,
44    witness: Vec<CamlFpVector>,
45    runtime_tables: Vec<CamlRuntimeTable<CamlFp>>,
46    prev_challenges: Vec<CamlFp>,
47    prev_sgs: Vec<CamlGVesta>,
48) -> Result<CamlProofWithPublic<CamlGVesta, CamlFp>, ocaml::Error> {
49    {
50        index
51            .as_ref()
52            .0
53            .srs
54            .with_lagrange_basis(index.as_ref().0.cs.domain.d1);
55    }
56
57    let prev = if prev_challenges.is_empty() {
58        Vec::new()
59    } else {
60        let challenges_per_sg = prev_challenges.len() / prev_sgs.len();
61        prev_sgs
62            .into_iter()
63            .map(Into::<Vesta>::into)
64            .enumerate()
65            .map(|(i, sg)| {
66                let chals = prev_challenges[(i * challenges_per_sg)..(i + 1) * challenges_per_sg]
67                    .iter()
68                    .map(Into::<Fp>::into)
69                    .collect();
70                let comm = PolyComm::<Vesta> { chunks: vec![sg] };
71                RecursionChallenge { chals, comm }
72            })
73            .collect()
74    };
75
76    let witness: Vec<Vec<_>> = witness.iter().map(|x| (**x).clone()).collect();
77    let witness: [Vec<_>; COLUMNS] = witness
78        .try_into()
79        .map_err(|_| ocaml::Error::Message("the witness should be a column of 15 vectors"))?;
80    let index: &ProverIndex<Vesta, OpeningProof<Vesta>> = &index.as_ref().0;
81    let runtime_tables: Vec<RuntimeTable<Fp>> =
82        runtime_tables.into_iter().map(Into::into).collect();
83
84    // public input
85    let public_input = witness[0][0..index.cs.public].to_vec();
86
87    if std::env::var("KIMCHI_PROVER_DUMP_ARGUMENTS").is_ok() {
88        kimchi::bench::bench_arguments_dump_into_file(&index.cs, &witness, &runtime_tables, &prev);
89    }
90
91    // NB: This method is designed only to be used by tests. However, since creating a new reference will cause `drop` to be called on it once we are done with it. Since `drop` calls `caml_shutdown` internally, we *really, really* do not want to do this, but we have no other way to get at the active runtime.
92    // TODO: There's actually a way to get a handle to the runtime as a function argument. Switch
93    // to doing this instead.
94    let runtime = unsafe { ocaml::Runtime::recover_handle() };
95
96    // Release the runtime lock so that other threads can run using it while we generate the proof.
97    runtime.releasing_runtime(|| {
98        let group_map = GroupMap::<Fq>::setup();
99        let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
100            &group_map,
101            witness,
102            &runtime_tables,
103            index,
104            prev,
105            None,
106            &mut rand::rngs::OsRng,
107        )
108        .map_err(|e| ocaml::Error::Error(e.into()))?;
109        Ok((proof, public_input).into())
110    })
111}
112
113#[ocaml_gen::func]
114#[ocaml::func]
115pub fn caml_pasta_fp_plonk_proof_create_and_verify(
116    index: CamlPastaFpPlonkIndexPtr<'static>,
117    witness: Vec<CamlFpVector>,
118    runtime_tables: Vec<CamlRuntimeTable<CamlFp>>,
119    prev_challenges: Vec<CamlFp>,
120    prev_sgs: Vec<CamlGVesta>,
121) -> Result<CamlProofWithPublic<CamlGVesta, CamlFp>, ocaml::Error> {
122    {
123        index
124            .as_ref()
125            .0
126            .srs
127            .with_lagrange_basis(index.as_ref().0.cs.domain.d1);
128    }
129    let prev = if prev_challenges.is_empty() {
130        Vec::new()
131    } else {
132        let challenges_per_sg = prev_challenges.len() / prev_sgs.len();
133        prev_sgs
134            .into_iter()
135            .map(Into::<Vesta>::into)
136            .enumerate()
137            .map(|(i, sg)| {
138                let chals = prev_challenges[(i * challenges_per_sg)..(i + 1) * challenges_per_sg]
139                    .iter()
140                    .map(Into::<Fp>::into)
141                    .collect();
142                let comm = PolyComm::<Vesta> { chunks: vec![sg] };
143                RecursionChallenge { chals, comm }
144            })
145            .collect()
146    };
147
148    let witness: Vec<Vec<_>> = witness.iter().map(|x| (**x).clone()).collect();
149    let witness: [Vec<_>; COLUMNS] = witness
150        .try_into()
151        .map_err(|_| ocaml::Error::Message("the witness should be a column of 15 vectors"))?;
152    let index: &ProverIndex<Vesta, OpeningProof<Vesta>> = &index.as_ref().0;
153    let runtime_tables: Vec<RuntimeTable<Fp>> =
154        runtime_tables.into_iter().map(Into::into).collect();
155
156    // public input
157    let public_input = witness[0][0..index.cs.public].to_vec();
158
159    // NB: This method is designed only to be used by tests. However, since creating a new reference will cause `drop` to be called on it once we are done with it. Since `drop` calls `caml_shutdown` internally, we *really, really* do not want to do this, but we have no other way to get at the active runtime.
160    // TODO: There's actually a way to get a handle to the runtime as a function argument. Switch
161    // to doing this instead.
162    let runtime = unsafe { ocaml::Runtime::recover_handle() };
163
164    // Release the runtime lock so that other threads can run using it while we generate the proof.
165    runtime.releasing_runtime(|| {
166        let group_map = GroupMap::<Fq>::setup();
167        let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
168            &group_map,
169            witness,
170            &runtime_tables,
171            index,
172            prev,
173            None,
174            &mut rand::rngs::OsRng,
175        )
176        .map_err(|e| ocaml::Error::Error(e.into()))?;
177
178        let verifier_index = index.verifier_index();
179
180        // Verify proof
181        verify::<Vesta, EFqSponge, EFrSponge, OpeningProof<Vesta>>(
182            &group_map,
183            &verifier_index,
184            &proof,
185            &public_input,
186        )?;
187
188        Ok((proof, public_input).into())
189    })
190}
191
192#[ocaml_gen::func]
193#[ocaml::func]
194pub fn caml_pasta_fp_plonk_proof_example_with_lookup(
195    srs: CamlFpSrs,
196    lazy_mode: bool,
197) -> (
198    CamlPastaFpPlonkIndex,
199    CamlFp,
200    CamlProofWithPublic<CamlGVesta, CamlFp>,
201) {
202    use ark_ff::Zero;
203    use kimchi::circuits::{
204        constraints::ConstraintSystem,
205        gate::{CircuitGate, GateType},
206        lookup::{
207            runtime_tables::{RuntimeTable, RuntimeTableCfg},
208            tables::LookupTable,
209        },
210        polynomial::COLUMNS,
211        wires::Wire,
212    };
213    use poly_commitment::ipa::endos;
214
215    let num_gates = 1000;
216    let num_tables: usize = 5;
217
218    // Even if using runtime tables, we need a fixed table with a zero row.
219    let fixed_tables = vec![LookupTable {
220        id: 0,
221        data: vec![vec![0, 0, 0, 0, 0].into_iter().map(Into::into).collect()],
222    }];
223
224    let mut runtime_tables_setup = vec![];
225    let first_column: Vec<_> = [8u32, 9, 8, 7, 1].into_iter().map(Into::into).collect();
226    for table_id in 0..num_tables {
227        let cfg = RuntimeTableCfg {
228            id: table_id as i32,
229            first_column: first_column.clone(),
230        };
231        runtime_tables_setup.push(cfg);
232    }
233
234    let data: Vec<Fp> = [0u32, 2, 3, 4, 5].into_iter().map(Into::into).collect();
235    let runtime_tables: Vec<RuntimeTable<Fp>> = runtime_tables_setup
236        .iter()
237        .map(|cfg| RuntimeTable {
238            id: cfg.id(),
239            data: data.clone(),
240        })
241        .collect();
242
243    // circuit
244    let mut gates = vec![];
245    for row in 0..num_gates {
246        gates.push(CircuitGate {
247            typ: GateType::Lookup,
248            wires: Wire::for_row(row),
249            coeffs: vec![],
250        });
251    }
252
253    // witness
254    let witness = {
255        let mut cols: [_; COLUMNS] = core::array::from_fn(|_col| vec![Fp::zero(); gates.len()]);
256
257        // only the first 7 registers are used in the lookup gate
258        let (lookup_cols, _rest) = cols.split_at_mut(7);
259
260        for row in 0..num_gates {
261            // the first register is the table id
262            lookup_cols[0][row] = ((row % num_tables) as u64).into();
263
264            // create queries into our runtime lookup table
265            let lookup_cols = &mut lookup_cols[1..];
266            for (chunk_id, chunk) in lookup_cols.chunks_mut(2).enumerate() {
267                // this could be properly fully random
268                if (row + chunk_id) % 2 == 0 {
269                    chunk[0][row] = 9u32.into(); // index
270                    chunk[1][row] = 2u32.into(); // value
271                } else {
272                    chunk[0][row] = 8u32.into(); // index
273                    chunk[1][row] = 3u32.into(); // value
274                }
275            }
276        }
277        cols
278    };
279
280    let num_public_inputs = 1;
281
282    // not sure if theres a smarter way instead of the double unwrap, but should be fine in the test
283    let cs = ConstraintSystem::<Fp>::create(gates)
284        .runtime(Some(runtime_tables_setup))
285        .lookup(fixed_tables)
286        .public(num_public_inputs)
287        .lazy_mode(lazy_mode)
288        .build()
289        .unwrap();
290
291    srs.0.with_lagrange_basis(cs.domain.d1);
292
293    let (endo_q, _endo_r) = endos::<Pallas>();
294    let index = ProverIndex::<Vesta, OpeningProof<Vesta>>::create(cs, endo_q, srs.0, lazy_mode);
295    let group_map = <Vesta as CommitmentCurve>::Map::setup();
296    let public_input = witness[0][0];
297    let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
298        &group_map,
299        witness,
300        &runtime_tables,
301        &index,
302        vec![],
303        None,
304        &mut rand::rngs::OsRng,
305    )
306    .unwrap();
307
308    let caml_prover_proof = (proof, vec![public_input]).into();
309
310    (
311        CamlPastaFpPlonkIndex(Box::new(index)),
312        public_input.into(),
313        caml_prover_proof,
314    )
315}
316
317#[ocaml_gen::func]
318#[ocaml::func]
319pub fn caml_pasta_fp_plonk_proof_example_with_foreign_field_mul(
320    srs: CamlFpSrs,
321    lazy_mode: bool,
322) -> (
323    CamlPastaFpPlonkIndex,
324    CamlProofWithPublic<CamlGVesta, CamlFp>,
325) {
326    use ark_ff::Zero;
327    use kimchi::circuits::{
328        constraints::ConstraintSystem,
329        gate::{CircuitGate, Connect},
330        polynomials::{foreign_field_common::BigUintForeignFieldHelpers, foreign_field_mul},
331        wires::Wire,
332    };
333    use num_bigint::{BigUint, RandBigInt};
334    use o1_utils::FieldHelpers;
335    use poly_commitment::ipa::endos;
336    use rand::{rngs::StdRng, SeedableRng};
337
338    let foreign_field_modulus = Fq::modulus_biguint();
339
340    // Layout
341    //      0-1  ForeignFieldMul | Zero
342    //      2-5  compact-multi-range-check (result range check)
343    //        6  "single" Generic (result bound)
344    //      7-10 multi-range-check (quotient range check)
345    //     11-14 multi-range-check (quotient_bound, product1_lo, product1_hi_0)
346    //     later limb-check result bound
347    //        15 Generic (left and right bounds)
348    //     16-19 multi-range-check (left multiplicand)
349    //     20-23 multi-range-check (right multiplicand)
350    //     24-27 multi-range-check (result bound, left bound, right bound)
351    // TODO: check when kimchi is merged to berkeley
352
353    // Create foreign field multiplication gates
354    let (mut next_row, mut gates) =
355        CircuitGate::<Fp>::create_foreign_field_mul(0, &foreign_field_modulus);
356
357    let rng = &mut StdRng::from_seed([2u8; 32]);
358    let left_input = rng.gen_biguint_range(&BigUint::zero(), &foreign_field_modulus);
359    let right_input = rng.gen_biguint_range(&BigUint::zero(), &foreign_field_modulus);
360
361    // Compute multiplication witness
362    let (mut witness, mut external_checks) =
363        foreign_field_mul::witness::create(&left_input, &right_input, &foreign_field_modulus);
364
365    // Result compact-multi-range-check
366    CircuitGate::extend_compact_multi_range_check(&mut gates, &mut next_row);
367    gates.connect_cell_pair((1, 0), (4, 1)); // remainder01
368    gates.connect_cell_pair((1, 1), (2, 0)); // remainder2
369    external_checks.extend_witness_compact_multi_range_checks(&mut witness);
370    // These are the coordinates (row, col) of the remainder limbs in the witness
371    // remainder0 -> (3, 0), remainder1 -> (4, 0), remainder2 -> (2,0)
372
373    // Constant single Generic gate for result bound
374    CircuitGate::extend_high_bounds(&mut gates, &mut next_row, &foreign_field_modulus);
375    gates.connect_cell_pair((6, 0), (1, 1)); // remainder2
376    external_checks.extend_witness_high_bounds_computation(&mut witness, &foreign_field_modulus);
377
378    // Quotient multi-range-check
379    CircuitGate::extend_multi_range_check(&mut gates, &mut next_row);
380    gates.connect_cell_pair((1, 2), (7, 0)); // quotient0
381    gates.connect_cell_pair((1, 3), (8, 0)); // quotient1
382    gates.connect_cell_pair((1, 4), (9, 0)); // quotient2
383                                             // Witness updated below
384
385    // Multiplication witness value quotient_bound, product1_lo, product1_hi_0 multi-range-check
386    CircuitGate::extend_multi_range_check(&mut gates, &mut next_row);
387    gates.connect_cell_pair((1, 5), (11, 0)); // quotient_bound
388    gates.connect_cell_pair((0, 6), (12, 0)); // product1_lo
389    gates.connect_cell_pair((1, 6), (13, 0)); // product1_hi_0
390                                              // Witness updated below
391
392    // Add witness for external multi-range checks:
393    // [quotient0, quotient1, quotient2]
394    // [quotient_bound, product1_lo, product1_hi_0]
395    external_checks.extend_witness_multi_range_checks(&mut witness);
396
397    // DESIGNER CHOICE: left and right (and result bound from before)
398    let left_limbs = left_input.to_field_limbs();
399    let right_limbs = right_input.to_field_limbs();
400    // Constant Double Generic gate for result and quotient bounds
401    external_checks.add_high_bound_computation(&left_limbs[2]);
402    external_checks.add_high_bound_computation(&right_limbs[2]);
403    CircuitGate::extend_high_bounds(&mut gates, &mut next_row, &foreign_field_modulus);
404    gates.connect_cell_pair((15, 0), (0, 2)); // left2
405    gates.connect_cell_pair((15, 3), (0, 5)); // right2
406    external_checks.extend_witness_high_bounds_computation(&mut witness, &foreign_field_modulus);
407
408    // Left input multi-range-check
409    external_checks.add_multi_range_check(&left_limbs);
410    CircuitGate::extend_multi_range_check(&mut gates, &mut next_row);
411    gates.connect_cell_pair((0, 0), (16, 0)); // left_input0
412    gates.connect_cell_pair((0, 1), (17, 0)); // left_input1
413    gates.connect_cell_pair((0, 2), (18, 0)); // left_input2
414                                              // Witness updated below
415
416    // Right input multi-range-check
417    external_checks.add_multi_range_check(&right_limbs);
418    CircuitGate::extend_multi_range_check(&mut gates, &mut next_row);
419    gates.connect_cell_pair((0, 3), (20, 0)); // right_input0
420    gates.connect_cell_pair((0, 4), (21, 0)); // right_input1
421    gates.connect_cell_pair((0, 5), (22, 0)); // right_input2
422                                              // Witness updated below
423
424    // Add witness for external multi-range checks:
425    // left and right limbs
426    external_checks.extend_witness_multi_range_checks(&mut witness);
427
428    // [result_bound, 0, 0]
429    // Bounds for result limb range checks
430    CircuitGate::extend_multi_range_check(&mut gates, &mut next_row);
431    gates.connect_cell_pair((6, 2), (24, 0)); // result_bound
432                                              // Witness updated below
433
434    // Multi-range check bounds for left and right inputs
435    let left_hi_bound =
436        foreign_field_mul::witness::compute_bound(&left_input, &foreign_field_modulus);
437    let right_hi_bound =
438        foreign_field_mul::witness::compute_bound(&right_input, &foreign_field_modulus);
439    external_checks.add_limb_check(&left_hi_bound.into());
440    external_checks.add_limb_check(&right_hi_bound.into());
441    gates.connect_cell_pair((15, 2), (25, 0)); // left_bound
442    gates.connect_cell_pair((15, 5), (26, 0)); // right_bound
443
444    external_checks.extend_witness_limb_checks(&mut witness);
445
446    // Temporary workaround for lookup-table/domain-size issue
447    for _ in 0..(1 << 13) {
448        gates.push(CircuitGate::zero(Wire::for_row(next_row)));
449        next_row += 1;
450    }
451
452    // Create constraint system
453    let cs = ConstraintSystem::<Fp>::create(gates)
454        .lazy_mode(lazy_mode)
455        .build()
456        .unwrap();
457
458    srs.0.with_lagrange_basis(cs.domain.d1);
459
460    let (endo_q, _endo_r) = endos::<Pallas>();
461    let index = ProverIndex::<Vesta, OpeningProof<Vesta>>::create(cs, endo_q, srs.0, lazy_mode);
462    let group_map = <Vesta as CommitmentCurve>::Map::setup();
463    let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
464        &group_map,
465        witness,
466        &[],
467        &index,
468        vec![],
469        None,
470        &mut rand::rngs::OsRng,
471    )
472    .unwrap();
473    (
474        CamlPastaFpPlonkIndex(Box::new(index)),
475        (proof, vec![]).into(),
476    )
477}
478
479#[ocaml_gen::func]
480#[ocaml::func]
481pub fn caml_pasta_fp_plonk_proof_example_with_range_check(
482    srs: CamlFpSrs,
483    lazy_mode: bool,
484) -> (
485    CamlPastaFpPlonkIndex,
486    CamlProofWithPublic<CamlGVesta, CamlFp>,
487) {
488    use ark_ff::Zero;
489    use kimchi::circuits::{
490        constraints::ConstraintSystem,
491        gate::CircuitGate,
492        polynomials::{foreign_field_common::BigUintForeignFieldHelpers, range_check},
493        wires::Wire,
494    };
495    use num_bigint::{BigUint, RandBigInt};
496    use o1_utils::BigUintFieldHelpers;
497    use poly_commitment::ipa::endos;
498    use rand::{rngs::StdRng, SeedableRng};
499
500    let rng = &mut StdRng::from_seed([255u8; 32]);
501
502    // Create range-check gadget
503    let (mut next_row, mut gates) = CircuitGate::<Fp>::create_multi_range_check(0);
504
505    // Create witness
506    let witness = range_check::witness::create_multi::<Fp>(
507        rng.gen_biguint_range(&BigUint::zero(), &BigUint::two_to_limb())
508            .to_field()
509            .expect("failed to convert to field"),
510        rng.gen_biguint_range(&BigUint::zero(), &BigUint::two_to_limb())
511            .to_field()
512            .expect("failed to convert to field"),
513        rng.gen_biguint_range(&BigUint::zero(), &BigUint::two_to_limb())
514            .to_field()
515            .expect("failed to convert to field"),
516    );
517
518    // Temporary workaround for lookup-table/domain-size issue
519    for _ in 0..(1 << 13) {
520        gates.push(CircuitGate::zero(Wire::for_row(next_row)));
521        next_row += 1;
522    }
523
524    // Create constraint system
525    let cs = ConstraintSystem::<Fp>::create(gates)
526        .lazy_mode(lazy_mode)
527        .build()
528        .unwrap();
529
530    srs.0.with_lagrange_basis(cs.domain.d1);
531
532    let (endo_q, _endo_r) = endos::<Pallas>();
533    let index = ProverIndex::<Vesta, OpeningProof<Vesta>>::create(cs, endo_q, srs.0, lazy_mode);
534    let group_map = <Vesta as CommitmentCurve>::Map::setup();
535    let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
536        &group_map,
537        witness,
538        &[],
539        &index,
540        vec![],
541        None,
542        &mut rand::rngs::OsRng,
543    )
544    .unwrap();
545    (
546        CamlPastaFpPlonkIndex(Box::new(index)),
547        (proof, vec![]).into(),
548    )
549}
550
551#[ocaml_gen::func]
552#[ocaml::func]
553pub fn caml_pasta_fp_plonk_proof_example_with_range_check0(
554    srs: CamlFpSrs,
555    lazy_mode: bool,
556) -> (
557    CamlPastaFpPlonkIndex,
558    CamlProofWithPublic<CamlGVesta, CamlFp>,
559) {
560    use ark_ff::Zero;
561    use kimchi::circuits::{
562        constraints::ConstraintSystem,
563        gate::{CircuitGate, Connect},
564        polynomial::COLUMNS,
565        polynomials::{generic::GenericGateSpec, range_check},
566        wires::Wire,
567    };
568    use poly_commitment::ipa::endos;
569
570    let gates = {
571        // Public input row with value 0
572        let mut gates = vec![CircuitGate::<Fp>::create_generic_gadget(
573            Wire::for_row(0),
574            GenericGateSpec::Const(Fp::zero()),
575            None,
576        )];
577        let mut row = 1;
578        CircuitGate::<Fp>::extend_range_check(&mut gates, &mut row);
579
580        // Temporary workaround for lookup-table/domain-size issue
581        for _ in 0..(1 << 13) {
582            gates.push(CircuitGate::zero(Wire::for_row(gates.len())));
583        }
584
585        // Connect the zero row to the range-check row to check prefix are zeros
586        gates.connect_64bit(0, 1);
587
588        gates
589    };
590
591    // witness
592    let witness = {
593        // create row for the zero value
594        let mut witness: [_; COLUMNS] = core::array::from_fn(|_col| vec![Fp::zero(); 1]);
595        // create row for the 64-bit value
596        range_check::witness::extend_single(&mut witness, Fp::from(2u128.pow(64) - 1));
597        witness
598    };
599
600    // not sure if theres a smarter way instead of the double unwrap, but should be fine in the test
601    let cs = ConstraintSystem::<Fp>::create(gates)
602        .lazy_mode(lazy_mode)
603        .build()
604        .unwrap();
605
606    srs.0.with_lagrange_basis(cs.domain.d1);
607
608    let (endo_q, _endo_r) = endos::<Pallas>();
609    let index = ProverIndex::<Vesta, OpeningProof<Vesta>>::create(cs, endo_q, srs.0, lazy_mode);
610    let group_map = <Vesta as CommitmentCurve>::Map::setup();
611    let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
612        &group_map,
613        witness,
614        &[],
615        &index,
616        vec![],
617        None,
618        &mut rand::rngs::OsRng,
619    )
620    .unwrap();
621    (
622        CamlPastaFpPlonkIndex(Box::new(index)),
623        (proof, vec![]).into(),
624    )
625}
626
627#[ocaml_gen::func]
628#[ocaml::func]
629pub fn caml_pasta_fp_plonk_proof_example_with_ffadd(
630    srs: CamlFpSrs,
631    lazy_mode: bool,
632) -> (
633    CamlPastaFpPlonkIndex,
634    CamlFp,
635    CamlProofWithPublic<CamlGVesta, CamlFp>,
636) {
637    use ark_ff::Zero;
638    use kimchi::circuits::{
639        constraints::ConstraintSystem,
640        gate::{CircuitGate, Connect},
641        polynomial::COLUMNS,
642        polynomials::{
643            foreign_field_add::witness::{create_chain, FFOps},
644            generic::GenericGateSpec,
645            range_check,
646        },
647        wires::Wire,
648    };
649    use num_bigint::BigUint;
650    use poly_commitment::ipa::endos;
651
652    // Includes a row to store value 1
653    let num_public_inputs = 1;
654    let operation = &[FFOps::Add];
655    let modulus = BigUint::from_bytes_be(&[
656        0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFE, 0xFF, 0xFF, 0xFF, 0xFF,
657        0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFE, 0xFF, 0xFF,
658        0xFC, 0x2F,
659    ]);
660
661    // circuit
662    // [0]       -> Public input row to store the value 1
663    // [1]       -> 1 ForeignFieldAdd row
664    // [2]       -> 1 ForeignFieldAdd row for final bound
665    // [3]       -> 1 Zero row for bound result
666    // [4..=7]   -> 1 Multi RangeCheck for left input
667    // [8..=11]  -> 1 Multi RangeCheck for right input
668    // [12..=15] -> 1 Multi RangeCheck for result
669    // [16..=19] -> 1 Multi RangeCheck for bound check
670    let gates = {
671        // Public input row
672        let mut gates = vec![CircuitGate::<Fp>::create_generic_gadget(
673            Wire::for_row(0),
674            GenericGateSpec::Pub,
675            None,
676        )];
677
678        let mut curr_row = num_public_inputs;
679        // Foreign field addition and bound check
680        CircuitGate::<Fp>::extend_chain_ffadd(&mut gates, 0, &mut curr_row, operation, &modulus);
681
682        // Extend rangechecks of left input, right input, result, and bound
683        for _ in 0..4 {
684            CircuitGate::extend_multi_range_check(&mut gates, &mut curr_row);
685        }
686        // Connect the witnesses of the addition to the corresponding range
687        // checks
688        gates.connect_ffadd_range_checks(1, Some(4), Some(8), 12);
689        // Connect the bound check range checks
690        gates.connect_ffadd_range_checks(2, None, None, 16);
691
692        // Temporary workaround for lookup-table/domain-size issue
693        for _ in 0..(1 << 13) {
694            gates.push(CircuitGate::zero(Wire::for_row(curr_row)));
695            curr_row += 1;
696        }
697
698        gates
699    };
700
701    // witness
702    let witness = {
703        // create row for the public value 1
704        let mut witness: [_; COLUMNS] = core::array::from_fn(|_col| vec![Fp::zero(); 1]);
705        witness[0][0] = Fp::one();
706        // create inputs to the addition
707        let left = modulus.clone() - BigUint::from_bytes_be(&[1]);
708        let right = modulus.clone() - BigUint::from_bytes_be(&[1]);
709        // create a chain of 1 addition
710        let add_witness = create_chain::<Fp>(&[left, right], operation, modulus);
711        for col in 0..COLUMNS {
712            witness[col].extend(add_witness[col].iter());
713        }
714        // extend range checks for all of left, right, output, and bound
715        let left = (witness[0][1], witness[1][1], witness[2][1]);
716        range_check::witness::extend_multi(&mut witness, left.0, left.1, left.2);
717        let right = (witness[3][1], witness[4][1], witness[5][1]);
718        range_check::witness::extend_multi(&mut witness, right.0, right.1, right.2);
719        let output = (witness[0][2], witness[1][2], witness[2][2]);
720        range_check::witness::extend_multi(&mut witness, output.0, output.1, output.2);
721        let bound = (witness[0][3], witness[1][3], witness[2][3]);
722        range_check::witness::extend_multi(&mut witness, bound.0, bound.1, bound.2);
723        witness
724    };
725
726    // not sure if theres a smarter way instead of the double unwrap, but should
727    // be fine in the test
728    let cs = ConstraintSystem::<Fp>::create(gates)
729        .public(num_public_inputs)
730        .lazy_mode(lazy_mode)
731        .build()
732        .unwrap();
733
734    srs.0.with_lagrange_basis(cs.domain.d1);
735
736    let (endo_q, _endo_r) = endos::<Pallas>();
737    let index = ProverIndex::<Vesta, OpeningProof<Vesta>>::create(cs, endo_q, srs.0, lazy_mode);
738    let group_map = <Vesta as CommitmentCurve>::Map::setup();
739    let public_input = witness[0][0];
740    let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
741        &group_map,
742        witness,
743        &[],
744        &index,
745        vec![],
746        None,
747        &mut rand::rngs::OsRng,
748    )
749    .unwrap();
750    (
751        CamlPastaFpPlonkIndex(Box::new(index)),
752        public_input.into(),
753        (proof, vec![public_input]).into(),
754    )
755}
756
757#[ocaml_gen::func]
758#[ocaml::func]
759pub fn caml_pasta_fp_plonk_proof_example_with_xor(
760    srs: CamlFpSrs,
761    lazy_mode: bool,
762) -> (
763    CamlPastaFpPlonkIndex,
764    (CamlFp, CamlFp),
765    CamlProofWithPublic<CamlGVesta, CamlFp>,
766) {
767    use ark_ff::Zero;
768    use kimchi::circuits::{
769        constraints::ConstraintSystem,
770        gate::{CircuitGate, Connect},
771        polynomial::COLUMNS,
772        polynomials::{generic::GenericGateSpec, xor},
773        wires::Wire,
774    };
775    use poly_commitment::ipa::endos;
776
777    let num_public_inputs = 2;
778
779    // circuit
780    let gates = {
781        // public inputs
782        let mut gates = vec![];
783        for row in 0..num_public_inputs {
784            gates.push(CircuitGate::<Fp>::create_generic_gadget(
785                Wire::for_row(row),
786                GenericGateSpec::Pub,
787                None,
788            ));
789        }
790        // 1 XOR of 128 bits. This will create 8 Xor16 gates and a Generic final
791        // gate with all zeros.
792        CircuitGate::<Fp>::extend_xor_gadget(&mut gates, 128);
793        // connect public inputs to the inputs of the XOR
794        gates.connect_cell_pair((0, 0), (2, 0));
795        gates.connect_cell_pair((1, 0), (2, 1));
796
797        // Temporary workaround for lookup-table/domain-size issue
798        for _ in 0..(1 << 13) {
799            gates.push(CircuitGate::zero(Wire::for_row(gates.len())));
800        }
801        gates
802    };
803
804    // witness
805    let witness = {
806        let mut cols: [_; COLUMNS] =
807            core::array::from_fn(|_col| vec![Fp::zero(); num_public_inputs]);
808
809        // initialize the 2 inputs
810        let input1 = 0xDC811727DAF22EC15927D6AA275F406Bu128;
811        let input2 = 0xA4F4417AF072DF9016A1EAB458DA80D1u128;
812        cols[0][0] = input1.into();
813        cols[0][1] = input2.into();
814
815        xor::extend_xor_witness::<Fp>(&mut cols, input1.into(), input2.into(), 128);
816        cols
817    };
818
819    // not sure if theres a smarter way instead of the double unwrap, but should
820    // be fine in the test
821    let cs = ConstraintSystem::<Fp>::create(gates)
822        .public(num_public_inputs)
823        .lazy_mode(lazy_mode)
824        .build()
825        .unwrap();
826
827    srs.0.with_lagrange_basis(cs.domain.d1);
828
829    let (endo_q, _endo_r) = endos::<Pallas>();
830    let index = ProverIndex::<Vesta, OpeningProof<Vesta>>::create(cs, endo_q, srs.0, lazy_mode);
831    let group_map = <Vesta as CommitmentCurve>::Map::setup();
832    let public_input = (witness[0][0], witness[0][1]);
833    let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
834        &group_map,
835        witness,
836        &[],
837        &index,
838        vec![],
839        None,
840        &mut rand::rngs::OsRng,
841    )
842    .unwrap();
843    (
844        CamlPastaFpPlonkIndex(Box::new(index)),
845        (public_input.0.into(), public_input.1.into()),
846        (proof, vec![public_input.0, public_input.1]).into(),
847    )
848}
849
850#[ocaml_gen::func]
851#[ocaml::func]
852pub fn caml_pasta_fp_plonk_proof_example_with_rot(
853    srs: CamlFpSrs,
854    lazy_mode: bool,
855) -> (
856    CamlPastaFpPlonkIndex,
857    (CamlFp, CamlFp),
858    CamlProofWithPublic<CamlGVesta, CamlFp>,
859) {
860    use ark_ff::Zero;
861    use kimchi::circuits::{
862        constraints::ConstraintSystem,
863        gate::{CircuitGate, Connect},
864        polynomial::COLUMNS,
865        polynomials::{
866            generic::GenericGateSpec,
867            rot::{self, RotMode},
868        },
869        wires::Wire,
870    };
871    use poly_commitment::ipa::endos;
872
873    // Includes the actual input of the rotation and a row with the zero value
874    let num_public_inputs = 2;
875    // 1 ROT of 32 to the left
876    let rot = 32;
877    let mode = RotMode::Left;
878
879    // circuit
880    let gates = {
881        let mut gates = vec![];
882        // public inputs
883        for row in 0..num_public_inputs {
884            gates.push(CircuitGate::<Fp>::create_generic_gadget(
885                Wire::for_row(row),
886                GenericGateSpec::Pub,
887                None,
888            ));
889        }
890        CircuitGate::<Fp>::extend_rot(&mut gates, rot, mode, 1);
891        // connect first public input to the word of the ROT
892        gates.connect_cell_pair((0, 0), (2, 0));
893
894        // Temporary workaround for lookup-table/domain-size issue
895        for _ in 0..(1 << 13) {
896            gates.push(CircuitGate::zero(Wire::for_row(gates.len())));
897        }
898
899        gates
900    };
901
902    // witness
903    let witness = {
904        // create one row for the public word
905        let mut cols: [_; COLUMNS] = core::array::from_fn(|_col| vec![Fp::zero(); 2]);
906
907        // initialize the public input containing the word to be rotated
908        let input = 0xDC811727DAF22EC1u64;
909        cols[0][0] = input.into();
910        rot::extend_rot::<Fp>(&mut cols, input, rot, mode);
911
912        cols
913    };
914
915    // not sure if theres a smarter way instead of the double unwrap, but should
916    // be fine in the test
917    let cs = ConstraintSystem::<Fp>::create(gates)
918        .public(num_public_inputs)
919        .lazy_mode(lazy_mode)
920        .build()
921        .unwrap();
922
923    srs.0.with_lagrange_basis(cs.domain.d1);
924
925    let (endo_q, _endo_r) = endos::<Pallas>();
926    let index = ProverIndex::<Vesta, OpeningProof<Vesta>>::create(cs, endo_q, srs.0, lazy_mode);
927    let group_map = <Vesta as CommitmentCurve>::Map::setup();
928    let public_input = (witness[0][0], witness[0][1]);
929    let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
930        &group_map,
931        witness,
932        &[],
933        &index,
934        vec![],
935        None,
936        &mut rand::rngs::OsRng,
937    )
938    .unwrap();
939    (
940        CamlPastaFpPlonkIndex(Box::new(index)),
941        (public_input.0.into(), public_input.1.into()),
942        (proof, vec![public_input.0, public_input.1]).into(),
943    )
944}
945
946#[ocaml_gen::func]
947#[ocaml::func]
948pub fn caml_pasta_fp_plonk_proof_verify(
949    index: CamlPastaFpPlonkVerifierIndex,
950    proof: CamlProofWithPublic<CamlGVesta, CamlFp>,
951) -> bool {
952    let group_map = <Vesta as CommitmentCurve>::Map::setup();
953
954    let (proof, public_input) = proof.into();
955    let verifier_index = index.into();
956    let context = Context {
957        verifier_index: &verifier_index,
958        proof: &proof,
959        public_input: &public_input,
960    };
961
962    batch_verify::<
963        Vesta,
964        DefaultFqSponge<VestaParameters, PlonkSpongeConstantsKimchi>,
965        DefaultFrSponge<Fp, PlonkSpongeConstantsKimchi>,
966        OpeningProof<Vesta>,
967    >(&group_map, &[context])
968    .is_ok()
969}
970
971#[ocaml_gen::func]
972#[ocaml::func]
973pub fn caml_pasta_fp_plonk_proof_batch_verify(
974    indexes: Vec<CamlPastaFpPlonkVerifierIndex>,
975    proofs: Vec<CamlProofWithPublic<CamlGVesta, CamlFp>>,
976) -> bool {
977    let ts: Vec<_> = indexes
978        .into_iter()
979        .zip(proofs.into_iter())
980        .map(|(caml_index, caml_proof)| {
981            let verifier_index: VerifierIndex<Vesta, OpeningProof<Vesta>> = caml_index.into();
982            let (proof, public_input): (ProverProof<Vesta, OpeningProof<Vesta>>, Vec<_>) =
983                caml_proof.into();
984            (verifier_index, proof, public_input)
985        })
986        .collect();
987    let ts_ref: Vec<Context<Vesta, OpeningProof<Vesta>>> = ts
988        .iter()
989        .map(|(verifier_index, proof, public_input)| Context {
990            verifier_index,
991            proof,
992            public_input,
993        })
994        .collect();
995    let group_map = GroupMap::<Fq>::setup();
996
997    batch_verify::<
998        Vesta,
999        DefaultFqSponge<VestaParameters, PlonkSpongeConstantsKimchi>,
1000        DefaultFrSponge<Fp, PlonkSpongeConstantsKimchi>,
1001        OpeningProof<Vesta>,
1002    >(&group_map, &ts_ref)
1003    .is_ok()
1004}
1005
1006#[ocaml_gen::func]
1007#[ocaml::func]
1008pub fn caml_pasta_fp_plonk_proof_dummy() -> CamlProofWithPublic<CamlGVesta, CamlFp> {
1009    fn comm() -> PolyComm<Vesta> {
1010        let g = Vesta::generator();
1011        PolyComm {
1012            chunks: vec![g, g, g],
1013        }
1014    }
1015
1016    let prev = RecursionChallenge {
1017        chals: vec![Fp::one(), Fp::one()],
1018        comm: comm(),
1019    };
1020    let prev_challenges = vec![prev.clone(), prev.clone(), prev];
1021
1022    let g = Vesta::generator();
1023    let proof = OpeningProof {
1024        lr: vec![(g, g), (g, g), (g, g)],
1025        z1: Fp::one(),
1026        z2: Fp::one(),
1027        delta: g,
1028        sg: g,
1029    };
1030    let eval = || PointEvaluations {
1031        zeta: vec![Fp::one()],
1032        zeta_omega: vec![Fp::one()],
1033    };
1034    let evals = ProofEvaluations {
1035        public: Some(eval()),
1036        w: core::array::from_fn(|_| eval()),
1037        coefficients: core::array::from_fn(|_| eval()),
1038        z: eval(),
1039        s: core::array::from_fn(|_| eval()),
1040        generic_selector: eval(),
1041        poseidon_selector: eval(),
1042        complete_add_selector: eval(),
1043        mul_selector: eval(),
1044        emul_selector: eval(),
1045        endomul_scalar_selector: eval(),
1046        range_check0_selector: None,
1047        range_check1_selector: None,
1048        foreign_field_add_selector: None,
1049        foreign_field_mul_selector: None,
1050        xor_selector: None,
1051        rot_selector: None,
1052        lookup_aggregation: None,
1053        lookup_table: None,
1054        lookup_sorted: array::from_fn(|_| None),
1055        runtime_lookup_table: None,
1056        runtime_lookup_table_selector: None,
1057        xor_lookup_selector: None,
1058        lookup_gate_lookup_selector: None,
1059        range_check_lookup_selector: None,
1060        foreign_field_mul_lookup_selector: None,
1061    };
1062
1063    let public = vec![Fp::one(), Fp::one()];
1064    let dlogproof = ProverProof {
1065        commitments: ProverCommitments {
1066            w_comm: core::array::from_fn(|_| comm()),
1067            z_comm: comm(),
1068            t_comm: comm(),
1069            lookup: None,
1070        },
1071        proof,
1072        evals,
1073        ft_eval1: Fp::one(),
1074        prev_challenges,
1075    };
1076
1077    (dlogproof, public).into()
1078}
1079
1080#[ocaml_gen::func]
1081#[ocaml::func]
1082pub fn caml_pasta_fp_plonk_proof_deep_copy(
1083    x: CamlProofWithPublic<CamlGVesta, CamlFp>,
1084) -> CamlProofWithPublic<CamlGVesta, CamlFp> {
1085    x
1086}