[ "/&|k26z", [ [ "Vale.X64.InsStack.va_lemma_Stack_lemma", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Vale.X64.Machine_s.Block", "disc_equation_Vale.X64.Machine_s.Block", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.State.state_eq", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_equal_intro", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "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", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs" ], 0, "adc93e71763c49cdb23cc11c627bded4" ], [ "Vale.X64.InsStack.va_wpProof_Stack_lemma", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.InsStack.va_wp_Stack_lemma", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.state_eq", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "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_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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", "unit_typing" ], 0, "4e38e93a31ba8ca5bd6fc96e3dca5e73" ], [ "Vale.X64.InsStack.va_quick_Stack_lemma", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.X64.Decls.va_fuel", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "0747ad9058c6ff746112f0702e91af68" ], [ "Vale.X64.InsStack.va_lemma_Pop", 1, 2, 2, [ "@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_f8666440faa91836cc5a13998af863fc", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "Vale.X64.Flags_interpretation_Tm_arrow_c9f84314ba6aade3760e20965d165b65", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_2eb22b38a6da10fb966327d892d8131d", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_aa589b9ef510f53ad802095d5dd3ddab", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Pervasives.Native.Mktuple2", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.X64.Bytes_Code_s.Pop", "constructor_distinct_Vale.X64.Machine_s.Ins", "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.Machine_Semantics_s.Machine_stack", "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state", "data_elim_Vale.X64.Machine_s.Ins", "data_elim_Vale.X64.Machine_s.OReg", "data_elim_Vale.X64.State.Mkvale_state", "data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok", "data_typing_intro_Vale.X64.Machine_s.MReg@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Vale.X64.Machine_s.Ins", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equation_FStar.FunctionalExtensionality.feq", "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.HeapImpl.vale_heaplets", "equation_Vale.Arch.HeapTypes_s.memTaint_t", "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.Decls.eval_code", "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_is_dst_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Flags.sel_curry", "equation_Vale.X64.Flags.to_fun", "equation_Vale.X64.Lemmas.eval_ins", "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.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.ocmp", "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_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.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.Memory.memtaint", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.Stack_i.init_rsp", "equation_Vale.X64.Stack_i.valid_src_stack64", "equation_Vale.X64.Stack_i.valid_taint_stack64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.StateLemmas.state_of_S", "equation_Vale.X64.StateLemmas.state_to_S", "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_stack", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.X64.Flags.sel_curry", "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_s.t_reg", "function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl", "int_inversion", "int_typing", "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821", "interpretation_Tm_abs_4671ae2ba06d701a8ddfd527a574fa44", "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749", "interpretation_Tm_abs_b3799bd9160660915dad8cdf26d6109c", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "kinding_Vale.Arch.HeapTypes_s.taint@tok", "kinding_Vale.X64.Machine_s.reg@tok", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_upd_eq", "lemma_Vale.X64.Regs.lemma_upd_ne", "lemma_Vale.X64.Stack_Sems.equiv_free_stack", "lemma_Vale.X64.Stack_Sems.equiv_init_rsp", "lemma_Vale.X64.Stack_Sems.equiv_load_stack64", "lemma_Vale.X64.Stack_Sems.equiv_valid_src_stack64", "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", "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_v", "projection_inverse_Vale.X64.Bytes_Code_s.Pop_a", "projection_inverse_Vale.X64.Bytes_Code_s.Pop_dst", "projection_inverse_Vale.X64.Bytes_Code_s.Pop_t", "projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp", "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.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_r", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "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_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_423a970236765465eb8eb63b6e1b8f53", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_a51eae56a5c39d95827d04b5f0544d43", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c2c488db3214c38826155caf10d30036", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64", "token_correspondence_Vale.X64.Flags.sel_curry", "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_FStar.Map.sel", "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749", "typing_Tm_abs_f086d77986b470aab4bfebc171e6c366", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.MachineHeap_s.get_heap_val64", "typing_Vale.X64.Decls.update_operand", "typing_Vale.X64.Decls.va_is_dst_opr64", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_stack", "typing_Vale.X64.Flags.of_fun", "typing_Vale.X64.InsStack.va_code_Pop", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "typing_Vale.X64.Machine_Semantics_s.eval_maddr", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins", "typing_Vale.X64.Machine_Semantics_s.match_n", "typing_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags_", "typing_Vale.X64.Machine_Semantics_s.update_rsp_", "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_Sems.stack_to_s", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.Stack_i.valid_src_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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.State.update_reg", "typing_Vale.X64.StateLemmas.state_to_S", "unit_typing" ], 0, "62f3dcbc0517ba8b7b935d930b25e6b9" ], [ "Vale.X64.InsStack.va_wpProof_Pop", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2", "bool_inversion", "constructor_distinct_Prims.Nil", "constructor_distinct_Vale.X64.QuickCode.Mod_reg", "data_typing_intro_Prims.Nil@tok", "equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_is_dst_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_operand_dst_opr64", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.InsStack.va_wp_Pop", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.Stack_i.free_stack64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "kinding_Vale.X64.QuickCode.mod_t@tok", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Stack_Sems.equiv_init_rsp", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "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.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Prims.Nil_a", "projection_inverse_Vale.X64.QuickCode.Mod_reg__0", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Decls.update_operand", "typing_Vale.X64.Decls.va_is_dst_opr64", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Stack_i.free_stack64", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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.eval_operand", "typing_tok_Vale.X64.QuickCode.Mod_None@tok", "unit_typing" ], 0, "f4cf53517aca937f2fa066ecb65e66d6" ], [ "Vale.X64.InsStack.va_quick_Pop", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.X64.Decls.va_fuel", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "1a9d4c1b40d96fe9d3c005776cb86fa5" ], [ "Vale.X64.InsStack.va_lemma_Push", 1, 2, 0, [ "@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_f8666440faa91836cc5a13998af863fc", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "Vale.X64.Bytes_Code_s_interpretation_Tm_arrow_af0bd51d3b53ddf4528e9746830b24b5", "Vale.X64.Flags_interpretation_Tm_arrow_c9f84314ba6aade3760e20965d165b65", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Pervasives.Native.Mktuple2", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.X64.Bytes_Code_s.Push", "constructor_distinct_Vale.X64.Machine_s.Ins", "constructor_distinct_Vale.X64.Machine_s.MConst", "constructor_distinct_Vale.X64.Machine_s.OStack", "data_typing_intro_Vale.X64.Bytes_Code_s.Push@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Vale.X64.Machine_s.Ins", "disc_equation_Vale.X64.Machine_s.OReg", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Bytes_Code_s.instr_annotation_t", "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_operand_reg_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Flags.sel_curry", "equation_Vale.X64.Flags.to_fun", "equation_Vale.X64.Lemmas.eval_ins", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.eval_maddr", "equation_Vale.X64.Machine_Semantics_s.flags_t", "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.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_Semantics_s.regs_t", "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.reg_64", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Memory.memtaint", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.Stack_i.store_taint_stack64", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.valid_src_operand", "equation_Vale.X64.StateLemmas.state_of_S", "equation_Vale.X64.StateLemmas.state_to_S", "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.X64.Flags.sel_curry", "function_token_typing_Vale.X64.Machine_s.t_reg", "function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl", "int_inversion", "int_typing", "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821", "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_ec68e3b9ffa3f3f4eb4169d3e7e95c77", "interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "kinding_Vale.X64.Machine_Semantics_s.instr_annotation@tok", "kinding_Vale.X64.Machine_s.reg@tok", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_upd_eq", "lemma_Vale.X64.Regs.lemma_upd_ne", "lemma_Vale.X64.Stack_Sems.equiv_init_rsp", "lemma_Vale.X64.StateLemmas.lemma_to_eval_operand", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "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.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_v", "projection_inverse_Vale.X64.Bytes_Code_s.Push_a", "projection_inverse_Vale.X64.Bytes_Code_s.Push_src", "projection_inverse_Vale.X64.Bytes_Code_s.Push_t", "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.OStack_m", "projection_inverse_Vale.X64.Machine_s.OStack_tc", "projection_inverse_Vale.X64.Machine_s.OStack_tr", "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_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7", "refinement_interpretation_Tm_refine_423a970236765465eb8eb63b6e1b8f53", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64", "token_correspondence_Vale.X64.Flags.sel_curry", "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "token_correspondence_Vale.X64.Machine_Semantics_s.instr_annotation@tok", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_ins_st", "token_correspondence_Vale.X64.Machine_s.t_reg", "true_interp", "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749", "typing_Tm_abs_f086d77986b470aab4bfebc171e6c366", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Decls.va_upd_stack", "typing_Vale.X64.Decls.va_upd_stackTaint", "typing_Vale.X64.Flags.of_fun", "typing_Vale.X64.InsStack.va_code_Push", "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_stackTaint", "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins", "typing_Vale.X64.Machine_Semantics_s.update_rsp_", "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_Vale.X64.State.update_reg", "typing_Vale.X64.StateLemmas.state_to_S", "typing_tok_Vale.Arch.HeapTypes_s.Public@tok", "unit_typing" ], 0, "2b4c442683e62369af38178dbb220138" ], [ "Vale.X64.InsStack.va_wpProof_Push", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.InsStack.va_wp_Push", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.Stack_i.init_rsp", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.Stack_i.store_taint_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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_tok_Vale.Arch.HeapTypes_s.Public@tok", "unit_typing" ], 0, "dcc85ef23af0b2f0734a263f5b1c1c37" ], [ "Vale.X64.InsStack.va_quick_Push", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.X64.Decls.va_fuel", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "f9ba1f35253a5296fd7fee63db056553" ], [ "Vale.X64.InsStack.va_lemma_Pop_Secret", 1, 2, 2, [ "@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_f8666440faa91836cc5a13998af863fc", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "Vale.X64.Flags_interpretation_Tm_arrow_c9f84314ba6aade3760e20965d165b65", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_2eb22b38a6da10fb966327d892d8131d", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_aa589b9ef510f53ad802095d5dd3ddab", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Pervasives.Native.Mktuple2", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.X64.Bytes_Code_s.Pop", "constructor_distinct_Vale.X64.Machine_s.Ins", "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.Machine_Semantics_s.Machine_stack", "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state", "data_elim_Vale.X64.Machine_s.Ins", "data_elim_Vale.X64.Machine_s.OReg", "data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok", "data_typing_intro_Vale.X64.Machine_s.MReg@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Vale.X64.Machine_s.Ins", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equation_FStar.FunctionalExtensionality.feq", "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.HeapImpl.vale_heaplets", "equation_Vale.Arch.HeapTypes_s.memTaint_t", "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.Decls.eval_code", "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_is_dst_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Flags.sel_curry", "equation_Vale.X64.Flags.to_fun", "equation_Vale.X64.Lemmas.eval_ins", "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.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.ocmp", "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_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.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.Memory.memtaint", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.Stack_i.init_rsp", "equation_Vale.X64.Stack_i.valid_src_stack64", "equation_Vale.X64.Stack_i.valid_taint_stack64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.StateLemmas.state_of_S", "equation_Vale.X64.StateLemmas.state_to_S", "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_stack", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.X64.Flags.sel_curry", "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_s.t_reg", "function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl", "int_inversion", "int_typing", "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821", "interpretation_Tm_abs_4671ae2ba06d701a8ddfd527a574fa44", "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749", "interpretation_Tm_abs_b3799bd9160660915dad8cdf26d6109c", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "kinding_Vale.Arch.HeapTypes_s.taint@tok", "kinding_Vale.X64.Machine_s.reg@tok", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_upd_eq", "lemma_Vale.X64.Regs.lemma_upd_ne", "lemma_Vale.X64.Stack_Sems.equiv_free_stack", "lemma_Vale.X64.Stack_Sems.equiv_init_rsp", "lemma_Vale.X64.Stack_Sems.equiv_load_stack64", "lemma_Vale.X64.Stack_Sems.equiv_valid_src_stack64", "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", "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_v", "projection_inverse_Vale.X64.Bytes_Code_s.Pop_a", "projection_inverse_Vale.X64.Bytes_Code_s.Pop_dst", "projection_inverse_Vale.X64.Bytes_Code_s.Pop_t", "projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp", "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.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_r", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "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_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_423a970236765465eb8eb63b6e1b8f53", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_a51eae56a5c39d95827d04b5f0544d43", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c2c488db3214c38826155caf10d30036", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64", "token_correspondence_Vale.X64.Flags.sel_curry", "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_FStar.Map.sel", "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749", "typing_Tm_abs_f086d77986b470aab4bfebc171e6c366", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.MachineHeap_s.get_heap_val64", "typing_Vale.X64.Decls.update_operand", "typing_Vale.X64.Decls.va_is_dst_opr64", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_stack", "typing_Vale.X64.Flags.of_fun", "typing_Vale.X64.InsStack.va_code_Pop_Secret", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "typing_Vale.X64.Machine_Semantics_s.eval_maddr", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins", "typing_Vale.X64.Machine_Semantics_s.match_n", "typing_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags_", "typing_Vale.X64.Machine_Semantics_s.update_rsp_", "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_Sems.stack_to_s", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.Stack_i.valid_src_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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.State.update_reg", "typing_Vale.X64.StateLemmas.state_to_S", "unit_typing" ], 0, "0b0c6b4a3577ee4ae0107d80024a6ccd" ], [ "Vale.X64.InsStack.va_wpProof_Pop_Secret", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2", "bool_inversion", "constructor_distinct_Prims.Nil", "constructor_distinct_Vale.X64.QuickCode.Mod_reg", "data_typing_intro_Prims.Nil@tok", "equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_is_dst_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_operand_dst_opr64", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.InsStack.va_wp_Pop_Secret", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.Stack_i.free_stack64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "kinding_Vale.X64.QuickCode.mod_t@tok", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Stack_Sems.equiv_init_rsp", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "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.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Prims.Nil_a", "projection_inverse_Vale.X64.QuickCode.Mod_reg__0", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Decls.update_operand", "typing_Vale.X64.Decls.va_is_dst_opr64", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Stack_i.free_stack64", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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.eval_operand", "typing_tok_Vale.X64.QuickCode.Mod_None@tok", "unit_typing" ], 0, "61be5feca17e39bb5a73fd12b6f71adb" ], [ "Vale.X64.InsStack.va_quick_Pop_Secret", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.X64.Decls.va_fuel", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "8846e1875a13de35a0c3efdcfeda0992" ], [ "Vale.X64.InsStack.va_lemma_Push_Secret", 1, 2, 0, [ "@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_f8666440faa91836cc5a13998af863fc", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "Vale.X64.Bytes_Code_s_interpretation_Tm_arrow_af0bd51d3b53ddf4528e9746830b24b5", "Vale.X64.Flags_interpretation_Tm_arrow_c9f84314ba6aade3760e20965d165b65", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Pervasives.Native.Mktuple2", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.X64.Bytes_Code_s.Push", "constructor_distinct_Vale.X64.Machine_s.Ins", "constructor_distinct_Vale.X64.Machine_s.MConst", "constructor_distinct_Vale.X64.Machine_s.OStack", "data_typing_intro_Vale.X64.Bytes_Code_s.Push@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Vale.X64.Machine_s.Ins", "disc_equation_Vale.X64.Machine_s.OReg", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Bytes_Code_s.instr_annotation_t", "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_operand_reg_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Flags.sel_curry", "equation_Vale.X64.Flags.to_fun", "equation_Vale.X64.Lemmas.eval_ins", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.eval_maddr", "equation_Vale.X64.Machine_Semantics_s.flags_t", "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.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_Semantics_s.regs_t", "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.reg_64", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_Vale.X64.Memory.memtaint", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.Stack_i.store_taint_stack64", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.valid_src_operand", "equation_Vale.X64.StateLemmas.state_of_S", "equation_Vale.X64.StateLemmas.state_to_S", "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.X64.Flags.sel_curry", "function_token_typing_Vale.X64.Machine_s.t_reg", "function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl", "int_inversion", "int_typing", "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821", "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_ec68e3b9ffa3f3f4eb4169d3e7e95c77", "interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "kinding_Vale.X64.Machine_Semantics_s.instr_annotation@tok", "kinding_Vale.X64.Machine_s.reg@tok", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_upd_eq", "lemma_Vale.X64.Regs.lemma_upd_ne", "lemma_Vale.X64.Stack_Sems.equiv_init_rsp", "lemma_Vale.X64.StateLemmas.lemma_to_eval_operand", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "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.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_v", "projection_inverse_Vale.X64.Bytes_Code_s.Push_a", "projection_inverse_Vale.X64.Bytes_Code_s.Push_src", "projection_inverse_Vale.X64.Bytes_Code_s.Push_t", "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.OStack_m", "projection_inverse_Vale.X64.Machine_s.OStack_tc", "projection_inverse_Vale.X64.Machine_s.OStack_tr", "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_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7", "refinement_interpretation_Tm_refine_423a970236765465eb8eb63b6e1b8f53", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64", "token_correspondence_Vale.X64.Flags.sel_curry", "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "token_correspondence_Vale.X64.Machine_Semantics_s.instr_annotation@tok", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_ins_st", "token_correspondence_Vale.X64.Machine_s.t_reg", "true_interp", "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749", "typing_Tm_abs_f086d77986b470aab4bfebc171e6c366", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Decls.va_upd_stack", "typing_Vale.X64.Decls.va_upd_stackTaint", "typing_Vale.X64.Flags.of_fun", "typing_Vale.X64.InsStack.va_code_Push_Secret", "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_stackTaint", "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins", "typing_Vale.X64.Machine_Semantics_s.update_rsp_", "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_Vale.X64.State.update_reg", "typing_Vale.X64.StateLemmas.state_to_S", "typing_tok_Vale.Arch.HeapTypes_s.Public@tok", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok", "unit_typing" ], 0, "3bc3db7d7621d18e6ce216bfcfad6d5f" ], [ "Vale.X64.InsStack.va_wpProof_Push_Secret", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.InsStack.va_wp_Push_Secret", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.Stack_i.init_rsp", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.Stack_i.store_taint_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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_tok_Vale.Arch.HeapTypes_s.Secret@tok", "unit_typing" ], 0, "72081cc439d316698f9f9a9db32262a7" ], [ "Vale.X64.InsStack.va_quick_Push_Secret", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.X64.Decls.va_fuel", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "7523e016407c3dcc1e632e45d72d98dc" ], [ "Vale.X64.InsStack.va_code_Load64_stack", 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, "1009b48b632fddf2d957c0590cac13ae" ], [ "Vale.X64.InsStack.va_lemma_Load64_stack", 1, 2, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented", "@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_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_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_3862c4e8ff39bfc3871b6a47e7ff5b2e", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.X64.Flags_interpretation_Tm_arrow_c9f84314ba6aade3760e20965d165b65", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_2eb22b38a6da10fb966327d892d8131d", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_798f93baee047c0793beddf8ae4ab551", "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_b72d599fc3c0eb1fc86c5d80a692be46", "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", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Pervasives.Native.Mktuple2", "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.Bytes_Code_s.Instr", "constructor_distinct_Vale.X64.Instruction_s.IOp64", "constructor_distinct_Vale.X64.Instruction_s.IOpEx", "constructor_distinct_Vale.X64.Instruction_s.Out", "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags", "constructor_distinct_Vale.X64.Machine_Semantics_s.AnnotateNone", "constructor_distinct_Vale.X64.Machine_s.Ins", "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_Prims.Cons", "data_elim_Vale.X64.Bytes_Code_s.Instr", "data_elim_Vale.X64.Instruction_s.InstrTypeRecord", "data_elim_Vale.X64.Machine_Semantics_s.Machine_stack", "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state", "data_elim_Vale.X64.Machine_s.Ins", "data_elim_Vale.X64.Machine_s.MemAccess", "data_elim_Vale.X64.Machine_s.OReg", "data_elim_Vale.X64.State.Mkvale_state", "data_typing_intro_Prims.Nil@tok", "data_typing_intro_Vale.X64.Instruction_s.InstrTypeRecord@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Vale.X64.Machine_s.Ins", "disc_equation_Vale.X64.Machine_s.OReg", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equality_tok_Vale.X64.Instruction_s.IOp64@tok", "equality_tok_Vale.X64.Instruction_s.Out@tok", "equality_tok_Vale.X64.Instruction_s.PreserveFlags@tok", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_FStar.Option.mapTot", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Arch.HeapTypes_s.memTaint_t", "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.Decls.eval_code", "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_is_dst_opr64", "equation_Vale.X64.Decls.va_operand_reg_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Flags.sel_curry", "equation_Vale.X64.Flags.to_fun", "equation_Vale.X64.Instruction_s.instr_dep", "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.Instructions_s.eval_Mov64", "equation_Vale.X64.Lemmas.eval_ins", "equation_Vale.X64.Machine_Semantics_s.apply_option", "equation_Vale.X64.Machine_Semantics_s.bind_option", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.eval_instr", "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.ins", "equation_Vale.X64.Machine_Semantics_s.instr_apply_eval", "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit", "equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit", "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.obs_operand_explicit", "equation_Vale.X64.Machine_Semantics_s.ocmp", "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.state_or_fail", "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.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_to_int", "equation_Vale.X64.Memory.memtaint", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.Stack_i.valid_src_stack64", "equation_Vale.X64.Stack_i.valid_taint_stack64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.valid_src_operand", "equation_Vale.X64.StateLemmas.state_of_S", "equation_Vale.X64.StateLemmas.state_to_S", "equation_Vale.X64.Taint_Semantics.mk_ins", "equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented", "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_operands_t_args.fuel_instrumented", "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented", "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "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.reg", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.int", "function_token_typing_Prims.unit", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.X64.Flags.sel_curry", "function_token_typing_Vale.X64.Instruction_s.instr_out", "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st", "function_token_typing_Vale.X64.Machine_s.t_reg", "function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion", "int_typing", "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659", "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821", "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749", "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e", "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0", "interpretation_Tm_abs_d7e539669515a49f97544a169303f779", "interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "kinding_FStar.Pervasives.Native.tuple2@tok", "kinding_Vale.Arch.HeapTypes_s.taint@tok", "kinding_Vale.X64.Instruction_s.instr_operand@tok", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "kinding_Vale.X64.Machine_s.reg@tok", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_Vale.Lib.Map16.lemma_equal_intro", "lemma_Vale.X64.Flags.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_upd_eq", "lemma_Vale.X64.Regs.lemma_upd_ne", "lemma_Vale.X64.Stack_Sems.equiv_load_stack64", "lemma_Vale.X64.Stack_Sems.equiv_valid_src_stack64", "lemma_Vale.X64.Stack_Sems.lemma_stack_from_to", "lemma_Vale.X64.StateLemmas.lemma_to_eval_operand", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "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", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace", "proj_equation_Vale.X64.Machine_s.OReg_r", "proj_equation_Vale.X64.Machine_s.Reg_rf", "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.Mktuple2__b", "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.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.IOpEx__0", "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", "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.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", "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_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_423a970236765465eb8eb63b6e1b8f53", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55", "refinement_interpretation_Tm_refine_a51eae56a5c39d95827d04b5f0544d43", "refinement_interpretation_Tm_refine_c2c488db3214c38826155caf10d30036", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64", "token_correspondence_Vale.X64.Flags.sel_curry", "token_correspondence_Vale.X64.Instructions_s.eval_Mov64", "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "token_correspondence_Vale.X64.Machine_Semantics_s.instr_annotation@tok", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "token_correspondence_Vale.X64.Machine_s.t_reg", "true_interp", "typing_FStar.Map.sel", "typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2", "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba", "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749", "typing_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e", "typing_Tm_abs_aee666efb78d12d75e614f775e4a068c", "typing_Tm_abs_f086d77986b470aab4bfebc171e6c366", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.Arch.MachineHeap_s.valid_addr64", "typing_Vale.X64.Decls.update_operand", "typing_Vale.X64.Decls.va_is_dst_opr64", "typing_Vale.X64.Flags.of_fun", "typing_Vale.X64.InsStack.va_code_Load64_stack", "typing_Vale.X64.Instruction_s.instr_eval", "typing_Vale.X64.Instructions_s.ins_Mov64", "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.apply_option", "typing_Vale.X64.Machine_Semantics_s.eval_instr", "typing_Vale.X64.Machine_Semantics_s.eval_operand", "typing_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts", "typing_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit", "typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit", "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins", "typing_Vale.X64.Machine_Semantics_s.match_n", "typing_Vale.X64.Machine_Semantics_s.obs_operand_explicit", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "typing_Vale.X64.Machine_s.operand64", "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_Sems.stack_to_s", "typing_Vale.X64.Stack_i.valid_src_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint", "typing_Vale.X64.StateLemmas.state_to_S", "typing_tok_Vale.X64.Instruction_s.IOp64@tok", "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok", "unit_inversion", "unit_typing" ], 0, "4c19025abb224844fabf55d623cf45b3" ], [ "Vale.X64.InsStack.va_wpProof_Load64_stack", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "@fuel_irrelevance_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Vale.X64.QuickCode.Mod_reg", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Nil@tok", "equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_is_dst_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_operand_dst_opr64", "equation_Vale.X64.InsStack.va_wp_Load64_stack", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.update_state_mod", "equation_Vale.X64.QuickCode.va_mod_dst_opr64", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "kinding_Vale.X64.QuickCode.mod_t@tok", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "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.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "projection_inverse_Vale.X64.QuickCode.Mod_reg__0", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.Decls.update_operand", "typing_Vale.X64.Decls.va_is_dst_opr64", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.QuickCode.va_mod_dst_opr64", "typing_Vale.X64.Stack_i.load_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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_tok_Vale.X64.QuickCode.Mod_None@tok", "unit_typing" ], 0, "87d8171569f475f3c909f6c962b6090b" ], [ "Vale.X64.InsStack.va_quick_Load64_stack", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.X64.Decls.va_fuel", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "c1e0d98c67c2b8d56c2d0835130c1bb1" ], [ "Vale.X64.InsStack.va_lemma_PushXmm", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Vale.X64.Machine_s.Block", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Prims.Cons", "disc_equation_Vale.X64.Machine_s.Block", "disc_equation_Vale.X64.Machine_s.OReg", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.state_inv", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_is_dst_opr64", "equation_Vale.X64.Decls.va_operand_reg_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Machine_Semantics_s.ins", "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.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Stack_i.store_stack64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat64", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_upd_eq", "lemma_Vale.X64.Regs.lemma_upd_ne", "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Block_block", "proj_equation_Vale.X64.Machine_s.OReg_r", "proj_equation_Vale.X64.Machine_s.Reg_rf", "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_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Vale.X64.Machine_s.Block_block", "projection_inverse_Vale.X64.Machine_s.Block_t_ins", "projection_inverse_Vale.X64.Machine_s.Block_t_ocmp", "projection_inverse_Vale.X64.Machine_s.Reg_r", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "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_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_e7e8c9464c24212d7cc1d1b3047a8440", "refinement_kinding_Tm_refine_c365eb902b454950de62fba701d9049d", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Decls.update_operand", "typing_Vale.X64.Decls.va_is_dst_opr64", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_stack", "typing_Vale.X64.Decls.va_upd_stackTaint", "typing_Vale.X64.Machine_s.__proj__OReg__item__r", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.Stack_i.store_stack64", "typing_Vale.X64.Stack_i.store_taint_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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.State.eval_operand", "typing_Vale.X64.State.update_reg", "typing_tok_Vale.Arch.HeapTypes_s.Public@tok" ], 0, "4d5bd62d65d88cbc86626669e4fdafcd" ], [ "Vale.X64.InsStack.va_wpProof_PushXmm", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2", "bool_inversion", "constructor_distinct_Prims.Nil", "constructor_distinct_Vale.X64.QuickCode.Mod_None", "constructor_distinct_Vale.X64.QuickCode.Mod_reg", "data_typing_intro_Prims.Nil@tok", "disc_equation_Vale.X64.Machine_s.OReg", "equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_operand_reg_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_operand_reg_opr64", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.InsStack.va_wp_PushXmm", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.Stack_i.init_rsp", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "kinding_Vale.X64.QuickCode.mod_t@tok", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "primitive_Prims.op_Equality", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "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.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Prims.Nil_a", "projection_inverse_Vale.X64.QuickCode.Mod_reg__0", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Decls.update_operand", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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.State.eval_operand", "typing_tok_Vale.X64.QuickCode.Mod_None@tok", "unit_typing" ], 0, "ae3ab00f533f044ea830c7f62925fefc" ], [ "Vale.X64.InsStack.va_quick_PushXmm", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.X64.Decls.va_fuel", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "d987174b7f5c139e41e1b8c6650e136f" ], [ "Vale.X64.InsStack.va_lemma_PopXmm", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Vale.X64.Machine_s.Block", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Prims.Cons", "disc_equation_Vale.X64.Machine_s.Block", "disc_equation_Vale.X64.Machine_s.OReg", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.state_inv", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_is_dst_opr64", "equation_Vale.X64.Decls.va_operand_reg_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.valid_operand", "equation_Vale.X64.Machine_Semantics_s.free_stack_", "equation_Vale.X64.Machine_Semantics_s.ins", "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.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Stack_i.free_stack64", "equation_Vale.X64.Stack_i.init_rsp", "equation_Vale.X64.Stack_i.valid_src_stack64", "equation_Vale.X64.Stack_i.valid_taint_stack64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "equation_Vale.X64.State.valid_src_operand", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat64", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_upd_eq", "lemma_Vale.X64.Regs.lemma_upd_ne", "lemma_Vale.X64.Stack_i.lemma_compose_free_stack64", "lemma_Vale.X64.Stack_i.lemma_free_stack_same_load64", "lemma_Vale.X64.Stack_i.lemma_free_stack_same_valid64", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp", "proj_equation_Vale.X64.Machine_s.Block_block", "proj_equation_Vale.X64.Machine_s.OReg_r", "proj_equation_Vale.X64.Machine_s.Reg_rf", "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_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp", "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.Reg_rf", "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_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_3cd7fcef26b89f34f3c6fbae0545ada5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_e7e8c9464c24212d7cc1d1b3047a8440", "refinement_kinding_Tm_refine_c365eb902b454950de62fba701d9049d", "true_interp", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Decls.update_operand", "typing_Vale.X64.Decls.va_is_dst_opr64", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Decls.va_upd_stack", "typing_Vale.X64.InsStack.va_code_Pop", "typing_Vale.X64.InsStack.va_lemma_Pop", "typing_Vale.X64.Machine_s.__proj__OReg__item__r", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.Stack_i.free_stack64", "typing_Vale.X64.Stack_i.load_stack64", "typing_Vale.X64.Stack_i.valid_src_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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.update_reg", "typing_Vale.X64.State.update_reg_xmm" ], 0, "c886d2cc4096b2fa8c8ea48ca8234023" ], [ "Vale.X64.InsStack.va_wpProof_PopXmm", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "@fuel_irrelevance_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Vale.X64.QuickCode.Mod_None", "constructor_distinct_Vale.X64.QuickCode.Mod_reg", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Nil@tok", "disc_equation_Vale.X64.Machine_s.OReg", "equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "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.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_operand_reg_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_operand_reg_opr64", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.InsStack.va_wp_PopXmm", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.update_state_mod", "equation_Vale.X64.QuickCode.va_mod_xmm", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.Stack_i.free_stack64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "kinding_Vale.X64.QuickCode.mod_t@tok", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Stack_Sems.equiv_init_rsp", "primitive_Prims.op_Equality", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "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.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "projection_inverse_Vale.X64.QuickCode.Mod_reg__0", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Decls.update_operand", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.QuickCode.va_mod_xmm", "typing_Vale.X64.Stack_i.free_stack64", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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.eval_operand", "typing_Vale.X64.State.update_reg_xmm", "typing_tok_Vale.X64.QuickCode.Mod_None@tok", "unit_typing" ], 0, "36f6d971255dcaa5929bb0d0c789bd01" ], [ "Vale.X64.InsStack.va_quick_PopXmm", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.X64.Decls.va_fuel", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "8e5dbcf0c9be9afee1234acfae674f92" ], [ "Vale.X64.InsStack.va_lemma_PushXmm_Secret", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Vale.X64.Machine_s.Block", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Prims.Cons", "disc_equation_Vale.X64.Machine_s.Block", "disc_equation_Vale.X64.Machine_s.OReg", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.state_inv", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_is_dst_opr64", "equation_Vale.X64.Decls.va_operand_reg_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Machine_Semantics_s.ins", "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.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Stack_i.store_stack64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat64", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_upd_eq", "lemma_Vale.X64.Regs.lemma_upd_ne", "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_s.Block_block", "proj_equation_Vale.X64.Machine_s.OReg_r", "proj_equation_Vale.X64.Machine_s.Reg_rf", "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_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Vale.X64.Machine_s.Block_block", "projection_inverse_Vale.X64.Machine_s.Block_t_ins", "projection_inverse_Vale.X64.Machine_s.Block_t_ocmp", "projection_inverse_Vale.X64.Machine_s.Reg_r", "projection_inverse_Vale.X64.Machine_s.Reg_rf", "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_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_e7e8c9464c24212d7cc1d1b3047a8440", "refinement_kinding_Tm_refine_c365eb902b454950de62fba701d9049d", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Decls.update_operand", "typing_Vale.X64.Decls.va_is_dst_opr64", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_stack", "typing_Vale.X64.Decls.va_upd_stackTaint", "typing_Vale.X64.Machine_s.__proj__OReg__item__r", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.Stack_i.store_stack64", "typing_Vale.X64.Stack_i.store_taint_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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.State.eval_operand", "typing_Vale.X64.State.update_reg", "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok" ], 0, "1a5d31de2cc7177651d02213fd68e682" ], [ "Vale.X64.InsStack.va_wpProof_PushXmm_Secret", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2", "bool_inversion", "constructor_distinct_Prims.Nil", "constructor_distinct_Vale.X64.QuickCode.Mod_None", "constructor_distinct_Vale.X64.QuickCode.Mod_reg", "data_typing_intro_Prims.Nil@tok", "disc_equation_Vale.X64.Machine_s.OReg", "equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_operand_reg_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_operand_reg_opr64", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.InsStack.va_wp_PushXmm_Secret", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.Stack_i.init_rsp", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing", "kinding_Vale.X64.QuickCode.mod_t@tok", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "primitive_Prims.op_Equality", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "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.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Prims.Nil_a", "projection_inverse_Vale.X64.QuickCode.Mod_reg__0", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Decls.update_operand", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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.State.eval_operand", "typing_tok_Vale.X64.QuickCode.Mod_None@tok", "unit_typing" ], 0, "50e458aae859ace109d78f7a2e486140" ], [ "Vale.X64.InsStack.va_quick_PushXmm_Secret", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.X64.Decls.va_fuel", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "61a69924fbc01fecba6673cd72553c8e" ], [ "Vale.X64.InsStack.va_lemma_PopXmm_Secret", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Vale.X64.Machine_s.Block", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Prims.Cons", "disc_equation_Vale.X64.Machine_s.Block", "disc_equation_Vale.X64.Machine_s.OReg", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.state_inv", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_is_dst_opr64", "equation_Vale.X64.Decls.va_operand_reg_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.valid_operand", "equation_Vale.X64.Machine_Semantics_s.free_stack_", "equation_Vale.X64.Machine_Semantics_s.ins", "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.reg_xmm", "equation_Vale.X64.Machine_s.t_reg", "equation_Vale.X64.Machine_s.t_reg_file", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.Stack_i.free_stack64", "equation_Vale.X64.Stack_i.init_rsp", "equation_Vale.X64.Stack_i.valid_src_stack64", "equation_Vale.X64.Stack_i.valid_taint_stack64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "equation_Vale.X64.State.valid_src_operand", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.int", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "function_token_typing_Vale.Def.Words_s.nat64", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion", "int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_intro", "lemma_Vale.X64.Regs.lemma_upd_eq", "lemma_Vale.X64.Regs.lemma_upd_ne", "lemma_Vale.X64.Stack_i.lemma_compose_free_stack64", "lemma_Vale.X64.Stack_i.lemma_free_stack_same_load64", "lemma_Vale.X64.Stack_i.lemma_free_stack_same_valid64", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp", "proj_equation_Vale.X64.Machine_s.Block_block", "proj_equation_Vale.X64.Machine_s.OReg_r", "proj_equation_Vale.X64.Machine_s.Reg_rf", "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_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp", "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.Reg_rf", "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_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_3cd7fcef26b89f34f3c6fbae0545ada5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_e7e8c9464c24212d7cc1d1b3047a8440", "refinement_kinding_Tm_refine_c365eb902b454950de62fba701d9049d", "true_interp", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Decls.update_operand", "typing_Vale.X64.Decls.va_is_dst_opr64", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Decls.va_upd_stack", "typing_Vale.X64.InsStack.va_code_Pop_Secret", "typing_Vale.X64.InsStack.va_lemma_Pop_Secret", "typing_Vale.X64.Machine_s.__proj__OReg__item__r", "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd", "typing_Vale.X64.Stack_i.free_stack64", "typing_Vale.X64.Stack_i.load_stack64", "typing_Vale.X64.Stack_i.valid_src_stack64", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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.update_reg", "typing_Vale.X64.State.update_reg_xmm" ], 0, "0f4b19d7f8a040f034ab511816b03b43" ], [ "Vale.X64.InsStack.va_wpProof_PopXmm_Secret", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "@fuel_irrelevance_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Vale.X64.QuickCode.Mod_None", "constructor_distinct_Vale.X64.QuickCode.Mod_reg", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Nil@tok", "disc_equation_Vale.X64.Machine_s.OReg", "equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets", "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.CPU_Features_s.sse_enabled", "equation_Vale.X64.Decls.upd_register", "equation_Vale.X64.Decls.update_operand", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_operand_reg_opr64", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_operand_reg_opr64", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.InsStack.va_wp_PopXmm_Secret", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Machine_s.reg_xmm", "equation_Vale.X64.Memory.vale_full_heap_equal", "equation_Vale.X64.QuickCode.t_require", "equation_Vale.X64.QuickCode.update_state_mod", "equation_Vale.X64.QuickCode.va_mod_xmm", "equation_Vale.X64.QuickCode.va_t_ensure", "equation_Vale.X64.Stack_i.free_stack64", "equation_Vale.X64.State.eval_operand", "equation_Vale.X64.State.state_eq", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_inversion", "int_typing", "kinding_Vale.X64.QuickCode.mod_t@tok", "lemma_Vale.Lib.Map16.lemma_equal_elim", "lemma_Vale.X64.Flags.lemma_equal_elim", "lemma_Vale.X64.Regs.lemma_equal_elim", "lemma_Vale.X64.Stack_Sems.equiv_init_rsp", "primitive_Prims.op_Equality", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "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.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "projection_inverse_Vale.X64.QuickCode.Mod_reg__0", "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802", "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets", "typing_Vale.X64.CPU_Features_s.sse_enabled", "typing_Vale.X64.Decls.update_operand", "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.QuickCode.va_mod_xmm", "typing_Vale.X64.Stack_i.free_stack64", "typing_Vale.X64.Stack_i.init_rsp", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags", "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.eval_operand", "typing_Vale.X64.State.update_reg_xmm", "typing_tok_Vale.X64.QuickCode.Mod_None@tok", "unit_typing" ], 0, "895c31e8ff514c961d358bb63a19f91b" ], [ "Vale.X64.InsStack.va_quick_PopXmm_Secret", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.X64.Decls.va_fuel", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "3ca62bae7c88357c45a97ea4e42e4dce" ] ] ]