def aes_parse_decoded_if_some

qasim-bend-kit@0.1.0.2 · proof/AES_EnvelopeProof.bend:795

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

795def aes_parse_decoded_if_some(+nonce: List<&2, U32>,
796    +tag: List<&2, U32>, +ciphertext: List<&2, U32>,
797    ns: Maybe<&0, {List.length(&2, U32,
798        aes_hex_mask_bytes(nonce)) == 12n : Nat}>,
799    ts: Maybe<&0, {List.length(&2, U32,
800        aes_hex_mask_bytes(tag)) == 16n : Nat}>,
801    nv: Maybe<&0, {AES.bytes_valid(aes_hex_mask_bytes(nonce)) ==
802        True{} : Bool}>,
803    tv: Maybe<&0, {AES.bytes_valid(aes_hex_mask_bytes(tag)) ==
804        True{} : Bool}>,
805    cv: Maybe<&0, {AES.bytes_valid(aes_hex_mask_bytes(ciphertext)) ==
806        True{} : Bool}>,
807    ns_present: {Maybe.is_some(&0,
808        {List.length(&2, U32, aes_hex_mask_bytes(nonce)) == 12n : Nat},
809        ns) == True{} : Bool},
810    ts_present: {Maybe.is_some(&0,
811        {List.length(&2, U32, aes_hex_mask_bytes(tag)) == 16n : Nat},
812        ts) == True{} : Bool},
813    nv_present: {Maybe.is_some(&0,
814        {AES.bytes_valid(aes_hex_mask_bytes(nonce)) == True{} : Bool},
815        nv) == True{} : Bool},
816    tv_present: {Maybe.is_some(&0,
817        {AES.bytes_valid(aes_hex_mask_bytes(tag)) == True{} : Bool},
818        tv) == True{} : Bool},
819    cv_present: {Maybe.is_some(&0,
820        {AES.bytes_valid(aes_hex_mask_bytes(ciphertext)) == True{} : Bool},
821        cv) == True{} : Bool}) ->
822    {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
823        AES.parse_decoded(aes_hex_mask_bytes(nonce),
824            aes_hex_mask_bytes(tag), aes_hex_mask_bytes(ciphertext),
825            ns, ts, nv, tv, cv)) ==
826     Done{"v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++
827         "." ++ AES.hex_bytes(ciphertext)} :
828        Result<&2, &2, AES.Error, String>}:
829    match ns:
830        case None{}:
831            Empty.absurd(aes_parse_decoded_map_goal(nonce, tag,
832                ciphertext, None{}, ts, nv, tv, cv),
833                aes_false_true(ns_present))
834        case Some{ns_proof}:
835            match ts:
836                case None{}:
837                    Empty.absurd(aes_parse_decoded_map_goal(nonce, tag,
838                        ciphertext, Some{ns_proof}, None{}, nv, tv, cv),
839                        aes_false_true(ts_present))
840                case Some{ts_proof}:
841                    match nv:
842                        case None{}:
843                            Empty.absurd(aes_parse_decoded_map_goal(nonce,
844                                tag, ciphertext, Some{ns_proof},
845                                Some{ts_proof}, None{}, tv, cv),
846                                aes_false_true(nv_present))
847                        case Some{nv_proof}:
848                            match tv:
849                                case None{}:
850                                    Empty.absurd(aes_parse_decoded_map_goal(
851                                        nonce, tag, ciphertext,
852                                        Some{ns_proof}, Some{ts_proof},
853                                        Some{nv_proof}, None{}, cv),
854                                        aes_false_true(tv_present))
855                                case Some{tv_proof}:
856                                    match cv:
857                                        case None{}:
858                                            Empty.absurd(
859                                                aes_parse_decoded_map_goal(
860                                                    nonce, tag, ciphertext,
861                                                    Some{ns_proof},
862                                                    Some{ts_proof},
863                                                    Some{nv_proof},
864                                                    Some{tv_proof}, None{}),
865                                                aes_false_true(cv_present))
866                                        case Some{cv_proof}:
867                                            aes_parse_decoded_masked_map(
868                                                nonce, tag, ciphertext,
869                                                ns_proof, ts_proof,
870                                                nv_proof, tv_proof,
871                                                cv_proof)