1	# Byte-string helpers the modes and MACs share: XOR of two byte strings, a
2	# byte repeated, and a message cut into pieces of a block size.
3	import Base
4	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
5	
6	# xs xor ys, element by element, over xs's length (a missing element of ys
7	# counts as 0)
8	def cr.oct.xorl(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
9	  match xs:
10	    case Nil{}:
11	      Nil{}
12	    case Con{x, xt}:
13	      match ys:
14	        case Nil{}:
15	          Con{U32.xor(x, 0), cr.oct.xorl(xt, Nil{})}
16	        case Con{y, yt}:
17	          Con{U32.xor(x, y), cr.oct.xorl(xt, yt)}
18	
19	# a xor b, byte by byte, over a's length (b's missing bytes count as 0)
20	def CrOct.xor(a: B.Octets, b: B.Octets) -> B.Octets:
21	  B.Octets.of_list(cr.oct.xorl(B.Octets.to_list(a), B.Octets.to_list(b)))
22	
23	def cr.oct.rep(n: Nat, +b: U32) -> List<&2, U32>:
24	  match n:
25	    case 0n:
26	      Nil{}
27	    case 1n+p:
28	      Con{b, cr.oct.rep(p, b)}
29	
30	# the byte b, n times
31	def CrOct.rep(n: Nat, +b: U32) -> B.Octets:
32	  B.Octets.of_list(cr.oct.rep(n, b))
33	
34	def cr.oct.rev(xs: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
35	  match xs:
36	    case Nil{}:
37	      acc
38	    case Con{h, t}:
39	      cr.oct.rev(t, Con{h, acc})
40	
41	def cr.oct.revs(xs: List<&2, List<&2, U32>>, acc: List<&2, List<&2, U32>>) -> List<&2, List<&2, U32>>:
42	  match xs:
43	    case Nil{}:
44	      acc
45	    case Con{h, t}:
46	      cr.oct.revs(t, Con{h, acc})
47	
48	def cr.oct.flush(cur: List<&2, U32>, acc: List<&2, List<&2, U32>>) -> List<&2, List<&2, U32>>:
49	  match cur:
50	    case Nil{}:
51	      acc
52	    case Con{h, t}:
53	      Con{cr.oct.rev(Con{h, t}, Nil{}), acc}
54	
55	def cr.oct.pieces.step(full: Bool, +c: List<&2, U32>, acc: List<&2, List<&2, U32>>) -> List<&2, List<&2, U32>>:
56	  match full:
57	    case True{}:
58	      Con{cr.oct.rev(c, Nil{}), acc}
59	    case False{}:
60	      acc
61	
62	def cr.oct.pieces.cur(full: Bool, +c: List<&2, U32>) -> List<&2, U32>:
63	  match full:
64	    case True{}:
65	      Nil{}
66	    case False{}:
67	      c
68	
69	def cr.oct.pieces.i(full: Bool, +i: Nat) -> Nat:
70	  match full:
71	    case True{}:
72	      0n
73	    case False{}:
74	      i
75	
76	# the pieces of xs, last first: whole n-byte pieces, then what is left
77	# (cur: the piece being filled, reversed, i bytes long)
78	def cr.oct.pieces.go(xs: List<&2, U32>, +n: Nat, +i: Nat, +cur: List<&2, U32>, acc: List<&2, List<&2, U32>>) -> List<&2, List<&2, U32>>:
79	  match xs:
80	    case Nil{}:
81	      cr.oct.flush(cur, acc)
82	    case Con{x, t}:
83	      +c : List<&2, U32> = Con{x, cur}
84	      +full = Nat.is_eq(1n+i, n)
85	      cr.oct.pieces.go(t, n, cr.oct.pieces.i(full, 1n+i), cr.oct.pieces.cur(full, c), cr.oct.pieces.step(full, c, acc))
86	
87	# xs cut into pieces of n bytes, in order: every piece but the last has n
88	# bytes, the last 1 to n (no pieces for no bytes)
89	def CrOct.pieces(n: Nat, xs: List<&2, U32>) -> List<&2, List<&2, U32>>:
90	  cr.oct.revs(cr.oct.pieces.go(xs, n, 0n, Nil{}, Nil{}), Nil{})