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

(* StructRecord
  {
    name := "Mapping";
    const_params := [];
    ty_params := [ "K"; "V" ];
    fields :=
      [
        ("_key", Ty.apply (Ty.path "core::marker::PhantomData") [] [ K ]);
        ("_value", Ty.apply (Ty.path "core::marker::PhantomData") [] [ V ])
      ];
  } *)

Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_erc1155_Mapping_K_V.
  Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc1155::Mapping") [] [ K; V ].
  
  (* Default *)
  Definition default (K V : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self K V in
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "erc1155::Mapping"
          [
            ("_key",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply (Ty.path "core::marker::PhantomData") [] [ K ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("_value",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply (Ty.path "core::marker::PhantomData") [] [ V ],
                  [],
                  "default",
                  []
                |),
                []
              |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    forall (K V : Ty.t),
    M.IsTraitInstance
      "core::default::Default"
      (Self K V)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method (default K V)) ].
End Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_erc1155_Mapping_K_V.

Module Impl_erc1155_Mapping_K_V.
  Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc1155::Mapping") [] [ K; V ].
  
  (*
      fn contains(&self, _key: &K) -> bool {
          unimplemented!()
      }
  *)
  Parameter contains : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_contains :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "contains" (contains K V).
  
  (*
      fn get(&self, _key: &K) -> Option<V> {
          unimplemented!()
      }
  *)
  Parameter get : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_get :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "get" (get K V).
  
  (*
      fn insert(&mut self, _key: K, _value: V) -> Option<u32> {
          unimplemented!()
      }
  *)
  Parameter insert : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_insert :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "insert" (insert K V).
  
  (*
      fn remove(&self, _key: K) {
          unimplemented!()
      }
  *)
  Parameter remove : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_remove :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "remove" (remove K V).
  
  (*
      fn size(&self, _key: K) -> Option<u32> {
          unimplemented!()
      }
  *)
  Parameter size : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_size :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "size" (size K V).
  
  (*
      fn take(&self, _key: K) -> Option<V> {
          unimplemented!()
      }
  *)
  Parameter take : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_take :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "take" (take K V).
End Impl_erc1155_Mapping_K_V.

(* StructTuple
  {
    name := "AccountId";
    const_params := [];
    ty_params := [];
    fields := [ Ty.path "u128" ];
  } *)

Module Impl_core_default_Default_for_erc1155_AccountId.
  Definition Self : Ty.t := Ty.path "erc1155::AccountId".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructTuple
          "erc1155::AccountId"
          [
            M.call_closure (|
              M.get_trait_method (| "core::default::Default", Ty.path "u128", [], "default", [] |),
              []
            |)
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::default::Default"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method default) ].
End Impl_core_default_Default_for_erc1155_AccountId.

Module Impl_core_clone_Clone_for_erc1155_AccountId.
  Definition Self : Ty.t := Ty.path "erc1155::AccountId".
  
  (* Clone *)
  Definition clone (ε : list Value.t) (τ : 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 "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::clone::Clone"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("clone", InstanceField.Method clone) ].
End Impl_core_clone_Clone_for_erc1155_AccountId.

Module Impl_core_marker_Copy_for_erc1155_AccountId.
  Definition Self : Ty.t := Ty.path "erc1155::AccountId".
  
  Axiom Implements :
    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
End Impl_core_marker_Copy_for_erc1155_AccountId.

Module Impl_core_marker_StructuralPartialEq_for_erc1155_AccountId.
  Definition Self : Ty.t := Ty.path "erc1155::AccountId".
  
  Axiom Implements :
    M.IsTraitInstance
      "core::marker::StructuralPartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_core_marker_StructuralPartialEq_for_erc1155_AccountId.

Module Impl_core_cmp_PartialEq_for_erc1155_AccountId.
  Definition Self : Ty.t := Ty.path "erc1155::AccountId".
  
  (* PartialEq *)
  Definition eq (ε : list Value.t) (τ : 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
        BinOp.eq (|
          M.read (|
            M.SubPointer.get_struct_tuple_field (| M.read (| self |), "erc1155::AccountId", 0 |)
          |),
          M.read (|
            M.SubPointer.get_struct_tuple_field (| M.read (| other |), "erc1155::AccountId", 0 |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("eq", InstanceField.Method eq) ].
End Impl_core_cmp_PartialEq_for_erc1155_AccountId.

Module Impl_core_convert_From_array_Usize_32_u8_for_erc1155_AccountId.
  Definition Self : Ty.t := Ty.path "erc1155::AccountId".
  
  (*
      fn from(_v: [u8; 32]) -> Self {
          unimplemented!()
      }
  *)
  Parameter from : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::convert::From"
      Self
      (* Trait polymorphic types *)
      [ (* T *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ] ]
      (* Instance *) [ ("from", InstanceField.Method from) ].
End Impl_core_convert_From_array_Usize_32_u8_for_erc1155_AccountId.

Axiom Balance : (Ty.path "erc1155::Balance") = (Ty.path "u128").

(* StructRecord
  {
    name := "Env";
    const_params := [];
    ty_params := [];
    fields := [ ("caller", Ty.path "erc1155::AccountId") ];
  } *)

(*
fn zero_address() -> AccountId {
    [0u8; 32].into()
}
*)
Definition zero_address (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.call_closure (|
        M.get_trait_method (|
          "core::convert::Into",
          Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ],
          [ Ty.path "erc1155::AccountId" ],
          "into",
          []
        |),
        [ repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) ]
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_zero_address : M.IsFunction "erc1155::zero_address" zero_address.

Definition value_ON_ERC_1155_RECEIVED_SELECTOR : Value.t :=
  M.run
    ltac:(M.monadic
      (M.alloc (|
        Value.Array
          [
            Value.Integer IntegerKind.U8 242;
            Value.Integer IntegerKind.U8 58;
            Value.Integer IntegerKind.U8 110;
            Value.Integer IntegerKind.U8 97
          ]
      |))).

Definition _ON_ERC_1155_BATCH_RECEIVED_SELECTOR : Value.t :=
  M.run
    ltac:(M.monadic
      (M.alloc (|
        Value.Array
          [
            Value.Integer IntegerKind.U8 188;
            Value.Integer IntegerKind.U8 25;
            Value.Integer IntegerKind.U8 124;
            Value.Integer IntegerKind.U8 129
          ]
      |))).

Axiom TokenId : (Ty.path "erc1155::TokenId") = (Ty.path "u128").

(*
Enum Error
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "UnexistentToken";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "ZeroAddressTransfer";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "NotApproved";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "InsufficientBalance";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "SelfApproval";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "BatchTransferMismatch";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

Module Impl_core_marker_StructuralPartialEq_for_erc1155_Error.
  Definition Self : Ty.t := Ty.path "erc1155::Error".
  
  Axiom Implements :
    M.IsTraitInstance
      "core::marker::StructuralPartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_core_marker_StructuralPartialEq_for_erc1155_Error.

Module Impl_core_cmp_PartialEq_for_erc1155_Error.
  Definition Self : Ty.t := Ty.path "erc1155::Error".
  
  (* PartialEq *)
  Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        M.read (|
          let~ __self_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "erc1155::Error" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "erc1155::Error" ]
                |),
                [ M.read (| other |) ]
              |)
            |) in
          M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("eq", InstanceField.Method eq) ].
End Impl_core_cmp_PartialEq_for_erc1155_Error.

Module Impl_core_cmp_Eq_for_erc1155_Error.
  Definition Self : Ty.t := Ty.path "erc1155::Error".
  
  (* Eq *)
  Definition assert_receiver_is_total_eq
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        Value.Tuple []))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::Eq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
End Impl_core_cmp_Eq_for_erc1155_Error.

Axiom Result :
  forall (T : Ty.t),
  (Ty.apply (Ty.path "erc1155::Result") [] [ T ]) =
    (Ty.apply (Ty.path "core::result::Result") [] [ T; Ty.path "erc1155::Error" ]).

(* Trait *)
(* Empty module 'Erc1155' *)

(* Trait *)
(* Empty module 'Erc1155TokenReceiver' *)

Axiom Owner : (Ty.path "erc1155::Owner") = (Ty.path "erc1155::AccountId").

Axiom Operator : (Ty.path "erc1155::Operator") = (Ty.path "erc1155::AccountId").

(* StructRecord
  {
    name := "TransferSingle";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("operator", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "erc1155::AccountId" ]);
        ("from", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "erc1155::AccountId" ]);
        ("to", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "erc1155::AccountId" ]);
        ("token_id", Ty.path "u128");
        ("value", Ty.path "u128")
      ];
  } *)

