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

Module Impl_dns_Mapping_K_V.
  Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "dns::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 new() -> Mapping<K, V> {
          unimplemented!()
      }
  *)
  Parameter new : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_new :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "new" (new 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_dns_Mapping_K_V.

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

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

Module Impl_core_clone_Clone_for_dns_AccountId.
  Definition Self : Ty.t := Ty.path "dns::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_dns_AccountId.

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

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

Module Impl_core_cmp_PartialEq_for_dns_AccountId.
  Definition Self : Ty.t := Ty.path "dns::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 |), "dns::AccountId", 0 |)
          |),
          M.read (|
            M.SubPointer.get_struct_tuple_field (| M.read (| other |), "dns::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_dns_AccountId.

Module Impl_core_convert_From_array_Usize_32_u8_for_dns_AccountId.
  Definition Self : Ty.t := Ty.path "dns::AccountId".
  
  (*
      fn from(_value: [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_dns_AccountId.

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

Axiom Hash :
  (Ty.path "dns::Hash") =
    (Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ]).

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

(* StructRecord
  {
    name := "Register";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("name",
          Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ]);
        ("from", Ty.path "dns::AccountId")
      ];
  } *)

(* StructRecord
  {
    name := "SetAddress";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("name",
          Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ]);
        ("from", Ty.path "dns::AccountId");
        ("old_address", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "dns::AccountId" ]);
        ("new_address", Ty.path "dns::AccountId")
      ];
  } *)

(* StructRecord
  {
    name := "Transfer";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("name",
          Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ]);
        ("from", Ty.path "dns::AccountId");
        ("old_owner", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "dns::AccountId" ]);
        ("new_owner", Ty.path "dns::AccountId")
      ];
  } *)

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

Module Impl_dns_Env.
  Definition Self : Ty.t := Ty.path "dns::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 |), "dns::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_dns_Env.

(* StructRecord
  {
    name := "DomainNameService";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("name_to_address",
          Ty.apply
            (Ty.path "dns::Mapping")
            []
            [
              Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ];
              Ty.path "dns::AccountId"
            ]);
        ("name_to_owner",
          Ty.apply
            (Ty.path "dns::Mapping")
            []
            [
              Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ];
              Ty.path "dns::AccountId"
            ]);
        ("default_address", Ty.path "dns::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 "dns::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 "dns::zero_address" zero_address.

Module Impl_core_default_Default_for_dns_DomainNameService.
  Definition Self : Ty.t := Ty.path "dns::DomainNameService".
  
  (*
      fn default() -> Self {
          let mut name_to_address = Mapping::new();
          name_to_address.insert(Hash::default(), zero_address());
          let mut name_to_owner = Mapping::new();
          name_to_owner.insert(Hash::default(), zero_address());
  
          Self {
              name_to_address,
              name_to_owner,
              default_address: zero_address(),
          }
      }
  *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.read (|
          let~ name_to_address :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "dns::Mapping")
                    []
                    [
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        [ Ty.path "u8" ];
                      Ty.path "dns::AccountId"
                    ],
                  "new",
                  []
                |),
                []
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "dns::Mapping")
                    []
                    [
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        [ Ty.path "u8" ];
                      Ty.path "dns::AccountId"
                    ],
                  "insert",
                  []
                |),
                [
                  name_to_address;
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        [ Ty.path "u8" ],
                      [],
                      "default",
                      []
                    |),
                    []
                  |);
                  M.call_closure (| M.get_function (| "dns::zero_address", [] |), [] |)
                ]
              |)
            |) in
          let~ name_to_owner :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "dns::Mapping")
                    []
                    [
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        [ Ty.path "u8" ];
                      Ty.path "dns::AccountId"
                    ],
                  "new",
                  []
                |),
                []
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "dns::Mapping")
                    []
                    [
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        [ Ty.path "u8" ];
                      Ty.path "dns::AccountId"
                    ],
                  "insert",
                  []
                |),
                [
                  name_to_owner;
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        [ Ty.path "u8" ],
                      [],
                      "default",
                      []
                    |),
                    []
                  |);
                  M.call_closure (| M.get_function (| "dns::zero_address", [] |), [] |)
                ]
              |)
            |) in
          M.alloc (|
            Value.StructRecord
              "dns::DomainNameService"
              [
                ("name_to_address", M.read (| name_to_address |));
                ("name_to_owner", M.read (| name_to_owner |));
                ("default_address",
                  M.call_closure (| M.get_function (| "dns::zero_address", [] |), [] |))
              ]
          |)
        |)))
    | _, _, _ => 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_dns_DomainNameService.

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

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

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

Module Impl_core_cmp_Eq_for_dns_Error.
  Definition Self : Ty.t := Ty.path "dns::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_dns_Error.

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

