Merge pull request #6 from mileschet/feature/lisp

Feature/lisp

lisp/lisp.rs

@@ -1,27 +1,18 @@
 #![allow(non_snake_case)]
 
 use crate::types::LispCircuit;
-use crate::MalVal::Zk;
 use bellman::groth16::PreparedVerifyingKey;
-use sapvi::{ZKVMCircuit, ZKVirtualMachine};
 
 use simplelog::*;
 
-use bellman::{gadgets::Assignment, groth16, Circuit, ConstraintSystem, SynthesisError};
+use bellman::{groth16};
 use bls12_381::Bls12;
-use bls12_381::Scalar;
-use ff::PrimeField;
 use fnv::FnvHashMap;
 use itertools::Itertools;
 use rand::rngs::OsRng;
 use std::time::Instant;
-use std::{borrow::BorrowMut, rc::Rc};
-use std::{
-    cell::RefCell,
-    ops::{AddAssign, MulAssign, SubAssign},
-};
+use std::{rc::Rc};
 use types::EnforceAllocation;
-use MalVal::ZKScalar;
 
 #[macro_use]
 extern crate clap;
@@ -307,8 +298,8 @@ fn eval(mut ast: MalVal, mut env: Env) -> MalRet {
                         continue 'tco;
                     }
                     Sym(ref a0sym) if a0sym == "prove" => {
-                        let a1 = l[0].clone();
-                        println!("prove {:?}", a1);
+                        let a1 = l[1].clone();
+                        ast = eval(a1.clone(), env.clone())?;
                         prove(a1.clone(), env.clone())
                     }
                     Sym(ref a0sym) if a0sym == "alloc-input" => {
@@ -534,25 +525,23 @@ pub fn prove(_ast: MalVal, env: Env) -> MalRet {
     // TODO remove it
     let _quantity = bls12_381::Scalar::from(3);
 
-    // Create an instance of our circuit (with the preimage as a witness).
-    let params = {
-        let c = LispCircuit {
-            params: vec![],
-            allocs: FnvHashMap::default(),
-            alloc_inputs: FnvHashMap::default(),
-            constraints: vec![],
-            env: env.clone(),
-        };
-        groth16::generate_random_parameters::<Bls12, _, _>(c, &mut OsRng).unwrap()
-    };
+    let allocs_input = get_allocations(&env, "AllocationsInput");
+    let allocs = get_allocations(&env, "Allocations");
+    let enforce_allocs = get_enforce_allocs(&env);
 
     let circuit = LispCircuit {
         params: vec![],
-        allocs: FnvHashMap::default(),
-        alloc_inputs: FnvHashMap::default(),
-        constraints: vec![],
+        allocs: allocs.as_ref().clone(),
+        alloc_inputs: allocs_input.as_ref().clone(),
+        constraints: enforce_allocs,
         env: env.clone(),
     };
+    // Create an instance of our circuit (with the preimage as a witness).
+    // todo check if circuit.clone is valid
+    let params = {
+        let c = circuit.clone();
+        groth16::generate_random_parameters::<Bls12, _, _>(c, &mut OsRng).unwrap()
+    };
     let start = Instant::now();
     // Create a Groth16 proof with our parameters.
     let _proof = groth16::create_random_proof(circuit, &params, &mut OsRng).unwrap();

lisp/new-cs.lisp

@@ -6,8 +6,8 @@
       x3 (alloc "x3" (* aux (* aux aux)))
       input (alloc-input "input" aux)
       ]
+(prove
  (setup 
-   ;; (enforce left right output)
   (
   (enforce  
     (
@@ -33,6 +33,6 @@
   )
   )
  )
-(prove)
+)
 )
 ;; (println 'verify  (MyCircuit (scalar 27)))

lisp/run.sh

@@ -1 +1,2 @@
+#export RUST_BACKTRACE=full
 cargo run --bin lisp load new-cs.lisp

lisp/types.rs

@@ -1,6 +1,10 @@
-use bellman::Circuit;
-use bellman::ConstraintSystem;
-use bellman::SynthesisError;
+use bellman::{
+    gadgets::{
+        Assignment,
+    },
+    groth16, Circuit, ConstraintSystem, SynthesisError,
+};
+use std::ops::{Add, AddAssign, MulAssign, SubAssign};
 use std::cell::RefCell;
 use std::rc::Rc;
 //use std::collections::HashMap;
@@ -10,6 +14,7 @@ use itertools::Itertools;
 use crate::env::{env_bind, Env};
 use crate::types::MalErr::{ErrMalVal, ErrString};
 use crate::types::MalVal::{Atom, Bool, Func, Hash, Int, List, MalFunc, Nil, Str, Sym, Vector};
+use bellman::Variable;
 use bls12_381::Scalar;
 
 #[derive(Debug, Clone)]
@@ -37,11 +42,84 @@ pub struct LispCircuit {
 impl Circuit<bls12_381::Scalar> for LispCircuit {
     fn synthesize<CS: ConstraintSystem<bls12_381::Scalar>>(
         self,
-        _cs: &mut CS,
+        cs: &mut CS,
     ) -> Result<(), SynthesisError> {
-        println!("something called this");
-        for alloc_value in &self.allocs {
+        let mut variables: FnvHashMap<String, Variable> = FnvHashMap::default();
+
+        println!("Allocations\n");
+        for (k, v) in &self.allocs {
+            if let MalVal::ZKScalar(val) = v {
+                println!("val {:?}", val);
+                let var = cs.alloc(|| "alloc", || Ok(*val))?;
+                variables.insert(k.to_string(), var);
+            } else {
+                println!("k {:?} v {:?}", k, v);
+            }
+        }
+
+        println!("Allocations Input\n");
+        for (k, v) in &self.alloc_inputs {
+            if let MalVal::ZKScalar(val) = v {
+                println!("val {:?}", val);
+                let var = cs.alloc_input(|| "alloc", || Ok(*val))?;
+                variables.insert(k.to_string(), var);
+            } else {
+                println!("k {:?} v {:?}", k, v);
+            }
+        }
+
+        println!("Enforce Allocations\n");
+        for alloc_value in &self.constraints {
             println!("{:?}", alloc_value);
+            let coeff = bls12_381::Scalar::one();
+            let mut left = bellman::LinearCombination::<Scalar>::zero();
+            let mut right = bellman::LinearCombination::<Scalar>::zero();
+            let mut output = bellman::LinearCombination::<Scalar>::zero();
+            for values in alloc_value.left.iter() {
+                let (a, b) = values;
+                let mut val_b = CS::one();
+                if b != "cs::one" {
+                    val_b = *variables.get(b).unwrap();
+                }
+                if a == "scalar::one" {
+                    left = left + (coeff, val_b);
+                } else if a == "scalar::one::neg" {
+                    left = left + (coeff.neg(), val_b);
+                } 
+            }
+
+            for values in alloc_value.right.iter() {
+                let (a, b) = values;
+                let mut val_b = CS::one();
+                if b != "cs::one" {
+                    val_b = *variables.get(b).unwrap();
+                }
+                if a == "scalar::one" {
+                    right = right + (coeff, val_b);
+                } else if a == "scalar::one::neg" {
+                    right = right + (coeff.neg(), val_b);
+                } 
+            }
+
+            for values in alloc_value.output.iter() {
+                let (a, b) = values;
+                let mut val_b = CS::one();
+                if b != "cs::one" {
+                    val_b = *variables.get(b).unwrap();
+                }
+                if a == "scalar::one" {
+                    output = output + (coeff, val_b);
+                } else if a == "scalar::one::neg" {
+                    output = output + (coeff.neg(), val_b);
+                } 
+            }
+
+            cs.enforce(
+                || "constraint",
+                |_| left.clone(),
+                |_| right.clone(),
+                |_| output.clone(),
+            );
         }
 
         Ok(())