four.hoon 5.8 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234
  1. /= ztd-three /common/ztd/three
  2. => ztd-three
  3. ~% %proof-lib ..merkle ~
  4. :: proof-library
  5. |%
  6. +| %sur-proof-stream
  7. +$ noun-digests (list noun-digest:tip5)
  8. +$ proof-path [leaf=fpoly path=noun-digests]
  9. +$ proof-path-bf [leaf=bpoly path=noun-digests]
  10. ::
  11. +$ proof-data
  12. $% [%m-root p=noun-digest:tip5] :: merk-root
  13. [%puzzle commitment=noun-digest:tip5 nonce=noun-digest:tip5 len=@ p=*]
  14. [%codeword p=fpoly]
  15. [%terms p=bpoly] :: terminals
  16. [%m-paths a=proof-path b=proof-path c=proof-path]
  17. [%m-path p=proof-path] :: merk-path
  18. [%m-pathbf p=proof-path-bf] :: merk-path-bf
  19. [%comp-m p=noun-digest:tip5 num=@] :: composition-merk
  20. [%evals p=fpoly] :: evaluations
  21. [%heights p=(list @)] :: n, where 2^n is the number of rows
  22. ==
  23. ::
  24. +$ proof-objects (list proof-data)
  25. ::
  26. +$ proof
  27. $: objects=proof-objects
  28. hashes=(list noun-digest:tip5)
  29. read-index=@
  30. ==
  31. ::
  32. ++ hashable-proof-objects
  33. ~/ %hashable-proof-objects
  34. |= ps=proof-objects
  35. ^- hashable:tip5
  36. [%list (turn ps hashable-proof-data)]
  37. ::
  38. ++ hash-proof
  39. ~/ %hash-proof
  40. |= p=proof
  41. ^- noun-digest:tip5
  42. =/ rng (absorb-proof-objects objects.p ~)
  43. =^ lis=(list belt) rng (belts:rng 5)
  44. =- ?> ?=(noun-digest:tip5 -) -
  45. (list-to-tuple:tip5 lis)
  46. ::
  47. ++ absorb-proof-objects
  48. ~/ %absorb-proof-objects
  49. |= [objs=proof-objects hashes=(list noun-digest:tip5)]
  50. ^+ tog:tip5
  51. =. objs (slag (lent hashes) objs)
  52. =/ lis-digests=[%list (list hashable:tip5)]
  53. =/ h (hashable-noun-digests:tip5 hashes)
  54. ?> ?=(%list -.h)
  55. h
  56. =/ lis-objects=[%list (list hashable:tip5)]
  57. =/ h (hashable-proof-objects objs)
  58. ?> ?=(%list -.h)
  59. h
  60. =/ big-lis=(list noun-digest:tip5)
  61. (turn `(list hashable:tip5)`(weld +.lis-digests +.lis-objects) hash-hashable:tip5)
  62. =/ sponge (new:sponge:tip5)
  63. |-
  64. ?~ big-lis
  65. (new:tog:tip5 sponge:sponge)
  66. =+ [a=@ b=@ c=@ d=@ e=@]=i.big-lis
  67. =/ lis=(list belt) [a b c d e ~]
  68. $(big-lis t.big-lis, sponge (absorb:sponge lis))
  69. ::
  70. ::
  71. ++ hashable-proof-data
  72. ~/ %hashable-proof-data
  73. |= pd=proof-data
  74. ^- hashable:tip5
  75. ?- -.pd
  76. %m-root [leaf+%m-root hash+p.pd]
  77. %puzzle [leaf+%puzzle hash+commitment.pd hash+nonce.pd leaf+len.pd leaf+p.pd]
  78. %comp-m [leaf+%comp-m hash+p.pd leaf+num.pd]
  79. %heights [leaf+%heights leaf+p.pd]
  80. %codeword [leaf+%codeword (hashable-fpoly:tip5 p.pd)]
  81. %evals [leaf+%evals (hashable-fpoly:tip5 p.pd)]
  82. %terms [leaf+%terms (hashable-bpoly:tip5 p.pd)]
  83. ::
  84. %m-pathbf
  85. :- leaf+%m-pathbf
  86. :- (hashable-bpoly:tip5 leaf.p.pd)
  87. (hashable-noun-digests:tip5 path.p.pd)
  88. ::
  89. %m-path
  90. :- leaf+%m-mpath
  91. :- (hashable-fpoly:tip5 leaf.p.pd)
  92. (hashable-noun-digests:tip5 path.p.pd)
  93. ::
  94. %m-paths
  95. :- leaf+%m-mpaths
  96. :+ :- (hashable-fpoly:tip5 leaf.a.pd)
  97. (hashable-noun-digests:tip5 path.a.pd)
  98. :- (hashable-fpoly:tip5 leaf.b.pd)
  99. (hashable-noun-digests:tip5 path.b.pd)
  100. :- (hashable-fpoly:tip5 leaf.c.pd)
  101. (hashable-noun-digests:tip5 path.c.pd)
  102. ==
  103. ::
  104. ++ hash-proof-data
  105. ~/ %hash-proof-data
  106. |= pd=proof-data
  107. ^- noun-digest:tip5
  108. (hash-hashable:tip5 (hashable-proof-data pd))
  109. ::
  110. +| %sur-fock
  111. ::
  112. :: $zero-map: see description
  113. ::
  114. :: Nock 10 edits the noun so it has subject for the original noun and new-subject for the
  115. :: new edited noun. Nock 0 is proved exactly like a nock 10 but with new-subject=subject.
  116. :: So when recording a nock 0 you want to just pass subject in for new-subject.
  117. :: Basically a nock 0 is a special case of nock 10 where the edited tree is the original tree.
  118. +$ zero-map (map subject=* (map [axis=* new-subject=*] count=@))
  119. +$ decode-map (map [formula=* head=* tail=*] count=@)
  120. +$ fock-return
  121. $+ fock-return
  122. $: queue=(list *)
  123. zeroes=zero-map
  124. decodes=decode-map
  125. [s=* f=*]
  126. ::jutes=(list [@tas sam=* prod=*])
  127. ==
  128. :: $dyck-stack: horner accumulated stack of dyck path
  129. :: $dyck-felt: felt representing dyck-stack
  130. :: $leaf-stack: horner accumulated stack of leaves
  131. :: $leaf-felt: felt representing leaf-stack
  132. :: $ion-fprint: compressed $ion-triple: a*len + b*dyck-felt + c*leaf-felt
  133. :: $ion-triple: dyck encoding of a noun. called the ION fingerprint in the EDEN paper.
  134. :: $compute-stack: horner accumulated stack of packed-tree-felts
  135. :: $compute-felt: felt representing compute-stack
  136. :: $tree-data:
  137. ::
  138. :: .len: length of the leaf stack
  139. +$ tree-data
  140. $~ [pone pzero pzero 0]
  141. $: size=pelt :: alf^len
  142. dyck=pelt
  143. leaf=pelt
  144. n=*
  145. ==
  146. ::
  147. +$ pelt $~(pzero @ux)
  148. ::
  149. ++ pzero `pelt`(lift 0)
  150. ++ pone `pelt`(lift 1)
  151. ::
  152. ++ pelt-lift
  153. ~/ %pelt-lift
  154. |= b=belt
  155. ^- pelt
  156. (lift b)
  157. ::
  158. ++ padd
  159. ~/ %padd
  160. |= [p=pelt q=pelt]
  161. ^- pelt
  162. (fadd p q)
  163. ::
  164. ++ pneg
  165. ~/ %pneg
  166. |= p=pelt
  167. ^- pelt
  168. (fneg p)
  169. ::
  170. ++ psub
  171. ~/ %psub
  172. |= [p=pelt q=pelt]
  173. ^- pelt
  174. (fsub p q)
  175. ::
  176. ++ pmul
  177. ~/ %pmul
  178. |= [p=pelt q=pelt]
  179. ^- pelt
  180. (fmul p q)
  181. ::
  182. ++ pscal
  183. ~/ %pscal
  184. |= [c=belt p=pelt]
  185. ^- pelt
  186. dat:(bpscal c [3 p])
  187. ::
  188. ::
  189. ++ pinv
  190. ~/ %pinv
  191. |= p=pelt
  192. ^- pelt
  193. (finv p)
  194. ::
  195. :: +ppow: field power; computes x^n
  196. ++ ppow
  197. ~/ %ppow
  198. |= [x=pelt n=@]
  199. (fpow x n)
  200. ::
  201. ++ print-pelt
  202. ~/ %print-pelt
  203. |= [=pelt t=(list belt)]
  204. ^- (list belt)
  205. :^ (~(snag bop [3 pelt]) 0)
  206. (~(snag bop [3 pelt]) 1)
  207. (~(snag bop [3 pelt]) 2)
  208. t
  209. ::
  210. ++ got-pelt
  211. ~/ %got-pelt
  212. |= [mp=(map term belt) t=term]
  213. ^- pelt
  214. =< dat
  215. %- init-bpoly
  216. :~ (~(got by mp) (crip (weld (trip t) "-a")))
  217. (~(got by mp) (crip (weld (trip t) "-b")))
  218. (~(got by mp) (crip (weld (trip t) "-c")))
  219. ==
  220. ::
  221. ++ compress-pelt
  222. ~/ %compress-pelt
  223. |= [cs=(list pelt) ps=(list pelt)]
  224. ^- pelt
  225. %+ roll (zip-up cs ps)
  226. |= [[c=pelt p=pelt] acc=pelt]
  227. ^- pelt
  228. (padd acc (pmul c p))
  229. ::
  230. +$ compute-queue (list tree-data)
  231. ::
  232. +| %constants
  233. ++ ext-degree 3 :: goldilocks field degree
  234. --