(* 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_trait_erc20_Mapping_K_V.
  Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "trait_erc20::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
          "trait_erc20::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_trait_erc20_Mapping_K_V.

Module Impl_trait_erc20_Mapping_K_V.
  Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "trait_erc20::Mapping") [] [ 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) {
          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).
End Impl_trait_erc20_Mapping_K_V.

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

Module Impl_core_default_Default_for_trait_erc20_AccountId.
  Definition Self : Ty.t := Ty.path "trait_erc20::AccountId".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructTuple
          "trait_erc20::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_trait_erc20_AccountId.

Module Impl_core_clone_Clone_for_trait_erc20_AccountId.
  Definition Self : Ty.t := Ty.path "trait_erc20::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_trait_erc20_AccountId.

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

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

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

(*
Enum Error
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "InsufficientBalance";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "InsufficientAllowance";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

Module Impl_core_fmt_Debug_for_trait_erc20_Error.
  Definition Self : Ty.t := Ty.path "trait_erc20::Error".
  
  (* Debug *)
  Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.call_closure (|
          M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
          [
            M.read (| f |);
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "trait_erc20::Error::InsufficientBalance" |) in
                      M.alloc (| M.read (| Value.String "InsufficientBalance" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "trait_erc20::Error::InsufficientAllowance" |) in
                      M.alloc (| M.read (| Value.String "InsufficientAllowance" |) |)))
                ]
              |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::fmt::Debug"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
End Impl_core_fmt_Debug_for_trait_erc20_Error.

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

Module Impl_core_cmp_PartialEq_for_trait_erc20_Error.
  Definition Self : Ty.t := Ty.path "trait_erc20::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 "trait_erc20::Error" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "trait_erc20::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_trait_erc20_Error.

Module Impl_core_cmp_Eq_for_trait_erc20_Error.
  Definition Self : Ty.t := Ty.path "trait_erc20::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_trait_erc20_Error.

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

(* Trait *)
(* Empty module 'BaseErc20' *)

(* StructRecord
  {
    name := "Erc20";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("total_supply", Ty.path "u128");
        ("balances",
          Ty.apply
            (Ty.path "trait_erc20::Mapping")
            []
            [ Ty.path "trait_erc20::AccountId"; Ty.path "u128" ]);
        ("allowances",
          Ty.apply
            (Ty.path "trait_erc20::Mapping")
            []
            [
              Ty.tuple [ Ty.path "trait_erc20::AccountId"; Ty.path "trait_erc20::AccountId" ];
              Ty.path "u128"
            ])
      ];
  } *)

Module Impl_core_default_Default_for_trait_erc20_Erc20.
  Definition Self : Ty.t := Ty.path "trait_erc20::Erc20".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "trait_erc20::Erc20"
          [
            ("total_supply",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "u128",
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("balances",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "trait_erc20::Mapping")
                    []
                    [ Ty.path "trait_erc20::AccountId"; Ty.path "u128" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("allowances",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "trait_erc20::Mapping")
                    []
                    [
                      Ty.tuple
                        [ Ty.path "trait_erc20::AccountId"; Ty.path "trait_erc20::AccountId" ];
                      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_trait_erc20_Erc20.

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

(* StructRecord
  {
    name := "Approval";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("owner", Ty.path "trait_erc20::AccountId");
        ("spender", Ty.path "trait_erc20::AccountId");
        ("value", Ty.path "u128")
      ];
  } *)

(*
Enum Event
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "Transfer";
        item := StructTuple [ Ty.path "trait_erc20::Transfer" ];
        discriminant := None;
      };
      {
        name := "Approval";
        item := StructTuple [ Ty.path "trait_erc20::Approval" ];
        discriminant := None;
      }
    ];
}
*)

Module Impl_trait_erc20_Env.
  Definition Self : Ty.t := Ty.path "trait_erc20::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 |), "trait_erc20::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_trait_erc20_Env.

