val lemma_reorder :
  orig:va_code ->
  hint:va_code ->
  transformed:va_code ->
  va_s0:va_state -> va_sM:va_state -> va_fM:va_fuel ->
  Ghost (va_state & va_fuel)
    (requires (
        (va_require_total transformed (reorder orig hint).result va_s0) /\
        (va_get_ok va_s0) /\
        (va_ensure_total orig va_s0 va_sM va_fM) /\
        (va_get_ok va_sM)))
    (ensures (fun (va_sM', va_fM') ->
         (va_fM' == va_fM) /\
         (equiv_states va_sM va_sM') /\
         (va_ensure_total transformed va_s0 va_sM' va_fM') /\
         (va_get_ok va_sM')))
let lemma_reorder orig hint transformed va_s0 va_sM va_fM =
  if code_modifies_ghost orig then (va_sM, va_fM) else
  let orig' = IR.purge_empty_codes [orig] in
  match IR.find_transformation_hints orig' [hint] with
  | Err _ -> va_sM, va_fM
  | Ok ts ->
    match IR.perform_reordering_with_hints ts orig' with
    | Err _ -> va_sM, va_fM
    | Ok tr ->
      lemma_code_codes orig va_fM (state_to_S va_s0);
      IR.lemma_purge_empty_codes [orig] va_fM (state_to_S va_s0);
      IR.lemma_perform_reordering_with_hints ts orig' va_fM (state_to_S va_s0);
      lemma_codes_code tr va_fM (state_to_S va_s0);
      let Some s = machine_eval_code orig va_fM (state_to_S va_s0) in
      let Some s' = machine_eval_code transformed va_fM (state_to_S va_s0) in
      lemma_IR_equiv_states_to_equiv_states s s';
      assert (eval_code orig va_s0 va_fM va_sM);
      assert ({s with ms_trace = []} == (state_to_S va_sM));
      let va_sM' = state_of_S s' in
      lemma_to_of s';
      assert (state_to_S va_sM' == {s' with ms_trace = []});
      assert (state_to_S va_sM == {s with ms_trace = []});
      assert (IR.equiv_states ({s with ms_trace = []}) ({s' with ms_trace = []}));
      assert (equiv_states va_sM va_sM');
      assert (va_ensure_total transformed va_s0 va_sM' va_fM);
      va_sM', va_fM
val lemma_reorder :
  orig:va_code ->
  hint:va_code ->
  transformed:va_code ->
  va_s0:va_state -> va_sM:va_state -> va_fM:va_fuel ->
  Ghost (va_state & va_fuel)
    (requires (
        (va_require_total transformed (reorder orig hint).result va_s0) /\
        (va_get_ok va_s0) /\
        (va_ensure_total orig va_s0 va_sM va_fM) /\
        (va_get_ok va_sM)))
    (ensures (fun (va_sM', va_fM') ->
         (va_fM' == va_fM) /\
         (equiv_states va_sM va_sM') /\
         (va_ensure_total transformed va_s0 va_sM' va_fM') /\
         (va_get_ok va_sM')))
let lemma_reorder orig hint transformed va_s0 va_sM va_fM =
if code_modifies_ghost orig
then (va_sM, va_fM)
else
  let orig' = IR.purge_empty_codes [orig] in
  match IR.find_transformation_hints orig' [hint] with
  | Err _ -> va_sM, va_fM
  | Ok ts ->
    match IR.perform_reordering_with_hints ts orig' with
    | Err _ -> va_sM, va_fM
    | Ok tr ->
      lemma_code_codes orig va_fM (state_to_S va_s0);
      IR.lemma_purge_empty_codes [orig] va_fM (state_to_S va_s0);
      IR.lemma_perform_reordering_with_hints ts orig' va_fM (state_to_S va_s0);
      lemma_codes_code tr va_fM (state_to_S va_s0);
      let Some s = machine_eval_code orig va_fM (state_to_S va_s0) in
      let Some s' = machine_eval_code transformed va_fM (state_to_S va_s0) in
      lemma_IR_equiv_states_to_equiv_states s s';
      assert (eval_code orig va_s0 va_fM va_sM);
      assert ({ s with ms_trace = [] } == (state_to_S va_sM));
      let va_sM' = state_of_S s' in
      lemma_to_of s';
      assert (state_to_S va_sM' == { s' with ms_trace = [] });
      assert (state_to_S va_sM == { s with ms_trace = [] });
      assert (IR.equiv_states ({ s with ms_trace = [] }) ({ s' with ms_trace = [] }));
      assert (equiv_states va_sM va_sM');
      assert (va_ensure_total transformed va_s0 va_sM' va_fM);
      va_sM', va_fM
Vale.Transformers.Transform.fst.checked
Vale.X64.StateLemmas.fst.checked Vale.X64.StateLemmas.fst.checked Vale.X64.State.fsti.checked Vale.X64.Print_s.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Lemmas.fsti.checked Vale.X64.Decls.fst.checked Vale.X64.Decls.fst.checked Vale.Transformers.PrefetchElim.fst.checked Vale.Transformers.PeepHole.fsti.checked Vale.Transformers.MovMovElim.fst.checked Vale.Transformers.MovbeElim.fst.checked Vale.Transformers.InstructionReorder.fst.checked Vale.Def.PossiblyMonad.fst.checked Vale.Arch.HeapLemmas.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.Transformers.Transform.fst
Vale.X64.Decls.va_code Vale.X64.Decls.va_state Vale.X64.Decls.va_fuel Vale.X64.Lemmas.code_modifies_ghost FStar.Pervasives.Native.Mktuple2 Prims.bool Vale.Transformers.InstructionReorder.find_transformation_hints Prims.Cons Vale.X64.Bytes_Code_s.code_t Vale.X64.Machine_Semantics_s.instr_annotation Prims.Nil Prims.string Vale.Transformers.InstructionReorder.transformation_hints Vale.Transformers.InstructionReorder.perform_reordering_with_hints Vale.X64.Machine_Semantics_s.codes Vale.X64.Machine_Semantics_s.machine_state Prims.unit Prims._assert Vale.X64.Decls.va_ensure_total Vale.Transformers.Transform.equiv_states Vale.Transformers.InstructionReorder.equiv_states Vale.X64.Machine_Semantics_s.Mkmachine_state Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stack Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint Vale.X64.Machine_s.observation Prims.eq2 Vale.X64.StateLemmas.state_to_S Vale.X64.StateLemmas.lemma_to_of Vale.X64.State.vale_state Vale.X64.StateLemmas.state_of_S Vale.X64.Lemmas.eval_code Vale.Transformers.Transform.lemma_IR_equiv_states_to_equiv_states FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.option Vale.X64.StateLemmas.machine_eval_code Vale.Transformers.Transform.lemma_codes_code Vale.Transformers.InstructionReorder.lemma_perform_reordering_with_hints Vale.Transformers.InstructionReorder.lemma_purge_empty_codes Vale.Transformers.Transform.lemma_code_codes Vale.Transformers.InstructionReorder.purge_empty_codes
module Vale.Transformers.Transform

module BS = Vale.X64.Machine_Semantics_s

open Vale.X64.Machine_Semantics_s
open Vale.X64.Machine_s
open Vale.Def.PossiblyMonad
open Vale.X64.Decls

open Vale.X64.State

open Vale.X64.Lemmas
open Vale.X64.StateLemmas
open Vale.Arch.HeapLemmas

friend Vale.X64.Decls
friend Vale.X64.StateLemmas

module IR = Vale.Transformers.InstructionReorder
module PH = Vale.Transformers.PeepHole
module ME = Vale.Transformers.MovbeElim

unfold
let transformation_result_of_possibly_codes (c:possibly codes) (if_fail:code) =
  match c with
  | Ok c -> {
      success = ttrue;
      result = Block c;
    }
  | Err reason -> {
      success = ffalse reason;
      result = if_fail;
    }

let prints_to_same_code (c1 c2:code) : pbool =
  let open Vale.X64.Print_s in
  ((print_code c1 0 gcc) = (print_code c2 0 gcc)) /-
  ("Not matching codes: \n" ^
   "\tCode:\n" ^
   fst (print_code c1 0 gcc) ^
   "\tExpected code:\n" ^
   fst (print_code c2 0 gcc) ^
   "\n")

/// Reordering transformation

(* See fsti *)
let reorder orig hint =
  transformation_result_of_possibly_codes (
    if code_modifies_ghost orig then Err "code directly modifies ghost state (via ins_Ghost instruction)" else
    let orig' = IR.purge_empty_codes [orig] in
    let+ ts = IR.find_transformation_hints orig' [hint] in
    let+ transformed = IR.perform_reordering_with_hints ts orig' in
    prints_to_same_code (Block transformed) hint;+
    return transformed
  ) orig

#push-options "--max_fuel 2 --max_ifuel 1"
let lemma_code_codes (c:code) (fuel:nat) (s:machine_state) :
  Lemma
    (ensures (machine_eval_code c fuel s == machine_eval_codes [c] fuel s)) = ()

let lemma_codes_code (c:codes) (fuel:nat) (s:machine_state) :
  Lemma
    (ensures (machine_eval_codes c fuel s == machine_eval_code (Block c) fuel s)) = ()
#pop-options

let lemma_IR_equiv_states_to_equiv_states (s1 s2:machine_state) :
  Lemma
    (requires (
        (IR.equiv_states s1 s2)))
    (ensures (
        (equiv_states (state_of_S s1) (state_of_S s2)))) = ()

(* See fsti *)
val lemma_reorder :
  orig:va_code ->
  hint:va_code ->
  transformed:va_code ->
  va_s0:va_state -> va_sM:va_state -> va_fM:va_fuel ->
  Ghost (va_state & va_fuel)
    (requires (
        (va_require_total transformed (reorder orig hint).result va_s0) /\
        (va_get_ok va_s0) /\
        (va_ensure_total orig va_s0 va_sM va_fM) /\
        (va_get_ok va_sM)))
    (ensures (fun (va_sM', va_fM') ->
         (va_fM' == va_fM) /\
         (equiv_states va_sM va_sM') /\
         (va_ensure_total transformed va_s0 va_sM' va_fM') /\
         (va_get_ok va_sM')))

    orig: Vale.X64.Decls.va_code ->
    hint: Vale.X64.Decls.va_code ->
    transformed: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    va_sM: Vale.X64.Decls.va_state ->
    va_fM: Vale.X64.Decls.va_fuel
  -> Prims.Ghost (Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel)