[ "(\u001bá,\u0011þxï§x½$\u001d\u0012­Ô", [ [ "Vale.Transformers.Transform.transformation_result_of_possibly_codes", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "disc_equation_Vale.Def.PossiblyMonad.Err", "disc_equation_Vale.Def.PossiblyMonad.Ok", "equation_Vale.X64.Machine_Semantics_s.codes", "fuel_guarded_inversion_Vale.Def.PossiblyMonad.possibly" ], 0, "917188bd9f0226bd1f6b8c4437afed4a" ], [ "Vale.Transformers.Transform.prints_to_same_code", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "assumption_FStar.Pervasives.Native.tuple2__uu___haseq", "equation_Prims.eqtype", "function_token_typing_Prims.int", "function_token_typing_Prims.string", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "bd05e3d29902267b6f9dbc4bc4c69fae" ], [ "Vale.Transformers.Transform.lemma_code_codes", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@query", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_elim_FStar.Pervasives.Native.Some", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Nil@tok", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equation_Prims.nat", "equation_Vale.X64.Bytes_Code_s.codes_t", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "function_token_typing_Vale.X64.Machine_Semantics_s.code", "int_inversion", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code" ], 0, "da931eb9a015626c9837ad9621baf063" ], [ "Vale.Transformers.Transform.lemma_codes_code", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@query", "constructor_distinct_Vale.X64.Machine_s.Block", "data_typing_intro_Vale.X64.Machine_s.Block@tok", "equation_Prims.nat", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Bytes_Code_s.codes_t", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "function_token_typing_Vale.X64.Machine_Semantics_s.ins", "int_inversion", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok", "projection_inverse_Vale.X64.Machine_s.Block_block", "projection_inverse_Vale.X64.Machine_s.Block_t_ins", "projection_inverse_Vale.X64.Machine_s.Block_t_ocmp", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "a9d4c980cc7f41e8ed9c53d0597bb67e" ], [ "Vale.Transformers.Transform.lemma_IR_equiv_states_to_equiv_states", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_Vale.Transformers.Common.equiv_states", "equation_Vale.Transformers.InstructionReorder.equiv_states", "equation_Vale.X64.Machine_Semantics_s.cf", "equation_Vale.X64.Machine_Semantics_s.flags_t", "equation_Vale.X64.Machine_Semantics_s.overflow", "equation_Vale.X64.Machine_s.flag", "equation_Vale.X64.StateLemmas.state_of_S", "int_typing", "interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366", "lemma_Vale.X64.Regs.lemma_equal_intro", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_423a970236765465eb8eb63b6e1b8f53", "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "typing_Vale.X64.Flags.of_fun", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.StateLemmas.state_of_S" ], 0, "e3ffab73eac14f8cb568e011a9eb7dea" ], [ "Vale.Transformers.Transform.lemma_reorder", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.X64.Flags_interpretation_Tm_arrow_c9f84314ba6aade3760e20965d165b65", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.Def.PossiblyMonad.Err", "constructor_distinct_Vale.Def.PossiblyMonad.Ok", "constructor_distinct_Vale.X64.Machine_s.Block", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Vale.Def.PossiblyMonad.Err", "disc_equation_Vale.Def.PossiblyMonad.Ok", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_Prims.nat", "equation_Vale.Transformers.Common.equiv_states", "equation_Vale.Transformers.InstructionReorder.equiv_states", "equation_Vale.Transformers.InstructionReorder.transformation_hints", "equation_Vale.Transformers.Transform.reorder", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Flags.sel_curry", "equation_Vale.X64.Flags.to_fun", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.eval_code", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.Machine_Semantics_s.cf", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "equation_Vale.X64.Machine_Semantics_s.flags_t", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_Semantics_s.overflow", "equation_Vale.X64.Machine_Semantics_s.regs_t", "equation_Vale.X64.Machine_s.flag", "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_Vale.X64.StateLemmas.state_of_S", "equation_Vale.X64.StateLemmas.state_to_S", "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Vale.X64.Decls.va_transformation_result", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.X64.Flags.sel_curry", "function_token_typing_Vale.X64.Machine_s.t_reg", "int_inversion", "int_typing", "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "kinding_Vale.X64.Machine_s.reg@tok", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_FStar.Pervasives.invertOption", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_intro", "lemma_Vale.X64.Stack_Sems.lemma_stack_from_to", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Vale.X64.Decls.Mkva_transformation_result_result", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Vale.Def.PossiblyMonad.Err__a", "projection_inverse_Vale.Def.PossiblyMonad.Err_reason", "projection_inverse_Vale.Def.PossiblyMonad.Ok__a", "projection_inverse_Vale.Def.PossiblyMonad.Ok_v", "projection_inverse_Vale.X64.Decls.Mkva_transformation_result_result", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint", "projection_inverse_Vale.X64.Machine_s.Block_block", "projection_inverse_Vale.X64.Machine_s.Block_t_ins", "projection_inverse_Vale.X64.Machine_s.Block_t_ocmp", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7", "refinement_interpretation_Tm_refine_423a970236765465eb8eb63b6e1b8f53", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64", "token_correspondence_Vale.X64.Flags.sel_curry", "token_correspondence_Vale.X64.Machine_s.t_reg", "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "typing_Tm_abs_f086d77986b470aab4bfebc171e6c366", "typing_Vale.Transformers.Transform.reorder", "typing_Vale.X64.Decls.__proj__Mkva_transformation_result__item__result", "typing_Vale.X64.Flags.of_fun", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_Vale.X64.StateLemmas.state_of_S", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "8a704235a621ae08389e71284651c890" ], [ "Vale.Transformers.Transform.lemma_check_if_same_printed_code", 1, 1, 0, [ "@query", "equation_Prims.nat", "equation_Vale.Transformers.Common.equiv_states", "equation_Vale.Transformers.Transform.check_if_same_printed_code", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_require_total", "lemma_Vale.X64.Regs.lemma_equal_intro", "proj_equation_Vale.X64.Decls.Mkva_transformation_result_result", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Vale.X64.Decls.Mkva_transformation_result_result", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs" ], 0, "19cbc5a679d7765f08fb04692614ae02" ], [ "Vale.Transformers.Transform.movbe_elim", 1, 1, 0, [ "@query", "lemma_Vale.Transformers.MovbeElim.movbe_elim_correct" ], 0, "112999b4e7744be2b96f2f16b7690c54" ], [ "Vale.Transformers.Transform.lemma_movbe_elim", 1, 1, 0, [ "@query", "equation_Vale.Transformers.Transform.movbe_elim", "lemma_Vale.Transformers.MovbeElim.movbe_elim_correct" ], 0, "4222391f0d61da74174146751022a4de" ], [ "Vale.Transformers.Transform.mov_mov_elim", 1, 1, 0, [ "@query", "lemma_Vale.Transformers.MovMovElim.mov_mov_elim_correct" ], 0, "9a901b16316b57358c630984565d4ee6" ], [ "Vale.Transformers.Transform.lemma_mov_mov_elim", 1, 1, 0, [ "@query", "equation_Vale.Transformers.Transform.mov_mov_elim", "lemma_Vale.Transformers.MovMovElim.mov_mov_elim_correct" ], 0, "ff7be4e5405b7be519fc082a8f50dbf5" ], [ "Vale.Transformers.Transform.prefetch_elim", 1, 1, 0, [ "@query", "lemma_Vale.Transformers.PrefetchElim.prefetch_elim_correct" ], 0, "a5406fd1f318d83af25880ee74160ffc" ], [ "Vale.Transformers.Transform.lemma_prefetch_elim", 1, 1, 0, [ "@query", "equation_Vale.Transformers.Transform.prefetch_elim", "lemma_Vale.Transformers.PrefetchElim.prefetch_elim_correct" ], 0, "c62eb1e2c222f35feb6576e312de00c5" ] ] ]