1	# Twofish (B. Schneier, J. Kelsey, D. Whiting, D. Wagner, C. Hall, N.
2	# Ferguson, "Twofish: A 128-Bit Block Cipher", AES submission, 1998): a
3	# 128-bit block cipher with 128-, 192- or 256-bit keys, as a cipher for
4	# cipher-modes' modes (~LcTwofishKey, ~LcTwofish.encrypt, ~LcTwofish.decrypt).
5	#
6	# Twofish reads the block as four little-endian words; a CmBlock holds
7	# big-endian words, so the cipher swaps each word's bytes on the way in and
8	# out. The key schedule turns the key into a list of steps, each one
9	# invertible: the byte swap, the whitening XORs, the sixteen rounds
10	#   (R0, R1, R2, R3) -> ((R2 xor F0) >>> 1, (R3 <<< 1) xor F1, R0, R1)
11	# with (F0, F1) = F(R0, R1, r), and the swap that undoes the last round's
12	# exchange of halves. Encryption runs the steps first to last; decryption
13	# undoes them last to first, the same function as the paper's decryption, and
14	# decrypt(encrypt(b)) == b is provable for every key and block: a round is
15	# undone whatever F is. The byte swaps and the 1-bit rotations a round undoes
16	# are computed on bits (legacy-ciphers.bend), so a proof computes through
17	# them; F (the key-dependent S-boxes, the MDS matrix, the PHT) and the key
18	# schedule use native word operations.
19	import Base
20	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
21	import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
22	import ./legacy_ciphers.bend as L
23	
24	# The permutations q0 and q1 (section 4.3.5): their 4-bit tables t0 .. t3
25	
26	def tf.q0.t() -> List<&2, U32>:
27	  [8, 1, 7, 13, 6, 15, 3, 2, 0, 11, 5, 9, 14, 12, 10, 4,
28	    14, 12, 11, 8, 1, 2, 3, 5, 15, 4, 10, 6, 7, 0, 9, 13,
29	    11, 10, 5, 14, 6, 13, 9, 0, 12, 8, 15, 3, 2, 4, 7, 1,
30	    13, 7, 15, 4, 1, 2, 6, 14, 9, 11, 3, 0, 8, 5, 12, 10]
31	
32	def tf.q1.t() -> List<&2, U32>:
33	  [2, 8, 11, 13, 15, 7, 6, 14, 3, 1, 9, 4, 0, 10, 12, 5,
34	    1, 14, 2, 11, 4, 12, 3, 7, 6, 13, 10, 5, 15, 9, 0, 8,
35	    4, 12, 7, 5, 1, 6, 9, 10, 0, 14, 13, 8, 2, 11, 3, 15,
36	    11, 9, 5, 1, 12, 3, 13, 14, 6, 4, 7, 15, 2, 0, 8, 10]
37	
38	# entry x of table i (0 to 3) of ts
39	def tf.t(+ts: List<&2, U32>, i: Nat, +x: U32) -> U32:
40	  L.lc.at(ts, Nat.add(Nat.mul(16n, i), U32.to_nat(x)))
41	
42	# a 4-bit value rotated right by one bit
43	def tf.ror4(+x: U32) -> U32:
44	  U32.and(15, U32.or(U32.shr(x), U32.shln(x, 3n)))
45	
46	def tf.q.half(+a: U32, +b: U32) -> U32:
47	  U32.xor(U32.xor(a, tf.ror4(b)), U32.and(15, U32.shln(a, 3n)))
48	
49	def tf.q.go(+ts: List<&2, U32>, +a2: U32, +b2: U32) -> U32:
50	  U32.add(U32.mul(16, tf.t(ts, 3n, tf.q.half(a2, b2))), tf.t(ts, 2n, U32.xor(a2, b2)))
51	
52	# q(x) from its tables
53	def tf.q.raw(+ts: List<&2, U32>, +x: U32) -> U32:
54	  +a0 = U32.shrn(x, 4n)
55	  +b0 = U32.and(15, x)
56	  tf.q.go(ts, tf.t(ts, 0n, U32.xor(a0, b0)), tf.t(ts, 1n, tf.q.half(a0, b0)))
57	
58	def tf.gen(~f: U32 -> U32, n: Nat, +i: U32) -> List<&2, U32>:
59	  match n:
60	    case 0n:
61	      Nil{}
62	    case 1n+p:
63	      Con{f(i), tf.gen(~f, p, U32.add(i, 1))}
64	
65	def tf.q0() -> L.LcTab:
66	  L.lc.tab(8n, tf.gen(~(x => tf.q.raw(tf.q0.t(), x)), 256n, 0))
67	
68	def tf.q1() -> L.LcTab:
69	  L.lc.tab(8n, tf.gen(~(x => tf.q.raw(tf.q1.t(), x)), 256n, 0))
70	
71	# The tables, built once per key (internal): q0, q1 and the MDS columns
72	type LcTfTabs is Data:
73	  LcTfTabs{q0: L.LcTab, q1: L.LcTab, m0: L.LcTab, m1: L.LcTab, m2: L.LcTab, m3: L.LcTab}
74	
75	def tf.q(t: LcTfTabs, one: Bool, +x: U32) -> U32:
76	  match t:
77	    case LcTfTabs{q0, q1, m0, m1, m2, m3}:
78	      match one:
79	        case True{}:
80	          L.lc.tab.get(8n, q1, x)
81	        case False{}:
82	          L.lc.tab.get(8n, q0, x)
83	
84	# GF(2^8) multiplication modulo the polynomial poly (with its x^8 term)
85	
86	def tf.xt(+a: U32, +poly: U32) -> U32:
87	  U32.and(255, U32.xor(U32.shl(a), U32.and(poly, U32.sub(0, U32.and(1, U32.shrn(a, 7n))))))
88	
89	def tf.gmul.go(n: Nat, +a: U32, +b: U32, +poly: U32, p: U32) -> U32:
90	  match n:
91	    case 0n:
92	      p
93	    case 1n+q:
94	      tf.gmul.go(q, tf.xt(a, poly), U32.shr(b), poly, U32.xor(p, U32.and(a, U32.sub(0, U32.and(1, b)))))
95	
96	def tf.gmul(+a: U32, +b: U32, +poly: U32) -> U32:
97	  tf.gmul.go(8n, a, b, poly, 0)
98	
99	# The MDS matrix (section 4.2), over GF(2^8) modulo x^8 + x^6 + x^5 + x^3 + 1;
100	# column j as a table: entry x is the word (MDS[0][j] x, .., MDS[3][j] x),
101	# row 0 in the low byte
102	
103	def tf.mds.m() -> List<&2, U32>:
104	  [1, 239, 91, 91,
105	    91, 239, 239, 1,
106	    239, 91, 1, 239,
107	    239, 1, 239, 91]
108	
109	def tf.mds.col(+j: Nat, +x: U32) -> U32:
110	  +m = tf.mds.m()
111	  L.lc.le(tf.gmul(L.lc.at(m, j), x, 105), tf.gmul(L.lc.at(m, Nat.add(4n, j)), x, 105), tf.gmul(L.lc.at(m, Nat.add(8n, j)), x, 105), tf.gmul(L.lc.at(m, Nat.add(12n, j)), x, 105))
112	
113	def tf.mds0() -> L.LcTab:
114	  L.lc.tab(8n, tf.gen(~(x => tf.mds.col(0n, x)), 256n, 0))
115	
116	def tf.mds1() -> L.LcTab:
117	  L.lc.tab(8n, tf.gen(~(x => tf.mds.col(1n, x)), 256n, 0))
118	
119	def tf.mds2() -> L.LcTab:
120	  L.lc.tab(8n, tf.gen(~(x => tf.mds.col(2n, x)), 256n, 0))
121	
122	def tf.mds3() -> L.LcTab:
123	  L.lc.tab(8n, tf.gen(~(x => tf.mds.col(3n, x)), 256n, 0))
124	
125	def tf.tables() -> LcTfTabs:
126	  LcTfTabs{tf.q0(), tf.q1(), tf.mds0(), tf.mds1(), tf.mds2(), tf.mds3()}
127	
128	def tf.mds(t: LcTfTabs, +y: U32) -> U32:
129	  match t:
130	    case LcTfTabs{q0, q1, m0, m1, m2, m3}:
131	      U32.xor(U32.xor(L.lc.tab.get(8n, m0, L.lc.byte(y, 0n)), L.lc.tab.get(8n, m1, L.lc.byte(y, 1n))), U32.xor(L.lc.tab.get(8n, m2, L.lc.byte(y, 2n)), L.lc.tab.get(8n, m3, L.lc.byte(y, 3n))))
132	
133	# The function h (section 4.3.2)
134	
135	# byte i of x through q (q1 if p_i), then XOR byte i of l
136	def tf.stage(+t: LcTfTabs, p0: Bool, p1: Bool, p2: Bool, p3: Bool, +x: U32, +l: U32) -> U32:
137	  L.lc.le(U32.xor(tf.q(t, p0, L.lc.byte(x, 0n)), L.lc.byte(l, 0n)), U32.xor(tf.q(t, p1, L.lc.byte(x, 1n)), L.lc.byte(l, 1n)), U32.xor(tf.q(t, p2, L.lc.byte(x, 2n)), L.lc.byte(l, 2n)), U32.xor(tf.q(t, p3, L.lc.byte(x, 3n)), L.lc.byte(l, 3n)))
138	
139	# the stages every key length shares: with L_1, with L_0, then q alone
140	def tf.h2(+t: LcTfTabs, +x: U32, +l0: U32, +l1: U32) -> U32:
141	  tf.mds(t, tf.stage(t, True{}, False{}, True{}, False{}, tf.stage(t, False{}, False{}, True{}, True{}, tf.stage(t, False{}, True{}, False{}, True{}, x, l1), l0), 0))
142	
143	def tf.h3(+t: LcTfTabs, +x: U32, +l0: U32, +l1: U32, +l2: U32) -> U32:
144	  tf.h2(t, tf.stage(t, True{}, True{}, False{}, False{}, x, l2), l0, l1)
145	
146	def tf.h4(+t: LcTfTabs, +x: U32, +l0: U32, +l1: U32, +l2: U32, +l3: U32) -> U32:
147	  tf.h3(t, tf.stage(t, True{}, False{}, False{}, True{}, x, l3), l0, l1, l2)
148	
149	# h(X, L) for L = L_0 .. L_(k-1), k = 2, 3 or 4
150	def tf.h(+t: LcTfTabs, +x: U32, l: List<&2, U32>) -> U32:
151	  match l:
152	    case Con{l0, Con{l1, Nil{}}}:
153	      tf.h2(t, x, l0, l1)
154	    case Con{l0, Con{l1, Con{l2, Nil{}}}}:
155	      tf.h3(t, x, l0, l1, l2)
156	    case Con{l0, Con{l1, Con{l2, Con{l3, more}}}}:
157	      tf.h4(t, x, l0, l1, l2, l3)
158	    case _:
159	      0
160	
161	# The function F (section 4.3): g(X) = h(X, S), then the PHT and the round
162	# subkeys K_(2r+8), K_(2r+9); F0 and F1 as an LcBlock64
163	
164	def tf.f(+t: LcTfTabs, +s: List<&2, U32>, r0: U32, r1: U32, ka: U32, kb: U32) -> L.LcBlock64:
165	  +t0 = tf.h(t, r0, s)
166	  +t1 = tf.h(t, L.lc.rotl(r1, 8n), s)
167	  L.LcBlock64{U32.add(U32.add(t0, t1), ka), U32.add(U32.add(t0, U32.add(t1, t1)), kb)}
168	
169	def tf.f0(x: L.LcBlock64) -> U32:
170	  match x:
171	    case L.LcBlock64{a, b}:
172	      a
173	
174	def tf.f1(x: L.LcBlock64) -> U32:
175	  match x:
176	    case L.LcBlock64{a, b}:
177	      b
178	
179	# The steps of the cipher (internal)
180	type LcTfOp is Data:
181	  LcTfBswap{}
182	  LcTfWhite{k: M.CmBlock}
183	  LcTfRound{t: LcTfTabs, s: List<&2, U32>, ka: U32, kb: U32}
184	  LcTfSwap{}
185	
186	def tf.op(o: LcTfOp, s: M.CmBlock) -> M.CmBlock:
187	  match o:
188	    case LcTfBswap{}:
189	      match s:
190	        case M.CmBlock{a, b, c, d}:
191	          M.CmBlock{L.lc.bswap.bits(a), L.lc.bswap.bits(b), L.lc.bswap.bits(c), L.lc.bswap.bits(d)}
192	    case LcTfWhite{k}:
193	      M.CmBlock.xor(s, k)
194	    case LcTfRound{tb, sk, ka, kb}:
195	      match s:
196	        case M.CmBlock{+r0, +r1, r2, r3}:
197	          +f = tf.f(tb, sk, r0, r1, ka, kb)
198	          M.CmBlock{L.lc.rotl31.bits(U32.xor(r2, tf.f0(f))), U32.xor(L.lc.rotl1.bits(r3), tf.f1(f)), r0, r1}
199	    case LcTfSwap{}:
200	      match s:
201	        case M.CmBlock{a, b, c, d}:
202	          M.CmBlock{c, d, a, b}
203	
204	# the step undone
205	def tf.unop(o: LcTfOp, s: M.CmBlock) -> M.CmBlock:
206	  match o:
207	    case LcTfBswap{}:
208	      match s:
209	        case M.CmBlock{a, b, c, d}:
210	          M.CmBlock{L.lc.bswap.bits(a), L.lc.bswap.bits(b), L.lc.bswap.bits(c), L.lc.bswap.bits(d)}
211	    case LcTfWhite{k}:
212	      M.CmBlock.xor(s, k)
213	    case LcTfRound{tb, sk, ka, kb}:
214	      match s:
215	        case M.CmBlock{a, b, +c, +d}:
216	          +f = tf.f(tb, sk, c, d, ka, kb)
217	          M.CmBlock{c, d, U32.xor(L.lc.rotl1.bits(a), tf.f0(f)), L.lc.rotl31.bits(U32.xor(b, tf.f1(f)))}
218	    case LcTfSwap{}:
219	      match s:
220	        case M.CmBlock{a, b, c, d}:
221	          M.CmBlock{c, d, a, b}
222	
223	def tf.run(os: List<&2, LcTfOp>, s: M.CmBlock) -> M.CmBlock:
224	  match os:
225	    case Nil{}:
226	      s
227	    case Con{o, t}:
228	      tf.run(t, tf.op(o, s))
229	
230	def tf.unrun(os: List<&2, LcTfOp>, s: M.CmBlock) -> M.CmBlock:
231	  match os:
232	    case Nil{}:
233	      s
234	    case Con{o, t}:
235	      tf.unop(o, tf.unrun(t, s))
236	
237	# The key schedule (section 4.3)
238	
239	# the little-endian words of the key bytes xs, every other one from word i
240	def tf.words(n: Nat, +xs: List<&2, U32>, +i: Nat) -> List<&2, U32>:
241	  match n:
242	    case 0n:
243	      Nil{}
244	    case 1n+p:
245	      +j = Nat.mul(4n, i)
246	      Con{L.lc.le(L.lc.at(xs, j), L.lc.at(xs, Nat.add(j, 1n)), L.lc.at(xs, Nat.add(j, 2n)), L.lc.at(xs, Nat.add(j, 3n))), tf.words(p, xs, Nat.add(i, 2n))}
247	
248	# The RS matrix (section 4.3), over GF(2^8) modulo x^8 + x^6 + x^3 + x^2 + 1
249	def tf.rs() -> List<&2, U32>:
250	  [1, 164, 85, 135, 90, 88, 219, 158,
251	    164, 86, 130, 243, 30, 198, 104, 229,
252	    2, 161, 252, 193, 71, 174, 61, 25,
253	    164, 85, 135, 90, 88, 219, 158, 3]
254	
255	# row r of RS times the 8 key bytes from byte j
256	def tf.rs.row(n: Nat, +xs: List<&2, U32>, +r: Nat, +j: Nat, +c: Nat, acc: U32) -> U32:
257	  match n:
258	    case 0n:
259	      acc
260	    case 1n+p:
261	      tf.rs.row(p, xs, r, j, Nat.add(c, 1n), U32.xor(acc, tf.gmul(L.lc.at(tf.rs(), Nat.add(Nat.mul(8n, r), c)), L.lc.at(xs, Nat.add(j, c)), 77)))
262	
263	# S_i: RS times key bytes 8i .. 8i + 7
264	def tf.s_word(+xs: List<&2, U32>, +i: Nat) -> U32:
265	  +j = Nat.mul(8n, i)
266	  L.lc.le(tf.rs.row(8n, xs, 0n, j, 0n, 0), tf.rs.row(8n, xs, 1n, j, 0n, 0), tf.rs.row(8n, xs, 2n, j, 0n, 0), tf.rs.row(8n, xs, 3n, j, 0n, 0))
267	
268	# S = (S_(k-1), .., S_0), the k words of the key-dependent S-boxes
269	def tf.svec(n: Nat, +xs: List<&2, U32>, +i: Nat, acc: List<&2, U32>) -> List<&2, U32>:
270	  match n:
271	    case 0n:
272	      acc
273	    case 1n+p:
274	      tf.svec(p, xs, Nat.add(i, 1n), Con{tf.s_word(xs, i), acc})
275	
276	# K_(2i) and K_(2i+1) as an LcBlock64
277	def tf.kpair(+t: LcTfTabs, +me: List<&2, U32>, +mo: List<&2, U32>, +i: U32) -> L.LcBlock64:
278	  +a = tf.h(t, U32.mul(U32.mul(2, i), 16843009), me)
279	  +b = L.lc.rotl(tf.h(t, U32.mul(U32.add(U32.mul(2, i), 1), 16843009), mo), 8n)
280	  L.LcBlock64{U32.add(a, b), L.lc.rotl(U32.add(a, U32.add(b, b)), 9n)}
281	
282	# the rounds' steps from round r, with the pairs K_(2r+8), K_(2r+9) in ks
283	def tf.rounds(ks: List<&2, L.LcBlock64>, +t: LcTfTabs, +s: List<&2, U32>) -> List<&2, LcTfOp>:
284	  match ks:
285	    case Nil{}:
286	      Nil{}
287	    case Con{L.LcBlock64{a, b}, rest}:
288	      Con{LcTfRound{t, s, a, b}, tf.rounds(rest, t, s)}
289	
290	def tf.kpairs(n: Nat, +t: LcTfTabs, +me: List<&2, U32>, +mo: List<&2, U32>, +i: U32) -> List<&2, L.LcBlock64>:
291	  match n:
292	    case 0n:
293	      Nil{}
294	    case 1n+p:
295	      Con{tf.kpair(t, me, mo, i), tf.kpairs(p, t, me, mo, U32.add(i, 1))}
296	
297	def tf.white.le(a: L.LcBlock64, b: L.LcBlock64) -> LcTfOp:
298	  match a b:
299	    case L.LcBlock64{k0, k1} L.LcBlock64{k2, k3}:
300	      LcTfWhite{M.CmBlock{k0, k1, k2, k3}}
301	
302	def tf.append(xs: List<&2, LcTfOp>, ys: List<&2, LcTfOp>) -> List<&2, LcTfOp>:
303	  match xs:
304	    case Nil{}:
305	      ys
306	    case Con{h, t}:
307	      Con{h, tf.append(t, ys)}
308	
309	# the steps from the subkey pairs (K_0, K_1) .. (K_38, K_39)
310	def tf.ops(ks: List<&2, L.LcBlock64>, +t: LcTfTabs, +s: List<&2, U32>) -> List<&2, LcTfOp>:
311	  match ks:
312	    case Con{p0, Con{p1, Con{p2, Con{p3, rest}}}}:
313	      Con{LcTfBswap{}, Con{tf.white.le(p0, p1), tf.append(tf.rounds(rest, t, s), [LcTfSwap{}, tf.white.le(p2, p3), LcTfBswap{}])}}
314	    case _:
315	      Nil{}
316	
317	# A Twofish key: the steps of the cipher (opaque; built by LcTwofish.key)
318	type LcTwofishKey is Data:
319	  LcTwofishKey{ops: List<&2, LcTfOp>}
320	
321	# the key from k = 2, 3 or 4 64-bit words of key bytes xs
322	def tf.key(+k: Nat, +xs: List<&2, U32>) -> LcTwofishKey:
323	  +t = tf.tables()
324	  LcTwofishKey{tf.ops(tf.kpairs(20n, t, tf.words(k, xs, 0n), tf.words(k, xs, 1n), 0), t, tf.svec(k, xs, 0n, Nil{}))}
325	
326	def tf.key.pick(n16: Bool, n24: Bool, n32: Bool, +xs: List<&2, U32>) -> Result<&2, &2, L.LcError, LcTwofishKey>:
327	  match n16 n24 n32:
328	    case True{} _ _:
329	      Done{tf.key(2n, xs)}
330	    case False{} True{} _:
331	      Done{tf.key(3n, xs)}
332	    case False{} False{} True{}:
333	      Done{tf.key(4n, xs)}
334	    case False{} False{} False{}:
335	      Fail{L.LcBadKeyLength{B.len(xs)}}
336	
337	# The cipher
338	
339	# a 16-, 24- or 32-byte key (Twofish-128, -192, -256, by its length)
340	def LcTwofish.key(o: B.Octets) -> Result<&2, &2, L.LcError, LcTwofishKey>:
341	  +xs = B.Octets.to_list(o)
342	  +n = B.len(xs)
343	  tf.key.pick(Nat.is_eq(n, 16n), Nat.is_eq(n, 24n), Nat.is_eq(n, 32n), xs)
344	
345	# the key padded with zero bytes to 16, 24 or 32 bytes (section 4.3: keys
346	# shorter than 256 bits are padded with zeros to the next defined length)
347	def tf.pad.pick(n16: Bool, n24: Bool, n32: Bool, +n: Nat, +xs: List<&2, U32>) -> Result<&2, &2, L.LcError, LcTwofishKey>:
348	  match n16 n24 n32:
349	    case True{} _ _:
350	      Done{tf.key(2n, B.append(xs, B.zeros(Nat.sub(16n, n))))}
351	    case False{} True{} _:
352	      Done{tf.key(3n, B.append(xs, B.zeros(Nat.sub(24n, n))))}
353	    case False{} False{} True{}:
354	      Done{tf.key(4n, B.append(xs, B.zeros(Nat.sub(32n, n))))}
355	    case False{} False{} False{}:
356	      Fail{L.LcBadKeyLength{n}}
357	
358	# a key of 1 to 32 bytes, zero-padded as the specification says
359	def LcTwofish.key_padded(o: B.Octets) -> Result<&2, &2, L.LcError, LcTwofishKey>:
360	  +xs = B.Octets.to_list(o)
361	  +n = B.len(xs)
362	  tf.pad.pick(Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, 16n)), Nat.is_le(n, 24n), Nat.is_le(n, 32n), n, xs)
363	
364	def LcTwofish.encrypt(k: LcTwofishKey, b: M.CmBlock) -> M.CmBlock:
365	  match k:
366	    case LcTwofishKey{ops}:
367	      tf.run(ops, b)
368	
369	def LcTwofish.decrypt(k: LcTwofishKey, b: M.CmBlock) -> M.CmBlock:
370	  match k:
371	    case LcTwofishKey{ops}:
372	      tf.unrun(ops, b)