Fast Inverse Square Root written in Rust, translated to Coq using https://github.com/formal-land/coq-of-rust

main.rs

fn q_rsqrt(number: f32) -> f32 {
    let threehalfs: f32 = 1.5;
    let x2: f32 = number * 0.5;
    let mut y: f32 = number;

    let i: u32 = y.to_bits(); // safely get the bit representation of the float
    let i: u32 = 0x5f3759df - (i >> 1); // what the heck?
    y = f32::from_bits(i); // safely convert bits back to float

    y * (threehalfs - (x2 * y * y)) // 1st iteration
    // y * (threehalfs - (x2 * y * y)) // 2nd iteration, can be removed
}

fn main() {
    println!("{}", q_rsqrt(4.0));
}

main.v

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

(*
fn q_rsqrt(number: f32) -> f32 {
    let threehalfs: f32 = 1.5;
    let x2: f32 = number * 0.5;
    let mut y: f32 = number;

    let i: u32 = y.to_bits(); // safely get the bit representation of the float
    let i: u32 = 0x5f3759df - (i >> 1); // what the heck?
    y = f32::from_bits(i); // safely convert bits back to float

    y * (threehalfs - (x2 * y * y)) // 1st iteration
    // y * (threehalfs - (x2 * y * y)) // 2nd iteration, can be removed
}
*)
Definition q_rsqrt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ number ] =>
    ltac:(M.monadic
      (let number := M.alloc (| number |) in
      M.read (|
        let~ threehalfs : Ty.path "f32" := M.copy (| UnsupportedLiteral |) in
        let~ x2 : Ty.path "f32" :=
          M.alloc (| BinOp.Wrap.mul (| M.read (| number |), M.read (| UnsupportedLiteral |) |) |) in
        let~ y : Ty.path "f32" := M.copy (| number |) in
        let~ i : Ty.path "u32" :=
          M.alloc (|
            M.call_closure (|
              Ty.path "u32",
              M.get_associated_function (| Ty.path "f32", "to_bits", [], [] |),
              [ M.read (| y |) ]
            |)
          |) in
        let~ i : Ty.path "u32" :=
          M.alloc (|
            BinOp.Wrap.sub (|
              Value.Integer IntegerKind.U32 1597463007,
              BinOp.Wrap.shr (| M.read (| i |), Value.Integer IntegerKind.I32 1 |)
            |)
          |) in
        let~ _ : Ty.tuple [] :=
          M.alloc (|
            M.write (|
              y,
              M.call_closure (|
                Ty.path "f32",
                M.get_associated_function (| Ty.path "f32", "from_bits", [], [] |),
                [ M.read (| i |) ]
              |)
            |)
          |) in
        M.alloc (|
          BinOp.Wrap.mul (|
            M.read (| y |),
            BinOp.Wrap.sub (|
              M.read (| threehalfs |),
              BinOp.Wrap.mul (|
                BinOp.Wrap.mul (| M.read (| x2 |), M.read (| y |) |),
                M.read (| y |)
              |)
            |)
          |)
        |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Global Instance Instance_IsFunction_q_rsqrt : M.IsFunction.Trait "main::q_rsqrt" q_rsqrt.
Admitted.
Global Typeclasses Opaque q_rsqrt.

(*
fn main() {
    println!("{}", q_rsqrt(4.0));
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ _ : Ty.tuple [] :=
          let~ _ : Ty.tuple [] :=
            M.alloc (|
              M.call_closure (|
                Ty.tuple [],
                M.get_function (| "std::io::stdio::_print", [], [] |),
                [
                  M.call_closure (|
                    Ty.path "core::fmt::Arguments",
                    M.get_associated_function (|
                      Ty.path "core::fmt::Arguments",
                      "new_v1",
                      [ Value.Integer IntegerKind.Usize 2; Value.Integer IntegerKind.Usize 1 ],
                      []
                    |),
                    [
                      M.borrow (|
                        Pointer.Kind.Ref,
                        M.deref (|
                          M.borrow (|
                            Pointer.Kind.Ref,
                            M.alloc (|
                              Value.Array
                                [ M.read (| Value.String "" |); M.read (| Value.String "
" |) ]
                            |)
                          |)
                        |)
                      |);
                      M.borrow (|
                        Pointer.Kind.Ref,
                        M.deref (|
                          M.borrow (|
                            Pointer.Kind.Ref,
                            M.alloc (|
                              Value.Array
                                [
                                  M.call_closure (|
                                    Ty.path "core::fmt::rt::Argument",
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_display",
                                      [],
                                      [ Ty.path "f32" ]
                                    |),
                                    [
                                      M.borrow (|
                                        Pointer.Kind.Ref,
                                        M.deref (|
                                          M.borrow (|
                                            Pointer.Kind.Ref,
                                            M.alloc (|
                                              M.call_closure (|
                                                Ty.path "f32",
                                                M.get_function (| "main::q_rsqrt", [], [] |),
                                                [ M.read (| UnsupportedLiteral |) ]
                                              |)
                                            |)
                                          |)
                                        |)
                                      |)
                                    ]
                                  |)
                                ]
                            |)
                          |)
                        |)
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Global Instance Instance_IsFunction_main : M.IsFunction.Trait "main::main" main.
Admitted.
Global Typeclasses Opaque main.