six.hoon 9.9 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309
  1. /= ztd-five /common/ztd/five
  2. => ztd-five
  3. ~% %fri ..proof-stream ~
  4. :: fri
  5. |%
  6. +$ fri-input
  7. $: offset=belt
  8. omega=belt
  9. init-domain-len=@
  10. expansion-fac=@
  11. num-spot-checks=@
  12. folding-deg=@
  13. ==
  14. ::
  15. ++ compute-eval-domain
  16. ~/ %compute-eval-domain
  17. |= [domain-len=@ omega=belt offset=@]
  18. ^- (list belt)
  19. ~+
  20. =- (flop acc)
  21. %+ roll (range domain-len)
  22. |= [i=@ acc=(list felt) omega-pow=_1]
  23. :_ (bmul omega-pow omega)
  24. [(bmul offset omega-pow) acc]
  25. ::
  26. ++ fri-door
  27. =, merkle
  28. =, proof-stream
  29. ~/ %fri-door
  30. =| fri-input
  31. |%
  32. ++ log-folding-deg
  33. ~+
  34. ^- @
  35. (dec (xeb folding-deg))
  36. ::
  37. ++ last-codeword-len
  38. ~+
  39. ^- @
  40. (div init-domain-len (pow folding-deg num-rounds))
  41. ::
  42. ++ eval-domain
  43. ~+
  44. ^- (list belt)
  45. (compute-eval-domain init-domain-len omega offset)
  46. ::
  47. ++ num-rounds
  48. ~+
  49. ^- @
  50. =/ len init-domain-len
  51. =/ num 0
  52. |-
  53. ?: &((gth len expansion-fac) (lth (mul 4 num-spot-checks) len))
  54. $(num +(num), len (div len folding-deg))
  55. (max 1 (dec num))
  56. ::
  57. ::
  58. ++ prove
  59. ~/ %prove
  60. |= [codeword=fpoly stream=proof]
  61. ^- [fri-indices=(list @) stream=proof]
  62. |^
  63. :: commit phase
  64. =^ codewords=(list codeword-data) stream
  65. (commit codeword stream)
  66. ::
  67. :: query phase
  68. (query codewords stream)
  69. ::
  70. ::
  71. +$ codeword-data [codeword=mary merk=(unit [depth=@ heap=merk-heap])]
  72. ::
  73. ++ query
  74. |= [codewords=(list codeword-data) stream=proof]
  75. ^- [fri-indices=(list @) stream=proof]
  76. ::
  77. :: Get random indices from the verifier to spot-check the folding
  78. =/ rng ~(prover-fiat-shamir proof-stream stream)
  79. =^ fri-indices=(list @) rng
  80. %- indices:rng
  81. :+ num-spot-checks
  82. init-domain-len
  83. last-codeword-len
  84. ::
  85. =- [fri-indices stream]
  86. %^ zip-roll (range num-rounds) codewords
  87. |= [[round=@ data=codeword-data] indices=_fri-indices stream=_stream]
  88. =/ len len.array:(~(change-step ave codeword.data) 3)
  89. =- [(flop new-indices) stream]
  90. %+ roll indices
  91. |= [idx=@ new-indices=(list @) stream=_stream]
  92. ::
  93. =/ coset-idx (mod idx (div len folding-deg))
  94. =/ merk (need merk.data)
  95. =/ axis (index-to-axis depth.merk coset-idx)
  96. :: Compute merkle opening to idx in codeword and send to the verifier
  97. =/ leaf=fpoly
  98. (~(snag-as-fpoly ave codeword.data) coset-idx)
  99. =/ opening=merk-proof:merkle
  100. (build-merk-proof:merkle heap.merk axis)
  101. :- [coset-idx new-indices]
  102. (~(push proof-stream stream) [%m-path leaf path.opening])
  103. ::
  104. ++ commit
  105. |= [codeword=fpoly stream=proof]
  106. ^- [codewords=(list codeword-data) stream=proof]
  107. =- [(flop codewords) stream]
  108. %+ roll (range +(num-rounds))
  109. |= [round=@ codeword=_codeword codewords=(list codeword-data) omega=_(lift omega) round-offset=_(lift offset) stream=_stream]
  110. ?: =(round num-rounds)
  111. :: If it's the last round, send the raw codeword to the verifier instead
  112. :: of a merkle tree
  113. :* zero-fpoly
  114. codewords
  115. (fpow omega folding-deg)
  116. (fpow round-offset folding-deg)
  117. (~(push proof-stream stream) [%codeword codeword])
  118. ==
  119. ::
  120. =/ num (div len.codeword folding-deg)
  121. ::
  122. :: sort codeword into cosets
  123. =/ cosets=mary
  124. %- zing-fpolys
  125. %+ turn (range num)
  126. |= k=@
  127. %- init-fpoly
  128. %+ turn (range folding-deg)
  129. |= i=@
  130. =/ idx (add (mul i num) k)
  131. (~(snag fop codeword) idx)
  132. ::
  133. :: send codeword (as cosets) to verifier
  134. =/ merk=(pair @ merk-heap:merkle)
  135. (build-merk-heap:merkle cosets)
  136. =. stream
  137. (~(push proof-stream stream) [%m-root h.q.merk])
  138. ::
  139. :: get challenge from verifier
  140. =/ rng ~(prover-fiat-shamir proof-stream stream)
  141. =^ alpha=felt rng $:felt:rng
  142. ::
  143. :: compute new codeword
  144. =/ new-codeword=fpoly
  145. %- init-fpoly
  146. %+ turn (range len.array.cosets)
  147. |= i=@
  148. =/ coset=fpoly (~(snag-as-fpoly ave cosets) i)
  149. =/ eval-point=felt (fdiv alpha (fmul round-offset (fpow omega i)))
  150. ::=/ eval-point=felt (fdiv alpha (fpow omega i))
  151. (fpeval (fp-ifft coset) eval-point)
  152. ::
  153. :* new-codeword
  154. [[cosets (some merk)] codewords]
  155. (fpow omega folding-deg)
  156. (fpow round-offset folding-deg)
  157. stream
  158. ==
  159. --
  160. ::
  161. ++ verify
  162. ~/ %verify
  163. |= [stream=proof root=noun-digest:tip5]
  164. ^- [[top-level-indices=(list @) merks=(list merk-data) deep-cosets=(map @ fpoly) res=?] proof]
  165. ::
  166. :: extract roots and alphas values from commit phase
  167. =^ [roots=(list noun-digest:tip5) alphas=(list felt)] stream
  168. =/ roots=(list noun-digest:tip5) [root]~
  169. =- [[(flop roots) (flop alphas)] str]
  170. %+ roll (range num-rounds)
  171. |= [i=@ str=_stream roots=_roots alphas=(list felt)]
  172. ?: =(i 0)
  173. :+ str roots
  174. ^- (list felt)
  175. :_ alphas
  176. =/ rng ~(verifier-fiat-shamir proof-stream str)
  177. =^ felt rng $:felt:rng
  178. felt
  179. =^ root str
  180. =^(r str ~(pull proof-stream str) ?>(?=(%m-root -.r) p.r^str))
  181. :+ str
  182. [root roots]
  183. ^- (list felt)
  184. :_ alphas
  185. =/ rng ~(verifier-fiat-shamir proof-stream str)
  186. =^ felt rng $:felt:rng
  187. felt
  188. ?> =((lent roots) (lent alphas))
  189. ::
  190. :: extract last codeword
  191. =^ last-codeword=fpoly stream
  192. =^(c stream ~(pull proof-stream stream) ?>(?=(%codeword -.c) p.c^stream))
  193. ::
  194. :: Verify that the last codeword is low degree
  195. ~| "last codeword len is not correct"
  196. ?> =(len.last-codeword last-codeword-len)
  197. =/ poly (fp-ifft last-codeword)
  198. =/ deg (fdegree ~(to-poly fop poly))
  199. =/ degree-bound
  200. %+ div
  201. (div init-domain-len expansion-fac)
  202. (pow folding-deg num-rounds)
  203. ~| "last codeword is not low degree"
  204. ?> (lth deg degree-bound)
  205. ::
  206. :: get indices
  207. =/ [top-level-indices=(list @) *]
  208. =/ rng ~(verifier-fiat-shamir proof-stream stream)
  209. %- indices:rng
  210. :+ num-spot-checks
  211. init-domain-len
  212. last-codeword-len
  213. ::
  214. :: Read cosets out of first codeword
  215. =^ [indices=(list @) deep-cosets=(map @ fpoly) merks=(list merk-data)] stream
  216. =- [[(flop new-indices) cosets merks] stream]
  217. %+ roll top-level-indices
  218. |= [idx=@ [new-indices=(list @) cosets=(map @ fpoly) merks=(list merk-data)] stream=_stream]
  219. =/ coset-idx (mod idx (div init-domain-len folding-deg))
  220. =/ depth (xeb (div init-domain-len folding-deg))
  221. =/ axis (index-to-axis depth coset-idx)
  222. :: read opening for index from proof
  223. =^ opening=proof-path stream
  224. =^(o stream ~(pull proof-stream stream) ?>(?=(%m-path -.o) p.o^stream))
  225. ::
  226. :_ stream
  227. :+ [idx new-indices]
  228. (~(put by cosets) coset-idx leaf.opening)
  229. :- [(hash-hashable:tip5 (hashable-fpoly:tip5 leaf.opening)) axis root path.opening]
  230. merks
  231. ::
  232. ::
  233. =- [[top-level-indices merks deep-cosets %.y] stream]
  234. %+ roll (range num-rounds)
  235. |= $: round=@
  236. roots=_(tail roots)
  237. alphas=_alphas
  238. prev-indices=_indices
  239. prev-cosets=_deep-cosets
  240. prev-len=_init-domain-len
  241. omega=_(lift omega)
  242. round-offset=_(lift offset)
  243. merks=_merks
  244. stream=_stream
  245. ==
  246. ::
  247. =/ new-len (div prev-len folding-deg)
  248. :: Read all cosets out of the next codeword
  249. =^ [indices=(list @) cosets=(map @ fpoly) merks=(list merk-data)] stream
  250. ?: =(+(round) num-rounds)
  251. :: if it's the last round, we use the codeword which was written into
  252. :: the proof in the clear
  253. [[~ ~ merks] stream]
  254. =/ root (head roots)
  255. =- [[(flop new-indices) cosets merks] stream]
  256. %+ roll prev-indices
  257. |= [prev-idx=@ new-indices=(list @) cosets=(map @ fpoly) merks=_merks stream=_stream]
  258. =/ new-idx (mod prev-idx (div prev-len folding-deg))
  259. =/ coset-idx (mod new-idx (div new-len folding-deg))
  260. =/ depth (xeb (div new-len folding-deg))
  261. =/ axis (index-to-axis depth coset-idx)
  262. :: read opening for index from proof
  263. =^ opening=proof-path stream
  264. =^(o stream ~(pull proof-stream stream) ?>(?=(%m-path -.o) p.o^stream))
  265. ::
  266. :^ [new-idx new-indices]
  267. (~(put by cosets) coset-idx leaf.opening)
  268. :- [(hash-hashable:tip5 (hashable-fpoly:tip5 leaf.opening)) axis root path.opening]
  269. merks
  270. stream
  271. ::
  272. ::
  273. :: Check folds
  274. =/ alpha (head alphas)
  275. =/ res=?
  276. %+ levy prev-indices
  277. |= prev-idx=@
  278. =/ prev-coset-idx (mod prev-idx (div prev-len folding-deg))
  279. =/ folded-val=felt
  280. =/ coeffs=fpoly
  281. (fp-ifft (~(got by prev-cosets) prev-coset-idx))
  282. =/ eval-point=felt
  283. (fdiv alpha (fmul round-offset (fpow omega prev-coset-idx)))
  284. (fpeval coeffs eval-point)
  285. =/ new-coset-idx (mod prev-coset-idx (div new-len folding-deg))
  286. =/ new-codeword-val=felt
  287. ?: =(+(round) num-rounds)
  288. :: for the last round, just read the value directly out of the last codeword
  289. (~(snag fop last-codeword) prev-coset-idx)
  290. =/ entry (div prev-coset-idx (div new-len folding-deg))
  291. =/ coset (~(got by cosets) new-coset-idx)
  292. (~(snag fop coset) entry)
  293. =(folded-val new-codeword-val)
  294. ::
  295. :: crash if folds were incorrect
  296. ?> =(res %.y)
  297. ::
  298. :* ?~(roots roots (tail roots))
  299. ?~(alphas alphas (tail alphas))
  300. indices
  301. cosets
  302. new-len
  303. (fpow omega folding-deg)
  304. (fpow round-offset folding-deg)
  305. merks
  306. stream
  307. ==
  308. -- ::fri-door
  309. -- ::fri