val va_code_StoreBe64_buffer : h:va_operand_heaplet -> dst:va_operand_reg_opr64 ->
  src:va_operand_reg_opr64 -> offset:int -> t:taint -> Tot va_code
let va_code_StoreBe64_buffer h dst src offset t =
  (mk_ins (make_instr_annotate (I.ins_MovBe64) (S.AnnotateMovbe64 ()) (OMem ((MReg (get_reg dst)
    offset, t))) src))
val va_code_StoreBe64_buffer : h:va_operand_heaplet -> dst:va_operand_reg_opr64 ->
  src:va_operand_reg_opr64 -> offset:int -> t:taint -> Tot va_code
let va_code_StoreBe64_buffer h dst src offset t =
(mk_ins (make_instr_annotate (I.ins_MovBe64)
        (S.AnnotateMovbe64 ())
        (OMem ((MReg (get_reg dst) offset, t)))
        src))
Vale.X64.InsMem.fst.checked
Vale.X64.Taint_Semantics.fst.checked Vale.X64.StateLemmas.fsti.checked Vale.X64.Print_s.fst.checked Vale.X64.Memory_Sems.fsti.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Instructions_s.fsti.checked Vale.X64.InsLemmas.fsti.checked Vale.X64.Decls.fst.checked Vale.Lib.Seqs.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Seq.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.X64.InsMem.fst
Vale.X64.Decls.va_operand_heaplet Vale.X64.Decls.va_operand_reg_opr64 Prims.int Vale.Arch.HeapTypes_s.taint Vale.X64.Taint_Semantics.mk_ins Vale.X64.InsLemmas.make_instr_annotate Prims.Cons Vale.X64.Instruction_s.instr_out Vale.X64.Instruction_s.out Vale.X64.Instruction_s.op64 Prims.Nil Vale.X64.Instruction_s.instr_operand Vale.X64.Instruction_s.PreserveFlags Vale.X64.Instructions_s.ins_MovBe64 Vale.X64.Machine_Semantics_s.AnnotateMovbe64 Vale.X64.Instruction_s.InstrTypeRecord Vale.X64.Machine_s.OMem Vale.X64.Machine_s.nat64 Vale.X64.Machine_s.reg_64 FStar.Pervasives.Native.Mktuple2 Vale.X64.Machine_s.maddr Vale.X64.Machine_s.MReg Vale.X64.Decls.get_reg Vale.X64.Decls.va_code
module Vale.X64.InsMem
open Vale.X64
open Vale.X64.StateLemmas
open Vale.X64.InsLemmas
open Vale.Arch.Heap
open Vale.Arch.HeapImpl
module I = Vale.X64.Instructions_s
module S = Vale.X64.Machine_Semantics_s
module P = Vale.X64.Print_s
open Vale.X64.Taint_Semantics

friend Vale.X64.Decls
#reset-options "--initial_fuel 2 --max_fuel 2 --max_ifuel 2 --z3rlimit 20"
//-- Mem64_in
//--
//-- Mem64_lemma

[@ "opaque_to_smt"]
let va_code_Mem64_lemma () =
  (va_Block (va_CNil ()))

