def feed_append

bend-osdev-hashes@0.1.0.0 · PROOF.bend:16

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

16# The engine: feeding xs ++ ys is feeding xs, then ys (induction on xs)
17def feed_append(~C: Data, ~compress: C -> List<&2, U32> -> C, ~last: U32, xs: List<&2, U32>, +ys: List<&2, U32>, s: Hs.HsMdState<C>) -> {Hs.hs.md.feed(~C, ~compress, ~last, B.append(xs, ys), s) == Hs.hs.md.feed(~C, ~compress, ~last, ys, Hs.hs.md.feed(~C, ~compress, ~last, xs, s)) : Hs.HsMdState<C>}:
18  match xs:
19    case Nil{}:
20      {==}
21    case Con{x, t}:
22      feed_append(~C, ~compress, ~last, t, ys, Hs.hs.md.step(~C, ~compress, ~last, s, x))