Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
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,
"65539d98825fa13d5075b792ab6297ff"
],
[
"MerkleTree.mt_free_hash",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"0660799a0899149d86d065f07a10edef"
],
[
"MerkleTree.mt_init_path",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"535fbeb1390795a215b2d7d3138f952a"
],
[
"MerkleTree.mt_free_path",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"f463e04b0e6a84f75d157cf4c91dda19"
],
[
"MerkleTree.mt_get_path_length",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"261798e46130042a341abc6a1eac66ff"
],
[
"MerkleTree.mt_get_path_step",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"13664153c4824b5f771404a9b626e6c9"
],
[
"MerkleTree.mt_get_path_step_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"e97b8dbefa99abf8e0006d9b953692ed"
],
[
"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,
"12f30711e59bb12904275a603e167ab7"
],
[
"MerkleTree.mt_create_custom",
2,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"602d53011a0a5cb010ec5a23122b5c8a"
],
[
"MerkleTree.mt_free",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"70fe5bd9b5d1a413cb730e6e200d8792"
],
[
"MerkleTree.mt_insert",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"3f0cff8eee62fc566cfc568cf5612d96"
],
[
"MerkleTree.mt_insert_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"7787671bd2535749709510f668da2989"
],
[
"MerkleTree.mt_get_root",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"9a5f65a50185e025fd76ea58d139b956"
],
[
"MerkleTree.mt_get_root_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"3a42f59cbaf6b40ddfa7f978c320f9a6"
],
[
"MerkleTree.mt_get_path",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"9896c99152cb10db01db68ede2214860"
],
[
"MerkleTree.mt_get_path_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"46bf344ca6c602edd1903ddc8a9050e4"
],
[
"MerkleTree.mt_flush",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"5795dfa647c7eec54ae9ffdd49ef0584"
],
[
"MerkleTree.mt_flush_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"f9a4d5ebfcbe808af3a5ca828463e7b2"
],
[
"MerkleTree.mt_flush_to",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"32d6ce119ea83a3b4ae4a5d8208fccb2"
],
[
"MerkleTree.mt_flush_to_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"1ff511b962a1187f1372763febb27933"
],
[
"MerkleTree.mt_retract_to",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"aef4de81f653a277f4fa1193eec4f543"
],
[
"MerkleTree.mt_retract_to_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"e2d38c5ba859b0fb49baa18b81509e64"
],
[
"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,
"6b53cec1d1cf48a7bbbae2384fc63650"
],
[
"MerkleTree.mt_verify",
2,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"9efd761b94db3ad2e4921242e292d790"
],
[
"MerkleTree.mt_verify_pre",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"e26a8eee23a676d2458b37323c5b91e0"
],
[
"MerkleTree.mt_serialize_size",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"887aa0d024cfd750787332016b073e16"
],
[
"MerkleTree.mt_serialize",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"abde880af2e37c8cc7c5b9391ae030ac"
],
[
"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,
"4d7cd46becb81df22d5fadc1043b2e3f"
],
[
"MerkleTree.mt_deserialize",
2,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"1e5312e74e2323601d0e43888d66c391"
],
[
"MerkleTree.mt_serialize_path",
1,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"ce4f28ba498a44ffb7cbf09953dc9a1c"
],
[
"MerkleTree.mt_deserialize_path",
1,
2,
1,
[ "@query" ],
0,
"e822c144dd96963a0f0e2d1069390904"
],
[
"MerkleTree.mt_deserialize_path",
2,
2,
1,
[
"@query", "equation_FStar.Monotonic.HyperStack.mem",
"equation_MerkleTree.pf"
],
0,
"08c1ed1a093e015d6f81a2d0ea16faa4"
]
]
]
Computing file changes ...
