def output_matches

qasim-bend-kit@0.1.0.2 · proof/AES_KnownAnswerProof.bend:61

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_CoreTagProof.bend as Fields

61def output_matches(+nonce: AES.Nonce, +output: Core.GcmOutput,
62    +ciphertext: List<&2, U32>, +tag_bytes: List<&2, U32>,
63    ciphertext_matches: {Fields.output_ciphertext(output) == ciphertext :
64        List<&2, U32>},
65    tag_matches: {Fields.output_tag(output) == tag_bytes : List<&2, U32>}) ->
66    @+tag_size: {List.length(&2, U32, tag_bytes) == 16n : Nat} ->
67    @+tag_valid: {AES.bytes_valid(tag_bytes) == True{} : Bool} ->
68    @+ciphertext_valid: {AES.bytes_valid(ciphertext) == True{} : Bool} ->
69    {AES.encrypt_output_from_gcm(nonce, output) ==
70     Done{AES.Envelope{nonce, ciphertext,
71        AES.Tag{tag_bytes, tag_size, tag_valid}, ciphertext_valid}} :
72        Result<&2, &2, AES.Error, AES.Envelope>}:
73    match output:
74        case Core.GcmOutput{+actual_ciphertext, actual_ciphertext_valid,
75            +actual_tag, actual_tag_valid, actual_tag_size, _, _, _, _}:
76            tag_size => tag_valid => ciphertext_valid =>
77                +actual_valid = AES.core_bytes_valid_proof(actual_ciphertext,
78                    actual_ciphertext_valid)
79                +actual_tag_value = {AES.Tag{actual_tag, actual_tag_size,
80                    AES.core_bytes_valid_proof(actual_tag, actual_tag_valid)} :
81                    AES.Tag}
82                +expected_tag_value = {AES.Tag{tag_bytes, tag_size, tag_valid} :
83                    AES.Tag}
84                tag_eq = tag_equal(actual_tag, actual_tag_size,
85                    AES.core_bytes_valid_proof(actual_tag, actual_tag_valid),
86                    tag_bytes, tag_matches, tag_size, tag_valid)
87                envelope_eq = envelope_equal(nonce, actual_ciphertext,
88                    actual_tag_value, actual_valid, ciphertext,
89                    expected_tag_value, ciphertext_matches, tag_eq,
90                    ciphertext_valid)
91                Equal.cong(AES.Envelope,
92                    Result<&2, &2, AES.Error, AES.Envelope>, value => Done{value},
93                    AES.envelope_from_gcm_checked(nonce, output),
94                    AES.Envelope{nonce, ciphertext, expected_tag_value,
95                        ciphertext_valid}, envelope_eq)