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

kimchi_stubs/
pasta_fp_plonk_proof.rs
