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