law sha256_reified

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/packed/legacy_model.bend as Legacy
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/packed/packed_array_proof.bend as A
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha/packed.bend as R

907law sha256_reified:
908  for -a: Array<U32>
909  for +length: Nat
910  for view: Sigma<&2,&1,A.Tree,t => {a == A.thaw(t) : Array<U32>}>
911  {Legacy.sha256_packed(a,length) == R.sha256(a,length) : Maybe<&2,List<&2,U32>>}