Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
Hacl.Spec.Curve25519.Field51.Definition.fst.hints
[
"{�q��&K�%w�w/\"�",
[
[
"Hacl.Spec.Curve25519.Field51.Definition.s64x5",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Curve25519.Field51.Definition.scale64",
"refinement_interpretation_Tm_refine_f29871d3a89d1e1bc374a18797629923"
],
0,
"af7a3361a9bb73795a0964ba9b4adbd8"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.s128x5",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Curve25519.Field51.Definition.scale128",
"refinement_interpretation_Tm_refine_53e76104623db325c3ccc5c7426058ab"
],
0,
"c8791e25def4ec1d43628b04d107955b"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.op_Plus_Star",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"53564a60cbf9e1cbe8885c117ee7253d"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.op_Star_Star",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"b764308e675b1a5e471f9e034bff0216"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.lemma_mul_le_scale64",
1,
2,
1,
[ "@query" ],
0,
"046c6ee01a88f7ad739f557bb6ede56c"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.op_Star_Hat",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Curve25519.Field51.Definition.scale64",
"equation_Hacl.Spec.Curve25519.Field51.Definition.scale64_5",
"equation_Prims.nat", "int_inversion", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_663c12b322f48469426a5b8197cd0ebb",
"refinement_interpretation_Tm_refine_f29871d3a89d1e1bc374a18797629923"
],
0,
"132dbf1a86ee96b75f0d977db42764d5"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.pow51",
1,
2,
1,
[ "@query" ],
0,
"9b00eb76c12e606c97f87f7ed1c9b2d4"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.mask51",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_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.U64@tok"
],
0,
"e3e6a04174d26796a85bf1985aa26d96"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.felem_fits1",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"348e327e6b69e58a247c4dff01b106cd"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.felem_wide_fits1",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.U128@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"8a2774596562c289534188971c4007aa"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.felem_fits5",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Curve25519.Field51.Definition.scale64_5",
"equation_Prims.nat",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__5",
"refinement_interpretation_Tm_refine_663c12b322f48469426a5b8197cd0ebb"
],
0,
"0e792d415174a517b976388938a3a52a"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.felem_wide_fits5",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Curve25519.Field51.Definition.scale128_5",
"equation_Prims.nat",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__5",
"refinement_interpretation_Tm_refine_3781545d89a72c1167cd3e7b244dbf3c"
],
0,
"5a2cccafc55674f0736e565917462086"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.as_nat5",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a",
"typing_Hacl.Spec.Curve25519.Field51.Definition.pow51",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"c71ac13511a1bc96aa32cfc4d7dc0cba"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.wide_as_nat5",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U128@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_4b944ca09ad96bece941715cac814505",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_fd395a7c68ba47ba743b0f42bf0c166a",
"typing_Hacl.Spec.Curve25519.Field51.Definition.pow51"
],
0,
"b563cf723f38db07bf9e8f08c3193f96"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.feval",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"d170861316b4ffc87483944695b71548"
],
[
"Hacl.Spec.Curve25519.Field51.Definition.feval_wide",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"77dfe50b7b2e8b57d96c03c306438992"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...