Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
Vale.Interop.fst.hints
[
"���\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,
"b1892d3eca4d97a87312d5ace99b1d6f"
],
[
"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,
"940f982b2450e45a075376ad478e8251"
],
[
"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,
"54b412dc66721316ce23826eb56b7e5d"
],
[
"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,
"543eb50986fd6e7e6e52c1cac457dada"
],
[
"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,
"697b9ccea012d8b06f0c69565dd4833f"
],
[
"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,
"327d93affa4a4dcc5a4787fd4b31982a"
],
[
"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,
"5cb6013bcfc9546f4a13f85c852f7300"
],
[
"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,
"9f1b2a1ce10686b098e14bf06804121a"
],
[
"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,
"8d9c5fbd23a10f4156de9ca7922460d0"
],
[
"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,
"fb6a5d27cb99b546eba2dfa590727154"
],
[
"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,
"99d5f8ed4e982b6476f13c8a301c384c"
],
[
"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,
"b257d6679b47919800b3d31500e87982"
],
[
"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,
"12931a5ddee30ee911f6815046962ac6"
],
[
"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,
"0a5b9ff272b3721eea4bcffce4888849"
],
[
"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,
"a1788a75638c0217c04a7707bc10bcbc"
],
[
"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,
"bc887e6fe495d542a5d47d728ace76c9"
],
[
"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_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.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,
"ddc048590c000cc4b03a8282342db0f8"
],
[
"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,
"c53d48211375eabaa1bba232a314eb87"
],
[
"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,
"780c90518deb03cbd1faa459128b99ef"
],
[
"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,
"3386d5eb7f33263129d0fba6a1302ed2"
],
[
"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_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_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,
"c6bbe62c76fb1dc337dc0a998145f909"
],
[
"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,
"9fb9dc7a49ea0eb476d9fe00dbbc1172"
],
[
"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",
"Vale.Interop.Types_pretyping_cc6beaf9e2624d0643670c917b6f53e1",
"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_Prims.Cons", "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_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.Types.get_downview",
"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.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.Heap_s.InteropHeap_hs",
"proj_equation_Vale.Interop.Types.Buffer_src",
"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.down_mem_aux",
"typing_Vale.Interop.write_buffer_vale"
],
0,
"4ea9b78733d48f6b9649d19ae07eb7d1"
],
[
"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,
"dbd496f058bf960ea66ee1a4de8796b2"
],
[
"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",
"Vale.Interop.Types_pretyping_cc6beaf9e2624d0643670c917b6f53e1",
"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_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_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,
"459b824aad58edaf433c51881dda5392"
],
[
"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,
"e603073859ef849469e9af9c689ec1d9"
],
[
"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,
"1e9fed33a15655dfe3db8b09d3966282"
],
[
"Vale.Interop.same_unspecified_down",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"refinement_interpretation_Tm_refine_011c19c35e55781ddb5bbdc0d9eead95"
],
0,
"67514184f999bb85ad0e6787ac6dca0a"
],
[
"Vale.Interop.same_unspecified_down",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"refinement_interpretation_Tm_refine_011c19c35e55781ddb5bbdc0d9eead95"
],
0,
"e873975ce507de6c021c04c2b551145f"
],
[
"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,
"10cce7e012fdfcc6ecf7dd50bc5d0c41"
],
[
"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,
"8418d6673723b159a423519debc2e962"
],
[
"Vale.Interop.up_mem_aux",
1,
2,
1,
[ "@query" ],
0,
"2e382d9bcda48eed5a1019127093df17"
],
[
"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.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_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_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.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_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_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.domain", "typing_FStar.Map.sel",
"typing_FStar.Monotonic.HyperHeap.rid", "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,
"0ca95e354b2066c33d4054d240da452e"
],
[
"Vale.Interop.up_mem",
1,
2,
1,
[ "@query" ],
0,
"3577dd9755604a9b0971e775167ad7de"
],
[
"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,
"efed1b7fc0a1ec72296e31159ae9adce"
],
[
"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,
"78145fc59ee47b19424dbc759e76f15e"
],
[
"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_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_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "int_typing",
"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_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_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.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,
"d40cdbb3639289293f85b147183713f9"
],
[
"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,
"59c237d2a9226bf14877226575c5a1ad"
],
[
"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,
"f1ac1aed08d1411e1f430a56b5c1c2bd"
],
[
"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,
"9dbf25425919cbeb47ee2c4592a14296"
],
[
"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,
"58432d453ae38897ede20bfdf61fb622"
],
[
"Vale.Interop.up_down_identity",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_3a2dd58f50cd5923bb942c80f67255f6"
],
0,
"b86fc9201eaa562651f7ab18e1066b25"
],
[
"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,
"87feeb17f94c76c3a377538e715c4871"
],
[
"Vale.Interop.update_buffer_up_mem_aux",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_FStar.Seq.Properties.lseq",
"equation_LowStar.BufferView.Down.buffer", "equation_Prims.eqtype",
"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.Types.b8",
"function_token_typing_Prims.__cache_version_number__",
"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_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_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a59745a3ad7ef5f619e237e3b367ec0a",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_d2fc72c0eb1a60cd80867fbd57769cfc",
"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,
"d777b792ba75e4acf0ab4c6fe65fe367"
],
[
"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_elim_Vale.Interop.Types.Buffer",
"data_typing_intro_Prims.Cons@tok", "disc_equation_Prims.Cons",
"disc_equation_Prims.Nil", "eq2-interp",
"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_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_Forall",
"equation_Prims.nat", "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.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.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",
"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",
"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_0dbdff46d67e5b175b2f3cc0cb46b974",
"refinement_interpretation_Tm_refine_0e4cf65f7351e0808e0a2ed028012cbb",
"refinement_interpretation_Tm_refine_1369401d66ae6f83682a5955a8b9280a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4f48f97d5ef775a2195e0899eac73e60",
"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_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"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.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Seq.Base.index", "typing_FStar.Set.empty",
"typing_FStar.Set.intersect", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.UInt.fits",
"typing_FStar.UInt8.t", "typing_FStar.UInt8.v",
"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,
"1707c146db6a3b10a86b2490504bed8a"
],
[
"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,
"a163bba24ce5e792a6f71bb8fb40ecb4"
],
[
"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,
"91184f1efa31d45a28088da76cc2c9eb"
]
]
]
Computing file changes ...