Module Impl_trait_erc20_Erc20.
  Definition Self : Ty.t := Ty.path "trait_erc20::Erc20".
  
  (*
      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 "trait_erc20::Erc20", "init_env", [] |),
          []
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_env : M.IsAssociatedFunction Self "env" env.
  
  (*
      pub fn new(total_supply: Balance) -> Self {
          let mut balances = Mapping::default();
          let caller = Self::init_env().caller();
          balances.insert(caller, total_supply);
          Self::init_env().emit_event(Event::Transfer(Transfer {
              from: None,
              to: Some(caller),
              value: total_supply,
          }));
          Self {
              total_supply,
              balances,
              allowances: Default::default(),
          }
      }
  *)
  Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ total_supply ] =>
      ltac:(M.monadic
        (let total_supply := M.alloc (| total_supply |) in
        M.read (|
          let~ balances :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "trait_erc20::Mapping")
                    []
                    [ Ty.path "trait_erc20::AccountId"; Ty.path "u128" ],
                  [],
                  "default",
                  []
                |),
                []
              |)
            |) in
          let~ caller :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "trait_erc20::Env", "caller", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "trait_erc20::Erc20", "init_env", [] |),
                      []
                    |)
                  |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "trait_erc20::Mapping")
                    []
                    [ Ty.path "trait_erc20::AccountId"; Ty.path "u128" ],
                  "insert",
                  []
                |),
                [ balances; M.read (| caller |); M.read (| total_supply |) ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "trait_erc20::Env", "emit_event", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "trait_erc20::Erc20", "init_env", [] |),
                      []
                    |)
                  |);
                  Value.StructTuple
                    "trait_erc20::Event::Transfer"
                    [
                      Value.StructRecord
                        "trait_erc20::Transfer"
                        [
                          ("from", Value.StructTuple "core::option::Option::None" []);
                          ("to",
                            Value.StructTuple "core::option::Option::Some" [ M.read (| caller |) ]);
                          ("value", M.read (| total_supply |))
                        ]
                    ]
                ]
              |)
            |) in
          M.alloc (|
            Value.StructRecord
              "trait_erc20::Erc20"
              [
                ("total_supply", M.read (| total_supply |));
                ("balances", M.read (| balances |));
                ("allowances",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply
                        (Ty.path "trait_erc20::Mapping")
                        []
                        [
                          Ty.tuple
                            [ Ty.path "trait_erc20::AccountId"; Ty.path "trait_erc20::AccountId" ];
                          Ty.path "u128"
                        ],
                      [],
                      "default",
                      []
                    |),
                    []
                  |))
              ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  
  (*
      fn balance_of_impl(&self, owner: &AccountId) -> Balance {
          self.balances.get(owner).unwrap_or_default()
      }
  *)
  Definition balance_of_impl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owner ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owner := M.alloc (| owner |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u128" ],
            "unwrap_or_default",
            []
          |),
          [
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "trait_erc20::Mapping")
                  []
                  [ Ty.path "trait_erc20::AccountId"; Ty.path "u128" ],
                "get",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "trait_erc20::Erc20",
                  "balances"
                |);
                M.read (| owner |)
              ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_balance_of_impl :
    M.IsAssociatedFunction Self "balance_of_impl" balance_of_impl.
  
  (*
      fn allowance_impl(&self, owner: &AccountId, spender: &AccountId) -> Balance {
          self.allowances.get(&( *owner, *spender)).unwrap_or_default()
      }
  *)
  Definition allowance_impl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owner; spender ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owner := M.alloc (| owner |) in
        let spender := M.alloc (| spender |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u128" ],
            "unwrap_or_default",
            []
          |),
          [
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "trait_erc20::Mapping")
                  []
                  [
                    Ty.tuple [ Ty.path "trait_erc20::AccountId"; Ty.path "trait_erc20::AccountId" ];
                    Ty.path "u128"
                  ],
                "get",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "trait_erc20::Erc20",
                  "allowances"
                |);
                M.alloc (|
                  Value.Tuple [ M.read (| M.read (| owner |) |); M.read (| M.read (| spender |) |) ]
                |)
              ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_allowance_impl :
    M.IsAssociatedFunction Self "allowance_impl" allowance_impl.
  
  (*
      fn transfer_from_to(&mut self, from: &AccountId, to: &AccountId, value: Balance) -> Result<()> {
          let from_balance = self.balance_of_impl(from);
          if from_balance < value {
              return Err(Error::InsufficientBalance);
          }
  
          self.balances.insert( *from, from_balance - value);
          let to_balance = self.balance_of_impl(to);
          self.balances.insert( *to, to_balance + value);
          self.env().emit_event(Event::Transfer(Transfer {
              from: Some( *from),
              to: Some( *to),
              value,
          }));
          Ok(())
      }
  *)
  Definition transfer_from_to (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; from; to; value ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let from := M.alloc (| from |) in
        let to := M.alloc (| to |) in
        let value := M.alloc (| value |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ from_balance :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "trait_erc20::Erc20",
                      "balance_of_impl",
                      []
                    |),
                    [ M.read (| self |); M.read (| from |) ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (| M.read (| from_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"
                                  [ Value.StructTuple "trait_erc20::Error::InsufficientBalance" [] ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "trait_erc20::Mapping")
                        []
                        [ Ty.path "trait_erc20::AccountId"; Ty.path "u128" ],
                      "insert",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "trait_erc20::Erc20",
                        "balances"
                      |);
                      M.read (| M.read (| from |) |);
                      BinOp.Wrap.sub (| M.read (| from_balance |), M.read (| value |) |)
                    ]
                  |)
                |) in
              let~ to_balance :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "trait_erc20::Erc20",
                      "balance_of_impl",
                      []
                    |),
                    [ M.read (| self |); M.read (| to |) ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "trait_erc20::Mapping")
                        []
                        [ Ty.path "trait_erc20::AccountId"; Ty.path "u128" ],
                      "insert",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "trait_erc20::Erc20",
                        "balances"
                      |);
                      M.read (| M.read (| to |) |);
                      BinOp.Wrap.add (| M.read (| to_balance |), M.read (| value |) |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "trait_erc20::Env", "emit_event", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "trait_erc20::Erc20", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |);
                      Value.StructTuple
                        "trait_erc20::Event::Transfer"
                        [
                          Value.StructRecord
                            "trait_erc20::Transfer"
                            [
                              ("from",
                                Value.StructTuple
                                  "core::option::Option::Some"
                                  [ M.read (| M.read (| from |) |) ]);
                              ("to",
                                Value.StructTuple
                                  "core::option::Option::Some"
                                  [ M.read (| M.read (| to |) |) ]);
                              ("value", M.read (| value |))
                            ]
                        ]
                    ]
                  |)
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_transfer_from_to :
    M.IsAssociatedFunction Self "transfer_from_to" transfer_from_to.
