law blocks_zero_reified

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

import Base
import bend-collections@1.0.0.0/proofs/crypto/sha/packed/packed_array_proof.bend as A
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

792law blocks_zero_reified:
793  for +extra: Nat
794  for +index: U32
795  for +remain: Nat
796  for +total: Nat
797  for -a: Array<U32>
798  for +s: S.State
799  for view: Sigma<&2,&1,A.Tree,t => {a == A.thaw(t) : Array<U32>}>
800  {P.blocks(extra,0n,index,remain,total,(a,s)) == R.blocks(extra,0n,index,remain,total,(a,s)) : Array<U32> & S.State}