Revision 5b2fbf3c4989a9b0587a00578f69f3041df3f957 authored by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC, committed by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC
1 parent d4ca892
Vale.Transformers.PeepHole.fst.hints
[
"��g�)���B0�\u0019�pzx",
[
[
"Vale.Transformers.PeepHole.eval_inss",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_cbd406ad1c569fe5d8e5528c486a860b_0",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Vale.X64.Machine_Semantics_s.ins",
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"354eea8ab193692ef6eb38013f1b2e81"
],
[
"Vale.Transformers.PeepHole.peephole_correct",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Transformers.PeepHole_interpretation_Tm_arrow_66d5817f40439558e3cb160ddb3dfc8d",
"bool_inversion", "bool_typing",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Vale.X64.Machine_Semantics_s.ins",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"kinding_Prims.list@tok", "lemma_FStar.Pervasives.invertOption",
"token_correspondence_Vale.Transformers.PeepHole.__proj__Mkpre_peephole__item__ph",
"typing_Vale.Transformers.PeepHole.__proj__Mkpre_peephole__item__ph"
],
0,
"657cdc432a407666fc47907ed9e8eb86"
],
[
"Vale.Transformers.PeepHole.num_ins_in_code",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_97ef5ff619e486c846fe112d821f649f_0",
"disc_equation_Vale.X64.Machine_s.Block",
"disc_equation_Vale.X64.Machine_s.IfElse",
"disc_equation_Vale.X64.Machine_s.Ins",
"disc_equation_Vale.X64.Machine_s.While", "equation_Prims.nat",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.codes",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"fuel_guarded_inversion_Vale.X64.Machine_s.precode",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifFalse",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifTrue",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Vale.X64.Machine_s.Block",
"subterm_ordering_Vale.X64.Machine_s.IfElse",
"subterm_ordering_Vale.X64.Machine_s.While"
],
0,
"0c8cb3875b45eb19b6fc2e8bd182f3b8"
],
[
"Vale.Transformers.PeepHole.num_ins_in_code",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_69b3af25a4334715774d1242034fc6f2_0",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"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",
"fuel_guarded_inversion_Prims.list",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Prims.Cons"
],
0,
"26469b74019c1530cba1d1c46132cdd9"
],
[
"Vale.Transformers.PeepHole.lemma_num_ins_in_codes_append",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented",
"@query", "binder_x_69b3af25a4334715774d1242034fc6f2_0",
"binder_x_69b3af25a4334715774d1242034fc6f2_1",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"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_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"function_token_typing_Vale.X64.Machine_Semantics_s.code",
"int_inversion", "int_typing", "projection_inverse_BoxInt_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",
"subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.append",
"typing_Vale.Transformers.PeepHole.num_ins_in_codes"
],
0,
"8f9109613e189382f21b305a41078cc1"
],
[
"Vale.Transformers.PeepHole.pull_instructions_from_codes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Vale.X64.Machine_Semantics_s.codes",
"equation_Vale.X64.Machine_Semantics_s.ins",
"function_token_typing_Vale.X64.Machine_Semantics_s.codes",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"kinding_FStar.Pervasives.Native.tuple2@tok",
"kinding_Prims.list@tok", "lemma_FStar.Pervasives.invertOption"
],
0,
"f65f10717e4d66340965d13932a6782a"
],
[
"Vale.Transformers.PeepHole.pull_instructions_from_codes",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.InstructionReorder.num_blocks_in_codes.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.InstructionReorder.num_blocks_in_codes.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"binder_x_69b3af25a4334715774d1242034fc6f2_0",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_1", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Machine_s.Block",
"constructor_distinct_Vale.X64.Machine_s.IfElse",
"constructor_distinct_Vale.X64.Machine_s.Ins",
"constructor_distinct_Vale.X64.Machine_s.While",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Machine_s.Block",
"disc_equation_Vale.X64.Machine_s.IfElse",
"disc_equation_Vale.X64.Machine_s.Ins",
"disc_equation_Vale.X64.Machine_s.While",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Bytes_Code_s.codes_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.codes",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.InstructionReorder.num_blocks_in_codes.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_s.precode",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.X64.Machine_Semantics_s.code",
"function_token_typing_Vale.X64.Machine_Semantics_s.codes",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"int_inversion", "int_typing",
"kinding_FStar.Pervasives.Native.tuple2@tok",
"kinding_Prims.list@tok", "lemma_FStar.Pervasives.invertOption",
"lemma_Vale.Transformers.InstructionReorder.lemma_num_blocks_in_codes_append",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"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.Machine_s.IfElse_ifCond",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifFalse",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifTrue",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ins",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.Ins_ins",
"projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
"projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.While_t_ins",
"projection_inverse_Vale.X64.Machine_s.While_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.While_whileBody",
"projection_inverse_Vale.X64.Machine_s.While_whileCond",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_77a7ca92c1a2fe6770bb4573a450e23b",
"token_correspondence_Vale.Transformers.InstructionReorder.num_blocks_in_codes.fuel_instrumented",
"token_correspondence_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"typing_FStar.List.Tot.Base.append",
"typing_Vale.Transformers.InstructionReorder.num_blocks_in_codes",
"typing_Vale.Transformers.PeepHole.num_ins_in_codes",
"typing_Vale.Transformers.PeepHole.pull_instructions_from_codes",
"typing_tok_Prims.LexTop@tok", "well-founded-ordering-on-nat"
],
0,
"63728e7a03f9d37b81029e19332d40df"
],
[
"Vale.Transformers.PeepHole.wrap_instructions",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_cbd406ad1c569fe5d8e5528c486a860b_0",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Vale.X64.Machine_Semantics_s.ins",
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"b9c9b71c488f594d83fb1dba8728f555"
],
[
"Vale.Transformers.PeepHole.apply_peephole_to_codes",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented",
"@query", "Prims_pretyping_e4836109f73687024ac3edd113084865",
"Vale.Transformers.PeepHole_interpretation_Tm_arrow_66d5817f40439558e3cb160ddb3dfc8d",
"binder_x_5a90b144a8bba2eba7f8b447c7aac61c_0",
"binder_x_69b3af25a4334715774d1242034fc6f2_1", "bool_inversion",
"bool_typing", "constructor_distinct_Prims.Cons",
"data_elim_Vale.Transformers.PeepHole.Mkpre_peephole",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.Transformers.PeepHole.peephole",
"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.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Transformers.PeepHole.pre_peephole",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"int_inversion", "kinding_Prims.list@tok",
"lemma_FStar.Pervasives.invertOption",
"proj_equation_Vale.Transformers.PeepHole.Mkpre_peephole_ph",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"refinement_interpretation_Tm_refine_2cf553ec9082501e522042064a5e3413",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Transformers.PeepHole.__proj__Mkpre_peephole__item__ph",
"token_correspondence_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Transformers.PeepHole.num_ins_in_codes",
"typing_tok_Prims.LexTop@tok", "well-founded-ordering-on-nat"
],
0,
"c55c57950d7c1eaa40033f7f97af6ab2"
],
[
"Vale.Transformers.PeepHole.apply_peephole_to_code",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"@query", "Prims_pretyping_e4836109f73687024ac3edd113084865",
"Vale.Transformers.PeepHole_interpretation_Tm_arrow_66d5817f40439558e3cb160ddb3dfc8d",
"binder_x_5a90b144a8bba2eba7f8b447c7aac61c_0",
"binder_x_97ef5ff619e486c846fe112d821f649f_1", "bool_inversion",
"bool_typing", "constructor_distinct_Vale.X64.Machine_s.IfElse",
"constructor_distinct_Vale.X64.Machine_s.While",
"data_elim_Vale.Transformers.PeepHole.Mkpre_peephole",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Machine_s.Block",
"disc_equation_Vale.X64.Machine_s.IfElse",
"disc_equation_Vale.X64.Machine_s.Ins",
"disc_equation_Vale.X64.Machine_s.While",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.Transformers.PeepHole.peephole",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"fuel_guarded_inversion_Vale.Transformers.PeepHole.pre_peephole",
"fuel_guarded_inversion_Vale.X64.Machine_s.precode",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"int_inversion", "int_typing", "kinding_Prims.list@tok",
"lemma_FStar.Pervasives.invertOption",
"proj_equation_Vale.Transformers.PeepHole.Mkpre_peephole_ph",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifCond",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifFalse",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifTrue",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ins",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.While_t_ins",
"projection_inverse_Vale.X64.Machine_s.While_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.While_whileBody",
"projection_inverse_Vale.X64.Machine_s.While_whileCond",
"refinement_interpretation_Tm_refine_2cf553ec9082501e522042064a5e3413",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Vale.X64.Machine_s.IfElse",
"subterm_ordering_Vale.X64.Machine_s.While",
"token_correspondence_Vale.Transformers.PeepHole.__proj__Mkpre_peephole__item__ph",
"token_correspondence_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"typing_Vale.Transformers.PeepHole.num_ins_in_code",
"typing_tok_Prims.LexTop@tok", "well-founded-ordering-on-nat"
],
0,
"e1966524a353c0af568aabe507148086"
],
[
"Vale.Transformers.PeepHole.lemma_wrap_instructions",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Transformers.PeepHole.eval_inss.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"@query", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.Some",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_with_fuel_Vale.Transformers.PeepHole.eval_inss.fuel_instrumented",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Negation",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_033d09e5e2a2ac9c3463068ecee6a128",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_Vale.Transformers.PeepHole.eval_inss",
"typing_Vale.Transformers.PeepHole.wrap_instructions",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_codes"
],
0,
"a87c4751065f3578f5ca21f673eb5d3c"
],
[
"Vale.Transformers.PeepHole.lemma_wrap_instructions",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Transformers.PeepHole.eval_inss.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.PeepHole.wrap_instructions.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.Transformers.PeepHole.eval_inss.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.PeepHole.wrap_instructions.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"@query", "binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_cbd406ad1c569fe5d8e5528c486a860b_0", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.Machine_s.Ins",
"data_typing_intro_Vale.X64.Machine_s.Ins@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Prims.nat",
"equation_Vale.Transformers.InstructionReorder.equiv_states",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_Vale.Transformers.PeepHole.eval_inss.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.PeepHole.wrap_instructions.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_code_ins",
"int_inversion",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Negation",
"proj_equation_FStar.Pervasives.Native.Some_v",
"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",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"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.Ins_ins",
"projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
"projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
"typing_Vale.Transformers.PeepHole.eval_inss",
"typing_Vale.Transformers.PeepHole.wrap_instructions",
"typing_Vale.X64.Decls.ocmp",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_codes",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_ins"
],
0,
"26c4cfc0fa42e209f49e2b05a78a206b"
],
[
"Vale.Transformers.PeepHole.lemma_pull_instructions_from_codes",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"@query", "b2t_def", "bool_inversion", "bool_typing",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some", "equation_Prims.nat",
"equation_Prims.squash",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"int_inversion",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2b947b7b609ad8d3e71a99527c20b1b1",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Transformers.PeepHole.eval_inss",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_codes"
],
0,
"aa96dc68c8a4c824470616f0000ce06f"
],
[
"Vale.Transformers.PeepHole.lemma_pull_instructions_from_codes",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.InstructionReorder.num_blocks_in_codes.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.PeepHole.eval_inss.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.PeepHole.pull_instructions_from_codes.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_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.InstructionReorder.num_blocks_in_codes.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.PeepHole.eval_inss.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.PeepHole.pull_instructions_from_codes.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865", "b2t_def",
"binder_x_69b3af25a4334715774d1242034fc6f2_0",
"binder_x_8afd38cc1321157644dafce503e55d5a_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_1", "bool_inversion",
"bool_typing", "constructor_distinct_BoxBool",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Machine_s.Block",
"constructor_distinct_Vale.X64.Machine_s.Ins",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Machine_s.Block",
"disc_equation_Vale.X64.Machine_s.Ins",
"equality_tok_Prims.LexTop@tok", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
"equation_Vale.Transformers.InstructionReorder.equiv_states",
"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_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_Vale.Transformers.InstructionReorder.num_blocks_in_codes.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.PeepHole.eval_inss.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.PeepHole.pull_instructions_from_codes.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.X64.Machine_Semantics_s.code",
"function_token_typing_Vale.X64.Machine_Semantics_s.codes",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_code_ins",
"int_inversion", "int_typing",
"kinding_FStar.Pervasives.Native.tuple2@tok",
"kinding_Prims.list@tok",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"kinding_Vale.X64.Machine_s.observation@tok",
"lemma_FStar.Pervasives.invertOption",
"lemma_Vale.Transformers.InstructionReorder.lemma_num_blocks_in_codes_append",
"primitive_Prims.op_Equality", "primitive_Prims.op_Negation",
"proj_equation_FStar.Pervasives.Native.Some_v",
"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",
"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_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"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.Machine_s.Ins_ins",
"projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
"projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"token_correspondence_Vale.Transformers.InstructionReorder.num_blocks_in_codes.fuel_instrumented",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
"typing_FStar.List.Tot.Base.append",
"typing_Vale.Transformers.InstructionReorder.num_blocks_in_codes",
"typing_Vale.Transformers.PeepHole.num_ins_in_codes",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
"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.__proj__Mkmachine_state__item__ms_stack",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_trace",
"typing_Vale.X64.Machine_Semantics_s.ins_obs",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_codes",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_ins",
"typing_tok_Prims.LexTop@tok", "unit_inversion", "unit_typing",
"well-founded-ordering-on-nat"
],
0,
"3104bdd35fb3e65926add27ae18991f2"
],
[
"Vale.Transformers.PeepHole.lemma_apply_peephole_to_codes",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"@query", "b2t_def", "bool_inversion", "bool_typing",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Vale.Transformers.PeepHole.peephole",
"fuel_guarded_inversion_Vale.Transformers.PeepHole.pre_peephole",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"int_inversion",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2cf553ec9082501e522042064a5e3413",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a53c6427828097480ce9cd103407e5a0",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Transformers.PeepHole.apply_peephole_to_codes",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_codes"
],
0,
"7f186d9938b24d48c93d4d23e1e01bec"
],
[
"Vale.Transformers.PeepHole.lemma_apply_peephole_to_codes",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Transformers.PeepHole.apply_peephole_to_codes.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.PeepHole.eval_inss.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.PeepHole.pull_instructions_from_codes.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.PeepHole.wrap_instructions.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.Transformers.PeepHole.apply_peephole_to_codes.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"@query", "Prims_pretyping_e4836109f73687024ac3edd113084865",
"Vale.Transformers.PeepHole_interpretation_Tm_arrow_66d5817f40439558e3cb160ddb3dfc8d",
"b2t_def", "binder_x_5a90b144a8bba2eba7f8b447c7aac61c_0",
"binder_x_69b3af25a4334715774d1242034fc6f2_1",
"binder_x_8afd38cc1321157644dafce503e55d5a_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Machine_s.Block",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Transformers.PeepHole.Mkpre_peephole",
"data_typing_intro_Vale.X64.Machine_s.Block@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Prims.pos",
"equation_Vale.Transformers.InstructionReorder.equiv_states",
"equation_Vale.Transformers.PeepHole.peephole",
"equation_Vale.Transformers.PeepHole.peephole_correct",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Bytes_Code_s.codes_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.codes",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_Vale.Transformers.PeepHole.apply_peephole_to_codes.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.PeepHole.pull_instructions_from_codes.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Transformers.PeepHole.pre_peephole",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Vale.X64.Machine_Semantics_s.codes",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"int_inversion", "kinding_FStar.Pervasives.Native.tuple2@tok",
"kinding_Prims.list@tok",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"l_imp-interp", "lemma_FStar.Pervasives.invertOption",
"primitive_Prims.op_Negation",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.Transformers.PeepHole.Mkpre_peephole_input_hint",
"proj_equation_Vale.Transformers.PeepHole.Mkpre_peephole_ph",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"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.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"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_2cf553ec9082501e522042064a5e3413",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_77a7ca92c1a2fe6770bb4573a450e23b",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Transformers.PeepHole.__proj__Mkpre_peephole__item__ph",
"token_correspondence_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Transformers.PeepHole.__proj__Mkpre_peephole__item__input_hint",
"typing_Vale.Transformers.PeepHole.apply_peephole_to_codes",
"typing_Vale.Transformers.PeepHole.eval_inss",
"typing_Vale.Transformers.PeepHole.num_ins_in_codes",
"typing_Vale.Transformers.PeepHole.pull_instructions_from_codes",
"typing_Vale.Transformers.PeepHole.wrap_instructions",
"typing_Vale.X64.Decls.ocmp",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_codes",
"typing_tok_Prims.LexTop@tok", "unit_inversion", "unit_typing",
"well-founded-ordering-on-nat"
],
0,
"d1c838f28a6b417b8a7c4c621a2113c3"
],
[
"Vale.Transformers.PeepHole.lemma_apply_peephole_to_code",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@query", "b2t_def", "bool_inversion", "bool_typing",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Machine_s.While", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Vale.Transformers.PeepHole.peephole",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"fuel_guarded_inversion_Vale.Transformers.PeepHole.pre_peephole",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"int_inversion",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_00a7f4f660dc1fda2a82818f3e83adae",
"refinement_interpretation_Tm_refine_1f783155915c89403784ec33ec50b830",
"refinement_interpretation_Tm_refine_2cf553ec9082501e522042064a5e3413",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_431b677f65ae9da9d34d0bf514ee8129",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Transformers.PeepHole.apply_peephole_to_code",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code"
],
0,
"4ba26b51d36357628f0cc13aae8de4d4"
],
[
"Vale.Transformers.PeepHole.lemma_apply_peephole_to_code",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Transformers.PeepHole.apply_peephole_to_code.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.PeepHole.apply_peephole_to_codes.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.PeepHole.num_ins_in_code.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.Transformers.PeepHole.apply_peephole_to_code.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Transformers.PeepHole_interpretation_Tm_arrow_66d5817f40439558e3cb160ddb3dfc8d",
"b2t_def", "binder_x_5a90b144a8bba2eba7f8b447c7aac61c_0",
"binder_x_8afd38cc1321157644dafce503e55d5a_3",
"binder_x_97ef5ff619e486c846fe112d821f649f_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Machine_s.Block",
"constructor_distinct_Vale.X64.Machine_s.IfElse",
"constructor_distinct_Vale.X64.Machine_s.Ins",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Transformers.PeepHole.Mkpre_peephole",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_Vale.X64.Machine_s.Block",
"disc_equation_Vale.X64.Machine_s.IfElse",
"disc_equation_Vale.X64.Machine_s.Ins",
"disc_equation_Vale.X64.Machine_s.While",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.nat",
"equation_Vale.Transformers.InstructionReorder.equiv_states",
"equation_Vale.Transformers.PeepHole.peephole",
"equation_Vale.Transformers.PeepHole.peephole_correct",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Bytes_Code_s.codes_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.codes",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_Vale.Transformers.PeepHole.apply_peephole_to_code.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_Vale.Transformers.PeepHole.pre_peephole",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_code_ins",
"int_inversion", "int_typing",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e",
"kinding_Prims.list@tok", "l_imp-interp",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Negation",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.Transformers.PeepHole.Mkpre_peephole_ph",
"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.Machine_Semantics_s.Mkmachine_state_ms_trace",
"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.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"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_Semantics_s.Mkmachine_state_ms_trace",
"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.Machine_s.IfElse_ifCond",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifFalse",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifTrue",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ins",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.Ins_ins",
"projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
"projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
"refinement_interpretation_Tm_refine_2cf553ec9082501e522042064a5e3413",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Vale.X64.Machine_s.IfElse",
"token_correspondence_Vale.Transformers.PeepHole.__proj__Mkpre_peephole__item__ph",
"token_correspondence_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Transformers.PeepHole.apply_peephole_to_code",
"typing_Vale.Transformers.PeepHole.apply_peephole_to_codes",
"typing_Vale.Transformers.PeepHole.num_ins_in_code",
"typing_Vale.Transformers.PeepHole.wrap_instructions",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_codes",
"typing_tok_Prims.LexTop@tok", "unit_inversion", "unit_typing",
"well-founded-ordering-on-nat"
],
0,
"838bb559db06c95fed188adc951e220c"
],
[
"Vale.Transformers.PeepHole.lemma_apply_peephole_to_code",
3,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@query", "b2t_def", "bool_inversion", "bool_typing",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Machine_s.While", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Vale.Transformers.PeepHole.peephole",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"fuel_guarded_inversion_Vale.Transformers.PeepHole.pre_peephole",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"int_inversion",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_00a7f4f660dc1fda2a82818f3e83adae",
"refinement_interpretation_Tm_refine_06fd7fc7166a06d991fdcc638ff3afa4",
"refinement_interpretation_Tm_refine_2cf553ec9082501e522042064a5e3413",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_80689205d8276babb0a20b7ecd1be1c2",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Transformers.PeepHole.apply_peephole_to_code",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code"
],
0,
"e58b167f4606a23f9bf848d86d96a4d8"
],
[
"Vale.Transformers.PeepHole.lemma_apply_peephole_to_code",
4,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Transformers.PeepHole.apply_peephole_to_code.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.PeepHole.apply_peephole_to_code.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Vale.X64.Machine_s_pretyping_8a3a692892c8a0ea1c9a86a6a3b7d69f",
"binder_x_5a90b144a8bba2eba7f8b447c7aac61c_0",
"binder_x_79caa643a1f84363a39118336c0fa141_1",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_Vale.X64.Machine_s.While",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"data_elim_Vale.X64.Machine_s.While",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Machine_s.While",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.Transformers.InstructionReorder.equiv_states",
"equation_Vale.Transformers.PeepHole.peephole",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_Vale.Transformers.PeepHole.apply_peephole_to_code.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.PeepHole.num_ins_in_code.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_Vale.Transformers.PeepHole.pre_peephole",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"fuel_guarded_inversion_Vale.X64.Machine_s.precode",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_Negation",
"proj_equation_FStar.Pervasives.Native.Some_v",
"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",
"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.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Machine_s.While_t_ins",
"projection_inverse_Vale.X64.Machine_s.While_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.While_whileBody",
"projection_inverse_Vale.X64.Machine_s.While_whileCond",
"refinement_interpretation_Tm_refine_00a7f4f660dc1fda2a82818f3e83adae",
"refinement_interpretation_Tm_refine_2cf553ec9082501e522042064a5e3413",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Vale.X64.Machine_s.While",
"typing_Vale.Transformers.PeepHole.apply_peephole_to_code",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_while",
"typing_tok_Prims.LexTop@tok", "unit_inversion", "unit_typing",
"well-founded-ordering-on-nat"
],
0,
"7c87538ff6a4041c155b2653913a0c80"
],
[
"Vale.Transformers.PeepHole.lemma_peephole_transform",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Lemmas.code_modifies_ghost.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_BoxBool",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Tm_unit",
"disc_equation_FStar.Pervasives.Native.Some",
"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.PeepHole.peephole_transform",
"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.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.regs_fun", "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",
"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_s.reg@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"lemma_Vale.X64.Stack_Sems.lemma_stack_from_to",
"primitive_Prims.op_Negation",
"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",
"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.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.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
"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.PeepHole.peephole_transform",
"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.Regs.of_fun", "typing_Vale.X64.Regs.to_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"
],
0,
"e4503333afbacd6ad75d0dde5095bc7b"
],
[
"Vale.Transformers.PeepHole.coerce_to_normal",
1,
1,
0,
[ "@query" ],
0,
"7338f61b47d5476f48484c263527eba8"
],
[
"Vale.Transformers.PeepHole.lemma_update_to_valid_destination_keeps_it_as_valid_src",
1,
0,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
"FStar.Map_interpretation_Tm_arrow_b19283e90b47034162373413c6a19933",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
"Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"bool_inversion", "bool_typing", "constructor_distinct_Tm_unit",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_Vale.X64.Machine_Semantics_s.Machine_stack",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"data_elim_Vale.X64.Machine_s.OMem",
"data_elim_Vale.X64.Machine_s.OReg",
"data_elim_Vale.X64.Machine_s.OStack",
"data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
"data_typing_intro_Vale.Def.Words_s.Mktwo@tok",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equation_FStar.FunctionalExtensionality.feq", "equation_Prims.eq2",
"equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
"equation_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Arch.MachineHeap_s.update_heap64_def",
"equation_Vale.Arch.MachineHeap_s.valid_addr",
"equation_Vale.Def.Words.Two_s.nat_to_two",
"equation_Vale.Def.Words.Two_s.two_to_nat",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_Semantics_s.eval_maddr",
"equation_Vale.X64.Machine_Semantics_s.eval_operand",
"equation_Vale.X64.Machine_Semantics_s.update_mem_and_taint",
"equation_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags__",
"equation_Vale.X64.Machine_Semantics_s.update_reg_",
"equation_Vale.X64.Machine_Semantics_s.update_reg_64_",
"equation_Vale.X64.Machine_Semantics_s.update_stack_and_taint",
"equation_Vale.X64.Machine_Semantics_s.valid_dst_operand64",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.tmaddr",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_stack",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand",
"function_token_typing_FStar.Map.upd",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val64",
"function_token_typing_Vale.Arch.MachineHeap_s.update_heap64",
"function_token_typing_Vale.Arch.MachineHeap_s.valid_addr64",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"function_token_typing_Vale.X64.Machine_s.t_reg",
"function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl",
"int_inversion", "int_typing",
"interpretation_Tm_abs_1eab5700ef81b3c102d114cb086eb6dc",
"interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"kinding_Vale.X64.Machine_s.reg@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_union",
"lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8",
"lemma_Vale.X64.Machine_Semantics_s.lemma_is_machine_heap_update64",
"lemma_Vale.X64.Memory_Sems.lemma_heap_get_heap",
"lemma_Vale.X64.Memory_Sems.lemma_heap_taint",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"proj_equation_Vale.Def.Words_s.Mktwo_hi",
"proj_equation_Vale.Def.Words_s.Mktwo_lo",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"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",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mktwo_hi",
"projection_inverse_Vale.Def.Words_s.Mktwo_lo",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_stack_mem",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"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",
"refinement_interpretation_Tm_refine_0030c490ddf8a8ae33d539152b909139",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6dcab90f61547a5eea7e0f9da709087b",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c",
"refinement_interpretation_Tm_refine_a51eae56a5c39d95827d04b5f0544d43",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap64_def",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"token_correspondence_Vale.X64.Machine_s.t_reg",
"typing_FStar.Map.domain", "typing_FStar.Map.sel",
"typing_FStar.Map.upd", "typing_FStar.Set.singleton",
"typing_FStar.Set.union", "typing_Prims.pow2",
"typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"typing_Vale.Arch.Heap.heap_get", "typing_Vale.Arch.Heap.heap_taint",
"typing_Vale.Arch.Heap.heap_upd",
"typing_Vale.Arch.MachineHeap_s.update_heap64",
"typing_Vale.Arch.MachineHeap_s.valid_addr",
"typing_Vale.Def.Words.Four_s.four_to_nat",
"typing_Vale.Def.Words.Four_s.nat_to_four",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
"typing_Vale.Def.Words_s.__proj__Mktwo__item__hi",
"typing_Vale.Def.Words_s.int_to_natN",
"typing_Vale.Def.Words_s.natN",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint",
"typing_Vale.X64.Machine_Semantics_s.eval_maddr",
"typing_Vale.X64.Machine_Semantics_s.eval_operand",
"typing_Vale.X64.Machine_Semantics_s.match_n",
"typing_Vale.X64.Machine_Semantics_s.update_n",
"typing_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags__",
"typing_Vale.X64.Machine_Semantics_s.valid_dst_operand64",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint"
],
0,
"d4edbe7e1b3f733a5fdcfa9ca40d7e38"
],
[
"Vale.Transformers.PeepHole.lemma_double_update_reg",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
"Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
"disc_equation_Vale.X64.Machine_s.OReg", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
"equation_FStar.FunctionalExtensionality.feq", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.Arch.HeapTypes_s.memTaint_t",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Transformers.InstructionReorder.equiv_states",
"equation_Vale.Transformers.InstructionReorder.equiv_states_ext",
"equation_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags__",
"equation_Vale.X64.Machine_Semantics_s.update_reg_",
"equation_Vale.X64.Machine_Semantics_s.update_reg_64_",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.X64.Machine_s.t_reg",
"function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
"interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"kinding_Vale.Arch.HeapTypes_s.taint@tok",
"kinding_Vale.X64.Machine_s.reg@tok", "l_and-interp",
"lemma_FStar.FunctionalExtensionality.extensionality",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_FStar.Map.lemma_equal_elim",
"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.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_BoxBool_proj_0",
"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_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_Vale.X64.Machine_s.OReg_r",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c2c488db3214c38826155caf10d30036",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"token_correspondence_Vale.X64.Machine_s.t_reg",
"typing_FStar.FunctionalExtensionality.on_domain",
"typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"typing_Vale.X64.Machine_Semantics_s.__proj__Machine_stack__item__stack_mem",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stack",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint",
"typing_tok_Vale.Arch.HeapTypes_s.Public@tok"
],
0,
"6b2a1b202a2302e7ea1a5b881759e612"
]
]
]
Computing file changes ...
