Block.block_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 33-40 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=33&end_line=40

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

# THEOREM: the implementation's block is C2SP's block ctr
def block_correct(+k: B.Key, +ctr: U32) -> {R.vec(B.block(k, ctr)) == S.c2sp_block(S.key_list(k), ctr) : List<&2, U32>}:
  +v = B.dr(B.dr(B.dr(B.dr(B.init(k, ctr)))))
  Equal.trans(List<&2, U32>, R.vec(B.finish(k, v)), S.subtract(S.add_words(R.vec(v), R.vec(B.init(k, ctr))), ctr), S.subtract(S.add_words(S.double_rounds(4n, S.initial(S.key_list(k), ctr)), S.initial(S.key_list(k), ctr)), ctr),
    R.finish_correct(k, v, ctr),
    Equal.trans(List<&2, U32>, S.subtract(S.add_words(R.vec(v), R.vec(B.init(k, ctr))), ctr), S.subtract(S.add_words(S.double_rounds(4n, S.initial(S.key_list(k), ctr)), R.vec(B.init(k, ctr))), ctr), S.subtract(S.add_words(S.double_rounds(4n, S.initial(S.key_list(k), ctr)), S.initial(S.key_list(k), ctr)), ctr),
      Equal.cong(List<&2, U32>, List<&2, U32>, x => S.subtract(S.add_words(x, R.vec(B.init(k, ctr))), ctr), R.vec(v), S.double_rounds(4n, S.initial(S.key_list(k), ctr)), rounds_correct(k, ctr)),
      Equal.cong(List<&2, U32>, List<&2, U32>, x => S.subtract(S.add_words(S.double_rounds(4n, S.initial(S.key_list(k), ctr)), x), ctr), R.vec(B.init(k, ctr)), S.initial(S.key_list(k), ctr), R.init_correct(k, ctr))))

Uses (19):
  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=rounds_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/rounds.bend&name=finish_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=add_words
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend&name=c2sp_block
  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/spec/math/random/chacha8rand.bend&name=subtract
  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=block
  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=finish
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/chacha8/block.bend&name=init