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