1use ark_crypto_primitives::snark::{FromFieldElementsGadget, SNARKGadget, SNARK};
 2use ark_ec::AffineRepr;
 3use ark_ec::CurveGroup;
 4use ark_ff::{fields::Fp256, Field, PrimeField};
 5use ark_r1cs_std::{
 6    alloc::{AllocVar, AllocationMode},
 7    bits::uint8::UInt8,
 8    boolean::Boolean,
 9    eq::EqGadget,
10    fields::{fp::FpVar, FieldVar},
11    groups::GroupOpsBounds,
12    prelude::CurveVar,
13    ToBitsGadget,
14};
15use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, Namespace, SynthesisError};
16use ark_std::ops::Mul;
17
18use core::{borrow::Borrow, marker::PhantomData};
19use derivative::Derivative;
20
21// pub trait Nova<F: PrimeField> {}
22
23pub trait Config<Fq: PrimeField, Fr: PrimeField> {
24    type AugmentedFunctionCircuit: SNARK<Fq>; // F'
25    type FunctionCircuit: ConstraintSynthesizer<Fq>; // F
26    type DummyStepCircuit: SNARK<Fr>;
27}
28
29pub struct AugmentedFCircuit<
30    Fq: PrimeField,
31    Fr: PrimeField,
32    C: CurveGroup,
33    GC: CurveVar<C, Fq>,
34    Cfg: Config<Fq, Fr>,
35> {
36    pub dummystep_vk: Option<<Cfg::DummyStepCircuit as SNARK<Fr>>::VerifyingKey>,
37    _c: PhantomData<C>,
38    _gc: PhantomData<GC>,
39}
40
41impl<Fq: PrimeField, Fr: PrimeField, C: CurveGroup, GC: CurveVar<C, Fq>, Cfg: Config<Fq, Fr>>
42    ConstraintSynthesizer<Fq> for AugmentedFCircuit<Fq, Fr, C, GC, Cfg>
43{
44    fn generate_constraints(self, cs: ConstraintSystemRef<Fq>) -> Result<(), SynthesisError> {
45        unimplemented!();
46    }
47}
48
49pub struct NIFSGadget<F: PrimeField, C: CurveGroup, GC: CurveVar<C, F>> {
50    _f: PhantomData<F>,
51    _c: PhantomData<C>,
52    _gc: PhantomData<GC>,
53}
54
55impl<F: PrimeField, C: CurveGroup, GC: CurveVar<C, F>> NIFSGadget<F, C, GC> {
56    // implements the constraints for NIFS.V
57    pub fn verify(
58        r: FpVar<F>,
59        cmT: GC,
60        // phi1, phi2 and phi3
61        cmE1: GC,
62        cmE2: GC,
63        cmE3: GC,
64        u1: FpVar<F>,
65        u2: FpVar<F>,
66        u3: FpVar<F>,
67        cmW1: GC,
68        cmW2: GC,
69        cmW3: GC,
70        // x's size will depend on the num_publicinputs of F circuit
71        x1: Vec<FpVar<F>>,
72        x2: Vec<FpVar<F>>,
73        x3: Vec<FpVar<F>>,
74    ) -> Result<Boolean<F>, SynthesisError> {
75        let r2 = r.square()?;
76        cmE3.is_eq(
77            &(cmE1
78                + cmT.scalar_mul_le(r.to_bits_le()?.iter())?
79                + cmE2.scalar_mul_le(r2.to_bits_le()?.iter())?),
80        )?;
81        u3.is_eq(&(u1 + r.clone() * u2))?;
82        cmW3.is_eq(&(cmW1 + cmW2.scalar_mul_le(r.to_bits_le()?.iter())?))
83
84        // TODO x's check
85    }
86}