val eval_ins (c: code) (s0: state)
    : Pure (state & fuel) (requires Ins? c) (ensures fun (sM, f0) -> eval_code c s0 f0 sM)
val eval_ins (c: code) (s0: state)
    : Pure (state & fuel) (requires Ins? c) (ensures fun (sM, f0) -> eval_code c s0 f0 sM)
let eval_ins (c:code) (s0:state) : Pure (state & fuel)
  (requires Ins? c)
  (ensures fun (sM, f0) ->
    eval_code c s0 f0 sM
  ) =
  let f0 = 0 in
  let (Some sM) = S.eval_code c f0 s0 in
  (sM, f0)
module Vale.PPC64LE.Lemmas
open Vale.Def.Prop_s
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.StateLemmas
module S = Vale.PPC64LE.Semantics_s
open Vale.Arch.Heap
open Vale.Arch.HeapImpl
open Vale.Arch.HeapLemmas

unfold let code = S.code
unfold let codes = S.codes
unfold let ocmp = S.ocmp
unfold let fuel = nat

let xer_ov (xer:xer_t) : bool = S.xer_ov xer
let xer_ca (xer:xer_t) : bool = S.xer_ca xer
let update_xer_ov (xer:xer_t) (new_xer_ov:bool) = S.update_xer_ov xer new_xer_ov
let update_xer_ca (xer:xer_t) (new_xer_ca:bool) = S.update_xer_ca xer new_xer_ca

let rec code_modifies_ghost (c:code) : bool =
  match c with
  | Ins (S.Ghost _) -> true
  | Ins _ -> false
  | Block cs -> codes_modifies_ghost cs
  | IfElse _ c1 c2 -> code_modifies_ghost c1 || code_modifies_ghost c2
  | While _ c -> code_modifies_ghost c
and codes_modifies_ghost (cs:codes) : bool =
  match cs with
  | [] -> false
  | c::cs -> code_modifies_ghost c || codes_modifies_ghost cs

let core_state (ignore_ghost:bool) (s:state) : state =
  {s with
    ms_heap = if ignore_ghost then heap_ignore_ghost_machine s.ms_heap else s.ms_heap;
  }

let state_eq_S (ignore_ghost:bool) (s1 s2:state) =
  machine_state_eq (core_state ignore_ghost s1) (core_state ignore_ghost s2)

let state_eq_opt (ignore_ghost:bool) (s1 s2:option state) =
  match (s1, s2) with
  | (Some s1, Some s2) -> state_eq_S ignore_ghost s1 s2
  | _ -> s1 == s2

let eval_code (c:code) (s0:state) (f0:fuel) (s1:state) : Type0 =
  state_eq_opt (code_modifies_ghost c) (S.eval_code c f0 s0) (Some s1)

let eval_code2 (c:code) (s0:state) (f0:fuel) (s1:state) : prop0 =
  Some s1 == S.eval_code c f0 s0
/
Vale.PPC64LE.StateLemmas.fsti.checked Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Machine_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Arch.HeapLemmas.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.PPC64LE.Lemmas.fsti
c: Vale.PPC64LE.Lemmas.code -> s0: Vale.PPC64LE.State.state
  -> Prims.Pure (Vale.PPC64LE.State.state * Vale.PPC64LE.Lemmas.fuel)
Vale.PPC64LE.Lemmas.code Vale.PPC64LE.State.state Vale.PPC64LE.Machine_s.state FStar.Pervasives.Native.Mktuple2 Vale.PPC64LE.Lemmas.fuel FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.option Vale.PPC64LE.Semantics_s.eval_code Prims.int Prims.b2t Vale.PPC64LE.Machine_s.uu___is_Ins Vale.PPC64LE.Semantics_s.ins Vale.PPC64LE.Semantics_s.ocmp Vale.PPC64LE.Lemmas.eval_code
let eval_ins (c: code) (s0: state)
    : Pure (state & fuel) (requires Ins? c) (ensures fun (sM, f0) -> eval_code c s0 f0 sM) =
  
let f0 = 0 in
let Some sM = S.eval_code c f0 s0 in
(sM, f0)