law stream_correct

bend-collections@1.0.0.0 · proofs/crypto/sha/conformance.bend:2144

import Base
import bend-collections@1.0.0.0/src/crypto/sha/state.bend as S
import bend-collections@1.0.0.0/src/crypto/sha/core.bend as C

2144# Streaming refines the generic block decoder, instantiated with the FIPS
2145# table, applied to the padded message. After a complete block the count grows
2146# by 64 exactly as the remaining length shrinks. For a short tail, count = 64k
2147# fixes n mod 64 to the tail length, so the modular zero count is concrete and
2148# finish_go packs the same 64 or 128 bytes that block_bytes decodes.
2149law stream_correct:
2150  for +bytes: List<&2, U32>
2151  for +k: Nat
2152  for +extra: Nat
2153  for +s: S.State
2154  {C.stream(bytes, mul64(k), extra, s) == C.block_bytes(List.append(&2, U32, bytes,
2155    C.suffix(Nat.add(List.length(&2, U32, bytes), mul64(k)))), extra, C.round_constants(), s) : S.State}