val va_get_mem_layout (s: va_state) : vale_heap_layout
let va_get_mem_layout (s:va_state) : vale_heap_layout = s.vs_heap.vf_layout
val va_get_mem_layout (s: va_state) : vale_heap_layout
let va_get_mem_layout (s: va_state) : vale_heap_layout =
s.vs_heap.vf_layout
Vale.X64.Decls.fsti.checked
Vale.X64.State.fsti.checked Vale.X64.Stack_i.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.Flags.fsti.checked Vale.Lib.Map16.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Arch.HeapTypes_s.fst.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.All.fst.checked
Vale.X64.Decls.fsti
Vale.X64.Decls.va_state Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout Vale.X64.State.__proj__Mkvale_state__item__vs_heap Vale.Arch.HeapImpl.vale_heap_layout
module Vale.X64.Decls
open FStar.Mul
open Vale.Arch.HeapTypes_s
open Vale.Arch.HeapImpl
module M = Vale.X64.Memory
module S = Vale.X64.Stack_i
module Map16 = Vale.Lib.Map16

// This interface should hide all of Machine_Semantics_s.
// (It should not refer to Machine_Semantics_s, directly or indirectly.)
// It should not refer to StateLemmas, Lemmas, or Print_s,
// because they refer to Machine_Semantics_s.
// Stack_i, Memory, Regs, Flags and State are ok, because they do not refer to Machine_Semantics_s.

open Vale.Def.Prop_s
open Vale.X64.Machine_s
open Vale.X64.State
open Vale.Def.Types_s

unfold let vale_heap = M.vale_heap
unfold let vale_full_heap = M.vale_full_heap
unfold let heaplet_id = M.heaplet_id
unfold let quad32 = quad32

val cf (flags:Flags.t) : bool
val overflow (flags:Flags.t) : bool
val valid_cf (flags:Flags.t) : bool
val valid_of (flags:Flags.t) : bool
val updated_cf (new_flags:Flags.t) (new_cf:bool) : Pure bool
  (requires True)
  (ensures fun b -> b <==> cf new_flags == new_cf /\ valid_cf new_flags)
val updated_of (new_flags:Flags.t) (new_of:bool) : Pure bool
  (requires True)
  (ensures fun b -> b <==> overflow new_flags == new_of /\ valid_of new_flags)
val maintained_cf (new_flags:Flags.t) (flags:Flags.t) : Pure bool
  (requires True)
  (ensures fun b -> b <==> cf new_flags == cf flags /\ valid_cf new_flags == valid_cf flags)
val maintained_of (new_flags:Flags.t) (flags:Flags.t) : Pure bool
  (requires True)
  (ensures fun b -> b <==> overflow new_flags == overflow flags /\ valid_of new_flags == valid_of flags)

