1	import Base
2	import ../libs/AES256GCM.bend as AES
3	import ../libs/AES256GCMCore.bend as Core
4	import ./AES_CoreTagProof.bend as Fields
5	import ./AES_CertificateProof.bend as Certificate
6	
7	def tag_equal(+bytes: List<&2, U32>,
8	    +size: {List.length(&2, U32, bytes) == 16n : Nat},
9	    +valid: {AES.bytes_valid(bytes) == True{} : Bool},
10	    +expected: List<&2, U32>, same: {bytes == expected : List<&2, U32>}) ->
11	    @+expected_size: {List.length(&2, U32, expected) == 16n : Nat} ->
12	    @+expected_valid: {AES.bytes_valid(expected) == True{} : Bool} ->
13	    {AES.Tag{bytes, size, valid} ==
14	     AES.Tag{expected, expected_size, expected_valid} : AES.Tag}:
15	    %same :
16	        @+expected_size: {List.length(&2, U32, _) == 16n : Nat} ->
17	        @+expected_valid: {AES.bytes_valid(_) == True{} : Bool} ->
18	        {AES.Tag{bytes, size, valid} ==
19	         AES.Tag{_, expected_size, expected_valid} : AES.Tag}
20	    expected_size => expected_valid =>
21	        Equal.trans(AES.Tag, AES.Tag{bytes, size, valid},
22	            AES.Tag{bytes, expected_size, valid},
23	            AES.Tag{bytes, expected_size, expected_valid},
24	            Equal.cong({List.length(&2, U32, bytes) == 16n : Nat}, AES.Tag,
25	                proof => AES.Tag{bytes, proof, valid}, size, expected_size,
26	                Certificate.nat_unique(List.length(&2, U32, bytes), 16n,
27	                    size, expected_size)),
28	            Equal.cong({AES.bytes_valid(bytes) == True{} : Bool}, AES.Tag,
29	                proof => AES.Tag{bytes, expected_size, proof}, valid,
30	                expected_valid, Certificate.bool_unique(AES.bytes_valid(bytes),
31	                    True{}, valid, expected_valid)))
32	
33	def 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)))
60	
61	def 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)
96	
97	def encrypt_matches(+key: AES.SecretKey, +nonce: AES.Nonce,
98	    +aad: List<&2, U32>, +plaintext: List<&2, U32>,
99	    +ciphertext: List<&2, U32>, +tag_bytes: List<&2, U32>,
100	    aad_valid: {AES.aad_valid(aad) == True{} : Bool},
101	    plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
102	    ciphertext_matches: {Fields.output_ciphertext(AES.encrypt_valid_output(
103	        key, nonce, aad, plaintext)) == ciphertext : List<&2, U32>},
104	    tag_matches: {Fields.output_tag(AES.encrypt_valid_output(key, nonce, aad,
105	        plaintext)) == tag_bytes : List<&2, U32>},
106	    +tag_size: {List.length(&2, U32, tag_bytes) == 16n : Nat},
107	    +tag_valid: {AES.bytes_valid(tag_bytes) == True{} : Bool},
108	    +ciphertext_valid: {AES.bytes_valid(ciphertext) == True{} : Bool}) ->
109	    {AES.encrypt(key, nonce, aad, plaintext) ==
110	     Done{AES.Envelope{nonce, ciphertext,
111	        AES.Tag{tag_bytes, tag_size, tag_valid}, ciphertext_valid}} :
112	        Result<&2, &2, AES.Error, AES.Envelope>}:
113	    aad_checked = Equal.cong(Bool,
114	        Result<&2, &2, AES.Error, AES.Envelope>,
115	        flag => AES.encrypt_checked(key, nonce, aad, plaintext, flag,
116	            AES.plaintext_valid(plaintext)), AES.aad_valid(aad), True{},
117	        aad_valid)
118	    plaintext_checked = Equal.cong(Bool,
119	        Result<&2, &2, AES.Error, AES.Envelope>,
120	        flag => AES.encrypt_checked(key, nonce, aad, plaintext, True{}, flag),
121	        AES.plaintext_valid(plaintext), True{}, plaintext_valid)
122	    output_eq = output_matches(nonce,
123	        AES.encrypt_valid_output(key, nonce, aad, plaintext), ciphertext,
124	        tag_bytes, ciphertext_matches, tag_matches, tag_size, tag_valid,
125	        ciphertext_valid)
126	    Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
127	        AES.encrypt(key, nonce, aad, plaintext),
128	        AES.encrypt_valid(key, nonce, aad, plaintext),
129	        Done{AES.Envelope{nonce, ciphertext,
130	            AES.Tag{tag_bytes, tag_size, tag_valid}, ciphertext_valid}},
131	        Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
132	            AES.encrypt(key, nonce, aad, plaintext),
133	            AES.encrypt_checked(key, nonce, aad, plaintext, True{},
134	                AES.plaintext_valid(plaintext)),
135	            AES.encrypt_valid(key, nonce, aad, plaintext),
136	            aad_checked, plaintext_checked), output_eq)