Conformance.window_rounds_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 60-81 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=60&end_line=81

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 window_rounds_correct:
  for +q: Nat
  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 +rest: List<&2, T.Lane>
  for +ks: List<&2, T.Lane>
  for +s: T.State
  {C.window_rounds(q, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) == F.rounds(ks, F.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest))(s) : T.State}

Uses (13):
  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=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/conformance.bend&name=next_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/conformance.bend&name=step_correct
  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=step
  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=next
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend&name=step
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend&name=window_rounds
  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