Revision 059787e63538941130606248805cab290fdbc5d7 authored by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC, committed by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC
1 parent 03f1e46
Spec.P256.fst.hints
[
"�H�k�\u0001(*�R�\u0013^�Ǵ",
[
[
"Spec.P256.bCoordinateP256",
1,
0,
0,
[ "@query" ],
0,
"c70808a1dc74709ecd06ae8641369b34"
],
[
"Spec.P256.basePoint",
1,
0,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"c419e912a5701e124500f450c210b424"
],
[
"Spec.P256._point_double",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.P256.Definitions.point_nat_prime",
"equation_Spec.P256.Definitions.prime256",
"primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"refinement_interpretation_Tm_refine_3952aa58162b0446b1249aba52d1eb89",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"ddd2516263852e6b5f31dc082a37e199"
],
[
"Spec.P256._point_add",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.P256.Definitions.point_nat_prime",
"equation_Spec.P256.Definitions.prime256", "int_typing",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"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_3952aa58162b0446b1249aba52d1eb89",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"true_interp"
],
0,
"f3bdc984c4431504487ab90c9647e266"
],
[
"Spec.P256._norm",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.P256.Definitions.prime256",
"equation_Spec.P256.Lemmas.modp_inv2_pow",
"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.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"fd70c6dbc93cf5fb14431b507d7bf5d8"
],
[
"Spec.P256.scalar",
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.minint", "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,
"5de1e563484c737302737c296ea82776"
],
[
"Spec.P256.ith_bit",
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.minint", "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,
"2c4748dfa0a98aeb3c8aae90c591d9b8"
],
[
"Spec.P256.ith_bit",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Division",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_31c7d3d85d92cb942c95a78642e657c7",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"3c2804861c0cc765706fa52ae988f68d"
],
[
"Spec.P256._ml_step",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U64",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_31c7d3d85d92cb942c95a78642e657c7",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"15d434707c27ec092969dc83be97266d"
],
[
"Spec.P256.scalar_multiplication",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"equation_Spec.P256.Definitions.prime256",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
"typing_Spec.P256.Definitions.prime256"
],
0,
"0315f506d9671928e6031a18da2873e7"
],
[
"Spec.P256.secret_to_public",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"equation_Spec.P256.Definitions.prime256",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
"typing_Spec.P256.Definitions.prime256"
],
0,
"42e054587ee70c93339df0fc163f8863"
],
[
"Spec.P256.isPointOnCurve",
1,
0,
0,
[ "@query" ],
0,
"3ef111374c8446af37b129e1afadf6d4"
],
[
"Spec.P256.point_prime_to_coordinates",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "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,
"3ccc71e1db438619a781d9b7cec9c580"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...