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

Module Impl_mother_Mapping_K_V.
  Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "mother::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_mother_Mapping_K_V.

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

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

Module Impl_core_clone_Clone_for_mother_AccountId.
  Definition Self : Ty.t := Ty.path "mother::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_mother_AccountId.

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

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

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

Module Impl_core_cmp_Eq_for_mother_AccountId.
  Definition Self : Ty.t := Ty.path "mother::AccountId".
  
  (* 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
        M.read (|
          M.match_operator (|
            Value.DeclaredButUndefined,
            [ fun γ => ltac:(M.monadic (M.alloc (| 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_mother_AccountId.

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

Axiom BlockNumber : (Ty.path "mother::BlockNumber") = (Ty.path "u32").

Axiom Hash :
  (Ty.path "mother::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 "mother::AccountId") ];
  } *)

(* StructTuple
  {
    name := "Bids";
    const_params := [];
    ty_params := [];
    fields :=
      [
        Ty.apply
          (Ty.path "alloc::vec::Vec")
          []
          [
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.tuple [ Ty.path "mother::AccountId"; Ty.path "u128" ] ];
                Ty.path "alloc::alloc::Global"
              ];
            Ty.path "alloc::alloc::Global"
          ]
      ];
  } *)

Module Impl_core_default_Default_for_mother_Bids.
  Definition Self : Ty.t := Ty.path "mother::Bids".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructTuple
          "mother::Bids"
          [
            M.call_closure (|
              M.get_trait_method (|
                "core::default::Default",
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.tuple [ Ty.path "mother::AccountId"; Ty.path "u128" ] ];
                        Ty.path "alloc::alloc::Global"
                      ];
                    Ty.path "alloc::alloc::Global"
                  ],
                [],
                "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_mother_Bids.

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

Module Impl_core_cmp_PartialEq_for_mother_Bids.
  Definition Self : Ty.t := Ty.path "mother::Bids".
  
  (* 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.call_closure (|
          M.get_trait_method (|
            "core::cmp::PartialEq",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.tuple [ Ty.path "mother::AccountId"; Ty.path "u128" ] ];
                    Ty.path "alloc::alloc::Global"
                  ];
                Ty.path "alloc::alloc::Global"
              ],
            [
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [ Ty.tuple [ Ty.path "mother::AccountId"; Ty.path "u128" ] ];
                      Ty.path "alloc::alloc::Global"
                    ];
                  Ty.path "alloc::alloc::Global"
                ]
            ],
            "eq",
            []
          |),
          [
            M.SubPointer.get_struct_tuple_field (| M.read (| self |), "mother::Bids", 0 |);
            M.SubPointer.get_struct_tuple_field (| M.read (| other |), "mother::Bids", 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_mother_Bids.

Module Impl_core_cmp_Eq_for_mother_Bids.
  Definition Self : Ty.t := Ty.path "mother::Bids".
  
  (* 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
        M.read (|
          M.match_operator (|
            Value.DeclaredButUndefined,
            [ fun γ => ltac:(M.monadic (M.alloc (| 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_mother_Bids.

Module Impl_core_clone_Clone_for_mother_Bids.
  Definition Self : Ty.t := Ty.path "mother::Bids".
  
  (* 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
        Value.StructTuple
          "mother::Bids"
          [
            M.call_closure (|
              M.get_trait_method (|
                "core::clone::Clone",
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.tuple [ Ty.path "mother::AccountId"; Ty.path "u128" ] ];
                        Ty.path "alloc::alloc::Global"
                      ];
                    Ty.path "alloc::alloc::Global"
                  ],
                [],
                "clone",
                []
              |),
              [ M.SubPointer.get_struct_tuple_field (| M.read (| self |), "mother::Bids", 0 |) ]
            |)
          ]))
    | _, _, _ => 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_mother_Bids.

(*
Enum Outline
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "NoWinner";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "WinnerDetected";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "PayoutCompleted";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

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

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

Module Impl_core_cmp_Eq_for_mother_Outline.
  Definition Self : Ty.t := Ty.path "mother::Outline".
  
  (* 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_mother_Outline.

Module Impl_core_clone_Clone_for_mother_Outline.
  Definition Self : Ty.t := Ty.path "mother::Outline".
  
  (* 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 (|
            self,
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.read (| γ |) in
                  let _ := M.is_struct_tuple (| γ, "mother::Outline::NoWinner" |) in
                  M.alloc (| Value.StructTuple "mother::Outline::NoWinner" [] |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.read (| γ |) in
                  let _ := M.is_struct_tuple (| γ, "mother::Outline::WinnerDetected" |) in
                  M.alloc (| Value.StructTuple "mother::Outline::WinnerDetected" [] |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.read (| γ |) in
                  let _ := M.is_struct_tuple (| γ, "mother::Outline::PayoutCompleted" |) in
                  M.alloc (| Value.StructTuple "mother::Outline::PayoutCompleted" [] |)))
            ]
          |)
        |)))
    | _, _, _ => 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_mother_Outline.

(*
Enum Status
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "NotStarted";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "OpeningPeriod";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "EndingPeriod";
        item := StructTuple [ Ty.path "u32" ];
        discriminant := None;
      };
      {
        name := "Ended";
        item := StructTuple [ Ty.path "mother::Outline" ];
        discriminant := None;
      };
      {
        name := "RfDelay";
        item := StructTuple [ Ty.path "u32" ];
        discriminant := None;
      }
    ];
}
*)

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

Module Impl_core_cmp_PartialEq_for_mother_Status.
  Definition Self : Ty.t := Ty.path "mother::Status".
  
  (* 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 "mother::Status" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "mother::Status" ]
                |),
                [ M.read (| other |) ]
              |)
            |) in
          M.alloc (|
            LogicalOp.and (|
              BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |),
              ltac:(M.monadic
                (M.read (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let γ0_0 := M.read (| γ0_0 |) in
                          let γ2_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ0_0,
                              "mother::Status::EndingPeriod",
                              0
                            |) in
                          let __self_0 := M.alloc (| γ2_0 |) in
                          let γ0_1 := M.read (| γ0_1 |) in
                          let γ2_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ0_1,
                              "mother::Status::EndingPeriod",
                              0
                            |) in
                          let __arg1_0 := M.alloc (| γ2_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::cmp::PartialEq",
                                Ty.apply (Ty.path "&") [] [ Ty.path "u32" ],
                                [ Ty.apply (Ty.path "&") [] [ Ty.path "u32" ] ],
                                "eq",
                                []
                              |),
                              [ __self_0; __arg1_0 ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let γ0_0 := M.read (| γ0_0 |) in
                          let γ2_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ0_0,
                              "mother::Status::Ended",
                              0
                            |) in
                          let __self_0 := M.alloc (| γ2_0 |) in
                          let γ0_1 := M.read (| γ0_1 |) in
                          let γ2_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ0_1,
                              "mother::Status::Ended",
                              0
                            |) in
                          let __arg1_0 := M.alloc (| γ2_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::cmp::PartialEq",
                                Ty.apply (Ty.path "&") [] [ Ty.path "mother::Outline" ],
                                [ Ty.apply (Ty.path "&") [] [ Ty.path "mother::Outline" ] ],
                                "eq",
                                []
                              |),
                              [ __self_0; __arg1_0 ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let γ0_0 := M.read (| γ0_0 |) in
                          let γ2_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ0_0,
                              "mother::Status::RfDelay",
                              0
                            |) in
                          let __self_0 := M.alloc (| γ2_0 |) in
                          let γ0_1 := M.read (| γ0_1 |) in
                          let γ2_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ0_1,
                              "mother::Status::RfDelay",
                              0
                            |) in
                          let __arg1_0 := M.alloc (| γ2_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::cmp::PartialEq",
                                Ty.apply (Ty.path "&") [] [ Ty.path "u32" ],
                                [ Ty.apply (Ty.path "&") [] [ Ty.path "u32" ] ],
                                "eq",
                                []
                              |),
                              [ __self_0; __arg1_0 ]
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                    ]
                  |)
                |)))
            |)
          |)
        |)))
    | _, _, _ => 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_mother_Status.