Module Impl_dns_DomainNameService.
  Definition Self : Ty.t := Ty.path "dns::DomainNameService".
  
  (*
      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 "dns::DomainNameService", "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 "dns::DomainNameService",
            [],
            "default",
            []
          |),
          []
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  
  (*
      pub fn register(&mut self, name: Hash) -> Result<()> {
          let caller = self.env().caller();
          if self.name_to_owner.contains(&name) {
              return Err(Error::NameAlreadyExists);
          }
  
          self.name_to_owner.insert(name, caller);
          self.env()
              .emit_event(Event::Register(Register { name, from: caller }));
  
          Ok(())
      }
  *)
  Definition register (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; name ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let name := M.alloc (| name |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ caller :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "dns::Env", "caller", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "dns::DomainNameService",
                            "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_associated_function (|
                                  Ty.apply
                                    (Ty.path "dns::Mapping")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "array")
                                        [ Value.Integer IntegerKind.Usize 32 ]
                                        [ Ty.path "u8" ];
                                      Ty.path "dns::AccountId"
                                    ],
                                  "contains",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "dns::DomainNameService",
                                    "name_to_owner"
                                  |);
                                  name
                                ]
                              |)
                            |)) 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 "dns::Error::NameAlreadyExists" [] ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "dns::Mapping")
                        []
                        [
                          Ty.apply
                            (Ty.path "array")
                            [ Value.Integer IntegerKind.Usize 32 ]
                            [ Ty.path "u8" ];
                          Ty.path "dns::AccountId"
                        ],
                      "insert",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "dns::DomainNameService",
                        "name_to_owner"
                      |);
                      M.read (| name |);
                      M.read (| caller |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "dns::Env", "emit_event", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "dns::DomainNameService",
                            "env",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |);
                      Value.StructTuple
                        "dns::Event::Register"
                        [
                          Value.StructRecord
                            "dns::Register"
                            [ ("name", M.read (| name |)); ("from", M.read (| caller |)) ]
                        ]
                    ]
                  |)
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_register : M.IsAssociatedFunction Self "register" register.
  
  (*
      fn get_owner_or_default(&self, name: Hash) -> AccountId {
          self.name_to_owner
              .get(&name)
              .unwrap_or(self.default_address)
      }
  *)
  Definition get_owner_or_default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; name ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let name := M.alloc (| name |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "dns::AccountId" ],
            "unwrap_or",
            []
          |),
          [
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "dns::Mapping")
                  []
                  [
                    Ty.apply
                      (Ty.path "array")
                      [ Value.Integer IntegerKind.Usize 32 ]
                      [ Ty.path "u8" ];
                    Ty.path "dns::AccountId"
                  ],
                "get",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "dns::DomainNameService",
                  "name_to_owner"
                |);
                name
              ]
            |);
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "dns::DomainNameService",
                "default_address"
              |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_get_owner_or_default :
    M.IsAssociatedFunction Self "get_owner_or_default" get_owner_or_default.
  
  (*
      pub fn set_address(&mut self, name: Hash, new_address: AccountId) -> Result<()> {
          let caller = self.env().caller();
          let owner = self.get_owner_or_default(name);
          if caller != owner {
              return Err(Error::CallerIsNotOwner);
          }
  
          let old_address = self.name_to_address.get(&name);
          self.name_to_address.insert(name, new_address);
  
          self.env().emit_event(Event::SetAddress(SetAddress {
              name,
              from: caller,
              old_address,
              new_address,
          }));
          Ok(())
      }
  *)
  Definition set_address (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; name; new_address ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let name := M.alloc (| name |) in
        let new_address := M.alloc (| new_address |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ caller :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "dns::Env", "caller", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "dns::DomainNameService",
                            "env",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ owner :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "dns::DomainNameService",
                      "get_owner_or_default",
                      []
                    |),
                    [ M.read (| self |); M.read (| name |) ]
                  |)
                |) 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 "dns::AccountId",
                                  [ Ty.path "dns::AccountId" ],
                                  "ne",
                                  []
                                |),
                                [ caller; owner ]
                              |)
                            |)) 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 "dns::Error::CallerIsNotOwner" [] ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ old_address :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "dns::Mapping")
                        []
                        [
                          Ty.apply
                            (Ty.path "array")
                            [ Value.Integer IntegerKind.Usize 32 ]
                            [ Ty.path "u8" ];
                          Ty.path "dns::AccountId"
                        ],
                      "get",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "dns::DomainNameService",
                        "name_to_address"
                      |);
                      name
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "dns::Mapping")
                        []
                        [
                          Ty.apply
                            (Ty.path "array")
                            [ Value.Integer IntegerKind.Usize 32 ]
                            [ Ty.path "u8" ];
                          Ty.path "dns::AccountId"
                        ],
                      "insert",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "dns::DomainNameService",
                        "name_to_address"
                      |);
                      M.read (| name |);
                      M.read (| new_address |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "dns::Env", "emit_event", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "dns::DomainNameService",
                            "env",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |);
                      Value.StructTuple
                        "dns::Event::SetAddress"
                        [
                          Value.StructRecord
                            "dns::SetAddress"
                            [
                              ("name", M.read (| name |));
                              ("from", M.read (| caller |));
                              ("old_address", M.read (| old_address |));
                              ("new_address", M.read (| new_address |))
                            ]
                        ]
                    ]
                  |)
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_set_address : M.IsAssociatedFunction Self "set_address" set_address.
  
  (*
      pub fn transfer(&mut self, name: Hash, to: AccountId) -> Result<()> {
          let caller = self.env().caller();
          let owner = self.get_owner_or_default(name);
          if caller != owner {
              return Err(Error::CallerIsNotOwner);
          }
  
          let old_owner = self.name_to_owner.get(&name);
          self.name_to_owner.insert(name, to);
  
          self.env().emit_event(Event::Transfer(Transfer {
              name,
              from: caller,
              old_owner,
              new_owner: to,
          }));
  
          Ok(())
      }
  *)
  Definition transfer (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; name; to ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let name := M.alloc (| name |) in
        let to := M.alloc (| to |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ caller :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "dns::Env", "caller", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "dns::DomainNameService",
                            "env",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ owner :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "dns::DomainNameService",
                      "get_owner_or_default",
                      []
                    |),
                    [ M.read (| self |); M.read (| name |) ]
                  |)
                |) 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 "dns::AccountId",
                                  [ Ty.path "dns::AccountId" ],
                                  "ne",
                                  []
                                |),
                                [ caller; owner ]
                              |)
                            |)) 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 "dns::Error::CallerIsNotOwner" [] ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ old_owner :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "dns::Mapping")
                        []
                        [
                          Ty.apply
                            (Ty.path "array")
                            [ Value.Integer IntegerKind.Usize 32 ]
                            [ Ty.path "u8" ];
                          Ty.path "dns::AccountId"
                        ],
                      "get",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "dns::DomainNameService",
                        "name_to_owner"
                      |);
                      name
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "dns::Mapping")
                        []
                        [
                          Ty.apply
                            (Ty.path "array")
                            [ Value.Integer IntegerKind.Usize 32 ]
                            [ Ty.path "u8" ];
                          Ty.path "dns::AccountId"
                        ],
                      "insert",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "dns::DomainNameService",
                        "name_to_owner"
                      |);
                      M.read (| name |);
                      M.read (| to |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "dns::Env", "emit_event", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "dns::DomainNameService",
                            "env",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |);
                      Value.StructTuple
                        "dns::Event::Transfer"
                        [
                          Value.StructRecord
                            "dns::Transfer"
                            [
                              ("name", M.read (| name |));
                              ("from", M.read (| caller |));
                              ("old_owner", M.read (| old_owner |));
                              ("new_owner", M.read (| to |))
                            ]
                        ]
                    ]
                  |)
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_transfer : M.IsAssociatedFunction Self "transfer" transfer.
  
  (*
      fn get_address_or_default(&self, name: Hash) -> AccountId {
          self.name_to_address
              .get(&name)
              .unwrap_or(self.default_address)
      }
  *)
  Definition get_address_or_default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; name ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let name := M.alloc (| name |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "dns::AccountId" ],
            "unwrap_or",
            []
          |),
          [
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "dns::Mapping")
                  []
                  [
                    Ty.apply
                      (Ty.path "array")
                      [ Value.Integer IntegerKind.Usize 32 ]
                      [ Ty.path "u8" ];
                    Ty.path "dns::AccountId"
                  ],
                "get",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "dns::DomainNameService",
                  "name_to_address"
                |);
                name
              ]
            |);
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "dns::DomainNameService",
                "default_address"
              |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_get_address_or_default :
    M.IsAssociatedFunction Self "get_address_or_default" get_address_or_default.
  
  (*
      pub fn get_address(&self, name: Hash) -> AccountId {
          self.get_address_or_default(name)
      }
  *)
  Definition get_address (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; name ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let name := M.alloc (| name |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.path "dns::DomainNameService",
            "get_address_or_default",
            []
          |),
          [ M.read (| self |); M.read (| name |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_get_address : M.IsAssociatedFunction Self "get_address" get_address.
  
  (*
      pub fn get_owner(&self, name: Hash) -> AccountId {
          self.get_owner_or_default(name)
      }
  *)
  Definition get_owner (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; name ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let name := M.alloc (| name |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.path "dns::DomainNameService",
            "get_owner_or_default",
            []
          |),
          [ M.read (| self |); M.read (| name |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_get_owner : M.IsAssociatedFunction Self "get_owner" get_owner.
End Impl_dns_DomainNameService.
