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

Module num.
  Module dec2flt.
    Module lemire.
      (*
      pub fn compute_float<F: RawFloat>(q: i64, mut w: u64) -> BiasedFp {
          let fp_zero = BiasedFp::zero_pow2(0);
          let fp_inf = BiasedFp::zero_pow2(F::INFINITE_POWER);
          let fp_error = BiasedFp::zero_pow2(-1);
      
          // Short-circuit if the value can only be a literal 0 or infinity.
          if w == 0 || q < F::SMALLEST_POWER_OF_TEN as i64 {
              return fp_zero;
          } else if q > F::LARGEST_POWER_OF_TEN as i64 {
              return fp_inf;
          }
          // Normalize our significant digits, so the most-significant bit is set.
          let lz = w.leading_zeros();
          w <<= lz;
          let (lo, hi) = compute_product_approx(q, w, F::MANTISSA_EXPLICIT_BITS + 3);
          if lo == 0xFFFF_FFFF_FFFF_FFFF {
              // If we have failed to approximate w x 5^-q with our 128-bit value.
              // Since the addition of 1 could lead to an overflow which could then
              // round up over the half-way point, this can lead to improper rounding
              // of a float.
              //
              // However, this can only occur if q ∈ [-27, 55]. The upper bound of q
              // is 55 because 5^55 < 2^128, however, this can only happen if 5^q > 2^64,
              // since otherwise the product can be represented in 64-bits, producing
              // an exact result. For negative exponents, rounding-to-even can
              // only occur if 5^-q < 2^64.
              //
              // For detailed explanations of rounding for negative exponents, see
              // <https://arxiv.org/pdf/2101.11408.pdf#section.9.1>. For detailed
              // explanations of rounding for positive exponents, see
              // <https://arxiv.org/pdf/2101.11408.pdf#section.8>.
              let inside_safe_exponent = (q >= -27) && (q <= 55);
              if !inside_safe_exponent {
                  return fp_error;
              }
          }
          let upperbit = (hi >> 63) as i32;
          let mut mantissa = hi >> (upperbit + 64 - F::MANTISSA_EXPLICIT_BITS as i32 - 3);
          let mut power2 = power(q as i32) + upperbit - lz as i32 - F::MINIMUM_EXPONENT;
          if power2 <= 0 {
              if -power2 + 1 >= 64 {
                  // Have more than 64 bits below the minimum exponent, must be 0.
                  return fp_zero;
              }
              // Have a subnormal value.
              mantissa >>= -power2 + 1;
              mantissa += mantissa & 1;
              mantissa >>= 1;
              power2 = (mantissa >= (1_u64 << F::MANTISSA_EXPLICIT_BITS)) as i32;
              return BiasedFp { f: mantissa, e: power2 };
          }
          // Need to handle rounding ties. Normally, we need to round up,
          // but if we fall right in between and we have an even basis, we
          // need to round down.
          //
          // This will only occur if:
          //  1. The lower 64 bits of the 128-bit representation is 0.
          //      IE, 5^q fits in single 64-bit word.
          //  2. The least-significant bit prior to truncated mantissa is odd.
          //  3. All the bits truncated when shifting to mantissa bits + 1 are 0.
          //
          // Or, we may fall between two floats: we are exactly halfway.
          if lo <= 1
              && q >= F::MIN_EXPONENT_ROUND_TO_EVEN as i64
              && q <= F::MAX_EXPONENT_ROUND_TO_EVEN as i64
              && mantissa & 3 == 1
              && (mantissa << (upperbit + 64 - F::MANTISSA_EXPLICIT_BITS as i32 - 3)) == hi
          {
              // Zero the lowest bit, so we don't round up.
              mantissa &= !1_u64;
          }
          // Round-to-even, then shift the significant digits into place.
          mantissa += mantissa & 1;
          mantissa >>= 1;
          if mantissa >= (2_u64 << F::MANTISSA_EXPLICIT_BITS) {
              // Rounding up overflowed, so the carry bit is set. Set the
              // mantissa to 1 (only the implicit, hidden bit is set) and
              // increase the exponent.
              mantissa = 1_u64 << F::MANTISSA_EXPLICIT_BITS;
              power2 += 1;
          }
          // Zero out the hidden bit.
          mantissa &= !(1_u64 << F::MANTISSA_EXPLICIT_BITS);
          if power2 >= F::INFINITE_POWER {
              // Exponent is above largest normal value, must be infinite.
              return fp_inf;
          }
          BiasedFp { f: mantissa, e: power2 }
      }
      *)
      Definition compute_float (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ F ], [ q; w ] =>
          ltac:(M.monadic
            (let q := M.alloc (| q |) in
            let w := M.alloc (| w |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ fp_zero :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::num::dec2flt::common::BiasedFp",
                          "zero_pow2",
                          []
                        |),
                        [ Value.Integer IntegerKind.I32 0 ]
                      |)
                    |) in
                  let~ fp_inf :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::num::dec2flt::common::BiasedFp",
                          "zero_pow2",
                          []
                        |),
                        [
                          M.read (|
                            M.get_constant (|
                              "core::num::dec2flt::float::RawFloat::INFINITE_POWER"
                            |)
                          |)
                        ]
                      |)
                    |) in
                  let~ fp_error :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::num::dec2flt::common::BiasedFp",
                          "zero_pow2",
                          []
                        |),
                        [ Value.Integer IntegerKind.I32 (-1) ]
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  LogicalOp.or (|
                                    BinOp.eq (| M.read (| w |), Value.Integer IntegerKind.U64 0 |),
                                    ltac:(M.monadic
                                      (BinOp.lt (|
                                        M.read (| q |),
                                        M.rust_cast
                                          (M.read (|
                                            M.get_constant (|
                                              "core::num::dec2flt::float::RawFloat::SMALLEST_POWER_OF_TEN"
                                            |)
                                          |))
                                      |)))
                                  |)
                                |)) 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 (| fp_zero |) |) |) |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.gt (|
                                            M.read (| q |),
                                            M.rust_cast
                                              (M.read (|
                                                M.get_constant (|
                                                  "core::num::dec2flt::float::RawFloat::LARGEST_POWER_OF_TEN"
                                                |)
                                              |))
                                          |)
                                        |)) 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 (| fp_inf |) |) |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |)))
                      ]
                    |) in
                  let~ lz :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "u64", "leading_zeros", [] |),
                        [ M.read (| w |) ]
                      |)
                    |) in
                  let~ _ :=
                    let β := w in
                    M.write (| β, BinOp.Wrap.shl (| M.read (| β |), M.read (| lz |) |) |) in
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::num::dec2flt::lemire::compute_product_approx",
                          []
                        |),
                        [
                          M.read (| q |);
                          M.read (| w |);
                          BinOp.Wrap.add (|
                            M.read (|
                              M.get_constant (|
                                "core::num::dec2flt::float::RawFloat::MANTISSA_EXPLICIT_BITS"
                              |)
                            |),
                            Value.Integer IntegerKind.Usize 3
                          |)
                        ]
                      |)
                    |),
                    [
                      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 lo := M.copy (| γ0_0 |) in
                          let hi := M.copy (| γ0_1 |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.eq (|
                                            M.read (| lo |),
                                            Value.Integer IntegerKind.U64 18446744073709551615
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ inside_safe_exponent :=
                                      M.alloc (|
                                        LogicalOp.and (|
                                          BinOp.ge (|
                                            M.read (| q |),
                                            Value.Integer IntegerKind.I64 (-27)
                                          |),
                                          ltac:(M.monadic
                                            (BinOp.le (|
                                              M.read (| q |),
                                              Value.Integer IntegerKind.I64 55
                                            |)))
                                        |)
                                      |) in
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  UnOp.not (| M.read (| inside_safe_exponent |) |)
                                                |)) 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 (| fp_error |) |) |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ upperbit :=
                            M.alloc (|
                              M.rust_cast
                                (BinOp.Wrap.shr (|
                                  M.read (| hi |),
                                  Value.Integer IntegerKind.I32 63
                                |))
                            |) in
                          let~ mantissa :=
                            M.alloc (|
                              BinOp.Wrap.shr (|
                                M.read (| hi |),
                                BinOp.Wrap.sub (|
                                  BinOp.Wrap.sub (|
                                    BinOp.Wrap.add (|
                                      M.read (| upperbit |),
                                      Value.Integer IntegerKind.I32 64
                                    |),
                                    M.rust_cast
                                      (M.read (|
                                        M.get_constant (|
                                          "core::num::dec2flt::float::RawFloat::MANTISSA_EXPLICIT_BITS"
                                        |)
                                      |))
                                  |),
                                  Value.Integer IntegerKind.I32 3
                                |)
                              |)
                            |) in
                          let~ power2 :=
                            M.alloc (|
                              BinOp.Wrap.sub (|
                                BinOp.Wrap.sub (|
                                  BinOp.Wrap.add (|
                                    M.call_closure (|
                                      M.get_function (| "core::num::dec2flt::lemire::power", [] |),
                                      [ M.rust_cast (M.read (| q |)) ]
                                    |),
                                    M.read (| upperbit |)
                                  |),
                                  M.rust_cast (M.read (| lz |))
                                |),
                                M.read (|
                                  M.get_constant (|
                                    "core::num::dec2flt::float::RawFloat::MINIMUM_EXPONENT"
                                  |)
                                |)
                              |)
                            |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.le (|
                                            M.read (| power2 |),
                                            Value.Integer IntegerKind.I32 0
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          BinOp.ge (|
                                                            BinOp.Wrap.add (|
                                                              UnOp.neg (| M.read (| power2 |) |),
                                                              Value.Integer IntegerKind.I32 1
                                                            |),
                                                            Value.Integer IntegerKind.I32 64
                                                          |)
                                                        |)) 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 (| fp_zero |) |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          let~ _ :=
                                            let β := mantissa in
                                            M.write (|
                                              β,
                                              BinOp.Wrap.shr (|
                                                M.read (| β |),
                                                BinOp.Wrap.add (|
                                                  UnOp.neg (| M.read (| power2 |) |),
                                                  Value.Integer IntegerKind.I32 1
                                                |)
                                              |)
                                            |) in
                                          let~ _ :=
                                            let β := mantissa in
                                            M.write (|
                                              β,
                                              BinOp.Wrap.add (|
                                                M.read (| β |),
                                                BinOp.bit_and
                                                  (M.read (| mantissa |))
                                                  (Value.Integer IntegerKind.U64 1)
                                              |)
                                            |) in
                                          let~ _ :=
                                            let β := mantissa in
                                            M.write (|
                                              β,
                                              BinOp.Wrap.shr (|
                                                M.read (| β |),
                                                Value.Integer IntegerKind.I32 1
                                              |)
                                            |) in
                                          let~ _ :=
                                            M.write (|
                                              power2,
                                              M.rust_cast
                                                (BinOp.ge (|
                                                  M.read (| mantissa |),
                                                  BinOp.Wrap.shl (|
                                                    Value.Integer IntegerKind.U64 1,
                                                    M.read (|
                                                      M.get_constant (|
                                                        "core::num::dec2flt::float::RawFloat::MANTISSA_EXPLICIT_BITS"
                                                      |)
                                                    |)
                                                  |)
                                                |))
                                            |) in
                                          M.return_ (|
                                            Value.StructRecord
                                              "core::num::dec2flt::common::BiasedFp"
                                              [
                                                ("f", M.read (| mantissa |));
                                                ("e", M.read (| power2 |))
                                              ]
                                          |)
                                        |)
                                      |)
                                    |)));
                                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 (|
                                          LogicalOp.and (|
                                            LogicalOp.and (|
                                              LogicalOp.and (|
                                                LogicalOp.and (|
                                                  BinOp.le (|
                                                    M.read (| lo |),
                                                    Value.Integer IntegerKind.U64 1
                                                  |),
                                                  ltac:(M.monadic
                                                    (BinOp.ge (|
                                                      M.read (| q |),
                                                      M.rust_cast
                                                        (M.read (|
                                                          M.get_constant (|
                                                            "core::num::dec2flt::float::RawFloat::MIN_EXPONENT_ROUND_TO_EVEN"
                                                          |)
                                                        |))
                                                    |)))
                                                |),
                                                ltac:(M.monadic
                                                  (BinOp.le (|
                                                    M.read (| q |),
                                                    M.rust_cast
                                                      (M.read (|
                                                        M.get_constant (|
                                                          "core::num::dec2flt::float::RawFloat::MAX_EXPONENT_ROUND_TO_EVEN"
                                                        |)
                                                      |))
                                                  |)))
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.eq (|
                                                  BinOp.bit_and
                                                    (M.read (| mantissa |))
                                                    (Value.Integer IntegerKind.U64 3),
                                                  Value.Integer IntegerKind.U64 1
                                                |)))
                                            |),
                                            ltac:(M.monadic
                                              (BinOp.eq (|
                                                BinOp.Wrap.shl (|
                                                  M.read (| mantissa |),
                                                  BinOp.Wrap.sub (|
                                                    BinOp.Wrap.sub (|
                                                      BinOp.Wrap.add (|
                                                        M.read (| upperbit |),
                                                        Value.Integer IntegerKind.I32 64
                                                      |),
                                                      M.rust_cast
                                                        (M.read (|
                                                          M.get_constant (|
                                                            "core::num::dec2flt::float::RawFloat::MANTISSA_EXPLICIT_BITS"
                                                          |)
                                                        |))
                                                    |),
                                                    Value.Integer IntegerKind.I32 3
                                                  |)
                                                |),
                                                M.read (| hi |)
                                              |)))
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ _ :=
                                      let β := mantissa in
                                      M.write (|
                                        β,
                                        BinOp.bit_and
                                          (M.read (| β |))
                                          (UnOp.not (| Value.Integer IntegerKind.U64 1 |))
                                      |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ _ :=
                            let β := mantissa in
                            M.write (|
                              β,
                              BinOp.Wrap.add (|
                                M.read (| β |),
                                BinOp.bit_and
                                  (M.read (| mantissa |))
                                  (Value.Integer IntegerKind.U64 1)
                              |)
                            |) in
                          let~ _ :=
                            let β := mantissa in
                            M.write (|
                              β,
                              BinOp.Wrap.shr (| M.read (| β |), Value.Integer IntegerKind.I32 1 |)
                            |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.ge (|
                                            M.read (| mantissa |),
                                            BinOp.Wrap.shl (|
                                              Value.Integer IntegerKind.U64 2,
                                              M.read (|
                                                M.get_constant (|
                                                  "core::num::dec2flt::float::RawFloat::MANTISSA_EXPLICIT_BITS"
                                                |)
                                              |)
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        mantissa,
                                        BinOp.Wrap.shl (|
                                          Value.Integer IntegerKind.U64 1,
                                          M.read (|
                                            M.get_constant (|
                                              "core::num::dec2flt::float::RawFloat::MANTISSA_EXPLICIT_BITS"
                                            |)
                                          |)
                                        |)
                                      |) in
                                    let~ _ :=
                                      let β := power2 in
                                      M.write (|
                                        β,
                                        BinOp.Wrap.add (|
                                          M.read (| β |),
                                          Value.Integer IntegerKind.I32 1
                                        |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ _ :=
                            let β := mantissa in
                            M.write (|
                              β,
                              BinOp.bit_and
                                (M.read (| β |))
                                (UnOp.not (|
                                  BinOp.Wrap.shl (|
                                    Value.Integer IntegerKind.U64 1,
                                    M.read (|
                                      M.get_constant (|
                                        "core::num::dec2flt::float::RawFloat::MANTISSA_EXPLICIT_BITS"
                                      |)
                                    |)
                                  |)
                                |))
                            |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.ge (|
                                            M.read (| power2 |),
                                            M.read (|
                                              M.get_constant (|
                                                "core::num::dec2flt::float::RawFloat::INFINITE_POWER"
                                              |)
                                            |)
                                          |)
                                        |)) 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 (| fp_inf |) |) |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (|
                            Value.StructRecord
                              "core::num::dec2flt::common::BiasedFp"
                              [ ("f", M.read (| mantissa |)); ("e", M.read (| power2 |)) ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_compute_float :
        M.IsFunction "core::num::dec2flt::lemire::compute_float" compute_float.
      
      (*
      fn power(q: i32) -> i32 {
          (q.wrapping_mul(152_170 + 65536) >> 16) + 63
      }
      *)
      Definition power (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ q ] =>
          ltac:(M.monadic
            (let q := M.alloc (| q |) in
            BinOp.Wrap.add (|
              BinOp.Wrap.shr (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "i32", "wrapping_mul", [] |),
                  [
                    M.read (| q |);
                    BinOp.Wrap.add (|
                      Value.Integer IntegerKind.I32 152170,
                      Value.Integer IntegerKind.I32 65536
                    |)
                  ]
                |),
                Value.Integer IntegerKind.I32 16
              |),
              Value.Integer IntegerKind.I32 63
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_power : M.IsFunction "core::num::dec2flt::lemire::power" power.
      
      (*
      fn full_multiplication(a: u64, b: u64) -> (u64, u64) {
          let r = (a as u128) * (b as u128);
          (r as u64, (r >> 64) as u64)
      }
      *)
      Definition full_multiplication (ε : 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 (|
              let~ r :=
                M.alloc (|
                  BinOp.Wrap.mul (| M.rust_cast (M.read (| a |)), M.rust_cast (M.read (| b |)) |)
                |) in
              M.alloc (|
                Value.Tuple
                  [
                    M.rust_cast (M.read (| r |));
                    M.rust_cast
                      (BinOp.Wrap.shr (| M.read (| r |), Value.Integer IntegerKind.I32 64 |))
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_full_multiplication :
        M.IsFunction "core::num::dec2flt::lemire::full_multiplication" full_multiplication.
      
      (*
      fn compute_product_approx(q: i64, w: u64, precision: usize) -> (u64, u64) {
          debug_assert!(q >= SMALLEST_POWER_OF_FIVE as i64);
          debug_assert!(q <= LARGEST_POWER_OF_FIVE as i64);
          debug_assert!(precision <= 64);
      
          let mask = if precision < 64 {
              0xFFFF_FFFF_FFFF_FFFF_u64 >> precision
          } else {
              0xFFFF_FFFF_FFFF_FFFF_u64
          };
      
          // 5^q < 2^64, then the multiplication always provides an exact value.
          // That means whenever we need to round ties to even, we always have
          // an exact value.
          let index = (q - SMALLEST_POWER_OF_FIVE as i64) as usize;
          let (lo5, hi5) = POWER_OF_FIVE_128[index];
          // Only need one multiplication as long as there is 1 zero but
          // in the explicit mantissa bits, +1 for the hidden bit, +1 to
          // determine the rounding direction, +1 for if the computed
          // product has a leading zero.
          let (mut first_lo, mut first_hi) = full_multiplication(w, lo5);
          if first_hi & mask == mask {
              // Need to do a second multiplication to get better precision
              // for the lower product. This will always be exact
              // where q is < 55, since 5^55 < 2^128. If this wraps,
              // then we need to round up the hi product.
              let (_, second_hi) = full_multiplication(w, hi5);
              first_lo = first_lo.wrapping_add(second_hi);
              if second_hi > first_lo {
                  first_hi += 1;
              }
          }
          (first_lo, first_hi)
      }
      *)
      Definition compute_product_approx (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ q; w; precision ] =>
          ltac:(M.monadic
            (let q := M.alloc (| q |) in
            let w := M.alloc (| w |) in
            let precision := M.alloc (| precision |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.use (M.alloc (| Value.Bool true |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        UnOp.not (|
                                          BinOp.ge (|
                                            M.read (| q |),
                                            M.rust_cast
                                              (M.read (|
                                                M.get_constant (|
                                                  "core::num::dec2flt::table::SMALLEST_POWER_OF_FIVE"
                                                |)
                                              |))
                                          |)
                                        |)
                                      |)) 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", [] |),
                                        [
                                          M.read (|
                                            Value.String
                                              "assertion failed: q >= SMALLEST_POWER_OF_FIVE as i64"
                                          |)
                                        ]
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) 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 (| Value.Bool true |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        UnOp.not (|
                                          BinOp.le (|
                                            M.read (| q |),
                                            M.rust_cast
                                              (M.read (|
                                                M.get_constant (|
                                                  "core::num::dec2flt::table::LARGEST_POWER_OF_FIVE"
                                                |)
                                              |))
                                          |)
                                        |)
                                      |)) 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", [] |),
                                        [
                                          M.read (|
                                            Value.String
                                              "assertion failed: q <= LARGEST_POWER_OF_FIVE as i64"
                                          |)
                                        ]
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) 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 (| Value.Bool true |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        UnOp.not (|
                                          BinOp.le (|
                                            M.read (| precision |),
                                            Value.Integer IntegerKind.Usize 64
                                          |)
                                        |)
                                      |)) 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", [] |),
                                        [
                                          M.read (|
                                            Value.String "assertion failed: precision <= 64"
                                          |)
                                        ]
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ mask :=
                M.copy (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.read (| precision |),
                                  Value.Integer IntegerKind.Usize 64
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            BinOp.Wrap.shr (|
                              Value.Integer IntegerKind.U64 18446744073709551615,
                              M.read (| precision |)
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.alloc (| Value.Integer IntegerKind.U64 18446744073709551615 |)))
                    ]
                  |)
                |) in
              let~ index :=
                M.alloc (|
                  M.rust_cast
                    (BinOp.Wrap.sub (|
                      M.read (| q |),
                      M.rust_cast
                        (M.read (|
                          M.get_constant (| "core::num::dec2flt::table::SMALLEST_POWER_OF_FIVE" |)
                        |))
                    |))
                |) in
              M.match_operator (|
                M.SubPointer.get_array_field (|
                  M.read (| M.get_constant (| "core::num::dec2flt::table::POWER_OF_FIVE_128" |) |),
                  index
                |),
                [
                  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 lo5 := M.copy (| γ0_0 |) in
                      let hi5 := M.copy (| γ0_1 |) in
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "core::num::dec2flt::lemire::full_multiplication",
                              []
                            |),
                            [ M.read (| w |); M.read (| lo5 |) ]
                          |)
                        |),
                        [
                          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 first_lo := M.copy (| γ0_0 |) in
                              let first_hi := M.copy (| γ0_1 |) in
                              let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              BinOp.eq (|
                                                BinOp.bit_and
                                                  (M.read (| first_hi |))
                                                  (M.read (| mask |)),
                                                M.read (| mask |)
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::num::dec2flt::lemire::full_multiplication",
                                                []
                                              |),
                                              [ M.read (| w |); M.read (| hi5 |) ]
                                            |)
                                          |),
                                          [
                                            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 second_hi := M.copy (| γ0_1 |) in
                                                let~ _ :=
                                                  M.write (|
                                                    first_lo,
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path "u64",
                                                        "wrapping_add",
                                                        []
                                                      |),
                                                      [
                                                        M.read (| first_lo |);
                                                        M.read (| second_hi |)
                                                      ]
                                                    |)
                                                  |) in
                                                M.match_operator (|
                                                  M.alloc (| Value.Tuple [] |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ :=
                                                          M.use
                                                            (M.alloc (|
                                                              BinOp.gt (|
                                                                M.read (| second_hi |),
                                                                M.read (| first_lo |)
                                                              |)
                                                            |)) in
                                                        let _ :=
                                                          M.is_constant_or_break_match (|
                                                            M.read (| γ |),
                                                            Value.Bool true
                                                          |) in
                                                        let~ _ :=
                                                          let β := first_hi in
                                                          M.write (|
                                                            β,
                                                            BinOp.Wrap.add (|
                                                              M.read (| β |),
                                                              Value.Integer IntegerKind.U64 1
                                                            |)
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (M.alloc (| Value.Tuple [] |)))
                                                  ]
                                                |)))
                                          ]
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (|
                                Value.Tuple [ M.read (| first_lo |); M.read (| first_hi |) ]
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_compute_product_approx :
        M.IsFunction "core::num::dec2flt::lemire::compute_product_approx" compute_product_approx.
    End lemire.
  End dec2flt.
End num.
