diff --git a/phase2/src/bin/prove.rs b/phase2/src/bin/prove.rs
new file mode 100644
index 0000000..793e648
--- /dev/null
+++ b/phase2/src/bin/prove.rs
@@ -0,0 +1,64 @@
+#![allow(unused_imports)]
+
+extern crate phase2;
+extern crate bellman_ce;
+
+use phase2::circom_circuit::CircomCircuit;
+use std::fs::OpenOptions;
+use phase2::parameters::MPCParameters;
+use bellman_ce::groth16::{Proof, generate_random_parameters, prepare_verifying_key, create_random_proof, verify_proof};
+use std::sync::Arc;
+
+use bellman_ce::pairing::bn256::{
+    Bn256,
+};
+
+use bellman_ce::pairing::{
+    Engine,
+    CurveAffine,
+    ff::{
+        Field,
+        PrimeField,
+    },
+};
+
+use bellman_ce::{
+    Circuit,
+    SynthesisError,
+    Variable,
+    Index,
+    ConstraintSystem,
+    LinearCombination,
+};
+
+fn main() {
+    let should_filter_points_at_infinity = false;
+    let rng = &mut rand::XorShiftRng::new_unseeded(); // TODO: change this unsafe unseeded random (!)
+
+    let mut c = CircomCircuit::from_json("circuit.json");
+    c.load_witness_json("witness.json");
+    let input = c.inputs.to_vec();
+
+    let reader = OpenOptions::new()
+        .read(true)
+        .open("circom4.params")
+        .expect("unable to open.");
+
+    let mut params = MPCParameters::read(reader, should_filter_points_at_infinity, true).expect("unable to read params");
+
+    params.filter_params();
+    let params = params.get_params();
+
+    println!("Proving...");
+    let proof = create_random_proof(c, &*params, rng).unwrap();
+
+    println!("Checking proof");
+    let pvk = prepare_verifying_key(&params.vk);
+    let result = verify_proof(
+        &pvk,
+        &proof,
+        &input[1..]
+    ).unwrap();
+    assert!(result, "Proof is correct");
+    println!("Done!")
+}
\ No newline at end of file
diff --git a/phase2/src/circom_circuit.rs b/phase2/src/circom_circuit.rs
index 7d4d424..0d262ac 100644
--- a/phase2/src/circom_circuit.rs
+++ b/phase2/src/circom_circuit.rs
@@ -34,63 +34,99 @@ struct CircuitJson {
     pub num_variables: usize,
 }
 
-pub struct CircomCircuit<'a> {
-    pub file_name: &'a str,
+#[derive(Clone)]
+pub struct CircomCircuit<E: Engine> {
+    pub num_inputs: usize,
+    pub num_aux: usize,
+    pub num_constraints: usize,
+    pub inputs: Vec<E::Fr>,
+    pub aux: Vec<E::Fr>,
+    pub constraints: Vec<(
+        Vec<(usize, E::Fr)>,
+        Vec<(usize, E::Fr)>,
+        Vec<(usize, E::Fr)>,
+    )>,
+}
+
+impl<'a, E: Engine> CircomCircuit<E> {
+    pub fn load_witness_json(&mut self, filename: &str) {
+        let witness: Vec<String> = serde_json::from_str(&fs::read_to_string(filename).unwrap()).unwrap();
+        let witness = witness.into_iter().map(|x| E::Fr::from_str(&x).unwrap()).collect::<Vec<E::Fr>>();
+        self.inputs = witness[..self.num_inputs].to_vec();
+        self.aux = witness[self.num_inputs..].to_vec();
+    }
+
+    pub fn from_json(filename: &str) -> CircomCircuit::<E> {
+        let circuit_json: CircuitJson = serde_json::from_str(&fs::read_to_string(filename).unwrap()).unwrap();
+
+        let num_inputs = circuit_json.num_inputs + circuit_json.num_outputs + 1;
+        let num_aux = circuit_json.num_variables - num_inputs;
+
+        fn convert_constraint<EE: Engine>(lc: &BTreeMap<String, String>) -> Vec<(usize, EE::Fr)> {
+            let mut coeffs = vec![];
+            for (var_index_str, coefficient_str) in lc {
+                coeffs.push((var_index_str.parse().unwrap(), EE::Fr::from_str(coefficient_str).unwrap()));
+            }
+            return coeffs;
+        }
+
+        let mut constraints = vec![];
+        for constraint in circuit_json.constraints.iter() {
+            constraints.push((convert_constraint::<E>(&constraint[0]), convert_constraint::<E>(&constraint[1]), convert_constraint::<E>(&constraint[2])));
+        }
+
+        return CircomCircuit {
+            num_inputs: num_inputs,
+            num_aux: num_aux,
+            num_constraints: circuit_json.num_variables,
+            inputs: vec![],
+            aux: vec![],
+            constraints: constraints,
+        };
+    }
 }
 
 /// Our demo circuit implements this `Circuit` trait which
 /// is used during paramgen and proving in order to
 /// synthesize the constraint system.
