val reorder :
  orig:va_code ->
  hint:va_code ->
  va_transformation_result
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
val reorder :
  orig:va_code ->
  hint:va_code ->
  va_transformation_result
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
      let+ _ = prints_to_same_code (Block transformed) hint in
      return transformed)
  orig
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.Transformers.Transform.transformation_result_of_possibly_codes Vale.X64.Lemmas.code_modifies_ghost Vale.Def.PossiblyMonad.Err Vale.X64.Lemmas.codes Prims.bool Vale.Def.PossiblyMonad.op_let_Plus Vale.Transformers.InstructionReorder.transformation_hints Vale.X64.Machine_Semantics_s.codes Vale.Transformers.InstructionReorder.find_transformation_hints Prims.Cons Vale.X64.Bytes_Code_s.code_t Vale.X64.Machine_Semantics_s.instr_annotation Prims.Nil Vale.Transformers.InstructionReorder.perform_reordering_with_hints Prims.unit Vale.Transformers.Transform.prints_to_same_code Vale.X64.Machine_s.Block Vale.X64.Bytes_Code_s.instruction_t Vale.X64.Bytes_Code_s.ocmp Vale.Def.PossiblyMonad.return Vale.Def.PossiblyMonad.possibly Vale.Transformers.InstructionReorder.purge_empty_codes Vale.X64.Decls.va_transformation_result
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 *)
val reorder :
  orig:va_code ->
  hint:va_code ->
  va_transformation_result
orig: Vale.X64.Decls.va_code -> hint: Vale.X64.Decls.va_code
  -> Vale.X64.Decls.va_transformation_result