val lemma_valid_src_operand128_and_taint (o:operand128) (s:vale_state) : Lemma
  (requires valid_operand128 o s)
  (ensures S.valid_src_operand128_and_taint o (state_to_S s))
  [SMTPat (S.valid_src_operand128_and_taint o (state_to_S s))]
let lemma_valid_src_operand128_and_taint o s =
  let h = get_vale_heap s.vs_heap in
  match o with
  | OMem (m, t) ->
    let addr = eval_maddr m s in
    let aux (b:buffer128) (i:int) : Lemma
      (requires valid_buf_maddr128 addr h s.vs_heap.vf_layout b i t)
      (ensures S.valid_src_operand128_and_taint o (state_to_S s))
      =
      lemma_heap_get_heap s.vs_heap;
      lemma_valid_taint128 b (full_heap_taint s.vs_heap) h i t
      in
    Classical.forall_intro_2 (fun b i -> (fun b -> Classical.move_requires (aux b)) b i)
  | OStack (m, t) -> lemma_valid_taint_stack128 (eval_maddr m s) t s.vs_stackTaint
  | _ -> ()
val lemma_valid_src_operand128_and_taint (o:operand128) (s:vale_state) : Lemma
  (requires valid_operand128 o s)
  (ensures S.valid_src_operand128_and_taint o (state_to_S s))
  [SMTPat (S.valid_src_operand128_and_taint o (state_to_S s))]
let lemma_valid_src_operand128_and_taint o s =
let h = get_vale_heap s.vs_heap in
match o with
| OMem (m, t) ->
  let addr = eval_maddr m s in
  let aux (b: buffer128) (i: int)
      : Lemma (requires valid_buf_maddr128 addr h s.vs_heap.vf_layout b i t)
        (ensures S.valid_src_operand128_and_taint o (state_to_S s)) =
    lemma_heap_get_heap s.vs_heap;
    lemma_valid_taint128 b (full_heap_taint s.vs_heap) h i t
  in
  Classical.forall_intro_2 (fun b i -> (fun b -> Classical.move_requires (aux b)) b i)
| OStack (m, t) -> lemma_valid_taint_stack128 (eval_maddr m s) t s.vs_stackTaint
| _ -> ()
Vale.X64.InsLemmas.fst.checked
Vale.X64.Taint_Semantics.fst.checked Vale.X64.StateLemmas.fsti.checked Vale.X64.Stack_i.fsti.checked Vale.X64.Memory_Sems.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Decls.fst.checked Vale.Arch.HeapTypes_s.fst.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked
Vale.X64.InsLemmas.fst
Vale.X64.Machine_s.operand128 Vale.X64.State.vale_state Vale.X64.Machine_s.maddr Vale.Arch.HeapTypes_s.taint FStar.Classical.forall_intro_2 Vale.X64.Memory.buffer128 Prims.int Prims.l_imp Vale.X64.Decls.valid_buf_maddr128 Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout Vale.X64.State.__proj__Mkvale_state__item__vs_heap Prims.b2t Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint Vale.X64.StateLemmas.state_to_S FStar.Classical.move_requires Prims.unit Prims.squash Prims.Nil FStar.Pervasives.pattern Vale.X64.Memory.lemma_valid_taint128 Vale.Arch.HeapImpl.full_heap_taint Vale.X64.Memory_Sems.lemma_heap_get_heap Vale.X64.State.eval_maddr Vale.X64.Stack_i.lemma_valid_taint_stack128 Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint Vale.X64.Machine_s.operand Vale.X64.Machine_s.quad32 Vale.X64.Machine_s.reg_xmm Vale.Arch.HeapImpl.vale_heap Vale.X64.Memory.get_vale_heap
module Vale.X64.InsLemmas

open FStar.Mul
open Vale.Arch.HeapTypes_s
open Vale.Arch.HeapImpl
open Vale.X64.StateLemmas
open Vale.X64.Taint_Semantics
open Vale.X64.Memory
open Vale.X64.Stack_i
open Vale.X64.Memory_Sems

friend Vale.X64.Decls

let lemma_valid_src_operand64_and_taint o s =
  let h = get_vale_heap s.vs_heap in
  match o with
  | OMem (m, t) ->
    let addr = eval_maddr m s in
    let aux (b:buffer64) (i:int) : Lemma
      (requires valid_buf_maddr64 addr h s.vs_heap.vf_layout b i t)
      (ensures S.valid_src_operand64_and_taint o (state_to_S s))
      =
      lemma_heap_get_heap s.vs_heap;
      lemma_valid_taint64 b (full_heap_taint s.vs_heap) h i t
      in
    Classical.forall_intro_2 (fun b i -> (fun b -> Classical.move_requires (aux b)) b i)
  | OStack (m, t) -> lemma_valid_taint_stack64 (eval_maddr m s) t s.vs_stackTaint
  | _ -> ()
val lemma_valid_src_operand128_and_taint (o:operand128) (s:vale_state) : Lemma
  (requires valid_operand128 o s)
  (ensures S.valid_src_operand128_and_taint o (state_to_S s))
  [SMTPat (S.valid_src_operand128_and_taint o (state_to_S s))]
o: Vale.X64.Machine_s.operand128 -> s: Vale.X64.State.vale_state
  -> FStar.Pervasives.Lemma (requires Vale.X64.Decls.valid_operand128 o s)
      (ensures
        Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint o
          (Vale.X64.StateLemmas.state_to_S s))
      [
        SMTPat (Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint o
              (Vale.X64.StateLemmas.state_to_S s))
      ]