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

Module extension.
  Module cpi_guard.
    Module instruction.
      (*
      Enum CpiGuardInstruction
      {
        ty_params := [];
        variants :=
          [
            {
              name := "Enable";
              item := StructTuple [];
              discriminant := None;
            };
            {
              name := "Disable";
              item := StructTuple [];
              discriminant := None;
            }
          ];
      }
      *)
      
      Module Impl_core_clone_Clone_for_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction.
        Definition Self : Ty.t :=
          Ty.path "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction".
        
        (* 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.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_cpi_guard_instruction_CpiGuardInstruction.
      
      Module Impl_core_marker_Copy_for_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction.
        Definition Self : Ty.t :=
          Ty.path "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::Copy"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_Copy_for_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction.
      
      Module Impl_core_fmt_Debug_for_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction.
        Definition Self : Ty.t :=
          Ty.path "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction".
        
        (* 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", "write_str", [] |),
                [
                  M.read (| f |);
                  M.read (|
                    M.match_operator (|
                      self,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            M.alloc (| M.read (| Value.String "Enable" |) |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            M.alloc (| M.read (| Value.String "Disable" |) |)))
                      ]
                    |)
                  |)
                ]
              |)))
          | _, _ => 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_cpi_guard_instruction_CpiGuardInstruction.
      
      Module Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction.
        Definition Self : Ty.t :=
          Ty.path "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction.
      
      Module Impl_core_cmp_PartialEq_for_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction.
        Definition Self : Ty.t :=
          Ty.path "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction".
        
        (* 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.read (|
                let __self_tag :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::intrinsics::discriminant_value",
                        [
                          Ty.path
                            "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction"
                        ]
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                let __arg1_tag :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::intrinsics::discriminant_value",
                        [
                          Ty.path
                            "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction"
                        ]
                      |),
                      [ M.read (| other |) ]
                    |)
                  |) in
                M.alloc (| BinOp.Pure.eq (M.read (| __self_tag |)) (M.read (| __arg1_tag |)) |)
              |)))
          | _, _ => 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_cpi_guard_instruction_CpiGuardInstruction.
      
      Module Impl_core_convert_From_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction_for_u8.
        Definition Self : Ty.t := Ty.path "u8".
        
        (* IntoPrimitive *)
        Definition from (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ enum_value ] =>
            ltac:(M.monadic
              (let enum_value := M.alloc (| enum_value |) in
              M.rust_cast (M.read (| enum_value |))))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::convert::From"
            Self
            (* Trait polymorphic types *)
            [
              (* T *)
              Ty.path "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction"
            ]
            (* Instance *) [ ("from", InstanceField.Method from) ].
      End Impl_core_convert_From_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction_for_u8.
      
      Module Impl_num_enum_TryFromPrimitive_for_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction.
        Definition Self : Ty.t :=
          Ty.path "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction".
        
        (* TryFromPrimitive *)
        Definition _Primitive : Ty.t := Ty.path "u8".
        
        (* TryFromPrimitive *)
        Definition _Error : Ty.t :=
          Ty.apply
            (Ty.path "num_enum::TryFromPrimitiveError")
            [ Ty.path "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction" ].
        
        (* TryFromPrimitive *)
        (* Ty.apply (Ty.path "&") [ Ty.path "str" ] *)
        Definition value_NAME : Value.t :=
          M.run ltac:(M.monadic (Value.String "CpiGuardInstruction")).
        
        (* TryFromPrimitive *)
        Definition try_from_primitive (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ number ] =>
            ltac:(M.monadic
              (let number := M.alloc (| number |) in
              M.read (|
                M.match_operator (|
                  number,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Integer 0 |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Ok"
                            [
                              Value.StructTuple
                                "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction::Enable"
                                []
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Integer 1 |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Ok"
                            [
                              Value.StructTuple
                                "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction::Disable"
                                []
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Err"
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "num_enum::TryFromPrimitiveError")
                                    [
                                      Ty.path
                                        "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction"
                                    ],
                                  "new",
                                  []
                                |),
                                [ M.read (| number |) ]
                              |)
                            ]
                        |)))
                  ]
                |)
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "num_enum::TryFromPrimitive"
            Self
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Primitive", InstanceField.Ty _Primitive);
              ("Error", InstanceField.Ty _Error);
              ("value_NAME", InstanceField.Constant value_NAME);
              ("try_from_primitive", InstanceField.Method try_from_primitive)
            ].
      End Impl_num_enum_TryFromPrimitive_for_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction.
      
      Module Impl_core_convert_TryFrom_u8_for_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction.
        Definition Self : Ty.t :=
          Ty.path "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction".
        
        (* TryFromPrimitive *)
        Definition _Error : Ty.t :=
          Ty.apply
            (Ty.path "num_enum::TryFromPrimitiveError")
            [ Ty.path "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction" ].
        
        (* TryFromPrimitive *)
        Definition try_from (τ : list Ty.t) (α : list Value.t) : M :=
          match τ, α with
          | [], [ number ] =>
            ltac:(M.monadic
              (let number := M.alloc (| number |) in
              M.call_closure (|
                M.get_trait_method (|
                  "num_enum::TryFromPrimitive",
                  Ty.path "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction",
                  [],
                  "try_from_primitive",
                  []
                |),
                [ M.read (| number |) ]
              |)))
          | _, _ => M.impossible
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::convert::TryFrom"
            Self
            (* Trait polymorphic types *) [ (* T *) Ty.path "u8" ]
            (* Instance *)
            [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
      End Impl_core_convert_TryFrom_u8_for_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction.
      
      Module Impl_num_enum_CannotDeriveBothFromPrimitiveAndTryFromPrimitive_for_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction.
        Definition Self : Ty.t :=
          Ty.path "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction".
        
        Axiom Implements :
          M.IsTraitInstance
            "num_enum::CannotDeriveBothFromPrimitiveAndTryFromPrimitive"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_num_enum_CannotDeriveBothFromPrimitiveAndTryFromPrimitive_for_spl_token_2022_extension_cpi_guard_instruction_CpiGuardInstruction.
      
      (*
      pub fn enable_cpi_guard(
          token_program_id: &Pubkey,
          account: &Pubkey,
          owner: &Pubkey,
          signers: &[&Pubkey],
      ) -> Result<Instruction, ProgramError> {
          check_program_account(token_program_id)?;
          let mut accounts = vec![
              AccountMeta::new( *account, false),
              AccountMeta::new_readonly( *owner, signers.is_empty()),
          ];
          for signer_pubkey in signers.iter() {
              accounts.push(AccountMeta::new_readonly( **signer_pubkey, true));
          }
          Ok(encode_instruction(
              token_program_id,
              accounts,
              TokenInstruction::CpiGuardExtension,
              CpiGuardInstruction::Enable,
              &(),
          ))
      }
      *)
      Definition enable_cpi_guard (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [], [ token_program_id; account; owner; signers ] =>
          ltac:(M.monadic
            (let token_program_id := M.alloc (| token_program_id |) in
            let account := M.alloc (| account |) in
            let owner := M.alloc (| owner |) in
            let signers := M.alloc (| signers |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let _ :=
                    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.tuple []; Ty.path "solana_program::program_error::ProgramError"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_function (| "spl_token_2022::check_program_account", [] |),
                              [ M.read (| token_program_id |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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_program::instruction::Instruction";
                                            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 accounts :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "slice")
                            [ Ty.path "solana_program::instruction::AccountMeta" ],
                          "into_vec",
                          [ Ty.path "alloc::alloc::Global" ]
                        |),
                        [
                          (* Unsize *)
                          M.pointer_coercion
                            (M.read (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::boxed::Box")
                                    [
                                      Ty.apply
                                        (Ty.path "array")
                                        [ Ty.path "solana_program::instruction::AccountMeta" ];
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  "new",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "solana_program::instruction::AccountMeta",
                                            "new",
                                            []
                                          |),
                                          [ M.read (| M.read (| account |) |); Value.Bool false ]
                                        |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "solana_program::instruction::AccountMeta",
                                            "new_readonly",
                                            []
                                          |),
                                          [
                                            M.read (| M.read (| owner |) |);
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "slice")
                                                  [
                                                    Ty.apply
                                                      (Ty.path "&")
                                                      [ Ty.path "solana_program::pubkey::Pubkey" ]
                                                  ],
                                                "is_empty",
                                                []
                                              |),
                                              [ M.read (| signers |) ]
                                            |)
                                          ]
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            |))
                        ]
                      |)
                    |) in
                  let _ :=
                    M.use
                      (M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::collect::IntoIterator",
                              Ty.apply
                                (Ty.path "core::slice::iter::Iter")
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    [ Ty.path "solana_program::pubkey::Pubkey" ]
                                ],
                              [],
                              "into_iter",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "slice")
                                    [
                                      Ty.apply
                                        (Ty.path "&")
                                        [ Ty.path "solana_program::pubkey::Pubkey" ]
                                    ],
                                  "iter",
                                  []
                                |),
                                [ M.read (| signers |) ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let iter := M.copy (| γ |) in
                              M.loop (|
                                ltac:(M.monadic
                                  (let _ :=
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::iterator::Iterator",
                                            Ty.apply
                                              (Ty.path "core::slice::iter::Iter")
                                              [
                                                Ty.apply
                                                  (Ty.path "&")
                                                  [ Ty.path "solana_program::pubkey::Pubkey" ]
                                              ],
                                            [],
                                            "next",
                                            []
                                          |),
                                          [ iter ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.alloc (|
                                              M.never_to_any (| M.read (| M.break (||) |) |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::option::Option::Some",
                                                0
                                              |) in
                                            let signer_pubkey := M.copy (| γ0_0 |) in
                                            let _ :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "alloc::vec::Vec")
                                                      [
                                                        Ty.path
                                                          "solana_program::instruction::AccountMeta";
                                                        Ty.path "alloc::alloc::Global"
                                                      ],
                                                    "push",
                                                    []
                                                  |),
                                                  [
                                                    accounts;
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path
                                                          "solana_program::instruction::AccountMeta",
                                                        "new_readonly",
                                                        []
                                                      |),
                                                      [
                                                        M.read (|
                                                          M.read (| M.read (| signer_pubkey |) |)
                                                        |);
                                                        Value.Bool true
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                              |)))
                        ]
                      |)) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Ok"
                      [
                        M.call_closure (|
                          M.get_function (|
                            "spl_token_2022::instruction::encode_instruction",
                            [
                              Ty.path
                                "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction";
                              Ty.tuple []
                            ]
                          |),
                          [
                            M.read (| token_program_id |);
                            M.read (| accounts |);
                            Value.StructTuple
                              "spl_token_2022::instruction::TokenInstruction::CpiGuardExtension"
                              [];
                            Value.StructTuple
                              "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction::Enable"
                              [];
                            M.alloc (| Value.Tuple [] |)
                          ]
                        |)
                      ]
                  |)
                |)))
            |)))
        | _, _ => M.impossible
        end.
      
      (*
      pub fn disable_cpi_guard(
          token_program_id: &Pubkey,
          account: &Pubkey,
          owner: &Pubkey,
          signers: &[&Pubkey],
      ) -> Result<Instruction, ProgramError> {
          check_program_account(token_program_id)?;
          let mut accounts = vec![
              AccountMeta::new( *account, false),
              AccountMeta::new_readonly( *owner, signers.is_empty()),
          ];
          for signer_pubkey in signers.iter() {
              accounts.push(AccountMeta::new_readonly( **signer_pubkey, true));
          }
          Ok(encode_instruction(
              token_program_id,
              accounts,
              TokenInstruction::CpiGuardExtension,
              CpiGuardInstruction::Disable,
              &(),
          ))
      }
      *)
      Definition disable_cpi_guard (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [], [ token_program_id; account; owner; signers ] =>
          ltac:(M.monadic
            (let token_program_id := M.alloc (| token_program_id |) in
            let account := M.alloc (| account |) in
            let owner := M.alloc (| owner |) in
            let signers := M.alloc (| signers |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let _ :=
                    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.tuple []; Ty.path "solana_program::program_error::ProgramError"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_function (| "spl_token_2022::check_program_account", [] |),
                              [ M.read (| token_program_id |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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_program::instruction::Instruction";
                                            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 accounts :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "slice")
                            [ Ty.path "solana_program::instruction::AccountMeta" ],
                          "into_vec",
                          [ Ty.path "alloc::alloc::Global" ]
                        |),
                        [
                          (* Unsize *)
                          M.pointer_coercion
                            (M.read (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::boxed::Box")
                                    [
                                      Ty.apply
                                        (Ty.path "array")
                                        [ Ty.path "solana_program::instruction::AccountMeta" ];
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  "new",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "solana_program::instruction::AccountMeta",
                                            "new",
                                            []
                                          |),
                                          [ M.read (| M.read (| account |) |); Value.Bool false ]
                                        |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "solana_program::instruction::AccountMeta",
                                            "new_readonly",
                                            []
                                          |),
                                          [
                                            M.read (| M.read (| owner |) |);
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "slice")
                                                  [
                                                    Ty.apply
                                                      (Ty.path "&")
                                                      [ Ty.path "solana_program::pubkey::Pubkey" ]
                                                  ],
                                                "is_empty",
                                                []
                                              |),
                                              [ M.read (| signers |) ]
                                            |)
                                          ]
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            |))
                        ]
                      |)
                    |) in
                  let _ :=
                    M.use
                      (M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::collect::IntoIterator",
                              Ty.apply
                                (Ty.path "core::slice::iter::Iter")
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    [ Ty.path "solana_program::pubkey::Pubkey" ]
                                ],
                              [],
                              "into_iter",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "slice")
                                    [
                                      Ty.apply
                                        (Ty.path "&")
                                        [ Ty.path "solana_program::pubkey::Pubkey" ]
                                    ],
                                  "iter",
                                  []
                                |),
                                [ M.read (| signers |) ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let iter := M.copy (| γ |) in
                              M.loop (|
                                ltac:(M.monadic
                                  (let _ :=
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::iterator::Iterator",
                                            Ty.apply
                                              (Ty.path "core::slice::iter::Iter")
                                              [
                                                Ty.apply
                                                  (Ty.path "&")
                                                  [ Ty.path "solana_program::pubkey::Pubkey" ]
                                              ],
                                            [],
                                            "next",
                                            []
                                          |),
                                          [ iter ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.alloc (|
                                              M.never_to_any (| M.read (| M.break (||) |) |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::option::Option::Some",
                                                0
                                              |) in
                                            let signer_pubkey := M.copy (| γ0_0 |) in
                                            let _ :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "alloc::vec::Vec")
                                                      [
                                                        Ty.path
                                                          "solana_program::instruction::AccountMeta";
                                                        Ty.path "alloc::alloc::Global"
                                                      ],
                                                    "push",
                                                    []
                                                  |),
                                                  [
                                                    accounts;
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path
                                                          "solana_program::instruction::AccountMeta",
                                                        "new_readonly",
                                                        []
                                                      |),
                                                      [
                                                        M.read (|
                                                          M.read (| M.read (| signer_pubkey |) |)
                                                        |);
                                                        Value.Bool true
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                              |)))
                        ]
                      |)) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Ok"
                      [
                        M.call_closure (|
                          M.get_function (|
                            "spl_token_2022::instruction::encode_instruction",
                            [
                              Ty.path
                                "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction";
                              Ty.tuple []
                            ]
                          |),
                          [
                            M.read (| token_program_id |);
                            M.read (| accounts |);
                            Value.StructTuple
                              "spl_token_2022::instruction::TokenInstruction::CpiGuardExtension"
                              [];
                            Value.StructTuple
                              "spl_token_2022::extension::cpi_guard::instruction::CpiGuardInstruction::Disable"
                              [];
                            M.alloc (| Value.Tuple [] |)
                          ]
                        |)
                      ]
                  |)
                |)))
            |)))
        | _, _ => M.impossible
        end.
    End instruction.
  End cpi_guard.
End extension.
