def ks_xs_append

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

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

215def ks_xs_append(~S: Data, ~next: S -> St.CrKsStep<S>, xs: List<&2, U32>, +ys: List<&2, U32>, +s: S) -> {St.cr.ks.xs(~S, ~next, B.append(xs, ys), s) == B.append(St.cr.ks.xs(~S, ~next, xs, s), St.cr.ks.xs(~S, ~next, ys, St.cr.ks.after(~S, ~next, xs, s))) : List<&2, U32>}:
216  match xs:
217    case Nil{}:
218      {==}
219    case Con{+x, +t}:
220      %ks_xs_append(~S, ~next, t, ys, St.CrKsStep.st(~S, next(s))) : {Con{B.byte(U32.xor(x, St.CrKsStep.k(~S, next(s)))), St.cr.ks.xs(~S, ~next, B.append(t, ys), St.CrKsStep.st(~S, next(s)))} == Con{B.byte(U32.xor(x, St.CrKsStep.k(~S, next(s)))), _} : List<&2, U32>}
221      {==}