def canonical_map_from_encoded

qasim-bend-kit@0.1.0.2 · proof/AES_CanonicalProof.bend:84

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/proof/AES_StringEqProof.bend as StringEq

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)))