Revision 724d1045f60f13d79df1afc5190955afdfa73ec1 authored by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC, committed by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC
Co-authored-by: @protz
1 parent ca37fbf
Spec.P256.MontgomeryMultiplication.PointDouble.fst.hints
[
"@�\"\u0014��&m<\u0017�5\u0010��S",
[
[
"Spec.P256.MontgomeryMultiplication.PointDouble.lemma_xToSpecification",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
"refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1",
"typing_Spec.P256.Definitions.prime256"
],
0,
"29daca9507bdd627c525aa82f9ba2d17"
],
[
"Spec.P256.MontgomeryMultiplication.PointDouble.lemma_xToSpecification",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
],
0,
"da28f6dd1e6ed70a952ac83e8dd9f12a"
],
[
"Spec.P256.MontgomeryMultiplication.PointDouble.lemma_xToSpecification",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
"equation_Spec.P256._point_double",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"refinement_interpretation_Tm_refine_8807a8a6db5cf1a86cc29f7b64a93885",
"refinement_interpretation_Tm_refine_93e2420a1bc2654a04bc10881f331e3b",
"refinement_interpretation_Tm_refine_a92851949b382679e8dc999df60d181e"
],
0,
"e1ef097de3e55c2cca36fa654d0eb4b3"
],
[
"Spec.P256.MontgomeryMultiplication.PointDouble.lemma_yToSpecification",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.P256.Definitions.prime256",
"equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
],
0,
"7bb6654e41690119d3f164f1846ea4ad"
],
[
"Spec.P256.MontgomeryMultiplication.PointDouble.lemma_yToSpecification",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat",
"equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
],
0,
"dc9471f7cbdcd16dc427c7173af0d490"
],
[
"Spec.P256.MontgomeryMultiplication.PointDouble.lemma_yToSpecification",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
"equation_Spec.P256._point_double", "int_typing",
"lemma_Spec.P256.MontgomeryMultiplication.lemmaToDomainAndBackIsTheSame",
"primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a92851949b382679e8dc999df60d181e",
"refinement_interpretation_Tm_refine_a9a8ee103221296ed130a43a8be51fb9",
"refinement_interpretation_Tm_refine_ac652f9023b70de96af3f923ebf68db3",
"refinement_interpretation_Tm_refine_cf60fc7ec5c165f556fc4bba108ab85b",
"refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
],
0,
"9f68781c33c06495f8a88c80c3555ea3"
],
[
"Spec.P256.MontgomeryMultiplication.PointDouble.lemma_zToSpecification",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1"
],
0,
"ca9dda96abd8a50d3b4802c117e61192"
],
[
"Spec.P256.MontgomeryMultiplication.PointDouble.lemma_zToSpecification",
2,
2,
1,
[ "@query" ],
0,
"bda35c403a628ead06a4e9881f51ec7b"
],
[
"Spec.P256.MontgomeryMultiplication.PointDouble.lemma_zToSpecification",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.P256.MontgomeryMultiplication.PointDouble.prime",
"equation_Spec.P256._point_double",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"refinement_interpretation_Tm_refine_4429a03440a4f885fdd4b2268b6cb06f"
],
0,
"812add578385ab64ec33b1d7e63850ee"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...