[ "\u000bƻ1goY;j", [ [ "Hacl.Spec.BignumQ.Mul.mask56", 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.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "3e6ebfb3a09eb6b28fd41c6ecd52cc44" ], [ "Hacl.Spec.BignumQ.Mul.mask40", 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.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "6c3e3820b0cd52908456e1ab46c90348" ], [ "Hacl.Spec.BignumQ.Mul.make_m", 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.SEC", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.BignumQ.Definitions.max56", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits1", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits5", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_18f063c2ec4382cf4aefc7b128c6b43d", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5aaca6e055c22a3765b4832b5e8b66a4", "refinement_interpretation_Tm_refine_a50f64e9be6d63b9c0a090ec6ccb675f", "refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e", "refinement_interpretation_Tm_refine_e175af5a8ddc5fffb77fad4a10b889b3", "typing_Hacl.Spec.BignumQ.Definitions.max56", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "0b6e55d9e83fc4b00ca52bf518b8f9ca" ], [ "Hacl.Spec.BignumQ.Mul.make_mu", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Ed25519.q", "int_typing", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Prims.pow2" ], 0, "2b7d2345da711cb5fc2fe6139b09f7bd" ], [ "Hacl.Spec.BignumQ.Mul.make_mu", 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.SEC", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.BignumQ.Definitions.as_nat5", "equation_Hacl.Spec.BignumQ.Definitions.max56", "equation_Hacl.Spec.BignumQ.Definitions.pow112", "equation_Hacl.Spec.BignumQ.Definitions.pow168", "equation_Hacl.Spec.BignumQ.Definitions.pow224", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits1", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits5", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Ed25519.q", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_1abb07d7d75be075a0023021cd98a69b", "refinement_interpretation_Tm_refine_2e739850431d3afa3ff5a8223f84e321", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_72e7deed3816b5a928a9ed1d5e94be4d", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_794593c6337f5c176f77bf24aa931f76", "refinement_interpretation_Tm_refine_c11b30f5d946d1589d5ccb1e81ab53ea", "typing_Hacl.Spec.BignumQ.Definitions.max56", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "d2f78b5bf0146b441e727cd78b6fc8ad" ], [ "Hacl.Spec.BignumQ.Mul.choose", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "function_token_typing_Prims.__cache_version_number__", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "ee9963b79cefd80d21bdb2b840c98ec8" ], [ "Hacl.Spec.BignumQ.Mul.subm_step", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "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_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.BignumQ.Definitions.max56", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits1", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.shift_left_lemma", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.sub_mod_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.BignumQ.Definitions.max56", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "ca6ca73eb9452c928368809a9b991456" ], [ "Hacl.Spec.BignumQ.Mul.subm_conditional", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_typing_intro_FStar.Pervasives.Native.Mktuple5@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.BignumQ.Definitions.as_nat5", "equation_Hacl.Spec.BignumQ.Definitions.max56", "equation_Hacl.Spec.BignumQ.Definitions.pow112", "equation_Hacl.Spec.BignumQ.Definitions.pow168", "equation_Hacl.Spec.BignumQ.Definitions.pow224", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Definitions.qelem5", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits1", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits5", "equation_Hacl.Spec.BignumQ.Mul.make_m", "equation_Hacl.Spec.BignumQ.Mul.subm_step", "equation_Lib.IntTypes.bits", "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", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3ae0993553c878ac2a54593109e95c5a", "refinement_interpretation_Tm_refine_43fe62832600a09c963cc175576577cf", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_b4bde97cf54f36b26323c16a35da1f99", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "typing_Hacl.Spec.BignumQ.Definitions.as_nat5", "typing_Hacl.Spec.BignumQ.Definitions.pow112", "typing_Hacl.Spec.BignumQ.Definitions.pow168", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Hacl.Spec.BignumQ.Mul.make_m", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "unit_typing" ], 0, "a8f3588581f13c543e1caadd025eef80" ], [ "Hacl.Spec.BignumQ.Mul.carry56", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "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_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Mul.mask56", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mod_mask", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.shift_left_lemma", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_69475382d3b6868fbf246fcbad1bad67", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_d96d126280e4d44b4c6d27838df6e25f", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Hacl.Spec.BignumQ.Mul.mask56", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.shift_left", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "26f6324604e793f6825e625f2e11aed8" ], [ "Hacl.Spec.BignumQ.Mul.add_modq5", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.BignumQ.Definitions.as_nat5", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_97a99675a52b4c387c2b702ed78b46df", "typing_Hacl.Spec.BignumQ.Definitions.as_nat5" ], 0, "41c743da8bb3e047647b713db1a1c552" ], [ "Hacl.Spec.BignumQ.Mul.add_modq5", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.BignumQ.Definitions.as_nat5", "equation_Hacl.Spec.BignumQ.Definitions.max56", "equation_Hacl.Spec.BignumQ.Definitions.pow112", "equation_Hacl.Spec.BignumQ.Definitions.pow168", "equation_Hacl.Spec.BignumQ.Definitions.pow224", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits1", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits5", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Spec.Ed25519.q", "int_inversion", "int_typing", "lemma_Lib.IntTypes.add_lemma", "lemma_Spec.Curve25519.Lemmas.lemma_pow2_256", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_207bd418030414c32f7ebbc47cc48626", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "typing_Hacl.Spec.BignumQ.Definitions.as_nat5", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Lib.IntTypes.v", "typing_Spec.Ed25519.q", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "80f58b32cff67e00dfe4d7d014b599db" ], [ "Hacl.Spec.BignumQ.Mul.carry56_wide", 1, 0, 0, [ "@query" ], 0, "069f3730ae4e5ba74f13a56a9593a67f" ], [ "Hacl.Spec.BignumQ.Mul.carry56_wide", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "disc_equation_Lib.IntTypes.SEC", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Mul.mask56", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mod_mask", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.shift_left_lemma", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7", "refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e", "refinement_interpretation_Tm_refine_69475382d3b6868fbf246fcbad1bad67", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_d96d126280e4d44b4c6d27838df6e25f", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Hacl.Spec.BignumQ.Mul.mask56", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.cast", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.shift_left", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "76ab2c904bd181629116e1c658215869" ], [ "Hacl.Spec.BignumQ.Mul.mul64_wide_5", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.BignumQ.Definitions.max56", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits1", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_Lib.IntTypes.mul64_wide_lemma", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Hacl.Spec.BignumQ.Definitions.max56", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "18d5f91b68231e0b6596af2fc36fb110" ], [ "Hacl.Spec.BignumQ.Mul.add2", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "lemma_Lib.IntTypes.add_mod_lemma", "primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok" ], 0, "099fce7dea78383230405207bbe0e4e6" ], [ "Hacl.Spec.BignumQ.Mul.add3", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "int_typing", "lemma_Lib.IntTypes.add_mod_lemma", "primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok" ], 0, "25560733118c49d02a1d22fb82fd96c9" ], [ "Hacl.Spec.BignumQ.Mul.add4", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "int_typing", "lemma_Lib.IntTypes.add_mod_lemma", "primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok" ], 0, "2a00d3f9219e114c76268fb4a3eb0693" ], [ "Hacl.Spec.BignumQ.Mul.add5", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "int_typing", "lemma_Lib.IntTypes.add_mod_lemma", "primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok" ], 0, "7464013a2c4c757834dd0203d2bc7e29" ], [ "Hacl.Spec.BignumQ.Mul.add_inner_carry", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "lemma_Lib.IntTypes.add_mod_lemma", "primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok" ], 0, "bde442d515e26d550cc01094939f7b72" ], [ "Hacl.Spec.BignumQ.Mul.lemma_mult_distr_3", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "986dc5bb1f5d7c3b1088a2a933c2649a" ], [ "Hacl.Spec.BignumQ.Mul.mul_5", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_typing_intro_FStar.Pervasives.Native.Mktuple10@tok", "disc_equation_Lib.IntTypes.SEC", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.BignumQ.Definitions.as_nat5", "equation_Hacl.Spec.BignumQ.Definitions.max56", "equation_Hacl.Spec.BignumQ.Definitions.pow112", "equation_Hacl.Spec.BignumQ.Definitions.pow168", "equation_Hacl.Spec.BignumQ.Definitions.pow224", "equation_Hacl.Spec.BignumQ.Definitions.pow280", "equation_Hacl.Spec.BignumQ.Definitions.pow336", "equation_Hacl.Spec.BignumQ.Definitions.pow392", "equation_Hacl.Spec.BignumQ.Definitions.pow448", "equation_Hacl.Spec.BignumQ.Definitions.pow504", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits1", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits5", "equation_Hacl.Spec.BignumQ.Definitions.qelem_wide5", "equation_Hacl.Spec.BignumQ.Definitions.qelem_wide_fits5", "equation_Hacl.Spec.BignumQ.Definitions.wide_as_nat5", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple10__1", "projection_inverse_FStar.Pervasives.Native.Mktuple10__10", "projection_inverse_FStar.Pervasives.Native.Mktuple10__2", "projection_inverse_FStar.Pervasives.Native.Mktuple10__3", "projection_inverse_FStar.Pervasives.Native.Mktuple10__4", "projection_inverse_FStar.Pervasives.Native.Mktuple10__5", "projection_inverse_FStar.Pervasives.Native.Mktuple10__6", "projection_inverse_FStar.Pervasives.Native.Mktuple10__7", "projection_inverse_FStar.Pervasives.Native.Mktuple10__8", "projection_inverse_FStar.Pervasives.Native.Mktuple10__9", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3ae0993553c878ac2a54593109e95c5a", "refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7", "refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca", "refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_b4bde97cf54f36b26323c16a35da1f99", "typing_Hacl.Spec.BignumQ.Definitions.max56", "typing_Hacl.Spec.BignumQ.Definitions.pow112", "typing_Hacl.Spec.BignumQ.Definitions.pow168", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Lib.IntTypes.cast", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "898c5c353c67bbbddeefdb449b150812" ], [ "Hacl.Spec.BignumQ.Mul.low_mul_5", 1, 0, 0, [ "@query" ], 0, "e8377420d7173e4961bbb706c47b8113" ], [ "Hacl.Spec.BignumQ.Mul.low_mul_5", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_typing_intro_FStar.Pervasives.Native.Mktuple5@tok", "disc_equation_Lib.IntTypes.SEC", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.BignumQ.Definitions.as_nat5", "equation_Hacl.Spec.BignumQ.Definitions.max56", "equation_Hacl.Spec.BignumQ.Definitions.pow112", "equation_Hacl.Spec.BignumQ.Definitions.pow168", "equation_Hacl.Spec.BignumQ.Definitions.pow224", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Definitions.qelem5", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits1", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits5", "equation_Hacl.Spec.BignumQ.Mul.carry56_wide", "equation_Hacl.Spec.BignumQ.Mul.mask40", "equation_Hacl.Spec.BignumQ.Mul.mask56", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.nonzero", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_02c7515aef59683872b048b7945272f9", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_1d075c2b4eb4555ec002539cc444233c", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3ae0993553c878ac2a54593109e95c5a", "refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7", "refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_54ad52c049613f8f3fee7e3ae9247d79", "refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e", "refinement_interpretation_Tm_refine_56f024905e54f7a7d9065c3d9ff152a1", "refinement_interpretation_Tm_refine_69475382d3b6868fbf246fcbad1bad67", "refinement_interpretation_Tm_refine_83334bd06f45f9fd691276ba5ae008c5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_aa512d78a1f26a6b89df530adc55c568", "refinement_interpretation_Tm_refine_b4bde97cf54f36b26323c16a35da1f99", "refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e", "refinement_interpretation_Tm_refine_c8b4f655312a08975d9ec949fea4e098", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.BignumQ.Definitions.max56", "typing_Hacl.Spec.BignumQ.Definitions.pow112", "typing_Hacl.Spec.BignumQ.Definitions.pow168", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Hacl.Spec.BignumQ.Mul.add2", "typing_Hacl.Spec.BignumQ.Mul.add3", "typing_Hacl.Spec.BignumQ.Mul.add4", "typing_Hacl.Spec.BignumQ.Mul.add_inner_carry", "typing_Hacl.Spec.BignumQ.Mul.carry56_wide", "typing_Hacl.Spec.BignumQ.Mul.mask40", "typing_Hacl.Spec.BignumQ.Mul.mask56", "typing_Hacl.Spec.BignumQ.Mul.mul64_wide_5", "typing_Lib.IntTypes.cast", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "715c49a090d8b8af50b8601cf8672e31" ], [ "Hacl.Spec.BignumQ.Mul.div_2_24_step", 1, 0, 0, [ "@query" ], 0, "0b417d527b632312a24e8dedd073eb3d" ], [ "Hacl.Spec.BignumQ.Mul.div_2_24_step", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "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_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mod_mask", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.shift_left_lemma", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_d96d126280e4d44b4c6d27838df6e25f", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Lib.IntTypes.logand", "typing_Lib.IntTypes.logor", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.shift_left", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "c8d6fcdd357ad66246711f737efc0130" ], [ "Hacl.Spec.BignumQ.Mul.div_248", 1, 0, 0, [ "@query" ], 0, "6db8437ddc89e6777fbae857a1f3d987" ], [ "Hacl.Spec.BignumQ.Mul.div_248", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.BignumQ.Definitions.as_nat5", "equation_Hacl.Spec.BignumQ.Definitions.max56", "equation_Hacl.Spec.BignumQ.Definitions.pow112", "equation_Hacl.Spec.BignumQ.Definitions.pow168", "equation_Hacl.Spec.BignumQ.Definitions.pow224", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits1", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits5", "equation_Hacl.Spec.BignumQ.Definitions.qelem_wide_fits5", "equation_Prims.nat", "int_inversion", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple10__10", "projection_inverse_FStar.Pervasives.Native.Mktuple10__5", "projection_inverse_FStar.Pervasives.Native.Mktuple10__6", "projection_inverse_FStar.Pervasives.Native.Mktuple10__7", "projection_inverse_FStar.Pervasives.Native.Mktuple10__8", "projection_inverse_FStar.Pervasives.Native.Mktuple10__9", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3ae0993553c878ac2a54593109e95c5a", "refinement_interpretation_Tm_refine_b4bde97cf54f36b26323c16a35da1f99", "typing_Hacl.Spec.BignumQ.Definitions.max56", "typing_Hacl.Spec.BignumQ.Definitions.pow112", "typing_Hacl.Spec.BignumQ.Definitions.pow168", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow56" ], 0, "3b4b13f2f4488fa8b7d81398d00f165a" ], [ "Hacl.Spec.BignumQ.Mul.div_2_40_step", 1, 0, 0, [ "@query" ], 0, "d7f121b1901fdbd73a3d00dba0f19371" ], [ "Hacl.Spec.BignumQ.Mul.div_2_40_step", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "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_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Mul.mask40", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mod_mask", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.shift_left_lemma", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_54ad52c049613f8f3fee7e3ae9247d79", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_d96d126280e4d44b4c6d27838df6e25f", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Hacl.Spec.BignumQ.Mul.mask40", "typing_Lib.IntTypes.logand", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.shift_left", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "7bd8c8ba7727641deb47cda7f5a5aa34" ], [ "Hacl.Spec.BignumQ.Mul.div_264", 1, 0, 0, [ "@query" ], 0, "4233955f74f683fcfc72c1542a892b47" ], [ "Hacl.Spec.BignumQ.Mul.div_264", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.BignumQ.Definitions.as_nat5", "equation_Hacl.Spec.BignumQ.Definitions.max56", "equation_Hacl.Spec.BignumQ.Definitions.pow112", "equation_Hacl.Spec.BignumQ.Definitions.pow168", "equation_Hacl.Spec.BignumQ.Definitions.pow224", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits1", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits5", "equation_Hacl.Spec.BignumQ.Definitions.qelem_wide_fits5", "equation_Prims.nat", "int_inversion", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple10__10", "projection_inverse_FStar.Pervasives.Native.Mktuple10__5", "projection_inverse_FStar.Pervasives.Native.Mktuple10__6", "projection_inverse_FStar.Pervasives.Native.Mktuple10__7", "projection_inverse_FStar.Pervasives.Native.Mktuple10__8", "projection_inverse_FStar.Pervasives.Native.Mktuple10__9", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3ae0993553c878ac2a54593109e95c5a", "refinement_interpretation_Tm_refine_b4bde97cf54f36b26323c16a35da1f99", "typing_Hacl.Spec.BignumQ.Definitions.max56", "typing_Hacl.Spec.BignumQ.Definitions.pow112", "typing_Hacl.Spec.BignumQ.Definitions.pow168", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow56" ], 0, "e6fd058d5c9f365cde3fe9e3f3bc5a2e" ], [ "Hacl.Spec.BignumQ.Mul.mod_264", 1, 0, 0, [ "@query" ], 0, "bae88a298276deca4fee74269f5315ac" ], [ "Hacl.Spec.BignumQ.Mul.mod_264", 2, 0, 0, [ "@query", "equation_Hacl.Spec.BignumQ.Mul.mask40", "projection_inverse_FStar.Pervasives.Native.Mktuple10__1", "projection_inverse_FStar.Pervasives.Native.Mktuple10__2", "projection_inverse_FStar.Pervasives.Native.Mktuple10__3", "projection_inverse_FStar.Pervasives.Native.Mktuple10__4", "projection_inverse_FStar.Pervasives.Native.Mktuple10__5" ], 0, "36e1bb6fc744f557e484cf514f7c0ae1" ], [ "Hacl.Spec.BignumQ.Mul.subm_last_step", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "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_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.shift_left_lemma", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.sub_mod_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "8af65324d8bd52aade0e5feccac8c171" ], [ "Hacl.Spec.BignumQ.Mul.sub_mod_264", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_typing_intro_FStar.Pervasives.Native.Mktuple5@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_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.BignumQ.Definitions.as_nat5", "equation_Hacl.Spec.BignumQ.Definitions.max56", "equation_Hacl.Spec.BignumQ.Definitions.pow112", "equation_Hacl.Spec.BignumQ.Definitions.pow168", "equation_Hacl.Spec.BignumQ.Definitions.pow224", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Definitions.qelem5", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits1", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits5", "equation_Hacl.Spec.BignumQ.Mul.subm_last_step", "equation_Hacl.Spec.BignumQ.Mul.subm_step", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.shift_left_lemma", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.sub_mod_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_3ae0993553c878ac2a54593109e95c5a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_b4bde97cf54f36b26323c16a35da1f99", "refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e", "refinement_interpretation_Tm_refine_d96d126280e4d44b4c6d27838df6e25f", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.BignumQ.Definitions.as_nat5", "typing_Hacl.Spec.BignumQ.Definitions.max56", "typing_Hacl.Spec.BignumQ.Definitions.pow112", "typing_Hacl.Spec.BignumQ.Definitions.pow168", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Lib.IntTypes.add", "typing_Lib.IntTypes.op_At_Percent_Dot", "typing_Lib.IntTypes.shift_left", "typing_Lib.IntTypes.sub_mod", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "7dd455dd741cae4e3050a2f3d6542516" ], [ "Hacl.Spec.BignumQ.Mul.barrett_reduction5", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Ed25519.q", "int_typing", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Prims.pow2" ], 0, "035f28d64d5d907d0d91e96639c3b1fd" ], [ "Hacl.Spec.BignumQ.Mul.barrett_reduction5", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.BignumQ.Definitions.as_nat5", "equation_Hacl.Spec.BignumQ.Definitions.max56", "equation_Hacl.Spec.BignumQ.Definitions.pow112", "equation_Hacl.Spec.BignumQ.Definitions.pow168", "equation_Hacl.Spec.BignumQ.Definitions.pow224", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits1", "equation_Hacl.Spec.BignumQ.Definitions.qelem_wide_fits5", "equation_Hacl.Spec.BignumQ.Mul.make_m", "equation_Hacl.Spec.BignumQ.Mul.make_mu", "equation_Hacl.Spec.BignumQ.Mul.mask56", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Ed25519.q", "int_inversion", "int_typing", "lemma_Lib.IntTypes.v_mk_int", "lemma_Spec.Curve25519.Lemmas.lemma_pow2_256", "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple10__1", "projection_inverse_FStar.Pervasives.Native.Mktuple10__10", "projection_inverse_FStar.Pervasives.Native.Mktuple10__2", "projection_inverse_FStar.Pervasives.Native.Mktuple10__3", "projection_inverse_FStar.Pervasives.Native.Mktuple10__4", "projection_inverse_FStar.Pervasives.Native.Mktuple10__5", "projection_inverse_FStar.Pervasives.Native.Mktuple10__6", "projection_inverse_FStar.Pervasives.Native.Mktuple10__7", "projection_inverse_FStar.Pervasives.Native.Mktuple10__8", "projection_inverse_FStar.Pervasives.Native.Mktuple10__9", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_207bd418030414c32f7ebbc47cc48626", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_43fe62832600a09c963cc175576577cf", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_69475382d3b6868fbf246fcbad1bad67", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_89fbd05d82b937dfd20f026b42e08599", "typing_Hacl.Spec.BignumQ.Definitions.as_nat5", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Hacl.Spec.BignumQ.Mul.make_m", "typing_Hacl.Spec.BignumQ.Mul.mask56", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_Spec.Ed25519.q", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "unit_typing" ], 0, "4b0c70af3df3396d74cedd56b5c1cca2" ], [ "Hacl.Spec.BignumQ.Mul.mul_modq5", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Ed25519.q", "int_typing", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Prims.pow2" ], 0, "dd3307915bce48b8945859e467532ee1" ], [ "Hacl.Spec.BignumQ.Mul.mul_modq5", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.BignumQ.Definitions.as_nat5", "equation_Prims.nat", "projection_inverse_FStar.Pervasives.Native.Mktuple10__1", "projection_inverse_FStar.Pervasives.Native.Mktuple10__10", "projection_inverse_FStar.Pervasives.Native.Mktuple10__2", "projection_inverse_FStar.Pervasives.Native.Mktuple10__3", "projection_inverse_FStar.Pervasives.Native.Mktuple10__4", "projection_inverse_FStar.Pervasives.Native.Mktuple10__5", "projection_inverse_FStar.Pervasives.Native.Mktuple10__6", "projection_inverse_FStar.Pervasives.Native.Mktuple10__7", "projection_inverse_FStar.Pervasives.Native.Mktuple10__8", "projection_inverse_FStar.Pervasives.Native.Mktuple10__9", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Hacl.Spec.BignumQ.Definitions.as_nat5" ], 0, "5be3809befcdd06fe86847f2f0a3805a" ] ] ]