def cr.ks.xs

bend-osdev-crypto@0.1.0.0 · stream.bend:61

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

61# The structural forms the proofs reason about: the data, byte by byte, and
62# the state after it
63def cr.ks.xs(~S: Data, ~next: S -> CrKsStep<S>, ys: List<&2, U32>, +s: S) -> List<&2, U32>:
64  match ys:
65    case Nil{}:
66      Nil{}
67    case Con{x, t}:
68      Con{B.byte(U32.xor(x, CrKsStep.k(~S, next(s)))), cr.ks.xs(~S, ~next, t, CrKsStep.st(~S, next(s)))}