def rc4_go_ref

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

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

8430# the loop, for every list and state, is the structural output reversed
8431# onto what it had
8432def rc4_go_ref(xs: List<&2, U32>, +st: R.LcRc4State, +acc: List<&2, U32>) -> {R.rc4.go(xs, st, acc) == R.LcRc4Run{R.rc4.after(xs, st), R.rc4.rev_onto(acc, R.rc4.xs(xs, st))} : R.LcRc4Run}:
8433  match xs:
8434    case Nil{}:
8435      {==}
8436    case Con{x, t}:
8437      rc4_go_ref(t, R.rc4.step.st(R.rc4.next(st)), Con{B.byte(U32.xor(x, R.rc4.step.k(R.rc4.next(st)))), acc})