1	import Base
2	import ../libs/AES256GCM.bend as AES
3	import ../libs/AES256GCMCore.bend as Core
4	import ./AES_TagCompareProof.bend as Compare
5	
6	def rejects_comparison(+words: List<&2, U32>,
7	    +envelope: AES.Envelope, +supplied: List<&2, U32>,
8	    +expected: List<&2, U32>,
9	    changed: {supplied != expected : List<&2, U32>}) ->
10	    {AES.decrypt_auth_result(words, envelope,
11	        AES.bytes_equal_full_scan(supplied, expected)) ==
12	     Fail{AES.AuthenticationFailed{}} :
13	        Result<&2, &2, AES.Error, List<&2, U32>>}:
14	    Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>,
15	        authenticated => AES.decrypt_auth_result(words, envelope,
16	            authenticated),
17	        AES.bytes_equal_full_scan(supplied, expected), False{},
18	        Compare.unequal_is_false(supplied, expected, changed))
19	
20	def rejects_tag(+words: List<&2, U32>, +nonce: List<&2, U32>,
21	    +aad: List<&2, U32>, +ciphertext: List<&2, U32>,
22	    +envelope: AES.Envelope, +tag: AES.Tag,
23	    +original: List<&2, U32>,
24	    canonical: {original == Core.gcm_tag_bytes(Core.gcm_tag_output(
25	        words, nonce, aad, ciphertext)) : List<&2, U32>},
26	    changed: {AES.tag_bytes(tag) != original : List<&2, U32>}) ->
27	    {AES.decrypt_authenticated_tag(words, nonce, aad, ciphertext, envelope,
28	        tag) == Fail{AES.AuthenticationFailed{}} :
29	        Result<&2, &2, AES.Error, List<&2, U32>>}:
30	    match tag:
31	        case AES.Tag{bytes, size, valid}:
32	            rejects_comparison(words, envelope, bytes,
33	                Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad,
34	                    ciphertext)),
35	                same => changed(Equal.trans(List<&2, U32>, bytes,
36	                    Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce,
37	                        aad, ciphertext)), original, same,
38	                    Equal.sym(List<&2, U32>, original,
39	                        Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce,
40	                            aad, ciphertext)), canonical))))