val va_lemma_Copy16 : va_b0:va_code -> va_s0:va_state -> t:taint -> bsrc:buffer64 -> bdst:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Copy16 t) va_s0 /\ va_get_ok va_s0 /\
    Vale.X64.Decls.locs_disjoint ([Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bsrc;
    Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bdst]) /\ Vale.X64.Decls.validSrcAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRsi va_s0) bsrc 2 (va_get_mem_layout va_s0) t /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) bdst 2
    (va_get_mem_layout va_s0) t))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    Vale.X64.Decls.locs_disjoint ([Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bsrc;
    Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bdst]) /\ Vale.X64.Decls.validSrcAddrs64
    (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRsi va_sM) bsrc 2 (va_get_mem_layout va_sM) t /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) bdst 2
    (va_get_mem_layout va_sM) t /\ (forall i . 0 <= i /\ i < 2 ==> Vale.X64.Decls.buffer64_read
    bdst i (va_get_mem_heaplet 0 va_sM) == Vale.X64.Decls.buffer64_read bsrc i (va_get_mem_heaplet
    0 va_sM)) /\ Vale.X64.Decls.modifies_mem (Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64
    bdst) (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet 0 va_sM) /\ va_state_eq va_sM
    (va_update_mem_heaplet 0 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)))))))
let va_lemma_Copy16 va_b0 va_s0 t bsrc bdst =
  va_reveal_opaque (`%va_code_Copy16) (va_code_Copy16 t);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let (va_s2, va_fc2) = va_lemma_Load64_buffer (va_hd va_b1) va_s0 (va_op_heaplet_mem_heaplet 0)
    (va_op_dst_opr64_reg64 rRax) (va_op_reg_opr64_reg64 rRsi) 0 t bsrc 0 in
  let va_b2 = va_tl va_b1 in
  let (va_s3, va_fc3) = va_lemma_Load64_buffer (va_hd va_b2) va_s2 (va_op_heaplet_mem_heaplet 0)
    (va_op_dst_opr64_reg64 rRcx) (va_op_reg_opr64_reg64 rRsi) 8 t bsrc 1 in
  let va_b3 = va_tl va_b2 in
  let (va_s4, va_fc4) = va_lemma_Store64_buffer (va_hd va_b3) va_s3 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rRax) 0 t bdst 0 in
  let va_b4 = va_tl va_b3 in
  let (va_s5, va_fc5) = va_lemma_Store64_buffer (va_hd va_b4) va_s4 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rRcx) 8 t bdst 1 in
  let va_b5 = va_tl va_b4 in
  let (va_sM, va_f5) = va_lemma_empty_total va_s5 va_b5 in
  let va_f4 = va_lemma_merge_total va_b4 va_s4 va_fc5 va_s5 va_f5 va_sM in
  let va_f3 = va_lemma_merge_total va_b3 va_s3 va_fc4 va_s4 va_f4 va_sM in
  let va_f2 = va_lemma_merge_total va_b2 va_s2 va_fc3 va_s3 va_f3 va_sM in
  let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc2 va_s2 va_f2 va_sM in
  (va_sM, va_fM)
val va_lemma_Copy16 : va_b0:va_code -> va_s0:va_state -> t:taint -> bsrc:buffer64 -> bdst:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Copy16 t) va_s0 /\ va_get_ok va_s0 /\
    Vale.X64.Decls.locs_disjoint ([Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bsrc;
    Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bdst]) /\ Vale.X64.Decls.validSrcAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRsi va_s0) bsrc 2 (va_get_mem_layout va_s0) t /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) bdst 2
    (va_get_mem_layout va_s0) t))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    Vale.X64.Decls.locs_disjoint ([Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bsrc;
    Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bdst]) /\ Vale.X64.Decls.validSrcAddrs64
    (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRsi va_sM) bsrc 2 (va_get_mem_layout va_sM) t /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) bdst 2
    (va_get_mem_layout va_sM) t /\ (forall i . 0 <= i /\ i < 2 ==> Vale.X64.Decls.buffer64_read
    bdst i (va_get_mem_heaplet 0 va_sM) == Vale.X64.Decls.buffer64_read bsrc i (va_get_mem_heaplet
    0 va_sM)) /\ Vale.X64.Decls.modifies_mem (Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64
    bdst) (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet 0 va_sM) /\ va_state_eq va_sM
    (va_update_mem_heaplet 0 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)))))))
let va_lemma_Copy16 va_b0 va_s0 t bsrc bdst =
va_reveal_opaque (`%va_code_Copy16) (va_code_Copy16 t);
let va_old_s:va_state = va_s0 in
let va_b1:va_codes = va_get_block va_b0 in
let va_s2, va_fc2 =
  va_lemma_Load64_buffer (va_hd va_b1)
    va_s0
    (va_op_heaplet_mem_heaplet 0)
    (va_op_dst_opr64_reg64 rRax)
    (va_op_reg_opr64_reg64 rRsi)
    0
    t
    bsrc
    0
