val eval_code_eq_f (c: code) (f: fuel) (s1 s2: state)
    : Lemma (requires state_eq_S false s1 s2)
      (ensures state_eq_opt false (S.eval_code c f s1) (S.eval_code c f s2))
      [SMTPat (S.eval_code c f s1); SMTPat (S.eval_code c f s2)]
let eval_code_eq_f (c:code) (f:fuel) (s1 s2:state) : Lemma
  (requires state_eq_S false s1 s2)
  (ensures state_eq_opt false (S.eval_code c f s1) (S.eval_code c f s2))
  [SMTPat (S.eval_code c f s1); SMTPat (S.eval_code c f s2)]
  =
  eval_code_eq_core false c f s1; eval_code_eq_core false c f s2
val eval_code_eq_f (c: code) (f: fuel) (s1 s2: state)
    : Lemma (requires state_eq_S false s1 s2)
      (ensures state_eq_opt false (S.eval_code c f s1) (S.eval_code c f s2))
      [SMTPat (S.eval_code c f s1); SMTPat (S.eval_code c f s2)]
let eval_code_eq_f (c: code) (f: fuel) (s1 s2: state)
    : Lemma (requires state_eq_S false s1 s2)
      (ensures state_eq_opt false (S.eval_code c f s1) (S.eval_code c f s2))
      [SMTPat (S.eval_code c f s1); SMTPat (S.eval_code c f s2)] =
eval_code_eq_core false c f s1;
eval_code_eq_core false c f s2
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
Vale.PPC64LE.Lemmas.code Vale.PPC64LE.Lemmas.fuel Vale.PPC64LE.State.state Vale.PPC64LE.Lemmas.eval_code_eq_core Prims.unit Vale.PPC64LE.Lemmas.state_eq_S Prims.squash Vale.PPC64LE.Lemmas.state_eq_opt Vale.PPC64LE.Semantics_s.eval_code Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat FStar.Pervasives.Native.option Vale.PPC64LE.Machine_s.state Prims.Nil
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
  ))
  =
  lemma_heap_ignore_ghost_machine s.ms_heap (core_state g s).ms_heap;
  use_machine_state_equal ()

let eval_ocmp_eq_core (g:bool) (cond:ocmp) (s:state) : Lemma
  (ensures (
    let (s1, b1) = S.run_ocmp s cond in
    let (s2, b2) = S.run_ocmp (core_state g s) cond in
    state_eq_S g s1 s2 /\ b1 == b2
  ))
  =
  ()

#restart-solver
let rec eval_code_eq_core (g:bool) (c:code) (f:fuel) (s:state) : Lemma
  (ensures state_eq_opt g (S.eval_code c f s) (S.eval_code c f (core_state g s)))
  (decreases %[f; c])
  =
  match c with
  | Ins i -> eval_code_eq_ins g i s
  | Block cs -> eval_codes_eq_core g cs f s
  | IfElse cond ct cf ->
    eval_ocmp_eq_core g cond s;
    let (s', _) = S.run_ocmp s cond in
    let (t', _) = S.run_ocmp (core_state g s) cond in
    eval_code_eq_core g ct f s';
    eval_code_eq_core g ct f t';
    eval_code_eq_core g cf f s';
    eval_code_eq_core g cf f t';
    ()
  | While cond body -> eval_while_eq_core g cond body f s
and eval_codes_eq_core (g:bool) (cs:codes) (f:fuel) (s:state) : Lemma
  (ensures state_eq_opt g (S.eval_codes cs f s) (S.eval_codes cs f (core_state g s)))
  (decreases %[f; cs])
  =
  match cs with
  | [] -> ()
  | c'::cs' -> (
      eval_code_eq_core g c' f s;
      match (S.eval_code c' f s, S.eval_code c' f (core_state g s)) with
      | (None, None) -> ()
      | (Some s', Some t') -> eval_codes_eq_core g cs' f s'; eval_codes_eq_core g cs' f t'
    )
and eval_while_eq_core (g:bool) (cond:ocmp) (body:code) (f:fuel) (s:state) : Lemma
  (ensures state_eq_opt g (S.eval_while cond body f s) (S.eval_while cond body f (core_state g s)))
  (decreases %[f; body])
  =
  if f > 0 then (
    eval_ocmp_eq_core g cond s;
    let (s1, _) = S.run_ocmp s cond in
    let (t1, _) = S.run_ocmp (core_state g s) cond in
    eval_code_eq_core g body (f - 1) s1;
    eval_code_eq_core g body (f - 1) t1;
    match (S.eval_code body (f - 1) s1, S.eval_code body (f - 1) t1) with
    | (None, None) -> ()
    | (Some s2, Some t2) ->
      eval_while_eq_core g cond body (f - 1) s2;
      eval_while_eq_core g cond body (f - 1) t2;
      ()
  )

let eval_code_eq_f (c:code) (f:fuel) (s1 s2:state) : Lemma
  (requires state_eq_S false s1 s2)
  (ensures state_eq_opt false (S.eval_code c f s1) (S.eval_code c f s2))
  [SMTPat (S.eval_code c f s1); SMTPat (S.eval_code c f s2)]
val eval_code_eq_f (c: code) (f: fuel) (s1 s2: state)
    : Lemma (requires state_eq_S false s1 s2)
      (ensures state_eq_opt false (S.eval_code c f s1) (S.eval_code c f s2))
      [SMTPat (S.eval_code c f s1); SMTPat (S.eval_code c f s2)]

    c: Vale.PPC64LE.Lemmas.code ->
    f: Vale.PPC64LE.Lemmas.fuel ->
    s1: Vale.PPC64LE.State.state ->
    s2: Vale.PPC64LE.State.state
  -> FStar.Pervasives.Lemma (requires Vale.PPC64LE.Lemmas.state_eq_S false s1 s2)
      (ensures
        Vale.PPC64LE.Lemmas.state_eq_opt false
          (Vale.PPC64LE.Semantics_s.eval_code c f s1)
          (Vale.PPC64LE.Semantics_s.eval_code c f s2))
      [
        SMTPat (Vale.PPC64LE.Semantics_s.eval_code c f s1);
        SMTPat (Vale.PPC64LE.Semantics_s.eval_code c f s2)
      ]