law fused_compress_correct

bend-collections@1.0.0.0 · proofs/crypto/sha/packed/conformance.bend:198

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

198law fused_compress_correct:
199  for +block: List<&2, U32>
200  for +extra: Nat
201  for +ks: List<&2, U32>
202  for +s: S.State
203  {C.fused_compress(block, extra, ks, s) == C.compress(C.schedule(extra, block), ks, s) : S.State}