law hash_tail

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake2s/reads.bend:875

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/blake2s.bend as K
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend as R

875law hash_tail:
876  for -a: Array<U32>
877  for +length: Nat
878  {R.blocks(10n,K.leading(length),0,0,0,Nat.sub(length,Nat.mul(64n,K.leading(length))),(a,K.initial())) == R.hash(10n,a,length) : T.State}