(* StructRecord
  {
    name := "ApprovalForAll";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("owner", Ty.path "erc1155::AccountId");
        ("operator", Ty.path "erc1155::AccountId");
        ("approved", Ty.path "bool")
      ];
  } *)

(* StructRecord
  {
    name := "Uri";
    const_params := [];
    ty_params := [];
    fields := [ ("value", Ty.path "alloc::string::String"); ("token_id", Ty.path "u128") ];
  } *)

(*
Enum Event
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "TransferSingle";
        item := StructTuple [ Ty.path "erc1155::TransferSingle" ];
        discriminant := None;
      };
      {
        name := "ApprovalForAll";
        item := StructTuple [ Ty.path "erc1155::ApprovalForAll" ];
        discriminant := None;
      };
      {
        name := "Uri";
        item := StructTuple [ Ty.path "erc1155::Uri" ];
        discriminant := None;
      }
    ];
}
*)

Module Impl_erc1155_Env.
  Definition Self : Ty.t := Ty.path "erc1155::Env".
  
  (*
      fn caller(&self) -> AccountId {
          self.caller
      }
  *)
  Definition caller (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          M.SubPointer.get_struct_record_field (| M.read (| self |), "erc1155::Env", "caller" |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_caller : M.IsAssociatedFunction Self "caller" caller.
  
  (*
      fn emit_event(&self, _event: Event) {
          unimplemented!()
      }
  *)
  Parameter emit_event : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_emit_event : M.IsAssociatedFunction Self "emit_event" emit_event.
End Impl_erc1155_Env.

(* StructRecord
  {
    name := "Contract";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("balances",
          Ty.apply
            (Ty.path "erc1155::Mapping")
            []
            [ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "u128" ]; Ty.path "u128" ]);
        ("approvals",
          Ty.apply
            (Ty.path "erc1155::Mapping")
            []
            [ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "erc1155::AccountId" ]; Ty.tuple []
            ]);
        ("token_id_nonce", Ty.path "u128")
      ];
  } *)

