1	# bend-osdev-legacy-ciphers: the older block and stream ciphers a kernel's
2	# crypto layer still carries (DES, 3DES, SM4, Camellia, Serpent, Twofish,
3	# ARIA, CAST-256, Blowfish, CAST-128, TEA, XTEA, FCrypt, RC4), one file per
4	# cipher. This file holds what they share: the package's error type, the
5	# 64-bit block, word helpers, tables, and Feistel rounds over any round
6	# function.
7	#
8	# The 128-bit block ciphers (sm4.bend, camellia.bend, serpent.bend,
9	# twofish.bend, aria.bend, cast6.bend) work on cipher-modes' CmBlock, so they
10	# plug into every mode there as the template arguments ~K, ~enc, ~dec. The
11	# 64-bit ones (des.bend, tdes.bend, blowfish.bend, cast5.bend, tea.bend,
12	# xtea.bend, fcrypt.bend) work on LcBlock64 below, and the 64-bit modes in
13	# modes64.bend.
14	import Base
15	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
16	import bend-osdev-word64@0.1.0.0/word64.bend as W
17	
18	# Every failure the package reports
19	type LcError is Data:
20	  LcBadKeyLength{got: Nat}
21	  LcBadIvLength{got: Nat}
22	  LcNotBlockMultiple{len: Nat}
23	
24	# A 64-bit block: two 32-bit words, big-endian (hi holds bytes 0 to 3, byte 0
25	# in its top 8 bits). Every value of the type is a block, so "decryption
26	# inverts encryption" can be stated for every block. The type is open: a
27	# cipher may build and match blocks directly.
28	type LcBlock64 is Data:
29	  LcBlock64{hi: U32, lo: U32}
30	
31	def LcBlock64.zero() -> LcBlock64:
32	  LcBlock64{0, 0}
33	
34	def LcBlock64.xor(a: LcBlock64, b: LcBlock64) -> LcBlock64:
35	  match a b:
36	    case LcBlock64{a0, a1} LcBlock64{b0, b1}:
37	      LcBlock64{U32.xor(a0, b0), U32.xor(a1, b1)}
38	
39	# Words, natively: fast, for the parts of a cipher no proof inverts (round
40	# functions and key schedules). n is 1 to 31.
41	
42	def lc.rotl(+x: U32, +n: Nat) -> U32:
43	  U32.or(U32.shln(x, n), U32.shrn(x, Nat.sub(32n, n)))
44	
45	# byte n of x, counting from the least significant (n = 0 to 3)
46	def lc.byte(x: U32, n: Nat) -> U32:
47	  U32.and(255, U32.shrn(x, Nat.mul(8n, n)))
48	
49	# the word with bytes a (most significant), b, c, d
50	def lc.be(a: U32, b: U32, c: U32, d: U32) -> U32:
51	  U32.or(U32.or(U32.shln(U32.and(255, a), 24n), U32.shln(U32.and(255, b), 16n)), U32.or(U32.shln(U32.and(255, c), 8n), U32.and(255, d)))
52	
53	# the word with bytes a (least significant), b, c, d
54	def lc.le(a: U32, b: U32, c: U32, d: U32) -> U32:
55	  lc.be(d, c, b, a)
56	
57	# bit i of x (0 the least significant), as 0 or 1
58	def lc.bit(x: U32, i: Nat) -> U32:
59	  U32.and(1, U32.shrn(x, i))
60	
61	# element n of a list of words (0 past the end)
62	def lc.at(xs: List<&2, U32>, n: Nat) -> U32:
63	  match xs:
64	    case Nil{}:
65	      0
66	    case Con{h, t}:
67	      match n:
68	        case 0n:
69	          h
70	        case 1n+p:
71	          lc.at(t, p)
72	
73	# Words as bits: for the steps a proof must undo (rotations, byte swaps, bit
74	# permutations). They are built by slicing a word's bits (bend-osdev-word64's
75	# W64.bits), so a proof about a symbolic word computes through them; they are
76	# slower than the native forms above.
77	
78	# the (m + n)-bit word w rotated left by n
79	def lc.wrotl(+m: Nat, +n: Nat, +w: Word(Nat.add(m, n))) -> Word(Nat.add(n, m)):
80	  W.W64.bits.cat(n, m, W.W64.bits.hi(m, n, w), W.W64.bits.lo(m, n, w))
81	
82	def lc.rotl1.bits(x: U32) -> U32:
83	  match x:
84	    case U32{+w}:
85	      U32{lc.wrotl(31n, 1n, w)}
86	
87	def lc.rotl3.bits(x: U32) -> U32:
88	  match x:
89	    case U32{+w}:
90	      U32{lc.wrotl(29n, 3n, w)}
91	
92	def lc.rotl5.bits(x: U32) -> U32:
93	  match x:
94	    case U32{+w}:
95	      U32{lc.wrotl(27n, 5n, w)}
96	
97	def lc.rotl7.bits(x: U32) -> U32:
98	  match x:
99	    case U32{+w}:
100	      U32{lc.wrotl(25n, 7n, w)}
101	
102	def lc.rotl10.bits(x: U32) -> U32:
103	  match x:
104	    case U32{+w}:
105	      U32{lc.wrotl(22n, 10n, w)}
106	
107	def lc.rotl13.bits(x: U32) -> U32:
108	  match x:
109	    case U32{+w}:
110	      U32{lc.wrotl(19n, 13n, w)}
111	
112	def lc.rotl19.bits(x: U32) -> U32:
113	  match x:
114	    case U32{+w}:
115	      U32{lc.wrotl(13n, 19n, w)}
116	
117	def lc.rotl22.bits(x: U32) -> U32:
118	  match x:
119	    case U32{+w}:
120	      U32{lc.wrotl(10n, 22n, w)}
121	
122	def lc.rotl25.bits(x: U32) -> U32:
123	  match x:
124	    case U32{+w}:
125	      U32{lc.wrotl(7n, 25n, w)}
126	
127	def lc.rotl27.bits(x: U32) -> U32:
128	  match x:
129	    case U32{+w}:
130	      U32{lc.wrotl(5n, 27n, w)}
131	
132	def lc.rotl29.bits(x: U32) -> U32:
133	  match x:
134	    case U32{+w}:
135	      U32{lc.wrotl(3n, 29n, w)}
136	
137	def lc.rotl31.bits(x: U32) -> U32:
138	  match x:
139	    case U32{+w}:
140	      U32{lc.wrotl(1n, 31n, w)}
141	
142	# the low 8 bits of a word, as bits, and the byte with these bits
143	def lc.bits8(b: U32) -> Word(8n):
144	  match b:
145	    case U32{w}:
146	      W.W64.bits.lo(8n, 24n, w)
147	
148	def lc.of8(s: Word(8n)) -> U32:
149	  U32{W.W64.bits.cat(8n, 24n, s, Word.zero(24n))}
150	
151	# the word with bytes a (most significant), b, c, d, by bits
152	def lc.be.bits(a: U32, b: U32, c: U32, d: U32) -> U32:
153	  U32{W.W64.bits.cat(8n, 24n, lc.bits8(d), W.W64.bits.cat(8n, 16n, lc.bits8(c), W.W64.bits.cat(8n, 8n, lc.bits8(b), lc.bits8(a))))}
154	
155	# the bytes of w, by bits: b0 the most significant
156	def lc.b0.bits(w: U32) -> U32:
157	  match w:
158	    case U32{x}:
159	      lc.of8(W.W64.bits.hi(8n, 8n, W.W64.bits.hi(8n, 16n, W.W64.bits.hi(8n, 24n, x))))
160	
161	def lc.b1.bits(w: U32) -> U32:
162	  match w:
163	    case U32{x}:
164	      lc.of8(W.W64.bits.lo(8n, 8n, W.W64.bits.hi(8n, 16n, W.W64.bits.hi(8n, 24n, x))))
165	
166	def lc.b2.bits(w: U32) -> U32:
167	  match w:
168	    case U32{x}:
169	      lc.of8(W.W64.bits.lo(8n, 16n, W.W64.bits.hi(8n, 24n, x)))
170	
171	def lc.b3.bits(w: U32) -> U32:
172	  match w:
173	    case U32{x}:
174	      lc.of8(W.W64.bits.lo(8n, 24n, x))
175	
176	# the word with its bytes in reverse order (big-endian to little-endian)
177	def lc.bswap.bits(+w: U32) -> U32:
178	  lc.be.bits(lc.b3.bits(w), lc.b2.bits(w), lc.b1.bits(w), lc.b0.bits(w))
179	
180	# the bits of a word, most significant first, in front of acc
181	def lc.msb.go(n: Nat, w: Word(n), acc: List<&2, Bool>) -> List<&2, Bool>:
182	  match n:
183	    case 0n:
184	      acc
185	    case 1n+p:
186	      match w:
187	        case WCon{h, t}:
188	          lc.msb.go(p, t, Con{h, acc})
189	
190	def lc.msb(x: U32, acc: List<&2, Bool>) -> List<&2, Bool>:
191	  match x:
192	    case U32{w}:
193	      lc.msb.go(32n, w, acc)
194	
195	# bs reversed, in front of acc
196	def lc.rev_bits(bs: List<&2, Bool>, acc: List<&2, Bool>) -> List<&2, Bool>:
197	  match bs:
198	    case Nil{}:
199	      acc
200	    case Con{h, t}:
201	      lc.rev_bits(t, Con{h, acc})
202	
203	# all but the first n of bs
204	def lc.drop_bits(n: Nat, bs: List<&2, Bool>) -> List<&2, Bool>:
205	  match n:
206	    case 0n:
207	      bs
208	    case 1n+p:
209	      match bs:
210	        case Nil{}:
211	          Nil{}
212	        case Con{h, t}:
213	          lc.drop_bits(p, t)
214	
215	# the n-bit word whose bits, least significant first, are the first n of bs
216	# (False past the end)
217	def lc.word_lsb(n: Nat, bs: List<&2, Bool>) -> Word(n):
218	  match n:
219	    case 0n:
220	      WNil{}
221	    case 1n+p:
222	      match bs:
223	        case Nil{}:
224	          WCon{False{}, lc.word_lsb(p, Nil{})}
225	        case Con{h, t}:
226	          WCon{h, lc.word_lsb(p, t)}
227	
228	# the element i of bs (False past the end)
229	def lc.nth(bs: List<&2, Bool>, i: Nat) -> Bool:
230	  match bs:
231	    case Nil{}:
232	      False{}
233	    case Con{h, t}:
234	      match i:
235	        case 0n:
236	          h
237	        case 1n+p:
238	          lc.nth(t, p)
239	
240	# Tables: a complete binary tree of words, read by the bits of an index. Bend
241	# 2.0.37 recomputes a table def at every call, so a cipher builds its tables
242	# once, when its key is made, and keeps them in the key.
243	
244	type LcTab is Data:
245	  LcLeaf{v: U32}
246	  LcNode{l: LcTab, r: LcTab}
247	
248	def lc.tab.leaves(xs: List<&2, U32>) -> List<&2, LcTab>:
249	  match xs:
250	    case Nil{}:
251	      Nil{}
252	    case Con{h, t}:
253	      Con{LcLeaf{h}, lc.tab.leaves(t)}
254	
255	def lc.tab.pairs(ts: List<&2, LcTab>) -> List<&2, LcTab>:
256	  match ts:
257	    case Con{a, Con{b, t}}:
258	      Con{LcNode{a, b}, lc.tab.pairs(t)}
259	    case _:
260	      Nil{}
261	
262	def lc.tab.up(n: Nat, ts: List<&2, LcTab>) -> List<&2, LcTab>:
263	  match n:
264	    case 0n:
265	      ts
266	    case 1n+p:
267	      lc.tab.up(p, lc.tab.pairs(ts))
268	
269	def lc.tab.root(ts: List<&2, LcTab>) -> LcTab:
270	  match ts:
271	    case Nil{}:
272	      LcLeaf{0}
273	    case Con{h, t}:
274	      h
275	
276	# the table of the 2^d words xs (entry i is element i)
277	def lc.tab(d: Nat, xs: List<&2, U32>) -> LcTab:
278	  lc.tab.root(lc.tab.up(d, lc.tab.leaves(xs)))
279	
280	def lc.tab.pick(one: Bool, l: LcTab, r: LcTab) -> LcTab:
281	  match one:
282	    case True{}:
283	      r
284	    case False{}:
285	      l
286	
287	# entry i of a table of depth d (i below 2^d)
288	def lc.tab.get(d: Nat, t: LcTab, +i: U32) -> U32:
289	  match d:
290	    case 0n:
291	      match t:
292	        case LcLeaf{v}:
293	          v
294	        case LcNode{l, r}:
295	          0
296	    case 1n+(+p):
297	      match t:
298	        case LcLeaf{v}:
299	          v
300	        case LcNode{l, r}:
301	          lc.tab.get(p, lc.tab.pick(U32.is_eq(lc.bit(i, p), 1), l, r), i)
302	
303	# the bits of i (below 2^d) that pick its entry, most significant first
304	def lc.tab.path(d: Nat, +i: U32) -> List<&2, Bool>:
305	  match d:
306	    case 0n:
307	      Nil{}
308	    case 1n+(+p):
309	      Con{U32.is_eq(lc.bit(i, p), 1), lc.tab.path(p, i)}
310	
311	def lc.tab.set.go(t: LcTab, path: List<&2, Bool>, v: U32) -> LcTab:
312	  match t:
313	    case LcLeaf{w}:
314	      LcLeaf{v}
315	    case LcNode{l, r}:
316	      match path:
317	        case Nil{}:
318	          LcNode{l, r}
319	        case Con{b, rest}:
320	          match b:
321	            case True{}:
322	              LcNode{l, lc.tab.set.go(r, rest, v)}
323	            case False{}:
324	              LcNode{lc.tab.set.go(l, rest, v), r}
325	
326	# entry i of a table of depth d set to v (i below 2^d)
327	def lc.tab.set(d: Nat, t: LcTab, +i: U32, v: U32) -> LcTab:
328	  lc.tab.set.go(t, lc.tab.path(d, i), v)
329	
330	# Feistel rounds over any round function f (CAST-128, FCrypt): the round with
331	# round key k is (L, R) -> (R, L xor f(k, R)), and it is undone by
332	# (L', R') -> (R' xor f(k, L'), L') whatever f is, so a list of rounds is
333	# undone by its rounds undone in reverse order (PROOF.bend: fe_*)
334	
335	def lc.fe.step(~RK: Data, ~f: RK -> U32 -> U32, k: RK, b: LcBlock64) -> LcBlock64:
336	  match b:
337	    case LcBlock64{l, +r}:
338	      LcBlock64{r, U32.xor(l, f(k, r))}
339	
340	def lc.fe.unstep(~RK: Data, ~f: RK -> U32 -> U32, k: RK, b: LcBlock64) -> LcBlock64:
341	  match b:
342	    case LcBlock64{+l, r}:
343	      LcBlock64{U32.xor(r, f(k, l)), l}
344	
345	def lc.fe.run(~RK: Data, ~f: RK -> U32 -> U32, ks: List<&2, RK>, b: LcBlock64) -> LcBlock64:
346	  match ks:
347	    case Nil{}:
348	      b
349	    case Con{k, t}:
350	      lc.fe.run(~RK, ~f, t, lc.fe.step(~RK, ~f, k, b))
351	
352	def lc.fe.unrun(~RK: Data, ~f: RK -> U32 -> U32, ks: List<&2, RK>, b: LcBlock64) -> LcBlock64:
353	  match ks:
354	    case Nil{}:
355	      b
356	    case Con{k, t}:
357	      lc.fe.unstep(~RK, ~f, k, lc.fe.unrun(~RK, ~f, t, b))
358	
359	# the two halves exchanged
360	def lc.swap(b: LcBlock64) -> LcBlock64:
361	  match b:
362	    case LcBlock64{h, l}:
363	      LcBlock64{l, h}
364	
365	# Blocks as byte strings (built on bits, so the round trip is provable)
366	
367	# the 8 bytes of a block in front of rest
368	def lc.block_bytes(b: LcBlock64, rest: List<&2, U32>) -> List<&2, U32>:
369	  match b:
370	    case LcBlock64{+hi, +lo}:
371	      Con{lc.b0.bits(hi), Con{lc.b1.bits(hi), Con{lc.b2.bits(hi), Con{lc.b3.bits(hi), Con{lc.b0.bits(lo), Con{lc.b1.bits(lo), Con{lc.b2.bits(lo), Con{lc.b3.bits(lo), rest}}}}}}}}
372	
373	def lc.block8(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32, a5: U32, a6: U32, a7: U32) -> LcBlock64:
374	  LcBlock64{lc.be.bits(a0, a1, a2, a3), lc.be.bits(a4, a5, a6, a7)}
375	
376	def LcBlock64.to_octets(b: LcBlock64) -> B.Octets:
377	  B.Octets.of_list(lc.block_bytes(b, Nil{}))
378	
379	def lc.block_of(xs: List<&2, U32>) -> Maybe<&2, LcBlock64>:
380	  match xs:
381	    case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Nil{}}}}}}}}}:
382	      Some{lc.block8(a0, a1, a2, a3, a4, a5, a6, a7)}
383	    case _:
384	      None{}
385	
386	# an 8-byte string as a block (big-endian words); None for any other length
387	def LcBlock64.of_octets(o: B.Octets) -> Maybe<&2, LcBlock64>:
388	  lc.block_of(B.Octets.to_list(o))
389	
390	def LcBlock64.hex(b: LcBlock64) -> String:
391	  B.hex(lc.block_bytes(b, Nil{}))