nock-common.hoon 5.0 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177
  1. :: nock-common: common arms between nock-prover and nock-verifier
  2. /= compute-table /common/table/verifier/compute
  3. /= memory-table /common/table/verifier/memory
  4. /= * /common/zeke
  5. |%
  6. :: all values in this table must generally be in the order of the tables
  7. :: specified in the following arm.
  8. ++ static-table-names
  9. ^- (list term) ^~
  10. %- sort
  11. :_ t-order
  12. :~ name:static:common:compute-table
  13. name:static:common:memory-table
  14. ==
  15. ::
  16. :: +core-table-names: tables utilized for every proof
  17. ++ core-table-names
  18. ^~ ^- (list term)
  19. %- sort
  20. :_ t-order
  21. :~ name:static:common:compute-table
  22. name:static:common:memory-table
  23. ==
  24. :: +opt-static-table-names: static tables only used when jute-flag=%.y
  25. ::
  26. :: TODO make these tables optional depending on whether these jutes are
  27. :: actually used
  28. ++ opt-static-table-names
  29. ^~ ^- (list term)
  30. ~
  31. ::
  32. :: +opt-dynamic-table-names: dynamic tables only used when jute-flag=%.y
  33. ++ opt-dynamic-table-names
  34. ^~ ^- (list term)
  35. ~
  36. ::
  37. ++ gen-table-names
  38. ^- (list term)
  39. %- sort
  40. :_ t-order
  41. %+ weld
  42. core-table-names
  43. (weld opt-static-table-names opt-dynamic-table-names)
  44. ::
  45. ++ dynamic-table-names
  46. ^~ ^- (list term)
  47. ~
  48. ::
  49. ++ all-table-names
  50. ^~ ^- (list term)
  51. %- sort
  52. :_ t-order
  53. (weld static-table-names dynamic-table-names)
  54. ::
  55. :: Widths of static tables. Dynamic tables (ie jute) need to be computed separately and passed
  56. :: in specific data needed for each table.
  57. ++ table-base-widths-static
  58. ^~ ^- (list @)
  59. %+ turn all-static-table-widths
  60. |=([name=term base-width=@ ext-width=@ mega-ext-width=@ full-width=@] base-width)
  61. ::
  62. ++ table-ext-widths-static
  63. ^~ ^- (list @)
  64. %+ turn all-static-table-widths
  65. |=([name=term base-width=@ ext-width=@ mega-ext-width=@ full-width=@] ext-width)
  66. ::
  67. ++ table-mega-ext-widths-static
  68. ^~ ^- (list @)
  69. %+ turn all-static-table-widths
  70. |=([name=term base-width=@ ext-width=@ mega-ext-width=@ full-width=@] mega-ext-width)
  71. ::
  72. ++ table-full-widths-static
  73. ^~ ^- (list @)
  74. %+ turn all-static-table-widths
  75. |=([name=term base-width=@ ext-width=@ mega-ext-width=@ full-width=@] full-width)
  76. ::
  77. ++ core-table-base-widths-static
  78. ^~ ^- (list @)
  79. %+ turn core-table-names
  80. |=(name=term base-width:(~(got by width-map) name))
  81. ::
  82. ++ core-table-full-widths-static
  83. ^~ ^- (list @)
  84. %+ turn core-table-names
  85. |=(name=term full-width:(~(got by width-map) name))
  86. ::
  87. ++ custom-table-base-widths-static
  88. |= table-names=(list term)
  89. ^- (list @)
  90. %+ turn table-names
  91. |=(name=term base-width:(~(got by width-map) name))
  92. ::
  93. ++ custom-table-full-widths-static
  94. |= table-names=(list term)
  95. ^- (list @)
  96. %+ turn table-names
  97. |=(name=term full-width:(~(got by width-map) name))
  98. ::
  99. ++ width-map
  100. ^~ ^- (map name=term [base-width=@ ext-width=@ mega-ext-width=@ full-width=@])
  101. %. all-static-table-widths
  102. %~ gas by
  103. ^* %+ map name=term
  104. [base-width=@ ext-width=@ mega-ext-width=@ full-width=@]
  105. ::
  106. ++ all-static-table-widths
  107. ^~ ^- (list [name=term base-width=@ ext-width=@ mega-ext-width=@ full-width=@])
  108. %- sort
  109. :_ tg-order
  110. :~
  111. ::
  112. :* name:static:common:compute-table
  113. (lent basic-column-names:static:common:compute-table)
  114. (lent ext-column-names:static:common:compute-table)
  115. (lent mega-ext-column-names:static:common:compute-table)
  116. (lent column-names:static:common:compute-table)
  117. ==
  118. ::
  119. :* name:static:common:memory-table
  120. (lent basic-column-names:static:common:memory-table)
  121. (lent ext-column-names:static:common:memory-table)
  122. (lent mega-ext-column-names:static:common:memory-table)
  123. (lent column-names:static:common:memory-table)
  124. ==
  125. ==
  126. ::
  127. ++ all-verifier-funcs
  128. ^~ ^- (list verifier-funcs)
  129. %- turn
  130. :_ tail
  131. %- sort
  132. :_ tg-order
  133. :~ [name:static:common:compute-table funcs:engine:compute-table]
  134. [name:static:common:memory-table funcs:engine:memory-table]
  135. ==
  136. ::
  137. ++ all-terminal-names
  138. ^~ ^- (list (list term))
  139. %- turn
  140. :_ tail
  141. %- sort
  142. :_ tg-order
  143. :~ [name:static:common:compute-table terminal-names:static:common:compute-table]
  144. [name:static:common:memory-table terminal-names:static:common:memory-table]
  145. ==
  146. ::
  147. ++ all-verifier-funcs-map
  148. ^~ ^- (map term verifier-funcs)
  149. %- ~(gas by *(map term verifier-funcs))
  150. :~ :- name:static:common:compute-table
  151. funcs:engine:compute-table
  152. :- name:static:common:memory-table
  153. funcs:engine:memory-table
  154. ==
  155. ::
  156. ++ remove-unused-constraints
  157. |= [pre=preprocess table-names=(list term) override=(unit (list term))]
  158. ^- preprocess
  159. ::
  160. =? cd.pre !=(~ override)
  161. %- ~(gas by *table-to-constraint-degree)
  162. %+ iturn table-names
  163. |= [j=@ name=term]
  164. ^- [@ constraint-degrees]
  165. =/ idx (i name all-table-names)
  166. [j (~(got by cd.pre) idx)]
  167. ::
  168. =? constraint-map.pre !=(~ override)
  169. %- ~(gas by *(map @ constraints))
  170. %+ iturn table-names
  171. |= [j=@ name=term]
  172. ^- [@ constraints]
  173. =/ idx (i name all-table-names)
  174. [j (~(got by constraint-map.pre) idx)]
  175. ::
  176. pre
  177. --