Rounds.finish_correct: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/rounds.bend as Rounds
Lines 35-48 of bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/rounds.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/rounds.bend&start_line=35&end_line=48

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend as B
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A

# the key words added back, C2SP's subtractions of the constants and the
# counter, and the zero nonce words: the words the implementation keeps
def finish_correct(+k: B.Key, +v: B.Vector, +ctr: U32) -> {vec(B.finish(k,v)) == S.subtract(S.add_words(vec(v),vec(B.init(k,ctr))),ctr) : List<&2,U32>}:
  match k v:
    case B.K{k0,k1,k2,k3,k4,k5,k6,k7} B.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}:
      %Equal.sym(U32,U32.sub(U32.add(v0,1634760805),1634760805),v0,cancel(v0,1634760805)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [_,U32.sub(U32.add(v1,857760878),857760878),U32.sub(U32.add(v2,2036477234),2036477234),U32.sub(U32.add(v3,1797285236),1797285236),U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),U32.sub(U32.add(v12,ctr),ctr),U32.add(v13,0),U32.add(v14,0),U32.add(v15,0)] : List<&2,U32>}
      %Equal.sym(U32,U32.sub(U32.add(v1,857760878),857760878),v1,cancel(v1,857760878)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [v0,_,U32.sub(U32.add(v2,2036477234),2036477234),U32.sub(U32.add(v3,1797285236),1797285236),U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),U32.sub(U32.add(v12,ctr),ctr),U32.add(v13,0),U32.add(v14,0),U32.add(v15,0)] : List<&2,U32>}
      %Equal.sym(U32,U32.sub(U32.add(v2,2036477234),2036477234),v2,cancel(v2,2036477234)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [v0,v1,_,U32.sub(U32.add(v3,1797285236),1797285236),U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),U32.sub(U32.add(v12,ctr),ctr),U32.add(v13,0),U32.add(v14,0),U32.add(v15,0)] : List<&2,U32>}
      %Equal.sym(U32,U32.sub(U32.add(v3,1797285236),1797285236),v3,cancel(v3,1797285236)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [v0,v1,v2,_,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),U32.sub(U32.add(v12,ctr),ctr),U32.add(v13,0),U32.add(v14,0),U32.add(v15,0)] : List<&2,U32>}
      %Equal.sym(U32,U32.sub(U32.add(v12,ctr),ctr),v12,cancel(v12,ctr)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),_,U32.add(v13,0),U32.add(v14,0),U32.add(v15,0)] : List<&2,U32>}
      %Equal.sym(U32,U32.add(v13,0),v13,A.add_zero(v13)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,_,U32.add(v14,0),U32.add(v15,0)] : List<&2,U32>}
      %Equal.sym(U32,U32.add(v14,0),v14,A.add_zero(v14)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,_,U32.add(v15,0)] : List<&2,U32>}
      %Equal.sym(U32,U32.add(v15,0),v15,A.add_zero(v15)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,_] : List<&2,U32>}
      {==}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/rounds.bend&name=cancel
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/rounds.bend&name=vec
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend&name=add_words
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend&name=subtract
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend&name=Key
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend&name=Vector
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend&name=finish
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend&name=init