law sha256_packed_correct

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

import Base
import bend-collections@1.0.0.0/proofs/crypto/sha/packed/legacy_model.bend as SHA
import bend-collections@1.0.0.0/spec/crypto/sha/packed.bend as PackedSpec

29# A separate packed-format contract; the original list-to-FIPS theorem is unchanged.
30law sha256_packed_correct:
31  for words: Array<U32>
32  for +byte_length: Nat
33  {SHA.sha256_packed(words,byte_length) == PackedSpec.sha256(words,byte_length) : Maybe<&2,List<&2,U32>>}