Revision 5b2fbf3c4989a9b0587a00578f69f3041df3f957 authored by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC, committed by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC
1 parent d4ca892
Vale.X64.Memory.fst.hints
[
"�z\u000f\r�Ra�[�.�W\u0016Z�",
[
[
"Vale.X64.Memory.base_typ_as_vale_type",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt128",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt16",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt32",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt64",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt8",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat16", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"0f826a2e1fe730291cdc1cc49d6641dd"
],
[
"Vale.X64.Memory.v_of_typ",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt16",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt32",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt128",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt16",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt32",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt64",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt8",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat16", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"5bb027bfa97c458190d3a1903808cfae"
],
[
"Vale.X64.Memory.v_to_typ",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt16",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt32",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt128",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt16",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt32",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt64",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt8",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat16", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"a918346aaf7d3514bd9c713e73b37d1c"
],
[
"Vale.X64.Memory.lemma_v_to_of_typ",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat16", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.v_of_typ",
"equation_Vale.X64.Memory.v_to_typ",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt16.vu_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_FStar.UInt64.vu_inv", "lemma_FStar.UInt8.vu_inv",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"3e109a4522979e230a158656ab11325f"
],
[
"Vale.X64.Memory.uint_view",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt16",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt32",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt128",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt16",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt32",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt64",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.Interop.Views.up_view128",
"equation_Vale.Interop.Views.up_view16",
"equation_Vale.Interop.Views.up_view32",
"equation_Vale.Interop.Views.up_view64",
"equation_Vale.Interop.Views.up_view8",
"equation_Vale.X64.Memory.uint128_view",
"equation_Vale.X64.Memory.uint16_view",
"equation_Vale.X64.Memory.uint32_view",
"equation_Vale.X64.Memory.uint64_view",
"equation_Vale.X64.Memory.uint8_view",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"proj_equation_LowStar.BufferView.Up.View_n",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_LowStar.BufferView.Up.View_n"
],
0,
"dfb25f14969c94b89fb8b528a6edc8a7"
],
[
"Vale.X64.Memory.buffer_as_seq",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.HeapImpl.buffer",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca"
],
0,
"7cb7c046ea2cafc2d2ed756019a6cc14"
],
[
"Vale.X64.Memory.buffer_length",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.HeapImpl.buffer",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca"
],
0,
"41b7da4f644142bc86125c2b1b13f8d1"
],
[
"Vale.X64.Memory.modifies",
1,
2,
1,
[ "@query" ],
0,
"a1aa4a622ba8fa3c31b2057b3b1734cf"
],
[
"Vale.X64.Memory.index64_heap_aux",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"FStar.UInt8_pretyping_512f0e4172b97206a8b0e16196475713",
"Vale.Def.Words.Four_s_interpretation_Tm_arrow_8e8890e19356591ca1f9e83b434ba1ba",
"Vale.X64.Memory_interpretation_Tm_arrow_efe96bb9514bece12be080c2a3348ae5",
"Vale.X64.Memory_interpretation_Tm_arrow_f4c4992cf843ea442af1288d1d5d4d22",
"b2t_def", "bool_inversion", "bool_typing",
"data_typing_intro_Vale.Def.Words_s.Mktwo@tok",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"equation_Vale.Def.Types_s.le_bytes_to_nat64_def",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words.Seq_s.seq_to_two_LE",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Views.get64_def",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_FStar.UInt8.v",
"function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val64",
"function_token_typing_Vale.Def.Types_s.le_bytes_to_nat64",
"function_token_typing_Vale.Def.Words.Four_s.four_to_nat",
"function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.Interop.Views.get64", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"interpretation_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
"interpretation_Tm_abs_ad3ad425f83578beeb8ba014cbc730a3",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt64.vu_inv",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_35a56cb7608bf4720ad612ec0cf582b4",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_528966909e656beff90629dc95073b2d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_553972523c0ad0511a59f7cdbdcafe94",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a97bb01c04ffe0871485a0f7264ef673",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_FStar.UInt8.v",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"token_correspondence_Vale.Def.Types_s.le_bytes_to_nat64_def",
"token_correspondence_Vale.Def.Words.Four_s.four_to_nat",
"token_correspondence_Vale.Interop.Views.get64_def",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_FStar.UInt64.v", "typing_FStar.UInt8.t", "typing_Prims.pow2",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
"typing_Tm_abs_ad3ad425f83578beeb8ba014cbc730a3",
"typing_Vale.Def.Types_s.le_bytes_to_nat64",
"typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"typing_Vale.Def.Words.Two_s.two_to_nat",
"typing_Vale.Def.Words_s.natN", "typing_Vale.Interop.Views.get64"
],
0,
"56e8c8e37041296787c15a55d90e8577"
],
[
"Vale.X64.Memory.index_helper",
1,
2,
1,
[ "@query" ],
0,
"fe03033893b5e0b84fa309b0fed277cf"
],
[
"Vale.X64.Memory.index_mul_helper",
1,
2,
1,
[
"@query", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0"
],
0,
"279975fa53f16ea942aaa0b8327de6dd"
],
[
"Vale.X64.Memory.index64_get_heap_val64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Heap_s.correct_down",
"equation_Vale.Interop.Heap_s.correct_down_p",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.Interop.Views.up_view64",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.uint64_view",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.v_to_typ",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"proj_equation_LowStar.BufferView.Up.View_get",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Types.Buffer_src",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_LowStar.BufferView.Up.View_get",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_35a56cb7608bf4720ad612ec0cf582b4",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_9539918077828aa633026534394b5105",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b4c3192994dcc590bdf90a64a565ac51",
"refinement_interpretation_Tm_refine_bac48341d72c9512b36c265d7915272a",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_ed56f0a463ff0657a36c83fe878c0439",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f0b69480f5e055250ddc6c0968678616",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"token_correspondence_LowStar.BufferView.Up.__proj__View__item__get",
"token_correspondence_Vale.Interop.Views.get64",
"token_correspondence_Vale.X64.Memory.v_to_typ",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt8.t",
"typing_LowStar.BufferView.Up.as_seq",
"typing_LowStar.BufferView.Up.mk_buffer",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"eef55874739c2d80165ca848458f75d9"
],
[
"Vale.X64.Memory.index128_get_heap_val128_aux",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"FStar.UInt8_pretyping_512f0e4172b97206a8b0e16196475713",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.X64.Memory_interpretation_Tm_arrow_efe96bb9514bece12be080c2a3348ae5",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat",
"equation_Vale.Arch.MachineHeap_s.get_heap_val32_def",
"equation_Vale.Def.Types_s.le_bytes_to_quad32_def",
"equation_Vale.Def.Words.Seq_s.seq_to_four_LE",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Interop.Views.get128_def",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_FStar.UInt8.v",
"function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val32",
"function_token_typing_Vale.Def.Types_s.le_bytes_to_quad32",
"function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.Interop.Views.get128", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"interpretation_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
"interpretation_Tm_abs_ad3ad425f83578beeb8ba014cbc730a3",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_528966909e656beff90629dc95073b2d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val32_def",
"token_correspondence_Vale.Def.Types_s.le_bytes_to_quad32_def",
"token_correspondence_Vale.Def.Words.Four_s.four_to_nat",
"token_correspondence_Vale.Interop.Views.get128_def",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_FStar.UInt8.t",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8"
],
0,
"2aab1ffab1d6b84204248f9a6f8e0855"
],
[
"Vale.X64.Memory.index128_get_heap_val128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Heap_s.correct_down",
"equation_Vale.Interop.Heap_s.correct_down_p",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.Interop.Views.up_view128",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.uint128_view",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.v_to_typ",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.Seq.Base.index", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"proj_equation_LowStar.BufferView.Up.View_get",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Types.Buffer_src",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_LowStar.BufferView.Up.View_get",
"refinement_interpretation_Tm_refine_00753086f0a5091e4281a2f51c385e86",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_37e4cb0cef5519eccc60c9f31370a875",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_9b11903c06962c65f1bc43f9bd25a2d5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b4c3192994dcc590bdf90a64a565ac51",
"refinement_interpretation_Tm_refine_bac48341d72c9512b36c265d7915272a",
"refinement_interpretation_Tm_refine_c1351167a99542736ca91bc659666fba",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"token_correspondence_LowStar.BufferView.Up.__proj__View__item__get",
"token_correspondence_Vale.Interop.Views.get128",
"token_correspondence_Vale.X64.Memory.v_to_typ",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
"typing_LowStar.BufferView.Up.as_seq",
"typing_LowStar.BufferView.Up.mk_buffer",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"3af5125e9c7f8bec2624a724772d7f4c"
],
[
"Vale.X64.Memory.lemma_modifies_goal_directed",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.modifies_goal_directed" ],
0,
"e9cd692456afacad3668c3854c1e82d2"
],
[
"Vale.X64.Memory.buffer_length_buffer_as_seq",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.uint_view",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"lemma_FStar.Seq.Base.lemma_init_len", "primitive_Prims.op_Modulus",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Types.Buffer_src",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"typing_FStar.UInt8.t", "typing_LowStar.BufferView.Up.as_seq",
"typing_LowStar.BufferView.Up.mk_buffer",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view"
],
0,
"fe9dc206040ca4044c4408015535fbb5"
],
[
"Vale.X64.Memory.same_underlying_seq",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.uint_view",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_Vale.Lib.BufferViewHelpers.lemma_uv_equal",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Types.Buffer_src",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_8ae5e7ec51c01b06a6c5c069c9bd60bc",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b10d136d804d19dcb00be7bd6d8c57c4",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.as_seq",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view", "typing_tok_Prims.LexTop@tok",
"well-founded-ordering-on-nat"
],
0,
"ae49655542d357d0221e32757c4fa3bc"
],
[
"Vale.X64.Memory.modifies_buffer_elim",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.b8_preorder",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.loc",
"equation_Vale.X64.Memory.loc_buffer",
"equation_Vale.X64.Memory.loc_disjoint",
"equation_Vale.X64.Memory.modifies",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"proj_equation_Vale.Interop.Types.Buffer_src",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.as_seq",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_as_seq"
],
0,
"13159c6ddd9e6cfda814125027033082"
],
[
"Vale.X64.Memory.modifies_buffer_addr",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.modifies",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs"
],
0,
"59ee41dec7e14362fb58208a3f022534"
],
[
"Vale.X64.Memory.modifies_buffer_readable",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.modifies"
],
0,
"c129f446ddc11758d9f3e8cf8fa9efd4"
],
[
"Vale.X64.Memory.loc_disjoint_none_r",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_disjoint",
"equation_Vale.X64.Memory.loc_none"
],
0,
"f4dc97ce78f61d524f68b7662c693df2"
],
[
"Vale.X64.Memory.loc_disjoint_union_r",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_disjoint",
"equation_Vale.X64.Memory.loc_union"
],
0,
"d8c92850dd0fd8013acce8268ebfd716"
],
[
"Vale.X64.Memory.loc_includes_refl",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.loc_includes" ],
0,
"f7f0653275c845105677ef140a5590da"
],
[
"Vale.X64.Memory.loc_includes_trans",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.loc_includes" ],
0,
"a3b40b5e986605a42143209afd5d4c99"
],
[
"Vale.X64.Memory.loc_includes_union_r",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.loc_union"
],
0,
"1e356905ffbb5a1998c926822211d337"
],
[
"Vale.X64.Memory.loc_includes_union_l",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.loc_union"
],
0,
"3e7bebaf9a814da0c9859524af19de2a"
],
[
"Vale.X64.Memory.loc_includes_union_l_buffer",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.loc_union"
],
0,
"15fb31196d25ab7675d674724045abfb"
],
[
"Vale.X64.Memory.loc_includes_none",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.loc_none"
],
0,
"cec00d9898be4225107d9841216fe0be"
],
[
"Vale.X64.Memory.modifies_refl",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Base.interop_heap",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.Set.lemma_equal_refl",
"proj_equation_Vale.Interop.Base.InteropHeap_hs",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_7ae5a5d89e52da1d5454233e706a9bd8",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_Vale.Interop.Base.__proj__InteropHeap__item__hs"
],
0,
"965775654e09193517a5e948ea8f088d"
],
[
"Vale.X64.Memory.modifies_goal_directed_refl",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Memory.modifies_goal_directed",
"equation_Vale.X64.Memory.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Base.interop_heap",
"lemma_Vale.X64.Memory.modifies_refl"
],
0,
"784f212d76937df4520084e6137f4589"
],
[
"Vale.X64.Memory.modifies_loc_includes",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Base.interop_heap"
],
0,
"704c762ae53da5446b261218bcac1d61"
],
[
"Vale.X64.Memory.modifies_trans",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Memory.loc_union",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Base.interop_heap",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"proj_equation_Vale.Interop.Base.InteropHeap_hs",
"refinement_interpretation_Tm_refine_7ae5a5d89e52da1d5454233e706a9bd8",
"typing_Vale.Interop.Base.__proj__InteropHeap__item__hs"
],
0,
"10fa9ca68212b8a476fdad08c59c0119"
],
[
"Vale.X64.Memory.modifies_goal_directed_trans",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.modifies_goal_directed",
"lemma_Vale.X64.Memory.loc_includes_refl",
"lemma_Vale.X64.Memory.loc_includes_union_r"
],
0,
"84e53f09e39292583b46b11d33a49a41"
],
[
"Vale.X64.Memory.modifies_goal_directed_trans2",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.modifies_goal_directed" ],
0,
"9b253995f16086713a40f9024df2515e"
],
[
"Vale.X64.Memory.default_of_typ",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt128",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt16",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt32",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt64",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt8", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat16", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
"inversion-interp", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"8364ce8a5f7f460ee08cac392bf63d3b"
],
[
"Vale.X64.Memory.buffer_read",
1,
0,
0,
[ "@query", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq" ],
0,
"5f2d13476ed04ab49141e5725612f7a3"
],
[
"Vale.X64.Memory.buffer_read",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.buffer",
"equation_Vale.X64.Memory.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Base.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_7c64067490892c791d00e02d4d1ae606"
],
0,
"70fe72a8dd3a7161f2fbc09fe42bf946"
],
[
"Vale.X64.Memory.seq_upd",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865", "bool_inversion",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_upd", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6d5ab57ac719f3d34aaa0ac8c62a3164",
"refinement_interpretation_Tm_refine_87f65bf36fef1b919603d458579dd2c0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Seq.Base.index", "typing_LowStar.BufferView.Up.as_seq",
"typing_LowStar.BufferView.Up.length", "typing_tok_Prims.LexTop@tok",
"well-founded-ordering-on-nat"
],
0,
"20c170f301a29e8c4c5ab1c0b4aa48c4"
],
[
"Vale.X64.Memory.buffer_write",
1,
0,
0,
[ "@query", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq" ],
0,
"79b76c63b694e6b7b6e3e73589dfaa44"
],
[
"Vale.X64.Memory.buffer_write",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Interop.Heap_s_pretyping_40dec2fdc42f7b5efafe5762d6761d53",
"b2t_def", "bool_inversion", "equation_FStar.Seq.Properties.lseq",
"equation_LowStar.BufferView.Down.buffer", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.b8_preorder",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.get_heaplet_id",
"equation_Vale.X64.Memory.loc_buffer",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.v_of_typ",
"fuel_guarded_inversion_FStar.Pervasives.dtuple4",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Seq.Base.index", "int_inversion",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"kinding_Vale.Interop.Heap_s.interop_heap@tok",
"lemma_FStar.Ghost.reveal_hide", "lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_upd",
"lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.Memory.lemma_v_to_of_typ",
"primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
"proj_equation_FStar.Pervasives.Mkdtuple4__1",
"proj_equation_FStar.Pervasives.Mkdtuple4__2",
"proj_equation_FStar.Pervasives.Mkdtuple4__3",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_heapletId",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_ih",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"proj_equation_Vale.Interop.Types.Buffer_src",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Arch.HeapImpl.ValeHeap_heapletId",
"projection_inverse_Vale.Arch.HeapImpl.ValeHeap_ih",
"projection_inverse_Vale.Interop.Heap_s.InteropHeap_addrs",
"projection_inverse_Vale.Interop.Heap_s.InteropHeap_hs",
"projection_inverse_Vale.Interop.Heap_s.InteropHeap_ptrs",
"refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_Vale.X64.Memory.v_to_typ",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.upd",
"typing_FStar.UInt8.t", "typing_LowStar.BufferView.Up.as_seq",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view", "typing_Vale.X64.Memory.v_of_typ"
],
0,
"5dcecdba5c9bf8118abb2915bba6fe41"
],
[
"Vale.X64.Memory.addr_in_ptr",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"Vale.X64.Memory_interpretation_Tm_arrow_c6d3514b44a5d23e21840ab42c97b95a",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.X64.Memory.scale_by",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5a79161a3dd9ab53bf9fe8b0d8ed8106",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc",
"typing_tok_Prims.LexTop@tok", "well-founded-ordering-on-nat"
],
0,
"a80b1bdf7dabccca2025e5ffc9f748cb"
],
[
"Vale.X64.Memory.get_addr_in_ptr",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
"constructor_distinct_Tm_unit", "equality_tok_Prims.LexTop@tok",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.valid_offset",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Vale.Interop.Types.view_n", "typing_tok_Prims.LexTop@tok",
"well-founded-ordering-on-nat"
],
0,
"8d414124fae102a129f03be9889333e8"
],
[
"Vale.X64.Memory.valid_buffer",
1,
0,
0,
[
"@query", "constructor_distinct_BoxInt",
"constructor_distinct_Tm_unit", "equation_Vale.Interop.Types.view_n",
"projection_inverse_BoxInt_proj_0"
],
0,
"ea8d91db05ec43bc7e434debe9091516"
],
[
"Vale.X64.Memory.valid_mem_aux",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_8f6e895a49590f9a95c242bbf7466dd9_3",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_2",
"binder_x_ae567c2fb75be05905677af440075565_1", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt16@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt32@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"false_interp", "fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"kinding_Vale.Interop.Types.b8@tok", "l_or-interp",
"lemma_FStar.Map.lemma_ContainsDom", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_541f1e3ffa4cb0ce48061607f4ffdae6",
"refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"subterm_ordering_Prims.Cons", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.X64.Memory.valid_buffer",
"typing_Vale.X64.Memory.valid_mem_aux"
],
0,
"71234324fbcb61f5b651adc0bcf68645"
],
[
"Vale.X64.Memory.valid_mem",
1,
1,
1,
[
"@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list"
],
0,
"7455e1e2a0869f7b0e4d46e6aa58e978"
],
[
"Vale.X64.Memory.find_valid_buffer_aux",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"lemma_FStar.Pervasives.invertOption",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_c1e93b92239b5fc8740b70715accee64",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Arch.HeapImpl.buffer"
],
0,
"8b198c8d111c5a7553d9ad62d8517777"
],
[
"Vale.X64.Memory.find_valid_buffer_aux",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.valid_mem_aux.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Memory.valid_mem_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_8f6e895a49590f9a95c242bbf7466dd9_3",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_2",
"binder_x_ae567c2fb75be05905677af440075565_1", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"equation_with_fuel_Vale.X64.Memory.valid_mem_aux.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"kinding_Vale.Interop.Types.b8@tok", "l_or-interp",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fe1f3df3f116883725cc7f3aa34f4080",
"subterm_ordering_Prims.Cons", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Arch.HeapImpl._ih", "typing_Vale.Arch.HeapImpl.buffer",
"typing_Vale.X64.Memory.valid_mem_aux"
],
0,
"58d7964891e5cf088fae6276f1fcb54d"
],
[
"Vale.X64.Memory.find_valid_buffer",
1,
1,
1,
[
"@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list"
],
0,
"d597c0d84cd975573b37207bb54401cf"
],
[
"Vale.X64.Memory.find_valid_buffer_aux_ps",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_Prims.squash", "l_and-interp",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"7cbfeb7f8821d64a6da22536428936f9"
],
[
"Vale.X64.Memory.find_valid_buffer_aux_ps",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.find_valid_buffer_aux.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Memory.find_valid_buffer_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_8f6e895a49590f9a95c242bbf7466dd9_3",
"binder_x_8f6e895a49590f9a95c242bbf7466dd9_4",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_2",
"binder_x_ae567c2fb75be05905677af440075565_1", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt16@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt32@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.pos",
"equation_Prims.squash", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"equation_with_fuel_Vale.X64.Memory.find_valid_buffer_aux.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "int_typing", "kinding_Vale.Interop.Types.b8@tok",
"l_and-interp", "l_or-interp", "lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_AmpAmp",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_92021f726392e5bad2e8fce80b5e9a8b",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"subterm_ordering_Prims.Cons", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_Vale.Arch.HeapImpl._ih", "typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.find_valid_buffer_aux",
"typing_Vale.X64.Memory.scale_by"
],
0,
"72b15edf28943d486eae310893e6ad41"
],
[
"Vale.X64.Memory.find_valid_buffer_ps",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.find_valid_buffer",
"equation_Vale.X64.Memory.sub_list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"int_inversion"
],
0,
"52f96a11a02232eda881990372d8d391"
],
[
"Vale.X64.Memory.find_valid_buffer_valid_offset",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"bool_inversion", "data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Arch.HeapImpl.ValeHeap",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"disc_equation_FStar.Pervasives.Native.None",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt16@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt32@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.find_valid_buffer",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "kinding_Vale.Interop.Heap_s.interop_heap@tok",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_ih",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699",
"refinement_interpretation_Tm_refine_92021f726392e5bad2e8fce80b5e9a8b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_e71863c9702f0243be00371e81c075e8",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_FStar.Ghost.reveal", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Arch.HeapImpl._ih", "typing_Vale.Arch.HeapImpl.buffer",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.find_valid_buffer",
"typing_Vale.X64.Memory.find_valid_buffer_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt16@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt32@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"7f7bb109a4e2f428fedf1f1f4339d10b"
],
[
"Vale.X64.Memory.writeable_mem_aux",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"b2t_def", "binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_8f6e895a49590f9a95c242bbf7466dd9_3",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_2",
"binder_x_ae567c2fb75be05905677af440075565_1", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_elim_Vale.Interop.Types.Buffer",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt16@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt32@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.writeable_buffer",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"false_interp", "fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"kinding_Vale.Interop.Types.b8@tok", "l_or-interp",
"lemma_FStar.Map.lemma_ContainsDom", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_0309fb9650d237a486c5dceda5246c92",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_257f34044a0ca6d5caaa8860ef678921",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"subterm_ordering_Prims.Cons", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.valid_buffer",
"typing_Vale.X64.Memory.writeable_buffer",
"typing_Vale.X64.Memory.writeable_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"9d97f692702384609ce38f7244d399af"
],
[
"Vale.X64.Memory.writeable_mem",
1,
1,
1,
[
"@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list"
],
0,
"c35e418adabed0dd57ec4287308ac052"
],
[
"Vale.X64.Memory.find_writeable_buffer_aux",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"lemma_FStar.Pervasives.invertOption",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_c1e93b92239b5fc8740b70715accee64",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Arch.HeapImpl.buffer"
],
0,
"758182a0e4ade17968b62c6d7ef2b96b"
],
[
"Vale.X64.Memory.find_writeable_buffer_aux",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.writeable_mem_aux.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Memory.writeable_mem_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_8f6e895a49590f9a95c242bbf7466dd9_3",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_2",
"binder_x_ae567c2fb75be05905677af440075565_1", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.writeable_buffer",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"equation_with_fuel_Vale.X64.Memory.writeable_mem_aux.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"kinding_Vale.Interop.Types.b8@tok", "l_or-interp",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_257f34044a0ca6d5caaa8860ef678921",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fe1f3df3f116883725cc7f3aa34f4080",
"subterm_ordering_Prims.Cons", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Arch.HeapImpl._ih", "typing_Vale.Arch.HeapImpl.buffer",
"typing_Vale.X64.Memory.writeable_mem_aux"
],
0,
"451a651003064b55915e4a4886a4e6a4"
],
[
"Vale.X64.Memory.find_writeable_buffer",
1,
1,
1,
[
"@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list"
],
0,
"e60a8166d06dd70468443973ec102a92"
],
[
"Vale.X64.Memory.load_mem",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"constructor_distinct_FStar.Pervasives.Native.Some",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.find_valid_buffer",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "primitive_Prims.op_AmpAmp",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_92021f726392e5bad2e8fce80b5e9a8b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.find_valid_buffer_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"f8597b935e785690b7a0b3f6aab593be"
],
[
"Vale.X64.Memory.length_t_eq",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.X64.Memory.buffer_length",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_Vale.Interop.Types.b8", "int_inversion",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"primitive_Prims.op_Modulus",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Types.Buffer_src",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6042c299b005b6766d280ae906dedfbc",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.length",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.uint_view"
],
0,
"00a0476385acce19964b431065fd1b68"
],
[
"Vale.X64.Memory.get_addr_ptr",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.find_valid_buffer",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"int_inversion", "primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_92021f726392e5bad2e8fce80b5e9a8b",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.X64.Memory.find_valid_buffer_aux",
"typing_Vale.X64.Memory.valid_mem"
],
0,
"32ec67b554e8b03df3d7ca67ed39fed1"
],
[
"Vale.X64.Memory.load_buffer_read",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"b2t_def", "constructor_distinct_Tm_unit", "equation_Prims.nat",
"equation_Prims.pos", "equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.find_valid_buffer",
"equation_Vale.X64.Memory.get_addr_ptr",
"equation_Vale.X64.Memory.load_mem",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem",
"equation_Vale.X64.Memory.valid_offset",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Some_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_92021f726392e5bad2e8fce80b5e9a8b",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.find_valid_buffer_aux",
"typing_Vale.X64.Memory.uint_view"
],
0,
"d28b6dfb9e66c6758fa47356a2b61e16"
],
[
"Vale.X64.Memory.store_mem",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"b2t_def", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Tm_unit",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_write",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.find_writeable_buffer",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"equation_Vale.X64.Memory.writeable_buffer",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "lemma_FStar.Pervasives.invertOption",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_GreaterThanOrEqual",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_4222c0a0845174bddfc525ea3f317b0e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Arch.HeapImpl._ih", "typing_Vale.Arch.HeapImpl.buffer",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.find_writeable_buffer_aux",
"typing_Vale.X64.Memory.uint_view",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"1beb2f0e16938dadf8834fc17eb2194e"
],
[
"Vale.X64.Memory.store_buffer_write",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"b2t_def", "bool_inversion", "constructor_distinct_Tm_unit",
"disc_equation_FStar.Pervasives.Native.Some", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.find_writeable_buffer",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.store_mem",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"equation_Vale.X64.Memory.writeable_buffer",
"equation_Vale.X64.Memory.writeable_mem",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_src",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_257f34044a0ca6d5caaa8860ef678921",
"refinement_interpretation_Tm_refine_4222c0a0845174bddfc525ea3f317b0e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_aa311741644f2a2768d777f8e523a38c",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.find_writeable_buffer_aux",
"typing_Vale.X64.Memory.uint_view",
"typing_Vale.X64.Memory.writeable_mem",
"typing_Vale.X64.Memory.writeable_mem_aux"
],
0,
"ae8e0209cbac23c95284bc84a4c404aa"
],
[
"Vale.X64.Memory.valid_mem128",
1,
0,
0,
[
"@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list"
],
0,
"6bcd4364e8c93bdeffbdc50d8bf982b6"
],
[
"Vale.X64.Memory.writeable_mem128",
1,
0,
0,
[
"@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list"
],
0,
"8e4dabf946ff3a292d0661442dad8f84"
],
[
"Vale.X64.Memory.lemma_valid_mem64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem",
"equation_Vale.X64.Memory.valid_mem64",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"139ac7585532905fbbc31dda931f4e6a"
],
[
"Vale.X64.Memory.lemma_writeable_mem64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.writeable_mem",
"equation_Vale.X64.Memory.writeable_mem64",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8", "int_inversion",
"int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_257f34044a0ca6d5caaa8860ef678921",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.writeable_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"768dcd8c2c4a1acc170c0b25caaf0a7f"
],
[
"Vale.X64.Memory.lemma_store_mem",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Memory.get_addr_in_ptr.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.writeable_mem_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Heap_s_interpretation_Tm_arrow_49af84408b2fd68795c64e188f731e93",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"b2t_def", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Tm_unit",
"disc_equation_FStar.Pervasives.Native.None",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Prims.squash", "equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Heap_s.disjoint_or_eq_b8",
"equation_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8_preorder",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.disjoint_addr",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_write",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.find_writeable_buffer",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.store_mem",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"equation_Vale.X64.Memory.writeable_buffer",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"function_token_typing_Vale.Interop.Heap_s.list_disjoint_or_eq",
"function_token_typing_Vale.Interop.Types.addr_map_pred",
"int_inversion", "int_typing",
"interpretation_Tm_abs_0b45d135b1bf428b90ecd044d0c4f361",
"l_and-interp", "l_quant_interp_bd1f5246e6f57b3b0174bc6d256820c5",
"lemma_FStar.Pervasives.invertOption",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"proj_equation_Vale.Interop.Types.Buffer_src",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_257f34044a0ca6d5caaa8860ef678921",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4222c0a0845174bddfc525ea3f317b0e",
"refinement_interpretation_Tm_refine_45eda407d0825ef421aab011ebbcaeff",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"token_correspondence_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
"typing_LowStar.BufferView.Down.length",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Vale.Arch.HeapImpl._ih", "typing_Vale.Arch.HeapImpl.buffer",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.find_writeable_buffer_aux",
"typing_Vale.X64.Memory.get_addr_in_ptr",
"typing_Vale.X64.Memory.uint_view",
"typing_Vale.X64.Memory.writeable_mem_aux"
],
0,
"1b13f3c236a91f892e2a4fc4ec257995"
],
[
"Vale.X64.Memory.lemma_load_mem64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"3019701ac9aa241997bd3b5c1363fdf7"
],
[
"Vale.X64.Memory.lemma_load_mem64",
2,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Memory.get_addr_in_ptr.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.valid_mem_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Heap_s.disjoint_or_eq_b8",
"equation_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8_preorder",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.disjoint_addr",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.buffer_read",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.default_of_typ",
"equation_Vale.X64.Memory.find_valid_buffer",
"equation_Vale.X64.Memory.load_mem",
"equation_Vale.X64.Memory.load_mem64",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem",
"equation_Vale.X64.Memory.valid_mem64",
"equation_Vale.X64.Memory.valid_offset",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Vale.Interop.Heap_s.list_disjoint_or_eq",
"function_token_typing_Vale.Interop.Types.addr_map_pred",
"function_token_typing_Vale.X64.Memory.buffer64", "int_inversion",
"int_typing",
"interpretation_Tm_abs_0b45d135b1bf428b90ecd044d0c4f361",
"l_and-interp", "l_quant_interp_bd1f5246e6f57b3b0174bc6d256820c5",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Pervasives.invertOption",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Negation",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_45eda407d0825ef421aab011ebbcaeff",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_92021f726392e5bad2e8fce80b5e9a8b",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"token_correspondence_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_FStar.UInt8.t", "typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.find_valid_buffer_aux",
"typing_Vale.X64.Memory.get_addr_in_ptr",
"typing_Vale.X64.Memory.uint_view",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"d5b9563a624cad072a383e9b63128f4c"
],
[
"Vale.X64.Memory.lemma_store_mem64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
"equation_Prims.squash", "l_and-interp",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"9fa733ad5a70677108ee818fc1afb94b"
],
[
"Vale.X64.Memory.lemma_store_mem64",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.store_mem64",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem",
"equation_Vale.X64.Memory.valid_mem64",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8", "int_inversion",
"int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_Negation",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.store_mem64",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"3663bc5e148640b891c94620d946011e"
],
[
"Vale.X64.Memory.lemma_valid_mem128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem128",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"87101f485210eff3017319c20bc0be7f"
],
[
"Vale.X64.Memory.lemma_writeable_mem128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.writeable_mem128",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8", "int_inversion",
"int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_257f34044a0ca6d5caaa8860ef678921",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.writeable_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"c61aeaef27043a7bbd328b68c1f29d95"
],
[
"Vale.X64.Memory.lemma_load_mem128",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Memory.get_addr_in_ptr.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.valid_mem_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Heap_s.disjoint_or_eq_b8",
"equation_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8_preorder",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.disjoint_addr",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.find_valid_buffer",
"equation_Vale.X64.Memory.load_mem",
"equation_Vale.X64.Memory.load_mem128",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem128",
"equation_Vale.X64.Memory.valid_offset",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Vale.Interop.Heap_s.list_disjoint_or_eq",
"function_token_typing_Vale.Interop.Types.addr_map_pred",
"int_inversion", "int_typing",
"interpretation_Tm_abs_0b45d135b1bf428b90ecd044d0c4f361",
"l_and-interp", "l_quant_interp_bd1f5246e6f57b3b0174bc6d256820c5",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Negation",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_45eda407d0825ef421aab011ebbcaeff",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_92021f726392e5bad2e8fce80b5e9a8b",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"token_correspondence_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt8.t",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.find_valid_buffer_aux",
"typing_Vale.X64.Memory.get_addr_in_ptr",
"typing_Vale.X64.Memory.uint_view",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"ac6a9d8840d5167c8aec3b2b2ad145e3"
],
[
"Vale.X64.Memory.lemma_store_mem128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
"equation_Prims.squash", "l_and-interp",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"e7da9f646d03180dc1c715ab0b5f2d2a"
],
[
"Vale.X64.Memory.lemma_store_mem128",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.store_mem128",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem128",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8", "int_inversion",
"int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_Negation",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.store_mem128",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"f1ced8423574dcac1c0c5235919cc4f5"
],
[
"Vale.X64.Memory.apply_taint_buf",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.X64.Memory.valid_taint_b8",
"equation_Vale.X64.Memory.valid_taint_buf",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"int_inversion", "int_typing",
"l_quant_interp_eec16fb10e3c0be0be37de5656d5d0d7",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"8e2d01dd1d785c03c97461802d3417fd"
],
[
"Vale.X64.Memory.lemma_valid_taint64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.nat", "equation_Vale.Interop.Types.view_n",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.valid_taint_b8",
"equation_Vale.X64.Memory.valid_taint_buf",
"equation_Vale.X64.Memory.valid_taint_buf64",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"int_inversion", "l_quant_interp_eec16fb10e3c0be0be37de5656d5d0d7",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ed56f0a463ff0657a36c83fe878c0439"
],
0,
"719cb493380bc61c0156e599279d4f54"
],
[
"Vale.X64.Memory.lemma_valid_taint128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat", "equation_Vale.Interop.Types.view_n",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.valid_taint_buf128", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1351167a99542736ca91bc659666fba"
],
0,
"5ffb38b078085437879a0df1f4f6af9c"
],
[
"Vale.X64.Memory.same_memTaint",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
"equation_Prims.eqtype", "equation_Vale.Arch.HeapTypes_s.memTaint_t",
"equation_Vale.X64.Memory.memtaint",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "int_inversion",
"kinding_Vale.Arch.HeapTypes_s.taint@tok",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_equal_elim",
"lemma_FStar.Map.lemma_equal_intro",
"lemma_FStar.Set.lemma_equal_elim",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_c2c488db3214c38826155caf10d30036",
"typing_FStar.Map.domain", "typing_FStar.Set.complement",
"typing_FStar.Set.empty",
"typing_tok_Vale.Arch.HeapTypes_s.Public@tok"
],
0,
"14d403f216cc3d513b88acdc64886018"
],
[
"Vale.X64.Memory.modifies_valid_taint",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.valid_taint_b8",
"equation_Vale.X64.Memory.valid_taint_buf",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_typing", "l_quant_interp_eec16fb10e3c0be0be37de5656d5d0d7",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9bdf64b2660adb592eaffa73ced680cc",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca"
],
0,
"ee6a0bf1f5181a6025a50191b01ca550"
],
[
"Vale.X64.Memory.modifies_same_heaplet_id",
1,
1,
1,
[
"@query", "equation_Vale.X64.Memory.get_heaplet_id",
"equation_Vale.X64.Memory.modifies"
],
0,
"dd95284f233fbc39bfb6801ef81245bc"
],
[
"Vale.X64.Memory.init_heaplets_req",
1,
1,
1,
[ "@query" ],
0,
"34325edef73c119aef4f51b8799348dd"
],
[
"Vale.X64.Memory.loc_mutable_buffers",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_3f2ea7e07cd8972f5ae069cf16ee234e_0",
"data_elim_Prims.Cons", "disc_equation_Prims.Cons",
"disc_equation_Prims.Nil",
"disc_equation_Vale.Arch.HeapImpl.Immutable",
"disc_equation_Vale.Arch.HeapImpl.Mutable",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.buffer_info",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.mutability",
"proj_equation_Prims.Cons_hd",
"proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_mutable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons",
"typing_Vale.Arch.HeapImpl.__proj__Mkbuffer_info__item__bi_mutable"
],
0,
"6c760799e37bab658aec4da0d8682b6a"
],
[
"Vale.X64.Memory.write_taint_lemma",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
"equation_Prims.squash", "l_and-interp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"687a1771f2feedaf7a6fd4dc41c22ea9"
],
[
"Vale.X64.Memory.write_taint_lemma",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Interop.Base.write_taint.fuel_instrumented",
"@fuel_irrelevance_Vale.Interop.Base.write_taint.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"Vale.Interop.Base_interpretation_Tm_ghost_arrow_6b4b417e1383ee3b4792f0b5428180ab",
"Vale.X64.Memory_interpretation_Tm_ghost_arrow_2d7469efb5ea1a486ea676065315b855",
"b2t_def", "binder_x_40dec2fdc42f7b5efafe5762d6761d53_1",
"binder_x_6d4cfc2a8480745fc461c4428588c8e0_3",
"binder_x_9cdee1dee4a021122574b44c25299169_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_e7fff4bad6aea127cbbd202a00eaae18_4", "bool_inversion",
"bool_typing", "data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_elim_Vale.Interop.Types.Buffer",
"data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.eqtype",
"equation_Prims.l_Forall", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.Arch.HeapTypes_s.memTaint_t",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.memtaint",
"equation_with_fuel_Vale.Interop.Base.write_taint.fuel_instrumented",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.taint",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.int", "int_inversion", "int_typing",
"kinding_Vale.Arch.HeapTypes_s.taint@tok", "l_and-interp",
"l_quant_interp_1e77134a67a9a168a843bbc4a6ae3587",
"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.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5e8a4b3047c38f1ce9b8b1959bab0bd7",
"refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699",
"refinement_interpretation_Tm_refine_c2c488db3214c38826155caf10d30036",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Set.complement", "typing_FStar.Set.empty",
"typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.length",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.get_downview",
"typing_tok_Prims.LexTop@tok",
"typing_tok_Vale.Arch.HeapTypes_s.Public@tok",
"typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"well-founded-ordering-on-nat"
],
0,
"4f55025db81dff4c3402f7beb299ed64"
],
[
"Vale.X64.Memory.valid_memtaint",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@query",
"FStar.List.Tot.Base_interpretation_Tm_ghost_arrow_d7e9834b8fd0407a723f5f3f4b012fdd",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"Vale.Interop.Base_interpretation_Tm_ghost_arrow_65ec90b9a641de16cd2204a5fec1203d",
"Vale.Interop.Base_interpretation_Tm_ghost_arrow_6b4b417e1383ee3b4792f0b5428180ab",
"Vale.X64.Memory_interpretation_Tm_ghost_arrow_2d7469efb5ea1a486ea676065315b855",
"binder_x_8f6e895a49590f9a95c242bbf7466dd9_0",
"binder_x_9cdee1dee4a021122574b44c25299169_2",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_1", "bool_inversion",
"bool_typing", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil",
"data_elim_Vale.Arch.HeapImpl.ValeHeap",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_elim_Vale.Interop.Types.Buffer",
"data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapTypes_s.memTaint_t",
"equation_Vale.Interop.Base.create_memtaint",
"equation_Vale.Interop.Heap_s.disjoint_or_eq_b8",
"equation_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8_preorder",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.disjoint_addr",
"equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.valid_taint_b8",
"equation_Vale.X64.Memory.valid_taint_bufs",
"equation_with_fuel_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"false_interp", "fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Interop.Base.write_taint",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"function_token_typing_Vale.Interop.Heap_s.list_disjoint_or_eq",
"function_token_typing_Vale.Interop.Types.addr_map_pred",
"int_typing",
"interpretation_Tm_abs_0b45d135b1bf428b90ecd044d0c4f361",
"kinding_Vale.Arch.HeapTypes_s.taint@tok",
"kinding_Vale.Interop.Heap_s.interop_heap@tok",
"kinding_Vale.Interop.Types.b8@tok", "l_and-interp", "l_or-interp",
"l_quant_interp_bd1f5246e6f57b3b0174bc6d256820c5",
"l_quant_interp_eec16fb10e3c0be0be37de5656d5d0d7",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomConstMap",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty",
"primitive_Prims.op_BarBar", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Negation",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_ih",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"proj_equation_Vale.Interop.Types.Buffer_src",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5e8a4b3047c38f1ce9b8b1959bab0bd7",
"refinement_interpretation_Tm_refine_c2c488db3214c38826155caf10d30036",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_e71863c9702f0243be00371e81c075e8",
"refinement_kinding_Tm_refine_c2c488db3214c38826155caf10d30036",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Interop.Base.write_taint",
"token_correspondence_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"typing_FStar.Ghost.reveal", "typing_FStar.Map.const",
"typing_FStar.Map.domain", "typing_FStar.Set.complement",
"typing_FStar.Set.empty", "typing_FStar.Set.mem",
"typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.length",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.get_downview",
"typing_tok_Vale.Arch.HeapTypes_s.Public@tok"
],
0,
"c8ba0e27dee99da079d3705f6d073e8b"
],
[
"Vale.X64.Memory.valid_layout_data_buffer",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl.buffer",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"typing_Vale.Interop.Types.view_n"
],
0,
"6ec753eb893213554043f869de2f6f70"
],
[
"Vale.X64.Memory.valid_layout_buffer_id",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Vale.Arch.HeapImpl.heaplet_id",
"lemma_FStar.Pervasives.invertOption",
"projection_inverse_BoxBool_proj_0",
"refinement_kinding_Tm_refine_c365eb902b454950de62fba701d9049d",
"typing_FStar.Pervasives.Native.uu___is_Some"
],
0,
"67dbe9f95c501e4be1f2a2d8486bbb42"
],
[
"Vale.X64.Memory.inv_heaplet",
1,
1,
1,
[ "@query" ],
0,
"275d28dcad6291e87a1baddca7819f85"
],
[
"Vale.X64.Memory.inv_heaplets",
1,
1,
1,
[ "@query" ],
0,
"9e7ed69a3b751ec57d0045551332c6e7"
],
[
"Vale.X64.Memory.heaps_match",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.HeapImpl.buffer",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc"
],
0,
"196d62e174d379fc91276542384b3eb9"
],
[
"Vale.X64.Memory.lemma_heaps_match",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
"equation_Prims.squash", "equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.X64.Memory.buffer_info_has_id", "l_and-interp",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc"
],
0,
"edf3dbd812f10b59aa0fddf820f53edf"
],
[
"Vale.X64.Memory.lemma_heaps_match",
2,
1,
1,
[
"@query", "equation_Vale.X64.Memory.buffer_info_has_id",
"equation_Vale.X64.Memory.heaps_match",
"proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet"
],
0,
"0a3b22354a68182b7a758fc6dfd9c9f5"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...