law md_streaming

bend-osdev-hashes@0.1.0.0 · LAWS.bend:20

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

20# The engine (hashes.bend), for every chaining value type, compression
21# function and block size: a ++ b is a, then b, from every state
22law md_streaming:
23  for ~C: Data
24  for ~compress: C -> List<&2, U32> -> C
25  for ~last: U32
26  for s: Hs.HsMdState<C>
27  for +a: B.Octets
28  for +b: B.Octets
29  {Hs.HsMd.update(~C, ~compress, ~last, s, B.Octets.append(a, b)) == Hs.HsMd.update(~C, ~compress, ~last, Hs.HsMd.update(~C, ~compress, ~last, s, a), b) : Hs.HsMdState<C>}