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

(*
pub fn ui_amount_to_amount(ui_amount: f64, decimals: u8) -> u64 {
    (ui_amount * 10_usize.pow(decimals as u32) as f64) as u64
}
*)
Definition ui_amount_to_amount (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ ui_amount; decimals ] =>
    ltac:(M.monadic
      (let ui_amount := M.alloc (| ui_amount |) in
      let decimals := M.alloc (| decimals |) in
      M.rust_cast
        (BinOp.Panic.mul (|
          Integer.Usize,
          M.read (| ui_amount |),
          M.rust_cast
            (M.call_closure (|
              M.get_associated_function (| Ty.path "usize", "pow", [] |),
              [ Value.Integer 10; M.rust_cast (M.read (| decimals |)) ]
            |))
        |))))
  | _, _ => M.impossible
  end.

(*
pub fn amount_to_ui_amount(amount: u64, decimals: u8) -> f64 {
    amount as f64 / 10_usize.pow(decimals as u32) as f64
}
*)
Definition amount_to_ui_amount (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ amount; decimals ] =>
    ltac:(M.monadic
      (let amount := M.alloc (| amount |) in
      let decimals := M.alloc (| decimals |) in
      BinOp.Panic.div (|
        Integer.Usize,
        M.rust_cast (M.read (| amount |)),
        M.rust_cast
          (M.call_closure (|
            M.get_associated_function (| Ty.path "usize", "pow", [] |),
            [ Value.Integer 10; M.rust_cast (M.read (| decimals |)) ]
          |))
      |)))
  | _, _ => M.impossible
  end.

(*
pub fn amount_to_ui_amount_string(amount: u64, decimals: u8) -> String {
    let decimals = decimals as usize;
    if decimals > 0 {
        // Left-pad zeros to decimals + 1, so we at least have an integer zero
        let mut s = format!("{:01$}", amount, decimals + 1);
        // Add the decimal point (Sorry, "," locales!)
        s.insert(s.len() - decimals, '.');
        s
    } else {
        amount.to_string()
    }
}
*)
Definition amount_to_ui_amount_string (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ amount; decimals ] =>
    ltac:(M.monadic
      (let amount := M.alloc (| amount |) in
      let decimals := M.alloc (| decimals |) in
      M.read (|
        let decimals := M.alloc (| M.rust_cast (M.read (| decimals |)) |) in
        M.match_operator (|
          M.alloc (| Value.Tuple [] |),
          [
            fun γ =>
              ltac:(M.monadic
                (let γ :=
                  M.use (M.alloc (| BinOp.Pure.gt (M.read (| decimals |)) (Value.Integer 0) |)) in
                let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                let s :=
                  M.copy (|
                    let res :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (| "alloc::fmt::format", [] |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Arguments",
                                "new_v1_formatted",
                                []
                              |),
                              [
                                (* Unsize *)
                                M.pointer_coercion
                                  (M.alloc (| Value.Array [ M.read (| Value.String "" |) ] |));
                                (* Unsize *)
                                M.pointer_coercion
                                  (M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Argument",
                                            "new_display",
                                            [ Ty.path "u64" ]
                                          |),
                                          [ amount ]
                                        |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Argument",
                                            "from_usize",
                                            []
                                          |),
                                          [
                                            M.alloc (|
                                              BinOp.Panic.add (|
                                                Integer.Usize,
                                                M.read (| decimals |),
                                                Value.Integer 1
                                              |)
                                            |)
                                          ]
                                        |)
                                      ]
                                  |));
                                (* Unsize *)
                                M.pointer_coercion
                                  (M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Placeholder",
                                            "new",
                                            []
                                          |),
                                          [
                                            Value.Integer 0;
                                            Value.UnicodeChar 32;
                                            Value.StructTuple
                                              "core::fmt::rt::Alignment::Unknown"
                                              [];
                                            Value.Integer 8;
                                            Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                            Value.StructTuple
                                              "core::fmt::rt::Count::Param"
                                              [ Value.Integer 1 ]
                                          ]
                                        |)
                                      ]
                                  |));
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::fmt::rt::UnsafeArg",
                                    "new",
                                    []
                                  |),
                                  []
                                |)
                              ]
                            |)
                          ]
                        |)
                      |) in
                    res
                  |) in
                let _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "alloc::string::String", "insert", [] |),
                      [
                        s;
                        BinOp.Panic.sub (|
                          Integer.Usize,
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "alloc::string::String",
                              "len",
                              []
                            |),
                            [ s ]
                          |),
                          M.read (| decimals |)
                        |);
                        Value.UnicodeChar 46
                      ]
                    |)
                  |) in
                s));
            fun γ =>
              ltac:(M.monadic
                (M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "alloc::string::ToString",
                      Ty.path "u64",
                      [],
                      "to_string",
                      []
                    |),
                    [ amount ]
                  |)
                |)))
          ]
        |)
      |)))
  | _, _ => M.impossible
  end.

