law window_compress16_correct

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

import Base
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

360law window_compress16_correct:
361  for +a: U32
362  for +b: U32
363  for +c: U32
364  for +d: U32
365  for +e: U32
366  for +f: U32
367  for +g: U32
368  for +h: U32
369  for +i: U32
370  for +j: U32
371  for +k: U32
372  for +l: U32
373  for +m: U32
374  for +n: U32
375  for +o: U32
376  for +p: U32
377  for +extra: Nat
378  for +ks: List<&2, U32>
379  for +s: S.State
380  {C.window_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, extra, ks, s) ==
381    C.fused_compress([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], extra, ks, s) : S.State}