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

Module alloc.
  (* StructTuple
    {
      name := "AllocError";
      const_params := [];
      ty_params := [];
      fields := [];
    } *)
  
  Module Impl_core_marker_Copy_for_core_alloc_AllocError.
    Definition Self : Ty.t := Ty.path "core::alloc::AllocError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_core_alloc_AllocError.
  
  Module Impl_core_clone_Clone_for_core_alloc_AllocError.
    Definition Self : Ty.t := Ty.path "core::alloc::AllocError".
    
    (* 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.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_core_alloc_AllocError.
  
  Module Impl_core_marker_StructuralPartialEq_for_core_alloc_AllocError.
    Definition Self : Ty.t := Ty.path "core::alloc::AllocError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_core_alloc_AllocError.
  
  Module Impl_core_cmp_PartialEq_for_core_alloc_AllocError.
    Definition Self : Ty.t := Ty.path "core::alloc::AllocError".
    
    (* 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
          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_core_alloc_AllocError.
  
  Module Impl_core_cmp_Eq_for_core_alloc_AllocError.
    Definition Self : Ty.t := Ty.path "core::alloc::AllocError".
    
    (* 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_core_alloc_AllocError.
  
  Module Impl_core_fmt_Debug_for_core_alloc_AllocError.
    Definition Self : Ty.t := Ty.path "core::alloc::AllocError".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
            [ M.read (| f |); M.read (| Value.String "AllocError" |) ]
          |)))
      | _, _, _ => 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_core_alloc_AllocError.
  
  Module Impl_core_error_Error_for_core_alloc_AllocError.
    Definition Self : Ty.t := Ty.path "core::alloc::AllocError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_error_Error_for_core_alloc_AllocError.
  
  Module Impl_core_fmt_Display_for_core_alloc_AllocError.
    Definition Self : Ty.t := Ty.path "core::alloc::AllocError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            f.write_str("memory allocation failed")
        }
    *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
            [ M.read (| f |); M.read (| Value.String "memory allocation failed" |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Display"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Display_for_core_alloc_AllocError.
  
  (* Trait *)
  Module Allocator.
    Definition allocate_zeroed
        (Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self; layout ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let layout := M.alloc (| layout |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ ptr :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::ptr::non_null::NonNull")
                                  []
                                  [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                                Ty.path "core::alloc::AllocError"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::alloc::Allocator",
                                Self,
                                [],
                                "allocate",
                                []
                              |),
                              [ M.read (| self |); M.read (| layout |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                                            Ty.path "core::alloc::AllocError"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "core::alloc::AllocError"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "*mut") [] [ Ty.path "u8" ],
                        "write_bytes",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ Ty.path "u8" ],
                            "as_ptr",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::ptr::non_null::NonNull")
                                  []
                                  [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                                "as_non_null_ptr",
                                []
                              |),
                              [ M.read (| ptr |) ]
                            |)
                          ]
                        |);
                        Value.Integer IntegerKind.U8 0;
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::ptr::non_null::NonNull")
                              []
                              [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                            "len",
                            []
                          |),
                          [ M.read (| ptr |) ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| ptr |) ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_allocate_zeroed :
      M.IsProvidedMethod "core::alloc::Allocator" "allocate_zeroed" allocate_zeroed.
    Definition grow (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; ptr; old_layout; new_layout ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let ptr := M.alloc (| ptr |) in
          let old_layout := M.alloc (| old_layout |) in
          let new_layout := M.alloc (| new_layout |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use (M.alloc (| Value.Bool true |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          UnOp.not (|
                                            BinOp.ge (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::alloc::layout::Layout",
                                                  "size",
                                                  []
                                                |),
                                                [ new_layout ]
                                              |),
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::alloc::layout::Layout",
                                                  "size",
                                                  []
                                                |),
                                                [ old_layout ]
                                              |)
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.call_closure (|
                                          M.get_function (| "core::panicking::panic_fmt", [] |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "core::fmt::Arguments",
                                                "new_const",
                                                []
                                              |),
                                              [
                                                M.alloc (|
                                                  Value.Array
                                                    [
                                                      M.read (|
                                                        Value.String
                                                          "`new_layout.size()` must be greater than or equal to `old_layout.size()`"
                                                      |)
                                                    ]
                                                |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ new_ptr :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::ptr::non_null::NonNull")
                                  []
                                  [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                                Ty.path "core::alloc::AllocError"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::alloc::Allocator",
                                Self,
                                [],
                                "allocate",
                                []
                              |),
                              [ M.read (| self |); M.read (| new_layout |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                                            Ty.path "core::alloc::AllocError"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "core::alloc::AllocError"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |)
                  |) in
                let~ _ :=
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::intrinsics::copy_nonoverlapping",
                          [ Ty.path "u8" ]
                        |),
                        [
                          (* MutToConstPointer *)
                          M.pointer_coercion
                            (M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::ptr::non_null::NonNull")
                                  []
                                  [ Ty.path "u8" ],
                                "as_ptr",
                                []
                              |),
                              [ M.read (| ptr |) ]
                            |));
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::ptr::non_null::NonNull")
                                []
                                [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                              "as_mut_ptr",
                              []
                            |),
                            [ M.read (| new_ptr |) ]
                          |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::alloc::layout::Layout",
                              "size",
                              []
                            |),
                            [ old_layout ]
                          |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::alloc::Allocator",
                          Self,
                          [],
                          "deallocate",
                          []
                        |),
                        [ M.read (| self |); M.read (| ptr |); M.read (| old_layout |) ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| new_ptr |) ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_grow : M.IsProvidedMethod "core::alloc::Allocator" "grow" grow.
    Definition grow_zeroed
        (Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self; ptr; old_layout; new_layout ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let ptr := M.alloc (| ptr |) in
          let old_layout := M.alloc (| old_layout |) in
          let new_layout := M.alloc (| new_layout |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use (M.alloc (| Value.Bool true |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          UnOp.not (|
                                            BinOp.ge (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::alloc::layout::Layout",
                                                  "size",
                                                  []
                                                |),
                                                [ new_layout ]
                                              |),
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::alloc::layout::Layout",
                                                  "size",
                                                  []
                                                |),
                                                [ old_layout ]
                                              |)
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.call_closure (|
                                          M.get_function (| "core::panicking::panic_fmt", [] |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "core::fmt::Arguments",
                                                "new_const",
                                                []
                                              |),
                                              [
                                                M.alloc (|
                                                  Value.Array
                                                    [
                                                      M.read (|
                                                        Value.String
                                                          "`new_layout.size()` must be greater than or equal to `old_layout.size()`"
                                                      |)
                                                    ]
                                                |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ new_ptr :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::ptr::non_null::NonNull")
                                  []
                                  [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                                Ty.path "core::alloc::AllocError"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::alloc::Allocator",
                                Self,
                                [],
                                "allocate_zeroed",
                                []
                              |),
                              [ M.read (| self |); M.read (| new_layout |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                                            Ty.path "core::alloc::AllocError"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "core::alloc::AllocError"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |)
                  |) in
                let~ _ :=
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::intrinsics::copy_nonoverlapping",
                          [ Ty.path "u8" ]
                        |),
                        [
                          (* MutToConstPointer *)
                          M.pointer_coercion
                            (M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::ptr::non_null::NonNull")
                                  []
                                  [ Ty.path "u8" ],
                                "as_ptr",
                                []
                              |),
                              [ M.read (| ptr |) ]
                            |));
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::ptr::non_null::NonNull")
                                []
                                [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                              "as_mut_ptr",
                              []
                            |),
                            [ M.read (| new_ptr |) ]
                          |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::alloc::layout::Layout",
                              "size",
                              []
                            |),
                            [ old_layout ]
                          |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::alloc::Allocator",
                          Self,
                          [],
                          "deallocate",
                          []
                        |),
                        [ M.read (| self |); M.read (| ptr |); M.read (| old_layout |) ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| new_ptr |) ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_grow_zeroed :
      M.IsProvidedMethod "core::alloc::Allocator" "grow_zeroed" grow_zeroed.
    Definition shrink (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; ptr; old_layout; new_layout ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let ptr := M.alloc (| ptr |) in
          let old_layout := M.alloc (| old_layout |) in
          let new_layout := M.alloc (| new_layout |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use (M.alloc (| Value.Bool true |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          UnOp.not (|
                                            BinOp.le (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::alloc::layout::Layout",
                                                  "size",
                                                  []
                                                |),
                                                [ new_layout ]
                                              |),
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::alloc::layout::Layout",
                                                  "size",
                                                  []
                                                |),
                                                [ old_layout ]
                                              |)
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.call_closure (|
                                          M.get_function (| "core::panicking::panic_fmt", [] |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "core::fmt::Arguments",
                                                "new_const",
                                                []
                                              |),
                                              [
                                                M.alloc (|
                                                  Value.Array
                                                    [
                                                      M.read (|
                                                        Value.String
                                                          "`new_layout.size()` must be smaller than or equal to `old_layout.size()`"
                                                      |)
                                                    ]
                                                |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ new_ptr :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::ptr::non_null::NonNull")
                                  []
                                  [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                                Ty.path "core::alloc::AllocError"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::alloc::Allocator",
                                Self,
                                [],
                                "allocate",
                                []
                              |),
                              [ M.read (| self |); M.read (| new_layout |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
                                            Ty.path "core::alloc::AllocError"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "core::alloc::AllocError"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |)
                  |) in
                let~ _ :=
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::intrinsics::copy_nonoverlapping",
                          [ Ty.path "u8" ]
                        |),
                        [
                          (* MutToConstPointer *)
                          M.pointer_coercion
                            (M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::ptr::non_null::NonNull")
                                  []
                                  [ Ty.path "u8" ],
                                "as_ptr",
                                []
                              |),
                              [ M.read (| ptr |) ]
                            |));
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::ptr::non_null::NonNull")
                                []
                                [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                              "as_mut_ptr",
                              []
                            |),
                            [ M.read (| new_ptr |) ]
                          |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::alloc::layout::Layout",
                              "size",
                              []
                            |),
                            [ new_layout ]
                          |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::alloc::Allocator",
                          Self,
                          [],
                          "deallocate",
                          []
                        |),
                        [ M.read (| self |); M.read (| ptr |); M.read (| old_layout |) ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| new_ptr |) ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_shrink : M.IsProvidedMethod "core::alloc::Allocator" "shrink" shrink.
    Definition by_ref (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| self |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_by_ref : M.IsProvidedMethod "core::alloc::Allocator" "by_ref" by_ref.
  End Allocator.
  
  Module Impl_core_alloc_Allocator_where_core_alloc_Allocator_A_where_core_marker_Sized_A_for_ref__A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ A ].
    
    (*
        fn allocate(&self, layout: Layout) -> Result<NonNull<[u8]>, AllocError> {
            ( **self).allocate(layout)
        }
    *)
    Definition allocate (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self; layout ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let layout := M.alloc (| layout |) in
          M.call_closure (|
            M.get_trait_method (| "core::alloc::Allocator", A, [], "allocate", [] |),
            [ M.read (| M.read (| self |) |); M.read (| layout |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn allocate_zeroed(&self, layout: Layout) -> Result<NonNull<[u8]>, AllocError> {
            ( **self).allocate_zeroed(layout)
        }
    *)
    Definition allocate_zeroed
        (A : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self; layout ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let layout := M.alloc (| layout |) in
          M.call_closure (|
            M.get_trait_method (| "core::alloc::Allocator", A, [], "allocate_zeroed", [] |),
            [ M.read (| M.read (| self |) |); M.read (| layout |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        unsafe fn deallocate(&self, ptr: NonNull<u8>, layout: Layout) {
            // SAFETY: the safety contract must be upheld by the caller
            unsafe { ( **self).deallocate(ptr, layout) }
        }
    *)
    Definition deallocate (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self; ptr; layout ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let ptr := M.alloc (| ptr |) in
          let layout := M.alloc (| layout |) in
          M.call_closure (|
            M.get_trait_method (| "core::alloc::Allocator", A, [], "deallocate", [] |),
            [ M.read (| M.read (| self |) |); M.read (| ptr |); M.read (| layout |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        unsafe fn grow(
            &self,
            ptr: NonNull<u8>,
            old_layout: Layout,
            new_layout: Layout,
        ) -> Result<NonNull<[u8]>, AllocError> {
            // SAFETY: the safety contract must be upheld by the caller
            unsafe { ( **self).grow(ptr, old_layout, new_layout) }
        }
    *)
    Definition grow (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self; ptr; old_layout; new_layout ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let ptr := M.alloc (| ptr |) in
          let old_layout := M.alloc (| old_layout |) in
          let new_layout := M.alloc (| new_layout |) in
          M.call_closure (|
            M.get_trait_method (| "core::alloc::Allocator", A, [], "grow", [] |),
            [
              M.read (| M.read (| self |) |);
              M.read (| ptr |);
              M.read (| old_layout |);
              M.read (| new_layout |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        unsafe fn grow_zeroed(
            &self,
            ptr: NonNull<u8>,
            old_layout: Layout,
            new_layout: Layout,
        ) -> Result<NonNull<[u8]>, AllocError> {
            // SAFETY: the safety contract must be upheld by the caller
            unsafe { ( **self).grow_zeroed(ptr, old_layout, new_layout) }
        }
    *)
    Definition grow_zeroed (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self; ptr; old_layout; new_layout ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let ptr := M.alloc (| ptr |) in
          let old_layout := M.alloc (| old_layout |) in
          let new_layout := M.alloc (| new_layout |) in
          M.call_closure (|
            M.get_trait_method (| "core::alloc::Allocator", A, [], "grow_zeroed", [] |),
            [
              M.read (| M.read (| self |) |);
              M.read (| ptr |);
              M.read (| old_layout |);
              M.read (| new_layout |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        unsafe fn shrink(
            &self,
            ptr: NonNull<u8>,
            old_layout: Layout,
            new_layout: Layout,
        ) -> Result<NonNull<[u8]>, AllocError> {
            // SAFETY: the safety contract must be upheld by the caller
            unsafe { ( **self).shrink(ptr, old_layout, new_layout) }
        }
    *)
    Definition shrink (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self; ptr; old_layout; new_layout ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let ptr := M.alloc (| ptr |) in
          let old_layout := M.alloc (| old_layout |) in
          let new_layout := M.alloc (| new_layout |) in
          M.call_closure (|
            M.get_trait_method (| "core::alloc::Allocator", A, [], "shrink", [] |),
            [
              M.read (| M.read (| self |) |);
              M.read (| ptr |);
              M.read (| old_layout |);
              M.read (| new_layout |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::alloc::Allocator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("allocate", InstanceField.Method (allocate A));
          ("allocate_zeroed", InstanceField.Method (allocate_zeroed A));
          ("deallocate", InstanceField.Method (deallocate A));
          ("grow", InstanceField.Method (grow A));
          ("grow_zeroed", InstanceField.Method (grow_zeroed A));
          ("shrink", InstanceField.Method (shrink A))
        ].
  End Impl_core_alloc_Allocator_where_core_alloc_Allocator_A_where_core_marker_Sized_A_for_ref__A.
End alloc.
