(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module extension.
  Module confidential_transfer.
    Module account_info.
      (* StructRecord
        {
          name := "EmptyAccountAccountInfo";
          ty_params := [];
          fields :=
            [
              ("available_balance",
                Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext")
            ];
        } *)
      
      Module Impl_core_clone_Clone_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo".
        
        (* Clone *)
        Definition clone (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  Value.DeclaredButUndefined,
                  [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
                |)
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::clone::Clone"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method clone) ].
      End Impl_core_clone_Clone_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
      
      Module Impl_core_marker_Copy_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::Copy"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_Copy_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
      
      Module Impl_core_fmt_Debug_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo".
        
        (* Debug *)
        Definition fmt (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "debug_struct_field1_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "EmptyAccountAccountInfo" |);
                  M.read (| Value.String "available_balance" |);
                  (* Unsize *)
                  M.pointer_coercion
                    (M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo",
                        "available_balance"
                      |)
                    |))
                ]
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::fmt::Debug"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
      End Impl_core_fmt_Debug_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
      
      Module Impl_core_default_Default_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo".
        
        (* Default *)
        Definition default (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo"
                [
                  ("available_balance",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path
                          "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                        [],
                        "default",
                        []
                      |),
                      []
                    |))
                ]))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::default::Default"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method default) ].
      End Impl_core_default_Default_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
      
      Module Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
      
      Module Impl_core_cmp_PartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo".
        
        (* PartialEq *)
        Definition eq (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                  [ Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext"
                  ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo",
                    "available_balance"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo",
                    "available_balance"
                  |)
                ]
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::cmp::PartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("eq", InstanceField.Method eq) ].
      End Impl_core_cmp_PartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
      
      Module Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "bytemuck::pod::Pod"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
      
      Module Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "bytemuck::zeroable::Zeroable"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
      
      Module Impl_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo".
        
        (*
            pub fn new(account: &ConfidentialTransferAccount) -> Self {
                Self {
                    available_balance: account.available_balance,
                }
            }
        *)
        Definition new (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ account ] =>
            ltac:(M.monadic
              (let account := M.alloc (| account |) in
              Value.StructRecord
                "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo"
                [
                  ("available_balance",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| account |),
                        "spl_token_2022::extension::confidential_transfer::ConfidentialTransferAccount",
                        "available_balance"
                      |)
                    |))
                ]))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
        
        (*
            pub fn generate_proof_data(
                &self,
                elgamal_keypair: &ElGamalKeypair,
            ) -> Result<ZeroBalanceProofData, TokenError> {
                let available_balance = self
                    .available_balance
                    .try_into()
                    .map_err(|_| TokenError::MalformedCiphertext)?;
        
                ZeroBalanceProofData::new(elgamal_keypair, &available_balance)
                    .map_err(|_| TokenError::ProofGeneration)
            }
        *)
        Definition generate_proof_data (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; elgamal_keypair ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let elgamal_keypair := M.alloc (| elgamal_keypair |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [
                                    Ty.path
                                      "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                    Ty.path "spl_token_2022::error::TokenError"
                                  ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      [
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                      ],
                                    "map_err",
                                    [
                                      Ty.path "spl_token_2022::error::TokenError";
                                      Ty.function
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path
                                                "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                            ]
                                        ]
                                        (Ty.path "spl_token_2022::error::TokenError")
                                    ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::TryInto",
                                        Ty.path
                                          "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                                        [
                                          Ty.path
                                            "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext"
                                        ],
                                        "try_into",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "spl_token_2022::extension::confidential_transfer::account_info::EmptyAccountAccountInfo",
                                            "available_balance"
                                          |)
                                        |)
                                      ]
                                    |);
                                    M.closure
                                      (fun γ =>
                                        ltac:(M.monadic
                                          match γ with
                                          | [ α0 ] =>
                                            M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (Value.StructTuple
                                                      "spl_token_2022::error::TokenError::MalformedCiphertext"
                                                      []))
                                              ]
                                            |)
                                          | _ => M.impossible (||)
                                          end))
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::instruction::zero_balance::ZeroBalanceProofData";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::result::Result")
                            [
                              Ty.path
                                "solana_zk_token_sdk::instruction::zero_balance::ZeroBalanceProofData";
                              Ty.path "solana_zk_token_sdk::errors::ProofGenerationError"
                            ],
                          "map_err",
                          [
                            Ty.path "spl_token_2022::error::TokenError";
                            Ty.function
                              [
                                Ty.tuple
                                  [ Ty.path "solana_zk_token_sdk::errors::ProofGenerationError" ]
                              ]
                              (Ty.path "spl_token_2022::error::TokenError")
                          ]
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path
                                "solana_zk_token_sdk::instruction::zero_balance::ZeroBalanceProofData",
                              "new",
                              []
                            |),
                            [ M.read (| elgamal_keypair |); available_balance ]
                          |);
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [ α0 ] =>
                                  M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (Value.StructTuple
                                            "spl_token_2022::error::TokenError::ProofGeneration"
                                            []))
                                    ]
                                  |)
                                | _ => M.impossible (||)
                                end))
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_generate_proof_data :
          M.IsAssociatedFunction Self "generate_proof_data" generate_proof_data.
      End Impl_spl_token_2022_extension_confidential_transfer_account_info_EmptyAccountAccountInfo.
      
      (* StructRecord
        {
          name := "ApplyPendingBalanceAccountInfo";
          ty_params := [];
          fields :=
            [
              ("pending_balance_credit_counter", Ty.path "spl_pod::primitives::PodU64");
              ("pending_balance_lo",
                Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext");
              ("pending_balance_hi",
                Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext");
              ("decryptable_available_balance",
                Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext")
            ];
        } *)
      
      Module Impl_core_clone_Clone_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo".
        
        (* Clone *)
        Definition clone (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  Value.DeclaredButUndefined,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          Value.DeclaredButUndefined,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  Value.DeclaredButUndefined,
                                  [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
                                |)))
                          ]
                        |)))
                  ]
                |)
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::clone::Clone"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method clone) ].
      End Impl_core_clone_Clone_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
      
      Module Impl_core_marker_Copy_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::Copy"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_Copy_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
      
      Module Impl_core_fmt_Debug_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo".
        
        (* Debug *)
        Definition fmt (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "debug_struct_field4_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "ApplyPendingBalanceAccountInfo" |);
                  M.read (| Value.String "pending_balance_credit_counter" |);
                  (* Unsize *)
                  M.pointer_coercion
                    (M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                      "pending_balance_credit_counter"
                    |));
                  M.read (| Value.String "pending_balance_lo" |);
                  (* Unsize *)
                  M.pointer_coercion
                    (M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                      "pending_balance_lo"
                    |));
                  M.read (| Value.String "pending_balance_hi" |);
                  (* Unsize *)
                  M.pointer_coercion
                    (M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                      "pending_balance_hi"
                    |));
                  M.read (| Value.String "decryptable_available_balance" |);
                  (* Unsize *)
                  M.pointer_coercion
                    (M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                        "decryptable_available_balance"
                      |)
                    |))
                ]
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::fmt::Debug"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
      End Impl_core_fmt_Debug_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
      
      Module Impl_core_default_Default_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo".
        
        (* Default *)
        Definition default (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo"
                [
                  ("pending_balance_credit_counter",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path "spl_pod::primitives::PodU64",
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("pending_balance_lo",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path
                          "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("pending_balance_hi",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path
                          "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("decryptable_available_balance",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path
                          "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext",
                        [],
                        "default",
                        []
                      |),
                      []
                    |))
                ]))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::default::Default"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method default) ].
      End Impl_core_default_Default_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
      
      Module Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
      
      Module Impl_core_cmp_PartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo".
        
        (* PartialEq *)
        Definition eq (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              LogicalOp.and (|
                LogicalOp.and (|
                  LogicalOp.and (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.path "spl_pod::primitives::PodU64",
                        [ Ty.path "spl_pod::primitives::PodU64" ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                          "pending_balance_credit_counter"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                          "pending_balance_credit_counter"
                        |)
                      ]
                    |),
                    ltac:(M.monadic
                      (M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialEq",
                          Ty.path
                            "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                          [
                            Ty.path
                              "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext"
                          ],
                          "eq",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                            "pending_balance_lo"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                            "pending_balance_lo"
                          |)
                        ]
                      |)))
                  |),
                  ltac:(M.monadic
                    (M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.path
                          "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                        [
                          Ty.path
                            "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext"
                        ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                          "pending_balance_hi"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                          "pending_balance_hi"
                        |)
                      ]
                    |)))
                |),
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.path
                        "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext",
                      [
                        Ty.path
                          "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext"
                      ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                        "decryptable_available_balance"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                        "decryptable_available_balance"
                      |)
                    ]
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::cmp::PartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("eq", InstanceField.Method eq) ].
      End Impl_core_cmp_PartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
      
      Module Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "bytemuck::pod::Pod"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
      
      Module Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "bytemuck::zeroable::Zeroable"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
      
      Module Impl_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo".
        
        (*
            pub fn new(account: &ConfidentialTransferAccount) -> Self {
                Self {
                    pending_balance_credit_counter: account.pending_balance_credit_counter,
                    pending_balance_lo: account.pending_balance_lo,
                    pending_balance_hi: account.pending_balance_hi,
                    decryptable_available_balance: account.decryptable_available_balance,
                }
            }
        *)
        Definition new (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ account ] =>
            ltac:(M.monadic
              (let account := M.alloc (| account |) in
              Value.StructRecord
                "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo"
                [
                  ("pending_balance_credit_counter",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| account |),
                        "spl_token_2022::extension::confidential_transfer::ConfidentialTransferAccount",
                        "pending_balance_credit_counter"
                      |)
                    |));
                  ("pending_balance_lo",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| account |),
                        "spl_token_2022::extension::confidential_transfer::ConfidentialTransferAccount",
                        "pending_balance_lo"
                      |)
                    |));
                  ("pending_balance_hi",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| account |),
                        "spl_token_2022::extension::confidential_transfer::ConfidentialTransferAccount",
                        "pending_balance_hi"
                      |)
                    |));
                  ("decryptable_available_balance",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| account |),
                        "spl_token_2022::extension::confidential_transfer::ConfidentialTransferAccount",
                        "decryptable_available_balance"
                      |)
                    |))
                ]))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
        
        (*
            pub fn pending_balance_credit_counter(&self) -> u64 {
                self.pending_balance_credit_counter.into()
            }
        *)
        Definition pending_balance_credit_counter (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::Into",
                  Ty.path "spl_pod::primitives::PodU64",
                  [ Ty.path "u64" ],
                  "into",
                  []
                |),
                [
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                      "pending_balance_credit_counter"
                    |)
                  |)
                ]
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_pending_balance_credit_counter :
          M.IsAssociatedFunction
            Self
            "pending_balance_credit_counter"
            pending_balance_credit_counter.
        
        (*
            fn decrypted_pending_balance_lo(
                &self,
                elgamal_secret_key: &ElGamalSecretKey,
            ) -> Result<u64, TokenError> {
                let pending_balance_lo = self
                    .pending_balance_lo
                    .try_into()
                    .map_err(|_| TokenError::MalformedCiphertext)?;
                elgamal_secret_key
                    .decrypt_u32(&pending_balance_lo)
                    .ok_or(TokenError::AccountDecryption)
            }
        *)
        Definition decrypted_pending_balance_lo (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; elgamal_secret_key ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let elgamal_secret_key := M.alloc (| elgamal_secret_key |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let pending_balance_lo :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [
                                    Ty.path
                                      "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                    Ty.path "spl_token_2022::error::TokenError"
                                  ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      [
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                      ],
                                    "map_err",
                                    [
                                      Ty.path "spl_token_2022::error::TokenError";
                                      Ty.function
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path
                                                "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                            ]
                                        ]
                                        (Ty.path "spl_token_2022::error::TokenError")
                                    ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::TryInto",
                                        Ty.path
                                          "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                                        [
                                          Ty.path
                                            "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext"
                                        ],
                                        "try_into",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                                            "pending_balance_lo"
                                          |)
                                        |)
                                      ]
                                    |);
                                    M.closure
                                      (fun γ =>
                                        ltac:(M.monadic
                                          match γ with
                                          | [ α0 ] =>
                                            M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (Value.StructTuple
                                                      "spl_token_2022::error::TokenError::MalformedCiphertext"
                                                      []))
                                              ]
                                            |)
                                          | _ => M.impossible (||)
                                          end))
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path "u64";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::option::Option") [ Ty.path "u64" ],
                          "ok_or",
                          [ Ty.path "spl_token_2022::error::TokenError" ]
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "solana_zk_token_sdk::encryption::elgamal::ElGamalSecretKey",
                              "decrypt_u32",
                              []
                            |),
                            [ M.read (| elgamal_secret_key |); pending_balance_lo ]
                          |);
                          Value.StructTuple
                            "spl_token_2022::error::TokenError::AccountDecryption"
                            []
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_decrypted_pending_balance_lo :
          M.IsAssociatedFunction Self "decrypted_pending_balance_lo" decrypted_pending_balance_lo.
        
        (*
            fn decrypted_pending_balance_hi(
                &self,
                elgamal_secret_key: &ElGamalSecretKey,
            ) -> Result<u64, TokenError> {
                let pending_balance_hi = self
                    .pending_balance_hi
                    .try_into()
                    .map_err(|_| TokenError::MalformedCiphertext)?;
                elgamal_secret_key
                    .decrypt_u32(&pending_balance_hi)
                    .ok_or(TokenError::AccountDecryption)
            }
        *)
        Definition decrypted_pending_balance_hi (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; elgamal_secret_key ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let elgamal_secret_key := M.alloc (| elgamal_secret_key |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let pending_balance_hi :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [
                                    Ty.path
                                      "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                    Ty.path "spl_token_2022::error::TokenError"
                                  ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      [
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                      ],
                                    "map_err",
                                    [
                                      Ty.path "spl_token_2022::error::TokenError";
                                      Ty.function
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path
                                                "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                            ]
                                        ]
                                        (Ty.path "spl_token_2022::error::TokenError")
                                    ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::TryInto",
                                        Ty.path
                                          "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                                        [
                                          Ty.path
                                            "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext"
                                        ],
                                        "try_into",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                                            "pending_balance_hi"
                                          |)
                                        |)
                                      ]
                                    |);
                                    M.closure
                                      (fun γ =>
                                        ltac:(M.monadic
                                          match γ with
                                          | [ α0 ] =>
                                            M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (Value.StructTuple
                                                      "spl_token_2022::error::TokenError::MalformedCiphertext"
                                                      []))
                                              ]
                                            |)
                                          | _ => M.impossible (||)
                                          end))
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path "u64";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::option::Option") [ Ty.path "u64" ],
                          "ok_or",
                          [ Ty.path "spl_token_2022::error::TokenError" ]
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "solana_zk_token_sdk::encryption::elgamal::ElGamalSecretKey",
                              "decrypt_u32",
                              []
                            |),
                            [ M.read (| elgamal_secret_key |); pending_balance_hi ]
                          |);
                          Value.StructTuple
                            "spl_token_2022::error::TokenError::AccountDecryption"
                            []
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_decrypted_pending_balance_hi :
          M.IsAssociatedFunction Self "decrypted_pending_balance_hi" decrypted_pending_balance_hi.
        
        (*
            fn decrypted_available_balance(&self, aes_key: &AeKey) -> Result<u64, TokenError> {
                let decryptable_available_balance = self
                    .decryptable_available_balance
                    .try_into()
                    .map_err(|_| TokenError::MalformedCiphertext)?;
                aes_key
                    .decrypt(&decryptable_available_balance)
                    .ok_or(TokenError::AccountDecryption)
            }
        *)
        Definition decrypted_available_balance (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; aes_key ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let aes_key := M.alloc (| aes_key |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let decryptable_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [
                                    Ty.path
                                      "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                    Ty.path "spl_token_2022::error::TokenError"
                                  ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      [
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::auth_encryption::AuthenticatedEncryptionError"
                                      ],
                                    "map_err",
                                    [
                                      Ty.path "spl_token_2022::error::TokenError";
                                      Ty.function
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path
                                                "solana_zk_token_sdk::encryption::auth_encryption::AuthenticatedEncryptionError"
                                            ]
                                        ]
                                        (Ty.path "spl_token_2022::error::TokenError")
                                    ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::TryInto",
                                        Ty.path
                                          "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext",
                                        [
                                          Ty.path
                                            "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext"
                                        ],
                                        "try_into",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                                            "decryptable_available_balance"
                                          |)
                                        |)
                                      ]
                                    |);
                                    M.closure
                                      (fun γ =>
                                        ltac:(M.monadic
                                          match γ with
                                          | [ α0 ] =>
                                            M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (Value.StructTuple
                                                      "spl_token_2022::error::TokenError::MalformedCiphertext"
                                                      []))
                                              ]
                                            |)
                                          | _ => M.impossible (||)
                                          end))
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path "u64";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::option::Option") [ Ty.path "u64" ],
                          "ok_or",
                          [ Ty.path "spl_token_2022::error::TokenError" ]
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "solana_zk_token_sdk::encryption::auth_encryption::AeKey",
                              "decrypt",
                              []
                            |),
                            [ M.read (| aes_key |); decryptable_available_balance ]
                          |);
                          Value.StructTuple
                            "spl_token_2022::error::TokenError::AccountDecryption"
                            []
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_decrypted_available_balance :
          M.IsAssociatedFunction Self "decrypted_available_balance" decrypted_available_balance.
        
        (*
            pub fn new_decryptable_available_balance(
                &self,
                elgamal_secret_key: &ElGamalSecretKey,
                aes_key: &AeKey,
            ) -> Result<AeCiphertext, TokenError> {
                let decrypted_pending_balance_lo = self.decrypted_pending_balance_lo(elgamal_secret_key)?;
                let decrypted_pending_balance_hi = self.decrypted_pending_balance_hi(elgamal_secret_key)?;
                let pending_balance =
                    combine_balances(decrypted_pending_balance_lo, decrypted_pending_balance_hi)
                        .ok_or(TokenError::AccountDecryption)?;
                let current_available_balance = self.decrypted_available_balance(aes_key)?;
                let new_decrypted_available_balance = current_available_balance
                    .checked_add(pending_balance)
                    .unwrap(); // total balance cannot exceed `u64`
        
                Ok(aes_key.encrypt(new_decrypted_available_balance))
            }
        *)
        Definition new_decryptable_available_balance (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; elgamal_secret_key; aes_key ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let elgamal_secret_key := M.alloc (| elgamal_secret_key |) in
              let aes_key := M.alloc (| aes_key |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let decrypted_pending_balance_lo :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [ Ty.path "u64"; Ty.path "spl_token_2022::error::TokenError" ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path
                                      "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                                    "decrypted_pending_balance_lo",
                                    []
                                  |),
                                  [ M.read (| self |); M.read (| elgamal_secret_key |) ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    let decrypted_pending_balance_hi :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [ Ty.path "u64"; Ty.path "spl_token_2022::error::TokenError" ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path
                                      "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                                    "decrypted_pending_balance_hi",
                                    []
                                  |),
                                  [ M.read (| self |); M.read (| elgamal_secret_key |) ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    let pending_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [ Ty.path "u64"; Ty.path "spl_token_2022::error::TokenError" ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::option::Option") [ Ty.path "u64" ],
                                    "ok_or",
                                    [ Ty.path "spl_token_2022::error::TokenError" ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_function (|
                                        "spl_token_2022::extension::confidential_transfer::account_info::combine_balances",
                                        []
                                      |),
                                      [
                                        M.read (| decrypted_pending_balance_lo |);
                                        M.read (| decrypted_pending_balance_hi |)
                                      ]
                                    |);
                                    Value.StructTuple
                                      "spl_token_2022::error::TokenError::AccountDecryption"
                                      []
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    let current_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [ Ty.path "u64"; Ty.path "spl_token_2022::error::TokenError" ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path
                                      "spl_token_2022::extension::confidential_transfer::account_info::ApplyPendingBalanceAccountInfo",
                                    "decrypted_available_balance",
                                    []
                                  |),
                                  [ M.read (| self |); M.read (| aes_key |) ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    let new_decrypted_available_balance :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::option::Option") [ Ty.path "u64" ],
                            "unwrap",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "u64", "checked_add", [] |),
                              [ M.read (| current_available_balance |); M.read (| pending_balance |)
                              ]
                            |)
                          ]
                        |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "solana_zk_token_sdk::encryption::auth_encryption::AeKey",
                              "encrypt",
                              []
                            |),
                            [ M.read (| aes_key |); M.read (| new_decrypted_available_balance |) ]
                          |)
                        ]
                    |)
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_new_decryptable_available_balance :
          M.IsAssociatedFunction
            Self
            "new_decryptable_available_balance"
            new_decryptable_available_balance.
      End Impl_spl_token_2022_extension_confidential_transfer_account_info_ApplyPendingBalanceAccountInfo.
      
      (* StructRecord
        {
          name := "WithdrawAccountInfo";
          ty_params := [];
          fields :=
            [
              ("available_balance",
                Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext");
              ("decryptable_available_balance",
                Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext")
            ];
        } *)
      
      Module Impl_core_clone_Clone_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo".
        
        (* Clone *)
        Definition clone (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  Value.DeclaredButUndefined,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          Value.DeclaredButUndefined,
                          [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
                        |)))
                  ]
                |)
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::clone::Clone"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method clone) ].
      End Impl_core_clone_Clone_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
      
      Module Impl_core_marker_Copy_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::Copy"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_Copy_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
      
      Module Impl_core_fmt_Debug_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo".
        
        (* Debug *)
        Definition fmt (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "debug_struct_field2_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "WithdrawAccountInfo" |);
                  M.read (| Value.String "available_balance" |);
                  (* Unsize *)
                  M.pointer_coercion
                    (M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo",
                      "available_balance"
                    |));
                  M.read (| Value.String "decryptable_available_balance" |);
                  (* Unsize *)
                  M.pointer_coercion
                    (M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo",
                        "decryptable_available_balance"
                      |)
                    |))
                ]
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::fmt::Debug"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
      End Impl_core_fmt_Debug_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
      
      Module Impl_core_default_Default_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo".
        
        (* Default *)
        Definition default (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo"
                [
                  ("available_balance",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path
                          "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("decryptable_available_balance",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path
                          "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext",
                        [],
                        "default",
                        []
                      |),
                      []
                    |))
                ]))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::default::Default"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method default) ].
      End Impl_core_default_Default_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
      
      Module Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
      
      Module Impl_core_cmp_PartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo".
        
        (* PartialEq *)
        Definition eq (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              LogicalOp.and (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.path
                      "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                    [
                      Ty.path
                        "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext"
                    ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo",
                      "available_balance"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo",
                      "available_balance"
                    |)
                  ]
                |),
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.path
                        "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext",
                      [
                        Ty.path
                          "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext"
                      ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo",
                        "decryptable_available_balance"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo",
                        "decryptable_available_balance"
                      |)
                    ]
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::cmp::PartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("eq", InstanceField.Method eq) ].
      End Impl_core_cmp_PartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
      
      Module Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "bytemuck::pod::Pod"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
      
      Module Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "bytemuck::zeroable::Zeroable"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
      
      Module Impl_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo".
        
        (*
            pub fn new(account: &ConfidentialTransferAccount) -> Self {
                Self {
                    available_balance: account.available_balance,
                    decryptable_available_balance: account.decryptable_available_balance,
                }
            }
        *)
        Definition new (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ account ] =>
            ltac:(M.monadic
              (let account := M.alloc (| account |) in
              Value.StructRecord
                "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo"
                [
                  ("available_balance",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| account |),
                        "spl_token_2022::extension::confidential_transfer::ConfidentialTransferAccount",
                        "available_balance"
                      |)
                    |));
                  ("decryptable_available_balance",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| account |),
                        "spl_token_2022::extension::confidential_transfer::ConfidentialTransferAccount",
                        "decryptable_available_balance"
                      |)
                    |))
                ]))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
        
        (*
            fn decrypted_available_balance(&self, aes_key: &AeKey) -> Result<u64, TokenError> {
                let decryptable_available_balance = self
                    .decryptable_available_balance
                    .try_into()
                    .map_err(|_| TokenError::MalformedCiphertext)?;
                aes_key
                    .decrypt(&decryptable_available_balance)
                    .ok_or(TokenError::AccountDecryption)
            }
        *)
        Definition decrypted_available_balance (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; aes_key ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let aes_key := M.alloc (| aes_key |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let decryptable_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [
                                    Ty.path
                                      "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                    Ty.path "spl_token_2022::error::TokenError"
                                  ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      [
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::auth_encryption::AuthenticatedEncryptionError"
                                      ],
                                    "map_err",
                                    [
                                      Ty.path "spl_token_2022::error::TokenError";
                                      Ty.function
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path
                                                "solana_zk_token_sdk::encryption::auth_encryption::AuthenticatedEncryptionError"
                                            ]
                                        ]
                                        (Ty.path "spl_token_2022::error::TokenError")
                                    ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::TryInto",
                                        Ty.path
                                          "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext",
                                        [
                                          Ty.path
                                            "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext"
                                        ],
                                        "try_into",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo",
                                            "decryptable_available_balance"
                                          |)
                                        |)
                                      ]
                                    |);
                                    M.closure
                                      (fun γ =>
                                        ltac:(M.monadic
                                          match γ with
                                          | [ α0 ] =>
                                            M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (Value.StructTuple
                                                      "spl_token_2022::error::TokenError::MalformedCiphertext"
                                                      []))
                                              ]
                                            |)
                                          | _ => M.impossible (||)
                                          end))
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path "u64";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::option::Option") [ Ty.path "u64" ],
                          "ok_or",
                          [ Ty.path "spl_token_2022::error::TokenError" ]
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "solana_zk_token_sdk::encryption::auth_encryption::AeKey",
                              "decrypt",
                              []
                            |),
                            [ M.read (| aes_key |); decryptable_available_balance ]
                          |);
                          Value.StructTuple
                            "spl_token_2022::error::TokenError::AccountDecryption"
                            []
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_decrypted_available_balance :
          M.IsAssociatedFunction Self "decrypted_available_balance" decrypted_available_balance.
        
        (*
            pub fn generate_proof_data(
                &self,
                withdraw_amount: u64,
                elgamal_keypair: &ElGamalKeypair,
                aes_key: &AeKey,
            ) -> Result<WithdrawData, TokenError> {
                let current_available_balance = self
                    .available_balance
                    .try_into()
                    .map_err(|_| TokenError::MalformedCiphertext)?;
                let current_decrypted_available_balance = self.decrypted_available_balance(aes_key)?;
        
                WithdrawData::new(
                    withdraw_amount,
                    elgamal_keypair,
                    current_decrypted_available_balance,
                    &current_available_balance,
                )
                .map_err(|_| TokenError::ProofGeneration)
            }
        *)
        Definition generate_proof_data (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; withdraw_amount; elgamal_keypair; aes_key ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let withdraw_amount := M.alloc (| withdraw_amount |) in
              let elgamal_keypair := M.alloc (| elgamal_keypair |) in
              let aes_key := M.alloc (| aes_key |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let current_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [
                                    Ty.path
                                      "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                    Ty.path "spl_token_2022::error::TokenError"
                                  ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      [
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                      ],
                                    "map_err",
                                    [
                                      Ty.path "spl_token_2022::error::TokenError";
                                      Ty.function
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path
                                                "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                            ]
                                        ]
                                        (Ty.path "spl_token_2022::error::TokenError")
                                    ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::TryInto",
                                        Ty.path
                                          "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                                        [
                                          Ty.path
                                            "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext"
                                        ],
                                        "try_into",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo",
                                            "available_balance"
                                          |)
                                        |)
                                      ]
                                    |);
                                    M.closure
                                      (fun γ =>
                                        ltac:(M.monadic
                                          match γ with
                                          | [ α0 ] =>
                                            M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (Value.StructTuple
                                                      "spl_token_2022::error::TokenError::MalformedCiphertext"
                                                      []))
                                              ]
                                            |)
                                          | _ => M.impossible (||)
                                          end))
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::instruction::withdraw::WithdrawData";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    let current_decrypted_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [ Ty.path "u64"; Ty.path "spl_token_2022::error::TokenError" ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path
                                      "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo",
                                    "decrypted_available_balance",
                                    []
                                  |),
                                  [ M.read (| self |); M.read (| aes_key |) ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::instruction::withdraw::WithdrawData";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::result::Result")
                            [
                              Ty.path "solana_zk_token_sdk::instruction::withdraw::WithdrawData";
                              Ty.path "solana_zk_token_sdk::errors::ProofGenerationError"
                            ],
                          "map_err",
                          [
                            Ty.path "spl_token_2022::error::TokenError";
                            Ty.function
                              [
                                Ty.tuple
                                  [ Ty.path "solana_zk_token_sdk::errors::ProofGenerationError" ]
                              ]
                              (Ty.path "spl_token_2022::error::TokenError")
                          ]
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "solana_zk_token_sdk::instruction::withdraw::WithdrawData",
                              "new",
                              []
                            |),
                            [
                              M.read (| withdraw_amount |);
                              M.read (| elgamal_keypair |);
                              M.read (| current_decrypted_available_balance |);
                              current_available_balance
                            ]
                          |);
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [ α0 ] =>
                                  M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (Value.StructTuple
                                            "spl_token_2022::error::TokenError::ProofGeneration"
                                            []))
                                    ]
                                  |)
                                | _ => M.impossible (||)
                                end))
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_generate_proof_data :
          M.IsAssociatedFunction Self "generate_proof_data" generate_proof_data.
        
        (*
            pub fn new_decryptable_available_balance(
                &self,
                withdraw_amount: u64,
                aes_key: &AeKey,
            ) -> Result<AeCiphertext, TokenError> {
                let current_decrypted_available_balance = self.decrypted_available_balance(aes_key)?;
                let new_decrypted_available_balance = current_decrypted_available_balance
                    .checked_sub(withdraw_amount)
                    .ok_or(TokenError::InsufficientFunds)?;
        
                Ok(aes_key.encrypt(new_decrypted_available_balance))
            }
        *)
        Definition new_decryptable_available_balance (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; withdraw_amount; aes_key ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let withdraw_amount := M.alloc (| withdraw_amount |) in
              let aes_key := M.alloc (| aes_key |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let current_decrypted_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [ Ty.path "u64"; Ty.path "spl_token_2022::error::TokenError" ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path
                                      "spl_token_2022::extension::confidential_transfer::account_info::WithdrawAccountInfo",
                                    "decrypted_available_balance",
                                    []
                                  |),
                                  [ M.read (| self |); M.read (| aes_key |) ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    let new_decrypted_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [ Ty.path "u64"; Ty.path "spl_token_2022::error::TokenError" ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::option::Option") [ Ty.path "u64" ],
                                    "ok_or",
                                    [ Ty.path "spl_token_2022::error::TokenError" ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "u64",
                                        "checked_sub",
                                        []
                                      |),
                                      [
                                        M.read (| current_decrypted_available_balance |);
                                        M.read (| withdraw_amount |)
                                      ]
                                    |);
                                    Value.StructTuple
                                      "spl_token_2022::error::TokenError::InsufficientFunds"
                                      []
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "solana_zk_token_sdk::encryption::auth_encryption::AeKey",
                              "encrypt",
                              []
                            |),
                            [ M.read (| aes_key |); M.read (| new_decrypted_available_balance |) ]
                          |)
                        ]
                    |)
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_new_decryptable_available_balance :
          M.IsAssociatedFunction
            Self
            "new_decryptable_available_balance"
            new_decryptable_available_balance.
      End Impl_spl_token_2022_extension_confidential_transfer_account_info_WithdrawAccountInfo.
      
      (* StructRecord
        {
          name := "TransferAccountInfo";
          ty_params := [];
          fields :=
            [
              ("available_balance",
                Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext");
              ("decryptable_available_balance",
                Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext")
            ];
        } *)
      
      Module Impl_core_clone_Clone_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo".
        
        (* Clone *)
        Definition clone (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  Value.DeclaredButUndefined,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          Value.DeclaredButUndefined,
                          [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
                        |)))
                  ]
                |)
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::clone::Clone"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method clone) ].
      End Impl_core_clone_Clone_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
      
      Module Impl_core_marker_Copy_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::Copy"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_Copy_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
      
      Module Impl_core_fmt_Debug_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo".
        
        (* Debug *)
        Definition fmt (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "debug_struct_field2_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "TransferAccountInfo" |);
                  M.read (| Value.String "available_balance" |);
                  (* Unsize *)
                  M.pointer_coercion
                    (M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo",
                      "available_balance"
                    |));
                  M.read (| Value.String "decryptable_available_balance" |);
                  (* Unsize *)
                  M.pointer_coercion
                    (M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo",
                        "decryptable_available_balance"
                      |)
                    |))
                ]
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::fmt::Debug"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
      End Impl_core_fmt_Debug_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
      
      Module Impl_core_default_Default_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo".
        
        (* Default *)
        Definition default (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo"
                [
                  ("available_balance",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path
                          "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("decryptable_available_balance",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path
                          "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext",
                        [],
                        "default",
                        []
                      |),
                      []
                    |))
                ]))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::default::Default"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method default) ].
      End Impl_core_default_Default_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
      
      Module Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
      
      Module Impl_core_cmp_PartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo".
        
        (* PartialEq *)
        Definition eq (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              LogicalOp.and (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.path
                      "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                    [
                      Ty.path
                        "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext"
                    ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo",
                      "available_balance"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo",
                      "available_balance"
                    |)
                  ]
                |),
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.path
                        "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext",
                      [
                        Ty.path
                          "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext"
                      ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo",
                        "decryptable_available_balance"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo",
                        "decryptable_available_balance"
                      |)
                    ]
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::cmp::PartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("eq", InstanceField.Method eq) ].
      End Impl_core_cmp_PartialEq_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
      
      Module Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "bytemuck::pod::Pod"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
      
      Module Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo".
        
        Axiom Implements :
          M.IsTraitInstance
            "bytemuck::zeroable::Zeroable"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
      
      Module Impl_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
        Definition Self : Ty.t :=
          Ty.path
            "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo".
        
        (*
            pub fn new(account: &ConfidentialTransferAccount) -> Self {
                Self {
                    available_balance: account.available_balance,
                    decryptable_available_balance: account.decryptable_available_balance,
                }
            }
        *)
        Definition new (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ account ] =>
            ltac:(M.monadic
              (let account := M.alloc (| account |) in
              Value.StructRecord
                "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo"
                [
                  ("available_balance",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| account |),
                        "spl_token_2022::extension::confidential_transfer::ConfidentialTransferAccount",
                        "available_balance"
                      |)
                    |));
                  ("decryptable_available_balance",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| account |),
                        "spl_token_2022::extension::confidential_transfer::ConfidentialTransferAccount",
                        "decryptable_available_balance"
                      |)
                    |))
                ]))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
        
        (*
            fn decrypted_available_balance(&self, aes_key: &AeKey) -> Result<u64, TokenError> {
                let decryptable_available_balance = self
                    .decryptable_available_balance
                    .try_into()
                    .map_err(|_| TokenError::MalformedCiphertext)?;
                aes_key
                    .decrypt(&decryptable_available_balance)
                    .ok_or(TokenError::AccountDecryption)
            }
        *)
        Definition decrypted_available_balance (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; aes_key ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let aes_key := M.alloc (| aes_key |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let decryptable_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [
                                    Ty.path
                                      "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                    Ty.path "spl_token_2022::error::TokenError"
                                  ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      [
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::auth_encryption::AuthenticatedEncryptionError"
                                      ],
                                    "map_err",
                                    [
                                      Ty.path "spl_token_2022::error::TokenError";
                                      Ty.function
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path
                                                "solana_zk_token_sdk::encryption::auth_encryption::AuthenticatedEncryptionError"
                                            ]
                                        ]
                                        (Ty.path "spl_token_2022::error::TokenError")
                                    ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::TryInto",
                                        Ty.path
                                          "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext",
                                        [
                                          Ty.path
                                            "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext"
                                        ],
                                        "try_into",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo",
                                            "decryptable_available_balance"
                                          |)
                                        |)
                                      ]
                                    |);
                                    M.closure
                                      (fun γ =>
                                        ltac:(M.monadic
                                          match γ with
                                          | [ α0 ] =>
                                            M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (Value.StructTuple
                                                      "spl_token_2022::error::TokenError::MalformedCiphertext"
                                                      []))
                                              ]
                                            |)
                                          | _ => M.impossible (||)
                                          end))
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path "u64";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::option::Option") [ Ty.path "u64" ],
                          "ok_or",
                          [ Ty.path "spl_token_2022::error::TokenError" ]
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "solana_zk_token_sdk::encryption::auth_encryption::AeKey",
                              "decrypt",
                              []
                            |),
                            [ M.read (| aes_key |); decryptable_available_balance ]
                          |);
                          Value.StructTuple
                            "spl_token_2022::error::TokenError::AccountDecryption"
                            []
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_decrypted_available_balance :
          M.IsAssociatedFunction Self "decrypted_available_balance" decrypted_available_balance.
        
        (*
            pub fn generate_transfer_proof_data(
                &self,
                transfer_amount: u64,
                elgamal_keypair: &ElGamalKeypair,
                aes_key: &AeKey,
                destination_elgamal_pubkey: &ElGamalPubkey,
                auditor_elgamal_pubkey: Option<&ElGamalPubkey>,
            ) -> Result<TransferData, TokenError> {
                let current_source_available_balance = self
                    .available_balance
                    .try_into()
                    .map_err(|_| TokenError::MalformedCiphertext)?;
                let current_source_decrypted_available_balance =
                    self.decrypted_available_balance(aes_key)?;
        
                let default_auditor_pubkey = ElGamalPubkey::default();
                let auditor_elgamal_pubkey = auditor_elgamal_pubkey.unwrap_or(&default_auditor_pubkey);
        
                TransferData::new(
                    transfer_amount,
                    (
                        current_source_decrypted_available_balance,
                        &current_source_available_balance,
                    ),
                    elgamal_keypair,
                    (destination_elgamal_pubkey, auditor_elgamal_pubkey),
                )
                .map_err(|_| TokenError::ProofGeneration)
            }
        *)
        Definition generate_transfer_proof_data (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [],
              [
                self;
                transfer_amount;
                elgamal_keypair;
                aes_key;
                destination_elgamal_pubkey;
                auditor_elgamal_pubkey
              ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let transfer_amount := M.alloc (| transfer_amount |) in
              let elgamal_keypair := M.alloc (| elgamal_keypair |) in
              let aes_key := M.alloc (| aes_key |) in
              let destination_elgamal_pubkey := M.alloc (| destination_elgamal_pubkey |) in
              let auditor_elgamal_pubkey := M.alloc (| auditor_elgamal_pubkey |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let current_source_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [
                                    Ty.path
                                      "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                    Ty.path "spl_token_2022::error::TokenError"
                                  ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      [
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                      ],
                                    "map_err",
                                    [
                                      Ty.path "spl_token_2022::error::TokenError";
                                      Ty.function
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path
                                                "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                            ]
                                        ]
                                        (Ty.path "spl_token_2022::error::TokenError")
                                    ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::TryInto",
                                        Ty.path
                                          "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                                        [
                                          Ty.path
                                            "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext"
                                        ],
                                        "try_into",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo",
                                            "available_balance"
                                          |)
                                        |)
                                      ]
                                    |);
                                    M.closure
                                      (fun γ =>
                                        ltac:(M.monadic
                                          match γ with
                                          | [ α0 ] =>
                                            M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (Value.StructTuple
                                                      "spl_token_2022::error::TokenError::MalformedCiphertext"
                                                      []))
                                              ]
                                            |)
                                          | _ => M.impossible (||)
                                          end))
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::instruction::transfer::without_fee::TransferData";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    let current_source_decrypted_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [ Ty.path "u64"; Ty.path "spl_token_2022::error::TokenError" ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path
                                      "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo",
                                    "decrypted_available_balance",
                                    []
                                  |),
                                  [ M.read (| self |); M.read (| aes_key |) ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::instruction::transfer::without_fee::TransferData";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    let default_auditor_pubkey :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::default::Default",
                            Ty.path "solana_zk_token_sdk::encryption::elgamal::ElGamalPubkey",
                            [],
                            "default",
                            []
                          |),
                          []
                        |)
                      |) in
                    let auditor_elgamal_pubkey :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  [
                                    Ty.path
                                      "solana_zk_token_sdk::encryption::elgamal::ElGamalPubkey"
                                  ]
                              ],
                            "unwrap_or",
                            []
                          |),
                          [ M.read (| auditor_elgamal_pubkey |); default_auditor_pubkey ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::result::Result")
                            [
                              Ty.path
                                "solana_zk_token_sdk::instruction::transfer::without_fee::TransferData";
                              Ty.path "solana_zk_token_sdk::errors::ProofGenerationError"
                            ],
                          "map_err",
                          [
                            Ty.path "spl_token_2022::error::TokenError";
                            Ty.function
                              [
                                Ty.tuple
                                  [ Ty.path "solana_zk_token_sdk::errors::ProofGenerationError" ]
                              ]
                              (Ty.path "spl_token_2022::error::TokenError")
                          ]
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path
                                "solana_zk_token_sdk::instruction::transfer::without_fee::TransferData",
                              "new",
                              []
                            |),
                            [
                              M.read (| transfer_amount |);
                              Value.Tuple
                                [
                                  M.read (| current_source_decrypted_available_balance |);
                                  current_source_available_balance
                                ];
                              M.read (| elgamal_keypair |);
                              Value.Tuple
                                [
                                  M.read (| destination_elgamal_pubkey |);
                                  M.read (| auditor_elgamal_pubkey |)
                                ]
                            ]
                          |);
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [ α0 ] =>
                                  M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (Value.StructTuple
                                            "spl_token_2022::error::TokenError::ProofGeneration"
                                            []))
                                    ]
                                  |)
                                | _ => M.impossible (||)
                                end))
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_generate_transfer_proof_data :
          M.IsAssociatedFunction Self "generate_transfer_proof_data" generate_transfer_proof_data.
        
        (*
            pub fn generate_split_transfer_proof_data(
                &self,
                transfer_amount: u64,
                source_elgamal_keypair: &ElGamalKeypair,
                aes_key: &AeKey,
                destination_elgamal_pubkey: &ElGamalPubkey,
                auditor_elgamal_pubkey: Option<&ElGamalPubkey>,
            ) -> Result<
                (
                    CiphertextCommitmentEqualityProofData,
                    BatchedGroupedCiphertext2HandlesValidityProofData,
                    BatchedRangeProofU128Data,
                    SourceDecryptHandles,
                ),
                TokenError,
            > {
                let current_available_balance = self
                    .available_balance
                    .try_into()
                    .map_err(|_| TokenError::MalformedCiphertext)?;
                let current_decryptable_available_balance = self
                    .decryptable_available_balance
                    .try_into()
                    .map_err(|_| TokenError::MalformedCiphertext)?;
        
                transfer_split_proof_data(
                    &current_available_balance,
                    &current_decryptable_available_balance,
                    transfer_amount,
                    source_elgamal_keypair,
                    aes_key,
                    destination_elgamal_pubkey,
                    auditor_elgamal_pubkey,
                )
            }
        *)
        Definition generate_split_transfer_proof_data (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [],
              [
                self;
                transfer_amount;
                source_elgamal_keypair;
                aes_key;
                destination_elgamal_pubkey;
                auditor_elgamal_pubkey
              ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let transfer_amount := M.alloc (| transfer_amount |) in
              let source_elgamal_keypair := M.alloc (| source_elgamal_keypair |) in
              let aes_key := M.alloc (| aes_key |) in
              let destination_elgamal_pubkey := M.alloc (| destination_elgamal_pubkey |) in
              let auditor_elgamal_pubkey := M.alloc (| auditor_elgamal_pubkey |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let current_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [
                                    Ty.path
                                      "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                    Ty.path "spl_token_2022::error::TokenError"
                                  ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      [
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                      ],
                                    "map_err",
                                    [
                                      Ty.path "spl_token_2022::error::TokenError";
                                      Ty.function
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path
                                                "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                            ]
                                        ]
                                        (Ty.path "spl_token_2022::error::TokenError")
                                    ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::TryInto",
                                        Ty.path
                                          "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                                        [
                                          Ty.path
                                            "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext"
                                        ],
                                        "try_into",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo",
                                            "available_balance"
                                          |)
                                        |)
                                      ]
                                    |);
                                    M.closure
                                      (fun γ =>
                                        ltac:(M.monadic
                                          match γ with
                                          | [ α0 ] =>
                                            M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (Value.StructTuple
                                                      "spl_token_2022::error::TokenError::MalformedCiphertext"
                                                      []))
                                              ]
                                            |)
                                          | _ => M.impossible (||)
                                          end))
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.path
                                                      "solana_zk_token_sdk::instruction::ciphertext_commitment_equality::CiphertextCommitmentEqualityProofData";
                                                    Ty.path
                                                      "solana_zk_token_sdk::instruction::batched_grouped_ciphertext_validity::BatchedGroupedCiphertext2HandlesValidityProofData";
                                                    Ty.path
                                                      "solana_zk_token_sdk::instruction::batched_range_proof::batched_range_proof_u128::BatchedRangeProofU128Data";
                                                    Ty.path
                                                      "spl_token_2022::extension::confidential_transfer::ciphertext_extraction::SourceDecryptHandles"
                                                  ];
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    let current_decryptable_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [
                                    Ty.path
                                      "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                    Ty.path "spl_token_2022::error::TokenError"
                                  ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      [
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::auth_encryption::AuthenticatedEncryptionError"
                                      ],
                                    "map_err",
                                    [
                                      Ty.path "spl_token_2022::error::TokenError";
                                      Ty.function
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path
                                                "solana_zk_token_sdk::encryption::auth_encryption::AuthenticatedEncryptionError"
                                            ]
                                        ]
                                        (Ty.path "spl_token_2022::error::TokenError")
                                    ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::TryInto",
                                        Ty.path
                                          "solana_zk_token_sdk::zk_token_elgamal::pod::auth_encryption::AeCiphertext",
                                        [
                                          Ty.path
                                            "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext"
                                        ],
                                        "try_into",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo",
                                            "decryptable_available_balance"
                                          |)
                                        |)
                                      ]
                                    |);
                                    M.closure
                                      (fun γ =>
                                        ltac:(M.monadic
                                          match γ with
                                          | [ α0 ] =>
                                            M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (Value.StructTuple
                                                      "spl_token_2022::error::TokenError::MalformedCiphertext"
                                                      []))
                                              ]
                                            |)
                                          | _ => M.impossible (||)
                                          end))
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.path
                                                      "solana_zk_token_sdk::instruction::ciphertext_commitment_equality::CiphertextCommitmentEqualityProofData";
                                                    Ty.path
                                                      "solana_zk_token_sdk::instruction::batched_grouped_ciphertext_validity::BatchedGroupedCiphertext2HandlesValidityProofData";
                                                    Ty.path
                                                      "solana_zk_token_sdk::instruction::batched_range_proof::batched_range_proof_u128::BatchedRangeProofU128Data";
                                                    Ty.path
                                                      "spl_token_2022::extension::confidential_transfer::ciphertext_extraction::SourceDecryptHandles"
                                                  ];
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "spl_token_2022::extension::confidential_transfer::split_proof_generation::transfer_split_proof_data",
                          []
                        |),
                        [
                          current_available_balance;
                          current_decryptable_available_balance;
                          M.read (| transfer_amount |);
                          M.read (| source_elgamal_keypair |);
                          M.read (| aes_key |);
                          M.read (| destination_elgamal_pubkey |);
                          M.read (| auditor_elgamal_pubkey |)
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_generate_split_transfer_proof_data :
          M.IsAssociatedFunction
            Self
            "generate_split_transfer_proof_data"
            generate_split_transfer_proof_data.
        
        (*
            pub fn generate_transfer_with_fee_proof_data(
                &self,
                transfer_amount: u64,
                elgamal_keypair: &ElGamalKeypair,
                aes_key: &AeKey,
                destination_elgamal_pubkey: &ElGamalPubkey,
                auditor_elgamal_pubkey: Option<&ElGamalPubkey>,
                withdraw_withheld_authority_elgamal_pubkey: &ElGamalPubkey,
                fee_rate_basis_points: u16,
                maximum_fee: u64,
            ) -> Result<TransferWithFeeData, TokenError> {
                let current_source_available_balance = self
                    .available_balance
                    .try_into()
                    .map_err(|_| TokenError::MalformedCiphertext)?;
                let current_source_decrypted_available_balance =
                    self.decrypted_available_balance(aes_key)?;
        
                let default_auditor_pubkey = ElGamalPubkey::default();
                let auditor_elgamal_pubkey = auditor_elgamal_pubkey.unwrap_or(&default_auditor_pubkey);
        
                let fee_parameters = FeeParameters {
                    fee_rate_basis_points,
                    maximum_fee,
                };
        
                TransferWithFeeData::new(
                    transfer_amount,
                    (
                        current_source_decrypted_available_balance,
                        &current_source_available_balance,
                    ),
                    elgamal_keypair,
                    (destination_elgamal_pubkey, auditor_elgamal_pubkey),
                    fee_parameters,
                    withdraw_withheld_authority_elgamal_pubkey,
                )
                .map_err(|_| TokenError::ProofGeneration)
            }
        *)
        Definition generate_transfer_with_fee_proof_data (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [],
              [
                self;
                transfer_amount;
                elgamal_keypair;
                aes_key;
                destination_elgamal_pubkey;
                auditor_elgamal_pubkey;
                withdraw_withheld_authority_elgamal_pubkey;
                fee_rate_basis_points;
                maximum_fee
              ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let transfer_amount := M.alloc (| transfer_amount |) in
              let elgamal_keypair := M.alloc (| elgamal_keypair |) in
              let aes_key := M.alloc (| aes_key |) in
              let destination_elgamal_pubkey := M.alloc (| destination_elgamal_pubkey |) in
              let auditor_elgamal_pubkey := M.alloc (| auditor_elgamal_pubkey |) in
              let withdraw_withheld_authority_elgamal_pubkey :=
                M.alloc (| withdraw_withheld_authority_elgamal_pubkey |) in
              let fee_rate_basis_points := M.alloc (| fee_rate_basis_points |) in
              let maximum_fee := M.alloc (| maximum_fee |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let current_source_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [
                                    Ty.path
                                      "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                    Ty.path "spl_token_2022::error::TokenError"
                                  ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      [
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext";
                                        Ty.path
                                          "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                      ],
                                    "map_err",
                                    [
                                      Ty.path "spl_token_2022::error::TokenError";
                                      Ty.function
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path
                                                "solana_zk_token_sdk::encryption::elgamal::ElGamalError"
                                            ]
                                        ]
                                        (Ty.path "spl_token_2022::error::TokenError")
                                    ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::TryInto",
                                        Ty.path
                                          "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                                        [
                                          Ty.path
                                            "solana_zk_token_sdk::encryption::elgamal::ElGamalCiphertext"
                                        ],
                                        "try_into",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo",
                                            "available_balance"
                                          |)
                                        |)
                                      ]
                                    |);
                                    M.closure
                                      (fun γ =>
                                        ltac:(M.monadic
                                          match γ with
                                          | [ α0 ] =>
                                            M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (Value.StructTuple
                                                      "spl_token_2022::error::TokenError::MalformedCiphertext"
                                                      []))
                                              ]
                                            |)
                                          | _ => M.impossible (||)
                                          end))
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::instruction::transfer::with_fee::TransferWithFeeData";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    let current_source_decrypted_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [ Ty.path "u64"; Ty.path "spl_token_2022::error::TokenError" ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path
                                      "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo",
                                    "decrypted_available_balance",
                                    []
                                  |),
                                  [ M.read (| self |); M.read (| aes_key |) ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::instruction::transfer::with_fee::TransferWithFeeData";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    let default_auditor_pubkey :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::default::Default",
                            Ty.path "solana_zk_token_sdk::encryption::elgamal::ElGamalPubkey",
                            [],
                            "default",
                            []
                          |),
                          []
                        |)
                      |) in
                    let auditor_elgamal_pubkey :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  [
                                    Ty.path
                                      "solana_zk_token_sdk::encryption::elgamal::ElGamalPubkey"
                                  ]
                              ],
                            "unwrap_or",
                            []
                          |),
                          [ M.read (| auditor_elgamal_pubkey |); default_auditor_pubkey ]
                        |)
                      |) in
                    let fee_parameters :=
                      M.alloc (|
                        Value.StructRecord
                          "solana_zk_token_sdk::instruction::transfer::FeeParameters"
                          [
                            ("fee_rate_basis_points", M.read (| fee_rate_basis_points |));
                            ("maximum_fee", M.read (| maximum_fee |))
                          ]
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::result::Result")
                            [
                              Ty.path
                                "solana_zk_token_sdk::instruction::transfer::with_fee::TransferWithFeeData";
                              Ty.path "solana_zk_token_sdk::errors::ProofGenerationError"
                            ],
                          "map_err",
                          [
                            Ty.path "spl_token_2022::error::TokenError";
                            Ty.function
                              [
                                Ty.tuple
                                  [ Ty.path "solana_zk_token_sdk::errors::ProofGenerationError" ]
                              ]
                              (Ty.path "spl_token_2022::error::TokenError")
                          ]
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path
                                "solana_zk_token_sdk::instruction::transfer::with_fee::TransferWithFeeData",
                              "new",
                              []
                            |),
                            [
                              M.read (| transfer_amount |);
                              Value.Tuple
                                [
                                  M.read (| current_source_decrypted_available_balance |);
                                  current_source_available_balance
                                ];
                              M.read (| elgamal_keypair |);
                              Value.Tuple
                                [
                                  M.read (| destination_elgamal_pubkey |);
                                  M.read (| auditor_elgamal_pubkey |)
                                ];
                              M.read (| fee_parameters |);
                              M.read (| withdraw_withheld_authority_elgamal_pubkey |)
                            ]
                          |);
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [ α0 ] =>
                                  M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (Value.StructTuple
                                            "spl_token_2022::error::TokenError::ProofGeneration"
                                            []))
                                    ]
                                  |)
                                | _ => M.impossible (||)
                                end))
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_generate_transfer_with_fee_proof_data :
          M.IsAssociatedFunction
            Self
            "generate_transfer_with_fee_proof_data"
            generate_transfer_with_fee_proof_data.
        
        (*
            pub fn new_decryptable_available_balance(
                &self,
                transfer_amount: u64,
                aes_key: &AeKey,
            ) -> Result<AeCiphertext, TokenError> {
                let current_decrypted_available_balance = self.decrypted_available_balance(aes_key)?;
                let new_decrypted_available_balance = current_decrypted_available_balance
                    .checked_sub(transfer_amount)
                    .ok_or(TokenError::InsufficientFunds)?;
        
                Ok(aes_key.encrypt(new_decrypted_available_balance))
            }
        *)
        Definition new_decryptable_available_balance (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ self; transfer_amount; aes_key ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let transfer_amount := M.alloc (| transfer_amount |) in
              let aes_key := M.alloc (| aes_key |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let current_decrypted_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [ Ty.path "u64"; Ty.path "spl_token_2022::error::TokenError" ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path
                                      "spl_token_2022::extension::confidential_transfer::account_info::TransferAccountInfo",
                                    "decrypted_available_balance",
                                    []
                                  |),
                                  [ M.read (| self |); M.read (| aes_key |) ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    let new_decrypted_available_balance :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  [ Ty.path "u64"; Ty.path "spl_token_2022::error::TokenError" ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::option::Option") [ Ty.path "u64" ],
                                    "ok_or",
                                    [ Ty.path "spl_token_2022::error::TokenError" ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "u64",
                                        "checked_sub",
                                        []
                                      |),
                                      [
                                        M.read (| current_decrypted_available_balance |);
                                        M.read (| transfer_amount |)
                                      ]
                                    |);
                                    Value.StructTuple
                                      "spl_token_2022::error::TokenError::InsufficientFunds"
                                      []
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path
                                                  "solana_zk_token_sdk::encryption::auth_encryption::AeCiphertext";
                                                Ty.path "spl_token_2022::error::TokenError"
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                [
                                                  Ty.path "core::convert::Infallible";
                                                  Ty.path "spl_token_2022::error::TokenError"
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "solana_zk_token_sdk::encryption::auth_encryption::AeKey",
                              "encrypt",
                              []
                            |),
                            [ M.read (| aes_key |); M.read (| new_decrypted_available_balance |) ]
                          |)
                        ]
                    |)
                  |)))
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom AssociatedFunction_new_decryptable_available_balance :
          M.IsAssociatedFunction
            Self
            "new_decryptable_available_balance"
            new_decryptable_available_balance.
      End Impl_spl_token_2022_extension_confidential_transfer_account_info_TransferAccountInfo.
      
      (*
      fn combine_balances(balance_lo: u64, balance_hi: u64) -> Option<u64> {
          balance_hi
              .checked_shl(PENDING_BALANCE_LO_BIT_LENGTH)?
              .checked_add(balance_lo)
      }
      *)
      Definition combine_balances (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [], [ balance_lo; balance_hi ] =>
          ltac:(M.monadic
            (let balance_lo := M.alloc (| balance_lo |) in
            let balance_hi := M.alloc (| balance_hi |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_associated_function (| Ty.path "u64", "checked_add", [] |),
                  [
                    M.read (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply (Ty.path "core::option::Option") [ Ty.path "u64" ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (| Ty.path "u64", "checked_shl", [] |),
                                [
                                  M.read (| balance_hi |);
                                  M.read (|
                                    M.get_constant (|
                                      "spl_token_2022::extension::confidential_transfer::PENDING_BALANCE_LO_BIT_LENGTH"
                                    |)
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Break",
                                  0
                                |) in
                              let residual := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::try_trait::FromResidual",
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            [ Ty.path "u64" ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "from_residual",
                                          []
                                        |),
                                        [ M.read (| residual |) ]
                                      |)
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Continue",
                                  0
                                |) in
                              let val := M.copy (| γ0_0 |) in
                              val))
                        ]
                      |)
                    |);
                    M.read (| balance_lo |)
                  ]
                |)))
            |)))
        | _, _ => M.impossible
        end.
    End account_info.
  End confidential_transfer.
End extension.