(*
pub fn amount_to_ui_amount_string_trimmed(amount: u64, decimals: u8) -> String {
    let mut s = amount_to_ui_amount_string(amount, decimals);
    if decimals > 0 {
        let zeros_trimmed = s.trim_end_matches('0');
        s = zeros_trimmed.trim_end_matches('.').to_string();
    }
    s
}
*)
Definition amount_to_ui_amount_string_trimmed (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ amount; decimals ] =>
    ltac:(M.monadic
      (let amount := M.alloc (| amount |) in
      let decimals := M.alloc (| decimals |) in
      M.read (|
        let s :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "spl_token_2022::amount_to_ui_amount_string", [] |),
              [ M.read (| amount |); M.read (| decimals |) ]
            |)
          |) in
        let _ :=
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.use (M.alloc (| BinOp.Pure.gt (M.read (| decimals |)) (Value.Integer 0) |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  let zeros_trimmed :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "str",
                          "trim_end_matches",
                          [ Ty.path "char" ]
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.path "alloc::string::String",
                              [],
                              "deref",
                              []
                            |),
                            [ s ]
                          |);
                          Value.UnicodeChar 48
                        ]
                      |)
                    |) in
                  let _ :=
                    M.write (|
                      s,
                      M.call_closure (|
                        M.get_trait_method (|
                          "alloc::string::ToString",
                          Ty.path "str",
                          [],
                          "to_string",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "str",
                              "trim_end_matches",
                              [ Ty.path "char" ]
                            |),
                            [ M.read (| zeros_trimmed |); Value.UnicodeChar 46 ]
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)));
              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
            ]
          |) in
        s
      |)))
  | _, _ => M.impossible
  end.

