Incremental.step512_inv: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend as Incremental
Lines 571-576 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend&start_line=571&end_line=576

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T512
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend as C512
import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as H

law step512_inv:
  for +st: H.Sha512State
  for +xs: List<&2, U32>
  for +q: Nat
  for +z: List<&2, U32>
  {C512.blocks(C512.lanes(List.append(&2, U32, List.append(&2, U32, buf512(st), xs), z)), q, C512.round_constants(), st512(st)) == C512.blocks(C512.lanes(List.append(&2, U32, buf512(H.step512(st, xs, q)), z)), q, C512.round_constants(), st512(H.step512(st, xs, q))) : T512.State}

Uses (14):
  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.length
  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-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend&name=absorb512_inv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend&name=buf512
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend&name=st512
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend&name=Sha512State
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend&name=step512
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend&name=blocks
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend&name=lanes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend&name=round_constants
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend&name=State