def exact_roundtrip_result

qasim-bend-kit@0.1.0.2 · proof/AES_IdentityProof.bend:140

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 Logic

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