one.hoon 35 KB

12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697989910010110210310410510610710810911011111211311411511611711811912012112212312412512612712812913013113213313413513613713813914014114214314414514614714814915015115215315415515615715815916016116216316416516616716816917017117217317417517617717817918018118218318418518618718818919019119219319419519619719819920020120220320420520620720820921021121221321421521621721821922022122222322422522622722822923023123223323423523623723823924024124224324424524624724824925025125225325425525625725825926026126226326426526626726826927027127227327427527627727827928028128228328428528628728828929029129229329429529629729829930030130230330430530630730830931031131231331431531631731831932032132232332432532632732832933033133233333433533633733833934034134234334434534634734834935035135235335435535635735835936036136236336436536636736836937037137237337437537637737837938038138238338438538638738838939039139239339439539639739839940040140240340440540640740840941041141241341441541641741841942042142242342442542642742842943043143243343443543643743843944044144244344444544644744844945045145245345445545645745845946046146246346446546646746846947047147247347447547647747847948048148248348448548648748848949049149249349449549649749849950050150250350450550650750850951051151251351451551651751851952052152252352452552652752852953053153253353453553653753853954054154254354454554654754854955055155255355455555655755855956056156256356456556656756856957057157257357457557657757857958058158258358458558658758858959059159259359459559659759859960060160260360460560660760860961061161261361461561661761861962062162262362462562662762862963063163263363463563663763863964064164264364464564664764864965065165265365465565665765865966066166266366466566666766866967067167267367467567667767867968068168268368468568668768868969069169269369469569669769869970070170270370470570670770870971071171271371471571671771871972072172272372472572672772872973073173273373473573673773873974074174274374474574674774874975075175275375475575675775875976076176276376476576676776876977077177277377477577677777877978078178278378478578678778878979079179279379479579679779879980080180280380480580680780880981081181281381481581681781881982082182282382482582682782882983083183283383483583683783883984084184284384484584684784884985085185285385485585685785885986086186286386486586686786886987087187287387487587687787887988088188288388488588688788888989089189289389489589689789889990090190290390490590690790890991091191291391491591691791891992092192292392492592692792892993093193293393493593693793893994094194294394494594694794894995095195295395495595695795895996096196296396496596696796896997097197297397497597697797897998098198298398498598698798898999099199299399499599699799899910001001100210031004100510061007100810091010101110121013101410151016101710181019102010211022102310241025102610271028102910301031103210331034103510361037103810391040104110421043104410451046104710481049105010511052105310541055105610571058105910601061106210631064106510661067106810691070107110721073107410751076107710781079108010811082108310841085108610871088108910901091109210931094109510961097109810991100110111021103110411051106110711081109111011111112111311141115111611171118111911201121112211231124112511261127112811291130113111321133113411351136113711381139114011411142114311441145114611471148114911501151115211531154115511561157115811591160116111621163116411651166116711681169117011711172117311741175117611771178117911801181118211831184118511861187118811891190119111921193119411951196119711981199120012011202120312041205120612071208120912101211121212131214121512161217121812191220122112221223122412251226122712281229123012311232123312341235123612371238123912401241124212431244124512461247124812491250125112521253125412551256125712581259126012611262126312641265126612671268126912701271127212731274127512761277127812791280128112821283128412851286128712881289129012911292129312941295129612971298129913001301130213031304130513061307130813091310131113121313131413151316131713181319132013211322132313241325132613271328132913301331133213331334133513361337133813391340134113421343134413451346134713481349135013511352135313541355135613571358135913601361136213631364136513661367136813691370137113721373137413751376137713781379138013811382138313841385138613871388
  1. ~% %zeke ..ut ~
  2. :: math-base: base field definitions and arithmetic
  3. |%
  4. +| %sur-field
  5. :: $belt: base field element
  6. ::
  7. :: An integer in the interval [0, p).
  8. :: Due to a well chosen p, almost all numbers representable with 64 bits
  9. :: are present in the interval.
  10. ::
  11. :: In other words, a belt under our choice of p will always fit in 64 bits.
  12. ::
  13. +$ belt @
  14. ::
  15. :: $felt: extension field element
  16. ::
  17. :: A list of base field elements encoded as a byte array in a single atom.
  18. :: Note that a high bit is set to force allocation of the whole memory region.
  19. ::
  20. :: The length is assumed by field math door defined later on,
  21. :: based on degree provided to it.
  22. ::
  23. :: If G is a degree 3 extension field over field F, then G's elements
  24. :: are 4-tuples of the form F^4 = (F, F, F, F). E.g., if F = {0, 1},
  25. :: an element of F would be 1, while an example element of G is (0, 1, 1, 0).
  26. ::
  27. :: The felt type represents exactly such elements of our extension field G.
  28. ::
  29. :: Since the extension field over the base field "happens to be" a polynomial ring,
  30. :: the felt (1, 2, 3) can be thought of as a polynomial (1 + 2x + 3x^2).
  31. :: However, it is recommended by the elders to avoid thinking of felts
  32. :: as polynomials, and to maintain a more abstract conception of them as tuples.
  33. ::
  34. +$ felt @ux
  35. ::
  36. :: $melt: Montgomery space element
  37. ::
  38. :: `Montgomery space` is obtained from the base field (Z_p, +, •) by replacing ordinary
  39. :: modular multiplication • with Montgomery multiplication *: a*b = abr^{-1} mod p, where
  40. :: r = 2^64. The map a --> r•a is a field isomorphism, so in particular
  41. :: (r•a)*(r•b) = r•(a*b). Note that (r mod p) is the mult. identity in Montgomery space.
  42. ::
  43. +$ melt @
  44. ::
  45. :: $bpoly: a polynomial of explicit length with base field coefficients.
  46. ::
  47. :: A pair of a length (must fit within 32 bits) and dat, which is
  48. :: a list of base field coefficients, encoded as a byte array.
  49. :: Note that a high bit is set to force allocation of the whole memory region.
  50. ::
  51. :: Critically, a bpoly is isomorphic to a felt (at least when its lte is lower than degree).
  52. ::
  53. :: In other words, a polynomial defined as a list of base element coefficients
  54. :: is equivalent to a single element of the extension field.
  55. ::
  56. :: N.B: Sometimes, bpoly is used to represent a list of belt values
  57. :: of length greater than degree that are not meant to be interpreted
  58. :: as extension field elements (!).
  59. ::
  60. :: TODO: would be nice to have a separate typedef for the arb. len. list case
  61. ::
  62. +$ bpoly [len=@ dat=@ux]
  63. ::
  64. :: $fpoly: a polynomial of explicit length with *extension field* coefficients.
  65. ::
  66. :: A pair of a length (must fit inside 32 bits) and dat, a big atom
  67. :: made up of (D * len) base field coefficients, where D is the extension degree.
  68. :: Note that a high bit is set to force allocation of the whole memory region.
  69. ::
  70. :: Put another way, an fpoly is a polynomial whose coefficients are felts
  71. :: (i.e. tuple of belts) instead of numbers (belts).
  72. ::
  73. :: N.B: Sometimes, fpoly is used to represent a list of felt values
  74. :: that aren't meant to be interpreted interpreted as polynomials
  75. :: with felt coefficients (!).
  76. ::
  77. +$ fpoly [len=@ dat=@ux]
  78. ::
  79. ::
  80. :: $poly: list of coefficients [a_0 a_1 a_2 ... ] representing a_0 + a_1*x + a_2*x^2 + ...
  81. ::
  82. :: Note any polynomial has an infinite set of list representatives by adding 0's
  83. :: arbitrarily to the end of the list.
  84. :: Note also that ~ represents the zero polynomial.
  85. ::
  86. :: Somewhat surprisingly, this type can reprsent both polynomials
  87. :: whose coefficients are belts (aka felts), and polynomials whose
  88. :: coefficients are themselves felts, aka fpolys. This works because felts
  89. :: are encoded as a single atom, the same form factor as belts.
  90. ::
  91. +$ poly (list @)
  92. ::
  93. ::: $array
  94. ::
  95. :: An array of u64 words stored as an atom. This is exactly the same thing as bpoly and fpoly
  96. :: but is more general and used for any data you want to store in a contiguous array and not
  97. :: only polynomials.
  98. ::
  99. +$ array [len=@ dat=@ux]
  100. ::
  101. :: $mary
  102. ::
  103. :: An array where each element is step size (in u64 words). This can be used to build
  104. :: multi-dimensional arrays or to store any data you want in one contiguous array.
  105. ::
  106. +$ mary [step=@ =array]
  107. ::
  108. :: $mp-mega: multivariate polynomials in their final form
  109. ::
  110. :: The multivariate polynomial is stored in a sparse map like in the multi-poly data type.
  111. :: For each monomial term, there is a key and a value. The value is just the belt coefficient.
  112. :: The key is a bpoly which packs in each element of the monomial. It looks like this:
  113. ::
  114. :: [term term term ... term]=bpoly
  115. ::
  116. :: where each term is one 64-bit direct atom. The format of a term is this:
  117. ::
  118. :: 3 bits - type of term
  119. :: 10 bits - index of term into list of variables / challenges / dynamics
  120. :: 30 bits - exponent as @ud
  121. ::
  122. :: [TTIIIIIIIIIIEEEEEEEEEEEEEEEEEEEEEEEEEEEEEE]
  123. ::
  124. :: This only uses 43 bits which is plenty since the exponent can only be max 4 anyway.
  125. :: So it safely fits inside a direct atom.
  126. ::
  127. :: The type of term can be:
  128. :: con - constant (so it's just the zero bpoly and the coefficient is the value)
  129. :: var - variable. the index is the index of the variable.
  130. :: rnd - random challenge from the verifier. the index is the index into the challenge list.
  131. :: dyn - dynamic element so terminal. the index is the index into the dynamic list.
  132. ::
  133. :: The reason for this is that the constraints are static and so we would like to build
  134. :: them into an efficient data structure during a preprocess step and not every time we
  135. :: generate a proof. The problem is that we don't know the challenges or the dynamics until
  136. :: we are in the middle of generating a proof. So we store the index of the challenges and
  137. :: dynamics in the data structure and read them out when we evaluate or substitute the polys.
  138. ::
  139. +$ mp-mega (map bpoly belt)
  140. +$ mp-comp [dep=(list mp-mega) com=(list mp-mega)]
  141. +$ mp-ultra
  142. $% [%mega mp-mega]
  143. [%comp mp-comp]
  144. ==
  145. ::
  146. :: $mp-graph: A multi-poly stored as an expression graph to preserve semantic information.
  147. ::
  148. +$ mp-graph
  149. $~ [%con a=0]
  150. $% [%con a=belt] :: belt constant
  151. [%rnd t=term] :: random challenge, labeled by name
  152. [%var col=@] :: variable. col is 0-based column index
  153. [%dyn d=term] :: dynamic values for dynamically generated constraint
  154. [%add a=mp-graph b=mp-graph]
  155. [%sub a=mp-graph b=mp-graph]
  156. [%mul a=mp-graph b=mp-graph]
  157. ::
  158. :: note: inv used for field inversion of constant polynomial
  159. [%inv a=mp-graph]
  160. [%neg a=mp-graph]
  161. [%pow a=mp-graph n=@]
  162. [%scal c=belt a=mp-graph]
  163. [%mon-belt c=belt v=bpoly]
  164. [%mon-exp c=mp-graph v=bpoly]
  165. [%addl l=(list mp-graph)]
  166. [%rnd-e t=term]
  167. [%dyn-e d=term]
  168. [%nil ~] :: annihilate
  169. ==
  170. ::
  171. +| %lib-list
  172. +$ elt @ux
  173. ::
  174. ++ rip-correct
  175. ~/ %rip-correct
  176. |= [a=bite b=@]
  177. ^- (list @)
  178. ?: =(0 b) ~[0]
  179. (rip a b)
  180. ::
  181. ++ mary-to-list
  182. ~/ %mary-to-list
  183. |= ma=mary
  184. ^- (list elt)
  185. ?: =(len.array.ma 0) ~
  186. %+ turn (snip (rip [6 step.ma] dat.array.ma))
  187. |= elem=@
  188. ^- elt
  189. %+ add elem
  190. ?:(=(step.ma 1) 0 (lsh [6 step.ma] 1))
  191. ::
  192. ++ zing-bpolys
  193. ~/ %zing-bpolys
  194. |= l=(list bpoly)
  195. ^- mary
  196. ?~ l !! :: can't return zero-mary because we can't figure out the step from ~
  197. %+ do-init-mary len:(head l)
  198. (turn l |=(=bpoly dat.bpoly))
  199. ::
  200. ++ zing-fpolys
  201. ~/ %zing-fpolys
  202. |= l=(list fpoly)
  203. ^- mary
  204. ?~ l !! :: can't return zero-mary because we can't figure out the step from ~
  205. %+ do-init-mary (mul 3 len:(head l))
  206. (turn l |=(=fpoly dat.fpoly))
  207. ::
  208. ++ zing-marys
  209. ~/ %zing-marys
  210. |= l=(list mary)
  211. ^- mary
  212. ?~ l !! :: can't return zero-mary because we can't figure out the step from ~
  213. %+ do-init-mary len.array:(head l)
  214. (turn l |=(=mary dat.array.mary))
  215. ::
  216. :: +met-elt measure the size of the elements in a mary
  217. ::
  218. :: This is used to compute what the step should be when turning a list into a mary.
  219. :: If elt is larger than a belt, then (met 6 elt) will include the word for the high bit.
  220. :: We don't want this and so subtract it off. But if elt is a belt then it has no high bit.
  221. :: (met 6 elt) will return 1 and (dec (met 6 elt)) would erroneously return 0. So this is special
  222. :: cased by setting the max to be 2. This way belts return the correct size of 1.
  223. ++ met-elt
  224. |= =elt
  225. ^- @
  226. (dec (max 2 (met 6 elt)))
  227. ::
  228. ++ init-mary
  229. ~/ %init-mary
  230. |= poly=(list elt)
  231. ^- mary
  232. ?~ poly !! :: can't return zero-mary because we can't figure out the step from ~
  233. (do-init-mary (met-elt (head poly)) poly)
  234. ::
  235. ++ do-init-mary
  236. ~/ %do-init-mary
  237. |= [step=@ poly=(list elt)]
  238. ^- mary
  239. ?: =(~ poly)
  240. ~(zero-mary mary-utils step)
  241. ?> (lth (lent poly) (bex 32))
  242. ?> (levy poly |=(=elt &((~(fet mary-utils step) elt) =(step (met-elt elt)))))
  243. :- step
  244. :- (lent poly)
  245. =/ high-bit (lsh [0 (mul (bex 6) (mul step (lent poly)))] 1)
  246. (add (rep [6 step] poly) high-bit)
  247. ::
  248. ++ mary-utils
  249. ~/ %mary-utils
  250. |_ step=@
  251. ++ fet
  252. ~/ %fet
  253. |= a=@
  254. ^- ?
  255. ~+
  256. =/ v (rip-correct 6 a)
  257. ?& |(&(=((lent v) 1) =(step 1)) =((lent v) +(step)))
  258. (levy v based)
  259. ==
  260. ::
  261. ++ lift-elt
  262. ~/ %lift-elt
  263. |= a=@
  264. ^- elt
  265. ?:(=(step 1) `@ux`a dat:(init-bpoly [a (reap (dec step) 0)]))
  266. ::
  267. ++ zero-mary
  268. ~+
  269. ^- mary
  270. ?: =(step 1) [1 1 `@ux`0]
  271. (init-mary ~[(lift-elt 0)])
  272. --
  273. ::
  274. ++ ave
  275. ~/ %ave
  276. =| ma=mary
  277. |%
  278. ++ flop
  279. ^- mary
  280. =/ p to-poly
  281. (do-init-mary step.ma (^flop p))
  282. ::
  283. ++ zip
  284. ~/ %zip
  285. |= [na=mary a=$-([elt elt] elt)]
  286. ^- mary
  287. ?> =(len.array.ma len.array.na)
  288. :- step.ma
  289. :- len.array.ma
  290. =/ i 0
  291. |-
  292. ?: =(i len.array.ma)
  293. dat.array.ma
  294. =/ mi (snag i)
  295. =/ ni (~(snag ave na) i)
  296. $(i +(i), ma (stow i (a mi ni)))
  297. ::
  298. ++ zero-extend
  299. ~/ %zero-extend
  300. |= n=@
  301. ^- mary
  302. :- step.ma
  303. :- (add len.array.ma n)
  304. =/ i 0
  305. =/ dat dat.array.ma
  306. |-
  307. ?: =(i n)
  308. dat
  309. %_ $
  310. dat dat.array:(~(snoc ave [step.ma (add len.array.ma i) dat]) (~(lift-elt mary-utils step.ma) 0))
  311. i +(i)
  312. ==
  313. ::
  314. ++ weld
  315. ~/ %weld
  316. |= ma2=mary
  317. ^- mary
  318. :- step.ma
  319. :- (add len.array.ma len.array.ma2)
  320. =/ i 0
  321. =/ dat dat.array.ma
  322. |-
  323. ?: =(i len.array.ma2)
  324. dat
  325. %_ $
  326. dat dat.array:(~(snoc ave [step.ma (add len.array.ma i) dat]) (~(snag ave ma2) i))
  327. i +(i)
  328. ==
  329. ::
  330. ++ head
  331. ^- elt
  332. (snag 0)
  333. ::
  334. ++ rear
  335. ^- elt
  336. (snag (dec len.array.ma))
  337. ::
  338. ++ snag-as-mary
  339. ~/ %snag-as-mary
  340. |= i=@
  341. ^- mary
  342. [step.ma 1 (snag i)]
  343. ::
  344. ++ snag-as-fpoly
  345. ~/ %snag-as-fpoly
  346. |= i=@
  347. ^- fpoly
  348. [(div step.ma 3) (snag i)]
  349. ::
  350. ++ snag-as-bpoly
  351. ~/ %snag-as-bpoly
  352. |= i=@
  353. ^- bpoly
  354. :- step.ma
  355. =/ dat (snag i)
  356. ?: =(step.ma 1)
  357. =/ high-bit (lsh [0 (mul (bex 6) step.ma)] 1)
  358. (add high-bit dat)
  359. dat
  360. ::
  361. ++ snag
  362. ~/ %snag
  363. |= i=@
  364. ^- elt
  365. ?> (lth i len.array.ma)
  366. =/ res (cut 6 [(mul i step.ma) step.ma] dat.array.ma)
  367. ?: =(step.ma 1) res
  368. =/ high-bit (lsh [0 (mul (bex 6) step.ma)] 1)
  369. (add high-bit res)
  370. ::
  371. ++ scag
  372. ~/ %scag
  373. |= i=@
  374. ^- mary
  375. ?: =(i 0)
  376. ~(zero-mary mary-utils step.ma)
  377. ?: (gte i len.array.ma) ma
  378. :- step.ma
  379. :- i
  380. =/ high-bit (lsh [0 (mul i (mul (bex 6) step.ma))] 1)
  381. %+ add high-bit
  382. (cut 6 [0 (mul i step.ma)] dat.array.ma)
  383. ::
  384. ++ slag
  385. ~/ %slag
  386. |= i=@
  387. ^- mary
  388. ?: (gte i len.array.ma)
  389. ~(zero-mary mary-utils step.ma)
  390. [step.ma (sub len.array.ma i) (rsh [6 (mul i step.ma)] dat.array.ma)]
  391. ::
  392. ++ swag
  393. ~/ %swag
  394. |= [i=@ j=@]
  395. ^- mary
  396. (~(scag ave (slag i)) j)
  397. ::
  398. ++ snoc
  399. ~/ %snoc
  400. |= j=elt
  401. ^- mary
  402. :: fix bunt
  403. ::
  404. :: *bpoly should be [1 0x1] not [1 0x0] so it has a high bit with no data. We can't
  405. :: change the bunt right now, so this is a workaround just for snoc. Without it,
  406. :: snoccing onto *bpoly fails.
  407. =. ma
  408. ?. =(ma [1 *bpoly]) ma
  409. [1 0 0x1]
  410. ?> (~(fet mary-utils step.ma) j)
  411. :- step.ma
  412. :- +(len.array.ma)
  413. =/ new-high-bit (lsh [0 (mul (bex 6) (mul step.ma +(len.array.ma)))] 1)
  414. =/ old-high-bit (lsh [0 (mul (bex 6) (mul step.ma len.array.ma))] 1)
  415. %^ sew 6
  416. [(mul len.array.ma step.ma) step.ma j]
  417. (sub (add new-high-bit dat.array.ma) old-high-bit)
  418. ::
  419. ++ weld-step
  420. ~/ %weld-step
  421. |= na=mary
  422. ^- mary
  423. ?> =(len.array.ma len.array.na)
  424. %+ roll (range len.array.na)
  425. =/ mu=mary
  426. :+ (add step.ma step.na)
  427. len.array.ma
  428. (lsh [6 (mul (add step.ma step.na) len.array.ma)] 1)
  429. |= [i=@ mu=_mu]
  430. =; weld-dat
  431. (~(stow ave mu) i weld-dat)
  432. =/ r1 (snag i)
  433. =? r1 !=(step.ma 1)
  434. (sub r1 (lsh [6 step.ma] 1))
  435. =/ r2 (~(snag ave na) i)
  436. =? r2 !=(step.na 1)
  437. (add (lsh [6 step.na] 1) r2)
  438. (add (lsh [6 step.ma] r2) r1)
  439. ::
  440. ++ stow
  441. ~/ %stow
  442. |= [i=@ j=elt]
  443. ^- mary
  444. ?> (~(fet mary-utils step.ma) j)
  445. ?> (lth i len.array.ma)
  446. =/ item
  447. ?: =(step.ma 1)
  448. j
  449. (rep 6 (snip (rip 6 j)))
  450. [step.ma len.array.ma (sew 6 [(mul i step.ma) step.ma item] dat.array.ma)]
  451. ::
  452. ++ change-step
  453. ~/ %change-step
  454. |= [new-step=@]
  455. ^- mary
  456. ?: =(step.ma new-step) ma
  457. ?> =((mod (mul step.ma len.array.ma) new-step) 0)
  458. :+ new-step
  459. (div (mul step.ma len.array.ma) new-step)
  460. dat.array.ma
  461. ::
  462. ++ to-poly
  463. ^- poly
  464. (mary-to-list ma)
  465. ::
  466. ++ transpose
  467. ~/ %transpose
  468. |= offset=@
  469. ^- mary
  470. =/ res-step (mul len.array.ma offset)
  471. =/ res-len (div step.ma offset)
  472. =/ res=mary [res-step [res-len (lsh [6 (mul res-step res-len)] 1)]]
  473. =/ num-cols res-len
  474. =/ num-rows len.array.ma
  475. %+ roll (range num-cols)
  476. |= [i=@ m=_res]
  477. %+ roll (range num-rows)
  478. |= [j=@ m=_m]
  479. =/ target-index (add (mul i num-rows) j)
  480. ::
  481. =/ source (cut 6 [(mul offset (add (mul j num-cols) i)) offset] dat.array.ma)
  482. m(dat.array (sew 6 [(mul offset target-index) offset source] dat.array.m))
  483. ::
  484. :: check if len matches the actual size of dat
  485. ++ chck
  486. ^- ?
  487. =((mul step.ma len.array.ma) (dec (met 6 dat.array.ma)))
  488. -- :: ave
  489. ::
  490. ++ transpose-fpolys
  491. ~/ %transpose-fpolys
  492. |= fpolys=mary
  493. ^- mary
  494. (~(transpose ave fpolys) 3)
  495. ::
  496. ++ transpose-bpolys
  497. ~/ %transpose-bpolys
  498. |= bpolys=mary
  499. ^- mary
  500. (~(transpose ave bpolys) 1)
  501. ::
  502. ++ array-op
  503. ~/ %array-op
  504. |_ step=@
  505. ::
  506. ++ ops
  507. =| fp=array
  508. ~/ %ops
  509. |%
  510. ++ op ~(. ave [step fp])
  511. ++ flop
  512. ^- fpoly
  513. array:flop:op
  514. ++ zip
  515. ~/ %zip
  516. |= [gp=fpoly a=$-([felt felt] felt)]
  517. ^- fpoly
  518. array:(zip:op [step gp] a)
  519. ::
  520. ++ zero-extend
  521. ~/ %zero-extend
  522. |= n=@
  523. array:(zero-extend:op n)
  524. ::
  525. ++ weld
  526. ~/ %weld
  527. |= fp2=fpoly
  528. ^- fpoly
  529. array:(weld:op [step fp2])
  530. ::
  531. ++ head
  532. ^- felt
  533. (snag 0)
  534. ::
  535. ++ rear
  536. ^- felt
  537. (snag (dec len.fp))
  538. ::
  539. ++ snag
  540. ~/ %snag
  541. |= i=@
  542. ^- felt
  543. (snag:op i)
  544. ::
  545. ++ scag
  546. ~/ %scag
  547. |= i=@
  548. ^- fpoly
  549. array:(scag:op i)
  550. ::
  551. ++ slag
  552. ~/ %slag
  553. |= i=@
  554. ^- fpoly
  555. array:(slag:op i)
  556. ::
  557. ++ swag
  558. ~/ %swag
  559. |= [i=@ j=@]
  560. ^- fpoly
  561. array:(swag:op i j)
  562. ::
  563. ++ snoc
  564. ~/ %snoc
  565. |= j=felt
  566. ^- fpoly
  567. array:(snoc:op j)
  568. ::
  569. ++ stow
  570. ~/ %stow
  571. |= [i=@ j=felt]
  572. ^- fpoly
  573. array:(stow:op i j)
  574. ::
  575. ++ to-poly
  576. ^- poly
  577. (mary-to-list [step fp])
  578. ::
  579. ++ chck
  580. ^- ?
  581. chck:op
  582. --
  583. --
  584. ::
  585. :: turn a 1-dimensional array into a 1-element 2-dimensional array
  586. ++ lift-mop
  587. |= fp=fpoly
  588. ^- mary
  589. [(mul 3 len.fp) 1 dat.fp]
  590. ::
  591. :: +fpoly-to-mary
  592. ::
  593. :: View an fpoly as a 3-step mary.
  594. ::
  595. :: Note that +fpoly-to-marry just views the fpoly as an mary. It has the same length
  596. :: and each element is a felt. +lift-mop on the other hand turns the fpoly into an array
  597. :: of fpolys which has step=len.fpoly and contains exactly one element- the fpoly passed in.
  598. ::
  599. ++ fpoly-to-mary
  600. |= fp=fpoly
  601. ^- mary
  602. [3 fp]
  603. ::
  604. :: +bpoly-to-mary: view a bpoly as 1-step mary
  605. ++ bpoly-to-mary
  606. |= bp=bpoly
  607. ^- mary
  608. [1 bp]
  609. ::
  610. :: +i: reverse index lookup:
  611. ::
  612. :: given an item and a list,
  613. :: produce the index of the item in the list
  614. ++ i
  615. ~+
  616. |= [item=@tas lis=(list @tas)]
  617. ::TODO make this wet
  618. ^- @
  619. (need (find ~[item] lis))
  620. ::
  621. ++ zip-up
  622. ~/ %zip-up
  623. |* [p=(list) q=(list)]
  624. ^- (list _?>(?&(?=(^ p) ?=(^ q)) [i.p i.q]))
  625. (zip p q same)
  626. ::
  627. ++ zip
  628. ~/ %zip
  629. |* [p=(list) q=(list) r=gate]
  630. ^- (list _?>(?&(?=(^ p) ?=(^ q)) (r i.p i.q)))
  631. |-
  632. ?: ?&(?=(~ p) ?=(~ q))
  633. ~
  634. ?. ?&(?=(^ p) ?=(^ q)) ~|(%zip-fail-unequal-lengths !!)
  635. [i=(r i.p i.q) t=$(p t.p, q t.q)]
  636. ::
  637. ++ sum
  638. ~/ %sum
  639. |= lis=(list @)
  640. ^- @
  641. %+ roll lis
  642. |= [a=@ r=@]
  643. (add a r)
  644. ::
  645. ++ mul-all
  646. ~/ %mul-all
  647. |= [lis=(list @) x=@]
  648. ^- (list @)
  649. %+ turn lis
  650. |=(a=@ (mul a x))
  651. ::
  652. ++ add-all
  653. ~/ %add-all
  654. |= [lis=(list @) x=@]
  655. ^- (list @)
  656. %+ turn lis
  657. |=(a=@ (add a x))
  658. ::
  659. ++ mod-all
  660. ~/ %mod-all
  661. |= [lis=(list @) x=@]
  662. ^- (list @)
  663. %+ turn lis
  664. |=(a=@ (mod a x))
  665. ::
  666. ++ zip-roll
  667. ~/ %zip-roll
  668. |* [p=(list) q=(list) r=_=>(~ |=([[* *] *] +<+))]
  669. |- ^+ ,.+<+.r
  670. ?~ p
  671. ?~ q
  672. +<+.r
  673. !!
  674. ?. ?=(^ q) ~|(%zip-roll-fail-unequal-lengths !!)
  675. $(p t.p, q t.q, r r(+<+ (r [i.p i.q] +<+.r)))
  676. ::
  677. ++ range
  678. ~/ %range
  679. |= $@(@ ?(@ (pair @ @)))
  680. ^- (list @)
  681. ?@ +< ?~(+< ~ (gulf 0 (dec +<)))
  682. (gulf p (dec q))
  683. ::
  684. :: +mevy: maybe error levy
  685. ::
  686. ++ mevy
  687. :: ~ if no failures or (some err) of the first error encountered
  688. ~/ %mevy
  689. |* [a=(list) b=$-(* (unit))]
  690. =* b-product _?>(?=(^ a) (b i.a))
  691. |- ^- b-product
  692. ?~ a ~
  693. ?^ err=(b i.a) err
  694. $(a t.a)
  695. ::
  696. :: +iturn: indexed turn. Gate gets a 0-based index of which list element it is on.
  697. ++ iturn
  698. ~/ %iturn
  699. |* [a=(list) b=_|=([@ *] +<+)]
  700. ^- (list _?>(?=(^ a) (b i.a)))
  701. =/ n 0
  702. |-
  703. ?~ a ~
  704. [i=(b [n i.a]) t=$(a t.a, n +(n))]
  705. ::
  706. :: +median: computes the median value of a (list @)
  707. ::
  708. :: if the length of the list is odd, its the middle value. if its
  709. :: even, we average the two middle values (rounding down)
  710. ++ median
  711. ~/ %median
  712. |= xs=(list @)
  713. ^- @
  714. =/ len=@ (lent xs)
  715. =/ parity=@ (mod (lent xs) 2)
  716. =/ sorted=(list @) (sort xs lth)
  717. |-
  718. ?~ sorted ~|("median of empty list" !!)
  719. ::TODO why do i need to cast to (list @) everywhere?
  720. ?: ?& =(parity 0) :: even case
  721. =(len 2) :: 2 elements remain
  722. ==
  723. %- div
  724. :_ 2
  725. %+ add (snag 0 `(list @)`sorted)
  726. (snag 1 `(list @)`sorted)
  727. ?: ?& =(parity 1) :: odd case
  728. =(len 1) :: 1 element remains
  729. ==
  730. (snag 0 `(list @)`sorted)
  731. :: otherwise, remove first and last element and repeat
  732. %_ $
  733. sorted (snip (slag 1 `(list @)`sorted))
  734. len (dec (dec len))
  735. ==
  736. ::
  737. :: clev: cleave a list into a list of lists w specified sizes (unless list is exhausted)
  738. :: TODO: could be made wet wrt a
  739. ++ clev
  740. |= [a=(list @) sizes=(list @)]
  741. ^- (list (list @))
  742. =- (flop acc)
  743. %+ roll sizes
  744. |= [s=@ a=_a acc=(list (list @))]
  745. :- (slag s a)
  746. [(scag s a) acc]
  747. ::
  748. ::
  749. +| %base58
  750. ++ en-base58
  751. |= dat=@
  752. =/ cha
  753. '123456789ABCDEFGHJKLMNPQRSTUVWXYZabcdefghijkmnopqrstuvwxyz'
  754. %- flop
  755. |- ^- tape
  756. ?: =(0 dat) ~
  757. :- (cut 3 [(mod dat 58) 1] cha)
  758. $(dat (div dat 58))
  759. ::
  760. ++ de-base58
  761. |= t=tape
  762. =- (scan t (bass 58 (plus -)))
  763. ;~ pose
  764. (cook |=(a=@ (sub a 56)) (shim 'A' 'H'))
  765. (cook |=(a=@ (sub a 57)) (shim 'J' 'N'))
  766. (cook |=(a=@ (sub a 58)) (shim 'P' 'Z'))
  767. (cook |=(a=@ (sub a 64)) (shim 'a' 'k'))
  768. (cook |=(a=@ (sub a 65)) (shim 'm' 'z'))
  769. (cook |=(a=@ (sub a 49)) (shim '1' '9'))
  770. ==
  771. ::
  772. +| %constants
  773. :: +p: field characteristic p = 2^64 - 2^32 + 1 = (2^32)*3*5*17*257*65537 + 1
  774. :: +r: radix r = 2^64
  775. :: +r-mod-p: r-mod-p = r - p
  776. :: +r2: r^2 mod p = (2^32 - 1)^2 = 2^64 - 2*2^32 + 1 = p - 2^32
  777. :: +rp: r*p
  778. :: +g: ord(g) = p - 1, i.e. g generates the (multiplicative group of the) field
  779. :: +h: ord(h) = 2^32, i.e. h = (2^32)th root of unity
  780. ++ p 0xffff.ffff.0000.0001
  781. ++ r 0x1.0000.0000.0000.0000
  782. ++ r-mod-p 4.294.967.295
  783. ++ r2 0xffff.fffe.0000.0001
  784. ++ rp 0xffff.ffff.0000.0001.0000.0000.0000.0000
  785. ++ g 7
  786. ++ h 20.033.703.337
  787. +| %base-field
  788. :: +based: in base field?
  789. ++ based
  790. ~/ %based
  791. |= a=@
  792. ^- ?
  793. (lth a p)
  794. ::
  795. :: is this noun based
  796. ++ based-noun
  797. ~/ %based-noun
  798. |= n=*
  799. ^- ?
  800. ?@ n
  801. (based n)
  802. &($(n -.n) $(n +.n))
  803. ::
  804. :: +badd: base field addition
  805. ++ badd
  806. ~/ %badd
  807. |= [a=belt b=belt]
  808. ^- belt
  809. ?> ?&((based a) (based b))
  810. (mod (add a b) p)
  811. ::
  812. :: +bneg: base field negation
  813. ++ bneg
  814. ~/ %bneg
  815. |= a=belt
  816. ^- belt
  817. ?> (based a)
  818. ?: =(a 0)
  819. 0
  820. (sub p a)
  821. ::
  822. :: +bsub: base field subtraction
  823. ++ bsub
  824. ~/ %bsub
  825. |= [a=belt b=belt]
  826. ^- belt
  827. (badd a (bneg b))
  828. ::
  829. :: +bmul: base field multiplication
  830. ++ bmul
  831. ~/ %bmul
  832. |= [a=belt b=belt]
  833. ^- belt
  834. ?> ?&((based a) (based b))
  835. (mod (mul a b) p)
  836. ::
  837. :: +bmix: binary XOR mod p
  838. ++ bmix
  839. ~/ %bmix
  840. |= [a=@ b=@]
  841. ^- @
  842. (mod (mix a b) p)
  843. ::
  844. :: +mont-reduction: special algorithm; computes x•r^{-1} = (xr^{-1} mod p).
  845. ::
  846. :: Note this is the inverse of x --> r•x, so conceptually this is a map from
  847. :: Montgomery space to the base field.
  848. ::
  849. :: It's `special` bc we gain efficiency by examining the general algo by hand
  850. :: and deducing the form of the final answer, which we can code directly.
  851. :: If you compute the algo by hand you will find it convenient to write
  852. :: x = x_2*2^64 + x_1*2^32 + x_0 where x_2 is a 64-bit number less than
  853. :: p (so x < pr) and x_1, x_0 are 32-bit numbers.
  854. :: The formula comes, basically, to (x_2 - (2^32(x_0 + x_1) - x_1 - f*p));
  855. :: f is a flag bit for the overflow of 2^32(x_0 + x_1) past 64 bits.
  856. :: "Basically" means we have to add p if the formula is negative.
  857. ++ mont-reduction
  858. ~/ %mont-reduction
  859. |= x=melt
  860. ^- belt
  861. ?> (lth x rp)
  862. =/ x1 (cut 5 [1 1] x)
  863. =/ x2 (rsh 6 x)
  864. =/ c
  865. =/ x0 (end 5 x)
  866. (lsh 5 (add x0 x1))
  867. =/ f (rsh 6 c)
  868. =/ d (sub c (add x1 (mul f p)))
  869. ?: (gte x2 d)
  870. (sub x2 d)
  871. (sub (add x2 p) d)
  872. ::
  873. :: +montiply: computes a*b = (abr^{-1} mod p); note mul, not fmul: avoids mod p reduction!
  874. ++ montiply
  875. ~/ %montiply
  876. |: [a=`melt`r-mod-p b=`melt`r-mod-p]
  877. ^- belt
  878. ~+
  879. ?> ?&((based a) (based b))
  880. (mont-reduction (mul a b))
  881. ::
  882. :: +montify: transform to Montgomery space, i.e. compute x•r = xr mod p
  883. ++ montify
  884. ~/ %montify
  885. |= x=belt
  886. ^- melt
  887. ~+
  888. (montiply x r2)
  889. ::
  890. :: +bpow: fast modular exponentiation using x^n mod p = 1*(xr)*...*(xr)
  891. ++ bpow
  892. ~/ %bpow
  893. |= [x=belt n=@]
  894. ^- belt
  895. ?> (based x)
  896. ~+
  897. %. [1 (montify x) n]
  898. |= [y=melt x=melt n=@]
  899. ^- melt
  900. ?: =(n 0)
  901. y
  902. :: parity flag
  903. =/ f=@ (end 0 n)
  904. ?: =(0 f)
  905. $(x (montiply x x), n (rsh 0 n))
  906. $(y (montiply y x), x (montiply x x), n (rsh 0 n))
  907. ::
  908. :: +binv: base field multiplicative inversion
  909. ++ binv
  910. ~/ %binv
  911. |= x=belt
  912. ^- belt
  913. ~+
  914. |^
  915. ~| "x not in field"
  916. ?> (based x)
  917. ~| "cannot divide by 0"
  918. ?< =(x 0)
  919. =/ y=melt (montify x)
  920. =/ y2 (montiply y (montiply y y))
  921. =/ y3 (montiply y (montiply y2 y2))
  922. =/ y5 (montiply y2 (montwop y3 2))
  923. =/ y10 (montiply y5 (montwop y5 5))
  924. =/ y20 (montiply y10 (montwop y10 10))
  925. =/ y30 (montiply y10 (montwop y20 10))
  926. =/ y31 (montiply y (montiply y30 y30))
  927. %- mont-reduction
  928. %+ montiply y
  929. =+ (montiply (montwop y31 32) y31)
  930. (montiply - -)
  931. ++ montwop
  932. |= [a=melt n=@]
  933. ^- melt
  934. ~+
  935. ?> (based a)
  936. ?: =(n 0)
  937. a
  938. $(a (montiply a a), n (sub n 1))
  939. --
  940. ::
  941. :: +bdiv: base field division
  942. ++ bdiv
  943. ~/ %bdiv
  944. |= [a=belt b=belt]
  945. ^- belt
  946. (bmul a (binv b))
  947. ::
  948. ++ ordered-root
  949. ~/ %ordered-root
  950. |= n=@
  951. ^- @
  952. ~+
  953. |^
  954. ?> (lte n (bex 32))
  955. ?> =((dis n (dec n)) 0) :: assert it's a power of two
  956. =/ log-of-n (dec (xeb n))
  957. ?> (lth log-of-n (lent roots))
  958. (snag log-of-n roots)
  959. ::
  960. :: precomputed roots matching the ROOTS array in belt.rs
  961. ++ roots
  962. ^- (list @)
  963. :~ 0x1 0xffff.ffff.0000.0000 0x1.0000.0000.0000 0xffff.fffe.ff00.0001
  964. 0xefff.ffff.0000.0001 0x3fff.ffff.c000 0x80.0000.0000 0xf800.07ff.0800.0001
  965. 0xbf79.143c.e60c.a966 0x1905.d02a.5c41.1f4e 0x9d8f.2ad7.8bfe.d972 0x653.b480.1da1.c8cf
  966. 0xf2c3.5199.959d.fcb6 0x1544.ef23.35d1.7997 0xe0ee.0993.10bb.a1e2 0xf6b2.cffe.2306.baac
  967. 0x54df.9630.bf79.450e 0xabd0.a6e8.aa3d.8a0e 0x8128.1a7b.05f9.beac 0xfbd4.1c6b.8caa.3302
  968. 0x30ba.2ecd.5e93.e76d 0xf502.aef5.3232.2654 0x4b2a.18ad.e672.46b5 0xea9d.5a13.36fb.c98b
  969. 0x86cd.cc31.c307.e171 0x4bba.f597.6ecf.efd8 0xed41.d05b.78d6.e286 0x10d7.8dd8.915a.171d
  970. 0x5904.9500.004a.4485 0xdfa8.c93b.a46d.2666 0x7e9b.d009.b86a.0845 0x400a.7f75.5588.e659
  971. 0x1856.29dc.da58.878c
  972. ==
  973. --
  974. ::
  975. :: +compute-size: computes the size in bits of a jammed noun
  976. ::
  977. ++ compute-size-jam
  978. |= n=*
  979. ^- @
  980. (met 0 (jam n))
  981. ::
  982. :: +compute-size-noun: computes the size in bits of a noun in unrolled form in the memory arena
  983. ::
  984. ++ compute-size-noun
  985. |= n=*
  986. ^- @
  987. |-
  988. ?@ n
  989. ?> (based n) :: check that atom is a belt
  990. 64
  991. (add 64 (add $(n -.n) $(n +.n)))
  992. ::
  993. +| %bpoly
  994. :: +bcan: gives the canonical leading-zero-stripped representation of p(x)
  995. ++ bcan
  996. |= p=poly
  997. ^- poly
  998. =. p (flop p)
  999. |-
  1000. ?~ p
  1001. :: TODO: fix this
  1002. ~[0]
  1003. ?: =(i.p 0)
  1004. $(p t.p)
  1005. (flop p)
  1006. ::
  1007. ::
  1008. :: +bdegree: computes the degree of a polynomial
  1009. ::
  1010. :: Not just (dec (lent p)) because we need to discard possible extraneous "leading zeroes"!
  1011. :: Be very careful in using lent vs. degree!
  1012. :: NOTE: degree(~) = 0 when it should really be -∞ to preserve degree(fg) = degree(f) +
  1013. :: degree(g). So if we use the RHS of this equation to compute the LHS the cases where
  1014. :: either are the zero polynomial must be handled separately.
  1015. ++ bdegree
  1016. |= p=poly
  1017. ^- @
  1018. =/ cp=poly (bcan p)
  1019. ?~ cp 0
  1020. (dec (lent cp))
  1021. ::
  1022. :: +bzero-extend: make the zero coefficients for powers of x higher than deg(p) explicit
  1023. ++ bzero-extend
  1024. |= [p=poly much=@]
  1025. ^- poly
  1026. (weld p (reap much 0))
  1027. ::
  1028. :: +binary-zero-extend: extend with zeroes until the length is the next power of 2
  1029. ++ bbinary-zero-extend
  1030. |= [p=poly]
  1031. ^- poly
  1032. ?~ p ~
  1033. =/ l=@ (lent p)
  1034. ?: =((dis l (dec l)) 0)
  1035. p
  1036. (bzero-extend p (sub (bex (xeb l)) l))
  1037. ::
  1038. :: +poly-to-map: takes list (a_i) and makes map i --> a_i
  1039. ++ poly-to-map
  1040. |= p=poly
  1041. ^- (map @ felt)
  1042. =| mp=(map @ felt)
  1043. =/ i=@ 0
  1044. |-
  1045. ?~ p
  1046. mp
  1047. $(mp (~(put by mp) i i.p), p t.p, i +(i))
  1048. ::
  1049. :: +map-to-poly: inverse of poly-to-map
  1050. ++ map-to-poly
  1051. :: keys need to be 0, 1, 2, ... which is enforced by "got" below
  1052. |= mp=(map @ felt)
  1053. ^- poly
  1054. =| p=poly
  1055. =/ size=@ ~(wyt by mp)
  1056. =/ i=@ size
  1057. |-
  1058. ?: =(i 0)
  1059. p
  1060. $(p [(~(got by mp) (dec i)) p], i (dec i))
  1061. ::
  1062. ++ bop ~(ops array-op 1)
  1063. ::
  1064. :: +init-bpoly: given a list of belts, create a bpoly representing it
  1065. ++ init-bpoly
  1066. ~/ %init-bpoly
  1067. |= poly=(list belt)
  1068. ^- bpoly
  1069. ?: =(~ poly)
  1070. zero-bpoly
  1071. ?> (lth (lent poly) (bex 32))
  1072. :- (lent poly)
  1073. =/ high-bit (lsh [0 (mul (bex 6) (lent poly))] 1)
  1074. (add (rep 6 poly) high-bit)
  1075. ::
  1076. ++ bpoly-to-list
  1077. ~/ %bpoly-to-list
  1078. |= bp=bpoly
  1079. ^- poly
  1080. ?> !=(len.bp 0)
  1081. (snip (rip 6 dat.bp))
  1082. ::
  1083. ::
  1084. ++ zero-bpoly ~+((init-bpoly ~[0]))
  1085. ++ one-bpoly ~+((init-bpoly ~[1]))
  1086. ++ id-bpoly
  1087. ~+
  1088. ^- bpoly
  1089. (init-bpoly ~[0 1])
  1090. ::
  1091. ++ bpcan
  1092. |= bp=bpoly
  1093. ^- bpoly
  1094. =/ p ~(to-poly bop bp)
  1095. (init-bpoly (bcan p))
  1096. ::
  1097. ::
  1098. ++ bp-is-zero
  1099. ~/ %bp-is-zero
  1100. |= p=bpoly
  1101. ^- ?
  1102. ~+
  1103. =. p (bpcan p)
  1104. |(=(len.p 0) =(p zero-bpoly))
  1105. ::
  1106. ::
  1107. ++ bp-is-one
  1108. ~/ %bp-is-one
  1109. |= p=bpoly
  1110. ^- ?
  1111. ~+
  1112. =. p (bpcan p)
  1113. &(=(len.p 1) =((~(snag bop p) 0) 1))
  1114. ::
  1115. :: +bpadd: base field polynomial addition
  1116. ++ bpadd
  1117. ~/ %bpadd
  1118. |: [bp=`bpoly`zero-bpoly bq=`bpoly`zero-bpoly]
  1119. ^- bpoly
  1120. ?> &(!=(len.bp 0) !=(len.bq 0))
  1121. =/ p (bpoly-to-list bp)
  1122. =/ q (bpoly-to-list bq)
  1123. =/ lp (lent p)
  1124. =/ lq (lent q)
  1125. =/ m (max lp lq)
  1126. =: p (weld p (reap (sub m lp) 0))
  1127. q (weld q (reap (sub m lq) 0))
  1128. ==
  1129. %- init-bpoly
  1130. (zip p q badd)
  1131. ::
  1132. :: +bpneg: additive inverse of a base field polynomial
  1133. ++ bpneg
  1134. ~/ %bpneg
  1135. |= bp=bpoly
  1136. ^- bpoly
  1137. ?> !=(len.bp 0)
  1138. =/ p (bpoly-to-list bp)
  1139. %- init-bpoly
  1140. (turn p bneg)
  1141. ::
  1142. :: +bpsub: field polynomial subtraction
  1143. ++ bpsub
  1144. ~/ %bpsub
  1145. |= [p=bpoly q=bpoly]
  1146. ^- bpoly
  1147. (bpadd p (bpneg q))
  1148. ::
  1149. :: bpscal: multiply base field scalar c by base field polynomial p
  1150. ++ bpscal
  1151. ~/ %bpscal
  1152. |= [c=belt bp=bpoly]
  1153. ^- bpoly
  1154. =/ p (bpoly-to-list bp)
  1155. %- init-bpoly
  1156. %+ turn p
  1157. (cury bmul c)
  1158. ::
  1159. :: +bpmul: base field polynomial multiplication; naive algorithm; necessary for fmul!
  1160. ++ bpmul
  1161. ~/ %bpmul
  1162. |: [bp=`bpoly`one-bpoly bq=`bpoly`one-bpoly]
  1163. ^- bpoly
  1164. ?> &(!=(len.bp 0) !=(len.bq 0))
  1165. %- init-bpoly
  1166. ?: ?|(=(bp zero-bpoly) =(bq zero-bpoly))
  1167. ~[0]
  1168. =/ p (bpoly-to-list bp)
  1169. =/ q (bpoly-to-list bq)
  1170. =/ v=(list melt)
  1171. %- weld
  1172. :_ (turn p montify)
  1173. (reap (dec (lent q)) 0)
  1174. =/ w=(list melt) (flop (turn q montify))
  1175. =| prod=poly
  1176. |-
  1177. ?~ v
  1178. (flop prod)
  1179. %= $
  1180. v t.v
  1181. ::
  1182. prod
  1183. :_ prod
  1184. %. [v w]
  1185. :: computes a "dot product" (actually a bilinear form that just looks like
  1186. :: one) of v and w by implicitly zero-extending if lengths unequal we
  1187. :: don't actually zero-extend to save a constant time factor
  1188. |= [v=(list melt) w=(list melt)]
  1189. ^- melt
  1190. =| dot=belt
  1191. |-
  1192. ?: ?|(?=(~ v) ?=(~ w))
  1193. (mont-reduction dot)
  1194. $(v t.v, w t.w, dot (badd dot (montiply i.v i.w)))
  1195. ==
  1196. ::
  1197. :: +bp-hadamard
  1198. ::
  1199. :: Hadamard product of two bpolys. This is just a fancy name for pointwise multiplication.
  1200. ++ bp-hadamard
  1201. ~/ %bp-hadamard
  1202. |: [bp=`bpoly`one-bpoly bq=`bpoly`one-bpoly]
  1203. ^- bpoly
  1204. ?> =(len.bp len.bq)
  1205. ?: |(=(len.bp 0) =(len.bq 0)) zero-bpoly
  1206. (~(zip bop bp) bq bmul)
  1207. ::
  1208. ::
  1209. :: +bpdvr: base field polynomial division with remainder
  1210. ::
  1211. :: Analogous to integer division: (bpdvr a b) = [q r] where a = bq + r and degree(r)
  1212. :: < degree(b). (Using the mathematical degree where degree(~) = -∞.)
  1213. :: This implies q and r are unique.
  1214. ::
  1215. :: Algorithm is the usual one taught in high school.
  1216. ++ bpdvr
  1217. ~/ %bpdvr
  1218. |: [ba=`bpoly`one-bpoly bb=`bpoly`one-bpoly]
  1219. ^- [q=bpoly r=bpoly]
  1220. ?> &(!=(len.ba 0) !=(len.bb 0))
  1221. =/ a (bpoly-to-list ba)
  1222. =/ b (bpoly-to-list bb)
  1223. :: rem = remainder; a is effectively first candidate since (degree a) < (degree b) => done
  1224. :: rem, b are written high powers to low, as in high school algorithm
  1225. =^ rem b
  1226. :- (flop (bcan a))
  1227. (flop (bcan b))
  1228. ~| "Cannot divide by the zero polynomial."
  1229. ?< ?=(~ b)
  1230. =/ db (dec (lent b))
  1231. :: db = 0, rem = ~ => condition below this one is false and we fail the subsequent assertion;
  1232. :: Problem is (degree ~) = 0 is wrong mathematically; so we simply handle db = 0 separately.
  1233. ?: =(db 0)
  1234. :_ zero-bpoly
  1235. (bpscal (binv i.b) ba)
  1236. :: coeff = next coefficient added to the quotient, starting with highest power
  1237. =| coeff=belt
  1238. =| quot=poly
  1239. |-
  1240. ?: (lth (bdegree (flop rem)) db)
  1241. :- (init-bpoly quot)
  1242. (init-bpoly (bcan (flop rem)))
  1243. ?< ?=(~ rem)
  1244. =/ new-coeff (bdiv i.rem i.b)
  1245. =/ new-rem
  1246. %- bpoly-to-list
  1247. (bpsub (init-bpoly rem) (bpscal new-coeff (init-bpoly b)))
  1248. ?< ?=(~ new-rem)
  1249. %= $
  1250. coeff new-coeff
  1251. quot [new-coeff quot]
  1252. rem t.new-rem
  1253. ==
  1254. ::
  1255. :: +bpdiv: a/b for base field polynomials; q component of bpdvr
  1256. ++ bpdiv
  1257. ~/ %bpdiv
  1258. |= [a=bpoly b=bpoly]
  1259. ^- bpoly
  1260. q:(bpdvr a b)
  1261. ::
  1262. :: +bppow:: bppow: compute (p(x))^k
  1263. ++ bppow
  1264. ~/ %bppow
  1265. |= [bp=bpoly k=@]
  1266. ^- bpoly
  1267. ~+
  1268. ?> !=(len.bp 0)
  1269. %. [(init-bpoly ~[1]) bp k]
  1270. |= [q=bpoly p=bpoly k=@]
  1271. ?: =(k 0)
  1272. q
  1273. =/ f=@ (end 0 k)
  1274. ?: =(f 0)
  1275. %_ $
  1276. p (bpmul p p)
  1277. k (rsh 0 k)
  1278. ==
  1279. %_ $
  1280. q (bpmul q p)
  1281. p (bpmul p p)
  1282. k (rsh 0 k)
  1283. ==
  1284. ::
  1285. ::
  1286. :: +bpmod: a mod b for base field polynomials; r component of bpdvr
  1287. ++ bpmod
  1288. ~/ %bpmod
  1289. |= [a=bpoly b=bpoly]
  1290. ^- bpoly
  1291. r:(bpdvr a b)
  1292. ::
  1293. :: +bpegcd: base field polynomial extended Euclidean algorithm
  1294. ::
  1295. :: Gives gcd = d and u, v such that d = ua + vb from the Euclidean algorithm.
  1296. :: The algorithm is based on repeatedly dividing-with-remainder: a = bq + r,
  1297. :: b = rq_1 + r_1, etc. since gcd(a, b) = gcd(b, r) = ... (exercise) etc. The
  1298. :: pairs being divided in sequence are (a, b), (b, r), (r, r_1), etc. with update
  1299. :: rule new_first = old_second, new_second = remainder upon division of old_first
  1300. :: and old_second. One stops when a division by 0 would be necessary to generate
  1301. :: new_second, and then d = gcd is the second of the last full pair generated.
  1302. :: To see that u and v exist, repeatedly write d in terms of earlier and earlier
  1303. :: dividing pairs. To progressively generate the correct u, v, reexamine the original
  1304. :: calculation and write the remainders in terms of a, b at each step. Since each
  1305. :: remainder depends on the previous two, the same is true of u and v. This is the
  1306. :: reason for e.g. m1.u, which semantically is `u at time minus 1`; one can verify
  1307. :: the given initialization of these quantities.
  1308. :: NOTE: mathematically, gcd is not unique (only up to a scalar).
  1309. ++ bpegcd
  1310. ~/ %bpegcd
  1311. |= [a=bpoly b=bpoly]
  1312. ^- [d=bpoly u=bpoly v=bpoly]
  1313. =/ [u=[m1=bpoly m2=bpoly] v=[m1=bpoly m2=bpoly]]
  1314. :- zero-bpoly^one-bpoly
  1315. one-bpoly^zero-bpoly
  1316. |-
  1317. ?: =((bcan (bpoly-to-list b)) ~[0])
  1318. :+ (init-bpoly (bcan (bpoly-to-list a)))
  1319. (init-bpoly (bcan (bpoly-to-list m2.u)))
  1320. (init-bpoly (bcan (bpoly-to-list m2.v)))
  1321. =/ q-r (bpdvr a b)
  1322. %= $
  1323. a b
  1324. b r:q-r
  1325. u [(bpsub m2.u (bpmul q:q-r m1.u)) m1.u]
  1326. v [(bpsub m2.v (bpmul q:q-r m1.v)) m1.v]
  1327. ==
  1328. ::
  1329. :: +bpeval: evaluate a bpoly at a belt
  1330. ++ bpeval
  1331. ~/ %bpeval
  1332. |: [bp=`bpoly`one-bpoly x=`belt`1]
  1333. ^- belt
  1334. ~+
  1335. ?: (bp-is-zero bp) 0
  1336. ?: =(len.bp 1) (~(snag bop bp) 0)
  1337. =/ p ~(to-poly bop bp)
  1338. =. p (flop p)
  1339. =/ res=@ 0
  1340. |-
  1341. ?~ p !!
  1342. ?~ t.p
  1343. (badd (bmul res x) i.p)
  1344. :: based on p(x) = (...((a_n)x + a_{n-1})x + a_{n-2})x + ... )
  1345. $(res (badd (bmul res x) i.p), p t.p)
  1346. ::
  1347. :: construct the constant bpoly f(X)=c
  1348. ++ bp-c
  1349. |= c=belt
  1350. ^- bpoly
  1351. ~+
  1352. (init-bpoly ~[c])
  1353. ::
  1354. :: +bp-decompose
  1355. ::
  1356. :: given a polynomial f(X) of degree at most D*N, decompose into D polynomials
  1357. :: {h_i(X) : 0 <= i < D} each of degree at most N such that
  1358. ::
  1359. :: f(X) = h_0(X^D) + X*h_1(X^D) + X^2*h_2(X^D) + ... + X^{D-1}*h_{D-1}(X^D)
  1360. ::
  1361. :: This is just a generalization of splitting a polynomial into even and odd terms
  1362. :: as the FFT does.
  1363. :: h_i(X) is the terms whose degree is congruent to i modulo D.
  1364. ::
  1365. :: Passing in d=2 will split into even and odd terms.
  1366. ::
  1367. ++ bp-decompose
  1368. ~/ %bp-decompose
  1369. |= [p=bpoly d=@]
  1370. ^- (list bpoly)
  1371. =/ total-deg=@ (bdegree (bpoly-to-list p))
  1372. =/ deg=@
  1373. =/ dvr (dvr total-deg d)
  1374. ?:(=(q.dvr 0) p.dvr (add p.dvr 1))
  1375. =/ acc=(list (list belt)) (reap d ~)
  1376. =-
  1377. %+ turn -
  1378. |= poly=(list belt)
  1379. ?~ poly zero-bpoly
  1380. (init-bpoly (flop poly))
  1381. %+ roll (range (add 1 deg))
  1382. |= [n=@ acc=_acc]
  1383. %+ iturn acc
  1384. |= [i=@ l=(list belt)]
  1385. =/ idx (add (mul n d) i)
  1386. ?: (gth idx total-deg) l
  1387. [(~(snag bop p) idx) l]
  1388. --