[ "§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, "cae333b9ce5cceb190ea2acac027e2ac" ], [ "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.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", "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.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, "64a397f68ae3991a8f02e2c5a915636e" ], [ "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.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", "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.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, "37813ac406325410b0076c167a1e0462" ], [ "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, "4f8b6020d32a3ffb663395998fa3f84b" ], [ "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", "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_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_LowStar.BufferView.Up.View_n" ], 0, "a119f6215459e4a873f68ea3623fea92" ], [ "Vale.X64.Memory.buffer_as_seq", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Vale.Arch.HeapImpl.buffer", "refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca" ], 0, "9008144e45df89e5ea1f3205f856c577" ], [ "Vale.X64.Memory.buffer_length", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Vale.Arch.HeapImpl.buffer", "refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca" ], 0, "fdaecd7db7f3a35aed9e994bddc7d45c" ], [ "Vale.X64.Memory.modifies", 1, 2, 1, [ "@query" ], 0, "4e8e17f71d2e425c55cdc0b8d87a5b47" ], [ "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, "4b732c3fd7c5616f6cbc62384e65d86a" ], [ "Vale.X64.Memory.index_helper", 1, 2, 1, [ "@query" ], 0, "8c5eecd674182766fd8b57aa9c212728" ], [ "Vale.X64.Memory.index_mul_helper", 1, 2, 1, [ "@query", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, "18dbe03aa08da9c13658f3bc41a19dac" ], [ "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, "0c6d13a57da9a0063d3349901a010206" ], [ "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, "f9d4ec53878273f7d404abc93c905af3" ], [ "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, "781f337bb806a400e02d909b34b9d75a" ], [ "Vale.X64.Memory.lemma_modifies_goal_directed", 1, 0, 0, [ "@query", "equation_Vale.X64.Memory.modifies_goal_directed" ], 0, "2133bf80557a022820cf81bfbdfd9f33" ], [ "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, "43b2a274f5a308179407e639ee164482" ], [ "Vale.X64.Memory.same_underlying_seq", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "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.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_Vale.Lib.BufferViewHelpers.lemma_uv_equal", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_Equality", "proj_equation_Vale.Interop.Heap_s.InteropHeap_hs", "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_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca", "refinement_interpretation_Tm_refine_f0ac14b89ed9937127ef9c7557190460", "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", "well-founded-ordering-on-nat" ], 0, "114596003f4d04d23d81aac956dfbc0d" ], [ "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, "ab89da397305d7d8ee8f580c7de5d6b7" ], [ "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, "705d5782934631e191e23249a6e946c6" ], [ "Vale.X64.Memory.modifies_buffer_readable", 1, 0, 0, [ "@query", "equation_Vale.X64.Memory.buffer_readable", "equation_Vale.X64.Memory.modifies" ], 0, "c4fe1d60269e3f8bcc61894a97310f42" ], [ "Vale.X64.Memory.loc_disjoint_none_r", 1, 0, 0, [ "@query", "equation_Vale.X64.Memory.loc_disjoint", "equation_Vale.X64.Memory.loc_none" ], 0, "834260cbfb0623114ff622dc8e017dfe" ], [ "Vale.X64.Memory.loc_disjoint_union_r", 1, 0, 0, [ "@query", "equation_Vale.X64.Memory.loc_disjoint", "equation_Vale.X64.Memory.loc_union" ], 0, "ec1cee711bb542bd0545ef379ff7e551" ], [ "Vale.X64.Memory.loc_includes_refl", 1, 0, 0, [ "@query", "equation_Vale.X64.Memory.loc_includes" ], 0, "5f26dc1b905126635670494e972b59ae" ], [ "Vale.X64.Memory.loc_includes_trans", 1, 0, 0, [ "@query", "equation_Vale.X64.Memory.loc_includes" ], 0, "9a0fa220aa1727bf4b4aa19fddfad541" ], [ "Vale.X64.Memory.loc_includes_union_r", 1, 0, 0, [ "@query", "equation_Vale.X64.Memory.loc_includes", "equation_Vale.X64.Memory.loc_union" ], 0, "da1bfd6a61c31c00f065b6bee5ddb297" ], [ "Vale.X64.Memory.loc_includes_union_l", 1, 0, 0, [ "@query", "equation_Vale.X64.Memory.loc_includes", "equation_Vale.X64.Memory.loc_union" ], 0, "ffe90b049cc00bf2c5d8b20e9320fc10" ], [ "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, "85d248d72cfeb0e4c8c51b5bbec37a09" ], [ "Vale.X64.Memory.loc_includes_none", 1, 0, 0, [ "@query", "equation_Vale.X64.Memory.loc_includes", "equation_Vale.X64.Memory.loc_none" ], 0, "4b04accca5907ca0a2d17145e60eb1d0" ], [ "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, "bad30a5566919cc942d32838747ddaa6" ], [ "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, "df535ab3417fc2b643adff2d72d09cce" ], [ "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, "8d2626db199e4f53c89b140a64401a08" ], [ "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, "5060cedc9f57d210b6692447e5fb0c06" ], [ "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, "aaae9a1b07479a2d707fb18bccefc691" ], [ "Vale.X64.Memory.modifies_goal_directed_trans2", 1, 0, 0, [ "@query", "equation_Vale.X64.Memory.modifies_goal_directed" ], 0, "7a23c75bff0c6e826dd3be9e84af04d3" ], [ "Vale.X64.Memory.default_of_typ", 1, 0, 0, [ "@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", "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", "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_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_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "5aef742144675fd09df024670f3187fa" ], [ "Vale.X64.Memory.buffer_read", 1, 0, 0, [ "@query", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq" ], 0, "a223012df28c783deb349e89e0b7173a" ], [ "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, "795b02f006ca33336246de11aa44347d" ], [ "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, "c76cc5dac756efd169f3367e4977744c" ], [ "Vale.X64.Memory.buffer_write", 1, 0, 0, [ "@query", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq" ], 0, "c2587762b64221eaf91d5f02b4479f84" ], [ "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, "33c892ccd2714c40700399793ab907f5" ], [ "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, "297ffeabf8c2913400df809dae37f76b" ], [ "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, "f95636cdfc3569cfdf70ec3d890db025" ], [ "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, "27598b87b4c4c48d8c08186c17e8765b" ], [ "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.Nil", "data_elim_Prims.Cons", "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_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list", "equation_Vale.X64.Memory.valid_buffer", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "false_interp", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap", "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "kinding_Vale.Interop.Types.b8@tok", "l_or-interp", "lemma_FStar.Map.lemma_ContainsDom", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699", "refinement_interpretation_Tm_refine_ad5f9e9e07a5ab25763e7f2290e5f84c", "refinement_interpretation_Tm_refine_c8f24b12ae1a99947f0a92d23a8cce9f", "refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca", "subterm_ordering_Prims.Cons", "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.X64.Memory.valid_buffer", "typing_Vale.X64.Memory.valid_mem_aux" ], 0, "28a6d12eddf53839b7932c7245dca97f" ], [ "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, "f161a6973bbc26ecdb562d16c07ddfa8" ], [ "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, "bd72d17c0aa8d20f357641f8014fbcae" ], [ "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.Nil", "data_elim_FStar.Pervasives.Native.Some", "data_elim_Prims.Cons", "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", "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.op_Equals_Equals_Equals", "equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list", "equation_Vale.X64.Memory.valid_buffer", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "equation_with_fuel_Vale.X64.Memory.valid_mem_aux.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "kinding_Vale.Interop.Types.b8@tok", "l_or-interp", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.None_a", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_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.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Vale.Arch.HeapImpl._ih", "typing_Vale.Arch.HeapImpl.buffer", "typing_Vale.X64.Memory.valid_mem_aux" ], 0, "ea7392fa16cb590c0a80af44f4f787f9" ], [ "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, "f5e3b641fa081fabe5edeb0629c9f99d" ], [ "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, "e0c363d041ca0811cf7d6b3681d65776" ], [ "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.op_Equals_Equals_Equals", "equation_Prims.squash", "equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.buffer_addr", "equation_Vale.X64.Memory.scale_by", "equation_Vale.X64.Memory.sub_list", "equation_Vale.X64.Memory.valid_buffer", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "equation_with_fuel_Vale.X64.Memory.find_valid_buffer_aux.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap", "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs", "int_inversion", "int_typing", "kinding_Vale.Interop.Types.b8@tok", "l_and-interp", "l_or-interp", "lemma_FStar.Map.lemma_ContainsDom", "primitive_Prims.op_AmpAmp", "proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs", "proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699", "refinement_interpretation_Tm_refine_92021f726392e5bad2e8fce80b5e9a8b", "refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448", "refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.X64.Memory.find_valid_buffer_aux.fuel_instrumented", "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" ], 0, "45bf251fd32ccbee51d94c0178578a17" ], [ "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, "656231317ab159099a81b62168b0b69b" ], [ "Vale.X64.Memory.find_valid_buffer_valid_offset", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Interop.Heap_s_interpretation_Tm_arrow_49af84408b2fd68795c64e188f731e93", "Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3", "bool_inversion", "data_elim_FStar.Pervasives.Native.Some", "data_elim_Vale.Arch.HeapImpl.ValeHeap", "data_elim_Vale.Interop.Heap_s.InteropHeap", "disc_equation_FStar.Pervasives.Native.None", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt16@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt32@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.nat", "equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Types.addr_map", "equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.buffer_addr", "equation_Vale.X64.Memory.find_valid_buffer", "equation_Vale.X64.Memory.sub_list", "equation_Vale.X64.Memory.valid_buffer", "equation_Vale.X64.Memory.valid_offset", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap", "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs", "int_inversion", "kinding_Vale.Interop.Heap_s.interop_heap@tok", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "proj_equation_Vale.Arch.HeapImpl.ValeHeap_ih", "proj_equation_Vale.Interop.Heap_s.InteropHeap_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_b0e983e2a97bd15fdd0ab53f8b017a6f", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_e71863c9702f0243be00371e81c075e8", "refinement_interpretation_Tm_refine_efd4ef517629f7c86a95b395d9e0faca", "refinement_interpretation_Tm_refine_fb46804529de36a0e6813ea1066a078a", "token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs", "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_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, "ebdade7a3c43b1e47a54b8fe4836dbc3" ], [ "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.Nil", "data_elim_Prims.Cons", "data_elim_Vale.Interop.Heap_s.InteropHeap", "data_elim_Vale.Interop.Types.Buffer", "data_typing_intro_Vale.Arch.HeapTypes_s.TUInt16@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt16@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt32@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.Interop.Types.view_n", "equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.buffer_writeable", "equation_Vale.X64.Memory.sub_list", "equation_Vale.X64.Memory.valid_buffer", "equation_Vale.X64.Memory.writeable_buffer", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "false_interp", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap", "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "kinding_Vale.Interop.Types.b8@tok", "l_or-interp", "lemma_FStar.Map.lemma_ContainsDom", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs", "proj_equation_Vale.Interop.Types.Buffer_writeable", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_257f34044a0ca6d5caaa8860ef678921", "refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699", "refinement_interpretation_Tm_refine_dec7b1927c1b898a76bc71660ded97c6", "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.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Vale.Arch.HeapImpl._ih", "typing_Vale.Interop.Types.__proj__Buffer__item__writeable", "typing_Vale.X64.Memory.addr_in_ptr", "typing_Vale.X64.Memory.valid_buffer", "typing_Vale.X64.Memory.writeable_buffer", "typing_Vale.X64.Memory.writeable_mem_aux", "typing_tok_Vale.Arch.HeapTypes_s.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, "1c82bfc88e8071a181a45e3bd5934a49" ], [ "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, "4220b8a5eac714c34c8a59119a306fba" ], [ "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, "fe7f5e3188622f86954b81efa19eaedf" ], [ "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.Nil", "data_elim_FStar.Pervasives.Native.Some", "data_elim_Prims.Cons", "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", "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.op_Equals_Equals_Equals", "equation_Vale.Arch.HeapImpl._ih", "equation_Vale.Arch.HeapImpl.buffer", "equation_Vale.X64.Memory.b8", "equation_Vale.X64.Memory.sub_list", "equation_Vale.X64.Memory.valid_buffer", "equation_Vale.X64.Memory.writeable_buffer", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "equation_with_fuel_Vale.X64.Memory.writeable_mem_aux.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "kinding_Vale.Interop.Types.b8@tok", "l_or-interp", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.None_a", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_257f34044a0ca6d5caaa8860ef678921", "refinement_interpretation_Tm_refine_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.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Vale.Arch.HeapImpl._ih", "typing_Vale.Arch.HeapImpl.buffer", "typing_Vale.X64.Memory.writeable_mem_aux" ], 0, "66357319de46788a4b2dd3278d5e58a1" ], [ "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, "2845a0e42d97dfd2a284182b769a0c51" ], [ "Vale.X64.Memory.load_mem", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3", "data_elim_Vale.Interop.Heap_s.InteropHeap", "disc_equation_FStar.Pervasives.Native.None", "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.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", "lemma_FStar.Pervasives.invertOption", "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_774ba3f728d91ead8ef40be66c9802e5", "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.Arch.HeapImpl.buffer", "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" ], 0, "88df604516dca1c0b471834cb684ab28" ], [ "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, "67772f4ff7d4c18abdf7b5c30e90214a" ], [ "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, "2a76ff95fe7790be436fa232877b6e13" ], [ "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, "699a59903d248c0a72bea9718c7d1c73" ], [ "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.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Tm_unit", "disc_equation_FStar.Pervasives.Native.None", "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.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.valid_buffer", "equation_Vale.X64.Memory.valid_offset", "equation_Vale.X64.Memory.writeable_buffer", "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.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_0dbdff46d67e5b175b2f3cc0cb46b974", "refinement_interpretation_Tm_refine_4222c0a0845174bddfc525ea3f317b0e", "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_fb46804529de36a0e6813ea1066a078a", "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.Interop.Types.view_n", "typing_Vale.X64.Memory.addr_in_ptr", "typing_Vale.X64.Memory.find_writeable_buffer_aux" ], 0, "b63d0769d0981ac0ee2ef243761b9946" ], [ "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, "b0a94e33bdc4b537f727d77a4e60b9df" ], [ "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, "72f48413f7f269e2a231ed00ea5cc01a" ], [ "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, "7d2209f88a56c6925747d799c7d7e93d" ], [ "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, "ab45599c01570e396a311b833125053a" ], [ "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, "ee224224548f1e0d53bc7389ae393606" ], [ "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, "a4b16b15712631b4e7e5d297e5bcdb91" ], [ "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, "db52aa3d7f5c6ae67482cce4215e1b89" ], [ "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, "97f4d6cb5c2f583b943caa2f4a9b2354" ], [ "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, "cfcdbe1df4b2879476f0d7bd8649e9e6" ], [ "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, "b6a99377cd1d34e05e2f30573a2cc717" ], [ "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, "758883b46de618171a5f77d9826b7774" ], [ "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, "023d0c10f8d9841b8ad86a27324f47d0" ], [ "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, "336c6a3570ccdf1b563c4b2d5804d4f4" ], [ "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, "55be5c9eff03fedd0d031a2d85c2d103" ], [ "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, "1ad4a639ee3b31942b46f3eb070b3078" ], [ "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, "5dcb719c630a53faaa321d1d359d0d62" ], [ "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, "1a7e4e98c48eb77ca7a51656da80a211" ], [ "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, "1c91fbb0a561475c0df8c3c3c74bd4db" ], [ "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, "8c98d2c4b59b7d7318e05f43a076d78d" ], [ "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, "c37027627e524b17a113587437a7eef6" ], [ "Vale.X64.Memory.modifies_same_heaplet_id", 1, 1, 1, [ "@query", "equation_Vale.X64.Memory.get_heaplet_id", "equation_Vale.X64.Memory.modifies" ], 0, "d92be1eb16c6a3abeb377efe73932397" ], [ "Vale.X64.Memory.init_heaplets_req", 1, 1, 1, [ "@query" ], 0, "8ca97897af86b7748f23e6e5e8111635" ], [ "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, "5d81e60311b9d045f151759978d23048" ], [ "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, "1c9a0a912b0a1042cb0bd4b8dbfadecc" ], [ "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, "58eed7d72fa1d539f8c621a8b15eebee" ], [ "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_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", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_elim_Vale.Interop.Heap_s.InteropHeap", "data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "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.Interop.Types.down_view", "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_LowStar.BufferView.Down.view", "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_inversion", "int_typing", "interpretation_Tm_abs_0b45d135b1bf428b90ecd044d0c4f361", "kinding_Vale.Arch.HeapTypes_s.taint@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.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_kinding_Tm_refine_c2c488db3214c38826155caf10d30036", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.Interop.Heap_s.list_disjoint_or_eq_def", "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.down_view", "typing_Vale.Interop.Types.get_downview", "typing_tok_Vale.Arch.HeapTypes_s.Public@tok" ], 0, "42d1e089825975baf9df9c8c1032d089" ], [ "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, "80cb766ea6a302a9ca7906eacaf02cd8" ], [ "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, "58e075e1294fb71e2c6e652a07fbdbbb" ], [ "Vale.X64.Memory.inv_heaplet", 1, 1, 1, [ "@query" ], 0, "943e642ddef3a3e6ed6345b8d80d2e1a" ], [ "Vale.X64.Memory.inv_heaplets", 1, 1, 1, [ "@query" ], 0, "d62326d6e14a3e383b8154ff771248bf" ], [ "Vale.X64.Memory.heaps_match", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "equation_Vale.Arch.HeapImpl.buffer", "refinement_interpretation_Tm_refine_e5f0372e4b8607a08675a75fa5d733cc" ], 0, "6a4320ba787baaf2759ab4528f6c4c33" ], [ "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, "24d53627d11ee570cc35ad370282bf58" ], [ "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, "380c0d7a3e2dc5a7499ae63c6cd95781" ] ] ]