[ "‰j\u0003ˆ–Hú»ð\u001c\n;3“éM", [ [ "Spec.Ed25519.Lemmas.elem_add_cm", 1, 0, 0, [ "@query", "equation_Lib.NatMod.add_mod", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Curve25519.zero", "primitive_Prims.op_Addition" ], 0, "7cb7d1f1f00a677519fa6a304c66cc15" ], [ "Spec.Ed25519.Lemmas.elem_mul_cm", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Lib.NatMod.mul_mod", "equation_Lib.NatMod.one_mod", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.one", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.one" ], 0, "3ea39a90daa351813fbb8dacc2fc09b0" ], [ "Spec.Ed25519.Lemmas.fmul_zero_l", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.Lemmas.elem_add_cm", "equation_Spec.Ed25519.Lemmas.elem_mul_cm", "function_token_typing_Spec.Curve25519.op_Star_Percent", "int_inversion", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "proj_equation_FStar.Algebra.CommMonoid.CM_mult", "proj_equation_FStar.Algebra.CommMonoid.CM_unit", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Algebra.CommMonoid.CM_mult", "projection_inverse_FStar.Algebra.CommMonoid.CM_unit", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "token_correspondence_FStar.Algebra.CommMonoid.__proj__CM__item__mult" ], 0, "038fa3538133405bc2a49fd2f296f796" ], [ "Spec.Ed25519.Lemmas.op_Tilde_Percent", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "37e82cc9ff07c62c6d43f4608e6af7b1" ], [ "Spec.Ed25519.Lemmas.fadd_opp", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.Lemmas.op_Tilde_Percent", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Minus", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.prime" ], 0, "1c9038ee223f1dee39435f9dd637c2c9" ], [ "Spec.Ed25519.Lemmas.elem_cr", 1, 0, 0, [ "@query", "equation_Lib.NatMod.add_mod", "equation_Lib.NatMod.mul_mod", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Ed25519.Lemmas.elem_add_cm", "equation_Spec.Ed25519.Lemmas.elem_mul_cm", "function_token_typing_Spec.Curve25519.op_Plus_Percent", "proj_equation_FStar.Algebra.CommMonoid.CM_mult", "proj_equation_FStar.Algebra.CommMonoid.CM_unit", "projection_inverse_FStar.Algebra.CommMonoid.CM_mult", "projection_inverse_FStar.Algebra.CommMonoid.CM_unit", "token_correspondence_FStar.Algebra.CommMonoid.__proj__CM__item__mult", "token_correspondence_Spec.Curve25519.op_Plus_Percent", "token_correspondence_Spec.Curve25519.op_Star_Percent" ], 0, "0624065770c3933511e265ee39bbaee8" ], [ "Spec.Ed25519.Lemmas.ed25519_semiring", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "8c63d7ce9d3c33343c6b87d19268557e" ], [ "Spec.Ed25519.Lemmas.denominator_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Ed25519.PointOps.d", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "8a06ae911cb09df38d1b3f7983a37112" ], [ "Spec.Ed25519.Lemmas.denominator_lemma1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "f4a26d69ca8b929242aae4ff5c776bf5" ], [ "Spec.Ed25519.Lemmas.fdiv_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "d6f6173987a0f592baec6e3698d4f176" ], [ "Spec.Ed25519.Lemmas.fdiv_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "31a75637850d51c3d827a27501ea80eb" ], [ "Spec.Ed25519.Lemmas.fdiv_lemma", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Math.Euclid.is_prime", "equation_Lib.NatMod.div_mod", "equation_Lib.NatMod.inv_mod", "equation_Lib.NatMod.mul_mod", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.one", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.PointOps.fexp", "equation_Spec.Ed25519.PointOps.finv", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "primitive_Prims.op_Subtraction", "refinement_interpretation_Tm_refine_0d3678ae138cce9eddce0f44e8d2aec1", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "645440108e718e2e885b231185f90281" ], [ "Spec.Ed25519.Lemmas.fdiv_one_lemma", 1, 0, 0, [ "@query", "equation_FStar.Math.Euclid.is_prime", "equation_Lib.NatMod.div_mod", "equation_Lib.NatMod.inv_mod", "equation_Lib.NatMod.mul_mod", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.one", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.fexp", "equation_Spec.Ed25519.PointOps.finv", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "primitive_Prims.op_Subtraction" ], 0, "cc8e20b3d27d06eb81fa1ac1f8e37c5c" ], [ "Spec.Ed25519.Lemmas.fdiv_one_lemma1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "f0be1e7181cde753c8353c5643423aef" ], [ "Spec.Ed25519.Lemmas.fdiv_one_lemma1", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "3d0a9f9a62b943dde117c3212aa35bfb" ], [ "Spec.Ed25519.Lemmas.fdiv_one_lemma1", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Lib.NatMod.mul_mod", "equation_Lib.NatMod.one_mod", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.one", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.one" ], 0, "34512cb44ed72f4ec9a93331995d43d4" ], [ "Spec.Ed25519.Lemmas.fdiv_cancel_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "c0692e48d1eb574cc96e59cbb81218bc" ], [ "Spec.Ed25519.Lemmas.fdiv_cancel_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "8fe9803a4a3b34c678f7e5c434a8d095" ], [ "Spec.Ed25519.Lemmas.fdiv_cancel_lemma", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Math.Euclid.is_prime", "equation_Lib.NatMod.div_mod", "equation_Lib.NatMod.inv_mod", "equation_Lib.NatMod.mul_mod", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.PointOps.fexp", "equation_Spec.Ed25519.PointOps.finv", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "int_inversion", "primitive_Prims.op_Subtraction", "refinement_interpretation_Tm_refine_0d3678ae138cce9eddce0f44e8d2aec1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "f7b6f7867db55d3d26ee3deb4bee002e" ], [ "Spec.Ed25519.Lemmas.fdiv_to_one_denominator", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "b3140f68a49760e38c753329afe22eae" ], [ "Spec.Ed25519.Lemmas.fdiv_to_one_denominator", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "dbc25cfa799058f8aca4629940f1db33" ], [ "Spec.Ed25519.Lemmas.fdiv_to_one_denominator", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Math.Euclid.is_prime", "equation_Lib.NatMod.div_mod", "equation_Lib.NatMod.inv_mod", "equation_Lib.NatMod.mul_mod", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.PointOps.fexp", "equation_Spec.Ed25519.PointOps.finv", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "int_inversion", "primitive_Prims.op_Subtraction", "refinement_interpretation_Tm_refine_0d3678ae138cce9eddce0f44e8d2aec1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "a12e246c33ba57c27cd4f5c27488201e" ], [ "Spec.Ed25519.Lemmas.fmul_zero_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.op_Star_Percent", "unit_inversion", "unit_typing" ], 0, "b2370bd1e1e2faba7d8758cb398ae1f7" ], [ "Spec.Ed25519.Lemmas.fmul_nonzero_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "2858f9b7cd438b481701733805cdf61a" ], [ "Spec.Ed25519.Lemmas.fmul_nonzero_lemma", 2, 0, 0, [ "@query", "equation_Spec.Curve25519.zero" ], 0, "036275d6a7fde36e85d43e365f29d41b" ], [ "Spec.Ed25519.Lemmas.finv2_nonzero_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "a22a856b25bc0c1472d53f65d784d494" ], [ "Spec.Ed25519.Lemmas.finv2_nonzero_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.one", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.one" ], 0, "4f2ba1500a9e326d3e2e150a220d386c" ], [ "Spec.Ed25519.Lemmas.lemma_aff_double_aux", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "f03cf746b8a1d4c2568799210f3e734f" ], [ "Spec.Ed25519.Lemmas.lemma_aff_double_aux", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.op_Subtraction_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.d", "int_inversion", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.op_Star_Percent", "typing_Spec.Curve25519.op_Subtraction_Percent", "typing_Spec.Ed25519.PointOps.d" ], 0, "136cde50e3c781ff9ac3fe7dd62cd2ca" ], [ "Spec.Ed25519.Lemmas.aff_point_at_infinity_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.one", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.op_Subtraction_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.PointOps.aff_point_add", "equation_Spec.Ed25519.PointOps.aff_point_at_infinity", "equation_Spec.Ed25519.PointOps.d", "int_inversion", "int_typing", "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_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.op_Star_Percent", "typing_Spec.Curve25519.zero", "typing_Spec.Ed25519.PointOps.d" ], 0, "bb4fdabf4c5e6bacb5df769b6d152c44" ], [ "Spec.Ed25519.Lemmas.aff_point_add_comm_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Ed25519.PointOps.aff_point_add", "equation_Spec.Ed25519.PointOps.d", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "e27cb25893c9e126c7b9f9830a0a7231" ], [ "Spec.Ed25519.Lemmas.aff_point_double_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Spec.Curve25519.elem", "equation_Spec.Ed25519.PointOps.aff_point_add", "equation_Spec.Ed25519.PointOps.aff_point_double", "equation_Spec.Ed25519.PointOps.d", "equation_Spec.Ed25519.PointOps.is_on_curve", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_30ebfcd9193ad561f2f74576fbc2006b", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "true_interp", "typing_Spec.Ed25519.PointOps.d" ], 0, "c11bcf6036a2c03981b61f93ce26ef18" ], [ "Spec.Ed25519.Lemmas.aff_point_double_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Spec.Curve25519.elem", "equation_Spec.Ed25519.PointOps.d", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "f6c1761904b3db95beefe645f6dae0bf" ], [ "Spec.Ed25519.Lemmas.aff_point_double_lemma", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Ed25519.PointOps.d", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "0c4d0c9ea725657ba7ed087ad18c3897" ], [ "Spec.Ed25519.Lemmas.lemma_neg_sqr", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "0023fc9ed00adaf83b1df90afb884e1a" ], [ "Spec.Ed25519.Lemmas.lemma_neg_sqr", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "int_inversion", "primitive_Prims.op_Minus", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "d842d48413608c7d6b2916ed022ba6ea" ], [ "Spec.Ed25519.Lemmas.aff_point_negate_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.aff_point_negate", "equation_Spec.Ed25519.PointOps.d", "equation_Spec.Ed25519.PointOps.is_on_curve", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "fce3cc59c6de804f0e13097386f776cc" ], [ "Spec.Ed25519.Lemmas.to_aff_point_at_infinity_lemma", 1, 0, 0, [ "@query", "equation_Spec.Curve25519.elem", "equation_Spec.Ed25519.PointOps.aff_point_at_infinity", "equation_Spec.Ed25519.PointOps.point_at_infinity", "equation_Spec.Ed25519.PointOps.to_aff_point", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3" ], 0, "f78becc4336b85b725f5623ed0671f1a" ], [ "Spec.Ed25519.Lemmas.ext_dx1x2y1y2", 1, 0, 0, [ "@query", "equation_Spec.Curve25519.elem", "equation_Spec.Ed25519.PointOps.is_ext", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "equation_Spec.Ed25519.PointOps.to_aff_point", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3", "true_interp" ], 0, "a7c882ddd6fc05d921cfba6d9c0ba091" ], [ "Spec.Ed25519.Lemmas.ext_dx1x2y1y2", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Lib.NatMod.nat_mod", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.d", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "05ba8f38c4b7adfc24c3e8666828f57d" ], [ "Spec.Ed25519.Lemmas.ext_dx1x2y1y2_mulz1z2", 1, 0, 0, [ "@query", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Ed25519.PointOps.is_ext", "primitive_Prims.op_Multiply", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3" ], 0, "264efb0f28e57db9d6dc61ecae575f02" ], [ "Spec.Ed25519.Lemmas.ext_dx1x2y1y2_mulz1z2", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Lib.NatMod.nat_mod", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.prime", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "274f12f0d9ff0e018c3bf4825b79bffc" ], [ "Spec.Ed25519.Lemmas.ext_x1x2_plus_y1y2", 1, 0, 0, [ "@query", "equation_Lib.NatMod.add_mod", "equation_Lib.NatMod.mul_mod", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.finv", "equation_Spec.Ed25519.PointOps.is_ext", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "equation_Spec.Ed25519.PointOps.to_aff_point", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3" ], 0, "319e2d2c880ba7cb9616122d97c770df" ], [ "Spec.Ed25519.Lemmas.ext_x1y2_plus_y1x2", 1, 0, 0, [ "@query", "equation_Lib.NatMod.add_mod", "equation_Lib.NatMod.mul_mod", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.finv", "equation_Spec.Ed25519.PointOps.is_ext", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "equation_Spec.Ed25519.PointOps.to_aff_point", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3" ], 0, "e15cfaaf40341d5a3af9343a607fdbbc" ], [ "Spec.Ed25519.Lemmas.ext_yy_minus_xx", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "21740e3fc71e09810990a1515b576de3" ], [ "Spec.Ed25519.Lemmas.ext_yy_minus_xx", 2, 0, 0, [ "@query", "equation_Lib.NatMod.mul_mod", "equation_Lib.NatMod.sub_mod", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.op_Subtraction_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.finv", "equation_Spec.Ed25519.PointOps.is_ext", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "equation_Spec.Ed25519.PointOps.to_aff_point", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3" ], 0, "63f3362fa93843c35c42683d57eaf3a3" ], [ "Spec.Ed25519.Lemmas.ext_2_minus_yy_plus_xx", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "0636eea47a57a15669fff0e692277991" ], [ "Spec.Ed25519.Lemmas.ext_2_minus_yy_plus_xx", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Subtraction_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.to_aff_point", "int_inversion", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Spec.Curve25519.prime" ], 0, "aae4e78c6e4120f14ebe973256995024" ], [ "Spec.Ed25519.Lemmas.ext_2_minus_yy_plus_xx_mul_zz", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "03840bb1bbff14bac6ac9cc0cc5d7160" ], [ "Spec.Ed25519.Lemmas.ext_2_minus_yy_plus_xx_mul_zz", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Lib.NatMod.mul_mod", "equation_Lib.NatMod.sub_mod", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.op_Subtraction_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.is_ext", "equation_Spec.Ed25519.PointOps.to_aff_point", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "9dd9ddfa85332b4b49824a0e9b1beaa7" ], [ "Spec.Ed25519.Lemmas.ext_denominator_lemma1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "a2c57289c8fc47e80777b9f34df57b35" ], [ "Spec.Ed25519.Lemmas.ext_denominator_lemma1", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Lib.NatMod.add_mod", "equation_Lib.NatMod.mul_mod", "equation_Lib.NatMod.sub_mod", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.one", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.op_Subtraction_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.d", "equation_Spec.Ed25519.PointOps.is_ext", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "int_inversion", "int_typing", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.op_Star_Percent", "typing_Spec.Ed25519.PointOps.d" ], 0, "0f0d588f4dab3a32c4659f2c748081e7" ], [ "Spec.Ed25519.Lemmas.ext_denominator_lemma2", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Ed25519.PointOps.d", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "6887a4bba5fe1a341ca4e8b876c74ffd" ], [ "Spec.Ed25519.Lemmas.ext_denominator_lemma2", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Lib.NatMod.mul_mod", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.d", "equation_Spec.Ed25519.PointOps.is_ext", "equation_Spec.Ed25519.PointOps.is_on_curve", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "e2d8d2cf8d2e67bd11da4860d2a1d12a" ], [ "Spec.Ed25519.Lemmas.point_add_expand_eh_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "98e2945845d1e8da1883faa743e1f1ad" ], [ "Spec.Ed25519.Lemmas.point_add_expand_eh_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.op_Subtraction_Percent", "equation_Spec.Curve25519.prime", "int_inversion", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Addition", "primitive_Prims.op_Minus", "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", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.op_Plus_Percent", "typing_Spec.Curve25519.op_Subtraction_Percent" ], 0, "ef3861e806bd942c8732c86f03b489fc" ], [ "Spec.Ed25519.Lemmas.point_add_expand_gf_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "dc656b026b326e76bf8a057d8e487aec" ], [ "Spec.Ed25519.Lemmas.point_add_expand_gf_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Lib.NatMod.add_mod", "equation_Lib.NatMod.inv_mod", "equation_Lib.NatMod.mul_mod", "equation_Lib.NatMod.sub_mod", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.op_Subtraction_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.fexp", "equation_Spec.Ed25519.PointOps.finv", "equation_Spec.Ed25519.PointOps.is_ext", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6f5166e806a315ada23b109e7e1ca079", "true_interp" ], 0, "b46ae34d8e47334dcdf477665543fb0d" ], [ "Spec.Ed25519.Lemmas.point_add_expand_gf_lemma", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Spec.Curve25519.elem", "equation_Spec.Ed25519.PointOps.d", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "c6e8e6b3fa059534a6cea60d3c26a557" ], [ "Spec.Ed25519.Lemmas.point_add_expand_gf_lemma", 4, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Spec.Curve25519.elem", "equation_Spec.Ed25519.PointOps.d", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "745942514185c3650a4c5af093015741" ], [ "Spec.Ed25519.Lemmas.point_add_expand_gf_lemma", 5, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.d", "equation_Spec.Ed25519.PointOps.fexp", "equation_Spec.Ed25519.PointOps.finv", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a7a18b3d2bbe32ad1d7773e62663094f", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_ca6b598692b75a640e75f32aa4134bcd", "typing_Spec.Ed25519.PointOps.d", "typing_Spec.Ed25519.PointOps.finv" ], 0, "26e12437a5b6c5e76da6e60ca7e21dc8" ], [ "Spec.Ed25519.Lemmas.point_add_expand_gf_lemma_non_zero", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Ed25519.PointOps.d", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "041c177120ed31f82fcd4384cc5617ad" ], [ "Spec.Ed25519.Lemmas.point_add_expand_gf_lemma_non_zero", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.PointOps.d", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "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_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "37afaae2f35c0d8fb372c6e97cf31249" ], [ "Spec.Ed25519.Lemmas.fghe_relation", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "6b1410c7e8edf5335db9cce0f482ab28" ], [ "Spec.Ed25519.Lemmas.fghe_relation", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Lib.NatMod.mul_mod", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "int_inversion", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "7e6869411706180cf94871a569c2afad" ], [ "Spec.Ed25519.Lemmas.fghe_relation", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.prime", "equation_Spec.Curve25519.zero", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.zero" ], 0, "f7c5c617c5118cea54719391cb1b2cb1" ], [ "Spec.Ed25519.Lemmas.to_aff_point_add_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Lib.NatMod.add_mod", "equation_Lib.NatMod.mul_mod", "equation_Lib.NatMod.sub_mod", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.one", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.op_Subtraction_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.PointOps.aff_point_add", "equation_Spec.Ed25519.PointOps.d", "equation_Spec.Ed25519.PointOps.is_ext", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "equation_Spec.Ed25519.PointOps.point_add", "equation_Spec.Ed25519.PointOps.point_inv", "equation_Spec.Ed25519.PointOps.to_aff_point", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "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_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "8cf1bb4b44202f7b63c51d4fd1dc5a2f" ], [ "Spec.Ed25519.Lemmas.point_double_expand_eh_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "894a2c7038b025a2610b4240e6bbbb66" ], [ "Spec.Ed25519.Lemmas.point_double_expand_eh_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.op_Subtraction_Percent", "equation_Spec.Curve25519.prime", "int_inversion", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Addition", "primitive_Prims.op_Minus", "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", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "true_interp" ], 0, "d59fac6a8d0de3d3b5396d85c1448593" ], [ "Spec.Ed25519.Lemmas.point_double_expand_eh_lemma", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "12cc873e448a0b41766d163a7f90d5f9" ], [ "Spec.Ed25519.Lemmas.point_double_expand_gf_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "01df30b151ca9324a9dd1648c481a7cf" ], [ "Spec.Ed25519.Lemmas.point_double_expand_gf_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.op_Subtraction_Percent", "equation_Spec.Curve25519.prime", "int_inversion", "int_typing", "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_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "c04387cfc5c2e5da620f7896380488ff" ], [ "Spec.Ed25519.Lemmas.point_double_expand_gf_lemma_non_zero", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Ed25519.PointOps.d", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "0ba61c463c8e8cd4bc4b7fb374239aa3" ], [ "Spec.Ed25519.Lemmas.point_double_expand_gf_lemma_non_zero", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.prime", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.PointOps.d", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Modulus", "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", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.op_Star_Percent", "typing_Spec.Curve25519.op_Subtraction_Percent", "typing_Spec.Ed25519.PointOps.d" ], 0, "d454179e24c4fa33c3f4e8496db9c330" ], [ "Spec.Ed25519.Lemmas.to_aff_point_double_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Lib.NatMod.add_mod", "equation_Lib.NatMod.mul_mod", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.PointOps.aff_point_double", "equation_Spec.Ed25519.PointOps.d", "equation_Spec.Ed25519.PointOps.is_ext", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "equation_Spec.Ed25519.PointOps.point_double", "equation_Spec.Ed25519.PointOps.point_inv", "equation_Spec.Ed25519.PointOps.to_aff_point", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "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_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.prime", "typing_Spec.Ed25519.PointOps.d" ], 0, "3bfe063bc742eaaa3a39c6da6a4fccea" ], [ "Spec.Ed25519.Lemmas.to_aff_point_negate", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.aff_point_negate", "equation_Spec.Ed25519.PointOps.d", "equation_Spec.Ed25519.PointOps.finv", "equation_Spec.Ed25519.PointOps.is_ext", "equation_Spec.Ed25519.PointOps.is_on_curve", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "equation_Spec.Ed25519.PointOps.point_inv", "equation_Spec.Ed25519.PointOps.point_negate", "equation_Spec.Ed25519.PointOps.to_aff_point", "int_inversion", "int_typing", "primitive_Prims.op_Minus", "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "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_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Ed25519.PointOps.d" ], 0, "83392207772b7e6b35f27f57a10d978d" ], [ "Spec.Ed25519.Lemmas.fmul_both_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "c252634628f5df34cd594b2999385013" ], [ "Spec.Ed25519.Lemmas.fmul_both_lemma_neq", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "12272f59ad91223ebe7144d97bc14a67" ], [ "Spec.Ed25519.Lemmas.fmul_both_lemma_neq", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "int_inversion", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_204172c059689dbecd30c46aec891ea9", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "e910ee2fb92238b2aed7b781d70e35e8" ], [ "Spec.Ed25519.Lemmas.lemma_fmul_assoc1", 1, 0, 0, [ "@query", "true_interp" ], 0, "05a521aa711b8b0f8d1f99202cf4393b" ], [ "Spec.Ed25519.Lemmas.lemma_fmul_assoc1", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "9fdcf267ec6e87adda33bb0eff264013" ], [ "Spec.Ed25519.Lemmas.fdiv_lemma1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.PointOps.op_Slash_Percent", "refinement_interpretation_Tm_refine_204172c059689dbecd30c46aec891ea9", "true_interp" ], 0, "56514d32b64d9bb62111f0e52117a16b" ], [ "Spec.Ed25519.Lemmas.fdiv_lemma1", 2, 0, 0, [ "@query" ], 0, "7331a6940e1530446e445fe9cb18896a" ], [ "Spec.Ed25519.Lemmas.fdiv_lemma1", 3, 0, 0, [ "@query" ], 0, "d72b6dd1625aedb9a62b05fe72b81fdd" ], [ "Spec.Ed25519.Lemmas.fdiv_lemma1", 4, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.prime", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_204172c059689dbecd30c46aec891ea9", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "8167735a8e8598f9cdf04b467cfd09d3" ], [ "Spec.Ed25519.Lemmas.fdiv_lemma1", 5, 0, 0, [ "@query" ], 0, "7aed32b70c6a58e45c20e27b5323deb0" ], [ "Spec.Ed25519.Lemmas.fdiv_lemma1", 6, 0, 0, [ "@query" ], 0, "3612f502cc3975350cbaadff4dca13bc" ], [ "Spec.Ed25519.Lemmas.fdiv_lemma1", 7, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.prime", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_204172c059689dbecd30c46aec891ea9", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655" ], 0, "55e0c5b4b3d364fe44e0d20681bbe322" ], [ "Spec.Ed25519.Lemmas.point_equal_lemma_aux1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "4828061634f20c263f5dd40bbb2667d8" ], [ "Spec.Ed25519.Lemmas.point_equal_lemma_aux1", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "7a85b25c7ee44b77441d1b5addf0a0f2" ], [ "Spec.Ed25519.Lemmas.point_equal_lemma_aux2", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "int_inversion", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_204172c059689dbecd30c46aec891ea9", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.op_Star_Percent" ], 0, "c4aa496126b9c56aae6d8bf486677e88" ], [ "Spec.Ed25519.Lemmas.point_equal_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.PointOps.is_ext", "equation_Spec.Ed25519.PointOps.point_equal", "equation_Spec.Ed25519.PointOps.to_aff_point", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "primitive_Prims.op_disEquality", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__1", "projection_inverse_FStar.Pervasives.Native.Mktuple4__2", "projection_inverse_FStar.Pervasives.Native.Mktuple4__3", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "unit_inversion", "unit_typing" ], 0, "dd232f09cea73b629bf80833703056d6" ], [ "Spec.Ed25519.Lemmas.aff_g_is_on_curve", 1, 0, 0, [ "@query", "equation_Spec.Ed25519.PointOps.aff_g" ], 0, "0529173023d3767658d06af4be653678" ], [ "Spec.Ed25519.Lemmas.g_is_on_curve", 1, 0, 0, [ "@query", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.one", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.PointOps.aff_g", "equation_Spec.Ed25519.PointOps.g", "equation_Spec.Ed25519.PointOps.g_x", "equation_Spec.Ed25519.PointOps.g_y", "equation_Spec.Ed25519.PointOps.is_ext", "equation_Spec.Ed25519.PointOps.point_inv", "equation_Spec.Ed25519.PointOps.to_aff_point", "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" ], 0, "53c4075111f1801c0b5890b3d48153af" ], [ "Spec.Ed25519.Lemmas.recover_x_lemma_aux", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Lib.NatMod.mul_mod", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.one", "equation_Spec.Curve25519.op_Plus_Percent", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.op_Subtraction_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.d", "equation_Spec.Ed25519.PointOps.finv", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "true_interp", "typing_Spec.Curve25519.one", "typing_Spec.Curve25519.op_Plus_Percent", "typing_Spec.Curve25519.op_Star_Percent", "typing_Spec.Curve25519.op_Subtraction_Percent", "typing_Spec.Ed25519.PointOps.d", "typing_Spec.Ed25519.PointOps.finv" ], 0, "93cb1c50ae7e7ae5d6c4413721085994" ], [ "Spec.Ed25519.Lemmas.recover_x_lemma_aux", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Lib.NatMod.nat_mod", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.one", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.op_Subtraction_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Ed25519.PointOps.d", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.one", "typing_Spec.Curve25519.op_Star_Percent", "typing_Spec.Curve25519.op_Subtraction_Percent", "typing_Spec.Ed25519.PointOps.d" ], 0, "6d59dc68a4f345515ac1cc0cfdfce0d9" ], [ "Spec.Ed25519.Lemmas.recover_x_lemma", 1, 0, 0, [ "@query" ], 0, "1f092ecca9bd6faf72af1b187293e1e2" ], [ "Spec.Ed25519.Lemmas.recover_x_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.one", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.op_Subtraction_Percent", "equation_Spec.Curve25519.prime", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.PointOps.d", "equation_Spec.Ed25519.PointOps.finv", "equation_Spec.Ed25519.PointOps.is_on_curve", "equation_Spec.Ed25519.PointOps.modp_sqrt_m1", "equation_Spec.Ed25519.PointOps.recover_x", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c9f318957334bae90e9d8f370d26a655", "int_inversion", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_Minus", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "typing_Spec.Curve25519.one", "typing_Spec.Curve25519.op_Plus_Percent", "typing_Spec.Curve25519.op_Star_Percent", "typing_Spec.Curve25519.op_Subtraction_Percent", "typing_Spec.Ed25519.PointOps.d", "typing_Spec.Ed25519.PointOps.finv", "unit_inversion", "unit_typing" ], 0, "a702e2ab9752e7917b93c601303b1449" ], [ "Spec.Ed25519.Lemmas.point_decompress_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_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, "9547d4c9bf7a9d709be48ed8cdd4f99d" ], [ "Spec.Ed25519.Lemmas.point_decompress_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_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, "80d13d2370da4f47fb4070ada079d665" ], [ "Spec.Ed25519.Lemmas.point_decompress_lemma", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Prims.nonzero", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.one", "equation_Spec.Curve25519.zero", "equation_Spec.Ed25519.PointOps.ext_point", "equation_Spec.Ed25519.PointOps.is_ext", "equation_Spec.Ed25519.PointOps.point_decompress", "equation_Spec.Ed25519.PointOps.point_inv", "equation_Spec.Ed25519.PointOps.to_aff_point", "int_inversion", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "proj_equation_FStar.Pervasives.Native.Some_v", "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.Some_v", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42" ], 0, "2e50bbd4dbaaa470be46c6fd941bfdec" ], [ "Spec.Ed25519.Lemmas.lemma_fpow1", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Spec.Curve25519.fpow.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "equation_Prims.pos", "equation_with_fuel_Spec.Curve25519.fpow.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "int_typing", "primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "c0269b36571531794ec31b0b79da8b35" ], [ "Spec.Ed25519.Lemmas.lemma_fpow_unfold0", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2e4eb0dfc8e927c366ec35a49feaf594", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "5fd6c98dfa207ad8773a5bb7a777d370" ], [ "Spec.Ed25519.Lemmas.lemma_fpow_unfold0", 2, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Spec.Curve25519.fpow.fuel_instrumented", "@fuel_irrelevance_Spec.Curve25519.fpow.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "equation_Prims.pos", "equation_with_fuel_Spec.Curve25519.fpow.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2e4eb0dfc8e927c366ec35a49feaf594", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "5d8964833a9e06923e3b412ee2c75591" ], [ "Spec.Ed25519.Lemmas.lemma_fpow_unfold1", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "lemma_Spec.Curve25519.Lemmas.lemma_div_n", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5c810aa3d09a59fa0969eff7c23d634f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "6e1bd5fa754482446232cd420053eb3b" ], [ "Spec.Ed25519.Lemmas.lemma_fpow_unfold1", 2, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Spec.Curve25519.fpow.fuel_instrumented", "@fuel_irrelevance_Spec.Curve25519.fpow.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "equation_with_fuel_Spec.Curve25519.fpow.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_5c810aa3d09a59fa0969eff7c23d634f" ], 0, "c9c5af2865513ca85f7d302138830ff0" ], [ "Spec.Ed25519.Lemmas.fpow_is_pow", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "95fe44ba20ccf45e600dc0134e9c440d" ], [ "Spec.Ed25519.Lemmas.fpow_is_pow", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "refinement_interpretation_Tm_refine_35f987cde49ff82813b1b8be8301e9bd", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "fd08e1567022525259f49a75fb97ba92" ], [ "Spec.Ed25519.Lemmas.fpow_is_pow", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Lib.NatMod.pow.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_c5a18afe0d0cc18c721b3fa79b570491_0", "binder_x_f26957a7e62b271a8736230b1e9c83c1_1", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.op_Star_Percent", "equation_Spec.Curve25519.prime", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "e753dc630a2f4ff5328a37783b29cbe9" ], [ "Spec.Ed25519.Lemmas.fpow_is_pow_mod", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "678ac160ed2b54c91df29db807f73284" ], [ "Spec.Ed25519.Lemmas.fpow_is_pow_mod", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Curve25519.prime", "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "9674fee661e68bf214cca2f010874d46" ] ] ]