val va_wp_Memcpy
      (win: bool)
      (dst src: buffer64)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0
let va_wp_Memcpy (win:bool) (dst:buffer64) (src:buffer64) (va_s0:va_state) (va_k:(va_state -> unit
  -> Type0)) : Type0 =
  (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) (va_if win (fun _ -> va_get_reg64 rRdx va_s0) (fun _ -> va_get_reg64 rRsi
    va_s0)) src 2 (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validDstAddrs64 (va_get_mem
    va_s0) (va_if win (fun _ -> va_get_reg64 rRcx va_s0) (fun _ -> 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 /\ (forall
    (va_x_mem:vale_heap) (va_x_rax:nat64) (va_x_rcx:nat64) (va_x_r9:nat64)
    (va_x_memLayout:vale_heap_layout) (va_x_heap1:vale_heap) . let va_sM = va_upd_mem_heaplet 1
    va_x_heap1 (va_upd_mem_layout va_x_memLayout (va_upd_reg64 rR9 va_x_r9 (va_upd_reg64 rRcx
    va_x_rcx (va_upd_reg64 rRax va_x_rax (va_upd_mem va_x_mem va_s0))))) in va_get_ok va_sM /\
    Vale.X64.Memory.buffer_as_seq #Vale.X64.Memory.vuint64 (va_get_mem va_sM) dst ==
    Vale.X64.Memory.buffer_as_seq #Vale.X64.Memory.vuint64 (va_get_mem va_sM) src /\
    Vale.X64.Decls.modifies_mem (Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 dst)
    (va_get_mem va_s0) (va_get_mem va_sM) ==> va_k va_sM (())))
val va_wp_Memcpy
      (win: bool)
      (dst src: buffer64)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0
let va_wp_Memcpy
      (win: bool)
      (dst src: buffer64)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0 =
(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)
    (va_if win (fun _ -> va_get_reg64 rRdx va_s0) (fun _ -> va_get_reg64 rRsi va_s0))
    src
    2
    (va_get_mem_layout va_s0)
    Secret /\
  Vale.X64.Decls.validDstAddrs64 (va_get_mem va_s0)
    (va_if win (fun _ -> va_get_reg64 rRcx va_s0) (fun _ -> 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 /\
  (forall (va_x_mem: vale_heap)
      (va_x_rax: nat64)
      (va_x_rcx: nat64)
      (va_x_r9: nat64)
      (va_x_memLayout: vale_heap_layout)
      (va_x_heap1: vale_heap).
      let va_sM =
        va_upd_mem_heaplet 1
          va_x_heap1
          (va_upd_mem_layout va_x_memLayout
              (va_upd_reg64 rR9
                  va_x_r9
                  (va_upd_reg64 rRcx
                      va_x_rcx
                      (va_upd_reg64 rRax va_x_rax (va_upd_mem va_x_mem va_s0)))))
      in
      va_get_ok va_sM /\
      Vale.X64.Memory.buffer_as_seq #Vale.X64.Memory.vuint64 (va_get_mem va_sM) dst ==
      Vale.X64.Memory.buffer_as_seq #Vale.X64.Memory.vuint64 (va_get_mem va_sM) src /\
      Vale.X64.Decls.modifies_mem (Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 dst)
        (va_get_mem va_s0)
        (va_get_mem va_sM) ==>
      va_k va_sM (())))
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
Prims.bool Vale.X64.Memory.buffer64 Vale.X64.Decls.va_state Prims.unit Prims.l_and 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_if Vale.Def.Types_s.nat64 Vale.X64.Decls.va_get_reg64 Vale.X64.Machine_s.rRdx Prims.l_not Vale.X64.Machine_s.rRsi Vale.Arch.HeapTypes_s.Secret Vale.X64.Decls.validDstAddrs64 Vale.X64.Machine_s.rRcx Vale.X64.Machine_s.rRdi Prims.eq2 Prims.int Vale.X64.Decls.buffer_length Prims.l_Forall Vale.X64.InsBasic.vale_heap Vale.X64.Memory.nat64 Vale.Arch.HeapImpl.vale_heap_layout Prims.l_imp FStar.Seq.Base.seq Vale.X64.Memory.base_typ_as_vale_type Vale.X64.Memory.buffer_as_seq Vale.X64.Decls.modifies_mem Vale.X64.State.vale_state Vale.X64.Decls.va_upd_mem_heaplet Vale.X64.Decls.va_upd_mem_layout Vale.X64.Decls.va_upd_reg64 Vale.X64.Machine_s.rR9 Vale.X64.Machine_s.rRax Vale.X64.Decls.va_upd_mem
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
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)
let va_ens_Memcpy (va_b0:va_code) (va_s0:va_state) (win:bool) (dst:buffer64) (src:buffer64)
  (va_sM:va_state) (va_fM:va_fuel) : prop =
  (va_req_Memcpy va_b0 va_s0 win dst src /\ va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok
    va_sM /\ Vale.X64.Memory.buffer_as_seq #Vale.X64.Memory.vuint64 (va_get_mem va_sM) dst ==
    Vale.X64.Memory.buffer_as_seq #Vale.X64.Memory.vuint64 (va_get_mem va_sM) src /\
    Vale.X64.Decls.modifies_mem (Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 dst)
    (va_get_mem va_s0) (va_get_mem va_sM) /\ va_state_eq va_sM (va_update_mem_heaplet 1 va_sM
    (va_update_mem_layout va_sM (va_update_reg64 rR9 va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem va_sM va_s0))))))))

val va_lemma_Memcpy : va_b0:va_code -> va_s0:va_state -> win:bool -> dst:buffer64 -> src:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (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))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    Vale.X64.Memory.buffer_as_seq #Vale.X64.Memory.vuint64 (va_get_mem va_sM) dst ==
    Vale.X64.Memory.buffer_as_seq #Vale.X64.Memory.vuint64 (va_get_mem va_sM) src /\
    Vale.X64.Decls.modifies_mem (Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 dst)
    (va_get_mem va_s0) (va_get_mem va_sM) /\ va_state_eq va_sM (va_update_mem_heaplet 1 va_sM
    (va_update_mem_layout va_sM (va_update_reg64 rR9 va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem va_sM va_s0)))))))))
[@ va_qattr]
let va_wp_Memcpy (win:bool) (dst:buffer64) (src:buffer64) (va_s0:va_state) (va_k:(va_state -> unit
val va_wp_Memcpy
      (win: bool)
      (dst src: buffer64)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0

    win: Prims.bool ->
    dst: Vale.X64.Memory.buffer64 ->
    src: Vale.X64.Memory.buffer64 ->
    va_s0: Vale.X64.Decls.va_state ->
    va_k: (_: Vale.X64.Decls.va_state -> _: Prims.unit -> Type0)
  -> Type0