AESZipLengthProof.stream_step_length: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend as AESZipLengthProof
Lines 128-151 of qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&start_line=128&end_line=151

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

def stream_step_length(+words: List<&2, U32>,
    +counter: List<&2, U32>, +acc: List<&2, U32>) ->
    {List.length(&2, U32, List.append(&2, U32,
        List.reverse(&2, U32,
            Core.aes256_encrypt_expanded(words, counter)), acc)) ==
     Nat.add(16n, List.length(&2, U32, acc)) : Nat}:
    +block = Core.aes256_encrypt_expanded(words, counter)
    Equal.trans(Nat,
        List.length(&2, U32,
            List.append(&2, U32, List.reverse(&2, U32, block), acc)),
        Nat.add(List.length(&2, U32,
            List.reverse(&2, U32, block)),
            List.length(&2, U32, acc)),
        Nat.add(16n, List.length(&2, U32, acc)),
        append_length(List.reverse(&2, U32, block), acc),
        Equal.cong(Nat, Nat,
            n => Nat.add(n, List.length(&2, U32, acc)),
            List.length(&2, U32, List.reverse(&2, U32, block)),
            16n,
            Equal.trans(Nat,
                List.length(&2, U32, List.reverse(&2, U32, block)),
                List.length(&2, U32, block), 16n,
                reverse_length(block),
                encrypt_block_length(words, counter))))

Uses (13):
  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=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.reverse
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  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=aes256_encrypt_expanded
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&name=append_length
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&name=encrypt_block_length
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&name=reverse_length