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

Module extension.
  Module memo_transfer.
    (* StructRecord
      {
        name := "MemoTransfer";
        ty_params := [];
        fields := [ ("require_incoming_transfer_memos", Ty.path "spl_pod::primitives::PodBool") ];
      } *)
    
    Module Impl_core_clone_Clone_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::memo_transfer::MemoTransfer".
      
      (* Clone *)
      Definition clone (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
              |)
            |)))
        | _, _ => M.impossible
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
    
    Module Impl_core_marker_Copy_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::memo_transfer::MemoTransfer".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
    
    Module Impl_core_fmt_Debug_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::memo_transfer::MemoTransfer".
      
      (* Debug *)
      Definition fmt (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_struct_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "MemoTransfer" |);
                M.read (| Value.String "require_incoming_transfer_memos" |);
                (* Unsize *)
                M.pointer_coercion
                  (M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "spl_token_2022::extension::memo_transfer::MemoTransfer",
                      "require_incoming_transfer_memos"
                    |)
                  |))
              ]
            |)))
        | _, _ => M.impossible
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
    
    Module Impl_core_default_Default_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::memo_transfer::MemoTransfer".
      
      (* Default *)
      Definition default (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "spl_token_2022::extension::memo_transfer::MemoTransfer"
              [
                ("require_incoming_transfer_memos",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "spl_pod::primitives::PodBool",
                      [],
                      "default",
                      []
                    |),
                    []
                  |))
              ]))
        | _, _ => M.impossible
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::default::Default"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("default", InstanceField.Method default) ].
    End Impl_core_default_Default_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
    
    Module Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::memo_transfer::MemoTransfer".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
    
    Module Impl_core_cmp_PartialEq_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::memo_transfer::MemoTransfer".
      
      (* PartialEq *)
      Definition eq (τ : list Ty.t) (α : list Value.t) : M :=
        match τ, α with
        | [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.path "spl_pod::primitives::PodBool",
                [ Ty.path "spl_pod::primitives::PodBool" ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "spl_token_2022::extension::memo_transfer::MemoTransfer",
                  "require_incoming_transfer_memos"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "spl_token_2022::extension::memo_transfer::MemoTransfer",
                  "require_incoming_transfer_memos"
                |)
              ]
            |)))
        | _, _ => M.impossible
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
    
    Module Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::memo_transfer::MemoTransfer".
      
      Axiom Implements :
        M.IsTraitInstance
          "bytemuck::pod::Pod"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_bytemuck_pod_Pod_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
    
    Module Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::memo_transfer::MemoTransfer".
      
      Axiom Implements :
        M.IsTraitInstance
          "bytemuck::zeroable::Zeroable"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_bytemuck_zeroable_Zeroable_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
    
    Module Impl_spl_token_2022_extension_Extension_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
      Definition Self : Ty.t := Ty.path "spl_token_2022::extension::memo_transfer::MemoTransfer".
      
      (*     const TYPE: ExtensionType = ExtensionType::MemoTransfer; *)
      (* Ty.path "spl_token_2022::extension::ExtensionType" *)
      Definition value_TYPE : Value.t :=
        M.run
          ltac:(M.monadic
            (M.alloc (|
              Value.StructTuple "spl_token_2022::extension::ExtensionType::MemoTransfer" []
            |))).
      
      Axiom Implements :
        M.IsTraitInstance
          "spl_token_2022::extension::Extension"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("value_TYPE", InstanceField.Constant value_TYPE) ].
    End Impl_spl_token_2022_extension_Extension_for_spl_token_2022_extension_memo_transfer_MemoTransfer.
    
    (*
    pub fn memo_required<BSE: BaseStateWithExtensions<S>, S: BaseState>(account_state: &BSE) -> bool {
        if let Ok(extension) = account_state.get_extension::<MemoTransfer>() {
            return extension.require_incoming_transfer_memos.into();
        }
        false
    }
    *)
    Definition memo_required (τ : list Ty.t) (α : list Value.t) : M :=
      match τ, α with
      | [ BSE; _ as S ], [ account_state ] =>
        ltac:(M.monadic
          (let account_state := M.alloc (| account_state |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let _ :=
                  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::BaseStateWithExtensions",
                                  BSE,
                                  [ S ],
                                  "get_extension",
                                  [ Ty.path "spl_token_2022::extension::memo_transfer::MemoTransfer"
                                  ]
                                |),
                                [ M.read (| account_state |) ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::result::Result::Ok",
                              0
                            |) in
                          let extension := M.copy (| γ0_0 |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::convert::Into",
                                      Ty.path "spl_pod::primitives::PodBool",
                                      [ Ty.path "bool" ],
                                      "into",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| extension |),
                                          "spl_token_2022::extension::memo_transfer::MemoTransfer",
                                          "require_incoming_transfer_memos"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.Bool false |)
              |)))
          |)))
      | _, _ => M.impossible
      end.
    
    (*
    pub fn check_previous_sibling_instruction_is_memo() -> Result<(), ProgramError> {
        let is_memo_program = |program_id: &Pubkey| -> bool {
            program_id == &spl_memo::id() || program_id == &spl_memo::v1::id()
        };
        let previous_instruction = get_processed_sibling_instruction(0);
        match previous_instruction {
            Some(instruction) if is_memo_program(&instruction.program_id) => {}
            _ => {
                return Err(TokenError::NoMemo.into());
            }
        }
        Ok(())
    }
    *)
    Definition check_previous_sibling_instruction_is_memo (τ : list Ty.t) (α : list Value.t) : M :=
      match τ, α with
      | [], [] =>
        ltac:(M.monadic
          (M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let is_memo_program :=
                  M.alloc (|
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [ α0 ] =>
                            M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let program_id := M.copy (| γ |) in
                                    LogicalOp.or (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::cmp::PartialEq",
                                          Ty.apply
                                            (Ty.path "&")
                                            [ Ty.path "solana_program::pubkey::Pubkey" ],
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              [ Ty.path "solana_program::pubkey::Pubkey" ]
                                          ],
                                          "eq",
                                          []
                                        |),
                                        [
                                          program_id;
                                          M.alloc (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_function (| "spl_memo::id", [] |),
                                                []
                                              |)
                                            |)
                                          |)
                                        ]
                                      |),
                                      ltac:(M.monadic
                                        (M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::PartialEq",
                                            Ty.apply
                                              (Ty.path "&")
                                              [ Ty.path "solana_program::pubkey::Pubkey" ],
                                            [
                                              Ty.apply
                                                (Ty.path "&")
                                                [ Ty.path "solana_program::pubkey::Pubkey" ]
                                            ],
                                            "eq",
                                            []
                                          |),
                                          [
                                            program_id;
                                            M.alloc (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_function (| "spl_memo::v1::id", [] |),
                                                  []
                                                |)
                                              |)
                                            |)
                                          ]
                                        |)))
                                    |)))
                              ]
                            |)
                          | _ => M.impossible (||)
                          end))
                  |) in
                let previous_instruction :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "solana_program::instruction::get_processed_sibling_instruction",
                        []
                      |),
                      [ Value.Integer 0 ]
                    |)
                  |) in
                let _ :=
                  M.match_operator (|
                    previous_instruction,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let instruction := M.copy (| γ0_0 |) in
                          let γ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::function::Fn",
                                  Ty.function
                                    [
                                      Ty.tuple
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            [ Ty.path "solana_program::pubkey::Pubkey" ]
                                        ]
                                    ]
                                    (Ty.path "bool"),
                                  [
                                    Ty.tuple
                                      [
                                        Ty.apply
                                          (Ty.path "&")
                                          [ Ty.path "solana_program::pubkey::Pubkey" ]
                                      ]
                                  ],
                                  "call",
                                  []
                                |),
                                [
                                  is_memo_program;
                                  Value.Tuple
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        instruction,
                                        "solana_program::instruction::Instruction",
                                        "program_id"
                                      |)
                                    ]
                                ]
                              |)
                            |) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::convert::Into",
                                          Ty.path "spl_token_2022::error::TokenError",
                                          [ Ty.path "solana_program::program_error::ProgramError" ],
                                          "into",
                                          []
                                        |),
                                        [
                                          Value.StructTuple
                                            "spl_token_2022::error::TokenError::NoMemo"
                                            []
                                        ]
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _ => M.impossible
      end.
  End memo_transfer.
End extension.
