val lemma_opr_Mem128
      (id: heaplet_id)
      (s: va_state)
      (base: operand64)
      (offset: int)
      (t: taint)
      (b: M.buffer128)
      (index: int)
    : Lemma
      (requires
        (let h = Map16.sel s.vs_heap.vf_heaplets id in
          M.mem_inv s.vs_heap /\ OReg? base /\ valid_src_addr h b index /\
          M.valid_layout_buffer b (s.vs_heap.vf_layout) h false /\
          M.valid_taint_buf128 b h (full_heap_taint s.vs_heap) t /\
          eval_operand base s + offset == M.buffer_addr b h + 16 * index))
      (ensures
        (let h = Map16.sel s.vs_heap.vf_heaplets id in
          valid_operand128 (va_opr_code_Mem128 id base offset t) s /\
          M.load_mem128 (M.buffer_addr b h + 16 * index) (M.get_vale_heap s.vs_heap) ==
          M.buffer_read b index h))
let lemma_opr_Mem128 (id:heaplet_id) (s:va_state) (base:operand64) (offset:int) (t:taint) (b:M.buffer128) (index:int) : Lemma
  (requires (
    let h = Map16.sel s.vs_heap.vf_heaplets id in
    M.mem_inv s.vs_heap /\
    OReg? base /\
    valid_src_addr h b index /\
    M.valid_layout_buffer b (s.vs_heap.vf_layout) h false /\
    M.valid_taint_buf128 b h (full_heap_taint s.vs_heap) t /\
    eval_operand base s + offset == M.buffer_addr b h + 16 * index
  ))
  (ensures (
    let h = Map16.sel s.vs_heap.vf_heaplets id in
    valid_operand128 (va_opr_code_Mem128 id base offset t) s /\
    M.load_mem128 (M.buffer_addr b h + 16 * index) (M.get_vale_heap s.vs_heap) == M.buffer_read b index h
  ))
  =
  Vale.X64.Memory_Sems.low_lemma_load_mem128_full b index s.vs_heap t id;
  let h = M.get_vale_heap s.vs_heap in
  let t = va_opr_code_Mem128 id base offset t in
  M.lemma_valid_mem128 b index h;
  let OMem (m, t) = t in
  assert (valid_buf_maddr128 (eval_maddr m s) h s.vs_heap.vf_layout b index t);
  M.lemma_load_mem128 b index h
val lemma_opr_Mem128
      (id: heaplet_id)
      (s: va_state)
      (base: operand64)
      (offset: int)
      (t: taint)
      (b: M.buffer128)
      (index: int)
    : Lemma
      (requires
        (let h = Map16.sel s.vs_heap.vf_heaplets id in
          M.mem_inv s.vs_heap /\ OReg? base /\ valid_src_addr h b index /\
          M.valid_layout_buffer b (s.vs_heap.vf_layout) h false /\
          M.valid_taint_buf128 b h (full_heap_taint s.vs_heap) t /\
          eval_operand base s + offset == M.buffer_addr b h + 16 * index))
      (ensures
        (let h = Map16.sel s.vs_heap.vf_heaplets id in
          valid_operand128 (va_opr_code_Mem128 id base offset t) s /\
          M.load_mem128 (M.buffer_addr b h + 16 * index) (M.get_vale_heap s.vs_heap) ==
          M.buffer_read b index h))
let lemma_opr_Mem128
      (id: heaplet_id)
      (s: va_state)
      (base: operand64)
      (offset: int)
      (t: taint)
      (b: M.buffer128)
      (index: int)
    : Lemma
      (requires
        (let h = Map16.sel s.vs_heap.vf_heaplets id in
          M.mem_inv s.vs_heap /\ OReg? base /\ valid_src_addr h b index /\
          M.valid_layout_buffer b (s.vs_heap.vf_layout) h false /\
          M.valid_taint_buf128 b h (full_heap_taint s.vs_heap) t /\
          eval_operand base s + offset == M.buffer_addr b h + 16 * index))
      (ensures
        (let h = Map16.sel s.vs_heap.vf_heaplets id in
          valid_operand128 (va_opr_code_Mem128 id base offset t) s /\
          M.load_mem128 (M.buffer_addr b h + 16 * index) (M.get_vale_heap s.vs_heap) ==
          M.buffer_read b index h)) =
