1	# bend-osdev-aead: authenticated encryption with associated data, as
2	# instances of bend-osdev-crypto's AEAD interface (crypto/aead.bend, the
3	# shape of RFC 5116): AEGIS-128 (aegis128.bend), encrypt-then-MAC over any
4	# cipher and any MAC (authenc.bend), and the IV generators ESSIV
5	# (essiv.bend), seqiv (seqiv.bend) and echainiv (echainiv.bend), which turn
6	# one AEAD (or, for ESSIV, one cipher with an IV) into another.
7	#
8	# This file holds what they share: a ciphertext with its tag appended, and
9	# split again. Bend imports do not re-export: import the files you use.
10	import Base
11	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
12	import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
13	
14	# A ciphertext and its tag, split from the bytes of both (the tag the last
15	# tlen bytes; CrTooShort for fewer than tlen bytes)
16	type AdSplit is Data:
17	  AdSplit{c: B.Octets, t: B.Octets}
18	
19	def ad.split.pick(short: Bool, +tlen: Nat, +o: B.Octets) -> Result<&2, &2, Cr.CrError, AdSplit>:
20	  match short:
21	    case True{}:
22	      Fail{Cr.CrTooShort{B.Octets.len(o)}}
23	    case False{}:
24	      +n = Nat.sub(B.Octets.len(o), tlen)
25	      Done{AdSplit{B.Octets.take(n, o), B.Octets.drop(n, o)}}
26	
27	def AdTag.split(+tlen: Nat, +o: B.Octets) -> Result<&2, &2, Cr.CrError, AdSplit>:
28	  ad.split.pick(Nat.is_lt(B.Octets.len(o), tlen), tlen, o)
29	
30	# the ciphertext with its tag appended
31	def AdTag.join(c: B.Octets, t: B.Octets) -> B.Octets:
32	  B.Octets.append(c, t)
33	
34	# Whether two tags are equal, every byte compared (no early exit)
35	def AdTag.is_eq(a: B.Octets, b: B.Octets) -> Bool:
36	  B.Octets.is_eq(a, b)