law window_rounds_correct

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

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

218law window_rounds_correct:
219  for +q: Nat
220  for +a: U32
221  for +b: U32
222  for +c: U32
223  for +d: U32
224  for +e: U32
225  for +f: U32
226  for +g: U32
227  for +h: U32
228  for +i: U32
229  for +j: U32
230  for +k: U32
231  for +l: U32
232  for +m: U32
233  for +n: U32
234  for +o: U32
235  for +p: U32
236  for +rest: List<&2, U32>
237  for +ks: List<&2, U32>
238  for +s: S.State
239  {C.window_rounds(q, C.W{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) ==
240    C.expanded_rounds(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest, ks, s) : S.State}