Core.init_correct: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/core.bend as Core
Lines 135-148 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/core.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/core.bend&start_line=135&end_line=148

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/core.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as R

law init_correct:
  for +k0: U32
  for +k1: U32
  for +k2: U32
  for +k3: U32
  for +k4: U32
  for +k5: U32
  for +k6: U32
  for +k7: U32
  for +c: U32
  for +n0: U32
  for +n1: U32
  for +n2: U32
  {vec(C.init(k0, k1, k2, k3, k4, k5, k6, k7, c, n0, n1, n2)) == R.state([k0, k1, k2, k3, k4, k5, k6, k7], c, [n0, n1, n2]) : List<&2, U32>}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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/chacha/core.bend&name=vec
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend&name=state
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/core.bend&name=init