Conformance.stream_correct: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/conformance.bend as Conformance
Lines 2144-2155 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/conformance.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/conformance.bend&start_line=2144&end_line=2155

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/src/crypto/sha/core.bend as C

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

Uses (27):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.replicate
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/conformance.bend&name=fips16_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/conformance.bend&name=mod_tail
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/conformance.bend&name=mul64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/list_proofs.bend&name=add_swap
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=bit_length
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=block_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=fips_compress16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=len_hi
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=len_lo
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=round_constants
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=stream
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=suffix
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend&name=window_compress16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend&name=State