1	import Base
2	
3	# Arithmetic modulo p = 2^130 - 5 on little-endian lists of U32 limbs of
4	# radix 2^8 (TweetNaCl's representation): a list [l0, l1, ...] stands for
5	# l0 + 2^8 l1 + 2^16 l2 + ... . Limbs may exceed 8 bits between carry
6	# passes; every operation below keeps them under 2^31 on the Poly1305 path
7	# (proofs/crypto/poly1305/ bounds each step), so no U32 operation wraps.
8	#
9	# Constant time: every loop runs over public lengths; the only data-dependent
10	# choice (the final conditional subtraction of p) is a mask select, with no
11	# branch and no secret-dependent memory access. Bend has no timing model, so
12	# this is a property of the code's shape, not a proved fact.
13	
14	# The first limb (0 for the empty list) and the rest.
15	def hd0(xs: List<&2, U32>) -> U32:
16	  match xs:
17	    case Nil{}: 0
18	    case x <> t: x
19	
20	def tl(xs: List<&2, U32>) -> List<&2, U32>:
21	  match xs:
22	    case Nil{}: Nil{}
23	    case x <> t: t
24	
25	# Limb-wise sum (the shorter list is padded with zeros), no carries.
26	def add(a: List<&2, U32>, b: List<&2, U32>) -> List<&2, U32>:
27	  match a b:
28	    case Nil{} _: b
29	    case x <> at Nil{}: x <> at
30	    case x <> at y <> bt: U32.add(x, y) <> add(at, bt)
31	
32	# Every limb times c, no carries.
33	def scale(+c: U32, a: List<&2, U32>) -> List<&2, U32>:
34	  match a:
35	    case Nil{}: Nil{}
36	    case x <> t: U32.mul(x, c) <> scale(c, t)
37	
38	# Schoolbook product, no carries: x r0 + 2^8 (x r1 + 2^8 (...)).
39	def mul(+x: List<&2, U32>, r: List<&2, U32>) -> List<&2, U32>:
40	  match r:
41	    case Nil{}: Nil{}
42	    case r0 <> rs: add(scale(r0, x), 0 <> mul(x, rs))
43	
44	def take(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
45	  match n xs:
46	    case 0n _: Nil{}
47	    case 1n+k Nil{}: Nil{}
48	    case 1n+k x <> rest: x <> take(k, rest)
49	
50	def skip(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
51	  match n xs:
52	    case 0n _: xs
53	    case 1n+k Nil{}: Nil{}
54	    case 1n+k x <> rest: skip(k, rest)
55	
56	# The first n limbs, padded with zeros to exactly n.
57	def fit(n: Nat, +xs: List<&2, U32>) -> List<&2, U32>:
58	  match n:
59	    case 0n: Nil{}
60	    case 1n+k: hd0(xs) <> fit(k, tl(xs))
61	
62	# 2^136 = 64 p + 320: limbs 17.. are folded onto limbs 0.. times 320.
63	def fold(+z: List<&2, U32>) -> List<&2, U32>:
64	  add(take(17n, z), scale(320, skip(17n, z)))
65	
66	# A carry pass over n limbs, each kept to 8 bits; the carry u and all limbs
67	# from n on (one, on the Poly1305 path) are summed into the top limb.
68	def carry(n: Nat, +ds: List<&2, U32>, u: U32) -> List<&2, U32>:
69	  match n:
70	    case 0n: [U32.add(u, hd0(ds))]
71	    case 1n+k:
72	      +s = U32.add(u, hd0(ds))
73	      U32.and(s, 255) <> carry(k, tl(ds), U32.shrn(s, 8n))
74	
75	# Limb n (the top one) reduced to its low 2 bits, i.e. the value below 2^130
76	# when n = 16; quot is the rest of limb n, the multiple of 2^130.
77	def split(n: Nat, +xs: List<&2, U32>) -> List<&2, U32>:
78	  match n:
79	    case 0n: [U32.and(hd0(xs), 3)]
80	    case 1n+k: hd0(xs) <> split(k, tl(xs))
81	
82	def quot(n: Nat, +xs: List<&2, U32>) -> U32:
83	  match n:
84	    case 0n: U32.shrn(hd0(xs), 2n)
85	    case 1n+k: quot(k, tl(xs))
86	
87	# Partial reduction of 17 limbs: carry, then 2^130 q = p q + 5 q, so q is
88	# folded back as 5 q on limb 0 and carried again. The result has limbs 0..15
89	# below 2^8 and a value below 5 * 2^128 < 2p.
90	def reduce(+d: List<&2, U32>) -> List<&2, U32>:
91	  +t = carry(16n, d, 0)
92	  carry(16n, add([U32.mul(quot(16n, t), 5)], split(16n, t)), 0)
93	
94	# One Poly1305 block: h = (h + c) r, partially reduced mod p.
95	def block(+r: List<&2, U32>, h: List<&2, U32>, c: List<&2, U32>) -> List<&2, U32>:
96	  reduce(fold(mul(add(h, c), r)))
97	
98	# a when m is all zeros, b when m is all ones.
99	def pick(+m: U32, +a: U32, b: U32) -> U32:
100	  U32.xor(a, U32.and(m, U32.xor(a, b)))
101	
102	def select(+m: U32, a: List<&2, U32>, b: List<&2, U32>) -> List<&2, U32>:
103	  match a b:
104	    case x <> at y <> bt: pick(m, x, y) <> select(m, at, bt)
105	    case _ _: Nil{}
106	
107	# The low 16 limbs of h mod p, for h below 2p: g = h + 5 has bit 130 set
108	# exactly when h >= p, and then its low 128 bits are those of h - p.
109	def freeze(+h: List<&2, U32>) -> List<&2, U32>:
110	  +g = carry(16n, add(h, [5]), 0)
111	  +b = U32.shrn(hd0(skip(16n, g)), 2n)
112	  select(U32.sub(0, b), take(16n, h), take(16n, g))
113	
114	# n bytes of the value of ds + u (mod 2^(8n)).
115	def bytes(n: Nat, +ds: List<&2, U32>, u: U32) -> List<&2, U32>:
116	  match n:
117	    case 0n: Nil{}
118	    case 1n+k:
119	      +s = U32.add(u, hd0(ds))
120	      U32.and(s, 255) <> bytes(k, tl(ds), U32.shrn(s, 8n))
121	
122	# The tag bytes: the low 128 bits of (h mod p) + s. (Entered through a match
123	# on s, both arms the same: while s is unknown a proof's goal stays one call
124	# instead of sixteen unfolded byte steps.)
125	def fin(+h: List<&2, U32>, s: List<&2, U32>) -> List<&2, U32>:
126	  match s:
127	    case Nil{}: bytes(16n, add(freeze(h), Nil{}), 0)
128	    case y <> ys: bytes(16n, add(freeze(h), y <> ys), 0)