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

Module offchain.
  (*
  pub async fn create_transfer_checked_instruction_with_extra_metas<F, Fut>(
      token_program_id: &Pubkey,
      source_pubkey: &Pubkey,
      mint_pubkey: &Pubkey,
      destination_pubkey: &Pubkey,
      authority_pubkey: &Pubkey,
      signer_pubkeys: &[&Pubkey],
      amount: u64,
      decimals: u8,
      fetch_account_data_fn: F,
  ) -> Result<Instruction, AccountFetchError>
  where
      F: Fn(Pubkey) -> Fut,
      Fut: Future<Output = AccountDataResult>,
  {
      let mut transfer_instruction = crate::instruction::transfer_checked(
          token_program_id,
          source_pubkey,
          mint_pubkey,
          destination_pubkey,
          authority_pubkey,
          signer_pubkeys,
          amount,
          decimals,
      )?;
  
      add_extra_account_metas(
          &mut transfer_instruction,
          source_pubkey,
          mint_pubkey,
          destination_pubkey,
          authority_pubkey,
          amount,
          fetch_account_data_fn,
      )
      .await?;
  
      Ok(transfer_instruction)
  }
  *)
  Definition create_transfer_checked_instruction_with_extra_metas
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match τ, α with
    | [ F; Fut ],
        [
          token_program_id;
          source_pubkey;
          mint_pubkey;
          destination_pubkey;
          authority_pubkey;
          signer_pubkeys;
          amount;
          decimals;
          fetch_account_data_fn
        ] =>
      ltac:(M.monadic
        (let token_program_id := M.alloc (| token_program_id |) in
        let source_pubkey := M.alloc (| source_pubkey |) in
        let mint_pubkey := M.alloc (| mint_pubkey |) in
        let destination_pubkey := M.alloc (| destination_pubkey |) in
        let authority_pubkey := M.alloc (| authority_pubkey |) in
        let signer_pubkeys := M.alloc (| signer_pubkeys |) in
        let amount := M.alloc (| amount |) in
        let decimals := M.alloc (| decimals |) in
        let fetch_account_data_fn := M.alloc (| fetch_account_data_fn |) in
        M.closure
          (fun γ =>
            ltac:(M.monadic
              match γ with
              | [ α0 ] =>
                M.match_operator (|
                  M.alloc (| α0 |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let _task_context := M.copy (| γ |) in
                        M.read (|
                          let token_program_id := M.copy (| token_program_id |) in
                          let source_pubkey := M.copy (| source_pubkey |) in
                          let mint_pubkey := M.copy (| mint_pubkey |) in
                          let destination_pubkey := M.copy (| destination_pubkey |) in
                          let authority_pubkey := M.copy (| authority_pubkey |) in
                          let signer_pubkeys := M.copy (| signer_pubkeys |) in
                          let amount := M.copy (| amount |) in
                          let decimals := M.copy (| decimals |) in
                          let fetch_account_data_fn := M.copy (| fetch_account_data_fn |) in
                          M.use
                            (let transfer_instruction :=
                              M.copy (|
                                M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::Try",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          [
                                            Ty.path "solana_program::instruction::Instruction";
                                            Ty.path "solana_program::program_error::ProgramError"
                                          ],
                                        [],
                                        "branch",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_function (|
                                            "spl_token_2022::instruction::transfer_checked",
                                            []
                                          |),
                                          [
                                            M.read (| token_program_id |);
                                            M.read (| source_pubkey |);
                                            M.read (| mint_pubkey |);
                                            M.read (| destination_pubkey |);
                                            M.read (| authority_pubkey |);
                                            M.read (| signer_pubkeys |);
                                            M.read (| amount |);
                                            M.read (| decimals |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |),
                                  [
                                    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.apply
                                                          (Ty.path "alloc::boxed::Box")
                                                          [
                                                            Ty.dyn
                                                              [ ("core::error::Error::Trait", []) ];
                                                            Ty.path "alloc::alloc::Global"
                                                          ]
                                                      ],
                                                    [
                                                      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.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.apply
                                            (Ty.path "alloc::boxed::Box")
                                            [
                                              Ty.dyn [ ("core::error::Error::Trait", []) ];
                                              Ty.path "alloc::alloc::Global"
                                            ]
                                        ],
                                      [],
                                      "branch",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::future::into_future::IntoFuture",
                                                Ty.associated,
                                                [],
                                                "into_future",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "spl_token_2022::offchain::add_extra_account_metas",
                                                    [ F; Fut ]
                                                  |),
                                                  [
                                                    transfer_instruction;
                                                    M.read (| source_pubkey |);
                                                    M.read (| mint_pubkey |);
                                                    M.read (| destination_pubkey |);
                                                    M.read (| authority_pubkey |);
                                                    M.read (| amount |);
                                                    M.read (| fetch_account_data_fn |)
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let __awaitee := M.copy (| γ |) in
                                                M.loop (|
                                                  ltac:(M.monadic
                                                    (let _ :=
                                                      M.match_operator (|
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::future::future::Future",
                                                              Ty.associated,
                                                              [],
                                                              "poll",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path "core::pin::Pin")
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path "&mut")
                                                                        [ Ty.associated ]
                                                                    ],
                                                                  "new_unchecked",
                                                                  []
                                                                |),
                                                                [ __awaitee ]
                                                              |);
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "core::future::get_context",
                                                                  []
                                                                |),
                                                                [ M.read (| _task_context |) ]
                                                              |)
                                                            ]
                                                          |)
                                                        |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_struct_tuple_field (|
                                                                  γ,
                                                                  "core::task::poll::Poll::Ready",
                                                                  0
                                                                |) in
                                                              let result := M.copy (| γ0_0 |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (| M.break (||) |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (M.alloc (| Value.Tuple [] |)))
                                                        ]
                                                      |) in
                                                    let _ :=
                                                      M.write (|
                                                        _task_context,
                                                        M.read (|
                                                          yield (| M.alloc (| Value.Tuple [] |) |)
                                                        |)
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)))
                                                |)))
                                          ]
                                        |)
                                      |)
                                    ]
                                  |)
                                |),
                                [
                                  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.apply
                                                        (Ty.path "alloc::boxed::Box")
                                                        [
                                                          Ty.dyn
                                                            [ ("core::error::Error::Trait", []) ];
                                                          Ty.path "alloc::alloc::Global"
                                                        ]
                                                    ],
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::result::Result")
                                                      [
                                                        Ty.path "core::convert::Infallible";
                                                        Ty.apply
                                                          (Ty.path "alloc::boxed::Box")
                                                          [
                                                            Ty.dyn
                                                              [ ("core::error::Error::Trait", []) ];
                                                            Ty.path "alloc::alloc::Global"
                                                          ]
                                                      ]
                                                  ],
                                                  "from_residual",
                                                  []
                                                |),
                                                [ M.read (| residual |) ]
                                              |)
                                            |)
                                          |)
                                        |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::ops::control_flow::ControlFlow::Continue",
                                          0
                                        |) in
                                      let val := M.copy (| γ0_0 |) in
                                      val))
                                ]
                              |) in
                            M.alloc (|
                              Value.StructTuple
                                "core::result::Result::Ok"
                                [ M.read (| transfer_instruction |) ]
                            |))
                        |)))
                  ]
                |)
              | _ => M.impossible (||)
              end))))
    | _, _ => M.impossible
    end.
  
  Module create_transfer_checked_instruction_with_extra_metas.
    (* Error OpaqueTy *)
  End create_transfer_checked_instruction_with_extra_metas.
  
  (*
  pub async fn add_extra_account_metas<F, Fut>(
      instruction: &mut Instruction,
      source_pubkey: &Pubkey,
      mint_pubkey: &Pubkey,
      destination_pubkey: &Pubkey,
      authority_pubkey: &Pubkey,
      amount: u64,
      fetch_account_data_fn: F,
  ) -> Result<(), AccountFetchError>
  where
      F: Fn(Pubkey) -> Fut,
      Fut: Future<Output = AccountDataResult>,
  {
      let mint_data = fetch_account_data_fn( *mint_pubkey)
          .await?
          .ok_or(ProgramError::InvalidAccountData)?;
      let mint = StateWithExtensions::<Mint>::unpack(&mint_data)?;
  
      if let Some(program_id) = transfer_hook::get_program_id(&mint) {
          add_extra_account_metas_for_execute(
              instruction,
              &program_id,
              source_pubkey,
              mint_pubkey,
              destination_pubkey,
              authority_pubkey,
              amount,
              fetch_account_data_fn,
          )
          .await?;
      }
  
      Ok(())
  }
  *)
  Definition add_extra_account_metas (τ : list Ty.t) (α : list Value.t) : M :=
    match τ, α with
    | [ F; Fut ],
        [
          instruction;
          source_pubkey;
          mint_pubkey;
          destination_pubkey;
          authority_pubkey;
          amount;
          fetch_account_data_fn
        ] =>
      ltac:(M.monadic
        (let instruction := M.alloc (| instruction |) in
        let source_pubkey := M.alloc (| source_pubkey |) in
        let mint_pubkey := M.alloc (| mint_pubkey |) in
        let destination_pubkey := M.alloc (| destination_pubkey |) in
        let authority_pubkey := M.alloc (| authority_pubkey |) in
        let amount := M.alloc (| amount |) in
        let fetch_account_data_fn := M.alloc (| fetch_account_data_fn |) in
        M.closure
          (fun γ =>
            ltac:(M.monadic
              match γ with
              | [ α0 ] =>
                M.match_operator (|
                  M.alloc (| α0 |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let _task_context := M.copy (| γ |) in
                        M.read (|
                          let instruction := M.copy (| instruction |) in
                          let source_pubkey := M.copy (| source_pubkey |) in
                          let mint_pubkey := M.copy (| mint_pubkey |) in
                          let destination_pubkey := M.copy (| destination_pubkey |) in
                          let authority_pubkey := M.copy (| authority_pubkey |) in
                          let amount := M.copy (| amount |) in
                          let fetch_account_data_fn := M.copy (| fetch_account_data_fn |) in
                          M.use
                            (let mint_data :=
                              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 "alloc::vec::Vec")
                                              [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ];
                                            Ty.path "solana_program::program_error::ProgramError"
                                          ],
                                        [],
                                        "branch",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              [
                                                Ty.apply
                                                  (Ty.path "alloc::vec::Vec")
                                                  [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]
                                              ],
                                            "ok_or",
                                            [ Ty.path "solana_program::program_error::ProgramError"
                                            ]
                                          |),
                                          [
                                            M.read (|
                                              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 "core::option::Option")
                                                            [
                                                              Ty.apply
                                                                (Ty.path "alloc::vec::Vec")
                                                                [
                                                                  Ty.path "u8";
                                                                  Ty.path "alloc::alloc::Global"
                                                                ]
                                                            ];
                                                          Ty.apply
                                                            (Ty.path "alloc::boxed::Box")
                                                            [
                                                              Ty.dyn
                                                                [ ("core::error::Error::Trait", [])
                                                                ];
                                                              Ty.path "alloc::alloc::Global"
                                                            ]
                                                        ],
                                                      [],
                                                      "branch",
                                                      []
                                                    |),
                                                    [
                                                      M.read (|
                                                        M.match_operator (|
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::future::into_future::IntoFuture",
                                                                Fut,
                                                                [],
                                                                "into_future",
                                                                []
                                                              |),
                                                              [
                                                                M.call_closure (|
                                                                  M.get_trait_method (|
                                                                    "core::ops::function::Fn",
                                                                    F,
                                                                    [
                                                                      Ty.tuple
                                                                        [
                                                                          Ty.path
                                                                            "solana_program::pubkey::Pubkey"
                                                                        ]
                                                                    ],
                                                                    "call",
                                                                    []
                                                                  |),
                                                                  [
                                                                    fetch_account_data_fn;
                                                                    Value.Tuple
                                                                      [
                                                                        M.read (|
                                                                          M.read (| mint_pubkey |)
                                                                        |)
                                                                      ]
                                                                  ]
                                                                |)
                                                              ]
                                                            |)
                                                          |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let __awaitee := M.copy (| γ |) in
                                                                M.loop (|
                                                                  ltac:(M.monadic
                                                                    (let _ :=
                                                                      M.match_operator (|
                                                                        M.alloc (|
                                                                          M.call_closure (|
                                                                            M.get_trait_method (|
                                                                              "core::future::future::Future",
                                                                              Fut,
                                                                              [],
                                                                              "poll",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "core::pin::Pin")
                                                                                    [
                                                                                      Ty.apply
                                                                                        (Ty.path
                                                                                          "&mut")
                                                                                        [ Fut ]
                                                                                    ],
                                                                                  "new_unchecked",
                                                                                  []
                                                                                |),
                                                                                [ __awaitee ]
                                                                              |);
                                                                              M.call_closure (|
                                                                                M.get_function (|
                                                                                  "core::future::get_context",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.read (|
                                                                                    _task_context
                                                                                  |)
                                                                                ]
                                                                              |)
                                                                            ]
                                                                          |)
                                                                        |),
                                                                        [
                                                                          fun γ =>
                                                                            ltac:(M.monadic
                                                                              (let γ0_0 :=
                                                                                M.SubPointer.get_struct_tuple_field (|
                                                                                  γ,
                                                                                  "core::task::poll::Poll::Ready",
                                                                                  0
                                                                                |) in
                                                                              let result :=
                                                                                M.copy (| γ0_0 |) in
                                                                              M.alloc (|
                                                                                M.never_to_any (|
                                                                                  M.read (|
                                                                                    M.break (||)
                                                                                  |)
                                                                                |)
                                                                              |)));
                                                                          fun γ =>
                                                                            ltac:(M.monadic
                                                                              (M.alloc (|
                                                                                Value.Tuple []
                                                                              |)))
                                                                        ]
                                                                      |) in
                                                                    let _ :=
                                                                      M.write (|
                                                                        _task_context,
                                                                        M.read (|
                                                                          yield (|
                                                                            M.alloc (|
                                                                              Value.Tuple []
                                                                            |)
                                                                          |)
                                                                        |)
                                                                      |) in
                                                                    M.alloc (| Value.Tuple [] |)))
                                                                |)))
                                                          ]
                                                        |)
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  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.apply
                                                                        (Ty.path
                                                                          "alloc::boxed::Box")
                                                                        [
                                                                          Ty.dyn
                                                                            [
                                                                              ("core::error::Error::Trait",
                                                                                [])
                                                                            ];
                                                                          Ty.path
                                                                            "alloc::alloc::Global"
                                                                        ]
                                                                    ],
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::result::Result")
                                                                      [
                                                                        Ty.path
                                                                          "core::convert::Infallible";
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "alloc::boxed::Box")
                                                                          [
                                                                            Ty.dyn
                                                                              [
                                                                                ("core::error::Error::Trait",
                                                                                  [])
                                                                              ];
                                                                            Ty.path
                                                                              "alloc::alloc::Global"
                                                                          ]
                                                                      ]
                                                                  ],
                                                                  "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))
                                                ]
                                              |)
                                            |);
                                            Value.StructTuple
                                              "solana_program::program_error::ProgramError::InvalidAccountData"
                                              []
                                          ]
                                        |)
                                      ]
                                    |)
                                  |),
                                  [
                                    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.apply
                                                          (Ty.path "alloc::boxed::Box")
                                                          [
                                                            Ty.dyn
                                                              [ ("core::error::Error::Trait", []) ];
                                                            Ty.path "alloc::alloc::Global"
                                                          ]
                                                      ],
                                                    [
                                                      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 mint :=
                              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::StateWithExtensions")
                                              [ Ty.path "spl_token_2022::state::Mint" ];
                                            Ty.path "solana_program::program_error::ProgramError"
                                          ],
                                        [],
                                        "branch",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path
                                                "spl_token_2022::extension::StateWithExtensions")
                                              [ Ty.path "spl_token_2022::state::Mint" ],
                                            "unpack",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::deref::Deref",
                                                Ty.apply
                                                  (Ty.path "alloc::vec::Vec")
                                                  [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                                                [],
                                                "deref",
                                                []
                                              |),
                                              [ mint_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.apply
                                                          (Ty.path "alloc::boxed::Box")
                                                          [
                                                            Ty.dyn
                                                              [ ("core::error::Error::Trait", []) ];
                                                            Ty.path "alloc::alloc::Global"
                                                          ]
                                                      ],
                                                    [
                                                      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.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "spl_token_2022::extension::transfer_hook::get_program_id",
                                              [
                                                Ty.path "spl_token_2022::state::Mint";
                                                Ty.apply
                                                  (Ty.path
                                                    "spl_token_2022::extension::StateWithExtensions")
                                                  [ Ty.path "spl_token_2022::state::Mint" ]
                                              ]
                                            |),
                                            [ mint ]
                                          |)
                                        |) in
                                      let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let program_id := M.copy (| γ0_0 |) in
                                      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.apply
                                                      (Ty.path "alloc::boxed::Box")
                                                      [
                                                        Ty.dyn
                                                          [ ("core::error::Error::Trait", []) ];
                                                        Ty.path "alloc::alloc::Global"
                                                      ]
                                                  ],
                                                [],
                                                "branch",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.match_operator (|
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::future::into_future::IntoFuture",
                                                          Ty.associated,
                                                          [],
                                                          "into_future",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_function (|
                                                              "spl_transfer_hook_interface::offchain::add_extra_account_metas_for_execute",
                                                              [ F; Fut ]
                                                            |),
                                                            [
                                                              M.read (| instruction |);
                                                              program_id;
                                                              M.read (| source_pubkey |);
                                                              M.read (| mint_pubkey |);
                                                              M.read (| destination_pubkey |);
                                                              M.read (| authority_pubkey |);
                                                              M.read (| amount |);
                                                              M.read (| fetch_account_data_fn |)
                                                            ]
                                                          |)
                                                        ]
                                                      |)
                                                    |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let __awaitee := M.copy (| γ |) in
                                                          M.loop (|
                                                            ltac:(M.monadic
                                                              (let _ :=
                                                                M.match_operator (|
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::future::future::Future",
                                                                        Ty.associated,
                                                                        [],
                                                                        "poll",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::pin::Pin")
                                                                              [
                                                                                Ty.apply
                                                                                  (Ty.path "&mut")
                                                                                  [ Ty.associated ]
                                                                              ],
                                                                            "new_unchecked",
                                                                            []
                                                                          |),
                                                                          [ __awaitee ]
                                                                        |);
                                                                        M.call_closure (|
                                                                          M.get_function (|
                                                                            "core::future::get_context",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.read (|
                                                                              _task_context
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |),
                                                                  [
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (let γ0_0 :=
                                                                          M.SubPointer.get_struct_tuple_field (|
                                                                            γ,
                                                                            "core::task::poll::Poll::Ready",
                                                                            0
                                                                          |) in
                                                                        let result :=
                                                                          M.copy (| γ0_0 |) in
                                                                        M.alloc (|
                                                                          M.never_to_any (|
                                                                            M.read (|
                                                                              M.break (||)
                                                                            |)
                                                                          |)
                                                                        |)));
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (M.alloc (|
                                                                          Value.Tuple []
                                                                        |)))
                                                                  ]
                                                                |) in
                                                              let _ :=
                                                                M.write (|
                                                                  _task_context,
                                                                  M.read (|
                                                                    yield (|
                                                                      M.alloc (| Value.Tuple [] |)
                                                                    |)
                                                                  |)
                                                                |) in
                                                              M.alloc (| Value.Tuple [] |)))
                                                          |)))
                                                    ]
                                                  |)
                                                |)
                                              ]
                                            |)
                                          |),
                                          [
                                            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.apply
                                                                  (Ty.path "alloc::boxed::Box")
                                                                  [
                                                                    Ty.dyn
                                                                      [
                                                                        ("core::error::Error::Trait",
                                                                          [])
                                                                      ];
                                                                    Ty.path "alloc::alloc::Global"
                                                                  ]
                                                              ],
                                                            [
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                [
                                                                  Ty.path
                                                                    "core::convert::Infallible";
                                                                  Ty.apply
                                                                    (Ty.path "alloc::boxed::Box")
                                                                    [
                                                                      Ty.dyn
                                                                        [
                                                                          ("core::error::Error::Trait",
                                                                            [])
                                                                        ];
                                                                      Ty.path "alloc::alloc::Global"
                                                                    ]
                                                                ]
                                                            ],
                                                            "from_residual",
                                                            []
                                                          |),
                                                          [ M.read (| residual |) ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ0_0 :=
                                                  M.SubPointer.get_struct_tuple_field (|
                                                    γ,
                                                    "core::ops::control_flow::ControlFlow::Continue",
                                                    0
                                                  |) in
                                                let val := M.copy (| γ0_0 |) in
                                                val))
                                          ]
                                        |) in
                                      M.alloc (| Value.Tuple [] |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (|
                              Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                            |))
                        |)))
                  ]
                |)
              | _ => M.impossible (||)
              end))))
    | _, _ => M.impossible
    end.
  
  Module add_extra_account_metas.
    (* Error OpaqueTy *)
  End add_extra_account_metas.
End offchain.
