Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Vale.X64.InsStack.fst.hints
[
"��Z\u0017g�-�9\u0012����̆",
[
[
"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.X64.Flags_interpretation_Tm_arrow_cdf1f6cd0d3b8802627536b71c7dc9b7",
"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_aa589b9ef510f53ad802095d5dd3ddab",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
"Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"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.Mkmachine_state",
"data_elim_Vale.X64.Machine_s.Ins",
"data_elim_Vale.X64.Machine_s.OReg",
"data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
"data_typing_intro_Vale.X64.Machine_s.MReg@tok",
"data_typing_intro_Vale.X64.Machine_s.OStack@tok",
"data_typing_intro_Vale.X64.Machine_s.Public@tok",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"data_typing_intro_Vale.X64.Machine_s.Secret@tok",
"disc_equation_Vale.X64.Machine_s.Ins", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Public@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "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.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.Decls.va_update_operand",
"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_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.memTaint_t",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Machine_s.t_reg_to_int",
"equation_Vale.X64.Machine_s.tmaddr",
"equation_Vale.X64.Memory.memtaint",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"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.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_Prims.int",
"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", "int_inversion",
"int_typing",
"interpretation_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
"interpretation_Tm_abs_1f233bb62d19e8ce94de2fc1626a49a7",
"interpretation_Tm_abs_2ec28a45999dc3312d0fe2f037d28c23",
"interpretation_Tm_abs_4185c7ad5dc50a20deee59c126b9b37b",
"interpretation_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
"interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"interpretation_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"interpretation_Tm_abs_e2479503b19175531f3a0a4826867fc8",
"kinding_Vale.X64.Machine_s.maddr@tok",
"kinding_Vale.X64.Machine_s.reg@tok",
"kinding_Vale.X64.Machine_s.taint@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"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_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_memTaint",
"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_memTaint",
"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_memTaint",
"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_memTaint",
"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_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_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_ecc48c71754f7b5abdcddeebd08f827a",
"refinement_interpretation_Tm_refine_fa487b99512a5379228c58a2b84595be",
"refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
"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_14a3aa8102b38210dfdbec5a683db924",
"typing_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
"typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"typing_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
"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_update_operand",
"typing_Vale.X64.Flags.of_fun",
"typing_Vale.X64.InsStack.va_code_Pop",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"typing_Vale.X64.Machine_Semantics_s.eval_maddr",
"typing_Vale.X64.Machine_Semantics_s.eval_operand",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code",
"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_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_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,
"cdd486e410d56aea585ea7b889fb243b"
],
[
"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", "eq2-interp",
"equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_stack",
"equation_Vale.X64.Decls.va_update_operand",
"equation_Vale.X64.InsStack.va_wp_Pop",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"kinding_Vale.X64.QuickCode.mod_t@tok",
"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.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"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_memTaint",
"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.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_update_operand",
"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_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,
"7361543e2d31cffb8606f0fde553078d"
],
[
"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,
"84ee3307e84a5d4ff0b6f2186d95e47e"
],
[
"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.X64.Flags_interpretation_Tm_arrow_cdf1f6cd0d3b8802627536b71c7dc9b7",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100",
"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_38835f297fb700457da67879cc31d6a6",
"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.Machine_s.Reg@tok",
"disc_equation_Vale.X64.Machine_s.Ins",
"disc_equation_Vale.X64.Machine_s.OReg", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Public@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"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.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.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_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_heap_impl_equal",
"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.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.unit",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"function_token_typing_Vale.X64.Machine_s.t_reg", "int_inversion",
"int_typing",
"interpretation_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
"interpretation_Tm_abs_1f233bb62d19e8ce94de2fc1626a49a7",
"interpretation_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
"interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"interpretation_Tm_abs_7014ad76387a50b1e635f52d31b3e116",
"interpretation_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"kinding_Vale.X64.Machine_s.reg@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"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_memTaint",
"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_memTaint",
"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_memTaint",
"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_memTaint",
"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_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_c55af5cefb01844d307de87b2d347802",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"token_correspondence_Vale.X64.Machine_s.t_reg", "true_interp",
"typing_FStar.Pervasives.Native.snd",
"typing_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
"typing_Tm_abs_1f233bb62d19e8ce94de2fc1626a49a7",
"typing_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
"typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"typing_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
"typing_Vale.X64.Decls.va_upd_ok",
"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_regs",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint",
"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.X64.Machine_s.Public@tok", "unit_typing"
],
0,
"b4a229934a1e3d5b106932ab994e08c7"
],
[
"Vale.X64.InsStack.va_wpProof_Push",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_Vale.X64.Machine_s.Public@tok",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"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_reg",
"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_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"lemma_Vale.X64.Flags.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_memTaint",
"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.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_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.X64.Machine_s.Public@tok", "unit_typing"
],
0,
"f36d535130854728821a89a2ff01fb8e"
],
[
"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,
"951a2076b812b26b4b58f5a26498cca0"
],
[
"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.X64.Flags_interpretation_Tm_arrow_cdf1f6cd0d3b8802627536b71c7dc9b7",
"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_aa589b9ef510f53ad802095d5dd3ddab",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
"Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"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.Mkmachine_state",
"data_elim_Vale.X64.Machine_s.Ins",
"data_elim_Vale.X64.Machine_s.OReg",
"data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
"data_typing_intro_Vale.X64.Machine_s.MReg@tok",
"data_typing_intro_Vale.X64.Machine_s.OStack@tok",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"data_typing_intro_Vale.X64.Machine_s.Secret@tok",
"disc_equation_Vale.X64.Machine_s.Ins", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "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.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.Decls.va_update_operand",
"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_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.memTaint_t",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Machine_s.t_reg_to_int",
"equation_Vale.X64.Machine_s.tmaddr",
"equation_Vale.X64.Memory.memtaint",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"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.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_Prims.int",
"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", "int_inversion",
"int_typing",
"interpretation_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
"interpretation_Tm_abs_1f233bb62d19e8ce94de2fc1626a49a7",
"interpretation_Tm_abs_2ec28a45999dc3312d0fe2f037d28c23",
"interpretation_Tm_abs_4185c7ad5dc50a20deee59c126b9b37b",
"interpretation_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
"interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"interpretation_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"interpretation_Tm_abs_e2479503b19175531f3a0a4826867fc8",
"kinding_Vale.X64.Machine_s.maddr@tok",
"kinding_Vale.X64.Machine_s.reg@tok",
"kinding_Vale.X64.Machine_s.taint@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"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_memTaint",
"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_memTaint",
"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_memTaint",
"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_memTaint",
"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_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_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_ecc48c71754f7b5abdcddeebd08f827a",
"refinement_interpretation_Tm_refine_fa487b99512a5379228c58a2b84595be",
"refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
"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_14a3aa8102b38210dfdbec5a683db924",
"typing_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
"typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"typing_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
"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_update_operand",
"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_ok",
"typing_Vale.X64.Machine_Semantics_s.eval_maddr",
"typing_Vale.X64.Machine_Semantics_s.eval_operand",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code",
"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_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_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,
"9126cc4c287a19b0430a0fde291a4d82"
],
[
"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", "eq2-interp",
"equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_stack",
"equation_Vale.X64.Decls.va_update_operand",
"equation_Vale.X64.InsStack.va_wp_Pop_Secret",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"kinding_Vale.X64.QuickCode.mod_t@tok",
"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.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"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_memTaint",
"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.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_update_operand",
"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_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,
"cc9161693219f771b6ba0a0180bdff6a"
],
[
"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,
"3a3f29b23f983a1642dea905b69995e8"
],
[
"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.X64.Flags_interpretation_Tm_arrow_cdf1f6cd0d3b8802627536b71c7dc9b7",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100",
"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_38835f297fb700457da67879cc31d6a6",
"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.Machine_s.Reg@tok",
"disc_equation_Vale.X64.Machine_s.Ins",
"disc_equation_Vale.X64.Machine_s.OReg", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Public@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"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.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.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_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_heap_impl_equal",
"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.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.unit",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"function_token_typing_Vale.X64.Machine_s.t_reg", "int_inversion",
"int_typing",
"interpretation_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
"interpretation_Tm_abs_1f233bb62d19e8ce94de2fc1626a49a7",
"interpretation_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
"interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"interpretation_Tm_abs_7014ad76387a50b1e635f52d31b3e116",
"interpretation_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"kinding_Vale.X64.Machine_s.reg@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"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_memTaint",
"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_memTaint",
"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_memTaint",
"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_memTaint",
"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_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_c55af5cefb01844d307de87b2d347802",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"token_correspondence_Vale.X64.Machine_s.t_reg", "true_interp",
"typing_FStar.Pervasives.Native.snd",
"typing_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
"typing_Tm_abs_1f233bb62d19e8ce94de2fc1626a49a7",
"typing_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
"typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"typing_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
"typing_Vale.X64.Decls.va_upd_ok",
"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_regs",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint",
"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.X64.Machine_s.Public@tok", "unit_typing"
],
0,
"aaaa414f31e92fcdd31e878ed800bdeb"
],
[
"Vale.X64.InsStack.va_wpProof_Push_Secret",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"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_reg",
"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_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"lemma_Vale.X64.Flags.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_memTaint",
"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.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_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.X64.Machine_s.Secret@tok", "unit_typing"
],
0,
"05cfff4a05a98dd61fd7e019045e8c7d"
],
[
"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,
"9b1946f22633611761c56fd1f649a0dc"
],
[
"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,
"b3253ad7729d85b68f66115ffbaa3d08"
],
[
"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_cdf1f6cd0d3b8802627536b71c7dc9b7",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100",
"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.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_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_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.X64.Instruction_s.IOp64@tok",
"equality_tok_Vale.X64.Instruction_s.Out@tok",
"equality_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
"equality_tok_Vale.X64.Machine_s.Public@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.eqtype",
"equation_Prims.nat",
"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.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_update_operand",
"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_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.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.memTaint_t",
"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_heap_impl_equal",
"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.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_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.int",
"function_token_typing_Prims.unit",
"function_token_typing_Vale.X64.Instruction_s.instr_out",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"function_token_typing_Vale.X64.Machine_s.t_reg",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
"int_typing",
"interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
"interpretation_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
"interpretation_Tm_abs_1f233bb62d19e8ce94de2fc1626a49a7",
"interpretation_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
"interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
"interpretation_Tm_abs_a7fc7c3035a1a3dfe26ac53ca2f3dd49",
"interpretation_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
"interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
"kinding_FStar.Pervasives.Native.tuple2@tok",
"kinding_Vale.X64.Instruction_s.instr_operand@tok",
"kinding_Vale.X64.Machine_s.reg@tok",
"kinding_Vale.X64.Machine_s.taint@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"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_memTaint",
"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_memTaint",
"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_memTaint",
"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_memTaint",
"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_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_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_ecc48c71754f7b5abdcddeebd08f827a",
"refinement_interpretation_Tm_refine_fa487b99512a5379228c58a2b84595be",
"refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
"token_correspondence_Vale.X64.Instructions_s.eval_Mov64",
"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_14a3aa8102b38210dfdbec5a683db924",
"typing_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
"typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"typing_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
"typing_Vale.Arch.MachineHeap_s.valid_addr64",
"typing_Vale.X64.Decls.va_is_dst_opr64",
"typing_Vale.X64.Decls.va_update_operand",
"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.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.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.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_typing"
],
0,
"8581cc90550282cc9193d86fc8b57dd6"
],
[
"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", "eq2-interp",
"equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"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_reg",
"equation_Vale.X64.Decls.va_update_operand",
"equation_Vale.X64.InsStack.va_wp_Load64_stack",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.QuickCode.update_state_mod",
"equation_Vale.X64.QuickCode.va_mod_dst_opr64",
"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.X64.State.vale_state", "int_inversion",
"int_typing", "kinding_Vale.X64.QuickCode.mod_t@tok",
"lemma_Vale.X64.Flags.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_memTaint",
"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.X64.Decls.va_is_dst_opr64",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_update_operand",
"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_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,
"a5b5ba2e6362c5deae9140ff6661aae8"
],
[
"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,
"9e0f24b440143113fa7880af3a43cd8d"
],
[
"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", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Public@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.ins",
"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.Decls.va_update_operand",
"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_heap_impl_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.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat64",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
"int_typing", "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.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_memTaint",
"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_memTaint",
"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.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.Decls.va_update_operand",
"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_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.X64.Machine_s.Public@tok"
],
0,
"79ed8896e6216bb526e8d7f1d6a15166"
],
[
"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", "eq2-interp",
"equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_stack",
"equation_Vale.X64.Decls.va_upd_stackTaint",
"equation_Vale.X64.Decls.va_update_operand",
"equation_Vale.X64.InsStack.va_wp_PushXmm",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"kinding_Vale.X64.QuickCode.mod_t@tok",
"lemma_Vale.X64.Flags.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"primitive_Prims.op_Equality",
"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_memTaint",
"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_memTaint",
"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.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg64",
"typing_Vale.X64.Decls.va_update_operand",
"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_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,
"1bc71aab892434c999e43e93aaf5910d"
],
[
"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,
"00c3ad899443b126a8ed9d3a38b24bb8"
],
[
"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", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Public@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Decls.ins",
"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_update_operand",
"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_heap_impl_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.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat64",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
"int_typing", "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.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_memTaint",
"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_memTaint",
"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_983e6c379e95abfa99ec316d0742e807",
"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.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.Decls.va_update_operand",
"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_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,
"086fc59b6cc91883b3d745cb7a91dcb8"
],
[
"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", "eq2-interp",
"equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat",
"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.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_stack",
"equation_Vale.X64.Decls.va_update_operand",
"equation_Vale.X64.InsStack.va_wp_PopXmm",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.QuickCode.update_state_mod",
"equation_Vale.X64.QuickCode.va_mod_xmm",
"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.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"int_typing", "kinding_Vale.X64.QuickCode.mod_t@tok",
"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.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"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_memTaint",
"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.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg64",
"typing_Vale.X64.Decls.va_update_operand",
"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_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,
"4544ba1dc2b90f7d4fb5382fb9752bce"
],
[
"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,
"f304d5bdcd2ed3d29479d3f3e7a04365"
],
[
"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", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Decls.ins",
"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.Decls.va_update_operand",
"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_heap_impl_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.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat64",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
"int_typing", "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.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_memTaint",
"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_memTaint",
"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.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.Decls.va_update_operand",
"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_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.X64.Machine_s.Secret@tok"
],
0,
"ca89f4e69b89c488c0282062ff696fc9"
],
[
"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", "eq2-interp",
"equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_stack",
"equation_Vale.X64.Decls.va_upd_stackTaint",
"equation_Vale.X64.Decls.va_update_operand",
"equation_Vale.X64.InsStack.va_wp_PushXmm_Secret",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"kinding_Vale.X64.QuickCode.mod_t@tok",
"lemma_Vale.X64.Flags.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"primitive_Prims.op_Equality",
"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_memTaint",
"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_memTaint",
"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.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg64",
"typing_Vale.X64.Decls.va_update_operand",
"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_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,
"802fecf840d6301637cd6aa1df378c1d"
],
[
"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,
"75a617472912e242c0c7e980be6b4c56"
],
[
"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", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Decls.ins",
"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_update_operand",
"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_heap_impl_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.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat64",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
"int_typing", "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.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_memTaint",
"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_memTaint",
"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_983e6c379e95abfa99ec316d0742e807",
"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.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.Decls.va_update_operand",
"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_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,
"64760e08d36b5323d0202fad55258c70"
],
[
"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", "eq2-interp",
"equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat",
"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.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_stack",
"equation_Vale.X64.Decls.va_update_operand",
"equation_Vale.X64.InsStack.va_wp_PopXmm_Secret",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.QuickCode.update_state_mod",
"equation_Vale.X64.QuickCode.va_mod_xmm",
"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.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"int_typing", "kinding_Vale.X64.QuickCode.mod_t@tok",
"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.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"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_memTaint",
"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.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg64",
"typing_Vale.X64.Decls.va_update_operand",
"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_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,
"fc443b9d02216648a873bd383a228d19"
],
[
"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,
"d999ea55b1ad02b73e1cd3c0dfd326a2"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...