[ "i­æN/·‰)@\\àäøÀ\"¸", [ [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_mod_sub_distr", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "2e63a57a694f0deba8827bb6bf8f3160" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_mod_sub_distr", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Minus", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "44f085892b48b56d66e6b41a2dcb6b8b" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_mul5_distr_r", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, "54bba59a978fc4d43772c927141ae57d" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_mul5_distr_l", 1, 2, 1, [ "@query", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, "356843614e6605f25e7de25196619dfd" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_mul_assos_3", 1, 2, 1, [ "@query", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, "bf476ee8af694c5efc431fc45771833c" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_mul_assos_4", 1, 2, 1, [ "@query", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, "158494a5dbee659be792b82a05bc74a4" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_mul_assos_5", 1, 2, 1, [ "@query", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, "a39d873993987b2cee26389af7b7f6a3" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_mul_assos_6", 1, 2, 1, [ "@query", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, "f94333d276f88686ed61718aa065db8f" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_add_le", 1, 2, 1, [ "@query", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0" ], 0, "fb1c4cdf4004c33deef5b48fa8552114" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_mul_le", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "e4c45401977edab4a9e939db89338d6d" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_prime", 1, 2, 1, [ "@query" ], 0, "6efa00e59594b256e93dd556fd3f9922" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_prime", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "78628710925c5f5c590445573df55f4a" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_add_zero", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "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_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_2579ef65ff8a5f937032f9984aa0f197", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_72460157ddb4b66d47add31d925bcdc9", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_b961c75d0ccf86ee74b6c5c2e9719d75", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "f5aba12f75810c7f56e1f3d96a92aac2" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_add_zero", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.as_nat5", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.feval", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "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.Curve25519.prime", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "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.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_2579ef65ff8a5f937032f9984aa0f197", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_72460157ddb4b66d47add31d925bcdc9", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_b961c75d0ccf86ee74b6c5c2e9719d75", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_Spec.Curve25519.prime", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "a2a172ce49d9203c97842881ac734ff2" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_pow51", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "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", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "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_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "e2baef58fa0fd331b47ab7e059752d43" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_pow51", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.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.pos", "equation_Spec.Curve25519.prime", "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.mul_lemma", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Addition", "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.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_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86", "refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "77f4ca5ff81bd135cca60fa4a61cb0e0" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_pow51_pow51", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "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", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.Curve25519.prime", "int_typing", "l_and-interp", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "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__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "d49686cf16a8d730f48cba39880f3214" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_pow51_pow51", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "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.pos", "equation_Spec.Curve25519.prime", "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_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_Spec.Curve25519.prime", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "2b8b0647886112978a24c5bb12950901" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_pow51_pow51_pow51", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "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", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.Curve25519.prime", "int_typing", "l_and-interp", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "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__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "4856f111accf6f11b085e315bf736658" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_pow51_pow51_pow51", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "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.pos", "equation_Spec.Curve25519.prime", "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_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_Spec.Curve25519.prime", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "9ef1ede62287fe30b95e395110aadadc" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_pow51_pow51_pow51_pow51", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "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", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.Curve25519.prime", "int_typing", "l_and-interp", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "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__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_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "76e56fa3bcf01a67ff853eebf3eb51e7" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_pow51_pow51_pow51_pow51", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "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.pos", "equation_Spec.Curve25519.prime", "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_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_Spec.Curve25519.prime", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "dc05d74b3358f69df94f0dac25482908" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_1", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "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", "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_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_94abc477f2ed5df378a3bafff4c88f95", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "50899d71b8bd969fd0affcc42a56f6fe" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_1", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "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.Curve25519.prime", "primitive_Prims.op_Addition", "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.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_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_94abc477f2ed5df378a3bafff4c88f95", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_Spec.Curve25519.prime", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "7ea9de52447752eaedd8e345a2b30f6c" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_2", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "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.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "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__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_94abc477f2ed5df378a3bafff4c88f95", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "8a3760326b8293b8563ae44538f6bb63" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_2", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "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.Curve25519.prime", "int_inversion", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Addition", "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.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_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_94abc477f2ed5df378a3bafff4c88f95", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_Spec.Curve25519.prime", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "0e73f8b5381c4b28231e0bc0711dfdd4" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_3", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "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.Curve25519.prime", "int_typing", "lemma_Lib.IntTypes.mul_lemma", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "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__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_94abc477f2ed5df378a3bafff4c88f95", "refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86", "refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "2b62bac82249986488c82bf92dc0e408" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_3", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "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.Curve25519.prime", "int_inversion", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Addition", "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.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_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_94abc477f2ed5df378a3bafff4c88f95", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_Spec.Curve25519.prime", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "74cdc4212c60d86fc75b4a950219d35b" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_4", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "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.Curve25519.prime", "int_typing", "lemma_Lib.IntTypes.mul_lemma", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_94abc477f2ed5df378a3bafff4c88f95", "refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86", "refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "6603983650d2d73babf40abdd70f5afe" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5_4", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "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.Curve25519.prime", "int_inversion", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_94abc477f2ed5df378a3bafff4c88f95", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_Spec.Curve25519.prime", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "b4894052522b6cf1f2b526d8dcbf1e64" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "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__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_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_94abc477f2ed5df378a3bafff4c88f95", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "67adfae1a25798cf3d77c36bce418978" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul5", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.as_nat5", "equation_Hacl.Spec.Curve25519.Field51.Definition.feval", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Curve25519.fmul", "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing", "lemma_FStar.UInt.pow2_values", "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", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "a7c7e263d41e37cec0c6fea6d5ee386a" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_smul_felem5", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.as_nat5", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51" ], 0, "45ef991a3951e08a5faed594afd9090a" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_smul_add_felem5", 1, 2, 1, [ "@query", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0" ], 0, "36c374f11954759a67a88667b61a942f" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_smul_add_felem5", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.as_nat5", "equation_Hacl.Spec.Curve25519.Field51.Definition.wide_as_nat5", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51" ], 0, "38c44d92d87526384aa6126e1babf979" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_carry51", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_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", "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.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "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.l_and", "equation_Prims.nat", "equation_Prims.squash", "int_typing", "l_and-interp", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "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_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "58ed0182f7fba2995008dfcb7e9ffd1e" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_carry51", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.SEC", "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.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.mask51", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "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", "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.mod_mask_lemma", "lemma_Lib.IntTypes.shift_left_lemma", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_36a04e927def1e73ac998ceb9d1e059e", "refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7", "refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_bdb08f3a637b4bb308d38cb72629d758", "refinement_interpretation_Tm_refine_d96d126280e4d44b4c6d27838df6e25f", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Curve25519.Field51.Definition.mask51", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.cast", "typing_Lib.IntTypes.logand", "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, "97d1a23368bc308272dfe72bea34d67f" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_carry51_wide", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "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", "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.Curve25519.Field51.Definition.felem_wide_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "equation_Hacl.Spec.Curve25519.Field51.Definition.scale64", "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_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_Addition", "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", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_407aa2139044a2a0797b68b34a4ca8fe", "refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7", "refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e", "refinement_interpretation_Tm_refine_6b9f7cae344d91c7aa92678ecb566528", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f29871d3a89d1e1bc374a18797629923", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "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, "96068967aeb028ee76570c51b32bb641" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_carry51_wide", 2, 2, 1, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "d3e1ae1c84a18216d57c362f3847c70d" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_carry51_wide", 3, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "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", "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.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_wide_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.mask51", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "equation_Hacl.Spec.Curve25519.Field51.Definition.scale64", "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", "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.pow2_127", "lemma_Lib.IntTypes.shift_left_lemma", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_407aa2139044a2a0797b68b34a4ca8fe", "refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7", "refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e", "refinement_interpretation_Tm_refine_6b9f7cae344d91c7aa92678ecb566528", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_bdb08f3a637b4bb308d38cb72629d758", "refinement_interpretation_Tm_refine_d96d126280e4d44b4c6d27838df6e25f", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f29871d3a89d1e1bc374a18797629923", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Curve25519.Field51.Definition.mask51", "typing_Hacl.Spec.Curve25519.Field51.Definition.max51", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.cast", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.shift_left", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "b0571c0faa433cb9e6312a2a2026d27f" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_carry5_simplify", 1, 2, 1, [ "@query" ], 0, "0d5deb90e28ce565c32dc5157df68bb9" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_carry5_simplify", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_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.SEC", "constructor_distinct_Lib.IntTypes.U64", "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.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Curve25519.prime", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_774ba3f728d91ead8ef40be66c9802e5", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_Spec.Curve25519.prime", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "a574fe36baa18c28e4d6b7061c3a5a3f" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_load_felem5", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "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_774ba3f728d91ead8ef40be66c9802e5", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "094a24b1307699ad16130fed9009eac9" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_load_felem5", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "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.U32@tok" ], 0, "2266a5c111d14099ddefec9e3c9b57f6" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_load_felem5", 3, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_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", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.as_nat5", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Prims.int", "haseqTm_refine_774ba3f728d91ead8ef40be66c9802e5", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3", "projection_inverse_FStar.Pervasives.Native.Mktuple4__4", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "4bc0b5f6b748f6b98596d8a384b8d7e6" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_load_felem_fits5", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "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.U32@tok" ], 0, "1f05b6e9f442ed75331b2c747e386cd0" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_load_felem_fits5", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "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.U32@tok" ], 0, "e0be2353a8427d277bf0a72044390094" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_load_felem_fits5", 3, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_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", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "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.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Prims.int", "haseqTm_refine_774ba3f728d91ead8ef40be66c9802e5", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "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.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3", "projection_inverse_FStar.Pervasives.Native.Mktuple4__4", "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_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "c7e7addb770443eb94549cdf4710f738" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_load_felem", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "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", "equality_tok_Lib.IntTypes.PUB@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.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_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "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_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "1438d7c11661df322e6ced5b2ebbfaa4" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_load_felem", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "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.U32@tok" ], 0, "94fc3b43d8b5c4c3ac66bbbf252f7b01" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_load_felem", 3, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "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", "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.Curve25519.Field51.Definition.mask51", "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", "equation_with_fuel_Prims.pow2.fuel_instrumented", "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_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.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3", "projection_inverse_FStar.Pervasives.Native.Mktuple4__4", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_20db9f9dd768f904363bb6893463cf77", "refinement_interpretation_Tm_refine_268ab4bc475893c8de6a5846dd99e5a2", "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_bdb08f3a637b4bb308d38cb72629d758", "refinement_interpretation_Tm_refine_d96d126280e4d44b4c6d27838df6e25f", "refinement_interpretation_Tm_refine_e1a33452d1fa5489d94e8d9e8379a02a", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f23da3d6844e650e3d4b882c16b6f0c9", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Curve25519.Field51.Definition.mask51", "typing_Lib.IntTypes.bits", "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.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "5d2e41869560404c05ebc4f23a2409a5" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_subtract_p5_0", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "23b6a37ca2155ab0d72d6e9f072e609c" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_subtract_p5_0", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.as_nat5", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "equation_Lib.IntTypes.v", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Curve25519.prime", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_774ba3f728d91ead8ef40be66c9802e5", "int_inversion", "int_typing", "lemma_Lib.IntTypes.v_injective", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality", "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_1c51b94209c49ed05998f398ca6d983f", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "b2e7781408337a13482c8e077e4170cb" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_subtract_p5_1", 1, 2, 1, [ "@query" ], 0, "ceb2c0abfb1354834868d8e029fca140" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_subtract_p5_1", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.as_nat5", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "equation_Lib.IntTypes.v", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Curve25519.prime", "function_token_typing_Prims.int", "haseqTm_refine_774ba3f728d91ead8ef40be66c9802e5", "int_inversion", "int_typing", "lemma_Lib.IntTypes.v_injective", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "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.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_1c51b94209c49ed05998f398ca6d983f", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.as_nat5", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "5b494e52c0be0c411be440230638f7ca" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_subtract_p", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "8fc3fc49fcef1fe7b8be1d12d7b1e229" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_subtract_p", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint64", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality", "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_1c51b94209c49ed05998f398ca6d983f", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.max51", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51" ], 0, "9e971609931a2229236443a043059bc2" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_store_felem2", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "2b96fa7fdea1c721144616120ffc9852" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_store_felem2", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_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.bits", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_v", "equation_Prims.nat", "equation_Prims.pos", "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion", "int_typing", "lemma_Lib.IntTypes.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", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_Prims.pow2" ], 0, "4fb7501d6ca65e33c26087cccbbf8587" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_store_felem1", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "694bae66a6b7bd5b365320e4767cf843" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_store_felem1", 2, 2, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos", "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_127", "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", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "244648cc32eadda3caa2507bada430fa" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_as_nat1", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_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.Curve25519.Field51.Definition.as_nat5", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem5", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple5", "function_token_typing_Prims.int", "haseqTm_refine_774ba3f728d91ead8ef40be66c9802e5", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51" ], 0, "8a9b76d25c783d142c1b156937eb7014" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_store_felem0", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nonzero", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f" ], 0, "d4120e1222fba5a0d78223f6e7d93c79" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_store_felem0", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "data_elim_FStar.Pervasives.Native.Mktuple5", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem5", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos", "equation_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple5", "function_token_typing_Prims.int", "haseqTm_refine_774ba3f728d91ead8ef40be66c9802e5", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_127", "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", "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_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7ae794b9ae0de2fb99f6920e42e7ff85", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "8bbee09f8ec8f5bc1de43f446b2fa27e" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_store_felem", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "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", "equality_tok_Lib.IntTypes.PUB@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.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "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_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7ae794b9ae0de2fb99f6920e42e7ff85", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t" ], 0, "df86ddbed3ca0d216f26018d13019be0" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_store_felem", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "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", "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.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "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.eqtype", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Prims.int", "haseqTm_refine_774ba3f728d91ead8ef40be66c9802e5", "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", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "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.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_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7ae794b9ae0de2fb99f6920e42e7ff85", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "266d8dac4248c82493a949e4dbc4f2ae" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_cswap2_step", 1, 2, 1, [ "@MaxIFuel_assumption", "@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", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_f41f4015e22b272c5f61be9cc1570311", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "fb6d7d4fbe794da39e2bc1656f841d4b" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_cswap2_step", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b", "Prims_pretyping_ae567c2fb75be05905677af440075565", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "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", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Lib.IntTypes.logand", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "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_Multiply", "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_b47cabb890633249ae7f38d35cac724e", "refinement_interpretation_Tm_refine_f41f4015e22b272c5f61be9cc1570311", "typing_Lib.IntTypes.bits", "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, "f304a54f136109e1e1ce006418b622a8" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.mul64_wide_add3_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "equation_Hacl.Spec.Curve25519.Field51.Definition.scale64", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Prims.int", "haseqTm_refine_774ba3f728d91ead8ef40be66c9802e5", "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", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_e23dd143272aac060aa1fee6dcb25a2b", "refinement_interpretation_Tm_refine_f29871d3a89d1e1bc374a18797629923", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "true_interp", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "8596e7f8eca8d427116a857efa7f56cd" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul_fsqr50", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, "04995390eb58a5bf66923082502480f2" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul_fsqr51", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "int_typing", "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51" ], 0, "7947cfcc2874c7e5cb8626c9604231c5" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul_fsqr52", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "int_typing", "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51" ], 0, "e835155abe900f889b7a1c6c93201eb9" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul_fsqr53", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51" ], 0, "1ab6105c95f2bd2b8f456957df5d2a8e" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul_fsqr54", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51" ], 0, "03dd8606249cf7ca0026835c00e434a6" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul_fsqr5", 1, 2, 1, [ "@query" ], 0, "1b0d788a2b1dc294b8bb75e2221347b6" ], [ "Hacl.Spec.Curve25519.Field51.Lemmas.lemma_fmul_fsqr5", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1", "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5", "equation_Hacl.Spec.Curve25519.Field51.Definition.max51", "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.Curve25519.prime", "int_inversion", "int_typing", "lemma_Lib.IntTypes.mul_lemma", "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_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8fa1f3ecf338f3010649aa74976fe1b1", "refinement_interpretation_Tm_refine_94abc477f2ed5df378a3bafff4c88f95", "refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86", "refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1", "refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a", "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51", "typing_Lib.IntTypes.v", "typing_Spec.Curve25519.prime", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "6b9aab4411d50e2d964f89d0929cf86c" ] ] ]