diff --git a/lisp/core.rs b/lisp/core.rs
index b641aac3d..3a721c265 100644
--- a/lisp/core.rs
+++ b/lisp/core.rs
@@ -254,6 +254,22 @@ fn conj(a: MalArgs) -> MalRet {
 
 fn sub_scalar(a: MalArgs) -> MalRet {
     match (a[0].clone(), a[1].clone()) {
+        (Func(_, _), ZKScalar(a1)) => {
+            if let Vector(ref values, _) = a[0].apply(vec![]).unwrap() {
+                if let ZKScalar(mut a0) = values[0] {
+                    a0.sub_assign(a1);
+                    Ok(ZKScalar(a0))
+                } else {
+                    error("scalar sub expect (zkscalar, zkscalar) found (func, zkscalar)")
+                }
+            } else {
+                error("scalar sub expect (zkscalar, zkscalar)")
+            }
+        }
+        (ZKScalar(mut a0), ZKScalar(a1)) => {
+            a0.sub_assign(a1);
+            Ok(ZKScalar(a0))
+        }
         (Str(a0), Str(a1)) => {
             let (mut s0, s1) = (
                 bls12_381::Scalar::from_string(&a0),
@@ -262,7 +278,7 @@ fn sub_scalar(a: MalArgs) -> MalRet {
             s0.sub_assign(s1);
             Ok(Str(std::string::ToString::to_string(&s0)[2..].to_string()))
         }
-        _ => error("scalar sub expected (scalar, scalar)"),
+        _ => error("scalar sub expected (zkscalar, zkscalar)"),
     }
 }
 
@@ -384,6 +400,18 @@ fn scalar_from(a: MalArgs) -> MalRet {
 
 fn add_scalar(a: MalArgs) -> MalRet {
     match (a[0].clone(), a[1].clone()) {
+        (Func(_, _), ZKScalar(a1)) => {
+            if let Vector(ref values, _) = a[0].apply(vec![]).unwrap() {
+                if let ZKScalar(mut a0) = values[0] {
+                    a0.add_assign(a1);
+                    Ok(ZKScalar(a0))
+                } else {
+                    error("scalar add expect (zkscalar, zkscalar) found (func, zkscalar)")
+                }
+            } else {
+                error("scalar add expect (zkscalar, zkscalar)")
+            }
+        }
         (ZKScalar(a0), ZKScalar(a1)) => {
             let (mut z0, z1) = (a0.clone(), a1.clone());
             z0.add_assign(z1);
@@ -397,7 +425,7 @@ fn add_scalar(a: MalArgs) -> MalRet {
             s0.add_assign(s1);
             Ok(ZKScalar(s0))
         }
-        _ => error(&format!("add scalar expected (scalar, scalar)\n {:?}", a).to_string()),
+        _ => error(&format!("scalar add expect (zkscalar, zkscalar) found \n {:?}", a).to_string()),
     }
 }
 
diff --git a/lisp/inverse.lisp b/lisp/inverse.lisp
new file mode 100644
index 000000000..34aa17c42
--- /dev/null
+++ b/lisp/inverse.lisp
@@ -0,0 +1,34 @@
+(println "new-cs.lisp")
+
+( (let* [aux (scalar 3)
+      x (alloc "x" aux)
+      x2 (alloc "x2" (* aux aux))
+      x3 (alloc "x3" (* aux (* aux aux)))
+      input (alloc-input "input" (scalar 3))
+      ]
+(prove
+ (setup 
+  (
+  (enforce 
+    (scalar::one input)
+    (scalar::one cs::one)
+    (scalar::one x3)  
+  )
+
+  (enforce 
+    (scalar::one x2)
+    (scalar::one x)
+    (scalar::one x3)
+  )
+
+  (enforce  
+    (scalar::one x)
+    (scalar::one x)
+    (scalar::one x2)
+  )
+  )
+  )
+ )
+)
+)
+;; (println 'verify  (MyCircuit (scalar 27)))
diff --git a/lisp/jubjub-add.lisp b/lisp/jubjub-add.lisp
index 0abff8ff1..9ad56cec3 100644
--- a/lisp/jubjub-add.lisp
+++ b/lisp/jubjub-add.lisp
@@ -1,30 +1,29 @@
 (println "jubjub-add.lisp")
-;; Compute U = (u1 + v1) * (v2 - EDWARDS_A*u2)
-;;           = (u1 + v1) * (u2 + v2)
-( (let* [
+(def! param1 (scalar "15a36d1f0f390d8852a35a8c1908dd87a361ee3fd48fdf77b9819dc82d90607e"))
+(def! param2 (scalar "015d8c7f5b43fe33f7891142c001d9251f3abeeb98fad3e87b0dc53c4ebf1891"))
+(def! param3 (scalar "15a36d1f0f390d8852a35a8c1908dd87a361ee3fd48fdf77b9819dc82d90607e"))
+(def! param4 (scalar "015d8c7f5b43fe33f7891142c001d9251f3abeeb98fad3e87b0dc53c4ebf1891"))
+
+(
+    (let* [
+      u1 (alloc-input "u1" param1)
+      v1 (alloc-input "v1" param2)
+      u2 (alloc-input  "u2" param3)
+      v2 (alloc-input  "v2" param4)
       EDWARDS_D (alloc-const "EDWARDS_D" (scalar "2a9318e74bfa2b48f5fd9207e6bd7fd4292d7f6d37579d2601065fd6d6343eb1"))
-      u1 (alloc-input "u1" (scalar "15a36d1f0f390d8852a35a8c1908dd87a361ee3fd48fdf77b9819dc82d90607e"))
-      v1 (alloc-input "v1" (scalar "015d8c7f5b43fe33f7891142c001d9251f3abeeb98fad3e87b0dc53c4ebf1891"))
-      u2 (alloc-input  "u2" (scalar "15a36d1f0f390d8852a35a8c1908dd87a361ee3fd48fdf77b9819dc82d90607e"))
-      v2 (alloc-input  "v2" (scalar "015d8c7f5b43fe33f7891142c001d9251f3abeeb98fad3e87b0dc53c4ebf1891"))
       U (alloc "U" (* (+ u1 u2) (+ v1 v2)))
       A (alloc "A" (* v2 u1))
       B (alloc "B" (* u2 v1))
       C (alloc "C" (* EDWARDS_D (* A B)))
-      u3 (alloc "u3" (/ (* A A) (* scalar::one C)))
+      u3 (alloc "u3" (/ (+ A B) (+ scalar::one C)))
+      v3 (alloc "v3" (/ (- (- U A) B) (- scalar::one C)))
       ]
-(prove
- (setup 
+    (prove
+        (setup 
   (
   (enforce  
-    (
-     (scalar::one u1)
-     (scalar::one v1)
-    )
-    (
-     (scalar::one u2)
-     (scalar::one v2)
-    )
+    ((scalar::one u1) (scalar::one v1))
+    ((scalar::one u2) (scalar::one v2))
     (scalar::one U)
   )
   (enforce
@@ -32,9 +31,17 @@
     (scalar::one B)
     (scalar::one C)
   )
+  (enforce
+    (scalar::one C)
+    (scalar::one u3)
+    ((scalar::one A) (scalar::one B))
+  )
+  (enforce
+    (scalar::one::neg C)
+    (scalar::one v3)
+    ((scalar::one::neg U) (scalar::one::neg A) (scalar::one::neg B))
+  )
   )
  )
-)
-)
- )
+)))
 ;; (println 'verify  (MyCircuit (scalar 27)))
diff --git a/lisp/lisp.rs b/lisp/lisp.rs
index 4f322c0ee..be133575e 100644
--- a/lisp/lisp.rs
+++ b/lisp/lisp.rs
@@ -3,15 +3,18 @@
 use crate::types::LispCircuit;
 use bellman::groth16::PreparedVerifyingKey;
 
+use sapvi::{BlsStringConversion, Decodable, Encodable, ZKContract, ZKProof};
 use simplelog::*;
 
-use bellman::{groth16};
+use bellman::groth16;
 use bls12_381::Bls12;
 use fnv::FnvHashMap;
 use itertools::Itertools;
 use rand::rngs::OsRng;
+use std::fs;
+use std::fs::File;
+use std::rc::Rc;
 use std::time::Instant;
-use std::{rc::Rc};
 use types::EnforceAllocation;
 
 #[macro_use]
@@ -518,17 +521,12 @@ pub fn setup(_ast: MalVal, env: Env) -> Result<PreparedVerifyingKey<Bls12>, MalE
     let start = Instant::now();
     // Create parameters for our circuit. In a production deployment these would
     // be generated securely using a multiparty computation.
-    let allocs_input = get_allocations(&env, "AllocationsInput");
-    let allocs = get_allocations(&env, "Allocations");
-    let allocs_const = get_allocations(&env, "AllocationsConst");
-    let enforce_allocs = get_enforce_allocs(&env);
 
     let c = LispCircuit {
-        params: allocs_const.as_ref().clone(),
-        allocs: allocs.as_ref().clone(),
-        alloc_inputs: allocs_input.as_ref().clone(),
-        constraints: enforce_allocs,
-        env: env.clone(),
+        params: None,
+        allocs: None,
+        alloc_inputs: None,
+        constraints: None,
     };
     // TODO move to another fn
     let random_parameters =
@@ -540,31 +538,40 @@ pub fn setup(_ast: MalVal, env: Env) -> Result<PreparedVerifyingKey<Bls12>, MalE
 }
 
 pub fn prove(_ast: MalVal, env: Env) -> MalRet {
-    // TODO remove it
-    let _quantity = bls12_381::Scalar::from(3);
-
     let allocs_input = get_allocations(&env, "AllocationsInput");
     let allocs = get_allocations(&env, "Allocations");
     let enforce_allocs = get_enforce_allocs(&env);
     let allocs_const = get_allocations(&env, "AllocationsConst");
 
+    let start = Instant::now();
     let circuit = LispCircuit {
-        params:  allocs_const.as_ref().clone(),
-        allocs: allocs.as_ref().clone(),
-        alloc_inputs: allocs_input.as_ref().clone(),
-        constraints: enforce_allocs,
-        env: env.clone(),
+        params: Some(allocs_const.as_ref().clone()),
+        allocs: Some(allocs.as_ref().clone()),
+        alloc_inputs: Some(allocs_input.as_ref().clone()),
+        constraints: Some(enforce_allocs),
     };
-    // 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();
+
+    let proof = groth16::create_random_proof(circuit, &params, &mut OsRng).unwrap();
+    let mut buf = File::create("proof.output").unwrap();
+    proof.write(buf);
     println!("Prove: [{:?}]", start.elapsed());
+    let proof_file = File::open("proof.output").unwrap();
+    let reader = std::io::BufReader::new(proof_file);
+    let proof_read: groth16::Proof<bls12_381::Bls12> = groth16::Proof::read(reader).unwrap();
+    let mut vec_input = vec![];
+    for (k, val) in allocs_input.iter() {
+        if let MalVal::ZKScalar(v) = val {
+            vec_input.push(*v);
+        }
+    }
+    let pvk = setup(_ast.clone(), env.clone()).unwrap();
+    println!("{:?}", vec_input);
+    let verify_result = groth16::verify_proof(&pvk, &proof, &vec_input.as_slice());
+    println!("{:?}", verify_result);
     Ok(MalVal::Nil)
 }
 
diff --git a/lisp/new-cs.lisp b/lisp/new-cs.lisp
index bc33782e2..f28a446cf 100644
--- a/lisp/new-cs.lisp
+++ b/lisp/new-cs.lisp
@@ -4,17 +4,13 @@
       x (alloc "x" aux)
       x2 (alloc "x2" (* aux aux))
       x3 (alloc "x3" (* aux (* aux aux)))
-      input (alloc-input "input" aux)
+      input (alloc-input "input" (scalar 27))
       ]
 (prove
  (setup 
   (
   (enforce  
-    (
-     (scalar::one x)
-     (scalar::one x2)
-    )
-    ;;(scalar::one::neg x)
+    (scalar::one x)
     (scalar::one x)
     (scalar::one x2)
   )
diff --git a/lisp/run.sh b/lisp/run.sh
index 9f0c05186..9d9b6f16d 100755
--- a/lisp/run.sh
+++ b/lisp/run.sh
@@ -1,2 +1,3 @@
-#export RUST_BACKTRACE=full
-cargo run --bin lisp load jubjub-add.lisp
+export RUST_BACKTRACE=full
+#cargo run --bin lisp load jubjub-add.lisp
+cargo run --bin lisp load inverse.lisp
diff --git a/lisp/types.rs b/lisp/types.rs
index 4c4367a36..129fad361 100644
--- a/lisp/types.rs
+++ b/lisp/types.rs
@@ -1,11 +1,7 @@
-use bellman::{
-    gadgets::{
-        Assignment,
-    },
-    groth16, Circuit, ConstraintSystem, SynthesisError,
-};
-use std::ops::{Add, AddAssign, MulAssign, SubAssign};
+use bellman::{gadgets::Assignment, groth16, Circuit, ConstraintSystem, SynthesisError};
+use sapvi::bls_extensions::BlsStringConversion;
 use std::cell::RefCell;
+use std::ops::{Add, AddAssign, MulAssign, SubAssign};
 use std::rc::Rc;
 //use std::collections::HashMap;
 use fnv::FnvHashMap;
@@ -32,11 +28,10 @@ pub struct EnforceAllocation {
 
 #[derive(Debug, Clone)]
 pub struct LispCircuit {
-    pub params: FnvHashMap<String, MalVal>,
-    pub allocs: FnvHashMap<String, MalVal>,
-    pub alloc_inputs: FnvHashMap<String, MalVal>,
-    pub constraints: Vec<EnforceAllocation>,
-    pub env: Env,
+    pub params: Option<FnvHashMap<String, MalVal>>,
+    pub allocs: Option<FnvHashMap<String, MalVal>>,
+    pub alloc_inputs: Option<FnvHashMap<String, MalVal>>,
+    pub constraints: Option<Vec<EnforceAllocation>>,
 }
 
 impl Circuit<bls12_381::Scalar> for LispCircuit {
@@ -45,39 +40,56 @@ impl Circuit<bls12_381::Scalar> for LispCircuit {
         cs: &mut CS,
     ) -> Result<(), SynthesisError> {
         let mut variables: FnvHashMap<String, Variable> = FnvHashMap::default();
+        let mut params_const = self.params.unwrap_or(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);
+        for (k, v) in &self.allocs.unwrap_or(FnvHashMap::default()) {
+            println!("k {:?} v {:?}", k, v);
+            match v {
+                MalVal::ZKScalar(val) => {
+                    let var = cs.alloc(|| "alloc", || Ok(*val))?;
+                    variables.insert(k.to_string(), var);
+                }
+                MalVal::Str(val) => {
+                    let val_scalar = bls12_381::Scalar::from_string(&*val);
+                    let var = cs.alloc(|| "alloc", || Ok(val_scalar))?;
+                    variables.insert(k.to_string(), var);
+                }
+                _ => {
+                    println!("not allocated 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);
+        for (k, v) in &self.alloc_inputs.unwrap_or(FnvHashMap::default()) {
+            println!("k {:?} v {:?}", k, v);
+            match v {
+                MalVal::ZKScalar(val) => {
+                    let var = cs.alloc_input(|| "alloc", || Ok(*val))?;
+                    variables.insert(k.to_string(), var);
+                }
+                MalVal::Str(val) => {
+                    let val_scalar = bls12_381::Scalar::from_string(&*val);
+                    let var = cs.alloc_input(|| "alloc", || Ok(val_scalar))?;
+                    variables.insert(k.to_string(), var);
+                }
+                _ => {
+                    println!("not allocated k {:?} v {:?}", k, v);
+                }
             }
         }
 
         println!("Enforce Allocations\n");
-        for alloc_value in &self.constraints {
-            println!("{:?}", alloc_value);
+        // we need to keep order 
+        for alloc_value in self.constraints.unwrap_or(Vec::<EnforceAllocation>::new()).iter() {
             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() {
-                println!("values {:?}", values);
                 let (a, b) = values;
+                println!("a {:?} b {:?}", a, b);
                 let mut val_b = CS::one();
                 if b != "cs::one" {
                     val_b = *variables.get(b).unwrap();
@@ -87,11 +99,11 @@ impl Circuit<bls12_381::Scalar> for LispCircuit {
                 } else if a == "scalar::one::neg" {
                     left = left + (coeff.neg(), val_b);
                 } else {
-                  if let Some(value) = self.params.get(a) {
-                    if let MalVal::ZKScalar(val) = value {
-                      left = left + (*val, val_b);
-                    }
-                  }
+                    if let Some(value) = params_const.get(a) {
+                        if let MalVal::ZKScalar(val) = value {
+                            left = left + (*val, val_b);
+                        }
+                    } 
                 }
             }
 
@@ -105,7 +117,7 @@ impl Circuit<bls12_381::Scalar> for LispCircuit {
                     right = right + (coeff, val_b);
                 } else if a == "scalar::one::neg" {
                     right = right + (coeff.neg(), val_b);
-                } 
+                }
             }
 
             for values in alloc_value.output.iter() {
@@ -118,7 +130,7 @@ impl Circuit<bls12_381::Scalar> for LispCircuit {
                     output = output + (coeff, val_b);
                 } else if a == "scalar::one::neg" {
                     output = output + (coeff.neg(), val_b);
-                } 
+                }
             }
 
             cs.enforce(
@@ -127,6 +139,7 @@ impl Circuit<bls12_381::Scalar> for LispCircuit {
                 |_| right.clone(),
                 |_| output.clone(),
             );
+            
         }
 
         Ok(())