val va_req_Fmul (va_b0: va_code) (va_s0: va_state) (tmp_b inA_b dst_b inB_b: buffer64) : prop
let va_req_Fmul (va_b0:va_code) (va_s0:va_state) (tmp_b:buffer64) (inA_b:buffer64) (dst_b:buffer64)
  (inB_b:buffer64) : prop =
  (va_require_total va_b0 (va_code_Fmul ()) va_s0 /\ va_get_ok va_s0 /\ (let (tmp_in:nat64) =
    va_get_reg64 rRdi va_s0 in let (inA_in:nat64) = va_get_reg64 rRsi va_s0 in let (dst_in:nat64) =
    va_get_reg64 rR15 va_s0 in let (inB_in:nat64) = va_get_reg64 rRcx va_s0 in adx_enabled /\
    bmi2_enabled /\ Vale.X64.Memory.is_initial_heap (va_get_mem_layout va_s0) (va_get_mem va_s0) /\
    (Vale.X64.Decls.buffers_disjoint dst_b inA_b \/ dst_b == inA_b) /\
    (Vale.X64.Decls.buffers_disjoint dst_b inB_b \/ dst_b == inB_b) /\
    (Vale.X64.Decls.buffers_disjoint dst_b tmp_b \/ dst_b == tmp_b) /\
    Vale.X64.Decls.buffers_disjoint tmp_b inA_b /\ Vale.X64.Decls.buffers_disjoint tmp_b inB_b /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem va_s0) dst_in dst_b 4 (va_get_mem_layout va_s0)
    Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem va_s0) inA_in inA_b 4 (va_get_mem_layout
    va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem va_s0) inB_in inB_b 4
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validDstAddrs64 (va_get_mem va_s0) tmp_in
    tmp_b 8 (va_get_mem_layout va_s0) Secret))
val va_req_Fmul (va_b0: va_code) (va_s0: va_state) (tmp_b inA_b dst_b inB_b: buffer64) : prop
let va_req_Fmul (va_b0: va_code) (va_s0: va_state) (tmp_b inA_b dst_b inB_b: buffer64) : prop =
(va_require_total va_b0 (va_code_Fmul ()) va_s0 /\ va_get_ok va_s0 /\
  (let tmp_in:nat64 = va_get_reg64 rRdi va_s0 in
    let inA_in:nat64 = va_get_reg64 rRsi va_s0 in
    let dst_in:nat64 = va_get_reg64 rR15 va_s0 in
    let inB_in:nat64 = va_get_reg64 rRcx va_s0 in
    adx_enabled /\ bmi2_enabled /\
    Vale.X64.Memory.is_initial_heap (va_get_mem_layout va_s0) (va_get_mem va_s0) /\
    (Vale.X64.Decls.buffers_disjoint dst_b inA_b \/ dst_b == inA_b) /\
    (Vale.X64.Decls.buffers_disjoint dst_b inB_b \/ dst_b == inB_b) /\
    (Vale.X64.Decls.buffers_disjoint dst_b tmp_b \/ dst_b == tmp_b) /\
    Vale.X64.Decls.buffers_disjoint tmp_b inA_b /\ Vale.X64.Decls.buffers_disjoint tmp_b inB_b /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem va_s0)
      dst_in
      dst_b
      4
      (va_get_mem_layout va_s0)
      Secret /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem va_s0)
      inA_in
      inA_b
      4
      (va_get_mem_layout va_s0)
      Secret /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem va_s0)
      inB_in
      inB_b
      4
      (va_get_mem_layout va_s0)
      Secret /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem va_s0)
      tmp_in
      tmp_b
      8
      (va_get_mem_layout va_s0)
      Secret))
Vale.Curve25519.X64.FastWide.fsti.checked
Vale.X64.State.fsti.checked Vale.X64.Stack_i.fsti.checked Vale.X64.QuickCodes.fsti.checked Vale.X64.QuickCode.fst.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.InsStack.fsti.checked Vale.X64.InsMem.fsti.checked Vale.X64.InsBasic.fsti.checked Vale.X64.Flags.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.Fast_defs.fst.checked Vale.Arch.Types.fsti.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.Curve25519.X64.FastWide.fsti
Vale.X64.Decls.va_code Vale.X64.Decls.va_state Vale.X64.Memory.buffer64 Prims.l_and Vale.X64.Decls.va_require_total Vale.Curve25519.X64.FastWide.va_code_Fmul Prims.b2t Vale.X64.Decls.va_get_ok Vale.X64.CPU_Features_s.adx_enabled Vale.X64.CPU_Features_s.bmi2_enabled Vale.X64.Memory.is_initial_heap Vale.X64.Decls.va_get_mem_layout Vale.X64.Decls.va_get_mem Prims.l_or Vale.X64.Decls.buffers_disjoint Prims.eq2 Vale.X64.Decls.validDstAddrs64 Vale.Arch.HeapTypes_s.Secret Vale.X64.Decls.validSrcAddrs64 Vale.Def.Words_s.nat64 Vale.X64.Decls.va_get_reg64 Vale.X64.Machine_s.rRcx Vale.X64.Machine_s.rR15 Vale.X64.Machine_s.rRsi Vale.X64.Machine_s.rRdi Prims.prop
module Vale.Curve25519.X64.FastWide
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.Arch.HeapImpl
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.Stack_i
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.InsStack
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open Vale.Curve25519.Fast_defs
open Vale.X64.CPU_Features_s
//-- Fmul

val va_code_Fmul : va_dummy:unit -> Tot va_code

val va_codegen_success_Fmul : va_dummy:unit -> Tot va_pbool
let va_req_Fmul (va_b0:va_code) (va_s0:va_state) (tmp_b:buffer64) (inA_b:buffer64) (dst_b:buffer64)
val va_req_Fmul (va_b0: va_code) (va_s0: va_state) (tmp_b inA_b dst_b inB_b: buffer64) : prop

    va_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    tmp_b: Vale.X64.Memory.buffer64 ->
    inA_b: Vale.X64.Memory.buffer64 ->
    dst_b: Vale.X64.Memory.buffer64 ->
    inB_b: Vale.X64.Memory.buffer64
  -> Prims.prop