two circuits merged and executing the proof

lisp/jubjub-mul.lisp

@@ -0,0 +1,60 @@
+(println "jubjub-mul.lisp")
+(def! param4 (scalar "015d8c7f5b43fe33f7891142c001d9251f3abeeb98fad3e87b0dc53c4ebf1891"))
+(def! param3 (scalar "15a36d1f0f390d8852a35a8c1908dd87a361ee3fd48fdf77b9819dc82d90607e"))
+(def! param2 (scalar "015d8c7f5b43fe33f7891142c001d9251f3abeeb98fad3e87b0dc53c4ebf1891"))
+(def! param1 (scalar "15a36d1f0f390d8852a35a8c1908dd87a361ee3fd48fdf77b9819dc82d90607e"))
+
+(setup
+    (prove 
+(
+    (zk* [
+      u11 (alloc "u11" (scalar 2))
+      v11 (alloc "v11" (scalar 2))
+      U1 (alloc-input "U1" (* u11 v11))
+      ]
+  (
+    (enforce  
+      (scalar::one u11) 
+      (scalar::one v11)
+      (scalar::one U1)
+    )
+  )
+  )
+    (zk* [
+      u1 (alloc "u1" param1)
+      v1 (alloc "v1" param2)
+      u2 (alloc "u2" param3)
+      v2 (alloc "v2" param4)
+      EDWARDS_D (alloc-const "EDWARDS_D" (scalar "2a9318e74bfa2b48f5fd9207e6bd7fd4292d7f6d37579d2601065fd6d6343eb1"))
+      U (alloc "U" (* (+ u1 v1) (+ u2 v2)))
+      A (alloc "A" (* v2 u1))
+      B (alloc "B" (* u2 v1))
+      C (alloc "C" (* EDWARDS_D (* A B)))
+      u3 (alloc-input "u3" (/ (+ A B) (+ scalar::one C)))
+      v3 (alloc-input "v3" (/ (- (- U A) B) (- scalar::one C)))
+      ]
+  (
+  (enforce  
+    ((scalar::one u1) (scalar::one v1))
+    ((scalar::one u2) (scalar::one v2))
+    (scalar::one U)
+  )
+  (enforce
+    (EDWARDS_D A)
+    (scalar::one B)
+    (scalar::one C)
+  )
+  (enforce
+    ((scalar::one cs::one)(scalar::one C))
+    (scalar::one u3)
+    ((scalar::one A) (scalar::one B))
+  )
+  (enforce
+    ((scalar::one cs::one) (scalar::one::neg C))
+    (scalar::one v3)
+    ((scalar::one U) (scalar::one::neg A) (scalar::one::neg B))
+  )
+  )
+ )
+)
+))

lisp/lisp.rs

@@ -167,10 +167,34 @@ fn eval(mut ast: MalVal, mut env: Env) -> MalRet {
                     Sym(ref a0sym) if a0sym == "def!" => {
                         env_set(&env, l[1].clone(), eval(l[2].clone(), env.clone())?)
                     }
+                    Sym(ref a0sym) if a0sym == "zk*" => {
+                        let (a1, a2) = (l[1].clone(), l[2].clone());
+                        match a1 {
+                            List(ref binds, _) | Vector(ref binds, _) => {
+                                for (b, e) in binds.iter().tuples() {
+                                    match b {
+                                        Sym(_) => {
+                                            let _ = env_set(
+                                                &env,
+                                                b.clone(),
+                                                eval(e.clone(), env.clone())?,
+                                            );
+                                        }
+                                        _ => {
+                                            return error("let* with non-Sym binding");
+                                        }
+                                    }
+                                }
+                            }
+                            _ => {
+                                return error("let* with non-List bindings");
+                            }
+                        };
+                        ast = a2;
+                        continue 'tco;
+                    }
                     Sym(ref a0sym) if a0sym == "let*" => {
-                        // TODO let should be restored to the first purpose
-                        // and the new let* without an env creation should be availaable
-                        //                        env = env_new(Some(env.clone()));
+                        env = env_new(Some(env.clone()));
                         let (a1, a2) = (l[1].clone(), l[2].clone());
                         match a1 {
                             List(ref binds, _) | Vector(ref binds, _) => {