1	# RC4 as a stream cipher: legacy-ciphers' RC4 (RFC 6229's description), and
2	# RC4-drop[n] (RFC 4345). RC4 is broken (RFC 7465 forbids it in TLS): it is
3	# here to read and write what already uses it. The instance:
4	#   ~R.LcRc4State, ~R.LcRc4Out, ~CrRc4.start, ~R.LcRc4.update,
5	#   ~R.LcRc4.out_state, ~R.LcRc4.out_data
6	# and with the first n keystream bytes dropped, ~CrRc4.start_drop(~n) in
7	# place of ~CrRc4.start.
8	import Base
9	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
10	import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
11	import bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend as R
12	import ./crypto.bend as Cr
13	import ./inst_lc.bend as LC
14	
15	def cr.rc4.start(+n: Nat, r: Result<&2, &2, L.LcError, R.LcRc4State>) -> Result<&2, &2, Cr.CrError, R.LcRc4State>:
16	  do Result<&2, &2, Cr.CrError, R.LcRc4State>:
17	    Cr.CrError.check(Nat.is_eq(n, 0n), Cr.CrBadIvLength{n})
18	    LC.CrLc.lift(~R.LcRc4State, r)
19	
20	# the state for a key of 1 to 256 bytes (CrBadKeyLength otherwise); RC4 has
21	# no IV, so the IV must be empty (CrBadIvLength otherwise)
22	def CrRc4.start(key: B.Octets, iv: B.Octets) -> Result<&2, &2, Cr.CrError, R.LcRc4State>:
23	  cr.rc4.start(B.Octets.len(iv), R.LcRc4.start(key))
24	
25	# the same, with the first n keystream bytes dropped (RC4-drop[n])
26	def CrRc4.start_drop(~n: Nat, key: B.Octets, iv: B.Octets) -> Result<&2, &2, Cr.CrError, R.LcRc4State>:
27	  cr.rc4.start(B.Octets.len(iv), R.LcRc4.start_drop(key, n))