vmac.bend

bend-osdev-crypto@0.1.0.0 · 467 lines · 71 definitions

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).
29import Base
30import bend-osdev-bytes@0.1.0.0/bytes.bend as B
31import bend-osdev-word64@0.1.0.0/word64.bend as W
32import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
33import bend-osdev-crypto@0.1.0.0/mac.bend as Mc
34import bend-osdev-crypto@0.1.0.0/octets.bend as O
35
36# 128-bit numbers (internal)
37type CrU128 is Data:
38  CrU128{hi: W.W64, lo: W.W64}
39
40def 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
47def cr.vm.u(+lo: W.W64) -> CrU128:
48  CrU128{W.W64.zero(), lo}
49
50# a + b mod 2^128
51def 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
57def cr.vm.w(+a: U32) -> W.W64:
58  W.W64.from_u32(a)
59
60# the 128-bit product of two 64-bit words
61def 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
76def 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
87def cr.vm.at(+xs: List<&2, U32>, +i: Nat) -> U32:
88  B.byte(cr.vm.at.go(xs, i))
89
90def 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
93def 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
97def 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
100def 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
103def 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
111def 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
118def 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
123def 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
130def 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
133def 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
142def 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
147def 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
158def 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)
164def 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
169def cr.vm.m63() -> W.W64:
170  W.W64.from_parts(2147483647, 4294967295)
171
172def 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
180def 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
185def 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
193def 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
198def cr.vm.reduce(+x: CrU128) -> CrU128:
199  cr.vm.norm(cr.vm.fold(cr.vm.fold(x)))
200
201def 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)
208def 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
211def 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
216def 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
221def 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
227def 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
232def 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
239def 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
246def 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
256def 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)
260def 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
265def 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
272def 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
279def cr.vm.mod64(+x: CrU128) -> W.W64:
280  cr.vm.last64(cr.vm.f64(cr.vm.f64(x)))
281
282def 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
287type CrVmQr is Data:
288  CrVmQr{q1: U32, q0: U32, r: U32}
289
290def 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
298def 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
304def 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
312type CrVmIter is Data:
313  CrVmIter{nh: List<&2, W.W64>, poly: CrU128, k1: W.W64, k2: W.W64}
314
315def 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
323def 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
330def 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
341def 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
345def 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
351def 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)
358type CrVmacKey<-K: Data> is Data:
359  CrVmacKey{k: K, iters: List<&2, CrVmIter>}
360
361def 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
370def 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)
376def 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
380def 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
390def 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
397def 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
404def 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
411def 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
423def 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
431def 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
437def 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
446def 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
450def 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
459def 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
462def 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)
466def 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)