Module Impl_core_cmp_Eq_for_mother_Status.
  Definition Self : Ty.t := Ty.path "mother::Status".
  
  (* 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
        M.read (|
          M.match_operator (|
            Value.DeclaredButUndefined,
            [
              fun γ =>
                ltac:(M.monadic
                  (M.match_operator (|
                    Value.DeclaredButUndefined,
                    [ fun γ => ltac:(M.monadic (M.alloc (| 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_mother_Status.

Module Impl_core_clone_Clone_for_mother_Status.
  Definition Self : Ty.t := Ty.path "mother::Status".
  
  (* 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 (|
            self,
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.read (| γ |) in
                  let _ := M.is_struct_tuple (| γ, "mother::Status::NotStarted" |) in
                  M.alloc (| Value.StructTuple "mother::Status::NotStarted" [] |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.read (| γ |) in
                  let _ := M.is_struct_tuple (| γ, "mother::Status::OpeningPeriod" |) in
                  M.alloc (| Value.StructTuple "mother::Status::OpeningPeriod" [] |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.read (| γ |) in
                  let γ1_0 :=
                    M.SubPointer.get_struct_tuple_field (|
                      γ,
                      "mother::Status::EndingPeriod",
                      0
                    |) in
                  let __self_0 := M.alloc (| γ1_0 |) in
                  M.alloc (|
                    Value.StructTuple
                      "mother::Status::EndingPeriod"
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::clone::Clone",
                            Ty.path "u32",
                            [],
                            "clone",
                            []
                          |),
                          [ M.read (| __self_0 |) ]
                        |)
                      ]
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.read (| γ |) in
                  let γ1_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "mother::Status::Ended", 0 |) in
                  let __self_0 := M.alloc (| γ1_0 |) in
                  M.alloc (|
                    Value.StructTuple
                      "mother::Status::Ended"
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::clone::Clone",
                            Ty.path "mother::Outline",
                            [],
                            "clone",
                            []
                          |),
                          [ M.read (| __self_0 |) ]
                        |)
                      ]
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.read (| γ |) in
                  let γ1_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "mother::Status::RfDelay", 0 |) in
                  let __self_0 := M.alloc (| γ1_0 |) in
                  M.alloc (|
                    Value.StructTuple
                      "mother::Status::RfDelay"
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::clone::Clone",
                            Ty.path "u32",
                            [],
                            "clone",
                            []
                          |),
                          [ M.read (| __self_0 |) ]
                        |)
                      ]
                  |)))
            ]
          |)
        |)))
    | _, _, _ => 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_mother_Status.

