law kr64_correct

bend-collections@1.0.0.0 · proofs/crypto/sha/packed/conformance.bend:660

import Base
import bend-collections@1.0.0.0/src/crypto/sha/packed/core.bend as Runtime
import bend-collections@1.0.0.0/src/crypto/sha/state.bend as S
import bend-collections@1.0.0.0/proofs/crypto/sha/packed/core_model.bend as C

660# Each literal-constant round refines one step of window_rounds over the
661# remaining FIPS constants; the window variables stay abstract, so every proof
662# is one unfolding followed by the next round's lemma.
663law kr64_correct:
664  for +q: Nat
665  for +win: Runtime.ShaWindow
666  for +s: S.State
667  {Runtime.kr64(q, win, s) == C.window_rounds(q, win, Nil{}, s) : S.State}