law stream_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha/packed/conformance.bend:2145

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/packed/core_model.bend as C

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