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

Module metadata.
  (* StructRecord
    {
      name := "Metadata";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("key",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]);
          ("value",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ])
        ];
    } *)
  
  Module Impl_core_clone_Clone_for_move_core_types_metadata_Metadata.
    Definition Self : Ty.t := Ty.path "move_core_types::metadata::Metadata".
    
    (* 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
            "move_core_types::metadata::Metadata"
            [
              ("key",
                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 |),
                      "move_core_types::metadata::Metadata",
                      "key"
                    |)
                  ]
                |));
              ("value",
                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 |),
                      "move_core_types::metadata::Metadata",
                      "value"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => 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_move_core_types_metadata_Metadata.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_core_types_metadata_Metadata.
    Definition Self : Ty.t := Ty.path "move_core_types::metadata::Metadata".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_core_types_metadata_Metadata.
  
  Module Impl_core_cmp_PartialEq_for_move_core_types_metadata_Metadata.
    Definition Self : Ty.t := Ty.path "move_core_types::metadata::Metadata".
    
    (* 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 (|
            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 |),
                  "move_core_types::metadata::Metadata",
                  "key"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "move_core_types::metadata::Metadata",
                  "key"
                |)
              ]
            |),
            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 |),
                    "move_core_types::metadata::Metadata",
                    "value"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "move_core_types::metadata::Metadata",
                    "value"
                  |)
                ]
              |)))
          |)))
      | _, _, _ => 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_move_core_types_metadata_Metadata.
  
  Module Impl_core_cmp_Eq_for_move_core_types_metadata_Metadata.
    Definition Self : Ty.t := Ty.path "move_core_types::metadata::Metadata".
    
    (* 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_move_core_types_metadata_Metadata.
  
  Module Impl_core_fmt_Debug_for_move_core_types_metadata_Metadata.
    Definition Self : Ty.t := Ty.path "move_core_types::metadata::Metadata".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field2_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "Metadata" |);
              M.read (| Value.String "key" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_core_types::metadata::Metadata",
                "key"
              |);
              M.read (| Value.String "value" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_core_types::metadata::Metadata",
                  "value"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_move_core_types_metadata_Metadata.
  
  Module underscore.
    Module Impl_serde_ser_Serialize_for_move_core_types_metadata_Metadata.
      Definition Self : Ty.t := Ty.path "move_core_types::metadata::Metadata".
      
      (* Serialize *)
      Definition serialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ __S ], [ self; __serializer ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let __serializer := M.alloc (| __serializer |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ __serde_state :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::Serializer",
                              __S,
                              [],
                              "serialize_struct",
                              []
                            |),
                            [
                              M.read (| __serializer |);
                              M.read (| Value.String "Metadata" |);
                              BinOp.Wrap.add (|
                                BinOp.Wrap.add (|
                                  M.rust_cast (Value.Bool false),
                                  Value.Integer IntegerKind.Usize 1
                                |),
                                Value.Integer IntegerKind.Usize 1
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::result::Result::Ok",
                                  0
                                |) in
                              let __val := M.copy (| γ0_0 |) in
                              __val));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::result::Result::Err",
                                  0
                                |) in
                              let __err := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      Value.StructTuple
                                        "core::result::Result::Err"
                                        [ M.read (| __err |) ]
                                    |)
                                  |)
                                |)
                              |)))
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::SerializeStruct",
                            Ty.associated,
                            [],
                            "serialize_field",
                            [
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]
                            ]
                          |),
                          [
                            __serde_state;
                            M.read (| Value.String "key" |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "move_core_types::metadata::Metadata",
                              "key"
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Ok",
                                0
                              |) in
                            let __val := M.copy (| γ0_0 |) in
                            __val));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Err",
                                0
                              |) in
                            let __err := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Err"
                                      [ M.read (| __err |) ]
                                  |)
                                |)
                              |)
                            |)))
                      ]
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::SerializeStruct",
                            Ty.associated,
                            [],
                            "serialize_field",
                            [
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]
                            ]
                          |),
                          [
                            __serde_state;
                            M.read (| Value.String "value" |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "move_core_types::metadata::Metadata",
                              "value"
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Ok",
                                0
                              |) in
                            let __val := M.copy (| γ0_0 |) in
                            __val));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Err",
                                0
                              |) in
                            let __err := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Err"
                                      [ M.read (| __err |) ]
                                  |)
                                |)
                              |)
                            |)))
                      ]
                    |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "serde::ser::SerializeStruct",
                        Ty.associated,
                        [],
                        "end",
                        []
                      |),
                      [ M.read (| __serde_state |) ]
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "serde::ser::Serialize"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("serialize", InstanceField.Method serialize) ].
    End Impl_serde_ser_Serialize_for_move_core_types_metadata_Metadata.
    Module Impl_serde_de_Deserialize_for_move_core_types_metadata_Metadata.
      Definition Self : Ty.t := Ty.path "move_core_types::metadata::Metadata".
      
      (* Deserialize *)
      Definition deserialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ __D ], [ __deserializer ] =>
          ltac:(M.monadic
            (let __deserializer := M.alloc (| __deserializer |) in
            M.call_closure (|
              M.get_trait_method (|
                "serde::de::Deserializer",
                __D,
                [],
                "deserialize_struct",
                [ Ty.path "move_core_types::metadata::_'1::deserialize::__Visitor" ]
              |),
              [
                M.read (| __deserializer |);
                M.read (| Value.String "Metadata" |);
                M.read (|
                  M.get_constant (| "move_core_types::metadata::_'1::deserialize::FIELDS" |)
                |);
                Value.StructRecord
                  "move_core_types::metadata::_'1::deserialize::__Visitor"
                  [
                    ("marker", Value.StructTuple "core::marker::PhantomData" []);
                    ("lifetime", Value.StructTuple "core::marker::PhantomData" [])
                  ]
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "serde::de::Deserialize"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("deserialize", InstanceField.Method deserialize) ].
    End Impl_serde_de_Deserialize_for_move_core_types_metadata_Metadata.
  End underscore.
  
End metadata.
