law blocks_correct

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

import Base
import bend-collections@1.0.0.0/src/crypto/sha/packed/packed.bend as P
import bend-collections@1.0.0.0/spec/crypto/sha/packed.bend as R
import bend-collections@1.0.0.0/src/crypto/sha/state.bend as S

783law blocks_correct:
784  for +extra: Nat
785  for +n: Nat
786  for +index: U32
787  for +remain: Nat
788  for +total: Nat
789  for pair: Array<U32> & S.State
790  {P.blocks(extra,n,index,remain,total,pair) == R.blocks(extra,n,index,remain,total,pair) : Array<U32> & S.State}