Vale.X64.Memory_Sems.low_lemma_load_mem128_full b index s.vs_heap t id;
let h = M.get_vale_heap s.vs_heap in
let t = va_opr_code_Mem128 id base offset t in
M.lemma_valid_mem128 b index h;
let OMem (m, t) = t in
assert (valid_buf_maddr128 (eval_maddr m s) h s.vs_heap.vf_layout b index t);
M.lemma_load_mem128 b index h
Vale.X64.Decls.fst.checked
Vale.X64.StateLemmas.fsti.checked Vale.X64.State.fsti.checked Vale.X64.Print_s.fst.checked Vale.X64.Memory_Sems.fsti.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Lemmas.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Def.PossiblyMonad.fst.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Map.fsti.checked FStar.IO.fst.checked
Vale.X64.Decls.fst
Vale.X64.Decls.heaplet_id Vale.X64.Decls.va_state Vale.X64.Machine_s.operand64 Prims.int Vale.Arch.HeapTypes_s.taint Vale.X64.Memory.buffer128 Vale.X64.Machine_s.maddr Vale.X64.Memory.lemma_load_mem128 Prims.unit Prims._assert Vale.X64.Decls.valid_buf_maddr128 Vale.X64.State.eval_maddr Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout Vale.X64.State.__proj__Mkvale_state__item__vs_heap Vale.X64.Machine_s.operand128 Vale.X64.Memory.lemma_valid_mem128 Vale.X64.Decls.va_opr_code_Mem128 Vale.Arch.HeapImpl.vale_heap Vale.X64.Memory.get_vale_heap Vale.X64.Memory_Sems.low_lemma_load_mem128_full Prims.l_and Vale.X64.Memory.mem_inv Prims.b2t Vale.X64.Machine_s.uu___is_OReg Vale.X64.Machine_s.nat64 Vale.X64.Machine_s.reg_64 Vale.X64.Decls.valid_src_addr Vale.X64.Memory.vuint128 Vale.X64.Memory.valid_layout_buffer Vale.X64.Memory.valid_taint_buf128 Vale.Arch.HeapImpl.full_heap_taint Prims.eq2 Prims.op_Addition Vale.X64.State.eval_operand Vale.X64.Memory.buffer_addr FStar.Mul.op_Star Vale.Lib.Map16.sel Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets Prims.squash Vale.X64.Decls.valid_operand128 Vale.Def.Words_s.four Vale.Def.Types_s.nat32 Vale.X64.Memory.load_mem128 Vale.X64.Memory.buffer_read Prims.Nil FStar.Pervasives.pattern
module Vale.X64.Decls
open FStar.Mul
open Vale.X64.Machine_s
open Vale.X64
open Vale.X64.State
open Vale.X64.StateLemmas
open FStar.UInt
module P = Vale.X64.Print_s
module BC = Vale.X64.Bytes_Code_s
module BS = Vale.X64.Machine_Semantics_s
#reset-options "--max_fuel 0 --max_ifuel 0 --smtencoding.elim_box true --smtencoding.l_arith_repr boxwrap --smtencoding.nl_arith_repr boxwrap --z3cliopt smt.arith.nl=true --using_facts_from 'Prims FStar.UInt Vale.Def.Words_s FStar.UInt64'"
let lemma_mul_in_bounds (x y:nat64) : Lemma (requires x * y < pow2_64) (ensures FStar.UInt.mul_mod #64 x y == x * y) = ()

#reset-options "--z3cliopt smt.arith.nl=true --using_facts_from Prims --using_facts_from FStar.Math"
let lemma_mul_nat (x:nat) (y:nat) : Lemma (ensures 0 <= (x * y)) = ()
#reset-options "--initial_fuel 2 --max_fuel 2"

let cf flags = match Lemmas.cf flags with | Some v -> v | None -> false
let overflow flags = match Lemmas.overflow flags with | Some v -> v | None -> false
let valid_cf flags = match Lemmas.cf flags with | Some v -> true | None -> false
let valid_of flags = match Lemmas.overflow flags with | Some v -> true | None -> false
let updated_cf new_flags new_cf = Lemmas.cf new_flags = Some new_cf
let updated_of new_flags new_cf = Lemmas.overflow new_flags = Some new_cf
let maintained_cf new_flags flags = Lemmas.cf new_flags = Lemmas.cf flags
let maintained_of new_flags flags = Lemmas.overflow new_flags = Lemmas.overflow flags
let ins = BS.ins
type ocmp = BS.ocmp
type va_fuel = nat

type va_pbool = Vale.Def.PossiblyMonad.pbool
let va_ttrue () = Vale.Def.PossiblyMonad.ttrue
let va_ffalse = Vale.Def.PossiblyMonad.ffalse
let va_pbool_and x y = Vale.Def.PossiblyMonad.((&&.)) x y
let get_reason p =
  match p with
  | Vale.Def.PossiblyMonad.Ok () -> None
  | Vale.Def.PossiblyMonad.Err reason -> Some reason

let mul_nat_helper x y =
  FStar.Math.Lemmas.nat_times_nat_is_nat x y

let va_fuel_default () = 0

let lemma_opr_Mem64 (id:heaplet_id) (s:va_state) (base:operand64) (offset:int) (b:M.buffer64) (index:int) (t:taint) : Lemma
  (requires (
    let h = Map16.sel s.vs_heap.vf_heaplets id in
    M.mem_inv s.vs_heap /\
    OReg? base /\
    valid_src_addr h b index /\
    M.valid_layout_buffer b (s.vs_heap.vf_layout) h false /\
    M.valid_taint_buf64 b h (full_heap_taint s.vs_heap) t /\
    eval_operand base s + offset == M.buffer_addr b h + 8 * index
  ))
  (ensures (
    let h = Map16.sel s.vs_heap.vf_heaplets id in
    valid_operand (va_opr_code_Mem64 id base offset t) s /\
    M.load_mem64 (M.buffer_addr b h + 8 * index) (s.vs_heap.vf_heap) == M.buffer_read b index h
  ))
  =
  Vale.X64.Memory_Sems.low_lemma_load_mem64_full b index s.vs_heap t id;
  let h = M.get_vale_heap s.vs_heap in
  let t = va_opr_code_Mem64 id base offset t in
  M.lemma_valid_mem64 b index h;
  let OMem (m, t) = t in
  assert (valid_buf_maddr64 (eval_maddr m s) h s.vs_heap.vf_layout b index t);
  M.lemma_load_mem64 b index h

let lemma_opr_Mem128 (id:heaplet_id) (s:va_state) (base:operand64) (offset:int) (t:taint) (b:M.buffer128) (index:int) : Lemma
  (requires (
    let h = Map16.sel s.vs_heap.vf_heaplets id in
    M.mem_inv s.vs_heap /\
    OReg? base /\
    valid_src_addr h b index /\
    M.valid_layout_buffer b (s.vs_heap.vf_layout) h false /\
    M.valid_taint_buf128 b h (full_heap_taint s.vs_heap) t /\
    eval_operand base s + offset == M.buffer_addr b h + 16 * index
  ))
  (ensures (
    let h = Map16.sel s.vs_heap.vf_heaplets id in
    valid_operand128 (va_opr_code_Mem128 id base offset t) s /\
    M.load_mem128 (M.buffer_addr b h + 16 * index) (M.get_vale_heap s.vs_heap) == M.buffer_read b index h
  ))
val lemma_opr_Mem128
      (id: heaplet_id)
      (s: va_state)
      (base: operand64)
      (offset: int)
      (t: taint)
      (b: M.buffer128)
      (index: int)
    : Lemma
      (requires
        (let h = Map16.sel s.vs_heap.vf_heaplets id in
          M.mem_inv s.vs_heap /\ OReg? base /\ valid_src_addr h b index /\
          M.valid_layout_buffer b (s.vs_heap.vf_layout) h false /\
          M.valid_taint_buf128 b h (full_heap_taint s.vs_heap) t /\
          eval_operand base s + offset == M.buffer_addr b h + 16 * index))
      (ensures
        (let h = Map16.sel s.vs_heap.vf_heaplets id in
          valid_operand128 (va_opr_code_Mem128 id base offset t) s /\
          M.load_mem128 (M.buffer_addr b h + 16 * index) (M.get_vale_heap s.vs_heap) ==
          M.buffer_read b index h))

    id: Vale.X64.Decls.heaplet_id ->
    s: Vale.X64.Decls.va_state ->
    base: Vale.X64.Machine_s.operand64 ->
    offset: Prims.int ->
    t: Vale.Arch.HeapTypes_s.taint ->
    b: Vale.X64.Memory.buffer128 ->
    index: Prims.int
  -> FStar.Pervasives.Lemma
      (requires
        (let h = Vale.Lib.Map16.sel (Mkvale_full_heap?.vf_heaplets (Mkvale_state?.vs_heap s)) id in
          Vale.X64.Memory.mem_inv (Mkvale_state?.vs_heap s) /\ OReg? base /\
          Vale.X64.Decls.valid_src_addr h b index /\
          Vale.X64.Memory.valid_layout_buffer b
            (Mkvale_full_heap?.vf_layout (Mkvale_state?.vs_heap s))
            h
            false /\
          Vale.X64.Memory.valid_taint_buf128 b
            h
            (Vale.Arch.HeapImpl.full_heap_taint (Mkvale_state?.vs_heap s))
            t /\
          Vale.X64.State.eval_operand base s + offset ==
          Vale.X64.Memory.buffer_addr b h + 16 * index))
      (ensures
        (let h = Vale.Lib.Map16.sel (Mkvale_full_heap?.vf_heaplets (Mkvale_state?.vs_heap s)) id in
          Vale.X64.Decls.valid_operand128 (Vale.X64.Decls.va_opr_code_Mem128 id base offset t) s /\
          Vale.X64.Memory.load_mem128 (Vale.X64.Memory.buffer_addr b h + 16 * index)
            (Vale.X64.Memory.get_vale_heap (Mkvale_state?.vs_heap s)) ==
          Vale.X64.Memory.buffer_read b index h))