[ "¨Ÿã\u0002Z\u000bVºø\fyR„%zÀ", [ [ "Vale.Interop.write_vale_mem", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "5ab67afdbe956e885b753cdc26cbf927" ], [ "Vale.Interop.write_vale_mem", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "binder_x_74f682bc25113c64084a04765516a401_4", "binder_x_ae567c2fb75be05905677af440075565_2", "binder_x_b2564773453bdfb53f032dbd3679709e_3", "binder_x_cabf339c83086244c77449dbb6cc3cbc_1", "equality_tok_Prims.LexTop@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.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_14ac14fe5618e6aa6489208789111683", "refinement_interpretation_Tm_refine_1f9c035e3d5700980b3b63c565438b2f", "refinement_interpretation_Tm_refine_34ff444db0d6e38eb310a45b8a17c132", "refinement_interpretation_Tm_refine_4f3f4c0e7452015453e686b55c18c37e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "well-founded-ordering-on-nat" ], 0, "67e6a8c7e2e090670bd36eaf329bd61c" ], [ "Vale.Interop.frame_write_vale_mem", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "0a02b488f13c0420e9d75a5058e33873" ], [ "Vale.Interop.frame_write_vale_mem", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_correspondence_Vale.Interop.write_vale_mem.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Vale.Interop.write_vale_mem.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "binder_x_74f682bc25113c64084a04765516a401_4", "binder_x_ae567c2fb75be05905677af440075565_2", "binder_x_ae567c2fb75be05905677af440075565_5", "binder_x_b2564773453bdfb53f032dbd3679709e_3", "binder_x_b5ecdf6b68431b1ae5a51ce9723a824d_0", "binder_x_cabf339c83086244c77449dbb6cc3cbc_1", "equality_tok_Prims.LexTop@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.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_with_fuel_Vale.Interop.write_vale_mem.fuel_instrumented", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_14ac14fe5618e6aa6489208789111683", "refinement_interpretation_Tm_refine_1f9c035e3d5700980b3b63c565438b2f", "refinement_interpretation_Tm_refine_34ff444db0d6e38eb310a45b8a17c132", "refinement_interpretation_Tm_refine_4f3f4c0e7452015453e686b55c18c37e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d", "refinement_interpretation_Tm_refine_92bffd61ccbecc2ffeb38c51b31903f3", "refinement_interpretation_Tm_refine_a8d5bc6eafc44205d392093af1e7f064", "refinement_interpretation_Tm_refine_cb7955f07f21ce8668d576ee8dfdce26", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "well-founded-ordering-on-nat" ], 0, "c4c9b0e89f9a13406099319fc4754e65" ], [ "Vale.Interop.load_store_write_vale_mem", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_eae35c292e6ea58af33a2672308f11de" ], 0, "5343831afdde6c9eff25f6c7b1473a24" ], [ "Vale.Interop.load_store_write_vale_mem", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_correspondence_Vale.Interop.write_vale_mem.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Vale.Interop.write_vale_mem.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "binder_x_74f682bc25113c64084a04765516a401_4", "binder_x_ae567c2fb75be05905677af440075565_2", "binder_x_b2564773453bdfb53f032dbd3679709e_3", "binder_x_b5ecdf6b68431b1ae5a51ce9723a824d_0", "binder_x_cabf339c83086244c77449dbb6cc3cbc_1", "equality_tok_Prims.LexTop@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.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_with_fuel_Vale.Interop.write_vale_mem.fuel_instrumented", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_14ac14fe5618e6aa6489208789111683", "refinement_interpretation_Tm_refine_1f9c035e3d5700980b3b63c565438b2f", "refinement_interpretation_Tm_refine_34ff444db0d6e38eb310a45b8a17c132", "refinement_interpretation_Tm_refine_4f3f4c0e7452015453e686b55c18c37e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d", "refinement_interpretation_Tm_refine_92bffd61ccbecc2ffeb38c51b31903f3", "refinement_interpretation_Tm_refine_a8d5bc6eafc44205d392093af1e7f064", "refinement_interpretation_Tm_refine_cb7955f07f21ce8668d576ee8dfdce26", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "well-founded-ordering-on-nat" ], 0, "1a76c76e4d39c1d65206f6dda7c0cfd7" ], [ "Vale.Interop.domain_write_vale_mem", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "608eb56b99ffc5418acbe707e2aa8b3e" ], [ "Vale.Interop.domain_write_vale_mem", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_correspondence_Vale.Interop.write_vale_mem.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Vale.Interop.write_vale_mem.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "binder_x_74f682bc25113c64084a04765516a401_4", "binder_x_ae567c2fb75be05905677af440075565_2", "binder_x_b2564773453bdfb53f032dbd3679709e_3", "binder_x_b5ecdf6b68431b1ae5a51ce9723a824d_0", "binder_x_cabf339c83086244c77449dbb6cc3cbc_1", "bool_inversion", "equality_tok_Prims.LexTop@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.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_with_fuel_Vale.Interop.write_vale_mem.fuel_instrumented", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_14ac14fe5618e6aa6489208789111683", "refinement_interpretation_Tm_refine_1f9c035e3d5700980b3b63c565438b2f", "refinement_interpretation_Tm_refine_34ff444db0d6e38eb310a45b8a17c132", "refinement_interpretation_Tm_refine_4f3f4c0e7452015453e686b55c18c37e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d", "refinement_interpretation_Tm_refine_92bffd61ccbecc2ffeb38c51b31903f3", "refinement_interpretation_Tm_refine_a8d5bc6eafc44205d392093af1e7f064", "refinement_interpretation_Tm_refine_cb7955f07f21ce8668d576ee8dfdce26", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Map.domain", "typing_FStar.Set.mem", "typing_FStar.UInt.fits", "typing_Vale.Interop.write_vale_mem", "well-founded-ordering-on-nat" ], 0, "709df32fb0c17ebf61b7daaa9c2832bf" ], [ "Vale.Interop.domain2_write_vale_mem", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "96af51baf7851f164e13e316bb619e95" ], [ "Vale.Interop.domain2_write_vale_mem", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_correspondence_Vale.Interop.write_vale_mem.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Vale.Interop.write_vale_mem.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "binder_x_74f682bc25113c64084a04765516a401_4", "binder_x_ae567c2fb75be05905677af440075565_2", "binder_x_b2564773453bdfb53f032dbd3679709e_3", "binder_x_b5ecdf6b68431b1ae5a51ce9723a824d_0", "binder_x_cabf339c83086244c77449dbb6cc3cbc_1", "bool_inversion", "equality_tok_Prims.LexTop@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.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_with_fuel_Vale.Interop.write_vale_mem.fuel_instrumented", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_14ac14fe5618e6aa6489208789111683", "refinement_interpretation_Tm_refine_1f9c035e3d5700980b3b63c565438b2f", "refinement_interpretation_Tm_refine_34ff444db0d6e38eb310a45b8a17c132", "refinement_interpretation_Tm_refine_4f3f4c0e7452015453e686b55c18c37e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d", "refinement_interpretation_Tm_refine_92bffd61ccbecc2ffeb38c51b31903f3", "refinement_interpretation_Tm_refine_a8d5bc6eafc44205d392093af1e7f064", "refinement_interpretation_Tm_refine_cb7955f07f21ce8668d576ee8dfdce26", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Map.domain", "typing_FStar.Set.mem", "typing_Vale.Interop.write_vale_mem", "well-founded-ordering-on-nat" ], 0, "48bed6a5d22080eebc1b47bfa5202782" ], [ "Vale.Interop.monotone_domain_write_vale_mem", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "04854bf5f352ede782e15e9ac82d4e9f" ], [ "Vale.Interop.monotone_domain_write_vale_mem", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_correspondence_Vale.Interop.write_vale_mem.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Vale.Interop.write_vale_mem.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "binder_x_74f682bc25113c64084a04765516a401_4", "binder_x_ae567c2fb75be05905677af440075565_2", "binder_x_b2564773453bdfb53f032dbd3679709e_3", "binder_x_b5ecdf6b68431b1ae5a51ce9723a824d_0", "binder_x_cabf339c83086244c77449dbb6cc3cbc_1", "bool_inversion", "equality_tok_Prims.LexTop@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.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_with_fuel_Vale.Interop.write_vale_mem.fuel_instrumented", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_14ac14fe5618e6aa6489208789111683", "refinement_interpretation_Tm_refine_1f9c035e3d5700980b3b63c565438b2f", "refinement_interpretation_Tm_refine_34ff444db0d6e38eb310a45b8a17c132", "refinement_interpretation_Tm_refine_4f3f4c0e7452015453e686b55c18c37e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d", "refinement_interpretation_Tm_refine_92bffd61ccbecc2ffeb38c51b31903f3", "refinement_interpretation_Tm_refine_a8d5bc6eafc44205d392093af1e7f064", "refinement_interpretation_Tm_refine_cb7955f07f21ce8668d576ee8dfdce26", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Map.domain", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_FStar.UInt.fits", "typing_Vale.Interop.write_vale_mem", "well-founded-ordering-on-nat" ], 0, "a8d2267d539952ca7c0809cd565af571" ], [ "Vale.Interop.correct_down_p_cancel", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "bool_typing", "data_elim_Vale.Interop.Types.Buffer", "equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Interop.Heap_s.correct_down_p", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.down_view", "fuel_guarded_inversion_LowStar.BufferView.Down.view", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "int_inversion", "int_typing", "proj_equation_Vale.Interop.Heap_s.InteropHeap_hs", "proj_equation_Vale.Interop.Types.Buffer_src", "proj_equation_Vale.Interop.Types.Buffer_writeable", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.as_seq", "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.b8_preorder", "typing_Vale.Interop.Types.base_typ_as_type", "typing_Vale.Interop.Types.down_view", "typing_Vale.Interop.Types.get_downview" ], 0, "8c0e701cc344119a42a0eec7ec9d4aa9" ], [ "Vale.Interop.correct_down_p_frame", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing", "data_elim_Vale.Interop.Heap_s.InteropHeap", "data_elim_Vale.Interop.Types.Buffer", "equation_FStar.Seq.Properties.lseq", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Interop.Heap_s.correct_down_p", "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.disjoint", "fuel_guarded_inversion_LowStar.BufferView.Down.view", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Vale.Interop.Types.addr_map_pred", "int_typing", "interpretation_Tm_abs_0b45d135b1bf428b90ecd044d0c4f361", "l_and-interp", "l_quant_interp_bd1f5246e6f57b3b0174bc6d256820c5", "primitive_Prims.op_BarBar", "primitive_Prims.op_LessThan", "proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs", "proj_equation_Vale.Interop.Heap_s.InteropHeap_hs", "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", "refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448", "token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs", "typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.as_seq", "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.b8_preorder", "typing_Vale.Interop.Types.base_typ_as_type", "typing_Vale.Interop.Types.down_view", "typing_Vale.Interop.Types.get_downview" ], 0, "ec8c2b3423cc66460c98ae2c8764cd6b" ], [ "Vale.Interop.addrs_ptr_lemma", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.Interop.Heap_s.addrs_ptr.fuel_instrumented", "@fuel_irrelevance_Vale.Interop.Heap_s.addrs_ptr.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_a2b389b19c9bd00c88f8324fd9c67eb4_2", "binder_x_a80cf7dbe7f42351daa33346677274e2_1", "binder_x_ae567c2fb75be05905677af440075565_4", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "binder_x_d81ce3e0a7e9266eb475a56ef4ca0603_3", "bool_inversion", "equality_tok_Prims.LexTop@tok", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Interop.Types.base_typ_as_type", "equation_with_fuel_Vale.Interop.Heap_s.addrs_ptr.fuel_instrumented", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_union", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5e8a4b3047c38f1ce9b8b1959bab0bd7", "refinement_interpretation_Tm_refine_dd20688ba5635abfb47e96fd328dd7c1", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.length", "typing_Vale.Interop.Heap_s.addrs_ptr", "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", "well-founded-ordering-on-nat" ], 0, "c853be3accc6632ec36be3e2e93dd3c5" ], [ "Vale.Interop.addrs_set_lemma_aux", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Interop.Types.base_typ_as_type", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.length", "typing_Vale.Interop.Types.__proj__Buffer__item__bsrc", "typing_Vale.Interop.Types.__proj__Buffer__item__src", "typing_Vale.Interop.Types.__proj__Buffer__item__writeable", "typing_Vale.Interop.Types.b8_preorder", "typing_Vale.Interop.Types.base_typ_as_type", "typing_Vale.Interop.Types.get_downview" ], 0, "66e33d48ec75ced265f03cbbbfde6196" ], [ "Vale.Interop.addrs_set_lemma_aux", 2, 2, 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.Interop.Heap_s_interpretation_Tm_ghost_arrow_95b27f3bf28277eb7cdde7555d40ab25", "Vale.Interop_interpretation_Tm_ghost_arrow_ad81c22b48c89af0ca992049f0f766b3", "binder_x_03377d74198295feb783e0c699138481_1", "binder_x_a80cf7dbe7f42351daa33346677274e2_0", "binder_x_ae567c2fb75be05905677af440075565_3", "binder_x_d81ce3e0a7e9266eb475a56ef4ca0603_2", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Interop.Types.addr_map", "equation_Vale.Interop.Types.base_typ_as_type", "equation_with_fuel_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "false_interp", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Interop.Heap_s.addrs_ptr", "int_inversion", "int_typing", "kinding_Vale.Interop.Types.b8@tok", "l_or-interp", "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_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5e8a4b3047c38f1ce9b8b1959bab0bd7", "refinement_interpretation_Tm_refine_edf53be96ed83aa35407092156fe2ef2", "refinement_interpretation_Tm_refine_fb1a7adb3dbc242ef08ed91190fbd1ca", "subterm_ordering_Prims.Cons", "typing_FStar.Set.mem", "typing_FStar.Set.set", "typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.length", "typing_Vale.Interop.Types.__proj__Buffer__item__bsrc", "typing_Vale.Interop.Types.__proj__Buffer__item__src", "typing_Vale.Interop.Types.__proj__Buffer__item__writeable", "typing_Vale.Interop.Types.b8_preorder", "typing_Vale.Interop.Types.base_typ_as_type", "typing_Vale.Interop.Types.get_downview" ], 0, "8c6becee645cb2e0da558b17ff71780a" ], [ "Vale.Interop.addrs_set_lemma", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "equation_Vale.Interop.Heap_s.addrs_set", "equation_Vale.Interop.valid_addr", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "int_inversion", "lemma_FStar.Set.mem_empty" ], 0, "e6f1ee7447cbb93b123237d23b53a84b" ], [ "Vale.Interop.addrs_set_mem", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "int_inversion", "refinement_interpretation_Tm_refine_f053bb82fde0bb5e3b79f846e507678a" ], 0, "f2f7de31a964d2e2a44fabf745a3f77b" ], [ "Vale.Interop.write_buffer_vale", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Seq.Properties.lseq", "equation_Prims.nat", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e" ], 0, "e1d0c3ec2ea26f03f38385c177216203" ], [ "Vale.Interop.down_mem_aux", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented", "@query", "Vale.Interop.Heap_s_pretyping_40dec2fdc42f7b5efafe5762d6761d53", "binder_x_03377d74198295feb783e0c699138481_2", "binder_x_21370f7ddf8d50c820cf6bee9e83cc2d_4", "binder_x_40dec2fdc42f7b5efafe5762d6761d53_1", "binder_x_4d87d79814a1a8e492c4d803230b2edf_3", "binder_x_a40f7e487c1020b3b67e6b8bc15f0ef4_0", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Cons@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_FStar.Seq.Properties.lseq", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Interop.Heap_s.disjoint_or_eq_b8", "equation_Vale.Interop.Heap_s.list_disjoint_or_eq_def", "equation_Vale.Interop.disjoint", "equation_Vale.Interop.write_buffer_vale", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "false_interp", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Vale.Interop.Heap_s.list_disjoint_or_eq", "kinding_Vale.Interop.Types.b8@tok", "l_or-interp", "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_0461e75a646cbadf79d6506a42fd03fe", "refinement_interpretation_Tm_refine_0a0f9ff82d2826751d46936e8dab3101", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_ad57436920afdd2862ab5aae22751992", "refinement_interpretation_Tm_refine_cbd5e1eee0ce2bbd77c945327f17d907", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.Interop.Heap_s.list_disjoint_or_eq_def" ], 0, "140aa65022a01b339265066f98856cda" ], [ "Vale.Interop.lemma_write_buffer_domain", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "bool_typing", "data_elim_Vale.Interop.Types.Buffer", "equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.write_buffer_vale", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_empty", "lemma_FStar.Set.mem_union", "primitive_Prims.op_BarBar", "proj_equation_Vale.Interop.Types.Buffer_writeable", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "typing_FStar.Map.domain", "typing_FStar.Set.mem", "typing_FStar.Set.union", "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" ], 0, "bb1bcba25a0f1630f7bebd49ac890318" ], [ "Vale.Interop.lemma_down_mem_aux_domain", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_correspondence_Vale.Interop.down_mem_aux.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_irrelevance_Vale.Interop.down_mem_aux.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Interop.Heap_s_pretyping_40dec2fdc42f7b5efafe5762d6761d53", "binder_x_03377d74198295feb783e0c699138481_2", "binder_x_40dec2fdc42f7b5efafe5762d6761d53_1", "binder_x_4d87d79814a1a8e492c4d803230b2edf_3", "binder_x_a40f7e487c1020b3b67e6b8bc15f0ef4_0", "binder_x_ae567c2fb75be05905677af440075565_5", "binder_x_b51720e983b9c27a92c87a9d9497e534_4", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_elim_Vale.Interop.Heap_s.InteropHeap", "data_typing_intro_Prims.Cons@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Seq.Properties.lseq", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Interop.Heap_s.disjoint_or_eq_b8", "equation_Vale.Interop.Heap_s.list_disjoint_or_eq_def", "equation_Vale.Interop.Heap_s.mk_addr_map", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.down_view", "equation_Vale.Interop.disjoint", "equation_Vale.Interop.write_buffer_vale", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "equation_with_fuel_Vale.Interop.down_mem_aux.fuel_instrumented", "false_interp", "fuel_guarded_inversion_LowStar.BufferView.Down.view", "fuel_guarded_inversion_Prims.list", "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_Prims.int", "function_token_typing_Vale.Def.Words_s.nat8", "function_token_typing_Vale.Interop.Heap_s.list_disjoint_or_eq", "int_inversion", "int_typing", "kinding_Vale.Interop.Types.b8@tok", "l_or-interp", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_empty", "lemma_FStar.Set.mem_union", "primitive_Prims.op_BarBar", "proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs", "proj_equation_Vale.Interop.Types.Buffer_src", "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_0461e75a646cbadf79d6506a42fd03fe", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0a0f9ff82d2826751d46936e8dab3101", "refinement_interpretation_Tm_refine_33cc421ea02f3f3f4c2a3516094392e6", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_3b4ccb64568b95e1eecc4d73b5a24707", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4d9b072f672371f6b87de17de2fda8d9", "refinement_interpretation_Tm_refine_4e6ff91458b7269e02c2aa8dd7d7b82a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5e8a4b3047c38f1ce9b8b1959bab0bd7", "refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699", "refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837", "refinement_interpretation_Tm_refine_9a80b5dfa5564a90c3ca0d543ef7d0b7", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_ad57436920afdd2862ab5aae22751992", "refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448", "refinement_interpretation_Tm_refine_dbe23ff6cb9d4dcade7118b84967c33e", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.Interop.Heap_s.list_disjoint_or_eq_def", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Set.empty", "typing_FStar.Set.mem", "typing_FStar.Set.union", "typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.as_seq", "typing_LowStar.BufferView.Down.length", "typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs", "typing_Vale.Interop.Heap_s.addrs_ptr", "typing_Vale.Interop.Heap_s.global_addrs_map", "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.write_buffer_vale" ], 0, "be74db74a9fc21008af15bc2cef04cef" ], [ "Vale.Interop.down_mem", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Prims.Nil", "data_elim_Vale.Interop.Heap_s.InteropHeap", "data_typing_intro_Prims.Nil@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.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Heap_s.addrs_set", "equation_Vale.Interop.Heap_s.correct_down", "equation_Vale.Interop.valid_addr", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "false_interp", "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_Prims.int", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "kinding_Vale.Interop.Types.b8@tok", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_empty", "primitive_Prims.op_AmpAmp", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_1fba7ece2969e47624842f4169de1234", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699", "refinement_interpretation_Tm_refine_6c6bee8722d5bad4ddf174209b7edaa3", "refinement_interpretation_Tm_refine_8732d2792d5c1e00a22b6183f1a80f51", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_FStar.Map.const", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Set.empty", "typing_FStar.Set.mem", "typing_Vale.Interop.Heap_s.addrs_set" ], 0, "9d60ed80e22d036fd5b54cd138f71d14" ], [ "Vale.Interop.frame_down_mem_aux", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_correspondence_Vale.Interop.down_mem_aux.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_irrelevance_Vale.Interop.down_mem_aux.fuel_instrumented", "@query", "Vale.Interop.Heap_s_pretyping_40dec2fdc42f7b5efafe5762d6761d53", "binder_x_03377d74198295feb783e0c699138481_2", "binder_x_21370f7ddf8d50c820cf6bee9e83cc2d_4", "binder_x_40dec2fdc42f7b5efafe5762d6761d53_1", "binder_x_4d87d79814a1a8e492c4d803230b2edf_3", "binder_x_a40f7e487c1020b3b67e6b8bc15f0ef4_0", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Cons@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_FStar.Seq.Properties.lseq", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Interop.Heap_s.disjoint_or_eq_b8", "equation_Vale.Interop.Heap_s.list_disjoint_or_eq_def", "equation_Vale.Interop.disjoint", "equation_Vale.Interop.write_buffer_vale", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "equation_with_fuel_Vale.Interop.down_mem_aux.fuel_instrumented", "false_interp", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Vale.Interop.Heap_s.list_disjoint_or_eq", "kinding_Vale.Interop.Types.b8@tok", "l_or-interp", "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_0461e75a646cbadf79d6506a42fd03fe", "refinement_interpretation_Tm_refine_0a0f9ff82d2826751d46936e8dab3101", "refinement_interpretation_Tm_refine_4e6ff91458b7269e02c2aa8dd7d7b82a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_a5b41528274692e74fb6e856b9525329", "refinement_interpretation_Tm_refine_ad57436920afdd2862ab5aae22751992", "refinement_interpretation_Tm_refine_cbd5e1eee0ce2bbd77c945327f17d907", "refinement_interpretation_Tm_refine_dbe23ff6cb9d4dcade7118b84967c33e", "refinement_interpretation_Tm_refine_fb1a7adb3dbc242ef08ed91190fbd1ca", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.Interop.Heap_s.list_disjoint_or_eq_def" ], 0, "52ad6c853564ccc52b92476ce6301252" ], [ "Vale.Interop.same_unspecified_down_aux", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_Vale.Interop.Types.b8", "refinement_interpretation_Tm_refine_011c19c35e55781ddb5bbdc0d9eead95" ], 0, "7121d57127d485b21f49d5ce367d3a1d" ], [ "Vale.Interop.same_unspecified_down_aux", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@query", "Vale.Interop.Types_pretyping_cc6beaf9e2624d0643670c917b6f53e1", "constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Nil@tok", "equation_Vale.Interop.Heap_s.addrs_set", "equation_Vale.Interop.Heap_s.mem_of_hs_roots", "equation_Vale.Interop.down_mem", "equation_Vale.Interop.valid_addr", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "false_interp", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs", "int_inversion", "kinding_Vale.Interop.Types.b8@tok", "proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs", "proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs", "projection_inverse_Prims.Nil_a", "projection_inverse_Vale.Interop.Heap_s.InteropHeap_addrs", "projection_inverse_Vale.Interop.Heap_s.InteropHeap_ptrs", "refinement_interpretation_Tm_refine_011c19c35e55781ddb5bbdc0d9eead95", "refinement_interpretation_Tm_refine_195aade13e651466afbb34ebee3ab204", "refinement_interpretation_Tm_refine_f053bb82fde0bb5e3b79f846e507678a", "refinement_interpretation_Tm_refine_fb1a7adb3dbc242ef08ed91190fbd1ca" ], 0, "04ad5b7a6f083ea4346b8efd05b58bdc" ], [ "Vale.Interop.same_unspecified_down", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_Vale.Interop.Types.b8", "refinement_interpretation_Tm_refine_011c19c35e55781ddb5bbdc0d9eead95" ], 0, "b9acfac39bbc9b10818e5b0198f7f844" ], [ "Vale.Interop.same_unspecified_down", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_Vale.Interop.Types.b8", "refinement_interpretation_Tm_refine_011c19c35e55781ddb5bbdc0d9eead95" ], 0, "a6c6a9c314b46f474eb6db7568303cdf" ], [ "Vale.Interop.get_seq_heap", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Interop_interpretation_Tm_arrow_26ff148c0f90a45f463a84c61946fd2d", "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.down_view", "fuel_guarded_inversion_LowStar.BufferView.Down.view", "fuel_guarded_inversion_Vale.Interop.Types.b8", "int_typing", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Interop.Types.Buffer_src", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9bdf64b2660adb592eaffa73ced680cc", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_FStar.UInt8.t", "typing_Vale.Interop.Types.__proj__Buffer__item__src", "typing_Vale.Interop.Types.down_view" ], 0, "6c24b1493f1b133fad9cfba930a6e154" ], [ "Vale.Interop.get_seq_heap_as_seq", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Vale.Interop_interpretation_Tm_arrow_26ff148c0f90a45f463a84c61946fd2d", "bool_inversion", "bool_typing", "data_elim_Vale.Interop.Heap_s.InteropHeap", "data_elim_Vale.Interop.Types.Buffer", "equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Interop.Heap_s.correct_down_p", "equation_Vale.Interop.Heap_s.mk_addr_map", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.down_view", "equation_Vale.Interop.Types.get_downview", "equation_Vale.Interop.get_seq_heap", "fuel_guarded_inversion_LowStar.BufferView.Down.view", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs", "int_inversion", "int_typing", "interpretation_Tm_abs_ad85920da55bfb7f2b90fdba1b44b2e1", "lemma_FStar.Seq.Base.init_index_", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.UInt8.uv_inv", "proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs", "proj_equation_Vale.Interop.Heap_s.InteropHeap_hs", "proj_equation_Vale.Interop.Types.Buffer_src", "proj_equation_Vale.Interop.Types.Buffer_writeable", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837", "refinement_interpretation_Tm_refine_9bdf64b2660adb592eaffa73ced680cc", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_bac48341d72c9512b36c265d7915272a", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.index", "typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.as_seq", "typing_LowStar.BufferView.Down.length", "typing_Tm_abs_ad85920da55bfb7f2b90fdba1b44b2e1", "typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs", "typing_Vale.Interop.Heap_s.global_addrs_map", "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.down_view", "typing_Vale.Interop.Types.get_downview", "typing_Vale.Interop.get_seq_heap" ], 0, "dad5c110f5c7daac518fd1e84dc58665" ], [ "Vale.Interop.up_mem_aux", 1, 2, 1, [ "@query" ], 0, "0b9ddc6c28358ca5ffd97e9371bee8b7" ], [ "Vale.Interop.up_mem_aux", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Interop_interpretation_Tm_arrow_26ff148c0f90a45f463a84c61946fd2d", "b2t_def", "binder_x_03377d74198295feb783e0c699138481_1", "binder_x_03377d74198295feb783e0c699138481_2", "binder_x_42b77fb15436db2979e1388533012436_0", "binder_x_a734470775d7bd1ac67eb44b41a783a6_3", "bool_inversion", "bool_typing", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_elim_Vale.Interop.Heap_s.InteropHeap", "data_typing_intro_Prims.Cons@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "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_LowStar.BufferView.Down.buffer", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Heap_s.addrs_set", "equation_Vale.Interop.Heap_s.correct_down", "equation_Vale.Interop.Heap_s.correct_down_p", "equation_Vale.Interop.Heap_s.disjoint_or_eq_b8", "equation_Vale.Interop.Heap_s.list_disjoint_or_eq_def", "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.get_seq_heap", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "false_interp", "fuel_guarded_inversion_FStar.Pervasives.dtuple4", "fuel_guarded_inversion_LowStar.BufferView.Down.view", "fuel_guarded_inversion_Prims.list", "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_Prims.int", "function_token_typing_Vale.Def.Words_s.nat8", "function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs", "function_token_typing_Vale.Interop.Heap_s.list_disjoint_or_eq", "int_typing", "interpretation_Tm_abs_ad85920da55bfb7f2b90fdba1b44b2e1", "kinding_Vale.Interop.Types.b8@tok", "l_or-interp", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Seq.Base.init_index_", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_refl", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt8.vu_inv", "lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_regions", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Mkdtuple4__1", "proj_equation_FStar.Pervasives.Mkdtuple4__2", "proj_equation_FStar.Pervasives.Mkdtuple4__3", "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", "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", "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_0461e75a646cbadf79d6506a42fd03fe", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699", "refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837", "refinement_interpretation_Tm_refine_9bdf64b2660adb592eaffa73ced680cc", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_b5b8aa7fe8e1f8de462247efdeb2f0f1", "refinement_interpretation_Tm_refine_bac48341d72c9512b36c265d7915272a", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "subterm_ordering_Prims.Cons", "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.Map.domain", "typing_FStar.Map.sel", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Set.empty", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.as_seq", "typing_LowStar.BufferView.Down.length", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_Tm_abs_ad85920da55bfb7f2b90fdba1b44b2e1", "typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs", "typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs", "typing_Vale.Interop.Heap_s.addrs_set", "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" ], 0, "c9c0821850a32bf544b22b93a12741d0" ], [ "Vale.Interop.up_mem", 1, 2, 1, [ "@query" ], 0, "ac92a92b389c86a9c0133a9f0138fafc" ], [ "Vale.Interop.up_mem", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@query", "constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Nil@tok", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "false_interp", "fuel_guarded_inversion_Vale.Interop.Types.b8", "kinding_Vale.Interop.Types.b8@tok", "projection_inverse_Prims.Nil_a" ], 0, "d4c3dc7c4fe19ae860a6fa6f2e183c9e" ], [ "Vale.Interop.down_up_identity_aux", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Vale.Interop.Heap_s.correct_down", "equation_Vale.Interop.Types.b8", "fuel_guarded_inversion_Vale.Interop.Types.b8_", "refinement_interpretation_Tm_refine_26bf6c918a9a6a8e28c8a7da62af89b0", "refinement_interpretation_Tm_refine_4522c68cc58b27fd5780156de9e4df3b", "refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371" ], 0, "ffcd5be88dd458e5da9bbc8bc4d3b34c" ], [ "Vale.Interop.down_up_identity_aux", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_correspondence_Vale.Interop.up_mem_aux.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_irrelevance_Vale.Interop.up_mem_aux.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Interop_interpretation_Tm_arrow_26ff148c0f90a45f463a84c61946fd2d", "binder_x_03377d74198295feb783e0c699138481_1", "binder_x_03377d74198295feb783e0c699138481_2", "binder_x_42b77fb15436db2979e1388533012436_0", "binder_x_6b22ef6a8f229dcbf8070d562ece1375_3", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_elim_Vale.Interop.Heap_s.InteropHeap", "data_typing_intro_Prims.Cons@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_FStar.Seq.Properties.lseq", "equation_LowStar.BufferView.Down.buffer", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Interop.Heap_s.correct_down", "equation_Vale.Interop.Heap_s.correct_down_p", "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.get_seq_heap", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "equation_with_fuel_Vale.Interop.up_mem_aux.fuel_instrumented", "false_interp", "fuel_guarded_inversion_FStar.Pervasives.dtuple4", "fuel_guarded_inversion_LowStar.BufferView.Down.view", "fuel_guarded_inversion_Prims.list", "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_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs", "int_inversion", "interpretation_Tm_abs_ad85920da55bfb7f2b90fdba1b44b2e1", "kinding_Vale.Interop.Types.b8@tok", "l_or-interp", "lemma_FStar.Seq.Base.init_index_", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.UInt8.uv_inv", "lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view", "proj_equation_FStar.Pervasives.Mkdtuple4__1", "proj_equation_FStar.Pervasives.Mkdtuple4__2", "proj_equation_FStar.Pervasives.Mkdtuple4__3", "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", "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_0461e75a646cbadf79d6506a42fd03fe", "refinement_interpretation_Tm_refine_1369401d66ae6f83682a5955a8b9280a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699", "refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837", "refinement_interpretation_Tm_refine_821baf50316b2523cd200c1c0c5a4067", "refinement_interpretation_Tm_refine_9bdf64b2660adb592eaffa73ced680cc", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_bac48341d72c9512b36c265d7915272a", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "subterm_ordering_Prims.Cons", "typing_FStar.Seq.Base.index", "typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.as_seq", "typing_LowStar.BufferView.Down.length", "typing_Tm_abs_ad85920da55bfb7f2b90fdba1b44b2e1", "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.down_view" ], 0, "a220027f15f1ef0cb029e22cb20acacb" ], [ "Vale.Interop.down_up_identity", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Vale.Interop.Heap_s_interpretation_Tm_ghost_arrow_918a6217dad728349cf023555f8761c0", "equation_Vale.Interop.Heap_s.correct_down", "equation_Vale.Interop.Heap_s.down_mem_t", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "refinement_interpretation_Tm_refine_b50f45fba9bc6f60eec05ca9dc1f94ef", "typing_Vale.Interop.down_mem" ], 0, "0268e8dacd41958dd1d792e8fc075e60" ], [ "Vale.Interop.down_up_identity", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@query", "constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Nil@tok", "equation_Vale.Interop.up_mem", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "false_interp", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "kinding_Vale.Interop.Types.b8@tok", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_b50f45fba9bc6f60eec05ca9dc1f94ef" ], 0, "4eee06b3a5f1761ef50374a48c6449e9" ], [ "Vale.Interop.correct_down_p_same_sel", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype", "equation_Vale.Interop.Heap_s.correct_down_p", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.down_view", "fuel_guarded_inversion_LowStar.BufferView.Down.view", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "int_inversion", "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_76e59c7a065e37ed8356ffe7fa5f9837", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_bac48341d72c9512b36c265d7915272a", "typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.as_seq", "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" ], 0, "c3c74d7b81e741ddd6912d2f4384c7eb" ], [ "Vale.Interop.up_down_identity_aux", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Interop.Heap_s_interpretation_Tm_ghost_arrow_918a6217dad728349cf023555f8761c0", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Interop.Heap_s.correct_down", "equation_Vale.Interop.Heap_s.down_mem_t", "equation_Vale.Interop.down_mem", "equation_Vale.Interop.valid_addr", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Set.lemma_equal_elim", "refinement_interpretation_Tm_refine_b50f45fba9bc6f60eec05ca9dc1f94ef", "refinement_interpretation_Tm_refine_f053bb82fde0bb5e3b79f846e507678a", "typing_FStar.Map.domain", "typing_Vale.Interop.Heap_s.addrs_set", "typing_Vale.Interop.down_mem" ], 0, "cadd0af2f09637b768fd28575ebcbbf0" ], [ "Vale.Interop.up_down_identity", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_3a2dd58f50cd5923bb942c80f67255f6" ], 0, "54a5bd8612d0454bfcac2e53dbe0717d" ], [ "Vale.Interop.up_down_identity", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "data_elim_Vale.Interop.Heap_s.InteropHeap", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Interop.Heap_s.addrs_set", "equation_Vale.Interop.Heap_s.correct_down", "equation_Vale.Interop.Heap_s.mem_of_hs_roots", "equation_Vale.Interop.valid_addr", "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.Def.Words_s.nat8", "int_inversion", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_equal_elim", "lemma_FStar.Map.lemma_equal_intro", "lemma_FStar.Set.lemma_equal_elim", "proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs", "proj_equation_Vale.Interop.Heap_s.InteropHeap_hs", "proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs", "refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe", "refinement_interpretation_Tm_refine_219d50ffa8841a417ab97c45ba2e1cc6", "refinement_interpretation_Tm_refine_3a2dd58f50cd5923bb942c80f67255f6", "refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699", "refinement_interpretation_Tm_refine_8c41f6f180b71033245cdc7aca5395e0", "refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f", "typing_FStar.Map.domain", "typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs", "typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs", "typing_Vale.Interop.Heap_s.addrs_set" ], 0, "9576a2e992fb06b69b3679a7f6d65c39" ], [ "Vale.Interop.update_buffer_up_mem_aux", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Seq.Properties.lseq", "equation_LowStar.BufferView.Down.buffer", "equation_Prims.eqtype", "equation_Prims.l_and", "equation_Prims.squash", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "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.get_seq_heap", "fuel_guarded_inversion_FStar.Pervasives.dtuple4", "fuel_guarded_inversion_LowStar.BufferView.Down.view", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Words_s.nat8", "l_and-interp", "l_quant_interp_31b11ee0751d315194beda71382ee5a5", "lemma_FStar.Set.lemma_equal_elim", "lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view", "proj_equation_FStar.Pervasives.Mkdtuple4__1", "proj_equation_FStar.Pervasives.Mkdtuple4__2", "proj_equation_FStar.Pervasives.Mkdtuple4__3", "proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs", "proj_equation_Vale.Interop.Heap_s.InteropHeap_hs", "proj_equation_Vale.Interop.Types.Buffer_bsrc", "proj_equation_Vale.Interop.Types.Buffer_src", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_680c8fa1151b64031916ed41bb96d9be", "refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f", "typing_FStar.Map.domain", "typing_FStar.UInt8.t", "typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs", "typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs", "typing_Vale.Interop.Heap_s.addrs_set", "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.get_seq_heap" ], 0, "a6b20a99f3dc16e13b6c101a35ed4167" ], [ "Vale.Interop.update_buffer_up_mem_aux", 2, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_correspondence_Vale.Interop.up_mem_aux.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Vale.Interop.up_mem_aux.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Interop.Types_pretyping_cc6beaf9e2624d0643670c917b6f53e1", "Vale.Interop_interpretation_Tm_arrow_26ff148c0f90a45f463a84c61946fd2d", "b2t_def", "binder_x_03377d74198295feb783e0c699138481_2", "binder_x_03377d74198295feb783e0c699138481_3", "binder_x_42b77fb15436db2979e1388533012436_0", "binder_x_42b77fb15436db2979e1388533012436_1", "binder_x_aa43c49dd85e19ddcec101eda2efb815_5", "binder_x_cc6beaf9e2624d0643670c917b6f53e1_4", "bool_inversion", "bool_typing", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_elim_Vale.Interop.Heap_s.InteropHeap", "data_typing_intro_Prims.Cons@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp", "equation_FStar.Monotonic.HyperStack.live_region", "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_LowStar.BufferView.Down.buffer", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.l_Forall", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.squash", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Heap_s.addrs_set", "equation_Vale.Interop.Heap_s.correct_down_p", "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.get_seq_heap", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "equation_with_fuel_Vale.Interop.up_mem_aux.fuel_instrumented", "false_interp", "fuel_guarded_inversion_FStar.Pervasives.dtuple4", "fuel_guarded_inversion_LowStar.BufferView.Down.view", "fuel_guarded_inversion_Prims.list", "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.Def.Words_s.nat8", "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", "interpretation_Tm_abs_ad85920da55bfb7f2b90fdba1b44b2e1", "kinding_Vale.Interop.Types.b8@tok", "l_and-interp", "l_or-interp", "l_quant_interp_67783243426a60b39d9fb919f9ee0e7a", "l_quant_interp_bd1f5246e6f57b3b0174bc6d256820c5", "l_quant_interp_decc1164beb863c8f91695473785a596", "l_quant_interp_f162ed645e98138b81049100b6d3ba68", "lemma_FStar.Seq.Base.init_index_", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_refl", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt8.vu_inv", "lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.live_region_frameOf", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_regions", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Mkdtuple4__1", "proj_equation_FStar.Pervasives.Mkdtuple4__2", "proj_equation_FStar.Pervasives.Mkdtuple4__3", "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", "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", "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_0461e75a646cbadf79d6506a42fd03fe", "refinement_interpretation_Tm_refine_0dbdff46d67e5b175b2f3cc0cb46b974", "refinement_interpretation_Tm_refine_0e4cf65f7351e0808e0a2ed028012cbb", "refinement_interpretation_Tm_refine_1369401d66ae6f83682a5955a8b9280a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699", "refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837", "refinement_interpretation_Tm_refine_9bdf64b2660adb592eaffa73ced680cc", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_bac48341d72c9512b36c265d7915272a", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448", "refinement_interpretation_Tm_refine_cb48431194770620248f529214b5785a", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "subterm_ordering_Prims.Cons", "token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs", "token_correspondence_Vale.Interop.Heap_s.list_disjoint_or_eq_def", "typing_FStar.Map.domain", "typing_FStar.Map.sel", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.live_region", "typing_FStar.Set.empty", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.UInt8.t", "typing_LowStar.BufferView.Down.as_seq", "typing_LowStar.BufferView.Down.length", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_Tm_abs_ad85920da55bfb7f2b90fdba1b44b2e1", "typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs", "typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs", "typing_Vale.Interop.Heap_s.addrs_set", "typing_Vale.Interop.Heap_s.mk_addr_map", "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.get_seq_heap" ], 0, "4e7f8823beffef6aeeef596804b75e30" ], [ "Vale.Interop.update_buffer_up_mem", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "data_elim_Vale.Interop.Heap_s.InteropHeap", "equation_FStar.Seq.Properties.lseq", "equation_LowStar.BufferView.Down.buffer", "equation_Prims.eqtype", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Interop.Heap_s.correct_down", "equation_Vale.Interop.Types.down_view", "equation_Vale.Interop.Types.get_downview", "fuel_guarded_inversion_FStar.Pervasives.dtuple4", "fuel_guarded_inversion_LowStar.BufferView.Down.view", "fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap", "fuel_guarded_inversion_Vale.Interop.Types.b8", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Words_s.nat8", "lemma_FStar.Set.lemma_equal_elim", "lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view", "proj_equation_FStar.Pervasives.Mkdtuple4__1", "proj_equation_FStar.Pervasives.Mkdtuple4__2", "proj_equation_FStar.Pervasives.Mkdtuple4__3", "proj_equation_Vale.Interop.Heap_s.InteropHeap_hs", "proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_50d3b3dd51fb0799a5eeaaea500ed7b0", "refinement_interpretation_Tm_refine_61ad87a48c5493622a87dee22c6da699", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_b50f45fba9bc6f60eec05ca9dc1f94ef", "refinement_interpretation_Tm_refine_f053bb82fde0bb5e3b79f846e507678a", "typing_FStar.Map.domain", "typing_FStar.UInt8.t", "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" ], 0, "97b46c3c76c355aba7f546e9e00f41d0" ], [ "Vale.Interop.update_buffer_up_mem", 2, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Interop.Types_pretyping_cc6beaf9e2624d0643670c917b6f53e1", "constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Nil@tok", "equation_Vale.Arch.MachineHeap_s.machine_heap", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Interop.Heap_s.correct_down", "equation_Vale.Interop.up_mem", "equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented", "false_interp", "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.Def.Words_s.nat8", "kinding_Vale.Interop.Types.b8@tok", "lemma_FStar.Set.lemma_equal_elim", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_50d3b3dd51fb0799a5eeaaea500ed7b0", "refinement_interpretation_Tm_refine_b50f45fba9bc6f60eec05ca9dc1f94ef", "refinement_interpretation_Tm_refine_f053bb82fde0bb5e3b79f846e507678a", "typing_FStar.Map.domain", "typing_Vale.Interop.Heap_s.addrs_set" ], 0, "af2bf8ae5cea584105bdb3576fb10b44" ] ] ]