law window_compress16_correct
bend-collections@1.0.0.0 · proofs/crypto/sha/conformance.bend:359
import bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend as Conformance
import Base
import bend-collections@1.0.0.0/src/crypto/sha/state.bend as S
import bend-collections@1.0.0.0/src/crypto/sha/core.bend as C
359law window_compress16_correct:
360 for +a: U32
361 for +b: U32
362 for +c: U32
363 for +d: U32
364 for +e: U32
365 for +f: U32
366 for +g: U32
367 for +h: U32
368 for +i: U32
369 for +j: U32
370 for +k: U32
371 for +l: U32
372 for +m: U32
373 for +n: U32
374 for +o: U32
375 for +p: U32
376 for +extra: Nat
377 for +ks: List<&2, U32>
378 for +s: S.State
379 {C.window_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, extra, ks, s) ==
380 C.fused_compress([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], extra, ks, s) : S.State}