AESZipLengthProof.ctr_encrypt_ciphertext_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 178-192 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=178&end_line=192

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

def ctr_encrypt_ciphertext_length(+words: List<&2, U32>,
    +nonce: List<&2, U32>, +plaintext: List<&2, U32>) ->
    {List.length(&2, U32,
        Core.gcm_ciphertext_bytes(
            Core.gcm_ctr_encrypt(words, nonce, plaintext))) ==
     List.length(&2, U32, plaintext) : Nat}:
    +start = Core.gcm_inc32(Core.gcm_j0(nonce))
    +stream = Core.gcm_ctr_stream_exact(
        List.length(&2, U32, plaintext), words, start)
    zip_length_equal(plaintext, stream,
        Equal.sym(Nat,
            List.length(&2, U32, stream),
            List.length(&2, U32, plaintext),
            ctr_stream_exact_length(List.length(&2, U32, plaintext),
                words, start)))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  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=gcm_ciphertext_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/libs/AES256GCMCore.bend&name=gcm_ctr_stream_exact
  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/libs/AES256GCMCore.bend&name=gcm_j0
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&name=ctr_stream_exact_length
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&name=zip_length_equal