def envelope_equal

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

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend as Certificate

33def envelope_equal(+nonce: AES.Nonce, +ciphertext: List<&2, U32>,
34    +tag: AES.Tag, +valid: {AES.bytes_valid(ciphertext) == True{} : Bool},
35    +expected_ciphertext: List<&2, U32>, +expected_tag: AES.Tag,
36    same_ciphertext: {ciphertext == expected_ciphertext : List<&2, U32>},
37    same_tag: {tag == expected_tag : AES.Tag}) ->
38    @+expected_valid: {AES.bytes_valid(expected_ciphertext) == True{} : Bool} ->
39    {AES.Envelope{nonce, ciphertext, tag, valid} ==
40     AES.Envelope{nonce, expected_ciphertext, expected_tag, expected_valid} :
41        AES.Envelope}:
42    %same_ciphertext :
43        @+expected_valid: {AES.bytes_valid(_) == True{} : Bool} ->
44        {AES.Envelope{nonce, ciphertext, tag, valid} ==
45         AES.Envelope{nonce, _, expected_tag, expected_valid} : AES.Envelope}
46    expected_valid =>
47        Equal.trans(AES.Envelope,
48            AES.Envelope{nonce, ciphertext, tag, valid},
49            AES.Envelope{nonce, ciphertext, expected_tag, valid},
50            AES.Envelope{nonce, ciphertext, expected_tag, expected_valid},
51            Equal.cong(AES.Tag, AES.Envelope,
52                value => AES.Envelope{nonce, ciphertext, value, valid},
53                tag, expected_tag, same_tag),
54            Equal.cong({AES.bytes_valid(ciphertext) == True{} : Bool},
55                AES.Envelope,
56                proof => AES.Envelope{nonce, ciphertext, expected_tag, proof},
57                valid, expected_valid,
58                Certificate.bool_unique(AES.bytes_valid(ciphertext), True{},
59                    valid, expected_valid)))