(* StructRecord
  {
    name := "Auction";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("name", Ty.path "alloc::string::String");
        ("subject",
          Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ]);
        ("bids", Ty.path "mother::Bids");
        ("terms",
          Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 3 ] [ Ty.path "u32" ]);
        ("status", Ty.path "mother::Status");
        ("finalized", Ty.path "bool");
        ("vector",
          Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ])
      ];
  } *)

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

Module Impl_core_cmp_PartialEq_for_mother_Auction.
  Definition Self : Ty.t := Ty.path "mother::Auction".
  
  (* 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
        LogicalOp.and (|
          LogicalOp.and (|
            LogicalOp.and (|
              LogicalOp.and (|
                LogicalOp.and (|
                  LogicalOp.and (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.path "alloc::string::String",
                        [ Ty.path "alloc::string::String" ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "mother::Auction",
                          "name"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "mother::Auction",
                          "name"
                        |)
                      ]
                    |),
                    ltac:(M.monadic
                      (M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialEq",
                          Ty.apply
                            (Ty.path "array")
                            [ Value.Integer IntegerKind.Usize 32 ]
                            [ Ty.path "u8" ],
                          [
                            Ty.apply
                              (Ty.path "array")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [ Ty.path "u8" ]
                          ],
                          "eq",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "mother::Auction",
                            "subject"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "mother::Auction",
                            "subject"
                          |)
                        ]
                      |)))
                  |),
                  ltac:(M.monadic
                    (M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.path "mother::Bids",
                        [ Ty.path "mother::Bids" ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "mother::Auction",
                          "bids"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "mother::Auction",
                          "bids"
                        |)
                      ]
                    |)))
                |),
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 3 ]
                        [ Ty.path "u32" ],
                      [
                        Ty.apply
                          (Ty.path "array")
                          [ Value.Integer IntegerKind.Usize 3 ]
                          [ Ty.path "u32" ]
                      ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "mother::Auction",
                        "terms"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "mother::Auction",
                        "terms"
                      |)
                    ]
                  |)))
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.path "mother::Status",
                    [ Ty.path "mother::Status" ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "mother::Auction",
                      "status"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "mother::Auction",
                      "status"
                    |)
                  ]
                |)))
            |),
            ltac:(M.monadic
              (BinOp.eq (|
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "mother::Auction",
                    "finalized"
                  |)
                |),
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "mother::Auction",
                    "finalized"
                  |)
                |)
              |)))
          |),
          ltac:(M.monadic
            (M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                [
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]
                ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "mother::Auction",
                  "vector"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "mother::Auction",
                  "vector"
                |)
              ]
            |)))
        |)))
    | _, _, _ => 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_mother_Auction.

