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

Module extension.
  Module transfer_hook.
    (* StructRecord
      {
        name := "TransferHook";
        ty_params := [];
        fields :=
          [
            ("authority", Ty.path "spl_pod::optional_keys::OptionalNonZeroPubkey");
            ("program_id", Ty.path "spl_pod::optional_keys::OptionalNonZeroPubkey")
          ];
      } *)
    
    Module Impl_core_clone_Clone_for_spl_token_2022_extension_transfer_hook_TransferHook.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::transfer_hook::TransferHook".
      
      (* 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_transfer_hook_TransferHook.
    
    Module Impl_core_marker_Copy_for_spl_token_2022_extension_transfer_hook_TransferHook.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::transfer_hook::TransferHook".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_spl_token_2022_extension_transfer_hook_TransferHook.
    
    Module Impl_core_fmt_Debug_for_spl_token_2022_extension_transfer_hook_TransferHook.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::transfer_hook::TransferHook".
      
      (* 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 "TransferHook" |);
                M.read (| Value.String "authority" |);
                (* Unsize *)
                M.pointer_coercion
                  (M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "spl_token_2022::extension::transfer_hook::TransferHook",
                    "authority"
                  |));
                M.read (| Value.String "program_id" |);
                (* Unsize *)
                M.pointer_coercion
                  (M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "spl_token_2022::extension::transfer_hook::TransferHook",
                      "program_id"
                    |)
                  |))
              ]
            |)))
        | _, _ => 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_transfer_hook_TransferHook.
    
    Module Impl_core_default_Default_for_spl_token_2022_extension_transfer_hook_TransferHook.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::transfer_hook::TransferHook".
      
      (* Default *)
      Definition default (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "spl_token_2022::extension::transfer_hook::TransferHook"
              [
                ("authority",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "spl_pod::optional_keys::OptionalNonZeroPubkey",
                      [],
                      "default",
                      []
                    |),
                    []
                  |));
                ("program_id",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "spl_pod::optional_keys::OptionalNonZeroPubkey",
                      [],
                      "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_transfer_hook_TransferHook.
    
    Module Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_transfer_hook_TransferHook.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::transfer_hook::TransferHook".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_transfer_hook_TransferHook.
    
    Module Impl_core_cmp_PartialEq_for_spl_token_2022_extension_transfer_hook_TransferHook.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::transfer_hook::TransferHook".
      
      (* 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 "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::transfer_hook::TransferHook",
                    "authority"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "spl_token_2022::extension::transfer_hook::TransferHook",
                    "authority"
                  |)
                ]
              |),
              ltac:(M.monadic
                (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::transfer_hook::TransferHook",
                      "program_id"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "spl_token_2022::extension::transfer_hook::TransferHook",
                      "program_id"
                    |)
                  ]
                |)))
            |)))
        | _, _ => 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_transfer_hook_TransferHook.
    
    Module Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_transfer_hook_TransferHook.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::transfer_hook::TransferHook".
      
      Axiom Implements :
        M.IsTraitInstance
          "bytemuck::pod::Pod"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_transfer_hook_TransferHook.
    
    Module Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_transfer_hook_TransferHook.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::transfer_hook::TransferHook".
      
      Axiom Implements :
        M.IsTraitInstance
          "bytemuck::zeroable::Zeroable"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_transfer_hook_TransferHook.
    
    (* StructRecord
      {
        name := "TransferHookAccount";
        ty_params := [];
        fields := [ ("transferring", Ty.path "spl_pod::primitives::PodBool") ];
      } *)
    
    Module Impl_core_clone_Clone_for_spl_token_2022_extension_transfer_hook_TransferHookAccount.
      Definition Self : Ty.t :=
        Ty.path "spl_token_2022::extension::transfer_hook::TransferHookAccount".
      
      (* 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_transfer_hook_TransferHookAccount.
    
    Module Impl_core_marker_Copy_for_spl_token_2022_extension_transfer_hook_TransferHookAccount.
      Definition Self : Ty.t :=
        Ty.path "spl_token_2022::extension::transfer_hook::TransferHookAccount".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_spl_token_2022_extension_transfer_hook_TransferHookAccount.
    
    Module Impl_core_fmt_Debug_for_spl_token_2022_extension_transfer_hook_TransferHookAccount.
      Definition Self : Ty.t :=
        Ty.path "spl_token_2022::extension::transfer_hook::TransferHookAccount".
      
      (* 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 "TransferHookAccount" |);
                M.read (| Value.String "transferring" |);
                (* Unsize *)
                M.pointer_coercion
                  (M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "spl_token_2022::extension::transfer_hook::TransferHookAccount",
                      "transferring"
                    |)
                  |))
              ]
            |)))
        | _, _ => 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_transfer_hook_TransferHookAccount.
    
    Module Impl_core_default_Default_for_spl_token_2022_extension_transfer_hook_TransferHookAccount.
      Definition Self : Ty.t :=
        Ty.path "spl_token_2022::extension::transfer_hook::TransferHookAccount".
      
      (* Default *)
      Definition default (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "spl_token_2022::extension::transfer_hook::TransferHookAccount"
              [
                ("transferring",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "spl_pod::primitives::PodBool",
                      [],
                      "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_transfer_hook_TransferHookAccount.
    
    Module Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_transfer_hook_TransferHookAccount.
      Definition Self : Ty.t :=
        Ty.path "spl_token_2022::extension::transfer_hook::TransferHookAccount".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_transfer_hook_TransferHookAccount.
    
    Module Impl_core_cmp_PartialEq_for_spl_token_2022_extension_transfer_hook_TransferHookAccount.
      Definition Self : Ty.t :=
        Ty.path "spl_token_2022::extension::transfer_hook::TransferHookAccount".
      
      (* 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 "spl_pod::primitives::PodBool",
                [ Ty.path "spl_pod::primitives::PodBool" ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "spl_token_2022::extension::transfer_hook::TransferHookAccount",
                  "transferring"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "spl_token_2022::extension::transfer_hook::TransferHookAccount",
                  "transferring"
                |)
              ]
            |)))
        | _, _ => 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_transfer_hook_TransferHookAccount.
    
    Module Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_transfer_hook_TransferHookAccount.
      Definition Self : Ty.t :=
        Ty.path "spl_token_2022::extension::transfer_hook::TransferHookAccount".
      
      Axiom Implements :
        M.IsTraitInstance
          "bytemuck::pod::Pod"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_transfer_hook_TransferHookAccount.
    
    Module Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_transfer_hook_TransferHookAccount.
      Definition Self : Ty.t :=
        Ty.path "spl_token_2022::extension::transfer_hook::TransferHookAccount".
      
      Axiom Implements :
        M.IsTraitInstance
          "bytemuck::zeroable::Zeroable"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_transfer_hook_TransferHookAccount.
    
    Module Impl_spl_token_2022_extension_Extension_for_spl_token_2022_extension_transfer_hook_TransferHook.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::transfer_hook::TransferHook".
      
      (*     const TYPE: ExtensionType = ExtensionType::TransferHook; *)
      (* 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::TransferHook" []
            |))).
      
      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_transfer_hook_TransferHook.
    
    Module Impl_spl_token_2022_extension_Extension_for_spl_token_2022_extension_transfer_hook_TransferHookAccount.
      Definition Self : Ty.t :=
        Ty.path "spl_token_2022::extension::transfer_hook::TransferHookAccount".
      
      (*     const TYPE: ExtensionType = ExtensionType::TransferHookAccount; *)
      (* 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::TransferHookAccount" []
            |))).
      
      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_transfer_hook_TransferHookAccount.
    
    (*
    pub fn get_program_id<S: BaseState, BSE: BaseStateWithExtensions<S>>(
        state: &BSE,
    ) -> Option<Pubkey> {
        state
            .get_extension::<TransferHook>()
            .ok()
            .and_then(|e| Option::<Pubkey>::from(e.program_id))
    }
    *)
    Definition get_program_id (τ : list Ty.t) (α : list Value.t) : M :=
      match τ, α with
      | [ _ as S; BSE ], [ state ] =>
        ltac:(M.monadic
          (let state := M.alloc (| state |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::option::Option")
                [
                  Ty.apply
                    (Ty.path "&")
                    [ Ty.path "spl_token_2022::extension::transfer_hook::TransferHook" ]
                ],
              "and_then",
              [
                Ty.path "solana_program::pubkey::Pubkey";
                Ty.function
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&")
                          [ Ty.path "spl_token_2022::extension::transfer_hook::TransferHook" ]
                      ]
                  ]
                  (Ty.apply
                    (Ty.path "core::option::Option")
                    [ Ty.path "solana_program::pubkey::Pubkey" ])
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::result::Result")
                    [
                      Ty.apply
                        (Ty.path "&")
                        [ Ty.path "spl_token_2022::extension::transfer_hook::TransferHook" ];
                      Ty.path "solana_program::program_error::ProgramError"
                    ],
                  "ok",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "spl_token_2022::extension::BaseStateWithExtensions",
                      BSE,
                      [ S ],
                      "get_extension",
                      [ Ty.path "spl_token_2022::extension::transfer_hook::TransferHook" ]
                    |),
                    [ M.read (| state |) ]
                  |)
                ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let e := M.copy (| γ |) in
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::convert::From",
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    [ Ty.path "solana_program::pubkey::Pubkey" ],
                                  [ Ty.path "spl_pod::optional_keys::OptionalNonZeroPubkey" ],
                                  "from",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| e |),
                                      "spl_token_2022::extension::transfer_hook::TransferHook",
                                      "program_id"
                                    |)
                                  |)
                                ]
                              |)))
                        ]
                      |)
                    | _ => M.impossible (||)
                    end))
            ]
          |)))
      | _, _ => M.impossible
      end.
    
    (*
    pub fn set_transferring<BSE: BaseStateWithExtensionsMut<S>, S: BaseState>(
        account: &mut BSE,
    ) -> Result<(), ProgramError> {
        let account_extension = account.get_extension_mut::<TransferHookAccount>()?;
        account_extension.transferring = true.into();
        Ok(())
    }
    *)
    Definition set_transferring (τ : list Ty.t) (α : list Value.t) : M :=
      match τ, α with
      | [ BSE; _ as S ], [ account ] =>
        ltac:(M.monadic
          (let account := M.alloc (| account |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let account_extension :=
                  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.apply
                                  (Ty.path "&mut")
                                  [
                                    Ty.path
                                      "spl_token_2022::extension::transfer_hook::TransferHookAccount"
                                  ];
                                Ty.path "solana_program::program_error::ProgramError"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "spl_token_2022::extension::BaseStateWithExtensionsMut",
                                BSE,
                                [ S ],
                                "get_extension_mut",
                                [
                                  Ty.path
                                    "spl_token_2022::extension::transfer_hook::TransferHookAccount"
                                ]
                              |),
                              [ M.read (| account |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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_program::program_error::ProgramError"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "solana_program::program_error::ProgramError"
                                            ]
                                        ],
                                        "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 _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| account_extension |),
                      "spl_token_2022::extension::transfer_hook::TransferHookAccount",
                      "transferring"
                    |),
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::convert::Into",
                        Ty.path "bool",
                        [ Ty.path "spl_pod::primitives::PodBool" ],
                        "into",
                        []
                      |),
                      [ Value.Bool true ]
                    |)
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _ => M.impossible
      end.
    
    (*
    pub fn unset_transferring(account_info: &AccountInfo) -> Result<(), ProgramError> {
        let mut account_data = account_info.data.borrow_mut();
        let mut account = PodStateWithExtensionsMut::<PodAccount>::unpack(&mut account_data)?;
        let account_extension = account.get_extension_mut::<TransferHookAccount>()?;
        account_extension.transferring = false.into();
        Ok(())
    }
    *)
    Definition unset_transferring (τ : list Ty.t) (α : list Value.t) : M :=
      match τ, α with
      | [], [ account_info ] =>
        ltac:(M.monadic
          (let account_info := M.alloc (| account_info |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let account_data :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::cell::RefCell")
                          [
                            Ty.apply
                              (Ty.path "&mut")
                              [ Ty.apply (Ty.path "slice") [ Ty.path "u8" ] ]
                          ],
                        "borrow_mut",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::Deref",
                            Ty.apply
                              (Ty.path "alloc::rc::Rc")
                              [
                                Ty.apply
                                  (Ty.path "core::cell::RefCell")
                                  [
                                    Ty.apply
                                      (Ty.path "&mut")
                                      [ Ty.apply (Ty.path "slice") [ Ty.path "u8" ] ]
                                  ];
                                Ty.path "alloc::alloc::Global"
                              ],
                            [],
                            "deref",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| account_info |),
                              "solana_program::account_info::AccountInfo",
                              "data"
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                let account :=
                  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.apply
                                  (Ty.path "spl_token_2022::extension::PodStateWithExtensionsMut")
                                  [ Ty.path "spl_token_2022::pod::PodAccount" ];
                                Ty.path "solana_program::program_error::ProgramError"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "spl_token_2022::extension::PodStateWithExtensionsMut")
                                  [ Ty.path "spl_token_2022::pod::PodAccount" ],
                                "unpack",
                                []
                              |),
                              [
                                M.read (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::deref::DerefMut",
                                      Ty.apply
                                        (Ty.path "core::cell::RefMut")
                                        [
                                          Ty.apply
                                            (Ty.path "&mut")
                                            [ Ty.apply (Ty.path "slice") [ Ty.path "u8" ] ]
                                        ],
                                      [],
                                      "deref_mut",
                                      []
                                    |),
                                    [ account_data ]
                                  |)
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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_program::program_error::ProgramError"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "solana_program::program_error::ProgramError"
                                            ]
                                        ],
                                        "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 account_extension :=
                  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.apply
                                  (Ty.path "&mut")
                                  [
                                    Ty.path
                                      "spl_token_2022::extension::transfer_hook::TransferHookAccount"
                                  ];
                                Ty.path "solana_program::program_error::ProgramError"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "spl_token_2022::extension::BaseStateWithExtensionsMut",
                                Ty.apply
                                  (Ty.path "spl_token_2022::extension::PodStateWithExtensionsMut")
                                  [ Ty.path "spl_token_2022::pod::PodAccount" ],
                                [ Ty.path "spl_token_2022::pod::PodAccount" ],
                                "get_extension_mut",
                                [
                                  Ty.path
                                    "spl_token_2022::extension::transfer_hook::TransferHookAccount"
                                ]
                              |),
                              [ account ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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_program::program_error::ProgramError"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "solana_program::program_error::ProgramError"
                                            ]
                                        ],
                                        "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 _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| account_extension |),
                      "spl_token_2022::extension::transfer_hook::TransferHookAccount",
                      "transferring"
                    |),
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::convert::Into",
                        Ty.path "bool",
                        [ Ty.path "spl_pod::primitives::PodBool" ],
                        "into",
                        []
                      |),
                      [ Value.Bool false ]
                    |)
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _ => M.impossible
      end.
  End transfer_hook.
End extension.
