Revision cef6a8e821f55e71b791555d22b45bd3debc2596 authored by Jonathan Protzenko on 08 May 2020, 16:26:29 UTC, committed by GitHub on 08 May 2020, 16:26:29 UTC
OCaml API: Don't run unit tests which require unsupported features
Vale.Curve25519.FastUtil_helpers.fst.hints
[
"ߣ(�V\\�F�V4�_�>�",
[
[
"Vale.Curve25519.FastUtil_helpers.sub_carry",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Curve25519.Fast_defs.bit",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b51b45ce195a33a465eab411d92fdae9",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"416b55b0a5a908982db39e1093e3de58"
],
[
"Vale.Curve25519.FastUtil_helpers.lemma_sub2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat",
"equation_Vale.Curve25519.FastUtil_helpers.sub_carry",
"equation_Vale.Curve25519.Fast_defs.bit",
"equation_Vale.Curve25519.Fast_defs.pow2_two",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b51b45ce195a33a465eab411d92fdae9",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"0fdc6d58759030d2be57369fff6a71e6"
],
[
"Vale.Curve25519.FastUtil_helpers.lemma_pow2_int_23",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Curve25519.FastUtil_helpers.pow2int_three",
"equation_Vale.Curve25519.FastUtil_helpers.pow2int_two",
"int_inversion", "int_typing", "projection_inverse_BoxInt_proj_0"
],
0,
"2bb954a9170c08df2e753de5004163ef"
],
[
"Vale.Curve25519.FastUtil_helpers.lemma_pow2_int_34",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Curve25519.FastUtil_helpers.pow2int_four",
"equation_Vale.Curve25519.FastUtil_helpers.pow2int_three",
"int_inversion", "projection_inverse_BoxInt_proj_0",
"typing_Vale.Curve25519.FastUtil_helpers.pow2int_four"
],
0,
"3dd5313a4130cf9ddf642d6d7590793d"
],
[
"Vale.Curve25519.FastUtil_helpers.lemma_sub3",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"4aaff5089e60cceb52e28aa39b71b4a3"
],
[
"Vale.Curve25519.FastUtil_helpers.lemma_sub3",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Curve25519.Fast_defs.bit",
"equation_Vale.Def.Words_s.nat64", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"true_interp"
],
0,
"d67775523511222197665cfb1cc6d00e"
],
[
"Vale.Curve25519.FastUtil_helpers.lemma_sub3",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Curve25519.Fast_defs.pow2_three",
"equation_Vale.Curve25519.Fast_defs.pow2_two",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_548c05480199a0cca35a3fd3322151fe"
],
0,
"a470f8696de1869fce7a6fc7b1d6f9f3"
],
[
"Vale.Curve25519.FastUtil_helpers.lemma_sub3",
4,
0,
0,
[ "@query" ],
0,
"a9176cccde828149b64227d4f6558f61"
],
[
"Vale.Curve25519.FastUtil_helpers.lemma_sub3",
5,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Curve25519.FastUtil_helpers.sub_carry",
"equation_Vale.Curve25519.Fast_defs.bit",
"equation_Vale.Def.Words_s.nat64", "int_inversion", "int_typing",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_1443269d7eadc969721b34d6f64e8860",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_548c05480199a0cca35a3fd3322151fe",
"refinement_interpretation_Tm_refine_a3acfd6805ff36eae3bce4fb321c9713",
"refinement_interpretation_Tm_refine_b51b45ce195a33a465eab411d92fdae9"
],
0,
"e20ede24aca012ac72f9b0f0d797d265"
],
[
"Vale.Curve25519.FastUtil_helpers.lemma_sub",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"6525a8b680b079da7f6277b059c8c5f0"
],
[
"Vale.Curve25519.FastUtil_helpers.lemma_sub",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Curve25519.Fast_defs.bit",
"equation_Vale.Def.Words_s.nat64", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"true_interp"
],
0,
"9748351b2aabbf7e0b7cd084ea8e2b42"
],
[
"Vale.Curve25519.FastUtil_helpers.lemma_sub",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Curve25519.Fast_defs.pow2_four",
"equation_Vale.Curve25519.Fast_defs.pow2_three",
"equation_Vale.Curve25519.Fast_defs.pow2_two",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a415f19ed81e26742f6055320e3cb3d0"
],
0,
"674dcb39da190d5444d1b34d2336cb20"
],
[
"Vale.Curve25519.FastUtil_helpers.lemma_sub",
4,
0,
0,
[ "@query" ],
0,
"9adaac1dcf1ff7f0bfdbda60b5aff9b0"
],
[
"Vale.Curve25519.FastUtil_helpers.lemma_sub",
5,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Curve25519.FastUtil_helpers.sub_carry",
"equation_Vale.Curve25519.Fast_defs.bit",
"equation_Vale.Def.Words_s.nat64", "int_inversion", "int_typing",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_1443269d7eadc969721b34d6f64e8860",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a3acfd6805ff36eae3bce4fb321c9713",
"refinement_interpretation_Tm_refine_a415f19ed81e26742f6055320e3cb3d0",
"refinement_interpretation_Tm_refine_b51b45ce195a33a465eab411d92fdae9"
],
0,
"a0d185c12e1dffc97279ec752ec8b6cf"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...