Conformance.compress16_correct: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/conformance.bend as Conformance
Lines 138-158 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/conformance.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/conformance.bend&start_line=138&end_line=158

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

law compress16_correct:
  for +a: T.Lane
  for +b: T.Lane
  for +c: T.Lane
  for +d: T.Lane
  for +e: T.Lane
  for +f: T.Lane
  for +g: T.Lane
  for +h: T.Lane
  for +i: T.Lane
  for +j: T.Lane
  for +k: T.Lane
  for +l: T.Lane
  for +m: T.Lane
  for +n: T.Lane
  for +o: T.Lane
  for +p: T.Lane
  for +q: Nat
  for +ks: List<&2, T.Lane>
  for +s: T.State
  {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}

Uses (17):
  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=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.reverse
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/conformance.bend&name=block_rounds_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/conformance.bend&name=feedforward_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend&name=compress
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend&name=extension
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend&name=rounds
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend&name=schedule
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend&name=Sched
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend&name=block_rounds
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend&name=compress16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend&name=feedforward
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend&name=Lane
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend&name=State