law final_extra_correct

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

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

767law final_extra_correct:
768  for +extra: Nat
769  for +more: Bool
770  for +total: Nat
771  for pair: Array<U32> & S.State
772  {P.final_extra(extra,more,total,pair) == R.final_extra(extra,more,total,pair) : Array<U32> & S.State}