law tail_word_correct

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

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

363law tail_word_correct:
364  for +short: Bool
365  for +w: U32
366  for +pos: Nat
367  for +remain: Nat
368  for +length: U32
369  {P.length_word(short,P.pad_word(w,pos,remain),length) == R.length_word(short,R.pad_word(w,pos,remain),length) : U32}