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
Spec.Agile.DH.fst.hints
[
"�䋺���\u0010'\r�cX�ʌ",
[
[
"Spec.Agile.DH.size_key",
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.S8",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Spec.Agile.DH.DH_Curve25519",
"disc_equation_Spec.Agile.DH.DH_P256",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm",
"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,
"6d31c3488016a020c4b4568effc66613"
],
[
"Spec.Agile.DH.size_public",
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.S8",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Spec.Agile.DH.DH_Curve25519",
"disc_equation_Spec.Agile.DH.DH_P256",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm",
"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,
"4e2670e3d53b45427e3e0fe4d9423425"
],
[
"Spec.Agile.DH.prime",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Spec.Agile.DH.DH_Curve25519",
"disc_equation_Spec.Agile.DH.DH_P256",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm"
],
0,
"c7828fdf92f2deb4b8e5b8e405c23d91"
],
[
"Spec.Agile.DH.clamp",
1,
2,
1,
[ "@query", "assumption_Spec.Agile.DH.algorithm__uu___haseq" ],
0,
"b4c64936036cc6f906fa318e3dc06ef6"
],
[
"Spec.Agile.DH.clamp",
2,
2,
1,
[ "@query", "assumption_Spec.Agile.DH.algorithm__uu___haseq" ],
0,
"33ec9f0b469885d28afaf4915403990b"
],
[
"Spec.Agile.DH.clamp",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"disc_equation_Spec.Agile.DH.DH_Curve25519",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equation_Lib.Sequence.lseq", "equation_Spec.Agile.DH.scalar",
"equation_Spec.Agile.DH.size_key",
"refinement_interpretation_Tm_refine_348df7b05282e4d51c99c6591007846e",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"4d3e6b914d9a5ae261736341faa854a4"
],
[
"Spec.Agile.DH.dh",
1,
2,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Agile.DH.DH_P256",
"disc_equation_Spec.Agile.DH.DH_Curve25519",
"disc_equation_Spec.Agile.DH.DH_P256",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Agile.DH.scalar",
"equation_Spec.Agile.DH.serialized_point",
"equation_Spec.Agile.DH.size_key",
"equation_Spec.Agile.DH.size_public", "equation_Spec.Curve25519.one",
"equation_Spec.Curve25519.serialized_point",
"equation_Spec.Curve25519.zero",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_Spec.Agile.DH.size_public", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"9242d3b7ec5761ab2d9d39d807537ccf"
],
[
"Spec.Agile.DH.secret_to_public",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Agile.DH.DH_P256",
"disc_equation_Spec.Agile.DH.DH_Curve25519",
"disc_equation_Spec.Agile.DH.DH_P256",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Prims.nat",
"equation_Spec.Agile.DH.scalar", "equation_Spec.Agile.DH.size_key",
"equation_Spec.Agile.DH.size_public",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.IntTypes.unsigned", "typing_Spec.Agile.DH.size_key",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"88f9c35bc67f58bc54a0f158b61025ef"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...