1	# bend-osdev-cipher-modes: block-cipher modes of operation over any 128-bit
2	# block cipher. This file holds what every mode shares: the 128-bit block, the
3	# package's error type, and the byte-level helpers the modes are built from.
4	#
5	# The block cipher is a parameter. Every mode takes it as template arguments:
6	#   ~K: Data                          the cipher's key (an expanded key schedule)
7	#   ~enc: K -> CmBlock -> CmBlock     encryption of one block
8	#   ~dec: K -> CmBlock -> CmBlock     decryption of one block (CBC, XTS only)
9	# and the key itself as +k: K. The modes never look inside K, so they run on
10	# any cipher with 128-bit blocks; aes.bend supplies AES-128 and AES-256.
11	#
12	# A CmBlock is four 32-bit words, big-endian: w0 holds bytes 0 to 3 of the
13	# block, byte 0 in its top 8 bits. Every value of the type is a block (there is
14	# no out-of-range byte), so a cipher's "decryption inverts encryption" can be
15	# stated for every block. The type is open: a cipher adapter may build and
16	# match blocks directly.
17	import Base
18	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
19	import bend-osdev-word64@0.1.0.0/word64.bend as W
20	
21	type CmBlock is Data:
22	  CmBlock{w0: U32, w1: U32, w2: U32, w3: U32}
23	
24	# Every failure a mode can report
25	type CmError is Data:
26	  CmBadKeyLength{got: Nat}
27	  CmBadIvLength{got: Nat}
28	  CmBadTweakLength{got: Nat}
29	  CmBadNonceLength{got: Nat}
30	  CmBadTagLength{got: Nat}
31	  CmBadBlockSize{got: Nat}
32	  CmNotBlockMultiple{len: Nat}
33	  CmTooShort{len: Nat}
34	  CmTooLong{len: Nat}
35	  CmBadPadding{}
36	  CmTagMismatch{}
37	
38	# Blocks
39	
40	def CmBlock.zero() -> CmBlock:
41	  CmBlock{0, 0, 0, 0}
42	
43	def CmBlock.xor(a: CmBlock, b: CmBlock) -> CmBlock:
44	  match a b:
45	    case CmBlock{a0, a1, a2, a3} CmBlock{b0, b1, b2, b3}:
46	      CmBlock{U32.xor(a0, b0), U32.xor(a1, b1), U32.xor(a2, b2), U32.xor(a3, b3)}
47	
48	# Bytes and words (internal). Words are split into bytes and joined back by
49	# bit slicing (bend-osdev-word64's W64.bits), not by shifts and masks, so that
50	# the round trips can be proved for every word.
51	
52	# a byte (the low 8 bits of x), as bend-osdev-bytes masks it
53	def cm.byte(x: U32) -> U32:
54	  B.byte(x)
55	
56	def cm.bits8(b: U32) -> Word(8n):
57	  match b:
58	    case U32{w}:
59	      W.W64.bits.lo(8n, 24n, w)
60	
61	def cm.of8(s: Word(8n)) -> U32:
62	  U32{W.W64.bits.cat(8n, 24n, s, Word.zero(24n))}
63	
64	# the word with bytes a, b, c, d, most significant first
65	def cm.word(a: U32, b: U32, c: U32, d: U32) -> U32:
66	  U32{W.W64.bits.cat(8n, 24n, cm.bits8(d), W.W64.bits.cat(8n, 16n, cm.bits8(c), W.W64.bits.cat(8n, 8n, cm.bits8(b), cm.bits8(a))))}
67	
68	# the bytes of w, most significant first
69	def cm.b0(w: U32) -> U32:
70	  match w:
71	    case U32{x}:
72	      cm.of8(W.W64.bits.hi(8n, 8n, W.W64.bits.hi(8n, 16n, W.W64.bits.hi(8n, 24n, x))))
73	
74	def cm.b1(w: U32) -> U32:
75	  match w:
76	    case U32{x}:
77	      cm.of8(W.W64.bits.lo(8n, 8n, W.W64.bits.hi(8n, 16n, W.W64.bits.hi(8n, 24n, x))))
78	
79	def cm.b2(w: U32) -> U32:
80	  match w:
81	    case U32{x}:
82	      cm.of8(W.W64.bits.lo(8n, 16n, W.W64.bits.hi(8n, 24n, x)))
83	
84	def cm.b3(w: U32) -> U32:
85	  match w:
86	    case U32{x}:
87	      cm.of8(W.W64.bits.lo(8n, 24n, x))
88	
89	# the four bytes of w, most significant first, in front of rest
90	def cm.unword(+w: U32, rest: List<&2, U32>) -> List<&2, U32>:
91	  Con{cm.b0(w), Con{cm.b1(w), Con{cm.b2(w), Con{cm.b3(w), rest}}}}
92	
93	def cm.w0(b: CmBlock) -> U32:
94	  match b:
95	    case CmBlock{w0, w1, w2, w3}:
96	      w0
97	
98	def cm.w1(b: CmBlock) -> U32:
99	  match b:
100	    case CmBlock{w0, w1, w2, w3}:
101	      w1
102	
103	def cm.w2(b: CmBlock) -> U32:
104	  match b:
105	    case CmBlock{w0, w1, w2, w3}:
106	      w2
107	
108	def cm.w3(b: CmBlock) -> U32:
109	  match b:
110	    case CmBlock{w0, w1, w2, w3}:
111	      w3
112	
113	# the 16 bytes of a block in front of rest (always 16 cells, whatever b is)
114	def cm.bytes_onto(+b: CmBlock, rest: List<&2, U32>) -> List<&2, U32>:
115	  cm.unword(cm.w0(b), cm.unword(cm.w1(b), cm.unword(cm.w2(b), cm.unword(cm.w3(b), rest))))
116	
117	def cm.bytes_of(b: CmBlock) -> List<&2, U32>:
118	  cm.bytes_onto(b, Nil{})
119	
120	def cm.block16(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32, a5: U32, a6: U32, a7: U32, a8: U32, a9: U32, a10: U32, a11: U32, a12: U32, a13: U32, a14: U32, a15: U32) -> CmBlock:
121	  CmBlock{cm.word(a0, a1, a2, a3), cm.word(a4, a5, a6, a7), cm.word(a8, a9, a10, a11), cm.word(a12, a13, a14, a15)}
122	
123	def cm.block_of.full(xs: List<&2, U32>) -> CmBlock:
124	  match xs:
125	    case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Con{a8, Con{a9, Con{a10, Con{a11, Con{a12, Con{a13, Con{a14, Con{a15, t}}}}}}}}}}}}}}}}:
126	      cm.block16(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15)
127	    case _:
128	      CmBlock.zero()
129	
130	# the block of the first 16 bytes of xs, zero-filled if xs is shorter
131	def cm.block_of(xs: List<&2, U32>) -> CmBlock:
132	  cm.block_of.full(B.append(B.take(16n, xs), B.zeros(16n)))
133	
134	# A byte string as its whole blocks and the 0 to 15 bytes after them
135	type CmSplit is Data:
136	  CmSplit{blocks: List<&2, CmBlock>, tail: List<&2, U32>}
137	
138	def cm.split.cons(b: CmBlock, s: CmSplit) -> CmSplit:
139	  match s:
140	    case CmSplit{bs, t}:
141	      CmSplit{Con{b, bs}, t}
142	
143	def cm.split(+xs: List<&2, U32>) -> CmSplit:
144	  match xs:
145	    case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Con{a8, Con{a9, Con{a10, Con{a11, Con{a12, Con{a13, Con{a14, Con{a15, t}}}}}}}}}}}}}}}}:
146	      cm.split.cons(cm.block16(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15), cm.split(t))
147	    case _:
148	      CmSplit{Nil{}, xs}
149	
150	def cm.split.blocks(s: CmSplit) -> List<&2, CmBlock>:
151	  match s:
152	    case CmSplit{bs, t}:
153	      bs
154	
155	def cm.split.tail(s: CmSplit) -> List<&2, U32>:
156	  match s:
157	    case CmSplit{bs, t}:
158	      t
159	
160	# the bytes of the blocks bs, in front of rest
161	def cm.join_onto(bs: List<&2, CmBlock>, rest: List<&2, U32>) -> List<&2, U32>:
162	  match bs:
163	    case Nil{}:
164	      rest
165	    case Con{b, t}:
166	      cm.bytes_onto(b, cm.join_onto(t, rest))
167	
168	def cm.join(bs: List<&2, CmBlock>) -> List<&2, U32>:
169	  cm.join_onto(bs, Nil{})
170	
171	# byte-wise XOR, as long as the shorter list
172	def cm.xor_bytes(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
173	  match xs ys:
174	    case Con{a, s} Con{b, t}:
175	      Con{cm.byte(U32.xor(a, b)), cm.xor_bytes(s, t)}
176	    case _ _:
177	      Nil{}
178	
179	# the OR of the byte-wise XORs: 0 exactly when the lists agree, computed
180	# without stopping at the first difference
181	# The same, tail-recursive. Bend 2.0.37's runtime overflows its stack at some
182	# tens of thousands of nested non-tail calls, so the structural forms above,
183	# which the proofs reason about, cannot run on long messages; the modes run
184	# these instead, and PROOF.bend proves each equal to its structural form for
185	# every input.
186	
187	# the blocks of bs in reverse order, in front of acc
188	def cm.blocks.rev_onto(bs: List<&2, CmBlock>, acc: List<&2, CmBlock>) -> List<&2, CmBlock>:
189	  match bs:
190	    case Nil{}:
191	      acc
192	    case Con{b, t}:
193	      cm.blocks.rev_onto(t, Con{b, acc})
194	
195	def cm.blocks.len.go(bs: List<&2, CmBlock>, n: Nat) -> Nat:
196	  match bs:
197	    case Nil{}:
198	      n
199	    case Con{b, t}:
200	      cm.blocks.len.go(t, 1n+n)
201	
202	# the number of blocks (List.length)
203	def cm.blocks.len(bs: List<&2, CmBlock>) -> Nat:
204	  cm.blocks.len.go(bs, 0n)
205	
206	# xs, then ys (List.append)
207	def cm.blocks.append(xs: List<&2, CmBlock>, ys: List<&2, CmBlock>) -> List<&2, CmBlock>:
208	  cm.blocks.rev_onto(cm.blocks.rev_onto(xs, Nil{}), ys)
209	
210	# the blocks split so far are kept reversed in acc (cm.split)
211	def cm.split.go(+xs: List<&2, U32>, acc: List<&2, CmBlock>) -> CmSplit:
212	  match xs:
213	    case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Con{a8, Con{a9, Con{a10, Con{a11, Con{a12, Con{a13, Con{a14, Con{a15, t}}}}}}}}}}}}}}}}:
214	      cm.split.go(t, Con{cm.block16(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15), acc})
215	    case _:
216	      CmSplit{cm.blocks.rev_onto(acc, Nil{}), xs}
217	
218	def cm.split.fast(+xs: List<&2, U32>) -> CmSplit:
219	  cm.split.go(xs, Nil{})
220	
221	# the bytes of the blocks rs (last first) in front of acc
222	def cm.join.go(rs: List<&2, CmBlock>, acc: List<&2, U32>) -> List<&2, U32>:
223	  match rs:
224	    case Nil{}:
225	      acc
226	    case Con{b, t}:
227	      cm.join.go(t, cm.bytes_onto(b, acc))
228	
229	# cm.join_onto
230	def cm.join_onto.fast(bs: List<&2, CmBlock>, rest: List<&2, U32>) -> List<&2, U32>:
231	  cm.join.go(cm.blocks.rev_onto(bs, Nil{}), rest)
232	
233	def cm.xor_bytes.go(xs: List<&2, U32>, ys: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
234	  match xs ys:
235	    case Con{a, s} Con{b, t}:
236	      cm.xor_bytes.go(s, t, Con{cm.byte(U32.xor(a, b)), acc})
237	    case _ _:
238	      B.rev(acc)
239	
240	# cm.xor_bytes
241	def cm.xor_bytes.fast(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
242	  cm.xor_bytes.go(xs, ys, Nil{})
243	
244	def cm.diff(xs: List<&2, U32>, ys: List<&2, U32>, acc: U32) -> U32:
245	  match xs ys:
246	    case Con{a, s} Con{b, t}:
247	      cm.diff(s, t, U32.or(acc, cm.byte(U32.xor(a, b))))
248	    case Nil{} Nil{}:
249	      acc
250	    case _ _:
251	      1
252	
253	# equality of two byte lists with no early exit of the same length (a tag check)
254	def cm.ct_eq(xs: List<&2, U32>, ys: List<&2, U32>) -> Bool:
255	  U32.is_eq(cm.diff(xs, ys, 0), 0)
256	
257	# 0 for a 0 bit, all ones for a 1 bit (the low bit of b)
258	def cm.mask(b: U32) -> U32:
259	  U32.sub(0, U32.and(1, b))
260	
261	# Checks, as steps of a Result block
262	
263	def cm.check(ok: Bool, e: CmError) -> Result<&2, &2, CmError, Unit>:
264	  match ok:
265	    case True{}:
266	      Done{Unit{}}
267	    case False{}:
268	      Fail{e}
269	
270	# a 16-byte value as a block, or the error e
271	def cm.need_block.pick(ok: Bool, xs: List<&2, U32>, e: CmError) -> Result<&2, &2, CmError, CmBlock>:
272	  match ok:
273	    case True{}:
274	      Done{cm.block_of(xs)}
275	    case False{}:
276	      Fail{e}
277	
278	def cm.need_block(+xs: List<&2, U32>, e: CmError) -> Result<&2, &2, CmError, CmBlock>:
279	  cm.need_block.pick(Nat.is_eq(B.len(xs), 16n), xs, e)
280	
281	# Blocks as byte strings
282	
283	def CmBlock.to_octets(b: CmBlock) -> B.Octets:
284	  B.Octets.of_list(cm.bytes_of(b))
285	
286	def CmBlock.of_octets.pick(ok: Bool, xs: List<&2, U32>) -> Maybe<&2, CmBlock>:
287	  match ok:
288	    case True{}:
289	      Some{cm.block_of(xs)}
290	    case False{}:
291	      None{}
292	
293	# a 16-byte string as a block; None for any other length
294	def CmBlock.of_octets(o: B.Octets) -> Maybe<&2, CmBlock>:
295	  +xs = B.Octets.to_list(o)
296	  CmBlock.of_octets.pick(Nat.is_eq(B.len(xs), 16n), xs)
297	
298	def CmBlock.hex(b: CmBlock) -> String:
299	  B.hex(cm.bytes_of(b))