|
@@ -119,19 +119,11 @@
|
|
|
))
|
|
))
|
|
|
))
|
|
))
|
|
|
|
|
|
|
|
-;; TODO implement alloc_conditionally
|
|
|
|
|
-;; cs.enforce(
|
|
|
|
|
-;; || "boolean constraint",
|
|
|
|
|
-;; |lc| lc + CS::one() - var,
|
|
|
|
|
-;; |lc| lc + var,
|
|
|
|
|
-;; |lc| lc,
|
|
|
|
|
-;; );
|
|
|
|
|
-
|
|
|
|
|
(defmacro! conditionally_select (fn* [u v condition] (
|
|
(defmacro! conditionally_select (fn* [u v condition] (
|
|
|
(let* [u-prime (gensym)
|
|
(let* [u-prime (gensym)
|
|
|
v-prime (gensym)] (
|
|
v-prime (gensym)] (
|
|
|
- `(def! ~u-prime (alloc ~u-prime (* ~u ~condition)))
|
|
|
|
|
- `(def! ~v-prime (alloc ~v-prime (* ~v ~condition)))
|
|
|
|
|
|
|
+ `(def! ~u-prime (alloc-input ~u-prime (* ~u ~condition)))
|
|
|
|
|
+ `(def! ~v-prime (alloc-input ~v-prime (* ~v ~condition)))
|
|
|
`(enforce
|
|
`(enforce
|
|
|
(scalar::one ~u)
|
|
(scalar::one ~u)
|
|
|
(scalar::one ~condition)
|
|
(scalar::one ~condition)
|
|
@@ -142,26 +134,102 @@
|
|
|
(scalar::one ~condition)
|
|
(scalar::one ~condition)
|
|
|
(scalar::one ~v-prime)
|
|
(scalar::one ~v-prime)
|
|
|
)
|
|
)
|
|
|
|
|
+ { "u-prime" u-prime, "v-prime" v-prime }
|
|
|
|
|
+ )
|
|
|
|
|
+))))
|
|
|
|
|
+
|
|
|
|
|
+(defmacro! jj-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
|
|
|
|
|
+)
|
|
|
|
|
+))
|
|
|
|
|
+
|
|
|
|
|
+;; cs.enforce(
|
|
|
|
|
+;; || "boolean constraint",
|
|
|
|
|
+;; |lc| lc + CS::one() - var,
|
|
|
|
|
+;; |lc| lc + var,
|
|
|
|
|
+;; |lc| lc,
|
|
|
|
|
+;; );
|
|
|
|
|
+(defmacro! zk-boolean (fn* [val] (
|
|
|
|
|
+ (let* [var (gensym)] (
|
|
|
|
|
+ `(alloc ~var ~val)
|
|
|
|
|
+ `(enforce
|
|
|
|
|
+ (scalar::one cs::one) (scalar::one ~var)
|
|
|
|
|
+ (scalar::one ~var)
|
|
|
|
|
+ ()
|
|
|
|
|
+ )
|
|
|
)
|
|
)
|
|
|
))))
|
|
))))
|
|
|
|
|
|
|
|
-(def! param1 (scalar 3))
|
|
|
|
|
-(def! param2 (scalar 9))
|
|
|
|
|
|
|
+;; b == (scalar "0000000000000000000000000000000000000000000000000000000000000000")
|
|
|
|
|
+;; u,v == jubjub ecc point
|
|
|
|
|
+(def! jj-mul (fn* [u v b] (
|
|
|
|
|
+ (def! result (unpack-bits b))
|
|
|
|
|
+ (eval (map zk-boolean result))
|
|
|
|
|
+ ;; 2nd step
|
|
|
|
|
+ ;; (map result [n](
|
|
|
|
|
+ ;; 1st just clone
|
|
|
|
|
+ ;; 2nd zk-double
|
|
|
|
|
+ ;; 3rd conditionally_select
|
|
|
|
|
+ ;; 4rd jj-add
|
|
|
|
|
+ ;; ))
|
|
|
|
|
+)))
|
|
|
|
|
+
|
|
|
(def! param3 (scalar "0000000000000000000000000000000000000000000000000000000000000000"))
|
|
(def! param3 (scalar "0000000000000000000000000000000000000000000000000000000000000000"))
|
|
|
(def! param-u (scalar "273f910d9ecc1615d8618ed1d15fef4e9472c89ac043042d36183b2cb4d7ef51"))
|
|
(def! param-u (scalar "273f910d9ecc1615d8618ed1d15fef4e9472c89ac043042d36183b2cb4d7ef51"))
|
|
|
(def! param-v (scalar "466a7e3a82f67ab1d32294fd89774ad6bc3332d0fa1ccd18a77a81f50667c8d7"))
|
|
(def! param-v (scalar "466a7e3a82f67ab1d32294fd89774ad6bc3332d0fa1ccd18a77a81f50667c8d7"))
|
|
|
(prove
|
|
(prove
|
|
|
(
|
|
(
|
|
|
- ;; (println (zk-square param1))
|
|
|
|
|
|
|
+ (jj-mul param-u param-v param3)
|
|
|
;; (println (zk-mul param1 param2))
|
|
;; (println (zk-mul param1 param2))
|
|
|
- ;; (println 'witness (zk-witness param-u param-v))
|
|
|
|
|
- ;; (println 'double (last (last (zk-double param-u param-v))))
|
|
|
|
|
- ;; (println 'nonzero (zk-nonzero? param3))
|
|
|
|
|
- ;; (println 'not-small-order? (zk-not-small-order? param-u param-v))
|
|
|
|
|
- (def! alloc-u (alloc "alloc-u" param-u))
|
|
|
|
|
- (def! alloc-v (alloc "alloc-v" param-v))
|
|
|
|
|
- (def! condition (alloc "condition" param3))
|
|
|
|
|
- (println 'conditionally_select
|
|
|
|
|
- (conditionally_select alloc-u alloc-v condition))
|
|
|
|
|
)
|
|
)
|
|
|
-)
|
|
|
|
|
|
|
+)
|
|
|
|
|
+
|
|
|
|
|
+;; following some examples
|
|
|
|
|
+;; (def! alloc-u (alloc "alloc-u" param-u))
|
|
|
|
|
+;; (def! alloc-v (alloc "alloc-v" param-v))
|
|
|
|
|
+;; (def! condition (alloc "condition" param3))
|
|
|
|
|
+;; (println 'conditionally_select
|
|
|
|
|
+;; (conditionally_select alloc-u alloc-v condition))
|
|
|
|
|
+;; (def! param1 (scalar 3))
|
|
|
|
|
+;; (def! param2 (scalar 9))
|
|
|
|
|
+;; (println (zk-square param1))
|
|
|
|
|
+;; (println (zk-mul param1 param2))
|
|
|
|
|
+;; (println 'witness (zk-witness param-u param-v))
|
|
|
|
|
+;; (println 'double (last (last (zk-double param-u param-v))))
|
|
|
|
|
+;; (println 'nonzero (zk-nonzero? param3))
|
|
|
|
|
+;; (println 'not-small-order? (zk-not-small-order? param-u param-v))
|