diff options
Diffstat (limited to 'ulib/.cache/LowStar.Monotonic.Buffer.fst.hints')
| -rw-r--r-- | ulib/.cache/LowStar.Monotonic.Buffer.fst.hints | 300 |
1 files changed, 237 insertions, 63 deletions
diff --git a/ulib/.cache/LowStar.Monotonic.Buffer.fst.hints b/ulib/.cache/LowStar.Monotonic.Buffer.fst.hints index c119afd..c0f54d6 100644 --- a/ulib/.cache/LowStar.Monotonic.Buffer.fst.hints +++ b/ulib/.cache/LowStar.Monotonic.Buffer.fst.hints @@ -1,5 +1,5 @@ [ - "}æ¼ás…\u0017×\u0018\u000e„µ•\f©ô", + "¿WðÆ\\nth\u001fû! Ãù¶Ö", [ [ "LowStar.Monotonic.Buffer.compatible_subseq_preorder", @@ -7597,6 +7597,53 @@ "a7faf525f3579dbe83db7eb345509968" ], [ + "LowStar.Monotonic.Buffer.region_lifetime_sub", + 1, + 2, + 1, + [ + "@MaxIFuel_assumption", "@query", + "FStar.UInt32_pretyping_041e3a67a2d2b51fd702f1f88cfc3b44", "b2t_def", + "constructor_distinct_LowStar.Monotonic.Buffer.Buffer", + "disc_equation_LowStar.Monotonic.Buffer.Buffer", + "disc_equation_LowStar.Monotonic.Buffer.Null", + "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", + "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", + "equation_LowStar.Monotonic.Buffer.buffer_compatible", + "equation_LowStar.Monotonic.Buffer.compatible_sub_preorder", + "equation_LowStar.Monotonic.Buffer.g_is_null", + "equation_LowStar.Monotonic.Buffer.mgsub", + "equation_LowStar.Monotonic.Buffer.region_lifetime_buf", + "equation_LowStar.Monotonic.Buffer.srel_to_lsrel", + "equation_Prims.nat", + "fuel_guarded_inversion_LowStar.Monotonic.Buffer.mbuffer", + "function_token_typing_FStar.UInt32.t", "int_inversion", + "int_typing", "lemma_FStar.Ghost.reveal_hide", + "lemma_LowStar.Monotonic.Buffer.frameOf_gsub", + "lemma_LowStar.Monotonic.Buffer.gsub_is_null", + "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", + "primitive_Prims.op_LessThanOrEqual", + "proj_equation_LowStar.Monotonic.Buffer.Buffer_content", + "proj_equation_LowStar.Monotonic.Buffer.Buffer_max_length", + "projection_inverse_BoxBool_proj_0", + "projection_inverse_BoxInt_proj_0", + "projection_inverse_LowStar.Monotonic.Buffer.Buffer_a", + "projection_inverse_LowStar.Monotonic.Buffer.Buffer_content", + "projection_inverse_LowStar.Monotonic.Buffer.Buffer_idx", + "projection_inverse_LowStar.Monotonic.Buffer.Buffer_length", + "projection_inverse_LowStar.Monotonic.Buffer.Buffer_max_length", + "projection_inverse_LowStar.Monotonic.Buffer.Buffer_rel", + "projection_inverse_LowStar.Monotonic.Buffer.Buffer_rrel", + "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", + "refinement_interpretation_Tm_refine_bdfec0f0dbe3345f1b7560a60ccfdd90", + "refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795", + "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", + "typing_FStar.UInt32.v" + ], + 0, + "14cc0cd4a9745910ffa6c06d7edae78c" + ], + [ "LowStar.Monotonic.Buffer.recallable_null", 1, 2, @@ -7609,7 +7656,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "dd60590f8727f81e67316f78c748a837" + "91b1bcd5d57f85387e591dcf0302438c" ], [ "LowStar.Monotonic.Buffer.recallable_mgsub", @@ -7624,7 +7671,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "5c9dbed963dbccfc65794cb5c980368b" + "42d59a6cc127c883ca10681ab3d6f5c6" ], [ "LowStar.Monotonic.Buffer.recallable_mgsub", @@ -7685,7 +7732,7 @@ "typing_LowStar.Monotonic.Buffer.srel_to_lsrel" ], 0, - "4ed6d1232019d902d1394b1bdbbe9299" + "00de36e1154e60257ab6733241fb7802" ], [ "LowStar.Monotonic.Buffer.recall", @@ -7740,7 +7787,7 @@ "typing_LowStar.Monotonic.Buffer.frameOf" ], 0, - "b9e0a7947de8a2035c879f713a436bc8" + "0de96820358549ec93dfc9f6f5b7243f" ], [ "LowStar.Monotonic.Buffer.witnessed", @@ -7763,7 +7810,7 @@ "typing_FStar.UInt32.v" ], 0, - "78536134fb78ffa7884484fe44b52138" + "3fa505b51ee91eacc42bcf3dc570780f" ], [ "LowStar.Monotonic.Buffer.lemma_stable_on_rel_is_stable_on_rrel", @@ -7814,7 +7861,7 @@ "typing_LowStar.Monotonic.Buffer.uu___is_Buffer" ], 0, - "28d5a903c81deb584edd6088dcd76e09" + "73ba5c4062d68a76381bb63969a1a799" ], [ "LowStar.Monotonic.Buffer.witness_p", @@ -7871,7 +7918,7 @@ "typing_LowStar.Monotonic.Buffer.as_seq", "unit_typing" ], 0, - "ee2ac028da91660ccd7bf79c1c54596f" + "0dbb1b64f40b26cb7bcd53cd7e01a9ed" ], [ "LowStar.Monotonic.Buffer.recall_p", @@ -7925,7 +7972,7 @@ "typing_FStar.UInt32.v" ], 0, - "f25caf1f8c52bdd2606725759fa10011" + "536e9a96038bfe2e0259430466e0ffe0" ], [ "LowStar.Monotonic.Buffer.witnessed_functorial", @@ -7934,7 +7981,7 @@ 1, [ "@query" ], 0, - "2f791ad4625a7f07ecf13b201b601fe0" + "6dd3f52cdf0dbc5d778c7e0a5ec100d0" ], [ "LowStar.Monotonic.Buffer.witnessed_functorial", @@ -7996,7 +8043,7 @@ "typing_LowStar.Monotonic.Buffer.length" ], 0, - "b48a05e5f6ce93cf501801dc8e2e9cc7" + "ebbcccf97fad38f8c1c37e5f4c5379c6" ], [ "LowStar.Monotonic.Buffer.witnessed_functorial_st", @@ -8005,7 +8052,7 @@ 1, [ "@query" ], 0, - "652b145c4a34b20ca9fa28af6c538a1d" + "67bdb199d01479b656d69eb7a19c65dd" ], [ "LowStar.Monotonic.Buffer.witnessed_functorial_st", @@ -8078,7 +8125,7 @@ "typing_LowStar.Monotonic.Buffer.uu___is_Null" ], 0, - "ff6fa1d1b1b47aed005b88a7ee84cabb" + "86ada5854ed7c0ef5ecef47e527debd1" ], [ "LowStar.Monotonic.Buffer.freeable", @@ -8100,7 +8147,7 @@ "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87" ], 0, - "56715e5eb384cffc450bf7eb7e391a70" + "95a1bc15a281b6dd14322fcbb6ac6845" ], [ "LowStar.Monotonic.Buffer.free", @@ -8173,7 +8220,7 @@ "typing_LowStar.Monotonic.Buffer.frameOf" ], 0, - "4ae33842c8f4757739c93756d0a8598c" + "a075837532d775d5ad47ac69309bec18" ], [ "LowStar.Monotonic.Buffer.freeable_length", @@ -8192,7 +8239,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "068d5f95b4e34d7b790f75ca537f1cbb" + "6857e45c28790dbfe853b6c029822414" ], [ "LowStar.Monotonic.Buffer.freeable_disjoint", @@ -8206,7 +8253,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "dba66e957ff420e68270f0074f04c724" + "22e44cda580a1af78901f87abb4eab5a" ], [ "LowStar.Monotonic.Buffer.freeable_disjoint", @@ -8294,7 +8341,7 @@ "typing_LowStar.Monotonic.Buffer.ubuffer___409" ], 0, - "94ed19e4678e9969e7af9a38bd345f65" + "17b28e19ea961764d074ad5a74e6ac2c" ], [ "LowStar.Monotonic.Buffer.freeable_disjoint'", @@ -8324,7 +8371,7 @@ "typing_LowStar.Monotonic.Buffer.frameOf" ], 0, - "10fce1e291b03a2423711906b21a96f7" + "0dc2c37e94bdd38af47712d2f3f829b8" ], [ "LowStar.Monotonic.Buffer.alloc_heap_common", @@ -8454,7 +8501,7 @@ "typing_LowStar.Monotonic.Buffer.srel_to_lsrel", "unit_typing" ], 0, - "654d3f82eff117316031204f68e503b9" + "2db2d55285fbbd7514d3b85e5cf6b30d" ], [ "LowStar.Monotonic.Buffer.alloc_heap_common", @@ -8574,7 +8621,7 @@ "typing_LowStar.Monotonic.Buffer.srel_to_lsrel", "unit_typing" ], 0, - "ba16904d5c2eaf0441a9e2ced4acf9bd" + "4f831f3da69861fea4ce680de16a84c6" ], [ "LowStar.Monotonic.Buffer.mgcmalloc", @@ -8588,7 +8635,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "1ae4a45d498319349b0766a0812deb17" + "0ed51e5696602629f9760ab80bbe7ed4" ], [ "LowStar.Monotonic.Buffer.mgcmalloc", @@ -8611,7 +8658,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "0d16e46647360ca12e1bb36c9fbece49" + "5d2872380d7d9fa3f01e9ee7c00ea81d" ], [ "LowStar.Monotonic.Buffer.read_sub_buffer", @@ -8677,7 +8724,7 @@ "typing_LowStar.Monotonic.Buffer.len", "unit_typing" ], 0, - "4e16c48ef32f486c16238716ea8058fc" + "a3dd3f470ac6604a52439461d0a5f125" ], [ "LowStar.Monotonic.Buffer.mgcmalloc_and_blit", @@ -8698,7 +8745,7 @@ "typing_FStar.UInt32.v" ], 0, - "53a78f7eec71e52f447d081c172e03fe" + "424398aabd0964003eaa2594554282bc" ], [ "LowStar.Monotonic.Buffer.mgcmalloc_and_blit", @@ -8742,7 +8789,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "d5e5777c5720d18b658e4b58f28cea45" + "8003fa1f553c05cb043e010698843e4c" ], [ "LowStar.Monotonic.Buffer.mgcmalloc_partial", @@ -8758,7 +8805,7 @@ "refinement_interpretation_Tm_refine_5b0eb244f918e6c8215083b2d9842d7b" ], 0, - "af6d304c774b15dd39055b2047c267e5" + "e55a7039f3d79a04946f1ce496ce0093" ], [ "LowStar.Monotonic.Buffer.mmalloc", @@ -8772,7 +8819,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "bedeff0e0dc1ac0ac61d668196c09427" + "cb70755b1c223f57f155ced5a75ec924" ], [ "LowStar.Monotonic.Buffer.mmalloc", @@ -8811,7 +8858,7 @@ "typing_LowStar.Monotonic.Buffer.len", "unit_typing" ], 0, - "13bd0ac045fc5adf6336f9e1e2c9a591" + "d6f9b35fb11602183e409aad25493f4d" ], [ "LowStar.Monotonic.Buffer.mmalloc_and_blit", @@ -8832,7 +8879,7 @@ "typing_FStar.UInt32.v" ], 0, - "96d34459b0e760dc88a47b62f2bdfad0" + "2c7e1f2148f5526f9214e227fe8b1def" ], [ "LowStar.Monotonic.Buffer.mmalloc_and_blit", @@ -8891,7 +8938,7 @@ "typing_LowStar.Monotonic.Buffer.len", "unit_typing" ], 0, - "f59d4b76f862f3c90d068bea357e8ad9" + "eac2b3bd454ad7e2060620a7fceb308e" ], [ "LowStar.Monotonic.Buffer.mmalloc_partial", @@ -8907,7 +8954,7 @@ "refinement_interpretation_Tm_refine_a6cf5e5c36c8ad78f0926c7c77a31f31" ], 0, - "1a546b4071fefea40e92e3db2053c683" + "59fea9194f58eff28543bc9633393176" ], [ "LowStar.Monotonic.Buffer.malloca", @@ -8925,7 +8972,7 @@ "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d" ], 0, - "bac7828372a749e651ebf1de99b01081" + "a2260206eab39d4692c6252445d0d65a" ], [ "LowStar.Monotonic.Buffer.malloca", @@ -9024,7 +9071,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "9ef16dcc19b6f8742c2601fa55284747" + "f9036a4fc20984787a95e334734a6f28" ], [ "LowStar.Monotonic.Buffer.malloca_and_blit", @@ -9047,7 +9094,7 @@ "typing_FStar.UInt32.v" ], 0, - "dfbd7aa79f311b2faea96b62cc9e59ef" + "2091c84503045909028618286aaf268c" ], [ "LowStar.Monotonic.Buffer.malloca_and_blit", @@ -9143,7 +9190,7 @@ "typing_FStar.UInt32.v", "typing_LowStar.Monotonic.Buffer.as_seq" ], 0, - "d530e505d6d682aca328b6321c49fade" + "a102ba7bd8c1bf31b7970070b94cb512" ], [ "LowStar.Monotonic.Buffer.malloca_of_list", @@ -9256,7 +9303,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "51f9f9df4b7064479328fbd28bff8817" + "02d3f13328f7b734e6b039a8f69714e2" ], [ "LowStar.Monotonic.Buffer.mgcmalloc_of_list", @@ -9368,7 +9415,7 @@ "typing_FStar.UInt.fits", "typing_FStar.UInt.max_int" ], 0, - "1ec6f793381995f2a5cad02f19320fcc" + "2fc41c93bbc50281c343dfbf2fd07750" ], [ "LowStar.Monotonic.Buffer.mgcmalloc_of_list_partial", @@ -9380,7 +9427,7 @@ "refinement_interpretation_Tm_refine_a6118af488767f45ce918c6f829632fa" ], 0, - "dc758d975e0cc39ea28ccc080260fa7f" + "bb8132bccb2596a011c31db7d4e3786a" ], [ "LowStar.Monotonic.Buffer.mmalloc_drgn", @@ -9394,7 +9441,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "90758b804c556bb31817232739e8030b" + "8dd965e03f21e1af6493d02911fa3334" ], [ "LowStar.Monotonic.Buffer.mmalloc_drgn", @@ -9501,7 +9548,7 @@ "typing_LowStar.Monotonic.Buffer.region_liveness_insensitive_locs" ], 0, - "8a64a89a7b551bdb0edf8ac86a847417" + "477509a55857cb8b4d4247b7af1c5136" ], [ "LowStar.Monotonic.Buffer.mmalloc_drgn_mm", @@ -9515,7 +9562,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "a076c2c7374f48784244d3500a7e885d" + "cedbbcbeb6ca970e150a0721a5d4fd74" ], [ "LowStar.Monotonic.Buffer.mmalloc_drgn_mm", @@ -9623,7 +9670,134 @@ "typing_LowStar.Monotonic.Buffer.region_liveness_insensitive_locs" ], 0, - "8e58664c7c9977bcfa0039f57aeadab2" + "03ad401f9a74911cd2d68495e992346b" + ], + [ + "LowStar.Monotonic.Buffer.mmalloc_drgn_and_blit", + 1, + 2, + 1, + [ + "@MaxIFuel_assumption", "@query", "b2t_def", + "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", + "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", + "int_inversion", "lemma_LowStar.Monotonic.Buffer.length_as_seq", + "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", + "primitive_Prims.op_LessThanOrEqual", + "projection_inverse_BoxBool_proj_0", + "projection_inverse_BoxInt_proj_0", + "refinement_interpretation_Tm_refine_75cc1b5adf98f48abab623cab9117c3d", + "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", + "typing_FStar.UInt32.v" + ], + 0, + "670fcf4a3c97b3b7d28fc23460598336" + ], + [ + "LowStar.Monotonic.Buffer.mmalloc_drgn_and_blit", + 2, + 2, + 1, + [ + "@MaxIFuel_assumption", "@query", + "FStar.UInt32_pretyping_041e3a67a2d2b51fd702f1f88cfc3b44", "b2t_def", + "bool_inversion", "bool_typing", + "constructor_distinct_LowStar.Monotonic.Buffer.Buffer", + "disc_equation_LowStar.Monotonic.Buffer.Null", + "equation_FStar.HyperStack.ST.d_hrid", + "equation_FStar.HyperStack.ST.equal_stack_domains", + "equation_FStar.HyperStack.ST.is_freeable_heap_region", + "equation_FStar.HyperStack.ST.mreference", + "equation_FStar.HyperStack.ST.ralloc_post", + "equation_FStar.Monotonic.HyperHeap.hmap", + "equation_FStar.Monotonic.HyperStack.contains", + "equation_FStar.Monotonic.HyperStack.is_heap_color", + "equation_FStar.Monotonic.HyperStack.is_mm", + "equation_FStar.Monotonic.HyperStack.live_region", + "equation_FStar.Monotonic.HyperStack.mem", + "equation_FStar.Monotonic.HyperStack.sel", + "equation_FStar.Monotonic.HyperStack.unused_in", + "equation_FStar.Monotonic.HyperStack.upd", + "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.Monotonic.Buffer.as_seq", + "equation_LowStar.Monotonic.Buffer.buffer_compatible", + "equation_LowStar.Monotonic.Buffer.frameOf", + "equation_LowStar.Monotonic.Buffer.g_is_null", + "equation_LowStar.Monotonic.Buffer.len", + "equation_LowStar.Monotonic.Buffer.length", + "equation_LowStar.Monotonic.Buffer.live", + "equation_LowStar.Monotonic.Buffer.loc", + "equation_LowStar.Monotonic.Buffer.loc_none", + "equation_LowStar.Monotonic.Buffer.region_lifetime_buf", + "equation_LowStar.Monotonic.Buffer.region_liveness_insensitive_locs", + "equation_LowStar.Monotonic.Buffer.srel_to_lsrel", + "equation_LowStar.Monotonic.Buffer.unused_in", "equation_Prims.nat", + "fuel_guarded_inversion_LowStar.Monotonic.Buffer.mbuffer", + "function_token_typing_FStar.Monotonic.Heap.heap", + "function_token_typing_FStar.UInt32.t", "int_inversion", + "int_typing", "l_and-interp", "lemma_FStar.Ghost.reveal_hide", + "lemma_FStar.Map.lemma_ContainsDom", + "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelUpd1", + "lemma_FStar.Monotonic.Heap.lemma_sel_upd1", + "lemma_FStar.Monotonic.Heap.lemma_upd_contains", + "lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors", + "lemma_FStar.Seq.Base.lemma_len_slice", + "lemma_FStar.Seq.Properties.slice_length", + "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.UInt32.vu_inv", + "lemma_LowStar.Monotonic.Buffer.length_as_seq", + "lemma_LowStar.Monotonic.Buffer.length_null_2", + "lemma_LowStar.Monotonic.Buffer.live_region_frameOf", + "lemma_LowStar.Monotonic.Buffer.loc_includes_none", + "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_region_mreference_weak", + "lemma_LowStar.Monotonic.Buffer.modifies_ralloc_post", + "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", + "primitive_Prims.op_BarBar", "primitive_Prims.op_LessThanOrEqual", + "primitive_Prims.op_Subtraction", + "proj_equation_LowStar.Monotonic.Buffer.Buffer_content", + "proj_equation_LowStar.Monotonic.Buffer.Buffer_max_length", + "projection_inverse_BoxBool_proj_0", + "projection_inverse_BoxInt_proj_0", + "projection_inverse_LowStar.Monotonic.Buffer.Buffer_a", + "projection_inverse_LowStar.Monotonic.Buffer.Buffer_content", + "projection_inverse_LowStar.Monotonic.Buffer.Buffer_idx", + "projection_inverse_LowStar.Monotonic.Buffer.Buffer_length", + "projection_inverse_LowStar.Monotonic.Buffer.Buffer_max_length", + "projection_inverse_LowStar.Monotonic.Buffer.Buffer_rel", + "projection_inverse_LowStar.Monotonic.Buffer.Buffer_rrel", + "refinement_interpretation_Tm_refine_003cbb363565c5358e7ed8a8d7dba6d4", + "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", + "refinement_interpretation_Tm_refine_2c7ecebd8a41d0890aab4251b61d6458", + "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", + "refinement_interpretation_Tm_refine_75cc1b5adf98f48abab623cab9117c3d", + "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", + "refinement_interpretation_Tm_refine_a6918a83312e51579e26340a47646253", + "refinement_interpretation_Tm_refine_e8c39d6ee903737b62bc3fc299bf243a", + "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", + "typing_FStar.HyperStack.ST.rid_of_drgn", "typing_FStar.Map.domain", + "typing_FStar.Map.sel", "typing_FStar.Map.upd", + "typing_FStar.Monotonic.Heap.contains", + "typing_FStar.Monotonic.Heap.unused_in", + "typing_FStar.Monotonic.Heap.upd", + "typing_FStar.Monotonic.HyperHeap.color", + "typing_FStar.Monotonic.HyperHeap.rid", + "typing_FStar.Monotonic.HyperStack.as_ref", + "typing_FStar.Monotonic.HyperStack.contains", + "typing_FStar.Monotonic.HyperStack.get_hmap", + "typing_FStar.Monotonic.HyperStack.get_rid_ctr", + "typing_FStar.Monotonic.HyperStack.get_tip", + "typing_FStar.Monotonic.HyperStack.is_heap_color", + "typing_FStar.Monotonic.HyperStack.is_mm", + "typing_FStar.Monotonic.HyperStack.live_region", + "typing_FStar.StrongExcludedMiddle.strong_excluded_middle", + "typing_FStar.UInt32.v", "typing_LowStar.Monotonic.Buffer.as_seq", + "typing_LowStar.Monotonic.Buffer.frameOf", + "typing_LowStar.Monotonic.Buffer.loc_none", + "typing_LowStar.Monotonic.Buffer.region_liveness_insensitive_locs" + ], + 0, + "b81f9e83d1ba8017207ccef7a1ba668f" ], [ "LowStar.Monotonic.Buffer.blit", @@ -9674,7 +9848,7 @@ "typing_LowStar.Monotonic.Buffer.length" ], 0, - "cac28a06e68130c5248527f15fd1089f" + "6481c88fcb2b5f198b01c12f0c0220ea" ], [ "LowStar.Monotonic.Buffer.blit", @@ -9823,7 +9997,7 @@ "unit_typing" ], 0, - "395c6b0e346badcce804a5e0be163a74" + "b7e3ef0fe671e5cf03430dcd3b21c6d8" ], [ "LowStar.Monotonic.Buffer.fill'", @@ -9963,7 +10137,7 @@ "unit_inversion", "unit_typing" ], 0, - "60bc0b4880f64b76c384c6f4641c07d6" + "b17bb1ae4cb22e07ff691c3f27b53927" ], [ "LowStar.Monotonic.Buffer.fill", @@ -9989,7 +10163,7 @@ "typing_FStar.UInt32.v", "typing_LowStar.Monotonic.Buffer.frameOf" ], 0, - "827e3873c2bbc04dada72fac00b2ec0e" + "f1d9479838e28bf76b2d37e4a61f4549" ], [ "LowStar.Monotonic.Buffer.fill", @@ -10025,7 +10199,7 @@ "typing_LowStar.Monotonic.Buffer.length" ], 0, - "6cab2e1f9638faf99077612539e08a0c" + "2d7797638f63b227647f74fdbe4721d0" ], [ "LowStar.Monotonic.Buffer.coerce", @@ -10037,7 +10211,7 @@ "refinement_interpretation_Tm_refine_de9aeb070296eed20d879692d0254af0" ], 0, - "f195e1ba302d768fcee8c3532c0c088d" + "11b8635da165d2218758eea46e415ba5" ], [ "LowStar.Monotonic.Buffer.cloc_cls", @@ -10046,7 +10220,7 @@ 1, [ "@query" ], 0, - "07bb710abc8443c281a9788adca35d32" + "dbbf98641b4de35491227751f9e72a62" ], [ "LowStar.Monotonic.Buffer.cloc_of_loc", @@ -10064,7 +10238,7 @@ "typing_LowStar.Monotonic.Buffer.cls" ], 0, - "f7b6941cfe6c54f830cc4ae55c7459ee" + "f4fd44ba5f671453ce8fb6bc325e0718" ], [ "LowStar.Monotonic.Buffer.loc_of_cloc", @@ -10082,7 +10256,7 @@ "typing_LowStar.Monotonic.Buffer.cls" ], 0, - "8f943a00bba9bdb17dbeda0374895229" + "08db922636bb64883f7a95984f4e6d4e" ], [ "LowStar.Monotonic.Buffer.loc_of_cloc_of_loc", @@ -10096,7 +10270,7 @@ "equation_LowStar.Monotonic.Buffer.loc_of_cloc" ], 0, - "1e7a2efb651ee8ec297aa959b22ed86c" + "7cfe1c4d4ee3216977d5c79367136e75" ], [ "LowStar.Monotonic.Buffer.cloc_of_loc_of_cloc", @@ -10110,7 +10284,7 @@ "equation_LowStar.Monotonic.Buffer.loc_of_cloc" ], 0, - "e57d3211b3e6b1f2e27b05a8fd889761" + "b1116df36f68fdc67a1401ec7557cdad" ], [ "LowStar.Monotonic.Buffer.cloc_of_loc_none", @@ -10130,7 +10304,7 @@ "typing_LowStar.Monotonic.Buffer.cloc_cls" ], 0, - "d696da44bc64e8998bf08418012d3a11" + "58b122253fa7dafb58968c35ec9ea7d3" ], [ "LowStar.Monotonic.Buffer.cloc_of_loc_union", @@ -10150,7 +10324,7 @@ "typing_LowStar.Monotonic.Buffer.cloc_cls" ], 0, - "2e5581b4990d9d3f952bb60ef056e864" + "a229d9cccbc9385ed47fc6305ca0718c" ], [ "LowStar.Monotonic.Buffer.cloc_of_loc_addresses", @@ -10164,7 +10338,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "937489461bba602f848fb09ab8f03d89" + "94d34f294d61917ddf34f17efd5037c0" ], [ "LowStar.Monotonic.Buffer.cloc_of_loc_addresses", @@ -10178,7 +10352,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "bc083669cd75161b921ab251775b01d0" + "096881568779ccc494658b6c2fdc10d5" ], [ "LowStar.Monotonic.Buffer.cloc_of_loc_addresses", @@ -10198,7 +10372,7 @@ "typing_LowStar.Monotonic.Buffer.cloc_cls" ], 0, - "54968dbbfb0f4c3a505aa3a5e01cb69c" + "02060c451849d3b29392a74f27a43bb7" ], [ "LowStar.Monotonic.Buffer.cloc_of_loc_regions", @@ -10218,7 +10392,7 @@ "typing_LowStar.Monotonic.Buffer.cloc_cls" ], 0, - "9ddab3594fe9d4aae6c5136bf6b28dd5" + "83890f26ab335964b99b8585eee5c604" ], [ "LowStar.Monotonic.Buffer.loc_includes_to_cloc", @@ -10238,7 +10412,7 @@ "typing_LowStar.Monotonic.Buffer.cloc_cls" ], 0, - "ac0e249e2c25ea2a519d53d3d16717db" + "69699f1b36dd6ffe50c8e5f7fbe484ef" ], [ "LowStar.Monotonic.Buffer.loc_disjoint_to_cloc", @@ -10258,7 +10432,7 @@ "typing_LowStar.Monotonic.Buffer.cloc_cls" ], 0, - "0fc5178781a003b35aa10a6dab39ff3b" + "ad13b69e57274164895d680310ec9d16" ], [ "LowStar.Monotonic.Buffer.modifies_to_cloc", @@ -10278,7 +10452,7 @@ "typing_LowStar.Monotonic.Buffer.cloc_cls" ], 0, - "a72983e37fe50cc6074a3c895769d8df" + "7f7d11e790f5c2c0584b7c23f3c50df6" ] ] ]
\ No newline at end of file |