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

kimchi_stubs/
pasta_fp_plonk_proof.rs
