AESNistVectorProof.checkpoint_partial_block_ciphertext: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend as AESNistVectorProof
Lines 291-293 of qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&start_line=291&end_line=293

import Base
import qasim-bend-kit@0.1.0.2/LAWS.bend as L
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
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_NistObservationProof.bend as Obs
import qasim-bend-kit@0.1.0.2/proof/AES_NistCtrProof.bend as Ctr

def checkpoint_partial_block_ciphertext() ->
    {Obs.ciphertext(Core.gcm_ctr_encrypt(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), partial_block_plaintext())) == partial_block_ciphertext() : List<&2, U32>}:
    Obs.finish_cipher(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), partial_block_plaintext(), Ctr.stream_60(), partial_block_ciphertext(), checkpoint_partial_block_plaintext_stream(), {==})

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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/LAWS.bend&name=aes256gcm_nist_nonce
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=raw_nonce_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_ctr_encrypt
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistCtrProof.bend&name=stream_60
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistKeyScheduleProof.bend&name=words_60
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&name=ciphertext
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&name=finish_cipher
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&name=checkpoint_partial_block_plaintext_stream
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&name=partial_block_ciphertext
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&name=partial_block_plaintext