AESCanonicalProof.canonical_sound_done: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_CanonicalProof.bend as AESCanonicalProof
Lines 11-38 of qasim-bend-kit@0.1.0.2/proof/AES_CanonicalProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CanonicalProof.bend&start_line=11&end_line=38

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

def canonical_sound_done(+text: String, +found: AES.Envelope,
    +envelope: AES.Envelope, canonical: Bool,
    link: {canonical == String.eq(AES.encode(found), text) : Bool},
    accepted: {AES.parse_canonical_decision(text, found, canonical) ==
        Done{envelope} : Result<&2, &2, AES.Error, AES.Envelope>}) ->
    {AES.encode(envelope) == text : String}:
    match canonical:
        case False{}:
            status = Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>,
                Bool,
                r => Result.is_done(&2, &2, AES.Error, AES.Envelope, r),
                AES.parse_canonical_decision(text, found, False{}),
                Done{envelope}, accepted)
            Empty.absurd({AES.encode(envelope) == text : String},
                StringEq.false_true(status))
        case True{}:
            encoded = Equal.cong(
                Result<&2, &2, AES.Error, AES.Envelope>, String,
                r => encoding_or(text, r),
                AES.parse_canonical_decision(text, found, True{}),
                Done{envelope}, accepted)
            Equal.trans(String,
                AES.encode(envelope), AES.encode(found), text,
                Equal.sym(String,
                    AES.encode(found), AES.encode(envelope), encoded),
                StringEq.string_eq_sound(AES.encode(found), text,
                    Equal.sym(Bool, True{},
                        String.eq(AES.encode(found), text), link)))

Uses (16):
  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=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.eq
  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/libs/AES256GCM.bend&name=parse_canonical_decision
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CanonicalProof.bend&name=encoding_or
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_StringEqProof.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_StringEqProof.bend&name=string_eq_sound