organizing return of zk defmacro

lisp/bits.lisp

@@ -1,9 +0,0 @@
-(def! bit-dec 
-      (fn* [x] (
-        (def! bits (unpack-bits x 256))                        
-        (def! enforce-step-1 (fn* [b] (enforce (add-one-lc0 (sub-lc0 b) (add-lc1 b))))
-        (map enforce-step-1 bits)
-        (map (fn* [b] ((add-lc0 b) double-coeff-lc) bits)                       
-        (enforce reset-coeff-lc sub-lc0 add-one-lc1)
-      )))))
-                            

lisp/inverse.lisp

@@ -1,34 +0,0 @@
-(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 27))
-      ]
-(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)))

lisp/jubjub-add-macro.lisp

@@ -1,60 +0,0 @@
-(println "jubjub-add-macro.lisp")
-
-;; export to external lib
-(def! inc (fn* [a] (i+ a 1)))
-(def! gensym
-  (let* [counter (atom 0)]
-    (fn* []
-      (symbol (str "G__" (swap! counter inc))))))
-
-
-(defmacro! jubjub-add (fn* [param1 param2 param3 param4]
-    (let* [u1 (gensym) v1 (gensym) u2 (gensym) v2 (gensym)
-           EDWARDS_D (gensym) U (gensym) A (gensym) B (gensym)
-           C (gensym) u3 (gensym) v3 (gensym)] (
-        `(def! ~u1 (alloc ~u1 param1))
-        `(def! ~v1 (alloc ~v1 param2))
-        `(def! ~u2 (alloc ~u2 param3))
-        `(def! ~v2 (alloc ~v2 param4)) 
-        `(def! ~EDWARDS_D (alloc-const ~EDWARDS_D (scalar "2a9318e74bfa2b48f5fd9207e6bd7fd4292d7f6d37579d2601065fd6d6343eb1")))
-        `(def! ~U (alloc ~U (* (+ ~u1 ~v1) (+ ~u2 ~v2))))
-        `(def! ~A (alloc ~A (* ~v2 ~u1)))
-        `(def! ~B (alloc ~B (* ~u2 ~v1)))
-        `(def! ~C (alloc ~C (* ~EDWARDS_D (* ~A ~B))))
-        `(def! ~u3 (alloc-input ~u3 (/ (+ ~A ~B) (+ scalar::one ~C))))
-        `(def! ~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))
-   )
-  )
-  ;; improve return values
-)
-))
-
-(def! param4 (scalar "015d8c7f5b43fe33f7891142c001d9251f3abeeb98fad3e87b0dc53c4ebf1891"))
-(def! param3 (scalar "15a36d1f0f390d8852a35a8c1908dd87a361ee3fd48fdf77b9819dc82d90607e"))
-(def! param2 (scalar "015d8c7f5b43fe33f7891142c001d9251f3abeeb98fad3e87b0dc53c4ebf1891"))
-(def! param1 (scalar "15a36d1f0f390d8852a35a8c1908dd87a361ee3fd48fdf77b9819dc82d90607e"))
-
-(prove (
-    (def! result1 (jubjub-add param1 param2 param3 param4))
-    (println 'jubjub-result result1)
-    ;;(jubjub-add param3 param4 param1 param2)
-))

lisp/jubjub-add.lisp

@@ -1,47 +0,0 @@
-(println "jubjub-add.lisp")
-(def! param4 (scalar "015d8c7f5b43fe33f7891142c001d9251f3abeeb98fad3e87b0dc53c4ebf1891"))
-(def! param3 (scalar "15a36d1f0f390d8852a35a8c1908dd87a361ee3fd48fdf77b9819dc82d90607e"))
-(def! param2 (scalar "015d8c7f5b43fe33f7891142c001d9251f3abeeb98fad3e87b0dc53c4ebf1891"))
-(def! param1 (scalar "15a36d1f0f390d8852a35a8c1908dd87a361ee3fd48fdf77b9819dc82d90607e"))
-
-(
-    (let* [
-      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)))
-      ]
-    (prove
-        (setup 
-  (
-  (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))
-  )
-  )
- )
-)))
-;; (println 'verify  (MyCircuit (scalar 27)))

lisp/jubjub-mul.lisp

@@ -1,61 +0,0 @@
-(println "jubjub-mul.lisp")
-
-(def! param4 (scalar "015d8c7f5b43fe33f7891142c001d9251f3abeeb98fad3e87b0dc53c4ebf1891"))
-(def! param3 (scalar "15a36d1f0f390d8852a35a8c1908dd87a361ee3fd48fdf77b9819dc82d90607e"))
-(def! param2 (scalar "015d8c7f5b43fe33f7891142c001d9251f3abeeb98fad3e87b0dc53c4ebf1891"))
-(def! param1 (scalar "15a36d1f0f390d8852a35a8c1908dd87a361ee3fd48fdf77b9819dc82d90607e"))
-
-;; (setup
-    (prove (      
-    (def! zk-square (fn* [var] (
-            (def! value (alloc "value" var))
-            (def! result (alloc "result" (square var)))
-            (enforce  
-                (scalar::one value) 
-                (scalar::one value)
-                (scalar::one result)
-            )
-        )
-    ))
-
-    (def! u1 (alloc "u1" param1))
-    (def! v1 (alloc "v1" param2))
-    (def! u2 (alloc "u2" param3))
-    (def! v2 (alloc "v2" param4))
-    (def! U (alloc "U" (* (+ u1 v1) (+ u2 v2))))
-    (def! A (alloc "A" (* v2 u1)))
-    (def! B (alloc "B" (* u2 v1)))
-    (def! EDWARDS_D (alloc-const "EDWARDS_D" (scalar "2a9318e74bfa2b48f5fd9207e6bd7fd4292d7f6d37579d2601065fd6d6343eb1")))
-    (def! C (alloc "C" (* EDWARDS_D (* A B))))
-    (def! u3 (alloc-input "u3" (/ (+ A B) (+ scalar::one C))))
-    (def! v3 (alloc-input "v3" (/ (- (- U A) B) (- scalar::one C))))
-    (zk-square param1)
-    ;; first solution to make this not override the last zk-square 
-    ;; is to use similar approach that we used on the pism
-    ;; add a custom arg to append on the variable name and so forth
-    ;; the other option is to infer the call eval number and add 
-    ;; something inside lisp
-    (zk-square param2)
-  (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

@@ -704,7 +704,6 @@ fn repl_load(file: String) -> Result<(), ()> {
         "(def! load-file (fn* (f) (eval (read-string (str \"(do \" (slurp f) \"\nnil)\")))))",
         &repl_env,
     );
-    //let _ = rep("(defmacro! cond (fn* (& xs) (if (> (count xs) 0) (list 'if (first xs) (if (> (count xs) 1) (nth xs 1) (throw \"odd number of forms to cond\")) (cons 'cond (rest (rest xs)))))))", &repl_env);
     match rep(&format!("(load-file \"{}\")", file), &repl_env) {
         Ok(_) => std::process::exit(0),
         Err(e) => {

lisp/macros.lisp

@@ -1,30 +0,0 @@
-;; testing macros
-
-(def! inc (fn* [a] (i+ a 1)))
-(def! gensym
-  (let* [counter (atom 0)]
-    (fn* []
-      (symbol (str "G__" (swap! counter inc))))))
-
-(defmacro! zk-square (fn* [var] (
-        (let* [v1 (gensym)
-               v2 (gensym)] (
-          (println 'values var)
-        `(alloc ~v1 ~var)
-        `(alloc ~v2 (square ~var))
-        `(enforce  
-            (scalar::one ~v1) 
-            (scalar::one ~v1) 
-            (scalar::one ~v2) 
-        )
-        )
-    ))
-))
-(def! param1 (scalar 1))
-(def! param2 (scalar 3))
-(prove 
-  (
-    (zk-square param1)  
-    (zk-square param2)
-  )
-)

lisp/new-cs.lisp

@@ -1,34 +0,0 @@
-(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 27))
-      ]
-(prove
- (setup 
-  (
-  (enforce  
-    (scalar::one x)
-    (scalar::one x)
-    (scalar::one x2)
-  )
-
-  (enforce 
-    (scalar::one x2)
-    (scalar::one x)
-    (scalar::one x3)
-  )
-
-  (enforce 
-    (scalar::one input)
-    (scalar::one cs::one)
-    (scalar::one x3)  
-  )
-  )
-  )
- )
-)
-)
-;; (println 'verify  (MyCircuit (scalar 27)))

lisp/new.lisp

@@ -1,17 +0,0 @@
-(def! x "73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000000")
-(def! one "0000000000000000000000000000000000000000000000000000000000000001")
-(def! bits (unpack-bits x))
-(defzk! circuit ())
-(def! cvalues (map (fn* [b] (eval
-                    (add lc0 one) 
-                    (sub lc0 b)
-                    (add lc1 x)
-                    enforce)
-                        ) bits))
-(def! cs (concat cvalues (list 
-                 'reset-coeff-lc
-                 (sub lc0 x)
-                 (add lc1 one)
-                 'enforce)))
-(println "bit-dec")
-(cs! circuit cs)