Module Impl_core_default_Default_for_erc1155_Contract.
  Definition Self : Ty.t := Ty.path "erc1155::Contract".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "erc1155::Contract"
          [
            ("balances",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "erc1155::Mapping")
                    []
                    [ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "u128" ]; Ty.path "u128" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("approvals",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "erc1155::Mapping")
                    []
                    [
                      Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "erc1155::AccountId" ];
                      Ty.tuple []
                    ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("token_id_nonce",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "u128",
                  [],
                  "default",
                  []
                |),
                []
              |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::default::Default"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method default) ].
End Impl_core_default_Default_for_erc1155_Contract.

Module Impl_erc1155_Contract.
  Definition Self : Ty.t := Ty.path "erc1155::Contract".
  
  (*
      fn init_env() -> Env {
          unimplemented!()
      }
  *)
  Parameter init_env : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_init_env : M.IsAssociatedFunction Self "init_env" init_env.
  
  (*
      fn env(&self) -> Env {
          Self::init_env()
      }
  *)
  Definition env (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.call_closure (|
          M.get_associated_function (| Ty.path "erc1155::Contract", "init_env", [] |),
          []
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_env : M.IsAssociatedFunction Self "env" env.
  
  (*
      pub fn new() -> Self {
          Default::default()
      }
  *)
  Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_trait_method (|
            "core::default::Default",
            Ty.path "erc1155::Contract",
            [],
            "default",
            []
          |),
          []
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  
  (*
      pub fn create(&mut self, value: Balance) -> TokenId {
          let caller = self.env().caller();
  
          // Given that TokenId is a `u128` the likelihood of this overflowing is pretty
          // slim.
          self.token_id_nonce += 1;
          self.balances.insert((caller, self.token_id_nonce), value);
  
          // Emit transfer event but with mint semantics
          self.env().emit_event(Event::TransferSingle(TransferSingle {
              operator: Some(caller),
              from: None,
              to: if value == 0 { None } else { Some(caller) },
              token_id: self.token_id_nonce,
              value,
          }));
  
          self.token_id_nonce
      }
  *)
  Definition create (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; value ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let value := M.alloc (| value |) in
        M.read (|
          let~ caller :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "erc1155::Env", "caller", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "erc1155::Contract", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |)
            |) in
          let~ _ :=
            let β :=
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "erc1155::Contract",
                "token_id_nonce"
              |) in
            M.write (|
              β,
              BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.U128 1 |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "erc1155::Mapping")
                    []
                    [ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "u128" ]; Ty.path "u128" ],
                  "insert",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "erc1155::Contract",
                    "balances"
                  |);
                  Value.Tuple
                    [
                      M.read (| caller |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "erc1155::Contract",
                          "token_id_nonce"
                        |)
                      |)
                    ];
                  M.read (| value |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "erc1155::Env", "emit_event", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "erc1155::Contract", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |);
                  Value.StructTuple
                    "erc1155::Event::TransferSingle"
                    [
                      Value.StructRecord
                        "erc1155::TransferSingle"
                        [
                          ("operator",
                            Value.StructTuple "core::option::Option::Some" [ M.read (| caller |) ]);
                          ("from", Value.StructTuple "core::option::Option::None" []);
                          ("to",
                            M.read (|
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            BinOp.eq (|
                                              M.read (| value |),
                                              Value.Integer IntegerKind.U128 0
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        Value.StructTuple "core::option::Option::None" []
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (M.alloc (|
                                        Value.StructTuple
                                          "core::option::Option::Some"
                                          [ M.read (| caller |) ]
                                      |)))
                                ]
                              |)
                            |));
                          ("token_id",
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "erc1155::Contract",
                                "token_id_nonce"
                              |)
                            |));
                          ("value", M.read (| value |))
                        ]
                    ]
                ]
              |)
            |) in
          M.SubPointer.get_struct_record_field (|
            M.read (| self |),
            "erc1155::Contract",
            "token_id_nonce"
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_create : M.IsAssociatedFunction Self "create" create.
  
  (*
      pub fn mint(&mut self, token_id: TokenId, value: Balance) -> Result<()> {
          ensure!(token_id <= self.token_id_nonce, Error::UnexistentToken);
  
          let caller = self.env().caller();
          self.balances.insert((caller, token_id), value);
  
          // Emit transfer event but with mint semantics
          self.env().emit_event(Event::TransferSingle(TransferSingle {
              operator: Some(caller),
              from: None,
              to: Some(caller),
              token_id,
              value,
          }));
  
          Ok(())
      }
  *)
  Definition mint (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; token_id; value ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let token_id := M.alloc (| token_id |) in
        let value := M.alloc (| value |) 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 (|
                              UnOp.not (|
                                BinOp.le (|
                                  M.read (| token_id |),
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "erc1155::Contract",
                                      "token_id_nonce"
                                    |)
                                  |)
                                |)
                              |)
                            |)) 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"
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::Into",
                                        Ty.path "erc1155::Error",
                                        [ Ty.path "erc1155::Error" ],
                                        "into",
                                        []
                                      |),
                                      [ Value.StructTuple "erc1155::Error::UnexistentToken" [] ]
                                    |)
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ caller :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "erc1155::Env", "caller", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "erc1155::Contract", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "erc1155::Mapping")
                        []
                        [ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "u128" ]; Ty.path "u128"
                        ],
                      "insert",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "erc1155::Contract",
                        "balances"
                      |);
                      Value.Tuple [ M.read (| caller |); M.read (| token_id |) ];
                      M.read (| value |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "erc1155::Env", "emit_event", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "erc1155::Contract", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |);
                      Value.StructTuple
                        "erc1155::Event::TransferSingle"
                        [
                          Value.StructRecord
                            "erc1155::TransferSingle"
                            [
                              ("operator",
                                Value.StructTuple
                                  "core::option::Option::Some"
                                  [ M.read (| caller |) ]);
                              ("from", Value.StructTuple "core::option::Option::None" []);
                              ("to",
                                Value.StructTuple
                                  "core::option::Option::Some"
                                  [ M.read (| caller |) ]);
                              ("token_id", M.read (| token_id |));
                              ("value", M.read (| value |))
                            ]
                        ]
                    ]
                  |)
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_mint : M.IsAssociatedFunction Self "mint" mint.
  
  (*
      fn perform_transfer(
          &mut self,
          from: AccountId,
          to: AccountId,
          token_id: TokenId,
          value: Balance,
      ) {
          let mut sender_balance = self
              .balances
              .get(&(from, token_id))
              .expect("Caller should have ensured that `from` holds `token_id`.");
          sender_balance -= value;
          self.balances.insert((from, token_id), sender_balance);
  
          let mut recipient_balance = self.balances.get(&(to, token_id)).unwrap_or(0 as u128);
          recipient_balance += value;
          self.balances.insert((to, token_id), recipient_balance);
  
          let caller = self.env().caller();
          self.env().emit_event(Event::TransferSingle(TransferSingle {
              operator: Some(caller),
              from: Some(from),
              to: Some(to),
              token_id,
              value,
          }));
      }
  *)
  Definition perform_transfer (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; from; to; token_id; value ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let from := M.alloc (| from |) in
        let to := M.alloc (| to |) in
        let token_id := M.alloc (| token_id |) in
        let value := M.alloc (| value |) in
        M.read (|
          let~ sender_balance :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u128" ],
                  "expect",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "erc1155::Mapping")
                        []
                        [ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "u128" ]; Ty.path "u128"
                        ],
                      "get",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "erc1155::Contract",
                        "balances"
                      |);
                      M.alloc (| Value.Tuple [ M.read (| from |); M.read (| token_id |) ] |)
                    ]
                  |);
                  M.read (|
                    Value.String "Caller should have ensured that `from` holds `token_id`."
                  |)
                ]
              |)
            |) in
          let~ _ :=
            let β := sender_balance in
            M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| value |) |) |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "erc1155::Mapping")
                    []
                    [ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "u128" ]; Ty.path "u128" ],
                  "insert",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "erc1155::Contract",
                    "balances"
                  |);
                  Value.Tuple [ M.read (| from |); M.read (| token_id |) ];
                  M.read (| sender_balance |)
                ]
              |)
            |) in
          let~ recipient_balance :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u128" ],
                  "unwrap_or",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "erc1155::Mapping")
                        []
                        [ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "u128" ]; Ty.path "u128"
                        ],
                      "get",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "erc1155::Contract",
                        "balances"
                      |);
                      M.alloc (| Value.Tuple [ M.read (| to |); M.read (| token_id |) ] |)
                    ]
                  |);
                  M.read (| M.use (M.alloc (| Value.Integer IntegerKind.U128 0 |)) |)
                ]
              |)
            |) in
          let~ _ :=
            let β := recipient_balance in
            M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| value |) |) |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "erc1155::Mapping")
                    []
                    [ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "u128" ]; Ty.path "u128" ],
                  "insert",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "erc1155::Contract",
                    "balances"
                  |);
                  Value.Tuple [ M.read (| to |); M.read (| token_id |) ];
                  M.read (| recipient_balance |)
                ]
              |)
            |) in
          let~ caller :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "erc1155::Env", "caller", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "erc1155::Contract", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "erc1155::Env", "emit_event", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "erc1155::Contract", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |);
                  Value.StructTuple
                    "erc1155::Event::TransferSingle"
                    [
                      Value.StructRecord
                        "erc1155::TransferSingle"
                        [
                          ("operator",
                            Value.StructTuple "core::option::Option::Some" [ M.read (| caller |) ]);
                          ("from",
                            Value.StructTuple "core::option::Option::Some" [ M.read (| from |) ]);
                          ("to",
                            Value.StructTuple "core::option::Option::Some" [ M.read (| to |) ]);
                          ("token_id", M.read (| token_id |));
                          ("value", M.read (| value |))
                        ]
                    ]
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_perform_transfer :
    M.IsAssociatedFunction Self "perform_transfer" perform_transfer.
  
  (*
      fn transfer_acceptance_check(
          &mut self,
          caller: AccountId,
          from: AccountId,
          to: AccountId,
          token_id: TokenId,
          value: Balance,
          data: Vec<u8>,
      ) {
          // This is disabled during tests due to the use of `invoke_contract()` not
          // being supported (tests end up panicking).
          #[cfg(not(test))]
          {
              use ink::env::call::{build_call, ExecutionInput, Selector};
  
              // If our recipient is a smart contract we need to see if they accept or
              // reject this transfer. If they reject it we need to revert the call.
              let result = build_call::<Environment>()
                  .call(to)
                  .gas_limit(5000)
                  .exec_input(
                      ExecutionInput::new(Selector::new(ON_ERC_1155_RECEIVED_SELECTOR))
                          .push_arg(caller)
                          .push_arg(from)
                          .push_arg(token_id)
                          .push_arg(value)
                          .push_arg(data),
                  )
                  .returns::<Vec<u8>>()
                  .params()
                  .try_invoke();
  
              match result {
                  Ok(v) => {
                      ink::env::debug_println!(
                          "Received return value \"{:?}\" from contract {:?}",
                          v.clone()
                              .expect("Call should be valid, don't expect a `LangError`."),
                          from
                      );
                      assert_eq!(
                          v.clone()
                              .expect("Call should be valid, don't expect a `LangError`."),
                          &ON_ERC_1155_RECEIVED_SELECTOR[..],
                          "The recipient contract at {to:?} does not accept token transfers.\n
                              Expected: {ON_ERC_1155_RECEIVED_SELECTOR:?}, Got {v:?}"
                      )
                  }
                  Err(e) => {
                      match e {
                          ink::env::Error::CodeNotFound | ink::env::Error::NotCallable => {
                              // Our recipient wasn't a smart contract, so there's
                              // nothing more for
                              // us to do
                              ink::env::debug_println!(
                                  "Recipient at {:?} from is not a smart contract ({:?})",
                                  from,
                                  e
                              );
                          }
                          _ => {
                              // We got some sort of error from the call to our
                              // recipient smart
                              // contract, and as such we must revert this call
                              panic!("Got error \"{e:?}\" while trying to call {from:?}")
                          }
                      }
                  }
              }
          }
      }
  *)
  Definition transfer_acceptance_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; caller; from; to; token_id; value; data ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let caller := M.alloc (| caller |) in
        let from := M.alloc (| from |) in
        let to := M.alloc (| to |) in
        let token_id := M.alloc (| token_id |) in
        let value := M.alloc (| value |) in
        let data := M.alloc (| data |) in
        Value.Tuple []))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_transfer_acceptance_check :
    M.IsAssociatedFunction Self "transfer_acceptance_check" transfer_acceptance_check.
