[
"‰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"
]
]
]