law rc4_streaming_data

bend-osdev-legacy-ciphers@0.1.0.0 · LAWS.bend:199

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend as R

199# data in pieces: the output of a ++ b is the output of a, then the output
200# of b from the state after a; and the state after a ++ b is the state
201# after a, then b
202law rc4_streaming_data:
203  for +st: R.LcRc4State
204  for +a: B.Octets
205  for +b: B.Octets
206  {R.LcRc4.out_data(R.LcRc4.update(st, B.Octets.append(a, b))) == B.Octets.append(R.LcRc4.out_data(R.LcRc4.update(st, a)), R.LcRc4.out_data(R.LcRc4.update(R.LcRc4.out_state(R.LcRc4.update(st, a)), b))) : B.Octets}