AESNistCtrProof.checkpoint_ctr3_stream: 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 35-43 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=35&end_line=43

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
import qasim-bend-kit@0.1.0.2/proof/AES_NistKeyScheduleProof.bend as Key
import qasim-bend-kit@0.1.0.2/proof/AES_NistCtr3BlockProof.bend as B3
import qasim-bend-kit@0.1.0.2/proof/AES_NistCtr3ComposeProof.bend as P3

def checkpoint_ctr3_stream(+remaining: Nat, +fuel: Nat, +next_counter: List<&2, U32>,
    count: {remaining == 16n+fuel : Nat},
    counter: {Core.gcm_inc32(B3.block()) == next_counter : List<&2, U32>}) ->
    {Core.gcm_ctr_stream_exact.go(remaining, Key.words_60(), B3.block(), Nil{}) == List.append(&2, U32, B3.result(), Core.gcm_ctr_stream_exact.go(fuel, Key.words_60(), next_counter, Nil{})) : List<&2, U32>}:
    Equal.trans(List<&2, U32>, Core.gcm_ctr_stream_exact.go(remaining, Key.words_60(), B3.block(), Nil{}), Core.aes_byte_at(B3.result(), 0n) <> Core.gcm_ctr_stream_exact.go(15n+fuel, Key.words_60(), Core.gcm_inc32(B3.block()), List.tail(&2, U32, B3.result())), List.append(&2, U32, B3.result(), Core.gcm_ctr_stream_exact.go(fuel, Key.words_60(), next_counter, Nil{})),
        stream_step(remaining, 15n+fuel, Key.words_60(), B3.block(), B3.result(), count, P3.expanded_block_matches()),
        Equal.trans(List<&2, U32>, Core.aes_byte_at(B3.result(), 0n) <> Core.gcm_ctr_stream_exact.go(15n+fuel, Key.words_60(), Core.gcm_inc32(B3.block()), List.tail(&2, U32, B3.result())), List.append(&2, U32, B3.result(), Core.gcm_ctr_stream_exact.go(fuel, Key.words_60(), Core.gcm_inc32(B3.block()), Nil{})), List.append(&2, U32, B3.result(), Core.gcm_ctr_stream_exact.go(fuel, Key.words_60(), next_counter, Nil{})), {==},
            Equal.cong(List<&2, U32>, List<&2, U32>, next => List.append(&2, U32, B3.result(), Core.gcm_ctr_stream_exact.go(fuel, Key.words_60(), next, Nil{})),
                Core.gcm_inc32(B3.block()), next_counter, counter)))

Uses (15):
  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.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=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
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistCtr3BlockProof.bend&name=block
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistCtr3BlockProof.bend&name=result
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistCtr3ComposeProof.bend&name=expanded_block_matches
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistCtrProof.bend&name=stream_step
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistKeyScheduleProof.bend&name=words_60