def ctr_decrypt_ciphertext_roundtrip

qasim-bend-kit@0.1.0.2 · proof/AES_MaskedXorProof.bend:276

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

276def ctr_decrypt_ciphertext_roundtrip(+words: List<&2, U32>,
277    +nonce: List<&2, U32>, +plaintext: List<&2, U32>,
278    +valid: {Core.gcm_bytes_valid(plaintext) == True{} : Bool}) ->
279    {Core.gcm_decrypt_expanded(words, nonce,
280        Core.gcm_zip_xor(plaintext,
281            Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
282                words, Core.gcm_inc32(Core.gcm_j0(nonce))))) ==
283     plaintext : List<&2, U32>}:
284    +start = Core.gcm_inc32(Core.gcm_j0(nonce))
285    +stream = Core.gcm_ctr_stream_exact(
286        List.length(&2, U32, plaintext), words, start)
287    +same_length = Equal.sym(Nat,
288        List.length(&2, U32, stream),
289        List.length(&2, U32, plaintext),
290        ZipLengthProof.ctr_stream_exact_length(
291            List.length(&2, U32, plaintext), words, start))
292    cipher_length = ZipLengthProof.zip_length_equal(plaintext, stream,
293        same_length)
294    decrypt_stream = Equal.cong(Nat, List<&2, U32>,
295        fuel => Core.gcm_ctr_stream_exact(fuel, words, start),
296        List.length(&2, U32,
297            Core.gcm_zip_xor(plaintext, stream)),
298        List.length(&2, U32, plaintext), cipher_length)
299    Equal.trans(List<&2, U32>,
300        Core.gcm_decrypt_expanded(words, nonce,
301            Core.gcm_zip_xor(plaintext, stream)),
302        Core.gcm_zip_xor(Core.gcm_zip_xor(plaintext, stream), stream),
303        plaintext,
304        Equal.cong(List<&2, U32>, List<&2, U32>,
305            stream2 => Core.gcm_zip_xor(
306                Core.gcm_zip_xor(plaintext, stream), stream2),
307            Core.gcm_ctr_stream_exact(
308                List.length(&2, U32,
309                    Core.gcm_zip_xor(plaintext, stream)), words, start),
310            stream, decrypt_stream),
311        Equal.trans(List<&2, U32>,
312            Core.gcm_zip_xor(Core.gcm_zip_xor(plaintext, stream), stream),
313            Core.gcm_mask_bytes(plaintext), plaintext,
314            zip_xor_involution(plaintext, stream, same_length),
315            mask_bytes_identity(plaintext, valid)))