//unfold let va_subscript = Map.sel
unfold let va_subscript (#a:eqtype) (#b:Type) (x:Map.t a b) (y:a) : Tot b = Map.sel x y
unfold let va_update = Map.upd
unfold let va_hd = Cons?.hd
//unfold let va_tl = Cons?.tl // F* inlines "let ... = va_tl ..." more than we'd like; revised definition below suppresses this

// REVIEW: reveal_opaque doesn't include zeta, so it fails for recursive functions
[@va_qattr] unfold let va_reveal_eq (#ax:Type) (s:string) (x x':ax) = norm [zeta; delta_only [s]] #ax x == x'
let va_reveal_opaque (s:string) = norm_spec [zeta; delta_only [s]]

// hide 'if' so that x and y get fully normalized
let va_if (#a:Type) (b:bool) (x:(_:unit{b}) -> GTot a) (y:(_:unit{~b}) -> GTot a) : GTot a =
  if b then x () else y ()

let total_if (#a:Type) (b:bool) (x y:a) : a =
  if b then x else y

let total_thunk_if (#a:Type) (b:bool) (x:(_:unit{b}) -> a) (y:(_:unit{~b}) -> a) : a =
  if b then x () else y ()

(* Type aliases *)
let va_int_at_least (k:int) = i:int{i >= k}
let va_int_at_most (k:int) = i:int{i <= k}
let va_int_range (k1 k2:int) = i:int{k1 <= i /\ i <= k2}
val ins : Type0
val ocmp : eqtype
unfold let va_code = precode ins ocmp
unfold let va_codes = list va_code
let va_tl (cs:va_codes) : Ghost va_codes (requires Cons? cs) (ensures fun tl -> tl == Cons?.tl cs) = Cons?.tl cs
unfold let va_state = vale_state
val va_fuel : Type0
unfold let va_operand_opr64 = operand64
let reg_operand = o:operand64{OReg? o}
let va_operand_reg_opr64 = o:operand64{OReg? o}
unfold let va_operand_dst_opr64 = operand64
unfold let va_operand_shift_amt64 = operand64
unfold let cmp_operand = o:operand64{not (OMem? o)}
unfold let va_operand_xmm = reg_xmm
unfold let va_operand_opr128 = operand128
unfold let va_operand_heaplet = heaplet_id

val va_pbool : Type0
val va_ttrue (_:unit) : va_pbool
val va_ffalse (reason:string) : va_pbool
val va_pbool_and (x y:va_pbool) : va_pbool
val get_reason (p:va_pbool) : option string

noeq
type va_transformation_result = {
  success : va_pbool;
  result : va_code;
}
unfold let va_get_success (r:va_transformation_result) : va_pbool = r.success
unfold let va_get_result (r:va_transformation_result) : va_code = r.result

val mul_nat_helper (x y:nat) : Lemma (x * y >= 0)
[@va_qattr] unfold let va_mul_nat (x y:nat) : nat =
  mul_nat_helper x y;
  x * y

[@va_qattr] unfold let va_expand_state (s:vale_state) : vale_state = state_eta s

unfold let get_reg (o:reg_operand) : reg = Reg 0 (OReg?.r o)
unfold let buffer_readable (#t:M.base_typ) (h:vale_heap) (b:M.buffer t) : GTot prop0 = M.buffer_readable #t h b
unfold let buffer_writeable (#t:M.base_typ) (b:M.buffer t) : GTot prop0 = M.buffer_writeable #t b
unfold let buffer_length (#t:M.base_typ) (b:M.buffer t) = M.buffer_length #t b
unfold let buffer8_as_seq (m:vale_heap) (b:M.buffer8) : GTot (Seq.seq nat8) = M.buffer_as_seq m b
unfold let buffer64_as_seq (m:vale_heap) (b:M.buffer64) : GTot (Seq.seq nat64) = M.buffer_as_seq m b
unfold let s64 (m:vale_heap) (b:M.buffer64) : GTot (Seq.seq nat64) = buffer64_as_seq m b
unfold let buffer128_as_seq (m:vale_heap) (b:M.buffer128) : GTot (Seq.seq quad32) = M.buffer_as_seq m b
unfold let s128 (m:vale_heap) (b:M.buffer128) : GTot (Seq.seq quad32) = buffer128_as_seq m b
unfold let valid_src_addr (#t:M.base_typ) (m:vale_heap) (b:M.buffer t) (i:int) : prop0 = M.valid_buffer_read m b i
unfold let valid_dst_addr (#t:M.base_typ) (m:vale_heap) (b:M.buffer t) (i:int) : prop0 = M.valid_buffer_write m b i
unfold let buffer64_read (b:M.buffer64) (i:int) (h:vale_heap) : GTot nat64 = M.buffer_read b i h
unfold let buffer128_read (b:M.buffer128) (i:int) (h:vale_heap) : GTot quad32 = M.buffer_read b i h
unfold let modifies_mem (s:M.loc) (h1 h2:vale_heap) : GTot prop0 = M.modifies s h1 h2
unfold let loc_buffer(#t:M.base_typ) (b:M.buffer t) = M.loc_buffer #t b
unfold let locs_disjoint = M.locs_disjoint
unfold let loc_union = M.loc_union

let valid_buf_maddr64 (addr:int) (s_mem:vale_heap) (layout:vale_heap_layout) (b:M.buffer64) (index:int) (t:taint) : prop0 =
  valid_src_addr s_mem b index /\
  M.valid_taint_buf64 b s_mem layout.vl_taint t /\
  addr == M.buffer_addr b s_mem + 8 * index

let valid_buf_maddr128 (addr:int) (s_mem:vale_heap) (layout:vale_heap_layout) (b:M.buffer128) (index:int) (t:taint) : prop0 =
  valid_src_addr s_mem b index /\
  M.valid_taint_buf128 b s_mem layout.vl_taint t /\
  addr == M.buffer_addr b s_mem + 16 * index

let valid_mem_operand64 (addr:int) (t:taint) (s_mem:vale_heap) (layout:vale_heap_layout) : prop0 =
  exists (b:M.buffer64) (index:int).{:pattern (M.valid_buffer_read s_mem b index)}
    valid_buf_maddr64 addr s_mem layout b index t

let valid_mem_operand128 (addr:int) (t:taint) (s_mem:vale_heap) (layout:vale_heap_layout) : prop0 =
  exists (b:M.buffer128) (index:int).{:pattern (M.valid_buffer_read s_mem b index)}
    valid_buf_maddr128 addr s_mem layout b index t

[@va_qattr]
let valid_operand (o:operand64) (s:vale_state) : prop0 =
  Vale.X64.State.valid_src_operand o s /\
  ( match o with
    | OMem (m, t) -> valid_mem_operand64 (eval_maddr m s) t (M.get_vale_heap s.vs_heap) s.vs_heap.vf_layout
    | OStack (m, t) -> S.valid_taint_stack64 (eval_maddr m s) t s.vs_stackTaint
    | _ -> True
  )

[@va_qattr]
let valid_operand128 (o:operand128) (s:vale_state) : prop0 =
  Vale.X64.State.valid_src_operand128 o s /\
  ( match o with
    | OMem (m, t) -> valid_mem_operand128 (eval_maddr m s) t (M.get_vale_heap s.vs_heap) s.vs_heap.vf_layout
    | OStack (m, t) -> S.valid_taint_stack128 (eval_maddr m s) t s.vs_stackTaint
    | _ -> True
  )

(* Constructors *)
val va_fuel_default : unit -> va_fuel
[@va_qattr] unfold let va_op_xmm_xmm (x:reg_xmm) : va_operand_xmm = x
[@va_qattr] unfold let va_op_opr64_reg64 (r:reg_64) : operand64 = OReg r
[@va_qattr] unfold let va_op_reg64_reg64 (r:reg_64) : operand64 = OReg r
[@va_qattr] unfold let va_op_opr128_xmm (x:reg_xmm) : operand128 = OReg x
[@va_qattr] unfold let va_const_opr64 (n:nat64) : operand64 = OConst n
[@va_qattr] unfold let va_const_shift_amt64 (n:nat64) : operand64 = OConst n
[@va_qattr] unfold let va_op_shift_amt64_reg64 (r:reg_64) : operand64 = OReg r
[@va_qattr] unfold let va_op_cmp_reg64 (r:reg_64) : cmp_operand = OReg r
[@va_qattr] unfold let va_const_cmp (n:nat64) : cmp_operand = OConst n
[@va_qattr] unfold let va_coerce_reg64_opr64_to_cmp (r:va_operand_reg_opr64) : cmp_operand = r
[@va_qattr] unfold let va_coerce_reg_opr64_to_dst_opr64 (o:va_operand_reg_opr64) : va_operand_dst_opr64 = o
[@va_qattr] unfold let va_coerce_reg_opr64_to_opr64 (o:va_operand_reg_opr64) : va_operand_opr64 = o
[@va_qattr] unfold let va_coerce_opr64_to_cmp (o:operand64{not (OMem? o)}) : cmp_operand = o
[@va_qattr] unfold let va_op_reg_opr64_reg64 (r:reg_64) : reg_operand = OReg r
[@va_qattr] unfold let va_op_dst_opr64_reg64 (r:reg_64) : operand64 = OReg r
[@va_qattr] unfold let va_coerce_dst_opr64_to_opr64 (o:operand64) : operand64 = o
[@va_qattr] unfold let va_coerce_xmm_to_opr128 (x:reg_xmm) : operand128 = OReg x
[@va_qattr] unfold let va_op_heaplet_mem_heaplet (h:heaplet_id) : heaplet_id = h

[@va_qattr]
unfold let va_opr_code_Mem64 (h:heaplet_id) (o:operand64) (offset:int) (t:taint) : operand64 =
  match o with
  | OConst n -> OMem (MConst (n + offset), t)
  | OReg r -> OMem (MReg (Reg 0 r) offset, t)
  | _ -> OMem (MConst 42, t)

[@va_qattr]
unfold let va_opr_code_Stack (o:operand64) (offset:int) (t:taint) : operand64 =
  match o with
  | OConst n -> OStack (MConst (n + offset), t)
  | OReg r -> OStack (MReg (Reg 0 r) offset, t)
  | _ -> OStack (MConst 42, t)

[@va_qattr]
unfold let va_opr_code_Mem128 (h:heaplet_id) (o:operand64) (offset:int) (t:taint) : operand128 =
  match o with
  | OReg r -> OMem (MReg (Reg 0 r) offset, t)
  | _ -> OMem (MConst 42, t)

val taint_at (memTaint:M.memtaint) (addr:int) : taint

(* Getters *)
[@va_qattr] unfold let va_get_ok (s:va_state) : bool = s.vs_ok
[@va_qattr] unfold let va_get_flags (s:va_state) : Flags.t = s.vs_flags
[@va_qattr] unfold let va_get_reg64 (r:reg_64) (s:va_state) : nat64 = eval_reg_64 r s
[@va_qattr] unfold let va_get_xmm (x:reg_xmm) (s:va_state) : quad32 = eval_reg_xmm x s
val va_get_mem_layout (s: va_state) : vale_heap_layout
s: Vale.X64.Decls.va_state -> Vale.Arch.HeapImpl.vale_heap_layout