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

import Base
import bend-collections@1.0.0.0/src/crypto/sha/core.bend as C
import bend-collections@1.0.0.0/spec/crypto/sha.bend as F

# Unlike the old theorem, there is NO arbitrary preprocessing parameter.
# This proves the actual implementation pipeline against the independent one.
law sha256_correct:
  for +bytes: List<&2, U32>
  {C.sha256(bytes) == F.hash(bytes, 48n, C.round_constants()) : List<&2, U32>}

Uses (26):
  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.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=Nat.add
  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/conformance.bend&name=block_bytes_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=digest_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=stream_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=suffix_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/list_proofs.bend&name=add_zero
  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=digest
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/sha.bend&name=hash
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/sha.bend&name=initial
  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/core.bend&name=block_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=digest
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=initial
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=round_constants
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=sha256
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=stream
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=suffix
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/state.bend&name=State