MerkleTree.fsti.hints
[
"�\u0015�d\u0015>%:�E��ȷC",
[
[
"MerkleTree.mt_init_hash",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"6b46ab16711be6ce85a1a029bd73a405"
],
[
"MerkleTree.mt_free_hash",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"a2e53d3f770f1d442bf9d153c03e0e83"
],
[
"MerkleTree.mt_init_path",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"fba4e59c165cb1ecb92325fe48ba6a95"
],
[
"MerkleTree.mt_free_path",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"7b72ad66b0e5256a7cc00f38cabc3bfd"
],
[
"MerkleTree.mt_get_path_length",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"5738b365c878091c30bb626add741ccc"
],
[
"MerkleTree.mt_get_path_step",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"f510ab4b4694674e795a8ea1d2efaa5b"
],
[
"MerkleTree.mt_get_path_step_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"20f98c6ad0f4799c0ba024e131708869"
],
[
"MerkleTree.mt_create_custom",
1,
2,
1,
[
"@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",
"equation_MerkleTree.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,
"45c32afa09a9a7e461b081e1454dc669"
],
[
"MerkleTree.mt_create_custom",
2,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"a60b4ad88e0331418b11f25071de3068"
],
[
"MerkleTree.mt_free",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"d3386165790e8be1192669bcc9de198a"
],
[
"MerkleTree.mt_insert",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"8c6811bfd4efebe3842249b54228f536"
],
[
"MerkleTree.mt_insert_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"c63b43b801e56f5b16f68a70e6c2fd54"
],
[
"MerkleTree.mt_get_root",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"bb9fdf5ed459134306fa8d50dfb97f1b"
],
[
"MerkleTree.mt_get_root_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"4957c1467c6934621bc94af5e454b9f2"
],
[
"MerkleTree.mt_get_path",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"fb389226cfb8c9b0fd14b7c613e65599"
],
[
"MerkleTree.mt_get_path_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"e2f0cb28286e0af14845c0e90aef4a56"
],
[
"MerkleTree.mt_flush",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"4df16eb98897381c1e19b975e3187703"
],
[
"MerkleTree.mt_flush_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"b4714e642fd81f03e61b8dd80a34857b"
],
[
"MerkleTree.mt_flush_to",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"0632b66073a29247d52022015e85c844"
],
[
"MerkleTree.mt_flush_to_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"4f6a594374cf2dfdc817f47e417798b8"
],
[
"MerkleTree.mt_retract_to",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"734ca9a75bfd5f346087904c3a32d4fb"
],
[
"MerkleTree.mt_retract_to_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"38b633417644d658b4e973e4f1230c50"
],
[
"MerkleTree.mt_verify",
1,
2,
1,
[
"@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",
"equation_MerkleTree.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",
"refinement_kinding_Tm_refine_56b4e6db87090880a4837304bb2a2909",
"typing_FStar.Ghost.reveal"
],
0,
"c2adbb8c1c6fb788a099993ddc0fad22"
],
[
"MerkleTree.mt_verify",
2,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"523fb39c784f6cf4747b71acb6107fae"
],
[
"MerkleTree.mt_verify_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"76c428b0ec4002a1f0b83cab500b6432"
],
[
"MerkleTree.mt_serialize_size",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"1404d85ec0ec55aad511d80739c3814c"
],
[
"MerkleTree.mt_serialize",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"4879f9d0a47369e50473cde9e3ba705e"
],
[
"MerkleTree.mt_deserialize",
1,
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",
"equation_MerkleTree.hash_size_t",
"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_40154c0b4f718f98d0b1641e5cde8819",
"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,
"77da716ed83e44903d1e06c6d2eed2d1"
],
[
"MerkleTree.mt_deserialize",
2,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"7ddc3155e0cab3fe3f7a0e11ce569bcb"
],
[
"MerkleTree.mt_serialize_path",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"a8ddfe80b0e1b782cafa531caf8aa8a7"
],
[
"MerkleTree.mt_deserialize_path",
1,
2,
1,
[ "@query" ],
0,
"c4fe3df9220491bfcb6bd7b75d3bfb69"
],
[
"MerkleTree.mt_deserialize_path",
2,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"0b161fb670575b618048e98772eb700c"
]
]
]