law pad_word_correct

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

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

355law pad_word_correct:
356  for +w: U32
357  for +pos: Nat
358  for +remain: Nat
359  {P.pad_word(w,pos,remain) == R.pad_word(w,pos,remain) : U32}