law rc4_stream_streaming_state

bend-osdev-crypto@0.1.0.0 · LAWS.bend:1170

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

1170# RC4 (legacy-ciphers): the state after a ++ b is the state after a, then b
1171law rc4_stream_streaming_state:
1172  for +s: R.LcRc4State
1173  for +a: B.Octets
1174  for +b: B.Octets
1175  {R.LcRc4.out_state(R.LcRc4.update(s, B.Octets.append(a, b))) == R.LcRc4.out_state(R.LcRc4.update(R.LcRc4.out_state(R.LcRc4.update(s, a)), b)) : R.LcRc4State}