Revision e56414221fb67ecff7d071497f8ba5d20e9c5ba9 authored by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC, committed by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC
1 parent db297bf
Vale.X64.Stack_i.fst.hints
[
"\u001b��\u000b\u0005<�=���1�&.v",
[
[
"Vale.X64.Stack_i.lemma_store_stack_same_valid64",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Map_interpretation_Tm_arrow_b19283e90b47034162373413c6a19933",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing",
"data_elim_Vale.X64.Machine_Semantics_s.Machine_stack",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Arch.MachineHeap_s.update_heap64_def",
"equation_Vale.Arch.MachineHeap_s.valid_addr",
"equation_Vale.Def.Words.Two_s.nat_to_two",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Stack_i.store_stack64",
"equation_Vale.X64.Stack_i.vale_stack",
"equation_Vale.X64.Stack_i.valid_src_stack64",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_stack",
"function_token_typing_FStar.Map.upd",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Arch.MachineHeap_s.update_heap64",
"function_token_typing_Vale.Arch.MachineHeap_s.valid_addr64",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_1eab5700ef81b3c102d114cb086eb6dc",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_union",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"proj_equation_Vale.Def.Words_s.Mktwo_hi",
"proj_equation_Vale.Def.Words_s.Mktwo_lo",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mktwo_hi",
"projection_inverse_Vale.Def.Words_s.Mktwo_lo",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_stack_mem",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap64_def",
"typing_FStar.Map.domain", "typing_FStar.Map.upd",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_Prims.pow2", "typing_Vale.Arch.MachineHeap_s.valid_addr",
"typing_Vale.Def.Words.Four_s.nat_to_four",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
"typing_Vale.X64.Stack_i.valid_src_stack64"
],
0,
"cf4880747cef5686d57598f812b253b3"
],
[
"Vale.X64.Stack_i.lemma_free_stack_same_valid64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Arch.MachineHeap_s.valid_addr",
"equation_Vale.Def.Words_s.nat8",
"equation_Vale.X64.Machine_Semantics_s.free_stack_",
"equation_Vale.X64.Stack_i.free_stack64",
"equation_Vale.X64.Stack_i.valid_src_stack64",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Arch.MachineHeap_s.valid_addr64",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_1eab5700ef81b3c102d114cb086eb6dc",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict", "primitive_Prims.op_AmpAmp",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_stack_mem",
"typing_FStar.Map.domain",
"typing_Vale.Arch.MachineHeap_s.valid_addr",
"typing_Vale.Lib.Set.remove_between",
"typing_Vale.X64.Stack_i.valid_src_stack64"
],
0,
"d43f3388fa0c3c4a8869911af5b9d807"
],
[
"Vale.X64.Stack_i.lemma_store_new_valid64",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Map_interpretation_Tm_arrow_b19283e90b47034162373413c6a19933",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"data_elim_Vale.X64.Machine_Semantics_s.Machine_stack",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Arch.MachineHeap_s.update_heap64_def",
"equation_Vale.Arch.MachineHeap_s.valid_addr",
"equation_Vale.Def.Words.Two_s.nat_to_two",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Stack_i.store_stack64",
"equation_Vale.X64.Stack_i.vale_stack",
"equation_Vale.X64.Stack_i.valid_src_stack64",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_stack",
"function_token_typing_FStar.Map.upd",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Arch.MachineHeap_s.update_heap64",
"function_token_typing_Vale.Arch.MachineHeap_s.valid_addr64",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_1eab5700ef81b3c102d114cb086eb6dc",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_union",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"proj_equation_Vale.Def.Words_s.Mktwo_hi",
"proj_equation_Vale.Def.Words_s.Mktwo_lo",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mktwo_hi",
"projection_inverse_Vale.Def.Words_s.Mktwo_lo",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_stack_mem",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap64_def",
"typing_FStar.Map.domain", "typing_FStar.Map.upd",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_Prims.pow2", "typing_Vale.Arch.MachineHeap_s.update_heap64",
"typing_Vale.Def.Words.Four_s.nat_to_four",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1"
],
0,
"98e401b385dfba758707ae8089c89bfe"
],
[
"Vale.X64.Stack_i.lemma_correct_store_load_stack64",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_Semantics_s.update_heap64",
"equation_Vale.X64.Stack_i.load_stack64",
"equation_Vale.X64.Stack_i.store_stack64",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_stack_mem"
],
0,
"eedf43b079bff730442e6e1bad0ba41d"
],
[
"Vale.X64.Stack_i.lemma_frame_store_load_stack64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"equation_Vale.X64.Stack_i.load_stack64",
"equation_Vale.X64.Stack_i.store_stack64",
"function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val64",
"int_inversion", "int_typing", "projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_stack_mem",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val64_def"
],
0,
"ed0c358cd4fc2cc05cb30e048b8c210b"
],
[
"Vale.X64.Stack_i.lemma_free_stack_same_load64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"equation_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Arch.MachineHeap_s.valid_addr",
"equation_Vale.Def.Words_s.nat8",
"equation_Vale.X64.Machine_Semantics_s.free_stack_",
"equation_Vale.X64.Stack_i.free_stack64",
"equation_Vale.X64.Stack_i.load_stack64",
"equation_Vale.X64.Stack_i.valid_src_stack64",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val64",
"function_token_typing_Vale.Arch.MachineHeap_s.valid_addr64",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_1eab5700ef81b3c102d114cb086eb6dc",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_SelRestrict", "primitive_Prims.op_AmpAmp",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_stack_mem",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"typing_FStar.Map.domain",
"typing_Vale.Arch.MachineHeap_s.valid_addr",
"typing_Vale.Lib.Set.remove_between",
"typing_Vale.X64.Stack_i.valid_src_stack64"
],
0,
"e240b3b9f93ed475ca5ed5cc98e5bcee"
],
[
"Vale.X64.Stack_i.lemma_compose_free_stack64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_Semantics_s.free_stack_",
"equation_Vale.X64.Stack_i.free_stack64",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat8",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_equal_elim",
"lemma_FStar.Map.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_stack_mem",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_Vale.Lib.Set.remove_between"
],
0,
"9bdea053239cda5ee3f5310da5c820ac"
],
[
"Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64",
1,
1,
0,
[ "@query" ],
0,
"17738d1c8774d64d1bc109d7a6a46ce6"
],
[
"Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_Semantics_s.free_stack_",
"equation_Vale.X64.Stack_i.free_stack64",
"equation_Vale.X64.Stack_i.init_rsp",
"equation_Vale.X64.Stack_i.vale_stack",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_stack",
"int_inversion",
"proj_equation_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp"
],
0,
"f996036c250e2b4ecc4ce9453187e5fa"
],
[
"Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64",
1,
1,
0,
[ "@query" ],
0,
"3f91722be80d596a869b39b6c522d29b"
],
[
"Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Stack_i.init_rsp",
"equation_Vale.X64.Stack_i.store_stack64",
"equation_Vale.X64.Stack_i.vale_stack",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp"
],
0,
"d8aa3a6df00c2038a5573025abdebb2e"
],
[
"Vale.X64.Stack_i.lemma_valid_taint_stack64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"equation_Vale.X64.Stack_i.valid_taint_stack64", "int_inversion",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0"
],
0,
"ecad7469cf7c530f70582d516df08453"
],
[
"Vale.X64.Stack_i.lemma_valid_taint_stack128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"b2t_def", "equality_tok_Vale.X64.Machine_s.Public@tok",
"equation_Vale.X64.Stack_i.valid_taint_stack128",
"equation_Vale.X64.Stack_i.valid_taint_stack64", "int_inversion",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"typing_tok_Vale.X64.Machine_s.Public@tok"
],
0,
"6f4f3c7a2caffdaf8b1656fbea2170b5"
],
[
"Vale.X64.Stack_i.lemma_valid_taint_stack64_reveal",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"b2t_def", "equality_tok_Vale.X64.Machine_s.Public@tok",
"equation_Vale.X64.Stack_i.valid_taint_stack64", "int_typing",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"typing_tok_Vale.X64.Machine_s.Public@tok"
],
0,
"f3577eff1f5301f09b0ec01827b91aed"
],
[
"Vale.X64.Stack_i.lemma_correct_store_load_taint_stack64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"b2t_def", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
"equation_Prims.nat", "equation_Vale.X64.Memory.memtaint",
"equation_Vale.X64.Stack_i.store_taint_stack64",
"equation_Vale.X64.Stack_i.valid_taint_stack64", "int_inversion",
"int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0030c490ddf8a8ae33d539152b909139",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.X64.Machine_Semantics_s.update_n",
"typing_tok_Vale.Arch.HeapTypes_s.Public@tok"
],
0,
"114754f2c2094873b1711d2de2251e3f"
],
[
"Vale.X64.Stack_i.lemma_frame_store_load_taint_stack64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.X64.Memory.memtaint",
"equation_Vale.X64.Stack_i.store_taint_stack64",
"equation_Vale.X64.Stack_i.valid_taint_stack64", "int_inversion",
"int_typing", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0030c490ddf8a8ae33d539152b909139",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.X64.Machine_Semantics_s.update_n"
],
0,
"d810fa0f0c27b8ae9274e9423a44fa7d"
]
]
]
Computing file changes ...