(*
pub fn try_ui_amount_into_amount(ui_amount: String, decimals: u8) -> Result<u64, ProgramError> {
    let decimals = decimals as usize;
    let mut parts = ui_amount.split('.');
    // splitting a string, even an empty one, will always yield an iterator of at
    // least length == 1
    let mut amount_str = parts.next().unwrap().to_string();
    let after_decimal = parts.next().unwrap_or("");
    let after_decimal = after_decimal.trim_end_matches('0');
    if (amount_str.is_empty() && after_decimal.is_empty())
        || parts.next().is_some()
        || after_decimal.len() > decimals
    {
        return Err(ProgramError::InvalidArgument);
    }

    amount_str.push_str(after_decimal);
    for _ in 0..decimals.saturating_sub(after_decimal.len()) {
        amount_str.push('0');
    }
    amount_str
        .parse::<u64>()
        .map_err(|_| ProgramError::InvalidArgument)
}
*)
Definition try_ui_amount_into_amount (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ ui_amount; decimals ] =>
    ltac:(M.monadic
      (let ui_amount := M.alloc (| ui_amount |) in
      let decimals := M.alloc (| decimals |) in
      M.catch_return (|
        ltac:(M.monadic
          (M.read (|
            let decimals := M.alloc (| M.rust_cast (M.read (| decimals |)) |) in
            let parts :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "str", "split", [ Ty.path "char" ] |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::Deref",
                        Ty.path "alloc::string::String",
                        [],
                        "deref",
                        []
                      |),
                      [ ui_amount ]
                    |);
                    Value.UnicodeChar 46
                  ]
                |)
              |) in
            let amount_str :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "alloc::string::ToString",
                    Ty.path "str",
                    [],
                    "to_string",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::option::Option")
                          [ Ty.apply (Ty.path "&") [ Ty.path "str" ] ],
                        "unwrap",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::iterator::Iterator",
                            Ty.apply (Ty.path "core::str::iter::Split") [ Ty.path "char" ],
                            [],
                            "next",
                            []
                          |),
                          [ parts ]
                        |)
                      ]
                    |)
                  ]
                |)
              |) in
            let after_decimal :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::option::Option")
                      [ Ty.apply (Ty.path "&") [ Ty.path "str" ] ],
                    "unwrap_or",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply (Ty.path "core::str::iter::Split") [ Ty.path "char" ],
                        [],
                        "next",
                        []
                      |),
                      [ parts ]
                    |);
                    M.read (| Value.String "" |)
                  ]
                |)
              |) in
            let after_decimal :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "str",
                    "trim_end_matches",
                    [ Ty.path "char" ]
                  |),
                  [ M.read (| after_decimal |); Value.UnicodeChar 48 ]
                |)
              |) in
            let _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            LogicalOp.or (|
                              LogicalOp.or (|
                                LogicalOp.and (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "alloc::string::String",
                                      "is_empty",
                                      []
                                    |),
                                    [ amount_str ]
                                  |),
                                  ltac:(M.monadic
                                    (M.call_closure (|
                                      M.get_associated_function (| Ty.path "str", "is_empty", [] |),
                                      [ M.read (| after_decimal |) ]
                                    |)))
                                |),
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        [ Ty.apply (Ty.path "&") [ Ty.path "str" ] ],
                                      "is_some",
                                      []
                                    |),
                                    [
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::iterator::Iterator",
                                            Ty.apply
                                              (Ty.path "core::str::iter::Split")
                                              [ Ty.path "char" ],
                                            [],
                                            "next",
                                            []
                                          |),
                                          [ parts ]
                                        |)
                                      |)
                                    ]
                                  |)))
                              |),
                              ltac:(M.monadic
                                (BinOp.Pure.gt
                                  (M.call_closure (|
                                    M.get_associated_function (| Ty.path "str", "len", [] |),
                                    [ M.read (| after_decimal |) ]
                                  |))
                                  (M.read (| decimals |))))
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.read (|
                            M.return_ (|
                              Value.StructTuple
                                "core::result::Result::Err"
                                [
                                  Value.StructTuple
                                    "solana_program::program_error::ProgramError::InvalidArgument"
                                    []
                                ]
                            |)
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "alloc::string::String", "push_str", [] |),
                  [ amount_str; M.read (| after_decimal |) ]
                |)
              |) in
            let _ :=
              M.use
                (M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::IntoIterator",
                        Ty.apply (Ty.path "core::ops::range::Range") [ Ty.path "usize" ],
                        [],
                        "into_iter",
                        []
                      |),
                      [
                        Value.StructRecord
                          "core::ops::range::Range"
                          [
                            ("start", Value.Integer 0);
                            ("end_",
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "usize",
                                  "saturating_sub",
                                  []
                                |),
                                [
                                  M.read (| decimals |);
                                  M.call_closure (|
                                    M.get_associated_function (| Ty.path "str", "len", [] |),
                                    [ M.read (| after_decimal |) ]
                                  |)
                                ]
                              |))
                          ]
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let iter := M.copy (| γ |) in
                        M.loop (|
                          ltac:(M.monadic
                            (let _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "core::ops::range::Range")
                                        [ Ty.path "usize" ],
                                      [],
                                      "next",
                                      []
                                    |),
                                    [ iter ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "alloc::string::String",
                                              "push",
                                              []
                                            |),
                                            [ amount_str; Value.UnicodeChar 48 ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::result::Result")
                    [ Ty.path "u64"; Ty.path "core::num::error::ParseIntError" ],
                  "map_err",
                  [
                    Ty.path "solana_program::program_error::ProgramError";
                    Ty.function
                      [ Ty.tuple [ Ty.path "core::num::error::ParseIntError" ] ]
                      (Ty.path "solana_program::program_error::ProgramError")
                  ]
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "str", "parse", [ Ty.path "u64" ] |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::deref::Deref",
                          Ty.path "alloc::string::String",
                          [],
                          "deref",
                          []
                        |),
                        [ amount_str ]
                      |)
                    ]
                  |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (Value.StructTuple
                                    "solana_program::program_error::ProgramError::InvalidArgument"
                                    []))
                            ]
                          |)
                        | _ => M.impossible (||)
                        end))
                ]
              |)
            |)
          |)))
      |)))
  | _, _ => M.impossible
  end.

