AESNistCtrProof.checkpoint_ctr5_partial: 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 78-82 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=78&end_line=82

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_NistCtr5BlockProof.bend as B5
import qasim-bend-kit@0.1.0.2/proof/AES_NistCtr5ComposeProof.bend as P5

def checkpoint_ctr5_partial() ->
    {Core.gcm_ctr_stream_exact.go(12n, Key.words_60(), B5.block(), Nil{}) == List.take(&2, U32, B5.result(), 12n) : List<&2, U32>}:
    Equal.trans(List<&2, U32>, Core.gcm_ctr_stream_exact.go(12n, Key.words_60(), B5.block(), Nil{}),
        Core.aes_byte_at(B5.result(), 0n) <> Core.gcm_ctr_stream_exact.go(11n, Key.words_60(), Core.gcm_inc32(B5.block()), List.tail(&2, U32, B5.result())),
        List.take(&2, U32, B5.result(), 12n), stream_step(12n, 11n, Key.words_60(), B5.block(), B5.result(), {==}, P5.expanded_block_matches()), {==})

Uses (13):
  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=List.take
  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_NistCtr5BlockProof.bend&name=block
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistCtr5BlockProof.bend&name=result
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistCtr5ComposeProof.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