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

(*
fn main() {
    use std::arch::asm;

    fn mul(a: u64, b: u64) -> u128 {
        let lo: u64;
        let hi: u64;

        unsafe {
            asm!(
                // The x86 mul instruction takes rax as an implicit input and writes
                // the 128-bit result of the multiplication to rax:rdx.
                "mul {}",
                in(reg) a,
                inlateout("rax") b => lo,
                lateout("rdx") hi
            );
        }

        ((hi as u128) << 64) + lo as u128
    }
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] => ltac:(M.monadic (Value.Tuple []))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_main : M.IsFunction "inline_assembly_inlateout_mul::main" main.

Module main.
  (*
      fn mul(a: u64, b: u64) -> u128 {
          let lo: u64;
          let hi: u64;
  
          unsafe {
              asm!(
                  // The x86 mul instruction takes rax as an implicit input and writes
                  // the 128-bit result of the multiplication to rax:rdx.
                  "mul {}",
                  in(reg) a,
                  inlateout("rax") b => lo,
                  lateout("rdx") hi
              );
          }
  
          ((hi as u128) << 64) + lo as u128
      }
  *)
  Definition mul (ε : 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~ lo := M.copy (| Value.DeclaredButUndefined |) in
          let~ hi := M.copy (| Value.DeclaredButUndefined |) in
          let~ _ :=
            let~ _ := InlineAssembly in
            M.alloc (| Value.Tuple [] |) in
          M.alloc (|
            BinOp.Wrap.add (|
              BinOp.Wrap.shl (| M.rust_cast (M.read (| hi |)), Value.Integer IntegerKind.I32 64 |),
              M.rust_cast (M.read (| lo |))
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_mul : M.IsFunction "inline_assembly_inlateout_mul::main::mul" mul.
End main.
