val fmul_regs_modified: MS.reg_64 -> bool
val fmul_regs_modified: MS.reg_64 -> bool
let fmul_regs_modified: MS.reg_64 -> bool = fun (r:MS.reg_64) ->
  let open MS in
  if r = rRax || r = rRbx || r = rRcx || r = rRdx || r = rRdi || r = rRsi || r = rR8 || r = rR9 || r = rR10 || r = rR11 || r = rR13 || r = rR14 then true
  else false
module Vale.Inline.X64.Fmul_inline

open FStar.Mul
open FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module DV = LowStar.BufferView.Down
open Vale.Def.Types_s

open Vale.Interop.Base
module IX64 = Vale.Interop.X64
module VSig = Vale.AsLowStar.ValeSig
module LSig = Vale.AsLowStar.LowStarSig
module ME = Vale.X64.Memory
module V = Vale.X64.Decls
module IA = Vale.Interop.Assumptions
module W = Vale.AsLowStar.Wrapper
open Vale.X64.MemoryAdapters
module VS = Vale.X64.State
module MS = Vale.X64.Machine_s
module PR = Vale.X64.Print_Inline_s

module FU = Vale.Curve25519.X64.FastUtil
module FH = Vale.Curve25519.X64.FastHybrid
module FW = Vale.Curve25519.X64.FastWide

let uint64 = UInt64.t

(* A little utility to trigger normalization in types *)
let as_t (#a:Type) (x:normal a) : a = x
let as_normal_t (#a:Type) (x:a) : normal a = x

[@__reduce__]
let b64 = buf_t TUInt64 TUInt64
[@__reduce__]
let t64_mod = TD_Buffer TUInt64 TUInt64 default_bq
[@__reduce__]
let t64_no_mod = TD_Buffer TUInt64 TUInt64 ({modified=false; strict_disjointness=false; taint=MS.Secret})
[@__reduce__]
let tuint64 = TD_Base TUInt64


[@__reduce__]
let fmul_dom: IX64.arity_ok 4 td =
  let y = [t64_mod; t64_no_mod; t64_no_mod; t64_mod] in
  assert_norm (List.length y = 4);
  y

(* Need to rearrange the order of arguments *)
[@__reduce__]
let fmul_pre : VSig.vale_pre fmul_dom =
  fun (c:V.va_code)
    (out:b64)
    (f1:b64)
    (f2:b64)
    (tmp:b64)
    (va_s0:V.va_state) ->
      FW.va_req_Fmul c va_s0
        (as_vale_buffer tmp) (as_vale_buffer f1) (as_vale_buffer out) (as_vale_buffer f2)

[@__reduce__]
let fmul_post : VSig.vale_post fmul_dom =
  fun (c:V.va_code)
    (out:b64)
    (f1:b64)
    (f2:b64)
    (tmp:b64)
    (va_s0:V.va_state)
    (va_s1:V.va_state)
    (f:V.va_fuel) ->
      FW.va_ens_Fmul c va_s0 (as_vale_buffer tmp) (as_vale_buffer f1) (as_vale_buffer out) (as_vale_buffer f2) va_s1 f
/
Vale.X64.State.fsti.checked Vale.X64.Print_Inline_s.fst.checked Vale.X64.MemoryAdapters.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.Decls.fsti.checked Vale.Interop.X64.fsti.checked Vale.Interop.Base.fst.checked Vale.Interop.Assumptions.fst.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.X64.FastWide.fsti.checked Vale.Curve25519.X64.FastUtil.fsti.checked Vale.Curve25519.X64.FastHybrid.fsti.checked Vale.AsLowStar.Wrapper.fsti.checked Vale.AsLowStar.ValeSig.fst.checked Vale.AsLowStar.MemoryHelpers.fsti.checked Vale.AsLowStar.LowStarSig.fst.checked prims.fst.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.UInt64.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.All.fst.checked
Vale.Inline.X64.Fmul_inline.fst
r: Vale.X64.Machine_s.reg_64 -> Prims.bool
Vale.X64.Machine_s.reg_64 Prims.op_BarBar Prims.op_Equality Vale.X64.Machine_s.rRax Vale.X64.Machine_s.rRbx Vale.X64.Machine_s.rRcx Vale.X64.Machine_s.rRdx Vale.X64.Machine_s.rRdi Vale.X64.Machine_s.rRsi Vale.X64.Machine_s.rR8 Vale.X64.Machine_s.rR9 Vale.X64.Machine_s.rR10 Vale.X64.Machine_s.rR11 Vale.X64.Machine_s.rR13 Vale.X64.Machine_s.rR14 Prims.bool
let fmul_regs_modified: MS.reg_64 -> bool =
  
fun (r: MS.reg_64) ->
  let open MS in
  if
    r = rRax || r = rRbx || r = rRcx || r = rRdx || r = rRdi || r = rRsi || r = rR8 || r = rR9 ||
    r = rR10 ||
    r = rR11 ||
    r = rR13 ||
    r = rR14
  then true
  else false