PROOF.rc4_update_ref: def of bend-osdev-legacy-ciphers@0.1.0.0
Import: import bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend as PROOF
Lines 8439-8441 of bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&start_line=8439&end_line=8441

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

def 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}:
  %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}
  {==}

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.to_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=rc4_go_ref
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend&name=LcRc4.update
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend&name=LcRc4Out
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend&name=LcRc4Run
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend&name=LcRc4State
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend&name=rc4.after
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend&name=rc4.go
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend&name=rc4.out
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend&name=rc4.rev_onto
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend&name=rc4.xs