one.hoon 35 KB

12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697989910010110210310410510610710810911011111211311411511611711811912012112212312412512612712812913013113213313413513613713813914014114214314414514614714814915015115215315415515615715815916016116216316416516616716816917017117217317417517617717817918018118218318418518618718818919019119219319419519619719819920020120220320420520620720820921021121221321421521621721821922022122222322422522622722822923023123223323423523623723823924024124224324424524624724824925025125225325425525625725825926026126226326426526626726826927027127227327427527627727827928028128228328428528628728828929029129229329429529629729829930030130230330430530630730830931031131231331431531631731831932032132232332432532632732832933033133233333433533633733833934034134234334434534634734834935035135235335435535635735835936036136236336436536636736836937037137237337437537637737837938038138238338438538638738838939039139239339439539639739839940040140240340440540640740840941041141241341441541641741841942042142242342442542642742842943043143243343443543643743843944044144244344444544644744844945045145245345445545645745845946046146246346446546646746846947047147247347447547647747847948048148248348448548648748848949049149249349449549649749849950050150250350450550650750850951051151251351451551651751851952052152252352452552652752852953053153253353453553653753853954054154254354454554654754854955055155255355455555655755855956056156256356456556656756856957057157257357457557657757857958058158258358458558658758858959059159259359459559659759859960060160260360460560660760860961061161261361461561661761861962062162262362462562662762862963063163263363463563663763863964064164264364464564664764864965065165265365465565665765865966066166266366466566666766866967067167267367467567667767867968068168268368468568668768868969069169269369469569669769869970070170270370470570670770870971071171271371471571671771871972072172272372472572672772872973073173273373473573673773873974074174274374474574674774874975075175275375475575675775875976076176276376476576676776876977077177277377477577677777877978078178278378478578678778878979079179279379479579679779879980080180280380480580680780880981081181281381481581681781881982082182282382482582682782882983083183283383483583683783883984084184284384484584684784884985085185285385485585685785885986086186286386486586686786886987087187287387487587687787887988088188288388488588688788888989089189289389489589689789889990090190290390490590690790890991091191291391491591691791891992092192292392492592692792892993093193293393493593693793893994094194294394494594694794894995095195295395495595695795895996096196296396496596696796896997097197297397497597697797897998098198298398498598698798898999099199299399499599699799899910001001100210031004100510061007100810091010101110121013101410151016101710181019102010211022102310241025102610271028102910301031103210331034103510361037103810391040104110421043104410451046104710481049105010511052105310541055105610571058105910601061106210631064106510661067106810691070107110721073107410751076107710781079108010811082108310841085108610871088108910901091109210931094109510961097109810991100110111021103110411051106110711081109111011111112111311141115111611171118111911201121112211231124112511261127112811291130113111321133113411351136113711381139114011411142114311441145114611471148114911501151115211531154115511561157115811591160116111621163116411651166116711681169117011711172117311741175117611771178117911801181118211831184118511861187118811891190119111921193119411951196119711981199120012011202120312041205120612071208120912101211121212131214121512161217121812191220122112221223122412251226122712281229123012311232123312341235123612371238123912401241124212431244124512461247124812491250125112521253125412551256125712581259126012611262126312641265126612671268126912701271127212731274127512761277127812791280128112821283128412851286128712881289129012911292129312941295129612971298129913001301130213031304130513061307130813091310131113121313131413151316131713181319132013211322132313241325132613271328132913301331133213331334133513361337133813391340134113421343134413451346134713481349135013511352135313541355135613571358135913601361136213631364136513661367136813691370137113721373
  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. ?> (~(fet mary-utils step.ma) j)
  403. :- step.ma
  404. :- +(len.array.ma)
  405. =/ new-high-bit (lsh [0 (mul (bex 6) (mul step.ma +(len.array.ma)))] 1)
  406. =/ old-high-bit (lsh [0 (mul (bex 6) (mul step.ma len.array.ma))] 1)
  407. %^ sew 6
  408. [(mul len.array.ma step.ma) step.ma j]
  409. (sub (add new-high-bit dat.array.ma) old-high-bit)
  410. ::
  411. ++ weld-step
  412. ~/ %weld-step
  413. |= na=mary
  414. ^- mary
  415. ?> =(len.array.ma len.array.na)
  416. %+ roll (range len.array.na)
  417. =/ mu=mary
  418. :+ (add step.ma step.na)
  419. len.array.ma
  420. (lsh [6 (mul (add step.ma step.na) len.array.ma)] 1)
  421. |= [i=@ mu=_mu]
  422. =; weld-dat
  423. (~(stow ave mu) i weld-dat)
  424. =/ r1 (snag i)
  425. =? r1 !=(step.ma 1)
  426. (sub r1 (lsh [6 step.ma] 1))
  427. =/ r2 (~(snag ave na) i)
  428. =? r2 !=(step.na 1)
  429. (add (lsh [6 step.na] 1) r2)
  430. (add (lsh [6 step.ma] r2) r1)
  431. ::
  432. ++ stow
  433. ~/ %stow
  434. |= [i=@ j=elt]
  435. ^- mary
  436. ?> (~(fet mary-utils step.ma) j)
  437. ?> (lth i len.array.ma)
  438. =/ item
  439. ?: =(step.ma 1)
  440. j
  441. (rep 6 (snip (rip 6 j)))
  442. [step.ma len.array.ma (sew 6 [(mul i step.ma) step.ma item] dat.array.ma)]
  443. ::
  444. ++ change-step
  445. ~/ %change-step
  446. |= [new-step=@]
  447. ^- mary
  448. ?: =(step.ma new-step) ma
  449. ?> =((mod (mul step.ma len.array.ma) new-step) 0)
  450. :+ new-step
  451. (div (mul step.ma len.array.ma) new-step)
  452. dat.array.ma
  453. ::
  454. ++ to-poly
  455. ^- poly
  456. (mary-to-list ma)
  457. ::
  458. ++ transpose
  459. ~/ %transpose
  460. |= offset=@
  461. ^- mary
  462. =/ res-step (mul len.array.ma offset)
  463. =/ res-len (div step.ma offset)
  464. =/ res=mary [res-step [res-len (lsh [6 (mul res-step res-len)] 1)]]
  465. =/ num-cols res-len
  466. =/ num-rows len.array.ma
  467. %+ roll (range num-cols)
  468. |= [i=@ m=_res]
  469. %+ roll (range num-rows)
  470. |= [j=@ m=_m]
  471. =/ target-index (add (mul i num-rows) j)
  472. ::
  473. =/ source (cut 6 [(mul offset (add (mul j num-cols) i)) offset] dat.array.ma)
  474. m(dat.array (sew 6 [(mul offset target-index) offset source] dat.array.m))
  475. ::
  476. :: check if len matches the actual size of dat
  477. ++ chck
  478. ^- ?
  479. =((mul step.ma len.array.ma) (dec (met 6 dat.array.ma)))
  480. -- :: ave
  481. ::
  482. ++ transpose-fpolys
  483. |= fpolys=mary
  484. ^- mary
  485. (~(transpose ave fpolys) 3)
  486. ::
  487. ++ transpose-bpolys
  488. |= bpolys=mary
  489. ^- mary
  490. (~(transpose ave bpolys) 1)
  491. ::
  492. ++ array-op
  493. ~/ %array-op
  494. |_ step=@
  495. ::
  496. ++ ops
  497. =| fp=array
  498. ~/ %ops
  499. |%
  500. ++ op ~(. ave [step fp])
  501. ++ flop
  502. ^- fpoly
  503. array:flop:op
  504. ++ zip
  505. ~/ %zip
  506. |= [gp=fpoly a=$-([felt felt] felt)]
  507. ^- fpoly
  508. array:(zip:op [step gp] a)
  509. ::
  510. ++ zero-extend
  511. ~/ %zero-extend
  512. |= n=@
  513. array:(zero-extend:op n)
  514. ::
  515. ++ weld
  516. ~/ %weld
  517. |= fp2=fpoly
  518. ^- fpoly
  519. array:(weld:op [step fp2])
  520. ::
  521. ++ head
  522. ^- felt
  523. (snag 0)
  524. ::
  525. ++ rear
  526. ^- felt
  527. (snag (dec len.fp))
  528. ::
  529. ++ snag
  530. ~/ %snag
  531. |= i=@
  532. ^- felt
  533. (snag:op i)
  534. ::
  535. ++ scag
  536. ~/ %scag
  537. |= i=@
  538. ^- fpoly
  539. array:(scag:op i)
  540. ::
  541. ++ slag
  542. ~/ %slag
  543. |= i=@
  544. ^- fpoly
  545. array:(slag:op i)
  546. ::
  547. ++ swag
  548. ~/ %swag
  549. |= [i=@ j=@]
  550. ^- fpoly
  551. array:(swag:op i j)
  552. ::
  553. ++ snoc
  554. ~/ %snoc
  555. |= j=felt
  556. ^- fpoly
  557. array:(snoc:op j)
  558. ::
  559. ++ stow
  560. ~/ %stow
  561. |= [i=@ j=felt]
  562. ^- fpoly
  563. array:(stow:op i j)
  564. ::
  565. ++ to-poly
  566. ^- poly
  567. (mary-to-list [step fp])
  568. ::
  569. ++ chck
  570. ^- ?
  571. chck:op
  572. --
  573. --
  574. ::
  575. :: turn a 1-dimensional array into a 1-element 2-dimensional array
  576. ++ lift-mop
  577. |= fp=fpoly
  578. ^- mary
  579. [(mul 3 len.fp) 1 dat.fp]
  580. ::
  581. :: +fpoly-to-mary
  582. ::
  583. :: View an fpoly as a 3-step mary.
  584. ::
  585. :: Note that +fpoly-to-marry just views the fpoly as an mary. It has the same length
  586. :: and each element is a felt. +lift-mop on the other hand turns the fpoly into an array
  587. :: of fpolys which has step=len.fpoly and contains exactly one element- the fpoly passed in.
  588. ::
  589. ++ fpoly-to-mary
  590. |= fp=fpoly
  591. ^- mary
  592. [3 fp]
  593. ::
  594. :: +bpoly-to-mary: view a bpoly as 1-step mary
  595. ++ bpoly-to-mary
  596. |= bp=bpoly
  597. ^- mary
  598. [1 bp]
  599. ::
  600. :: +i: reverse index lookup:
  601. ::
  602. :: given an item and a list,
  603. :: produce the index of the item in the list
  604. ++ i
  605. ~+
  606. |= [item=@tas lis=(list @tas)]
  607. ::TODO make this wet
  608. ^- @
  609. (need (find ~[item] lis))
  610. ::
  611. ++ zip-up
  612. ~/ %zip-up
  613. |* [p=(list) q=(list)]
  614. ^- (list _?>(?&(?=(^ p) ?=(^ q)) [i.p i.q]))
  615. (zip p q same)
  616. ::
  617. ++ zip
  618. ~/ %zip
  619. |* [p=(list) q=(list) r=gate]
  620. ^- (list _?>(?&(?=(^ p) ?=(^ q)) (r i.p i.q)))
  621. |-
  622. ?: ?&(?=(~ p) ?=(~ q))
  623. ~
  624. ?. ?&(?=(^ p) ?=(^ q)) ~|(%zip-fail-unequal-lengths !!)
  625. [i=(r i.p i.q) t=$(p t.p, q t.q)]
  626. ::
  627. ++ sum
  628. ~/ %sum
  629. |= lis=(list @)
  630. ^- @
  631. %+ roll lis
  632. |= [a=@ r=@]
  633. (add a r)
  634. ::
  635. ++ mul-all
  636. ~/ %mul-all
  637. |= [lis=(list @) x=@]
  638. ^- (list @)
  639. %+ turn lis
  640. |=(a=@ (mul a x))
  641. ::
  642. ++ add-all
  643. ~/ %add-all
  644. |= [lis=(list @) x=@]
  645. ^- (list @)
  646. %+ turn lis
  647. |=(a=@ (add a x))
  648. ::
  649. ++ mod-all
  650. ~/ %mod-all
  651. |= [lis=(list @) x=@]
  652. ^- (list @)
  653. %+ turn lis
  654. |=(a=@ (mod a x))
  655. ::
  656. ++ zip-roll
  657. ~/ %zip-roll
  658. |* [p=(list) q=(list) r=_=>(~ |=([[* *] *] +<+))]
  659. |- ^+ ,.+<+.r
  660. ?~ p
  661. ?~ q
  662. +<+.r
  663. !!
  664. ?. ?=(^ q) ~|(%zip-roll-fail-unequal-lengths !!)
  665. $(p t.p, q t.q, r r(+<+ (r [i.p i.q] +<+.r)))
  666. ::
  667. ++ range
  668. ~/ %range
  669. |= $@(@ ?(@ (pair @ @)))
  670. ^- (list @)
  671. ?@ +< ?~(+< ~ (gulf 0 (dec +<)))
  672. (gulf p (dec q))
  673. ::
  674. :: +mevy: maybe error levy
  675. ::
  676. ++ mevy
  677. :: ~ if no failures or (some err) of the first error encountered
  678. ~/ %mevy
  679. |* [a=(list) b=$-(* (unit))]
  680. =* b-product _?>(?=(^ a) (b i.a))
  681. |- ^- b-product
  682. ?~ a ~
  683. ?^ err=(b i.a) err
  684. $(a t.a)
  685. ::
  686. :: +iturn: indexed turn. Gate gets a 0-based index of which list element it is on.
  687. ++ iturn
  688. ~/ %iturn
  689. |* [a=(list) b=_|=([@ *] +<+)]
  690. ^- (list _?>(?=(^ a) (b i.a)))
  691. =/ n 0
  692. |-
  693. ?~ a ~
  694. [i=(b [n i.a]) t=$(a t.a, n +(n))]
  695. ::
  696. :: +median: computes the median value of a (list @)
  697. ::
  698. :: if the length of the list is odd, its the middle value. if its
  699. :: even, we average the two middle values (rounding down)
  700. ++ median
  701. ~/ %median
  702. |= xs=(list @)
  703. ^- @
  704. =/ len=@ (lent xs)
  705. =/ parity=@ (mod (lent xs) 2)
  706. =/ sorted=(list @) (sort xs lth)
  707. |-
  708. ?~ sorted ~|("median of empty list" !!)
  709. ::TODO why do i need to cast to (list @) everywhere?
  710. ?: ?& =(parity 0) :: even case
  711. =(len 2) :: 2 elements remain
  712. ==
  713. %- div
  714. :_ 2
  715. %+ add (snag 0 `(list @)`sorted)
  716. (snag 1 `(list @)`sorted)
  717. ?: ?& =(parity 1) :: odd case
  718. =(len 1) :: 1 element remains
  719. ==
  720. (snag 0 `(list @)`sorted)
  721. :: otherwise, remove first and last element and repeat
  722. %_ $
  723. sorted (snip (slag 1 `(list @)`sorted))
  724. len (dec (dec len))
  725. ==
  726. ::
  727. :: clev: cleave a list into a list of lists w specified sizes (unless list is exhausted)
  728. :: TODO: could be made wet wrt a
  729. ++ clev
  730. |= [a=(list @) sizes=(list @)]
  731. ^- (list (list @))
  732. =- (flop acc)
  733. %+ roll sizes
  734. |= [s=@ a=_a acc=(list (list @))]
  735. :- (slag s a)
  736. [(scag s a) acc]
  737. ::
  738. ::
  739. +| %base58
  740. ++ en-base58
  741. |= dat=@
  742. =/ cha
  743. '123456789ABCDEFGHJKLMNPQRSTUVWXYZabcdefghijkmnopqrstuvwxyz'
  744. %- flop
  745. |- ^- tape
  746. ?: =(0 dat) ~
  747. :- (cut 3 [(mod dat 58) 1] cha)
  748. $(dat (div dat 58))
  749. ::
  750. ++ de-base58
  751. |= t=tape
  752. =- (scan t (bass 58 (plus -)))
  753. ;~ pose
  754. (cook |=(a=@ (sub a 56)) (shim 'A' 'H'))
  755. (cook |=(a=@ (sub a 57)) (shim 'J' 'N'))
  756. (cook |=(a=@ (sub a 58)) (shim 'P' 'Z'))
  757. (cook |=(a=@ (sub a 64)) (shim 'a' 'k'))
  758. (cook |=(a=@ (sub a 65)) (shim 'm' 'z'))
  759. (cook |=(a=@ (sub a 49)) (shim '1' '9'))
  760. ==
  761. ::
  762. +| %constants
  763. :: +p: field characteristic p = 2^64 - 2^32 + 1 = (2^32)*3*5*17*257*65537 + 1
  764. :: +r: radix r = 2^64
  765. :: +r-mod-p: r-mod-p = r - p
  766. :: +r2: r^2 mod p = (2^32 - 1)^2 = 2^64 - 2*2^32 + 1 = p - 2^32
  767. :: +rp: r*p
  768. :: +g: ord(g) = p - 1, i.e. g generates the (multiplicative group of the) field
  769. :: +h: ord(h) = 2^32, i.e. h = (2^32)th root of unity
  770. ++ p 0xffff.ffff.0000.0001
  771. ++ r 0x1.0000.0000.0000.0000
  772. ++ r-mod-p 4.294.967.295
  773. ++ r2 0xffff.fffe.0000.0001
  774. ++ rp 0xffff.ffff.0000.0001.0000.0000.0000.0000
  775. ++ g 7
  776. ++ h 20.033.703.337
  777. +| %base-field
  778. :: +based: in base field?
  779. ++ based
  780. ~/ %based
  781. |= a=@
  782. ^- ?
  783. (lth a p)
  784. ::
  785. :: is this noun based
  786. ++ based-noun
  787. ~/ %based-noun
  788. |= n=*
  789. ^- ?
  790. ?@ n
  791. (based n)
  792. &($(n -.n) $(n +.n))
  793. ::
  794. :: +badd: base field addition
  795. ++ badd
  796. ~/ %badd
  797. |= [a=belt b=belt]
  798. ^- belt
  799. ?> ?&((based a) (based b))
  800. (mod (add a b) p)
  801. ::
  802. :: +bneg: base field negation
  803. ++ bneg
  804. ~/ %bneg
  805. |= a=belt
  806. ^- belt
  807. ?> (based a)
  808. ?: =(a 0)
  809. 0
  810. (sub p a)
  811. ::
  812. :: +bsub: base field subtraction
  813. ++ bsub
  814. ~/ %bsub
  815. |= [a=belt b=belt]
  816. ^- belt
  817. (badd a (bneg b))
  818. ::
  819. :: +bmul: base field multiplication
  820. ++ bmul
  821. ~/ %bmul
  822. |= [a=belt b=belt]
  823. ^- belt
  824. ?> ?&((based a) (based b))
  825. (mod (mul a b) p)
  826. ::
  827. :: +bmix: binary XOR mod p
  828. ++ bmix
  829. ~/ %bmix
  830. |= [a=@ b=@]
  831. ^- @
  832. (mod (mix a b) p)
  833. ::
  834. :: +mont-reduction: special algorithm; computes x•r^{-1} = (xr^{-1} mod p).
  835. ::
  836. :: Note this is the inverse of x --> r•x, so conceptually this is a map from
  837. :: Montgomery space to the base field.
  838. ::
  839. :: It's `special` bc we gain efficiency by examining the general algo by hand
  840. :: and deducing the form of the final answer, which we can code directly.
  841. :: If you compute the algo by hand you will find it convenient to write
  842. :: x = x_2*2^64 + x_1*2^32 + x_0 where x_2 is a 64-bit number less than
  843. :: p (so x < pr) and x_1, x_0 are 32-bit numbers.
  844. :: The formula comes, basically, to (x_2 - (2^32(x_0 + x_1) - x_1 - f*p));
  845. :: f is a flag bit for the overflow of 2^32(x_0 + x_1) past 64 bits.
  846. :: "Basically" means we have to add p if the formula is negative.
  847. ++ mont-reduction
  848. ~/ %mont-reduction
  849. |= x=melt
  850. ^- belt
  851. ?> (lth x rp)
  852. =/ x1 (cut 5 [1 1] x)
  853. =/ x2 (rsh 6 x)
  854. =/ c
  855. =/ x0 (end 5 x)
  856. (lsh 5 (add x0 x1))
  857. =/ f (rsh 6 c)
  858. =/ d (sub c (add x1 (mul f p)))
  859. ?: (gte x2 d)
  860. (sub x2 d)
  861. (sub (add x2 p) d)
  862. ::
  863. :: +montiply: computes a*b = (abr^{-1} mod p); note mul, not fmul: avoids mod p reduction!
  864. ++ montiply
  865. ~/ %montiply
  866. |: [a=`melt`r-mod-p b=`melt`r-mod-p]
  867. ^- belt
  868. ~+
  869. ?> ?&((based a) (based b))
  870. (mont-reduction (mul a b))
  871. ::
  872. :: +montify: transform to Montgomery space, i.e. compute x•r = xr mod p
  873. ++ montify
  874. ~/ %montify
  875. |= x=belt
  876. ^- melt
  877. ~+
  878. (montiply x r2)
  879. ::
  880. :: +bpow: fast modular exponentiation using x^n mod p = 1*(xr)*...*(xr)
  881. ++ bpow
  882. ~/ %bpow
  883. |= [x=belt n=@]
  884. ^- belt
  885. ?> (based x)
  886. ~+
  887. %. [1 (montify x) n]
  888. |= [y=melt x=melt n=@]
  889. ^- melt
  890. ?: =(n 0)
  891. y
  892. :: parity flag
  893. =/ f=@ (end 0 n)
  894. ?: =(0 f)
  895. $(x (montiply x x), n (rsh 0 n))
  896. $(y (montiply y x), x (montiply x x), n (rsh 0 n))
  897. ::
  898. :: +binv: base field multiplicative inversion
  899. ++ binv
  900. ~/ %binv
  901. |= x=belt
  902. ^- belt
  903. ~+
  904. |^
  905. ~| "x not in field"
  906. ?> (based x)
  907. ~| "cannot divide by 0"
  908. ?< =(x 0)
  909. =/ y=melt (montify x)
  910. =/ y2 (montiply y (montiply y y))
  911. =/ y3 (montiply y (montiply y2 y2))
  912. =/ y5 (montiply y2 (montwop y3 2))
  913. =/ y10 (montiply y5 (montwop y5 5))
  914. =/ y20 (montiply y10 (montwop y10 10))
  915. =/ y30 (montiply y10 (montwop y20 10))
  916. =/ y31 (montiply y (montiply y30 y30))
  917. %- mont-reduction
  918. %+ montiply y
  919. =+ (montiply (montwop y31 32) y31)
  920. (montiply - -)
  921. ++ montwop
  922. |= [a=melt n=@]
  923. ^- melt
  924. ~+
  925. ?> (based a)
  926. ?: =(n 0)
  927. a
  928. $(a (montiply a a), n (sub n 1))
  929. --
  930. ::
  931. :: +bdiv: base field division
  932. ++ bdiv
  933. ~/ %bdiv
  934. |= [a=belt b=belt]
  935. ^- belt
  936. (bmul a (binv b))
  937. ::
  938. ++ ordered-root
  939. ~/ %ordered-root
  940. |= n=@
  941. ^- @
  942. ~+
  943. |^
  944. ?> (lte n (bex 32))
  945. ?> =((dis n (dec n)) 0) :: assert it's a power of two
  946. =/ log-of-n (dec (xeb n))
  947. ?> (lth log-of-n (lent roots))
  948. (snag log-of-n roots)
  949. ::
  950. :: precomputed roots matching the ROOTS array in belt.rs
  951. ++ roots
  952. ^- (list @)
  953. :~ 0x1 0xffff.ffff.0000.0000 0x1.0000.0000.0000 0xffff.fffe.ff00.0001
  954. 0xefff.ffff.0000.0001 0x3fff.ffff.c000 0x80.0000.0000 0xf800.07ff.0800.0001
  955. 0xbf79.143c.e60c.a966 0x1905.d02a.5c41.1f4e 0x9d8f.2ad7.8bfe.d972 0x653.b480.1da1.c8cf
  956. 0xf2c3.5199.959d.fcb6 0x1544.ef23.35d1.7997 0xe0ee.0993.10bb.a1e2 0xf6b2.cffe.2306.baac
  957. 0x54df.9630.bf79.450e 0xabd0.a6e8.aa3d.8a0e 0x8128.1a7b.05f9.beac 0xfbd4.1c6b.8caa.3302
  958. 0x30ba.2ecd.5e93.e76d 0xf502.aef5.3232.2654 0x4b2a.18ad.e672.46b5 0xea9d.5a13.36fb.c98b
  959. 0x86cd.cc31.c307.e171 0x4bba.f597.6ecf.efd8 0xed41.d05b.78d6.e286 0x10d7.8dd8.915a.171d
  960. 0x5904.9500.004a.4485 0xdfa8.c93b.a46d.2666 0x7e9b.d009.b86a.0845 0x400a.7f75.5588.e659
  961. 0x1856.29dc.da58.878c
  962. ==
  963. --
  964. ::
  965. :: +compute-size: computes the size in bits of a jammed noun consisting of belts
  966. ::
  967. :: this is a shortcut to actually jamming a noun and counting the bits.
  968. ::TODO can this be made tail call optimized?
  969. ++ compute-size-belt-noun
  970. |= n=*
  971. ^- @
  972. |-
  973. ?@ n
  974. ?> (based n) :: check that atom is a belt
  975. p:(mat n)
  976. (add 2 (add $(n -.n) $(n +.n))) :: 2 bits per cell
  977. ::
  978. +| %bpoly
  979. :: +bcan: gives the canonical leading-zero-stripped representation of p(x)
  980. ++ bcan
  981. |= p=poly
  982. ^- poly
  983. =. p (flop p)
  984. |-
  985. ?~ p
  986. :: TODO: fix this
  987. ~[0]
  988. ?: =(i.p 0)
  989. $(p t.p)
  990. (flop p)
  991. ::
  992. ::
  993. :: +bdegree: computes the degree of a polynomial
  994. ::
  995. :: Not just (dec (lent p)) because we need to discard possible extraneous "leading zeroes"!
  996. :: Be very careful in using lent vs. degree!
  997. :: NOTE: degree(~) = 0 when it should really be -∞ to preserve degree(fg) = degree(f) +
  998. :: degree(g). So if we use the RHS of this equation to compute the LHS the cases where
  999. :: either are the zero polynomial must be handled separately.
  1000. ++ bdegree
  1001. |= p=poly
  1002. ^- @
  1003. =/ cp=poly (bcan p)
  1004. ?~ cp 0
  1005. (dec (lent cp))
  1006. ::
  1007. :: +bzero-extend: make the zero coefficients for powers of x higher than deg(p) explicit
  1008. ++ bzero-extend
  1009. |= [p=poly much=@]
  1010. ^- poly
  1011. (weld p (reap much 0))
  1012. ::
  1013. :: +binary-zero-extend: extend with zeroes until the length is the next power of 2
  1014. ++ bbinary-zero-extend
  1015. |= [p=poly]
  1016. ^- poly
  1017. ?~ p ~
  1018. =/ l=@ (lent p)
  1019. ?: =((dis l (dec l)) 0)
  1020. p
  1021. (bzero-extend p (sub (bex (xeb l)) l))
  1022. ::
  1023. :: +poly-to-map: takes list (a_i) and makes map i --> a_i
  1024. ++ poly-to-map
  1025. |= p=poly
  1026. ^- (map @ felt)
  1027. =| mp=(map @ felt)
  1028. =/ i=@ 0
  1029. |-
  1030. ?~ p
  1031. mp
  1032. $(mp (~(put by mp) i i.p), p t.p, i +(i))
  1033. ::
  1034. :: +map-to-poly: inverse of poly-to-map
  1035. ++ map-to-poly
  1036. :: keys need to be 0, 1, 2, ... which is enforced by "got" below
  1037. |= mp=(map @ felt)
  1038. ^- poly
  1039. =| p=poly
  1040. =/ size=@ ~(wyt by mp)
  1041. =/ i=@ size
  1042. |-
  1043. ?: =(i 0)
  1044. p
  1045. $(p [(~(got by mp) (dec i)) p], i (dec i))
  1046. ::
  1047. ++ bop ~(ops array-op 1)
  1048. ::
  1049. :: +init-bpoly: given a list of belts, create a bpoly representing it
  1050. ++ init-bpoly
  1051. ~/ %init-bpoly
  1052. |= poly=(list belt)
  1053. ^- bpoly
  1054. ?: =(~ poly)
  1055. zero-bpoly
  1056. ?> (lth (lent poly) (bex 32))
  1057. :- (lent poly)
  1058. =/ high-bit (lsh [0 (mul (bex 6) (lent poly))] 1)
  1059. (add (rep 6 poly) high-bit)
  1060. ::
  1061. ++ bpoly-to-list
  1062. ~/ %bpoly-to-list
  1063. |= bp=bpoly
  1064. ^- poly
  1065. ?> !=(len.bp 0)
  1066. (snip (rip 6 dat.bp))
  1067. ::
  1068. ::
  1069. ++ zero-bpoly ~+((init-bpoly ~[0]))
  1070. ++ one-bpoly ~+((init-bpoly ~[1]))
  1071. ++ id-bpoly
  1072. ~+
  1073. ^- bpoly
  1074. (init-bpoly ~[0 1])
  1075. ::
  1076. ++ bpcan
  1077. |= bp=bpoly
  1078. ^- bpoly
  1079. =/ p ~(to-poly bop bp)
  1080. (init-bpoly (bcan p))
  1081. ::
  1082. ::
  1083. ++ bp-is-zero
  1084. ~/ %bp-is-zero
  1085. |= p=bpoly
  1086. ^- ?
  1087. ~+
  1088. =. p (bpcan p)
  1089. |(=(len.p 0) =(p zero-bpoly))
  1090. ::
  1091. ::
  1092. ++ bp-is-one
  1093. ~/ %bp-is-one
  1094. |= p=bpoly
  1095. ^- ?
  1096. ~+
  1097. =. p (bpcan p)
  1098. &(=(len.p 1) =((~(snag bop p) 0) 1))
  1099. ::
  1100. :: +bpadd: base field polynomial addition
  1101. ++ bpadd
  1102. ~/ %bpadd
  1103. |: [bp=`bpoly`zero-bpoly bq=`bpoly`zero-bpoly]
  1104. ^- bpoly
  1105. ?> &(!=(len.bp 0) !=(len.bq 0))
  1106. =/ p (bpoly-to-list bp)
  1107. =/ q (bpoly-to-list bq)
  1108. =/ lp (lent p)
  1109. =/ lq (lent q)
  1110. =/ m (max lp lq)
  1111. =: p (weld p (reap (sub m lp) 0))
  1112. q (weld q (reap (sub m lq) 0))
  1113. ==
  1114. %- init-bpoly
  1115. (zip p q badd)
  1116. ::
  1117. :: +bpneg: additive inverse of a base field polynomial
  1118. ++ bpneg
  1119. ~/ %bpneg
  1120. |= bp=bpoly
  1121. ^- bpoly
  1122. ?> !=(len.bp 0)
  1123. =/ p (bpoly-to-list bp)
  1124. %- init-bpoly
  1125. (turn p bneg)
  1126. ::
  1127. :: +bpsub: field polynomial subtraction
  1128. ++ bpsub
  1129. ~/ %bpsub
  1130. |= [p=bpoly q=bpoly]
  1131. ^- bpoly
  1132. (bpadd p (bpneg q))
  1133. ::
  1134. :: bpscal: multiply base field scalar c by base field polynomial p
  1135. ++ bpscal
  1136. ~/ %bpscal
  1137. |= [c=belt bp=bpoly]
  1138. ^- bpoly
  1139. =/ p (bpoly-to-list bp)
  1140. %- init-bpoly
  1141. %+ turn p
  1142. (cury bmul c)
  1143. ::
  1144. :: +bpmul: base field polynomial multiplication; naive algorithm; necessary for fmul!
  1145. ++ bpmul
  1146. ~/ %bpmul
  1147. |: [bp=`bpoly`one-bpoly bq=`bpoly`one-bpoly]
  1148. ^- bpoly
  1149. ?> &(!=(len.bp 0) !=(len.bq 0))
  1150. %- init-bpoly
  1151. ?: ?|(=(bp zero-bpoly) =(bq zero-bpoly))
  1152. ~[0]
  1153. =/ p (bpoly-to-list bp)
  1154. =/ q (bpoly-to-list bq)
  1155. =/ v=(list melt)
  1156. %- weld
  1157. :_ (turn p montify)
  1158. (reap (dec (lent q)) 0)
  1159. =/ w=(list melt) (flop (turn q montify))
  1160. =| prod=poly
  1161. |-
  1162. ?~ v
  1163. (flop prod)
  1164. %= $
  1165. v t.v
  1166. ::
  1167. prod
  1168. :_ prod
  1169. %. [v w]
  1170. :: computes a "dot product" (actually a bilinear form that just looks like
  1171. :: one) of v and w by implicitly zero-extending if lengths unequal we
  1172. :: don't actually zero-extend to save a constant time factor
  1173. |= [v=(list melt) w=(list melt)]
  1174. ^- melt
  1175. =| dot=belt
  1176. |-
  1177. ?: ?|(?=(~ v) ?=(~ w))
  1178. (mont-reduction dot)
  1179. $(v t.v, w t.w, dot (badd dot (montiply i.v i.w)))
  1180. ==
  1181. ::
  1182. :: +bp-hadamard
  1183. ::
  1184. :: Hadamard product of two bpolys. This is just a fancy name for pointwise multiplication.
  1185. ++ bp-hadamard
  1186. ~/ %bp-hadamard
  1187. |: [bp=`bpoly`one-bpoly bq=`bpoly`one-bpoly]
  1188. ^- bpoly
  1189. ?> =(len.bp len.bq)
  1190. ?: |(=(len.bp 0) =(len.bq 0)) zero-bpoly
  1191. (~(zip bop bp) bq bmul)
  1192. ::
  1193. ::
  1194. :: +bpdvr: base field polynomial division with remainder
  1195. ::
  1196. :: Analogous to integer division: (bpdvr a b) = [q r] where a = bq + r and degree(r)
  1197. :: < degree(b). (Using the mathematical degree where degree(~) = -∞.)
  1198. :: This implies q and r are unique.
  1199. ::
  1200. :: Algorithm is the usual one taught in high school.
  1201. ++ bpdvr
  1202. ~/ %bpdvr
  1203. |: [ba=`bpoly`one-bpoly bb=`bpoly`one-bpoly]
  1204. ^- [q=bpoly r=bpoly]
  1205. ?> &(!=(len.ba 0) !=(len.bb 0))
  1206. =/ a (bpoly-to-list ba)
  1207. =/ b (bpoly-to-list bb)
  1208. :: rem = remainder; a is effectively first candidate since (degree a) < (degree b) => done
  1209. :: rem, b are written high powers to low, as in high school algorithm
  1210. =^ rem b
  1211. :- (flop (bcan a))
  1212. (flop (bcan b))
  1213. ~| "Cannot divide by the zero polynomial."
  1214. ?< ?=(~ b)
  1215. =/ db (dec (lent b))
  1216. :: db = 0, rem = ~ => condition below this one is false and we fail the subsequent assertion;
  1217. :: Problem is (degree ~) = 0 is wrong mathematically; so we simply handle db = 0 separately.
  1218. ?: =(db 0)
  1219. :_ zero-bpoly
  1220. (bpscal (binv i.b) ba)
  1221. :: coeff = next coefficient added to the quotient, starting with highest power
  1222. =| coeff=belt
  1223. =| quot=poly
  1224. |-
  1225. ?: (lth (bdegree (flop rem)) db)
  1226. :- (init-bpoly quot)
  1227. (init-bpoly (bcan (flop rem)))
  1228. ?< ?=(~ rem)
  1229. =/ new-coeff (bdiv i.rem i.b)
  1230. =/ new-rem
  1231. %- bpoly-to-list
  1232. (bpsub (init-bpoly rem) (bpscal new-coeff (init-bpoly b)))
  1233. ?< ?=(~ new-rem)
  1234. %= $
  1235. coeff new-coeff
  1236. quot [new-coeff quot]
  1237. rem t.new-rem
  1238. ==
  1239. ::
  1240. :: +bpdiv: a/b for base field polynomials; q component of bpdvr
  1241. ++ bpdiv
  1242. ~/ %bpdiv
  1243. |= [a=bpoly b=bpoly]
  1244. ^- bpoly
  1245. q:(bpdvr a b)
  1246. ::
  1247. :: +bppow:: bppow: compute (p(x))^k
  1248. ++ bppow
  1249. ~/ %bppow
  1250. |= [bp=bpoly k=@]
  1251. ^- bpoly
  1252. ~+
  1253. ?> !=(len.bp 0)
  1254. %. [(init-bpoly ~[1]) bp k]
  1255. |= [q=bpoly p=bpoly k=@]
  1256. ?: =(k 0)
  1257. q
  1258. =/ f=@ (end 0 k)
  1259. ?: =(f 0)
  1260. %_ $
  1261. p (bpmul p p)
  1262. k (rsh 0 k)
  1263. ==
  1264. %_ $
  1265. q (bpmul q p)
  1266. p (bpmul p p)
  1267. k (rsh 0 k)
  1268. ==
  1269. ::
  1270. ::
  1271. :: +bpmod: a mod b for base field polynomials; r component of bpdvr
  1272. ++ bpmod
  1273. ~/ %bpmod
  1274. |= [a=bpoly b=bpoly]
  1275. ^- bpoly
  1276. r:(bpdvr a b)
  1277. ::
  1278. :: +bpegcd: base field polynomial extended Euclidean algorithm
  1279. ::
  1280. :: Gives gcd = d and u, v such that d = ua + vb from the Euclidean algorithm.
  1281. :: The algorithm is based on repeatedly dividing-with-remainder: a = bq + r,
  1282. :: b = rq_1 + r_1, etc. since gcd(a, b) = gcd(b, r) = ... (exercise) etc. The
  1283. :: pairs being divided in sequence are (a, b), (b, r), (r, r_1), etc. with update
  1284. :: rule new_first = old_second, new_second = remainder upon division of old_first
  1285. :: and old_second. One stops when a division by 0 would be necessary to generate
  1286. :: new_second, and then d = gcd is the second of the last full pair generated.
  1287. :: To see that u and v exist, repeatedly write d in terms of earlier and earlier
  1288. :: dividing pairs. To progressively generate the correct u, v, reexamine the original
  1289. :: calculation and write the remainders in terms of a, b at each step. Since each
  1290. :: remainder depends on the previous two, the same is true of u and v. This is the
  1291. :: reason for e.g. m1.u, which semantically is `u at time minus 1`; one can verify
  1292. :: the given initialization of these quantities.
  1293. :: NOTE: mathematically, gcd is not unique (only up to a scalar).
  1294. ++ bpegcd
  1295. ~/ %bpegcd
  1296. |= [a=bpoly b=bpoly]
  1297. ^- [d=bpoly u=bpoly v=bpoly]
  1298. =/ [u=[m1=bpoly m2=bpoly] v=[m1=bpoly m2=bpoly]]
  1299. :- zero-bpoly^one-bpoly
  1300. one-bpoly^zero-bpoly
  1301. |-
  1302. ?: =((bcan (bpoly-to-list b)) ~[0])
  1303. :+ (init-bpoly (bcan (bpoly-to-list a)))
  1304. (init-bpoly (bcan (bpoly-to-list m2.u)))
  1305. (init-bpoly (bcan (bpoly-to-list m2.v)))
  1306. =/ q-r (bpdvr a b)
  1307. %= $
  1308. a b
  1309. b r:q-r
  1310. u [(bpsub m2.u (bpmul q:q-r m1.u)) m1.u]
  1311. v [(bpsub m2.v (bpmul q:q-r m1.v)) m1.v]
  1312. ==
  1313. ::
  1314. :: +bpeval: evaluate a bpoly at a belt
  1315. ++ bpeval
  1316. ~/ %bpeval
  1317. |: [bp=`bpoly`one-bpoly x=`belt`1]
  1318. ^- belt
  1319. ~+
  1320. ?: (bp-is-zero bp) 0
  1321. ?: =(len.bp 1) (~(snag bop bp) 0)
  1322. =/ p ~(to-poly bop bp)
  1323. =. p (flop p)
  1324. =/ res=@ 0
  1325. |-
  1326. ?~ p !!
  1327. ?~ t.p
  1328. (badd (bmul res x) i.p)
  1329. :: based on p(x) = (...((a_n)x + a_{n-1})x + a_{n-2})x + ... )
  1330. $(res (badd (bmul res x) i.p), p t.p)
  1331. ::
  1332. :: construct the constant bpoly f(X)=c
  1333. ++ bp-c
  1334. |= c=belt
  1335. ^- bpoly
  1336. ~+
  1337. (init-bpoly ~[c])
  1338. ::
  1339. :: +bp-decompose
  1340. ::
  1341. :: given a polynomial f(X) of degree at most D*N, decompose into D polynomials
  1342. :: {h_i(X) : 0 <= i < D} each of degree at most N such that
  1343. ::
  1344. :: 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)
  1345. ::
  1346. :: This is just a generalization of splitting a polynomial into even and odd terms
  1347. :: as the FFT does.
  1348. :: h_i(X) is the terms whose degree is congruent to i modulo D.
  1349. ::
  1350. :: Passing in d=2 will split into even and odd terms.
  1351. ::
  1352. ++ bp-decompose
  1353. ~/ %bp-decompose
  1354. |= [p=bpoly d=@]
  1355. ^- (list bpoly)
  1356. =/ total-deg=@ (bdegree (bpoly-to-list p))
  1357. =/ deg=@
  1358. =/ dvr (dvr total-deg d)
  1359. ?:(=(q.dvr 0) p.dvr (add p.dvr 1))
  1360. =/ acc=(list (list belt)) (reap d ~)
  1361. =-
  1362. %+ turn -
  1363. |= poly=(list belt)
  1364. ?~ poly zero-bpoly
  1365. (init-bpoly (flop poly))
  1366. %+ roll (range (add 1 deg))
  1367. |= [n=@ acc=_acc]
  1368. %+ iturn acc
  1369. |= [i=@ l=(list belt)]
  1370. =/ idx (add (mul n d) i)
  1371. ?: (gth idx total-deg) l
  1372. [(~(snag bop p) idx) l]
  1373. --