Conformance.fips16_correct: law of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend as Conformance
Lines 2115-2135 of bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&start_line=2115&end_line=2135

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

law fips16_correct:
  for +a: U32
  for +b: U32
  for +c: U32
  for +d: U32
  for +e: U32
  for +f: U32
  for +g: U32
  for +h: U32
  for +i: U32
  for +j: U32
  for +k: U32
  for +l: U32
  for +m: U32
  for +n: U32
  for +o: U32
  for +p: U32
  for +q: Nat
  for +s: S.State
  {C.fips_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, s) ==
    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}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr16_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=ShaWindow
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=feedforward
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=fips_compress16
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=kr16
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=round_constants
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=step
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=window_compress16
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/core.bend&name=window_rounds
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/state.bend&name=State