law compress16_correct

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

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

138law compress16_correct:
139  for +a: T.Lane
140  for +b: T.Lane
141  for +c: T.Lane
142  for +d: T.Lane
143  for +e: T.Lane
144  for +f: T.Lane
145  for +g: T.Lane
146  for +h: T.Lane
147  for +i: T.Lane
148  for +j: T.Lane
149  for +k: T.Lane
150  for +l: T.Lane
151  for +m: T.Lane
152  for +n: T.Lane
153  for +o: T.Lane
154  for +p: T.Lane
155  for +q: Nat
156  for +ks: List<&2, T.Lane>
157  for +s: T.State
158  {C.compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s) == F.compress(F.schedule(q, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p]), ks, s) : T.State}