AESIdentityProof.exact_roundtrip_result: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend as AESIdentityProof
Lines 140-157 of qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend&start_line=140&end_line=157

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

def exact_roundtrip_result(+envelope: AES.Envelope,
    result: Result<&2, &2, AES.Error, AES.Envelope>,
    encoded: {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode, result) ==
        Done{AES.encode(envelope)} : Result<&2, &2, AES.Error, String>}) ->
    {result == Done{envelope} : Result<&2, &2, AES.Error, AES.Envelope>}:
    match result:
        case Fail{error}:
            status = Equal.cong(Result<&2, &2, AES.Error, String>, Bool,
                value => Result.is_done(&2, &2, AES.Error, String, value),
                Fail{error}, Done{AES.encode(envelope)}, encoded)
            Empty.absurd({Fail{error} == Done{envelope} : Result<&2, &2, AES.Error, AES.Envelope>},
                Logic.false_true(status))
        case Done{+found}:
            text_same = Equal.cong(Result<&2, &2, AES.Error, String>, String,
                result_text,
                Done{AES.encode(found)}, Done{AES.encode(envelope)}, encoded)
            Equal.cong(AES.Envelope, Result<&2, &2, AES.Error, AES.Envelope>, value => Done{value},
                found, envelope, encode_injective(found, envelope, text_same))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.is_done
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.map
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Envelope
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=encode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend&name=encode_injective
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend&name=result_text
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_StringEqProof.bend&name=false_true