val va_lemma_Mem64_lemma : va_b0:va_code -> va_s0:va_state -> h:heaplet_id -> base:operand64 ->
  offset:int -> b:buffer64 -> index:int -> t:taint
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Mem64_lemma ()) va_s0 /\ va_get_ok va_s0 /\ (let
    heap_h = va_get_mem_heaplet h va_s0 in (OReg? base) /\ valid_src_addr heap_h b index /\
    valid_layout_buffer b (va_get_mem_layout va_s0) heap_h false /\ valid_taint_buf64 b heap_h
    ((va_get_mem_layout va_s0).vl_taint) t /\ eval_operand base va_s0 + offset == buffer_addr b
    heap_h + 8 `op_Multiply` index)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let heap_h = va_get_mem_heaplet h va_s0 in valid_operand (va_opr_code_Mem64 h base offset t)
    va_sM /\ load_mem64 (buffer_addr b heap_h + 8 `op_Multiply` index) (va_get_mem va_sM) ==
    buffer_read b index heap_h) /\ va_state_eq va_sM (va_update_ok va_sM va_s0)))
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)
val va_lemma_Mem64_lemma : va_b0:va_code -> va_s0:va_state -> h:heaplet_id -> base:operand64 ->
  offset:int -> b:buffer64 -> index:int -> t:taint
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Mem64_lemma ()) va_s0 /\ va_get_ok va_s0 /\ (let
    heap_h = va_get_mem_heaplet h va_s0 in (OReg? base) /\ valid_src_addr heap_h b index /\
    valid_layout_buffer b (va_get_mem_layout va_s0) heap_h false /\ valid_taint_buf64 b heap_h
    ((va_get_mem_layout va_s0).vl_taint) t /\ eval_operand base va_s0 + offset == buffer_addr b
    heap_h + 8 `op_Multiply` index)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let heap_h = va_get_mem_heaplet h va_s0 in valid_operand (va_opr_code_Mem64 h base offset t)
    va_sM /\ load_mem64 (buffer_addr b heap_h + 8 `op_Multiply` index) (va_get_mem va_sM) ==
    buffer_read b index heap_h) /\ va_state_eq va_sM (va_update_ok va_sM va_s0)))
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)
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_code Vale.X64.Decls.va_state Vale.Arch.HeapImpl.heaplet_id Vale.X64.Machine_s.operand64 Prims.int Vale.X64.Memory.buffer64 Vale.Arch.HeapTypes_s.taint Vale.X64.Decls.va_fuel FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.tuple2 Vale.X64.State.vale_state Vale.X64.Decls.va_lemma_empty_total Prims.unit Vale.X64.Decls.lemma_opr_Mem64 Vale.Arch.HeapImpl.vale_heap Vale.X64.Decls.va_get_mem_heaplet Prims.list Vale.X64.Machine_s.precode Vale.X64.Decls.ins Vale.X64.Decls.ocmp Vale.X64.Decls.va_get_block Vale.X64.Decls.va_reveal_opaque Vale.X64.InsMem.va_code_Mem64_lemma
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"]
val va_lemma_Mem64_lemma : va_b0:va_code -> va_s0:va_state -> h:heaplet_id -> base:operand64 ->
  offset:int -> b:buffer64 -> index:int -> t:taint
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Mem64_lemma ()) va_s0 /\ va_get_ok va_s0 /\ (let
    heap_h = va_get_mem_heaplet h va_s0 in (OReg? base) /\ valid_src_addr heap_h b index /\
    valid_layout_buffer b (va_get_mem_layout va_s0) heap_h false /\ valid_taint_buf64 b heap_h
    ((va_get_mem_layout va_s0).vl_taint) t /\ eval_operand base va_s0 + offset == buffer_addr b
    heap_h + 8 `op_Multiply` index)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let heap_h = va_get_mem_heaplet h va_s0 in valid_operand (va_opr_code_Mem64 h base offset t)
    va_sM /\ load_mem64 (buffer_addr b heap_h + 8 `op_Multiply` index) (va_get_mem va_sM) ==
    buffer_read b index heap_h) /\ va_state_eq va_sM (va_update_ok va_sM va_s0)))

    va_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    h: Vale.Arch.HeapImpl.heaplet_id ->
    base: Vale.X64.Machine_s.operand64 ->
    offset: Prims.int ->
    b: Vale.X64.Memory.buffer64 ->
    index: Prims.int ->
    t: Vale.Arch.HeapTypes_s.taint
  -> Prims.Ghost (Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel)