Revision 027cee49342e5e1ac0ccf4ca6e4b5b868e70a0a2 authored by Aseem Rastogi on 22 March 2020, 07:14:03 UTC, committed by Aseem Rastogi on 22 March 2020, 07:14:03 UTC
1 parent df0c85e
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,
"7b46270236fd5d3ec589feb72bf56818"
],
[
"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,
"b29a528b874fd2e14f79bcc5788bdcf8"
],
[
"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,
"47f828384ef90fa7f7e9a3c71c3727ab"
],
[
"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,
"038ccddd9f69c03954e31fe74738c0c5"
],
[
"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,
"9b5a12c3e6a6994651e9d11a85fdb48e"
],
[
"Vale.X64.Memory.buffer_as_seq",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.HeapImpl.buffer",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc"
],
0,
"cb967c43f7594eaf42d4aa958655d0c3"
],
[
"Vale.X64.Memory.buffer_length",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.HeapImpl.buffer",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc"
],
0,
"fd32d099a42c0c8df35cbea630587f69"
],
[
"Vale.X64.Memory.modifies",
1,
2,
1,
[ "@query" ],
0,
"f305e93c129b85e775ec44a0d436b7c4"
],
[
"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.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"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.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.t",
"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_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.length", "typing_FStar.UInt64.v",
"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,
"ad3a31e11958a4c47b184b9d9e4c71ed"
],
[
"Vale.X64.Memory.index_helper",
1,
2,
1,
[ "@query" ],
0,
"5e18179cfe082679fb62063ac0da9c9e"
],
[
"Vale.X64.Memory.index_mul_helper",
1,
2,
1,
[
"@query", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0"
],
0,
"3c42384216d078e439db2c122f2ab096"
],
[
"Vale.X64.Memory.index64_get_heap_val64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_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.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_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_FStar.UInt8.t",
"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",
"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_56096fe58a1a28fa9111e3bcee03c9a3",
"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_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_da4c19f66d305c887fb7cacf453b6648",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc",
"refinement_interpretation_Tm_refine_ecabe6d1a66ca016d7a422c6ed32bef0",
"refinement_interpretation_Tm_refine_ed56f0a463ff0657a36c83fe878c0439",
"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.Seq.Base.length",
"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.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,
"ece629d21d5e48467bd47312113f5f3c"
],
[
"Vale.X64.Memory.index128_get_heap_val128_aux",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.X64.Memory_interpretation_Tm_arrow_efe96bb9514bece12be080c2a3348ae5",
"equation_FStar.Seq.Properties.lseq", "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.t",
"function_token_typing_FStar.UInt8.v",
"function_token_typing_Prims.__cache_version_number__",
"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_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.length",
"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,
"d29686d0179902b30b9eb4d8b222ab61"
],
[
"Vale.X64.Memory.index128_get_heap_val128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_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.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_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_FStar.UInt8.t", "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",
"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_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_56096fe58a1a28fa9111e3bcee03c9a3",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b4c3192994dcc590bdf90a64a565ac51",
"refinement_interpretation_Tm_refine_c1351167a99542736ca91bc659666fba",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_da4c19f66d305c887fb7cacf453b6648",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc",
"refinement_interpretation_Tm_refine_e612ea51789c75cd9f0bbfd437d2161d",
"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_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.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,
"fa2570eeeb10a4c02f4ace8a62343c9e"
],
[
"Vale.X64.Memory.lemma_modifies_goal_directed",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.modifies_goal_directed" ],
0,
"1fd66a5342595950d0d4aa8295695e22"
],
[
"Vale.X64.Memory.buffer_length_buffer_as_seq",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_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.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_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_FStar.UInt8.t",
"lemma_FStar.Seq.Base.lemma_init_len", "primitive_Prims.op_Modulus",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"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_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc",
"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.get_downview",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view"
],
0,
"7a2228a1fcda45da02455b85b2adb97f"
],
[
"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.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_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"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",
"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_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc",
"typing_LowStar.BufferView.Down.as_seq",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.base_typ_as_type",
"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,
"2cc8f22eb26197c5e4e1adb1bea3b867"
],
[
"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.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_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.UInt8.t",
"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",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc",
"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.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_as_seq"
],
0,
"4e93ce080273e6f856369ea9ccc3562b"
],
[
"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,
"1c03a4c821fa50002aa2e3d1d75cfcbd"
],
[
"Vale.X64.Memory.modifies_buffer_readable",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.modifies"
],
0,
"b291d6ba2c6daec965f40f4d050f30be"
],
[
"Vale.X64.Memory.loc_disjoint_none_r",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_disjoint",
"equation_Vale.X64.Memory.loc_none"
],
0,
"7263e3464d9dcaaf1346449e0ea096df"
],
[
"Vale.X64.Memory.loc_disjoint_union_r",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_disjoint",
"equation_Vale.X64.Memory.loc_union"
],
0,
"74c6e842a43dd88edf257d5e955bb120"
],
[
"Vale.X64.Memory.loc_includes_refl",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.loc_includes" ],
0,
"2f65da6317ef1ad45cfa51a78f85ce65"
],
[
"Vale.X64.Memory.loc_includes_trans",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.loc_includes" ],
0,
"8c1faf4eb088b0665915f700eac5419d"
],
[
"Vale.X64.Memory.loc_includes_union_r",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.loc_union"
],
0,
"8aa8e9e9d69eddc0693c0f9f8f2f38b0"
],
[
"Vale.X64.Memory.loc_includes_union_l",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.loc_union"
],
0,
"5a7753201496014de68f0056e625e284"
],
[
"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,
"5dc16257fd3330853de9e9a5dcc12139"
],
[
"Vale.X64.Memory.loc_includes_none",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.loc_none"
],
0,
"8783b3713c65328d03fb8361992cf0b9"
],
[
"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,
"dd0abbeede43b1a2bb49c486f7f50761"
],
[
"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,
"d6f60dd95ad9b9d77469c92e7c52de01"
],
[
"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,
"51bf162d612424b83f0acccd8ec1ea1c"
],
[
"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,
"b8f02c7816f779c42f14bf9b9bafe2dd"
],
[
"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,
"a18d6627b2bb7a8ab867ff92eabc8550"
],
[
"Vale.X64.Memory.modifies_goal_directed_trans2",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.modifies_goal_directed" ],
0,
"7033f4b7a1e8254b884c80232a6e07e1"
],
[
"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,
"ec947afc3057a4d39547eab7cc434160"
],
[
"Vale.X64.Memory.buffer_read",
1,
0,
0,
[ "@query", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq" ],
0,
"cdbe919df4809bf13a026701744f8247"
],
[
"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,
"88258aaad56ed410e59b43634eee7610"
],
[
"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,
"8fdda7e0efc03718478ede84894968b4"
],
[
"Vale.X64.Memory.buffer_write",
1,
0,
0,
[ "@query", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq" ],
0,
"00aa0ce740ca5a1bd7383f0ca58e3a30"
],
[
"Vale.X64.Memory.buffer_write",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_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_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_FStar.UInt8.t", "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_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc",
"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_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,
"e294b836f2b2f458db72327e56fe6781"
],
[
"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,
"95231905993977c77cd09f84c8cb3a9e"
],
[
"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,
"2279683f209ab4c6365ceb1d37aed3a2"
],
[
"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,
"f1064ab68617bd43aa1f3b50659fe4c6"
],
[
"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",
"function_token_typing_Prims.__cache_version_number__",
"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_e5f0372e4b8607a08675a75fa5d733cc",
"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,
"8e6476939d3caa1832645d469b6abdbd"
],
[
"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,
"488f220bf826402b6447f1e4536dc3b1"
],
[
"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,
"2bea2d772e4f3c25e214f6db856adf8c"
],
[
"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",
"function_token_typing_Prims.__cache_version_number__",
"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_e5f0372e4b8607a08675a75fa5d733cc",
"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,
"a3bc576ca68774f800e24d603adf5a35"
],
[
"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,
"86197d6f529a3f3edb4794b905c9a7c0"
],
[
"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,
"6fb7c711e2b01a343b2fa1859744f9ff"
],
[
"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,
"321b591e1d7ea8425ac9144b8bef706e"
],
[
"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,
"bb24912766dec724b545c9e13e551543"
],
[
"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_e5f0372e4b8607a08675a75fa5d733cc",
"refinement_interpretation_Tm_refine_e71863c9702f0243be00371e81c075e8",
"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_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.Interop.Types.view_n", "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",
"function_token_typing_Prims.__cache_version_number__",
"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_e5f0372e4b8607a08675a75fa5d733cc",
"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_FStar.Monotonic.HyperStack.get_tip",
"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.TUInt16@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"2068d09c928e6e9c6c7b7c0cb80412c5"
],
[
"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,
"195e47a8cebd60efaa60502de7c91cb9"
],
[
"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,
"57f53a3fddef5f6fb8cc8c1efe406ac1"
],
[
"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",
"function_token_typing_Prims.__cache_version_number__",
"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_e5f0372e4b8607a08675a75fa5d733cc",
"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,
"2106ec3d80492b98bf1e9bf5846a8697"
],
[
"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,
"b14a0d23f3696b94c7b58ca102bb34b7"
],
[
"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_e5f0372e4b8607a08675a75fa5d733cc",
"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.view_n",
"equation_Vale.X64.Memory.buffer_length",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.UInt8.t", "int_inversion",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"primitive_Prims.op_Modulus",
"proj_equation_LowStar.BufferView.Up.View_n",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_61fd48df593a301427376419b4c16bc3",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc",
"typing_LowStar.BufferView.Down.length",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.uint_view"
],
0,
"687a7bed07e007af6880693a0049a12f"
],
[
"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,
"c6ea25de80b6bd714ec9b8612e4bd4eb"
],
[
"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_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc",
"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,
"ff2e44afbb11ca287d52423e3fce76f0"
],
[
"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_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc",
"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,
"70126526ae027fdb9a052dd6f7b0e7b4"
],
[
"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.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.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_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_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc",
"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__writeable",
"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,
"fa107e3d02fcf39e31b3377a14db596d"
],
[
"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,
"bef33506de742b94cb3f00901c85a515"
],
[
"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",
"function_token_typing_Prims.__cache_version_number__",
"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_e5f0372e4b8607a08675a75fa5d733cc",
"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,
"8e0c0ae99c7e4674f8019ea18c57d11c"
],
[
"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",
"function_token_typing_Prims.__cache_version_number__",
"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_e5f0372e4b8607a08675a75fa5d733cc",
"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,
"aa12b665f74d725f9c5769ab420535fb"
],
[
"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.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.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"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_e14098f86a865715fec85e921cb76329",
"l_and-interp", "l_quant_interp_5065bafc42b9acd51fbc0726cf70a262",
"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_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_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc",
"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_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.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,
"731f4ece2eb12acb798f31b4922fbe84"
],
[
"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,
"e257e2cf052811e7f68f98e331117db7"
],
[
"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_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"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_e14098f86a865715fec85e921cb76329",
"l_and-interp", "l_quant_interp_5065bafc42b9acd51fbc0726cf70a262",
"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_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_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc",
"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_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,
"872d5496d3c19558c71f6c4de7eeb5c7"
],
[
"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,
"b9e2d4e591fe6b2e5e70474b8159aee9"
],
[
"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",
"function_token_typing_Prims.__cache_version_number__",
"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_e5f0372e4b8607a08675a75fa5d733cc",
"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,
"537d1d14d2c2a15be192ab124bbe07e1"
],
[
"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",
"function_token_typing_Prims.__cache_version_number__",
"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_e5f0372e4b8607a08675a75fa5d733cc",
"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,
"25c1eb2f152492b8b6b2a6d69d00827d"
],
[
"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",
"function_token_typing_Prims.__cache_version_number__",
"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_e5f0372e4b8607a08675a75fa5d733cc",
"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,
"760a95a592faedd4abfd1d07cdd7950d"
],
[
"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_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"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_e14098f86a865715fec85e921cb76329",
"l_and-interp", "l_quant_interp_5065bafc42b9acd51fbc0726cf70a262",
"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_d2179e9e4c59ec138821d558895d918b",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc",
"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_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,
"67d9e624d77e7c035774e5bc13a601ac"
],
[
"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,
"d5dfd75d72c06ab2108c9f5dff1af763"
],
[
"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",
"function_token_typing_Prims.__cache_version_number__",
"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_e5f0372e4b8607a08675a75fa5d733cc",
"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,
"fed2e70c5bd8a04481fa67fbd3c8fb35"
],
[
"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_51cea0492a6da9c7ec4c55241bfa63b8",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"966386d40a4371ea1828958c8f6fce5a"
],
[
"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", "int_typing",
"l_quant_interp_51cea0492a6da9c7ec4c55241bfa63b8",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ed56f0a463ff0657a36c83fe878c0439"
],
0,
"d55618be5a5ea9675925cfa6118ea003"
],
[
"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,
"8f9c9ff37d25cac95126616ae792a11f"
],
[
"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,
"b9687732ea9dbbfa48956d1027844fdb"
],
[
"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_51cea0492a6da9c7ec4c55241bfa63b8",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c462162ea5e531ec044610a7443db5ca",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc"
],
0,
"cdeec051fd73b6e046736cd35e4ae8b2"
],
[
"Vale.X64.Memory.modifies_same_heaplet_id",
1,
1,
1,
[
"@query", "equation_Vale.X64.Memory.get_heaplet_id",
"equation_Vale.X64.Memory.modifies"
],
0,
"42feb7e79c5ccc27699654fcdc7a28e4"
],
[
"Vale.X64.Memory.init_heaplets_req",
1,
1,
1,
[ "@query" ],
0,
"3fcd22a5d727dbf3af2cf0798f33895b"
],
[
"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,
"da6d713691dc06d7d16d276580bb0570"
],
[
"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,
"4b37ccd321d54b5b28d30a03576d40ee"
],
[
"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_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"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_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_61ad87a48c5493622a87dee22c6da699",
"refinement_interpretation_Tm_refine_c2c488db3214c38826155caf10d30036",
"refinement_interpretation_Tm_refine_d6f8c42395292e0388746550e3316a09",
"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_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,
"ed60e7abfeafb3465955ee4553100f21"
],
[
"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_6b4b417e1383ee3b4792f0b5428180ab",
"Vale.Interop.Base_interpretation_Tm_ghost_arrow_e03cc6f9f4f5021e4d77d66b8e3c5d97",
"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_FStar.UInt8.t",
"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_inversion", "int_typing",
"interpretation_Tm_abs_e14098f86a865715fec85e921cb76329",
"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_5065bafc42b9acd51fbc0726cf70a262",
"l_quant_interp_51cea0492a6da9c7ec4c55241bfa63b8",
"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_c2c488db3214c38826155caf10d30036",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_d6f8c42395292e0388746550e3316a09",
"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_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,
"a3214a136bdcba9cc77228d4aa781c2f"
],
[
"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_e5f0372e4b8607a08675a75fa5d733cc",
"typing_Vale.Interop.Types.view_n"
],
0,
"d0e8142362686363e31edbce41cf557a"
],
[
"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,
"8e1347b8dc2d049e9b08dcf2886f9262"
],
[
"Vale.X64.Memory.inv_heaplet",
1,
1,
1,
[ "@query" ],
0,
"610c46ef24b616a0d9656e96c804ffc3"
],
[
"Vale.X64.Memory.inv_heaplets",
1,
1,
1,
[ "@query" ],
0,
"de4ae314179cabc68ead8f08bedc20de"
],
[
"Vale.X64.Memory.heaps_match",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.HeapImpl.buffer",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc"
],
0,
"0ae373f38db8a83fd72552531d765326"
],
[
"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,
"69a4faa700567e6cb2d42302fe1ad1a8"
],
[
"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,
"d21d40006bb4cd19ec7e6d4cb1ab5214"
]
]
]
Computing file changes ...
