AESNistCtrProof.stream_step: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_NistCtrProof.bend as AESNistCtrProof
Lines 13-23 of qasim-bend-kit@0.1.0.2/proof/AES_NistCtrProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistCtrProof.bend&start_line=13&end_line=23

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

def stream_step(+remaining: Nat, +fuel: Nat, +words: List<&2, U32>, +counter: List<&2, U32>, +block: List<&2, U32>,
    count: {remaining == 1n+fuel : Nat}, same: {Core.aes256_encrypt_expanded(words, counter) == block : List<&2, U32>}) ->
    {Core.gcm_ctr_stream_exact.go(remaining, words, counter, Nil{}) ==
     Core.aes_byte_at(block, 0n) <> Core.gcm_ctr_stream_exact.go(fuel, words, Core.gcm_inc32(counter), List.tail(&2, U32, block)) : List<&2, U32>}:
    Equal.trans(List<&2, U32>, Core.gcm_ctr_stream_exact.go(remaining, words, counter, Nil{}),
        Core.gcm_ctr_stream_exact.go(1n+fuel, words, counter, Nil{}),
        Core.aes_byte_at(block, 0n) <> Core.gcm_ctr_stream_exact.go(fuel, words, Core.gcm_inc32(counter), List.tail(&2, U32, block)),
        Equal.cong(Nat, List<&2, U32>, n => Core.gcm_ctr_stream_exact.go(n, words, counter, Nil{}), remaining, 1n+fuel, count),
        Equal.cong(List<&2, U32>, List<&2, U32>, value =>
            Core.aes_byte_at(value, 0n) <> Core.gcm_ctr_stream_exact.go(fuel, words, Core.gcm_inc32(counter), List.tail(&2, U32, value)),
            Core.aes256_encrypt_expanded(words, counter), block, same))

Uses (10):
  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.tail
  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=aes256_encrypt_expanded
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=aes_byte_at
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_ctr_stream_exact.go
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_inc32