law window_schedule_rounds_correct

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

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

257law window_schedule_rounds_correct:
258  for +ws: List<&2, U32>
259  for +extra: Nat
260  for +a: U32
261  for +b: U32
262  for +c: U32
263  for +d: U32
264  for +e: U32
265  for +f: U32
266  for +g: U32
267  for +h: U32
268  for +i: U32
269  for +j: U32
270  for +k: U32
271  for +l: U32
272  for +m: U32
273  for +n: U32
274  for +o: U32
275  for +p: U32
276  for +rest: List<&2, U32>
277  for +ks: List<&2, U32>
278  for +s: S.State
279  {C.window_schedule_rounds(ws, extra, Runtime.W{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) ==
280    C.schedule_rounds(ws, extra, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest, ks, s) : S.State}