law fips16_correct

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

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

2116law fips16_correct:
2117  for +a: U32
2118  for +b: U32
2119  for +c: U32
2120  for +d: U32
2121  for +e: U32
2122  for +f: U32
2123  for +g: U32
2124  for +h: U32
2125  for +i: U32
2126  for +j: U32
2127  for +k: U32
2128  for +l: U32
2129  for +m: U32
2130  for +n: U32
2131  for +o: U32
2132  for +p: U32
2133  for +q: Nat
2134  for +s: S.State
2135  {Runtime.fips_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, s) ==
2136    C.window_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, C.round_constants(), s) : S.State}