law kr16_correct
bend-collections@1.0.0.0 · proofs/crypto/sha/conformance.bend:2085
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
2085law kr16_correct:
2086 for +q: Nat
2087 for +x0: U32
2088 for +x1: U32
2089 for +x2: U32
2090 for +x3: U32
2091 for +x4: U32
2092 for +x5: U32
2093 for +x6: U32
2094 for +x7: U32
2095 for +x8: U32
2096 for +x9: U32
2097 for +x10: U32
2098 for +x11: U32
2099 for +x12: U32
2100 for +x13: U32
2101 for +x14: U32
2102 for +x15: U32
2103 for +s: S.State
2104 {C.kr16(q, C.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) ==
2105 C.window_rounds(q, C.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3835390401, 4022224774, 264347078, 604807628, 770255983, 1249150122, 1555081692, 1996064986, 2554220882, 2821834349, 2952996808, 3210313671, 3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : S.State}