Module Impl_core_cmp_Eq_for_mother_Auction.
  Definition Self : Ty.t := Ty.path "mother::Auction".
  
  (* 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
        M.read (|
          M.match_operator (|
            Value.DeclaredButUndefined,
            [
              fun γ =>
                ltac:(M.monadic
                  (M.match_operator (|
                    Value.DeclaredButUndefined,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            Value.DeclaredButUndefined,
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    Value.DeclaredButUndefined,
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (M.match_operator (|
                                            Value.DeclaredButUndefined,
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.match_operator (|
                                                    Value.DeclaredButUndefined,
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.match_operator (|
                                                            Value.DeclaredButUndefined,
                                                            [
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (M.alloc (| 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_mother_Auction.

Module Impl_core_clone_Clone_for_mother_Auction.
  Definition Self : Ty.t := Ty.path "mother::Auction".
  
  (* 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
        Value.StructRecord
          "mother::Auction"
          [
            ("name",
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.path "alloc::string::String",
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "mother::Auction",
                    "name"
                  |)
                ]
              |));
            ("subject",
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.apply
                    (Ty.path "array")
                    [ Value.Integer IntegerKind.Usize 32 ]
                    [ Ty.path "u8" ],
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "mother::Auction",
                    "subject"
                  |)
                ]
              |));
            ("bids",
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.path "mother::Bids",
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "mother::Auction",
                    "bids"
                  |)
                ]
              |));
            ("terms",
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.apply
                    (Ty.path "array")
                    [ Value.Integer IntegerKind.Usize 3 ]
                    [ Ty.path "u32" ],
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "mother::Auction",
                    "terms"
                  |)
                ]
              |));
            ("status",
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.path "mother::Status",
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "mother::Auction",
                    "status"
                  |)
                ]
              |));
            ("finalized",
              M.call_closure (|
                M.get_trait_method (| "core::clone::Clone", Ty.path "bool", [], "clone", [] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "mother::Auction",
                    "finalized"
                  |)
                ]
              |));
            ("vector",
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "mother::Auction",
                    "vector"
                  |)
                ]
              |))
          ]))
    | _, _, _ => 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_mother_Auction.

