Add zk-sum-check circuit written in Halo2 (still incomplete!)

packages/hoplite/src/dotprod.rs

@@ -1,6 +1,6 @@
 use crate::{
     commitments::Commitments, sumcheck::FromCircuitVal, utils::to_fq, Fq, MultiCommitGens,
-    DEGREE_BOUND, N_ROUNDS,
+    DEGREE_BOUND,
 };
 use libspartan::{
     group::CompressedGroup,

packages/hoplite/src/lib.rs

@@ -6,7 +6,6 @@ use libspartan::{
     transcript::{AppendToTranscript, ProofTranscript, Transcript},
     Instance, NIZKGens, NIZK,
 };
-
 pub mod commitments;
 pub mod dotprod;
 pub mod sumcheck;
@@ -21,14 +20,13 @@ use libspartan::commitments::Commitments;
 pub const DEGREE_BOUND: usize = 3;
 pub const N_ROUNDS: usize = 1;
 
-#[allow(dead_code)]
-fn verify_nizk(
+pub fn verify_nizk(
     inst: &Instance,
     num_cons: usize,
     num_vars: usize,
     input: &[libspartan::scalar::Scalar],
-    proof: NIZK,
-    gens: NIZKGens,
+    proof: &NIZK,
+    gens: &NIZKGens,
 ) {
     let mut transcript = Transcript::new(b"test_verify");
 
@@ -56,8 +54,8 @@ fn verify_nizk(
 
     let _tau = transcript.challenge_vector(b"challenge_tau", num_rounds_x);
 
-    let gens_1 = gens.gens_r1cs_sat.gens_sc.gens_1;
-    let gens_4 = gens.gens_r1cs_sat.gens_sc.gens_4;
+    let gens_1 = gens.gens_r1cs_sat.gens_sc.gens_1.clone();
+    let gens_4 = gens.gens_r1cs_sat.gens_sc.gens_4.clone();
 
     // ############################
     // # Verify Phase 1 SumCheck
@@ -141,8 +139,8 @@ mod tests {
             num_cons,
             num_vars,
             &assignment_inputs.assignment,
-            proof,
-            gens,
+            &proof,
+            &gens,
         );
     }
 }

packages/hoplite_circuit/Cargo.toml

@@ -0,0 +1,22 @@
+[package]
+name = "hoplite_circuit"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[features]
+default = ["dev-graph"]
+dev-graph = ["halo2_proofs/dev-graph", "plotters"]
+
+[dependencies]
+halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2", tag = "v2023_01_20" }
+halo2-base = { git = "https://github.com/axiom-crypto/halo2-lib.git", default-features = false, features = ["halo2-pse"] }
+halo2-ecc = { git = "https://github.com/axiom-crypto/halo2-lib.git", default-features = false, features = ["halo2-pse"] }
+num-bigint = { version = "0.4", features = ["rand"] }
+secpq_curves = { git = "https://github.com/DanTehrani/secpq_curves.git" }
+plotters = { version = "0.3.0", optional = true }
+tabbycat = { version = "0.1", features = ["attributes"], optional = true }
+spartan = { git = "https://github.com/DanTehrani/Spartan-secq", branch = "hoplite" }
+secq256k1 = { git = "https://github.com/personaelabs/spartan-ecdsa", branch = "main" }
+hoplite = { path = "../hoplite" }

packages/hoplite_circuit/src/chips/dotprod.rs

@@ -0,0 +1,116 @@
+use crate::{
+    chips::pedersen_commit::PedersenCommitChip,
+    {FpChip, Fq, FqChip, ZKDotProdProof},
+};
+use halo2_base::{utils::PrimeField, Context};
+use halo2_ecc::bigint::CRTInteger;
+use halo2_ecc::ecc::{EcPoint, EccChip};
+use halo2_ecc::fields::FieldChip;
+use halo2_proofs::circuit::Value;
+use hoplite::{commitments::MultiCommitGens, DEGREE_BOUND};
+
+pub struct AssignedZKDotProdProof<'v, F: PrimeField> {
+    pub delta: EcPoint<F, CRTInteger<'v, F>>,
+    pub beta: EcPoint<F, CRTInteger<'v, F>>,
+    pub z: [CRTInteger<'v, F>; DEGREE_BOUND + 1],
+    pub z_delta: CRTInteger<'v, F>,
+    pub z_beta: CRTInteger<'v, F>,
+}
+
+pub struct ZKDotProdChip<F: PrimeField> {
+    pub ecc_chip: EccChip<F, FpChip<F>>,
+    pub fq_chip: FqChip<F>,
+    pub pedersen_chip: PedersenCommitChip<F>,
+    window_bits: usize,
+}
+
+impl<F: PrimeField> ZKDotProdChip<F> {
+    pub fn construct(
+        ecc_chip: EccChip<F, FpChip<F>>,
+        fq_chip: FqChip<F>,
+        pedersen_chip: PedersenCommitChip<F>,
+    ) -> Self {
+        Self {
+            ecc_chip,
+            fq_chip,
+            pedersen_chip,
+            window_bits: 4,
+        }
+    }
+
+    fn dot_prod<'v>(
+        &self,
+        ctx: &mut Context<'v, F>,
+        a: &[CRTInteger<'v, F>],
+        b: &[CRTInteger<'v, F>],
+    ) -> CRTInteger<'v, F> {
+        let mut sum = self
+            .fq_chip
+            .load_private(ctx, FqChip::<F>::fe_to_witness(&Value::known(Fq::zero())));
+
+        // Implement this
+        for i in 0..a.len() {
+            let prod_no_carry = self.fq_chip.mul_no_carry(ctx, &a[i], &b[i]);
+            let sum_no_carry = self.fq_chip.add_no_carry(ctx, &sum, &prod_no_carry);
+            sum = self.fq_chip.carry_mod(ctx, &sum_no_carry);
+        }
+
+        sum
+    }
+
+    pub fn verify<'v>(
+        &self,
+        ctx: &mut Context<'v, F>,
+        tau: &EcPoint<F, CRTInteger<'v, F>>,
+        a: [CRTInteger<'v, F>; DEGREE_BOUND + 1],
+        com_poly: &EcPoint<F, CRTInteger<'v, F>>,
+        proof: AssignedZKDotProdProof<'v, F>,
+        gens_1: &MultiCommitGens,
+        gens_n: &MultiCommitGens,
+    ) {
+        let max_bits = self.fq_chip.limb_bits;
+
+        // TODO: Actually compute the challenge!
+        let c = self
+            .fq_chip
+            .load_private(ctx, FqChip::<F>::fe_to_witness(&Value::known(Fq::one())));
+
+        // (13)
+        let epsilon_c = self.ecc_chip.scalar_mult(
+            ctx,
+            &com_poly,
+            &c.truncation.limbs,
+            max_bits,
+            self.window_bits,
+        );
+
+        // (epsilon * c) + delta
+        let lhs = self
+            .ecc_chip
+            .add_unequal(ctx, &epsilon_c, &proof.delta, true);
+
+        // com(z, z_delta)
+        let rhs = self
+            .pedersen_chip
+            .multi_commit(ctx, &proof.z, &proof.z_delta, &gens_n);
+
+        self.ecc_chip.assert_equal(ctx, &lhs, &rhs);
+
+        // (14)
+        let tau_c = self
+            .ecc_chip
+            .scalar_mult(ctx, &tau, &c.truncation.limbs, max_bits, 4);
+
+        // (tau * c) + beta
+        let lhs = self.ecc_chip.add_unequal(ctx, &tau_c, &proof.beta, true);
+
+        let a_dot_z = self.dot_prod(ctx, &a, &proof.z);
+
+        // com((a ・ z), z_beta)
+        let rhs = self
+            .pedersen_chip
+            .commit(ctx, &a_dot_z, &proof.z_beta, &gens_1);
+
+        self.ecc_chip.assert_equal(ctx, &lhs, &rhs);
+    }
+}

packages/hoplite_circuit/src/chips/mod.rs

@@ -0,0 +1,2 @@
+pub mod dotprod;
+pub mod pedersen_commit;

packages/hoplite_circuit/src/chips/pedersen_commit.rs

@@ -0,0 +1,97 @@
+use crate::FpChip;
+use halo2_base::{utils::PrimeField, Context};
+use halo2_ecc::bigint::CRTInteger;
+use halo2_ecc::ecc::{fixed_base, EcPoint, EccChip};
+use hoplite::commitments::MultiCommitGens;
+use secpq_curves::group::Curve;
+
+#[derive(Clone)]
+pub struct PedersenCommitChip<F: PrimeField> {
+    pub ecc_chip: EccChip<F, FpChip<F>>,
+    pub fp_chip: FpChip<F>,
+    window_bits: usize,
+}
+
+impl<F: PrimeField> PedersenCommitChip<F> {
+    pub fn construct(ecc_chip: EccChip<F, FpChip<F>>, fp_chip: FpChip<F>) -> Self {
+        Self {
+            ecc_chip,
+            fp_chip,
+            window_bits: 4,
+        }
+    }
+
+    pub fn commit<'v>(
+        &self,
+        ctx: &mut Context<'v, F>,
+        x: &CRTInteger<'v, F>,
+        blinder: &CRTInteger<'v, F>,
+        gens: &MultiCommitGens,
+    ) -> EcPoint<F, CRTInteger<'v, F>> {
+        let max_bits = self.fp_chip.limb_bits;
+        let gx = fixed_base::scalar_multiply(
+            &self.fp_chip,
+            ctx,
+            &gens.G[0].to_affine(),
+            &x.truncation.limbs,
+            max_bits,
+            self.window_bits,
+        );
+
+        let hb = fixed_base::scalar_multiply(
+            &self.fp_chip,
+            ctx,
+            &gens.h.to_affine(),
+            &blinder.truncation.limbs,
+            max_bits,
+            self.window_bits,
+        );
+
+        let com = self.ecc_chip.add_unequal(ctx, &gx, &hb, true);
+        com
+    }
+
+    pub fn multi_commit<'v>(
+        &self,
+        ctx: &mut Context<'v, F>,
+        x: &[CRTInteger<'v, F>],
+        blinder: &CRTInteger<'v, F>,
+        gens: &MultiCommitGens,
+    ) -> EcPoint<F, CRTInteger<'v, F>> {
+        let max_bits = self.fp_chip.limb_bits;
+
+        let mut g_sum = fixed_base::scalar_multiply(
+            &self.fp_chip,
+            ctx,
+            &gens.G[0].to_affine(),
+            &x[0].truncation.limbs,
+            max_bits,
+            self.window_bits,
+        );
+
+        for (i, x_i) in x[1..].iter().enumerate() {
+            let g = fixed_base::scalar_multiply(
+                &self.fp_chip,
+                ctx,
+                &gens.G[i + 1].to_affine(),
+                &x_i.truncation.limbs,
+                max_bits,
+                self.window_bits,
+            );
+
+            g_sum = self.ecc_chip.add_unequal(ctx, &g_sum, &g, true);
+        }
+
+        let hb = fixed_base::scalar_multiply(
+            &self.fp_chip,
+            ctx,
+            &gens.h.to_affine(),
+            &blinder.truncation.limbs,
+            max_bits,
+            self.window_bits,
+        );
+
+        let com = self.ecc_chip.add_unequal(ctx, &g_sum, &hb, true);
+        com
+    }
+}

