AESNistObservationProof.stream_parameters: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend as AESNistObservationProof
Lines 18-29 of qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&start_line=18&end_line=29

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

def stream_parameters(+size: Nat, +words: List<&2, U32>, +start: List<&2, U32>,
    +known_size: Nat, +known_start: List<&2, U32>, +stream: List<&2, U32>,
    count: {size == known_size : Nat}, counter: {start == known_start : List<&2, U32>},
    computed: {Core.gcm_ctr_stream_exact.go(known_size, words, known_start, Nil{}) == stream : List<&2, U32>}) ->
    {Core.gcm_ctr_stream_exact(size, words, start) == stream : List<&2, U32>}:
    Equal.trans(List<&2, U32>, Core.gcm_ctr_stream_exact(size, words, start),
        Core.gcm_ctr_stream_exact.go(known_size, words, start, Nil{}), stream,
        Equal.cong(Nat, List<&2, U32>, n => Core.gcm_ctr_stream_exact.go(n, words, start, Nil{}), size, known_size, count),
        Equal.trans(List<&2, U32>, Core.gcm_ctr_stream_exact.go(known_size, words, start, Nil{}),
            Core.gcm_ctr_stream_exact.go(known_size, words, known_start, Nil{}), stream,
            Equal.cong(List<&2, U32>, List<&2, U32>, value => Core.gcm_ctr_stream_exact.go(known_size, words, value, Nil{}),
                start, known_start, counter), computed))

Uses (7):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_ctr_stream_exact
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_ctr_stream_exact.go