scalar division and jubjub.lisp updates

lisp/core.rs

@@ -277,6 +277,17 @@ fn mul_scalar(a: MalArgs) -> MalRet {
         _ => error("expected (scalar, scalar"),
     }
 }
+
+fn div_scalar(a: MalArgs) -> MalRet {
+    match (a[0].clone(), a[1].clone()) {
+        (Str(a0), Str(a1)) => {
+            let (mut s0, mut s1) = (Scalar::from_string(&a0), Scalar::from_string(&a1));
+            let ret = s1.invert().map(|other| *&s0 * other);
+            Ok(Str(std::string::ToString::to_string(&ret.unwrap())[2..].to_string()))
+        }
+        _ => error("expected (scalar, scalar"),
+    }
+}
 fn add_scalar(a: MalArgs) -> MalRet {
     match (a[0].clone(), a[1].clone()) {
         (Str(a0), Str(a1)) => {
@@ -358,7 +369,7 @@ pub fn ns() -> Vec<(&'static str, MalVal)> {
         ("+", func(add_scalar)),
         ("-", func(sub_scalar)),
         ("*", func(mul_scalar)),
-        ("/", func(fn_t_int_int!(Int, |i, j| { i / j }))),
+        ("/", func(div_scalar)),
         ("time-ms", func(time_ms)),
         ("i+", func(fn_t_int_int!(Int, |i, j| { i + j }))),
         ("i-", func(fn_t_int_int!(Int, |i, j| { i - j }))),

lisp/jubjub.lisp

@@ -7,6 +7,11 @@
 (def! one "0000000000000000000000000000000000000000000000000000000000000001")
 (defzk! circuit ())
 (def! U (fn* [x1 y1 x2 y2] (+ (+ x1 y1) (+ x2 y2))))
+(def! A (fn* [x1 y2] (* y2 x1)))
+(def! B (fn* [y1 x2] (* x2 y1)))
+(def! C (fn* [x1 y1 x2 y2] (* d (A x1 y2) (B y1 x2))))
+(def! P.x (fn* [x1 y1 x2 y2] (/ (+ (A x1 y2) (B y1 x2)) (+ one (C x1 y1 x2 y2)))))
+(def! P.y (fn* [x1 y1 x2 y2] (/ (- (U x1 y1 x2 y2) (A x1 y2) (B y1 x2)) (+ one (C x1 y1 x2 y2)))))
 (def! jubjub-add (fn* [x1 y1 x2 y2] (zkcons! circuit (
                     (add lc0 x1)
                     (add lc0 y1)
@@ -14,6 +19,20 @@
                     (add lc1 y2)
                     (add lc2 (U x1 y1 x2 y2))
                     enforce
+;; Compute P.x = (A + B) / (1 + C)
+                    (add lc0 one)
+                    (add lc0 (C x1 y1 x2 y2))
+                    (add lc1 (P.x x1 y1 x2 y2))
+                    (add lc1 (A x1 y2))
+                    (add lc1 (B y1 x2))
+                    enforce
+;; Compute P.y = (U - A - B) / (1 - C)                    
+                    (add lc0 one)
+                    (sub lc0 (C x1 y1 x2 y2))
+                    (add lc1 (P.y x1 y1 x2 y2))
+                    (add lc2 (U x1 y1 x2 y2))
+                    (sub lc2 (A x1 y2))
+                    (sub lc2 (B y1 x2))
+                    enforce 
                     ))))
 (println (jubjub-add a_u a_v b_u b_v))
-(println (U a_u a_v b_u b_v))