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

Module f64.
  Definition value_RADIX : Value.t :=
    M.run ltac:(M.monadic (M.get_constant (| "core::f64::RADIX" |))).
  
  Definition value_MANTISSA_DIGITS : Value.t :=
    M.run ltac:(M.monadic (M.get_constant (| "core::f64::MANTISSA_DIGITS" |))).
  
  Definition value_DIGITS : Value.t :=
    M.run ltac:(M.monadic (M.get_constant (| "core::f64::DIGITS" |))).
  
  Definition value_EPSILON : Value.t :=
    M.run ltac:(M.monadic (M.get_constant (| "core::f64::EPSILON" |))).
  
  Definition value_MIN : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::f64::MIN" |))).
  
  Definition value_MIN_POSITIVE : Value.t :=
    M.run ltac:(M.monadic (M.get_constant (| "core::f64::MIN_POSITIVE" |))).
  
  Definition value_MAX : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::f64::MAX" |))).
  
  Definition value_MIN_EXP : Value.t :=
    M.run ltac:(M.monadic (M.get_constant (| "core::f64::MIN_EXP" |))).
  
  Definition value_MAX_EXP : Value.t :=
    M.run ltac:(M.monadic (M.get_constant (| "core::f64::MAX_EXP" |))).
  
  Definition value_MIN_10_EXP : Value.t :=
    M.run ltac:(M.monadic (M.get_constant (| "core::f64::MIN_10_EXP" |))).
  
  Definition value_MAX_10_EXP : Value.t :=
    M.run ltac:(M.monadic (M.get_constant (| "core::f64::MAX_10_EXP" |))).
  
  Definition value_NAN : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::f64::NAN" |))).
  
  Definition value_INFINITY : Value.t :=
    M.run ltac:(M.monadic (M.get_constant (| "core::f64::INFINITY" |))).
  
  Definition value_NEG_INFINITY : Value.t :=
    M.run ltac:(M.monadic (M.get_constant (| "core::f64::NEG_INFINITY" |))).
  
  Module consts.
    Definition value_PI : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_TAU : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_PHI : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_EGAMMA : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_FRAC_PI_2 : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_FRAC_PI_3 : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_FRAC_PI_4 : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_FRAC_PI_6 : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_FRAC_PI_8 : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_FRAC_1_PI : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_FRAC_1_SQRT_PI : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_FRAC_1_SQRT_2PI : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_FRAC_2_PI : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_FRAC_2_SQRT_PI : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_SQRT_2 : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_FRAC_1_SQRT_2 : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_SQRT_3 : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_FRAC_1_SQRT_3 : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_E : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_LOG2_10 : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_LOG2_E : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_LOG10_2 : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_LOG10_E : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_LN_2 : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Definition value_LN_10 : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
  End consts.
  
  Module Impl_f64.
    Definition Self : Ty.t := Ty.path "f64".
    
    (*     pub const RADIX: u32 = 2; *)
    (* Ty.path "u32" *)
    Definition value_RADIX : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 2 |))).
    
    Axiom AssociatedConstant_value_RADIX : M.IsAssociatedConstant Self "value_RADIX" value_RADIX.
    
    (*     pub const MANTISSA_DIGITS: u32 = 53; *)
    (* Ty.path "u32" *)
    Definition value_MANTISSA_DIGITS : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 53 |))).
    
    Axiom AssociatedConstant_value_MANTISSA_DIGITS :
      M.IsAssociatedConstant Self "value_MANTISSA_DIGITS" value_MANTISSA_DIGITS.
    
    (*     pub const DIGITS: u32 = 15; *)
    (* Ty.path "u32" *)
    Definition value_DIGITS : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 15 |))).
    
    Axiom AssociatedConstant_value_DIGITS : M.IsAssociatedConstant Self "value_DIGITS" value_DIGITS.
    
    (*     pub const EPSILON: f64 = 2.2204460492503131e-16_f64; *)
    (* Ty.path "f64" *)
    Definition value_EPSILON : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Axiom AssociatedConstant_value_EPSILON :
      M.IsAssociatedConstant Self "value_EPSILON" value_EPSILON.
    
    (*     pub const MIN: f64 = -1.7976931348623157e+308_f64; *)
    (* Ty.path "f64" *)
    Definition value_MIN : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Axiom AssociatedConstant_value_MIN : M.IsAssociatedConstant Self "value_MIN" value_MIN.
    
    (*     pub const MIN_POSITIVE: f64 = 2.2250738585072014e-308_f64; *)
    (* Ty.path "f64" *)
    Definition value_MIN_POSITIVE : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Axiom AssociatedConstant_value_MIN_POSITIVE :
      M.IsAssociatedConstant Self "value_MIN_POSITIVE" value_MIN_POSITIVE.
    
    (*     pub const MAX: f64 = 1.7976931348623157e+308_f64; *)
    (* Ty.path "f64" *)
    Definition value_MAX : Value.t := M.run ltac:(M.monadic UnsupportedLiteral).
    
    Axiom AssociatedConstant_value_MAX : M.IsAssociatedConstant Self "value_MAX" value_MAX.
    
    (*     pub const MIN_EXP: i32 = -1021; *)
    (* Ty.path "i32" *)
    Definition value_MIN_EXP : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.I32 (-1021) |))).
    
    Axiom AssociatedConstant_value_MIN_EXP :
      M.IsAssociatedConstant Self "value_MIN_EXP" value_MIN_EXP.
    
    (*     pub const MAX_EXP: i32 = 1024; *)
    (* Ty.path "i32" *)
    Definition value_MAX_EXP : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.I32 1024 |))).
    
    Axiom AssociatedConstant_value_MAX_EXP :
      M.IsAssociatedConstant Self "value_MAX_EXP" value_MAX_EXP.
    
    (*     pub const MIN_10_EXP: i32 = -307; *)
    (* Ty.path "i32" *)
    Definition value_MIN_10_EXP : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.I32 (-307) |))).
    
    Axiom AssociatedConstant_value_MIN_10_EXP :
      M.IsAssociatedConstant Self "value_MIN_10_EXP" value_MIN_10_EXP.
    
    (*     pub const MAX_10_EXP: i32 = 308; *)
    (* Ty.path "i32" *)
    Definition value_MAX_10_EXP : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.I32 308 |))).
    
    Axiom AssociatedConstant_value_MAX_10_EXP :
      M.IsAssociatedConstant Self "value_MAX_10_EXP" value_MAX_10_EXP.
    
    (*     pub const NAN: f64 = 0.0_f64 / 0.0_f64; *)
    (* Ty.path "f64" *)
    Definition value_NAN : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            BinOp.Wrap.div (| M.read (| UnsupportedLiteral |), M.read (| UnsupportedLiteral |) |)
          |))).
    
    Axiom AssociatedConstant_value_NAN : M.IsAssociatedConstant Self "value_NAN" value_NAN.
    
    (*     pub const INFINITY: f64 = 1.0_f64 / 0.0_f64; *)
    (* Ty.path "f64" *)
    Definition value_INFINITY : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            BinOp.Wrap.div (| M.read (| UnsupportedLiteral |), M.read (| UnsupportedLiteral |) |)
          |))).
    
    Axiom AssociatedConstant_value_INFINITY :
      M.IsAssociatedConstant Self "value_INFINITY" value_INFINITY.
    
    (*     pub const NEG_INFINITY: f64 = -1.0_f64 / 0.0_f64; *)
    (* Ty.path "f64" *)
    Definition value_NEG_INFINITY : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            BinOp.Wrap.div (| M.read (| UnsupportedLiteral |), M.read (| UnsupportedLiteral |) |)
          |))).
    
    Axiom AssociatedConstant_value_NEG_INFINITY :
      M.IsAssociatedConstant Self "value_NEG_INFINITY" value_NEG_INFINITY.
    
    (*     const SIGN_MASK: u64 = 0x8000_0000_0000_0000; *)
    (* Ty.path "u64" *)
    Definition value_SIGN_MASK : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 9223372036854775808 |))).
    
    Axiom AssociatedConstant_value_SIGN_MASK :
      M.IsAssociatedConstant Self "value_SIGN_MASK" value_SIGN_MASK.
    
    (*     const EXP_MASK: u64 = 0x7ff0_0000_0000_0000; *)
    (* Ty.path "u64" *)
    Definition value_EXP_MASK : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 9218868437227405312 |))).
    
    Axiom AssociatedConstant_value_EXP_MASK :
      M.IsAssociatedConstant Self "value_EXP_MASK" value_EXP_MASK.
    
    (*     const MAN_MASK: u64 = 0x000f_ffff_ffff_ffff; *)
    (* Ty.path "u64" *)
    Definition value_MAN_MASK : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 4503599627370495 |))).
    
    Axiom AssociatedConstant_value_MAN_MASK :
      M.IsAssociatedConstant Self "value_MAN_MASK" value_MAN_MASK.
    
    (*     const TINY_BITS: u64 = 0x1; *)
    (* Ty.path "u64" *)
    Definition value_TINY_BITS : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 1 |))).
    
    Axiom AssociatedConstant_value_TINY_BITS :
      M.IsAssociatedConstant Self "value_TINY_BITS" value_TINY_BITS.
    
    (*     const NEG_TINY_BITS: u64 = Self::TINY_BITS | Self::SIGN_MASK; *)
    (* Ty.path "u64" *)
    Definition value_NEG_TINY_BITS : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            BinOp.bit_or
              (M.read (| M.get_constant (| "core::f64::TINY_BITS" |) |))
              (M.read (| M.get_constant (| "core::f64::SIGN_MASK" |) |))
          |))).
    
    Axiom AssociatedConstant_value_NEG_TINY_BITS :
      M.IsAssociatedConstant Self "value_NEG_TINY_BITS" value_NEG_TINY_BITS.
    
    (*
        pub const fn is_nan(self) -> bool {
            self != self
        }
    *)
    Definition is_nan (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.ne (| M.read (| self |), M.read (| self |) |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_nan : M.IsAssociatedFunction Self "is_nan" is_nan.
    
    (*
        pub(crate) const fn abs_private(self) -> f64 {
            // SAFETY: This transmutation is fine just like in `to_bits`/`from_bits`.
            unsafe { mem::transmute::<u64, f64>(mem::transmute::<f64, u64>(self) & !Self::SIGN_MASK) }
        }
    *)
    Definition abs_private (ε : 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_function (| "core::intrinsics::transmute", [ Ty.path "u64"; Ty.path "f64" ] |),
            [
              BinOp.bit_and
                (M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::transmute",
                    [ Ty.path "f64"; Ty.path "u64" ]
                  |),
                  [ M.read (| self |) ]
                |))
                (UnOp.not (| M.read (| M.get_constant (| "core::f64::SIGN_MASK" |) |) |))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_abs_private : M.IsAssociatedFunction Self "abs_private" abs_private.
    
    (*
        pub const fn is_infinite(self) -> bool {
            // Getting clever with transmutation can result in incorrect answers on some FPUs
            // FIXME: alter the Rust <-> Rust calling convention to prevent this problem.
            // See https://github.com/rust-lang/rust/issues/72327
            (self == f64::INFINITY) | (self == f64::NEG_INFINITY)
        }
    *)
    Definition is_infinite (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.bit_or
            (BinOp.eq (|
              M.read (| self |),
              M.read (| M.get_constant (| "core::f64::INFINITY" |) |)
            |))
            (BinOp.eq (|
              M.read (| self |),
              M.read (| M.get_constant (| "core::f64::NEG_INFINITY" |) |)
            |))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_infinite : M.IsAssociatedFunction Self "is_infinite" is_infinite.
    
    (*
        pub const fn is_finite(self) -> bool {
            // There's no need to handle NaN separately: if self is NaN,
            // the comparison is not true, exactly as desired.
            self.abs_private() < Self::INFINITY
        }
    *)
    Definition is_finite (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.lt (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "f64", "abs_private", [] |),
              [ M.read (| self |) ]
            |),
            M.read (| M.get_constant (| "core::f64::INFINITY" |) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_finite : M.IsAssociatedFunction Self "is_finite" is_finite.
    
    (*
        pub const fn is_subnormal(self) -> bool {
            matches!(self.classify(), FpCategory::Subnormal)
        }
    *)
    Definition is_subnormal (ε : 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 (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "f64", "classify", [] |),
                  [ M.read (| self |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::num::FpCategory::Subnormal" |) in
                    M.alloc (| Value.Bool true |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_subnormal : M.IsAssociatedFunction Self "is_subnormal" is_subnormal.
    
    (*
        pub const fn is_normal(self) -> bool {
            matches!(self.classify(), FpCategory::Normal)
        }
    *)
    Definition is_normal (ε : 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 (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "f64", "classify", [] |),
                  [ M.read (| self |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::num::FpCategory::Normal" |) in
                    M.alloc (| Value.Bool true |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_normal : M.IsAssociatedFunction Self "is_normal" is_normal.
    
    (*
        pub const fn classify(self) -> FpCategory {
            // We used to have complicated logic here that avoids the simple bit-based tests to work
            // around buggy codegen for x87 targets (see
            // https://github.com/rust-lang/rust/issues/114479). However, some LLVM versions later, none
            // of our tests is able to find any difference between the complicated and the naive
            // version, so now we are back to the naive version.
            let b = self.to_bits();
            match (b & Self::MAN_MASK, b & Self::EXP_MASK) {
                (0, Self::EXP_MASK) => FpCategory::Infinite,
                (_, Self::EXP_MASK) => FpCategory::Nan,
                (0, 0) => FpCategory::Zero,
                (_, 0) => FpCategory::Subnormal,
                _ => FpCategory::Normal,
            }
        }
    *)
    Definition classify (ε : 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~ b :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "f64", "to_bits", [] |),
                  [ M.read (| self |) ]
                |)
              |) in
            M.match_operator (|
              M.alloc (|
                Value.Tuple
                  [
                    BinOp.bit_and
                      (M.read (| b |))
                      (M.read (| M.get_constant (| "core::f64::MAN_MASK" |) |));
                    BinOp.bit_and
                      (M.read (| b |))
                      (M.read (| M.get_constant (| "core::f64::EXP_MASK" |) |))
                  ]
              |),
              [
                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 _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ0_0 |),
                        Value.Integer IntegerKind.U64 0
                      |) in
                    let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ0_1 |),
                        Value.Integer IntegerKind.U64 9218868437227405312
                      |) in
                    M.alloc (| Value.StructTuple "core::num::FpCategory::Infinite" [] |)));
                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 _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ0_1 |),
                        Value.Integer IntegerKind.U64 9218868437227405312
                      |) in
                    M.alloc (| Value.StructTuple "core::num::FpCategory::Nan" [] |)));
                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 _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ0_0 |),
                        Value.Integer IntegerKind.U64 0
                      |) in
                    let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ0_1 |),
                        Value.Integer IntegerKind.U64 0
                      |) in
                    M.alloc (| Value.StructTuple "core::num::FpCategory::Zero" [] |)));
                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 _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ0_1 |),
                        Value.Integer IntegerKind.U64 0
                      |) in
                    M.alloc (| Value.StructTuple "core::num::FpCategory::Subnormal" [] |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (| Value.StructTuple "core::num::FpCategory::Normal" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_classify : M.IsAssociatedFunction Self "classify" classify.
    
    (*
        pub const fn is_sign_positive(self) -> bool {
            !self.is_sign_negative()
        }
    *)
    Definition is_sign_positive (ε : 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 "f64", "is_sign_negative", [] |),
              [ M.read (| self |) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_sign_positive :
      M.IsAssociatedFunction Self "is_sign_positive" is_sign_positive.
    
    (*
        pub fn is_positive(self) -> bool {
            self.is_sign_positive()
        }
    *)
    Definition is_positive (ε : 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 "f64", "is_sign_positive", [] |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_positive : M.IsAssociatedFunction Self "is_positive" is_positive.
    
    (*
        pub const fn is_sign_negative(self) -> bool {
            // IEEE754 says: isSignMinus(x) is true if and only if x has negative sign. isSignMinus
            // applies to zeros and NaNs as well.
            // SAFETY: This is just transmuting to get the sign bit, it's fine.
            unsafe { mem::transmute::<f64, u64>(self) & Self::SIGN_MASK != 0 }
        }
    *)
    Definition is_sign_negative (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.ne (|
            BinOp.bit_and
              (M.call_closure (|
                M.get_function (|
                  "core::intrinsics::transmute",
                  [ Ty.path "f64"; Ty.path "u64" ]
                |),
                [ M.read (| self |) ]
              |))
              (M.read (| M.get_constant (| "core::f64::SIGN_MASK" |) |)),
            Value.Integer IntegerKind.U64 0
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_sign_negative :
      M.IsAssociatedFunction Self "is_sign_negative" is_sign_negative.
    
    (*
        pub fn is_negative(self) -> bool {
            self.is_sign_negative()
        }
    *)
    Definition is_negative (ε : 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 "f64", "is_sign_negative", [] |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_negative : M.IsAssociatedFunction Self "is_negative" is_negative.
    
    (*
        pub const fn next_up(self) -> Self {
            // Some targets violate Rust's assumption of IEEE semantics, e.g. by flushing
            // denormals to zero. This is in general unsound and unsupported, but here
            // we do our best to still produce the correct result on such targets.
            let bits = self.to_bits();
            if self.is_nan() || bits == Self::INFINITY.to_bits() {
                return self;
            }
    
            let abs = bits & !Self::SIGN_MASK;
            let next_bits = if abs == 0 {
                Self::TINY_BITS
            } else if bits == abs {
                bits + 1
            } else {
                bits - 1
            };
            Self::from_bits(next_bits)
        }
    *)
    Definition next_up (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ bits :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "f64", "to_bits", [] |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.or (|
                                  M.call_closure (|
                                    M.get_associated_function (| Ty.path "f64", "is_nan", [] |),
                                    [ M.read (| self |) ]
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.eq (|
                                      M.read (| bits |),
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "f64",
                                          "to_bits",
                                          []
                                        |),
                                        [ M.read (| M.get_constant (| "core::f64::INFINITY" |) |) ]
                                      |)
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (| M.read (| M.return_ (| M.read (| self |) |) |) |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ abs :=
                  M.alloc (|
                    BinOp.bit_and
                      (M.read (| bits |))
                      (UnOp.not (| M.read (| M.get_constant (| "core::f64::SIGN_MASK" |) |) |))
                  |) in
                let~ next_bits :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.eq (| M.read (| abs |), Value.Integer IntegerKind.U64 0 |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.get_constant (| "core::f64::TINY_BITS" |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.eq (| M.read (| bits |), M.read (| abs |) |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      BinOp.Wrap.add (|
                                        M.read (| bits |),
                                        Value.Integer IntegerKind.U64 1
                                      |)
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      BinOp.Wrap.sub (|
                                        M.read (| bits |),
                                        Value.Integer IntegerKind.U64 1
                                      |)
                                    |)))
                              ]
                            |)))
                      ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "f64", "from_bits", [] |),
                    [ M.read (| next_bits |) ]
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_next_up : M.IsAssociatedFunction Self "next_up" next_up.
    
    (*
        pub const fn next_down(self) -> Self {
            // Some targets violate Rust's assumption of IEEE semantics, e.g. by flushing
            // denormals to zero. This is in general unsound and unsupported, but here
            // we do our best to still produce the correct result on such targets.
            let bits = self.to_bits();
            if self.is_nan() || bits == Self::NEG_INFINITY.to_bits() {
                return self;
            }
    
            let abs = bits & !Self::SIGN_MASK;
            let next_bits = if abs == 0 {
                Self::NEG_TINY_BITS
            } else if bits == abs {
                bits - 1
            } else {
                bits + 1
            };
            Self::from_bits(next_bits)
        }
    *)
    Definition next_down (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ bits :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "f64", "to_bits", [] |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.or (|
                                  M.call_closure (|
                                    M.get_associated_function (| Ty.path "f64", "is_nan", [] |),
                                    [ M.read (| self |) ]
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.eq (|
                                      M.read (| bits |),
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "f64",
                                          "to_bits",
                                          []
                                        |),
                                        [
                                          M.read (|
                                            M.get_constant (| "core::f64::NEG_INFINITY" |)
                                          |)
                                        ]
                                      |)
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (| M.read (| M.return_ (| M.read (| self |) |) |) |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ abs :=
                  M.alloc (|
                    BinOp.bit_and
                      (M.read (| bits |))
                      (UnOp.not (| M.read (| M.get_constant (| "core::f64::SIGN_MASK" |) |) |))
                  |) in
                let~ next_bits :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.eq (| M.read (| abs |), Value.Integer IntegerKind.U64 0 |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.get_constant (| "core::f64::NEG_TINY_BITS" |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.eq (| M.read (| bits |), M.read (| abs |) |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      BinOp.Wrap.sub (|
                                        M.read (| bits |),
                                        Value.Integer IntegerKind.U64 1
                                      |)
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      BinOp.Wrap.add (|
                                        M.read (| bits |),
                                        Value.Integer IntegerKind.U64 1
                                      |)
                                    |)))
                              ]
                            |)))
                      ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "f64", "from_bits", [] |),
                    [ M.read (| next_bits |) ]
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_next_down : M.IsAssociatedFunction Self "next_down" next_down.
    
    (*
        pub fn recip(self) -> f64 {
            1.0 / self
        }
    *)
    Definition recip (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.Wrap.div (| M.read (| UnsupportedLiteral |), M.read (| self |) |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_recip : M.IsAssociatedFunction Self "recip" recip.
    
    (*
        pub fn to_degrees(self) -> f64 {
            // The division here is correctly rounded with respect to the true
            // value of 180/π. (This differs from f32, where a constant must be
            // used to ensure a correctly rounded result.)
            self * (180.0f64 / consts::PI)
        }
    *)
    Definition to_degrees (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.Wrap.mul (|
            M.read (| self |),
            BinOp.Wrap.div (|
              M.read (| UnsupportedLiteral |),
              M.read (| M.get_constant (| "core::f64::consts::PI" |) |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_degrees : M.IsAssociatedFunction Self "to_degrees" to_degrees.
    
    (*
        pub fn to_radians(self) -> f64 {
            const RADS_PER_DEG: f64 = consts::PI / 180.0;
            self * RADS_PER_DEG
        }
    *)
    Definition to_radians (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.Wrap.mul (|
            M.read (| self |),
            M.read (| M.get_constant (| "core::f64::to_radians::RADS_PER_DEG" |) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_radians : M.IsAssociatedFunction Self "to_radians" to_radians.
    
    (*
        pub fn max(self, other: f64) -> f64 {
            intrinsics::maxnumf64(self, other)
        }
    *)
    Definition max (ε : 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_function (| "core::intrinsics::maxnumf64", [] |),
            [ M.read (| self |); M.read (| other |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_max : M.IsAssociatedFunction Self "max" max.
    
    (*
        pub fn min(self, other: f64) -> f64 {
            intrinsics::minnumf64(self, other)
        }
    *)
    Definition min (ε : 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_function (| "core::intrinsics::minnumf64", [] |),
            [ M.read (| self |); M.read (| other |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_min : M.IsAssociatedFunction Self "min" min.
    
    (*
        pub fn maximum(self, other: f64) -> f64 {
            if self > other {
                self
            } else if other > self {
                other
            } else if self == other {
                if self.is_sign_positive() && other.is_sign_negative() { self } else { other }
            } else {
                self + other
            }
        }
    *)
    Definition maximum (ε : 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 (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use (M.alloc (| BinOp.gt (| M.read (| self |), M.read (| other |) |) |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    self));
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.gt (| M.read (| other |), M.read (| self |) |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            other));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.eq (| M.read (| self |), M.read (| other |) |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  LogicalOp.and (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path "f64",
                                                        "is_sign_positive",
                                                        []
                                                      |),
                                                      [ M.read (| self |) ]
                                                    |),
                                                    ltac:(M.monadic
                                                      (M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "f64",
                                                          "is_sign_negative",
                                                          []
                                                        |),
                                                        [ M.read (| other |) ]
                                                      |)))
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            self));
                                        fun γ => ltac:(M.monadic other)
                                      ]
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)
                                    |)))
                              ]
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_maximum : M.IsAssociatedFunction Self "maximum" maximum.
    
    (*
        pub fn minimum(self, other: f64) -> f64 {
            if self < other {
                self
            } else if other < self {
                other
            } else if self == other {
                if self.is_sign_negative() && other.is_sign_positive() { self } else { other }
            } else {
                // At least one input is NaN. Use `+` to perform NaN propagation and quieting.
                self + other
            }
        }
    *)
    Definition minimum (ε : 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 (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use (M.alloc (| BinOp.lt (| M.read (| self |), M.read (| other |) |) |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    self));
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.lt (| M.read (| other |), M.read (| self |) |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            other));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.eq (| M.read (| self |), M.read (| other |) |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  LogicalOp.and (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path "f64",
                                                        "is_sign_negative",
                                                        []
                                                      |),
                                                      [ M.read (| self |) ]
                                                    |),
                                                    ltac:(M.monadic
                                                      (M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "f64",
                                                          "is_sign_positive",
                                                          []
                                                        |),
                                                        [ M.read (| other |) ]
                                                      |)))
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            self));
                                        fun γ => ltac:(M.monadic other)
                                      ]
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)
                                    |)))
                              ]
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_minimum : M.IsAssociatedFunction Self "minimum" minimum.
    
    (*
        pub fn midpoint(self, other: f64) -> f64 {
            const LO: f64 = f64::MIN_POSITIVE * 2.;
            const HI: f64 = f64::MAX / 2.;
    
            let (a, b) = (self, other);
            let abs_a = a.abs_private();
            let abs_b = b.abs_private();
    
            if abs_a <= HI && abs_b <= HI {
                // Overflow is impossible
                (a + b) / 2.
            } else if abs_a < LO {
                // Not safe to halve `a` (would underflow)
                a + (b / 2.)
            } else if abs_b < LO {
                // Not safe to halve `b` (would underflow)
                (a / 2.) + b
            } else {
                // Safe to halve `a` and `b`
                (a / 2.) + (b / 2.)
            }
        }
    *)
    Definition midpoint (ε : 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 (|
            M.match_operator (|
              M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
              [
                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 a := M.copy (| γ0_0 |) in
                    let b := M.copy (| γ0_1 |) in
                    let~ abs_a :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "f64", "abs_private", [] |),
                          [ M.read (| a |) ]
                        |)
                      |) in
                    let~ abs_b :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "f64", "abs_private", [] |),
                          [ M.read (| b |) ]
                        |)
                      |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  LogicalOp.and (|
                                    BinOp.le (|
                                      M.read (| abs_a |),
                                      M.read (| M.get_constant (| "core::f64::midpoint::HI" |) |)
                                    |),
                                    ltac:(M.monadic
                                      (BinOp.le (|
                                        M.read (| abs_b |),
                                        M.read (| M.get_constant (| "core::f64::midpoint::HI" |) |)
                                      |)))
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              BinOp.Wrap.div (|
                                BinOp.Wrap.add (| M.read (| a |), M.read (| b |) |),
                                M.read (| UnsupportedLiteral |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.lt (|
                                            M.read (| abs_a |),
                                            M.read (|
                                              M.get_constant (| "core::f64::midpoint::LO" |)
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      BinOp.Wrap.add (|
                                        M.read (| a |),
                                        BinOp.Wrap.div (|
                                          M.read (| b |),
                                          M.read (| UnsupportedLiteral |)
                                        |)
                                      |)
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  BinOp.lt (|
                                                    M.read (| abs_b |),
                                                    M.read (|
                                                      M.get_constant (| "core::f64::midpoint::LO" |)
                                                    |)
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              BinOp.Wrap.add (|
                                                BinOp.Wrap.div (|
                                                  M.read (| a |),
                                                  M.read (| UnsupportedLiteral |)
                                                |),
                                                M.read (| b |)
                                              |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.alloc (|
                                              BinOp.Wrap.add (|
                                                BinOp.Wrap.div (|
                                                  M.read (| a |),
                                                  M.read (| UnsupportedLiteral |)
                                                |),
                                                BinOp.Wrap.div (|
                                                  M.read (| b |),
                                                  M.read (| UnsupportedLiteral |)
                                                |)
                                              |)
                                            |)))
                                      ]
                                    |)))
                              ]
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_midpoint : M.IsAssociatedFunction Self "midpoint" midpoint.
    
    (*
        pub unsafe fn to_int_unchecked<Int>(self) -> Int
        where
            Self: FloatToInt<Int>,
        {
            // SAFETY: the caller must uphold the safety contract for
            // `FloatToInt::to_int_unchecked`.
            unsafe { FloatToInt::<Int>::to_int_unchecked(self) }
        }
    *)
    Definition to_int_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ Int ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::convert::num::FloatToInt",
              Ty.path "f64",
              [ Int ],
              "to_int_unchecked",
              []
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_int_unchecked :
      M.IsAssociatedFunction Self "to_int_unchecked" to_int_unchecked.
    
    (*
        pub const fn to_bits(self) -> u64 {
            // SAFETY: `u64` is a plain old datatype so we can always transmute to it.
            unsafe { mem::transmute(self) }
        }
    *)
    Definition to_bits (ε : 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_function (| "core::intrinsics::transmute", [ Ty.path "f64"; Ty.path "u64" ] |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_bits : M.IsAssociatedFunction Self "to_bits" to_bits.
    
    (*
        pub const fn from_bits(v: u64) -> Self {
            // It turns out the safety issues with sNaN were overblown! Hooray!
            // SAFETY: `u64` is a plain old datatype so we can always transmute from it.
            unsafe { mem::transmute(v) }
        }
    *)
    Definition from_bits (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ v ] =>
        ltac:(M.monadic
          (let v := M.alloc (| v |) in
          M.call_closure (|
            M.get_function (| "core::intrinsics::transmute", [ Ty.path "u64"; Ty.path "f64" ] |),
            [ M.read (| v |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_bits : M.IsAssociatedFunction Self "from_bits" from_bits.
    
    (*
        pub const fn to_be_bytes(self) -> [u8; 8] {
            self.to_bits().to_be_bytes()
        }
    *)
    Definition to_be_bytes (ε : 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 "u64", "to_be_bytes", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "f64", "to_bits", [] |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_be_bytes : M.IsAssociatedFunction Self "to_be_bytes" to_be_bytes.
    
    (*
        pub const fn to_le_bytes(self) -> [u8; 8] {
            self.to_bits().to_le_bytes()
        }
    *)
    Definition to_le_bytes (ε : 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 "u64", "to_le_bytes", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "f64", "to_bits", [] |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_le_bytes : M.IsAssociatedFunction Self "to_le_bytes" to_le_bytes.
    
    (*
        pub const fn to_ne_bytes(self) -> [u8; 8] {
            self.to_bits().to_ne_bytes()
        }
    *)
    Definition to_ne_bytes (ε : 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 "u64", "to_ne_bytes", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "f64", "to_bits", [] |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_ne_bytes : M.IsAssociatedFunction Self "to_ne_bytes" to_ne_bytes.
    
    (*
        pub const fn from_be_bytes(bytes: [u8; 8]) -> Self {
            Self::from_bits(u64::from_be_bytes(bytes))
        }
    *)
    Definition from_be_bytes (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ bytes ] =>
        ltac:(M.monadic
          (let bytes := M.alloc (| bytes |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "f64", "from_bits", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "u64", "from_be_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_be_bytes :
      M.IsAssociatedFunction Self "from_be_bytes" from_be_bytes.
    
    (*
        pub const fn from_le_bytes(bytes: [u8; 8]) -> Self {
            Self::from_bits(u64::from_le_bytes(bytes))
        }
    *)
    Definition from_le_bytes (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ bytes ] =>
        ltac:(M.monadic
          (let bytes := M.alloc (| bytes |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "f64", "from_bits", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "u64", "from_le_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_le_bytes :
      M.IsAssociatedFunction Self "from_le_bytes" from_le_bytes.
    
    (*
        pub const fn from_ne_bytes(bytes: [u8; 8]) -> Self {
            Self::from_bits(u64::from_ne_bytes(bytes))
        }
    *)
    Definition from_ne_bytes (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ bytes ] =>
        ltac:(M.monadic
          (let bytes := M.alloc (| bytes |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "f64", "from_bits", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "u64", "from_ne_bytes", [] |),
                [ M.read (| bytes |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_ne_bytes :
      M.IsAssociatedFunction Self "from_ne_bytes" from_ne_bytes.
    
    (*
        pub fn total_cmp(&self, other: &Self) -> crate::cmp::Ordering {
            let mut left = self.to_bits() as i64;
            let mut right = other.to_bits() as i64;
    
            // In case of negatives, flip all the bits except the sign
            // to achieve a similar layout as two's complement integers
            //
            // Why does this work? IEEE 754 floats consist of three fields:
            // Sign bit, exponent and mantissa. The set of exponent and mantissa
            // fields as a whole have the property that their bitwise order is
            // equal to the numeric magnitude where the magnitude is defined.
            // The magnitude is not normally defined on NaN values, but
            // IEEE 754 totalOrder defines the NaN values also to follow the
            // bitwise order. This leads to order explained in the doc comment.
            // However, the representation of magnitude is the same for negative
            // and positive numbers – only the sign bit is different.
            // To easily compare the floats as signed integers, we need to
            // flip the exponent and mantissa bits in case of negative numbers.
            // We effectively convert the numbers to "two's complement" form.
            //
            // To do the flipping, we construct a mask and XOR against it.
            // We branchlessly calculate an "all-ones except for the sign bit"
            // mask from negative-signed values: right shifting sign-extends
            // the integer, so we "fill" the mask with sign bits, and then
            // convert to unsigned to push one more zero bit.
            // On positive values, the mask is all zeros, so it's a no-op.
            left ^= (((left >> 63) as u64) >> 1) as i64;
            right ^= (((right >> 63) as u64) >> 1) as i64;
    
            left.cmp(&right)
        }
    *)
    Definition total_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.read (|
            let~ left :=
              M.alloc (|
                M.rust_cast
                  (M.call_closure (|
                    M.get_associated_function (| Ty.path "f64", "to_bits", [] |),
                    [ M.read (| M.read (| self |) |) ]
                  |))
              |) in
            let~ right :=
              M.alloc (|
                M.rust_cast
                  (M.call_closure (|
                    M.get_associated_function (| Ty.path "f64", "to_bits", [] |),
                    [ M.read (| M.read (| other |) |) ]
                  |))
              |) in
            let~ _ :=
              let β := left in
              M.write (|
                β,
                BinOp.bit_xor
                  (M.read (| β |))
                  (M.rust_cast
                    (BinOp.Wrap.shr (|
                      M.rust_cast
                        (BinOp.Wrap.shr (| M.read (| left |), Value.Integer IntegerKind.I32 63 |)),
                      Value.Integer IntegerKind.I32 1
                    |)))
              |) in
            let~ _ :=
              let β := right in
              M.write (|
                β,
                BinOp.bit_xor
                  (M.read (| β |))
                  (M.rust_cast
                    (BinOp.Wrap.shr (|
                      M.rust_cast
                        (BinOp.Wrap.shr (| M.read (| right |), Value.Integer IntegerKind.I32 63 |)),
                      Value.Integer IntegerKind.I32 1
                    |)))
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::cmp::Ord", Ty.path "i64", [], "cmp", [] |),
                [ left; right ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_total_cmp : M.IsAssociatedFunction Self "total_cmp" total_cmp.
    
    (*
        pub fn clamp(mut self, min: f64, max: f64) -> f64 {
            assert!(min <= max, "min > max, or either was NaN. min = {min:?}, max = {max:?}");
            if self < min {
                self = min;
            }
            if self > max {
                self = max;
            }
            self
        }
    *)
    Definition clamp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; min; max ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let min := M.alloc (| min |) in
          let max := M.alloc (| max |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            UnOp.not (| BinOp.le (| M.read (| min |), M.read (| max |) |) |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::panicking::panic_fmt", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_v1",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.read (|
                                          Value.String "min > max, or either was NaN. min = "
                                        |);
                                        M.read (| Value.String ", max = " |)
                                      ]
                                  |);
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Argument",
                                            "new_debug",
                                            [ Ty.path "f64" ]
                                          |),
                                          [ min ]
                                        |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Argument",
                                            "new_debug",
                                            [ Ty.path "f64" ]
                                          |),
                                          [ max ]
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use (M.alloc (| BinOp.lt (| M.read (| self |), M.read (| min |) |) |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ := M.write (| self, M.read (| min |) |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use (M.alloc (| BinOp.gt (| M.read (| self |), M.read (| max |) |) |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ := M.write (| self, M.read (| max |) |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_clamp : M.IsAssociatedFunction Self "clamp" clamp.
  End Impl_f64.
End f64.
