[ "§\u0014XÇmâ‰Ðý%;)g uA", [ [ "MerkleTree.Low.Datastructures.hash_dummy", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.trivial_preorder", "function_token_typing_Lib.IntTypes.uint8", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.mnull" ], 0, "9a74f281de617996741ebe27c1237a9a" ], [ "MerkleTree.Low.Datastructures.hash_r_inv_reg", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_r_inv", "equation_MerkleTree.Low.Datastructures.hash_region_of", "function_token_typing_Lib.IntTypes.uint8", "lemma_LowStar.Monotonic.Buffer.live_region_frameOf", "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc", "typing_LowStar.Buffer.trivial_preorder" ], 0, "afc9013cbc930c7b4bc218c5c966b2c7" ], [ "MerkleTree.Low.Datastructures.hash_repr", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.gt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gt", "equation_MerkleTree.Low.Datastructures.hash_size_t", "int_typing", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec" ], 0, "463d6262aaa42ea11d211e2889d061b9" ], [ "MerkleTree.Low.Datastructures.hash_r_repr", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_r_inv", "function_token_typing_Lib.IntTypes.uint8", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "refinement_interpretation_Tm_refine_44548e614c5097c67290ae1b7ed38ae2", "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc", "typing_LowStar.Buffer.trivial_preorder" ], 0, "9809e21b9d00546905071427e9ea9383" ], [ "MerkleTree.Low.Datastructures.hash_r_sep", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.l_and", "equation_Prims.squash", "l_and-interp", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "40fb87a0481223f529fbf7e158aa83f5" ], [ "MerkleTree.Low.Datastructures.hash_r_sep", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion", "bool_typing", "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", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_r_inv", "equation_MerkleTree.Low.Datastructures.hash_r_repr", "equation_MerkleTree.Low.Datastructures.hash_region_of", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint8", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.subset_mem", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer", "primitive_Prims.op_Equality", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_MerkleTree.Low.Datastructures.hash_region_of" ], 0, "1b9a1e4dd91acea9c0db095ad920b9a5" ], [ "MerkleTree.Low.Datastructures.hash_irepr", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "lemma_FStar.Seq.Base.lemma_create_len", "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_02de1ca607024051b572624909ff5c56", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_64007e4a8c187c3787ce4f8705e9db35", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "3d8f78ac5776bb8661ebf98f3525968c" ], [ "MerkleTree.Low.Datastructures.hash_r_alloc", 1, 0, 0, [ "@query" ], 0, "1489969cae8e8e227129db7663fffe60" ], [ "MerkleTree.Low.Datastructures.hash_r_alloc", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.HyperStack.ST.erid", "equation_FStar.HyperStack.ST.is_eternal_region", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_heap_color", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.gt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gt", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.length", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_irepr", "equation_MerkleTree.Low.Datastructures.hash_r_alloc_p", "equation_MerkleTree.Low.Datastructures.hash_r_inv", "equation_MerkleTree.Low.Datastructures.hash_r_repr", "equation_MerkleTree.Low.Datastructures.hash_region_of", "equation_MerkleTree.Low.Datastructures.hash_repr", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing", "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_subset", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_44548e614c5097c67290ae1b7ed38ae2", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909", "refinement_interpretation_Tm_refine_5b03403a8d3fa4c655ec2b3c1e1359f8", "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc", "refinement_interpretation_Tm_refine_bc562ec116ca1fbdfe61157777df7cfa", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f812e4c8adc728ad9229afa07596fb23", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "true_interp", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.color", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.is_heap_color", "typing_FStar.Set.singleton", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.bits", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_unused_in", "typing_MerkleTree.Low.Datastructures.hash_r_repr", "typing_MerkleTree.Low.Datastructures.hash_repr", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "bb1c8b6f3148c2ccd2943e89645dbece" ], [ "MerkleTree.Low.Datastructures.hash_r_free", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion", "bool_typing", "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", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_r_inv", "equation_MerkleTree.Low.Datastructures.hash_region_of", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Set.mem_subset", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_addresses_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_007c3c80423debe26b11640cdf4d4e1f", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_8c0551b61a036b536158e72eb516544e", "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc", "refinement_kinding_Tm_refine_02de1ca607024051b572624909ff5c56", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.Ghost.reveal", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Set.singleton", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_MerkleTree.Low.Datastructures.hash_region_of" ], 0, "a08b69dd84d8ca651711aa121ac8c3e2" ], [ "MerkleTree.Low.Datastructures.hreg", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_MerkleTree.Low.Datastructures.hash_r_alloc_p", "refinement_interpretation_Tm_refine_425abd470ae75ea2fff9584e9122c94a", "true_interp" ], 0, "fd35a7dd3f3759e49958832942ae6731" ], [ "MerkleTree.Low.Datastructures.hash_copy", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_529fc5d835e99e9966347c4a5e502ac8" ], 0, "d7bddedd8fe7d3aa7ef20f4039a43db8" ], [ "MerkleTree.Low.Datastructures.hash_copy", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion", "bool_typing", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Monotonic.HyperHeap.disjoint", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.length", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_r_inv", "equation_MerkleTree.Low.Datastructures.hash_r_repr", "equation_MerkleTree.Low.Datastructures.hash_region_of", "equation_MerkleTree.Low.Datastructures.hash_repr", "equation_MerkleTree.New.High.hash", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_LowStar.Buffer.trivial_preorder", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Set.mem_subset", "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.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_29c27ac7c716b2238749315b70c9eca3", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_44548e614c5097c67290ae1b7ed38ae2", "refinement_interpretation_Tm_refine_529fc5d835e99e9966347c4a5e502ac8", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc", "refinement_interpretation_Tm_refine_e8212fc9d858ebf7ca7dfe61cb30d15a", "refinement_interpretation_Tm_refine_f812e4c8adc728ad9229afa07596fb23", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "true_interp", "typing_FStar.Monotonic.HyperHeap.disjoint", "typing_FStar.Monotonic.HyperHeap.includes", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Set.singleton", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_MerkleTree.Low.Datastructures.hash_r_repr", "typing_MerkleTree.Low.Datastructures.hash_region_of" ], 0, "a7430c6fc4b280cc6c030405496c7bc1" ], [ "MerkleTree.Low.Datastructures.hcpy", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_LowStar.Regional.rg_inv", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hreg", "function_token_typing_MerkleTree.Low.Datastructures.hash_r_inv", "function_token_typing_MerkleTree.Low.Datastructures.hash_r_repr", "proj_equation_LowStar.Regional.Rgl_r_inv", "proj_equation_LowStar.Regional.Rgl_r_repr", "proj_equation_LowStar.Regional.Rgl_region_of", "proj_equation_LowStar.Regional.Rgl_state", "projection_inverse_LowStar.Regional.Rgl_r_inv", "projection_inverse_LowStar.Regional.Rgl_r_repr", "projection_inverse_LowStar.Regional.Rgl_region_of", "projection_inverse_LowStar.Regional.Rgl_state", "refinement_interpretation_Tm_refine_425abd470ae75ea2fff9584e9122c94a", "refinement_interpretation_Tm_refine_529fc5d835e99e9966347c4a5e502ac8", "refinement_interpretation_Tm_refine_74ea8d30b6a6be04a6721874a9888775", "token_correspondence_LowStar.Regional.__proj__Rgl__item__r_repr", "token_correspondence_LowStar.Regional.__proj__Rgl__item__region_of", "token_correspondence_LowStar.Regional.rg_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_r_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_region_of" ], 0, "5ad5b736efd5d12e681df45fddd9f24c" ], [ "MerkleTree.Low.Datastructures.hash_vec_r_inv_reg", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_LowStar.Buffer.buffer", "equation_LowStar.RVector.rv_inv", "equation_LowStar.RVector.rv_itself_inv", "equation_LowStar.RVector.rvector", "equation_LowStar.Vector.live", "equation_LowStar.Vector.vector", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Datastructures.hash_vec_r_inv", "equation_MerkleTree.Low.Datastructures.hash_vec_region_of", "equation_MerkleTree.Low.Datastructures.hreg", "fuel_guarded_inversion_LowStar.Vector.vector_str", "lemma_LowStar.Monotonic.Buffer.live_region_frameOf", "proj_equation_LowStar.Vector.Vec_vs", "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Vector.__proj__Vec__item__vs", "typing_MerkleTree.Low.Datastructures.hash" ], 0, "ffced6ef85f495bc7a2f842e4f43c507" ], [ "MerkleTree.Low.Datastructures.hash_vec_repr", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.gt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gt", "equation_MerkleTree.Low.Datastructures.hash_size_t", "int_typing", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec" ], 0, "77046663a88e4804914148449e8cf680" ], [ "MerkleTree.Low.Datastructures.hash_vec_r_repr", 1, 0, 0, [ "@query", "equation_MerkleTree.Low.Datastructures.hash_vec_r_inv" ], 0, "613f91707102f419015fe163a476ed6b" ], [ "MerkleTree.Low.Datastructures.hash_vec_r_sep", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.l_and", "equation_Prims.squash", "l_and-interp", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "71445011e7bfc236b05322ad3d840f6b" ], [ "MerkleTree.Low.Datastructures.hash_vec_r_sep", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_typing", "equation_LowStar.RVector.as_seq", "equation_LowStar.RVector.loc_rvector", "equation_LowStar.RVector.rvector", "equation_LowStar.Vector.vector", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Datastructures.hash_vec_r_inv", "equation_MerkleTree.Low.Datastructures.hash_vec_r_repr", "equation_MerkleTree.Low.Datastructures.hash_vec_region_of", "equation_MerkleTree.Low.Datastructures.hreg", "fuel_guarded_inversion_LowStar.Vector.vector_str", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "proj_equation_LowStar.Regional.Rgl_repr", "projection_inverse_LowStar.Regional.Rgl_repr", "refinement_interpretation_Tm_refine_9a4f5366055910237954d85f232cccf4", "refinement_interpretation_Tm_refine_b793c488ad500e6b09ecca7df8a04085", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Set.singleton", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.RVector.as_seq", "typing_MerkleTree.Low.Datastructures.hash", "typing_MerkleTree.Low.Datastructures.hash_repr", "typing_MerkleTree.Low.Datastructures.hash_vec_region_of", "typing_MerkleTree.Low.Datastructures.hreg" ], 0, "955afb95418d65f17b4dd642dcc5e7b8" ], [ "MerkleTree.Low.Datastructures.hash_vec_irepr", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.gt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gt", "equation_MerkleTree.Low.Datastructures.hash_size_t", "int_typing", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec" ], 0, "9f97f4a331b8914f63bf1d88c4e03c12" ], [ "MerkleTree.Low.Datastructures.hash_vec_r_alloc", 1, 1, 0, [ "@query" ], 0, "6df21a999068ef9b47f2b198fea3f017" ], [ "MerkleTree.Low.Datastructures.hash_vec_r_alloc", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_LowStar.RVector.as_seq_seq.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.Signed", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "data_typing_intro_FStar.Pervasives.Native.None@tok", "disc_equation_FStar.Pervasives.Native.None", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.HyperStack.ST.erid", "equation_FStar.HyperStack.ST.is_eternal_region", "equation_FStar.Integers.int_t", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_region", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.gt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gt", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.fresh_loc", "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.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.rvector", "equation_LowStar.Vector.as_seq", "equation_LowStar.Vector.forall2_seq", "equation_LowStar.Vector.forall_seq", "equation_LowStar.Vector.freeable", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.vector", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_dummy", "equation_MerkleTree.Low.Datastructures.hash_repr", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Datastructures.hash_vec_irepr", "equation_MerkleTree.Low.Datastructures.hash_vec_r_alloc_p", "equation_MerkleTree.Low.Datastructures.hash_vec_r_inv", "equation_MerkleTree.Low.Datastructures.hash_vec_r_repr", "equation_MerkleTree.Low.Datastructures.hash_vec_region_of", "equation_MerkleTree.Low.Datastructures.hash_vec_repr", "equation_MerkleTree.Low.Datastructures.hreg", "equation_MerkleTree.New.High.hashes", "equation_Prims.eqtype", "equation_Prims.nat", "equation_with_fuel_LowStar.RVector.as_seq_seq.fuel_instrumented", "fuel_guarded_inversion_LowStar.Vector.vector_str", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "int_inversion", "int_typing", "lemma_FStar.Ghost.reveal_hide", "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.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Monotonic.HyperHeap.lemma_extends_only_parent", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.freeable_length", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.modifies_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.new_region_modifies", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "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", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.None_a", "projection_inverse_LowStar.Regional.Rgl_repr", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_161e04719814801d293219f408210f95", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_4097c547095e70012031c1b6bbc9fb12", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_562ac129d341d684eac8dd463a0f41fe", "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909", "refinement_interpretation_Tm_refine_69d1d206ddafb5a6092734ed6446bcfd", "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df", "refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955", "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_cbd24d5334c6bfffa6fd8a84fb787f7a", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f812e4c8adc728ad9229afa07596fb23", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.upd", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Seq.Base.empty", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.mnull", "typing_LowStar.Regional.__proj__Rgl__item__repr", "typing_LowStar.Vector.__proj__Vec__item__vs", "typing_LowStar.Vector.as_seq", "typing_LowStar.Vector.loc_vector", "typing_MerkleTree.Low.Datastructures.hash", "typing_MerkleTree.Low.Datastructures.hash_vec_repr", "typing_MerkleTree.Low.Datastructures.hreg" ], 0, "da15c80a7ddc26c7bd102bb1b47a47f4" ], [ "MerkleTree.Low.Datastructures.hash_vec_r_free", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_LowStar.RVector.loc_rvector", "equation_LowStar.RVector.rvector", "equation_LowStar.Vector.vector", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Datastructures.hash_vec_r_inv", "equation_MerkleTree.Low.Datastructures.hash_vec_region_of", "equation_MerkleTree.Low.Datastructures.hreg", "fuel_guarded_inversion_LowStar.Vector.vector_str", "refinement_interpretation_Tm_refine_326d2c83ca3ea5a5a1e77e4581cf27dc", "refinement_interpretation_Tm_refine_369f7ad234e2a7d85fc24f5ef92dd8c1", "refinement_interpretation_Tm_refine_f812e4c8adc728ad9229afa07596fb23" ], 0, "8482494f2df1e455ad9169208e726c3b" ], [ "MerkleTree.Low.Datastructures.hvreg", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_425abd470ae75ea2fff9584e9122c94a" ], 0, "79aab63f434ddee84396a25a519cffd7" ], [ "MerkleTree.Low.Datastructures.hash_vec_rv_inv_r_inv", 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_EverCrypt.Helpers.uint32_t", "equation_FStar.Integers.int_t", "equation_FStar.UInt.fits", "equation_FStar.UInt.lt", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lt", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.RVector.elems_inv", "equation_LowStar.RVector.rs_elems_inv", "equation_LowStar.RVector.rv_elems_inv", "equation_LowStar.RVector.rv_inv", "equation_LowStar.RVector.rvector", "equation_LowStar.Regional.rg_inv", "equation_LowStar.Vector.as_seq", "equation_LowStar.Vector.forall_seq", "equation_LowStar.Vector.get", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_dummy", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Datastructures.hreg", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_4097c547095e70012031c1b6bbc9fb12", "refinement_interpretation_Tm_refine_cbd783a3f1885e09765cbe0dbdd7a63a", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_LowStar.Regional.__proj__Rgl__item__r_inv", "token_correspondence_LowStar.Regional.rg_inv", "typing_FStar.UInt32.lt", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.mnull", "typing_LowStar.Vector.size_of", "typing_MerkleTree.Low.Datastructures.hash" ], 0, "7502ced0c8c47cceb64f2b54f3e93501" ], [ "MerkleTree.Low.Datastructures.hash_vv_rv_inv_r_inv", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash", "l_and-interp", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "7dd66131ddded51a35d9e81886844f3c" ], [ "MerkleTree.Low.Datastructures.hash_vv_rv_inv_r_inv", 2, 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_EverCrypt.Helpers.uint32_t", "equation_FStar.Integers.int_t", "equation_FStar.UInt.fits", "equation_FStar.UInt.lt", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lt", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.RVector.elems_inv", "equation_LowStar.RVector.rs_elems_inv", "equation_LowStar.RVector.rv_elems_inv", "equation_LowStar.RVector.rv_inv", "equation_LowStar.Regional.rg_inv", "equation_LowStar.Vector.as_seq", "equation_LowStar.Vector.forall_seq", "equation_LowStar.Vector.get", "equation_LowStar.Vector.size_of", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Datastructures.hash_vec_r_inv", "equation_MerkleTree.Low.Datastructures.hreg", "equation_MerkleTree.Low.Datastructures.hvreg", "function_token_typing_LowStar.Regional.__proj__Rgl__item__r_inv", "int_inversion", "int_typing", "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "proj_equation_LowStar.Regional.Rgl_r_inv", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_LowStar.Regional.Rgl_r_inv", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_4097c547095e70012031c1b6bbc9fb12", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "token_correspondence_LowStar.Regional.__proj__Rgl__item__r_inv", "token_correspondence_LowStar.Regional.rg_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_vec_r_inv", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.mnull", "typing_MerkleTree.Low.Datastructures.hash" ], 0, "2a27512f12c0acb35dee57a5deb01ec2" ], [ "MerkleTree.Low.Datastructures.hash_vv_rv_inv_disjoint", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash", "l_and-interp", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "1679048591510c4fe8650fd807e5e0f0" ], [ "MerkleTree.Low.Datastructures.hash_vv_rv_inv_disjoint", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "LowStar.Regional.Instances_interpretation_Tm_ghost_arrow_e79a3b97235ac88cf4ef318b133a3ada", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Signed", "constructor_distinct_FStar.Integers.Winfinite", "equality_tok_FStar.Integers.Winfinite@tok", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.Integers.int_t", "equation_FStar.Monotonic.HyperHeap.disjoint", "equation_FStar.UInt.fits", "equation_FStar.UInt.lt", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lt", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.RVector.elems_inv", "equation_LowStar.RVector.elems_reg", "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.Regional.Instances.vector_region_of", "equation_LowStar.Regional.Instances.vector_regional", "equation_LowStar.Regional.rg_inv", "equation_LowStar.Vector.as_seq", "equation_LowStar.Vector.forall_seq", "equation_LowStar.Vector.get", "equation_LowStar.Vector.size_of", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Datastructures.hash_vec_r_inv", "equation_MerkleTree.Low.Datastructures.hash_vec_region_of", "equation_MerkleTree.Low.Datastructures.hash_vv", "equation_MerkleTree.Low.Datastructures.hreg", "equation_MerkleTree.Low.Datastructures.hvreg", "equation_MerkleTree.Low.Datastructures.hvvreg", "function_token_typing_LowStar.Regional.Instances.vector_region_of", "int_inversion", "interpretation_Tm_abs_8af5505247aa684e407d3b8992667aef", "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.Monotonic.HyperHeap.lemma_disjoint_includes", "lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_trans", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "proj_equation_LowStar.Regional.Rgl_r_inv", "proj_equation_LowStar.Regional.Rgl_region_of", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_LowStar.Regional.Rgl_r_inv", "projection_inverse_LowStar.Regional.Rgl_region_of", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_4097c547095e70012031c1b6bbc9fb12", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "token_correspondence_LowStar.Regional.Instances.vector_region_of", "token_correspondence_LowStar.Regional.__proj__Rgl__item__region_of", "token_correspondence_LowStar.Regional.rg_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_vec_r_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_vec_region_of", "typing_FStar.Monotonic.HyperHeap.includes", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.mnull", "typing_MerkleTree.Low.Datastructures.hash_vec", "typing_MerkleTree.Low.Datastructures.hvreg" ], 0, "36f7fe094586a8aaba7cc11a49c459ad" ], [ "MerkleTree.Low.Datastructures.hash_vv_rv_inv_includes", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash", "l_and-interp", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "c0dbc6753ba788b562f96076ccc82486" ], [ "MerkleTree.Low.Datastructures.hash_vv_rv_inv_includes", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "LowStar.Regional.Instances_interpretation_Tm_ghost_arrow_e79a3b97235ac88cf4ef318b133a3ada", "MerkleTree.Low.Datastructures_interpretation_Tm_ghost_arrow_62be7e8e1a69604f9a36351a77d748fa", "MerkleTree.Low.Datastructures_interpretation_Tm_ghost_arrow_c55a67b27f4ea444400878ed4572b7c7", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Signed", "constructor_distinct_FStar.Integers.Winfinite", "equality_tok_FStar.Integers.Winfinite@tok", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.Integers.int_t", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.lt", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lt", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.RVector.elems_inv", "equation_LowStar.RVector.elems_reg", "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.rvector", "equation_LowStar.Regional.Instances.vector_region_of", "equation_LowStar.Regional.Instances.vector_regional", "equation_LowStar.Regional.rg_inv", "equation_LowStar.Vector.as_seq", "equation_LowStar.Vector.forall_seq", "equation_LowStar.Vector.get", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Datastructures.hash_vec_r_inv", "equation_MerkleTree.Low.Datastructures.hash_vec_region_of", "equation_MerkleTree.Low.Datastructures.hash_vv", "equation_MerkleTree.Low.Datastructures.hreg", "equation_MerkleTree.Low.Datastructures.hvreg", "equation_MerkleTree.Low.Datastructures.hvvreg", "fuel_guarded_inversion_LowStar.Vector.vector_str", "function_token_typing_LowStar.Regional.Instances.vector_region_of", "function_token_typing_MerkleTree.Low.Datastructures.hash_region_of", "function_token_typing_MerkleTree.Low.Datastructures.hash_vec_region_of", "int_inversion", "int_typing", "interpretation_Tm_abs_8af5505247aa684e407d3b8992667aef", "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_trans", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "proj_equation_LowStar.Regional.Rgl_r_inv", "proj_equation_LowStar.Regional.Rgl_region_of", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_LowStar.Regional.Rgl_r_inv", "projection_inverse_LowStar.Regional.Rgl_region_of", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_4097c547095e70012031c1b6bbc9fb12", "refinement_interpretation_Tm_refine_5a88c51956f007f77dee75dd2a07bb5a", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "token_correspondence_LowStar.Regional.Instances.vector_region_of", "token_correspondence_LowStar.Regional.__proj__Rgl__item__region_of", "token_correspondence_LowStar.Regional.rg_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_region_of", "token_correspondence_MerkleTree.Low.Datastructures.hash_vec_r_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_vec_region_of", "typing_FStar.Monotonic.HyperHeap.includes", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.mnull", "typing_LowStar.Vector.__proj__Vec__item__sz", "typing_LowStar.Vector.get", "typing_MerkleTree.Low.Datastructures.hash", "typing_MerkleTree.Low.Datastructures.hash_region_of", "typing_MerkleTree.Low.Datastructures.hash_vec", "typing_MerkleTree.Low.Datastructures.hvreg" ], 0, "acb8251091d4bf17f69111280718c9f3" ], [ "MerkleTree.Low.Datastructures.hash_vv_as_seq_get_index", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_LowStar.RVector.as_seq_seq.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Signed", "constructor_distinct_FStar.Integers.Winfinite", "equality_tok_FStar.Integers.Winfinite@tok", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.Integers.int_t", "equation_FStar.UInt.fits", "equation_FStar.UInt.gt", "equation_FStar.UInt.lt", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gt", "equation_FStar.UInt32.lt", "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.rs_elems_inv", "equation_LowStar.RVector.rv_elems_inv", "equation_LowStar.RVector.rv_inv", "equation_LowStar.RVector.rvector", "equation_LowStar.Regional.rg_inv", "equation_LowStar.Vector.as_seq", "equation_LowStar.Vector.forall_seq", "equation_LowStar.Vector.get", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_repr", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Datastructures.hash_vec_r_inv", "equation_MerkleTree.Low.Datastructures.hash_vec_r_repr", "equation_MerkleTree.Low.Datastructures.hash_vv", "equation_MerkleTree.Low.Datastructures.hreg", "equation_MerkleTree.Low.Datastructures.hvreg", "equation_MerkleTree.New.High.hash", "equation_Prims.nat", "equation_Prims.squash", "fuel_guarded_inversion_LowStar.Vector.vector_str", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.RVector.as_seq_seq_index", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "proj_equation_LowStar.Regional.Rgl_r_inv", "proj_equation_LowStar.Regional.Rgl_r_repr", "proj_equation_LowStar.Regional.Rgl_repr", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_LowStar.Regional.Rgl_r_inv", "projection_inverse_LowStar.Regional.Rgl_r_repr", "projection_inverse_LowStar.Regional.Rgl_repr", "refinement_interpretation_Tm_refine_03e0ee7c990720bc4bd1c73dc60b1ac5", "refinement_interpretation_Tm_refine_29c27ac7c716b2238749315b70c9eca3", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_4097c547095e70012031c1b6bbc9fb12", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_562ac129d341d684eac8dd463a0f41fe", "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909", "refinement_interpretation_Tm_refine_69d1d206ddafb5a6092734ed6446bcfd", "refinement_interpretation_Tm_refine_7108b467000c99be927e4d94496382d1", "refinement_interpretation_Tm_refine_78262dccf3c686c092c54c0e4056d92a", "refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955", "refinement_interpretation_Tm_refine_9a4f5366055910237954d85f232cccf4", "refinement_interpretation_Tm_refine_b793c488ad500e6b09ecca7df8a04085", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "token_correspondence_LowStar.Regional.__proj__Rgl__item__r_inv", "token_correspondence_LowStar.Regional.__proj__Rgl__item__r_repr", "token_correspondence_LowStar.Regional.rg_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_vec_r_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_vec_r_repr", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.mnull", "typing_LowStar.RVector.as_seq", "typing_LowStar.RVector.as_seq_seq", "typing_LowStar.Vector.as_seq", "typing_LowStar.Vector.size_of", "typing_MerkleTree.Low.Datastructures.hash", "typing_MerkleTree.Low.Datastructures.hash_vec", "typing_MerkleTree.Low.Datastructures.hreg", "typing_MerkleTree.Low.Datastructures.hvreg" ], 0, "d71236f997261cbd65631220ea5aca39" ], [ "MerkleTree.Low.Datastructures.hash_vv_as_seq_get_index", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_LowStar.RVector.as_seq_seq.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Signed", "constructor_distinct_FStar.Integers.Winfinite", "equality_tok_FStar.Integers.Winfinite@tok", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.Integers.int_t", "equation_FStar.UInt.fits", "equation_FStar.UInt.gte", "equation_FStar.UInt.lt", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gte", "equation_FStar.UInt32.lt", "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.rs_elems_inv", "equation_LowStar.RVector.rv_elems_inv", "equation_LowStar.RVector.rv_inv", "equation_LowStar.RVector.rv_itself_inv", "equation_LowStar.RVector.rvector", "equation_LowStar.Regional.rg_inv", "equation_LowStar.Vector.as_seq", "equation_LowStar.Vector.forall_seq", "equation_LowStar.Vector.freeable", "equation_LowStar.Vector.get", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_repr", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Datastructures.hash_vec_dummy", "equation_MerkleTree.Low.Datastructures.hash_vec_r_inv", "equation_MerkleTree.Low.Datastructures.hash_vec_r_repr", "equation_MerkleTree.Low.Datastructures.hash_vec_repr", "equation_MerkleTree.Low.Datastructures.hash_vv", "equation_MerkleTree.Low.Datastructures.hreg", "equation_MerkleTree.Low.Datastructures.hvreg", "equation_MerkleTree.New.High.hash", "equation_MerkleTree.New.High.hashes", "equation_Prims.nat", "fuel_guarded_inversion_LowStar.Vector.vector_str", "int_inversion", "int_typing", "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.UInt32.uv_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.RVector.as_seq_seq_index", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_LowStar.Regional.Rgl_r_inv", "proj_equation_LowStar.Regional.Rgl_r_repr", "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_LowStar.Regional.Rgl_r_inv", "projection_inverse_LowStar.Regional.Rgl_r_repr", "projection_inverse_LowStar.Regional.Rgl_repr", "refinement_interpretation_Tm_refine_03e0ee7c990720bc4bd1c73dc60b1ac5", "refinement_interpretation_Tm_refine_3396f1d518ffeb2163c25c13fcb1de13", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_4097c547095e70012031c1b6bbc9fb12", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_562ac129d341d684eac8dd463a0f41fe", "refinement_interpretation_Tm_refine_5a88c51956f007f77dee75dd2a07bb5a", "refinement_interpretation_Tm_refine_69d1d206ddafb5a6092734ed6446bcfd", "refinement_interpretation_Tm_refine_7108b467000c99be927e4d94496382d1", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955", "refinement_interpretation_Tm_refine_9a4f5366055910237954d85f232cccf4", "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7", "refinement_interpretation_Tm_refine_adefc58894388886573cb41ee073aed9", "refinement_interpretation_Tm_refine_b793c488ad500e6b09ecca7df8a04085", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "token_correspondence_LowStar.Regional.__proj__Rgl__item__r_repr", "token_correspondence_LowStar.Regional.rg_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_vec_r_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_vec_r_repr", "typing_FStar.Ghost.hide", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.gte", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.mnull", "typing_LowStar.RVector.as_seq", "typing_LowStar.RVector.as_seq_seq", "typing_LowStar.Vector.__proj__Vec__item__cap", "typing_LowStar.Vector.__proj__Vec__item__sz", "typing_LowStar.Vector.__proj__Vec__item__vs", "typing_LowStar.Vector.alloc_empty", "typing_LowStar.Vector.as_seq", "typing_LowStar.Vector.get", "typing_LowStar.Vector.size_of", "typing_MerkleTree.Low.Datastructures.hash", "typing_MerkleTree.Low.Datastructures.hash_repr", "typing_MerkleTree.Low.Datastructures.hash_vec", "typing_MerkleTree.Low.Datastructures.hash_vec_dummy", "typing_MerkleTree.Low.Datastructures.hreg", "typing_MerkleTree.Low.Datastructures.hvreg" ], 0, "a6ef9e7b466e75a781af0d93772822bf" ] ] ]