1	# XTEA (R. Needham, D. Wheeler, "Tea extensions", 1997, the routine
2	# "tean"): TEA with a different key schedule, a 64-bit block cipher with a
3	# 128-bit key. Each cycle is
4	#   y += (((z << 4) xor (z >> 5)) + z) xor (sum + k[sum & 3])
5	#   sum += delta
6	#   z += (((y << 4) xor (y >> 5)) + y) xor (sum + k[(sum >> 11) & 3])
7	# The key schedule computes each step's sum + k[..] once, as a step of
8	# tea.bend's (LcXteaY, LcXteaZ); decryption undoes the steps last to first,
9	# the paper's decoding, so decrypt(encrypt(b)) == b is provable for every key
10	# and block, as for TEA.
11	#
12	# The byte order of the words is a parameter, as for TEA: little-endian
13	# (the Linux kernel's "xtea") is LcXtea.key, big-endian LcXtea.key_be, and
14	# LcXtea.key_with takes the order and the number of cycles (32 recommended).
15	import Base
16	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
17	import ./legacy_ciphers.bend as L
18	import ./tea.bend as T
19	
20	# key word i & 3 of k0 .. k3
21	def xtea.kw(+i: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32) -> U32:
22	  L.lc.at([k0, k1, k2, k3], U32.to_nat(U32.and(3, i)))
23	
24	# XTEA's steps for n more cycles from sum s
25	def xtea.cycles(n: Nat, +s: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32) -> List<&2, T.LcTeaOp>:
26	  match n:
27	    case 0n:
28	      Nil{}
29	    case 1n+p:
30	      +s1 = U32.add(s, T.tea.delta())
31	      Con{T.LcXteaY{U32.add(s, xtea.kw(s, k0, k1, k2, k3))}, Con{T.LcXteaZ{U32.add(s1, xtea.kw(U32.shrn(s1, 11n), k0, k1, k2, k3))}, xtea.cycles(p, s1, k0, k1, k2, k3)}}
32	
33	# An XTEA key: the steps of the cipher (opaque; built by LcXtea.key)
34	type LcXteaKey is Data:
35	  LcXteaKey{ops: List<&2, T.LcTeaOp>}
36	
37	def xtea.key.pick(ok: Bool, +le: Bool, n: Nat, +xs: List<&2, U32>) -> Result<&2, &2, L.LcError, LcXteaKey>:
38	  match ok:
39	    case True{}:
40	      Done{LcXteaKey{T.tea.order(le, xtea.cycles(n, 0, T.tea.word(le, xs, 0n), T.tea.word(le, xs, 4n), T.tea.word(le, xs, 8n), T.tea.word(le, xs, 12n)))}}
41	    case False{}:
42	      Fail{L.LcBadKeyLength{B.len(xs)}}
43	
44	# The cipher
45	
46	# a 16-byte key, words in the order le picks (True: little-endian), and n
47	# cycles (32 recommended)
48	def LcXtea.key_with(le: Bool, n: Nat, o: B.Octets) -> Result<&2, &2, L.LcError, LcXteaKey>:
49	  +xs = B.Octets.to_list(o)
50	  xtea.key.pick(Nat.is_eq(B.len(xs), 16n), le, n, xs)
51	
52	# the named default: little-endian words (the Linux kernel's "xtea"), 32
53	# cycles
54	def LcXtea.key(o: B.Octets) -> Result<&2, &2, L.LcError, LcXteaKey>:
55	  LcXtea.key_with(True{}, 32n, o)
56	
57	# big-endian words, 32 cycles
58	def LcXtea.key_be(o: B.Octets) -> Result<&2, &2, L.LcError, LcXteaKey>:
59	  LcXtea.key_with(False{}, 32n, o)
60	
61	def LcXtea.encrypt(k: LcXteaKey, b: L.LcBlock64) -> L.LcBlock64:
62	  match k:
63	    case LcXteaKey{ops}:
64	      T.tea.run(ops, b)
65	
66	def LcXtea.decrypt(k: LcXteaKey, b: L.LcBlock64) -> L.LcBlock64:
67	  match k:
68	    case LcXteaKey{ops}:
69	      T.tea.unrun(ops, b)