[ "g)B0\u0019pzx", [ [ "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, "5ff09a493b48ea4089ab9382515adbb7" ], [ "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, "51c06c3be9265b52620ab5fef4c18b3d" ], [ "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, "a1559718789c4fc456d8113964b3d5be" ], [ "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, "eb5938a77a2910411773b968ac2f6f5c" ], [ "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, "101f8f4bbb2fa47239de5a27cc1307f7" ], [ "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, "3990f049b917a88affeadb72f1e449df" ], [ "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", "binder_x_69b3af25a4334715774d1242034fc6f2_0", "binder_x_f26957a7e62b271a8736230b1e9c83c1_1", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Prims.Nil", "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", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "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_hd", "projection_inverse_Prims.Cons_tl", "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.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", "well-founded-ordering-on-nat" ], 0, "9804584b33b69ac6e95ffde23703ad31" ], [ "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, "fab107373ffafcecd805a803f1087a16" ], [ "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_ae567c2fb75be05905677af440075565", "Vale.Transformers.PeepHole_interpretation_Tm_arrow_66d5817f40439558e3cb160ddb3dfc8d", "binder_x_5a90b144a8bba2eba7f8b447c7aac61c_0", "binder_x_69b3af25a4334715774d1242034fc6f2_1", "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", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "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_Prims.__cache_version_number__", "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", "proj_equation_Vale.Transformers.PeepHole.Mkpre_peephole_ph", "projection_inverse_BoxBool_proj_0", "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", "token_correspondence_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented", "typing_Vale.Transformers.PeepHole.num_ins_in_codes", "well-founded-ordering-on-nat" ], 0, "4a99cebd76d22a4f2d40f337ad4ebda2" ], [ "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", "Vale.Transformers.PeepHole_interpretation_Tm_arrow_66d5817f40439558e3cb160ddb3dfc8d", "binder_x_5a90b144a8bba2eba7f8b447c7aac61c_0", "binder_x_97ef5ff619e486c846fe112d821f649f_1", "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_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_Prims.op_Equals_Equals_Equals", "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_BoxBool_proj_0", "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", "well-founded-ordering-on-nat" ], 0, "d40f91a2c854868b10579954146e2b02" ], [ "Vale.Transformers.PeepHole.lemma_wrap_instructions", 1, 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.None", "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", "interpretation_Tm_abs_431565cf08dbebf07925447f42184424", "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", "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_codes", "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins" ], 0, "70780b278743cf79ed588ffb1b3fd195" ], [ "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", "primitive_Prims.op_Negation", "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.X64.Machine_Semantics_s.machine_eval_codes" ], 0, "e75bd11b607353308c63881c4663c9a4" ], [ "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.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", "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", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "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.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", "interpretation_Tm_abs_431565cf08dbebf07925447f42184424", "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_codes.fuel_instrumented", "typing_FStar.List.Tot.Base.append", "typing_Vale.Transformers.InstructionReorder.num_blocks_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_code", "typing_Vale.X64.Machine_Semantics_s.machine_eval_codes", "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "8918cdb821e68b783b93b84333fed27e" ], [ "Vale.Transformers.PeepHole.lemma_apply_peephole_to_codes", 1, 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.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", "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", "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_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state", "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", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "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.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_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_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", "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", "token_correspondence_Vale.Transformers.PeepHole.num_ins_in_codes.fuel_instrumented", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "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.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", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "f89922f1450de83c97c67651472f05d4" ], [ "Vale.Transformers.PeepHole.lemma_apply_peephole_to_code", 1, 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_f537159ed795b314b4e58c260361ae86", "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", "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", "constructor_distinct_Vale.X64.Machine_s.While", "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_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_FStar.Pervasives.Native.snd", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "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_431565cf08dbebf07925447f42184424", "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", "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", "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.fuel_instrumented", "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", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "b3de1bd31442bb71ece4e901b770bab3" ], [ "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.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_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", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "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", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "lemma_FStar.Pervasives.invertOption", "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_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_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", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "92ce0dff109a74c3e2b5dbec252e9912" ], [ "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, "c94aef0fb83f19040e0b063f8a3e332e" ], [ "Vale.Transformers.PeepHole.coerce_to_normal", 1, 1, 0, [ "@query" ], 0, "32c6cdc19dfeaaac5d9fa5e0be7780b9" ], [ "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, "bfca515bbf05aed4b05df96ac189a609" ], [ "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, "ad1e3021e93df28537d17434f2bb3908" ], [ "Vale.Transformers.PeepHole.lemma_double_update_reg", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "bc7a2dcafa4b9d2ec1ec0f676bba6d8a" ], [ "Vale.Transformers.PeepHole.lemma_double_update_reg", 3, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "f84ac63fddd3e3e2def0072f04f236cd" ] ] ]