1	import Base
2	import ../libs/AES256GCM.bend as AES
3	import ./AES_StringEqProof.bend as StringEq
4	
5	def encoding_or(text: String,
6	    result: Result<&2, &2, AES.Error, AES.Envelope>) -> String:
7	    match result:
8	        case Fail{error}: text
9	        case Done{envelope}: AES.encode(envelope)
10	
11	def canonical_sound_done(+text: String, +found: AES.Envelope,
12	    +envelope: AES.Envelope, canonical: Bool,
13	    link: {canonical == String.eq(AES.encode(found), text) : Bool},
14	    accepted: {AES.parse_canonical_decision(text, found, canonical) ==
15	        Done{envelope} : Result<&2, &2, AES.Error, AES.Envelope>}) ->
16	    {AES.encode(envelope) == text : String}:
17	    match canonical:
18	        case False{}:
19	            status = Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>,
20	                Bool,
21	                r => Result.is_done(&2, &2, AES.Error, AES.Envelope, r),
22	                AES.parse_canonical_decision(text, found, False{}),
23	                Done{envelope}, accepted)
24	            Empty.absurd({AES.encode(envelope) == text : String},
25	                StringEq.false_true(status))
26	        case True{}:
27	            encoded = Equal.cong(
28	                Result<&2, &2, AES.Error, AES.Envelope>, String,
29	                r => encoding_or(text, r),
30	                AES.parse_canonical_decision(text, found, True{}),
31	                Done{envelope}, accepted)
32	            Equal.trans(String,
33	                AES.encode(envelope), AES.encode(found), text,
34	                Equal.sym(String,
35	                    AES.encode(found), AES.encode(envelope), encoded),
36	                StringEq.string_eq_sound(AES.encode(found), text,
37	                    Equal.sym(Bool, True{},
38	                        String.eq(AES.encode(found), text), link)))
39	
40	def canonical_sound(+text: String,
41	    result: Result<&2, &2, AES.Error, AES.Envelope>,
42	    +envelope: AES.Envelope,
43	    accepted: {AES.parse_canonical(text, result) == Done{envelope} :
44	        Result<&2, &2, AES.Error, AES.Envelope>}) ->
45	    {AES.encode(envelope) == text : String}:
46	    match result:
47	        case Fail{error}:
48	            status = Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>, Bool,
49	                r => Result.is_done(&2, &2, AES.Error, AES.Envelope, r),
50	                AES.parse_canonical(text, Fail{error}), Done{envelope},
51	                accepted)
52	            Empty.absurd({AES.encode(envelope) == text : String},
53	                StringEq.false_true(status))
54	        case Done{+found}:
55	            canonical_sound_done(text, found, envelope,
56	                String.eq(AES.encode(found), text), {==}, accepted)
57	
58	def canonical_law(+text: String, +envelope: AES.Envelope,
59	    +parsed: {AES.parse(text) == Done{envelope} :
60	        Result<&2, &2, AES.Error, AES.Envelope>}) ->
61	    {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
62	        AES.parse(text)) == Done{text} :
63	        Result<&2, &2, AES.Error, String>}:
64	    encoded = canonical_sound(text,
65	        AES.parse_fields(String.split(text, Chr{46})), envelope, parsed)
66	    Equal.trans(Result<&2, &2, AES.Error, String>,
67	        Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
68	            AES.parse(text)),
69	        Done{AES.encode(envelope)}, Done{text},
70	        Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>,
71	            Result<&2, &2, AES.Error, String>,
72	            result => Result.map(&2, &2, AES.Error, AES.Envelope, String,
73	                AES.encode, result),
74	            AES.parse(text), Done{envelope}, parsed),
75	        Equal.cong(String, Result<&2, &2, AES.Error, String>,
76	            value => Done{value}, AES.encode(envelope), text, encoded))
77	
78	def map_done_text(+text: String,
79	    result: Result<&2, &2, AES.Error, String>) -> String:
80	    match result:
81	        case Fail{error}: text
82	        case Done{value}: value
83	
84	def canonical_map_from_encoded(+text: String,
85	    result: Result<&2, &2, AES.Error, AES.Envelope>,
86	    encoded: {Result.map(&2, &2, AES.Error, AES.Envelope, String,
87	        AES.encode, result) == Done{text} :
88	        Result<&2, &2, AES.Error, String>}) ->
89	    {Result.map(&2, &2, AES.Error, AES.Envelope, String,
90	        AES.encode, AES.parse_canonical(text, result)) == Done{text} :
91	        Result<&2, &2, AES.Error, String>}:
92	    match result:
93	        case Fail{error}:
94	            status = Equal.cong(Result<&2, &2, AES.Error, String>, Bool,
95	                r => Result.is_done(&2, &2, AES.Error, String, r),
96	                Fail{error}, Done{text}, encoded)
97	            Empty.absurd(
98	                {Result.map(&2, &2, AES.Error, AES.Envelope, String,
99	                    AES.encode, AES.parse_canonical(text, Fail{error})) ==
100	                    Done{text} : Result<&2, &2, AES.Error, String>},
101	                StringEq.false_true(status))
102	        case Done{+found}:
103	            found_text = Equal.cong(Result<&2, &2, AES.Error, String>,
104	                String, r => map_done_text(text, r),
105	                Done{AES.encode(found)}, Done{text}, encoded)
106	            %found_text :
107	                {Result.map(&2, &2, AES.Error, AES.Envelope, String,
108	                    AES.encode, AES.parse_canonical(_, Done{found})) ==
109	                 Done{_} : Result<&2, &2, AES.Error, String>}
110	            Equal.cong(Bool,
111	                Result<&2, &2, AES.Error, String>,
112	                b => Result.map(&2, &2, AES.Error, AES.Envelope,
113	                    String, AES.encode,
114	                    AES.parse_canonical_decision(AES.encode(found), found, b)),
115	                String.eq(AES.encode(found), AES.encode(found)), True{},
116	                StringEq.string_eq_self(AES.encode(found)))