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.X64.Leakage_s.fst.hints
[
"��\b����J\u0013\u0001͈��.�",
[
[
"Vale.X64.Leakage_s.publicCfFlagValuesAreSame",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Pervasives.Native.option__uu___haseq",
"equation_Prims.eqtype",
"equation_Vale.X64.Machine_Semantics_s.flag_val_t",
"function_token_typing_Prims.bool",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"5ac545ff270ab96fd6a9a275d49ed2d1"
],
[
"Vale.X64.Leakage_s.publicOfFlagValuesAreSame",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Pervasives.Native.option__uu___haseq",
"equation_Prims.eqtype",
"equation_Vale.X64.Machine_Semantics_s.flag_val_t",
"function_token_typing_Prims.bool",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"239f4c62c96257b137fb3e9b6e8279da"
],
[
"Vale.X64.Leakage_s.publicRegisterValuesAreSame",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.Def.Types_s.quad32",
"typing_Vale.X64.Machine_s.__proj__Reg__item__rf"
],
0,
"9c6c4ec16a34705530ae070bca42a40d"
],
[
"Vale.X64.Leakage_s.constTimeInvariant",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_Prims.list__uu___haseq",
"assumption_Vale.X64.Machine_s.observation__uu___haseq",
"equation_Prims.eqtype",
"kinding_Vale.X64.Machine_s.observation@tok",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"9000017fbe994d706adc9dc0162c6f59"
],
[
"Vale.X64.Leakage_s.isConstantTimeGivenStates",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_Prims.list__uu___haseq",
"assumption_Vale.X64.Machine_s.observation__uu___haseq",
"equation_Prims.eqtype",
"kinding_Vale.X64.Machine_s.observation@tok",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"ee4f464d801c5076120666618634d89c"
],
[
"Vale.X64.Leakage_s.is_explicit_leakage_free_lhs",
1,
1,
0,
[ "@query" ],
0,
"c99401cd16d9703c7e6d961f575f9589"
],
[
"Vale.X64.Leakage_s.is_explicit_leakage_free_rhs",
1,
1,
0,
[ "@query" ],
0,
"25cb7dcc93f1ec21474c6ba7e4c7f545"
],
[
"Vale.X64.Leakage_s.publicCfFlagValuesAreSame",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Pervasives.Native.option__uu___haseq",
"equation_Prims.eqtype",
"equation_Vale.X64.Machine_Semantics_s.flag_val_t",
"function_token_typing_Prims.bool",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"6d8bd288984f98b07063ef60bc6fb694"
],
[
"Vale.X64.Leakage_s.publicOfFlagValuesAreSame",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Pervasives.Native.option__uu___haseq",
"equation_Prims.eqtype",
"equation_Vale.X64.Machine_Semantics_s.flag_val_t",
"function_token_typing_Prims.bool",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"83e2cf63370acafc467db890350ff1e3"
],
[
"Vale.X64.Leakage_s.publicRegisterValuesAreSame",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.Def.Types_s.quad32",
"typing_Vale.X64.Machine_s.__proj__Reg__item__rf"
],
0,
"2262add7b31201c3f86b07cbdc24f9b7"
],
[
"Vale.X64.Leakage_s.constTimeInvariant",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_Prims.list__uu___haseq",
"assumption_Vale.X64.Machine_s.observation__uu___haseq",
"equation_Prims.eqtype",
"kinding_Vale.X64.Machine_s.observation@tok",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"65823c127f7ddb4847a6a16f1d92f911"
],
[
"Vale.X64.Leakage_s.isConstantTimeGivenStates",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_Prims.list__uu___haseq",
"assumption_Vale.X64.Machine_s.observation__uu___haseq",
"equation_Prims.eqtype",
"kinding_Vale.X64.Machine_s.observation@tok",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"23f039ef18c0994a1f1f775c6970c27f"
],
[
"Vale.X64.Leakage_s.is_explicit_leakage_free_lhs",
2,
1,
0,
[ "@query" ],
0,
"37287b7a4161a42d97c7d7fdfb0a1d19"
],
[
"Vale.X64.Leakage_s.is_explicit_leakage_free_rhs",
2,
1,
0,
[ "@query" ],
0,
"edbbfe8b83c65dd2e76ae9758382f289"
]
]
]
Computing file changes ...
