Block.rounds_correct: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/block.bend as Block
Lines 27-31 of bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/block.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/block.bend&start_line=27&end_line=31

import Base
import bend-collections-laws-math@1.0.0.0/src/math/random/chacha8/block.bend as B
import bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/rounds.bend as R

# the eight rounds on the initial state
def rounds_correct(+k: B.Key, +ctr: U32) -> {R.vec(B.dr(B.dr(B.dr(B.dr(B.init(k, ctr)))))) == S.double_rounds(4n, S.initial(S.key_list(k), ctr)) : List<&2, U32>}:
  Equal.trans(List<&2, U32>, R.vec(drs(4n, B.init(k, ctr))), S.double_rounds(4n, R.vec(B.init(k, ctr))), S.double_rounds(4n, S.initial(S.key_list(k), ctr)),
    drs_correct(4n, B.init(k, ctr)),
    Equal.cong(List<&2, U32>, List<&2, U32>, x => S.double_rounds(4n, x), R.vec(B.init(k, ctr)), S.initial(S.key_list(k), ctr), R.init_correct(k, ctr)))

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=Equal.trans
  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-math@1.0.0.0/proofs/math/random/chacha8/block.bend&name=drs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/block.bend&name=drs_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/rounds.bend&name=init_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/rounds.bend&name=vec
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend&name=double_rounds
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend&name=initial
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend&name=key_list
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/chacha8/block.bend&name=Key
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/chacha8/block.bend&name=dr
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/chacha8/block.bend&name=init