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

Module extension.
  Module memo_transfer.
    Module processor.
      (*
      fn process_toggle_required_memo_transfers(
          program_id: &Pubkey,
          accounts: &[AccountInfo],
          enable: bool,
      ) -> ProgramResult {
          let account_info_iter = &mut accounts.iter();
          let token_account_info = next_account_info(account_info_iter)?;
          let owner_info = next_account_info(account_info_iter)?;
          let owner_info_data_len = owner_info.data_len();
      
          let mut account_data = token_account_info.data.borrow_mut();
          let mut account = PodStateWithExtensionsMut::<PodAccount>::unpack(&mut account_data)?;
      
          Processor::validate_owner(
              program_id,
              &account.base.owner,
              owner_info,
              owner_info_data_len,
              account_info_iter.as_slice(),
          )?;
      
          let extension = if let Ok(extension) = account.get_extension_mut::<MemoTransfer>() {
              extension
          } else {
              account.init_extension::<MemoTransfer>(true)?
          };
          extension.require_incoming_transfer_memos = enable.into();
          Ok(())
      }
      *)
      Definition process_toggle_required_memo_transfers (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [], [ program_id; accounts; enable ] =>
          ltac:(M.monadic
            (let program_id := M.alloc (| program_id |) in
            let accounts := M.alloc (| accounts |) in
            let enable := M.alloc (| enable |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let account_info_iter :=
                    M.alloc (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "slice")
                              [ Ty.path "solana_program::account_info::AccountInfo" ],
                            "iter",
                            []
                          |),
                          [ M.read (| accounts |) ]
                        |)
                      |)
                    |) in
                  let token_account_info :=
                    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 "&")
                                    [ Ty.path "solana_program::account_info::AccountInfo" ];
                                  Ty.path "solana_program::program_error::ProgramError"
                                ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_function (|
                                  "solana_program::account_info::next_account_info",
                                  [
                                    Ty.apply
                                      (Ty.path "core::slice::iter::Iter")
                                      [ Ty.path "solana_program::account_info::AccountInfo" ]
                                  ]
                                |),
                                [ M.read (| account_info_iter |) ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Break",
                                  0
                                |) in
                              let residual := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::try_trait::FromResidual",
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            [
                                              Ty.tuple [];
                                              Ty.path "solana_program::program_error::ProgramError"
                                            ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path "core::convert::Infallible";
                                                Ty.path
                                                  "solana_program::program_error::ProgramError"
                                              ]
                                          ],
                                          "from_residual",
                                          []
                                        |),
                                        [ M.read (| residual |) ]
                                      |)
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Continue",
                                  0
                                |) in
                              let val := M.copy (| γ0_0 |) in
                              val))
                        ]
                      |)
                    |) in
                  let owner_info :=
                    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 "&")
                                    [ Ty.path "solana_program::account_info::AccountInfo" ];
                                  Ty.path "solana_program::program_error::ProgramError"
                                ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_function (|
                                  "solana_program::account_info::next_account_info",
                                  [
                                    Ty.apply
                                      (Ty.path "core::slice::iter::Iter")
                                      [ Ty.path "solana_program::account_info::AccountInfo" ]
                                  ]
                                |),
                                [ M.read (| account_info_iter |) ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Break",
                                  0
                                |) in
                              let residual := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::try_trait::FromResidual",
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            [
                                              Ty.tuple [];
                                              Ty.path "solana_program::program_error::ProgramError"
                                            ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path "core::convert::Infallible";
                                                Ty.path
                                                  "solana_program::program_error::ProgramError"
                                              ]
                                          ],
                                          "from_residual",
                                          []
                                        |),
                                        [ M.read (| residual |) ]
                                      |)
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Continue",
                                  0
                                |) in
                              let val := M.copy (| γ0_0 |) in
                              val))
                        ]
                      |)
                    |) in
                  let owner_info_data_len :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "solana_program::account_info::AccountInfo",
                          "data_len",
                          []
                        |),
                        [ M.read (| owner_info |) ]
                      |)
                    |) in
                  let account_data :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::cell::RefCell")
                            [
                              Ty.apply
                                (Ty.path "&mut")
                                [ Ty.apply (Ty.path "slice") [ Ty.path "u8" ] ]
                            ],
                          "borrow_mut",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.apply
                                (Ty.path "alloc::rc::Rc")
                                [
                                  Ty.apply
                                    (Ty.path "core::cell::RefCell")
                                    [
                                      Ty.apply
                                        (Ty.path "&mut")
                                        [ Ty.apply (Ty.path "slice") [ Ty.path "u8" ] ]
                                    ];
                                  Ty.path "alloc::alloc::Global"
                                ],
                              [],
                              "deref",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| token_account_info |),
                                "solana_program::account_info::AccountInfo",
                                "data"
                              |)
                            ]
                          |)
                        ]
                      |)
                    |) in
                  let account :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply
                                (Ty.path "core::result::Result")
                                [
                                  Ty.apply
                                    (Ty.path "spl_token_2022::extension::PodStateWithExtensionsMut")
                                    [ Ty.path "spl_token_2022::pod::PodAccount" ];
                                  Ty.path "solana_program::program_error::ProgramError"
                                ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "spl_token_2022::extension::PodStateWithExtensionsMut")
                                    [ Ty.path "spl_token_2022::pod::PodAccount" ],
                                  "unpack",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::deref::DerefMut",
                                        Ty.apply
                                          (Ty.path "core::cell::RefMut")
                                          [
                                            Ty.apply
                                              (Ty.path "&mut")
                                              [ Ty.apply (Ty.path "slice") [ Ty.path "u8" ] ]
                                          ],
                                        [],
                                        "deref_mut",
                                        []
                                      |),
                                      [ account_data ]
                                    |)
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Break",
                                  0
                                |) in
                              let residual := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::try_trait::FromResidual",
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            [
                                              Ty.tuple [];
                                              Ty.path "solana_program::program_error::ProgramError"
                                            ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              [
                                                Ty.path "core::convert::Infallible";
                                                Ty.path
                                                  "solana_program::program_error::ProgramError"
                                              ]
                                          ],
                                          "from_residual",
                                          []
                                        |),
                                        [ M.read (| residual |) ]
                                      |)
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Continue",
                                  0
                                |) in
                              let val := M.copy (| γ0_0 |) in
                              val))
                        ]
                      |)
                    |) in
                  let _ :=
                    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_associated_function (|
                                Ty.path "spl_token_2022::processor::Processor",
                                "validate_owner",
                                []
                              |),
                              [
                                M.read (| program_id |);
                                M.SubPointer.get_struct_record_field (|
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      account,
                                      "spl_token_2022::extension::PodStateWithExtensionsMut",
                                      "base"
                                    |)
                                  |),
                                  "spl_token_2022::pod::PodAccount",
                                  "owner"
                                |);
                                M.read (| owner_info |);
                                M.read (| owner_info_data_len |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::slice::iter::Iter")
                                      [ Ty.path "solana_program::account_info::AccountInfo" ],
                                    "as_slice",
                                    []
                                  |),
                                  [ M.read (| account_info_iter |) ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          [
                                            Ty.tuple [];
                                            Ty.path "solana_program::program_error::ProgramError"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "solana_program::program_error::ProgramError"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |) in
                  let extension :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "spl_token_2022::extension::BaseStateWithExtensionsMut",
                                      Ty.apply
                                        (Ty.path
                                          "spl_token_2022::extension::PodStateWithExtensionsMut")
                                        [ Ty.path "spl_token_2022::pod::PodAccount" ],
                                      [ Ty.path "spl_token_2022::pod::PodAccount" ],
                                      "get_extension_mut",
                                      [
                                        Ty.path
                                          "spl_token_2022::extension::memo_transfer::MemoTransfer"
                                      ]
                                    |),
                                    [ account ]
                                  |)
                                |) in
                              let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::result::Result::Ok",
                                  0
                                |) in
                              let extension := M.copy (| γ0_0 |) in
                              extension));
                          fun γ =>
                            ltac:(M.monadic
                              (M.alloc (|
                                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 "&mut")
                                                [
                                                  Ty.path
                                                    "spl_token_2022::extension::memo_transfer::MemoTransfer"
                                                ];
                                              Ty.path "solana_program::program_error::ProgramError"
                                            ],
                                          [],
                                          "branch",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "spl_token_2022::extension::BaseStateWithExtensionsMut",
                                              Ty.apply
                                                (Ty.path
                                                  "spl_token_2022::extension::PodStateWithExtensionsMut")
                                                [ Ty.path "spl_token_2022::pod::PodAccount" ],
                                              [ Ty.path "spl_token_2022::pod::PodAccount" ],
                                              "init_extension",
                                              [
                                                Ty.path
                                                  "spl_token_2022::extension::memo_transfer::MemoTransfer"
                                              ]
                                            |),
                                            [ account; Value.Bool true ]
                                          |)
                                        ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::ops::control_flow::ControlFlow::Break",
                                              0
                                            |) in
                                          let residual := M.copy (| γ0_0 |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                M.return_ (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::try_trait::FromResidual",
                                                      Ty.apply
                                                        (Ty.path "core::result::Result")
                                                        [
                                                          Ty.tuple [];
                                                          Ty.path
                                                            "solana_program::program_error::ProgramError"
                                                        ],
                                                      [
                                                        Ty.apply
                                                          (Ty.path "core::result::Result")
                                                          [
                                                            Ty.path "core::convert::Infallible";
                                                            Ty.path
                                                              "solana_program::program_error::ProgramError"
                                                          ]
                                                      ],
                                                      "from_residual",
                                                      []
                                                    |),
                                                    [ M.read (| residual |) ]
                                                  |)
                                                |)
                                              |)
                                            |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::ops::control_flow::ControlFlow::Continue",
                                              0
                                            |) in
                                          let val := M.copy (| γ0_0 |) in
                                          val))
                                    ]
                                  |)
                                |)
                              |)))
                        ]
                      |)
                    |) in
                  let _ :=
                    M.write (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| extension |),
                        "spl_token_2022::extension::memo_transfer::MemoTransfer",
                        "require_incoming_transfer_memos"
                      |),
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::convert::Into",
                          Ty.path "bool",
                          [ Ty.path "spl_pod::primitives::PodBool" ],
                          "into",
                          []
                        |),
                        [ M.read (| enable |) ]
                      |)
                    |) in
                  M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
                |)))
            |)))
        | _, _ => M.impossible
        end.
      
      (*
      pub(crate) fn process_instruction(
          program_id: &Pubkey,
          accounts: &[AccountInfo],
          input: &[u8],
      ) -> ProgramResult {
          check_program_account(program_id)?;
      
          match decode_instruction_type(input)? {
              RequiredMemoTransfersInstruction::Enable => {
                  msg!("RequiredMemoTransfersInstruction::Enable");
                  process_toggle_required_memo_transfers(program_id, accounts, true /* enable */)
              }
              RequiredMemoTransfersInstruction::Disable => {
                  msg!("RequiredMemoTransfersInstruction::Disable");
                  process_toggle_required_memo_transfers(program_id, accounts, false /* disable */)
              }
          }
      }
      *)
      Definition process_instruction (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [], [ program_id; accounts; input ] =>
          ltac:(M.monadic
            (let program_id := M.alloc (| program_id |) in
            let accounts := M.alloc (| accounts |) in
            let input := M.alloc (| input |) 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 (| 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.tuple [];
                                            Ty.path "solana_program::program_error::ProgramError"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "solana_program::program_error::ProgramError"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |) in
                  M.match_operator (|
                    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
                                  "spl_token_2022::extension::memo_transfer::instruction::RequiredMemoTransfersInstruction";
                                Ty.path "solana_program::program_error::ProgramError"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_function (|
                                "spl_token_2022::instruction::decode_instruction_type",
                                [
                                  Ty.path
                                    "spl_token_2022::extension::memo_transfer::instruction::RequiredMemoTransfersInstruction"
                                ]
                              |),
                              [ M.read (| input |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          [
                                            Ty.tuple [];
                                            Ty.path "solana_program::program_error::ProgramError"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "solana_program::program_error::ProgramError"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (| "solana_program::log::sol_log", [] |),
                                [
                                  M.read (|
                                    Value.String "RequiredMemoTransfersInstruction::Enable"
                                  |)
                                ]
                              |)
                            |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (|
                                "spl_token_2022::extension::memo_transfer::processor::process_toggle_required_memo_transfers",
                                []
                              |),
                              [ M.read (| program_id |); M.read (| accounts |); Value.Bool true ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (| "solana_program::log::sol_log", [] |),
                                [
                                  M.read (|
                                    Value.String "RequiredMemoTransfersInstruction::Disable"
                                  |)
                                ]
                              |)
                            |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (|
                                "spl_token_2022::extension::memo_transfer::processor::process_toggle_required_memo_transfers",
                                []
                              |),
                              [ M.read (| program_id |); M.read (| accounts |); Value.Bool false ]
                            |)
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _ => M.impossible
        end.
    End processor.
  End memo_transfer.
End extension.
