AESMaskedXorProof.ctr_decrypt_ciphertext_roundtrip: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend as AESMaskedXorProof
Lines 276-315 of qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&start_line=276&end_line=315

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_ZipLengthProof.bend as ZipLengthProof

def ctr_decrypt_ciphertext_roundtrip(+words: List<&2, U32>,
    +nonce: List<&2, U32>, +plaintext: List<&2, U32>,
    +valid: {Core.gcm_bytes_valid(plaintext) == True{} : Bool}) ->
    {Core.gcm_decrypt_expanded(words, nonce,
        Core.gcm_zip_xor(plaintext,
            Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
                words, Core.gcm_inc32(Core.gcm_j0(nonce))))) ==
     plaintext : List<&2, U32>}:
    +start = Core.gcm_inc32(Core.gcm_j0(nonce))
    +stream = Core.gcm_ctr_stream_exact(
        List.length(&2, U32, plaintext), words, start)
    +same_length = Equal.sym(Nat,
        List.length(&2, U32, stream),
        List.length(&2, U32, plaintext),
        ZipLengthProof.ctr_stream_exact_length(
            List.length(&2, U32, plaintext), words, start))
    cipher_length = ZipLengthProof.zip_length_equal(plaintext, stream,
        same_length)
    decrypt_stream = Equal.cong(Nat, List<&2, U32>,
        fuel => Core.gcm_ctr_stream_exact(fuel, words, start),
        List.length(&2, U32,
            Core.gcm_zip_xor(plaintext, stream)),
        List.length(&2, U32, plaintext), cipher_length)
    Equal.trans(List<&2, U32>,
        Core.gcm_decrypt_expanded(words, nonce,
            Core.gcm_zip_xor(plaintext, stream)),
        Core.gcm_zip_xor(Core.gcm_zip_xor(plaintext, stream), stream),
        plaintext,
        Equal.cong(List<&2, U32>, List<&2, U32>,
            stream2 => Core.gcm_zip_xor(
                Core.gcm_zip_xor(plaintext, stream), stream2),
            Core.gcm_ctr_stream_exact(
                List.length(&2, U32,
                    Core.gcm_zip_xor(plaintext, stream)), words, start),
            stream, decrypt_stream),
        Equal.trans(List<&2, U32>,
            Core.gcm_zip_xor(Core.gcm_zip_xor(plaintext, stream), stream),
            Core.gcm_mask_bytes(plaintext), plaintext,
            zip_xor_involution(plaintext, stream, same_length),
            mask_bytes_identity(plaintext, valid)))

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.sym
  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.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_bytes_valid
  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_decrypt_expanded
  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/libs/AES256GCMCore.bend&name=gcm_mask_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_zip_xor
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&name=mask_bytes_identity
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&name=zip_xor_involution
  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