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

Module alloc.
  Module layout.
    (*
    const fn size_align<T>() -> (usize, usize) {
        (mem::size_of::<T>(), mem::align_of::<T>())
    }
    *)
    Definition size_align (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [] =>
        ltac:(M.monadic
          (Value.Tuple
            [
              M.call_closure (| M.get_function (| "core::mem::size_of", [ T ] |), [] |);
              M.call_closure (| M.get_function (| "core::mem::align_of", [ T ] |), [] |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_size_align : M.IsFunction "core::alloc::layout::size_align" size_align.
    
    (* StructRecord
      {
        name := "Layout";
        const_params := [];
        ty_params := [];
        fields :=
          [ ("size", Ty.path "usize"); ("align", Ty.path "core::ptr::alignment::Alignment") ];
      } *)
    
    Module Impl_core_marker_Copy_for_core_alloc_layout_Layout.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::Layout".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_alloc_layout_Layout.
    
    Module Impl_core_clone_Clone_for_core_alloc_layout_Layout.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::Layout".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        Value.DeclaredButUndefined,
                        [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_alloc_layout_Layout.
    
    Module Impl_core_fmt_Debug_for_core_alloc_layout_Layout.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::Layout".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_struct_field2_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "Layout" |);
                M.read (| Value.String "size" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::alloc::layout::Layout",
                  "size"
                |);
                M.read (| Value.String "align" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::alloc::layout::Layout",
                    "align"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_alloc_layout_Layout.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_alloc_layout_Layout.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::Layout".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_alloc_layout_Layout.
    
    Module Impl_core_cmp_PartialEq_for_core_alloc_layout_Layout.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::Layout".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            LogicalOp.and (|
              BinOp.eq (|
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::alloc::layout::Layout",
                    "size"
                  |)
                |),
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "core::alloc::layout::Layout",
                    "size"
                  |)
                |)
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.path "core::ptr::alignment::Alignment",
                    [ Ty.path "core::ptr::alignment::Alignment" ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::alloc::layout::Layout",
                      "align"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "core::alloc::layout::Layout",
                      "align"
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_alloc_layout_Layout.
    
    Module Impl_core_cmp_Eq_for_core_alloc_layout_Layout.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::Layout".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        Value.DeclaredButUndefined,
                        [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_alloc_layout_Layout.
    
    Module Impl_core_hash_Hash_for_core_alloc_layout_Layout.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::Layout".
      
      (* Hash *)
      Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ __H ], [ self; state ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let state := M.alloc (| state |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::hash::Hash",
                      Ty.path "usize",
                      [],
                      "hash",
                      [ __H ]
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::alloc::layout::Layout",
                        "size"
                      |);
                      M.read (| state |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::hash::Hash",
                    Ty.path "core::ptr::alignment::Alignment",
                    [],
                    "hash",
                    [ __H ]
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::alloc::layout::Layout",
                      "align"
                    |);
                    M.read (| state |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::hash::Hash"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("hash", InstanceField.Method hash) ].
    End Impl_core_hash_Hash_for_core_alloc_layout_Layout.
    
    Module Impl_core_alloc_layout_Layout.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::Layout".
      
      (*
          pub const fn from_size_align(size: usize, align: usize) -> Result<Self, LayoutError> {
              if Layout::is_size_align_valid(size, align) {
                  // SAFETY: Layout::is_size_align_valid checks the preconditions for this call.
                  unsafe { Ok(Layout { size, align: mem::transmute(align) }) }
              } else {
                  Err(LayoutError)
              }
          }
      *)
      Definition from_size_align (ε : 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 (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::alloc::layout::Layout",
                                "is_size_align_valid",
                                []
                              |),
                              [ M.read (| size |); M.read (| align |) ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Ok"
                          [
                            Value.StructRecord
                              "core::alloc::layout::Layout"
                              [
                                ("size", M.read (| size |));
                                ("align",
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::intrinsics::transmute",
                                      [ Ty.path "usize"; Ty.path "core::ptr::alignment::Alignment" ]
                                    |),
                                    [ M.read (| align |) ]
                                  |))
                              ]
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [ Value.StructTuple "core::alloc::layout::LayoutError" [] ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_size_align :
        M.IsAssociatedFunction Self "from_size_align" from_size_align.
      
      (*
          const fn is_size_align_valid(size: usize, align: usize) -> bool {
              let Some(align) = Alignment::new(align) else { return false };
              if size > Self::max_size_for_align(align) {
                  return false;
              }
              true
          }
      *)
      Definition is_size_align_valid (ε : 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.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::ptr::alignment::Alignment",
                          "new",
                          []
                        |),
                        [ M.read (| align |) ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let align := M.copy (| γ0_0 |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.gt (|
                                            M.read (| size |),
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "core::alloc::layout::Layout",
                                                "max_size_for_align",
                                                []
                                              |),
                                              [ M.read (| align |) ]
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.read (| M.return_ (| Value.Bool false |) |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (| Value.Bool true |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_size_align_valid :
        M.IsAssociatedFunction Self "is_size_align_valid" is_size_align_valid.
      
      (*
          const fn max_size_for_align(align: Alignment) -> usize {
              // (power-of-two implies align != 0.)
      
              // Rounded up size is:
              //   size_rounded_up = (size + align - 1) & !(align - 1);
              //
              // We know from above that align != 0. If adding (align - 1)
              // does not overflow, then rounding up will be fine.
              //
              // Conversely, &-masking with !(align - 1) will subtract off
              // only low-order-bits. Thus if overflow occurs with the sum,
              // the &-mask cannot subtract enough to undo that overflow.
              //
              // Above implies that checking for summation overflow is both
              // necessary and sufficient.
      
              // SAFETY: the maximum possible alignment is `isize::MAX + 1`,
              // so the subtraction cannot overflow.
              unsafe { unchecked_sub(isize::MAX as usize + 1, align.as_usize()) }
          }
      *)
      Definition max_size_for_align (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ align ] =>
          ltac:(M.monadic
            (let align := M.alloc (| align |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::unchecked_sub", [ Ty.path "usize" ] |),
              [
                BinOp.Wrap.add (|
                  M.rust_cast (M.read (| M.get_constant (| "core::num::MAX" |) |)),
                  Value.Integer IntegerKind.Usize 1
                |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::ptr::alignment::Alignment",
                    "as_usize",
                    []
                  |),
                  [ M.read (| align |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_max_size_for_align :
        M.IsAssociatedFunction Self "max_size_for_align" max_size_for_align.
      
      (*
          const fn from_size_alignment(size: usize, align: Alignment) -> Result<Self, LayoutError> {
              if size > Self::max_size_for_align(align) {
                  return Err(LayoutError);
              }
      
              // SAFETY: Layout::size invariants checked above.
              Ok(Layout { size, align })
          }
      *)
      Definition from_size_alignment (ε : 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.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.gt (|
                                    M.read (| size |),
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::alloc::layout::Layout",
                                        "max_size_for_align",
                                        []
                                      |),
                                      [ M.read (| align |) ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Err"
                                      [ Value.StructTuple "core::alloc::layout::LayoutError" [] ]
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Ok"
                      [
                        Value.StructRecord
                          "core::alloc::layout::Layout"
                          [ ("size", M.read (| size |)); ("align", M.read (| align |)) ]
                      ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_size_alignment :
        M.IsAssociatedFunction Self "from_size_alignment" from_size_alignment.
      
      (*
          pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self {
              assert_unsafe_precondition!(
                  check_library_ub,
                  "Layout::from_size_align_unchecked requires that align is a power of 2 \
                  and the rounded-up allocation size does not exceed isize::MAX",
                  (
                      size: usize = size,
                      align: usize = align,
                  ) => Layout::is_size_align_valid(size, align)
              );
              // SAFETY: the caller is required to uphold the preconditions.
              unsafe { Layout { size, align: mem::transmute(align) } }
          }
      *)
      Definition from_size_align_unchecked
          (ε : 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~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::ub_checks", [] |),
                                []
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Self,
                                "precondition_check.from_size_align_unchecked",
                                []
                              |),
                              [ M.read (| size |); M.read (| align |) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                Value.StructRecord
                  "core::alloc::layout::Layout"
                  [
                    ("size", M.read (| size |));
                    ("align",
                      M.call_closure (|
                        M.get_function (|
                          "core::intrinsics::transmute",
                          [ Ty.path "usize"; Ty.path "core::ptr::alignment::Alignment" ]
                        |),
                        [ M.read (| align |) ]
                      |))
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_size_align_unchecked :
        M.IsAssociatedFunction Self "from_size_align_unchecked" from_size_align_unchecked.
      
      (*
          pub const fn size(&self) -> usize {
              self.size
          }
      *)
      Definition size (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::alloc::layout::Layout",
                "size"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_size : M.IsAssociatedFunction Self "size" size.
      
      (*
          pub const fn align(&self) -> usize {
              self.align.as_usize()
          }
      *)
      Definition align (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::ptr::alignment::Alignment",
                "as_usize",
                []
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::alloc::layout::Layout",
                    "align"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_align : M.IsAssociatedFunction Self "align" align.
      
      (*
          pub const fn new<T>() -> Self {
              let (size, align) = size_align::<T>();
              // SAFETY: if the type is instantiated, rustc already ensures that its
              // layout is valid. Use the unchecked constructor to avoid inserting a
              // panicking codepath that needs to be optimized out.
              unsafe { Layout::from_size_align_unchecked(size, align) }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [] =>
          ltac:(M.monadic
            (M.read (|
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::alloc::layout::size_align", [ T ] |),
                    []
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let size := M.copy (| γ0_0 |) in
                      let align := M.copy (| γ0_1 |) in
                      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 |) ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          pub const fn for_value<T: ?Sized>(t: &T) -> Self {
              let (size, align) = (mem::size_of_val(t), mem::align_of_val(t));
              // SAFETY: see rationale in `new` for why this is using the unsafe variant
              unsafe { Layout::from_size_align_unchecked(size, align) }
          }
      *)
      Definition for_value (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ t ] =>
          ltac:(M.monadic
            (let t := M.alloc (| t |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  Value.Tuple
                    [
                      M.call_closure (|
                        M.get_function (| "core::mem::size_of_val", [ T ] |),
                        [ M.read (| t |) ]
                      |);
                      M.call_closure (|
                        M.get_function (| "core::mem::align_of_val", [ T ] |),
                        [ M.read (| t |) ]
                      |)
                    ]
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let size := M.copy (| γ0_0 |) in
                      let align := M.copy (| γ0_1 |) in
                      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 |) ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_for_value : M.IsAssociatedFunction Self "for_value" for_value.
      
      (*
          pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self {
              // SAFETY: we pass along the prerequisites of these functions to the caller
              let (size, align) = unsafe { (mem::size_of_val_raw(t), mem::align_of_val_raw(t)) };
              // SAFETY: see rationale in `new` for why this is using the unsafe variant
              unsafe { Layout::from_size_align_unchecked(size, align) }
          }
      *)
      Definition for_value_raw (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ t ] =>
          ltac:(M.monadic
            (let t := M.alloc (| t |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  Value.Tuple
                    [
                      M.call_closure (|
                        M.get_function (| "core::mem::size_of_val_raw", [ T ] |),
                        [ M.read (| t |) ]
                      |);
                      M.call_closure (|
                        M.get_function (| "core::mem::align_of_val_raw", [ T ] |),
                        [ M.read (| t |) ]
                      |)
                    ]
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let size := M.copy (| γ0_0 |) in
                      let align := M.copy (| γ0_1 |) in
                      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 |) ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_for_value_raw :
        M.IsAssociatedFunction Self "for_value_raw" for_value_raw.
      
      (*
          pub const fn dangling(&self) -> NonNull<u8> {
              // SAFETY: align is guaranteed to be non-zero
              unsafe { NonNull::new_unchecked(crate::ptr::without_provenance_mut::<u8>(self.align())) }
          }
      *)
      Definition dangling (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ Ty.path "u8" ],
                "new_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_function (| "core::ptr::without_provenance_mut", [ Ty.path "u8" ] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::alloc::layout::Layout",
                        "align",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_dangling : M.IsAssociatedFunction Self "dangling" dangling.
      
      (*
          pub const fn align_to(&self, align: usize) -> Result<Self, LayoutError> {
              if let Some(align) = Alignment::new(align) {
                  Layout::from_size_alignment(self.size, Alignment::max(self.align, align))
              } else {
                  Err(LayoutError)
              }
          }
      *)
      Definition align_to (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; align ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let align := M.alloc (| align |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::ptr::alignment::Alignment",
                              "new",
                              []
                            |),
                            [ M.read (| align |) ]
                          |)
                        |) in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let align := M.copy (| γ0_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::alloc::layout::Layout",
                            "from_size_alignment",
                            []
                          |),
                          [
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::alloc::layout::Layout",
                                "size"
                              |)
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ptr::alignment::Alignment",
                                "max",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::alloc::layout::Layout",
                                    "align"
                                  |)
                                |);
                                M.read (| align |)
                              ]
                            |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [ Value.StructTuple "core::alloc::layout::LayoutError" [] ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_align_to : M.IsAssociatedFunction Self "align_to" align_to.
      
      (*
          pub const fn padding_needed_for(&self, align: usize) -> usize {
              // FIXME: Can we just change the type on this to `Alignment`?
              let Some(align) = Alignment::new(align) else { return usize::MAX };
              let len_rounded_up = self.size_rounded_up_to_custom_align(align);
              // SAFETY: Cannot overflow because the rounded-up value is never less
              unsafe { unchecked_sub(len_rounded_up, self.size) }
          }
      *)
      Definition padding_needed_for (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; align ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let align := M.alloc (| align |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::ptr::alignment::Alignment",
                      "new",
                      []
                    |),
                    [ M.read (| align |) ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let align := M.copy (| γ0_0 |) in
                      let~ len_rounded_up :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::alloc::layout::Layout",
                              "size_rounded_up_to_custom_align",
                              []
                            |),
                            [ M.read (| self |); M.read (| align |) ]
                          |)
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::intrinsics::unchecked_sub",
                            [ Ty.path "usize" ]
                          |),
                          [
                            M.read (| len_rounded_up |);
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::alloc::layout::Layout",
                                "size"
                              |)
                            |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_padding_needed_for :
        M.IsAssociatedFunction Self "padding_needed_for" padding_needed_for.
      
      (*
          const fn size_rounded_up_to_custom_align(&self, align: Alignment) -> usize {
              // SAFETY:
              // Rounded up value is:
              //   size_rounded_up = (size + align - 1) & !(align - 1);
              //
              // The arithmetic we do here can never overflow:
              //
              // 1. align is guaranteed to be > 0, so align - 1 is always
              //    valid.
              //
              // 2. size is at most `isize::MAX`, so adding `align - 1` (which is at
              //    most `isize::MAX`) can never overflow a `usize`.
              //
              // 3. masking by the alignment can remove at most `align - 1`,
              //    which is what we just added, thus the value we return is never
              //    less than the original `size`.
              //
              // (Size 0 Align MAX is already aligned, so stays the same, but things like
              // Size 1 Align MAX or Size isize::MAX Align 2 round up to `isize::MAX + 1`.)
              unsafe {
                  let align_m1 = unchecked_sub(align.as_usize(), 1);
                  let size_rounded_up = unchecked_add(self.size, align_m1) & !align_m1;
                  size_rounded_up
              }
          }
      *)
      Definition size_rounded_up_to_custom_align
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self; align ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let align := M.alloc (| align |) in
            M.read (|
              let~ align_m1 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::unchecked_sub", [ Ty.path "usize" ] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::ptr::alignment::Alignment",
                          "as_usize",
                          []
                        |),
                        [ M.read (| align |) ]
                      |);
                      Value.Integer IntegerKind.Usize 1
                    ]
                  |)
                |) in
              let~ size_rounded_up :=
                M.alloc (|
                  BinOp.bit_and
                    (M.call_closure (|
                      M.get_function (| "core::intrinsics::unchecked_add", [ Ty.path "usize" ] |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::alloc::layout::Layout",
                            "size"
                          |)
                        |);
                        M.read (| align_m1 |)
                      ]
                    |))
                    (UnOp.not (| M.read (| align_m1 |) |))
                |) in
              size_rounded_up
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_size_rounded_up_to_custom_align :
        M.IsAssociatedFunction
          Self
          "size_rounded_up_to_custom_align"
          size_rounded_up_to_custom_align.
      
      (*
          pub const fn pad_to_align(&self) -> Layout {
              // This cannot overflow. Quoting from the invariant of Layout:
              // > `size`, when rounded up to the nearest multiple of `align`,
              // > must not overflow isize (i.e., the rounded value must be
              // > less than or equal to `isize::MAX`)
              let new_size = self.size_rounded_up_to_custom_align(self.align);
      
              // SAFETY: padded size is guaranteed to not exceed `isize::MAX`.
              unsafe { Layout::from_size_align_unchecked(new_size, self.align()) }
          }
      *)
      Definition pad_to_align (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ new_size :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::alloc::layout::Layout",
                      "size_rounded_up_to_custom_align",
                      []
                    |),
                    [
                      M.read (| self |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::alloc::layout::Layout",
                          "align"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::alloc::layout::Layout",
                    "from_size_align_unchecked",
                    []
                  |),
                  [
                    M.read (| new_size |);
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::alloc::layout::Layout",
                        "align",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_pad_to_align :
        M.IsAssociatedFunction Self "pad_to_align" pad_to_align.
      
      (*
          pub const fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError> {
              let padded = self.pad_to_align();
              if let Ok(repeated) = padded.repeat_packed(n) {
                  Ok((repeated, padded.size()))
              } else {
                  Err(LayoutError)
              }
          }
      *)
      Definition repeat (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ padded :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::alloc::layout::Layout",
                      "pad_to_align",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::alloc::layout::Layout",
                              "repeat_packed",
                              []
                            |),
                            [ padded; M.read (| n |) ]
                          |)
                        |) in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Ok",
                          0
                        |) in
                      let repeated := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Ok"
                          [
                            Value.Tuple
                              [
                                M.read (| repeated |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::alloc::layout::Layout",
                                    "size",
                                    []
                                  |),
                                  [ padded ]
                                |)
                              ]
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [ Value.StructTuple "core::alloc::layout::LayoutError" [] ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_repeat : M.IsAssociatedFunction Self "repeat" repeat.
      
      (*
          pub const fn extend(&self, next: Self) -> Result<(Self, usize), LayoutError> {
              let new_align = Alignment::max(self.align, next.align);
              let offset = self.size_rounded_up_to_custom_align(next.align);
      
              // SAFETY: `offset` is at most `isize::MAX + 1` (such as from aligning
              // to `Alignment::MAX`) and `next.size` is at most `isize::MAX` (from the
              // `Layout` type invariant).  Thus the largest possible `new_size` is
              // `isize::MAX + 1 + isize::MAX`, which is `usize::MAX`, and cannot overflow.
              let new_size = unsafe { unchecked_add(offset, next.size) };
      
              if let Ok(layout) = Layout::from_size_alignment(new_size, new_align) {
                  Ok((layout, offset))
              } else {
                  Err(LayoutError)
              }
          }
      *)
      Definition extend (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; next ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let next := M.alloc (| next |) in
            M.read (|
              let~ new_align :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::ptr::alignment::Alignment",
                      "max",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::alloc::layout::Layout",
                          "align"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          next,
                          "core::alloc::layout::Layout",
                          "align"
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ offset :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::alloc::layout::Layout",
                      "size_rounded_up_to_custom_align",
                      []
                    |),
                    [
                      M.read (| self |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          next,
                          "core::alloc::layout::Layout",
                          "align"
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ new_size :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::unchecked_add", [ Ty.path "usize" ] |),
                    [
                      M.read (| offset |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          next,
                          "core::alloc::layout::Layout",
                          "size"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::alloc::layout::Layout",
                              "from_size_alignment",
                              []
                            |),
                            [ M.read (| new_size |); M.read (| new_align |) ]
                          |)
                        |) in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Ok",
                          0
                        |) in
                      let layout := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Ok"
                          [ Value.Tuple [ M.read (| layout |); M.read (| offset |) ] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [ Value.StructTuple "core::alloc::layout::LayoutError" [] ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_extend : M.IsAssociatedFunction Self "extend" extend.
      
      (*
          pub const fn repeat_packed(&self, n: usize) -> Result<Self, LayoutError> {
              if let Some(size) = self.size.checked_mul(n) {
                  // The safe constructor is called here to enforce the isize size limit.
                  Layout::from_size_alignment(size, self.align)
              } else {
                  Err(LayoutError)
              }
          }
      *)
      Definition repeat_packed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (| Ty.path "usize", "checked_mul", [] |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::alloc::layout::Layout",
                                  "size"
                                |)
                              |);
                              M.read (| n |)
                            ]
                          |)
                        |) in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let size := M.copy (| γ0_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::alloc::layout::Layout",
                            "from_size_alignment",
                            []
                          |),
                          [
                            M.read (| size |);
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::alloc::layout::Layout",
                                "align"
                              |)
                            |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [ Value.StructTuple "core::alloc::layout::LayoutError" [] ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_repeat_packed :
        M.IsAssociatedFunction Self "repeat_packed" repeat_packed.
      
      (*
          pub const fn extend_packed(&self, next: Self) -> Result<Self, LayoutError> {
              // SAFETY: each `size` is at most `isize::MAX == usize::MAX/2`, so the
              // sum is at most `usize::MAX/2*2 == usize::MAX - 1`, and cannot overflow.
              let new_size = unsafe { unchecked_add(self.size, next.size) };
              // The safe constructor enforces that the new size isn't too big for the alignment
              Layout::from_size_alignment(new_size, self.align)
          }
      *)
      Definition extend_packed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; next ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let next := M.alloc (| next |) in
            M.read (|
              let~ new_size :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::unchecked_add", [ Ty.path "usize" ] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::alloc::layout::Layout",
                          "size"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          next,
                          "core::alloc::layout::Layout",
                          "size"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::alloc::layout::Layout",
                    "from_size_alignment",
                    []
                  |),
                  [
                    M.read (| new_size |);
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::alloc::layout::Layout",
                        "align"
                      |)
                    |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_extend_packed :
        M.IsAssociatedFunction Self "extend_packed" extend_packed.
      
      (*
          pub const fn array<T>(n: usize) -> Result<Self, LayoutError> {
              // Reduce the amount of code we need to monomorphize per `T`.
              return inner(T::LAYOUT, n);
      
              #[inline]
              const fn inner(element_layout: Layout, n: usize) -> Result<Layout, LayoutError> {
                  let Layout { size: element_size, align } = element_layout;
      
                  // We need to check two things about the size:
                  //  - That the total size won't overflow a `usize`, and
                  //  - That the total size still fits in an `isize`.
                  // By using division we can check them both with a single threshold.
                  // That'd usually be a bad idea, but thankfully here the element size
                  // and alignment are constants, so the compiler will fold all of it.
                  if element_size != 0 && n > Layout::max_size_for_align(align) / element_size {
                      return Err(LayoutError);
                  }
      
                  // SAFETY: We just checked that we won't overflow `usize` when we multiply.
                  // This is a useless hint inside this function, but after inlining this helps
                  // deduplicate checks for whether the overall capacity is zero (e.g., in RawVec's
                  // allocation path) before/after this multiplication.
                  let array_size = unsafe { unchecked_mul(element_size, n) };
      
                  // SAFETY: We just checked above that the `array_size` will not
                  // exceed `isize::MAX` even when rounded up to the alignment.
                  // And `Alignment` guarantees it's a power of two.
                  unsafe { Ok(Layout::from_size_align_unchecked(array_size, align.as_usize())) }
              }
          }
      *)
      Definition array (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ n ] =>
          ltac:(M.monadic
            (let n := M.alloc (| n |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.never_to_any (|
                  M.read (|
                    M.return_ (|
                      M.call_closure (|
                        M.get_associated_function (| Self, "inner.array", [] |),
                        [
                          M.read (|
                            M.get_constant (| "core::mem::SizedTypeProperties::LAYOUT" |)
                          |);
                          M.read (| n |)
                        ]
                      |)
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_array : M.IsAssociatedFunction Self "array" array.
    End Impl_core_alloc_layout_Layout.
    
    Axiom LayoutErr :
      (Ty.path "core::alloc::layout::LayoutErr") = (Ty.path "core::alloc::layout::LayoutError").
    
    (* StructTuple
      {
        name := "LayoutError";
        const_params := [];
        ty_params := [];
        fields := [];
      } *)
    
    Module Impl_core_clone_Clone_for_core_alloc_layout_LayoutError.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::LayoutError".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructTuple "core::alloc::layout::LayoutError" []))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_alloc_layout_LayoutError.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_alloc_layout_LayoutError.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::LayoutError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_alloc_layout_LayoutError.
    
    Module Impl_core_cmp_PartialEq_for_core_alloc_layout_LayoutError.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::LayoutError".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.Bool true))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_alloc_layout_LayoutError.
    
    Module Impl_core_cmp_Eq_for_core_alloc_layout_LayoutError.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::LayoutError".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.Tuple []))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_alloc_layout_LayoutError.
    
    Module Impl_core_fmt_Debug_for_core_alloc_layout_LayoutError.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::LayoutError".
      
      (* 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 "LayoutError" |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_alloc_layout_LayoutError.
    
    Module Impl_core_error_Error_for_core_alloc_layout_LayoutError.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::LayoutError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::error::Error"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_error_Error_for_core_alloc_layout_LayoutError.
    
    Module Impl_core_fmt_Display_for_core_alloc_layout_LayoutError.
      Definition Self : Ty.t := Ty.path "core::alloc::layout::LayoutError".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              f.write_str("invalid parameters to Layout::from_size_align")
          }
      *)
      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 "invalid parameters to Layout::from_size_align" |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Display"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Display_for_core_alloc_layout_LayoutError.
  End layout.
End alloc.
