Revision 027cee49342e5e1ac0ccf4ca6e4b5b868e70a0a2 authored by Aseem Rastogi on 22 March 2020, 07:14:03 UTC, committed by Aseem Rastogi on 22 March 2020, 07:14:03 UTC
1 parent df0c85e
Spec.Agile.DH.fst.hints
[
"�@�GvJlC�\u0015\\9��`_",
[
[
"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,
"9752f524182df97b999ea2a704a2c9e3"
],
[
"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,
"ea700aac1cc32e03b487d2c6174319d2"
],
[
"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,
"dbdacef51b8beb1330880a4c282d7775"
],
[
"Spec.Agile.DH.order",
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,
"aa16b1a85a1a1b631c076bf81d3364b7"
],
[
"Spec.Agile.DH.clamp",
1,
2,
1,
[ "@query", "assumption_Spec.Agile.DH.algorithm__uu___haseq" ],
0,
"45d2d5ea2e4c37d8620203750d136676"
],
[
"Spec.Agile.DH.clamp",
2,
2,
1,
[ "@query", "assumption_Spec.Agile.DH.algorithm__uu___haseq" ],
0,
"00faba0106e9480a9d55204f6781b2db"
],
[
"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_P256@tok",
"equation_Lib.Sequence.lseq", "equation_Spec.Agile.DH.scalar",
"equation_Spec.Agile.DH.size_key",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm",
"refinement_interpretation_Tm_refine_9f39d862c04a0727f7dcc14ce89891ac",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"b26011b323a45be5e4aa2b09707e4e27"
],
[
"Spec.Agile.DH.scalarmult",
1,
2,
1,
[ "@query", "assumption_Spec.Agile.DH.algorithm__uu___haseq" ],
0,
"465fd523734f960b77d682ab19e70725"
],
[
"Spec.Agile.DH.scalarmult",
2,
2,
1,
[ "@query", "assumption_Spec.Agile.DH.algorithm__uu___haseq" ],
0,
"acb67b53e86a601a17033c38a8b77068"
],
[
"Spec.Agile.DH.scalarmult",
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_P256@tok",
"equation_Lib.Sequence.lseq", "equation_Spec.Agile.DH.scalar",
"equation_Spec.Agile.DH.serialized_point",
"equation_Spec.Agile.DH.size_key",
"equation_Spec.Agile.DH.size_public",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm",
"refinement_interpretation_Tm_refine_9f39d862c04a0727f7dcc14ce89891ac",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"77f8791a534c3d0659886c9fbc59be95"
],
[
"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",
"disc_equation_Spec.Agile.DH.DH_Curve25519",
"disc_equation_Spec.Agile.DH.DH_P256",
"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.unsigned",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
"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", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"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",
"refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_Spec.Agile.DH.size_public", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"67551f3913ca437c08be1514ed25db81"
],
[
"Spec.Agile.DH.secret_to_public",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Prims.Cons",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Agile.DH.DH_P256", "data_elim_Prims.Cons",
"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", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.Agile.DH.scalar",
"equation_Spec.Agile.DH.size_key",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Curve25519.basepoint_list",
"equation_Spec.Curve25519.basepoint_lseq",
"equation_Spec.Curve25519.one", "equation_Spec.Curve25519.zero",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm",
"function_token_typing_Lib.IntTypes.byte_t", "int_inversion",
"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",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f6c48ed0e29b67224e0bd751c7777fe9",
"token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Prims.pow2", "typing_Spec.Agile.DH.size_key",
"typing_Spec.Curve25519.basepoint_list",
"typing_Spec.Curve25519.basepoint_lseq",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"7a8672f1330d95d379631e1d9e0d0ba4"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...