AESEncryptProof.successful_encrypt_ctr_decrypts: def of qasim-bend-kit@0.1.0.2 Import: import qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend as AESEncryptProof Lines 364-404 of qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend&start_line=364&end_line=404 import Base 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_MaskedXorProof.bend as MaskedXorProof def successful_encrypt_ctr_decrypts(+key: AES.SecretKey, +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>, +envelope: AES.Envelope, aad_valid: {AES.aad_valid(aad) == True{} : Bool}, +plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool}, +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, AES.Error, AES.Envelope>}) -> {Core.gcm_decrypt_raw(AES.secret_key_bytes(key), AES.raw_nonce_bytes(nonce), AES.ciphertext(envelope)) == plaintext : List<&2, U32>}: +words = Core.aes256_expand(AES.secret_key_bytes(key)) aes_bytes_valid = MaskedXorProof.bool_and_true_left( AES.bytes_valid(plaintext), AES.bytes_length_limit(plaintext, 4294967264, 15), plaintext_valid) core_bytes_valid = Equal.trans(Bool, Core.gcm_bytes_valid(plaintext), AES.bytes_valid(plaintext), True{}, Equal.sym(Bool, AES.bytes_valid(plaintext), Core.gcm_bytes_valid(plaintext), AES.core_bytes_valid_eq(plaintext)), aes_bytes_valid) cipher = successful_encrypt_ciphertext_matches_ctr(key, nonce, aad, plaintext, envelope, aad_valid, plaintext_valid, encrypted) Equal.trans(List<&2, U32>, Core.gcm_decrypt_raw(AES.secret_key_bytes(key), AES.raw_nonce_bytes(nonce), AES.ciphertext(envelope)), Core.gcm_decrypt_raw(AES.secret_key_bytes(key), AES.raw_nonce_bytes(nonce), Core.gcm_zip_xor(plaintext, Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext), words, Core.gcm_inc32(Core.gcm_j0( AES.raw_nonce_bytes(nonce)))))), plaintext, Equal.cong(List<&2, U32>, List<&2, U32>, ciphertext => Core.gcm_decrypt_raw(AES.secret_key_bytes(key), AES.raw_nonce_bytes(nonce), ciphertext), AES.ciphertext(envelope), Core.gcm_zip_xor(plaintext, Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext), words, Core.gcm_inc32(Core.gcm_j0( AES.raw_nonce_bytes(nonce))))), cipher), MaskedXorProof.ctr_decrypt_ciphertext_roundtrip(words, AES.raw_nonce_bytes(nonce), plaintext, core_bytes_valid)) Uses (31): 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=Result 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/AES256GCM.bend&name=Envelope https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Error https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Nonce https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=SecretKey https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=aad_valid https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=bytes_length_limit https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=bytes_valid https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=ciphertext https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=core_bytes_valid_eq https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=encrypt https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=plaintext_valid 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/AES256GCM.bend&name=secret_key_bytes https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=aes256_expand 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_raw 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_zip_xor https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EncryptProof.bend&name=successful_encrypt_ciphertext_matches_ctr https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&name=bool_and_true_left https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&name=ctr_decrypt_ciphertext_roundtrip