Module Impl_core_default_Default_for_mother_Auction.
  Definition Self : Ty.t := Ty.path "mother::Auction".
  
  (*
      fn default() -> Auction {
          Auction {
              name: String::default(),
              subject: Hash::default(),
              bids: Bids::default(),
              terms: <[BlockNumber; 3]>::default(),
              status: Status::OpeningPeriod,
              finalized: false,
              vector: <Vec<u8>>::default(),
          }
      }
  *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "mother::Auction"
          [
            ("name",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "alloc::string::String",
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("subject",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "array")
                    [ Value.Integer IntegerKind.Usize 32 ]
                    [ Ty.path "u8" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("bids",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "mother::Bids",
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("terms",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "array")
                    [ Value.Integer IntegerKind.Usize 3 ]
                    [ Ty.path "u32" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("status", Value.StructTuple "mother::Status::OpeningPeriod" []);
            ("finalized", Value.Bool false);
            ("vector",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                  [],
                  "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_mother_Auction.

(*
Enum Failure
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "Revert";
        item := StructTuple [ Ty.path "alloc::string::String" ];
        discriminant := None;
      };
      {
        name := "Panic";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

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

Module Impl_core_cmp_PartialEq_for_mother_Failure.
  Definition Self : Ty.t := Ty.path "mother::Failure".
  
  (* 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 "mother::Failure" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "mother::Failure" ]
                |),
                [ M.read (| other |) ]
              |)
            |) in
          M.alloc (|
            LogicalOp.and (|
              BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |),
              ltac:(M.monadic
                (M.read (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let γ0_0 := M.read (| γ0_0 |) in
                          let γ2_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ0_0,
                              "mother::Failure::Revert",
                              0
                            |) in
                          let __self_0 := M.alloc (| γ2_0 |) in
                          let γ0_1 := M.read (| γ0_1 |) in
                          let γ2_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ0_1,
                              "mother::Failure::Revert",
                              0
                            |) in
                          let __arg1_0 := M.alloc (| γ2_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::cmp::PartialEq",
                                Ty.apply (Ty.path "&") [] [ Ty.path "alloc::string::String" ],
                                [ Ty.apply (Ty.path "&") [] [ Ty.path "alloc::string::String" ] ],
                                "eq",
                                []
                              |),
                              [ __self_0; __arg1_0 ]
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                    ]
                  |)
                |)))
            |)
          |)
        |)))
    | _, _, _ => 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_mother_Failure.

