[ "i$Hx\u001c2'\u001c", [ [ "Lib.Loops.for", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0e406ebb8fe1da55578bcffeb79cfd32", "refinement_interpretation_Tm_refine_427ccb352453c408ac8eeec6c2c8abc6", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "3c8777fb4ddf378520c7ef93416aaff9" ], [ "Lib.Loops.for", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0e406ebb8fe1da55578bcffeb79cfd32", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "213a4a8bd974e9f6e765e11ceadee878" ], [ "Lib.Loops.for", 3, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2eec29014a998085381126097e78648e", "refinement_interpretation_Tm_refine_3991c03789f1c4ac05e7539fb783f0dc", "refinement_interpretation_Tm_refine_427ccb352453c408ac8eeec6c2c8abc6", "refinement_interpretation_Tm_refine_59aa1409ea4db7e5203de2a10b240063", "refinement_interpretation_Tm_refine_f0665b2c8997b993e6d25453f31a67d6" ], 0, "41704cb031ec5356b3b8d897e8a3194d" ], [ "Lib.Loops.while", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_b16bf82b210653a34e4d7322fab91ffb" ], 0, "783c3ba8e7ba7ac629f920abb40dd2b8" ], [ "Lib.Loops.while", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_b16bf82b210653a34e4d7322fab91ffb" ], 0, "17c7d0f4d8023851fd1ece203c5d3789" ], [ "Lib.Loops.while", 3, 2, 1, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "function_token_typing_FStar.Monotonic.Heap.heap", "lemma_FStar.Map.lemma_ContainsDom", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_1bbd46b74c3d9d07e864ebebad14e47a", "refinement_interpretation_Tm_refine_2f71079aa0f268146f579ff4fe1cb716", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, "85a0e18d6a972cc4bcf6ba7cc7c1bcb7" ], [ "Lib.Loops.square_while", 1, 3, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.index.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.index.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Prims.Cons", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Nil@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.List.Tot.Base.hd", "equation_FStar.List.Tot.Base.tail", "equation_FStar.List.Tot.Base.tl", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_FStar.UInt.fits", "equation_FStar.UInt.lt", "equation_FStar.UInt.lte", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lt", "equation_FStar.UInt32.lte", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.size_t", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_with_fuel_FStar.List.Tot.Base.index.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_LowStar.Buffer.trivial_preorder", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "l_quant_interp_0d9bb479f8271a840b8a90a91aae9589", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Seq.Base.lemma_index_upd1", "lemma_FStar.Seq.Base.lemma_index_upd2", "lemma_FStar.Seq.Properties.lemma_seq_of_list_index", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "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", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_1b7393edf6a326b056dc89c5ff048e3f", "refinement_interpretation_Tm_refine_1ccfb21903aa30ace8832f7a4d067d9b", "refinement_interpretation_Tm_refine_29898ed1155f0017708e2ee870672a4b", "refinement_interpretation_Tm_refine_2d1e28ad8243ff0e836787677e62938b", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_75fb2e5ec7aa5205a84dd3e250de5c1d", "refinement_interpretation_Tm_refine_bf2fa1226f2c9a0f6671df3e80ddcb8e", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_interpretation_Tm_refine_c86aba5c6243e6b7f9a4b0ad41b4e9a0", "refinement_interpretation_Tm_refine_ccf9379f40d74db228b80a1b0a1035ad", "refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292", "refinement_interpretation_Tm_refine_ee8b234aa6cf07c6ef04345829148435", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f702079de7625457cbeca1b8dfcb175d", "refinement_interpretation_Tm_refine_fd3cc4075b582bc7a69e61c266c3cb03", "refinement_interpretation_Tm_refine_fec760cc08225eeaaed79ec2772ac402", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "true_interp", "typing_FStar.List.Tot.Base.index", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_rid_ctr", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Seq.Properties.seq_of_list", "typing_FStar.Set.complement", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "typing_FStar.UInt32.lt", "typing_FStar.UInt32.lte", "typing_FStar.UInt32.mul", "typing_FStar.UInt32.t", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.get", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, "a3fd8e3500b493e2617b46e8ce070ce7" ] ] ]