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

kimchi_stubs/
pasta_fp_plonk_proof.rs
