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

Module alloc.
  Parameter __rust_alloc : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function___rust_alloc : M.IsFunction "alloc::alloc::__rust_alloc" __rust_alloc.
  
  Parameter __rust_dealloc : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function___rust_dealloc : M.IsFunction "alloc::alloc::__rust_dealloc" __rust_dealloc.
  
  Parameter __rust_realloc : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function___rust_realloc : M.IsFunction "alloc::alloc::__rust_realloc" __rust_realloc.
  
  Parameter __rust_alloc_zeroed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function___rust_alloc_zeroed :
    M.IsFunction "alloc::alloc::__rust_alloc_zeroed" __rust_alloc_zeroed.
  
  Parameter __rust_no_alloc_shim_is_unstable : Value.t.
  
  (* StructTuple
    {
      name := "Global";
      const_params := [];
      ty_params := [];
      fields := [];
    } *)
  
  Module Impl_core_marker_Copy_for_alloc_alloc_Global.
    Definition Self : Ty.t := Ty.path "alloc::alloc::Global".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_alloc_alloc_Global.
  
  Module Impl_core_clone_Clone_for_alloc_alloc_Global.
    Definition Self : Ty.t := Ty.path "alloc::alloc::Global".
    
    (* 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_alloc_alloc_Global.
  
  Module Impl_core_default_Default_for_alloc_alloc_Global.
    Definition Self : Ty.t := Ty.path "alloc::alloc::Global".
    
    (* Default *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] => ltac:(M.monadic (Value.StructTuple "alloc::alloc::Global" []))
      | _, _, _ => 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_alloc_alloc_Global.
  
  Module Impl_core_fmt_Debug_for_alloc_alloc_Global.
    Definition Self : Ty.t := Ty.path "alloc::alloc::Global".
    
    (* 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 "Global" |) ]
          |)))
      | _, _, _ => 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_alloc_alloc_Global.
  
  (*
  pub unsafe fn alloc(layout: Layout) -> *mut u8 {
      unsafe {
          // Make sure we don't accidentally allow omitting the allocator shim in
          // stable code until it is actually stabilized.
          core::ptr::read_volatile(&__rust_no_alloc_shim_is_unstable);
  
          __rust_alloc(layout.size(), layout.align())
      }
  }
  *)
  Definition alloc (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ layout ] =>
      ltac:(M.monadic
        (let layout := M.alloc (| layout |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::ptr::read_volatile", [ Ty.path "u8" ] |),
                [ M.read (| M.get_constant (| "alloc::alloc::__rust_no_alloc_shim_is_unstable" |) |)
                ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_function (| "alloc::alloc::__rust_alloc", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::alloc::layout::Layout", "size", [] |),
                  [ layout ]
                |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::alloc::layout::Layout",
                    "align",
                    []
                  |),
                  [ layout ]
                |)
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_alloc : M.IsFunction "alloc::alloc::alloc" alloc.
  
  (*
  pub unsafe fn dealloc(ptr: *mut u8, layout: Layout) {
      unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) }
  }
  *)
  Definition dealloc (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ ptr; layout ] =>
      ltac:(M.monadic
        (let ptr := M.alloc (| ptr |) in
        let layout := M.alloc (| layout |) in
        M.call_closure (|
          M.get_function (| "alloc::alloc::__rust_dealloc", [] |),
          [
            M.read (| ptr |);
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::alloc::layout::Layout", "size", [] |),
              [ layout ]
            |);
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::alloc::layout::Layout", "align", [] |),
              [ layout ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_dealloc : M.IsFunction "alloc::alloc::dealloc" dealloc.
  
  (*
  pub unsafe fn realloc(ptr: *mut u8, layout: Layout, new_size: usize) -> *mut u8 {
      unsafe { __rust_realloc(ptr, layout.size(), layout.align(), new_size) }
  }
  *)
  Definition realloc (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ ptr; layout; new_size ] =>
      ltac:(M.monadic
        (let ptr := M.alloc (| ptr |) in
        let layout := M.alloc (| layout |) in
        let new_size := M.alloc (| new_size |) in
        M.call_closure (|
          M.get_function (| "alloc::alloc::__rust_realloc", [] |),
          [
            M.read (| ptr |);
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::alloc::layout::Layout", "size", [] |),
              [ layout ]
            |);
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::alloc::layout::Layout", "align", [] |),
              [ layout ]
            |);
            M.read (| new_size |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_realloc : M.IsFunction "alloc::alloc::realloc" realloc.
  
  (*
  pub unsafe fn alloc_zeroed(layout: Layout) -> *mut u8 {
      unsafe {
          // Make sure we don't accidentally allow omitting the allocator shim in
          // stable code until it is actually stabilized.
          core::ptr::read_volatile(&__rust_no_alloc_shim_is_unstable);
  
          __rust_alloc_zeroed(layout.size(), layout.align())
      }
  }
  *)
  Definition alloc_zeroed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ layout ] =>
      ltac:(M.monadic
        (let layout := M.alloc (| layout |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::ptr::read_volatile", [ Ty.path "u8" ] |),
                [ M.read (| M.get_constant (| "alloc::alloc::__rust_no_alloc_shim_is_unstable" |) |)
                ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_function (| "alloc::alloc::__rust_alloc_zeroed", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::alloc::layout::Layout", "size", [] |),
                  [ layout ]
                |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::alloc::layout::Layout",
                    "align",
                    []
                  |),
                  [ layout ]
                |)
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_alloc_zeroed : M.IsFunction "alloc::alloc::alloc_zeroed" alloc_zeroed.
  
  Module Impl_alloc_alloc_Global.
    Definition Self : Ty.t := Ty.path "alloc::alloc::Global".
    
    (*
        fn alloc_impl(&self, layout: Layout, zeroed: bool) -> Result<NonNull<[u8]>, AllocError> {
            match layout.size() {
                0 => Ok(NonNull::slice_from_raw_parts(layout.dangling(), 0)),
                // SAFETY: `layout` is non-zero in size,
                size => unsafe {
                    let raw_ptr = if zeroed { alloc_zeroed(layout) } else { alloc(layout) };
                    let ptr = NonNull::new(raw_ptr).ok_or(AllocError)?;
                    Ok(NonNull::slice_from_raw_parts(ptr, size))
                },
            }
        }
    *)
    Definition alloc_impl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; layout; zeroed ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let layout := M.alloc (| layout |) in
          let zeroed := M.alloc (| zeroed |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::alloc::layout::Layout",
                        "size",
                        []
                      |),
                      [ layout ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_constant_or_break_match (|
                            M.read (| γ |),
                            Value.Integer IntegerKind.Usize 0
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Ok"
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::ptr::non_null::NonNull")
                                    []
                                    [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                                  "slice_from_raw_parts",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::alloc::layout::Layout",
                                      "dangling",
                                      []
                                    |),
                                    [ layout ]
                                  |);
                                  Value.Integer IntegerKind.Usize 0
                                ]
                              |)
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let size := M.copy (| γ |) in
                        let~ raw_ptr :=
                          M.copy (|
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.use zeroed in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (| "alloc::alloc::alloc_zeroed", [] |),
                                        [ M.read (| layout |) ]
                                      |)
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      M.call_closure (|
                                        M.get_function (| "alloc::alloc::alloc", [] |),
                                        [ M.read (| layout |) ]
                                      |)
                                    |)))
                              ]
                            |)
                          |) in
                        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.path "u8" ];
                                        Ty.path "core::alloc::AllocError"
                                      ],
                                    [],
                                    "branch",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ Ty.path "u8" ]
                                          ],
                                        "ok_or",
                                        [ Ty.path "core::alloc::AllocError" ]
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ Ty.path "u8" ],
                                            "new",
                                            []
                                          |),
                                          [ M.read (| raw_ptr |) ]
                                        |);
                                        Value.StructTuple "core::alloc::AllocError" []
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                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
                        M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Ok"
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::ptr::non_null::NonNull")
                                    []
                                    [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                                  "slice_from_raw_parts",
                                  []
                                |),
                                [ M.read (| ptr |); M.read (| size |) ]
                              |)
                            ]
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_alloc_impl : M.IsAssociatedFunction Self "alloc_impl" alloc_impl.
    
    (*
        unsafe fn grow_impl(
            &self,
            ptr: NonNull<u8>,
            old_layout: Layout,
            new_layout: Layout,
            zeroed: bool,
        ) -> Result<NonNull<[u8]>, AllocError> {
            debug_assert!(
                new_layout.size() >= old_layout.size(),
                "`new_layout.size()` must be greater than or equal to `old_layout.size()`"
            );
    
            match old_layout.size() {
                0 => self.alloc_impl(new_layout, zeroed),
    
                // SAFETY: `new_size` is non-zero as `old_size` is greater than or equal to `new_size`
                // as required by safety conditions. Other conditions must be upheld by the caller
                old_size if old_layout.align() == new_layout.align() => unsafe {
                    let new_size = new_layout.size();
    
                    // `realloc` probably checks for `new_size >= old_layout.size()` or something similar.
                    hint::assert_unchecked(new_size >= old_layout.size());
    
                    let raw_ptr = realloc(ptr.as_ptr(), old_layout, new_size);
                    let ptr = NonNull::new(raw_ptr).ok_or(AllocError)?;
                    if zeroed {
                        raw_ptr.add(old_size).write_bytes(0, new_size - old_size);
                    }
                    Ok(NonNull::slice_from_raw_parts(ptr, new_size))
                },
    
                // SAFETY: because `new_layout.size()` must be greater than or equal to `old_size`,
                // both the old and new memory allocation are valid for reads and writes for `old_size`
                // bytes. Also, because the old allocation wasn't yet deallocated, it cannot overlap
                // `new_ptr`. Thus, the call to `copy_nonoverlapping` is safe. The safety contract
                // for `dealloc` must be upheld by the caller.
                old_size => unsafe {
                    let new_ptr = self.alloc_impl(new_layout, zeroed)?;
                    ptr::copy_nonoverlapping(ptr.as_ptr(), new_ptr.as_mut_ptr(), old_size);
                    self.deallocate(ptr, old_layout);
                    Ok(new_ptr)
                },
            }
        }
    *)
    Definition grow_impl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; ptr; old_layout; new_layout; zeroed ] =>
        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
          let zeroed := M.alloc (| zeroed |) 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
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::alloc::layout::Layout",
                        "size",
                        []
                      |),
                      [ old_layout ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_constant_or_break_match (|
                            M.read (| γ |),
                            Value.Integer IntegerKind.Usize 0
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "alloc::alloc::Global",
                              "alloc_impl",
                              []
                            |),
                            [ M.read (| self |); M.read (| new_layout |); M.read (| zeroed |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let old_size := M.copy (| γ |) in
                        let γ :=
                          M.alloc (|
                            BinOp.eq (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::alloc::layout::Layout",
                                  "align",
                                  []
                                |),
                                [ old_layout ]
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::alloc::layout::Layout",
                                  "align",
                                  []
                                |),
                                [ new_layout ]
                              |)
                            |)
                          |) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ new_size :=
                          M.alloc (|
                            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_function (| "core::hint::assert_unchecked", [] |),
                              [
                                BinOp.ge (|
                                  M.read (| new_size |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::alloc::layout::Layout",
                                      "size",
                                      []
                                    |),
                                    [ old_layout ]
                                  |)
                                |)
                              ]
                            |)
                          |) in
                        let~ raw_ptr :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (| "alloc::alloc::realloc", [] |),
                              [
                                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.read (| old_layout |);
                                M.read (| new_size |)
                              ]
                            |)
                          |) in
                        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.path "u8" ];
                                        Ty.path "core::alloc::AllocError"
                                      ],
                                    [],
                                    "branch",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ Ty.path "u8" ]
                                          ],
                                        "ok_or",
                                        [ Ty.path "core::alloc::AllocError" ]
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ Ty.path "u8" ],
                                            "new",
                                            []
                                          |),
                                          [ M.read (| raw_ptr |) ]
                                        |);
                                        Value.StructTuple "core::alloc::AllocError" []
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                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.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.use zeroed in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) 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 "*mut") [] [ Ty.path "u8" ],
                                              "add",
                                              []
                                            |),
                                            [ M.read (| raw_ptr |); M.read (| old_size |) ]
                                          |);
                                          Value.Integer IntegerKind.U8 0;
                                          BinOp.Wrap.sub (|
                                            M.read (| new_size |),
                                            M.read (| old_size |)
                                          |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Ok"
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::ptr::non_null::NonNull")
                                    []
                                    [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                                  "slice_from_raw_parts",
                                  []
                                |),
                                [ M.read (| ptr |); M.read (| new_size |) ]
                              |)
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let old_size := M.copy (| γ |) 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_associated_function (|
                                        Ty.path "alloc::alloc::Global",
                                        "alloc_impl",
                                        []
                                      |),
                                      [
                                        M.read (| self |);
                                        M.read (| new_layout |);
                                        M.read (| zeroed |)
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                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_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.read (| old_size |)
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::alloc::Allocator",
                                Ty.path "alloc::alloc::Global",
                                [],
                                "deallocate",
                                []
                              |),
                              [ M.read (| self |); M.read (| ptr |); M.read (| old_layout |) ]
                            |)
                          |) in
                        M.alloc (|
                          Value.StructTuple "core::result::Result::Ok" [ M.read (| new_ptr |) ]
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_grow_impl : M.IsAssociatedFunction Self "grow_impl" grow_impl.
  End Impl_alloc_alloc_Global.
  
  Module Impl_core_alloc_Allocator_for_alloc_alloc_Global.
    Definition Self : Ty.t := Ty.path "alloc::alloc::Global".
    
    (*
        fn allocate(&self, layout: Layout) -> Result<NonNull<[u8]>, AllocError> {
            self.alloc_impl(layout, false)
        }
    *)
    Definition allocate (ε : 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.call_closure (|
            M.get_associated_function (| Ty.path "alloc::alloc::Global", "alloc_impl", [] |),
            [ M.read (| self |); M.read (| layout |); Value.Bool false ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn allocate_zeroed(&self, layout: Layout) -> Result<NonNull<[u8]>, AllocError> {
            self.alloc_impl(layout, true)
        }
    *)
    Definition allocate_zeroed (ε : 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.call_closure (|
            M.get_associated_function (| Ty.path "alloc::alloc::Global", "alloc_impl", [] |),
            [ M.read (| self |); M.read (| layout |); Value.Bool true ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        unsafe fn deallocate(&self, ptr: NonNull<u8>, layout: Layout) {
            if layout.size() != 0 {
                // SAFETY: `layout` is non-zero in size,
                // other conditions must be upheld by the caller
                unsafe { dealloc(ptr.as_ptr(), layout) }
            }
        }
    *)
    Definition deallocate (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      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.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          BinOp.ne (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::alloc::layout::Layout",
                                "size",
                                []
                              |),
                              [ layout ]
                            |),
                            Value.Integer IntegerKind.Usize 0
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "alloc::alloc::dealloc", [] |),
                        [
                          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.read (| layout |)
                        ]
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => 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: all conditions must be upheld by the caller
            unsafe { self.grow_impl(ptr, old_layout, new_layout, false) }
        }
    *)
    Definition grow (ε : 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.call_closure (|
            M.get_associated_function (| Ty.path "alloc::alloc::Global", "grow_impl", [] |),
            [
              M.read (| self |);
              M.read (| ptr |);
              M.read (| old_layout |);
              M.read (| new_layout |);
              Value.Bool false
            ]
          |)))
      | _, _, _ => 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: all conditions must be upheld by the caller
            unsafe { self.grow_impl(ptr, old_layout, new_layout, true) }
        }
    *)
    Definition grow_zeroed (ε : 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.call_closure (|
            M.get_associated_function (| Ty.path "alloc::alloc::Global", "grow_impl", [] |),
            [
              M.read (| self |);
              M.read (| ptr |);
              M.read (| old_layout |);
              M.read (| new_layout |);
              Value.Bool true
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        unsafe fn shrink(
            &self,
            ptr: NonNull<u8>,
            old_layout: Layout,
            new_layout: Layout,
        ) -> Result<NonNull<[u8]>, AllocError> {
            debug_assert!(
                new_layout.size() <= old_layout.size(),
                "`new_layout.size()` must be smaller than or equal to `old_layout.size()`"
            );
    
            match new_layout.size() {
                // SAFETY: conditions must be upheld by the caller
                0 => unsafe {
                    self.deallocate(ptr, old_layout);
                    Ok(NonNull::slice_from_raw_parts(new_layout.dangling(), 0))
                },
    
                // SAFETY: `new_size` is non-zero. Other conditions must be upheld by the caller
                new_size if old_layout.align() == new_layout.align() => unsafe {
                    // `realloc` probably checks for `new_size <= old_layout.size()` or something similar.
                    hint::assert_unchecked(new_size <= old_layout.size());
    
                    let raw_ptr = realloc(ptr.as_ptr(), old_layout, new_size);
                    let ptr = NonNull::new(raw_ptr).ok_or(AllocError)?;
                    Ok(NonNull::slice_from_raw_parts(ptr, new_size))
                },
    
                // SAFETY: because `new_size` must be smaller than or equal to `old_layout.size()`,
                // both the old and new memory allocation are valid for reads and writes for `new_size`
                // bytes. Also, because the old allocation wasn't yet deallocated, it cannot overlap
                // `new_ptr`. Thus, the call to `copy_nonoverlapping` is safe. The safety contract
                // for `dealloc` must be upheld by the caller.
                new_size => unsafe {
                    let new_ptr = self.allocate(new_layout)?;
                    ptr::copy_nonoverlapping(ptr.as_ptr(), new_ptr.as_mut_ptr(), new_size);
                    self.deallocate(ptr, old_layout);
                    Ok(new_ptr)
                },
            }
        }
    *)
    Definition shrink (ε : 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
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::alloc::layout::Layout",
                        "size",
                        []
                      |),
                      [ new_layout ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_constant_or_break_match (|
                            M.read (| γ |),
                            Value.Integer IntegerKind.Usize 0
                          |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::alloc::Allocator",
                                Ty.path "alloc::alloc::Global",
                                [],
                                "deallocate",
                                []
                              |),
                              [ M.read (| self |); M.read (| ptr |); M.read (| old_layout |) ]
                            |)
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Ok"
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::ptr::non_null::NonNull")
                                    []
                                    [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                                  "slice_from_raw_parts",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::alloc::layout::Layout",
                                      "dangling",
                                      []
                                    |),
                                    [ new_layout ]
                                  |);
                                  Value.Integer IntegerKind.Usize 0
                                ]
                              |)
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let new_size := M.copy (| γ |) in
                        let γ :=
                          M.alloc (|
                            BinOp.eq (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::alloc::layout::Layout",
                                  "align",
                                  []
                                |),
                                [ old_layout ]
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::alloc::layout::Layout",
                                  "align",
                                  []
                                |),
                                [ new_layout ]
                              |)
                            |)
                          |) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (| "core::hint::assert_unchecked", [] |),
                              [
                                BinOp.le (|
                                  M.read (| new_size |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::alloc::layout::Layout",
                                      "size",
                                      []
                                    |),
                                    [ old_layout ]
                                  |)
                                |)
                              ]
                            |)
                          |) in
                        let~ raw_ptr :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (| "alloc::alloc::realloc", [] |),
                              [
                                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.read (| old_layout |);
                                M.read (| new_size |)
                              ]
                            |)
                          |) in
                        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.path "u8" ];
                                        Ty.path "core::alloc::AllocError"
                                      ],
                                    [],
                                    "branch",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ Ty.path "u8" ]
                                          ],
                                        "ok_or",
                                        [ Ty.path "core::alloc::AllocError" ]
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ Ty.path "u8" ],
                                            "new",
                                            []
                                          |),
                                          [ M.read (| raw_ptr |) ]
                                        |);
                                        Value.StructTuple "core::alloc::AllocError" []
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                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
                        M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Ok"
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::ptr::non_null::NonNull")
                                    []
                                    [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                                  "slice_from_raw_parts",
                                  []
                                |),
                                [ M.read (| ptr |); M.read (| new_size |) ]
                              |)
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let new_size := M.copy (| γ |) 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",
                                        Ty.path "alloc::alloc::Global",
                                        [],
                                        "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~ _ :=
                          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.read (| new_size |)
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::alloc::Allocator",
                                Ty.path "alloc::alloc::Global",
                                [],
                                "deallocate",
                                []
                              |),
                              [ M.read (| self |); M.read (| ptr |); M.read (| old_layout |) ]
                            |)
                          |) in
                        M.alloc (|
                          Value.StructTuple "core::result::Result::Ok" [ M.read (| new_ptr |) ]
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::alloc::Allocator"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("allocate", InstanceField.Method allocate);
          ("allocate_zeroed", InstanceField.Method allocate_zeroed);
          ("deallocate", InstanceField.Method deallocate);
          ("grow", InstanceField.Method grow);
          ("grow_zeroed", InstanceField.Method grow_zeroed);
          ("shrink", InstanceField.Method shrink)
        ].
  End Impl_core_alloc_Allocator_for_alloc_alloc_Global.
  
  (*
  unsafe fn exchange_malloc(size: usize, align: usize) -> *mut u8 {
      let layout = unsafe { Layout::from_size_align_unchecked(size, align) };
      match Global.allocate(layout) {
          Ok(ptr) => ptr.as_mut_ptr(),
          Err(_) => handle_alloc_error(layout),
      }
  }
  *)
  Definition exchange_malloc (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ size; align ] =>
      ltac:(M.monadic
        (let size := M.alloc (| size |) in
        let align := M.alloc (| align |) in
        M.read (|
          let~ layout :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::alloc::layout::Layout",
                  "from_size_align_unchecked",
                  []
                |),
                [ M.read (| size |); M.read (| align |) ]
              |)
            |) in
          M.match_operator (|
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::alloc::Allocator",
                  Ty.path "alloc::alloc::Global",
                  [],
                  "allocate",
                  []
                |),
                [ M.alloc (| Value.StructTuple "alloc::alloc::Global" [] |); M.read (| layout |) ]
              |)
            |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                  let ptr := M.copy (| γ0_0 |) in
                  M.alloc (|
                    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 (| ptr |) ]
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                  M.alloc (|
                    M.never_to_any (|
                      M.call_closure (|
                        M.get_function (| "alloc::alloc::handle_alloc_error", [] |),
                        [ M.read (| layout |) ]
                      |)
                    |)
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_exchange_malloc : M.IsFunction "alloc::alloc::exchange_malloc" exchange_malloc.
  
  Parameter __rust_alloc_error_handler : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Function___rust_alloc_error_handler :
    M.IsFunction "alloc::alloc::__rust_alloc_error_handler" __rust_alloc_error_handler.
  
  (*
  pub const fn handle_alloc_error(layout: Layout) -> ! {
      const fn ct_error(_: Layout) -> ! {
          panic!("allocation failed");
      }
  
      #[inline]
      fn rt_error(layout: Layout) -> ! {
          unsafe {
              __rust_alloc_error_handler(layout.size(), layout.align());
          }
      }
  
      #[cfg(not(feature = "panic_immediate_abort"))]
      {
          core::intrinsics::const_eval_select((layout,), ct_error, rt_error)
      }
  
      #[cfg(feature = "panic_immediate_abort")]
      ct_error(layout)
  }
  *)
  Definition handle_alloc_error (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ layout ] =>
      ltac:(M.monadic
        (let layout := M.alloc (| layout |) in
        M.call_closure (|
          M.get_function (|
            "core::intrinsics::const_eval_select",
            [
              Ty.tuple [ Ty.path "core::alloc::layout::Layout" ];
              Ty.function [ Ty.path "core::alloc::layout::Layout" ] (Ty.path "never");
              Ty.function [ Ty.path "core::alloc::layout::Layout" ] (Ty.path "never");
              Ty.path "never"
            ]
          |),
          [
            Value.Tuple [ M.read (| layout |) ];
            M.get_function (| "alloc::alloc::handle_alloc_error.ct_error", [] |);
            M.get_function (| "alloc::alloc::handle_alloc_error.rt_error", [] |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_handle_alloc_error :
    M.IsFunction "alloc::alloc::handle_alloc_error" handle_alloc_error.
  
  Module handle_alloc_error.
    (*
        const fn ct_error(_: Layout) -> ! {
            panic!("allocation failed");
        }
    *)
    Definition ct_error (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ β0 ] =>
        ltac:(M.monadic
          (let β0 := M.alloc (| β0 |) in
          M.match_operator (|
            β0,
            [
              fun γ =>
                ltac:(M.monadic
                  (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 "allocation failed" |) ]
                          |)
                        ]
                      |)
                    ]
                  |)))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_ct_error : M.IsFunction "alloc::alloc::handle_alloc_error::ct_error" ct_error.
    
    (*
        fn rt_error(layout: Layout) -> ! {
            unsafe {
                __rust_alloc_error_handler(layout.size(), layout.align());
            }
        }
    *)
    Definition rt_error (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ layout ] =>
        ltac:(M.monadic
          (let layout := M.alloc (| layout |) in
          M.call_closure (|
            M.get_function (| "alloc::alloc::__rust_alloc_error_handler", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::alloc::layout::Layout", "size", [] |),
                [ layout ]
              |);
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::alloc::layout::Layout", "align", [] |),
                [ layout ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_rt_error : M.IsFunction "alloc::alloc::handle_alloc_error::rt_error" rt_error.
  End handle_alloc_error.
  
  Module __alloc_error_handler.
    (*
        pub unsafe fn __rdl_oom(size: usize, _align: usize) -> ! {
            extern "Rust" {
                // This symbol is emitted by rustc next to __rust_alloc_error_handler.
                // Its value depends on the -Zoom={panic,abort} compiler option.
                static __rust_alloc_error_handler_should_panic: u8;
            }
    
            if unsafe { __rust_alloc_error_handler_should_panic != 0 } {
                panic!("memory allocation of {size} bytes failed")
            } else {
                core::panicking::panic_nounwind_fmt(
                    format_args!("memory allocation of {size} bytes failed"),
                    /* force_no_backtrace */ false,
                )
            }
        }
    *)
    Definition __rdl_oom (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ size; _align ] =>
        ltac:(M.monadic
          (let size := M.alloc (| size |) in
          let _align := M.alloc (| _align |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          BinOp.ne (|
                            M.read (|
                              M.read (|
                                M.get_constant (|
                                  "alloc::alloc::__alloc_error_handler::__rdl_oom::__rust_alloc_error_handler_should_panic"
                                |)
                              |)
                            |),
                            Value.Integer IntegerKind.U8 0
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::panicking::panic_fmt", [] |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [
                                    M.read (| Value.String "memory allocation of " |);
                                    M.read (| Value.String " bytes failed" |)
                                  ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [ Ty.path "usize" ]
                                      |),
                                      [ size ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::panicking::panic_nounwind_fmt", [] |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [
                                    M.read (| Value.String "memory allocation of " |);
                                    M.read (| Value.String " bytes failed" |)
                                  ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [ Ty.path "usize" ]
                                      |),
                                      [ size ]
                                    |)
                                  ]
                              |)
                            ]
                          |);
                          Value.Bool false
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function___rdl_oom :
      M.IsFunction "alloc::alloc::__alloc_error_handler::__rdl_oom" __rdl_oom.
    
    Module __rdl_oom.
      Parameter __rust_alloc_error_handler_should_panic : Value.t.
    End __rdl_oom.
  End __alloc_error_handler.
End alloc.