End Impl_erc1155_Contract.

Module Impl_erc1155_Erc1155_for_erc1155_Contract.
  Definition Self : Ty.t := Ty.path "erc1155::Contract".
  
  (*
      fn is_approved_for_all(&self, owner: AccountId, operator: AccountId) -> bool {
          self.approvals.contains(&(owner, operator))
      }
  *)
  Definition is_approved_for_all (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owner; operator ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owner := M.alloc (| owner |) in
        let operator := M.alloc (| operator |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply
              (Ty.path "erc1155::Mapping")
              []
              [ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "erc1155::AccountId" ]; Ty.tuple []
              ],
            "contains",
            []
          |),
          [
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "erc1155::Contract",
              "approvals"
            |);
            M.alloc (| Value.Tuple [ M.read (| owner |); M.read (| operator |) ] |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
      fn balance_of(&self, owner: AccountId, token_id: TokenId) -> Balance {
          self.balances.get(&(owner, token_id)).unwrap_or(0 as u128)
      }
  *)
  Definition balance_of (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owner; token_id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owner := M.alloc (| owner |) in
        let token_id := M.alloc (| token_id |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u128" ],
            "unwrap_or",
            []
          |),
          [
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "erc1155::Mapping")
                  []
                  [ Ty.tuple [ Ty.path "erc1155::AccountId"; Ty.path "u128" ]; Ty.path "u128" ],
                "get",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "erc1155::Contract",
                  "balances"
                |);
                M.alloc (| Value.Tuple [ M.read (| owner |); M.read (| token_id |) ] |)
              ]
            |);
            M.read (| M.use (M.alloc (| Value.Integer IntegerKind.U128 0 |)) |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
      fn safe_transfer_from(
          &mut self,
          from: AccountId,
          to: AccountId,
          token_id: TokenId,
          value: Balance,
          data: Vec<u8>,
      ) -> Result<()> {
          let caller = self.env().caller();
          if caller != from {
              ensure!(self.is_approved_for_all(from, caller), Error::NotApproved);
          }
  
          ensure!(to != zero_address(), Error::ZeroAddressTransfer);
  
          let balance = self.balance_of(from, token_id);
          ensure!(balance >= value, Error::InsufficientBalance);
  
          self.perform_transfer(from, to, token_id, value);
          self.transfer_acceptance_check(caller, from, to, token_id, value, data);
  
          Ok(())
      }
  *)
  Definition safe_transfer_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; from; to; token_id; value; data ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let from := M.alloc (| from |) in
        let to := M.alloc (| to |) in
        let token_id := M.alloc (| token_id |) in
        let value := M.alloc (| value |) in
        let data := M.alloc (| data |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ caller :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "erc1155::Env", "caller", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "erc1155::Contract", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |)
                |) in
              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.path "erc1155::AccountId",
                                  [ Ty.path "erc1155::AccountId" ],
                                  "ne",
                                  []
                                |),
                                [ caller; from ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        UnOp.not (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "erc1155::Erc1155",
                                              Ty.path "erc1155::Contract",
                                              [],
                                              "is_approved_for_all",
                                              []
                                            |),
                                            [
                                              M.read (| self |);
                                              M.read (| from |);
                                              M.read (| caller |)
                                            ]
                                          |)
                                        |)
                                      |)) 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"
                                            [
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::convert::Into",
                                                  Ty.path "erc1155::Error",
                                                  [ Ty.path "erc1155::Error" ],
                                                  "into",
                                                  []
                                                |),
                                                [ Value.StructTuple "erc1155::Error::NotApproved" []
                                                ]
                                              |)
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialEq",
                                    Ty.path "erc1155::AccountId",
                                    [ Ty.path "erc1155::AccountId" ],
                                    "ne",
                                    []
                                  |),
                                  [
                                    to;
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (| "erc1155::zero_address", [] |),
                                        []
                                      |)
                                    |)
                                  ]
                                |)
                              |)
                            |)) 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"
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::Into",
                                        Ty.path "erc1155::Error",
                                        [ Ty.path "erc1155::Error" ],
                                        "into",
                                        []
                                      |),
                                      [ Value.StructTuple "erc1155::Error::ZeroAddressTransfer" [] ]
                                    |)
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ balance :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "erc1155::Erc1155",
                      Ty.path "erc1155::Contract",
                      [],
                      "balance_of",
                      []
                    |),
                    [ M.read (| self |); M.read (| from |); M.read (| token_id |) ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (| BinOp.ge (| M.read (| balance |), M.read (| value |) |) |)
                            |)) 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"
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::Into",
                                        Ty.path "erc1155::Error",
                                        [ Ty.path "erc1155::Error" ],
                                        "into",
                                        []
                                      |),
                                      [ Value.StructTuple "erc1155::Error::InsufficientBalance" [] ]
                                    |)
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "erc1155::Contract",
                      "perform_transfer",
                      []
                    |),
                    [
                      M.read (| self |);
                      M.read (| from |);
                      M.read (| to |);
                      M.read (| token_id |);
                      M.read (| value |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "erc1155::Contract",
                      "transfer_acceptance_check",
                      []
                    |),
                    [
                      M.read (| self |);
                      M.read (| caller |);
                      M.read (| from |);
                      M.read (| to |);
                      M.read (| token_id |);
                      M.read (| value |);
                      M.read (| data |)
                    ]
                  |)
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
      fn safe_batch_transfer_from(
          &mut self,
          from: AccountId,
          to: AccountId,
          token_ids: Vec<TokenId>,
          values: Vec<Balance>,
          data: Vec<u8>,
      ) -> Result<()> {
          let caller = self.env().caller();
          if caller != from {
              ensure!(self.is_approved_for_all(from, caller), Error::NotApproved);
          }
  
          ensure!(to != zero_address(), Error::ZeroAddressTransfer);
          ensure!(!token_ids.is_empty(), Error::BatchTransferMismatch);
          ensure!(
              token_ids.len() == values.len(),
              Error::BatchTransferMismatch,
          );
  
          let transfers = token_ids.iter().zip(values.iter());
          for (&id, &v) in transfers.clone() {
              let balance = self.balance_of(from, id);
              ensure!(balance >= v, Error::InsufficientBalance);
          }
  
          for (&id, &v) in transfers {
              self.perform_transfer(from, to, id, v);
          }
  
          // Can use the any token ID/value here, we really just care about knowing if
          // `to` is a smart contract which accepts transfers
          self.transfer_acceptance_check(caller, from, to, token_ids[0], values[0], data);
  
          Ok(())
      }
  *)
  Definition safe_batch_transfer_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; from; to; token_ids; values; data ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let from := M.alloc (| from |) in
        let to := M.alloc (| to |) in
        let token_ids := M.alloc (| token_ids |) in
        let values := M.alloc (| values |) in
        let data := M.alloc (| data |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ caller :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "erc1155::Env", "caller", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "erc1155::Contract", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |)
                |) in
              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.path "erc1155::AccountId",
                                  [ Ty.path "erc1155::AccountId" ],
                                  "ne",
                                  []
                                |),
                                [ caller; from ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        UnOp.not (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "erc1155::Erc1155",
                                              Ty.path "erc1155::Contract",
                                              [],
                                              "is_approved_for_all",
                                              []
                                            |),
                                            [
                                              M.read (| self |);
                                              M.read (| from |);
                                              M.read (| caller |)
                                            ]
                                          |)
                                        |)
                                      |)) 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"
                                            [
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::convert::Into",
                                                  Ty.path "erc1155::Error",
                                                  [ Ty.path "erc1155::Error" ],
                                                  "into",
                                                  []
                                                |),
                                                [ Value.StructTuple "erc1155::Error::NotApproved" []
                                                ]
                                              |)
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialEq",
                                    Ty.path "erc1155::AccountId",
                                    [ Ty.path "erc1155::AccountId" ],
                                    "ne",
                                    []
                                  |),
                                  [
                                    to;
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (| "erc1155::zero_address", [] |),
                                        []
                                      |)
                                    |)
                                  ]
                                |)
                              |)
                            |)) 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"
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::Into",
                                        Ty.path "erc1155::Error",
                                        [ Ty.path "erc1155::Error" ],
                                        "into",
                                        []
                                      |),
                                      [ Value.StructTuple "erc1155::Error::ZeroAddressTransfer" [] ]
                                    |)
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                UnOp.not (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [ Ty.path "u128"; Ty.path "alloc::alloc::Global" ],
                                      "is_empty",
                                      []
                                    |),
                                    [ token_ids ]
                                  |)
                                |)
                              |)
                            |)) 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"
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::Into",
                                        Ty.path "erc1155::Error",
                                        [ Ty.path "erc1155::Error" ],
                                        "into",
                                        []
                                      |),
                                      [ Value.StructTuple "erc1155::Error::BatchTransferMismatch" []
                                      ]
                                    |)
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                BinOp.eq (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [ Ty.path "u128"; Ty.path "alloc::alloc::Global" ],
                                      "len",
                                      []
                                    |),
                                    [ token_ids ]
                                  |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [ Ty.path "u128"; Ty.path "alloc::alloc::Global" ],
                                      "len",
                                      []
                                    |),
                                    [ values ]
                                  |)
                                |)
                              |)
                            |)) 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"
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::Into",
                                        Ty.path "erc1155::Error",
                                        [ Ty.path "erc1155::Error" ],
                                        "into",
                                        []
                                      |),
                                      [ Value.StructTuple "erc1155::Error::BatchTransferMismatch" []
                                      ]
                                    |)
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ transfers :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u128" ],
                      [],
                      "zip",
                      [ Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u128" ] ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u128" ],
                          "iter",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [ Ty.path "u128"; Ty.path "alloc::alloc::Global" ],
                              [],
                              "deref",
                              []
                            |),
                            [ token_ids ]
                          |)
                        ]
                      |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u128" ],
                          "iter",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [ Ty.path "u128"; Ty.path "alloc::alloc::Global" ],
                              [],
                              "deref",
                              []
                            |),
                            [ values ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |) 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::iter::adapters::zip::Zip")
                            []
                            [
                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u128" ];
                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u128" ]
                            ],
                          [],
                          "into_iter",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.apply
                                (Ty.path "core::iter::adapters::zip::Zip")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::slice::iter::Iter")
                                    []
                                    [ Ty.path "u128" ];
                                  Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u128" ]
                                ],
                              [],
                              "clone",
                              []
                            |),
                            [ transfers ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::iter::adapters::zip::Zip")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::slice::iter::Iter")
                                              []
                                              [ Ty.path "u128" ];
                                            Ty.apply
                                              (Ty.path "core::slice::iter::Iter")
                                              []
                                              [ Ty.path "u128" ]
                                          ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ iter ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                        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 γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                        let γ1_0 := M.read (| γ1_0 |) in
                                        let id := M.copy (| γ1_0 |) in
                                        let γ1_1 := M.read (| γ1_1 |) in
                                        let v := M.copy (| γ1_1 |) in
                                        let~ balance :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "erc1155::Erc1155",
                                                Ty.path "erc1155::Contract",
                                                [],
                                                "balance_of",
                                                []
                                              |),
                                              [
                                                M.read (| self |);
                                                M.read (| from |);
                                                M.read (| id |)
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        UnOp.not (|
                                                          BinOp.ge (|
                                                            M.read (| balance |),
                                                            M.read (| v |)
                                                          |)
                                                        |)
                                                      |)) 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"
                                                            [
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::convert::Into",
                                                                  Ty.path "erc1155::Error",
                                                                  [ Ty.path "erc1155::Error" ],
                                                                  "into",
                                                                  []
                                                                |),
                                                                [
                                                                  Value.StructTuple
                                                                    "erc1155::Error::InsufficientBalance"
                                                                    []
                                                                ]
                                                              |)
                                                            ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |)) 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::iter::adapters::zip::Zip")
                            []
                            [
                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u128" ];
                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u128" ]
                            ],
                          [],
                          "into_iter",
                          []
                        |),
                        [ M.read (| transfers |) ]
                      |)
                    |),
                    [
                      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::iter::adapters::zip::Zip")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::slice::iter::Iter")
                                              []
                                              [ Ty.path "u128" ];
                                            Ty.apply
                                              (Ty.path "core::slice::iter::Iter")
                                              []
                                              [ Ty.path "u128" ]
                                          ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ iter ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                        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 γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                        let γ1_0 := M.read (| γ1_0 |) in
                                        let id := M.copy (| γ1_0 |) in
                                        let γ1_1 := M.read (| γ1_1 |) in
                                        let v := M.copy (| γ1_1 |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "erc1155::Contract",
                                                "perform_transfer",
                                                []
                                              |),
                                              [
                                                M.read (| self |);
                                                M.read (| from |);
                                                M.read (| to |);
                                                M.read (| id |);
                                                M.read (| v |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |)) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "erc1155::Contract",
                      "transfer_acceptance_check",
                      []
                    |),
                    [
                      M.read (| self |);
                      M.read (| caller |);
                      M.read (| from |);
                      M.read (| to |);
                      M.read (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::index::Index",
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [ Ty.path "u128"; Ty.path "alloc::alloc::Global" ],
                            [ Ty.path "usize" ],
                            "index",
                            []
                          |),
                          [ token_ids; Value.Integer IntegerKind.Usize 0 ]
                        |)
                      |);
                      M.read (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::index::Index",
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [ Ty.path "u128"; Ty.path "alloc::alloc::Global" ],
                            [ Ty.path "usize" ],
                            "index",
                            []
                          |),
                          [ values; Value.Integer IntegerKind.Usize 0 ]
                        |)
                      |);
                      M.read (| data |)
                    ]
                  |)
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
      fn balance_of_batch(&self, owners: Vec<AccountId>, token_ids: Vec<TokenId>) -> Vec<Balance> {
          let mut output = Vec::new();
          for o in &owners {
              for t in &token_ids {
                  let amount = self.balance_of( *o, *t);
                  output.push(amount);
              }
          }
          output
      }
  *)
  Definition balance_of_batch (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owners; token_ids ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owners := M.alloc (| owners |) in
        let token_ids := M.alloc (| token_ids |) in
        M.read (|
          let~ output :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u128"; Ty.path "alloc::alloc::Global" ],
                  "new",
                  []
                |),
                []
              |)
            |) 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 "&")
                        []
                        [
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [ Ty.path "erc1155::AccountId"; Ty.path "alloc::alloc::Global" ]
                        ],
                      [],
                      "into_iter",
                      []
                    |),
                    [ owners ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let iter := M.copy (| γ |) in
                      M.loop (|
                        ltac:(M.monadic
                          (let~ _ :=
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::iterator::Iterator",
                                    Ty.apply
                                      (Ty.path "core::slice::iter::Iter")
                                      []
                                      [ Ty.path "erc1155::AccountId" ],
                                    [],
                                    "next",
                                    []
                                  |),
                                  [ iter ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let _ :=
                                      M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                    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 o := M.copy (| γ0_0 |) in
                                    M.use
                                      (M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::collect::IntoIterator",
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::Vec")
                                                    []
                                                    [ Ty.path "u128"; Ty.path "alloc::alloc::Global"
                                                    ]
                                                ],
                                              [],
                                              "into_iter",
                                              []
                                            |),
                                            [ token_ids ]
                                          |)
                                        |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let iter := M.copy (| γ |) in
                                              M.loop (|
                                                ltac:(M.monadic
                                                  (let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::iter::traits::iterator::Iterator",
                                                            Ty.apply
                                                              (Ty.path "core::slice::iter::Iter")
                                                              []
                                                              [ Ty.path "u128" ],
                                                            [],
                                                            "next",
                                                            []
                                                          |),
                                                          [ iter ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let _ :=
                                                              M.is_struct_tuple (|
                                                                γ,
                                                                "core::option::Option::None"
                                                              |) in
                                                            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 t := M.copy (| γ0_0 |) in
                                                            let~ amount :=
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_trait_method (|
                                                                    "erc1155::Erc1155",
                                                                    Ty.path "erc1155::Contract",
                                                                    [],
                                                                    "balance_of",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (| self |);
                                                                    M.read (| M.read (| o |) |);
                                                                    M.read (| M.read (| t |) |)
                                                                  ]
                                                                |)
                                                              |) in
                                                            let~ _ :=
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.apply
                                                                      (Ty.path "alloc::vec::Vec")
                                                                      []
                                                                      [
                                                                        Ty.path "u128";
                                                                        Ty.path
                                                                          "alloc::alloc::Global"
                                                                      ],
                                                                    "push",
                                                                    []
                                                                  |),
                                                                  [ output; M.read (| amount |) ]
                                                                |)
                                                              |) in
                                                            M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)))
                                              |)))
                                        ]
                                      |))))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)))
                      |)))
                ]
              |)) in
          output
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
      fn set_approval_for_all(&mut self, operator: AccountId, approved: bool) -> Result<()> {
          let caller = self.env().caller();
          ensure!(operator != caller, Error::SelfApproval);
  
          if approved {
              self.approvals.insert((caller, operator), ());
          } else {
              self.approvals.remove((caller, operator));
          }
  
          self.env().emit_event(Event::ApprovalForAll(ApprovalForAll {
              owner: caller,
              operator,
              approved,
          }));
  
          Ok(())
      }
  *)
  Definition set_approval_for_all (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; operator; approved ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let operator := M.alloc (| operator |) in
        let approved := M.alloc (| approved |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ caller :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "erc1155::Env", "caller", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "erc1155::Contract", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialEq",
                                    Ty.path "erc1155::AccountId",
                                    [ Ty.path "erc1155::AccountId" ],
                                    "ne",
                                    []
                                  |),
                                  [ operator; caller ]
                                |)
                              |)
                            |)) 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"
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::Into",
                                        Ty.path "erc1155::Error",
                                        [ Ty.path "erc1155::Error" ],
                                        "into",
                                        []
                                      |),
                                      [ Value.StructTuple "erc1155::Error::SelfApproval" [] ]
                                    |)
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.use approved in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "erc1155::Mapping")
                                  []
                                  [
                                    Ty.tuple
                                      [ Ty.path "erc1155::AccountId"; Ty.path "erc1155::AccountId"
                                      ];
                                    Ty.tuple []
                                  ],
                                "insert",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "erc1155::Contract",
                                  "approvals"
                                |);
                                Value.Tuple [ M.read (| caller |); M.read (| operator |) ];
                                Value.Tuple []
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "erc1155::Mapping")
                                  []
                                  [
                                    Ty.tuple
                                      [ Ty.path "erc1155::AccountId"; Ty.path "erc1155::AccountId"
                                      ];
                                    Ty.tuple []
                                  ],
                                "remove",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "erc1155::Contract",
                                  "approvals"
                                |);
                                Value.Tuple [ M.read (| caller |); M.read (| operator |) ]
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "erc1155::Env", "emit_event", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "erc1155::Contract", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |);
                      Value.StructTuple
                        "erc1155::Event::ApprovalForAll"
                        [
                          Value.StructRecord
                            "erc1155::ApprovalForAll"
                            [
                              ("owner", M.read (| caller |));
                              ("operator", M.read (| operator |));
                              ("approved", M.read (| approved |))
                            ]
                        ]
                    ]
                  |)
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "erc1155::Erc1155"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [
        ("is_approved_for_all", InstanceField.Method is_approved_for_all);
        ("balance_of", InstanceField.Method balance_of);
        ("safe_transfer_from", InstanceField.Method safe_transfer_from);
        ("safe_batch_transfer_from", InstanceField.Method safe_batch_transfer_from);
        ("balance_of_batch", InstanceField.Method balance_of_batch);
        ("set_approval_for_all", InstanceField.Method set_approval_for_all)
      ].
