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

kimchi_stubs/
pasta_fp_plonk_proof.rs
