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)]
let downgrade_val_raise_val_u0_u1 #a x = FStar.Universe.downgrade_val_raise_val #a x
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)]
let downgrade_val_raise_val_u0_u1 #a x =
FStar.Universe.downgrade_val_raise_val #a x
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
FStar.Universe.downgrade_val_raise_val Prims.unit
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 = ()
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)]
x: a
  -> FStar.Pervasives.Lemma (ensures FStar.Universe.downgrade_val (FStar.Universe.raise_val x) == x)
      [SMTPat (FStar.Universe.raise_val x)]