val raise_location_val_eqt (#l: location_eq) (v: location_val_eqt l) : location_val_t l
let raise_location_val_eqt (#l:location_eq) (v:location_val_eqt l) : location_val_t l =
  coerce (FStar.Universe.raise_val v)
val raise_location_val_eqt (#l: location_eq) (v: location_val_eqt l) : location_val_t l
let raise_location_val_eqt (#l: location_eq) (v: location_val_eqt l) : location_val_t l =
coerce (FStar.Universe.raise_val v)
Vale.Transformers.Locations.fsti.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 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
Vale.Transformers.Locations.fsti
Vale.Transformers.Locations.location_eq Vale.Transformers.Locations.location_val_eqt Vale.X64.Instruction_s.coerce Vale.Transformers.Locations.location_val_t FStar.Universe.raise_t FStar.Universe.raise_val
module Vale.Transformers.Locations

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

(** An [location] is a portion of the [machine_state] that may be
    independently modified and/or accessed. *)
val location : eqtype

unfold
type locations = list location

(** [disjoint_location a1 a2] is true whenever locations [a1] and [a2]
    are disjoint. When not disjoint, it gives a reason for why not. *)
val disjoint_location : location -> location -> pbool

(** Disjointness is the same as syntactic equality on the locations. *)
val auto_lemma_disjoint_location :
  a1:location -> a2:location ->
  Lemma
    (ensures (!!(disjoint_location a1 a2) = (a1 <> a2)))
    [SMTPat (!!(disjoint_location a1 a2))]

(** Disjointness of a [location] from [locations] *)
let disjoint_location_from_locations (a:location) (l:locations) : pbool =
  for_all (fun b ->
      disjoint_location a b
    ) l

(** Disjointness of [locations] *)
let disjoint_locations (l1 l2:locations) : pbool =
  for_all (fun x ->
      disjoint_location_from_locations x l2
  ) l1

(** [disjoint_locations] is symmetric *)
let rec lemma_disjoint_locations_symmetric l1 l2 :
  Lemma
    (ensures (
        (!!(disjoint_locations l1 l2) = !!(disjoint_locations l2 l1))))
    (decreases %[L.length l1 + L.length l2]) =
  match l1, l2 with
  | [], [] -> ()
  | [], x :: xs | x :: xs, [] ->
    lemma_disjoint_locations_symmetric xs []
  | x :: xs, y :: ys ->
    lemma_disjoint_locations_symmetric l1 ys;
    lemma_disjoint_locations_symmetric xs l2;
    lemma_disjoint_locations_symmetric xs ys

(** Inversion lemma based on FStar.Universe.downgrade_val_raise_val, with more liberal SMTPat *)
val downgrade_val_raise_val_u0_u1 :
  #a:Type0 ->
  x:a ->
  Lemma
    (ensures FStar.Universe.downgrade_val u#0 u#1 (FStar.Universe.raise_val x) == x)
    [SMTPat (FStar.Universe.raise_val x)]

(** [location_val_t a] is the type of the value represented by the location [a]. *)
val location_val_t : location -> Type u#1

(** Same as location_val_t in cases where location_val_t is an eqtype, otherwise arbitrary *)
val location_val_eqt : location -> eqtype

(** Locations where location_val_t is an eqtype *)
let location_eq = l:location{location_val_t l == FStar.Universe.raise_t (location_val_eqt l)}

(** Coerce location_val_eqt to location_val_t *)
val raise_location_val_eqt (#l: location_eq) (v: location_val_eqt l) : location_val_t l
v: Vale.Transformers.Locations.location_val_eqt l -> Vale.Transformers.Locations.location_val_t l