Revision b5e85960e109efb08b9c65a4ab85c9b4ef926419 authored by Jay Bosamiya on 04 June 2019, 18:24:09 UTC, committed by Jay Bosamiya on 04 June 2019, 18:24:09 UTC
1 parent 2a5defc
Vale.X64.Stack_Sems.fst.hints
[
"@k\u001fID�tT���e\u0012\u0019\u001a ",
[
[
"Vale.X64.Stack_Sems.lemma_stack_from_to",
1,
1,
0,
[
"@query", "equation_Vale.X64.Stack_Sems.stack_from_s",
"equation_Vale.X64.Stack_Sems.stack_to_s"
],
0,
"0bcaad026d6ae2a92eecdf1f61d52d2d"
],
[
"Vale.X64.Stack_Sems.lemma_stack_to_from",
1,
1,
0,
[
"@query", "equation_Vale.X64.Stack_Sems.stack_from_s",
"equation_Vale.X64.Stack_Sems.stack_to_s"
],
0,
"517fe9ac9f3c691654a8f7a2ad64fd7b"
],
[
"Vale.X64.Stack_Sems.equiv_valid_src_stack64",
1,
1,
0,
[
"@query", "equation_Vale.X64.Stack_Sems.stack_to_s",
"equation_Vale.X64.Stack_i.valid_src_stack64"
],
0,
"1e72df6dc69b6af139b9f787146a486b"
],
[
"Vale.X64.Stack_Sems.equiv_load_stack64",
1,
1,
0,
[
"@query", "equation_Vale.X64.Stack_Sems.stack_to_s",
"equation_Vale.X64.Stack_i.load_stack64"
],
0,
"39954ff475faca583b20287f03db6a7c"
],
[
"Vale.X64.Stack_Sems.free_stack_same_load",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"equation_Vale.Def.Words_s.nat8",
"equation_Vale.X64.Machine_Semantics_s.free_stack_",
"equation_Vale.X64.Machine_Semantics_s.get_heap_val64",
"equation_Vale.X64.Machine_Semantics_s.get_heap_val64_def",
"equation_Vale.X64.Machine_Semantics_s.heap",
"equation_Vale.X64.Machine_Semantics_s.op_String_Access",
"equation_Vale.X64.Machine_Semantics_s.valid_addr",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.X64.Machine_Semantics_s.valid_addr64",
"int_inversion", "int_typing",
"interpretation_Tm_abs_8b02a72dff4a737742473cca123eface",
"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.Vale_stack_initial_rsp",
"projection_inverse_Vale.X64.Machine_Semantics_s.Vale_stack_stack_mem",
"token_correspondence_FStar.Map.sel",
"token_correspondence_Vale.X64.Machine_Semantics_s.get_heap_val64_def",
"token_correspondence_Vale.X64.Machine_Semantics_s.op_String_Access",
"typing_FStar.Map.domain", "typing_Vale.Lib.Set.remove_between",
"typing_Vale.X64.Machine_Semantics_s.valid_addr",
"typing_Vale.X64.Machine_Semantics_s.valid_addr64"
],
0,
"9aeb10be2da5e720b0bce0d9472465c4"
],
[
"Vale.X64.Stack_Sems.equiv_store_stack64",
1,
1,
0,
[
"@query", "equation_Vale.X64.Stack_Sems.stack_from_s",
"equation_Vale.X64.Stack_Sems.stack_to_s",
"equation_Vale.X64.Stack_i.store_stack64"
],
0,
"b1d3439d524d92e662cddba5132057ed"
],
[
"Vale.X64.Stack_Sems.equiv_init_rsp",
1,
1,
0,
[ "@query" ],
0,
"8ad30082577f57f10af714efd4f368b4"
],
[
"Vale.X64.Stack_Sems.equiv_init_rsp",
2,
1,
0,
[
"@query", "equation_Vale.X64.Stack_Sems.stack_to_s",
"equation_Vale.X64.Stack_i.init_rsp"
],
0,
"2265612ff566e393542745269cb00431"
],
[
"Vale.X64.Stack_Sems.equiv_free_stack",
1,
1,
0,
[
"@query", "equation_Vale.X64.Stack_Sems.stack_from_s",
"equation_Vale.X64.Stack_Sems.stack_to_s",
"equation_Vale.X64.Stack_i.free_stack64"
],
0,
"4d945966ced35568475d70297905598b"
],
[
"Vale.X64.Stack_Sems.equiv_valid_src_stack128",
1,
1,
0,
[
"@query", "equation_Vale.X64.Stack_Sems.stack_to_s",
"equation_Vale.X64.Stack_i.valid_src_stack128"
],
0,
"a4431623530b5b2a879898a6dd0a31dc"
],
[
"Vale.X64.Stack_Sems.equiv_load_stack128",
1,
1,
0,
[
"@query", "equation_Vale.X64.Stack_Sems.stack_to_s",
"equation_Vale.X64.Stack_i.load_stack128"
],
0,
"8c9de01f134535811173bc6a24582778"
],
[
"Vale.X64.Stack_Sems.free_stack_same_load128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"equation_Vale.Def.Words_s.nat8",
"equation_Vale.X64.Machine_Semantics_s.free_stack_",
"equation_Vale.X64.Machine_Semantics_s.get_heap_val128",
"equation_Vale.X64.Machine_Semantics_s.get_heap_val128_def",
"equation_Vale.X64.Machine_Semantics_s.get_heap_val32",
"equation_Vale.X64.Machine_Semantics_s.get_heap_val32_def",
"equation_Vale.X64.Machine_Semantics_s.heap",
"equation_Vale.X64.Machine_Semantics_s.op_String_Access",
"equation_Vale.X64.Machine_Semantics_s.valid_addr",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.X64.Machine_Semantics_s.valid_addr128",
"int_inversion", "int_typing",
"interpretation_Tm_abs_8ed52139a66f031c5a7a3981ff5d18eb",
"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.Vale_stack_initial_rsp",
"projection_inverse_Vale.X64.Machine_Semantics_s.Vale_stack_stack_mem",
"token_correspondence_FStar.Map.sel",
"token_correspondence_Vale.X64.Machine_Semantics_s.get_heap_val128_def",
"token_correspondence_Vale.X64.Machine_Semantics_s.get_heap_val32_def",
"token_correspondence_Vale.X64.Machine_Semantics_s.op_String_Access",
"typing_FStar.Map.domain", "typing_Vale.Lib.Set.remove_between",
"typing_Vale.X64.Machine_Semantics_s.valid_addr",
"typing_Vale.X64.Machine_Semantics_s.valid_addr128"
],
0,
"03bbfacb8a15cc7306f7def7d53122b1"
],
[
"Vale.X64.Stack_Sems.equiv_store_stack128",
1,
1,
0,
[
"@query", "equation_Vale.X64.Stack_Sems.stack_from_s",
"equation_Vale.X64.Stack_Sems.stack_to_s",
"equation_Vale.X64.Stack_i.store_stack128"
],
0,
"144c3f438b55045f7b752f088cd3c838"
]
]
]
Computing file changes ...