Module Impl_core_cmp_Eq_for_mother_Failure.
  Definition Self : Ty.t := Ty.path "mother::Failure".
  
  (* 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
        M.read (|
          M.match_operator (|
            Value.DeclaredButUndefined,
            [ fun γ => ltac:(M.monadic (M.alloc (| 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_mother_Failure.

(* StructRecord
  {
    name := "AuctionEchoed";
    const_params := [];
    ty_params := [];
    fields := [ ("auction", Ty.path "mother::Auction") ];
  } *)

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

Module Impl_mother_Env.
  Definition Self : Ty.t := Ty.path "mother::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 |), "mother::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_mother_Env.

(* StructRecord
  {
    name := "Mother";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("auction", Ty.path "mother::Auction");
        ("balances",
          Ty.apply (Ty.path "mother::Mapping") [] [ Ty.path "mother::AccountId"; Ty.path "u128" ])
      ];
  } *)

Module Impl_core_default_Default_for_mother_Mother.
  Definition Self : Ty.t := Ty.path "mother::Mother".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "mother::Mother"
          [
            ("auction",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "mother::Auction",
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("balances",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "mother::Mapping")
                    []
                    [ Ty.path "mother::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_mother_Mother.

Module Impl_mother_Mother.
  Definition Self : Ty.t := Ty.path "mother::Mother".
  
  (*
      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 "mother::Mother", "init_env", [] |),
          []
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_env : M.IsAssociatedFunction Self "env" env.
  
  (*
      pub fn new(auction: Auction) -> Self {
          Self {
              balances: Default::default(),
              auction,
          }
      }
  *)
  Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ auction ] =>
      ltac:(M.monadic
        (let auction := M.alloc (| auction |) in
        Value.StructRecord
          "mother::Mother"
          [
            ("balances",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "mother::Mapping")
                    []
                    [ Ty.path "mother::AccountId"; Ty.path "u128" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("auction", M.read (| auction |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  
  (*
      pub fn new_default() -> Self {
          Default::default()
      }
  *)
  Definition new_default (ε : 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 "mother::Mother",
            [],
            "default",
            []
          |),
          []
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_new_default : M.IsAssociatedFunction Self "new_default" new_default.
  
  (*
      pub fn failed_new(fail: bool) -> Result<Self, Failure> {
          if fail {
              Err(Failure::Revert("Reverting instantiation".to_string()))
          } else {
              Ok(Default::default())
          }
      }
  *)
  Definition failed_new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ fail ] =>
      ltac:(M.monadic
        (let fail := M.alloc (| fail |) in
        M.read (|
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.use fail in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Err"
                      [
                        Value.StructTuple
                          "mother::Failure::Revert"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "alloc::string::ToString",
                                Ty.path "str",
                                [],
                                "to_string",
                                []
                              |),
                              [ M.read (| Value.String "Reverting instantiation" |) ]
                            |)
                          ]
                      ]
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Ok"
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::default::Default",
                            Ty.path "mother::Mother",
                            [],
                            "default",
                            []
                          |),
                          []
                        |)
                      ]
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_failed_new : M.IsAssociatedFunction Self "failed_new" failed_new.
  
  (*
      pub fn echo_auction(&mut self, auction: Auction) -> Auction {
          self.env().emit_event(Event::AuctionEchoed(AuctionEchoed {
              auction: auction.clone(),
          }));
          auction
      }
  *)
  Definition echo_auction (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; auction ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let auction := M.alloc (| auction |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "mother::Env", "emit_event", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "mother::Mother", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |);
                  Value.StructTuple
                    "mother::Event::AuctionEchoed"
                    [
                      Value.StructRecord
                        "mother::AuctionEchoed"
                        [
                          ("auction",
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::clone::Clone",
                                Ty.path "mother::Auction",
                                [],
                                "clone",
                                []
                              |),
                              [ auction ]
                            |))
                        ]
                    ]
                ]
              |)
            |) in
          auction
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_echo_auction : M.IsAssociatedFunction Self "echo_auction" echo_auction.
  
  (*
      pub fn revert_or_trap(&mut self, fail: Option<Failure>) -> Result<(), Failure> {
          match fail {
              Some(Failure::Revert(_)) => {
                  Err(Failure::Revert("Reverting on user demand!".to_string()))
              }
              Some(Failure::Panic) => {
                  panic!("Trapping on user demand!")
              }
              None => Ok(()),
          }
      }
  *)
  Definition revert_or_trap (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; fail ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let fail := M.alloc (| fail |) in
        M.read (|
          M.match_operator (|
            fail,
            [
              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_struct_tuple_field (| γ0_0, "mother::Failure::Revert", 0 |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Err"
                      [
                        Value.StructTuple
                          "mother::Failure::Revert"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "alloc::string::ToString",
                                Ty.path "str",
                                [],
                                "to_string",
                                []
                              |),
                              [ M.read (| Value.String "Reverting on user demand!" |) ]
                            |)
                          ]
                      ]
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::option::Option::Some", 0 |) in
                  let _ := M.is_struct_tuple (| γ0_0, "mother::Failure::Panic" |) in
                  M.alloc (|
                    M.never_to_any (|
                      M.call_closure (|
                        M.get_function (|
                          "std::panicking::begin_panic",
                          [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                        |),
                        [ M.read (| Value.String "Trapping on user demand!" |) ]
                      |)
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                  M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_revert_or_trap :
    M.IsAssociatedFunction Self "revert_or_trap" revert_or_trap.
  
  (*
      pub fn debug_log(&mut self, _message: String) {
          println!("debug_log: {}", _message);
      }
  *)
  Definition debug_log (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; _message ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let _message := M.alloc (| _message |) in
        M.read (|
          let~ _ :=
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "std::io::stdio::_print", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                      [
                        M.alloc (|
                          Value.Array
                            [ M.read (| Value.String "debug_log: " |); M.read (| Value.String "
" |)
                            ]
                        |);
                        M.alloc (|
                          Value.Array
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::Argument",
                                  "new_display",
                                  [ Ty.path "alloc::string::String" ]
                                |),
                                [ _message ]
                              |)
                            ]
                        |)
                      ]
                    |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_debug_log : M.IsAssociatedFunction Self "debug_log" debug_log.
End Impl_mother_Mother.
