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.Stack_i.fst.hints
[
"�IP��X\u007f��J\u0005xL��\u001f",
[
[
"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",
"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.valid_addr64",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"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,
"58d6cb9e36c5d8c6674408686f14f6c6"
],
[
"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,
"5ede1e4a89e62518dd216e076d11156b"
],
[
"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",
"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.valid_addr64",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"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,
"1924a6ca4bc15823d4c0ed1b6d0c0591"
],
[
"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,
"f1cbfd569c5854f12e7a1cad52b601be"
],
[
"Vale.X64.Stack_i.lemma_frame_store_load_stack64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.MachineHeap_s.get_heap_val64",
"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.Def.Opaque_s.make_opaque",
"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,
"e888f3845702458b423455751108f843"
],
[
"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",
"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.valid_addr64",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"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,
"b018a19d4d0970f9b7b4a3f3a51edadb"
],
[
"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,
"92a4595c2b6b498b92befd9010a6c8e9"
],
[
"Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64",
1,
1,
0,
[ "@query" ],
0,
"a6ae7ebeaad5e72bd8eafca6673ed363"
],
[
"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,
"a1d670c435332bcd574f6a7fcc6dfad8"
],
[
"Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64",
1,
1,
0,
[ "@query" ],
0,
"844a26ef8adc704616eb9e4097c91e39"
],
[
"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,
"594638c2f0a603d7e598dbc8f5913166"
],
[
"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,
"a0b30a635b2f50683af6051b3606cb8f"
],
[
"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,
"a0f4ccb176f8b1b16541c2dc81ef1814"
],
[
"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,
"6bac584a35edc460e67750ac509a80d4"
],
[
"Vale.X64.Stack_i.lemma_correct_store_load_taint_stack64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"b2t_def", "equality_tok_Vale.X64.Machine_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_21546bbfcd6f29a8d6a0b4798ed975a5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.X64.Machine_Semantics_s.update_n",
"typing_tok_Vale.X64.Machine_s.Public@tok"
],
0,
"64c7fc70a6afbd190e5553616ed4b380"
],
[
"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_21546bbfcd6f29a8d6a0b4798ed975a5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.X64.Machine_Semantics_s.update_n"
],
0,
"ed0daa64dcd3cfb0012a6dbead2b3f20"
]
]
]
Computing file changes ...
