law hmac_crc32_streaming

bend-osdev-crypto@0.1.0.0 · LAWS.bend:1177

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crc@0.1.0.0/crc.bend as C
import bend-osdev-crypto@0.1.0.0/hmac.bend as Hm
import bend-osdev-crypto@0.1.0.0/inst_crc.bend as CR

1177# HMAC over CRC-32 of any parameter set (crc): the state after a ++ b is the state after a, then b
1178law hmac_crc32_streaming:
1179  for ~spec: C.Crc32Spec
1180  for s: Hm.CrHmacState<U32>
1181  for +a: B.Octets
1182  for +b: B.Octets
1183  {Hm.CrHmac.update(~U32, ~CR.CrCrc32.update(~spec), s, B.Octets.append(a, b)) == Hm.CrHmac.update(~U32, ~CR.CrCrc32.update(~spec), Hm.CrHmac.update(~U32, ~CR.CrCrc32.update(~spec), s, a), b) : Hm.CrHmacState<U32>}