-impl<'a, E: Engine> Circuit<E> for CircomCircuit<'a> {
+impl<'a, E: Engine> Circuit<E> for CircomCircuit<E> {
     fn synthesize<CS: ConstraintSystem<E>>(
         self,
         cs: &mut CS
     ) -> Result<(), SynthesisError>
     {
-        let content = fs::read_to_string(self.file_name)?;
-        let circuit_json: CircuitJson = serde_json::from_str(&content).unwrap();
-        let num_public_inputs = circuit_json.num_inputs + circuit_json.num_outputs + 1;
-        for i in 1..circuit_json.num_variables {
-            if i < num_public_inputs {
-                cs.alloc_input(|| format!("variable {}", i), || {
-                    Ok(E::Fr::from_str("1").unwrap())
-                })?;
-            } else {
-                cs.alloc(|| format!("variable {}", i), || {
-                    Ok(E::Fr::from_str("1").unwrap())
-                })?;
-            }
+        for i in 1..self.num_inputs {
+            cs.alloc_input(|| format!("variable {}", i),
+                           || {
+                Ok(if self.inputs.len() > 0 { self.inputs[i] } else { E::Fr::from_str("1").unwrap() })
+            })?;
         }
-        let mut constrained: BTreeMap<usize, bool> = BTreeMap::new();
-        let mut constraint_num = 0;
-        for (_i, constraint) in circuit_json.constraints.iter().enumerate() {
-            let mut lcs = vec![];
-            for lc_description in constraint {
-                let mut lc = LinearCombination::<E>::zero();
-                for (var_index_str, coefficient_str) in lc_description {
-                    let var_index_num: usize = var_index_str.parse().unwrap();
-                    let var_index = if var_index_num < num_public_inputs {
-                        Index::Input(var_index_num)
-                    } else {
-                        Index::Aux(var_index_num - num_public_inputs)
-                    };
-                    constrained.insert(var_index_num, true);
-                    lc = lc + (E::Fr::from_str(coefficient_str).unwrap(), Variable::new_unchecked(var_index));
-                }
-                lcs.push(lc);
-            }
-            cs.enforce(|| format!("constraint {}", constraint_num), |_| lcs[0].clone(), |_| lcs[1].clone(), |_| lcs[2].clone());
-            constraint_num += 1;
+
+        for i in 0..self.num_aux {
+            cs.alloc(|| format!("aux {}", i),
+                           || {
+                Ok(if self.aux.len() > 0 { self.aux[i] } else { E::Fr::from_str("1").unwrap() })
+            })?;
         }
-        println!("constraints: {}", circuit_json.constraints.len());
-        let mut unconstrained: BTreeMap<usize, bool> = BTreeMap::new();
-        for i in 0..circuit_json.num_variables {
-            if !constrained.contains_key(&i) {
-                unconstrained.insert(i, true);
+
+        fn make_lc<E: Engine>(lc_data: Vec<(usize, E::Fr)>, num_inputs: usize) -> LinearCombination<E> {
+            let mut lc = LinearCombination::<E>::zero();
+            for (index, coeff) in lc_data {
+                let var_index = if index < num_inputs {
+                    Index::Input(index)
+                } else {
+                    Index::Aux(index - num_inputs)
+                };
+                lc = lc + (coeff, Variable::new_unchecked(var_index))
             }
+            return lc;
         }
-        for (i, _) in unconstrained {
-            println!("variable {} is unconstrained", i);
+        for (i, constraint) in self.constraints.iter().enumerate() {
+            cs.enforce(|| format!("constraint {}", i),
+                       |_| make_lc(constraint.0.clone(), self.num_inputs),
+                       |_| make_lc(constraint.1.clone(), self.num_inputs),
+                       |_| make_lc(constraint.2.clone(), self.num_inputs),
+            );
         }
         Ok(())
     }
diff --git a/phase2/src/parameters.rs b/phase2/src/parameters.rs
index db380ef..1c6dd32 100644
--- a/phase2/src/parameters.rs
+++ b/phase2/src/parameters.rs
@@ -401,6 +401,14 @@ impl MPCParameters {
         &self.params
     }
 
+    pub fn filter_params(&mut self) {
+        self.params.vk.ic = self.params.vk.ic.clone().into_iter().filter(|x| !x.is_zero()).collect::<Vec<_>>();
+        self.params.h = Arc::new((*self.params.h).clone().into_iter().filter(|x| !x.is_zero()).collect::<Vec<_>>());
+        self.params.a = Arc::new((*self.params.a).clone().into_iter().filter(|x| !x.is_zero()).collect::<Vec<_>>());
+        self.params.b_g1 = Arc::new((*self.params.b_g1).clone().into_iter().filter(|x| !x.is_zero()).collect::<Vec<_>>());
+        self.params.b_g2 = Arc::new((*self.params.b_g2).clone().into_iter().filter(|x| !x.is_zero()).collect::<Vec<_>>());
+    }
+
     /// Contributes some randomness to the parameters. Only one
     /// contributor needs to be honest for the parameters to be
     /// secure.