def canonical_sound_done

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

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

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