End Impl_erc1155_Erc1155_for_erc1155_Contract.

Module Impl_erc1155_Erc1155TokenReceiver_for_erc1155_Contract.
  Definition Self : Ty.t := Ty.path "erc1155::Contract".
  
  (*
      fn on_received(
          &mut self,
          _operator: AccountId,
          _from: AccountId,
          _token_id: TokenId,
          _value: Balance,
          _data: Vec<u8>,
      ) -> Vec<u8> {
          // The ERC-1155 standard dictates that if a contract does not accept token
          // transfers directly to the contract, then the contract must
          // revert.
          //
          // This prevents a user from unintentionally transferring tokens to a smart
          // contract and getting their funds stuck without any sort of
          // recovery mechanism.
          //
          // Note that the choice of whether or not to accept tokens is implementation
          // specific, and we've decided to not accept them in this
          // implementation.
          unimplemented!("This smart contract does not accept token transfer.")
      }
  *)
  Definition on_received (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; _operator; _from; _token_id; _value; _data ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let _operator := M.alloc (| _operator |) in
        let _from := M.alloc (| _from |) in
        let _token_id := M.alloc (| _token_id |) in
        let _value := M.alloc (| _value |) in
        let _data := M.alloc (| _data |) in
        M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic_fmt", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                [
                  M.alloc (|
                    Value.Array
                      [
                        M.read (|
                          Value.String
                            "not implemented: This smart contract does not accept token transfer."
                        |)
                      ]
                  |);
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "core::fmt::rt::Argument", "none", [] |),
                      []
                    |)
                  |)
                ]
              |)
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
      fn on_batch_received(
          &mut self,
          _operator: AccountId,
          _from: AccountId,
          _token_ids: Vec<TokenId>,
          _values: Vec<Balance>,
          _data: Vec<u8>,
      ) -> Vec<u8> {
          // The ERC-1155 standard dictates that if a contract does not accept token
          // transfers directly to the contract, then the contract must
          // revert.
          //
          // This prevents a user from unintentionally transferring tokens to a smart
          // contract and getting their funds stuck without any sort of
          // recovery mechanism.
          //
          // Note that the choice of whether or not to accept tokens is implementation
          // specific, and we've decided to not accept them in this
          // implementation.
          unimplemented!("This smart contract does not accept batch token transfers.")
      }
  *)
  Definition on_batch_received (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; _operator; _from; _token_ids; _values; _data ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let _operator := M.alloc (| _operator |) in
        let _from := M.alloc (| _from |) in
        let _token_ids := M.alloc (| _token_ids |) in
        let _values := M.alloc (| _values |) in
        let _data := M.alloc (| _data |) in
        M.never_to_any (|
          M.call_closure (|
            M.get_function (| "core::panicking::panic_fmt", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                [
                  M.alloc (|
                    Value.Array
                      [
                        M.read (|
                          Value.String
                            "not implemented: This smart contract does not accept batch token transfers."
                        |)
                      ]
                  |);
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "core::fmt::rt::Argument", "none", [] |),
                      []
                    |)
                  |)
                ]
              |)
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "erc1155::Erc1155TokenReceiver"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [
        ("on_received", InstanceField.Method on_received);
        ("on_batch_received", InstanceField.Method on_batch_received)
      ].
End Impl_erc1155_Erc1155TokenReceiver_for_erc1155_Contract.
