val disjoint_location : location -> location -> pbool
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
val disjoint_location : location -> location -> pbool
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
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 FStar.Pervasives.Native.Mktuple2 Vale.Def.PossiblyMonad.ffalse Vale.Def.PossiblyMonad.ttrue Vale.X64.Machine_s.reg Vale.Def.PossiblyMonad.op_Slash_Subtraction Prims.op_disEquality Prims.op_Hat Vale.Transformers.Locations.aux_print_reg_from_location Vale.Def.PossiblyMonad.pbool
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 *)
val disjoint_location : location -> location -> pbool
a1: Vale.Transformers.Locations.location -> a2: Vale.Transformers.Locations.location
  -> Vale.Def.PossiblyMonad.pbool