[ "Á@‹‚1)Ø”óç²°\u007f\b™²", [ [ "MerkleTree.Low.VectorExtras.move_left", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Signed", "constructor_distinct_FStar.Integers.Winfinite", "equality_tok_FStar.Integers.Winfinite@tok", "equation_FStar.Integers.int_t", "equation_FStar.Monotonic.HyperStack.live_region", "equation_FStar.Seq.Properties.cons", "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.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "function_token_typing_LowStar.Buffer.trivial_preorder", "int_inversion", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_index_upd1", "lemma_FStar.Seq.Base.lemma_index_upd2", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_upd", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.live_region_frameOf", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "refinement_interpretation_Tm_refine_162c8b43d6c2dbc3017791d986dde750", "refinement_interpretation_Tm_refine_22ea23156c96d1f95a36c1bf3ce83086", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_35df10cd1ace067f48aa7c60a3c8908e", "refinement_interpretation_Tm_refine_4dc7ca08a7c220bf0bd3201470a78510", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6821f7f5df0d6d508418864506fe2cff", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955", "refinement_interpretation_Tm_refine_91e73391b85f4d08faee201335579e8f", "refinement_interpretation_Tm_refine_93e0fac69114331fd162ac2e8da2223c", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292", "refinement_interpretation_Tm_refine_e76a622bd15aa422686bd6352332d7cc", "refinement_interpretation_Tm_refine_e99858f6530b2a363562ffe6b95e1f41", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "true_interp", "typing_FStar.Monotonic.HyperStack.live_region", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.slice", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, "56c6054f25e5d5ec408076df6235627b" ], [ "MerkleTree.Low.VectorExtras.shrink", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.lte", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lte", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "fuel_guarded_inversion_LowStar.Vector.vector_str", "int_inversion", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_48c369ef9189ad76f46548f23cb76cdf", "refinement_interpretation_Tm_refine_562ac129d341d684eac8dd463a0f41fe", "refinement_interpretation_Tm_refine_de53286ac6ea7bcb1ee55a5646706534", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.v", "typing_LowStar.Vector.as_seq", "typing_LowStar.Vector.size_of" ], 0, "8f1e7b332f64e9d9ae57f6865e22f80a" ], [ "MerkleTree.Low.VectorExtras.shrink", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.gte", "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.gte", "equation_FStar.UInt32.lte", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.Vector.as_seq", "equation_LowStar.Vector.freeable", "equation_LowStar.Vector.live", "equation_LowStar.Vector.loc_vector", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "equation_Prims.nat", "fuel_guarded_inversion_LowStar.Vector.vector_str", "function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Seq.Properties.slice_slice", "lemma_FStar.Set.lemma_equal_refl", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_LowStar.Vector.Vec_sz", "proj_equation_LowStar.Vector.Vec_vs", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_LowStar.Vector.Vec_sz", "projection_inverse_LowStar.Vector.Vec_vs", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_3396f1d518ffeb2163c25c13fcb1de13", "refinement_interpretation_Tm_refine_48c369ef9189ad76f46548f23cb76cdf", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_562ac129d341d684eac8dd463a0f41fe", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_de53286ac6ea7bcb1ee55a5646706534", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_FStar.UInt32.gte", "typing_FStar.UInt32.lte", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Vector.__proj__Vec__item__cap", "typing_LowStar.Vector.__proj__Vec__item__vs", "typing_LowStar.Vector.as_seq", "typing_LowStar.Vector.loc_vector", "typing_LowStar.Vector.size_of" ], 0, "c3d15ce242b64a6f9402a676e4c85d0d" ], [ "MerkleTree.Low.VectorExtras.flush_inplace", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "equation_FStar.UInt.fits", "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.lte", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "equation_Prims.nat", "fuel_guarded_inversion_LowStar.Vector.vector_str", "int_inversion", "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_48c369ef9189ad76f46548f23cb76cdf", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_562ac129d341d684eac8dd463a0f41fe", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.lte", "typing_FStar.UInt32.v", "typing_LowStar.Vector.as_seq", "typing_LowStar.Vector.size_of" ], 0, "7c2ecf65a274970749e847396e386b20" ], [ "MerkleTree.Low.VectorExtras.flush_inplace", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W32", "equality_tok_FStar.Integers.W32@tok", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.HyperStack.ST.is_eternal_region", "equation_FStar.Integers.int_t", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.gte", "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.gte", "equation_FStar.UInt32.lte", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.Vector.as_seq", "equation_LowStar.Vector.freeable", "equation_LowStar.Vector.live", "equation_LowStar.Vector.loc_vector", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "equation_Prims.nat", "fuel_guarded_inversion_LowStar.Vector.vector_str", "function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Seq.Properties.slice_slice", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "lemma_LowStar.Monotonic.Buffer.freeable_length", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_LowStar.Vector.Vec_vs", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_06a3dd4e4f3249107da2d0b06d97a202", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_3396f1d518ffeb2163c25c13fcb1de13", "refinement_interpretation_Tm_refine_48c369ef9189ad76f46548f23cb76cdf", "refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_562ac129d341d684eac8dd463a0f41fe", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7", "refinement_interpretation_Tm_refine_aa4b3d268075d84252df525db1f85524", "refinement_interpretation_Tm_refine_be8c4716738c2a6b0c1ee477c48f8fea", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_de53286ac6ea7bcb1ee55a5646706534", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_FStar.UInt32.gte", "typing_FStar.UInt32.lte", "typing_FStar.UInt32.sub", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.mgsub", "typing_LowStar.Vector.__proj__Vec__item__cap", "typing_LowStar.Vector.__proj__Vec__item__vs", "typing_LowStar.Vector.as_seq", "typing_LowStar.Vector.loc_vector", "typing_LowStar.Vector.size_of" ], 0, "55edcbd7a60858312f780feb5123906d" ], [ "MerkleTree.Low.VectorExtras.rv_flush_inplace", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "equation_FStar.UInt.fits", "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.lte", "equation_LowStar.RVector.rvector", "equation_LowStar.Vector.as_seq", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "equation_Prims.nat", "fuel_guarded_inversion_LowStar.Regional.regional", "fuel_guarded_inversion_LowStar.Vector.vector_str", "int_inversion", "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_48c369ef9189ad76f46548f23cb76cdf", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_562ac129d341d684eac8dd463a0f41fe", "refinement_interpretation_Tm_refine_9a4f5366055910237954d85f232cccf4", "refinement_interpretation_Tm_refine_9cc2b349cdd7d1d478708dc21464f596", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.lte", "typing_FStar.UInt32.v", "typing_LowStar.Vector.as_seq", "typing_LowStar.Vector.size_of" ], 0, "e68ddb55c6cd46b3dbc889d808a6158d" ], [ "MerkleTree.Low.VectorExtras.rv_flush_inplace", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_LowStar.RVector.as_seq_seq.fuel_instrumented", "@fuel_correspondence_LowStar.RVector.rs_loc_elems.fuel_instrumented", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Signed", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.Winfinite", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.HyperStack.ST.is_eternal_region", "equation_FStar.Integers.int_t", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.gte", "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.gte", "equation_FStar.UInt32.lt", "equation_FStar.UInt32.lte", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.RVector.as_seq", "equation_LowStar.RVector.as_seq_sub", "equation_LowStar.RVector.elems_inv", "equation_LowStar.RVector.elems_reg", "equation_LowStar.RVector.loc_all_exts_from", "equation_LowStar.RVector.loc_rvector", "equation_LowStar.RVector.rs_elems_inv", "equation_LowStar.RVector.rs_elems_reg", "equation_LowStar.RVector.rv_elems_inv", "equation_LowStar.RVector.rv_elems_reg", "equation_LowStar.RVector.rv_inv", "equation_LowStar.RVector.rv_itself_inv", "equation_LowStar.RVector.rv_loc_elems", "equation_LowStar.RVector.rvector", "equation_LowStar.Vector.as_seq", "equation_LowStar.Vector.forall2_seq", "equation_LowStar.Vector.forall_seq", "equation_LowStar.Vector.freeable", "equation_LowStar.Vector.live", "equation_LowStar.Vector.loc_vector", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "equation_Prims.nat", "fuel_guarded_inversion_LowStar.Regional.regional", "fuel_guarded_inversion_LowStar.Vector.vector_str", "function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Seq.Properties.slice_slice", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "lemma_LowStar.Monotonic.Buffer.freeable_length", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "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_disjoint_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.RVector.as_seq_seq_index", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality", "proj_equation_LowStar.Regional.Rgl_repr", "proj_equation_LowStar.Vector.Vec_vs", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_03e0ee7c990720bc4bd1c73dc60b1ac5", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0b0f9776f8fbf33608e064dfe5c8ab0a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_11497e38c5d8e72f702b88e94e7dec14", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_1ffcdb8322b4b43633596ecc5d3b4123", "refinement_interpretation_Tm_refine_3396f1d518ffeb2163c25c13fcb1de13", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_3aeabc37e86f7b566e1052127e0672d1", "refinement_interpretation_Tm_refine_4097c547095e70012031c1b6bbc9fb12", "refinement_interpretation_Tm_refine_48c369ef9189ad76f46548f23cb76cdf", "refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_562ac129d341d684eac8dd463a0f41fe", "refinement_interpretation_Tm_refine_69d1d206ddafb5a6092734ed6446bcfd", "refinement_interpretation_Tm_refine_7028972db935cf1f2ecc12fc7857552a", "refinement_interpretation_Tm_refine_709aff84c75b0fff77dcbf3b529649dd", "refinement_interpretation_Tm_refine_7108b467000c99be927e4d94496382d1", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955", "refinement_interpretation_Tm_refine_9a4f5366055910237954d85f232cccf4", "refinement_interpretation_Tm_refine_9cc2b349cdd7d1d478708dc21464f596", "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7", "refinement_interpretation_Tm_refine_aa4b3d268075d84252df525db1f85524", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_e39578da040f6c7003161732bc9d6b85", "refinement_interpretation_Tm_refine_e7d1c8d8cd03a2e78447c400f48890d3", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fa35e0feeb188fbc071035c9b4fa011e", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_FStar.Set.complement", "typing_FStar.Set.empty", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "typing_FStar.UInt32.add", "typing_FStar.UInt32.gte", "typing_FStar.UInt32.lt", "typing_FStar.UInt32.lte", "typing_FStar.UInt32.sub", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.mgsub", "typing_LowStar.RVector.as_seq_seq", "typing_LowStar.RVector.loc_all_exts_from", "typing_LowStar.RVector.loc_rvector", "typing_LowStar.RVector.rs_loc_elems", "typing_LowStar.RVector.rv_loc_elems", "typing_LowStar.Regional.__proj__Rgl__item__repr", "typing_LowStar.Vector.__proj__Vec__item__cap", "typing_LowStar.Vector.__proj__Vec__item__vs", "typing_LowStar.Vector.as_seq", "typing_LowStar.Vector.size_of" ], 0, "0d91b535364357aa484d43644bc27f55" ] ] ]