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

Module ptr.
  Module alignment.
    (* StructTuple
      {
        name := "Alignment";
        const_params := [];
        ty_params := [];
        fields := [ Ty.path "core::ptr::alignment::AlignmentEnum" ];
      } *)
    
    Module Impl_core_marker_Copy_for_core_ptr_alignment_Alignment.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::Alignment".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_ptr_alignment_Alignment.
    
    Module Impl_core_clone_Clone_for_core_ptr_alignment_Alignment.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::Alignment".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_ptr_alignment_Alignment.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_ptr_alignment_Alignment.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::Alignment".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_ptr_alignment_Alignment.
    
    Module Impl_core_cmp_PartialEq_for_core_ptr_alignment_Alignment.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::Alignment".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.path "core::ptr::alignment::AlignmentEnum",
                [ Ty.path "core::ptr::alignment::AlignmentEnum" ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "core::ptr::alignment::Alignment",
                  0
                |);
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| other |),
                  "core::ptr::alignment::Alignment",
                  0
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_ptr_alignment_Alignment.
    
    Module Impl_core_cmp_Eq_for_core_ptr_alignment_Alignment.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::Alignment".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_ptr_alignment_Alignment.
    
    (*
    fn _alignment_can_be_structurally_matched(a: Alignment) -> bool {
        matches!(a, Alignment::MIN)
    }
    *)
    Definition _alignment_can_be_structurally_matched
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ a ] =>
        ltac:(M.monadic
          (let a := M.alloc (| a |) in
          M.read (|
            M.match_operator (|
              a,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::ptr::alignment::Alignment",
                        0
                      |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ0_0,
                        "core::ptr::alignment::AlignmentEnum::_Align1Shl0"
                      |) in
                    M.alloc (| Value.Bool true |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function__alignment_can_be_structurally_matched :
      M.IsFunction
        "core::ptr::alignment::_alignment_can_be_structurally_matched"
        _alignment_can_be_structurally_matched.
    
    Module Impl_core_ptr_alignment_Alignment.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::Alignment".
      
      (*     pub const MIN: Self = Self(AlignmentEnum::_Align1Shl0); *)
      (* Ty.path "core::ptr::alignment::Alignment" *)
      Definition value_MIN : Value.t :=
        M.run
          ltac:(M.monadic
            (M.alloc (|
              Value.StructTuple
                "core::ptr::alignment::Alignment"
                [ Value.StructTuple "core::ptr::alignment::AlignmentEnum::_Align1Shl0" [] ]
            |))).
      
      Axiom AssociatedConstant_value_MIN : M.IsAssociatedConstant Self "value_MIN" value_MIN.
      
      (*
          pub const fn of<T>() -> Self {
              // SAFETY: rustc ensures that type alignment is always a power of two.
              unsafe { Alignment::new_unchecked(mem::align_of::<T>()) }
          }
      *)
      Definition of (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [] =>
          ltac:(M.monadic
            (M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::ptr::alignment::Alignment",
                "new_unchecked",
                []
              |),
              [ M.call_closure (| M.get_function (| "core::mem::align_of", [ T ] |), [] |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_of : M.IsAssociatedFunction Self "of" of.
      
      (*
          pub const fn new(align: usize) -> Option<Self> {
              if align.is_power_of_two() {
                  // SAFETY: Just checked it only has one bit set
                  Some(unsafe { Self::new_unchecked(align) })
              } else {
                  None
              }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ align ] =>
          ltac:(M.monadic
            (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 "usize",
                                "is_power_of_two",
                                []
                              |),
                              [ M.read (| align |) ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ptr::alignment::Alignment",
                                "new_unchecked",
                                []
                              |),
                              [ M.read (| align |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          pub const unsafe fn new_unchecked(align: usize) -> Self {
              assert_unsafe_precondition!(
                  check_language_ub,
                  "Alignment::new_unchecked requires a power of two",
                  (align: usize = align) => align.is_power_of_two()
              );
      
              // SAFETY: By precondition, this must be a power of two, and
              // our variants encompass all possible powers of two.
              unsafe { mem::transmute::<usize, Alignment>(align) }
          }
      *)
      Definition new_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ align ] =>
          ltac:(M.monadic
            (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::ub_checks::check_language_ub", [] |),
                                []
                              |)
                            |)) 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.new_unchecked",
                                []
                              |),
                              [ M.read (| align |) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                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_new_unchecked :
        M.IsAssociatedFunction Self "new_unchecked" new_unchecked.
      
      (*
          pub const fn as_usize(self) -> usize {
              self.0 as usize
          }
      *)
      Definition as_usize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.rust_cast
              (M.read (|
                M.SubPointer.get_struct_tuple_field (| self, "core::ptr::alignment::Alignment", 0 |)
              |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_usize : M.IsAssociatedFunction Self "as_usize" as_usize.
      
      (*
          pub const fn as_nonzero(self) -> NonZero<usize> {
              // SAFETY: All the discriminants are non-zero.
              unsafe { NonZero::new_unchecked(self.as_usize()) }
          }
      *)
      Definition as_nonzero (ε : 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::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                "new_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::ptr::alignment::Alignment",
                    "as_usize",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_nonzero : M.IsAssociatedFunction Self "as_nonzero" as_nonzero.
      
      (*
          pub const fn log2(self) -> u32 {
              self.as_nonzero().trailing_zeros()
          }
      *)
      Definition log2 (ε : 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::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                "trailing_zeros",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::ptr::alignment::Alignment",
                    "as_nonzero",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_log2 : M.IsAssociatedFunction Self "log2" log2.
      
      (*
          pub const fn mask(self) -> usize {
              // SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
              !(unsafe { self.as_usize().unchecked_sub(1) })
          }
      *)
      Definition mask (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            UnOp.not (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "usize", "unchecked_sub", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::ptr::alignment::Alignment",
                      "as_usize",
                      []
                    |),
                    [ M.read (| self |) ]
                  |);
                  Value.Integer IntegerKind.Usize 1
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_mask : M.IsAssociatedFunction Self "mask" mask.
      
      (*
          pub(crate) const fn max(a: Self, b: Self) -> Self {
              if a.as_usize() > b.as_usize() { a } else { b }
          }
      *)
      Definition max (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ a; b ] =>
          ltac:(M.monadic
            (let a := M.alloc (| a |) in
            let b := M.alloc (| b |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.gt (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::ptr::alignment::Alignment",
                                  "as_usize",
                                  []
                                |),
                                [ M.read (| a |) ]
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::ptr::alignment::Alignment",
                                  "as_usize",
                                  []
                                |),
                                [ M.read (| b |) ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      a));
                  fun γ => ltac:(M.monadic b)
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_max : M.IsAssociatedFunction Self "max" max.
    End Impl_core_ptr_alignment_Alignment.
    
    Module Impl_core_fmt_Debug_for_core_ptr_alignment_Alignment.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::Alignment".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              write!(f, "{:?} (1 << {:?})", self.as_nonzero(), self.log2())
          }
      *)
      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_fmt", [] |),
              [
                M.read (| f |);
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                  [
                    M.alloc (|
                      Value.Array
                        [
                          M.read (| Value.String "" |);
                          M.read (| Value.String " (1 << " |);
                          M.read (| Value.String ")" |)
                        ]
                    |);
                    M.alloc (|
                      Value.Array
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::rt::Argument",
                              "new_debug",
                              [
                                Ty.apply
                                  (Ty.path "core::num::nonzero::NonZero")
                                  []
                                  [ Ty.path "usize" ]
                              ]
                            |),
                            [
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::ptr::alignment::Alignment",
                                    "as_nonzero",
                                    []
                                  |),
                                  [ M.read (| M.read (| self |) |) ]
                                |)
                              |)
                            ]
                          |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::rt::Argument",
                              "new_debug",
                              [ Ty.path "u32" ]
                            |),
                            [
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::ptr::alignment::Alignment",
                                    "log2",
                                    []
                                  |),
                                  [ M.read (| M.read (| self |) |) ]
                                |)
                              |)
                            ]
                          |)
                        ]
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => 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_ptr_alignment_Alignment.
    
    Module Impl_core_convert_TryFrom_core_num_nonzero_NonZero_usize_for_core_ptr_alignment_Alignment.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::Alignment".
      
      (*     type Error = num::TryFromIntError; *)
      Definition _Error : Ty.t := Ty.path "core::num::error::TryFromIntError".
      
      (*
          fn try_from(align: NonZero<usize>) -> Result<Alignment, Self::Error> {
              align.get().try_into()
          }
      *)
      Definition try_from (ε : 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_trait_method (|
                "core::convert::TryInto",
                Ty.path "usize",
                [ Ty.path "core::ptr::alignment::Alignment" ],
                "try_into",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                    "get",
                    []
                  |),
                  [ M.read (| align |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::TryFrom"
          Self
          (* Trait polymorphic types *)
          [ (* T *) Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ]
          (* Instance *)
          [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
    End Impl_core_convert_TryFrom_core_num_nonzero_NonZero_usize_for_core_ptr_alignment_Alignment.
    
    Module Impl_core_convert_TryFrom_usize_for_core_ptr_alignment_Alignment.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::Alignment".
      
      (*     type Error = num::TryFromIntError; *)
      Definition _Error : Ty.t := Ty.path "core::num::error::TryFromIntError".
      
      (*
          fn try_from(align: usize) -> Result<Alignment, Self::Error> {
              Self::new(align).ok_or(num::TryFromIntError(()))
          }
      *)
      Definition try_from (ε : 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_associated_function (|
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.path "core::ptr::alignment::Alignment" ],
                "ok_or",
                [ Ty.path "core::num::error::TryFromIntError" ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::ptr::alignment::Alignment",
                    "new",
                    []
                  |),
                  [ M.read (| align |) ]
                |);
                Value.StructTuple "core::num::error::TryFromIntError" [ Value.Tuple [] ]
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::TryFrom"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "usize" ]
          (* Instance *)
          [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
    End Impl_core_convert_TryFrom_usize_for_core_ptr_alignment_Alignment.
    
    Module Impl_core_convert_From_core_ptr_alignment_Alignment_for_core_num_nonzero_NonZero_usize.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ].
      
      (*
          fn from(align: Alignment) -> NonZero<usize> {
              align.as_nonzero()
          }
      *)
      Definition from (ε : 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_associated_function (|
                Ty.path "core::ptr::alignment::Alignment",
                "as_nonzero",
                []
              |),
              [ M.read (| align |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "core::ptr::alignment::Alignment" ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_core_ptr_alignment_Alignment_for_core_num_nonzero_NonZero_usize.
    
    Module Impl_core_convert_From_core_ptr_alignment_Alignment_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*
          fn from(align: Alignment) -> usize {
              align.as_usize()
          }
      *)
      Definition from (ε : 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_associated_function (|
                Ty.path "core::ptr::alignment::Alignment",
                "as_usize",
                []
              |),
              [ M.read (| align |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "core::ptr::alignment::Alignment" ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_core_ptr_alignment_Alignment_for_usize.
    
    Module Impl_core_cmp_Ord_for_core_ptr_alignment_Alignment.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::Alignment".
      
      (*
          fn cmp(&self, other: &Self) -> cmp::Ordering {
              self.as_nonzero().get().cmp(&other.as_nonzero().get())
          }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (| "core::cmp::Ord", Ty.path "usize", [], "cmp", [] |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                      "get",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::ptr::alignment::Alignment",
                          "as_nonzero",
                          []
                        |),
                        [ M.read (| M.read (| self |) |) ]
                      |)
                    ]
                  |)
                |);
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                      "get",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::ptr::alignment::Alignment",
                          "as_nonzero",
                          []
                        |),
                        [ M.read (| M.read (| other |) |) ]
                      |)
                    ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_core_ptr_alignment_Alignment.
    
    Module Impl_core_cmp_PartialOrd_for_core_ptr_alignment_Alignment.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::Alignment".
      
      (*
          fn partial_cmp(&self, other: &Self) -> Option<cmp::Ordering> {
              Some(self.cmp(other))
          }
      *)
      Definition partial_cmp (ε : 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.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::Ord",
                    Ty.path "core::ptr::alignment::Alignment",
                    [],
                    "cmp",
                    []
                  |),
                  [ M.read (| self |); M.read (| other |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
    End Impl_core_cmp_PartialOrd_for_core_ptr_alignment_Alignment.
    
    Module Impl_core_hash_Hash_for_core_ptr_alignment_Alignment.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::Alignment".
      
      (*
          fn hash<H: hash::Hasher>(&self, state: &mut H) {
              self.as_nonzero().hash(state)
          }
      *)
      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.call_closure (|
              M.get_trait_method (|
                "core::hash::Hash",
                Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                [],
                "hash",
                [ H ]
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::ptr::alignment::Alignment",
                      "as_nonzero",
                      []
                    |),
                    [ M.read (| M.read (| self |) |) ]
                  |)
                |);
                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_ptr_alignment_Alignment.
    
    Module Impl_core_default_Default_for_core_ptr_alignment_Alignment.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::Alignment".
      
      (*
          fn default() -> Alignment {
              Alignment::MIN
          }
      *)
      Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic (M.read (| M.get_constant (| "core::ptr::alignment::MIN" |) |)))
        | _, _, _ => 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_core_ptr_alignment_Alignment.
    
    (*
    Enum AlignmentEnum
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "_Align1Shl0";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl1";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl2";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl3";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl4";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl5";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl6";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl7";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl8";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl9";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl10";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl11";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl12";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl13";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl14";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl15";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl16";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl17";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl18";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl19";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl20";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl21";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl22";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl23";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl24";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl25";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl26";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl27";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl28";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl29";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl30";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl31";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl32";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl33";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl34";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl35";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl36";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl37";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl38";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl39";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl40";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl41";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl42";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl43";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl44";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl45";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl46";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl47";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl48";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl49";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl50";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl51";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl52";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl53";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl54";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl55";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl56";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl57";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl58";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl59";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl60";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl61";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl62";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "_Align1Shl63";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_marker_Copy_for_core_ptr_alignment_AlignmentEnum.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::AlignmentEnum".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_ptr_alignment_AlignmentEnum.
    
    Module Impl_core_clone_Clone_for_core_ptr_alignment_AlignmentEnum.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::AlignmentEnum".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_ptr_alignment_AlignmentEnum.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_ptr_alignment_AlignmentEnum.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::AlignmentEnum".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_ptr_alignment_AlignmentEnum.
    
    Module Impl_core_cmp_PartialEq_for_core_ptr_alignment_AlignmentEnum.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::AlignmentEnum".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::ptr::alignment::AlignmentEnum" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::ptr::alignment::AlignmentEnum" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_ptr_alignment_AlignmentEnum.
    
    Module Impl_core_cmp_Eq_for_core_ptr_alignment_AlignmentEnum.
      Definition Self : Ty.t := Ty.path "core::ptr::alignment::AlignmentEnum".
      
      (* 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_ptr_alignment_AlignmentEnum.
  End alignment.
End ptr.