in
let va_b2 = va_tl va_b1 in
let va_s3, va_fc3 =
  va_lemma_Load64_buffer (va_hd va_b2)
    va_s2
    (va_op_heaplet_mem_heaplet 0)
    (va_op_dst_opr64_reg64 rRcx)
    (va_op_reg_opr64_reg64 rRsi)
    8
    t
    bsrc
    1
in
let va_b3 = va_tl va_b2 in
let va_s4, va_fc4 =
  va_lemma_Store64_buffer (va_hd va_b3)
    va_s3
    (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rRax)
    0
    t
    bdst
    0
in
let va_b4 = va_tl va_b3 in
let va_s5, va_fc5 =
  va_lemma_Store64_buffer (va_hd va_b4)
    va_s4
    (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rRcx)
    8
    t
    bdst
    1
in
let va_b5 = va_tl va_b4 in
let va_sM, va_f5 = va_lemma_empty_total va_s5 va_b5 in
let va_f4 = va_lemma_merge_total va_b4 va_s4 va_fc5 va_s5 va_f5 va_sM in
let va_f3 = va_lemma_merge_total va_b3 va_s3 va_fc4 va_s4 va_f4 va_sM in
let va_f2 = va_lemma_merge_total va_b2 va_s2 va_fc3 va_s3 va_f3 va_sM in
let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc2 va_s2 va_f2 va_sM in
(va_sM, va_fM)
Vale.Test.X64.Memcpy.fst.checked
Vale.X64.State.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.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.Memcpy.fst
Vale.X64.Decls.va_code Vale.X64.Decls.va_state Vale.Arch.HeapTypes_s.taint Vale.X64.Memory.buffer64 Vale.X64.Decls.va_fuel FStar.Pervasives.Native.Mktuple2 Vale.X64.Decls.va_lemma_merge_total FStar.Pervasives.Native.tuple2 Vale.X64.State.vale_state Vale.X64.Decls.va_lemma_empty_total Prims.list Vale.X64.Machine_s.precode Vale.X64.Decls.ins Vale.X64.Decls.ocmp Vale.X64.Decls.va_tl Vale.X64.InsMem.va_lemma_Store64_buffer Vale.X64.Decls.va_hd Vale.X64.Decls.va_op_heaplet_mem_heaplet Vale.X64.Decls.va_op_reg_opr64_reg64 Vale.X64.Machine_s.rRdi Vale.X64.Machine_s.rRcx Vale.X64.Machine_s.rRax Vale.X64.InsMem.va_lemma_Load64_buffer Vale.X64.Decls.va_op_dst_opr64_reg64 Vale.X64.Machine_s.rRsi Vale.X64.Decls.va_get_block Prims.unit Vale.X64.Decls.va_reveal_opaque Vale.Test.X64.Memcpy.va_code_Copy16
module Vale.Test.X64.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
#reset-options "--z3rlimit 20"
//-- Copy16

