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