PROOF.xor_update_ref: def of bend-osdev-crypto@0.1.0.0
Import: import bend-osdev-crypto@0.1.0.0/PROOF.bend as PROOF
Lines 175-178 of bend-osdev-crypto@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-crypto@0.1.0.0/PROOF.bend&start_line=175&end_line=178

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/stream.bend as St

def xor_update_ref(~S: Data, ~next: S -> St.CrKsStep<S>, +s: S, +m: B.Octets) -> {St.CrXorOut{St.cr.ks.after(~S, ~next, B.Octets.to_list(m), s), B.Octets.of_list(St.cr.ks.xs(~S, ~next, B.Octets.to_list(m), s))} == St.CrXor.update(~S, ~next, s, m) : St.CrXorOut<S>}:
  %Equal.sym(St.CrKsRun<S>, St.cr.ks.go(~S, ~next, B.Octets.to_list(m), s, Nil{}), St.CrKsRun{St.cr.ks.after(~S, ~next, B.Octets.to_list(m), s), St.cr.rev_onto(St.cr.ks.xs(~S, ~next, B.Octets.to_list(m), s), Nil{})}, ks_go_ref(~S, ~next, B.Octets.to_list(m), s, Nil{})) : {St.CrXorOut{St.cr.ks.after(~S, ~next, B.Octets.to_list(m), s), B.Octets.of_list(St.cr.ks.xs(~S, ~next, B.Octets.to_list(m), s))} == St.cr.ks.out(~S, _) : St.CrXorOut<S>}
  %rev2(St.cr.ks.xs(~S, ~next, B.Octets.to_list(m), s), Nil{}) : {St.CrXorOut{St.cr.ks.after(~S, ~next, B.Octets.to_list(m), s), B.Octets.of_list(_)} == St.CrXorOut{St.cr.ks.after(~S, ~next, B.Octets.to_list(m), s), B.Octets.of_list(St.cr.rev_onto(St.cr.rev_onto(St.cr.ks.xs(~S, ~next, B.Octets.to_list(m), s), Nil{}), Nil{}))} : St.CrXorOut<S>}
  {==}

Uses (16):
  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.1/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.to_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/PROOF.bend&name=ks_go_ref
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/PROOF.bend&name=rev2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/stream.bend&name=CrKsRun
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/stream.bend&name=CrKsStep
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/stream.bend&name=CrXor.update
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/stream.bend&name=CrXorOut
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/stream.bend&name=cr.ks.after
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/stream.bend&name=cr.ks.go
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/stream.bend&name=cr.ks.out
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/stream.bend&name=cr.ks.xs
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/stream.bend&name=cr.rev_onto