Revision 0d9153dc34ee2dcf0821e3f21e825fc5bb8895b4 authored by Santiago Zanella-Beguelin on 11 December 2019, 17:46:08 UTC, committed by Santiago Zanella-Beguelin on 12 December 2019, 10:33:01 UTC
1 parent 7405f78
Vale.Interop.fst.hints
[
"��2��Z����9U��\"",
[
[
"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,
"4558139578ecb6a1bacb7a7030e1e8d9"
],
[
"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_51dbebd9cf59186809b4de77530fed70_3",
"binder_x_aba4fc5c8c7a0415fec2e0dba1a48ced_4",
"binder_x_c0440b3284ca737181333a4a33d51162_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.__cache_version_number__",
"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_177df2c7739f3742ccbbf596dce12069",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_564f6b69b5d05cb41cf584149360c7e2",
"refinement_interpretation_Tm_refine_d8fe84c8d5c9b29f3b9a7b277c3aaf91",
"refinement_interpretation_Tm_refine_edb4a1650c56ca2a2712ec5f68e13afa",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"well-founded-ordering-on-nat"
],
0,
"950e76729008462a756496fc515e7505"
],
[
"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,
"df94fd03538b386ce5621b6f10596a35"
],
[
"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_1fc216e94d386fef093b3463724fa369_0",
"binder_x_51dbebd9cf59186809b4de77530fed70_3",
"binder_x_aba4fc5c8c7a0415fec2e0dba1a48ced_4",
"binder_x_ae567c2fb75be05905677af440075565_2",
"binder_x_ae567c2fb75be05905677af440075565_5",
"binder_x_c0440b3284ca737181333a4a33d51162_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.__cache_version_number__",
"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_1114023a1eaeca0a803ad22cfa790148",
"refinement_interpretation_Tm_refine_177df2c7739f3742ccbbf596dce12069",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_564f6b69b5d05cb41cf584149360c7e2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_ad0fec184b727a328005de1153b24a78",
"refinement_interpretation_Tm_refine_d8fe84c8d5c9b29f3b9a7b277c3aaf91",
"refinement_interpretation_Tm_refine_e5d5a502c207d9c5cac1ea43b70ade32",
"refinement_interpretation_Tm_refine_edb4a1650c56ca2a2712ec5f68e13afa",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"well-founded-ordering-on-nat"
],
0,
"6b355cc50f1207d607c9ce9634ac77c6"
],
[
"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,
"477f001dd347a2651b8a3b1b17360c6f"
],
[
"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_1fc216e94d386fef093b3463724fa369_0",
"binder_x_51dbebd9cf59186809b4de77530fed70_3",
"binder_x_aba4fc5c8c7a0415fec2e0dba1a48ced_4",
"binder_x_ae567c2fb75be05905677af440075565_2",
"binder_x_c0440b3284ca737181333a4a33d51162_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.__cache_version_number__",
"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_1114023a1eaeca0a803ad22cfa790148",
"refinement_interpretation_Tm_refine_177df2c7739f3742ccbbf596dce12069",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_564f6b69b5d05cb41cf584149360c7e2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_ad0fec184b727a328005de1153b24a78",
"refinement_interpretation_Tm_refine_d8fe84c8d5c9b29f3b9a7b277c3aaf91",
"refinement_interpretation_Tm_refine_e5d5a502c207d9c5cac1ea43b70ade32",
"refinement_interpretation_Tm_refine_edb4a1650c56ca2a2712ec5f68e13afa",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"well-founded-ordering-on-nat"
],
0,
"d07f0fe1fbafe7cec2bc60804ca2da63"
],
[
"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,
"e232a38db743bde2833de41988210ae5"
],
[
"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_1fc216e94d386fef093b3463724fa369_0",
"binder_x_51dbebd9cf59186809b4de77530fed70_3",
"binder_x_aba4fc5c8c7a0415fec2e0dba1a48ced_4",
"binder_x_ae567c2fb75be05905677af440075565_2",
"binder_x_c0440b3284ca737181333a4a33d51162_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.__cache_version_number__",
"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_1114023a1eaeca0a803ad22cfa790148",
"refinement_interpretation_Tm_refine_177df2c7739f3742ccbbf596dce12069",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_564f6b69b5d05cb41cf584149360c7e2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_ad0fec184b727a328005de1153b24a78",
"refinement_interpretation_Tm_refine_d8fe84c8d5c9b29f3b9a7b277c3aaf91",
"refinement_interpretation_Tm_refine_e5d5a502c207d9c5cac1ea43b70ade32",
"refinement_interpretation_Tm_refine_edb4a1650c56ca2a2712ec5f68e13afa",
"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,
"53a686327ceafe1c000315210254da88"
],
[
"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,
"8ca995ff1c400cf9d13398a76f3f5ee6"
],
[
"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_1fc216e94d386fef093b3463724fa369_0",
"binder_x_51dbebd9cf59186809b4de77530fed70_3",
"binder_x_aba4fc5c8c7a0415fec2e0dba1a48ced_4",
"binder_x_ae567c2fb75be05905677af440075565_2",
"binder_x_c0440b3284ca737181333a4a33d51162_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.__cache_version_number__",
"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_1114023a1eaeca0a803ad22cfa790148",
"refinement_interpretation_Tm_refine_177df2c7739f3742ccbbf596dce12069",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_564f6b69b5d05cb41cf584149360c7e2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_ad0fec184b727a328005de1153b24a78",
"refinement_interpretation_Tm_refine_d8fe84c8d5c9b29f3b9a7b277c3aaf91",
"refinement_interpretation_Tm_refine_e5d5a502c207d9c5cac1ea43b70ade32",
"refinement_interpretation_Tm_refine_edb4a1650c56ca2a2712ec5f68e13afa",
"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,
"305af84f210864f75c8d411658a1710c"
],
[
"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,
"ab2622d6f10bd65d05ffad09a1e808fa"
],
[
"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_1fc216e94d386fef093b3463724fa369_0",
"binder_x_51dbebd9cf59186809b4de77530fed70_3",
"binder_x_aba4fc5c8c7a0415fec2e0dba1a48ced_4",
"binder_x_ae567c2fb75be05905677af440075565_2",
"binder_x_c0440b3284ca737181333a4a33d51162_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.__cache_version_number__",
"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_1114023a1eaeca0a803ad22cfa790148",
"refinement_interpretation_Tm_refine_177df2c7739f3742ccbbf596dce12069",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_564f6b69b5d05cb41cf584149360c7e2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_ad0fec184b727a328005de1153b24a78",
"refinement_interpretation_Tm_refine_d8fe84c8d5c9b29f3b9a7b277c3aaf91",
"refinement_interpretation_Tm_refine_e5d5a502c207d9c5cac1ea43b70ade32",
"refinement_interpretation_Tm_refine_edb4a1650c56ca2a2712ec5f68e13afa",
"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,
"1f48190a18505ce1e6e0a16d5092af40"
],
[
"Vale.Interop.correct_down_p_cancel",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat8",
"equation_Vale.Interop.Heap_s.correct_down_p",
"equation_Vale.Interop.Types.b8",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"primitive_Prims.op_Addition",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"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__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.get_downview"
],
0,
"74d2c398dee73b9b68985afd0aa4d582"
],
[
"Vale.Interop.correct_down_p_frame",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"equation_FStar.Seq.Properties.lseq",
"equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.nat",
"equation_Vale.Interop.Heap_s.correct_down_p",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.disjoint_addr",
"equation_Vale.Interop.disjoint",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t", "int_inversion", "int_typing",
"primitive_Prims.op_Addition", "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_rel",
"proj_equation_Vale.Interop.Types.Buffer_rrel",
"proj_equation_Vale.Interop.Types.Buffer_src",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_LowStar.BufferView.Down.as_seq",
"typing_LowStar.BufferView.Down.length",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.get_downview"
],
0,
"c88ea41c3ed18be8de88e79bbec622e2"
],
[
"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_a80cf7dbe7f42351daa33346677274e2_1",
"binder_x_ae567c2fb75be05905677af440075565_4",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_d81ce3e0a7e9266eb475a56ef4ca0603_3",
"binder_x_eea8dba8e070b31afbb128b24051b46c_2", "bool_inversion",
"equality_tok_Prims.LexTop@tok", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Interop.Types.b8",
"equation_with_fuel_Vale.Interop.Heap_s.addrs_ptr.fuel_instrumented",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "lemma_FStar.Set.mem_singleton",
"lemma_FStar.Set.mem_union", "primitive_Prims.op_Addition",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_aba125c2fdf18c30de849e118ca1f35e",
"refinement_interpretation_Tm_refine_ce4db8891538b6328516fc3336428086",
"typing_FStar.Set.mem", "typing_FStar.Set.singleton",
"typing_FStar.Set.union", "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__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.get_downview",
"well-founded-ordering-on-nat"
],
0,
"12f4248d7148caf5798e098df1710c7e"
],
[
"Vale.Interop.addrs_set_lemma_aux",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Interop.Types.b8",
"function_token_typing_FStar.UInt8.t",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"typing_LowStar.BufferView.Down.length",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.get_downview"
],
0,
"726a8a49cc5d077fa1abd38dd505c9e8"
],
[
"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_614bca55155151d5a1025517a3659f33",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"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.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"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_FStar.UInt8.t",
"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", "l_or-interp",
"primitive_Prims.op_Addition", "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_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_aba125c2fdf18c30de849e118ca1f35e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_edf53be96ed83aa35407092156fe2ef2",
"refinement_interpretation_Tm_refine_fb1a7adb3dbc242ef08ed91190fbd1ca",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"subterm_ordering_Prims.Cons", "typing_FStar.Set.mem",
"typing_FStar.Set.set", "typing_LowStar.BufferView.Down.length",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.get_downview"
],
0,
"27cf5ae24de29c44d834b2a9d2ace8ab"
],
[
"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,
"4915cdb2b0bab38f6daad4f3a3af49af"
],
[
"Vale.Interop.addrs_set_mem",
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", "equation_Vale.Interop.Types.b8",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_", "int_inversion",
"lemma_Vale.Interop.addrs_set_lemma",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"refinement_interpretation_Tm_refine_25f03280eee84f53f1b2ad3f058d1b9b",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371"
],
0,
"cb60013081164c77f1c3dcb61b2feffd"
],
[
"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,
"74fda8ac443652907563d14f168a9a58"
],
[
"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",
"equation_Vale.Interop.Types.b8", "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_", "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_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ad57436920afdd2862ab5aae22751992",
"refinement_interpretation_Tm_refine_cbd5e1eee0ce2bbd77c945327f17d907",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"subterm_ordering_Prims.Cons"
],
0,
"ecea4ccd290dc9d07dc4445c53feb3a7"
],
[
"Vale.Interop.lemma_write_buffer_domain",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.Types_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"bool_inversion", "data_elim_Vale.Interop.Heap_s.InteropHeap",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.nat",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"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_FStar.UInt8.t",
"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",
"int_inversion", "lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_empty", "lemma_FStar.Set.mem_union",
"primitive_Prims.op_Addition", "primitive_Prims.op_BarBar",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"typing_FStar.Map.domain", "typing_FStar.Set.mem",
"typing_FStar.Set.union", "typing_LowStar.BufferView.Down.length",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.get_downview"
],
0,
"4c66d11c1e643a191c3d24e116340584"
],
[
"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_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"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.nat",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.Heap_s.disjoint_or_eq_b8",
"equation_Vale.Interop.Heap_s.list_disjoint_or_eq",
"equation_Vale.Interop.Heap_s.mk_addr_map",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8", "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_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"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",
"int_inversion", "int_typing", "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_Addition",
"primitive_Prims.op_BarBar",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_addrs",
"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_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_33cc421ea02f3f3f4c2a3516094392e6",
"refinement_interpretation_Tm_refine_3b4ccb64568b95e1eecc4d73b5a24707",
"refinement_interpretation_Tm_refine_4d9b072f672371f6b87de17de2fda8d9",
"refinement_interpretation_Tm_refine_4e6ff91458b7269e02c2aa8dd7d7b82a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_9a80b5dfa5564a90c3ca0d543ef7d0b7",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_aba125c2fdf18c30de849e118ca1f35e",
"refinement_interpretation_Tm_refine_ad57436920afdd2862ab5aae22751992",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_dbe23ff6cb9d4dcade7118b84967c33e",
"refinement_interpretation_Tm_refine_fe084d710bd16568de37f3a949480eea",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"subterm_ordering_Prims.Cons", "typing_FStar.Map.contains",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Set.empty", "typing_FStar.Set.mem",
"typing_FStar.Set.union", "typing_LowStar.BufferView.Down.as_seq",
"typing_LowStar.BufferView.Down.length", "typing_Prims.uu___is_Nil",
"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__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.write_buffer_vale"
],
0,
"ab21a268f0d94d12bb12c70243202230"
],
[
"Vale.Interop.down_mem",
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", "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.Types.b8", "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", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_empty",
"lemma_Vale.Interop.addrs_set_lemma", "primitive_Prims.op_Addition",
"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_25f03280eee84f53f1b2ad3f058d1b9b",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6c6bee8722d5bad4ddf174209b7edaa3",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_8732d2792d5c1e00a22b6183f1a80f51",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f053bb82fde0bb5e3b79f846e507678a",
"refinement_interpretation_Tm_refine_fe084d710bd16568de37f3a949480eea",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"typing_FStar.Map.const", "typing_FStar.Map.contains",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Set.empty", "typing_FStar.Set.mem",
"typing_Vale.Interop.Heap_s.addrs_set"
],
0,
"1f9c98872d019e9fd6aebe8c2d29e199"
],
[
"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_Vale.Interop.Heap_s.disjoint_or_eq_b8",
"equation_Vale.Interop.Heap_s.list_disjoint_or_eq",
"equation_Vale.Interop.Types.b8", "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_", "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_703c6f879c5b001c36b204e25e1b2371",
"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",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"subterm_ordering_Prims.Cons"
],
0,
"fdb9cd18f833707dbe241a5810f6bee4"
],
[
"Vale.Interop.same_unspecified_down_aux",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_68aa0df7915bf348bcb6532fe1aaf275"
],
0,
"2f4c684dea1d804711ae5b4d9263a55e"
],
[
"Vale.Interop.same_unspecified_down_aux",
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.Heap_s.mem_of_hs_roots",
"equation_Vale.Interop.Types.b8", "equation_Vale.Interop.down_mem",
"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",
"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_195aade13e651466afbb34ebee3ab204",
"refinement_interpretation_Tm_refine_1ea192f769de03e3ae8a35b678483e00",
"refinement_interpretation_Tm_refine_68aa0df7915bf348bcb6532fe1aaf275",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_fb1a7adb3dbc242ef08ed91190fbd1ca",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371"
],
0,
"0231cfa23b4f011aadf080fe7e9f56f7"
],
[
"Vale.Interop.same_unspecified_down",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_68aa0df7915bf348bcb6532fe1aaf275"
],
0,
"f84d7851565017b9d83abc374f97285b"
],
[
"Vale.Interop.same_unspecified_down",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_68aa0df7915bf348bcb6532fe1aaf275"
],
0,
"44c037bfd1653583ae7d0e5e58737096"
],
[
"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",
"Vale.Interop_interpretation_Tm_arrow_992025dc489e7315d2abb53d1ad49c82",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "equation_Vale.Interop.Types.b8",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t", "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",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_ff9cf9634d9ad82e44410ccec01e1955"
],
0,
"63641ac0d368be063f2986ea0de369b0"
],
[
"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_992025dc489e7315d2abb53d1ad49c82",
"data_elim_Vale.Interop.Heap_s.InteropHeap",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.nat",
"equation_Vale.Interop.Heap_s.correct_down_p",
"equation_Vale.Interop.Heap_s.mk_addr_map",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.get_seq_heap",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion", "int_typing",
"interpretation_Tm_abs_b51c6477abe9001f80a2c30fadfd2dca",
"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",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_bccbced7332638ded7edb52a93b52677",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"refinement_interpretation_Tm_refine_ff9cf9634d9ad82e44410ccec01e1955",
"typing_FStar.Seq.Base.index",
"typing_LowStar.BufferView.Down.as_seq",
"typing_LowStar.BufferView.Down.length",
"typing_Tm_abs_b51c6477abe9001f80a2c30fadfd2dca",
"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__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.get_seq_heap"
],
0,
"81e8d66734dcbad7d9ce46b38352cad9"
],
[
"Vale.Interop.up_mem_aux",
1,
2,
1,
[ "@query" ],
0,
"a01ee55a83cfb94a3e35e82d60b7f4e0"
],
[
"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_992025dc489e7315d2abb53d1ad49c82",
"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_LowStar.Monotonic.Buffer.disjoint", "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",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"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",
"false_interp", "fuel_guarded_inversion_FStar.Pervasives.dtuple4",
"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.UInt8.t",
"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",
"int_typing",
"interpretation_Tm_abs_b51c6477abe9001f80a2c30fadfd2dca",
"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_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_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_b5b8aa7fe8e1f8de462247efdeb2f0f1",
"refinement_interpretation_Tm_refine_bccbced7332638ded7edb52a93b52677",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_fe084d710bd16568de37f3a949480eea",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"refinement_interpretation_Tm_refine_ff9cf9634d9ad82e44410ccec01e1955",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"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_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_b51c6477abe9001f80a2c30fadfd2dca",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Heap_s.addrs_set",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.get_downview"
],
0,
"a01d475a9e2876cd15786906ed306999"
],
[
"Vale.Interop.up_mem",
1,
2,
1,
[ "@query" ],
0,
"ca141303d8bc4b1aca6938510bbe3092"
],
[
"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_Vale.Interop.Types.b8",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"false_interp", "fuel_guarded_inversion_Vale.Interop.Types.b8_",
"projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371"
],
0,
"e84415f55478ed13fffadc97d613e6ff"
],
[
"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,
"e7564f3b664e1d404a1b54c6169bcfd9"
],
[
"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",
"Vale.Interop_interpretation_Tm_arrow_992025dc489e7315d2abb53d1ad49c82",
"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.Interop.Heap_s.correct_down",
"equation_Vale.Interop.Heap_s.correct_down_p",
"equation_Vale.Interop.Types.b8",
"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_Prims.list",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"int_inversion",
"interpretation_Tm_abs_b51c6477abe9001f80a2c30fadfd2dca",
"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_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_821baf50316b2523cd200c1c0c5a4067",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_bccbced7332638ded7edb52a93b52677",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_fe084d710bd16568de37f3a949480eea",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"refinement_interpretation_Tm_refine_ff9cf9634d9ad82e44410ccec01e1955",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"subterm_ordering_Prims.Cons", "typing_FStar.Seq.Base.index",
"typing_LowStar.BufferView.Down.as_seq",
"typing_LowStar.BufferView.Down.length",
"typing_Tm_abs_b51c6477abe9001f80a2c30fadfd2dca",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view"
],
0,
"6b63ad276fa7fb22cfc23f490f006fc9"
],
[
"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,
"7312bd5df1ead2388b0327d69798cc89"
],
[
"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.Types.b8",
"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",
"projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_b50f45fba9bc6f60eec05ca9dc1f94ef",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371"
],
0,
"6a1d76b929b9912eb5784bf129d6c790"
],
[
"Vale.Interop.correct_down_p_same_sel",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Properties.lseq",
"equation_Vale.Interop.Heap_s.correct_down_p",
"equation_Vale.Interop.Types.b8",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t", "int_inversion", "int_typing",
"primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_hs",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_bccbced7332638ded7edb52a93b52677",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"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__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.get_downview"
],
0,
"7e264a76448c7ea78d5d82aeb5dc4693"
],
[
"Vale.Interop.up_down_identity_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", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_40dec2fdc42f7b5efafe5762d6761d53_0",
"binder_x_ae567c2fb75be05905677af440075565_2",
"binder_x_fc78d7c96ee4b05d332ae57ac99aff6c_1",
"constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Nil@tok",
"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.correct_down",
"equation_Vale.Interop.Types.b8", "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.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",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_Vale.Interop.addrs_set_lemma",
"proj_equation_Vale.Interop.Heap_s.InteropHeap_ptrs",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_25f03280eee84f53f1b2ad3f058d1b9b",
"refinement_interpretation_Tm_refine_4e6ff91458b7269e02c2aa8dd7d7b82a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_7d5fdc58e4fedfc5e79017f738a06ce1",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_dbe23ff6cb9d4dcade7118b84967c33e",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"typing_FStar.Map.const", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Set.empty",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs",
"typing_Vale.Interop.Heap_s.addrs_set",
"typing_Vale.Interop.down_mem_aux"
],
0,
"ba8059ee0438a4ecc60488908bd2e721"
],
[
"Vale.Interop.up_down_identity",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_3a2dd58f50cd5923bb942c80f67255f6"
],
0,
"4f61d5b636f76b58d8c3a1dae19c1592"
],
[
"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",
"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_8c41f6f180b71033245cdc7aca5395e0",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_fe084d710bd16568de37f3a949480eea",
"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,
"558eee8b32f23a9ed2f00aaa109019c9"
],
[
"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.nat", "equation_Prims.squash",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Interop.Types.b8",
"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",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"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_471cb2fea0ea32360cc49236e412f9a6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b0e983e2a97bd15fdd0ab53f8b017a6f",
"refinement_interpretation_Tm_refine_eb772802b6a72ab41a7d02f51f67a266",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"typing_FStar.Map.domain", "typing_LowStar.BufferView.Down.length",
"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__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.get_seq_heap"
],
0,
"186f22defd7774e6ccd6a3be6abbe63b"
],
[
"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_interpretation_Tm_arrow_38b481003114a2f65ff9ca6b62dd14e3",
"Vale.Interop_interpretation_Tm_arrow_992025dc489e7315d2abb53d1ad49c82",
"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_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.Seq.Properties.lseq", "equation_FStar.Set.subset",
"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.nat64", "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",
"equation_Vale.Interop.Types.addr_map",
"equation_Vale.Interop.Types.b8",
"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_Prims.list",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_b51c6477abe9001f80a2c30fadfd2dca",
"l_and-interp", "l_or-interp",
"l_quant_interp_91881cc6bc0c184b2379e012860e0f2b",
"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.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_addresses",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_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_rel",
"proj_equation_Vale.Interop.Types.Buffer_rrel",
"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_04411f4ac756e7490a64e2db9bda29b2",
"refinement_interpretation_Tm_refine_0461e75a646cbadf79d6506a42fd03fe",
"refinement_interpretation_Tm_refine_0e4cf65f7351e0808e0a2ed028012cbb",
"refinement_interpretation_Tm_refine_1369401d66ae6f83682a5955a8b9280a",
"refinement_interpretation_Tm_refine_278e0f317328f9d18906d5e312751975",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_bccbced7332638ded7edb52a93b52677",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c8d14e43ad9ba7ceb64e36ef13e09448",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_fe084d710bd16568de37f3a949480eea",
"refinement_interpretation_Tm_refine_ff9c29737b4a7ad4656cd79051ec80a3",
"refinement_interpretation_Tm_refine_ff9cf9634d9ad82e44410ccec01e1955",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Interop.Heap_s.__proj__InteropHeap__item__addrs",
"typing_FStar.Map.domain", "typing_FStar.Map.sel",
"typing_FStar.Set.intersect", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton",
"typing_LowStar.BufferView.Down.as_seq",
"typing_LowStar.BufferView.Down.length",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Tm_abs_b51c6477abe9001f80a2c30fadfd2dca",
"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__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.disjoint_addr",
"typing_Vale.Interop.Types.down_view",
"typing_Vale.Interop.Types.get_downview",
"typing_Vale.Interop.get_seq_heap"
],
0,
"a5ed095490e7ed75eb9b73cb6cd44370"
],
[
"Vale.Interop.update_buffer_up_mem",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"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.b8",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"fuel_guarded_inversion_FStar.Pervasives.dtuple4",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.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",
"proj_equation_Vale.Interop.Types.Buffer_bsrc",
"proj_equation_Vale.Interop.Types.Buffer_src",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_50d3b3dd51fb0799a5eeaaea500ed7b0",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b50f45fba9bc6f60eec05ca9dc1f94ef",
"refinement_interpretation_Tm_refine_f053bb82fde0bb5e3b79f846e507678a",
"refinement_interpretation_Tm_refine_fe084d710bd16568de37f3a949480eea",
"typing_FStar.Map.domain",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__rel",
"typing_Vale.Interop.Types.__proj__Buffer__item__rrel",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view"
],
0,
"47687925dad23968be61228e2a96960c"
],
[
"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",
"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.Types.b8", "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",
"lemma_FStar.Set.lemma_equal_elim", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_50d3b3dd51fb0799a5eeaaea500ed7b0",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_b50f45fba9bc6f60eec05ca9dc1f94ef",
"refinement_interpretation_Tm_refine_f053bb82fde0bb5e3b79f846e507678a",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"typing_FStar.Map.domain", "typing_Vale.Interop.Heap_s.addrs_set"
],
0,
"de90aad7b5331647a8dcf9d5b419e80d"
]
]
]
Computing file changes ...
