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 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 }
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.Def.PossiblyMonad.possibly Vale.X64.Lemmas.codes Vale.X64.StateLemmas.code Vale.X64.Decls.Mkva_transformation_result Vale.Def.PossiblyMonad.ttrue Vale.X64.Machine_s.Block Vale.X64.Bytes_Code_s.instruction_t Vale.X64.Machine_Semantics_s.instr_annotation Vale.X64.Bytes_Code_s.ocmp Prims.string Vale.Def.PossiblyMonad.ffalse 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
val transformation_result_of_possibly_codes : c: Vale.Def.PossiblyMonad.possibly Vale.X64.Lemmas.codes -> if_fail: Vale.X64.StateLemmas.code
  -> Vale.X64.Decls.va_transformation_result
c: Vale.Def.PossiblyMonad.possibly Vale.X64.Lemmas.codes -> if_fail: Vale.X64.StateLemmas.code
  -> Vale.X64.Decls.va_transformation_result