def rc4_update_ref

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:8439

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

8439def rc4_update_ref(+st: R.LcRc4State, +m: B.Octets) -> {R.LcRc4Out{R.rc4.after(B.Octets.to_list(m), st), B.Octets.of_list(R.rc4.xs(B.Octets.to_list(m), st))} == R.LcRc4.update(st, m) : R.LcRc4Out}:
8440  %Equal.sym(R.LcRc4Run, R.rc4.go(B.Octets.to_list(m), st, Nil{}), R.LcRc4Run{R.rc4.after(B.Octets.to_list(m), st), R.rc4.rev_onto(Nil{}, R.rc4.xs(B.Octets.to_list(m), st))}, rc4_go_ref(B.Octets.to_list(m), st, Nil{})) : {R.LcRc4Out{R.rc4.after(B.Octets.to_list(m), st), B.Octets.of_list(R.rc4.xs(B.Octets.to_list(m), st))} == R.rc4.out(_) : R.LcRc4Out}
8441  {==}