Stream.inv: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/stream.bend as Stream
Lines 57-80 of bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/stream.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/stream.bend&start_line=57&end_line=80

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
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/src/math/random/chacha8.bend as C8
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/spec/math/random/source.bend as SRC
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/block.bend as PB

# the invariant: from state C{k, p, buf} the generator outputs buf, the rest
# of the iteration keyed by k, then C2SP's stream from the next key
def inv(+n: Nat, +k: B.Key, +buf: List<&2, W.U64>, +p: C8.Phase) -> {SRC.outputs(~C8.ChaCha8, ~C8.next, n, C8.C{k, p, buf}) == S.stream_go(n, app(buf, rest(S.key_list(k), p)), nk(S.key_list(k), p)) : List<&2, W.U64>}:
  match n:
    case 0n:
      {==}
    case 1n+m:
      match buf:
        case Con{x, t}:
          Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{x, l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, p, t}), S.stream_go(m, app(t, rest(S.key_list(k), p)), nk(S.key_list(k), p)), inv(m, k, t, p))
        case Nil{}:
          match p:
            case C8.G0{}:
              %Equal.sym(List<&2, W.U64>, B.group(k, 0), gw(k, 0), PB.group_correct(k, 0)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.C{k, C8.G1{}, _})), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.C{k, C8.G1{}, _})))} == S.stream_go(1n+m, [], S.key_list(k)) : List<&2, W.U64>}
              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 0)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, C8.G1{}, S.tail(gw(k, 0))}), S.stream_go(m, app(S.tail(gw(k, 0)), rest(S.key_list(k), C8.G1{})), S.next_key(S.key_list(k))), inv(m, k, S.tail(gw(k, 0)), C8.G1{}))
            case C8.G1{}:
              %Equal.sym(List<&2, W.U64>, B.group(k, 4), gw(k, 4), PB.group_correct(k, 4)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.C{k, C8.G2{}, _})), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.C{k, C8.G2{}, _})))} == S.stream_go(1n+m, rest(S.key_list(k), C8.G1{}), S.next_key(S.key_list(k))) : List<&2, W.U64>}
              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 4)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, C8.G2{}, S.tail(gw(k, 4))}), S.stream_go(m, app(S.tail(gw(k, 4)), rest(S.key_list(k), C8.G2{})), S.next_key(S.key_list(k))), inv(m, k, S.tail(gw(k, 4)), C8.G2{}))
            case C8.G2{}:
              %Equal.sym(List<&2, W.U64>, B.group(k, 8), gw(k, 8), PB.group_correct(k, 8)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.C{k, C8.G3{}, _})), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.C{k, C8.G3{}, _})))} == S.stream_go(1n+m, rest(S.key_list(k), C8.G2{}), S.next_key(S.key_list(k))) : List<&2, W.U64>}
              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 8)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, C8.G3{}, S.tail(gw(k, 8))}), S.stream_go(m, app(S.tail(gw(k, 8)), rest(S.key_list(k), C8.G3{})), S.next_key(S.key_list(k))), inv(m, k, S.tail(gw(k, 8)), C8.G3{}))
            case C8.G3{}:
              %Equal.sym(List<&2, W.U64>, B.group(k, 12), gw(k, 12), PB.group_correct(k, 12)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.last(_))), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.last(_))))} == S.stream_go(1n+m, rest(S.key_list(k), C8.G3{}), S.next_key(S.key_list(k))) : List<&2, W.U64>}
              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 12)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{C8.rekey(List.drop(&2, W.U64, gw(k, 12), 28n)), C8.G0{}, S.tail(List.take(&2, W.U64, gw(k, 12), 28n))}), S.stream_go(m, app(S.tail(List.take(&2, W.U64, gw(k, 12), 28n)), []), S.key_list(C8.rekey(List.drop(&2, W.U64, gw(k, 12), 28n)))), inv(m, C8.rekey(List.drop(&2, W.U64, gw(k, 12), 28n)), S.tail(List.take(&2, W.U64, gw(k, 12), 28n)), C8.G0{}))

Uses (28):
  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.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.drop
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.take
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/block.bend&name=group_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/stream.bend&name=app
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/stream.bend&name=gw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/stream.bend&name=nk
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/stream.bend&name=rest
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend&name=head
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend&name=key_list
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend&name=next_key
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend&name=stream_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend&name=tail
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/source.bend&name=fst64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/source.bend&name=outputs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/source.bend&name=snd64
  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=group
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8.bend&name=ChaCha8
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8.bend&name=Phase
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8.bend&name=last
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8.bend&name=next
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8.bend&name=pop
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8.bend&name=rekey
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend&name=U64