[ "p)šÆlæ.Ò`aãÕ®+.D", [ [ "Hacl.Bignum.bn_add1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_4fe0f7e228a856d0575495f6b377ee05", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "49fce80c9501ea0f7e586a0bfc32bbe7" ], [ "Hacl.Bignum.bn_sub1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_4fe0f7e228a856d0575495f6b377ee05", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "cc3909b3e888598f8d7555f3736326f9" ], [ "Hacl.Bignum.bn_add_eq_len_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "0b616e0b096f2c65cce94df13fa0fa49" ], [ "Hacl.Bignum.bn_sub_eq_len_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "26a9c853cfb319ccc0b69bfda4f653b1" ], [ "Hacl.Bignum.bn_add", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_dd894954154c0efc25ea48b66d8a9bbf", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "465f0c22e2c3bc257d98d96ca2a2a790" ], [ "Hacl.Bignum.bn_sub", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_dd894954154c0efc25ea48b66d8a9bbf", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "12cc51508fbf7cf31873ac23041317d0" ], [ "Hacl.Bignum.bn_reduce_once", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "af13db8471df4868cd64036ae7f23e35" ], [ "Hacl.Bignum.bn_add_mod_n_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "ed8463439749d3e395506f9b21a5cb8f" ], [ "Hacl.Bignum.bn_sub_mod_n_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "611f155cc5a0c67ae5790dde82209b65" ], [ "Hacl.Bignum.bn_mul1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "e4e8dfdfb627f76a371dd6ec28cf986e" ], [ "Hacl.Bignum.bn_karatsuba_mul_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_692121769a46bb8926d59b8ca3cd043a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "70c36fe23b07abca0d4d96f09081811a" ], [ "Hacl.Bignum.bn_mul_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2f1e932fa1e93c406800b418feeca6e3", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "ea6aa5b64a7523baa4ab43bc633fe848" ], [ "Hacl.Bignum.bn_karatsuba_sqr_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_692121769a46bb8926d59b8ca3cd043a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "4b62a4b32508037e1da8079756b89c8f" ], [ "Hacl.Bignum.bn_sqr_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_ad5c1623934a11c8d7877f0adfe0f6fc", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "ea5983901975de1e466248ee700eb71f" ], [ "Hacl.Bignum.bn_mul1_lshift_add_in_place", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_65c10f95049b68e16da55bde39a0ae86", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f313c5ebe0c62e04ca31eaab5f5c2839" ], [ "Hacl.Bignum.bn_rshift", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "function_token_typing_Lib.IntTypes.uint64", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f2cf9e6acf029a019e710f5cba6ade26" ], [ "Hacl.Bignum.bn_sub_mask", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "fc37637e174c302efb6f06d298b189e8" ], [ "Hacl.Bignum.bn_get_ith_bit", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_20041da81ea68980c160f95ec3014015", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "fc95df26888e1881a035951054432116" ], [ "Hacl.Bignum.bn_get_bits", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "refinement_interpretation_Tm_refine_26063e8f5832ae97bf1d9753b5b741be", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "c445834c27b5d30667a9ae363ef1a05b" ], [ "Hacl.Bignum.bn_set_ith_bit", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_20041da81ea68980c160f95ec3014015", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "64cd5ebecc7398863ac7e610d11ce3b9" ], [ "Hacl.Bignum.cswap2", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "75b829ab7949d8c053706f884b5ea0be" ], [ "Hacl.Bignum.bn", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Bignum.meta_len", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_06eb4f1fa9612b97cc2b633a94839814", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "d0cc553286fcd38fe71bacdfa022a3a9" ], [ "Hacl.Bignum.__proj__Mkbn__item__add", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "proj_equation_Hacl.Bignum.Mkbn_len", "projection_inverse_Hacl.Bignum.Mkbn_len", "refinement_interpretation_Tm_refine_6740e6b39a1a59b2160f9c68c24e3a76", "refinement_interpretation_Tm_refine_b704b54cd4b720c3c05be1fd667649db" ], 0, "994b7d2c1a0fb318e2b66b3e1700dce4" ], [ "Hacl.Bignum.__proj__Mkbn__item__sub", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "proj_equation_Hacl.Bignum.Mkbn_len", "projection_inverse_Hacl.Bignum.Mkbn_len", "refinement_interpretation_Tm_refine_6740e6b39a1a59b2160f9c68c24e3a76", "refinement_interpretation_Tm_refine_b704b54cd4b720c3c05be1fd667649db" ], 0, "99c769523e38a55644316ca7a748caa0" ], [ "Hacl.Bignum.__proj__Mkbn__item__add_mod_n", 1, 0, 0, [ "@query" ], 0, "2955d414517f147ba98c47e59909aa14" ], [ "Hacl.Bignum.__proj__Mkbn__item__add_mod_n", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "proj_equation_Hacl.Bignum.Mkbn_len", "projection_inverse_Hacl.Bignum.Mkbn_len", "refinement_interpretation_Tm_refine_825fe1ce5d530067039356208bd82ad4", "refinement_interpretation_Tm_refine_e0ab8a8974e5b3a9101c38b7001ed683" ], 0, "3826308481439fa5b5793fefe434e152" ], [ "Hacl.Bignum.__proj__Mkbn__item__sub_mod_n", 1, 0, 0, [ "@query" ], 0, "7992e3476188c9ab2e07cda13903b61a" ], [ "Hacl.Bignum.__proj__Mkbn__item__sub_mod_n", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "proj_equation_Hacl.Bignum.Mkbn_len", "projection_inverse_Hacl.Bignum.Mkbn_len", "refinement_interpretation_Tm_refine_825fe1ce5d530067039356208bd82ad4", "refinement_interpretation_Tm_refine_e0ab8a8974e5b3a9101c38b7001ed683" ], 0, "808ebd11abff6cc2fc02e0d1d71e0b0e" ], [ "Hacl.Bignum.__proj__Mkbn__item__mul", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92" ], 0, "bf769aacfe2e1d2b2eb6477422be903b" ], [ "Hacl.Bignum.__proj__Mkbn__item__mul", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "fuel_guarded_inversion_Hacl.Bignum.bn", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Hacl.Bignum.Mkbn_len", "projection_inverse_BoxInt_proj_0", "projection_inverse_Hacl.Bignum.Mkbn_len", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6065f173033e10a9ea94570e4e669b17", "refinement_interpretation_Tm_refine_81c7ef7d641d62c76efdc13fe91209b8", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "1604a5b8abef25ccbac60ca44bf49430" ], [ "Hacl.Bignum.__proj__Mkbn__item__sqr", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92" ], 0, "50bb592a1332a78282181bc4f1c05735" ], [ "Hacl.Bignum.__proj__Mkbn__item__sqr", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "fuel_guarded_inversion_Hacl.Bignum.bn", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Hacl.Bignum.Mkbn_len", "projection_inverse_BoxInt_proj_0", "projection_inverse_Hacl.Bignum.Mkbn_len", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f702b2e94467d77d49334956a3ab0680" ], [ "Hacl.Bignum.add_mod_n", 1, 0, 0, [ "@query" ], 0, "2267272040dc996ba36cb9dd227e7463" ], [ "Hacl.Bignum.sub_mod_n", 1, 0, 0, [ "@query" ], 0, "876cb83933d2eb0ad16aebbe8022f02e" ], [ "Hacl.Bignum.mul", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92" ], 0, "b0c13896676391d32aa674a87f015ded" ], [ "Hacl.Bignum.sqr", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92" ], 0, "c4c4b0e9ae4dc18137d68482b49a9e16" ], [ "Hacl.Bignum.bn_is_odd", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947" ], 0, "1654f1914367624a48378722749a7ee1" ], [ "Hacl.Bignum.bn_eq_mask_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_tok_Lib.Buffer.MUT@tok" ], 0, "19ef5576251c89c1e1faf3e6210721c8" ], [ "Hacl.Bignum.bn_is_zero_mask", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947" ], 0, "4e02418a960e123194d3f19180d04b4e" ], [ "Hacl.Bignum.bn_lt_mask_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_tok_Lib.Buffer.MUT@tok" ], 0, "aa96630edd1e9c1180aa7e8da8addac5" ], [ "Hacl.Bignum.bn_lt_pow2_mask", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_33847aeea1e1f6a30128d1c29277c83f", "refinement_interpretation_Tm_refine_4f32bc7da14f02bd3360820d3a0b92a4", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "4ea32c50ef98b39717860456fa2a18fb" ], [ "Hacl.Bignum.bn_gt_pow2_mask", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_33847aeea1e1f6a30128d1c29277c83f", "refinement_interpretation_Tm_refine_4f32bc7da14f02bd3360820d3a0b92a4", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "fd59208e43d8a702be7f4dc7053c795b" ], [ "Hacl.Bignum.bn_from_uint", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_4fe0f7e228a856d0575495f6b377ee05", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "72717fb9cb49584f70f20658e4b5589d" ], [ "Hacl.Bignum.bn_from_bytes_be", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.blocks", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56718590fe22c020c437a3dfde0cee6b", "refinement_interpretation_Tm_refine_834039b9477f844fb4d2de05cf4e8b52", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.numbytes", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "daaa6d5504785fc8228a16738c60e322" ], [ "Hacl.Bignum.bn_to_bytes_be", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.blocks", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_3b30e5cbbdc74f89ea2da23758cc9b99", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56718590fe22c020c437a3dfde0cee6b", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Hacl.Bignum.Definitions.blocks", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.numbytes", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "16441e480386b7d4e82fb9edeb3327d5" ], [ "Hacl.Bignum.bn_from_bytes_le", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.blocks", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56718590fe22c020c437a3dfde0cee6b", "refinement_interpretation_Tm_refine_834039b9477f844fb4d2de05cf4e8b52", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.numbytes", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "6bfb70120ae2361836a70bd8612435ae" ], [ "Hacl.Bignum.bn_to_bytes_le", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.blocks", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_3b30e5cbbdc74f89ea2da23758cc9b99", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56718590fe22c020c437a3dfde0cee6b", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Hacl.Bignum.Definitions.blocks", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.numbytes", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "c79cad07e31b6d819b364ab8f192ec47" ] ] ]