1	# VMAC over any block cipher of at least 128 bits (the block-cipher
2	# interface, block.bend), as T. Krovetz and W. Dai, "VMAC: Message
3	# Authentication Code using Universal Hashing" (draft-krovetz-vmac-01, 2007)
4	# specifies it with AES: a 64- or 128-bit tag (VMAC-64, VMAC-128) of a
5	# message under a key and a nonce of 1 to 15 bytes.
6	#
7	#   KDF(K, index, n): the first n bytes of E(K, index || 0), E(K, index || 1),
8	#     .. (the index a byte, the counter the block's other bytes, big-endian)
9	#   VHASH, one 64-bit word per 64 bits of tag (iter = 0, 1):
10	#     L1: NH over each 128-byte piece of the message (zero-padded to 16
11	#       bytes): the sum of (m_i + k_i)(m_(i+1) + k_(i+1)) mod 2^126 over the
12	#       piece's 64-bit words m (little-endian) and the NH key's k
13	#       (big-endian; KDF index 128, offset by 16 bytes per iter)
14	#     L2: y = 1, then y = y k + a mod 2^127 - 1 for each NH value a (the
15	#       poly key k from KDF index 192 with each 32-bit field's top 3 bits
16	#       cleared; y = k for an empty message), then plus (the message's bit
17	#       length mod 1024) 2^64
18	#     L3: ((m1 + k1)(m2 + k2)) mod 2^64 - 257, m1 and m2 y's quotient and
19	#       remainder by 2^64 - 2^32, k1 and k2 the iter-th pair of 64-bit words
20	#       of KDF index 224 both below 2^64 - 257
21	#   PDF: E(K, the nonce left-padded with zeros to a block) (for a 64-bit
22	#     tag, with the nonce's last bit cleared, and the half that bit picks)
23	#   the tag: each 64-bit word of the PDF plus the VHASH word, mod 2^64
24	#
25	# As a MAC (mac.bend), with the nonce as the message's first nlen bytes
26	# (CrVmac.mac): ~CrVmacKey<K>, ~CrVmac.key(..), ~CrVmac.mac(..),
27	# ~CrVmac.verify(..); verify is the interface's named default, so the MAC
28	# laws hold for VMAC over every cipher (LAWS.bend: vmac_accepts).
29	import Base
30	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
31	import bend-osdev-word64@0.1.0.0/word64.bend as W
32	import ./crypto.bend as Cr
33	import ./mac.bend as Mc
34	import ./octets.bend as O
35	
36	# 128-bit numbers (internal)
37	type CrU128 is Data:
38	  CrU128{hi: W.W64, lo: W.W64}
39	
40	def cr.vm.carry(c: Bool) -> W.W64:
41	  match c:
42	    case True{}:
43	      W.W64.one()
44	    case False{}:
45	      W.W64.zero()
46	
47	def cr.vm.u(+lo: W.W64) -> CrU128:
48	  CrU128{W.W64.zero(), lo}
49	
50	# a + b mod 2^128
51	def cr.vm.add(a: CrU128, b: CrU128) -> CrU128:
52	  match a b:
53	    case CrU128{ah, +al} CrU128{bh, bl}:
54	      +lo = W.W64.add(al, bl)
55	      CrU128{W.W64.add(W.W64.add(ah, bh), cr.vm.carry(W.W64.is_lt(lo, al))), lo}
56	
57	def cr.vm.w(+a: U32) -> W.W64:
58	  W.W64.from_u32(a)
59	
60	# the 128-bit product of two 64-bit words
61	def cr.vm.mul(+a: W.W64, +b: W.W64) -> CrU128:
62	  +al = W.W64.lo(a)
63	  +ah = W.W64.hi(a)
64	  +bl = W.W64.lo(b)
65	  +bh = W.W64.hi(b)
66	  +p0 = W.W64.mul(cr.vm.w(al), cr.vm.w(bl))
67	  +p1 = W.W64.mul(cr.vm.w(al), cr.vm.w(bh))
68	  +p2 = W.W64.mul(cr.vm.w(ah), cr.vm.w(bl))
69	  +p3 = W.W64.mul(cr.vm.w(ah), cr.vm.w(bh))
70	  +mid = W.W64.add(p1, p2)
71	  +lo = W.W64.add(p0, W.W64.shl(mid, 32n))
72	  CrU128{W.W64.add(W.W64.add(p3, W.W64.shr(mid, 32n)), W.W64.add(W.W64.shl(cr.vm.carry(W.W64.is_lt(mid, p1)), 32n), cr.vm.carry(W.W64.is_lt(lo, p0)))), lo}
73	
74	# Words of bytes
75	
76	def cr.vm.at.go(xs: List<&2, U32>, i: Nat) -> U32:
77	  match xs:
78	    case Nil{}:
79	      0
80	    case Con{h, t}:
81	      match i:
82	        case 0n:
83	          h
84	        case 1n+p:
85	          cr.vm.at.go(t, p)
86	
87	def cr.vm.at(+xs: List<&2, U32>, +i: Nat) -> U32:
88	  B.byte(cr.vm.at.go(xs, i))
89	
90	def cr.vm.u32be(+xs: List<&2, U32>, +i: Nat) -> U32:
91	  U32.or(U32.or(U32.shln(cr.vm.at(xs, i), 24n), U32.shln(cr.vm.at(xs, Nat.add(i, 1n)), 16n)), U32.or(U32.shln(cr.vm.at(xs, Nat.add(i, 2n)), 8n), cr.vm.at(xs, Nat.add(i, 3n))))
92	
93	def cr.vm.u32le(+xs: List<&2, U32>, +i: Nat) -> U32:
94	  U32.or(U32.or(U32.shln(cr.vm.at(xs, Nat.add(i, 3n)), 24n), U32.shln(cr.vm.at(xs, Nat.add(i, 2n)), 16n)), U32.or(U32.shln(cr.vm.at(xs, Nat.add(i, 1n)), 8n), cr.vm.at(xs, i)))
95	
96	# the big-endian and the little-endian 64-bit word at byte i
97	def cr.vm.w64be(+xs: List<&2, U32>, +i: Nat) -> W.W64:
98	  W.W64.from_parts(cr.vm.u32be(xs, i), cr.vm.u32be(xs, Nat.add(i, 4n)))
99	
100	def cr.vm.w64le(+xs: List<&2, U32>, +i: Nat) -> W.W64:
101	  W.W64.from_parts(cr.vm.u32le(xs, Nat.add(i, 4n)), cr.vm.u32le(xs, i))
102	
103	def cr.vm.word(be: Bool, +xs: List<&2, U32>, +i: Nat) -> W.W64:
104	  match be:
105	    case True{}:
106	      cr.vm.w64be(xs, i)
107	    case False{}:
108	      cr.vm.w64le(xs, i)
109	
110	# n big-endian (be True) or little-endian 64-bit words of xs from byte i
111	def cr.vm.words(n: Nat, +be: Bool, +xs: List<&2, U32>, +i: Nat) -> List<&2, W.W64>:
112	  match n:
113	    case 0n:
114	      Nil{}
115	    case 1n+p:
116	      Con{cr.vm.word(be, xs, i), cr.vm.words(p, be, xs, Nat.add(i, 8n))}
117	
118	def cr.vm.bytes64(+w: W.W64) -> List<&2, U32>:
119	  B.append(B.be32(W.W64.hi(w)), B.be32(W.W64.lo(w)))
120	
121	# The KDF: the bytes of E(K, index || counter), counter = 0, 1, ..
122	
123	def cr.vm.encb(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~blk_to: Blk -> B.Octets, +k: K, x: Maybe<&2, Blk>, +o: B.Octets) -> List<&2, U32>:
124	  match x:
125	    case None{}:
126	      B.Octets.to_list(o)
127	    case Some{b}:
128	      B.Octets.to_list(blk_to(enc(k, b)))
129	
130	def cr.vm.e(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K, +o: B.Octets) -> List<&2, U32>:
131	  cr.vm.encb(~K, ~Blk, ~enc, ~blk_to, k, blk_of(o), o)
132	
133	def cr.vm.kdf.go(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, blocks: Nat, +k: K, +index: U32, +c: U32) -> List<&2, U32>:
134	  match blocks:
135	    case 0n:
136	      Nil{}
137	    case 1n+p:
138	      +o = B.Octets.of_list(Con{index, B.append(B.zeros(Nat.sub(bsize, 5n)), B.be32(c))})
139	      B.append(cr.vm.e(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, o), cr.vm.kdf.go(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, p, k, index, U32.add(c, 1)))
140	
141	# the first n bytes of the KDF for index
142	def cr.vm.kdf(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K, +index: U32, +n: Nat) -> List<&2, U32>:
143	  B.take(n, cr.vm.kdf.go(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, Nat.add(Nat.div(n, bsize), 1n), k, index, 0))
144	
145	# L1: NH, mod 2^126
146	
147	def cr.vm.nh.go(ms: List<&2, W.W64>, ks: List<&2, W.W64>, y: CrU128) -> CrU128:
148	  match ms:
149	    case Con{m0, Con{m1, mt}}:
150	      match ks:
151	        case Con{k0, Con{k1, kt}}:
152	          cr.vm.nh.go(mt, kt, cr.vm.add(y, cr.vm.mul(W.W64.add(m0, k0), W.W64.add(m1, k1))))
153	        case _:
154	          y
155	    case _:
156	      y
157	
158	def cr.vm.mod126(x: CrU128) -> CrU128:
159	  match x:
160	    case CrU128{h, l}:
161	      CrU128{W.W64.and(h, W.W64.from_parts(1073741823, 4294967295)), l}
162	
163	# the NH value of a piece of 1 to 128 bytes (zero-padded to 16 bytes)
164	def cr.vm.nh(+ks: List<&2, W.W64>, +p: List<&2, U32>) -> CrU128:
165	  cr.vm.mod126(cr.vm.nh.go(cr.vm.words(Nat.mul(2n, Nat.div(Nat.add(B.len(p), 15n), 16n)), False{}, p, 0n), ks, cr.vm.u(W.W64.zero())))
166	
167	# L2: arithmetic mod p127 = 2^127 - 1
168	
169	def cr.vm.m63() -> W.W64:
170	  W.W64.from_parts(2147483647, 4294967295)
171	
172	def cr.vm.fold.pick(top: Bool, +h: W.W64, +l: W.W64) -> CrU128:
173	  match top:
174	    case True{}:
175	      cr.vm.add(CrU128{W.W64.and(h, cr.vm.m63()), l}, cr.vm.u(W.W64.one()))
176	    case False{}:
177	      CrU128{h, l}
178	
179	# x below 2^128 to a value congruent mod p127 below 2^127 + 1
180	def cr.vm.fold(x: CrU128) -> CrU128:
181	  match x:
182	    case CrU128{+h, +l}:
183	      cr.vm.fold.pick(W.W64.is_eq(W.W64.shr(h, 63n), W.W64.one()), h, l)
184	
185	def cr.vm.norm.pick(p: Bool, +x: CrU128) -> CrU128:
186	  match p:
187	    case True{}:
188	      cr.vm.u(W.W64.zero())
189	    case False{}:
190	      x
191	
192	# x (below 2^127 + 1) fully reduced mod p127
193	def cr.vm.norm(+x: CrU128) -> CrU128:
194	  match x:
195	    case CrU128{h, l}:
196	      cr.vm.norm.pick(Bool.and(W.W64.is_eq(h, cr.vm.m63()), W.W64.is_eq(l, W.W64.max())), x)
197	
198	def cr.vm.reduce(+x: CrU128) -> CrU128:
199	  cr.vm.norm(cr.vm.fold(cr.vm.fold(x)))
200	
201	def cr.vm.lt(a: CrU128, b: CrU128) -> Bool:
202	  match a b:
203	    case CrU128{+ah, al} CrU128{+bh, bl}:
204	      Bool.or(W.W64.is_lt(ah, bh), Bool.and(W.W64.is_eq(ah, bh), W.W64.is_lt(al, bl)))
205	
206	# the 256-bit number with 64-bit words x3, x2, x1, x0 reduced mod p127:
207	# (x >> 127) + (x mod 2^127)
208	def cr.vm.mm3(+x3: W.W64, +x2: W.W64, +x1: W.W64, +x0: W.W64) -> CrU128:
209	  cr.vm.reduce(cr.vm.fold(cr.vm.add(CrU128{W.W64.or(W.W64.shl(x3, 1n), W.W64.shr(x2, 63n)), W.W64.or(W.W64.shl(x2, 1n), W.W64.shr(x1, 63n))}, CrU128{W.W64.and(x1, cr.vm.m63()), x0})))
210	
211	def cr.vm.mm2(b: CrU128, +x1: W.W64, +x0: W.W64) -> CrU128:
212	  match b:
213	    case CrU128{x3, x2}:
214	      cr.vm.mm3(x3, x2, x1, x0)
215	
216	def cr.vm.mm1(a: CrU128, +x0: W.W64, +mh: W.W64, midc: Bool, +p3: CrU128) -> CrU128:
217	  match a:
218	    case CrU128{ac, x1}:
219	      cr.vm.mm2(cr.vm.add(cr.vm.add(p3, CrU128{cr.vm.carry(midc), mh}), cr.vm.u(ac)), x1, x0)
220	
221	def cr.vm.mm0(p0: CrU128, mid: CrU128, midc: Bool, +p3: CrU128) -> CrU128:
222	  match p0 mid:
223	    case CrU128{q0h, q0l} CrU128{mh, ml}:
224	      cr.vm.mm1(cr.vm.add(cr.vm.u(q0h), cr.vm.u(ml)), q0l, mh, midc, p3)
225	
226	# the 256-bit p3 2^128 + (p1 + p2) 2^64 + p0, reduced mod p127
227	def cr.vm.mulmod.go(p0: CrU128, +p1: CrU128, p2: CrU128, +p3: CrU128) -> CrU128:
228	  +mid = cr.vm.add(p1, p2)
229	  cr.vm.mm0(p0, mid, cr.vm.lt(mid, p1), p3)
230	
231	# a * b mod p127, for a, b below 2^127
232	def cr.vm.mulmod(a: CrU128, b: CrU128) -> CrU128:
233	  match a b:
234	    case CrU128{+ah, +al} CrU128{+bh, +bl}:
235	      cr.vm.mulmod.go(cr.vm.mul(al, bl), cr.vm.mul(al, bh), cr.vm.mul(ah, bl), cr.vm.mul(ah, bh))
236	
237	# L2 over the NH values of the pieces ps, from y; an empty message is the
238	# poly key itself
239	def cr.vm.poly.go(+nk: List<&2, W.W64>, +k: CrU128, ps: List<&2, List<&2, U32>>, +y: CrU128) -> CrU128:
240	  match ps:
241	    case Nil{}:
242	      y
243	    case Con{p, t}:
244	      cr.vm.poly.go(nk, k, t, cr.vm.reduce(cr.vm.add(cr.vm.mulmod(y, k), cr.vm.nh(nk, p))))
245	
246	def cr.vm.poly(+nk: List<&2, W.W64>, +k: CrU128, ps: List<&2, List<&2, U32>>) -> CrU128:
247	  match ps:
248	    case Nil{}:
249	      k
250	    case Con{p, t}:
251	      cr.vm.poly.go(nk, k, Con{p, t}, cr.vm.u(W.W64.one()))
252	
253	# L3: the 64-bit words of y's quotient and remainder by 2^64 - 2^32, then
254	# ((m1 + k1)(m2 + k2)) mod p64 = 2^64 - 257
255	
256	def cr.vm.p64() -> W.W64:
257	  W.W64.from_parts(4294967295, 4294967039)
258	
259	# x below 2^128, folded: hi 2^64 + lo = hi 257 + lo (mod p64)
260	def cr.vm.f64(x: CrU128) -> CrU128:
261	  match x:
262	    case CrU128{h, +l}:
263	      cr.vm.add(cr.vm.mul(h, cr.vm.w(257)), cr.vm.u(l))
264	
265	def cr.vm.sub64.pick(ge: Bool, +x: W.W64) -> W.W64:
266	  match ge:
267	    case True{}:
268	      W.W64.sub(x, cr.vm.p64())
269	    case False{}:
270	      x
271	
272	def cr.vm.last64(x: CrU128) -> W.W64:
273	  match x:
274	    case CrU128{h, +l}:
275	      +y = W.W64.add(l, W.W64.mul(h, cr.vm.w(257)))
276	      cr.vm.sub64.pick(W.W64.is_ge(y, cr.vm.p64()), y)
277	
278	# x below 2^130 (as hi, lo) mod p64
279	def cr.vm.mod64(+x: CrU128) -> W.W64:
280	  cr.vm.last64(cr.vm.f64(cr.vm.f64(x)))
281	
282	def cr.vm.digit(+r: W.W64, +d: U32) -> W.W64:
283	  W.W64.from_parts(W.W64.lo(r), d)
284	
285	# q (the quotient's two low base-2^32 digits) and r, for (x2, x1, x0)
286	# divided by 2^32 - 1, one digit at a time
287	type CrVmQr is Data:
288	  CrVmQr{q1: U32, q0: U32, r: U32}
289	
290	def cr.vm.qr(+x2: U32, +x1: U32, +x0: U32) -> CrVmQr:
291	  +d = cr.vm.w(4294967295)
292	  +r2 = W.W64.mod(cr.vm.w(x2), d)
293	  +c1 = cr.vm.digit(r2, x1)
294	  +r1 = W.W64.mod(c1, d)
295	  +c0 = cr.vm.digit(r1, x0)
296	  CrVmQr{W.W64.lo(W.W64.div(c1, d)), W.W64.lo(W.W64.div(c0, d)), W.W64.lo(W.W64.mod(c0, d))}
297	
298	def cr.vm.l3.go(qr: CrVmQr, +lo: U32, +k1: W.W64, +k2: W.W64) -> W.W64:
299	  match qr:
300	    case CrVmQr{q1, q0, r}:
301	      cr.vm.mod64(cr.vm.mul(cr.vm.mod64(cr.vm.add(cr.vm.u(W.W64.from_parts(q1, q0)), cr.vm.u(k1))), cr.vm.mod64(cr.vm.add(cr.vm.u(W.W64.from_parts(r, lo)), cr.vm.u(k2)))))
302	
303	# L3 of y (below p127) under k1, k2
304	def cr.vm.l3(y: CrU128, +k1: W.W64, +k2: W.W64) -> W.W64:
305	  match y:
306	    case CrU128{+h, +l}:
307	      cr.vm.l3.go(cr.vm.qr(W.W64.hi(h), W.W64.lo(h), W.W64.hi(l)), W.W64.lo(l), k1, k2)
308	
309	# The key
310	
311	# one VHASH word's keys: the NH key words, the poly key, the L3 pair
312	type CrVmIter is Data:
313	  CrVmIter{nh: List<&2, W.W64>, poly: CrU128, k1: W.W64, k2: W.W64}
314	
315	def cr.vm.l3keys.pick(ok: Bool, +a: W.W64, +b: W.W64, rest: List<&2, CrU128>) -> List<&2, CrU128>:
316	  match ok:
317	    case True{}:
318	      Con{CrU128{a, b}, rest}
319	    case False{}:
320	      rest
321	
322	# the L3 pairs of 64-bit words of the KDF bytes xs both below p64, in order
323	def cr.vm.l3keys(xs: List<&2, W.W64>) -> List<&2, CrU128>:
324	  match xs:
325	    case Con{+a, Con{+b, t}}:
326	      cr.vm.l3keys.pick(Bool.and(W.W64.is_lt(a, cr.vm.p64()), W.W64.is_lt(b, cr.vm.p64())), a, b, cr.vm.l3keys(t))
327	    case _:
328	      Nil{}
329	
330	def cr.vm.nth.pair(ps: List<&2, CrU128>, i: Nat) -> CrU128:
331	  match ps:
332	    case Nil{}:
333	      CrU128{W.W64.zero(), W.W64.zero()}
334	    case Con{h, t}:
335	      match i:
336	        case 0n:
337	          h
338	        case 1n+j:
339	          cr.vm.nth.pair(t, j)
340	
341	def cr.vm.u128.of(+xs: List<&2, U32>) -> CrU128:
342	  CrU128{cr.vm.w64be(xs, 0n), cr.vm.w64be(xs, 8n)}
343	
344	# the poly key mask: each 32-bit field's top 3 bits cleared
345	def cr.vm.pmask(x: CrU128) -> CrU128:
346	  match x:
347	    case CrU128{h, l}:
348	      +m = W.W64.from_parts(536870911, 536870911)
349	      CrU128{W.W64.and(h, m), W.W64.and(l, m)}
350	
351	def cr.vm.iter.of(+nh: List<&2, W.W64>, +poly: CrU128, kp: CrU128) -> CrVmIter:
352	  match kp:
353	    case CrU128{k1, k2}:
354	      CrVmIter{nh, poly, k1, k2}
355	
356	# A VMAC key: the cipher's key schedule and each VHASH word's keys (one for
357	# a 64-bit tag, two for a 128-bit tag; opaque)
358	type CrVmacKey<-K: Data> is Data:
359	  CrVmacKey{k: K, iters: List<&2, CrVmIter>}
360	
361	def cr.vm.iters(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, n: Nat, +k: K, +i: Nat, +l3: List<&2, CrU128>) -> List<&2, CrVmIter>:
362	  match n:
363	    case 0n:
364	      Nil{}
365	    case 1n+p:
366	      +nh = cr.vm.words(16n, True{}, B.drop(Nat.mul(16n, i), cr.vm.kdf(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, k, 128, Nat.add(128n, Nat.mul(16n, i)))), 0n)
367	      +poly = cr.vm.pmask(cr.vm.u128.of(B.drop(Nat.mul(16n, i), cr.vm.kdf(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, k, 192, Nat.mul(16n, Nat.add(i, 1n))))))
368	      Con{cr.vm.iter.of(nh, poly, cr.vm.nth.pair(l3, i)), cr.vm.iters(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, p, k, Nat.add(i, 1n), l3)}
369	
370	def cr.vm.key.of(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +words: Nat, +k: K) -> CrVmacKey<K>:
371	  +l3 = cr.vm.l3keys(cr.vm.words(32n, True{}, cr.vm.kdf(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, k, 224, 256n), 0n))
372	  CrVmacKey{k, cr.vm.iters(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, words, k, 0n, l3)}
373	
374	# The key for tags of words 64-bit words (1: VMAC-64, 2: VMAC-128) from a raw
375	# key the cipher takes (KDF index 224's first 16 pairs give the L3 keys)
376	def CrVmac.key(~K: Data, ~Blk: Data, ~bsize: Nat, ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ~words: Nat, o: B.Octets) -> Result<&2, &2, Cr.CrError, CrVmacKey<K>>:
377	  Result.map(&2, &2, Cr.CrError, K, CrVmacKey<K>, k => cr.vm.key.of(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, words, k), key(o))
378	
379	# VHASH: one word per iter
380	def cr.vm.vhash(its: List<&2, CrVmIter>, +ps: List<&2, List<&2, U32>>, +lenterm: W.W64) -> List<&2, W.W64>:
381	  match its:
382	    case Nil{}:
383	      Nil{}
384	    case Con{it, rest}:
385	      match it:
386	        case CrVmIter{nh, poly, k1, k2}:
387	          Con{cr.vm.l3(cr.vm.reduce(cr.vm.add(cr.vm.poly(nh, poly, ps), CrU128{lenterm, W.W64.zero()})), k1, k2), cr.vm.vhash(rest, ps, lenterm)}
388	
389	# the tag words: pad word + hash word, mod 2^64
390	def cr.vm.sum(ps: List<&2, W.W64>, hs: List<&2, W.W64>) -> List<&2, U32>:
391	  match ps hs:
392	    case Con{p, pt} Con{h, ht}:
393	      B.append(cr.vm.bytes64(W.W64.add(p, h)), cr.vm.sum(pt, ht))
394	    case _ _:
395	      Nil{}
396	
397	def cr.vm.len(its: List<&2, CrVmIter>) -> Nat:
398	  match its:
399	    case Nil{}:
400	      0n
401	    case Con{h, t}:
402	      1n+cr.vm.len(t)
403	
404	def cr.vm.pdf.last(one: Bool, +b: U32) -> U32:
405	  match one:
406	    case True{}:
407	      U32.and(254, b)
408	    case False{}:
409	      b
410	
411	def cr.vm.pdf.pick(one: Bool, odd: Bool, +t: List<&2, U32>, +words: Nat) -> List<&2, W.W64>:
412	  match one:
413	    case True{}:
414	      match odd:
415	        case True{}:
416	          [cr.vm.w64be(t, 8n)]
417	        case False{}:
418	          [cr.vm.w64be(t, 0n)]
419	    case False{}:
420	      cr.vm.words(words, True{}, t, 0n)
421	
422	# the PDF's words for a nonce of 1 to 15 bytes
423	def cr.vm.pdf(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K, +words: Nat, +nonce: List<&2, U32>) -> List<&2, W.W64>:
424	  +n = B.len(nonce)
425	  +last = cr.vm.at(nonce, Nat.sub(n, 1n))
426	  +bit = U32.and(1, last)
427	  +cleared = B.append(B.take(Nat.sub(n, 1n), nonce), [cr.vm.pdf.last(Nat.is_eq(words, 1n), last)])
428	  +t = cr.vm.e(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, B.Octets.of_list(B.append(B.zeros(Nat.sub(bsize, n)), cleared)))
429	  cr.vm.pdf.pick(Nat.is_eq(words, 1n), U32.is_eq(bit, 1), t, words)
430	
431	def cr.vm.tag.go(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, kk: CrVmacKey<K>, +nonce: List<&2, U32>, +m: List<&2, U32>) -> B.Octets:
432	  match kk:
433	    case CrVmacKey{+k, +its}:
434	      +lenterm = W.W64.from_u32(U32.mul(U32.from_nat(Nat.mod(B.len.fast(m), 128n)), 8))
435	      B.Octets.of_list(cr.vm.sum(cr.vm.pdf(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, k, cr.vm.len(its), nonce), cr.vm.vhash(its, O.CrOct.pieces(128n, m), lenterm)))
436	
437	def cr.vm.tag.pick(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ok: Bool, kk: CrVmacKey<K>, +nonce: B.Octets, m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
438	  match ok:
439	    case True{}:
440	      Done{cr.vm.tag.go(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, kk, B.Octets.to_list(nonce), B.Octets.to_list(m))}
441	    case False{}:
442	      Fail{Cr.CrBadNonceLength{B.Octets.len(nonce)}}
443	
444	# The tag of m under a nonce of 1 to bsize - 1 bytes (CrBadNonceLength
445	# otherwise): 8 bytes for a VMAC-64 key, 16 for a VMAC-128 key
446	def CrVmac.tag(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, kk: CrVmacKey<K>, +nonce: B.Octets, m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
447	  +n = B.Octets.len(nonce)
448	  cr.vm.tag.pick(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, Bool.and(Nat.is_lt(0n, n), Nat.is_lt(n, bsize)), kk, nonce, m)
449	
450	def cr.vm.or_empty(r: Result<&2, &2, Cr.CrError, B.Octets>) -> B.Octets:
451	  match r:
452	    case Fail{e}:
453	      B.Octets.empty()
454	    case Done{t}:
455	      t
456	
457	# As a MAC: the nonce is the message's first nlen bytes (1 to bsize - 1),
458	# the data the rest; a message too short for its nonce has the empty tag
459	def cr.vm.mac(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ~nlen: Nat, kk: CrVmacKey<K>, +m: B.Octets) -> B.Octets:
460	  cr.vm.or_empty(CrVmac.tag(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, kk, B.Octets.take(nlen, m), B.Octets.drop(nlen, m)))
461	
462	def CrVmac.mac(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ~nlen: Nat, kk: CrVmacKey<K>, m: B.Octets) -> B.Octets:
463	  cr.vm.mac(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, ~nlen, kk, m)
464	
465	# whether t is m's tag (every byte compared; the MAC interface's default)
466	def CrVmac.verify(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ~nlen: Nat, kk: CrVmacKey<K>, m: B.Octets, t: B.Octets) -> Bool:
467	  Mc.CrMac.verify_tag(~CrVmacKey<K>, ~CrVmac.mac(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, ~nlen), kk, m, t)