[@ "opaque_to_smt"]
let va_codegen_success_Mem64_lemma () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Mem64_lemma va_b0 va_s0 h base offset b index t =
  va_reveal_opaque (`%va_code_Mem64_lemma) (va_code_Mem64_lemma ());
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let heap_h = va_get_mem_heaplet h va_s0 in
  lemma_opr_Mem64 h va_s0 base offset b index t;
  let (va_sM, va_fM) = va_lemma_empty_total va_s0 va_b1 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Mem64_lemma h base offset b index t va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Mem64_lemma (va_code_Mem64_lemma ()) va_s0 h base offset b index t
    in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM va_s0));
  va_lemma_norm_mods ([]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
let create_heaplets_this (buffers:list buffer_info) (s:vale_state) : GTot vale_state =
  {s with vs_heap = Vale.X64.Memory_Sems.create_heaplets buffers s.vs_heap}

let destroy_heaplets_this (s:vale_state) : Ghost vale_state
  (requires state_inv s)
  (ensures fun _ -> True)
  =
  {s with vs_heap = Vale.X64.Memory_Sems.destroy_heaplets s.vs_heap}
//-- Vale.X64.StateLemmas.use_machine_state_equal
//--
//-- CreateHeaplets

[@ "opaque_to_smt"]
let va_code_CreateHeaplets () =
  (mk_ins (make_instr_annotate (I.ins_Ghost) (S.AnnotateGhost ())))

[@ "opaque_to_smt"]
let va_codegen_success_CreateHeaplets () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_CreateHeaplets va_b0 va_s0 buffers =
  va_reveal_opaque (`%va_code_CreateHeaplets) (va_code_CreateHeaplets ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr_annotate (I.ins_Ghost) (S.AnnotateGhost ()))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr_annotate (I.ins_Ghost) (S.AnnotateGhost
    ()))) va_s0 in
  let (bs:(FStar.Seq.Base.seq buffer_info)) = Vale.Lib.Seqs.list_to_seq #buffer_info buffers in
  Vale.Lib.Seqs.lemma_list_to_seq #buffer_info buffers;
  let va_sM = create_heaplets_this buffers va_sM in
  Vale.X64.Memory_Sems.lemma_create_heaplets buffers (va_old_s.vs_heap);
  Vale.X64.StateLemmas.use_machine_state_equal ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_CreateHeaplets buffers va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_CreateHeaplets (va_code_CreateHeaplets ()) va_s0 buffers in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_mem_layout va_sM (va_update_ok va_sM va_s0)));
  va_lemma_norm_mods ([va_Mod_mem_layout]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- DestroyHeaplets

[@ "opaque_to_smt"]
let va_code_DestroyHeaplets () =
  (mk_ins (make_instr_annotate (I.ins_Ghost) (S.AnnotateGhost ())))

[@ "opaque_to_smt"]
let va_codegen_success_DestroyHeaplets () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_DestroyHeaplets va_b0 va_s0 =
  va_reveal_opaque (`%va_code_DestroyHeaplets) (va_code_DestroyHeaplets ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr_annotate (I.ins_Ghost) (S.AnnotateGhost ()))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr_annotate (I.ins_Ghost) (S.AnnotateGhost
    ()))) va_s0 in
  let va_sM = destroy_heaplets_this va_sM in
  Vale.X64.Memory_Sems.lemma_destroy_heaplets (va_old_s.vs_heap);
  Vale.X64.StateLemmas.use_machine_state_equal ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_DestroyHeaplets va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_DestroyHeaplets (va_code_DestroyHeaplets ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_mem_layout va_sM (va_update_ok va_sM va_s0)));
  va_lemma_norm_mods ([va_Mod_mem_layout]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Load64_buffer

[@ "opaque_to_smt"]
let va_code_Load64_buffer h dst src offset t =
  (mk_ins (make_instr_annotate (I.ins_Mov64) (S.AnnotateMov64 ()) dst (OMem ((MReg (get_reg src)
    offset, t)))))

[@ "opaque_to_smt"]
let va_codegen_success_Load64_buffer h dst src offset t =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Load64_buffer va_b0 va_s0 h dst src offset t b index =
  va_reveal_opaque (`%va_code_Load64_buffer) (va_code_Load64_buffer h dst src offset t);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr_annotate (I.ins_Mov64) (S.AnnotateMov64 ()) dst (OMem ((MReg
    (get_reg src) offset, t))))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr_annotate (I.ins_Mov64) (S.AnnotateMov64 ())
    dst (OMem ((MReg (get_reg src) offset, t))))) va_s0 in
  Vale.X64.Memory_Sems.low_lemma_load_mem64_full b index (va_sM.vs_heap) t h;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Load64_buffer h dst src offset t b index va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Load64_buffer (va_code_Load64_buffer h dst src offset t) va_s0 h
    dst src offset t b index in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_dst_opr64 dst va_sM va_s0)));
  va_lemma_norm_mods ([va_mod_dst_opr64 dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Store64_buffer

[@ "opaque_to_smt"]
let va_code_Store64_buffer h dst src offset t =
  (mk_ins (make_instr_annotate (Vale.X64.Instructions_s.ins_Mov64) (S.AnnotateMov64 ()) (OMem
    ((MReg (get_reg dst) offset, t))) src))

[@ "opaque_to_smt"]
let va_codegen_success_Store64_buffer h dst src offset t =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Store64_buffer va_b0 va_s0 h dst src offset t b index =
  va_reveal_opaque (`%va_code_Store64_buffer) (va_code_Store64_buffer h dst src offset t);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr_annotate (Vale.X64.Instructions_s.ins_Mov64) (S.AnnotateMov64
    ()) (OMem ((MReg (get_reg dst) offset, t))) src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr_annotate (Vale.X64.Instructions_s.ins_Mov64)
    (S.AnnotateMov64 ()) (OMem ((MReg (get_reg dst) offset, t))) src)) va_s0 in
  Vale.X64.Memory_Sems.low_lemma_store_mem64_full b index (va_eval_reg_opr64 va_old_s src)
    (va_old_s.vs_heap) t h;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Store64_buffer h dst src offset t b index va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Store64_buffer (va_code_Store64_buffer h dst src offset t) va_s0 h
    dst src offset t b index in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_mem va_sM (va_update_ok va_sM (va_update_operand_heaplet h
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_mem; va_mod_heaplet h]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- LoadBe64_buffer

[@ "opaque_to_smt"]
let va_code_LoadBe64_buffer h dst src offset t =
  (mk_ins (make_instr_annotate (I.ins_MovBe64) (S.AnnotateMovbe64 ()) dst (OMem ((MReg (get_reg
    src) offset, t)))))

[@ "opaque_to_smt"]
let va_codegen_success_LoadBe64_buffer h dst src offset t =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_LoadBe64_buffer va_b0 va_s0 h dst src offset t b index =
  va_reveal_opaque (`%va_code_LoadBe64_buffer) (va_code_LoadBe64_buffer h dst src offset t);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr_annotate (I.ins_MovBe64) (S.AnnotateMovbe64 ()) dst (OMem ((MReg
    (get_reg src) offset, t))))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr_annotate (I.ins_MovBe64) (S.AnnotateMovbe64
    ()) dst (OMem ((MReg (get_reg src) offset, t))))) va_s0 in
  Vale.X64.Memory_Sems.low_lemma_load_mem64_full b index (va_sM.vs_heap) t h;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_LoadBe64_buffer h dst src offset t b index va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_LoadBe64_buffer (va_code_LoadBe64_buffer h dst src offset t) va_s0
    h dst src offset t b index in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_dst_opr64 dst va_sM va_s0)));
  va_lemma_norm_mods ([va_mod_dst_opr64 dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- StoreBe64_buffer

[@ "opaque_to_smt"]
val va_code_StoreBe64_buffer : h:va_operand_heaplet -> dst:va_operand_reg_opr64 ->
  src:va_operand_reg_opr64 -> offset:int -> t:taint -> Tot va_code

    h: Vale.X64.Decls.va_operand_heaplet ->
    dst: Vale.X64.Decls.va_operand_reg_opr64 ->
    src: Vale.X64.Decls.va_operand_reg_opr64 ->
    offset: Prims.int ->
    t: Vale.Arch.HeapTypes_s.taint
  -> Vale.X64.Decls.va_code