Conformance.block_bytes_correct: law of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend as Conformance
Lines 429-434 of bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend&start_line=429&end_line=434

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

law block_bytes_correct:
  for +bytes: List<&2, U32>
  for +extra: Nat
  for +ks: List<&2, U32>
  for +s: S.State
  {C.block_bytes(bytes, extra, ks, s) == F.blocks(F.schedules(F.words(bytes), extra), ks)(s) : S.State}

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend&name=compression_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend&name=fused_compress_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend&name=schedule_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend&name=window_compress16_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/core_model.bend&name=block_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/core_model.bend&name=schedule
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/core_model.bend&name=window_compress16
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/sha.bend&name=blocks
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/sha.bend&name=compress
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/sha.bend&name=schedules
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/sha.bend&name=words
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/packed/core.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/state.bend&name=State