End Impl_trait_erc20_Erc20.

Module Impl_trait_erc20_BaseErc20_for_trait_erc20_Erc20.
  Definition Self : Ty.t := Ty.path "trait_erc20::Erc20".
  
  (*
      fn total_supply(&self) -> Balance {
          self.total_supply
      }
  *)
  Definition total_supply (ε : 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 |),
            "trait_erc20::Erc20",
            "total_supply"
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
      fn balance_of(&self, owner: AccountId) -> Balance {
          self.balance_of_impl(&owner)
      }
  *)
  Definition balance_of (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owner ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owner := M.alloc (| owner |) in
        M.call_closure (|
          M.get_associated_function (| Ty.path "trait_erc20::Erc20", "balance_of_impl", [] |),
          [ M.read (| self |); owner ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
      fn allowance(&self, owner: AccountId, spender: AccountId) -> Balance {
          self.allowance_impl(&owner, &spender)
      }
  *)
  Definition allowance (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owner; spender ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owner := M.alloc (| owner |) in
        let spender := M.alloc (| spender |) in
        M.call_closure (|
          M.get_associated_function (| Ty.path "trait_erc20::Erc20", "allowance_impl", [] |),
          [ M.read (| self |); owner; spender ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
      fn transfer(&mut self, to: AccountId, value: Balance) -> Result<()> {
          let from = self.env().caller();
          self.transfer_from_to(&from, &to, value)
      }
  *)
  Definition transfer (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; to; value ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let to := M.alloc (| to |) in
        let value := M.alloc (| value |) in
        M.read (|
          let~ from :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "trait_erc20::Env", "caller", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "trait_erc20::Erc20", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "trait_erc20::Erc20", "transfer_from_to", [] |),
              [ M.read (| self |); from; to; M.read (| value |) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
      fn approve(&mut self, spender: AccountId, value: Balance) -> Result<()> {
          let owner = self.env().caller();
          self.allowances.insert((owner, spender), value);
          self.env().emit_event(Event::Approval(Approval {
              owner,
              spender,
              value,
          }));
          Ok(())
      }
  *)
  Definition approve (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; spender; value ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let spender := M.alloc (| spender |) in
        let value := M.alloc (| value |) in
        M.read (|
          let~ owner :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "trait_erc20::Env", "caller", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "trait_erc20::Erc20", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "trait_erc20::Mapping")
                    []
                    [
                      Ty.tuple
                        [ Ty.path "trait_erc20::AccountId"; Ty.path "trait_erc20::AccountId" ];
                      Ty.path "u128"
                    ],
                  "insert",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "trait_erc20::Erc20",
                    "allowances"
                  |);
                  Value.Tuple [ M.read (| owner |); M.read (| spender |) ];
                  M.read (| value |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "trait_erc20::Env", "emit_event", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "trait_erc20::Erc20", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |);
                  Value.StructTuple
                    "trait_erc20::Event::Approval"
                    [
                      Value.StructRecord
                        "trait_erc20::Approval"
                        [
                          ("owner", M.read (| owner |));
                          ("spender", M.read (| spender |));
                          ("value", M.read (| value |))
                        ]
                    ]
                ]
              |)
            |) in
          M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
      fn transfer_from(&mut self, from: AccountId, to: AccountId, value: Balance) -> Result<()> {
          let caller = self.env().caller();
          let allowance = self.allowance_impl(&from, &caller);
          if allowance < value {
              return Err(Error::InsufficientAllowance);
          }
          self.transfer_from_to(&from, &to, value)?;
          self.allowances.insert((from, caller), allowance - value);
          Ok(())
      }
  *)
  Definition transfer_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; from; to; value ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let from := M.alloc (| from |) in
        let to := M.alloc (| to |) in
        let value := M.alloc (| value |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ caller :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "trait_erc20::Env", "caller", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "trait_erc20::Erc20", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ allowance :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "trait_erc20::Erc20",
                      "allowance_impl",
                      []
                    |),
                    [ M.read (| self |); from; caller ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (| M.read (| allowance |), 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"
                                  [ Value.StructTuple "trait_erc20::Error::InsufficientAllowance" []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::Try",
                        Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [ Ty.tuple []; Ty.path "trait_erc20::Error" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "trait_erc20::Erc20",
                            "transfer_from_to",
                            []
                          |),
                          [ M.read (| self |); from; to; M.read (| value |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "trait_erc20::Error" ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [
                                          Ty.path "core::convert::Infallible";
                                          Ty.path "trait_erc20::Error"
                                        ]
                                    ],
                                    "from_residual",
                                    []
                                  |),
                                  [ M.read (| residual |) ]
                                |)
                              |)
                            |)
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        let val := M.copy (| γ0_0 |) in
                        val))
                  ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "trait_erc20::Mapping")
                        []
                        [
                          Ty.tuple
                            [ Ty.path "trait_erc20::AccountId"; Ty.path "trait_erc20::AccountId" ];
                          Ty.path "u128"
                        ],
                      "insert",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "trait_erc20::Erc20",
                        "allowances"
                      |);
                      Value.Tuple [ M.read (| from |); M.read (| caller |) ];
                      BinOp.Wrap.sub (| M.read (| allowance |), M.read (| value |) |)
                    ]
                  |)
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "trait_erc20::BaseErc20"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [
        ("total_supply", InstanceField.Method total_supply);
        ("balance_of", InstanceField.Method balance_of);
        ("allowance", InstanceField.Method allowance);
        ("transfer", InstanceField.Method transfer);
        ("approve", InstanceField.Method approve);
        ("transfer_from", InstanceField.Method transfer_from)
      ].
End Impl_trait_erc20_BaseErc20_for_trait_erc20_Erc20.
