val update_location :
  a:location ->
  v:location_val_t a ->
  machine_state ->
  s:machine_state{eval_location a s == v}
let update_location a v s =
  match a with
  | ALocMem ->
    let v = coerce v in
    { s with ms_heap = v }
  | ALocStack ->
    let v = FStar.Universe.downgrade_val (coerce v) in
    { s with ms_stack = fst v ; ms_stackTaint = snd v }
  | ALocReg r ->
    let v = FStar.Universe.downgrade_val v in
    update_reg' r v s
  | ALocCf ->
    let v = FStar.Universe.downgrade_val v in
    { s with ms_flags = FStar.FunctionalExtensionality.on_dom flag (fun f -> if f = fCarry then v else s.ms_flags f) }
  | ALocOf ->
    let v = FStar.Universe.downgrade_val v in
    { s with ms_flags = FStar.FunctionalExtensionality.on_dom flag (fun f -> if f = fOverflow then v else s.ms_flags f) }
val update_location :
  a:location ->
  v:location_val_t a ->
  machine_state ->
  s:machine_state{eval_location a s == v}
let update_location a v s =
match a with
| ALocMem ->
  let v = coerce v in
  { s with ms_heap = v }
| ALocStack ->
  let v = FStar.Universe.downgrade_val (coerce v) in
  { s with ms_stack = fst v; ms_stackTaint = snd v }
| ALocReg r ->
  let v = FStar.Universe.downgrade_val v in
  update_reg' r v s
| ALocCf ->
  let v = FStar.Universe.downgrade_val v in
  {
    s with
    ms_flags
    =
    FStar.FunctionalExtensionality.on_dom flag (fun f -> if f = fCarry then v else s.ms_flags f)
  }
| ALocOf ->
  let v = FStar.Universe.downgrade_val v in
  {
    s with
    ms_flags
    =
    FStar.FunctionalExtensionality.on_dom flag (fun f -> if f = fOverflow then v else s.ms_flags f)
  }
Vale.Transformers.Locations.fst.checked
Vale.X64.Print_s.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Instructions_s.fsti.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Def.PossiblyMonad.fst.checked Vale.Arch.HeapTypes_s.fst.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Universe.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked
Vale.Transformers.Locations.fst
Vale.Transformers.Locations.location Vale.Transformers.Locations.location_val_t Vale.X64.Machine_Semantics_s.machine_state Vale.X64.Machine_Semantics_s.Mkmachine_state Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stack Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_trace Vale.Arch.Heap.heap_impl Vale.X64.Instruction_s.coerce Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap FStar.Pervasives.Native.fst Vale.X64.Machine_Semantics_s.machine_stack Vale.Arch.HeapTypes_s.memTaint_t FStar.Pervasives.Native.snd FStar.Pervasives.Native.tuple2 FStar.Universe.downgrade_val FStar.Universe.raise_t Vale.X64.Machine_s.reg Vale.X64.Machine_Semantics_s.update_reg' Vale.X64.Machine_s.t_reg FStar.FunctionalExtensionality.on_dom Vale.X64.Machine_s.flag Vale.X64.Machine_Semantics_s.flag_val_t Prims.op_Equality Vale.X64.Machine_s.fCarry Prims.bool FStar.Pervasives.Native.option Vale.X64.Machine_s.fOverflow Prims.eq2 Vale.Transformers.Locations.eval_location
module Vale.Transformers.Locations

open Vale.Arch.HeapTypes_s
open Vale.Arch.Heap
open Vale.X64.Bytes_Code_s
open Vale.X64.Instruction_s
open Vale.X64.Instructions_s
open Vale.X64.Machine_Semantics_s
open Vale.X64.Machine_s
open Vale.X64.Print_s

open Vale.Def.PossiblyMonad

module L = FStar.List.Tot

(* See fsti *)
type location : eqtype =
  | ALocMem : location
  | ALocStack: location
  | ALocReg : reg -> location
  | ALocCf : location
  | ALocOf : location

let aux_print_reg_from_location (a:location{ALocReg? a}) : string =
  let ALocReg (Reg file id) = a in
  match file with
  | 0 -> print_reg_name id
  | 1 -> print_xmm id gcc

(* See fsti *)
let disjoint_location a1 a2 =
  match a1, a2 with
  | ALocCf, ALocCf -> ffalse "carry flag not disjoint from itself"
  | ALocOf, ALocOf -> ffalse "overflow flag not disjoint from itself"
  | ALocCf, _ | ALocOf, _ | _, ALocCf | _, ALocOf -> ttrue
  | ALocMem, ALocMem -> ffalse "memory not disjoint from itself"
  | ALocStack, ALocStack -> ffalse "stack not disjoint from itself"
  | ALocMem, ALocStack | ALocStack, ALocMem -> ttrue
  | ALocReg r1, ALocReg r2 ->
    (r1 <> r2) /- ("register " ^ aux_print_reg_from_location a1 ^ " not disjoint from itself")
  | ALocReg _, _ | _, ALocReg _ -> ttrue

(* See fsti *)
let auto_lemma_disjoint_location a1 a2 = ()

(* See fsti *)
let downgrade_val_raise_val_u0_u1 #a x = FStar.Universe.downgrade_val_raise_val #a x

(* See fsti *)
let location_val_t a =
  match a with
  | ALocMem -> heap_impl
  | ALocStack -> FStar.Universe.raise_t (machine_stack & memTaint_t)
  | ALocReg r -> FStar.Universe.raise_t (t_reg r)
  | ALocCf -> FStar.Universe.raise_t flag_val_t
  | ALocOf -> FStar.Universe.raise_t flag_val_t

(* See fsti *)
let location_val_eqt a =
  match a with
  | ALocMem -> unit
  | ALocStack -> unit
  | ALocReg r -> t_reg r
  | ALocCf -> flag_val_t
  | ALocOf -> flag_val_t

(* See fsti *)
let eval_location a s =
  match a with
  | ALocMem -> s.ms_heap
  | ALocStack -> FStar.Universe.raise_val (s.ms_stack, s.ms_stackTaint)
  | ALocReg r -> FStar.Universe.raise_val (eval_reg r s)
  | ALocCf -> FStar.Universe.raise_val (cf s.ms_flags)
  | ALocOf -> FStar.Universe.raise_val (overflow s.ms_flags)

(* See fsti *)
val update_location :
  a:location ->
  v:location_val_t a ->
  machine_state ->
  s:machine_state{eval_location a s == v}

    a: Vale.Transformers.Locations.location ->
    v: Vale.Transformers.Locations.location_val_t a ->
    s: Vale.X64.Machine_Semantics_s.machine_state
  -> s:
    Vale.X64.Machine_Semantics_s.machine_state{Vale.Transformers.Locations.eval_location a s == v}