packages/hoplite_circuit/src/lib.rs

@@ -0,0 +1,531 @@
+mod chips;
+
+use chips::{
+    dotprod::{AssignedZKDotProdProof, ZKDotProdChip},
+    pedersen_commit::PedersenCommitChip,
+};
+use halo2_base::{
+    utils::{modulus, PrimeField},
+    Context,
+};
+use halo2_ecc::{
+    bigint::CRTInteger,
+    ecc::{fixed_base, EccChip},
+    fields::fp::{FpConfig, FpStrategy},
+};
+use halo2_ecc::{ecc::EcPoint, fields::FieldChip};
+use halo2_proofs::{
+    circuit::{Layouter, SimpleFloorPlanner, Value},
+    plonk,
+    plonk::{Circuit, Column, ConstraintSystem, Instance},
+};
+use hoplite::{commitments::MultiCommitGens, dotprod::ZKDotProdProof, sumcheck::ZKSumCheckProof};
+
+use secpq_curves::group::cofactor::CofactorCurveAffine;
+use secpq_curves::{
+    group::{Curve, Group},
+    CurveAffine, Secq256k1, Secq256k1Affine,
+};
+
+pub type Fp = secpq_curves::Fq;
+pub type Fq = secpq_curves::Fp;
+
+pub type FqChip<F> = FpConfig<F, secpq_curves::Fp>;
+pub type FpChip<F> = FpConfig<F, secpq_curves::Fq>;
+
+trait AssignPoint<'v, F: PrimeField> {
+    fn assign(
+        &self,
+        ctx: &mut Context<'v, F>,
+        field_chip: &EccChip<F, FpChip<F>>,
+    ) -> EcPoint<F, CRTInteger<'v, F>>;
+}
+
+impl<'v, F: PrimeField> AssignPoint<'v, F> for Value<Secq256k1> {
+    fn assign(
+        &self,
+        ctx: &mut Context<'v, F>,
+        ecc_chip: &EccChip<F, FpChip<F>>,
+    ) -> EcPoint<F, CRTInteger<'v, F>> {
+        let x = self.and_then(|point| Value::known(*point.to_affine().coordinates().unwrap().x()));
+        let y = self.and_then(|point| Value::known(*point.to_affine().coordinates().unwrap().y()));
+        ecc_chip.load_private(ctx, (x, y))
+    }
+}
+
+#[derive(Clone, Debug)]
+pub struct ZKSumCheckCircuitConfig<F: PrimeField> {
+    field_config: FpChip<F>,
+    /// Public inputs
+    instance: Column<Instance>,
+    window_bits: usize,
+}
+
+pub struct ZKSumCheckCircuit {
+    proof: Value<ZKSumCheckProof>,
+    gens_n: MultiCommitGens,
+    gens_1: MultiCommitGens,
+    target_sum: Value<Secq256k1>,
+}
+
+pub struct CircuitParams {
+    strategy: FpStrategy,
+    degree: u32,
+    num_advice: usize,
+    num_lookup_advice: usize,
+    num_fixed: usize,
+    lookup_bits: usize,
+    limb_bits: usize,
+    num_limbs: usize,
+}
+
+impl<F: PrimeField> Circuit<F> for ZKSumCheckCircuit {
+    type Config = ZKSumCheckCircuitConfig<F>;
+    type FloorPlanner = SimpleFloorPlanner;
+
+    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
+        let params = CircuitParams {
+            strategy: FpStrategy::Simple,
+            degree: 18,
+            num_advice: 20,
+            num_lookup_advice: 6,
+            num_fixed: 1,
+            lookup_bits: 17,
+            limb_bits: 88,
+            num_limbs: 3,
+        };
+
+        let field_config = FpChip::<F>::configure(
+            meta,
+            params.strategy,
+            &[params.num_advice],
+            &[params.num_lookup_advice],
+            params.num_fixed,
+            params.lookup_bits,
+            params.limb_bits,
+            params.num_limbs,
+            modulus::<Fp>(),
+            0,
+            params.degree as usize,
+        );
+
+        let instance = meta.instance_column();
+
+        meta.enable_equality(instance);
+
+        ZKSumCheckCircuitConfig {
+            instance,
+            field_config,
+            window_bits: 4,
+        }
+    }
+
+    fn without_witnesses(&self) -> Self {
+        // TODO: This is temporary!
+        let gens_1 = MultiCommitGens {
+            G: vec![Secq256k1::generator(); 1],
+            h: Secq256k1::generator(),
+        };
+        let gens_4 = MultiCommitGens {
+            G: vec![Secq256k1::generator(); 4],
+            h: Secq256k1::generator(),
+        };
+
+        ZKSumCheckCircuit {
+            proof: Value::unknown(),
+            gens_1,
+            gens_n: gens_4,
+            target_sum: Value::unknown(),
+        }
+    }
+
+    fn synthesize(
+        &self,
+        config: Self::Config,
+        mut layouter: impl Layouter<F>,
+    ) -> Result<(), plonk::Error> {
+        // Scalar mult
+        let n_rounds = 1;
+
+        let fp_chip = config.field_config;
+        fp_chip.range.load_lookup_table(&mut layouter)?;
+
+        // Actually perform the calculation
+
+        let limb_bits = fp_chip.limb_bits;
+        let num_limbs = fp_chip.num_limbs;
+        let _num_fixed = fp_chip.range.gate.constants.len();
+        let _lookup_bits = fp_chip.range.lookup_bits;
+        let _num_advice = fp_chip.range.gate.num_advice;
+
+        //        let mut results = Vec::new();
+
+        layouter.assign_region(
+            || "",
+            |region| {
+                let mut ctx = fp_chip.new_context(region);
+
+                // We can construct the fp_chip from the config of the fp_chip
+                // (fp_chip can use the same columns as the fp_chip)
+                let fq_chip = FqChip::<F>::construct(
+                    fp_chip.range.clone(),
+                    limb_bits,
+                    num_limbs,
+                    modulus::<Fq>(),
+                );
+
+                let ecc_chip = EccChip::construct(fp_chip.clone());
+                let pedersen_chip =
+                    PedersenCommitChip::construct(ecc_chip.clone(), fp_chip.clone());
+
+                for i in 0..n_rounds {
+                    // Load claimed_sum
+                    let com_eval = self
+                        .proof
+                        .and_then(|proof| Value::known(proof.comm_evals[i]))
+                        .assign(&mut ctx, &ecc_chip);
+
+                    let com_round_sum = if i == 0 {
+                        self.target_sum
+                            .and_then(|target_sum| Value::known(target_sum))
+                            .assign(&mut ctx, &ecc_chip)
+                    } else {
+                        let com_eval = self
+                            .proof
+                            .and_then(|proof| Value::known(proof.comm_evals[i - 1]))
+                            .assign(&mut ctx, &ecc_chip);
+
+                        com_eval
+                    };
+
+                    let w_0: CRTInteger<F> = fq_chip.load_private(
+                        &mut ctx,
+                        FqChip::<F>::fe_to_witness(&Value::known(Fq::one())),
+                    );
+
+                    let w_1: CRTInteger<F> = fq_chip.load_private(
+                        &mut ctx,
+                        FqChip::<F>::fe_to_witness(&Value::known(Fq::one())),
+                    );
+
+                    let tau_0 = fixed_base::scalar_multiply(
+                        &fp_chip,
+                        &mut ctx,
+                        &Secq256k1Affine::generator(),
+                        &w_0.truncation.limbs,
+                        limb_bits,
+                        config.window_bits,
+                    );
+                    /*
+                    let tau_0 = ecc_chip.scalar_mult(
+                        &mut ctx,
+                        &com_round_sum,
+                        &w_0.truncation.limbs,
+                        limb_bits,
+                        config.window_bits,
+                    );
+                         */
+
+                    let tau_1 = ecc_chip.scalar_mult(
+                        &mut ctx,
+                        &com_eval,
+                        &w_1.truncation.limbs,
+                        limb_bits,
+                        config.window_bits,
+                    );
+
+                    let tau = ecc_chip.add_unequal(&mut ctx, &tau_0, &tau_1, true);
+
+                    let degree_bound = 3;
+
+                    // TODO: Compute "a"
+                    let a = [
+                        fq_chip.load_private(
+                            &mut ctx,
+                            FqChip::<F>::fe_to_witness(&Value::known(Fq::from(3))),
+                        ),
+                        fq_chip.load_private(
+                            &mut ctx,
+                            FqChip::<F>::fe_to_witness(&Value::known(Fq::from(2))),
+                        ),
+                        fq_chip.load_private(
+                            &mut ctx,
+                            FqChip::<F>::fe_to_witness(&Value::known(Fq::from(2))),
+                        ),
+                        fq_chip.load_private(
+                            &mut ctx,
+                            FqChip::<F>::fe_to_witness(&Value::known(Fq::from(2))),
+                        ),
+                    ];
+                    /*
+                    let a = vec![
+                        fq_chip.load_private(
+                            &mut ctx,
+                            FqChip::<F>::fe_to_witness(&Value::known(Fq::one()))
+                        );
+                        degree_bound + 1
+                    ];
+                    let a = {
+                        // the vector to use to decommit for sum-check test
+                        let a_sc = {
+                            let mut a = vec![Fp::one(); degree_bound + 1];
+                            a[0] += Fp::one();
+                            a
+                        };
+
+                        // the vector to use to decommit for evaluation
+                        let a_eval = {
+                            let mut a = vec![Fp::one(); degree_bound + 1];
+                            for j in 1..a.len() {
+                                a[j] = a[j - 1] * r_i;
+                            }
+                            a
+                        };
+
+                        // take weighted sum of the two vectors using w
+                        assert_eq!(a_sc.len(), a_eval.len());
+                        (0..a_sc.len())
+                            .map(|i| w_0 * a_sc[i] + w_1 * a_eval[i])
+                            .collect::<Vec<Fp>>()
+                    };
+                     */
+
+                    let zk_dot_prod_chip = ZKDotProdChip::construct(
+                        ecc_chip.clone(),
+                        fq_chip.clone(),
+                        pedersen_chip.clone(),
+                    );
+
+                    let com_poly_assigned = ecc_chip.load_private(
+                        &mut ctx,
+                        (
+                            self.proof
+                                .and_then(|proof| Value::known(proof.comm_polys[i].x)),
+                            self.proof
+                                .and_then(|proof| Value::known(proof.comm_polys[i].y)),
+                        ),
+                    );
+
+                    let z_delta = self
+                        .proof
+                        .and_then(|proof| Value::known(proof.proofs[i].z_delta));
+
+                    let z_beta = self
+                        .proof
+                        .and_then(|proof| Value::known(proof.proofs[i].z_beta));
+
+                    let delta_assinged = self
+                        .proof
+                        .and_then(|proof| Value::known(proof.proofs[i].delta))
+                        .assign(&mut ctx, &ecc_chip);
+
+                    let beta_assigned = self
+                        .proof
+                        .and_then(|proof| Value::known(proof.proofs[i].beta))
+                        .assign(&mut ctx, &ecc_chip);
+
+                    let mut z_assigned = vec![];
+
+                    for j in 0..(degree_bound + 1) {
+                        let z_j = self
+                            .proof
+                            .and_then(|proof| Value::known(proof.proofs[i].z[j]));
+
+                        z_assigned
+                            .push(fq_chip.load_private(&mut ctx, FqChip::<F>::fe_to_witness(&z_j)));
+                    }
+
+                    assert!(z_assigned.len() == (degree_bound + 1));
+
+                    let assigned_dot_prod_prood = AssignedZKDotProdProof {
+                        delta: delta_assinged,
+                        beta: beta_assigned,
+                        z_delta: fq_chip
+                            .load_private(&mut ctx, FqChip::<F>::fe_to_witness(&z_delta)),
+                        z_beta: fq_chip.load_private(&mut ctx, FqChip::<F>::fe_to_witness(&z_beta)),
+                        z: z_assigned.try_into().unwrap(),
+                    };
+
+                    zk_dot_prod_chip.verify(
+                        &mut ctx,
+                        &tau,
+                        a.try_into().unwrap(),
+                        &com_poly_assigned,
+                        assigned_dot_prod_prood,
+                        &self.gens_1,
+                        &self.gens_n,
+                    );
+                }
+
+                fp_chip.finalize(&mut ctx);
+
+                Ok(())
+            },
+        )?;
+
+        Ok(())
+    }
+}
+
+#[cfg(test)]
+mod tests {
+
+    use super::*;
+    use halo2_base::utils::decompose_biguint;
+    use halo2_proofs::{dev::MockProver, halo2curves::bn256::Fr};
+    use hoplite::{commitments::Commitments, sumcheck::ToCircuitVal, verify_nizk, Scalar};
+    use libspartan::{
+        transcript::Transcript, InputsAssignment, Instance, NIZKGens, VarsAssignment, NIZK,
+    };
+    use num_bigint::BigUint;
+    use secpq_curves::Fp;
+
+    #[allow(non_snake_case)]
+    #[test]
+    fn test_zk_sumcheck_circuit() {
+        // parameters of the R1CS instance
+        let num_cons = 1;
+        let num_vars = 0;
+        let num_inputs = 3;
+
+        // We will encode the above constraints into three matrices, where
+        // the coefficients in the matrix are in the little-endian byte order
+        let mut A: Vec<(usize, usize, [u8; 32])> = Vec::new(); // <row, column, value>
+        let mut B: Vec<(usize, usize, [u8; 32])> = Vec::new();
+        let mut C: Vec<(usize, usize, [u8; 32])> = Vec::new();
+
+        // Create a^2 + b + 13
+        A.push((0, num_vars + 2, Fq::one().to_bytes())); // 1*a
+        B.push((0, num_vars + 2, Fq::one().to_bytes())); // 1*a
+        C.push((0, num_vars + 1, Fq::one().to_bytes())); // 1*z
+        C.push((0, num_vars, (-Fq::from(13u64)).to_bytes())); // -13*1
+        C.push((0, num_vars + 3, (-Fq::one()).to_bytes())); // -1*b
+
+        // Var Assignments (Z_0 = 16 is the only output)
+        let vars = vec![Fq::zero().to_bytes(); num_vars];
+
+        // create an InputsAssignment (a = 1, b = 2)
+        let mut inputs = vec![Fq::zero().to_bytes(); num_inputs];
+        inputs[0] = Fq::from(16u64).to_bytes();
+        inputs[1] = Fq::from(1u64).to_bytes();
+        inputs[2] = Fq::from(2u64).to_bytes();
+
+        let assignment_inputs = InputsAssignment::new(&inputs).unwrap();
+        let assignment_vars = VarsAssignment::new(&vars).unwrap();
+
+        // Check if instance is satisfiable
+        let inst = Instance::new(num_cons, num_vars, num_inputs, &A, &B, &C).unwrap();
+        let res = inst.is_sat(&assignment_vars, &assignment_inputs);
+        assert!(res.unwrap(), "should be satisfied");
+
+        let gens = NIZKGens::new(num_cons, num_vars, num_inputs);
+
+        let mut prover_transcript = Transcript::new(b"test_verify");
+
+        let proof = NIZK::prove(
+            &inst,
+            assignment_vars,
+            &assignment_inputs,
+            &gens,
+            &mut prover_transcript,
+        );
+
+        verify_nizk(
+            &inst,
+            num_cons,
+            num_vars,
+            &assignment_inputs.assignment,
+            &proof,
+            &gens,
+        );
+
+        // Verify the phase 1 zk-sumcheck  proof
+        let sc_proof_phase1 = proof.r1cs_sat_proof.sc_proof_phase1.to_circuit_val();
+
+        let phase1_expected_sum = Secq256k1::identity();
+
+        let circuit = ZKSumCheckCircuit {
+            proof: Value::known(sc_proof_phase1),
+            target_sum: Value::known(phase1_expected_sum),
+            gens_1: gens.gens_r1cs_sat.gens_sc.gens_1.into(),
+            gens_n: gens.gens_r1cs_sat.gens_sc.gens_4.into(),
+        };
+
+        // Convert ZkSumCheckProof into a ZKSumCheckCircuit
+
+        /*
+        let claimed_sum_0_limbs: Vec<Fr> = decompose_biguint(
+            &BigUint::from_bytes_le(&phase1_expected_sum.x.to_bytes()),
+            3,
+            88,
+        );
+
+        let claimed_sum_1_limbs: Vec<Fr> = decompose_biguint(
+            &BigUint::from_bytes_le(&phase1_expected_sum.y.to_bytes()),
+            3,
+            88,
+        );
+         */
+
+        let k = 18;
+        //  let public_inputs = vec![claimed_sum_0_limbs, claimed_sum_1_limbs].concat();
+
+        let prover = MockProver::<Fr>::run(k, &circuit, vec![vec![]]).unwrap();
+        assert_eq!(prover.verify(), Ok(()));
+    }
+
+    /*
+    fn empty_round_proof() -> RoundProof {
+        let unknown_point = AffinePoint {
+            x: Value::unknown(),
+            y: Value::unknown(),
+        };
+        let dotprod_proof = ZKDotProdProof {
+            delta: unknown_point.clone(),
+            beta: unknown_point.clone(),
+            epsilon: unknown_point.clone(),
+            z_beta: Value::unknown(),
+            z: vec![Value::unknown(); 3],
+            z_delta: Value::unknown(),
+        };
+
+        RoundProof {
+            dotprod_proof,
+            com_eval: unknown_point,
+        }
+    }
+
+    #[test]
+    fn plot_circuit() {
+    use plotters::prelude::*;
+
+        let unknown_point = AffinePoint {
+            x: Value::unknown(),
+            y: Value::unknown(),
+        };
+
+        let circuit = ZKSumCheckCircuit {
+            claimed_sum: unknown_point.clone(),
+            round_proofs: vec![empty_round_proof(); 2],
+        };
+
+        let root = BitMapBackend::new("layout.png", (1024, 768)).into_drawing_area();
+        root.fill(&WHITE).unwrap();
+        let root = root
+            .titled("Example Circuit Layout", ("sans-serif", 60))
+            .unwrap();
+
+
+        halo2_proofs::dev::CircuitLayout::default()
+            // You can optionally render only a section of the circuit.
+            .view_width(0..2)
+            .view_height(0..16)
+            // You can hide labels, which can be useful with smaller areas.
+            .show_labels(false)
+            // Render the circuit onto your area!
+            // The first argument is the size parameter for the circuit.
+            .render::<Fr, _, _>(20, &circuit, &root)
+            .unwrap();
+    }
+     */
+}

