Revision 2fd16cc5351310efaa66a178d904ce978ad78b23 authored by Bryan Parno on 01 April 2019, 15:28:33 UTC, committed by Bryan Parno on 01 April 2019, 15:28:33 UTC
X64.Vale.InsStack.fst.hints
[
"����.A\r�\u0001�S��ӷ�",
[
[
"X64.Vale.InsStack.va_lemma_Pop",
1,
2,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
"Prims_interpretation_Tm_arrow_e06752ba152f81447b312efcdf8f0e23",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"X64.Bytes_Semantics_s_interpretation_Tm_arrow_17742a16dc7ea8ebf4db7d06d09f33c0",
"X64.Bytes_Semantics_s_interpretation_Tm_arrow_7c41dd7c95618d7271dfb9d558b1cdd8",
"X64.Bytes_Semantics_s_interpretation_Tm_arrow_ee7017858cc0d7eacce54d227f2089c3",
"X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
"X64.Machine_s_interpretation_Tm_arrow_196f8dfca6d67b0bd046e19b6a5a08e6",
"X64.Machine_s_pretyping_644ad5cdcea42fa4e9e52bbdd5021fb9",
"X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
"X64.Machine_s_pretyping_e51d9612683cb053e6b8236fad2673ca",
"X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
"bool_inversion", "bool_typing",
"constructor_distinct_FStar.Pervasives.Native.Mktuple2",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit",
"constructor_distinct_X64.Bytes_Semantics_s.Pop",
"constructor_distinct_X64.Machine_s.Ins",
"constructor_distinct_X64.Machine_s.MReg",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OMem",
"constructor_distinct_X64.Machine_s.OStack",
"constructor_distinct_X64.Machine_s.Rax",
"constructor_distinct_X64.Machine_s.Rsp",
"data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_Prims.Cons",
"data_elim_X64.Bytes_Semantics_s.Pop",
"data_elim_X64.Bytes_Semantics_s.Vale_stack",
"data_elim_X64.Machine_s.Ins", "data_elim_X64.Machine_s.OReg",
"data_elim_X64.Taint_Semantics_s.MktraceState",
"data_elim_X64.Taint_Semantics_s.TaintedIns",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_X64.Machine_s.Rbx@tok",
"data_typing_intro_X64.Machine_s.Secret@tok",
"disc_equation_X64.Bytes_Semantics_s.MOVDQU",
"disc_equation_X64.Bytes_Semantics_s.Mulx64",
"disc_equation_X64.Machine_s.Ins", "disc_equation_X64.Machine_s.Rsp",
"eq2-interp", "equality_tok_X64.Machine_s.Public@tok",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R11@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R13@tok",
"equality_tok_X64.Machine_s.R14@tok",
"equality_tok_X64.Machine_s.R15@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rbp@tok",
"equality_tok_X64.Machine_s.Rbx@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Rsp@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.List.Tot.Base.op_At",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.nat8",
"equation_Words_s.natN", "equation_X64.Bytes_Semantics_s.eval_ins",
"equation_X64.Bytes_Semantics_s.eval_maddr",
"equation_X64.Bytes_Semantics_s.eval_operand",
"equation_X64.Bytes_Semantics_s.free_stack",
"equation_X64.Bytes_Semantics_s.free_stack_",
"equation_X64.Bytes_Semantics_s.heap",
"equation_X64.Bytes_Semantics_s.st",
"equation_X64.Bytes_Semantics_s.update_operand_preserve_flags_",
"equation_X64.Bytes_Semantics_s.update_reg_",
"equation_X64.Bytes_Semantics_s.update_rsp_",
"equation_X64.Bytes_Semantics_s.valid_addr",
"equation_X64.Bytes_Semantics_s.valid_addr64",
"equation_X64.Bytes_Semantics_s.valid_dst_operand",
"equation_X64.Bytes_Semantics_s.valid_src_operand",
"equation_X64.Memory.memtaint",
"equation_X64.Taint_Semantics_s.extract_operands",
"equation_X64.Taint_Semantics_s.ins_obs",
"equation_X64.Taint_Semantics_s.operand_obs",
"equation_X64.Taint_Semantics_s.taint_eval_ins",
"equation_X64.Taint_Semantics_s.taint_match",
"equation_X64.Taint_Semantics_s.tainted_code",
"equation_X64.Taint_Semantics_s.update_taint",
"equation_X64.Vale.Decls.eval_code", "equation_X64.Vale.Decls.ins",
"equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_fuel",
"equation_X64.Vale.Decls.va_is_dst_opr64",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_stack",
"equation_X64.Vale.Decls.va_update_operand",
"equation_X64.Vale.InsStack.va_code_Pop",
"equation_X64.Vale.InsStack.va_transparent_code_Pop",
"equation_X64.Vale.Lemmas.eval_code",
"equation_X64.Vale.Lemmas.eval_ins",
"equation_X64.Vale.Lemmas.state_eq_S",
"equation_X64.Vale.Lemmas.state_eq_opt",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.valid_src_operand",
"equation_X64.Vale.StateLemmas.state_of_S",
"equation_X64.Vale.StateLemmas.state_to_S",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_X64.Bytes_Semantics_s.stack",
"fuel_guarded_inversion_X64.Bytes_Semantics_s.state",
"fuel_guarded_inversion_X64.Machine_s.reg",
"fuel_guarded_inversion_X64.Vale.Decls.tainted_operand",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
"function_token_typing_X64.Bytes_Semantics_s.free_stack",
"int_inversion", "int_typing",
"interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
"interpretation_Tm_abs_2fb25da66629b4ba64599cd5cd247317",
"interpretation_Tm_abs_4b95600523a97e68234eb97dde49e42a",
"interpretation_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
"interpretation_Tm_abs_74722fb662ef15cb6b81bf92b6bcee49",
"interpretation_Tm_abs_e4bbf0f30784e534db44e144328c14b5",
"interpretation_Tm_abs_f898ec4003bb089e0c1a55048fa7a11c",
"kinding_X64.Machine_s.observation@tok",
"kinding_X64.Machine_s.operand@tok", "kinding_X64.Machine_s.reg@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_FStar.List.Tot.Properties.append_l_nil",
"lemma_X64.Memory_Sems.get_hs_heap",
"lemma_X64.Stack_Sems.equiv_free_stack",
"lemma_X64.Stack_Sems.equiv_init_rsp",
"lemma_X64.Stack_Sems.equiv_load_stack64",
"lemma_X64.Stack_Sems.equiv_valid_src_stack64",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Regs.lemma_upd_eq",
"lemma_X64.Vale.Regs.lemma_upd_ne",
"lemma_X64.Vale.StateLemmas.lemma_to_eval_operand",
"lemma_X64.Vale.StateLemmas.lemma_to_flags",
"lemma_X64.Vale.StateLemmas.lemma_to_memTaint",
"lemma_X64.Vale.StateLemmas.lemma_to_ok",
"lemma_X64.Vale.StateLemmas.lemma_to_reg",
"lemma_X64.Vale.StateLemmas.lemma_to_trace",
"lemma_X64.Vale.StateLemmas.lemma_to_xmm",
"lemma_X64.Vale.Xmms.lemma_equal_intro", "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_X64.Bytes_Semantics_s.Mkstate_flags",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_stack",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
"proj_equation_X64.Bytes_Semantics_s.Vale_stack_initial_rsp",
"proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
"proj_equation_X64.Taint_Semantics_s.MktraceState_state",
"proj_equation_X64.Taint_Semantics_s.MktraceState_trace",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"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_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_stack",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
"projection_inverse_X64.Bytes_Semantics_s.Pop_dst",
"projection_inverse_X64.Bytes_Semantics_s.Vale_stack_initial_rsp",
"projection_inverse_X64.Machine_s.Ins_ins",
"projection_inverse_X64.Machine_s.Ins_t_ins",
"projection_inverse_X64.Machine_s.Ins_t_ocmp",
"projection_inverse_X64.Machine_s.MReg_offset",
"projection_inverse_X64.Machine_s.MReg_r",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Machine_s.OStack_m",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
"projection_inverse_X64.Taint_Semantics_s.TaintedIns_i",
"projection_inverse_X64.Taint_Semantics_s.TaintedIns_t",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2c90c44e0c3d494a57f4a23c91ef834a",
"refinement_interpretation_Tm_refine_33d3ef68371378c171a37d999106817a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4c6411da037541583c16876f5cc7dfe4",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"token_correspondence_X64.Bytes_Semantics_s.eval_ins",
"token_correspondence_X64.Bytes_Semantics_s.free_stack",
"true_interp", "typing_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
"typing_Tm_abs_91d6891d766466e9703afb13e7f1a1bf",
"typing_Tm_abs_e4bbf0f30784e534db44e144328c14b5",
"typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__ok",
"typing_X64.Bytes_Semantics_s.eval_operand",
"typing_X64.Bytes_Semantics_s.get_heap_val64",
"typing_X64.Bytes_Semantics_s.update_operand_preserve_flags_",
"typing_X64.Bytes_Semantics_s.update_rsp_",
"typing_X64.Bytes_Semantics_s.valid_addr",
"typing_X64.Stack_Sems.stack_to_s", "typing_X64.Stack_i.init_rsp",
"typing_X64.Stack_i.valid_src_stack64",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__i",
"typing_X64.Taint_Semantics_s.extract_operands",
"typing_X64.Taint_Semantics_s.ins_obs",
"typing_X64.Taint_Semantics_s.operand_obs",
"typing_X64.Taint_Semantics_s.operand_obs_list",
"typing_X64.Vale.Decls.va_is_dst_opr64",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_stack",
"typing_X64.Vale.Decls.va_update_operand",
"typing_X64.Vale.InsStack.va_transparent_code_Pop",
"typing_X64.Vale.Regs.of_fun", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__stack",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.StateLemmas.state_to_S",
"typing_tok_X64.Machine_s.Public@tok",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R11@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R13@tok",
"typing_tok_X64.Machine_s.R14@tok",
"typing_tok_X64.Machine_s.R15@tok",
"typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rbp@tok",
"typing_tok_X64.Machine_s.Rbx@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"e761370039a03ea77c51838d34920f53"
],
[
"X64.Vale.InsStack.va_wpMonotone_Pop",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_X64.Machine_s.Rsp@tok",
"equation_X64.Vale.InsStack.va_wp_Pop",
"fuel_guarded_inversion_X64.Vale.State.state",
"typing_X64.Vale.Decls.va_upd_operand_dst_opr64",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_stack",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"617ab98e6900cbc5260d1f7897307d54"
],
[
"X64.Vale.InsStack.va_wpCompute_Pop",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.InsStack.va_code_Pop",
"equation_X64.Vale.InsStack.va_wp_Pop",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"8f44c58eee838160aa8f13a5e9ac9c07"
],
[
"X64.Vale.InsStack.va_wpProof_Pop",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"e9b57e828c137ab8c33a0023086f66b5"
],
[
"X64.Vale.InsStack.va_wpProof_Pop",
2,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"X64.Vale.QuickCode_pretyping_5ef17715065c7f9c7618e13aa923e84c",
"bool_inversion", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OMem",
"constructor_distinct_X64.Machine_s.OStack",
"constructor_distinct_X64.Vale.QuickCode.Mod_reg",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equality_tok_X64.Machine_s.Rsp@tok",
"equality_tok_X64.Vale.QuickCode.Mod_None@tok", "equation_Prims.nat",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_fuel",
"equation_X64.Vale.Decls.va_is_dst_opr64",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_operand_dst_opr64",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_stack",
"equation_X64.Vale.Decls.va_update_operand",
"equation_X64.Vale.InsStack.va_code_Pop",
"equation_X64.Vale.InsStack.va_wpCompute_Pop",
"equation_X64.Vale.InsStack.va_wp_Pop",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.eval_operand",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_with_fuel_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"kinding_X64.Vale.QuickCode.mod_t@tok",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.StateLemmas.lemma_to_flags",
"lemma_X64.Vale.StateLemmas.lemma_to_ok",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"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_X64.Machine_s.OReg_r",
"projection_inverse_X64.Vale.QuickCode.Mod_reg__0",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"token_correspondence_X64.Vale.InsStack.va_wpCompute_Pop",
"typing_X64.Stack_i.free_stack64", "typing_X64.Stack_i.load_stack64",
"typing_X64.Vale.Decls.va_is_dst_opr64",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_update_operand",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__stack",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_tok_X64.Machine_s.Rsp@tok",
"typing_tok_X64.Vale.QuickCode.Mod_None@tok", "unit_typing"
],
0,
"361b34b56dfff66c4fa2d3ebc8b7bdba"
],
[
"X64.Vale.InsStack.va_lemma_Push",
1,
2,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
"@fuel_irrelevance_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
"Prims_interpretation_Tm_arrow_e06752ba152f81447b312efcdf8f0e23",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"X64.Bytes_Semantics_s_interpretation_Tm_arrow_ee7017858cc0d7eacce54d227f2089c3",
"X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
"X64.Machine_s_interpretation_Tm_arrow_196f8dfca6d67b0bd046e19b6a5a08e6",
"X64.Machine_s_pretyping_644ad5cdcea42fa4e9e52bbdd5021fb9",
"X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
"X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
"bool_inversion", "bool_typing",
"constructor_distinct_FStar.Pervasives.Native.Mktuple2",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit",
"constructor_distinct_X64.Bytes_Semantics_s.Push",
"constructor_distinct_X64.Machine_s.Ins",
"constructor_distinct_X64.Machine_s.MConst",
"constructor_distinct_X64.Machine_s.OStack",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_X64.Bytes_Semantics_s.Push",
"data_elim_X64.Machine_s.Ins",
"data_elim_X64.Taint_Semantics_s.MktraceState",
"data_elim_X64.Taint_Semantics_s.TaintedIns",
"data_typing_intro_X64.Machine_s.MConst@tok",
"data_typing_intro_X64.Machine_s.OStack@tok",
"data_typing_intro_X64.Machine_s.Rbx@tok",
"disc_equation_X64.Bytes_Semantics_s.MOVDQU",
"disc_equation_X64.Bytes_Semantics_s.Mulx64",
"disc_equation_X64.Machine_s.Ins",
"disc_equation_X64.Machine_s.OReg", "eq2-interp",
"equality_tok_X64.Machine_s.Public@tok",
"equality_tok_X64.Machine_s.Rsp@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_FStar.List.Tot.Base.op_At",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.nat8",
"equation_Words_s.natN", "equation_X64.Bytes_Semantics_s.eval_ins",
"equation_X64.Bytes_Semantics_s.eval_maddr",
"equation_X64.Bytes_Semantics_s.eval_operand",
"equation_X64.Bytes_Semantics_s.regs_t",
"equation_X64.Bytes_Semantics_s.update_operand_preserve_flags_",
"equation_X64.Bytes_Semantics_s.update_reg_",
"equation_X64.Bytes_Semantics_s.update_rsp_",
"equation_X64.Bytes_Semantics_s.update_stack",
"equation_X64.Bytes_Semantics_s.valid_dst_operand",
"equation_X64.Bytes_Semantics_s.valid_src_operand",
"equation_X64.Memory.memtaint",
"equation_X64.Taint_Semantics_s.extract_operands",
"equation_X64.Taint_Semantics_s.ins_obs",
"equation_X64.Taint_Semantics_s.operand_obs",
"equation_X64.Taint_Semantics_s.taint_eval_ins",
"equation_X64.Taint_Semantics_s.taint_match",
"equation_X64.Taint_Semantics_s.tainted_code",
"equation_X64.Vale.Decls.eval_code", "equation_X64.Vale.Decls.ins",
"equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_fuel",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_stack",
"equation_X64.Vale.InsStack.va_code_Push",
"equation_X64.Vale.InsStack.va_transparent_code_Push",
"equation_X64.Vale.Lemmas.eval_code",
"equation_X64.Vale.Lemmas.eval_ins",
"equation_X64.Vale.Lemmas.state_eq_S",
"equation_X64.Vale.Lemmas.state_eq_opt",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.valid_src_operand",
"equation_X64.Vale.StateLemmas.state_of_S",
"equation_X64.Vale.StateLemmas.state_to_S",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_X64.Bytes_Semantics_s.state",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
"int_inversion", "int_typing",
"interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
"interpretation_Tm_abs_4b95600523a97e68234eb97dde49e42a",
"interpretation_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
"interpretation_Tm_abs_718bd6c33b1a0b2a022bbb46f99b3434",
"interpretation_Tm_abs_74722fb662ef15cb6b81bf92b6bcee49",
"interpretation_Tm_abs_e4bbf0f30784e534db44e144328c14b5",
"kinding_X64.Machine_s.observation@tok",
"kinding_X64.Machine_s.reg@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_FStar.List.Tot.Properties.append_l_nil",
"lemma_X64.Memory_Sems.get_hs_heap",
"lemma_X64.Stack_Sems.equiv_init_rsp",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Regs.lemma_upd_eq",
"lemma_X64.Vale.Regs.lemma_upd_ne",
"lemma_X64.Vale.StateLemmas.lemma_to_eval_operand",
"lemma_X64.Vale.StateLemmas.lemma_to_flags",
"lemma_X64.Vale.StateLemmas.lemma_to_memTaint",
"lemma_X64.Vale.StateLemmas.lemma_to_ok",
"lemma_X64.Vale.StateLemmas.lemma_to_reg",
"lemma_X64.Vale.StateLemmas.lemma_to_trace",
"lemma_X64.Vale.StateLemmas.lemma_to_xmm",
"lemma_X64.Vale.Xmms.lemma_equal_intro", "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_X64.Bytes_Semantics_s.Mkstate_flags",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_stack",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
"proj_equation_X64.Bytes_Semantics_s.Vale_stack_initial_rsp",
"proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
"proj_equation_X64.Taint_Semantics_s.MktraceState_state",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"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_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_stack",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
"projection_inverse_X64.Bytes_Semantics_s.Push_src",
"projection_inverse_X64.Machine_s.Ins_ins",
"projection_inverse_X64.Machine_s.Ins_t_ins",
"projection_inverse_X64.Machine_s.Ins_t_ocmp",
"projection_inverse_X64.Machine_s.MConst_n",
"projection_inverse_X64.Machine_s.OStack_m",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
"projection_inverse_X64.Taint_Semantics_s.TaintedIns_i",
"projection_inverse_X64.Taint_Semantics_s.TaintedIns_t",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2c90c44e0c3d494a57f4a23c91ef834a",
"refinement_interpretation_Tm_refine_33d3ef68371378c171a37d999106817a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_b0ec1ad4c766f179179881d04d9cace4",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"token_correspondence_X64.Bytes_Semantics_s.eval_ins", "true_interp",
"typing_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
"typing_Tm_abs_91d6891d766466e9703afb13e7f1a1bf",
"typing_Tm_abs_e4bbf0f30784e534db44e144328c14b5",
"typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__ok",
"typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"typing_X64.Bytes_Semantics_s.update_operand_preserve_flags_",
"typing_X64.Bytes_Semantics_s.update_rsp_",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__trace",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__i",
"typing_X64.Taint_Semantics_s.extract_operands",
"typing_X64.Taint_Semantics_s.ins_obs",
"typing_X64.Taint_Semantics_s.operand_obs_list",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_stack",
"typing_X64.Vale.InsStack.va_transparent_code_Push",
"typing_X64.Vale.Regs.of_fun", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__stack",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.StateLemmas.state_to_S",
"typing_tok_X64.Machine_s.Public@tok",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"351570897d470116f33e95f7d70b4135"
],
[
"X64.Vale.InsStack.va_wpMonotone_Push",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_X64.Machine_s.Rsp@tok",
"equation_X64.Vale.Decls.va_operand_reg_opr64",
"equation_X64.Vale.InsStack.va_wp_Push",
"fuel_guarded_inversion_X64.Vale.State.state",
"refinement_interpretation_Tm_refine_93c4793e88ba66df1f803c1610135c3a",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_stack",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"1f0cf4bbf4a2d864b08aca08afde6a70"
],
[
"X64.Vale.InsStack.va_wpCompute_Push",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.InsStack.va_code_Push",
"equation_X64.Vale.InsStack.va_wp_Push",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"eb52ae8e689356bc5e4937e1191e4b1e"
],
[
"X64.Vale.InsStack.va_wpProof_Push",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"7ec0ede03354f4a5cfaa581ca67c2ace"
],
[
"X64.Vale.InsStack.va_wpProof_Push",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Tm_unit",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OMem",
"constructor_distinct_X64.Machine_s.OStack",
"disc_equation_X64.Machine_s.OReg", "eq2-interp",
"equality_tok_X64.Machine_s.Rsp@tok", "equation_Prims.nat",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_fuel",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_stack",
"equation_X64.Vale.InsStack.va_code_Push",
"equation_X64.Vale.InsStack.va_wpCompute_Push",
"equation_X64.Vale.InsStack.va_wp_Push",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"fuel_guarded_inversion_X64.Vale.State.state",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.StateLemmas.lemma_to_flags",
"lemma_X64.Vale.StateLemmas.lemma_to_ok",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"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_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"token_correspondence_X64.Vale.InsStack.va_wpCompute_Push",
"typing_X64.Vale.Decls.va_upd_ok", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__stack",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"4260524181183c0368133cd61f299ac2"
],
[
"X64.Vale.InsStack.va_lemma_Load64_stack",
1,
2,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
"Prims_interpretation_Tm_arrow_e06752ba152f81447b312efcdf8f0e23",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"X64.Bytes_Semantics_s_interpretation_Tm_arrow_cae2832fffdb5334dc1643f5adf1cfcf",
"X64.Bytes_Semantics_s_interpretation_Tm_arrow_ee7017858cc0d7eacce54d227f2089c3",
"X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
"X64.Machine_s_interpretation_Tm_arrow_196f8dfca6d67b0bd046e19b6a5a08e6",
"X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
"X64.Machine_s_pretyping_e51d9612683cb053e6b8236fad2673ca",
"X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
"X64.Vale.Decls_pretyping_f7549fd7938feffd48aa91731aea2868",
"bool_inversion", "bool_typing",
"constructor_distinct_FStar.Pervasives.Native.Mktuple2",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit",
"constructor_distinct_X64.Bytes_Semantics_s.Mov64",
"constructor_distinct_X64.Machine_s.Ins",
"constructor_distinct_X64.Machine_s.MReg",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OMem",
"constructor_distinct_X64.Machine_s.OStack",
"constructor_distinct_X64.Vale.Decls.TStack",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_X64.Bytes_Semantics_s.Vale_stack",
"data_elim_X64.Taint_Semantics_s.MktraceState",
"data_elim_X64.Vale.Decls.TReg", "data_typing_intro_Prims.Nil@tok",
"data_typing_intro_X64.Machine_s.MReg@tok",
"data_typing_intro_X64.Machine_s.OReg@tok",
"data_typing_intro_X64.Machine_s.OStack@tok",
"data_typing_intro_X64.Machine_s.Rbx@tok",
"data_typing_intro_X64.Machine_s.Secret@tok",
"data_typing_intro_X64.Taint_Semantics_s.TaintedIns@tok",
"data_typing_intro_X64.Vale.Decls.TStack@tok",
"disc_equation_X64.Bytes_Semantics_s.MOVDQU",
"disc_equation_X64.Bytes_Semantics_s.Mulx64",
"disc_equation_X64.Machine_s.Ins",
"disc_equation_X64.Machine_s.OReg",
"disc_equation_X64.Machine_s.Rsp",
"disc_equation_X64.Vale.Decls.TMem", "eq2-interp",
"equality_tok_X64.Bytes_Semantics_s.Mov64@tok",
"equality_tok_X64.Machine_s.Public@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.List.Tot.Base.op_At",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.nat8",
"equation_X64.Bytes_Semantics_s.eval_ins",
"equation_X64.Bytes_Semantics_s.eval_maddr",
"equation_X64.Bytes_Semantics_s.eval_operand",
"equation_X64.Bytes_Semantics_s.heap",
"equation_X64.Bytes_Semantics_s.update_operand_preserve_flags_",
"equation_X64.Bytes_Semantics_s.update_reg_",
"equation_X64.Bytes_Semantics_s.valid_addr",
"equation_X64.Bytes_Semantics_s.valid_addr64",
"equation_X64.Bytes_Semantics_s.valid_dst_operand",
"equation_X64.Bytes_Semantics_s.valid_src_operand",
"equation_X64.Memory.memtaint",
"equation_X64.Taint_Semantics.mk_taint_ins2",
"equation_X64.Taint_Semantics_s.extract_operands",
"equation_X64.Taint_Semantics_s.ins_obs",
"equation_X64.Taint_Semantics_s.operand_obs",
"equation_X64.Taint_Semantics_s.taint_eval_ins",
"equation_X64.Taint_Semantics_s.taint_match",
"equation_X64.Taint_Semantics_s.update_taint",
"equation_X64.Vale.Decls.eval_code",
"equation_X64.Vale.Decls.extract_taint",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_fuel",
"equation_X64.Vale.Decls.va_is_dst_opr64",
"equation_X64.Vale.Decls.va_operand_reg_opr64",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_update_operand",
"equation_X64.Vale.InsStack.va_code_Load64_stack",
"equation_X64.Vale.InsStack.va_transparent_code_Load64_stack",
"equation_X64.Vale.Lemmas.eval_code",
"equation_X64.Vale.Lemmas.eval_ins",
"equation_X64.Vale.Lemmas.state_eq_S",
"equation_X64.Vale.Lemmas.state_eq_opt",
"equation_X64.Vale.State.eval_operand",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.valid_src_operand",
"equation_X64.Vale.StateLemmas.state_of_S",
"equation_X64.Vale.StateLemmas.state_to_S",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
"fuel_guarded_inversion_X64.Bytes_Semantics_s.stack",
"fuel_guarded_inversion_X64.Bytes_Semantics_s.state",
"fuel_guarded_inversion_X64.Vale.Decls.tainted_operand",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
"int_inversion", "int_typing",
"interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
"interpretation_Tm_abs_3063697254a516954d0ad94bfd65dc7b",
"interpretation_Tm_abs_4b95600523a97e68234eb97dde49e42a",
"interpretation_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
"interpretation_Tm_abs_74722fb662ef15cb6b81bf92b6bcee49",
"interpretation_Tm_abs_e4bbf0f30784e534db44e144328c14b5",
"kinding_X64.Machine_s.observation@tok",
"kinding_X64.Machine_s.operand@tok", "kinding_X64.Machine_s.reg@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_FStar.List.Tot.Properties.append_l_nil",
"lemma_X64.Memory_Sems.get_hs_heap",
"lemma_X64.Stack_Sems.equiv_load_stack64",
"lemma_X64.Stack_Sems.equiv_valid_src_stack64",
"lemma_X64.Stack_Sems.lemma_stack_from_to",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Regs.lemma_upd_eq",
"lemma_X64.Vale.Regs.lemma_upd_ne",
"lemma_X64.Vale.StateLemmas.lemma_to_eval_operand",
"lemma_X64.Vale.StateLemmas.lemma_to_flags",
"lemma_X64.Vale.StateLemmas.lemma_to_memTaint",
"lemma_X64.Vale.StateLemmas.lemma_to_ok",
"lemma_X64.Vale.StateLemmas.lemma_to_reg",
"lemma_X64.Vale.StateLemmas.lemma_to_trace",
"lemma_X64.Vale.StateLemmas.lemma_to_xmm",
"lemma_X64.Vale.Xmms.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_Negation",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_flags",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_stack",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
"proj_equation_X64.Machine_s.OReg_r",
"proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
"proj_equation_X64.Taint_Semantics_s.MktraceState_state",
"proj_equation_X64.Taint_Semantics_s.MktraceState_trace",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"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_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_stack",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
"projection_inverse_X64.Bytes_Semantics_s.Mov64_dst",
"projection_inverse_X64.Bytes_Semantics_s.Mov64_src",
"projection_inverse_X64.Machine_s.Ins_ins",
"projection_inverse_X64.Machine_s.Ins_t_ins",
"projection_inverse_X64.Machine_s.Ins_t_ocmp",
"projection_inverse_X64.Machine_s.MReg_offset",
"projection_inverse_X64.Machine_s.MReg_r",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Machine_s.OStack_m",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
"projection_inverse_X64.Taint_Semantics_s.TaintedIns_i",
"projection_inverse_X64.Taint_Semantics_s.TaintedIns_t",
"projection_inverse_X64.Vale.Decls.TStack_m",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2c90c44e0c3d494a57f4a23c91ef834a",
"refinement_interpretation_Tm_refine_33d3ef68371378c171a37d999106817a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_7c9e5bdb9582a858897946d48f9f4d58",
"refinement_interpretation_Tm_refine_93c4793e88ba66df1f803c1610135c3a",
"token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"token_correspondence_X64.Bytes_Semantics_s.eval_ins", "true_interp",
"typing_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
"typing_Tm_abs_91d6891d766466e9703afb13e7f1a1bf",
"typing_Tm_abs_e4bbf0f30784e534db44e144328c14b5",
"typing_X64.Bytes_Semantics_s.valid_addr",
"typing_X64.Machine_s.__proj__OReg__item__r",
"typing_X64.Stack_Sems.stack_to_s",
"typing_X64.Stack_i.valid_src_stack64",
"typing_X64.Taint_Semantics.mk_taint_ins2",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__trace",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__i",
"typing_X64.Taint_Semantics_s.extract_operands",
"typing_X64.Taint_Semantics_s.ins_obs",
"typing_X64.Taint_Semantics_s.operand_obs",
"typing_X64.Taint_Semantics_s.operand_obs_list",
"typing_X64.Taint_Semantics_s.taint_eval_ins",
"typing_X64.Taint_Semantics_s.update_taint",
"typing_X64.Vale.Decls.va_is_dst_opr64",
"typing_X64.Vale.Decls.va_update_operand",
"typing_X64.Vale.Regs.of_fun", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__stack",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.StateLemmas.state_to_S",
"typing_tok_X64.Bytes_Semantics_s.Mov64@tok",
"typing_tok_X64.Machine_s.Public@tok", "unit_typing"
],
0,
"724362fa005512528fb85769491c78bb"
],
[
"X64.Vale.InsStack.va_wpMonotone_Load64_stack",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_X64.Vale.Decls.va_operand_reg_opr64",
"equation_X64.Vale.InsStack.va_wp_Load64_stack",
"fuel_guarded_inversion_X64.Vale.State.state",
"refinement_interpretation_Tm_refine_93c4793e88ba66df1f803c1610135c3a",
"typing_X64.Vale.Decls.va_upd_operand_dst_opr64", "unit_typing"
],
0,
"d28bc6a035eae2387f092b88dd90deca"
],
[
"X64.Vale.InsStack.va_wpCompute_Load64_stack",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.InsStack.va_code_Load64_stack",
"equation_X64.Vale.InsStack.va_wp_Load64_stack",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion"
],
0,
"7b58bbaba63b4f6b9681b5dc6125393f"
],
[
"X64.Vale.InsStack.va_wpProof_Load64_stack",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"d7750aed64bb290600d4c6e8e0daccf2"
],
[
"X64.Vale.InsStack.va_wpProof_Load64_stack",
2,
4,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"X64.Vale.QuickCode_pretyping_5ef17715065c7f9c7618e13aa923e84c",
"bool_inversion", "constructor_distinct_Prims.Nil",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OMem",
"constructor_distinct_X64.Machine_s.OStack",
"constructor_distinct_X64.Vale.QuickCode.Mod_reg",
"data_elim_Prims.Cons", "data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_X64.Vale.QuickCode.Mod_ok@tok",
"disc_equation_X64.Machine_s.OReg", "eq2-interp",
"equation_Prims.nat", "equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_fuel",
"equation_X64.Vale.Decls.va_is_dst_opr64",
"equation_X64.Vale.Decls.va_operand_reg_opr64",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_operand_dst_opr64",
"equation_X64.Vale.Decls.va_update_operand",
"equation_X64.Vale.InsStack.va_code_Load64_stack",
"equation_X64.Vale.InsStack.va_wpCompute_Load64_stack",
"equation_X64.Vale.InsStack.va_wp_Load64_stack",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_with_fuel_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
"fuel_guarded_inversion_X64.Vale.Decls.tainted_operand",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"int_typing", "kinding_X64.Vale.QuickCode.mod_t@tok",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.StateLemmas.lemma_to_flags",
"lemma_X64.Vale.StateLemmas.lemma_to_ok",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"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_X64.Machine_s.OReg_r",
"projection_inverse_X64.Vale.QuickCode.Mod_reg__0",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_93c4793e88ba66df1f803c1610135c3a",
"token_correspondence_X64.Vale.InsStack.va_wpCompute_Load64_stack",
"typing_X64.Stack_i.load_stack64",
"typing_X64.Vale.Decls.va_is_dst_opr64",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_update_operand",
"typing_X64.Vale.QuickCode.va_mod_dst_opr64",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__stack",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms", "unit_typing"
],
0,
"c1f57974d20d09730b7e9758c08b8786"
],
[
"X64.Vale.InsStack.va_lemma_PushXmm",
1,
2,
2,
[
"@MaxIFuel_assumption", "@query",
"X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
"bool_inversion", "constructor_distinct_Prims.Cons",
"constructor_distinct_X64.Machine_s.Block",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OMem",
"constructor_distinct_X64.Machine_s.OStack",
"constructor_distinct_X64.Machine_s.Rsp",
"data_elim_X64.Vale.Decls.TReg",
"data_typing_intro_X64.Machine_s.OReg@tok",
"data_typing_intro_X64.Machine_s.Rbx@tok",
"disc_equation_Prims.Cons", "disc_equation_X64.Machine_s.Block",
"disc_equation_X64.Machine_s.OReg",
"disc_equation_X64.Machine_s.Rsp", "eq2-interp",
"equality_tok_X64.Machine_s.Rsp@tok", "equation_Prims.nat",
"equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.ins",
"equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_fuel",
"equation_X64.Vale.Decls.va_is_dst_opr64",
"equation_X64.Vale.Decls.va_operand_reg_opr64",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_stack",
"equation_X64.Vale.Decls.va_update_operand",
"equation_X64.Vale.InsStack.va_code_PushXmm",
"equation_X64.Vale.InsStack.va_transparent_code_PushXmm",
"equation_X64.Vale.State.eval_operand",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"fuel_guarded_inversion_X64.Vale.Decls.tainted_operand",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"int_typing", "lemma_X64.Stack_i.lemma_same_init_rsp_store_stack64",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Regs.lemma_upd_eq",
"lemma_X64.Vale.Regs.lemma_upd_ne",
"lemma_X64.Vale.StateLemmas.lemma_to_ok",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl",
"proj_equation_X64.Machine_s.Block_block",
"proj_equation_X64.Machine_s.OReg_r",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"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_X64.Machine_s.Block_block",
"projection_inverse_X64.Machine_s.Block_t_ins",
"projection_inverse_X64.Machine_s.Block_t_ocmp",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_7c9e5bdb9582a858897946d48f9f4d58",
"refinement_interpretation_Tm_refine_93c4793e88ba66df1f803c1610135c3a",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_Arch.Types.lo64",
"typing_X64.Machine_s.__proj__OReg__item__r",
"typing_X64.Stack_i.store_stack64",
"typing_X64.Vale.Decls.va_is_dst_opr64",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_stack",
"typing_X64.Vale.Decls.va_update_operand",
"typing_X64.Vale.Regs.sel", "typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__stack",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.eval_operand", "typing_X64.Vale.Xmms.sel",
"typing_tok_X64.Machine_s.Rsp@tok"
],
0,
"b4c702ca0b1c19a9f22e9b7c7b4afa3e"
],
[
"X64.Vale.InsStack.va_wpMonotone_PushXmm",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_X64.Machine_s.Rsp@tok",
"equation_X64.Vale.Decls.va_operand_reg_opr64",
"equation_X64.Vale.InsStack.va_wp_PushXmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"refinement_interpretation_Tm_refine_93c4793e88ba66df1f803c1610135c3a",
"typing_X64.Vale.Decls.va_upd_operand_reg_opr64",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_stack",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"e12d70bab89bb59724287468050edb46"
],
[
"X64.Vale.InsStack.va_wpCompute_PushXmm",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.InsStack.va_code_PushXmm",
"equation_X64.Vale.InsStack.va_wp_PushXmm",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
],
0,
"4c347defc2aa1e27b098b5215c4b3b05"
],
[
"X64.Vale.InsStack.va_wpProof_PushXmm",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"ed5efaf32c27a11dd3e526db1d189c55"
],
[
"X64.Vale.InsStack.va_wpProof_PushXmm",
2,
2,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
"X64.Vale.QuickCode_pretyping_5ef17715065c7f9c7618e13aa923e84c",
"bool_inversion", "constructor_distinct_Prims.Nil",
"constructor_distinct_Prims.unit", "constructor_distinct_Tm_unit",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Vale.QuickCode.Mod_reg",
"constructor_distinct_X64.Vale.QuickCode.mod_t",
"data_elim_X64.Vale.QuickCode.Mod_reg",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_X64.Machine_s.OReg@tok",
"data_typing_intro_X64.Machine_s.Rbx@tok",
"data_typing_intro_X64.Vale.QuickCode.Mod_ok@tok",
"disc_equation_X64.Machine_s.OReg", "eq2-interp",
"equality_tok_X64.Machine_s.Rsp@tok", "equation_Prims.nat",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_fuel",
"equation_X64.Vale.Decls.va_operand_reg_opr64",
"equation_X64.Vale.Decls.va_reg_operand",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_operand_reg_opr64",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_stack",
"equation_X64.Vale.Decls.va_update_operand",
"equation_X64.Vale.InsStack.va_code_PushXmm",
"equation_X64.Vale.InsStack.va_wpCompute_PushXmm",
"equation_X64.Vale.InsStack.va_wp_PushXmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.QuickCode.va_mod_reg_opr64",
"equation_X64.Vale.State.eval_operand",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_with_fuel_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"kinding_X64.Vale.QuickCode.mod_t@tok",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.StateLemmas.lemma_to_flags",
"lemma_X64.Vale.StateLemmas.lemma_to_ok",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Machine_s.OReg_r",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"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.Nil_a",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Vale.QuickCode.Mod_reg__0",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_7c9e5bdb9582a858897946d48f9f4d58",
"refinement_interpretation_Tm_refine_93c4793e88ba66df1f803c1610135c3a",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.Vale.InsStack.va_wpCompute_PushXmm",
"typing_X64.Machine_s.__proj__OReg__item__r",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_update_operand",
"typing_X64.Vale.QuickCode.va_mod_reg_opr64",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__stack",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"9269c05a3bec685feadb9da88e8ff5fd"
],
[
"X64.Vale.InsStack.va_lemma_PopXmm",
1,
2,
2,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
"X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
"bool_inversion", "constructor_distinct_Prims.Cons",
"constructor_distinct_X64.Machine_s.Block",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OMem",
"constructor_distinct_X64.Machine_s.OStack",
"constructor_distinct_X64.Machine_s.Rsp",
"data_elim_X64.Taint_Semantics_s.MktraceState",
"data_elim_X64.Vale.Decls.TReg",
"data_typing_intro_X64.Machine_s.OReg@tok",
"data_typing_intro_X64.Machine_s.Rbx@tok",
"disc_equation_Prims.Cons", "disc_equation_X64.Machine_s.Block",
"disc_equation_X64.Machine_s.OReg",
"disc_equation_X64.Machine_s.Rsp", "eq2-interp",
"equality_tok_X64.Machine_s.Rsp@tok", "equation_Prims.nat",
"equation_Words_s.nat1", "equation_Words_s.nat64",
"equation_Words_s.natN", "equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.ins", "equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_fuel",
"equation_X64.Vale.Decls.va_is_dst_opr64",
"equation_X64.Vale.Decls.va_operand_reg_opr64",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_stack",
"equation_X64.Vale.Decls.va_update_operand",
"equation_X64.Vale.Decls.valid_operand",
"equation_X64.Vale.InsStack.va_code_PopXmm",
"equation_X64.Vale.InsStack.va_transparent_code_PopXmm",
"equation_X64.Vale.State.eval_operand",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"equation_X64.Vale.State.valid_src_operand",
"equation_X64.Vale.StateLemmas.state_to_S",
"fuel_guarded_inversion_X64.Vale.Decls.tainted_operand",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
"interpretation_Tm_abs_74722fb662ef15cb6b81bf92b6bcee49",
"interpretation_Tm_abs_c2eb935d8e03c1fc053c50aa71d8fa6b",
"lemma_X64.Stack_i.lemma_compose_free_stack64",
"lemma_X64.Stack_i.lemma_free_stack_same_load64",
"lemma_X64.Stack_i.lemma_free_stack_same_valid64",
"lemma_X64.Stack_i.lemma_same_init_rsp_free_stack64",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Regs.lemma_upd_eq",
"lemma_X64.Vale.Regs.lemma_upd_ne",
"lemma_X64.Vale.StateLemmas.lemma_to_flags",
"lemma_X64.Vale.StateLemmas.lemma_to_ok",
"lemma_X64.Vale.StateLemmas.lemma_to_reg",
"lemma_X64.Vale.StateLemmas.lemma_to_trace",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_upd_eq",
"lemma_X64.Vale.Xmms.lemma_upd_ne",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
"proj_equation_X64.Machine_s.Block_block",
"proj_equation_X64.Machine_s.OReg_r",
"proj_equation_X64.Taint_Semantics_s.MktraceState_state",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"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_X64.Bytes_Semantics_s.Mkstate_mem",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
"projection_inverse_X64.Machine_s.Block_block",
"projection_inverse_X64.Machine_s.Block_t_ins",
"projection_inverse_X64.Machine_s.Block_t_ocmp",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2c90c44e0c3d494a57f4a23c91ef834a",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_71709ae578a4508e1b8172135bc2d811",
"refinement_interpretation_Tm_refine_7c9e5bdb9582a858897946d48f9f4d58",
"refinement_interpretation_Tm_refine_93c4793e88ba66df1f803c1610135c3a",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"true_interp", "typing_Arch.Types.hi64",
"typing_Arch.Types.insert_nat64_opaque",
"typing_X64.Machine_s.__proj__OReg__item__r",
"typing_X64.Stack_i.free_stack64", "typing_X64.Stack_i.load_stack64",
"typing_X64.Stack_i.valid_src_stack64",
"typing_X64.Vale.Decls.va_is_dst_opr64",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_stack",
"typing_X64.Vale.Decls.va_update_operand",
"typing_X64.Vale.InsStack.va_code_Pop",
"typing_X64.Vale.InsStack.va_lemma_Pop", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__stack",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.eval_operand",
"typing_X64.Vale.State.update_xmm",
"typing_X64.Vale.StateLemmas.state_to_S", "typing_X64.Vale.Xmms.sel",
"typing_X64.Vale.Xmms.upd", "typing_tok_X64.Machine_s.Rsp@tok"
],
0,
"e4e5ce5a2b9233b132feee972f2a439d"
],
[
"X64.Vale.InsStack.va_wpMonotone_PopXmm",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_X64.Machine_s.Rsp@tok",
"equation_X64.Vale.Decls.va_operand_reg_opr64",
"equation_X64.Vale.InsStack.va_wp_PopXmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"refinement_interpretation_Tm_refine_93c4793e88ba66df1f803c1610135c3a",
"typing_X64.Vale.Decls.va_upd_operand_reg_opr64",
"typing_X64.Vale.Decls.va_upd_operand_xmm",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_stack",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"362b1a3cfb78d274cf46acf6414a80ec"
],
[
"X64.Vale.InsStack.va_wpCompute_PopXmm",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.InsStack.va_code_PopXmm",
"equation_X64.Vale.InsStack.va_wp_PopXmm",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
],
0,
"054052a2240f860e447daccefe47ef80"
],
[
"X64.Vale.InsStack.va_wpProof_PopXmm",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"ef8842e4e4d83f794a9786f75e223966"
],
[
"X64.Vale.InsStack.va_wpProof_PopXmm",
2,
2,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
"X64.Vale.QuickCode_pretyping_5ef17715065c7f9c7618e13aa923e84c",
"bool_inversion", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil", "constructor_distinct_Prims.unit",
"constructor_distinct_Tm_unit",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Vale.QuickCode.Mod_reg",
"constructor_distinct_X64.Vale.QuickCode.Mod_xmm",
"constructor_distinct_X64.Vale.QuickCode.mod_t",
"data_elim_X64.Vale.QuickCode.Mod_reg",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_X64.Machine_s.OReg@tok",
"data_typing_intro_X64.Machine_s.Rbx@tok",
"data_typing_intro_X64.Vale.QuickCode.Mod_ok@tok",
"disc_equation_X64.Machine_s.OReg", "eq2-interp",
"equality_tok_X64.Machine_s.Rsp@tok", "equation_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_fuel",
"equation_X64.Vale.Decls.va_operand_reg_opr64",
"equation_X64.Vale.Decls.va_reg_operand",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_operand_reg_opr64",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_stack",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.va_update_operand",
"equation_X64.Vale.InsStack.va_code_PopXmm",
"equation_X64.Vale.InsStack.va_wpCompute_PopXmm",
"equation_X64.Vale.InsStack.va_wp_PopXmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.QuickCode.update_state_mod",
"equation_X64.Vale.QuickCode.va_mod_reg_opr64",
"equation_X64.Vale.QuickCode.va_mod_xmm",
"equation_X64.Vale.State.eval_operand",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"equation_with_fuel_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"int_typing", "kinding_X64.Vale.QuickCode.mod_t@tok",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.StateLemmas.lemma_to_flags",
"lemma_X64.Vale.StateLemmas.lemma_to_ok",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Machine_s.OReg_r",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"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_X64.Machine_s.OReg_r",
"projection_inverse_X64.Vale.QuickCode.Mod_reg__0",
"projection_inverse_X64.Vale.QuickCode.Mod_xmm__0",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_7c9e5bdb9582a858897946d48f9f4d58",
"refinement_interpretation_Tm_refine_93c4793e88ba66df1f803c1610135c3a",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.Vale.InsStack.va_wpCompute_PopXmm",
"typing_X64.Machine_s.__proj__OReg__item__r",
"typing_X64.Stack_i.free_stack64", "typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_update_operand",
"typing_X64.Vale.QuickCode.va_mod_reg_opr64",
"typing_X64.Vale.QuickCode.va_mod_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__stack",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.eval_operand",
"typing_X64.Vale.State.update_xmm",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"e17f5ca72c0d460f96fc54fc953a029e"
]
]
]
Computing file changes ...
