law kr60_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha/conformance.bend:765

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend as S
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend as C

765law kr60_correct:
766  for +q: Nat
767  for +x0: U32
768  for +x1: U32
769  for +x2: U32
770  for +x3: U32
771  for +x4: U32
772  for +x5: U32
773  for +x6: U32
774  for +x7: U32
775  for +x8: U32
776  for +x9: U32
777  for +x10: U32
778  for +x11: U32
779  for +x12: U32
780  for +x13: U32
781  for +x14: U32
782  for +x15: U32
783  for +s: S.State
784  {C.kr60(q, C.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) ==
785    C.window_rounds(q, C.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2428436474, 2756734187, 3204031479, 3329325298], s) : S.State}