[
"(\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"
]
]
]