val prints_to_same_code (c1 c2: code) : pbool
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")
val prints_to_same_code (c1 c2: code) : pbool
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")
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.StateLemmas.code Vale.Def.PossiblyMonad.op_Slash_Subtraction Prims.op_Equality FStar.Pervasives.Native.tuple2 Prims.string Prims.int Vale.X64.Print_s.print_code Vale.X64.Print_s.gcc Prims.op_Hat FStar.Pervasives.Native.fst Vale.Def.PossiblyMonad.pbool
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;
    }
val prints_to_same_code (c1 c2: code) : pbool
c1: Vale.X64.StateLemmas.code -> c2: Vale.X64.StateLemmas.code -> Vale.Def.PossiblyMonad.pbool