1	# The stream-cipher interface, and stream ciphers built from a keystream
2	# generator.
3	#
4	# The interface (template arguments, in this order):
5	#   ~S: Data                                    the state: key, IV and position
6	#   ~O: Data                                    what one step answers
7	#   ~start: B.Octets -> B.Octets -> Result<&2, &2, CrError, S>
8	#                                               the state for a key and an IV
9	#                                               (a cipher without an IV takes
10	#                                               the empty one)
11	#   ~update: S -> B.Octets -> O                 the next piece of data,
12	#                                               encrypted or decrypted (the
13	#                                               same thing)
14	#   ~out_state: O -> S                          the state after the piece
15	#   ~out_data: O -> B.Octets                    the piece encrypted
16	# Laws, for every state and all data (README.md, "Laws"):
17	#   involution       out_data(update(s, out_data(update(s, m)))) == m
18	#   streaming_data   out_data(update(s, a ++ b)) == out_data(update(s, a)) ++
19	#                    out_data(update(out_state(update(s, a)), b))
20	#   streaming_state  out_state(update(s, a ++ b)) ==
21	#                    out_state(update(out_state(update(s, a)), b))
22	#
23	# Keystream generation is the extension point: CrXor turns any function that
24	# gives the next keystream byte and the next state (~next: S ->
25	# CrKsStep<S>) into a stream cipher with exactly this interface, and LAWS.bend
26	# proves its three laws for every such function, once. CTR mode (modes.bend)
27	# is one; RC4 (inst_rc4.bend) satisfies the interface directly.
28	import Base
29	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
30	import ./crypto.bend as Cr
31	
32	# A stream cipher in one call: the data under a key and an IV
33	def CrStream.crypt(~S: Data, ~O: Data, ~start: B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, S>, ~update: S -> B.Octets -> O, ~out_data: O -> B.Octets, key: B.Octets, iv: B.Octets, m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
34	  Result.map(&2, &2, Cr.CrError, S, B.Octets, s => out_data(update(s, m)), start(key, iv))
35	
36	# The next n keystream bytes (the data n zero bytes)
37	def CrStream.keystream(~S: Data, ~O: Data, ~update: S -> B.Octets -> O, ~out_data: O -> B.Octets, s: S, n: Nat) -> B.Octets:
38	  out_data(update(s, B.Octets.zeros(n)))
39	
40	# Keystream generators
41	
42	# one keystream byte and the state after it
43	type CrKsStep<-S: Data> is Data:
44	  CrKsStep{k: U32, st: S}
45	
46	# what CrXor.update answers: the state after the data, and the data
47	# encrypted (open type)
48	type CrXorOut<-S: Data> is Data:
49	  CrXorOut{state: S, data: B.Octets}
50	
51	def CrKsStep.k(~S: Data, r: CrKsStep<S>) -> U32:
52	  match r:
53	    case CrKsStep{k, st}:
54	      k
55	
56	def CrKsStep.st(~S: Data, r: CrKsStep<S>) -> S:
57	  match r:
58	    case CrKsStep{k, st}:
59	      st
60	
61	# The structural forms the proofs reason about: the data, byte by byte, and
62	# the state after it
63	def cr.ks.xs(~S: Data, ~next: S -> CrKsStep<S>, ys: List<&2, U32>, +s: S) -> List<&2, U32>:
64	  match ys:
65	    case Nil{}:
66	      Nil{}
67	    case Con{x, t}:
68	      Con{B.byte(U32.xor(x, CrKsStep.k(~S, next(s)))), cr.ks.xs(~S, ~next, t, CrKsStep.st(~S, next(s)))}
69	
70	def cr.ks.after(~S: Data, ~next: S -> CrKsStep<S>, ys: List<&2, U32>, +s: S) -> S:
71	  match ys:
72	    case Nil{}:
73	      s
74	    case Con{x, t}:
75	      cr.ks.after(~S, ~next, t, CrKsStep.st(~S, next(s)))
76	
77	# The loop that runs: tail-recursive, the output kept reversed, each
78	# keystream byte computed once
79	type CrKsRun<-S: Data> is Data:
80	  CrKsRun{st: S, rev: List<&2, U32>}
81	
82	def cr.rev_onto(xs: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
83	  match xs:
84	    case Nil{}:
85	      acc
86	    case Con{h, t}:
87	      cr.rev_onto(t, Con{h, acc})
88	
89	def cr.ks.go(~S: Data, ~next: S -> CrKsStep<S>, ys: List<&2, U32>, +s: S, acc: List<&2, U32>) -> CrKsRun<S>:
90	  match ys:
91	    case Nil{}:
92	      CrKsRun{s, acc}
93	    case Con{x, t}:
94	      +r = next(s)
95	      cr.ks.go(~S, ~next, t, CrKsStep.st(~S, r), Con{B.byte(U32.xor(x, CrKsStep.k(~S, r))), acc})
96	
97	def cr.ks.out(~S: Data, r: CrKsRun<S>) -> CrXorOut<S>:
98	  match r:
99	    case CrKsRun{st, rev}:
100	      CrXorOut{st, B.Octets.of_list(cr.rev_onto(rev, Nil{}))}
101	
102	# The stream cipher of a keystream generator: m XORed with the next len(m)
103	# keystream bytes, and the state after them
104	def CrXor.update(~S: Data, ~next: S -> CrKsStep<S>, s: S, m: B.Octets) -> CrXorOut<S>:
105	  cr.ks.out(~S, cr.ks.go(~S, ~next, B.Octets.to_list(m), s, Nil{}))
106	
107	def CrXor.out_state(~S: Data, o: CrXorOut<S>) -> S:
108	  match o:
109	    case CrXorOut{st, d}:
110	      st
111	
112	def CrXor.out_data(~S: Data, o: CrXorOut<S>) -> B.Octets:
113	  match o:
114	    case CrXorOut{st, d}:
115	      d