val va_code_Copy16 : t:taint -> Tot va_code
[@ "opaque_to_smt"]
let va_code_Copy16 t =
  (va_Block (va_CCons (va_code_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64
    rRax) (va_op_reg_opr64_reg64 rRsi) 0 t) (va_CCons (va_code_Load64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRcx) (va_op_reg_opr64_reg64 rRsi) 8 t)
    (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rRax) 0 t) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet
    0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rRcx) 8 t) (va_CNil ()))))))

val va_codegen_success_Copy16 : t:taint -> Tot va_pbool
[@ "opaque_to_smt"]
let va_codegen_success_Copy16 t =
  (va_pbool_and (va_codegen_success_Load64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_dst_opr64_reg64 rRax) (va_op_reg_opr64_reg64 rRsi) 0 t) (va_pbool_and
    (va_codegen_success_Load64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_dst_opr64_reg64 rRcx)
    (va_op_reg_opr64_reg64 rRsi) 8 t) (va_pbool_and (va_codegen_success_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rRax) 0 t)
    (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rRcx) 8 t) (va_ttrue ())))))


val va_lemma_Copy16 : va_b0:va_code -> va_s0:va_state -> t:taint -> bsrc:buffer64 -> bdst:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Copy16 t) va_s0 /\ va_get_ok va_s0 /\
    Vale.X64.Decls.locs_disjoint ([Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bsrc;
    Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bdst]) /\ Vale.X64.Decls.validSrcAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRsi va_s0) bsrc 2 (va_get_mem_layout va_s0) t /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) bdst 2
    (va_get_mem_layout va_s0) t))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    Vale.X64.Decls.locs_disjoint ([Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bsrc;
    Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bdst]) /\ Vale.X64.Decls.validSrcAddrs64
    (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRsi va_sM) bsrc 2 (va_get_mem_layout va_sM) t /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) bdst 2
    (va_get_mem_layout va_sM) t /\ (forall i . 0 <= i /\ i < 2 ==> Vale.X64.Decls.buffer64_read
    bdst i (va_get_mem_heaplet 0 va_sM) == Vale.X64.Decls.buffer64_read bsrc i (va_get_mem_heaplet
    0 va_sM)) /\ Vale.X64.Decls.modifies_mem (Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64
    bdst) (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet 0 va_sM) /\ va_state_eq va_sM
    (va_update_mem_heaplet 0 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)))))))
[@"opaque_to_smt"]
val va_lemma_Copy16 : va_b0:va_code -> va_s0:va_state -> t:taint -> bsrc:buffer64 -> bdst:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Copy16 t) va_s0 /\ va_get_ok va_s0 /\
    Vale.X64.Decls.locs_disjoint ([Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bsrc;
    Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bdst]) /\ Vale.X64.Decls.validSrcAddrs64
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRsi va_s0) bsrc 2 (va_get_mem_layout va_s0) t /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) bdst 2
    (va_get_mem_layout va_s0) t))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    Vale.X64.Decls.locs_disjoint ([Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bsrc;
    Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64 bdst]) /\ Vale.X64.Decls.validSrcAddrs64
    (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRsi va_sM) bsrc 2 (va_get_mem_layout va_sM) t /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_sM) (va_get_reg64 rRdi va_sM) bdst 2
    (va_get_mem_layout va_sM) t /\ (forall i . 0 <= i /\ i < 2 ==> Vale.X64.Decls.buffer64_read
    bdst i (va_get_mem_heaplet 0 va_sM) == Vale.X64.Decls.buffer64_read bsrc i (va_get_mem_heaplet
    0 va_sM)) /\ Vale.X64.Decls.modifies_mem (Vale.X64.Decls.loc_buffer #Vale.X64.Memory.vuint64
    bdst) (va_get_mem_heaplet 0 va_s0) (va_get_mem_heaplet 0 va_sM) /\ va_state_eq va_sM
    (va_update_mem_heaplet 0 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_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    t: Vale.Arch.HeapTypes_s.taint ->
    bsrc: Vale.X64.Memory.buffer64 ->
    bdst: Vale.X64.Memory.buffer64
  -> Prims.Ghost (Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel)