proof/AES_CanonicalProof.bend
qasim-bend-kit@0.1.0.2 · 116 lines · 6 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
3import qasim-bend-kit@0.1.0.2/proof/AES_StringEqProof.bend as StringEq
4
5def 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
11def 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
40def 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
58def 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
78def 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
84def 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)))