val eval_code_eq_ins (g: bool) (i: S.ins) (s: state)
    : Lemma
    (ensures
      (let s1 = S.run (S.eval_ins i) s in
        let s2 = S.run (S.eval_ins i) (core_state g s) in
        state_eq_S g s1 s2))
let eval_code_eq_ins (g:bool) (i:S.ins) (s:state) : Lemma
  (ensures (
    let s1 = S.run (S.eval_ins i) s in
    let s2 = S.run (S.eval_ins i) (core_state g s) in
    state_eq_S g s1 s2
  ))
  =
  lemma_heap_ignore_ghost_machine s.ms_heap (core_state g s).ms_heap;
  use_machine_state_equal ()
val eval_code_eq_ins (g: bool) (i: S.ins) (s: state)
    : Lemma
    (ensures
      (let s1 = S.run (S.eval_ins i) s in
        let s2 = S.run (S.eval_ins i) (core_state g s) in
        state_eq_S g s1 s2))
let eval_code_eq_ins (g: bool) (i: S.ins) (s: state)
    : Lemma
    (ensures
      (let s1 = S.run (S.eval_ins i) s in
        let s2 = S.run (S.eval_ins i) (core_state g s) in
        state_eq_S g s1 s2)) =
lemma_heap_ignore_ghost_machine s.ms_heap (core_state g s).ms_heap;
use_machine_state_equal ()
Vale.PPC64LE.Lemmas.fst.checked
Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Machine_s.fst.checked Vale.Arch.HeapLemmas.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
Vale.PPC64LE.Lemmas.fst
Prims.bool Vale.PPC64LE.Semantics_s.ins Vale.PPC64LE.State.state Vale.PPC64LE.State.use_machine_state_equal Prims.unit Vale.Arch.HeapLemmas.lemma_heap_ignore_ghost_machine Vale.PPC64LE.Machine_s.__proj__Mkstate__item__ms_heap Vale.PPC64LE.Lemmas.core_state Prims.l_True Prims.squash Vale.PPC64LE.Lemmas.state_eq_S Vale.PPC64LE.Machine_s.state Vale.PPC64LE.Semantics_s.run Vale.PPC64LE.Semantics_s.eval_ins Prims.Nil FStar.Pervasives.pattern
module Vale.PPC64LE.Lemmas
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
module S = Vale.PPC64LE.Semantics_s
open Vale.Arch.HeapLemmas

#reset-options "--initial_fuel 2 --max_fuel 2 --z3rlimit 400"

let eval_code_eq_ins (g:bool) (i:S.ins) (s:state) : Lemma
  (ensures (
    let s1 = S.run (S.eval_ins i) s in
    let s2 = S.run (S.eval_ins i) (core_state g s) in
    state_eq_S g s1 s2
  ))
val eval_code_eq_ins (g: bool) (i: S.ins) (s: state)
    : Lemma
    (ensures
      (let s1 = S.run (S.eval_ins i) s in
        let s2 = S.run (S.eval_ins i) (core_state g s) in
        state_eq_S g s1 s2))
g: Prims.bool -> i: Vale.PPC64LE.Semantics_s.ins -> s: Vale.PPC64LE.State.state
  -> FStar.Pervasives.Lemma
    (ensures
      (let s1 = Vale.PPC64LE.Semantics_s.run (Vale.PPC64LE.Semantics_s.eval_ins i) s in
        let s2 =
          Vale.PPC64LE.Semantics_s.run (Vale.PPC64LE.Semantics_s.eval_ins i)
            (Vale.PPC64LE.Lemmas.core_state g s)
        in
        Vale.PPC64LE.Lemmas.state_eq_S g s1 s2))