val s64 (m: vale_heap) (b: M.buffer64) : GTot (Seq.seq nat64)
let s64 (m:vale_heap) (b:M.buffer64) : GTot (Seq.seq nat64) = buffer64_as_seq m b
val s64 (m: vale_heap) (b: M.buffer64) : GTot (Seq.seq nat64)
let s64 (m: vale_heap) (b: M.buffer64) : GTot (Seq.seq nat64) =
buffer64_as_seq m b
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.vale_heap Vale.X64.Memory.buffer64 Vale.X64.Decls.buffer64_as_seq FStar.Seq.Base.seq Vale.Def.Types_s.nat64
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
val s64 (m: vale_heap) (b: M.buffer64) : GTot (Seq.seq nat64)
m: Vale.X64.Decls.vale_heap -> b: Vale.X64.Memory.buffer64
  -> Prims.GTot (FStar.Seq.Base.seq Vale.Def.Types_s.nat64)