Revision 724d1045f60f13d79df1afc5190955afdfa73ec1 authored by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC, committed by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC
Co-authored-by: @protz
1 parent ca37fbf
Vale.Arch.MachineHeap.fst.hints
[
"��s=z9\u0012\u0006�tG\u00133%,-",
[
[
"Vale.Arch.MachineHeap.same_mem_get_heap_val64",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
"data_typing_intro_Vale.Def.Words_s.Mktwo@tok", "equation_Prims.nat",
"equation_Prims.pos",
"equation_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"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.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_Vale.Def.Words_s.Mktwo_hi",
"projection_inverse_Vale.Def.Words_s.Mktwo_lo",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"typing_FStar.Map.sel", "typing_Prims.pow2",
"typing_Vale.Def.Words.Four_s.four_to_nat",
"typing_Vale.Def.Words_s.natN"
],
0,
"435b85cb68a7016a5d8ecc7802e1763d"
],
[
"Vale.Arch.MachineHeap.frame_update_heap64",
1,
1,
0,
[
"@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",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Arch.MachineHeap_s.update_heap64_def",
"equation_Vale.Def.Words.Two_s.nat_to_two",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"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.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.UInt.pow2_values", "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_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mktwo_hi",
"projection_inverse_Vale.Def.Words_s.Mktwo_lo",
"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.upd", "typing_Prims.pow2",
"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,
"44bf5a45a6059e509679674da1de709d"
],
[
"Vale.Arch.MachineHeap.correct_update_get64",
1,
1,
0,
[
"@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",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Arch.MachineHeap_s.update_heap64_def",
"equation_Vale.Def.Words.Two_s.nat_to_two",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"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.get_heap_val64",
"function_token_typing_Vale.Arch.MachineHeap_s.update_heap64",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_SelUpd1",
"lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8",
"lemma_Vale.Def.Words.Two.two_to_nat_to_two",
"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_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mktwo_hi",
"projection_inverse_Vale.Def.Words_s.Mktwo_lo",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Prims.pow2.fuel_instrumented",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap64_def",
"typing_FStar.Map.sel", "typing_FStar.Map.upd", "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",
"typing_Vale.Def.Words_s.natN"
],
0,
"145176e9e2c950ec3dc0ce7dadd6e629"
],
[
"Vale.Arch.MachineHeap.same_domain_update64",
1,
1,
0,
[
"@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",
"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.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"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_InDomUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro", "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",
"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.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.upd", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_Prims.pow2", "typing_Vale.Arch.MachineHeap_s.update_heap64",
"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"
],
0,
"81b59ae2a0fb9feeaf3e6acaa773d91d"
],
[
"Vale.Arch.MachineHeap.same_mem_get_heap_val32",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.MachineHeap_s.get_heap_val32_def",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Def.Words_s.nat8",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val32_def",
"typing_FStar.Map.sel", "typing_Prims.pow2",
"typing_Vale.Def.Words_s.natN"
],
0,
"9d40abf2eac4e0290aa8339a62daf7f9"
],
[
"Vale.Arch.MachineHeap.frame_update_heap32",
1,
1,
0,
[
"@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",
"equation_Prims.nat",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Arch.MachineHeap_s.update_heap32_def",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"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_heap32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.UInt.pow2_values",
"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",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap32_def",
"typing_FStar.Map.upd", "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,
"229e3380efde0a443c9d7c6d8f512716"
],
[
"Vale.Arch.MachineHeap.same_domain_update32",
1,
1,
0,
[
"@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",
"equation_Prims.nat",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Arch.MachineHeap_s.update_heap32_def",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"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_heap32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_union",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"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",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap32_def",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.upd", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_Vale.Arch.MachineHeap_s.update_heap32",
"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,
"a037e9b9ee8449401cb42e7cab93386e"
],
[
"Vale.Arch.MachineHeap.update_heap32_get_heap32",
1,
1,
0,
[
"@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",
"Vale.Arch.MachineHeap_s_interpretation_Tm_arrow_8c047871adfcc9e94a3b3d8d0c2d35be",
"bool_inversion", "data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
"equation_Prims.nat",
"equation_Vale.Arch.MachineHeap_s.get_heap_val32_def",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Arch.MachineHeap_s.update_heap32_def",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"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.get_heap_val32",
"function_token_typing_Vale.Arch.MachineHeap_s.update_heap32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Map.lemma_equal_elim",
"lemma_FStar.Map.lemma_equal_intro",
"lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_union",
"lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Words.Seq.nat_to_four_to_nat",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"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",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val32_def",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap32_def",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.sel", "typing_FStar.Map.upd",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_Vale.Arch.MachineHeap_s.get_heap_val32",
"typing_Vale.Arch.MachineHeap_s.update_heap32"
],
0,
"aba1139a4b399f6c6124f228ce8a4b94"
],
[
"Vale.Arch.MachineHeap.frame_update_heap128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.MachineHeap_s.update_heap128_def",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Arch.MachineHeap_s.update_heap128",
"int_inversion",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap128_def"
],
0,
"e7d9c512775be2b2e182c0bfc6565207"
],
[
"Vale.Arch.MachineHeap.correct_update_get32",
1,
1,
0,
[
"@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",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.MachineHeap_s.get_heap_val32_def",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Arch.MachineHeap_s.update_heap32_def",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"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.get_heap_val32",
"function_token_typing_Vale.Arch.MachineHeap_s.update_heap32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_SelUpd1",
"lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8",
"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",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val32_def",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap32_def",
"typing_FStar.Map.sel", "typing_FStar.Map.upd", "typing_Prims.pow2",
"typing_Vale.Arch.MachineHeap_s.update_heap32",
"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.Def.Words_s.natN"
],
0,
"0370ee27cbaf315e1ba59bbea84893d7"
],
[
"Vale.Arch.MachineHeap.correct_update_get128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.MachineHeap_s.get_heap_val128_def",
"equation_Vale.Arch.MachineHeap_s.get_heap_val32_def",
"equation_Vale.Arch.MachineHeap_s.update_heap128_def",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val128",
"function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val32",
"function_token_typing_Vale.Arch.MachineHeap_s.update_heap128",
"int_inversion", "int_typing",
"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",
"projection_inverse_BoxInt_proj_0",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val128_def",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val32_def",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap128_def"
],
0,
"ea3cd8434026ce4669a4235f0bb60e36"
],
[
"Vale.Arch.MachineHeap.same_domain_update128",
1,
2,
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",
"data_elim_Vale.Def.Words_s.Mkfour", "equation_Prims.nat",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Arch.MachineHeap_s.update_heap128_def",
"equation_Vale.Arch.MachineHeap_s.update_heap32_def",
"equation_Vale.Arch.MachineHeap_s.valid_addr",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"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_heap128",
"function_token_typing_Vale.Arch.MachineHeap_s.update_heap32",
"function_token_typing_Vale.Arch.MachineHeap_s.valid_addr128",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_14d403333eed8abd9b38f58babfc702d",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_union",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"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",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap128_def",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap32_def",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.upd", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_Vale.Arch.MachineHeap_s.update_heap128",
"typing_Vale.Arch.MachineHeap_s.update_heap32",
"typing_Vale.Arch.MachineHeap_s.valid_addr",
"typing_Vale.Arch.MachineHeap_s.valid_addr128",
"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,
"898847971b14311607c2150e551355e6"
],
[
"Vale.Arch.MachineHeap.same_mem_get_heap_val128",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.MachineHeap_s.get_heap_val128_def",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val128",
"int_inversion", "int_typing", "projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val128_def"
],
0,
"618db57a3f66db6595f7bce4282d663c"
]
]
]
Computing file changes ...
