law kr63_correct
bend-collections@1.0.0.0 · proofs/crypto/sha/conformance.bend:675
import bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend as Conformance
import Base
import bend-collections@1.0.0.0/src/crypto/sha/state.bend as S
import bend-collections@1.0.0.0/src/crypto/sha/core.bend as C
675law kr63_correct:
676 for +q: Nat
677 for +x0: U32
678 for +x1: U32
679 for +x2: U32
680 for +x3: U32
681 for +x4: U32
682 for +x5: U32
683 for +x6: U32
684 for +x7: U32
685 for +x8: U32
686 for +x9: U32
687 for +x10: U32
688 for +x11: U32
689 for +x12: U32
690 for +x13: U32
691 for +x14: U32
692 for +x15: U32
693 for +s: S.State
694 {C.kr63(q, C.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) ==
695 C.window_rounds(q, C.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3329325298], s) : S.State}