packages/hoplite_circuit/src/to_cirucit_val.rs

@@ -0,0 +1,52 @@
+use crate::{AffinePoint, Fp, Fq, RoundProof, ZKDotProdProof};
+use halo2_proofs::circuit::Value;
+use libspartan::{nizk::DotProductProof, sumcheck::ZKSumcheckInstanceProof};
+
+// We define our own trait rather than using the `From` trait because
+// we need to "convert to" some types that are defined outside of this crate.
+trait ToCircuitVal<V> {
+    fn to_circuit_val(&self) -> V;
+}
+
+impl ToCircuitVal<AffinePoint> for libspartan::group::CompressedGroup {
+    fn to_circuit_val(&self) -> AffinePoint {
+        let x_bytes: [u8; 32] = (*self.x().unwrap()).try_into().unwrap();
+        let y_bytes: [u8; 32] = (*self.y().unwrap()).try_into().unwrap();
+
+        let x = Value::known(Fp::from_bytes(&x_bytes).unwrap());
+        let y = Value::known(Fp::from_bytes(&y_bytes).unwrap());
+
+        AffinePoint { x, y }
+    }
+}
+
+impl ToCircuitVal<AffinePoint> for libspartan::group::GroupElement {
+    fn to_circuit_val(&self) -> AffinePoint {
+        self.compress().to_circuit_val()
+    }
+}
+
+impl ToCircuitVal<Value<Fq>> for libspartan::scalar::Scalar {
+    fn to_circuit_val(&self) -> Value<Fq> {
+        let bytes: [u8; 32] = self.to_bytes();
+        Value::known(Fq::from_bytes(&bytes).unwrap())
+    }
+}
+
+impl ToCircuitVal<ZKDotProdProof> for DotProductProof {
+    fn to_circuit_val(&self) -> ZKDotProdProof {
+        let delta = self.delta.to_circuit_val();
+        let beta = self.beta.to_circuit_val();
+        let z_beta = self.z_beta.to_circuit_val();
+        let z_delta = self.z_delta.to_circuit_val();
+        let z = self.z.into_iter().map(|z_i| z_i.to_circuit_val()).collect();
+
+        ZKDotProdProof {
+            delta,
+            beta,
+            z_beta,
+            z_delta,
+            z,
+        }
+    }
+}