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

Module extension.
  Module confidential_transfer_fee.
    Axiom EncryptedFee :
      (Ty.path "spl_token_2022::extension::confidential_transfer_fee::EncryptedFee") =
        (Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::instruction::FeeEncryption").
    
    Axiom EncryptedWithheldAmount :
      (Ty.path "spl_token_2022::extension::confidential_transfer_fee::EncryptedWithheldAmount") =
        (Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext").
    
    (* StructRecord
      {
        name := "ConfidentialTransferFeeConfig";
        ty_params := [];
        fields :=
          [
            ("authority", Ty.path "spl_pod::optional_keys::OptionalNonZeroPubkey");
            ("withdraw_withheld_authority_elgamal_pubkey",
              Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalPubkey");
            ("harvest_to_mint_enabled", Ty.path "spl_pod::primitives::PodBool");
            ("withheld_amount",
              Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext")
          ];
      } *)
    
    Module Impl_core_clone_Clone_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeConfig.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig".
      
      (* 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.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_fee_ConfidentialTransferFeeConfig.
    
    Module Impl_core_marker_Copy_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeConfig.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeConfig.
    
    Module Impl_core_fmt_Debug_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeConfig.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig".
      
      (* 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 "ConfidentialTransferFeeConfig" |);
                M.read (| Value.String "authority" |);
                (* Unsize *)
                M.pointer_coercion
                  (M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig",
                    "authority"
                  |));
                M.read (| Value.String "withdraw_withheld_authority_elgamal_pubkey" |);
                (* Unsize *)
                M.pointer_coercion
                  (M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig",
                    "withdraw_withheld_authority_elgamal_pubkey"
                  |));
                M.read (| Value.String "harvest_to_mint_enabled" |);
                (* Unsize *)
                M.pointer_coercion
                  (M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig",
                    "harvest_to_mint_enabled"
                  |));
                M.read (| Value.String "withheld_amount" |);
                (* Unsize *)
                M.pointer_coercion
                  (M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig",
                      "withheld_amount"
                    |)
                  |))
              ]
            |)))
        | _, _ => 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_fee_ConfidentialTransferFeeConfig.
    
    Module Impl_core_default_Default_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeConfig.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig".
      
      (* Default *)
      Definition default (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig"
              [
                ("authority",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "spl_pod::optional_keys::OptionalNonZeroPubkey",
                      [],
                      "default",
                      []
                    |),
                    []
                  |));
                ("withdraw_withheld_authority_elgamal_pubkey",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalPubkey",
                      [],
                      "default",
                      []
                    |),
                    []
                  |));
                ("harvest_to_mint_enabled",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "spl_pod::primitives::PodBool",
                      [],
                      "default",
                      []
                    |),
                    []
                  |));
                ("withheld_amount",
                  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_fee_ConfidentialTransferFeeConfig.
    
    Module Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeConfig.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeConfig.
    
    Module Impl_core_cmp_PartialEq_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeConfig.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig".
      
      (* 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::optional_keys::OptionalNonZeroPubkey",
                      [ Ty.path "spl_pod::optional_keys::OptionalNonZeroPubkey" ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig",
                        "authority"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig",
                        "authority"
                      |)
                    ]
                  |),
                  ltac:(M.monadic
                    (M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.path
                          "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalPubkey",
                        [
                          Ty.path
                            "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalPubkey"
                        ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig",
                          "withdraw_withheld_authority_elgamal_pubkey"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig",
                          "withdraw_withheld_authority_elgamal_pubkey"
                        |)
                      ]
                    |)))
                |),
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.path "spl_pod::primitives::PodBool",
                      [ Ty.path "spl_pod::primitives::PodBool" ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig",
                        "harvest_to_mint_enabled"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig",
                        "harvest_to_mint_enabled"
                      |)
                    ]
                  |)))
              |),
              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_fee::ConfidentialTransferFeeConfig",
                      "withheld_amount"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig",
                      "withheld_amount"
                    |)
                  ]
                |)))
            |)))
        | _, _ => 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_fee_ConfidentialTransferFeeConfig.
    
    Module Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeConfig.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig".
      
      Axiom Implements :
        M.IsTraitInstance
          "bytemuck::pod::Pod"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeConfig.
    
    Module Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeConfig.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig".
      
      Axiom Implements :
        M.IsTraitInstance
          "bytemuck::zeroable::Zeroable"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeConfig.
    
    Module Impl_spl_token_2022_extension_Extension_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeConfig.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeConfig".
      
      (*     const TYPE: ExtensionType = ExtensionType::ConfidentialTransferFeeConfig; *)
      (* Ty.path "spl_token_2022::extension::ExtensionType" *)
      Definition value_TYPE : Value.t :=
        M.run
          ltac:(M.monadic
            (M.alloc (|
              Value.StructTuple
                "spl_token_2022::extension::ExtensionType::ConfidentialTransferFeeConfig"
                []
            |))).
      
      Axiom Implements :
        M.IsTraitInstance
          "spl_token_2022::extension::Extension"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("value_TYPE", InstanceField.Constant value_TYPE) ].
    End Impl_spl_token_2022_extension_Extension_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeConfig.
    
    (* StructRecord
      {
        name := "ConfidentialTransferFeeAmount";
        ty_params := [];
        fields :=
          [
            ("withheld_amount",
              Ty.path "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext")
          ];
      } *)
    
    Module Impl_core_clone_Clone_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeAmount".
      
      (* 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_fee_ConfidentialTransferFeeAmount.
    
    Module Impl_core_marker_Copy_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeAmount".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
    
    Module Impl_core_fmt_Debug_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeAmount".
      
      (* 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 "ConfidentialTransferFeeAmount" |);
                M.read (| Value.String "withheld_amount" |);
                (* Unsize *)
                M.pointer_coercion
                  (M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeAmount",
                      "withheld_amount"
                    |)
                  |))
              ]
            |)))
        | _, _ => 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_fee_ConfidentialTransferFeeAmount.
    
    Module Impl_core_default_Default_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeAmount".
      
      (* Default *)
      Definition default (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeAmount"
              [
                ("withheld_amount",
                  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_fee_ConfidentialTransferFeeAmount.
    
    Module Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeAmount".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
    
    Module Impl_core_cmp_PartialEq_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeAmount".
      
      (* 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_fee::ConfidentialTransferFeeAmount",
                  "withheld_amount"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeAmount",
                  "withheld_amount"
                |)
              ]
            |)))
        | _, _ => 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_fee_ConfidentialTransferFeeAmount.
    
    Module Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeAmount".
      
      Axiom Implements :
        M.IsTraitInstance
          "bytemuck::pod::Pod"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
    
    Module Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeAmount".
      
      Axiom Implements :
        M.IsTraitInstance
          "bytemuck::zeroable::Zeroable"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
    
    Module Impl_spl_token_2022_extension_Extension_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeAmount".
      
      (*     const TYPE: ExtensionType = ExtensionType::ConfidentialTransferFeeAmount; *)
      (* Ty.path "spl_token_2022::extension::ExtensionType" *)
      Definition value_TYPE : Value.t :=
        M.run
          ltac:(M.monadic
            (M.alloc (|
              Value.StructTuple
                "spl_token_2022::extension::ExtensionType::ConfidentialTransferFeeAmount"
                []
            |))).
      
      Axiom Implements :
        M.IsTraitInstance
          "spl_token_2022::extension::Extension"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("value_TYPE", InstanceField.Constant value_TYPE) ].
    End Impl_spl_token_2022_extension_Extension_for_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
    
    Module Impl_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
      Definition Self : Ty.t :=
        Ty.path
          "spl_token_2022::extension::confidential_transfer_fee::ConfidentialTransferFeeAmount".
      
      (*
          pub fn closable(&self) -> ProgramResult {
              if self.withheld_amount == EncryptedWithheldAmount::zeroed() {
                  Ok(())
              } else {
                  Err(TokenError::ConfidentialTransferFeeAccountHasWithheldFee.into())
              }
          }
      *)
      Definition closable (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            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_fee::ConfidentialTransferFeeAmount",
                                  "withheld_amount"
                                |);
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "bytemuck::zeroable::Zeroable",
                                      Ty.path
                                        "solana_zk_token_sdk::zk_token_elgamal::pod::elgamal::ElGamalCiphertext",
                                      [],
                                      "zeroed",
                                      []
                                    |),
                                    []
                                  |)
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::convert::Into",
                                Ty.path "spl_token_2022::error::TokenError",
                                [ Ty.path "solana_program::program_error::ProgramError" ],
                                "into",
                                []
                              |),
                              [
                                Value.StructTuple
                                  "spl_token_2022::error::TokenError::ConfidentialTransferFeeAccountHasWithheldFee"
                                  []
                              ]
                            |)
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _ => M.impossible
        end.
      
      Axiom AssociatedFunction_closable : M.IsAssociatedFunction Self "closable" closable.
    End Impl_spl_token_2022_extension_confidential_transfer_fee_ConfidentialTransferFeeAmount.
  End confidential_transfer_fee.
End extension.
