def ctr_encrypt_ciphertext_length

qasim-bend-kit@0.1.0.2 · proof/AES_ZipLengthProof.bend:178

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

178def ctr_encrypt_ciphertext_length(+words: List<&2, U32>,
179    +nonce: List<&2, U32>, +plaintext: List<&2, U32>) ->
180    {List.length(&2, U32,
181        Core.gcm_ciphertext_bytes(
182            Core.gcm_ctr_encrypt(words, nonce, plaintext))) ==
183     List.length(&2, U32, plaintext) : Nat}:
184    +start = Core.gcm_inc32(Core.gcm_j0(nonce))
185    +stream = Core.gcm_ctr_stream_exact(
186        List.length(&2, U32, plaintext), words, start)
187    zip_length_equal(plaintext, stream,
188        Equal.sym(Nat,
189            List.length(&2, U32, stream),
190            List.length(&2, U32, plaintext),
191            ctr_stream_exact_length(List.length(&2, U32, plaintext),
192                words, start)))