[ "ăD\f8tQ>", [ [ "Vale.X64.Lemmas.code_modifies_ghost", 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_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "fuel_guarded_inversion_Vale.X64.Machine_s.precode", "subterm_ordering_Vale.X64.Machine_s.Block", "subterm_ordering_Vale.X64.Machine_s.IfElse", "subterm_ordering_Vale.X64.Machine_s.While" ], 0, "12b0ff4414b4218953172811c64455e9" ], [ "Vale.X64.Lemmas.code_modifies_ghost", 2, 1, 1, [ "@MaxIFuel_assumption", "@query", "binder_x_69b3af25a4334715774d1242034fc6f2_0", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "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", "subterm_ordering_Prims.Cons" ], 0, "400ec28da802c064e4ce04bfe504caca" ], [ "Vale.X64.Lemmas.eval_ins", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@query", "Vale.X64.State_pretyping_eb96f2119e19317ec6e3b596d5a46609", "constructor_distinct_FStar.Pervasives.Native.Some", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Vale.X64.Machine_s.Ins", "equation_Prims.nat", "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.machine_eval_code_ins_def", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_Vale.X64.StateLemmas.state_to_S", "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_code_ins", "interpretation_Tm_abs_431565cf08dbebf07925447f42184424", "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_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", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "3646198ee7652ea6dc6a897063d466cf" ], [ "Vale.X64.Lemmas.lemma_eq_instr_apply_eval_args", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented", "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented", "@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented", "@query", "binder_x_38287ca2033f50691479ff837e9de132_2", "binder_x_5b8a55910a662c783b1ed3212549410e_1", "binder_x_87dc12526be5fec62ede2129096a7dae_3", "binder_x_8afd38cc1321157644dafce503e55d5a_4", "binder_x_8afd38cc1321157644dafce503e55d5a_5", "binder_x_9480187c8e85713ad9eae72e33c57410_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_Tm_unit", "constructor_distinct_Vale.X64.Instruction_s.IOpEx", "constructor_distinct_Vale.X64.Instruction_s.IOpIm", "data_elim_Vale.X64.Instruction_s.IOp64One", "data_elim_Vale.X64.Instruction_s.IOpXmmOne", "data_elim_Vale.X64.Machine_Semantics_s.Machine_stack", "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "disc_equation_Vale.X64.Instruction_s.IOpEx", "disc_equation_Vale.X64.Instruction_s.IOpIm", "eq2-interp", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.squash", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Instruction_s.instr_operand_t", "equation_Vale.X64.Instruction_s.instr_out", "equation_Vale.X64.Instruction_s.instr_val_t", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Machine_Semantics_s.bind_option", "equation_Vale.X64.Machine_Semantics_s.eval_maddr", "equation_Vale.X64.Machine_Semantics_s.eval_mov128_op", "equation_Vale.X64.Machine_Semantics_s.eval_operand", "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit", "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_implicit", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "equation_Vale.X64.Machine_s.operand128", "equation_Vale.X64.Machine_s.operand64", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented", "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented", "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand", "fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit", "fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_stack", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "function_token_typing_Vale.X64.StateLemmas.same_heap_types", "int_inversion", "int_typing", "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap", "projection_inverse_BoxBool_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.Instruction_s.IOpEx__0", "projection_inverse_Vale.X64.Instruction_s.IOpIm__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_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_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "subterm_ordering_Prims.Cons", "typing_FStar.Pervasives.Native.fst", "typing_Vale.Arch.Heap.heap_get", "typing_Vale.Arch.MachineHeap_s.valid_addr128", "typing_Vale.Arch.MachineHeap_s.valid_addr64", "typing_Vale.X64.Instruction_s.instr_operand_t", "typing_Vale.X64.Instruction_s.instr_operands_t_args", "typing_Vale.X64.Instruction_s.instr_val_t", "typing_Vale.X64.Lemmas.core_state", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stack", "typing_Vale.X64.Machine_Semantics_s.eval_mov128_op", "typing_Vale.X64.Machine_Semantics_s.eval_operand", "typing_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit", "typing_Vale.X64.Machine_Semantics_s.instr_eval_operand_implicit", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "unit_inversion", "unit_typing" ], 0, "82097b740bf918a6772be0f04fa28886" ], [ "Vale.X64.Lemmas.lemma_eq_instr_apply_eval_inouts", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented", "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented", "@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented", "@query", "FStar.Pervasives.Native_pretyping_b53dbd183c526bc5d0f20d7b966ae125", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6", "binder_x_093c08543626f27b65f30658d7fc39bc_4", "binder_x_5b8a55910a662c783b1ed3212549410e_2", "binder_x_8afd38cc1321157644dafce503e55d5a_5", "binder_x_8afd38cc1321157644dafce503e55d5a_6", "binder_x_9480187c8e85713ad9eae72e33c57410_0", "binder_x_9480187c8e85713ad9eae72e33c57410_1", "binder_x_f5c27ac55c99c39df8fbe4adb077bc73_3", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_FStar.Pervasives.Native.option", "constructor_distinct_Prims.Nil", "constructor_distinct_Prims.unit", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.X64.Instruction_s.IOpEx", "constructor_distinct_Vale.X64.Instruction_s.IOpIm", "constructor_distinct_Vale.X64.Instruction_s.InOut", "constructor_distinct_Vale.X64.Instruction_s.Out", "data_elim_Prims.Cons", "data_elim_Vale.X64.Instruction_s.IOp64One", "data_elim_Vale.X64.Instruction_s.IOpXmmOne", "data_elim_Vale.X64.Machine_Semantics_s.Machine_stack", "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state", "data_typing_intro_Vale.X64.Instruction_s.Out@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.Instruction_s.IOpEx", "disc_equation_Vale.X64.Instruction_s.IOpIm", "disc_equation_Vale.X64.Instruction_s.InOut", "disc_equation_Vale.X64.Instruction_s.Out", "eq2-interp", "equality_tok_Vale.X64.Instruction_s.InOut@tok", "equality_tok_Vale.X64.Instruction_s.Out@tok", "equation_FStar.Pervasives.Native.fst", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.squash", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Instruction_s.instr_operand_t", "equation_Vale.X64.Instruction_s.instr_out", "equation_Vale.X64.Instruction_s.instr_val_t", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Machine_Semantics_s.bind_option", "equation_Vale.X64.Machine_Semantics_s.eval_maddr", "equation_Vale.X64.Machine_Semantics_s.eval_mov128_op", "equation_Vale.X64.Machine_Semantics_s.eval_operand", "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit", "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_implicit", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "equation_Vale.X64.Machine_s.operand128", "equation_Vale.X64.Machine_s.operand64", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented", "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented", "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand", "fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit", "fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit", "fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_inout", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_stack", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "function_token_typing_Vale.X64.StateLemmas.same_heap_types", "int_inversion", "int_typing", "interpretation_Tm_abs_c7148522b68166228dab1bc5afbb5dd9", "kinding_Vale.X64.Instruction_s.instr_operand@tok", "kinding_Vale.X64.Instruction_s.instr_operand_inout@tok", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_Prims.Cons_hd", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap", "projection_inverse_BoxBool_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_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "projection_inverse_Vale.X64.Instruction_s.IOpEx__0", "projection_inverse_Vale.X64.Instruction_s.IOpIm__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_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_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented", "typing_FStar.Pervasives.Native.__proj__Mktuple2__item___1", "typing_FStar.Pervasives.Native.fst", "typing_Vale.Arch.Heap.heap_get", "typing_Vale.Arch.MachineHeap_s.valid_addr128", "typing_Vale.Arch.MachineHeap_s.valid_addr64", "typing_Vale.X64.Instruction_s.instr_operand_t", "typing_Vale.X64.Instruction_s.instr_operands_t", "typing_Vale.X64.Instruction_s.instr_val_t", "typing_Vale.X64.Lemmas.core_state", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stack", "typing_Vale.X64.Machine_Semantics_s.eval_mov128_op", "typing_Vale.X64.Machine_Semantics_s.eval_operand", "typing_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit", "typing_Vale.X64.Machine_Semantics_s.instr_eval_operand_implicit", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "unit_inversion", "unit_typing" ], 0, "a6d0fcf9228f15bac9dc31228aa48904" ], [ "Vale.X64.Lemmas.lemma_eq_instr_write_outputs", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented", "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented", "@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "FStar.Pervasives.Native_pretyping_4894c30cf477acf9a27e7a844279eb08", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "Vale.X64.Flags_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100", "Vale.X64.Flags_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144", "Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6", "Vale.X64.Instruction_s_pretyping_dfa9c2e22fe11011bf212d55e07ed9db", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3", "binder_x_44c6303725e907c3759d9004241619c7_2", "binder_x_5b8a55910a662c783b1ed3212549410e_1", "binder_x_67735fae8b4e79dde4eed727828e245d_3", "binder_x_8afd38cc1321157644dafce503e55d5a_4", "binder_x_8afd38cc1321157644dafce503e55d5a_5", "binder_x_8afd38cc1321157644dafce503e55d5a_6", "binder_x_8afd38cc1321157644dafce503e55d5a_7", "binder_x_9480187c8e85713ad9eae72e33c57410_0", "bool_inversion", "bool_typing", "constructor_distinct_BoxBool", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.X64.Instruction_s.IOpEx", "data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_Vale.X64.Instruction_s.IOp64One", "data_elim_Vale.X64.Instruction_s.IOpIm", "data_elim_Vale.X64.Instruction_s.IOpXmmOne", "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.OStack", "data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok", "data_typing_intro_Vale.X64.Instruction_s.IOpFlagsCf@tok", "data_typing_intro_Vale.X64.Instruction_s.Out@tok", "data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "disc_equation_Vale.X64.Instruction_s.IOpEx", "disc_equation_Vale.X64.Instruction_s.IOpIm", "eq2-interp", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.is_restricted", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Instruction_s.instr_operand_t", "equation_Vale.X64.Instruction_s.instr_out", "equation_Vale.X64.Instruction_s.instr_val_t", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Machine_Semantics_s.eval_maddr", "equation_Vale.X64.Machine_Semantics_s.flags_t", "equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit", "equation_Vale.X64.Machine_Semantics_s.instr_write_output_implicit", "equation_Vale.X64.Machine_Semantics_s.regs_t", "equation_Vale.X64.Machine_Semantics_s.state_or_fail", "equation_Vale.X64.Machine_Semantics_s.update_cf_", "equation_Vale.X64.Machine_Semantics_s.update_mem128_and_taint", "equation_Vale.X64.Machine_Semantics_s.update_mem_and_taint", "equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__", "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_reg_xmm_", "equation_Vale.X64.Machine_Semantics_s.update_stack128_and_taint", "equation_Vale.X64.Machine_Semantics_s.update_stack_and_taint", "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128", "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand64", "equation_Vale.X64.Machine_s.flag", "equation_Vale.X64.Machine_s.operand128", "equation_Vale.X64.Machine_s.operand64", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Machine_s.tmaddr", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_Vale.X64.StateLemmas.machine_state_equal", "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented", "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented", "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand", "fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit", "fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit", "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.maddr", "fuel_guarded_inversion_Vale.X64.Machine_s.operand", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "function_token_typing_Prims.unit", "function_token_typing_Vale.X64.Instruction_s.instr_out", "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.StateLemmas.same_heap_types", "int_inversion", "int_typing", "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749", "interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366", "inversion-interp", "kinding_Vale.X64.Machine_s.reg@tok", "lemma_FStar.FunctionalExtensionality.extensionality", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_Vale.X64.Machine_Semantics_s.lemma_is_machine_heap_update128", "lemma_Vale.X64.Machine_Semantics_s.lemma_is_machine_heap_update64", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "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_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "projection_inverse_Vale.X64.Instruction_s.IOpEx__0", "projection_inverse_Vale.X64.Instruction_s.IOpIm__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", "refinement_interpretation_Tm_refine_0030c490ddf8a8ae33d539152b909139", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented", "token_correspondence_Vale.X64.Machine_s.t_reg", "typing_FStar.FunctionalExtensionality.on_domain", "typing_FStar.Pervasives.Native.fst", "typing_FStar.Pervasives.Native.snd", "typing_Prims.uu___is_Nil", "typing_Tm_abs_1abb9d76d736bf6d3482913e489aefa3", "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749", "typing_Tm_abs_f086d77986b470aab4bfebc171e6c366", "typing_Vale.Arch.Heap.heap_get", "typing_Vale.Arch.Heap.heap_taint", "typing_Vale.Arch.MachineHeap_s.update_heap128", "typing_Vale.Arch.MachineHeap_s.update_heap64", "typing_Vale.Arch.MachineHeap_s.valid_addr128", "typing_Vale.Arch.MachineHeap_s.valid_addr64", "typing_Vale.X64.Instruction_s.instr_operand_t", "typing_Vale.X64.Instruction_s.instr_operands_t", "typing_Vale.X64.Instruction_s.instr_val_t", "typing_Vale.X64.Lemmas.core_state", "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.eval_maddr", "typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit", "typing_Vale.X64.Machine_Semantics_s.instr_write_output_implicit", "typing_Vale.X64.Machine_Semantics_s.update_n", "typing_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__", "typing_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags__", "typing_Vale.X64.Machine_Semantics_s.valid_dst_operand128", "typing_Vale.X64.Machine_Semantics_s.valid_dst_operand64", "unit_inversion", "unit_typing" ], 0, "59b4ef3359ec8ea4190720252f57b1b7" ], [ "Vale.X64.Lemmas.eval_ins_eq_instr", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented", "@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_798f93baee047c0793beddf8ae4ab551", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_b72d599fc3c0eb1fc86c5d80a692be46", "Vale.X64.Machine_Semantics_s_pre_typing_Tm_arrow_2eb22b38a6da10fb966327d892d8131d", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Prims.unit", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_Vale.X64.Bytes_Code_s.Instr", "disc_equation_Vale.X64.Instruction_s.HavocFlags", "disc_equation_Vale.X64.Instruction_s.PreserveFlags", "equation_FStar.Option.mapTot", "equation_FStar.Pervasives.Native.snd", "equation_Vale.X64.Instruction_s.instr_eval_t", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Machine_Semantics_s.apply_option", "equation_Vale.X64.Machine_Semantics_s.eval_instr", "equation_Vale.X64.Machine_Semantics_s.instr_apply_eval", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st", "equation_Vale.X64.Machine_Semantics_s.st", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented", "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_Vale.X64.Instruction_s.flag_havoc", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659", "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821", "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e", "interpretation_Tm_abs_d7e539669515a49f97544a169303f779", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_args", "proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_outs", "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.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.Bytes_Code_s.Instr_a", "projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation", "projection_inverse_Vale.X64.Bytes_Code_s.Instr_i", "projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs", "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args", "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_havoc_flags", "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_i", "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs", "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", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_ins_st", "typing_FStar.Pervasives.Native.uu___is_Some", "typing_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e", "typing_Vale.X64.Instruction_s.instr_eval", "typing_Vale.X64.Instruction_s.instr_ret_t", "typing_Vale.X64.Machine_Semantics_s.apply_option", "typing_Vale.X64.Machine_Semantics_s.eval_instr", "typing_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts", "unit_typing" ], 0, "06a42935616f8c94bf3059932457793a" ], [ "Vale.X64.Lemmas.eval_code_eq_instr", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@query", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Vale.X64.Machine_s.Ins", "data_typing_intro_Vale.X64.Machine_s.Ins@tok", "disc_equation_Vale.X64.Bytes_Code_s.Instr", "equation_FStar.Pervasives.Native.snd", "equation_Prims.nat", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "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.machine_eval_ins_st", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "function_token_typing_Vale.X64.Machine_Semantics_s.ins", "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_code_ins", "int_inversion", "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821", "interpretation_Tm_abs_431565cf08dbebf07925447f42184424", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "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.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.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", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_ins_st" ], 0, "8a8e297f3d1f2a4b8f7b58b25aa00547" ], [ "Vale.X64.Lemmas.eval_code_eq_ins", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "Vale.X64.Flags_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_2eb22b38a6da10fb966327d892d8131d", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_aa589b9ef510f53ad802095d5dd3ddab", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_eabe638ef4af4b0ec65b4cf7bbb2dc65", "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_FStar.Pervasives.Native.Some", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.X64.Machine_s.Ins", "constructor_distinct_Vale.X64.Machine_s.MConst", "constructor_distinct_Vale.X64.Machine_s.MReg", "constructor_distinct_Vale.X64.Machine_s.OStack", "data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_FStar.Pervasives.Native.Some", "data_elim_Vale.X64.Bytes_Code_s.Pop", "data_elim_Vale.X64.Bytes_Code_s.Push", "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.OStack", "data_typing_intro_Prims.Nil@tok", "data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok", "data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok", "data_typing_intro_Vale.X64.Machine_s.Ins@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Vale.X64.Bytes_Code_s.Alloc", "disc_equation_Vale.X64.Bytes_Code_s.Dealloc", "disc_equation_Vale.X64.Bytes_Code_s.Instr", "disc_equation_Vale.X64.Bytes_Code_s.Pop", "disc_equation_Vale.X64.Bytes_Code_s.Push", "eq2-interp", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.is_restricted", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.eval_maddr", "equation_Vale.X64.Machine_Semantics_s.eval_operand", "equation_Vale.X64.Machine_Semantics_s.flags_t", "equation_Vale.X64.Machine_Semantics_s.free_stack", "equation_Vale.X64.Machine_Semantics_s.free_stack_", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ins_obs", "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.machine_eval_ins_st", "equation_Vale.X64.Machine_Semantics_s.operand_obs", "equation_Vale.X64.Machine_Semantics_s.regs_t", "equation_Vale.X64.Machine_Semantics_s.st", "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_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_rsp_", "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.flag", "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.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Machine_s.t_reg_to_int", "equation_Vale.X64.Machine_s.tmaddr", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_Vale.X64.StateLemmas.machine_state_equal", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.X64.Bytes_Code_s.instruction_t", "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", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "function_token_typing_Vale.X64.Machine_Semantics_s.free_stack", "function_token_typing_Vale.X64.Machine_Semantics_s.ins", "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_code_ins", "function_token_typing_Vale.X64.Machine_s.t_reg", "function_token_typing_Vale.X64.StateLemmas.same_heap_types", "int_inversion", "int_typing", "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821", "interpretation_Tm_abs_431565cf08dbebf07925447f42184424", "interpretation_Tm_abs_4671ae2ba06d701a8ddfd527a574fa44", "interpretation_Tm_abs_4d5af7e9216f96602071ec3a112fb4da", "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749", "interpretation_Tm_abs_b3799bd9160660915dad8cdf26d6109c", "interpretation_Tm_abs_b91bb16d538d3c642f9667f542c8ccae", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_ec68e3b9ffa3f3f4eb4169d3e7e95c77", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "inversion-interp", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok", "kinding_Vale.X64.Machine_s.observation@tok", "kinding_Vale.X64.Machine_s.reg@tok", "lemma_FStar.FunctionalExtensionality.extensionality", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_Vale.X64.Machine_Semantics_s.lemma_is_machine_heap_update64", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp", "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", "proj_equation_Vale.X64.Machine_s.Reg_rf", "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.Machine_Semantics_s.Machine_stack_initial_rsp", "projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_stack_mem", "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.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.MConst_n", "projection_inverse_Vale.X64.Machine_s.MReg_offset", "projection_inverse_Vale.X64.Machine_s.MReg_r", "projection_inverse_Vale.X64.Machine_s.OStack_m", "projection_inverse_Vale.X64.Machine_s.OStack_tc", "projection_inverse_Vale.X64.Machine_s.OStack_tr", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "refinement_interpretation_Tm_refine_0030c490ddf8a8ae33d539152b909139", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_a51eae56a5c39d95827d04b5f0544d43", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64", "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "token_correspondence_Vale.X64.Machine_Semantics_s.free_stack", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_ins_st", "token_correspondence_Vale.X64.Machine_s.t_reg", "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749", "typing_Tm_abs_f086d77986b470aab4bfebc171e6c366", "typing_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "typing_Vale.Arch.Heap.heap_get", "typing_Vale.Arch.Heap.heap_taint", "typing_Vale.Arch.MachineHeap_s.get_heap_val64", "typing_Vale.Arch.MachineHeap_s.update_heap64", "typing_Vale.Arch.MachineHeap_s.valid_addr64", "typing_Vale.X64.Lemmas.core_state", "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.eval_maddr", "typing_Vale.X64.Machine_Semantics_s.ins_obs", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "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.update_rsp_", "typing_Vale.X64.Machine_Semantics_s.valid_dst_operand64", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint" ], 0, "03f369592dd4af1e7076f1aee88fb5d8" ], [ "Vale.X64.Lemmas.eval_ocmp_eq_core", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "bool_typing", "constructor_distinct_Tm_unit", "data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_Vale.X64.Bytes_Code_s.OEq", "data_elim_Vale.X64.Bytes_Code_s.OGe", "data_elim_Vale.X64.Bytes_Code_s.OGt", "data_elim_Vale.X64.Bytes_Code_s.OLe", "data_elim_Vale.X64.Bytes_Code_s.OLt", "data_elim_Vale.X64.Bytes_Code_s.ONe", "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state", "data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "eq2-interp", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapLemmas.heap_ignore_ghost", "equation_Vale.Arch.HeapLemmas.heap_ignore_ghost_machine", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Machine_Semantics_s.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_operand", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "equation_Vale.X64.Machine_s.operand64", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.StateLemmas.machine_state_eq", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp", "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_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "function_token_typing_Vale.X64.Machine_Semantics_s.eval_ocmp_opaque", "function_token_typing_Vale.X64.Machine_Semantics_s.valid_ocmp_opaque", "function_token_typing_Vale.X64.StateLemmas.same_heap_types", "int_inversion", "interpretation_Tm_abs_275a4a20fec2a36f25eb34b853a79209", "interpretation_Tm_abs_b085815e1140e9a069ea4cab83d07665", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "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", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.X64.Lemmas.core_state", "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_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.eval_operand", "typing_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "typing_Vale.X64.Machine_Semantics_s.valid_ocmp_opaque", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint" ], 0, "2fa68e17bb999a93e99efa7d7d21d1dd" ], [ "Vale.X64.Lemmas.eval_code_eq_core", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_while.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", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "binder_x_8afd38cc1321157644dafce503e55d5a_3", "binder_x_97ef5ff619e486c846fe112d821f649f_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "binder_x_f537159ed795b314b4e58c260361ae86_0", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.Some", "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_Vale.X64.Machine_Semantics_s.Mkmachine_state", "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", "eq2-interp", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.squash", "equation_Vale.Arch.HeapLemmas.heap_ignore_ghost", "equation_Vale.Arch.HeapLemmas.heap_ignore_ghost_machine", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "fuel_guarded_inversion_Vale.X64.Machine_s.precode", "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_code_ins", "function_token_typing_Vale.X64.StateLemmas.same_heap_types", "int_inversion", "interpretation_Tm_abs_431565cf08dbebf07925447f42184424", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "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.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.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "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.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_2de20c066034c13bf76e9c0b94f4806c", "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", "typing_Vale.X64.Lemmas.core_state", "unit_inversion", "unit_typing" ], 0, "0bdcb753e45e34ee809a330dcf8b732e" ], [ "Vale.X64.Lemmas.eval_code_eq_core", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@query", "FStar.Pervasives.Native_pretyping_b53dbd183c526bc5d0f20d7b966ae125", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "binder_x_69b3af25a4334715774d1242034fc6f2_1", "binder_x_8afd38cc1321157644dafce503e55d5a_3", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "binder_x_f537159ed795b314b4e58c260361ae86_0", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_FStar.Pervasives.Native.option", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Prims.unit", "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.squash", "equation_Vale.Arch.HeapLemmas.heap_ignore_ghost", "equation_Vale.Arch.HeapLemmas.heap_ignore_ghost_machine", "equation_Vale.X64.Bytes_Code_s.codes_t", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "function_token_typing_Vale.X64.StateLemmas.same_heap_types", "int_inversion", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "lemma_FStar.Pervasives.invertOption", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "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.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.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "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", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "typing_Vale.X64.Lemmas.core_state", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "unit_inversion", "unit_typing" ], 0, "87d922bb00dc910e9c683138a66f5f71" ], [ "Vale.X64.Lemmas.eval_code_eq_core", 3, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_while.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", "FStar.Pervasives.Native_pretyping_b53dbd183c526bc5d0f20d7b966ae125", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_e4836109f73687024ac3edd113084865", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "binder_x_8afd38cc1321157644dafce503e55d5a_4", "binder_x_8d8114524e962c921a106571a277b146_1", "binder_x_97ef5ff619e486c846fe112d821f649f_2", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3", "binder_x_f537159ed795b314b4e58c260361ae86_0", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_FStar.Pervasives.Native.option", "constructor_distinct_Prims.unit", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Prims.LexTop@tok", "equation_FStar.Pervasives.Native.snd", "equation_Prims.nat", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "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_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_Negation", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "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_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.Pervasives.Native.uu___is_None", "typing_FStar.Pervasives.Native.uu___is_Some", "typing_Vale.X64.Lemmas.core_state", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok", "typing_Vale.X64.Machine_Semantics_s.machine_eval_while", "typing_tok_Prims.LexTop@tok", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "5308f7a1d73810801bb7267318f07a10" ], [ "Vale.X64.Lemmas.eval_code_eq_f", 1, 2, 0, [ "@MaxFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@query", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2" ], 0, "62cfa7757a76f2288a3f93f7ddae1031" ], [ "Vale.X64.Lemmas.eval_codes_eq_f", 1, 2, 0, [ "@MaxFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@query", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2" ], 0, "368082fc872143538d9eb77446e82c1f" ], [ "Vale.X64.Lemmas.eval_while_eq_f", 1, 2, 0, [ "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented", "@query", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.StateLemmas.machine_state_eq", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2" ], 0, "f62a89f298de035e655740f2cd61ca02" ], [ "Vale.X64.Lemmas.eval_code_eq_t", 1, 2, 0, [ "@MaxFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@query", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2" ], 0, "fe0d38fe841eb4ca765c05288d7ed4c6" ], [ "Vale.X64.Lemmas.eval_codes_eq_t", 1, 2, 0, [ "@MaxFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@query", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2" ], 0, "7811bc2f0be433bfc04a784741d1b25a" ], [ "Vale.X64.Lemmas.eval_while_eq_t", 1, 2, 0, [ "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented", "@query", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.StateLemmas.machine_state_eq", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2" ], 0, "8ce562c65e196f9c215309e26648d7a3" ], [ "Vale.X64.Lemmas.increase_fuel", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_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", "FStar.Pervasives.Native_pretyping_b53dbd183c526bc5d0f20d7b966ae125", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "binder_x_8afd38cc1321157644dafce503e55d5a_2", "binder_x_97ef5ff619e486c846fe112d821f649f_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5", "binder_x_f537159ed795b314b4e58c260361ae86_0", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_FStar.Pervasives.Native.option", "constructor_distinct_Prims.unit", "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", "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.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.eval_code_ts", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.StateLemmas.machine_state_eq", "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.X64.Machine_Semantics_s.machine_state", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "lemma_FStar.Pervasives.invertOption", "lemma_Vale.X64.Lemmas.eval_code_eq_t", "lemma_Vale.X64.Lemmas.eval_while_eq_f", "lemma_Vale.X64.Lemmas.eval_while_eq_t", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "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_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.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_b0c0a164db57ee69accea9cf5da2c9df", "subterm_ordering_Vale.X64.Machine_s.Block", "subterm_ordering_Vale.X64.Machine_s.IfElse", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "694b958b79e6dced07014953cb16214f" ], [ "Vale.X64.Lemmas.increase_fuel", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_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", "binder_x_69b3af25a4334715774d1242034fc6f2_1", "binder_x_8afd38cc1321157644dafce503e55d5a_2", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5", "binder_x_f537159ed795b314b4e58c260361ae86_0", "bool_inversion", "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.Block", "data_elim_FStar.Pervasives.Native.Some", "data_typing_intro_Vale.X64.Machine_s.Block@tok", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Bytes_Code_s.codes_t", "equation_Vale.X64.Lemmas.eval_code_ts", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.StateLemmas.machine_state_eq", "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", "int_inversion", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "lemma_FStar.Pervasives.invertOption", "lemma_Vale.X64.Lemmas.eval_codes_eq_f", "lemma_Vale.X64.Lemmas.eval_codes_eq_t", "projection_inverse_BoxBool_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_s.Block_block", "projection_inverse_Vale.X64.Machine_s.Block_t_ins", "projection_inverse_Vale.X64.Machine_s.Block_t_ocmp", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Prims.Cons", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code" ], 0, "6d328927f5a67442f931f79f7f3ba23a" ], [ "Vale.X64.Lemmas.lemma_cmp_eq", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "200b416f5969024cff1337f55fc6f1a5" ], [ "Vale.X64.Lemmas.lemma_cmp_eq", 2, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "d580fb35fa86f47a818d730bf144ef3c" ], [ "Vale.X64.Lemmas.lemma_cmp_eq", 3, 2, 0, [ "@MaxIFuel_assumption", "@query", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_eabe638ef4af4b0ec65b4cf7bbb2dc65", "bool_inversion", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.X64.Bytes_Code_s.OEq", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "equation_FStar.Pervasives.Native.snd", "equation_FStar.Pervasives.pattern", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Lemmas.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_operand", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.valid_src_operand", "equation_Vale.X64.StateLemmas.state_to_S", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_FStar.Pervasives.pattern", "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "function_token_typing_Vale.X64.Machine_Semantics_s.eval_ocmp_opaque", "int_inversion", "interpretation_Tm_abs_b085815e1140e9a069ea4cab83d07665", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "lemma_Vale.X64.StateLemmas.lemma_to_eval_operand", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Vale.X64.Bytes_Code_s.OEq_o1", "projection_inverse_Vale.X64.Bytes_Code_s.OEq_o2", "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", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "true_interp", "typing_FStar.Pervasives.Native.snd", "typing_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "typing_Vale.X64.Machine_Semantics_s.eval_operand", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.eval_operand", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "78a20773eaa7dc1b884313d1baa3db0a" ], [ "Vale.X64.Lemmas.lemma_cmp_ne", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "062bde0a663f5af36b2d4dbecf913bd6" ], [ "Vale.X64.Lemmas.lemma_cmp_ne", 2, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "694054fac8f15ee652f5a8067bbb9760" ], [ "Vale.X64.Lemmas.lemma_cmp_ne", 3, 2, 0, [ "@MaxIFuel_assumption", "@query", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_eabe638ef4af4b0ec65b4cf7bbb2dc65", "bool_inversion", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.X64.Bytes_Code_s.ONe", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "equation_FStar.Pervasives.Native.snd", "equation_FStar.Pervasives.pattern", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Lemmas.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_operand", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.valid_src_operand", "equation_Vale.X64.StateLemmas.state_to_S", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_FStar.Pervasives.pattern", "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "function_token_typing_Vale.X64.Machine_Semantics_s.eval_ocmp_opaque", "int_inversion", "interpretation_Tm_abs_b085815e1140e9a069ea4cab83d07665", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "lemma_Vale.X64.StateLemmas.lemma_to_eval_operand", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_disEquality", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Vale.X64.Bytes_Code_s.ONe_o1", "projection_inverse_Vale.X64.Bytes_Code_s.ONe_o2", "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", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "true_interp", "typing_FStar.Pervasives.Native.snd", "typing_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "typing_Vale.X64.Machine_Semantics_s.eval_operand", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.eval_operand", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "a5a88a053aa32297f7c2afaabd727cbe" ], [ "Vale.X64.Lemmas.lemma_cmp_le", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "edd66103ab29caa8d5dbc28138a99ded" ], [ "Vale.X64.Lemmas.lemma_cmp_le", 2, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "d83610e08f2f25d12f9ac55c0a1a79f3" ], [ "Vale.X64.Lemmas.lemma_cmp_le", 3, 2, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.X64.Bytes_Code_s.OLe", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "equation_FStar.Pervasives.Native.snd", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Lemmas.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_operand", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.valid_src_operand", "equation_Vale.X64.StateLemmas.state_to_S", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "function_token_typing_Vale.X64.Machine_Semantics_s.eval_ocmp_opaque", "int_inversion", "interpretation_Tm_abs_b085815e1140e9a069ea4cab83d07665", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "lemma_Vale.X64.StateLemmas.lemma_to_eval_operand", "primitive_Prims.op_BarBar", "primitive_Prims.op_LessThanOrEqual", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Vale.X64.Bytes_Code_s.OLe_o1", "projection_inverse_Vale.X64.Bytes_Code_s.OLe_o2", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "true_interp", "typing_Vale.X64.State.eval_operand" ], 0, "4e6e72a92e005327bedb829fdf05e857" ], [ "Vale.X64.Lemmas.lemma_cmp_ge", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "dfbee2587ce9802ff600f545de405645" ], [ "Vale.X64.Lemmas.lemma_cmp_ge", 2, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "3d16005bcf3cd2adab54b43b664f16d9" ], [ "Vale.X64.Lemmas.lemma_cmp_ge", 3, 2, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.X64.Bytes_Code_s.OGe", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "equation_FStar.Pervasives.Native.snd", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Lemmas.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_operand", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.valid_src_operand", "equation_Vale.X64.StateLemmas.state_to_S", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "function_token_typing_Vale.X64.Machine_Semantics_s.eval_ocmp_opaque", "int_inversion", "interpretation_Tm_abs_b085815e1140e9a069ea4cab83d07665", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "lemma_Vale.X64.StateLemmas.lemma_to_eval_operand", "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Vale.X64.Bytes_Code_s.OGe_o1", "projection_inverse_Vale.X64.Bytes_Code_s.OGe_o2", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "true_interp", "typing_Vale.X64.State.eval_operand" ], 0, "381db8a6d005379689a22b74eb099962" ], [ "Vale.X64.Lemmas.lemma_cmp_lt", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "40c65ac90217b16cc535097c3b0042d4" ], [ "Vale.X64.Lemmas.lemma_cmp_lt", 2, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "718ac90856cb711caa60d0be8077208e" ], [ "Vale.X64.Lemmas.lemma_cmp_lt", 3, 2, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.X64.Bytes_Code_s.OLt", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "equation_FStar.Pervasives.Native.snd", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Lemmas.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_operand", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.valid_src_operand", "equation_Vale.X64.StateLemmas.state_to_S", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "function_token_typing_Vale.X64.Machine_Semantics_s.eval_ocmp_opaque", "int_inversion", "interpretation_Tm_abs_b085815e1140e9a069ea4cab83d07665", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "lemma_Vale.X64.StateLemmas.lemma_to_eval_operand", "primitive_Prims.op_BarBar", "primitive_Prims.op_LessThan", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Vale.X64.Bytes_Code_s.OLt_o1", "projection_inverse_Vale.X64.Bytes_Code_s.OLt_o2", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "true_interp", "typing_Vale.X64.State.eval_operand" ], 0, "6e1b1384566b0ea7bcf7048ca951600e" ], [ "Vale.X64.Lemmas.lemma_cmp_gt", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "40b17d9d5fa2849d1a0f068dc178d7ca" ], [ "Vale.X64.Lemmas.lemma_cmp_gt", 2, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "81de5152dc00ef239954e1d7a55d155e" ], [ "Vale.X64.Lemmas.lemma_cmp_gt", 3, 2, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.X64.Bytes_Code_s.OGt", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "equation_FStar.Pervasives.Native.snd", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Lemmas.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_operand", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.valid_src_operand", "equation_Vale.X64.StateLemmas.state_to_S", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "function_token_typing_Vale.X64.Machine_Semantics_s.eval_ocmp_opaque", "int_inversion", "interpretation_Tm_abs_b085815e1140e9a069ea4cab83d07665", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "lemma_Vale.X64.StateLemmas.lemma_to_eval_operand", "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThan", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Vale.X64.Bytes_Code_s.OGt_o1", "projection_inverse_Vale.X64.Bytes_Code_s.OGt_o2", "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "true_interp", "typing_Vale.X64.State.eval_operand" ], 0, "e92dd486b6ade0cee0e98918bcd3d7b8" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_eq", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "bcfe6c85a497adf0ae66e860f7793321" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_eq", 2, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "52e0c5de0bcb655c3260b6117267b2f6" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_eq", 3, 2, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Vale.X64.Bytes_Code_s.OEq", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Lemmas.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.StateLemmas.state_to_S", "fuel_guarded_inversion_Vale.X64.State.vale_state", "lemma_Vale.X64.StateLemmas.lemma_to_valid_operand", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0", "projection_inverse_Vale.X64.Bytes_Code_s.OEq_o1", "projection_inverse_Vale.X64.Bytes_Code_s.OEq_o2", "refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "715ecbd6d47c769292705bb20224dec8" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_ne", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "ad8e6b239f693276fe542c6ce47df977" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_ne", 2, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "32d94407a0ca8faec53d921214563004" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_ne", 3, 2, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Vale.X64.Bytes_Code_s.ONe", "data_typing_intro_Vale.X64.Bytes_Code_s.ONe@tok", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Lemmas.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.StateLemmas.state_to_S", "fuel_guarded_inversion_Vale.X64.State.vale_state", "lemma_Vale.X64.StateLemmas.lemma_to_valid_operand", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0", "projection_inverse_Vale.X64.Bytes_Code_s.ONe_o1", "projection_inverse_Vale.X64.Bytes_Code_s.ONe_o2", "refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "typing_Vale.X64.Lemmas.valid_ocmp", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "b5f8ab249a83f44ec5337440a59463c8" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_le", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "cdd2d707b8cf5efa61a2e84e483bd0c8" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_le", 2, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "5b5594ac715a12f969a4c3a10a24f8a3" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_le", 3, 2, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Vale.X64.Bytes_Code_s.OLe", "data_typing_intro_Vale.X64.Bytes_Code_s.OLe@tok", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Lemmas.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.StateLemmas.state_to_S", "fuel_guarded_inversion_Vale.X64.State.vale_state", "lemma_Vale.X64.StateLemmas.lemma_to_valid_operand", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0", "projection_inverse_Vale.X64.Bytes_Code_s.OLe_o1", "projection_inverse_Vale.X64.Bytes_Code_s.OLe_o2", "refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "typing_Vale.X64.Lemmas.valid_ocmp", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "a9fbd63be1316966f3b09f16c05aca42" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_ge", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "a30e3daca885c6e4ba5727f8686854b5" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_ge", 2, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "063b0cef6278bb524f6966db293dc88d" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_ge", 3, 2, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Vale.X64.Bytes_Code_s.OGe", "data_typing_intro_Vale.X64.Bytes_Code_s.OGe@tok", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Lemmas.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.StateLemmas.state_to_S", "fuel_guarded_inversion_Vale.X64.State.vale_state", "lemma_Vale.X64.StateLemmas.lemma_to_valid_operand", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0", "projection_inverse_Vale.X64.Bytes_Code_s.OGe_o1", "projection_inverse_Vale.X64.Bytes_Code_s.OGe_o2", "refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "typing_Vale.X64.Lemmas.valid_ocmp", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "636dab22a7850d4700efa89a8fb4c828" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_lt", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "22a06df053b873612b5daca779fb9638" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_lt", 2, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "4a4dd13459d681a5d2a45f03a4c3adb3" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_lt", 3, 2, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Vale.X64.Bytes_Code_s.OLt", "data_typing_intro_Vale.X64.Bytes_Code_s.OLt@tok", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Lemmas.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.StateLemmas.state_to_S", "fuel_guarded_inversion_Vale.X64.State.vale_state", "lemma_Vale.X64.StateLemmas.lemma_to_valid_operand", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0", "projection_inverse_Vale.X64.Bytes_Code_s.OLt_o1", "projection_inverse_Vale.X64.Bytes_Code_s.OLt_o2", "refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "typing_Vale.X64.Lemmas.valid_ocmp", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "a74292b9f436d17c0301f0adfcc3ddb9" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_gt", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "9cd270a38ed6691ce94e40dad691ca77" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_gt", 2, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "f15be8dc591e787b3a9ce79e9658b853" ], [ "Vale.X64.Lemmas.lemma_valid_cmp_gt", 3, 2, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Vale.X64.Bytes_Code_s.OGt", "data_typing_intro_Vale.X64.Bytes_Code_s.OGt@tok", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Lemmas.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.StateLemmas.state_to_S", "fuel_guarded_inversion_Vale.X64.State.vale_state", "lemma_Vale.X64.StateLemmas.lemma_to_valid_operand", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0", "projection_inverse_Vale.X64.Bytes_Code_s.OGt_o1", "projection_inverse_Vale.X64.Bytes_Code_s.OGt_o2", "refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "typing_Vale.X64.Lemmas.valid_ocmp", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "57740fe1af3e661fc664957ca19c26af" ], [ "Vale.X64.Lemmas.lemma_merge_total", 1, 2, 0, [ "@query" ], 0, "b09c3117eeb5ecc06d71eb2e96a5368a" ], [ "Vale.X64.Lemmas.lemma_merge_total", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "@fuel_correspondence_Vale.X64.Lemmas.codes_modifies_ghost.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Lemmas.codes_modifies_ghost.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", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Vale.X64.Machine_s.Block", "data_elim_FStar.Pervasives.Native.Some", "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", "equation_Prims.nat", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Bytes_Code_s.codes_t", "equation_Vale.X64.Lemmas.compute_merge_total", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.eval_code", "equation_Vale.X64.Lemmas.eval_code_ts", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_Vale.X64.StateLemmas.state_to_S", "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "equation_with_fuel_Vale.X64.Lemmas.codes_modifies_ghost.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.State.vale_state", "function_token_typing_Vale.X64.Machine_Semantics_s.code", "function_token_typing_Vale.X64.Machine_Semantics_s.ins", "int_inversion", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "lemma_FStar.Pervasives.invertOption", "lemma_Vale.X64.Lemmas.eval_code_eq_f", "lemma_Vale.X64.Lemmas.eval_code_eq_t", "lemma_Vale.X64.Lemmas.eval_codes_eq_f", "lemma_Vale.X64.Lemmas.eval_codes_eq_t", "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThan", "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl", "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.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.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", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7aac12c24449a22c34d98a0ea8ed4a32", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "typing_Prims.__proj__Cons__item__hd", "typing_Prims.__proj__Cons__item__tl", "typing_Vale.X64.Lemmas.code_modifies_ghost", "typing_Vale.X64.Lemmas.core_state", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "62c51e5f904c6ab700674e3de8b26ca6" ], [ "Vale.X64.Lemmas.lemma_empty_total", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@query", "constructor_distinct_Prims.Nil", "constructor_distinct_Vale.X64.Machine_s.Block", "data_typing_intro_Prims.Nil@tok", "data_typing_intro_Vale.X64.Machine_s.Block@tok", "equation_Prims.nat", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Bytes_Code_s.codes_t", "equation_Vale.X64.Lemmas.eval_code", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "equation_with_fuel_Vale.X64.Lemmas.codes_modifies_ghost.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", "function_token_typing_Vale.X64.Machine_Semantics_s.code", "function_token_typing_Vale.X64.Machine_Semantics_s.ins", "int_typing", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok", "lemma_Vale.X64.Lemmas.eval_code_eq_f", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "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_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "32aff492573b94b8a37d952776080441" ], [ "Vale.X64.Lemmas.lemma_ifElse_total", 1, 2, 0, [ "@query", "equation_Prims.nat", "projection_inverse_FStar.Pervasives.Native.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2" ], 0, "afbe1bae86e0822307a420683800461c" ], [ "Vale.X64.Lemmas.lemma_havoc_flags", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.X64.Flags_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100", "Vale.X64.Flags_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144", "Vale.X64.Flags_interpretation_Tm_arrow_c9f84314ba6aade3760e20965d165b65", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.is_restricted", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_Vale.X64.Flags.sel_curry", "equation_Vale.X64.Flags.to_fun", "equation_Vale.X64.Lemmas.havoc_flags", "equation_Vale.X64.Machine_Semantics_s.flags_t", "equation_Vale.X64.Machine_Semantics_s.havoc_flags", "equation_Vale.X64.Machine_s.flag", "function_token_typing_Vale.X64.Flags.sel_curry", "function_token_typing_Vale.X64.Machine_Semantics_s.flags_none", "int_inversion", "interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366", "lemma_FStar.FunctionalExtensionality.extensionality", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "refinement_interpretation_Tm_refine_423a970236765465eb8eb63b6e1b8f53", "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64", "token_correspondence_Vale.X64.Flags.sel_curry", "typing_FStar.FunctionalExtensionality.on_domain", "typing_Tm_abs_f086d77986b470aab4bfebc171e6c366", "typing_Vale.X64.Flags.of_fun", "typing_Vale.X64.Flags.to_fun", "typing_Vale.X64.Lemmas.havoc_flags", "typing_Vale.X64.Machine_Semantics_s.havoc_flags" ], 0, "3d7d1d1c91750f42e2b9a5b6b469d607" ], [ "Vale.X64.Lemmas.lemma_ifElseTrue_total", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Vale.X64.Machine_s.IfElse", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok", "data_typing_intro_Vale.X64.Machine_s.BranchPredicate@tok", "data_typing_intro_Vale.X64.Machine_s.IfElse@tok", "data_typing_intro_Vale.X64.State.Mkvale_state@tok", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "eq2-interp", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Flags.to_fun", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.eval_code", "equation_Vale.X64.Lemmas.eval_ocmp", "equation_Vale.X64.Lemmas.lemma_havoc_flags", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.Lemmas.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.flags_t", "equation_Vale.X64.Machine_Semantics_s.havoc_flags", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_Semantics_s.regs_t", "equation_Vale.X64.Memory.memtaint", "equation_Vale.X64.Regs.regs_fun", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_Vale.X64.StateLemmas.state_to_S", "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "function_token_typing_Vale.X64.Lemmas.lemma_havoc_flags", "function_token_typing_Vale.X64.Machine_Semantics_s.ins", "function_token_typing_Vale.X64.Machine_Semantics_s.valid_ocmp_opaque", "function_token_typing_Vale.X64.StateLemmas.same_heap_types", "int_inversion", "interpretation_Tm_abs_275a4a20fec2a36f25eb34b853a79209", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "kinding_Vale.X64.Machine_s.observation@tok", "lemma_FStar.Pervasives.invertOption", "lemma_Vale.X64.Lemmas.eval_code_eq_f", "lemma_Vale.X64.Lemmas.eval_code_eq_t", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "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", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxBool_proj_0", "projection_inverse_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.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.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.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.X64.Flags.to_fun", "typing_Vale.X64.Lemmas.code_modifies_ghost", "typing_Vale.X64.Lemmas.eval_ocmp", "typing_Vale.X64.Lemmas.havoc_flags", "typing_Vale.X64.Lemmas.valid_ocmp", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_trace", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "typing_Vale.X64.Regs.to_fun", "typing_Vale.X64.Stack_Sems.stack_to_s", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "c770fc789cc36e8061b08399ef47b920" ], [ "Vale.X64.Lemmas.lemma_ifElseFalse_total", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Vale.X64.Machine_s.IfElse", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok", "data_typing_intro_Vale.X64.Machine_s.BranchPredicate@tok", "data_typing_intro_Vale.X64.Machine_s.IfElse@tok", "data_typing_intro_Vale.X64.State.Mkvale_state@tok", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "eq2-interp", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Flags.to_fun", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.eval_code", "equation_Vale.X64.Lemmas.eval_ocmp", "equation_Vale.X64.Lemmas.lemma_havoc_flags", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.Lemmas.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.flags_t", "equation_Vale.X64.Machine_Semantics_s.havoc_flags", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_Semantics_s.regs_t", "equation_Vale.X64.Memory.memtaint", "equation_Vale.X64.Regs.regs_fun", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_Vale.X64.StateLemmas.state_to_S", "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "function_token_typing_Vale.X64.Lemmas.lemma_havoc_flags", "function_token_typing_Vale.X64.Machine_Semantics_s.ins", "function_token_typing_Vale.X64.Machine_Semantics_s.valid_ocmp_opaque", "function_token_typing_Vale.X64.StateLemmas.same_heap_types", "int_inversion", "interpretation_Tm_abs_275a4a20fec2a36f25eb34b853a79209", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "kinding_Vale.X64.Machine_s.observation@tok", "lemma_FStar.Pervasives.invertOption", "lemma_Vale.X64.Lemmas.eval_code_eq_f", "lemma_Vale.X64.Lemmas.eval_code_eq_t", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "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", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxBool_proj_0", "projection_inverse_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.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.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.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.X64.Flags.to_fun", "typing_Vale.X64.Lemmas.code_modifies_ghost", "typing_Vale.X64.Lemmas.core_state", "typing_Vale.X64.Lemmas.eval_ocmp", "typing_Vale.X64.Lemmas.havoc_flags", "typing_Vale.X64.Lemmas.valid_ocmp", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_trace", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "typing_Vale.X64.Regs.to_fun", "typing_Vale.X64.Stack_Sems.stack_to_s", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "b8f73cdd3c7544fabf9cae9922725abe" ], [ "Vale.X64.Lemmas.eval_while_inv_temp", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "bbac7d04e593bf9aed67f3ae07b66f7a" ], [ "Vale.X64.Lemmas.lemma_while_total", 1, 2, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Vale.X64.Lemmas.eval_while_inv", "equation_Vale.X64.Lemmas.eval_while_inv_temp", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.StateLemmas.machine_state_eq", "int_inversion", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "2efcfe45e3f9819857b88ba426bdc799" ], [ "Vale.X64.Lemmas.lemma_whileTrue_total", 1, 2, 0, [ "@query", "equation_Prims.nat", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2" ], 0, "a48b97dc50e92a74fd82bac502f602f1" ], [ "Vale.X64.Lemmas.lemma_whileFalse_total", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.X64.State_pretyping_eb96f2119e19317ec6e3b596d5a46609", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Vale.X64.Machine_s.While", "data_typing_intro_Vale.X64.Machine_s.While@tok", "disc_equation_FStar.Pervasives.Native.Some", "eq2-interp", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.eval_code", "equation_Vale.X64.Lemmas.eval_ocmp", "equation_Vale.X64.Lemmas.eval_while_inv", "equation_Vale.X64.Lemmas.eval_while_inv_temp", "equation_Vale.X64.Lemmas.havoc_flags", "equation_Vale.X64.Lemmas.lemma_havoc_flags", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.Lemmas.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.havoc_flags", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_Vale.X64.StateLemmas.state_to_S", "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.X64.Lemmas.lemma_havoc_flags", "function_token_typing_Vale.X64.Machine_Semantics_s.ins", "function_token_typing_Vale.X64.Machine_Semantics_s.valid_ocmp_opaque", "int_inversion", "int_typing", "interpretation_Tm_abs_275a4a20fec2a36f25eb34b853a79209", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "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", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Vale.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.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", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.X64.Lemmas.eval_ocmp", "typing_Vale.X64.Lemmas.valid_ocmp", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "ea4bb78e7e8baef0444b4c619b04e753" ], [ "Vale.X64.Lemmas.lemma_whileMerge_total", 1, 2, 0, [ "@query" ], 0, "ca2748d40859b3ead8379e39234dbd97" ], [ "Vale.X64.Lemmas.lemma_whileMerge_total", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Lemmas.code_modifies_ghost.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", "Vale.X64.Bytes_Code_s_pretyping_8d8114524e962c921a106571a277b146", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Tm_unit", "data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_FStar.Pervasives.Native.Some", "data_elim_Vale.X64.Bytes_Code_s.OEq", "data_elim_Vale.X64.Bytes_Code_s.OGe", "data_elim_Vale.X64.Bytes_Code_s.OGt", "data_elim_Vale.X64.Bytes_Code_s.OLe", "data_elim_Vale.X64.Bytes_Code_s.OLt", "data_elim_Vale.X64.Bytes_Code_s.ONe", "data_elim_Vale.X64.Machine_s.While", "data_elim_Vale.X64.State.Mkvale_state", "data_typing_intro_Vale.X64.State.Mkvale_state@tok", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "disc_equation_Vale.X64.Machine_s.While", "eq2-interp", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapLemmas.heap_ignore_ghost", "equation_Vale.Arch.HeapLemmas.heap_ignore_ghost_machine", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Flags.to_fun", "equation_Vale.X64.Lemmas.core_state", "equation_Vale.X64.Lemmas.eval_code", "equation_Vale.X64.Lemmas.eval_code_ts", "equation_Vale.X64.Lemmas.eval_ocmp", "equation_Vale.X64.Lemmas.eval_while_inv", "equation_Vale.X64.Lemmas.eval_while_inv_temp", "equation_Vale.X64.Lemmas.lemma_havoc_flags", "equation_Vale.X64.Lemmas.state_eq_S", "equation_Vale.X64.Lemmas.state_eq_opt", "equation_Vale.X64.Lemmas.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.havoc_flags", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "equation_Vale.X64.Machine_s.operand64", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.StateLemmas.machine_state_eq", "equation_Vale.X64.StateLemmas.state_to_S", "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.X64.Lemmas.lemma_havoc_flags", "function_token_typing_Vale.X64.Machine_Semantics_s.ins", "function_token_typing_Vale.X64.Machine_Semantics_s.valid_ocmp_opaque", "int_inversion", "int_typing", "interpretation_Tm_abs_275a4a20fec2a36f25eb34b853a79209", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "lemma_FStar.Pervasives.invertOption", "lemma_Vale.X64.Lemmas.eval_code_eq_f", "lemma_Vale.X64.Lemmas.eval_code_eq_t", "lemma_Vale.X64.Lemmas.eval_while_eq_f", "lemma_Vale.X64.Lemmas.eval_while_eq_t", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_Negation", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "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", "proj_equation_Vale.X64.Machine_s.While_whileBody", "proj_equation_Vale.X64.Machine_s.While_whileCond", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint", "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.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8d7684ca1be7acf48e31bf17f1a9fe2b", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "token_correspondence_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented", "typing_Vale.X64.Lemmas.code_modifies_ghost", "typing_Vale.X64.Lemmas.core_state", "typing_Vale.X64.Lemmas.eval_ocmp", "typing_Vale.X64.Lemmas.havoc_flags", "typing_Vale.X64.Lemmas.valid_ocmp", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "typing_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "typing_Vale.X64.Machine_s.__proj__While__item__whileBody", "typing_Vale.X64.Machine_s.__proj__While__item__whileCond", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint", "typing_Vale.X64.StateLemmas.state_to_S" ], 0, "2583fb86366eba180bdec7cc24c62d19" ] ] ]