[ "\bų~4‹“\\–p—|F»’_", [ [ "MerkleTree.Low.Serialization.serialize_bool", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "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_FStar.UInt.fits", "equation_FStar.UInt.gte", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gte", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_p", "equation_MerkleTree.Low.Serialization.uint8_t", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_LowStar.Buffer.trivial_preorder", "int_inversion", "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.Map.lemma_ContainsDom", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "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_8f35a30b5723496a838bcc2be6799465", "refinement_interpretation_Tm_refine_cc76c1187479aaadac4ff31d2094b7c4", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fca1da8bf23eec7ba880d4dab9bb43f7", "true_interp", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, "097c63d7339ad1bb8bd11acfefb6c7b5" ], [ "MerkleTree.Low.Serialization.serialize_uint8_t", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.UInt.fits", "equation_FStar.UInt.gte", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gte", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_p", "equation_MerkleTree.Low.Serialization.uint8_t", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_LowStar.Buffer.trivial_preorder", "int_inversion", "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_LowStar.Monotonic.Buffer.modifies_refl", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_cc76c1187479aaadac4ff31d2094b7c4", "refinement_interpretation_Tm_refine_e633d96da2f5ad1e125b09ef53e4c4f2", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fca1da8bf23eec7ba880d4dab9bb43f7", "true_interp", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, "2ba3692b5d7b47f392f801819b0c70dd" ], [ "MerkleTree.Low.Serialization.serialize_uint16_t", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "equality_tok_FStar.Integers.W8@tok", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_MerkleTree.Low.Serialization.uint8_p", "equation_MerkleTree.Low.Serialization.uint8_t", "function_token_typing_FStar.Integers.uint_8", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_fca1da8bf23eec7ba880d4dab9bb43f7", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, "8a13167daaabff10f342d11455300406" ], [ "MerkleTree.Low.Serialization.serialize_uint32_t", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "equality_tok_FStar.Integers.W8@tok", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_MerkleTree.Low.Serialization.uint8_p", "equation_MerkleTree.Low.Serialization.uint8_t", "function_token_typing_FStar.Integers.uint_8", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_fca1da8bf23eec7ba880d4dab9bb43f7", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, "24a1ca13131719460b68904a53097c6d" ], [ "MerkleTree.Low.Serialization.serialize_uint64_t", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "equality_tok_FStar.Integers.W8@tok", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_MerkleTree.Low.Serialization.uint8_p", "equation_MerkleTree.Low.Serialization.uint8_t", "function_token_typing_FStar.Integers.uint_8", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_fca1da8bf23eec7ba880d4dab9bb43f7", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, "5cdf7e5aab078d783c719bd4ccaded6e" ], [ "MerkleTree.Low.Serialization.serialize_hash_i", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.lt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lt", "equation_Lib.IntTypes.byte_t", "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.length", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_p", "equation_MerkleTree.Low.Serialization.uint8_t", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "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_LessThan", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_519c1d4d0666e802c34e2e451d27063b", "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909", "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc", "refinement_interpretation_Tm_refine_cf65d243580d5162516eff3756abceb2", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fca1da8bf23eec7ba880d4dab9bb43f7", "typing_FStar.UInt32.lt", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, "b3fe1cfc3fed3412ac347c9b6733ceb3" ], [ "MerkleTree.Low.Serialization.serialize_hash", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "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_FStar.UInt.fits", "equation_FStar.UInt.gt", "equation_FStar.UInt.lt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gt", "equation_FStar.UInt32.lt", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_p", "equation_MerkleTree.Low.Serialization.uint8_t", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_519c1d4d0666e802c34e2e451d27063b", "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909", "refinement_interpretation_Tm_refine_cc76c1187479aaadac4ff31d2094b7c4", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, "87058536e3f71e7cc8975fcb5b34fb1e" ], [ "MerkleTree.Low.Serialization.u64_add_fits", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "equation_FStar.UInt.fits", "equation_FStar.UInt.gte", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt64.gte", "equation_MerkleTree.Low.Serialization.uint64_t", "equation_MerkleTree.Low.uint64_max", "equation_Prims.nat", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt64.vu_inv", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_4db8ba22c4504a66577a2159dcc603cd", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_FStar.UInt.max_int", "typing_FStar.UInt64.sub", "typing_FStar.UInt64.v", "typing_MerkleTree.Low.uint64_max" ], 0, "43204d5fa4d432b2f59546a6e1654355" ], [ "MerkleTree.Low.Serialization.hash_vec_bytes", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.Int.Cast.uint32_to_uint64", "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.uint8", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.RVector.rvector", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "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.Serialization.uint64_t", "equation_Prims.nat", "equation_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_LowStar.Vector.vector_str", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt64.vu_inv", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_48c1b5b4c02ad49f0760911a9d4b1fb4", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909", "refinement_interpretation_Tm_refine_5919d3f91c6fa6342ebeebd05831330c", "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_FStar.UInt64.uint_to_t", "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", "typing_MerkleTree.Low.Serialization.u64_add_fits" ], 0, "e9d3706ccfbab37ea97438a4d7ec4e8b" ], [ "MerkleTree.Low.Serialization.serialize_hash_vec_i", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Signed", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "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_FStar.UInt.fits", "equation_FStar.UInt.lt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lt", "equation_Lib.IntTypes.byte_t", "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.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.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.size_of", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_dummy", "equation_MerkleTree.Low.Datastructures.hash_r_inv", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Datastructures.hreg", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_p", "equation_MerkleTree.Low.Serialization.uint8_t", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_LowStar.Vector.vector_str", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "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.HyperStack.lemma_tip_top_smt", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.length_null_2", "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", "lemma_LowStar.RVector.rv_inv_preserved", "primitive_Prims.op_Addition", "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_FStar.Integers.Unsigned__0", "projection_inverse_LowStar.Regional.Rgl_r_inv", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_3e7d6d9effbbeae5539c0cb324d2cadb", "refinement_interpretation_Tm_refine_4097c547095e70012031c1b6bbc9fb12", "refinement_interpretation_Tm_refine_519c1d4d0666e802c34e2e451d27063b", "refinement_interpretation_Tm_refine_ac09e169622915d2fb30eeed97b3a2b2", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "token_correspondence_LowStar.Regional.rg_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_r_inv", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "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.loc_buffer", "typing_LowStar.Monotonic.Buffer.mnull", "typing_LowStar.Vector.size_of", "typing_MerkleTree.Low.Datastructures.hash", "typing_MerkleTree.Low.Datastructures.hreg" ], 0, "2e854d0e65e6bcabd4a5973b4f7b47dc" ], [ "MerkleTree.Low.Serialization.serialize_hash_vec", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.disjoint", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.gt", "equation_FStar.UInt.lt", "equation_FStar.UInt32.gt", "equation_FStar.UInt32.lt", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.RVector.loc_rvector", "equation_LowStar.RVector.rv_inv", "equation_LowStar.RVector.rv_itself_inv", "equation_LowStar.RVector.rvector", "equation_LowStar.Vector.freeable", "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_region_of", "equation_MerkleTree.Low.Datastructures.hreg", "equation_MerkleTree.Low.Datastructures.hvreg", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_p", "equation_MerkleTree.Low.Serialization.uint8_t", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_LowStar.Vector.vector_str", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "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.Monotonic.HyperStack.lemma_tip_top_smt", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "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_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_regions", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "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_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan", "primitive_Prims.op_Negation", "proj_equation_LowStar.Regional.Rgl_region_of", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_LowStar.Regional.Rgl_region_of", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7", "refinement_interpretation_Tm_refine_ac09e169622915d2fb30eeed97b3a2b2", "refinement_interpretation_Tm_refine_d96c0978ac30e5f0fd109eead55c3101", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "token_correspondence_LowStar.Regional.__proj__Rgl__item__region_of", "token_correspondence_MerkleTree.Low.Datastructures.hash_vec_region_of", "typing_FStar.Monotonic.HyperHeap.includes", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Set.empty", "typing_FStar.Set.intersect", "typing_FStar.Set.singleton", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.mnull", "typing_LowStar.RVector.loc_rvector", "typing_LowStar.Vector.__proj__Vec__item__vs", "typing_MerkleTree.Low.Datastructures.hash", "typing_MerkleTree.Low.Datastructures.hash_vec_region_of", "typing_MerkleTree.Low.Datastructures.hreg" ], 0, "acab870abf2e993c328e8e439fb820fc" ], [ "MerkleTree.Low.Serialization.hash_vv_bytes_i", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W64", "equality_tok_FStar.Integers.W64@tok", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Integers.int_t", "equation_FStar.Monotonic.Heap.equal_dom", "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_FStar.UInt.fits", "equation_FStar.UInt.gte", "equation_FStar.UInt.lt", "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_LowStar.RVector.rvector", "equation_LowStar.Vector.as_seq", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Datastructures.hash_vv", "equation_MerkleTree.Low.Serialization.hash_vec_bytes", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint64_t", "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.Map.lemma_ContainsDom", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "proj_equation_LowStar.Vector.Vec_sz", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_562ac129d341d684eac8dd463a0f41fe", "refinement_interpretation_Tm_refine_5919d3f91c6fa6342ebeebd05831330c", "refinement_interpretation_Tm_refine_dd6b31fbf6cc990de2d6442415284c3b", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt32.lt", "typing_FStar.UInt32.v", "typing_LowStar.Vector.__proj__Vec__item__sz", "typing_LowStar.Vector.as_seq", "typing_MerkleTree.Low.Datastructures.hash_vec", "typing_MerkleTree.Low.Serialization.hash_vec_bytes", "typing_MerkleTree.Low.Serialization.u64_add_fits" ], 0, "444abb037695d088c7f1d312596cdfd9" ], [ "MerkleTree.Low.Serialization.serialize_hash_vv_i", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "LowStar.Regional.Instances_interpretation_Tm_ghost_arrow_e79a3b97235ac88cf4ef318b133a3ada", "MerkleTree.Low.Datastructures_interpretation_Tm_ghost_arrow_c55a67b27f4ea444400878ed4572b7c7", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "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.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.disjoint", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.lt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lt", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.RVector.elems_inv", "equation_LowStar.RVector.elems_reg", "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.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.freeable", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "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_vv", "equation_MerkleTree.Low.Datastructures.hvreg", "equation_MerkleTree.Low.Datastructures.hvvreg", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_p", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_LowStar.Vector.vector_str", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_LowStar.Regional.Instances.vector_region_of", "function_token_typing_MerkleTree.Low.Datastructures.hash_vec_region_of", "int_inversion", "interpretation_Tm_abs_8af5505247aa684e407d3b8992667aef", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Monotonic.HyperHeap.lemma_disjoint_includes", "lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes", "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "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_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_regions", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "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_Equality", "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", "proj_equation_LowStar.Vector.Vec_vs", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_LowStar.Regional.Rgl_r_inv", "projection_inverse_LowStar.Regional.Rgl_region_of", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_26862678c89ff3fc205c8b94520ae4f0", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_4097c547095e70012031c1b6bbc9fb12", "refinement_interpretation_Tm_refine_446bf10afa9e2c979cbc68d89c3e36ad", "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "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", "typing_FStar.Monotonic.HyperHeap.includes", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Set.empty", "typing_FStar.Set.intersect", "typing_FStar.Set.singleton", "typing_FStar.UInt32.lt", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.mnull", "typing_LowStar.RVector.loc_rvector", "typing_LowStar.Vector.__proj__Vec__item__vs", "typing_LowStar.Vector.size_of", "typing_MerkleTree.Low.Datastructures.hash_vec", "typing_MerkleTree.Low.Datastructures.hvreg", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "9d23730e5a14f989bf9039a8078194ff" ], [ "MerkleTree.Low.Serialization.serialize_hash_vv", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "LowStar.Regional.Instances_interpretation_Tm_ghost_arrow_e79a3b97235ac88cf4ef318b133a3ada", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.disjoint", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.gt", "equation_FStar.UInt.lt", "equation_FStar.UInt32.gt", "equation_FStar.UInt32.lt", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.RVector.loc_rvector", "equation_LowStar.RVector.rv_inv", "equation_LowStar.RVector.rv_itself_inv", "equation_LowStar.RVector.rvector", "equation_LowStar.Regional.Instances.vector_dummy", "equation_LowStar.Regional.Instances.vector_region_of", "equation_LowStar.Regional.Instances.vector_regional", "equation_LowStar.Vector.freeable", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Datastructures.hash_vv", "equation_MerkleTree.Low.Datastructures.hvreg", "equation_MerkleTree.Low.Datastructures.hvvreg", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_p", "equation_MerkleTree.Low.Serialization.uint8_t", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_LowStar.Vector.vector_str", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_LowStar.Regional.Instances.vector_region_of", "kinding_LowStar.Regional.regional@tok", "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.Monotonic.HyperStack.lemma_tip_top_smt", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "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_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_regions", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "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_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan", "primitive_Prims.op_Negation", "proj_equation_LowStar.Regional.Rgl_region_of", "proj_equation_LowStar.Vector.Vec_vs", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_LowStar.Regional.Rgl_region_of", "refinement_interpretation_Tm_refine_26862678c89ff3fc205c8b94520ae4f0", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7", "refinement_interpretation_Tm_refine_adefc58894388886573cb41ee073aed9", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "token_correspondence_LowStar.Regional.Instances.vector_region_of", "token_correspondence_LowStar.Regional.__proj__Rgl__item__region_of", "typing_FStar.Ghost.hide", "typing_FStar.Monotonic.HyperHeap.includes", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Set.empty", "typing_FStar.Set.intersect", "typing_FStar.Set.singleton", "typing_FStar.UInt32.lt", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.mnull", "typing_LowStar.RVector.loc_rvector", "typing_LowStar.Regional.Instances.vector_dummy", "typing_LowStar.Vector.__proj__Vec__item__vs", "typing_LowStar.Vector.alloc_empty", "typing_LowStar.Vector.size_of", "typing_MerkleTree.Low.Datastructures.hash_vec", "typing_MerkleTree.Low.Datastructures.hvreg" ], 0, "59d63ceb3398a62948651f9365a06d22" ], [ "MerkleTree.Low.Serialization.deserialize_bool", 1, 0, 0, [ "@query" ], 0, "e6bb15c6808eeb267d8026b7e85b72aa" ], [ "MerkleTree.Low.Serialization.deserialize_bool", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Monotonic.Heap.equal_dom", "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_FStar.UInt.fits", "equation_FStar.UInt.gte", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gte", "equation_MerkleTree.Low.Serialization.const_uint8_p", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_pointer", "function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, "8b3686116c44a64fbc23944cbab6983a" ], [ "MerkleTree.Low.Serialization.deserialize_uint8_t", 1, 0, 0, [ "@query" ], 0, "7cefaa9238fed1f3c80811d2dc57be64" ], [ "MerkleTree.Low.Serialization.deserialize_uint8_t", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.UInt.fits", "equation_FStar.UInt.gte", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gte", "equation_MerkleTree.Low.Serialization.const_uint8_p", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_pointer", "int_inversion", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.v" ], 0, "b830642edfa9380fc6a68cc85eee40e1" ], [ "MerkleTree.Low.Serialization.deserialize_uint16_t", 1, 0, 0, [ "@query" ], 0, "ceb4baa9fb179acd4e34e0499ff610e5" ], [ "MerkleTree.Low.Serialization.deserialize_uint16_t", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Int.Cast.uint8_to_uint16", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_LowStar.ConstBuffer.as_mbuf", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_MerkleTree.Low.Serialization.const_uint8_p", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_pointer", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "int_typing", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt.shift_left_value_lemma", "lemma_Lib.IntTypes.pow2_4", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "refinement_interpretation_Tm_refine_541d06ed6731928026bc39b1981eb00a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Int.Cast.uint8_to_uint16", "typing_FStar.UInt.fits", "typing_FStar.UInt16.v", "typing_FStar.UInt32.v", "typing_FStar.UInt8.v", "typing_LowStar.ConstBuffer.as_mbuf", "typing_LowStar.ConstBuffer.as_qbuf", "typing_LowStar.ConstBuffer.qbuf_pre" ], 0, "e72e2cbf211026117134f46835e12c03" ], [ "MerkleTree.Low.Serialization.deserialize_uint32_t", 1, 0, 0, [ "@query" ], 0, "b7d095ef081e6af2b24548bc4d2b330f" ], [ "MerkleTree.Low.Serialization.deserialize_uint32_t", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Int.Cast.uint16_to_uint32", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_LowStar.ConstBuffer.as_mbuf", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_MerkleTree.Low.Serialization.const_uint8_p", "equation_MerkleTree.Low.Serialization.uint16_t", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_pointer", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "int_typing", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt.shift_left_value_lemma", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "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.Mktuple3__3", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_88c857def71d9b11ced5e5e041edc24e", "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Int.Cast.uint16_to_uint32", "typing_FStar.UInt.fits", "typing_FStar.UInt16.v", "typing_FStar.UInt32.v", "typing_LowStar.ConstBuffer.as_mbuf", "typing_LowStar.ConstBuffer.as_qbuf", "typing_LowStar.ConstBuffer.qbuf_pre" ], 0, "fb5226489e053698acbca3801d3251b8" ], [ "MerkleTree.Low.Serialization.deserialize_uint64_t", 1, 0, 0, [ "@query" ], 0, "c1e25d230348b592722b9a10513bebf5" ], [ "MerkleTree.Low.Serialization.deserialize_uint64_t", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W64", "equality_tok_FStar.Integers.W64@tok", "equation_FStar.BitVector.bv_t", "equation_FStar.BitVector.zero_vec", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Int.Cast.uint32_to_uint64", "equation_FStar.Integers.int_t", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_MerkleTree.Low.Serialization.const_uint8_p", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_pointer", "equation_Prims.nat", "equation_Prims.pos", "int_typing", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt.shift_left_value_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b", "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f", "refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.BitVector.zero_vec", "typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.UInt32.v", "typing_FStar.UInt64.v" ], 0, "2fbf9c95898cee07651650e723c5e10e" ], [ "MerkleTree.Low.Serialization.deserialize_hash", 1, 0, 0, [ "@query" ], 0, "83901a9ea3a7be1f9069763c3f552be1" ], [ "MerkleTree.Low.Serialization.deserialize_hash", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_LowStar.ConstBuffer.MUTABLE", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_LowStar.ConstBuffer.MUTABLE@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.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_heap_color", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Set.subset", "equation_FStar.UInt.fits", "equation_FStar.UInt.gt", "equation_FStar.UInt.gte", "equation_FStar.UInt.lt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gt", "equation_FStar.UInt32.gte", "equation_FStar.UInt32.lt", "equation_Lib.IntTypes.byte_t", "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.ConstBuffer.as_mbuf", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.live", "equation_LowStar.ConstBuffer.q_preorder", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.ConstBuffer.qbuf_qual", "equation_LowStar.ConstBuffer.qual_of", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Regional.rg_dummy", "equation_LowStar.Regional.rg_inv", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_dummy", "equation_MerkleTree.Low.Datastructures.hash_r_inv", "equation_MerkleTree.Low.Datastructures.hash_r_repr", "equation_MerkleTree.Low.Datastructures.hash_repr", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hreg", "equation_MerkleTree.Low.Serialization.const_uint8_p", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_pointer", "equation_MerkleTree.New.High.hash", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_LowStar.Regional.__proj__Rgl__item__r_inv", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "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.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_buffer_null", "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_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "lemma_LowStar.Monotonic.Buffer.modifies_remove_new_locs", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_LowStar.Regional.Rgl_dummy", "proj_equation_LowStar.Regional.Rgl_loc_of", "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.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_LowStar.Regional.Rgl_dummy", "projection_inverse_LowStar.Regional.Rgl_loc_of", "projection_inverse_LowStar.Regional.Rgl_r_inv", "projection_inverse_LowStar.Regional.Rgl_r_repr", "projection_inverse_LowStar.Regional.Rgl_repr", "refinement_interpretation_Tm_refine_0585ee3c240775258e9efb20961f9395", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_29c27ac7c716b2238749315b70c9eca3", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909", "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df", "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489", "refinement_interpretation_Tm_refine_aa4b3d268075d84252df525db1f85524", "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_bcef36c9fe2b6458c3fdda81179b025f", "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "token_correspondence_LowStar.Monotonic.Buffer.loc_buffer", "token_correspondence_LowStar.Regional.__proj__Rgl__item__loc_of", "token_correspondence_LowStar.Regional.__proj__Rgl__item__r_repr", "token_correspondence_LowStar.Regional.rg_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_r_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_r_repr", "typing_FStar.Ghost.reveal", "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.sub", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.ConstBuffer.as_mbuf", "typing_LowStar.ConstBuffer.as_qbuf", "typing_LowStar.ConstBuffer.cast", "typing_LowStar.ConstBuffer.qbuf_pre", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Regional.__proj__Rgl__item__irepr", "typing_LowStar.Regional.__proj__Rgl__item__repr", "typing_MerkleTree.Low.Datastructures.hash", "typing_MerkleTree.Low.Datastructures.hreg" ], 0, "f89351fced41ad9b4b3f80adda16349d" ], [ "MerkleTree.Low.Serialization.deserialize_hash_vec_i", 1, 0, 0, [ "@query" ], 0, "2954b25258e1ea5bd91775d29d32ae33" ], [ "MerkleTree.Low.Serialization.deserialize_hash_vec_i", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_LowStar.Vector.loc_vector_within.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U8@tok", "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.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_heap_color", "equation_FStar.Monotonic.HyperStack.is_tip", "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.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.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.ConstBuffer.as_mbuf", "equation_LowStar.ConstBuffer.live", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.RVector.rvector", "equation_LowStar.Vector.live", "equation_LowStar.Vector.loc_vector", "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.Serialization.const_uint8_p", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_pointer", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_LowStar.Vector.vector_str", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "int_inversion", "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.HyperStack.lemma_map_invariant", "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "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_3e7d6d9effbbeae5539c0cb324d2cadb", "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df", "refinement_interpretation_Tm_refine_7028972db935cf1f2ecc12fc7857552a", "refinement_interpretation_Tm_refine_709aff84c75b0fff77dcbf3b529649dd", "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489", "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7", "refinement_interpretation_Tm_refine_a43b4918a11b234508ae97d267788230", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_c11ee48277084f734442582a62372ec4", "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "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.get_tip", "typing_FStar.Monotonic.HyperStack.is_heap_color", "typing_FStar.UInt32.add", "typing_FStar.UInt32.lte", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.ConstBuffer.as_mbuf", "typing_LowStar.ConstBuffer.as_qbuf", "typing_LowStar.ConstBuffer.qbuf_pre", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Vector.__proj__Vec__item__vs", "typing_LowStar.Vector.loc_vector", "typing_LowStar.Vector.loc_vector_within", "typing_LowStar.Vector.size_of", "typing_MerkleTree.Low.Datastructures.hash" ], 0, "cf8cced4844547880ba1be5fdb691a3d" ], [ "MerkleTree.Low.Serialization.deserialize_hash_vec", 1, 0, 0, [ "@query" ], 0, "0cf777d7abd0d51682aad75c60dfe8b0" ], [ "MerkleTree.Low.Serialization.deserialize_hash_vec", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "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.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.mem", "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_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.ConstBuffer.as_mbuf", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.live", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.Vector.loc_vector", "equation_LowStar.Vector.vector", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_dummy", "equation_MerkleTree.Low.Serialization.const_uint8_p", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_pointer", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_LowStar.Vector.vector_str", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Spec.AES.elem", "int_inversion", "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.Set.lemma_equal_elim", "lemma_FStar.UInt32.uv_inv", "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.loc_union_loc_none_r", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "lemma_LowStar.Monotonic.Buffer.modifies_remove_new_locs", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df", "refinement_interpretation_Tm_refine_a43b4918a11b234508ae97d267788230", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.UInt32.gt", "typing_FStar.UInt32.lt", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.ConstBuffer.as_mbuf", "typing_LowStar.ConstBuffer.as_qbuf", "typing_LowStar.ConstBuffer.qbuf_pre", "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.Vector.loc_vector", "typing_MerkleTree.Low.Datastructures.hash", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "95997aff949f8891ceeb9e84c1528dc8" ], [ "MerkleTree.Low.Serialization.deserialize_hash_vv_i", 1, 0, 0, [ "@query" ], 0, "ebc7f8c216aa58e89fae4a5f84f660eb" ], [ "MerkleTree.Low.Serialization.deserialize_hash_vv_i", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_LowStar.Vector.loc_vector_within.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U8@tok", "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.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_heap_color", "equation_FStar.Monotonic.HyperStack.is_tip", "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_Lib.IntTypes.byte_t", "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.ConstBuffer.as_mbuf", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.live", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.RVector.rvector", "equation_LowStar.Vector.as_seq", "equation_LowStar.Vector.live", "equation_LowStar.Vector.loc_vector", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "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_dummy", "equation_MerkleTree.Low.Datastructures.hash_vec_repr", "equation_MerkleTree.Low.Datastructures.hash_vv", "equation_MerkleTree.Low.Serialization.const_uint8_p", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_pointer", "equation_MerkleTree.New.High.hashes", "equation_Prims.nat", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_LowStar.Vector.vector_str", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "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.Monotonic.HyperStack.lemma_map_invariant", "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "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_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "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_LessThan", "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_3396f1d518ffeb2163c25c13fcb1de13", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_446bf10afa9e2c979cbc68d89c3e36ad", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_562ac129d341d684eac8dd463a0f41fe", "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df", "refinement_interpretation_Tm_refine_7028972db935cf1f2ecc12fc7857552a", "refinement_interpretation_Tm_refine_709aff84c75b0fff77dcbf3b529649dd", "refinement_interpretation_Tm_refine_80922429ffacb2b807b93c3173eb2f07", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_9fc79620c5f19b63ca4421ee1b3e7489", "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7", "refinement_interpretation_Tm_refine_adefc58894388886573cb41ee073aed9", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_d1ad46dabfb91f0d027c88b59cc5fd9b", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "typing_FStar.Ghost.hide", "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.get_tip", "typing_FStar.Monotonic.HyperStack.is_heap_color", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.add", "typing_FStar.UInt32.lt", "typing_FStar.UInt32.lte", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.ConstBuffer.as_mbuf", "typing_LowStar.ConstBuffer.as_qbuf", "typing_LowStar.ConstBuffer.qbuf_pre", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_seq", "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.Vector.__proj__Vec__item__cap", "typing_LowStar.Vector.__proj__Vec__item__vs", "typing_LowStar.Vector.alloc_empty", "typing_LowStar.Vector.as_seq", "typing_LowStar.Vector.loc_vector", "typing_LowStar.Vector.loc_vector_within", "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" ], 0, "94a6f2219b641fabdae6bd961f6e75a0" ], [ "MerkleTree.Low.Serialization.deserialize_hash_vv", 1, 0, 0, [ "@query" ], 0, "269c22dbaa56190af1dcc5b63dd3cf4f" ], [ "MerkleTree.Low.Serialization.deserialize_hash_vv", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "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.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.mem", "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_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.ConstBuffer.as_mbuf", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.live", "equation_LowStar.ConstBuffer.loc_buffer", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.RVector.rvector", "equation_LowStar.Vector.loc_vector", "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_dummy", "equation_MerkleTree.Low.Serialization.const_uint8_p", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_pointer", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_LowStar.Vector.vector_str", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "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.Set.lemma_equal_elim", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "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_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "lemma_LowStar.Monotonic.Buffer.modifies_remove_new_locs", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df", "refinement_interpretation_Tm_refine_80922429ffacb2b807b93c3173eb2f07", "refinement_interpretation_Tm_refine_adefc58894388886573cb41ee073aed9", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "typing_FStar.Ghost.hide", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Set.singleton", "typing_FStar.UInt32.gt", "typing_FStar.UInt32.lt", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.ConstBuffer.as_mbuf", "typing_LowStar.ConstBuffer.as_qbuf", "typing_LowStar.ConstBuffer.loc_buffer", "typing_LowStar.ConstBuffer.qbuf_pre", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.mnull", "typing_LowStar.Vector.alloc_empty", "typing_LowStar.Vector.loc_vector", "typing_LowStar.Vector.size_of", "typing_MerkleTree.Low.Datastructures.hash", "typing_MerkleTree.Low.Datastructures.hash_vec", "typing_MerkleTree.Low.Datastructures.hash_vec_dummy", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "b614f80516dbb6d9a5574d6b650bee38" ], [ "MerkleTree.Low.Serialization.mt_serialize_size", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_LowStar.ConstBuffer.MUTABLE", "equality_tok_LowStar.ConstBuffer.MUTABLE@tok", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.q_preorder", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.ConstBuffer.qbuf_qual", "equation_LowStar.ConstBuffer.qual_of", "equation_MerkleTree.Low.const_mt_p", "equation_MerkleTree.Low.const_pointer", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3" ], 0, "3093d4bccb731bb4aabb24dbf1b1b1c2" ], [ "MerkleTree.Low.Serialization.mt_serialize_size", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "MerkleTree.Low_pretyping_ef3005027cf8c4be033bc0421455028c", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_LowStar.ConstBuffer.MUTABLE", "equality_tok_FStar.Integers.W64@tok", "equality_tok_LowStar.ConstBuffer.MUTABLE@tok", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.Int.Cast.uint32_to_uint64", "equation_FStar.Integers.int_t", "equation_FStar.Monotonic.HyperHeap.disjoint", "equation_FStar.UInt.fits", "equation_FStar.UInt.gte", "equation_FStar.UInt.lt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt64.gte", "equation_FStar.UInt64.lt", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.q_preorder", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.ConstBuffer.qbuf_qual", "equation_LowStar.ConstBuffer.qual_of", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.RVector.rv_inv", "equation_LowStar.RVector.rv_itself_inv", "equation_LowStar.RVector.rvector", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_LowStar.Vector.vector", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_r_inv", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Datastructures.hreg", "equation_MerkleTree.Low.Datastructures.hvreg", "equation_MerkleTree.Low.Serialization.hash_vec_bytes", "equation_MerkleTree.Low.Serialization.u64_add_fits", "equation_MerkleTree.Low.Serialization.uint64_t", "equation_MerkleTree.Low.const_mt_p", "equation_MerkleTree.Low.const_pointer", "equation_MerkleTree.Low.merkle_tree_size_lg", "equation_MerkleTree.Low.mt_safe", "equation_MerkleTree.Low.uint32_max", "equation_MerkleTree.Low.uint64_max", "equation_Prims.nat", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "kinding_MerkleTree.Low.merkle_tree@tok", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_FStar.UInt64.vu_inv", "lemma_LowStar.Monotonic.Buffer.freeable_length", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_LowStar.Regional.Rgl_r_inv", "proj_equation_MerkleTree.Low.MT_hash_size", "proj_equation_MerkleTree.Low.MT_hs", "proj_equation_MerkleTree.Low.MT_mroot", "proj_equation_MerkleTree.Low.MT_rhs", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_LowStar.Regional.Rgl_r_inv", "refinement_interpretation_Tm_refine_02a311be716ab03201b91cc11abde92c", "refinement_interpretation_Tm_refine_2ac8bed7a6398f84bccb91bd4fed7136", "refinement_interpretation_Tm_refine_48c1b5b4c02ad49f0760911a9d4b1fb4", "refinement_interpretation_Tm_refine_4db8ba22c4504a66577a2159dcc603cd", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909", "refinement_interpretation_Tm_refine_5919d3f91c6fa6342ebeebd05831330c", "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_b7508c8246dd025aecf4ee8c56206add", "refinement_interpretation_Tm_refine_bc552b2c624e2add758b3ac761c0c563", "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b", "refinement_interpretation_Tm_refine_e07051c88e3784a2480ae13a521fed4d", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_LowStar.Regional.__proj__Rgl__item__r_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_r_inv", "typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_FStar.UInt64.add", "typing_FStar.UInt64.mul", "typing_FStar.UInt64.sub", "typing_FStar.UInt64.uint_to_t", "typing_FStar.UInt64.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.ConstBuffer.as_qbuf", "typing_LowStar.ConstBuffer.q_preorder", "typing_LowStar.ConstBuffer.qbuf_pre", "typing_LowStar.ConstBuffer.qbuf_qual", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Vector.__proj__Vec__item__sz", "typing_MerkleTree.Low.Datastructures.hash", "typing_MerkleTree.Low.Serialization.hash_vec_bytes", "typing_MerkleTree.Low.Serialization.u64_add_fits", "typing_MerkleTree.Low.__proj__MT__item__hash_size", "typing_MerkleTree.Low.__proj__MT__item__hs", "typing_MerkleTree.Low.__proj__MT__item__mroot", "typing_MerkleTree.Low.__proj__MT__item__rhs", "typing_MerkleTree.Low.uint64_max" ], 0, "e56d6c15599db3b904d8e35fafe6473c" ], [ "MerkleTree.Low.Serialization.mt_serialize", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_LowStar.ConstBuffer.MUTABLE", "equality_tok_LowStar.ConstBuffer.MUTABLE@tok", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.q_preorder", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.ConstBuffer.qbuf_qual", "equation_LowStar.ConstBuffer.qual_of", "equation_MerkleTree.Low.const_mt_p", "equation_MerkleTree.Low.const_pointer", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3" ], 0, "6ff12944e879061ce39e557b4c33391d" ], [ "MerkleTree.Low.Serialization.mt_serialize", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "MerkleTree.Low_pretyping_ef3005027cf8c4be033bc0421455028c", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_LowStar.ConstBuffer.MUTABLE", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_LowStar.ConstBuffer.MUTABLE@tok", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Int.Cast.uint64_to_uint32", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.disjoint", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.q_preorder", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.ConstBuffer.qbuf_qual", "equation_LowStar.ConstBuffer.qual_of", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.RVector.rvector", "equation_LowStar.Regional.Instances.vector_region_of", "equation_LowStar.Regional.Instances.vector_regional", "equation_LowStar.Vector.vector", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_dummy", "equation_MerkleTree.Low.Datastructures.hash_r_inv", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "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", "equation_MerkleTree.Low.Serialization.uint64_t", "equation_MerkleTree.Low.Serialization.uint8_p", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_mt_p", "equation_MerkleTree.Low.const_pointer", "equation_MerkleTree.Low.mt_loc", "equation_MerkleTree.Low.mt_p", "equation_MerkleTree.Low.mt_safe", "equation_Prims.nat", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "kinding_MerkleTree.Low.merkle_tree@tok", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Monotonic.HyperHeap.lemma_disjoint_includes", "lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes", "lemma_FStar.Monotonic.HyperStack.lemma_map_invariant", "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "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_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_regions", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_LowStar.Regional.Rgl_r_inv", "proj_equation_LowStar.Regional.Rgl_region_of", "proj_equation_LowStar.Vector.Vec_vs", "proj_equation_MerkleTree.Low.MT_hash_size", "proj_equation_MerkleTree.Low.MT_hs", "proj_equation_MerkleTree.Low.MT_mroot", "proj_equation_MerkleTree.Low.MT_rhs", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_LowStar.Regional.Rgl_r_inv", "projection_inverse_LowStar.Regional.Rgl_region_of", "refinement_interpretation_Tm_refine_02a311be716ab03201b91cc11abde92c", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_9ff867c004d0e891d59193a1c818b2a7", "refinement_interpretation_Tm_refine_a2cc6d46f3d2c5d64a91203b6155bab3", "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_b7508c8246dd025aecf4ee8c56206add", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_LowStar.Regional.Instances.vector_region_of", "token_correspondence_LowStar.Regional.__proj__Rgl__item__r_inv", "token_correspondence_LowStar.Regional.__proj__Rgl__item__region_of", "token_correspondence_MerkleTree.Low.Datastructures.hash_r_inv", "token_correspondence_MerkleTree.Low.Datastructures.hash_vec_region_of", "typing_FStar.Monotonic.HyperHeap.disjoint", "typing_FStar.Monotonic.HyperHeap.includes", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Set.empty", "typing_FStar.Set.intersect", "typing_FStar.Set.singleton", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.ConstBuffer.as_qbuf", "typing_LowStar.ConstBuffer.q_preorder", "typing_LowStar.ConstBuffer.qbuf_pre", "typing_LowStar.ConstBuffer.qbuf_qual", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.get", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.mnull", "typing_LowStar.Vector.__proj__Vec__item__vs", "typing_MerkleTree.Low.Datastructures.hash", "typing_MerkleTree.Low.Datastructures.hash_vec", "typing_MerkleTree.Low.__proj__MT__item__hash_size", "typing_MerkleTree.Low.__proj__MT__item__hs", "typing_MerkleTree.Low.__proj__MT__item__mroot", "typing_MerkleTree.Low.__proj__MT__item__rhs", "typing_MerkleTree.Low.mt_loc" ], 0, "ad6de9ea0db38aa3ca46e39600bf157b" ], [ "MerkleTree.Low.Serialization.mt_deserialize", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.PUB@tok", "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.HyperStack.is_heap_color", "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.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer_or_null", "equation_LowStar.ConstBuffer.as_mbuf", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.Monotonic.Buffer.length", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Serialization.const_uint8_p", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_pointer", "equation_Prims.eqtype", "function_token_typing_Lib.IntTypes.byte_t", "haseqTm_refine_56b4e6db87090880a4837304bb2a2909", "int_typing", "kinding_MerkleTree.Low.merkle_tree@tok", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909", "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "typing_FStar.Ghost.reveal", "typing_FStar.Monotonic.HyperHeap.color", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperStack.is_heap_color", "typing_FStar.UInt32.t", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.ConstBuffer.as_mbuf", "typing_LowStar.ConstBuffer.as_qbuf", "typing_LowStar.ConstBuffer.qbuf_pre", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len" ], 0, "4a97c2761cea1d7e67008cd24108a854" ], [ "MerkleTree.Low.Serialization.mt_deserialize", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "equality_tok_FStar.Integers.W8@tok", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "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_LowStar.ConstBuffer.as_mbuf", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.Monotonic.Buffer.length", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Serialization.const_uint8_p", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_pointer", "function_token_typing_FStar.Integers.uint_8", "int_typing", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_075ca230542fbab87b93377fae66fe5c", "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "typing_FStar.Ghost.reveal", "typing_FStar.UInt32.v", "typing_LowStar.ConstBuffer.as_mbuf", "typing_LowStar.ConstBuffer.as_qbuf", "typing_LowStar.ConstBuffer.qbuf_pre", "typing_LowStar.Monotonic.Buffer.len" ], 0, "64cd24ab27715fcd74679c8a0a71db90" ], [ "MerkleTree.Low.Serialization.mt_deserialize", 3, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "MerkleTree.Low_pretyping_ef3005027cf8c4be033bc0421455028c", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U8", "data_typing_intro_FStar.Pervasives.Native.None@tok", "disc_equation_FStar.Pervasives.Native.None", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U8@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.Int.Cast.uint32_to_uint64", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.disjoint", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_region", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.gt", "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.gt", "equation_FStar.UInt32.gte", "equation_FStar.UInt32.lte", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer_or_null", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.ConstBuffer.as_mbuf", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.live", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.RVector.rvector", "equation_LowStar.Vector.size_of", "equation_LowStar.Vector.uint32_t", "equation_MerkleTree.Low.Datastructures.hash", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.Datastructures.hash_vec", "equation_MerkleTree.Low.Serialization.const_uint8_p", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_pointer", "equation_MerkleTree.Low.merkle_tree_conditions", "equation_MerkleTree.Low.merkle_tree_size_lg", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "int_inversion", "int_typing", "kinding_MerkleTree.Low.merkle_tree@tok", "lemma_FStar.Ghost.hide_reveal", "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_InDomUpd1", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Monotonic.HyperHeap.lemma_extends_only_parent", "lemma_FStar.Monotonic.HyperStack.lemma_map_invariant", "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "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_liveness_insensitive_buffer_weak", "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_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_LowStar.Vector.Vec_sz", "proj_equation_MerkleTree.Low.MT_hash_size", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_FStar.Pervasives.Native.None_a", "projection_inverse_MerkleTree.Low.MT_hash_size", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_075ca230542fbab87b93377fae66fe5c", "refinement_interpretation_Tm_refine_161e04719814801d293219f408210f95", "refinement_interpretation_Tm_refine_30494f3fd2c285e7cecf228074ade467", "refinement_interpretation_Tm_refine_33818f36d361a5f8bc0487fdff0c49fc", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56b4e6db87090880a4837304bb2a2909", "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df", "refinement_interpretation_Tm_refine_799df84338c1e83b596e1d04d8c7433c", "refinement_interpretation_Tm_refine_a3e91433acc705e2c7f5ab6f610b2493", "refinement_interpretation_Tm_refine_aac145f146e34cea91c3fd512c5b7261", "refinement_interpretation_Tm_refine_adba45e2c79a7a6d18ea513e3b9120dc", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cbd24d5334c6bfffa6fd8a84fb787f7a", "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc", "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b", "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909", "typing_FStar.Int.Cast.uint32_to_uint64", "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.Monotonic.HyperStack.get_tip", "typing_FStar.UInt.fits", "typing_FStar.UInt32.lte", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.ConstBuffer.as_mbuf", "typing_LowStar.ConstBuffer.as_qbuf", "typing_LowStar.ConstBuffer.length", "typing_LowStar.ConstBuffer.qbuf_pre", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.mnull", "typing_LowStar.Vector.size_of", "typing_MerkleTree.Low.Datastructures.hash" ], 0, "1aae2730c6b1b21af940e7215f72cd22" ], [ "MerkleTree.Low.Serialization.mt_serialize_path", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_LowStar.ConstBuffer.MUTABLE", "equality_tok_LowStar.ConstBuffer.MUTABLE@tok", "equation_EverCrypt.Helpers.uint32_t", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.q_preorder", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.ConstBuffer.qbuf_qual", "equation_LowStar.ConstBuffer.qual_of", "equation_MerkleTree.Low.Datastructures.hash_size_t", "equation_MerkleTree.Low.const_path_p", "equation_MerkleTree.Low.const_pointer", "equation_Prims.eqtype", "haseqTm_refine_56b4e6db87090880a4837304bb2a2909", "kinding_MerkleTree.Low.path@tok", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_bcef36c9fe2b6458c3fdda81179b025f", "typing_FStar.UInt32.t", "typing_LowStar.ConstBuffer.cast" ], 0, "60e0f1c011e151ba49061cc0ee4d9334" ], [ "MerkleTree.Low.Serialization.mt_serialize_path", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_LowStar.ConstBuffer.MUTABLE", "equality_tok_LowStar.ConstBuffer.MUTABLE@tok", "equation_FStar.Monotonic.HyperHeap.disjoint", "equation_LowStar.ConstBuffer.q_preorder", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.ConstBuffer.qbuf_qual", "equation_LowStar.ConstBuffer.qual_of", "equation_MerkleTree.Low.const_path_p", "equation_MerkleTree.Low.const_pointer", "equation_MerkleTree.Low.path_safe", "kinding_MerkleTree.Low.path@tok", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "typing_LowStar.ConstBuffer.as_qbuf", "typing_LowStar.ConstBuffer.qbuf_pre", "typing_LowStar.Monotonic.Buffer.frameOf" ], 0, "934f0c691041ca4397028cf999ee375e" ], [ "MerkleTree.Low.Serialization.mt_deserialize_path", 1, 1, 0, [ "@query" ], 0, "5f3663b9a21ca8bbb079d86ad8bab8d5" ], [ "MerkleTree.Low.Serialization.mt_deserialize_path", 2, 1, 0, [ "@query" ], 0, "ac2c1d16e54cb493fae82f0e1a07ab92" ], [ "MerkleTree.Low.Serialization.mt_deserialize_path", 3, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "MerkleTree.Low_pretyping_7e119b85ec1bddfeba5c5e23b7ab201f", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "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_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.HyperStack.ST.erid", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.disjoint", "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.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer_or_null", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.ConstBuffer.as_mbuf", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.live", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.Monotonic.Buffer.length", "equation_MerkleTree.Low.Serialization.const_uint8_p", "equation_MerkleTree.Low.Serialization.uint32_t", "equation_MerkleTree.Low.Serialization.uint8_t", "equation_MerkleTree.Low.const_pointer", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "int_inversion", "int_typing", "kinding_MerkleTree.Low.path@tok", "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_InDomUpd1", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "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_liveness_insensitive_buffer_weak", "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_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction", "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", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_075ca230542fbab87b93377fae66fe5c", "refinement_interpretation_Tm_refine_0bf64d9ba30241c6c2ada0c32b378b8c", "refinement_interpretation_Tm_refine_161e04719814801d293219f408210f95", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6c5072d4c9562dd38fd2703ecfb013df", "refinement_interpretation_Tm_refine_a3e91433acc705e2c7f5ab6f610b2493", "refinement_interpretation_Tm_refine_aac145f146e34cea91c3fd512c5b7261", "refinement_interpretation_Tm_refine_ae215dc23320c72afef105490c0b13c3", "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc", "refinement_interpretation_Tm_refine_d3f2784247189a47e567161c4f476e6f", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.ConstBuffer.as_mbuf", "typing_LowStar.ConstBuffer.as_qbuf", "typing_LowStar.ConstBuffer.qbuf_pre", "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" ], 0, "033c5eea6d266c845f219feace7925f5" ] ] ]