def xor_update_ref

bend-osdev-crypto@0.1.0.0 · PROOF.bend:175

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

175def 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>}:
176  %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>}
177  %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>}
178  {==}