1	import Base
2	import ../libs/AES256GCM.bend as AES
3	import ../libs/AES256GCMCore.bend as Core
4	import ./AES_EnvelopeProof.bend as Encoding
5	import ./AES_ConstructorProof.bend as Constructor
6	import ./AES_KnownAnswerProof.bend as Known
7	import ./AES_MaskedXorProof.bend as Masked
8	import ./AES_StringEqProof.bend as Logic
9	
10	def mask_word_same(+value: U32) ->
11	    {AES.hex_mask(value, 255) == Core.gcm_hex_mask(value, 255) : U32}:
12	    match value:
13	        case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
14	
15	def mask_same(+bytes: List<&2, U32>) ->
16	    {Encoding.aes_hex_mask_bytes(bytes) == Core.gcm_mask_bytes(bytes) : List<&2, U32>}:
17	    match bytes:
18	        case Nil{}: {==}
19	        case byte <> tail:
20	            Equal.trans(List<&2, U32>, Encoding.aes_hex_mask_bytes(byte <> tail),
21	                Core.gcm_hex_mask(byte, 255) <> Encoding.aes_hex_mask_bytes(tail), Core.gcm_mask_bytes(byte <> tail),
22	                Equal.cong(U32, List<&2, U32>, value => value <> Encoding.aes_hex_mask_bytes(tail),
23	                    AES.hex_mask(byte, 255), Core.gcm_hex_mask(byte, 255), mask_word_same(byte)),
24	                Equal.cong(List<&2, U32>, List<&2, U32>, xs => Core.gcm_hex_mask(byte, 255) <> xs,
25	                    Encoding.aes_hex_mask_bytes(tail), Core.gcm_mask_bytes(tail), mask_same(tail)))
26	
27	def mask_identity(+bytes: List<&2, U32>, valid: {AES.bytes_valid(bytes) == True{} : Bool}) ->
28	    {Encoding.aes_hex_mask_bytes(bytes) == bytes : List<&2, U32>}:
29	    core_valid = Equal.trans(Bool, Core.gcm_bytes_valid(bytes), AES.bytes_valid(bytes), True{},
30	        Equal.sym(Bool, AES.bytes_valid(bytes), Core.gcm_bytes_valid(bytes), AES.core_bytes_valid_eq(bytes)), valid)
31	    Equal.trans(List<&2, U32>, Encoding.aes_hex_mask_bytes(bytes), Core.gcm_mask_bytes(bytes), bytes,
32	        mask_same(bytes), Masked.mask_bytes_identity(bytes, core_valid))
33	
34	def decoded_or_empty(value: Maybe<&2, List<&2, U32>>) -> List<&2, U32>:
35	    match value:
36	        case None{}: Nil{}
37	        case Some{bytes}: bytes
38	
39	def hex_injective(+first: List<&2, U32>, +second: List<&2, U32>,
40	    first_valid: {AES.bytes_valid(first) == True{} : Bool},
41	    second_valid: {AES.bytes_valid(second) == True{} : Bool},
42	    same: {AES.hex_bytes(first) == AES.hex_bytes(second) : String}) ->
43	    {first == second : List<&2, U32>}:
44	    decoded = Equal.trans(Maybe<&2, List<&2, U32>>,
45	        Some{Encoding.aes_hex_mask_bytes(first)}, AES.decode_hex(AES.hex_bytes(first)),
46	        Some{Encoding.aes_hex_mask_bytes(second)},
47	        Equal.sym(Maybe<&2, List<&2, U32>>, AES.decode_hex(AES.hex_bytes(first)),
48	            Some{Encoding.aes_hex_mask_bytes(first)}, Encoding.aes_decode_hex_bytes(first)),
49	        Equal.trans(Maybe<&2, List<&2, U32>>, AES.decode_hex(AES.hex_bytes(first)),
50	            AES.decode_hex(AES.hex_bytes(second)), Some{Encoding.aes_hex_mask_bytes(second)},
51	            Equal.cong(String, Maybe<&2, List<&2, U32>>, AES.decode_hex,
52	                AES.hex_bytes(first), AES.hex_bytes(second), same), Encoding.aes_decode_hex_bytes(second)))
53	    masks_equal = Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, decoded_or_empty,
54	        Some{Encoding.aes_hex_mask_bytes(first)}, Some{Encoding.aes_hex_mask_bytes(second)}, decoded)
55	    Equal.trans(List<&2, U32>, first, Encoding.aes_hex_mask_bytes(first), second,
56	        Equal.sym(List<&2, U32>, Encoding.aes_hex_mask_bytes(first), first, mask_identity(first, first_valid)),
57	        Equal.trans(List<&2, U32>, Encoding.aes_hex_mask_bytes(first), Encoding.aes_hex_mask_bytes(second),
58	            second, masks_equal, mask_identity(second, second_valid)))
59	
60	def fields(+envelope: AES.Envelope) -> List<&2, String>:
61	    ["v1", AES.hex_bytes(AES.fixed_bytes(12n, AES.nonce_bytes(AES.envelope_nonce(envelope)))),
62	        AES.hex_bytes(AES.fixed_bytes(16n, AES.tag_bytes(AES.envelope_tag(envelope)))),
63	        AES.hex_bytes(AES.ciphertext(envelope))]
64	
65	def optional_text(value: Maybe<&2, String>) -> String:
66	    match value:
67	        case None{}: ""
68	        case Some{text}: text
69	
70	def field_text(index: Nat, parts: List<&2, String>) -> String:
71	    optional_text(List.get(&2, String, parts, index))
72	
73	def result_text(value: Result<&2, &2, AES.Error, String>) -> String:
74	    match value:
75	        case Fail{error}: ""
76	        case Done{text}: text
77	
78	def fields_equal(+first: AES.Envelope, +second: AES.Envelope,
79	    same: {AES.encode(first) == AES.encode(second) : String}) ->
80	    {fields(first) == fields(second) : List<&2, String>}:
81	    Equal.trans(List<&2, String>, fields(first), String.split(AES.encode(first), Chr{46}), fields(second),
82	        Equal.sym(List<&2, String>, String.split(AES.encode(first), Chr{46}), fields(first),
83	            Encoding.aes_encode_fields_split(first)),
84	        Equal.trans(List<&2, String>, String.split(AES.encode(first), Chr{46}),
85	            String.split(AES.encode(second), Chr{46}), fields(second),
86	            Equal.cong(String, List<&2, String>, text => String.split(text, Chr{46}),
87	                AES.encode(first), AES.encode(second), same), Encoding.aes_encode_fields_split(second)))
88	
89	def fixed_hex_equal(+n: Nat, +first: List<&2, U32>, +second: List<&2, U32>,
90	    first_size: {List.length(&2, U32, first) == n : Nat},
91	    second_size: {List.length(&2, U32, second) == n : Nat},
92	    same: {AES.hex_bytes(AES.fixed_bytes(n, first)) == AES.hex_bytes(AES.fixed_bytes(n, second)) : String}) ->
93	    {AES.hex_bytes(first) == AES.hex_bytes(second) : String}:
94	    first_path = Equal.cong(List<&2, U32>, String, bytes => AES.hex_bytes(bytes),
95	        AES.fixed_bytes(n, first), first, Encoding.aes_fixed_bytes_identity(n, first, first_size))
96	    second_path = Equal.cong(List<&2, U32>, String, bytes => AES.hex_bytes(bytes),
97	        AES.fixed_bytes(n, second), second, Encoding.aes_fixed_bytes_identity(n, second, second_size))
98	    Equal.trans(String, AES.hex_bytes(first), AES.hex_bytes(AES.fixed_bytes(n, first)), AES.hex_bytes(second),
99	        Equal.sym(String, AES.hex_bytes(AES.fixed_bytes(n, first)), AES.hex_bytes(first), first_path),
100	        Equal.trans(String, AES.hex_bytes(AES.fixed_bytes(n, first)), AES.hex_bytes(AES.fixed_bytes(n, second)),
101	            AES.hex_bytes(second), same, second_path))
102	
103	def encode_injective(+first: AES.Envelope, +second: AES.Envelope,
104	    same: {AES.encode(first) == AES.encode(second) : String}) -> {first == second : AES.Envelope}:
105	    match first second:
106	        case AES.Envelope{AES.Nonce{+bytes_a, +size_a, +nonce_valid_a},
107	                 +cipher_a, AES.Tag{+tag_bytes_a, +tag_size_a, +tag_valid_a}, +valid_a}
108	             AES.Envelope{AES.Nonce{+bytes_b, +size_b, +nonce_valid_b},
109	                 +cipher_b, AES.Tag{+tag_bytes_b, +tag_size_b, +tag_valid_b}, +valid_b}:
110	            +size_a_copy = size_a
111	            +size_b_copy = size_b
112	            +nonce_valid_a_copy = nonce_valid_a
113	            +nonce_valid_b_copy = nonce_valid_b
114	            +nonce_a = {AES.Nonce{bytes_a, size_a_copy, nonce_valid_a_copy} : AES.Nonce}
115	            +nonce_b = {AES.Nonce{bytes_b, size_b_copy, nonce_valid_b_copy} : AES.Nonce}
116	            +tag_a = {AES.Tag{tag_bytes_a, tag_size_a, tag_valid_a} : AES.Tag}
117	            +tag_b = {AES.Tag{tag_bytes_b, tag_size_b, tag_valid_b} : AES.Tag}
118	            +parts_same = fields_equal(first, second, same)
119	            nonce_hex = Equal.cong(List<&2, String>, String, parts => field_text(1n, parts),
120	                fields(first), fields(second), parts_same)
121	            tag_hex = Equal.cong(List<&2, String>, String, parts => field_text(2n, parts),
122	                fields(first), fields(second), parts_same)
123	            cipher_hex = Equal.cong(List<&2, String>, String, parts => field_text(3n, parts),
124	                fields(first), fields(second), parts_same)
125	            nonce_bytes_same = hex_injective(bytes_a, bytes_b, nonce_valid_a_copy, nonce_valid_b_copy,
126	                fixed_hex_equal(12n, bytes_a, bytes_b, size_a_copy, size_b_copy, nonce_hex))
127	            tag_bytes_same = hex_injective(tag_bytes_a, tag_bytes_b, tag_valid_a, tag_valid_b,
128	                fixed_hex_equal(16n, tag_bytes_a, tag_bytes_b, tag_size_a, tag_size_b, tag_hex))
129	            cipher_same = hex_injective(cipher_a, cipher_b, valid_a, valid_b, cipher_hex)
130	            nonce_same = Constructor.nonce_equal(bytes_a, size_a_copy, nonce_valid_a_copy, bytes_b,
131	                nonce_bytes_same, size_b_copy, nonce_valid_b_copy)
132	            tag_same = Known.tag_equal(tag_bytes_a, tag_size_a, tag_valid_a, tag_bytes_b,
133	                tag_bytes_same, tag_size_b, tag_valid_b)
134	            fields_same = Known.envelope_equal(nonce_a, cipher_a, tag_a, valid_a,
135	                cipher_b, tag_b, cipher_same, tag_same, valid_b)
136	            Equal.trans(AES.Envelope, first, AES.Envelope{nonce_a, cipher_b, tag_b, valid_b}, second,
137	                fields_same, Equal.cong(AES.Nonce, AES.Envelope,
138	                    nonce => AES.Envelope{nonce, cipher_b, tag_b, valid_b}, nonce_a, nonce_b, nonce_same))
139	
140	def exact_roundtrip_result(+envelope: AES.Envelope,
141	    result: Result<&2, &2, AES.Error, AES.Envelope>,
142	    encoded: {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode, result) ==
143	        Done{AES.encode(envelope)} : Result<&2, &2, AES.Error, String>}) ->
144	    {result == Done{envelope} : Result<&2, &2, AES.Error, AES.Envelope>}:
145	    match result:
146	        case Fail{error}:
147	            status = Equal.cong(Result<&2, &2, AES.Error, String>, Bool,
148	                value => Result.is_done(&2, &2, AES.Error, String, value),
149	                Fail{error}, Done{AES.encode(envelope)}, encoded)
150	            Empty.absurd({Fail{error} == Done{envelope} : Result<&2, &2, AES.Error, AES.Envelope>},
151	                Logic.false_true(status))
152	        case Done{+found}:
153	            text_same = Equal.cong(Result<&2, &2, AES.Error, String>, String,
154	                result_text,
155	                Done{AES.encode(found)}, Done{AES.encode(envelope)}, encoded)
156	            Equal.cong(AES.Envelope, Result<&2, &2, AES.Error, AES.Envelope>, value => Done{value},
157	                found, envelope, encode_injective(found, envelope, text_same))
158	
159	def exact_roundtrip(+envelope: AES.Envelope) ->
160	    {AES.parse(AES.encode(envelope)) == Done{envelope} : Result<&2, &2, AES.Error, AES.Envelope>}:
161	    exact_roundtrip_result(envelope, AES.parse(AES.encode(envelope)), Encoding.aes_envelope_roundtrip(envelope))