Revision 059787e63538941130606248805cab290fdbc5d7 authored by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC, committed by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC
1 parent 03f1e46
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,
"7d24859eaa3e6e8ae119a9cb39b7fb95"
],
[
"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,
"d83f88956ffd9680411f8670bee7d172"
],
[
"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,
"289487829bf4ee3545582f0ae2d0c8c9"
],
[
"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,
"934a6b7caf7a2609ac4ce762491d27c2"
],
[
"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,
"3b5baf22950dae52bc9b2907cf580a94"
],
[
"Vale.X64.Memory.buffer_as_seq",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.HeapImpl.buffer",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca"
],
0,
"590c1733f2990591a2504c596995f0d7"
],
[
"Vale.X64.Memory.buffer_length",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.HeapImpl.buffer",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca"
],
0,
"5a9d61c95afb047ffb3c30329805e742"
],
[
"Vale.X64.Memory.modifies",
1,
2,
1,
[ "@query" ],
0,
"ef6cda38d99bc9fff22513bd11ef18ac"
],
[
"Vale.X64.Memory.index64_heap_aux",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"FStar.UInt8_pretyping_512f0e4172b97206a8b0e16196475713",
"Vale.Def.Words.Four_s_interpretation_Tm_arrow_8e8890e19356591ca1f9e83b434ba1ba",
"Vale.X64.Memory_interpretation_Tm_arrow_efe96bb9514bece12be080c2a3348ae5",
"Vale.X64.Memory_interpretation_Tm_arrow_f4c4992cf843ea442af1288d1d5d4d22",
"b2t_def", "bool_inversion", "bool_typing",
"data_typing_intro_Vale.Def.Words_s.Mktwo@tok",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"equation_Vale.Def.Types_s.le_bytes_to_nat64_def",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words.Seq_s.seq_to_two_LE",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Views.get64_def",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_FStar.UInt8.v",
"function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val64",
"function_token_typing_Vale.Def.Types_s.le_bytes_to_nat64",
"function_token_typing_Vale.Def.Words.Four_s.four_to_nat",
"function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.Interop.Views.get64", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"interpretation_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
"interpretation_Tm_abs_ad3ad425f83578beeb8ba014cbc730a3",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt64.vu_inv",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_35a56cb7608bf4720ad612ec0cf582b4",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_528966909e656beff90629dc95073b2d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_553972523c0ad0511a59f7cdbdcafe94",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a97bb01c04ffe0871485a0f7264ef673",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_FStar.UInt8.v",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val64_def",
"token_correspondence_Vale.Def.Types_s.le_bytes_to_nat64_def",
"token_correspondence_Vale.Def.Words.Four_s.four_to_nat",
"token_correspondence_Vale.Interop.Views.get64_def",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_FStar.UInt64.v", "typing_FStar.UInt8.t", "typing_Prims.pow2",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
"typing_Tm_abs_ad3ad425f83578beeb8ba014cbc730a3",
"typing_Vale.Def.Types_s.le_bytes_to_nat64",
"typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"typing_Vale.Def.Words.Two_s.two_to_nat",
"typing_Vale.Def.Words_s.natN", "typing_Vale.Interop.Views.get64"
],
0,
"f35f2cfb13fc5f44db1040e3818c8c38"
],
[
"Vale.X64.Memory.index_helper",
1,
2,
1,
[ "@query" ],
0,
"7827145ad25d2025e98e9984021cb166"
],
[
"Vale.X64.Memory.index_mul_helper",
1,
2,
1,
[
"@query", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0"
],
0,
"5c7e8e305a33e1ef26f7b623a83b241f"
],
[
"Vale.X64.Memory.index64_get_heap_val64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Heap_s.correct_down",
"equation_Vale.Interop.Heap_s.correct_down_p",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.Interop.Views.up_view64",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.uint64_view",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.v_to_typ",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"proj_equation_LowStar.BufferView.Up.View_get",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Types.Buffer_src",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_LowStar.BufferView.Up.View_get",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_35a56cb7608bf4720ad612ec0cf582b4",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_9539918077828aa633026534394b5105",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b4c3192994dcc590bdf90a64a565ac51",
"refinement_interpretation_Tm_refine_bac48341d72c9512b36c265d7915272a",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_ed56f0a463ff0657a36c83fe878c0439",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f0b69480f5e055250ddc6c0968678616",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"token_correspondence_LowStar.BufferView.Up.__proj__View__item__get",
"token_correspondence_Vale.Interop.Views.get64",
"token_correspondence_Vale.X64.Memory.v_to_typ",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt8.t",
"typing_LowStar.BufferView.Up.as_seq",
"typing_LowStar.BufferView.Up.mk_buffer",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"9152e05a0f25b8e1b189790d6d6863e2"
],
[
"Vale.X64.Memory.index128_get_heap_val128_aux",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"FStar.UInt8_pretyping_512f0e4172b97206a8b0e16196475713",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.X64.Memory_interpretation_Tm_arrow_efe96bb9514bece12be080c2a3348ae5",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat",
"equation_Vale.Arch.MachineHeap_s.get_heap_val32_def",
"equation_Vale.Def.Types_s.le_bytes_to_quad32_def",
"equation_Vale.Def.Words.Seq_s.seq_to_four_LE",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Interop.Views.get128_def",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_FStar.UInt8.v",
"function_token_typing_Vale.Arch.MachineHeap_s.get_heap_val32",
"function_token_typing_Vale.Def.Types_s.le_bytes_to_quad32",
"function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.Interop.Views.get128", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"interpretation_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
"interpretation_Tm_abs_ad3ad425f83578beeb8ba014cbc730a3",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_528966909e656beff90629dc95073b2d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_Vale.Arch.MachineHeap_s.get_heap_val32_def",
"token_correspondence_Vale.Def.Types_s.le_bytes_to_quad32_def",
"token_correspondence_Vale.Def.Words.Four_s.four_to_nat",
"token_correspondence_Vale.Interop.Views.get128_def",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_FStar.UInt8.t",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8"
],
0,
"c166073b743ed37909f27a36e38bbce1"
],
[
"Vale.X64.Memory.index128_get_heap_val128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Heap_s.correct_down",
"equation_Vale.Interop.Heap_s.correct_down_p",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.Interop.Views.up_view128",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.uint128_view",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.v_to_typ",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.Seq.Base.index", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"proj_equation_LowStar.BufferView.Up.View_get",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Types.Buffer_src",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_LowStar.BufferView.Up.View_get",
"refinement_interpretation_Tm_refine_00753086f0a5091e4281a2f51c385e86",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_37e4cb0cef5519eccc60c9f31370a875",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_9b11903c06962c65f1bc43f9bd25a2d5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b4c3192994dcc590bdf90a64a565ac51",
"refinement_interpretation_Tm_refine_bac48341d72c9512b36c265d7915272a",
"refinement_interpretation_Tm_refine_c1351167a99542736ca91bc659666fba",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"token_correspondence_LowStar.BufferView.Up.__proj__View__item__get",
"token_correspondence_Vale.Interop.Views.get128",
"token_correspondence_Vale.X64.Memory.v_to_typ",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
"typing_LowStar.BufferView.Up.as_seq",
"typing_LowStar.BufferView.Up.mk_buffer",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"7c80a7654e8c83e4a178c499f311b156"
],
[
"Vale.X64.Memory.lemma_modifies_goal_directed",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.modifies_goal_directed" ],
0,
"62dd668d2b525a1bd9cb19619fce9edb"
],
[
"Vale.X64.Memory.buffer_length_buffer_as_seq",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.uint_view",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"lemma_FStar.Seq.Base.lemma_init_len", "primitive_Prims.op_Modulus",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Types.Buffer_src",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"typing_FStar.UInt8.t", "typing_LowStar.BufferView.Up.as_seq",
"typing_LowStar.BufferView.Up.mk_buffer",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view"
],
0,
"96fe15cad6fb79ae66ffbdcc0d389231"
],
[
"Vale.X64.Memory.same_underlying_seq",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.uint_view",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_Vale.Lib.BufferViewHelpers.lemma_uv_equal",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Types.Buffer_src",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_8ae5e7ec51c01b06a6c5c069c9bd60bc",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b10d136d804d19dcb00be7bd6d8c57c4",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.as_seq",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view", "typing_tok_Prims.LexTop@tok",
"well-founded-ordering-on-nat"
],
0,
"5c49233935e7a58515d76e608f40f6f2"
],
[
"Vale.X64.Memory.modifies_buffer_elim",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.b8_preorder",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.loc",
"equation_Vale.X64.Memory.loc_buffer",
"equation_Vale.X64.Memory.loc_disjoint",
"equation_Vale.X64.Memory.modifies",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"proj_equation_Vale.Interop.Types.Buffer_src",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.as_seq",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_as_seq"
],
0,
"6b2d36925e05554e0a9e1679d71814ce"
],
[
"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,
"1431d1e29e1d251da221e9cc31e01665"
],
[
"Vale.X64.Memory.modifies_buffer_readable",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.modifies"
],
0,
"1b7860d742ee412d56e3cc3abf9e69b7"
],
[
"Vale.X64.Memory.loc_disjoint_none_r",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_disjoint",
"equation_Vale.X64.Memory.loc_none"
],
0,
"881d854e05a22029710026a2c6fa2942"
],
[
"Vale.X64.Memory.loc_disjoint_union_r",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_disjoint",
"equation_Vale.X64.Memory.loc_union"
],
0,
"a17ef9b1e2e36ef3ea111a7b29dc391d"
],
[
"Vale.X64.Memory.loc_includes_refl",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.loc_includes" ],
0,
"b47bfc8fbd87fd9c7e3125f0fc87121b"
],
[
"Vale.X64.Memory.loc_includes_trans",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.loc_includes" ],
0,
"19df67d50c5556ff0c3b60d4ddbe197f"
],
[
"Vale.X64.Memory.loc_includes_union_r",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.loc_union"
],
0,
"d802b0659c8ebd42dbcaddeebc03261a"
],
[
"Vale.X64.Memory.loc_includes_union_l",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.loc_union"
],
0,
"3e557e1929668fc555433f3a193f9238"
],
[
"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,
"23db136c142f66584d1f20a63a858b0d"
],
[
"Vale.X64.Memory.loc_includes_none",
1,
0,
0,
[
"@query", "equation_Vale.X64.Memory.loc_includes",
"equation_Vale.X64.Memory.loc_none"
],
0,
"d02dc89a72b95bd0cf29ab6667aa8648"
],
[
"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,
"c34827fc9c2224c8364553c653f9d76a"
],
[
"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,
"ef7395d72c8f033db3696408a60ff216"
],
[
"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,
"dc995f4c6d0e905c27c86bc0a2121b8e"
],
[
"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,
"f21dc600538c435029e8c159f930883a"
],
[
"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,
"bb0a08b97c116bfda963b476166e3418"
],
[
"Vale.X64.Memory.modifies_goal_directed_trans2",
1,
0,
0,
[ "@query", "equation_Vale.X64.Memory.modifies_goal_directed" ],
0,
"68b58e8e0cb561f73cc5bd6c8be86895"
],
[
"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,
"9a882e58278766fd543181279551d701"
],
[
"Vale.X64.Memory.buffer_read",
1,
0,
0,
[ "@query", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq" ],
0,
"edc1cbee7e5373eb29124d779f6bae92"
],
[
"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,
"ae2490e0e73c40842e5257465c014a2e"
],
[
"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,
"335a640d112d6e409d6a7aa313ece205"
],
[
"Vale.X64.Memory.buffer_write",
1,
0,
0,
[ "@query", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq" ],
0,
"d60def3f47170ffb95f751b30c37da8e"
],
[
"Vale.X64.Memory.buffer_write",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Interop.Heap_s_pretyping_40dec2fdc42f7b5efafe5762d6761d53",
"b2t_def", "bool_inversion", "equation_FStar.Seq.Properties.lseq",
"equation_LowStar.BufferView.Down.buffer", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.b8_preorder",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer_as_seq",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.get_heaplet_id",
"equation_Vale.X64.Memory.loc_buffer",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.v_of_typ",
"fuel_guarded_inversion_FStar.Pervasives.dtuple4",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Seq.Base.index", "int_inversion",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"kinding_Vale.Interop.Heap_s.interop_heap@tok",
"lemma_FStar.Ghost.reveal_hide", "lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_upd",
"lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.Memory.lemma_v_to_of_typ",
"primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
"proj_equation_FStar.Pervasives.Mkdtuple4__1",
"proj_equation_FStar.Pervasives.Mkdtuple4__2",
"proj_equation_FStar.Pervasives.Mkdtuple4__3",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_heapletId",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_ih",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"proj_equation_Vale.Interop.Types.Buffer_src",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Arch.HeapImpl.ValeHeap_heapletId",
"projection_inverse_Vale.Arch.HeapImpl.ValeHeap_ih",
"projection_inverse_Vale.Interop.Heap_s.InteropHeap_addrs",
"projection_inverse_Vale.Interop.Heap_s.InteropHeap_hs",
"projection_inverse_Vale.Interop.Heap_s.InteropHeap_ptrs",
"refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_Vale.X64.Memory.v_to_typ",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.upd",
"typing_FStar.UInt8.t", "typing_LowStar.BufferView.Up.as_seq",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.uint_view", "typing_Vale.X64.Memory.v_of_typ"
],
0,
"f40831d4d36efffef680bb020d55283b"
],
[
"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,
"a41ac00030762302fc47687ed9cb9f97"
],
[
"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,
"352b06beebdb73dd7bbc3d6d1e28ea51"
],
[
"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,
"f502c3b103a18797a7dfa9041467aac7"
],
[
"Vale.X64.Memory.valid_mem_aux",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_8f6e895a49590f9a95c242bbf7466dd9_3",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_2",
"binder_x_ae567c2fb75be05905677af440075565_1", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt16@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt32@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"false_interp", "fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"kinding_Vale.Interop.Types.b8@tok", "l_or-interp",
"lemma_FStar.Map.lemma_ContainsDom", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_541f1e3ffa4cb0ce48061607f4ffdae6",
"refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"subterm_ordering_Prims.Cons", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.X64.Memory.valid_buffer",
"typing_Vale.X64.Memory.valid_mem_aux"
],
0,
"ada2456a870fb8334e5e95ee260a52d1"
],
[
"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,
"8ad3b37f33cb74b743799b5b3af9d883"
],
[
"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,
"0bb89b7119f65f26593d4af206765a8c"
],
[
"Vale.X64.Memory.find_valid_buffer_aux",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.valid_mem_aux.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Memory.valid_mem_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_8f6e895a49590f9a95c242bbf7466dd9_3",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_2",
"binder_x_ae567c2fb75be05905677af440075565_1", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"equation_with_fuel_Vale.X64.Memory.valid_mem_aux.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"kinding_Vale.Interop.Types.b8@tok", "l_or-interp",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fe1f3df3f116883725cc7f3aa34f4080",
"subterm_ordering_Prims.Cons", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Arch.HeapImpl._ih", "typing_Vale.Arch.HeapImpl.buffer",
"typing_Vale.X64.Memory.valid_mem_aux"
],
0,
"853690dcddd4cc09af07e88d8217320f"
],
[
"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,
"1e6a44acbd8baf6c340569799006c343"
],
[
"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,
"4ed677dfd05f80f2db156d3d81a610dc"
],
[
"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.squash",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer_addr",
"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_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.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.find_valid_buffer_aux"
],
0,
"d9e26c0f4a5e5705749f639eb5c673b3"
],
[
"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,
"ceaef1c849e9fe5d0e0bc37f911daa60"
],
[
"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", "int_typing",
"kinding_Vale.Interop.Heap_s.interop_heap@tok",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_ih",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699",
"refinement_interpretation_Tm_refine_92021f726392e5bad2e8fce80b5e9a8b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_e71863c9702f0243be00371e81c075e8",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_FStar.Ghost.reveal", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Arch.HeapImpl._ih", "typing_Vale.Arch.HeapImpl.buffer",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.find_valid_buffer",
"typing_Vale.X64.Memory.find_valid_buffer_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt16@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt32@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"7f7bb109a4e2f428fedf1f1f4339d10b"
],
[
"Vale.X64.Memory.writeable_mem_aux",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"b2t_def", "binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_8f6e895a49590f9a95c242bbf7466dd9_3",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_2",
"binder_x_ae567c2fb75be05905677af440075565_1", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_elim_Vale.Interop.Types.Buffer",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt16@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt32@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.writeable_buffer",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"false_interp", "fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"kinding_Vale.Interop.Types.b8@tok", "l_or-interp",
"lemma_FStar.Map.lemma_ContainsDom", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_0309fb9650d237a486c5dceda5246c92",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_257f34044a0ca6d5caaa8860ef678921",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"subterm_ordering_Prims.Cons", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.valid_buffer",
"typing_Vale.X64.Memory.writeable_buffer",
"typing_Vale.X64.Memory.writeable_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"3073b1f0fd2ea31542d0d631953325fc"
],
[
"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,
"e64607414ac576d29c40838222ed7afe"
],
[
"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,
"fe7791fb2144c3bdbe309bc8d1aba01d"
],
[
"Vale.X64.Memory.find_writeable_buffer_aux",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.writeable_mem_aux.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Memory.writeable_mem_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"binder_x_5d76a1fef4cd9dda5490f41345eda5bf_0",
"binder_x_8f6e895a49590f9a95c242bbf7466dd9_3",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_2",
"binder_x_ae567c2fb75be05905677af440075565_1", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.writeable_buffer",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"equation_with_fuel_Vale.X64.Memory.writeable_mem_aux.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"kinding_Vale.Interop.Types.b8@tok", "l_or-interp",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_257f34044a0ca6d5caaa8860ef678921",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fe1f3df3f116883725cc7f3aa34f4080",
"subterm_ordering_Prims.Cons", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Arch.HeapImpl._ih", "typing_Vale.Arch.HeapImpl.buffer",
"typing_Vale.X64.Memory.writeable_mem_aux"
],
0,
"76e41b360f8ae89ede0b19e629a9adde"
],
[
"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,
"97806fa779fb802ee2ff7f49c8331ab6"
],
[
"Vale.X64.Memory.load_mem",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"constructor_distinct_FStar.Pervasives.Native.Some",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.find_valid_buffer",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "primitive_Prims.op_AmpAmp",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_92021f726392e5bad2e8fce80b5e9a8b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.find_valid_buffer_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"f8597b935e785690b7a0b3f6aab593be"
],
[
"Vale.X64.Memory.length_t_eq",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.view_n",
"equation_Vale.X64.Memory.buffer_length",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_Vale.Interop.Types.b8", "int_inversion",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"primitive_Prims.op_Modulus",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Types.Buffer_src",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6042c299b005b6766d280ae906dedfbc",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.length",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.uint_view"
],
0,
"f385f12d2b5581ba5615a0b6611d7526"
],
[
"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,
"fa2a1c62a0bbadf5b3fd64a982e09ab5"
],
[
"Vale.X64.Memory.load_buffer_read",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"b2t_def", "constructor_distinct_Tm_unit", "equation_Prims.nat",
"equation_Prims.pos", "equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.find_valid_buffer",
"equation_Vale.X64.Memory.get_addr_ptr",
"equation_Vale.X64.Memory.load_mem",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem",
"equation_Vale.X64.Memory.valid_offset",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Some_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_92021f726392e5bad2e8fce80b5e9a8b",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.find_valid_buffer_aux",
"typing_Vale.X64.Memory.uint_view"
],
0,
"d28b6dfb9e66c6758fa47356a2b61e16"
],
[
"Vale.X64.Memory.store_mem",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"b2t_def", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Tm_unit",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_write",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.find_writeable_buffer",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"equation_Vale.X64.Memory.writeable_buffer",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "lemma_FStar.Pervasives.invertOption",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_GreaterThanOrEqual",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_4222c0a0845174bddfc525ea3f317b0e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.Arch.HeapImpl._ih", "typing_Vale.Arch.HeapImpl.buffer",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.find_writeable_buffer_aux",
"typing_Vale.X64.Memory.uint_view",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"4623e6f27fbe5298778d87c748790327"
],
[
"Vale.X64.Memory.store_buffer_write",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"b2t_def", "bool_inversion", "constructor_distinct_Tm_unit",
"disc_equation_FStar.Pervasives.Native.Some", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.find_writeable_buffer",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.store_mem",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"equation_Vale.X64.Memory.writeable_buffer",
"equation_Vale.X64.Memory.writeable_mem",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_src",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_257f34044a0ca6d5caaa8860ef678921",
"refinement_interpretation_Tm_refine_4222c0a0845174bddfc525ea3f317b0e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_aa311741644f2a2768d777f8e523a38c",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.find_writeable_buffer_aux",
"typing_Vale.X64.Memory.uint_view",
"typing_Vale.X64.Memory.writeable_mem",
"typing_Vale.X64.Memory.writeable_mem_aux"
],
0,
"ae8e0209cbac23c95284bc84a4c404aa"
],
[
"Vale.X64.Memory.valid_mem128",
1,
0,
0,
[
"@query", "equation_Vale.Interop.Types.b8",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list"
],
0,
"75765a05a80554b77b90e03c99dd475b"
],
[
"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,
"89137eaab04986831f33dd1fc28ec78a"
],
[
"Vale.X64.Memory.lemma_valid_mem64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem",
"equation_Vale.X64.Memory.valid_mem64",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"21cc8313c37a421d0bd74c6d0183e91e"
],
[
"Vale.X64.Memory.lemma_writeable_mem64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.writeable_mem",
"equation_Vale.X64.Memory.writeable_mem64",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8", "int_inversion",
"int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_257f34044a0ca6d5caaa8860ef678921",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.writeable_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"f2fa982449fad87a4c963127df17c29f"
],
[
"Vale.X64.Memory.lemma_store_mem",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Memory.get_addr_in_ptr.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.writeable_mem_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Heap_s_interpretation_Tm_arrow_49af84408b2fd68795c64e188f731e93",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"b2t_def", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Tm_unit",
"disc_equation_FStar.Pervasives.Native.None",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Prims.squash", "equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Heap_s.disjoint_or_eq_b8",
"equation_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8_preorder",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.disjoint_addr",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_write",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.find_writeable_buffer",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.store_mem",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_offset",
"equation_Vale.X64.Memory.writeable_buffer",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"function_token_typing_Vale.Interop.Heap_s.list_disjoint_or_eq",
"function_token_typing_Vale.Interop.Types.addr_map_pred",
"int_inversion", "int_typing",
"interpretation_Tm_abs_0b45d135b1bf428b90ecd044d0c4f361",
"l_and-interp", "l_quant_interp_bd1f5246e6f57b3b0174bc6d256820c5",
"lemma_FStar.Pervasives.invertOption",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"proj_equation_Vale.Interop.Types.Buffer_src",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_257f34044a0ca6d5caaa8860ef678921",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4222c0a0845174bddfc525ea3f317b0e",
"refinement_interpretation_Tm_refine_45eda407d0825ef421aab011ebbcaeff",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"token_correspondence_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
"typing_LowStar.BufferView.Down.length",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Vale.Arch.HeapImpl._ih", "typing_Vale.Arch.HeapImpl.buffer",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.find_writeable_buffer_aux",
"typing_Vale.X64.Memory.get_addr_in_ptr",
"typing_Vale.X64.Memory.uint_view",
"typing_Vale.X64.Memory.writeable_mem_aux"
],
0,
"0d98beef2b6a7ae708b34d7c24fb7c03"
],
[
"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,
"8a8e2b3c969525d406b887697ddd06c0"
],
[
"Vale.X64.Memory.lemma_load_mem64",
2,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Memory.get_addr_in_ptr.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.valid_mem_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Heap_s.disjoint_or_eq_b8",
"equation_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8_preorder",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.disjoint_addr",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.buffer_read",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.default_of_typ",
"equation_Vale.X64.Memory.find_valid_buffer",
"equation_Vale.X64.Memory.load_mem",
"equation_Vale.X64.Memory.load_mem64",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem",
"equation_Vale.X64.Memory.valid_mem64",
"equation_Vale.X64.Memory.valid_offset",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Vale.Interop.Heap_s.list_disjoint_or_eq",
"function_token_typing_Vale.Interop.Types.addr_map_pred",
"function_token_typing_Vale.X64.Memory.buffer64", "int_inversion",
"int_typing",
"interpretation_Tm_abs_0b45d135b1bf428b90ecd044d0c4f361",
"l_and-interp", "l_quant_interp_bd1f5246e6f57b3b0174bc6d256820c5",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Pervasives.invertOption",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Negation",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_45eda407d0825ef421aab011ebbcaeff",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_92021f726392e5bad2e8fce80b5e9a8b",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"token_correspondence_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_FStar.UInt8.t", "typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.find_valid_buffer_aux",
"typing_Vale.X64.Memory.get_addr_in_ptr",
"typing_Vale.X64.Memory.uint_view",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"5324c548d6ea333ca1f8898cad4f3923"
],
[
"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,
"782c4e3fdb1b4c2b7cbdcbb6b16548b4"
],
[
"Vale.X64.Memory.lemma_store_mem64",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.store_mem64",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem",
"equation_Vale.X64.Memory.valid_mem64",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8", "int_inversion",
"int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_Negation",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.store_mem64",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"89f30c89d30259b52d80e3cac219bdf9"
],
[
"Vale.X64.Memory.lemma_valid_mem128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem128",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"0f8bed24df2542dfb088f20b0120af2f"
],
[
"Vale.X64.Memory.lemma_writeable_mem128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.writeable_mem128",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8", "int_inversion",
"int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_257f34044a0ca6d5caaa8860ef678921",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.writeable_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"cd083ed43d368c1ef05d78e2217cff14"
],
[
"Vale.X64.Memory.lemma_load_mem128",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Memory.get_addr_in_ptr.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Memory.valid_mem_aux.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Heap_s.disjoint_or_eq_b8",
"equation_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8_preorder",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.disjoint_addr",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.buffer_length",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.find_valid_buffer",
"equation_Vale.X64.Memory.load_mem",
"equation_Vale.X64.Memory.load_mem128",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.uint_view",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem128",
"equation_Vale.X64.Memory.valid_offset",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Vale.Interop.Heap_s.list_disjoint_or_eq",
"function_token_typing_Vale.Interop.Types.addr_map_pred",
"int_inversion", "int_typing",
"interpretation_Tm_abs_0b45d135b1bf428b90ecd044d0c4f361",
"l_and-interp", "l_quant_interp_bd1f5246e6f57b3b0174bc6d256820c5",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Negation",
"proj_equation_LowStar.BufferView.Up.View_n",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_45eda407d0825ef421aab011ebbcaeff",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_92021f726392e5bad2e8fce80b5e9a8b",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_f3af5f28517536d6dbf79ec5d669f74d",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"token_correspondence_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt8.t",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.Types.view_n",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.find_valid_buffer_aux",
"typing_Vale.X64.Memory.get_addr_in_ptr",
"typing_Vale.X64.Memory.uint_view",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"e382e1befe41dac9e76334f31f422f8d"
],
[
"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,
"19507e78533259aeae99662ea4bb562a"
],
[
"Vale.X64.Memory.lemma_store_mem128",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.buffer_readable",
"equation_Vale.X64.Memory.buffer_writeable",
"equation_Vale.X64.Memory.store_mem128",
"equation_Vale.X64.Memory.sub_list",
"equation_Vale.X64.Memory.valid_buffer",
"equation_Vale.X64.Memory.valid_mem128",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8", "int_inversion",
"int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_Negation",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a",
"typing_Vale.Arch.HeapImpl._ih",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.X64.Memory.addr_in_ptr",
"typing_Vale.X64.Memory.store_mem128",
"typing_Vale.X64.Memory.valid_mem_aux",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"3697a43f385c299539e219f79e2dacc0"
],
[
"Vale.X64.Memory.apply_taint_buf",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.X64.Memory.valid_taint_b8",
"equation_Vale.X64.Memory.valid_taint_buf",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"int_inversion", "int_typing",
"l_quant_interp_eec16fb10e3c0be0be37de5656d5d0d7",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"e1eb20af58c027bfa377a5562235b9c2"
],
[
"Vale.X64.Memory.lemma_valid_taint64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.nat", "equation_Vale.Interop.Types.view_n",
"equation_Vale.X64.Memory.buffer_addr",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.valid_taint_b8",
"equation_Vale.X64.Memory.valid_taint_buf",
"equation_Vale.X64.Memory.valid_taint_buf64",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"int_inversion", "l_quant_interp_eec16fb10e3c0be0be37de5656d5d0d7",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ed56f0a463ff0657a36c83fe878c0439"
],
0,
"ae322c80807b90d3f37a02725995ad7f"
],
[
"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,
"8b94db75e117f7d9779e3192dbeca55e"
],
[
"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,
"e7b10a786d7780d5662afc685ffc9517"
],
[
"Vale.X64.Memory.modifies_valid_taint",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.buffer",
"equation_Vale.X64.Memory.modifies",
"equation_Vale.X64.Memory.valid_taint_b8",
"equation_Vale.X64.Memory.valid_taint_buf",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_typing", "l_quant_interp_eec16fb10e3c0be0be37de5656d5d0d7",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9bdf64b2660adb592eaffa73ced680cc",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca"
],
0,
"58011a789776e078e8cc2d14136327bd"
],
[
"Vale.X64.Memory.modifies_same_heaplet_id",
1,
1,
1,
[
"@query", "equation_Vale.X64.Memory.get_heaplet_id",
"equation_Vale.X64.Memory.modifies"
],
0,
"79caaf84e82e08db4a8ea5c1d63d30a0"
],
[
"Vale.X64.Memory.init_heaplets_req",
1,
1,
1,
[ "@query" ],
0,
"576e922d2ae2d04ea4c72665e400d093"
],
[
"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,
"291c55f099abe747079fbdd33c6c426e"
],
[
"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,
"2995c879f57a95a33cb9636585195638"
],
[
"Vale.X64.Memory.write_taint_lemma",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Interop.Base.write_taint.fuel_instrumented",
"@fuel_irrelevance_Vale.Interop.Base.write_taint.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"Vale.Interop.Base_interpretation_Tm_ghost_arrow_6b4b417e1383ee3b4792f0b5428180ab",
"Vale.X64.Memory_interpretation_Tm_ghost_arrow_2d7469efb5ea1a486ea676065315b855",
"b2t_def", "binder_x_40dec2fdc42f7b5efafe5762d6761d53_1",
"binder_x_6d4cfc2a8480745fc461c4428588c8e0_3",
"binder_x_9cdee1dee4a021122574b44c25299169_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_e7fff4bad6aea127cbbd202a00eaae18_4", "bool_inversion",
"bool_typing", "data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_elim_Vale.Interop.Types.Buffer",
"data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.eqtype",
"equation_Prims.l_Forall", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.Arch.HeapTypes_s.memTaint_t",
"equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.memtaint",
"equation_with_fuel_Vale.Interop.Base.write_taint.fuel_instrumented",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.taint",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.int", "int_inversion", "int_typing",
"kinding_Vale.Arch.HeapTypes_s.taint@tok", "l_and-interp",
"l_quant_interp_1e77134a67a9a168a843bbc4a6ae3587",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5e8a4b3047c38f1ce9b8b1959bab0bd7",
"refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699",
"refinement_interpretation_Tm_refine_c2c488db3214c38826155caf10d30036",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Set.complement", "typing_FStar.Set.empty",
"typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.length",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.get_downview",
"typing_tok_Prims.LexTop@tok",
"typing_tok_Vale.Arch.HeapTypes_s.Public@tok",
"typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"well-founded-ordering-on-nat"
],
0,
"8e616116a02a43fbd82c1af223fe8e49"
],
[
"Vale.X64.Memory.valid_memtaint",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@query",
"FStar.List.Tot.Base_interpretation_Tm_ghost_arrow_d7e9834b8fd0407a723f5f3f4b012fdd",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_5d76a1fef4cd9dda5490f41345eda5bf",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"Vale.Interop.Base_interpretation_Tm_ghost_arrow_65ec90b9a641de16cd2204a5fec1203d",
"Vale.Interop.Base_interpretation_Tm_ghost_arrow_6b4b417e1383ee3b4792f0b5428180ab",
"Vale.X64.Memory_interpretation_Tm_ghost_arrow_2d7469efb5ea1a486ea676065315b855",
"binder_x_8f6e895a49590f9a95c242bbf7466dd9_0",
"binder_x_9cdee1dee4a021122574b44c25299169_2",
"binder_x_a4de1f5acaac4388ed7e0a95db0c96a9_1", "bool_inversion",
"bool_typing", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil",
"data_elim_Vale.Arch.HeapImpl.ValeHeap",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"data_elim_Vale.Interop.Types.Buffer",
"data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok",
"data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl._ih",
"equation_Vale.Arch.HeapTypes_s.memTaint_t",
"equation_Vale.Interop.Base.create_memtaint",
"equation_Vale.Interop.Heap_s.disjoint_or_eq_b8",
"equation_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8_preorder",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.disjoint_addr",
"equation_Vale.X64.Memory.b8",
"equation_Vale.X64.Memory.valid_taint_b8",
"equation_Vale.X64.Memory.valid_taint_bufs",
"equation_with_fuel_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"false_interp", "fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Interop.Base.write_taint",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"function_token_typing_Vale.Interop.Heap_s.list_disjoint_or_eq",
"function_token_typing_Vale.Interop.Types.addr_map_pred",
"int_typing",
"interpretation_Tm_abs_0b45d135b1bf428b90ecd044d0c4f361",
"kinding_Vale.Arch.HeapTypes_s.taint@tok",
"kinding_Vale.Interop.Heap_s.interop_heap@tok",
"kinding_Vale.Interop.Types.b8@tok", "l_and-interp", "l_or-interp",
"l_quant_interp_bd1f5246e6f57b3b0174bc6d256820c5",
"l_quant_interp_eec16fb10e3c0be0be37de5656d5d0d7",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomConstMap",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty",
"primitive_Prims.op_BarBar", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Negation",
"proj_equation_Vale.Arch.HeapImpl.ValeHeap_ih",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"proj_equation_Vale.Interop.Types.Buffer_src",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5e8a4b3047c38f1ce9b8b1959bab0bd7",
"refinement_interpretation_Tm_refine_c2c488db3214c38826155caf10d30036",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_e71863c9702f0243be00371e81c075e8",
"refinement_kinding_Tm_refine_c2c488db3214c38826155caf10d30036",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Interop.Base.write_taint",
"token_correspondence_Vale.Interop.Heap_s.list_disjoint_or_eq_def",
"typing_FStar.Ghost.reveal", "typing_FStar.Map.const",
"typing_FStar.Map.domain", "typing_FStar.Set.complement",
"typing_FStar.Set.empty", "typing_FStar.Set.mem",
"typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.length",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.get_downview",
"typing_tok_Vale.Arch.HeapTypes_s.Public@tok"
],
0,
"30a46805a765010c61ae9b74d90288d7"
],
[
"Vale.X64.Memory.valid_layout_data_buffer",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"equation_Vale.Arch.HeapImpl.buffer",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca",
"typing_Vale.Interop.Types.view_n"
],
0,
"8e25062d80953604643fb3429659716d"
],
[
"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,
"c564a94e84b5a27270c97c0949539ffb"
],
[
"Vale.X64.Memory.inv_heaplet",
1,
1,
1,
[ "@query" ],
0,
"f173891d225e8d75ed4845c29c8f2979"
],
[
"Vale.X64.Memory.inv_heaplets",
1,
1,
1,
[ "@query" ],
0,
"6608b6e8ffb36a030a60a515b16ae430"
],
[
"Vale.X64.Memory.heaps_match",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.HeapImpl.buffer",
"refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc"
],
0,
"c42293662722f48b14d47ad83c133434"
],
[
"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,
"058c4f4bef074757c76ec8f126674d3c"
],
[
"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,
"8dd0c9978105c958da3bfbe5998e91ce"
]
]
]
Computing file changes ...
