Revision 493d130bb523940efde89a74951e7a449fec93b0 authored by Aymeric Fromherz on 24 March 2020, 14:39:08 UTC, committed by Aymeric Fromherz on 24 March 2020, 14:39:08 UTC
Hacl.Spec.BignumQ.Mul.fst.hints
[
"\u000b�ƻ1�g�o��Y;��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,
"748e17877a6d2bfec4696af3fdd2ca40"
],
[
"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,
"7a6582518414791cc16b8fc5d3f08043"
],
[
"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,
"0d9a5140aa611219d40d1fe8f8b017bc"
],
[
"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,
"f80c0d1ee6d82fc69e3badfc4999e8b2"
],
[
"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,
"bdb9a7ea6645056680766c4e1768ca2f"
],
[
"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,
"87460a81fba3bf9edf190bcbccc7b509"
],
[
"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_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_c6c18a7ceb46d419c35ff8551117551e",
"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.pow56",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"8206ac23e366500ffc2d42be542b04fb"
],
[
"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,
"16169791a73235a348dc6a536b876116"
],
[
"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", "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_1cc58e901e83e96dff5b4d1682343605",
"refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea",
"refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_69475382d3b6868fbf246fcbad1bad67",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e",
"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_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"e852c3ec4a080139ec90ff4152def0aa"
],
[
"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,
"21f2b44821b7284d83a4cd4342f45651"
],
[
"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,
"d44cb6bfe22684b8421c96d3833dca12"
],
[
"Hacl.Spec.BignumQ.Mul.carry56_wide",
1,
0,
0,
[ "@query" ],
0,
"da12b511a059d5cee93e9ab2c832ebbc"
],
[
"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_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_c6c18a7ceb46d419c35ff8551117551e",
"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,
"df4ac60dac2849408d7b4bc3d49396ba"
],
[
"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,
"417c8d776fe36c3bfd29f17b0adf0851"
],
[
"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,
"8397352a2923dac3a72d53926701c36d"
],
[
"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,
"7e4247c99c3966b1dfa122201b842139"
],
[
"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,
"6ecb0c5517074324192501df5750102c"
],
[
"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,
"276054ffc82ffc030bf9f0b4de11e129"
],
[
"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,
"804418d0f72688eec2b85e52417a7e41"
],
[
"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,
"fabc4454622ffa62e619c72a335f7aa2"
],
[
"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,
"392a07c97cc3950c57c3469480ae8d3e"
],
[
"Hacl.Spec.BignumQ.Mul.low_mul_5",
1,
0,
0,
[ "@query" ],
0,
"d566051ca2858418e3bc2dd81cdad63e"
],
[
"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,
"4cbb0e8243c6ec40db8635d460d53f72"
],
[
"Hacl.Spec.BignumQ.Mul.div_2_24_step",
1,
0,
0,
[ "@query" ],
0,
"97d371e4515ae64bfb14a19b3237c502"
],
[
"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_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_c6c18a7ceb46d419c35ff8551117551e",
"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,
"a6d4aa101956412fe1ed6d996b676dcc"
],
[
"Hacl.Spec.BignumQ.Mul.div_248",
1,
0,
0,
[ "@query" ],
0,
"ed24ec91e57798389a1aae2c41edfd2b"
],
[
"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,
"e5cab20cd2a607dd911106c8c1a74837"
],
[
"Hacl.Spec.BignumQ.Mul.div_2_40_step",
1,
0,
0,
[ "@query" ],
0,
"c38afb55b3c63d26c9f9378cdbdf07de"
],
[
"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_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_c6c18a7ceb46d419c35ff8551117551e",
"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,
"6154657185119564d5eedef7e4b8cd7d"
],
[
"Hacl.Spec.BignumQ.Mul.div_264",
1,
0,
0,
[ "@query" ],
0,
"0fc854a9607c9fc1bb9b074ef2de99e3"
],
[
"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,
"04b69e0ec0ee6eb1efa66f7d665f89a0"
],
[
"Hacl.Spec.BignumQ.Mul.mod_264",
1,
0,
0,
[ "@query" ],
0,
"e418f74693a4cbccd218e7c8c8f0e9de"
],
[
"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,
"fd4c591cdcdf4072244a808f6b498265"
],
[
"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",
"lemma_Lib.IntTypes.v_injective", "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_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_c6c18a7ceb46d419c35ff8551117551e",
"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,
"4aa1e8040256c8d958b455d85ef92772"
],
[
"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,
"76944bd892c69dff64e5853e9c6cfe2c"
],
[
"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,
"d8b6b73c1dbb62119f8394734e928b62"
],
[
"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,
"2a794f8cfd437fa669e262a4615dbbdb"
],
[
"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,
"a9cee02e57f338153aadfd445a63ab9a"
],
[
"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,
"4fd3e1f358750d68f95214832cf7986e"
]
]
]
Computing file changes ...
