law window_rounds_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha512/conformance.bend:60

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as F

60law window_rounds_correct:
61  for +q: Nat
62  for +a: T.Lane
63  for +b: T.Lane
64  for +c: T.Lane
65  for +d: T.Lane
66  for +e: T.Lane
67  for +f: T.Lane
68  for +g: T.Lane
69  for +h: T.Lane
70  for +i: T.Lane
71  for +j: T.Lane
72  for +k: T.Lane
73  for +l: T.Lane
74  for +m: T.Lane
75  for +n: T.Lane
76  for +o: T.Lane
77  for +p: T.Lane
78  for +rest: List<&2, T.Lane>
79  for +ks: List<&2, T.Lane>
80  for +s: T.State
81  {C.window_rounds(q, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) == F.rounds(ks, F.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest))(s) : T.State}