Definition value_ID : Value.t :=
  M.run
    ltac:(M.monadic
      (M.alloc (|
        M.call_closure (|
          M.get_associated_function (|
            Ty.path "solana_program::pubkey::Pubkey",
            "new_from_array",
            []
          |),
          [
            Value.Array
              [
                Value.Integer 6;
                Value.Integer 221;
                Value.Integer 246;
                Value.Integer 225;
                Value.Integer 238;
                Value.Integer 117;
                Value.Integer 143;
                Value.Integer 222;
                Value.Integer 24;
                Value.Integer 66;
                Value.Integer 93;
                Value.Integer 188;
                Value.Integer 228;
                Value.Integer 108;
                Value.Integer 205;
                Value.Integer 218;
                Value.Integer 182;
                Value.Integer 26;
                Value.Integer 252;
                Value.Integer 77;
                Value.Integer 131;
                Value.Integer 185;
                Value.Integer 13;
                Value.Integer 39;
                Value.Integer 254;
                Value.Integer 189;
                Value.Integer 249;
                Value.Integer 40;
                Value.Integer 216;
                Value.Integer 161;
                Value.Integer 139;
                Value.Integer 252
              ]
          ]
        |)
      |))).

(* solana_program::declare_id!("TokenzQdBNbLqP5VEhdkAS6EPFLC1PHnBqCXEpPxuEb") *)
Definition check_id (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ id ] =>
    ltac:(M.monadic
      (let id := M.alloc (| id |) in
      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",
          []
        |),
        [ id; M.alloc (| M.get_constant (| "spl_token_2022::ID" |) |) ]
      |)))
  | _, _ => M.impossible
  end.

(* solana_program::declare_id!("TokenzQdBNbLqP5VEhdkAS6EPFLC1PHnBqCXEpPxuEb") *)
Definition id (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [] => ltac:(M.monadic (M.read (| M.get_constant (| "spl_token_2022::ID" |) |)))
  | _, _ => M.impossible
  end.

(*
pub fn check_program_account(spl_token_program_id: &Pubkey) -> ProgramResult {
    if spl_token_program_id != &id() {
        return Err(ProgramError::IncorrectProgramId);
    }
    Ok(())
}
*)
Definition check_program_account (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ spl_token_program_id ] =>
    ltac:(M.monadic
      (let spl_token_program_id := M.alloc (| spl_token_program_id |) in
      M.catch_return (|
        ltac:(M.monadic
          (M.read (|
            let _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            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" ]
                                ],
                                "ne",
                                []
                              |),
                              [
                                spl_token_program_id;
                                M.alloc (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (| "spl_token_2022::id", [] |),
                                      []
                                    |)
                                  |)
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.read (|
                            M.return_ (|
                              Value.StructTuple
                                "core::result::Result::Err"
                                [
                                  Value.StructTuple
                                    "solana_program::program_error::ProgramError::IncorrectProgramId"
                                    []
                                ]
                            |)
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
          |)))
      |)))
  | _, _ => M.impossible
  end.

(*
pub fn check_spl_token_program_account(spl_token_program_id: &Pubkey) -> ProgramResult {
    if spl_token_program_id != &id() && spl_token_program_id != &spl_token::id() {
        return Err(ProgramError::IncorrectProgramId);
    }
    Ok(())
}
*)
Definition check_spl_token_program_account (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ spl_token_program_id ] =>
    ltac:(M.monadic
      (let spl_token_program_id := M.alloc (| spl_token_program_id |) in
      M.catch_return (|
        ltac:(M.monadic
          (M.read (|
            let _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            LogicalOp.and (|
                              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" ]
                                  ],
                                  "ne",
                                  []
                                |),
                                [
                                  spl_token_program_id;
                                  M.alloc (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (| "spl_token_2022::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" ]
                                    ],
                                    "ne",
                                    []
                                  |),
                                  [
                                    spl_token_program_id;
                                    M.alloc (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_function (| "spl_token::id", [] |),
                                          []
                                        |)
                                      |)
                                    |)
                                  ]
                                |)))
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.read (|
                            M.return_ (|
                              Value.StructTuple
                                "core::result::Result::Err"
                                [
                                  Value.StructTuple
                                    "solana_program::program_error::ProgramError::IncorrectProgramId"
                                    []
                                ]
                            |)
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
          |)))
      |)))
  | _, _ => M.impossible
  end.

