law kr62_correct

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

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

706law kr62_correct:
707  for +q: Nat
708  for +x0: U32
709  for +x1: U32
710  for +x2: U32
711  for +x3: U32
712  for +x4: U32
713  for +x5: U32
714  for +x6: U32
715  for +x7: U32
716  for +x8: U32
717  for +x9: U32
718  for +x10: U32
719  for +x11: U32
720  for +x12: U32
721  for +x13: U32
722  for +x14: U32
723  for +x15: U32
724  for +s: S.State
725  {Runtime.kr62(q, Runtime.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) ==
726    C.window_rounds(q, Runtime.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3204031479, 3329325298], s) : S.State}