[ "s—ÙЋ¦\u001f´Ð¸5Ó¥Ms?", [ [ "Hacl.Spec.BignumQ.Lemmas.feq", 1, 0, 0, [ "@query" ], 0, "b52ed3e60e20d93a5a1fe96ae5baa85f" ], [ "Hacl.Spec.BignumQ.Lemmas.eq_eq2", 1, 0, 0, [ "@query" ], 0, "f6290ef3030b39e591e8e8993b202c87" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mul_lt", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "7f9866e56c7048f3e8d6769e6ca2b4e4" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_as_nat5", 1, 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_Prims.nat", "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_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow56" ], 0, "ceef669459d7d33c3aa8a681891d262a" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_choose_step", 1, 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_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", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_f41f4015e22b272c5f61be9cc1570311", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "5a0b019ea844ae81f23bc1855ba82ed4" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_choose_step", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b", "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", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "function_token_typing_Lib.IntTypes.logand", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.sub_mod_lemma", "lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_cde1a45129380071fe620b72e00a03d7", "refinement_interpretation_Tm_refine_f41f4015e22b272c5f61be9cc1570311", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.logand", "typing_Lib.IntTypes.logxor", "typing_Lib.IntTypes.maxint", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "f0e9849f305dd6cc6cd898eb307a0144" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_subm_conditional", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, "db57a9036a06688aea4fab26f2aec31c" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div224", 1, 0, 0, [ "@query" ], 0, "9446e108699dff8dd258d26bce1a46d8" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div224", 2, 0, 0, [ "@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.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_wide_fits5", "equation_Hacl.Spec.BignumQ.Definitions.wide_as_nat5", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "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", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3ae0993553c878ac2a54593109e95c5a", "refinement_interpretation_Tm_refine_536778a75b4d7e28377dd170a08c019c", "refinement_interpretation_Tm_refine_537f796f66502bfab3d6bd4b61276d25", "refinement_interpretation_Tm_refine_770ab0bf9753aca6d20d9059a1d1935b", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_a8e17d3fd9b9936473002842f6275029", "refinement_interpretation_Tm_refine_ae79de13405c58c32c9304d0fb36a891", "refinement_interpretation_Tm_refine_b4bde97cf54f36b26323c16a35da1f99", "typing_Hacl.Spec.BignumQ.Definitions.pow112", "typing_Hacl.Spec.BignumQ.Definitions.pow168", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow280", "typing_Hacl.Spec.BignumQ.Definitions.pow336", "typing_Hacl.Spec.BignumQ.Definitions.pow392", "typing_Hacl.Spec.BignumQ.Definitions.pow448", "typing_Hacl.Spec.BignumQ.Definitions.pow504", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "fe2bcae65d31f1150e8d57abfb136397" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_aux", 1, 0, 0, [ "@query" ], 0, "62a2f63503d47a5dd28fd5322db32204" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_aux", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U64", "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.pow56", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.nonzero", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Spec.Curve25519.Lemmas.lemma_pow2_256", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Multiply", "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", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3ae0993553c878ac2a54593109e95c5a", "refinement_interpretation_Tm_refine_536778a75b4d7e28377dd170a08c019c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_b4bde97cf54f36b26323c16a35da1f99", "typing_Hacl.Spec.BignumQ.Definitions.pow112", "typing_Hacl.Spec.BignumQ.Definitions.pow168", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow280", "typing_Hacl.Spec.BignumQ.Definitions.pow56" ], 0, "036d37c3752e319d5386556581714561" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_aux", 3, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Hacl.Spec.BignumQ.Definitions.pow224", "equation_Prims.nonzero", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "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", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "typing_Hacl.Spec.BignumQ.Definitions.pow224" ], 0, "7e0ab1df87fc3890e121f90d14d30b61" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x5", 1, 0, 0, [ "@query" ], 0, "17fdef7547c68f96971323f1912ac310" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x5", 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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "b6f10bf6d5fa0bdce30d09ec63a16b82" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x6", 1, 0, 0, [ "@query" ], 0, "45f2c88b9745c6ecfd978a06834b8984" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x6", 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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "7fef4cdab77eb8f29d2fa80e41b5b7d3" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x6", 3, 0, 0, [ "@query" ], 0, "50b82452e565a41972adfa80b965d136" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x6", 4, 0, 0, [ "@query" ], 0, "c80d32846933214ef798defcecaa894c" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x6", 5, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "1f60e71e39632d1a350f71593d0d0fbc" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x6", 6, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "d725919353026c29c8e1aeae21c8f693" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x7", 1, 0, 0, [ "@query" ], 0, "bd660f5ff5e2bc2c41ea6a3f80b499ea" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x7", 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.U64@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "ec6ca18c28f52efaf841046adcb921f3" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x7", 3, 0, 0, [ "@query" ], 0, "607503252f181b2501c2c51ea70c6608" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x7", 4, 0, 0, [ "@query" ], 0, "762931bd599074ebf43608c2e51dcabc" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x7", 5, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "dc3e70c4c97abda8799865531170c51a" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x7", 6, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "635b310f9bdc9d51401fc9910bf91c7f" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x8", 1, 0, 0, [ "@query" ], 0, "8b2faf1fa5a6d821deb7aa95d246de9b" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x8", 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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "6520c7d0c46f62f4a6e89c1377345d50" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x8", 3, 0, 0, [ "@query" ], 0, "f31fa958f01249050474a55e3e047b78" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x8", 4, 0, 0, [ "@query" ], 0, "f73c4d56a44bb32f3f04944de9daec30" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x8", 5, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "6800e6a836436dffad13a2d05ce5a9b8" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x8", 6, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "e4b29d914f1c19f597dd390503602e37" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x9", 1, 0, 0, [ "@query" ], 0, "6dc20d1422214f4773197805d736f8da" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x9", 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_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Spec.Curve25519.Lemmas.lemma_pow2_256", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_a6e66cc87c9c29f23f71f89c04a9f0d2", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "f96962c0080e7582e7eb9da09092b05a" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x9", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.PUB", "disc_equation_Lib.IntTypes.SEC", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U16", "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "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_Lib.IntTypes.v", "equation_Prims.nat", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_a6e66cc87c9c29f23f71f89c04a9f0d2", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "6cf6f366852b9b8453746f5eb6f4aaf5" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248_x9", 4, 0, 0, [ "@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_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_a6e66cc87c9c29f23f71f89c04a9f0d2", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "2428ef5d07a34c7629ec509da6e106d8" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_wide_as_nat_pow512", 1, 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.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.wide_as_nat5", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "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", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_a8e17d3fd9b9936473002842f6275029", "typing_Hacl.Spec.BignumQ.Definitions.pow504", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "d90ce37254f5870835feae5364796b3e" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "503292e51e85c33abdeaf03da313e4dd" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "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_Prims.nonzero", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "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", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "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.pow112", "typing_Hacl.Spec.BignumQ.Definitions.pow168", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow56" ], 0, "d15fac389985d893f5eac00dbf980460" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248", 3, 0, 0, [ "@query" ], 0, "58f5d2940d28906e3b4bd50e9f4e7131" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248", 4, 0, 0, [ "@query" ], 0, "8e8feb9f47bf1c4ee464ec94eb57c85d" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248", 5, 0, 0, [ "@query" ], 0, "60e3c75de41cdb06e1c58f6618aba3c9" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248", 6, 0, 0, [ "@query" ], 0, "6edd69fceb35d0e9b715f9cb7a67d6f6" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248", 7, 0, 0, [ "@query" ], 0, "e39898fa4472c58b0b9e15f1ccd24240" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248", 8, 0, 0, [ "@query" ], 0, "06e56ee90cd82555b732a331a876dd39" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248", 9, 0, 0, [ "@query" ], 0, "a81289db74177de1e8156f37bbeda886" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248", 10, 0, 0, [ "@query" ], 0, "a0d32f347d647ff2485cbc3da9de9347" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248", 11, 0, 0, [ "@query" ], 0, "b0747dfd313b30bd91e56bc63c331f58" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248", 12, 0, 0, [ "@MaxIFuel_assumption", "@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.U64", "disc_equation_Lib.IntTypes.PUB", "disc_equation_Lib.IntTypes.SEC", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U16", "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.nonzero", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.sec_int_v", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "43c60eca1928ad667ce01abcb2ef7bd3" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div248", 13, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nonzero", "int_inversion", "primitive_Prims.op_Addition", "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", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "57eac78fdf5302d69c15879700822785" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_add_modq5", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "eq2-interp", "equation_Hacl.Spec.BignumQ.Definitions.as_nat5", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.squash", "l_and-interp", "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Hacl.Spec.BignumQ.Definitions.as_nat5" ], 0, "0b6a81a097d31babac54287fbeddbbc5" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_add_modq5", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits1", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits5", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Ed25519.q", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Prims.pow2" ], 0, "f495f30cb7e27e6ac299c2e44d937ff5" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_wide_as_nat_pow528", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "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.wide_as_nat5", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "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", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_a8e17d3fd9b9936473002842f6275029", "typing_Hacl.Spec.BignumQ.Definitions.pow504", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "55d8eaa4a175ea1fd41cb3bc402304a1" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_aux", 1, 0, 0, [ "@query" ], 0, "e95acde94eb2ef74bedd5ea0340df9ee" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_aux", 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", "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.pow448", "equation_Hacl.Spec.BignumQ.Definitions.pow504", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.nonzero", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "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", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3ae0993553c878ac2a54593109e95c5a", "refinement_interpretation_Tm_refine_536778a75b4d7e28377dd170a08c019c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_b4bde97cf54f36b26323c16a35da1f99", "typing_Hacl.Spec.BignumQ.Definitions.pow112", "typing_Hacl.Spec.BignumQ.Definitions.pow168", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow280", "typing_Hacl.Spec.BignumQ.Definitions.pow56" ], 0, "db21942cc20d0d34221f917ef9142cc0" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_aux", 3, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Hacl.Spec.BignumQ.Definitions.pow224", "equation_Prims.nonzero", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Multiply", "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", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "typing_Hacl.Spec.BignumQ.Definitions.pow224" ], 0, "7f4a93a0da264f3f8f3c4cd4c6a12f9f" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x5", 1, 0, 0, [ "@query" ], 0, "5c035341d7a70d424f05390d15473ff1" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x5", 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_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Prims.pow2" ], 0, "62999727cd278875e04f752b2d7a3524" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x5", 3, 0, 0, [ "@query" ], 0, "8f4103bb86c88e875dc6fc767489cbbb" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x5", 4, 0, 0, [ "@query" ], 0, "c389665add73c332d7e12dfe677ef4b6" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x5", 5, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "fb616dfffc15ec80916519c0fcf9ae47" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x5", 6, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "633a1ee8ef68128b8aba7b5ed13fb133" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x6", 1, 0, 0, [ "@query" ], 0, "22499c94a1816d77117e40c38ba8e5c2" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x6", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, "0afe149e4477c0c44ee104200db4d152" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x6", 3, 0, 0, [ "@query" ], 0, "be9b7bcb947df2c3b4fa86c3416db381" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x6", 4, 0, 0, [ "@query" ], 0, "c4bb64f295fe14e8d2b83f4ce6f5bd79" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x6", 5, 0, 0, [ "@MaxIFuel_assumption", "@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.U64", "disc_equation_Lib.IntTypes.PUB", "disc_equation_Lib.IntTypes.SEC", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U16", "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.nonzero", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.sec_int_v", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "7cb67a084d406b0098c33fbc9d50dd9a" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x6", 6, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "db73f90bee73248bd8d178763f89a647" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x7", 1, 0, 0, [ "@query" ], 0, "e1c6ea29e2a4e24b737d21490f2524f1" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x7", 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_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Prims.pow2" ], 0, "5529b4f713599ba22e2c7d659d0c51d4" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x7", 3, 0, 0, [ "@query" ], 0, "f23d2ff488bc64a968335d0e60d1dffb" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x7", 4, 0, 0, [ "@query" ], 0, "4069e25cd4c471f489f6764c260f802a" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x7", 5, 0, 0, [ "@MaxIFuel_assumption", "@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.U64", "disc_equation_Lib.IntTypes.PUB", "disc_equation_Lib.IntTypes.SEC", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U16", "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.nonzero", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.sec_int_v", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "4fe59b9f5e2aec541981b5ea6455de51" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x7", 6, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "0ea5c6d1f5b5ac31bb90f7038b4eb82e" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x8", 1, 0, 0, [ "@query" ], 0, "1fcdcfac51251ba46df453f4a7356fa9" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x8", 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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "68f82626b8bbace4ccb3e364c47a52e9" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x8", 3, 0, 0, [ "@query" ], 0, "ee29e5f7b18c08488ac995e55cf51844" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x8", 4, 0, 0, [ "@query" ], 0, "1c7c1983d3c37592789f78824f672384" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x8", 5, 0, 0, [ "@MaxIFuel_assumption", "@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.U64", "disc_equation_Lib.IntTypes.PUB", "disc_equation_Lib.IntTypes.SEC", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U16", "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.nonzero", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.sec_int_v", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "cda021491524e2a54e70d77fdc84b267" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x8", 6, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "fb2810b48be478d81e2dd1e1605cf7ee" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x9", 1, 0, 0, [ "@query" ], 0, "acc12dfc011fc4ebee08c9764d2ad760" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x9", 2, 0, 0, [ "@query", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, "c240448ccb4f7c8cc68d3428cc8fd955" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x9", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.PUB", "disc_equation_Lib.IntTypes.SEC", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U16", "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "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_Lib.IntTypes.v", "equation_Prims.nat", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_65e6e95777845e3a6b1720c178cb1ea5", "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, "f33b60713547d45a41d87c002236d8c1" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264_x9", 4, 0, 0, [ "@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_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_65e6e95777845e3a6b1720c178cb1ea5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "9fb33f21329c73d28ba6d4af6fd75005" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "c81952e6ffc9936cb07accfbc913727e" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "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_Prims.nonzero", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "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", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "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.pow112", "typing_Hacl.Spec.BignumQ.Definitions.pow168", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow56" ], 0, "085bf942cde3c2675159ea0e754d4484" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264", 3, 0, 0, [ "@query" ], 0, "dc79e9eb6663c50a0375815c9e6e86d0" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264", 4, 0, 0, [ "@query" ], 0, "e1b820a55182abf9c389858b3921ce4a" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264", 5, 0, 0, [ "@query" ], 0, "37b73ebb15af591f03e2eb6a4ba24813" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264", 6, 0, 0, [ "@query" ], 0, "b0280a06606e7a0de541f8987c1282af" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264", 7, 0, 0, [ "@query" ], 0, "60bc808077e1e59d96a2719a56cea27a" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264", 8, 0, 0, [ "@query" ], 0, "236b7a2506b8ba0abef347922d06a1a4" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264", 9, 0, 0, [ "@query" ], 0, "405276f3169efe2fa2177739943e1f17" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264", 10, 0, 0, [ "@query" ], 0, "f98209fe2cb5db2c56b30dc0996a8467" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264", 11, 0, 0, [ "@query" ], 0, "9e1f6488f3897fdc0c7c6d1ce25efde4" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264", 12, 0, 0, [ "@MaxIFuel_assumption", "@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.U64", "disc_equation_Lib.IntTypes.PUB", "disc_equation_Lib.IntTypes.SEC", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U16", "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.nonzero", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.sec_int_v", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "34929b8bdfcb06d191c347057f145374" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div264", 13, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nonzero", "int_inversion", "primitive_Prims.op_Addition", "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", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "4098964f8f9a6f1da71df703c92bb474" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mod_264_aux", 1, 0, 0, [ "@query" ], 0, "24038e72af2024c6b6291d65d25dc7d5" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mod_264_aux", 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.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.wide_as_nat5", "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.nonzero", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_4", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "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", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3ae0993553c878ac2a54593109e95c5a", "refinement_interpretation_Tm_refine_536778a75b4d7e28377dd170a08c019c", "refinement_interpretation_Tm_refine_537f796f66502bfab3d6bd4b61276d25", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_770ab0bf9753aca6d20d9059a1d1935b", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_a8e17d3fd9b9936473002842f6275029", "refinement_interpretation_Tm_refine_b4bde97cf54f36b26323c16a35da1f99", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_Hacl.Spec.BignumQ.Definitions.pow112", "typing_Hacl.Spec.BignumQ.Definitions.pow168", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow280", "typing_Hacl.Spec.BignumQ.Definitions.pow336", "typing_Hacl.Spec.BignumQ.Definitions.pow448", "typing_Hacl.Spec.BignumQ.Definitions.pow504", "typing_Hacl.Spec.BignumQ.Definitions.pow56" ], 0, "219daf96f71112e7f5ad3271d2c7ad07" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_as_nat_pow264", 1, 0, 0, [ "@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.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "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", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow56" ], 0, "e5fb501c76306df475e254618b8bf6d5" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mod_264", 1, 0, 0, [ "@MaxIFuel_assumption", "@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.U64@tok", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "typing_Hacl.Spec.BignumQ.Definitions.pow56" ], 0, "9b7b18bf1274820e0dd62de8ccaee4f4" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mod_264", 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.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.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_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.nonzero", "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.sub_lemma", "lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_AmpAmp", "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.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_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_3ae0993553c878ac2a54593109e95c5a", "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_b4bde97cf54f36b26323c16a35da1f99", "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.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.mk_int", "typing_Lib.IntTypes.shift_left", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "63912d25ebc6b16f7bdad47b04504d2e" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_as_nat_pow264_x4", 1, 0, 0, [ "@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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "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", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "36ecb90df4531498c22fe99d6b6d3d3f" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_sub_mod_264_aux", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Hacl.Spec.BignumQ.Definitions.pow112", "equation_Hacl.Spec.BignumQ.Definitions.pow168", "equation_Hacl.Spec.BignumQ.Definitions.pow224", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "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_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3ae0993553c878ac2a54593109e95c5a", "refinement_interpretation_Tm_refine_b4bde97cf54f36b26323c16a35da1f99", "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, "74055d96860b204bed601992627c4de8" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_sub_mod_264", 1, 0, 0, [ "@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.qelem_fits1", "equation_Hacl.Spec.BignumQ.Definitions.qelem_fits5", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "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.Mktuple5__5", "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.U64@tok" ], 0, "8b943ad699fdae58c570533697a26542" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mul_qelem5", 1, 0, 0, [ "@query", "true_interp" ], 0, "e498748fbbff897e104772475233294a" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mul_5_low_264", 1, 0, 0, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "c2c93e032a4c2859d941cd4909a6ef26" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mul_nat_is_nat", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "8b74173b86ee55cb449f3de1bd02863f" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_div_nat_is_nat", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Division", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "b454455cb9ee3f753d13f339db6c19c2" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mul_5'''", 1, 0, 0, [ "@query" ], 0, "7457f900c076fa0330052bfb0e1b6a9a" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mul_5'''", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "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.pow56", "equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_33729c5d4f8faa1a24bd377a5f1a394b", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_3ae0993553c878ac2a54593109e95c5a", "refinement_interpretation_Tm_refine_536778a75b4d7e28377dd170a08c019c", "refinement_interpretation_Tm_refine_537f796f66502bfab3d6bd4b61276d25", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_770ab0bf9753aca6d20d9059a1d1935b", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ae79de13405c58c32c9304d0fb36a891", "refinement_interpretation_Tm_refine_b4bde97cf54f36b26323c16a35da1f99", "typing_Hacl.Spec.BignumQ.Definitions.pow112", "typing_Hacl.Spec.BignumQ.Definitions.pow168", "typing_Hacl.Spec.BignumQ.Definitions.pow224", "typing_Hacl.Spec.BignumQ.Definitions.pow280", "typing_Hacl.Spec.BignumQ.Definitions.pow336", "typing_Hacl.Spec.BignumQ.Definitions.pow392", "typing_Hacl.Spec.BignumQ.Definitions.pow448", "typing_Hacl.Spec.BignumQ.Definitions.pow56", "typing_Prims.pow2" ], 0, "dfd0d4628203f13c60700e667d4e77d3" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mul_5'''", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "dc7d7087ea340e74bdb8b8a93a53fc28" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mod_264''", 1, 0, 0, [ "@query" ], 0, "9b550afea7e3edee5dc8220c2ec12149" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mod_264''", 2, 0, 0, [ "@query", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, "5e5c50ed0c3eac679c1cdd2be3b83b1d" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mod_264'", 1, 0, 0, [ "@query" ], 0, "94eb54478004341cd93e44c2bf975df6" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mod_264'", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.nonzero", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "65be1fff46c8fd1f95c42555aee9f7ec" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_aux_0", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Prims.pow2" ], 0, "eb5a6c9863ba310bcabd14a922d5e455" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mod_264_small", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "98ac8b32fef63041286f357163ccbeaf" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mod_264_small", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Prims.pow2" ], 0, "429abb107f71f649fdd0aa4969b5667d" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mod_264_", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "591c9c8d8398b65834535ee54bb09493" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mod_264_", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Hacl.Spec.BignumQ.Definitions.pow56", "equation_Prims.nat", "equation_Prims.nonzero", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_339b7a66f80446c2629e3a2df26840ea", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Hacl.Spec.BignumQ.Definitions.pow56" ], 0, "a26881c4188160fd17f470711737796c" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_mul_5_low_264", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.nonzero", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "c7cf0e27c3defa0f1db02ded9a216a13" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_optimized_barrett_reduce", 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, "e14691dcedad4024e3319901fd884c03" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_optimized_barrett_reduce", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Division", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ffd0c5340ae953c83a5f54ff2e5d47b3" ], 0, "dd3159689447e986209cffbec861f6f7" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_optimized_barrett_reduce2", 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, "52180b07471ed3118b55632425417def" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_optimized_barrett_reduce2", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ffd0c5340ae953c83a5f54ff2e5d47b3" ], 0, "da2b9d4444385d81b022b259152cccae" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_0", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_GreaterThan", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "03fc023d365f872b276a6c4945065f07" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "e2adc12748bb69dc3a93af37fa080efe" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_barrett_reduce'", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos", "equation_Spec.Ed25519.q", "int_typing", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Prims.pow2" ], 0, "90be1cbe0332f9232d5e24378e51fd8d" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_barrett_reduce''", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.Ed25519.q", "int_inversion", "int_typing", "l_and-interp", "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "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_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Prims.pow2" ], 0, "7f5024637880973a7ec5bd6dfeb85b9f" ], [ "Hacl.Spec.BignumQ.Lemmas.lemma_barrett_reduce'", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Division", "primitive_Prims.op_LessThan", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ffd0c5340ae953c83a5f54ff2e5d47b3" ], 0, "86e1972fead9a47f0c6311b104bd674f" ] ] ]