val va_req_Memcpy (va_b0: va_code) (va_s0: va_state) (win: bool) (dst src: buffer64) : prop
let va_req_Memcpy (va_b0:va_code) (va_s0:va_state) (win:bool) (dst:buffer64) (src:buffer64) : prop =
  (va_require_total va_b0 (va_code_Memcpy win) va_s0 /\ va_get_ok va_s0 /\
    Vale.X64.Memory.is_initial_heap (va_get_mem_layout va_s0) (va_get_mem va_s0) /\
    Vale.X64.Decls.locs_disjoint ([Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 dst;
    Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 src]) /\ Vale.X64.Decls.validSrcAddrs64
    (va_get_mem va_s0) (if win then va_get_reg64 rRdx va_s0 else va_get_reg64 rRsi va_s0) src 2
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validDstAddrs64 (va_get_mem va_s0) (if win
    then va_get_reg64 rRcx va_s0 else va_get_reg64 rRdi va_s0) dst 2 (va_get_mem_layout va_s0)
    Secret /\ Vale.X64.Decls.buffer_length #Vale.X64.Memory.vuint64 src == 2 /\
    Vale.X64.Decls.buffer_length #Vale.X64.Memory.vuint64 dst == 2)
val va_req_Memcpy (va_b0: va_code) (va_s0: va_state) (win: bool) (dst src: buffer64) : prop
let va_req_Memcpy (va_b0: va_code) (va_s0: va_state) (win: bool) (dst src: buffer64) : prop =
(va_require_total va_b0 (va_code_Memcpy win) va_s0 /\ va_get_ok va_s0 /\
  Vale.X64.Memory.is_initial_heap (va_get_mem_layout va_s0) (va_get_mem va_s0) /\
  Vale.X64.Decls.locs_disjoint ([
        Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 dst;
        Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 src
      ]) /\
  Vale.X64.Decls.validSrcAddrs64 (va_get_mem va_s0)
    (if win then va_get_reg64 rRdx va_s0 else va_get_reg64 rRsi va_s0)
    src
    2
    (va_get_mem_layout va_s0)
    Secret /\
  Vale.X64.Decls.validDstAddrs64 (va_get_mem va_s0)
    (if win then va_get_reg64 rRcx va_s0 else va_get_reg64 rRdi va_s0)
    dst
    2
    (va_get_mem_layout va_s0)
    Secret /\ Vale.X64.Decls.buffer_length #Vale.X64.Memory.vuint64 src == 2 /\
  Vale.X64.Decls.buffer_length #Vale.X64.Memory.vuint64 dst == 2)
Vale.Test.X64.Vale_memcpy.fsti.checked
Vale.X64.State.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.InsVector.fsti.checked Vale.X64.InsMem.fsti.checked Vale.X64.InsBasic.fsti.checked Vale.X64.Decls.fsti.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.Test.X64.Vale_memcpy.fsti
Vale.X64.Decls.va_code Vale.X64.Decls.va_state Prims.bool Vale.X64.Memory.buffer64 Prims.l_and Vale.X64.Decls.va_require_total Vale.Test.X64.Vale_memcpy.va_code_Memcpy Prims.b2t Vale.X64.Decls.va_get_ok Vale.X64.Memory.is_initial_heap Vale.X64.Decls.va_get_mem_layout Vale.X64.Decls.va_get_mem Vale.X64.Decls.locs_disjoint Prims.Cons Vale.X64.Memory.loc Vale.X64.Decls.loc_buffer Vale.X64.Memory.vuint64 Prims.Nil Vale.X64.Decls.validSrcAddrs64 Vale.X64.Decls.va_get_reg64 Vale.X64.Machine_s.rRdx Vale.X64.Machine_s.rRsi Prims.int Vale.Arch.HeapTypes_s.Secret Vale.X64.Decls.validDstAddrs64 Vale.X64.Machine_s.rRcx Vale.X64.Machine_s.rRdi Prims.eq2 Vale.X64.Decls.buffer_length Prims.prop
module Vale.Test.X64.Vale_memcpy

open Vale.Arch.HeapImpl
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.InsVector
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
#set-options "--z3rlimit 20"
//-- Memcpy

val va_code_Memcpy : win:bool -> Tot va_code

val va_codegen_success_Memcpy : win:bool -> Tot va_pbool
val va_req_Memcpy (va_b0: va_code) (va_s0: va_state) (win: bool) (dst src: buffer64) : prop

    va_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    win: Prims.bool ->
    dst: Vale.X64.Memory.buffer64 ->
    src: Vale.X64.Memory.buffer64
  -> Prims.prop