(*
pub fn check_zk_token_proof_program_account(zk_token_proof_program_id: &Pubkey) -> ProgramResult {
    if zk_token_proof_program_id != &solana_zk_token_sdk::zk_token_proof_program::id() {
        return Err(ProgramError::IncorrectProgramId);
    }
    Ok(())
}
*)
Definition check_zk_token_proof_program_account (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ zk_token_proof_program_id ] =>
    ltac:(M.monadic
      (let zk_token_proof_program_id := M.alloc (| zk_token_proof_program_id |) in
      M.catch_return (|
        ltac:(M.monadic
          (M.read (|
            let _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            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" ]
                                ],
                                "ne",
                                []
                              |),
                              [
                                zk_token_proof_program_id;
                                M.alloc (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "solana_zk_token_sdk::zk_token_proof_program::id",
                                        []
                                      |),
                                      []
                                    |)
                                  |)
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.read (|
                            M.return_ (|
                              Value.StructTuple
                                "core::result::Result::Err"
                                [
                                  Value.StructTuple
                                    "solana_program::program_error::ProgramError::IncorrectProgramId"
                                    []
                                ]
                            |)
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
          |)))
      |)))
  | _, _ => M.impossible
  end.

(*
pub fn check_system_program_account(system_program_id: &Pubkey) -> ProgramResult {
    if system_program_id != &system_program::id() {
        return Err(ProgramError::IncorrectProgramId);
    }
    Ok(())
}
*)
Definition check_system_program_account (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ system_program_id ] =>
    ltac:(M.monadic
      (let system_program_id := M.alloc (| system_program_id |) in
      M.catch_return (|
        ltac:(M.monadic
          (M.read (|
            let _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            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" ]
                                ],
                                "ne",
                                []
                              |),
                              [
                                system_program_id;
                                M.alloc (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (| "solana_program::system_program::id", [] |),
                                      []
                                    |)
                                  |)
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.read (|
                            M.return_ (|
                              Value.StructTuple
                                "core::result::Result::Err"
                                [
                                  Value.StructTuple
                                    "solana_program::program_error::ProgramError::IncorrectProgramId"
                                    []
                                ]
                            |)
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
          |)))
      |)))
  | _, _ => M.impossible
  end.

(*
pub fn cmp_pubkeys(a: &Pubkey, b: &Pubkey) -> bool {
    sol_memcmp(a.as_ref(), b.as_ref(), PUBKEY_BYTES) == 0
}
*)
Definition cmp_pubkeys (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ a; b ] =>
    ltac:(M.monadic
      (let a := M.alloc (| a |) in
      let b := M.alloc (| b |) in
      BinOp.Pure.eq
        (M.call_closure (|
          M.get_function (| "solana_program::program_memory::sol_memcmp", [] |),
          [
            M.call_closure (|
              M.get_trait_method (|
                "core::convert::AsRef",
                Ty.path "solana_program::pubkey::Pubkey",
                [ Ty.apply (Ty.path "slice") [ Ty.path "u8" ] ],
                "as_ref",
                []
              |),
              [ M.read (| a |) ]
            |);
            M.call_closure (|
              M.get_trait_method (|
                "core::convert::AsRef",
                Ty.path "solana_program::pubkey::Pubkey",
                [ Ty.apply (Ty.path "slice") [ Ty.path "u8" ] ],
                "as_ref",
                []
              |),
              [ M.read (| b |) ]
            |);
            M.read (| M.get_constant (| "solana_program::pubkey::PUBKEY_BYTES" |) |)
          ]
        |))
        (Value.Integer 0)))
  | _, _ => M.impossible
  end.
