law sha256_array_correct

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

import Base
import bend-collections@1.0.0.0/src/crypto/sha/packed/sha256.bend as Runtime
import bend-collections@1.0.0.0/src/crypto/sha/packed/buffer.bend as Buffer
import bend-collections@1.0.0.0/spec/crypto/sha/packed.bend as PackedSpec

35# Actual production array API; historical list laws above concern only its model.
36law sha256_array_correct:
37  for words: Array<U32>
38  for +byte_length: Nat
39  {Runtime.sha256(words,byte_length) == Buffer.result(PackedSpec.hash(words,byte_length)) : Maybe<&1,Array<U32>>}