mint2.lisp 13 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371
  1. (load-file "util.lisp")
  2. (def! zk-not-small-order? (fn* [u v] (
  3. (def! first-doubling (last (last (zk-double u v))))
  4. (def! second-doubling (last (last
  5. (zk-double (get first-doubling "u3") (get first-doubling "v3")))))
  6. (def! third-doubling (last (last
  7. (zk-double (get second-doubling "u3") (get second-doubling "v3")))))
  8. (zk-nonzero? (get third-doubling "u3"))
  9. )
  10. )
  11. )
  12. (defmacro! zk-nonzero? (fn* [var] (
  13. (let* [inv (gensym)
  14. v1 (gensym)] (
  15. `(alloc ~inv (invert ~var))
  16. `(alloc ~v1 ~var)
  17. `(enforce
  18. (scalar::one ~v1)
  19. (scalar::one ~inv)
  20. (scalar::one cs::one)
  21. )
  22. )
  23. ))
  24. ))
  25. (defmacro! zk-square (fn* [var] (
  26. (let* [v1 (gensym)
  27. v2 (gensym)] (
  28. `(alloc ~v1 ~var)
  29. `(def! output (alloc-input ~v2 (square ~var)))
  30. `(enforce
  31. (scalar::one ~v1)
  32. (scalar::one ~v1)
  33. (scalar::one ~v2)
  34. )
  35. `{ "v2" output }
  36. )
  37. ))
  38. ))
  39. (defmacro! zk-mul (fn* [val1 val2] (
  40. (let* [v1 (gensym)
  41. v2 (gensym)
  42. var (gensym)] (
  43. `(alloc ~v1 ~val1)
  44. `(alloc ~v2 ~val2)
  45. `(def! result (alloc-input ~var (* ~val1 ~val2)))
  46. `(enforce
  47. (scalar::one ~v1)
  48. (scalar::one ~v2)
  49. (scalar::one ~var)
  50. )
  51. `{ "result" result }
  52. )
  53. ))
  54. ))
  55. (defmacro! zk-witness (fn* [val1 val2] (
  56. (let* [u2 (gensym)
  57. v2 (gensym)
  58. u2v2 (gensym)
  59. EDWARDS_D (gensym)] (
  60. `(def! ~EDWARDS_D (alloc-const ~EDWARDS_D (scalar "2a9318e74bfa2b48f5fd9207e6bd7fd4292d7f6d37579d2601065fd6d6343eb1")))
  61. `(def! ~u2 (alloc ~u2 (get (nth (nth (zk-square ~val1) 0) 3) "v2")))
  62. `(def! ~v2 (alloc ~v2 (get (nth (nth (zk-square ~val2) 0) 3) "v2")))
  63. `(def! result (alloc-input ~u2v2 (get (last (last (zk-mul ~u2 ~v2))) "result")))
  64. `(enforce
  65. ((scalar::one::neg ~u2) (scalar::one ~v2))
  66. (scalar::one cs::one)
  67. ((scalar::one cs::one) (~EDWARDS_D ~u2v2))
  68. )
  69. `{ "result" result }
  70. )
  71. ))
  72. ))
  73. (defmacro! zk-double (fn* [val1 val2] (
  74. (let* [u (gensym)
  75. v (gensym)
  76. u3 (gensym)
  77. v3 (gensym)
  78. T (gensym)
  79. A (gensym)
  80. C (gensym)
  81. EDWARDS_D (gensym)] (
  82. `(def! ~EDWARDS_D (alloc-const ~EDWARDS_D (scalar "2a9318e74bfa2b48f5fd9207e6bd7fd4292d7f6d37579d2601065fd6d6343eb1")))
  83. `(def! ~u (alloc ~u ~val1))
  84. `(def! ~v (alloc ~v ~val2))
  85. `(def! ~T (alloc ~T (* (+ ~val1 ~val2) (+ ~val1 ~val2))))
  86. `(def! ~A (alloc ~A (* ~u ~v)))
  87. `(def! ~C (alloc ~C (* (square ~A) ~EDWARDS_D)))
  88. `(def! ~u3 (alloc ~u3 (/ (double ~A) (+ scalar::one ~C))))
  89. `(def! ~v3 (alloc ~v3 (/ (- ~T (double ~A)) (- scalar::one ~C))))
  90. `(enforce
  91. ((scalar::one ~u) (scalar::one ~v))
  92. ((scalar::one ~u) (scalar::one ~v))
  93. (scalar::one ~T)
  94. )
  95. `(enforce
  96. (~EDWARDS_D ~A)
  97. (scalar::one ~A)
  98. (scalar::one ~C)
  99. )
  100. `(enforce
  101. ((scalar::one cs::one) (scalar::one ~C))
  102. (scalar::one ~u3)
  103. ((scalar::one ~A) (scalar::one ~A))
  104. )
  105. `(enforce
  106. ((scalar::one cs::one) (scalar::one::neg ~C))
  107. (scalar::one ~v3)
  108. ((scalar::one ~T) (scalar::one::neg ~A) (scalar::one::neg ~A))
  109. )
  110. { "u3" u3, "v3" v3 }
  111. )
  112. ))
  113. ))
  114. (defmacro! conditionally-select (fn* [val1 val2 val3] (
  115. (let* [u-prime (gensym)
  116. v-prime (gensym)
  117. u (gensym)
  118. v (gensym)
  119. condition (gensym)
  120. ] (
  121. `(def! ~u (alloc ~u ~val1))
  122. `(def! ~v (alloc ~v ~val2))
  123. `(def! ~condition (alloc ~condition ~val3))
  124. `(def! ~u-prime (alloc ~u-prime (* ~u ~condition)))
  125. `(def! ~v-prime (alloc ~v-prime (* ~v ~condition)))
  126. `(enforce
  127. (scalar::one ~u)
  128. (scalar::one ~condition)
  129. (scalar::one ~u-prime)
  130. )
  131. `(enforce
  132. (scalar::one ~v)
  133. (scalar::one ~condition)
  134. (scalar::one ~v-prime)
  135. )
  136. { "u-prime" u-prime, "v-prime" v-prime }
  137. )
  138. ))))
  139. (defmacro! jj-add (fn* [param1 param2 param3 param4]
  140. (let* [u1 (gensym) v1 (gensym) u2 (gensym) v2 (gensym)
  141. EDWARDS_D (gensym) U (gensym) A (gensym) B (gensym)
  142. C (gensym) u3 (gensym) v3 (gensym)] (
  143. ;; debug
  144. ;; `(println 'jj-add ~param1 ~param2 ~param3 ~param4)
  145. `(def! ~u1 (alloc ~u1 ~param1))
  146. `(def! ~v1 (alloc ~v1 ~param2))
  147. `(def! ~u2 (alloc ~u2 ~param3))
  148. `(def! ~v2 (alloc ~v2 ~param4))
  149. `(def! ~EDWARDS_D (alloc-const ~EDWARDS_D (scalar "2a9318e74bfa2b48f5fd9207e6bd7fd4292d7f6d37579d2601065fd6d6343eb1")))
  150. `(def! ~U (alloc ~U (* (+ ~u1 ~v1) (+ ~u2 ~v2))))
  151. `(def! ~A (alloc ~A (* ~v2 ~u1)))
  152. `(def! ~B (alloc ~B (* ~u2 ~v1)))
  153. `(def! ~C (alloc ~C (* ~EDWARDS_D (* ~A ~B))))
  154. `(def! ~u3 (alloc ~u3 (/ (+ ~A ~B) (+ scalar::one ~C))))
  155. `(def! ~v3 (alloc ~v3 (/ (- (- ~U ~A) ~B) (- scalar::one ~C))))
  156. `(enforce
  157. ((scalar::one ~u1) (scalar::one ~v1))
  158. ((scalar::one ~u2) (scalar::one ~v2))
  159. (scalar::one ~U)
  160. )
  161. `(enforce
  162. (~EDWARDS_D ~A)
  163. (scalar::one ~B)
  164. (scalar::one ~C)
  165. )
  166. `(enforce
  167. ((scalar::one cs::one)(scalar::one ~C))
  168. (scalar::one ~u3)
  169. ((scalar::one ~A) (scalar::one ~B))
  170. )
  171. `(enforce
  172. ((scalar::one cs::one) (scalar::one::neg ~C))
  173. (scalar::one ~v3)
  174. ((scalar::one ~U) (scalar::one::neg ~A) (scalar::one::neg ~B))
  175. )
  176. `{ "u3" u3, "v3" v3 }
  177. )
  178. )
  179. ))
  180. (defmacro! zk-boolean (fn* [val] (
  181. (let* [var (gensym)] (
  182. `(alloc ~var ~val)
  183. `(enforce
  184. ((scalar::one cs::one) (scalar::one::neg ~var))
  185. (scalar::one ~var)
  186. ()
  187. )
  188. )
  189. ))))
  190. (def! jj-mul (fn* [u v b] (
  191. (def! result (unpack-bits b))
  192. (eval (map zk-boolean result))
  193. (def! val (last (last (zk-double u v))))
  194. (def! acc 0)
  195. (dotimes (count result) (
  196. (def! u3 (get val "u3"))
  197. (def! v3 (get val "v3"))
  198. (def! r (nth result acc))
  199. (def! cond-result (last (last (conditionally-select u3 v3 r))))
  200. (def! u-prime (get cond-result "u-prime"))
  201. (def! v-prime (get cond-result "v-prime"))
  202. (def! add-result (last (jj-add u3 v3 u-prime v-prime)))
  203. (def! u-add (get add-result "u3"))
  204. (def! v-add (get add-result "v3"))
  205. (def! val (last (last (zk-double u-add v-add))))
  206. (def! acc (i+ acc 1))
  207. ))
  208. (val)
  209. ;; { "u3" (get val "u3"), "v3" (get val "v3") }
  210. )))
  211. (load-file "mimc-constants.lisp")
  212. (defmacro! mimc-macro (fn* [left-value right-value acc] (
  213. (let* [tmp-xl (gensym2 'tmp_xl)
  214. xl-new-value (gensym2 'xl_new_value)
  215. cur-mimc-const (gensym2 'cur_mimc_const)
  216. xl (gensym2 'xl)
  217. xr (gensym2 'xr)] (
  218. `(def! ~xl (alloc ~xl ~left-value))
  219. `(def! ~xr (alloc ~xr ~right-value))
  220. `(def! ~cur-mimc-const (alloc-const ~cur-mimc-const (nth mimc-constants ~acc)))
  221. `(def! ~tmp-xl (alloc ~tmp-xl (square (+ ~cur-mimc-const ~xl))))
  222. `(enforce
  223. ((scalar::one ~xl) (~cur-mimc-const cs::one))
  224. ((scalar::one ~xl) (~cur-mimc-const cs::one))
  225. (scalar::one ~tmp-xl)
  226. )
  227. `(def! new-value (+ (* ~tmp-xl (+ ~cur-mimc-const ~xl)) ~xr))
  228. `(if (= ~acc 321)
  229. (def! ~xl-new-value (alloc-input ~xl-new-value new-value))
  230. (def! ~xl-new-value (alloc ~xl-new-value new-value))
  231. )
  232. `(enforce
  233. (scalar::one ~tmp-xl)
  234. ((scalar::one ~xl) (~cur-mimc-const cs::one))
  235. ((scalar::one ~xl-new-value) (scalar::one::neg ~xr))
  236. )
  237. `{ "left" new-value }
  238. )
  239. ))))
  240. (def! mimc (fn* [left right] (
  241. (def! acc 0)
  242. (def! xl left)
  243. (def! xr right)
  244. (dotimes 322 (
  245. (def! result (mimc-macro xl xr acc))
  246. (def! result-value (get (last (last result)) "left"))
  247. (println acc)
  248. (println xl xr)
  249. (println result-value)
  250. (def! xr xl)
  251. (def! xl result-value)
  252. (def! acc (i+ acc 1))
  253. ))
  254. )))
  255. (defmacro! rangeproof-alloc (fn* [value value-digit] (
  256. (let* [bit (gensym2 'bit)
  257. digit (gensym2 'digit)] (
  258. `(def! ~bit (alloc ~bit ~value))
  259. `(def! ~digit (alloc-const ~digit ~value-digit))
  260. `(enforce
  261. (scalar::one ~bit)
  262. ((scalar::one cs::one) (scalar::one::neg ~bit))
  263. ()
  264. )
  265. { "lc" ((str digit) (str bit)) }
  266. )))))
  267. (def! rangeproof (fn* [value] (
  268. (def! values-bit (unpack-bits value))
  269. (def! idx 0)
  270. (def! digit (scalar 1))
  271. (def! value-result ())
  272. (dotimes 64 (
  273. (def! bit (nth values-bit idx))
  274. (def! value-result
  275. (conj value-result
  276. (get (last (last
  277. (rangeproof-alloc bit digit))) "lc")))
  278. (println 'digit digit 'bit bit)
  279. (def! digit (double digit))
  280. (def! idx (i+ idx 1))
  281. ))
  282. (println 'value-result value-result)
  283. (def! value-alloc (alloc-input "value-alloc" value))
  284. (enforce
  285. (value-result)
  286. (scalar::one cs::one)
  287. (scalar::one value-alloc)
  288. )
  289. )))
  290. ;; (def! generator-coin )
  291. ;; (def! generator-value-commit )
  292. ;; (def! generator-value-random )
  293. ;; (def! mint-contract (fn* [secret-u secret-v value serial rnd-coin rnd-value] (
  294. ;; (def! result-mul (last (last (jj-mul bit secret-u secret-v generator-coin))) "lc")
  295. ;; (def! public-u (alloc "public-u" (get result-mul "u")))
  296. ;; (def! public-v (alloc "public-v" (get result-mul "v")))
  297. ;; ;; check return ?
  298. ;; (rangeproof value)
  299. ;; (def! add-result (last (jj-add
  300. ;; (jj-mul-1-u) (jj-mul-1-v) (jj-mul-2-u) (jj-mul-2-v) )))
  301. ;; (def! value-commit add-result)
  302. ;; (alloc "value-commit" value-commit)
  303. ;; )))
  304. (prove
  305. (
  306. (def! param-u (scalar "6800f4fa0f001cfc7ff6826ad58004b4d1d8da41af03744e3bce3b7793664337"))
  307. (def! param-v (scalar "6d81d3a9cb45dedbe6fb2a6e1e22ab50ad46f1b0473b803b3caefab9380b6a8b"))
  308. ;; (def! param-a (scalar 110))
  309. ;; (rangeproof param-a)
  310. ;; (def! param3 (rnd-scalar))
  311. ;; (jj-mul param-u param-v param3)
  312. )
  313. )
  314. ;; (defmacro! test (fn* [value value-digit] (
  315. ;; (let* [bit (gensym2 'bit)
  316. ;; digit (gensym2 'digit)] (
  317. ;; `(def! ~bit (alloc ~bit ~value))
  318. ;; `(def! ~digit (alloc ~digit ~value-digit))
  319. ;; (println (str digit))
  320. ;; )))))
  321. ;; (def! param-u (scalar "6800f4fa0f001cfc7ff6826ad58004b4d1d8da41af03744e3bce3b7793664337"))
  322. ;; (def! param-v (scalar "6d81d3a9cb45dedbe6fb2a6e1e22ab50ad46f1b0473b803b3caefab9380b6a8b"))
  323. ;; (println (test param-u param-v))
  324. ;; (mint-contract param-u param-v)
  325. ;; (def! param3 (rnd-scalar))
  326. ;; (def! param-u (scalar "6800f4fa0f001cfc7ff6826ad58004b4d1d8da41af03744e3bce3b7793664337"))
  327. ;; (def! param-v (scalar "6d81d3a9cb45dedbe6fb2a6e1e22ab50ad46f1b0473b803b3caefab9380b6a8b"))
  328. ;; (jj-mul param-u param-v param3)
  329. ;; following some examples
  330. ;; (def! left (scalar "15a36d1f0f390d8852a35a8c1908dd87a361ee3fd48fdf77b9819dc82d90607e"))
  331. ;; (def! right (scalar "015d8c7f5b43fe33f7891142c001d9251f3abeeb98fad3e87b0dc53c4ebf1891"))
  332. ;; (mimc left right)
  333. ;; (def! param3 (rnd-scalar))
  334. ;; (jj-mul param-u param-v param3)
  335. ;; (def! param3 (rnd-scalar))
  336. ;; (def! param-u (scalar "6800f4fa0f001cfc7ff6826ad58004b4d1d8da41af03744e3bce3b7793664337"))
  337. ;; (def! param-v (scalar "6d81d3a9cb45dedbe6fb2a6e1e22ab50ad46f1b0473b803b3caefab9380b6a8b"))
  338. ;; (jj-mul param-u param-v param3)
  339. ;; (def! param3 (rnd-scalar))
  340. ;; (println 'rnd-scalar param3)
  341. ;; (def! param-u (scalar "6800f4fa0f001cfc7ff6826ad58004b4d1d8da41af03744e3bce3b7793664337"))
  342. ;; (def! param-v (scalar "6d81d3a9cb45dedbe6fb2a6e1e22ab50ad46f1b0473b803b3caefab9380b6a8b"))
  343. ;; (println (zk-mul param1 param2))
  344. ;; (jj-mul param-u param-v param3)
  345. ;; (println (zk-mul param1 param2))
  346. ;; (def! param1 (scalar 3))
  347. ;; (def! param2 (scalar 9))
  348. ;; (println (zk-square param1))
  349. ;; (println (zk-mul param1 param2))
  350. ;; (println 'witness (zk-witness param-u param-v))
  351. ;; (println 'double (last (last (zk-double param-u param-v))))
  352. ;; (println 'nonzero (zk-nonzero? param3))
  353. ;; (println 'not-small-order? (zk-not-small-order? param-u param-v))