Comment

Cargo.toml

@@ -1,6 +1,8 @@
 [workspace]
 members = [
-    "packages/spartan_wasm",
+#    "packages/spartan_wasm",
     "packages/secq256k1",
-    "packages/poseidon",
+#    "packages/poseidon",
+    "packages/hoplite",
+    "packages/hoplite_circuit",
 ]

packages/hoplite/Cargo.toml

@@ -0,0 +1,12 @@
+[package]
+name = "hoplite"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+secq256k1 = { path = "../secq256k1" }
+spartan = { git = "https://github.com/DanTehrani/Spartan-secq", branch = "hoplite" }
+sha3 = { version = "0.8.2" }
+secpq_curves = { git = "https://github.com/DanTehrani/secpq_curves.git" }

packages/hoplite/README.md

@@ -0,0 +1,8 @@
+# Hoplite
+
+Hoplite is a Spartan reference implementation designed to be the spec for the Halo2 Spartan verification circuit. [Srinath's Spartan implementation](https://github.com/microsoft/Spartan) uses stateful classes, making it difficult to conceptualize the verification process in terms of circuit constraints. To better understand the verification process, it would be helpful to re-implement the verification in a circuit-like coding manner. For example
+
+- The verification should be stateless (i.e. should employ functional programming)
+- The R1CS matrices should be hard-coded into the circuit
+
+Additionally, this reference implementation should include thorough documentation to facilitate collaboration and audits.

packages/hoplite/spartan.md

@@ -0,0 +1,192 @@
+# Spartan: Full Protocol Description
+
+_This doc is a work in progress. Do not recommend reading._
+
+_Reference implementation: [Hoplite](https://github.com/personaelabs/Hoplite)_
+
+## Public Setup
+
+- Compute the Pedersen commitment generators using [hash-to-curve](https://github.com/personaelabs/spartan-ecdsa/blob/main/packages/secq256k1/src/hashtocurve.rs).
+
+## Building blocks
+
+$Fp$: The finite field used in the protocol.
+
+### Pedersen commitment
+
+Commitment
+Multi-commitments
+
+### proof-of-dot-prod
+
+TBD
+
+### proof-of-equality
+
+TBD
+
+### proof-of-opening
+
+TBD
+
+### zk-sum-check
+
+The details of the zk-sum-check protocol isn't provided in the Spartan paper (it only mentions that it uses methods form prior constructions). The following is a description of the zk-sum-check protocol used in the [original Spartan implementation](https://github.com/microsoft/Spartan).
+
+_Required prior knowledge: [The sum-check protocol](https://zkproof.org/2020/03/16/sum-checkprotocol/)_
+
+**Notations**
+
+- $g$: The polynomial which the sum is proven. We assume that $g$ is a multilinear polynomial (i.e. degree = 1) for simplicity.
+- $H$: The sum of evaluates of $g$ over the boolean hypercube.
+- $m$: The number of variables in $g$.
+- $s$: $\lfloor{log_2{m}}\rfloor$
+
+The protocol consists of $m$ rounds.
+
+**Prover: First round**
+
+In the first round, the prover computes
+$$g_1(X) = \sum_{i\in\{0, 1\}^{s-1}} g(X, x_2, ... x_m)$$
+
+In the standard sum-check protocol $g_1$ is sent to the verifier and the verifier checks
+$$g_1(0) + g_1(1) \stackrel{?}{=} H$$
+
+and
+
+$$g_1(r_1) \stackrel{?}{=} \sum_{i\in\{0, 1\}^{s-1}} g(r_1, x_2, ... x_m)$$
+
+where $r_1$ is a challenge.
+The evaluation of $g$ in the second check is proven in the successive sum-check protocol.
+
+In zk-sum-check, we instead provide the proof of evaluation of $g_1(0)$ $g_1(1)$ and $g_1(r_1)$ without revealing the coefficients of $g_1$, using proof-of-dot-product. For efficiency, we combine the evaluations into a single proof as follows.
+
+First, since we assume $g$ is a multilinear polynomial, we can write
+
+$$g_1(X) = p_1X + p_0$$
+where $p_0, p_1 \in Fp$ . $p_1$ is the coefficient and $p_0$ is the y-intercept.
+
+Before running proof-of-dot-prod, the prover must send commitments
+
+$$C_{g1} = \mathrm{multicom}((p_1, p_2), r_{g1})$$
+$$C_{eval} = \mathrm{com}(g_1(r), r_{eval})$$
+$$C_{sum} = \mathrm{com}((g_1(0) + g_1(1), r_{sum}))$$  
+to the verifier.
+
+The prover computes the weighted sum of and $g_1(0) + g_1(1)$  and $g(r_1)$ using weights $w_0, w_1 \in F_p$ sent from the verifier as
+$$(g_1(0) + g_1(1)) * w_0 + g_1(r_1) * w_1$$
+$$= p_1w_0 + 2p_0w_0 + p_1w_1r_1 + p_0w_1$$
+$$= p_1(w_0 + r_1w_1) + p_0(2w_0 + w_1)$$
+
+Thus, we use proof-of-dot-prod to prove
+$$(w_0 + r_1w_1, 2w_0 + w_1) \cdot (p_1, p_0) = (g_1(0) + g_1(1)) * w_0 + g_1(r_1) * w_1$$
+
+Now we proceed to the rest of the rounds
+
+### Prover: Rest of the rounds
+
+The rest of the rounds proceed similary as the first round except that prover proves the evaluations of the polynomial
+$$g_i(X) = \sum_{b\in \{0, 1\}^{s-1-i}}g(r_1, ...r_{i-1}, X, x_{i+1},...,{x_m})$$
+
+### Prover: Last round
+
+In the standard sum-check protocol, the verifier queries $g(r_1, ... ,r_m)$ using the oracle of $g$. and checks the result is equal to $g_m(r_m)$. In the Spartan's version of zk-sum-check, the prover instead provides the proof of evaluation of $g(r_1, ... ,r_m)$ **doing another zk-sum-check**. The details of this second zk-sum-check protocol is described later in this doc.
+
+### Verification
+
+The verifier receives
+
+- Claimed sum $H$
+- proof-of-dot-products $\{dp_1, dp_2, ... dp_m\}$
+
+Recall that the dot-product relation is
+$$(w_0 + r_1w_1, 2w_0 + w_1) \cdot (p_1, p_0) = (g_1(0) + g_1(1)) * w_0 + g_1(r_1) * w_1$$
+
+The verifier have access to $r_1, w_0, w_1$ and the commitments $Cy, Cx, C_{eval}$..
+The verifier computes the **target commitment**
+$$Ct = C_{sum} * w_0 + C_{eval} * w_1$$
+
+and checks the dot product proof
+
+$$
+TBD
+$$
+
+## Main Protocol
+
+Now we'll see how Spartan (_SpartanNIZK to be precise!_) uses the above building blocks to construct an NIZK for R1CS satisfiability.
+
+---
+
+**Below this is especially WIP! A lot of incomplete stuff!**
+
+1.$P$ Commit the witness polynomial
+
+- $P: C = PC.commit(pp, \bar{w}, S)$
+  send $C$ to the verifier 2.$V$ Randomly sample a challenge $\tau$ to query $\mathbb{g}$
+- $\tau \in \mathbb{F^{log_m}}$ and send $\tau$ to the prover
+
+4. Let $T_1 = 0$,
+5. $V: sample r_x \in \mathbb{F^{u1}}$
+6. $G_{io},\tau(x) = (\sum_{y \in \{0, 1\}^s} \widetilde{A}(x, y)\widetilde{Z}(y) + \sum_{y \in \{0, 1\}^s}\widetilde{B}(x, y)\widetilde{Z}(y) - \sum_{y \in \{0, 1\}^s}\widetilde{C}(x, y)\widetilde{Z}(y))\widetilde{eq}(x, \tau)$
+
+$\sum_{x \in \{0, 1\}^s} G_{io},\tau(x) = 0$ for a random $\tau$ iff all the constraints are satisfied
+
+- Run sumcheck on $G_{io},\tau(x)$
+- At the last step of the sum check where the verifier queries $G_{io}, \tau(x)$, we use the following sub-protocol.
+
+Define
+
+- $\bar{A}(x) = \sum_{y \in \{0, 1\}^s} \widetilde{A}(x, y)$
+- $\bar{B}(x) = \sum_{y \in \{0, 1\}^s} \widetilde{B}(x, y)$
+- $\bar{C}(x) = \sum_{y \in \{0, 1\}^s} \widetilde{C}(x, y)$
+- $M_{r_x}(y) = r_A *  \widetilde{A}(x, y)\widetilde{Z}(y) + r_B *  \widetilde{B}(x, y)\widetilde{Z}(y) + r_C *  \widetilde{C}(x, y)\widetilde{Z}(y)$
+
+Run the sum-check protocol to verify $M_{r_x}(y)$
+
+- $P$
+  - Send evaluations $v_A = \bar{A}(r_x), v_B = \bar{B}(r_x), v_C = \bar{C}(r_x)$ to the verifier.
+  - Send the opening $v_Z = Z(r_x)$ to the verifier
+- $V$
+  - Check $(v_A + v_B - v_C) * eq(r_x, \tau) = e_x$
+    The last part of the second sum-check protocol
+  - $v_1 = \widetilde{A}(r_x, r_y)$
+  - $v_2 = \widetilde{B}(r_x, r_y)$
+  - $v_3 = \widetilde{C}(r_x, r_y)$
+  - check taht $(r_A * v_1 + r_B * v_2 + r_C * v_3) * v_z = e_y$
+
+In the last round, the verifier needs to query $g(x)$. We will construct a protocol that is specific to Spartan that allows us to query $g(x)$ in zero-knowledge.
+
+### The second zk-sum-check
+
+Instead of constructing a generic method to evalute $g(X)$ in zk, we focus on $g(X)$ which is specific to Spartan. Recall that we want to prove the sum of
+$$G_{io},\tau(x) = (\sum_{y \in \{0, 1\}^s} \widetilde{A}(x, y)\widetilde{Z}(y) + \sum_{y \in \{0, 1\}^s}\widetilde{B}(x, y)\widetilde{Z}(y) - \sum_{y \in \{0, 1\}^s}\widetilde{C}(x, y)\widetilde{Z}(y))\widetilde{eq}(x, \tau)$$
+
+By looking at the terms of $\widetilde{F}(x)$, each term is in a form that is suitable to apply the SumCheck protocol. Assume for now that we can check the validity of each term (i.e each sum of $\widetilde{A}(x, y)\widetilde{Z}$, $\widetilde{B}(x, y)\widetilde{Z}$ and $\widetilde{C}(x, y)\widetilde{Z}$), we can check the relation of the sums as follows.
+
+Define
+
+- $\bar{A}(x) = \sum_{y \in \{0, 1\}^s} \widetilde{A}(x, y)$
+- $\bar{B}(x) = \sum_{y \in \{0, 1\}^s} \widetilde{B}(x, y)$
+- $\bar{C}(x) = \sum_{y \in \{0, 1\}^s} \widetilde{C}(x, y)$
+
+Now, recall that we want to evaluate $G_{io},\tau(x)$ only at the last round of the zk-sum-check over the all round_challenges $r_x = \{r_1, r_2, ... r_m\}$.
+
+Hence the prover can provide the evaluations $v_A, v_B$ and $v_C$ to the verifier.
+$$v_A = \bar{A}(r_x), v_B = \bar{B}(r_x), v_C = \bar{C}(r_x)$$
+The verifier checks that the evaluation of $G_{io}$ is equal to the evaluation of $g_m(r_m)$
+$$g_m(r_m) \stackrel{?}{=} (v_A + v_B - v_C)\widetilde{eq}(r_x, \tau)$$
+
+The verifier also needs to check the validity of $\bar{A}(x), \bar{B}(x), \bar{C}(x)$.
+This is where the second zk-sum-check comes in.
+
+We can check each term individually, but for efficiency, we use a random linear combination of the three terms.
+
+and sample challnges $r_A, r_B, r_C \in_R F_p$ to compute the random linear combination
+
+$$
+\widetilde{M}(x) \\ = r_A \bar{A}(r_x) + r_B\bar{B}(r_x) + r_C\bar{C}(r_x)  \\
+= (r_A\widetilde{A}(r_x, r_y) + r_B\widetilde{B}(r_x, r_y) + r_C\widetilde{C}(r_x, r_y))\widetilde{Z}(r_x, r_y)
+$$
+
+At the end of the second zk-sum-check, the verifier needs to evaluate $\widetilde{Z}(r_x, r_y)$. In order to evaluate without knowing the coefficients, we use the proof_log-of-dot-prod protocol. Note that the prover needs to commit to $Z(x)$ at the beginning so it cannot just come up with a $Z(x)$ that passes the final check of the second zk-sum-check.

packages/hoplite/src/commitments.rs

@@ -0,0 +1,83 @@
+use crate::Fq;
+use secpq_curves::Secq256k1;
+use secq256k1::{affine::Group, AffinePoint};
+use sha3::{
+    digest::{ExtendableOutput, Input},
+    Shake256,
+};
+use std::io::Read;
+
+use crate::sumcheck::ToCircuitVal;
+
+#[allow(non_snake_case)]
+pub struct MultiCommitGens {
+    pub G: Vec<Secq256k1>,
+    pub h: Secq256k1,
+}
+
+impl From<libspartan::commitments::MultiCommitGens> for MultiCommitGens {
+    fn from(gens: libspartan::commitments::MultiCommitGens) -> Self {
+        MultiCommitGens {
+            G: gens
+                .G
+                .iter()
+                .map(|g| g.compress().to_circuit_val())
+                .collect(),
+            h: gens.h.compress().to_circuit_val(),
+        }
+    }
+}
+
+impl MultiCommitGens {
+    pub fn new(n: usize, label: &[u8]) -> Self {
+        let mut shake = Shake256::default();
+        shake.input(label);
+        shake.input(AffinePoint::generator().compress().as_bytes());
+
+        let mut reader = shake.xof_result();
+        let mut gens: Vec<Secq256k1> = Vec::new();
+        let mut uniform_bytes = [0u8; 128];
+        for _ in 0..n + 1 {
+            reader.read_exact(&mut uniform_bytes).unwrap();
+            let gen = AffinePoint::from_uniform_bytes(&uniform_bytes).compress();
+            gens.push(gen.to_circuit_val());
+        }
+
+        MultiCommitGens {
+            G: gens[..n].to_vec(),
+            h: gens[n],
+        }
+    }
+}
+
+pub trait Commitments {
+    fn commit(&self, blind: &Fq, gens: &MultiCommitGens) -> Secq256k1;
+}
+
+impl Commitments for Fq {
+    fn commit(&self, blind: &Fq, gens: &MultiCommitGens) -> Secq256k1 {
+        gens.G[0] * self + gens.h * blind
+    }
+}
+
+impl Commitments for Vec<Fq> {
+    fn commit(&self, blind: &Fq, gens: &MultiCommitGens) -> Secq256k1 {
+        let mut result = Secq256k1::identity();
+        for (i, val) in self.iter().enumerate() {
+            result += gens.G[i] * val;
+        }
+        result += gens.h * blind;
+        result
+    }
+}
+
+impl Commitments for [Fq] {
+    fn commit(&self, blind: &Fq, gens: &MultiCommitGens) -> Secq256k1 {
+        let mut result = Secq256k1::identity();
+        for (i, val) in self.iter().enumerate() {
+            result += gens.G[i] * val;
+        }
+        result += gens.h * blind;
+        result
+    }
+}

packages/hoplite/src/dotprod.rs

@@ -0,0 +1,76 @@
+use crate::{
+    commitments::Commitments, sumcheck::FromCircuitVal, utils::to_fq, Fq, MultiCommitGens,
+    DEGREE_BOUND,
+};
+use libspartan::{
+    group::CompressedGroup,
+    transcript::{AppendToTranscript, ProofTranscript, Transcript},
+};
+use secpq_curves::Secq256k1;
+
+#[derive(Debug, Clone, Copy)]
+pub struct ZKDotProdProof {
+    pub delta: Secq256k1,
+    pub beta: Secq256k1,
+    pub z: [Fq; DEGREE_BOUND + 1],
+    pub z_delta: Fq,
+    pub z_beta: Fq,
+}
+
+// Utilities
+pub fn dot_prod(x: &[Fq], a: &[Fq]) -> Fq {
+    let mut result = Fq::zero();
+    for (x, a) in x.iter().zip(a.iter()) {
+        result += *x * *a;
+    }
+
+    result
+}
+
+// https://eprint.iacr.org/2017/1132.pdf
+// P.18, Figure 6, steps 4
+pub fn verify(
+    tau: &Secq256k1,
+    a: &[Fq],
+    proof: &ZKDotProdProof,
+    com_poly: &Secq256k1,
+    gens_1: &MultiCommitGens,
+    gens_n: &MultiCommitGens,
+    transcript: &mut Transcript,
+) -> bool {
+    transcript.append_protocol_name(b"dot product proof");
+
+    CompressedGroup::from_circuit_val(com_poly).append_to_transcript(b"Cx", transcript);
+
+    CompressedGroup::from_circuit_val(tau).append_to_transcript(b"Cy", transcript);
+
+    transcript.append_message(b"a", b"begin_append_vector");
+    for a_i in a {
+        transcript.append_message(b"a", &a_i.to_bytes());
+    }
+    transcript.append_message(b"a", b"end_append_vector");
+
+    CompressedGroup::from_circuit_val(&proof.delta).append_to_transcript(b"delta", transcript);
+
+    CompressedGroup::from_circuit_val(&proof.beta).append_to_transcript(b"beta", transcript);
+
+    let c = to_fq(&transcript.challenge_scalar(b"c"));
+
+    // (13)
+    let lhs = (com_poly * c) + proof.delta;
+    let rhs = proof.z.commit(&proof.z_delta, gens_n);
+
+    if lhs != rhs {
+        return false;
+    }
+
+    // (14)
+    let lhs = (tau * c) + proof.beta;
+    let rhs = dot_prod(&proof.z, a).commit(&proof.z_beta, gens_1);
+
+    if lhs != rhs {
+        return false;
+    }
+
+    return true;
+}

packages/hoplite/src/lib.rs

@@ -0,0 +1,152 @@
+use crate::sumcheck::ToCircuitVal;
+use commitments::MultiCommitGens;
+pub use libspartan::scalar::Scalar;
+use libspartan::{
+    math::Math,
+    transcript::{AppendToTranscript, ProofTranscript, Transcript},
+    Instance, NIZKGens, NIZK,
+};
+pub mod commitments;
+pub mod dotprod;
+pub mod sumcheck;
+use std::cmp::max;
+
+pub mod utils;
+
+pub type Fp = secpq_curves::Fq;
+pub type Fq = secpq_curves::Fp;
+use libspartan::commitments::Commitments;
+
+pub const DEGREE_BOUND: usize = 3;
+pub const N_ROUNDS: usize = 1;
+
+pub fn verify_nizk(
+    inst: &Instance,
+    num_cons: usize,
+    num_vars: usize,
+    input: &[libspartan::scalar::Scalar],
+    proof: &NIZK,
+    gens: &NIZKGens,
+) {
+    let mut transcript = Transcript::new(b"test_verify");
+
+    transcript.append_protocol_name(b"Spartan NIZK proof");
+    transcript.append_message(b"R1CSInstanceDigest", &inst.digest);
+
+    transcript.append_protocol_name(b"R1CS proof");
+    input.append_to_transcript(b"input", &mut transcript);
+
+    proof
+        .r1cs_sat_proof
+        .comm_vars
+        .append_to_transcript(b"poly_commitment", &mut transcript);
+
+    let num_rounds_x = if num_cons == 0 {
+        0
+    } else {
+        max(num_cons.log_2(), 1)
+    };
+    let _num_rounds_y = if num_vars == 0 {
+        0
+    } else {
+        (2 * num_vars).log_2()
+    };
+
+    let _tau = transcript.challenge_vector(b"challenge_tau", num_rounds_x);
+
+    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
+    // ############################
+
+    let sc_proof_phase1 = proof.r1cs_sat_proof.sc_proof_phase1.to_circuit_val();
+
+    let phase1_expected_sum = Scalar::zero()
+        .commit(&Scalar::zero(), &gens_1)
+        .compress()
+        .to_circuit_val();
+
+    assert!(sumcheck::verify(
+        &phase1_expected_sum,
+        &sc_proof_phase1,
+        &gens_1.into(),
+        &gens_4.into(),
+        &mut transcript,
+    ));
+
+    // ############################
+    // # Verify Phase 2 SumCheck
+    // ############################
+
+    // TBD
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use libspartan::{InputsAssignment, Instance, NIZKGens, VarsAssignment};
+
+    #[allow(non_snake_case)]
+    #[test]
+    fn test_verify_nizk() {
+        // 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,
+        );
+
+        // In the phase 1 sum check com_eval uses gens_1 and dot product uses gens_4
+        // com_eval uses gens_1, and dot product uses gen_3
+        verify_nizk(
+            &inst,
+            num_cons,
+            num_vars,
+            &assignment_inputs.assignment,
+            &proof,
+            &gens,
+        );
+    }
+}

packages/hoplite/src/sumcheck.rs

@@ -0,0 +1,227 @@
+use crate::{dotprod, dotprod::ZKDotProdProof, utils::to_fq, Fp, Fq, MultiCommitGens};
+use libspartan::{
+    group::CompressedGroup,
+    nizk::DotProductProof,
+    scalar::Scalar,
+    sumcheck::ZKSumcheckInstanceProof,
+    transcript::{AppendToTranscript, ProofTranscript, Transcript},
+};
+use secpq_curves::group::{prime::PrimeCurveAffine, Curve};
+use secpq_curves::{CurveAffine, Secq256k1, Secq256k1Affine};
+
+const N_ROUNDS: usize = 1;
+
+#[derive(Debug, Clone, Copy)]
+pub struct ZKSumCheckProof {
+    pub comm_polys: [Secq256k1; N_ROUNDS],
+    pub comm_evals: [Secq256k1; N_ROUNDS],
+    pub proofs: [ZKDotProdProof; N_ROUNDS],
+}
+
+// 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.
+pub trait ToCircuitVal<V> {
+    fn to_circuit_val(&self) -> V;
+}
+
+pub trait FromCircuitVal<V> {
+    fn from_circuit_val(v: &V) -> Self;
+}
+
+impl FromCircuitVal<Secq256k1> for CompressedGroup {
+    fn from_circuit_val(point: &Secq256k1) -> CompressedGroup {
+        if point.is_identity().into() {
+            return CompressedGroup::identity();
+        }
+
+        let coords = point.to_affine().coordinates().unwrap();
+        let mut x = coords.x().to_bytes();
+        let mut y = coords.y().to_bytes();
+
+        x.reverse();
+        y.reverse();
+
+        let result = CompressedGroup::from_affine_coordinates(&x.into(), &y.into(), true);
+
+        result
+    }
+}
+
+impl ToCircuitVal<Fq> for Scalar {
+    fn to_circuit_val(&self) -> Fq {
+        let bytes = self.to_bytes();
+        Fq::from_bytes(&bytes).unwrap()
+    }
+}
+use secq256k1::elliptic_curve::{
+    subtle::{Choice, ConditionallySelectable},
+    Field,
+};
+use secq256k1::{
+    affine::Group,
+    elliptic_curve::{subtle::ConstantTimeEq, PrimeField},
+};
+
+impl ToCircuitVal<Secq256k1> for CompressedGroup {
+    fn to_circuit_val(&self) -> Secq256k1 {
+        if self.is_identity() {
+            return Secq256k1::identity();
+        }
+
+        let mut x_bytes: [u8; 32] = (*self.x().unwrap()).try_into().unwrap();
+        // x_bytes is in big-endian!
+        x_bytes.reverse();
+
+        let x = Fp::from_bytes(&x_bytes).unwrap();
+
+        let coords = self.coordinates();
+        let y_odd: Choice = match coords.tag() {
+            secq256k1::elliptic_curve::sec1::Tag::CompressedOddY => Choice::from(1),
+            secq256k1::elliptic_curve::sec1::Tag::CompressedEvenY => Choice::from(0),
+            _ => Choice::from(0),
+        };
+
+        let x3 = x.square() * x;
+        let b = Fp::from_raw([7, 0, 0, 0]);
+        let y = (x3 + b).sqrt();
+
+        let res = y
+            .map(|y| {
+                let y = Fp::conditional_select(&-y, &y, y.is_odd().ct_eq(&y_odd));
+                let p = Secq256k1Affine::from_xy(x, y).unwrap();
+                p.to_curve()
+            })
+            .unwrap();
+
+        res
+    }
+}
+
+use crate::DEGREE_BOUND;
+
+impl ToCircuitVal<ZKDotProdProof> for DotProductProof {
+    fn to_circuit_val(&self) -> ZKDotProdProof {
+        assert!(self.z.len() == DEGREE_BOUND + 1);
+
+        ZKDotProdProof {
+            delta: self.delta.to_circuit_val(),
+            beta: self.beta.to_circuit_val(),
+            z_beta: self.z_beta.to_circuit_val(),
+            z_delta: self.z_delta.to_circuit_val(),
+            z: self
+                .z
+                .iter()
+                .map(|z_i| z_i.to_circuit_val())
+                .collect::<Vec<Fq>>()
+                .try_into()
+                .unwrap(),
+        }
+    }
+}
+
+impl ToCircuitVal<ZKSumCheckProof> for ZKSumcheckInstanceProof {
+    fn to_circuit_val(&self) -> ZKSumCheckProof {
+        assert!(self.proofs.len() == N_ROUNDS);
+
+        let mut dotprod_proofs = Vec::with_capacity(N_ROUNDS);
+        let mut comm_polys = Vec::with_capacity(N_ROUNDS);
+        let mut comm_evals = Vec::with_capacity(N_ROUNDS);
+        for i in 0..N_ROUNDS {
+            dotprod_proofs.push(self.proofs[i].to_circuit_val());
+            comm_polys.push(self.comm_polys[i].to_circuit_val());
+            comm_evals.push(self.comm_evals[i].to_circuit_val());
+        }
+
+        ZKSumCheckProof {
+            comm_polys: comm_polys.try_into().unwrap(),
+            comm_evals: comm_evals.try_into().unwrap(),
+            proofs: dotprod_proofs.try_into().unwrap(),
+        }
+    }
+}
+
+#[derive(Debug, Clone)]
+pub struct RoundProof {
+    pub dotprod_proof: ZKDotProdProof,
+    pub com_eval: Secq256k1,
+}
+
+// This function should be able to verify proofs generated by the above `prove` function
+// and also the proofs generated by the original Spartan implementation
+#[allow(dead_code)]
+pub fn verify(
+    target_com: &Secq256k1,
+    proof: &ZKSumCheckProof,
+    gens_1: &MultiCommitGens,
+    gens_n: &MultiCommitGens,
+    transcript: &mut Transcript,
+) -> bool {
+    for (i, round_dotprod_proof) in proof.proofs.iter().enumerate() {
+        let com_poly = &proof.comm_polys[i];
+        let com_poly_encoded = CompressedGroup::from_circuit_val(com_poly);
+        com_poly_encoded.append_to_transcript(b"comm_poly", transcript);
+
+        let com_eval = &proof.comm_evals[i];
+
+        let r_i = to_fq(&transcript.challenge_scalar(b"challenge_nextround"));
+
+        // The sum over (0, 1) is expected to be equal to the challenge evaluation of the prev round
+        let com_round_sum = if i == 0 {
+            target_com
+        } else {
+            &proof.comm_evals[i - 1]
+        };
+
+        let com_round_sum_encoded = CompressedGroup::from_circuit_val(com_round_sum);
+        com_round_sum_encoded.append_to_transcript(b"comm_claim_per_round", transcript);
+
+        CompressedGroup::from_circuit_val(&com_eval.clone())
+            .append_to_transcript(b"comm_eval", transcript);
+
+        let w_scalar = transcript.challenge_vector(b"combine_two_claims_to_one", 2);
+
+        let w = w_scalar.iter().map(|x| to_fq(x)).collect::<Vec<Fq>>();
+
+        let degree_bound = 3;
+        let a = {
+            // the vector to use to decommit for sum-check test
+            let a_sc = {
+                let mut a = vec![Fq::one(); degree_bound + 1];
+                a[0] += Fq::one();
+                a
+            };
+
+            // the vector to use to decommit for evaluation
+            let a_eval = {
+                let mut a = vec![Fq::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<Fq>>()
+        };
+
+        let tau = com_round_sum * w[0] + com_eval * w[1];
+
+        // Check that the dot product proofs are valid
+        if !dotprod::verify(
+            &tau,
+            &a,
+            &round_dotprod_proof,
+            com_poly,
+            &gens_1,
+            &gens_n,
+            transcript,
+        ) {
+            return false;
+        }
+    }
+
+    true
+}

packages/hoplite/src/utils.rs

@@ -0,0 +1,22 @@
+use crate::{Fp, Fq};
+
+pub fn hypercube(n: u32) -> Vec<Vec<u8>> {
+    let mut v = vec![];
+    for i in 0..(2u64.pow(n)) {
+        let mut row = vec![];
+        for j in 0..n {
+            row.push(((i >> j) & 1) as u8);
+        }
+        v.push(row);
+    }
+
+    v
+}
+
+pub fn to_fp(x: &libspartan::scalar::Scalar) -> Fp {
+    Fp::from_bytes(&x.to_bytes().into()).unwrap()
+}
+
+pub fn to_fq(x: &libspartan::scalar::Scalar) -> Fq {
+    Fq::from_bytes(&x.to_bytes().into()).unwrap()
+}

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,
+        }
+    }
+}