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    sponge::{DefaultFqSponge, DefaultFrSponge},
29};
30use poly_commitment::{
31    commitment::{CommitmentCurve, PolyComm},
32    ipa::OpeningProof,
33    lagrange_basis::WithLagrangeBasis,
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    let public_input = witness[0][0..index.cs.public].to_vec();
86
87    if std::env::var("KIMCHI_PROVER_DUMP_ARGUMENTS").is_ok() {
88        kimchi::bench::bench_arguments_dump_into_file(&index.cs, &witness, &runtime_tables, &prev);
89    }
90
91    let runtime = unsafe { ocaml::Runtime::recover_handle() };
95
96    runtime.releasing_runtime(|| {
98        let group_map = GroupMap::<Fq>::setup();
99        let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
100            &group_map,
101            witness,
102            &runtime_tables,
103            index,
104            prev,
105            None,
106            &mut rand::rngs::OsRng,
107        )
108        .map_err(|e| ocaml::Error::Error(e.into()))?;
109        Ok((proof, public_input).into())
110    })
111}
112
113#[ocaml_gen::func]
114#[ocaml::func]
115pub fn caml_pasta_fp_plonk_proof_create_and_verify(
116    index: CamlPastaFpPlonkIndexPtr<'static>,
117    witness: Vec<CamlFpVector>,
118    runtime_tables: Vec<CamlRuntimeTable<CamlFp>>,
119    prev_challenges: Vec<CamlFp>,
120    prev_sgs: Vec<CamlGVesta>,
121) -> Result<CamlProofWithPublic<CamlGVesta, CamlFp>, ocaml::Error> {
122    {
123        index
124            .as_ref()
125            .0
126            .srs
127            .with_lagrange_basis(index.as_ref().0.cs.domain.d1);
128    }
129    let prev = if prev_challenges.is_empty() {
130        Vec::new()
131    } else {
132        let challenges_per_sg = prev_challenges.len() / prev_sgs.len();
133        prev_sgs
134            .into_iter()
135            .map(Into::<Vesta>::into)
136            .enumerate()
137            .map(|(i, sg)| {
138                let chals = prev_challenges[(i * challenges_per_sg)..(i + 1) * challenges_per_sg]
139                    .iter()
140                    .map(Into::<Fp>::into)
141                    .collect();
142                let comm = PolyComm::<Vesta> { chunks: vec![sg] };
143                RecursionChallenge { chals, comm }
144            })
145            .collect()
146    };
147
148    let witness: Vec<Vec<_>> = witness.iter().map(|x| (**x).clone()).collect();
149    let witness: [Vec<_>; COLUMNS] = witness
150        .try_into()
151        .map_err(|_| ocaml::Error::Message("the witness should be a column of 15 vectors"))?;
152    let index: &ProverIndex<Vesta, OpeningProof<Vesta>> = &index.as_ref().0;
153    let runtime_tables: Vec<RuntimeTable<Fp>> =
154        runtime_tables.into_iter().map(Into::into).collect();
155
156    let public_input = witness[0][0..index.cs.public].to_vec();
158
159    let runtime = unsafe { ocaml::Runtime::recover_handle() };
163
164    runtime.releasing_runtime(|| {
166        let group_map = GroupMap::<Fq>::setup();
167        let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
168            &group_map,
169            witness,
170            &runtime_tables,
171            index,
172            prev,
173            None,
174            &mut rand::rngs::OsRng,
175        )
176        .map_err(|e| ocaml::Error::Error(e.into()))?;
177
178        let verifier_index = index.verifier_index();
179
180        verify::<Vesta, EFqSponge, EFrSponge, OpeningProof<Vesta>>(
182            &group_map,
183            &verifier_index,
184            &proof,
185            &public_input,
186        )?;
187
188        Ok((proof, public_input).into())
189    })
190}
191
192#[ocaml_gen::func]
193#[ocaml::func]
194pub fn caml_pasta_fp_plonk_proof_example_with_lookup(
195    srs: CamlFpSrs,
196    lazy_mode: bool,
197) -> (
198    CamlPastaFpPlonkIndex,
199    CamlFp,
200    CamlProofWithPublic<CamlGVesta, CamlFp>,
201) {
202    use ark_ff::Zero;
203    use kimchi::circuits::{
204        constraints::ConstraintSystem,
205        gate::{CircuitGate, GateType},
206        lookup::{
207            runtime_tables::{RuntimeTable, RuntimeTableCfg},
208            tables::LookupTable,
209        },
210        polynomial::COLUMNS,
211        wires::Wire,
212    };
213    use poly_commitment::ipa::endos;
214
215    let num_gates = 1000;
216    let num_tables: usize = 5;
217
218    let fixed_tables = vec![LookupTable {
220        id: 0,
221        data: vec![vec![0, 0, 0, 0, 0].into_iter().map(Into::into).collect()],
222    }];
223
224    let mut runtime_tables_setup = vec![];
225    let first_column: Vec<_> = [8u32, 9, 8, 7, 1].into_iter().map(Into::into).collect();
226    for table_id in 0..num_tables {
227        let cfg = RuntimeTableCfg {
228            id: table_id as i32,
229            first_column: first_column.clone(),
230        };
231        runtime_tables_setup.push(cfg);
232    }
233
234    let data: Vec<Fp> = [0u32, 2, 3, 4, 5].into_iter().map(Into::into).collect();
235    let runtime_tables: Vec<RuntimeTable<Fp>> = runtime_tables_setup
236        .iter()
237        .map(|cfg| RuntimeTable {
238            id: cfg.id(),
239            data: data.clone(),
240        })
241        .collect();
242
243    let mut gates = vec![];
245    for row in 0..num_gates {
246        gates.push(CircuitGate {
247            typ: GateType::Lookup,
248            wires: Wire::for_row(row),
249            coeffs: vec![],
250        });
251    }
252
253    let witness = {
255        let mut cols: [_; COLUMNS] = core::array::from_fn(|_col| vec![Fp::zero(); gates.len()]);
256
257        let (lookup_cols, _rest) = cols.split_at_mut(7);
259
260        for row in 0..num_gates {
261            lookup_cols[0][row] = ((row % num_tables) as u64).into();
263
264            let lookup_cols = &mut lookup_cols[1..];
266            for (chunk_id, chunk) in lookup_cols.chunks_mut(2).enumerate() {
267                if (row + chunk_id) % 2 == 0 {
269                    chunk[0][row] = 9u32.into(); chunk[1][row] = 2u32.into(); } else {
272                    chunk[0][row] = 8u32.into(); chunk[1][row] = 3u32.into(); }
275            }
276        }
277        cols
278    };
279
280    let num_public_inputs = 1;
281
282    let cs = ConstraintSystem::<Fp>::create(gates)
284        .runtime(Some(runtime_tables_setup))
285        .lookup(fixed_tables)
286        .public(num_public_inputs)
287        .lazy_mode(lazy_mode)
288        .build()
289        .unwrap();
290
291    srs.0.with_lagrange_basis(cs.domain.d1);
292
293    let (endo_q, _endo_r) = endos::<Pallas>();
294    let index = ProverIndex::<Vesta, OpeningProof<Vesta>>::create(cs, endo_q, srs.0, lazy_mode);
295    let group_map = <Vesta as CommitmentCurve>::Map::setup();
296    let public_input = witness[0][0];
297    let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
298        &group_map,
299        witness,
300        &runtime_tables,
301        &index,
302        vec![],
303        None,
304        &mut rand::rngs::OsRng,
305    )
306    .unwrap();
307
308    let caml_prover_proof = (proof, vec![public_input]).into();
309
310    (
311        CamlPastaFpPlonkIndex(Box::new(index)),
312        public_input.into(),
313        caml_prover_proof,
314    )
315}
316
317#[ocaml_gen::func]
318#[ocaml::func]
319pub fn caml_pasta_fp_plonk_proof_example_with_foreign_field_mul(
320    srs: CamlFpSrs,
321    lazy_mode: bool,
322) -> (
323    CamlPastaFpPlonkIndex,
324    CamlProofWithPublic<CamlGVesta, CamlFp>,
325) {
326    use ark_ff::Zero;
327    use kimchi::circuits::{
328        constraints::ConstraintSystem,
329        gate::{CircuitGate, Connect},
330        polynomials::{foreign_field_common::BigUintForeignFieldHelpers, foreign_field_mul},
331        wires::Wire,
332    };
333    use num_bigint::{BigUint, RandBigInt};
334    use o1_utils::FieldHelpers;
335    use poly_commitment::ipa::endos;
336    use rand::{rngs::StdRng, SeedableRng};
337
338    let foreign_field_modulus = Fq::modulus_biguint();
339
340    let (mut next_row, mut gates) =
355        CircuitGate::<Fp>::create_foreign_field_mul(0, &foreign_field_modulus);
356
357    let rng = &mut StdRng::from_seed([2u8; 32]);
358    let left_input = rng.gen_biguint_range(&BigUint::zero(), &foreign_field_modulus);
359    let right_input = rng.gen_biguint_range(&BigUint::zero(), &foreign_field_modulus);
360
361    let (mut witness, mut external_checks) =
363        foreign_field_mul::witness::create(&left_input, &right_input, &foreign_field_modulus);
364
365    CircuitGate::extend_compact_multi_range_check(&mut gates, &mut next_row);
367    gates.connect_cell_pair((1, 0), (4, 1)); gates.connect_cell_pair((1, 1), (2, 0)); external_checks.extend_witness_compact_multi_range_checks(&mut witness);
370    CircuitGate::extend_high_bounds(&mut gates, &mut next_row, &foreign_field_modulus);
375    gates.connect_cell_pair((6, 0), (1, 1)); external_checks.extend_witness_high_bounds_computation(&mut witness, &foreign_field_modulus);
377
378    CircuitGate::extend_multi_range_check(&mut gates, &mut next_row);
380    gates.connect_cell_pair((1, 2), (7, 0)); gates.connect_cell_pair((1, 3), (8, 0)); gates.connect_cell_pair((1, 4), (9, 0)); CircuitGate::extend_multi_range_check(&mut gates, &mut next_row);
387    gates.connect_cell_pair((1, 5), (11, 0)); gates.connect_cell_pair((0, 6), (12, 0)); gates.connect_cell_pair((1, 6), (13, 0)); external_checks.extend_witness_multi_range_checks(&mut witness);
396
397    let left_limbs = left_input.to_field_limbs();
399    let right_limbs = right_input.to_field_limbs();
400    external_checks.add_high_bound_computation(&left_limbs[2]);
402    external_checks.add_high_bound_computation(&right_limbs[2]);
403    CircuitGate::extend_high_bounds(&mut gates, &mut next_row, &foreign_field_modulus);
404    gates.connect_cell_pair((15, 0), (0, 2)); gates.connect_cell_pair((15, 3), (0, 5)); external_checks.extend_witness_high_bounds_computation(&mut witness, &foreign_field_modulus);
407
408    external_checks.add_multi_range_check(&left_limbs);
410    CircuitGate::extend_multi_range_check(&mut gates, &mut next_row);
411    gates.connect_cell_pair((0, 0), (16, 0)); gates.connect_cell_pair((0, 1), (17, 0)); gates.connect_cell_pair((0, 2), (18, 0)); external_checks.add_multi_range_check(&right_limbs);
418    CircuitGate::extend_multi_range_check(&mut gates, &mut next_row);
419    gates.connect_cell_pair((0, 3), (20, 0)); gates.connect_cell_pair((0, 4), (21, 0)); gates.connect_cell_pair((0, 5), (22, 0)); external_checks.extend_witness_multi_range_checks(&mut witness);
427
428    CircuitGate::extend_multi_range_check(&mut gates, &mut next_row);
431    gates.connect_cell_pair((6, 2), (24, 0)); let left_hi_bound =
436        foreign_field_mul::witness::compute_bound(&left_input, &foreign_field_modulus);
437    let right_hi_bound =
438        foreign_field_mul::witness::compute_bound(&right_input, &foreign_field_modulus);
439    external_checks.add_limb_check(&left_hi_bound.into());
440    external_checks.add_limb_check(&right_hi_bound.into());
441    gates.connect_cell_pair((15, 2), (25, 0)); gates.connect_cell_pair((15, 5), (26, 0)); external_checks.extend_witness_limb_checks(&mut witness);
445
446    for _ in 0..(1 << 13) {
448        gates.push(CircuitGate::zero(Wire::for_row(next_row)));
449        next_row += 1;
450    }
451
452    let cs = ConstraintSystem::<Fp>::create(gates)
454        .lazy_mode(lazy_mode)
455        .build()
456        .unwrap();
457
458    srs.0.with_lagrange_basis(cs.domain.d1);
459
460    let (endo_q, _endo_r) = endos::<Pallas>();
461    let index = ProverIndex::<Vesta, OpeningProof<Vesta>>::create(cs, endo_q, srs.0, lazy_mode);
462    let group_map = <Vesta as CommitmentCurve>::Map::setup();
463    let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
464        &group_map,
465        witness,
466        &[],
467        &index,
468        vec![],
469        None,
470        &mut rand::rngs::OsRng,
471    )
472    .unwrap();
473    (
474        CamlPastaFpPlonkIndex(Box::new(index)),
475        (proof, vec![]).into(),
476    )
477}
478
479#[ocaml_gen::func]
480#[ocaml::func]
481pub fn caml_pasta_fp_plonk_proof_example_with_range_check(
482    srs: CamlFpSrs,
483    lazy_mode: bool,
484) -> (
485    CamlPastaFpPlonkIndex,
486    CamlProofWithPublic<CamlGVesta, CamlFp>,
487) {
488    use ark_ff::Zero;
489    use kimchi::circuits::{
490        constraints::ConstraintSystem,
491        gate::CircuitGate,
492        polynomials::{foreign_field_common::BigUintForeignFieldHelpers, range_check},
493        wires::Wire,
494    };
495    use num_bigint::{BigUint, RandBigInt};
496    use o1_utils::BigUintFieldHelpers;
497    use poly_commitment::ipa::endos;
498    use rand::{rngs::StdRng, SeedableRng};
499
500    let rng = &mut StdRng::from_seed([255u8; 32]);
501
502    let (mut next_row, mut gates) = CircuitGate::<Fp>::create_multi_range_check(0);
504
505    let witness = range_check::witness::create_multi::<Fp>(
507        rng.gen_biguint_range(&BigUint::zero(), &BigUint::two_to_limb())
508            .to_field()
509            .expect("failed to convert to field"),
510        rng.gen_biguint_range(&BigUint::zero(), &BigUint::two_to_limb())
511            .to_field()
512            .expect("failed to convert to field"),
513        rng.gen_biguint_range(&BigUint::zero(), &BigUint::two_to_limb())
514            .to_field()
515            .expect("failed to convert to field"),
516    );
517
518    for _ in 0..(1 << 13) {
520        gates.push(CircuitGate::zero(Wire::for_row(next_row)));
521        next_row += 1;
522    }
523
524    let cs = ConstraintSystem::<Fp>::create(gates)
526        .lazy_mode(lazy_mode)
527        .build()
528        .unwrap();
529
530    srs.0.with_lagrange_basis(cs.domain.d1);
531
532    let (endo_q, _endo_r) = endos::<Pallas>();
533    let index = ProverIndex::<Vesta, OpeningProof<Vesta>>::create(cs, endo_q, srs.0, lazy_mode);
534    let group_map = <Vesta as CommitmentCurve>::Map::setup();
535    let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
536        &group_map,
537        witness,
538        &[],
539        &index,
540        vec![],
541        None,
542        &mut rand::rngs::OsRng,
543    )
544    .unwrap();
545    (
546        CamlPastaFpPlonkIndex(Box::new(index)),
547        (proof, vec![]).into(),
548    )
549}
550
551#[ocaml_gen::func]
552#[ocaml::func]
553pub fn caml_pasta_fp_plonk_proof_example_with_range_check0(
554    srs: CamlFpSrs,
555    lazy_mode: bool,
556) -> (
557    CamlPastaFpPlonkIndex,
558    CamlProofWithPublic<CamlGVesta, CamlFp>,
559) {
560    use ark_ff::Zero;
561    use kimchi::circuits::{
562        constraints::ConstraintSystem,
563        gate::{CircuitGate, Connect},
564        polynomial::COLUMNS,
565        polynomials::{generic::GenericGateSpec, range_check},
566        wires::Wire,
567    };
568    use poly_commitment::ipa::endos;
569
570    let gates = {
571        let mut gates = vec![CircuitGate::<Fp>::create_generic_gadget(
573            Wire::for_row(0),
574            GenericGateSpec::Const(Fp::zero()),
575            None,
576        )];
577        let mut row = 1;
578        CircuitGate::<Fp>::extend_range_check(&mut gates, &mut row);
579
580        for _ in 0..(1 << 13) {
582            gates.push(CircuitGate::zero(Wire::for_row(gates.len())));
583        }
584
585        gates.connect_64bit(0, 1);
587
588        gates
589    };
590
591    let witness = {
593        let mut witness: [_; COLUMNS] = core::array::from_fn(|_col| vec![Fp::zero(); 1]);
595        range_check::witness::extend_single(&mut witness, Fp::from(2u128.pow(64) - 1));
597        witness
598    };
599
600    let cs = ConstraintSystem::<Fp>::create(gates)
602        .lazy_mode(lazy_mode)
603        .build()
604        .unwrap();
605
606    srs.0.with_lagrange_basis(cs.domain.d1);
607
608    let (endo_q, _endo_r) = endos::<Pallas>();
609    let index = ProverIndex::<Vesta, OpeningProof<Vesta>>::create(cs, endo_q, srs.0, lazy_mode);
610    let group_map = <Vesta as CommitmentCurve>::Map::setup();
611    let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
612        &group_map,
613        witness,
614        &[],
615        &index,
616        vec![],
617        None,
618        &mut rand::rngs::OsRng,
619    )
620    .unwrap();
621    (
622        CamlPastaFpPlonkIndex(Box::new(index)),
623        (proof, vec![]).into(),
624    )
625}
626
627#[ocaml_gen::func]
628#[ocaml::func]
629pub fn caml_pasta_fp_plonk_proof_example_with_ffadd(
630    srs: CamlFpSrs,
631    lazy_mode: bool,
632) -> (
633    CamlPastaFpPlonkIndex,
634    CamlFp,
635    CamlProofWithPublic<CamlGVesta, CamlFp>,
636) {
637    use ark_ff::Zero;
638    use kimchi::circuits::{
639        constraints::ConstraintSystem,
640        gate::{CircuitGate, Connect},
641        polynomial::COLUMNS,
642        polynomials::{
643            foreign_field_add::witness::{create_chain, FFOps},
644            generic::GenericGateSpec,
645            range_check,
646        },
647        wires::Wire,
648    };
649    use num_bigint::BigUint;
650    use poly_commitment::ipa::endos;
651
652    let num_public_inputs = 1;
654    let operation = &[FFOps::Add];
655    let modulus = BigUint::from_bytes_be(&[
656        0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFE, 0xFF, 0xFF, 0xFF, 0xFF,
657        0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFE, 0xFF, 0xFF,
658        0xFC, 0x2F,
659    ]);
660
661    let gates = {
671        let mut gates = vec![CircuitGate::<Fp>::create_generic_gadget(
673            Wire::for_row(0),
674            GenericGateSpec::Pub,
675            None,
676        )];
677
678        let mut curr_row = num_public_inputs;
679        CircuitGate::<Fp>::extend_chain_ffadd(&mut gates, 0, &mut curr_row, operation, &modulus);
681
682        for _ in 0..4 {
684            CircuitGate::extend_multi_range_check(&mut gates, &mut curr_row);
685        }
686        gates.connect_ffadd_range_checks(1, Some(4), Some(8), 12);
689        gates.connect_ffadd_range_checks(2, None, None, 16);
691
692        for _ in 0..(1 << 13) {
694            gates.push(CircuitGate::zero(Wire::for_row(curr_row)));
695            curr_row += 1;
696        }
697
698        gates
699    };
700
701    let witness = {
703        let mut witness: [_; COLUMNS] = core::array::from_fn(|_col| vec![Fp::zero(); 1]);
705        witness[0][0] = Fp::one();
706        let left = modulus.clone() - BigUint::from_bytes_be(&[1]);
708        let right = modulus.clone() - BigUint::from_bytes_be(&[1]);
709        let add_witness = create_chain::<Fp>(&[left, right], operation, modulus);
711        for col in 0..COLUMNS {
712            witness[col].extend(add_witness[col].iter());
713        }
714        let left = (witness[0][1], witness[1][1], witness[2][1]);
716        range_check::witness::extend_multi(&mut witness, left.0, left.1, left.2);
717        let right = (witness[3][1], witness[4][1], witness[5][1]);
718        range_check::witness::extend_multi(&mut witness, right.0, right.1, right.2);
719        let output = (witness[0][2], witness[1][2], witness[2][2]);
720        range_check::witness::extend_multi(&mut witness, output.0, output.1, output.2);
721        let bound = (witness[0][3], witness[1][3], witness[2][3]);
722        range_check::witness::extend_multi(&mut witness, bound.0, bound.1, bound.2);
723        witness
724    };
725
726    let cs = ConstraintSystem::<Fp>::create(gates)
729        .public(num_public_inputs)
730        .lazy_mode(lazy_mode)
731        .build()
732        .unwrap();
733
734    srs.0.with_lagrange_basis(cs.domain.d1);
735
736    let (endo_q, _endo_r) = endos::<Pallas>();
737    let index = ProverIndex::<Vesta, OpeningProof<Vesta>>::create(cs, endo_q, srs.0, lazy_mode);
738    let group_map = <Vesta as CommitmentCurve>::Map::setup();
739    let public_input = witness[0][0];
740    let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
741        &group_map,
742        witness,
743        &[],
744        &index,
745        vec![],
746        None,
747        &mut rand::rngs::OsRng,
748    )
749    .unwrap();
750    (
751        CamlPastaFpPlonkIndex(Box::new(index)),
752        public_input.into(),
753        (proof, vec![public_input]).into(),
754    )
755}
756
757#[ocaml_gen::func]
758#[ocaml::func]
759pub fn caml_pasta_fp_plonk_proof_example_with_xor(
760    srs: CamlFpSrs,
761    lazy_mode: bool,
762) -> (
763    CamlPastaFpPlonkIndex,
764    (CamlFp, CamlFp),
765    CamlProofWithPublic<CamlGVesta, CamlFp>,
766) {
767    use ark_ff::Zero;
768    use kimchi::circuits::{
769        constraints::ConstraintSystem,
770        gate::{CircuitGate, Connect},
771        polynomial::COLUMNS,
772        polynomials::{generic::GenericGateSpec, xor},
773        wires::Wire,
774    };
775    use poly_commitment::ipa::endos;
776
777    let num_public_inputs = 2;
778
779    let gates = {
781        let mut gates = vec![];
783        for row in 0..num_public_inputs {
784            gates.push(CircuitGate::<Fp>::create_generic_gadget(
785                Wire::for_row(row),
786                GenericGateSpec::Pub,
787                None,
788            ));
789        }
790        CircuitGate::<Fp>::extend_xor_gadget(&mut gates, 128);
793        gates.connect_cell_pair((0, 0), (2, 0));
795        gates.connect_cell_pair((1, 0), (2, 1));
796
797        for _ in 0..(1 << 13) {
799            gates.push(CircuitGate::zero(Wire::for_row(gates.len())));
800        }
801        gates
802    };
803
804    let witness = {
806        let mut cols: [_; COLUMNS] =
807            core::array::from_fn(|_col| vec![Fp::zero(); num_public_inputs]);
808
809        let input1 = 0xDC811727DAF22EC15927D6AA275F406Bu128;
811        let input2 = 0xA4F4417AF072DF9016A1EAB458DA80D1u128;
812        cols[0][0] = input1.into();
813        cols[0][1] = input2.into();
814
815        xor::extend_xor_witness::<Fp>(&mut cols, input1.into(), input2.into(), 128);
816        cols
817    };
818
819    let cs = ConstraintSystem::<Fp>::create(gates)
822        .public(num_public_inputs)
823        .lazy_mode(lazy_mode)
824        .build()
825        .unwrap();
826
827    srs.0.with_lagrange_basis(cs.domain.d1);
828
829    let (endo_q, _endo_r) = endos::<Pallas>();
830    let index = ProverIndex::<Vesta, OpeningProof<Vesta>>::create(cs, endo_q, srs.0, lazy_mode);
831    let group_map = <Vesta as CommitmentCurve>::Map::setup();
832    let public_input = (witness[0][0], witness[0][1]);
833    let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
834        &group_map,
835        witness,
836        &[],
837        &index,
838        vec![],
839        None,
840        &mut rand::rngs::OsRng,
841    )
842    .unwrap();
843    (
844        CamlPastaFpPlonkIndex(Box::new(index)),
845        (public_input.0.into(), public_input.1.into()),
846        (proof, vec![public_input.0, public_input.1]).into(),
847    )
848}
849
850#[ocaml_gen::func]
851#[ocaml::func]
852pub fn caml_pasta_fp_plonk_proof_example_with_rot(
853    srs: CamlFpSrs,
854    lazy_mode: bool,
855) -> (
856    CamlPastaFpPlonkIndex,
857    (CamlFp, CamlFp),
858    CamlProofWithPublic<CamlGVesta, CamlFp>,
859) {
860    use ark_ff::Zero;
861    use kimchi::circuits::{
862        constraints::ConstraintSystem,
863        gate::{CircuitGate, Connect},
864        polynomial::COLUMNS,
865        polynomials::{
866            generic::GenericGateSpec,
867            rot::{self, RotMode},
868        },
869        wires::Wire,
870    };
871    use poly_commitment::ipa::endos;
872
873    let num_public_inputs = 2;
875    let rot = 32;
877    let mode = RotMode::Left;
878
879    let gates = {
881        let mut gates = vec![];
882        for row in 0..num_public_inputs {
884            gates.push(CircuitGate::<Fp>::create_generic_gadget(
885                Wire::for_row(row),
886                GenericGateSpec::Pub,
887                None,
888            ));
889        }
890        CircuitGate::<Fp>::extend_rot(&mut gates, rot, mode, 1);
891        gates.connect_cell_pair((0, 0), (2, 0));
893
894        for _ in 0..(1 << 13) {
896            gates.push(CircuitGate::zero(Wire::for_row(gates.len())));
897        }
898
899        gates
900    };
901
902    let witness = {
904        let mut cols: [_; COLUMNS] = core::array::from_fn(|_col| vec![Fp::zero(); 2]);
906
907        let input = 0xDC811727DAF22EC1u64;
909        cols[0][0] = input.into();
910        rot::extend_rot::<Fp>(&mut cols, input, rot, mode);
911
912        cols
913    };
914
915    let cs = ConstraintSystem::<Fp>::create(gates)
918        .public(num_public_inputs)
919        .lazy_mode(lazy_mode)
920        .build()
921        .unwrap();
922
923    srs.0.with_lagrange_basis(cs.domain.d1);
924
925    let (endo_q, _endo_r) = endos::<Pallas>();
926    let index = ProverIndex::<Vesta, OpeningProof<Vesta>>::create(cs, endo_q, srs.0, lazy_mode);
927    let group_map = <Vesta as CommitmentCurve>::Map::setup();
928    let public_input = (witness[0][0], witness[0][1]);
929    let proof = ProverProof::create_recursive::<EFqSponge, EFrSponge, _>(
930        &group_map,
931        witness,
932        &[],
933        &index,
934        vec![],
935        None,
936        &mut rand::rngs::OsRng,
937    )
938    .unwrap();
939    (
940        CamlPastaFpPlonkIndex(Box::new(index)),
941        (public_input.0.into(), public_input.1.into()),
942        (proof, vec![public_input.0, public_input.1]).into(),
943    )
944}
945
946#[ocaml_gen::func]
947#[ocaml::func]
948pub fn caml_pasta_fp_plonk_proof_verify(
949    index: CamlPastaFpPlonkVerifierIndex,
950    proof: CamlProofWithPublic<CamlGVesta, CamlFp>,
951) -> bool {
952    let group_map = <Vesta as CommitmentCurve>::Map::setup();
953
954    let (proof, public_input) = proof.into();
955    let verifier_index = index.into();
956    let context = Context {
957        verifier_index: &verifier_index,
958        proof: &proof,
959        public_input: &public_input,
960    };
961
962    batch_verify::<
963        Vesta,
964        DefaultFqSponge<VestaParameters, PlonkSpongeConstantsKimchi>,
965        DefaultFrSponge<Fp, PlonkSpongeConstantsKimchi>,
966        OpeningProof<Vesta>,
967    >(&group_map, &[context])
968    .is_ok()
969}
970
971#[ocaml_gen::func]
972#[ocaml::func]
973pub fn caml_pasta_fp_plonk_proof_batch_verify(
974    indexes: Vec<CamlPastaFpPlonkVerifierIndex>,
975    proofs: Vec<CamlProofWithPublic<CamlGVesta, CamlFp>>,
976) -> bool {
977    let ts: Vec<_> = indexes
978        .into_iter()
979        .zip(proofs.into_iter())
980        .map(|(caml_index, caml_proof)| {
981            let verifier_index: VerifierIndex<Vesta, OpeningProof<Vesta>> = caml_index.into();
982            let (proof, public_input): (ProverProof<Vesta, OpeningProof<Vesta>>, Vec<_>) =
983                caml_proof.into();
984            (verifier_index, proof, public_input)
985        })
986        .collect();
987    let ts_ref: Vec<Context<Vesta, OpeningProof<Vesta>>> = ts
988        .iter()
989        .map(|(verifier_index, proof, public_input)| Context {
990            verifier_index,
991            proof,
992            public_input,
993        })
994        .collect();
995    let group_map = GroupMap::<Fq>::setup();
996
997    batch_verify::<
998        Vesta,
999        DefaultFqSponge<VestaParameters, PlonkSpongeConstantsKimchi>,
1000        DefaultFrSponge<Fp, PlonkSpongeConstantsKimchi>,
1001        OpeningProof<Vesta>,
1002    >(&group_map, &ts_ref)
1003    .is_ok()
1004}
1005
1006#[ocaml_gen::func]
1007#[ocaml::func]
1008pub fn caml_pasta_fp_plonk_proof_dummy() -> CamlProofWithPublic<CamlGVesta, CamlFp> {
1009    fn comm() -> PolyComm<Vesta> {
1010        let g = Vesta::generator();
1011        PolyComm {
1012            chunks: vec![g, g, g],
1013        }
1014    }
1015
1016    let prev = RecursionChallenge {
1017        chals: vec![Fp::one(), Fp::one()],
1018        comm: comm(),
1019    };
1020    let prev_challenges = vec![prev.clone(), prev.clone(), prev];
1021
1022    let g = Vesta::generator();
1023    let proof = OpeningProof {
1024        lr: vec![(g, g), (g, g), (g, g)],
1025        z1: Fp::one(),
1026        z2: Fp::one(),
1027        delta: g,
1028        sg: g,
1029    };
1030    let eval = || PointEvaluations {
1031        zeta: vec![Fp::one()],
1032        zeta_omega: vec![Fp::one()],
1033    };
1034    let evals = ProofEvaluations {
1035        public: Some(eval()),
1036        w: core::array::from_fn(|_| eval()),
1037        coefficients: core::array::from_fn(|_| eval()),
1038        z: eval(),
1039        s: core::array::from_fn(|_| eval()),
1040        generic_selector: eval(),
1041        poseidon_selector: eval(),
1042        complete_add_selector: eval(),
1043        mul_selector: eval(),
1044        emul_selector: eval(),
1045        endomul_scalar_selector: eval(),
1046        range_check0_selector: None,
1047        range_check1_selector: None,
1048        foreign_field_add_selector: None,
1049        foreign_field_mul_selector: None,
1050        xor_selector: None,
1051        rot_selector: None,
1052        lookup_aggregation: None,
1053        lookup_table: None,
1054        lookup_sorted: array::from_fn(|_| None),
1055        runtime_lookup_table: None,
1056        runtime_lookup_table_selector: None,
1057        xor_lookup_selector: None,
1058        lookup_gate_lookup_selector: None,
1059        range_check_lookup_selector: None,
1060        foreign_field_mul_lookup_selector: None,
1061    };
1062
1063    let public = vec![Fp::one(), Fp::one()];
1064    let dlogproof = ProverProof {
1065        commitments: ProverCommitments {
1066            w_comm: core::array::from_fn(|_| comm()),
1067            z_comm: comm(),
1068            t_comm: comm(),
1069            lookup: None,
1070        },
1071        proof,
1072        evals,
1073        ft_eval1: Fp::one(),
1074        prev_challenges,
1075    };
1076
1077    (dlogproof, public).into()
1078}
1079
1080#[ocaml_gen::func]
1081#[ocaml::func]
1082pub fn caml_pasta_fp_plonk_proof_deep_copy(
1083    x: CamlProofWithPublic<CamlGVesta, CamlFp>,
1084) -> CamlProofWithPublic<CamlGVesta, CamlFp> {
1085    x
1086}