Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Vale.X64.Instructions_s.fst.hints
[
"2\u0019�9\u0006�6�1\r\u0016\u0002���",
[
[
"Vale.X64.Instructions_s.eval_Add64",
1,
1,
0,
[ "@query" ],
0,
"695772913ecc1ae17d82b2eb56555d1d"
],
[
"Vale.X64.Instructions_s.eval_AddLea64",
1,
1,
0,
[ "@query" ],
0,
"2af2132e2eb42c4d6230306b842d0e15"
],
[
"Vale.X64.Instructions_s.ins_AddLea64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "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.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"ab9a6ce822cbfd075f34c85f56b0f270"
],
[
"Vale.X64.Instructions_s.eval_AddCarry64",
1,
1,
0,
[ "@query" ],
0,
"76e7923466d11f5af655eb287250c08e"
],
[
"Vale.X64.Instructions_s.eval_Adcx64_Adox64",
1,
1,
0,
[ "@query" ],
0,
"1a9f333ee570be3fe8f2e76cf2cf656d"
],
[
"Vale.X64.Instructions_s.eval_Sub64",
1,
1,
0,
[ "@query" ],
0,
"606fe3bfd40f49db0ff7903640617aba"
],
[
"Vale.X64.Instructions_s.eval_Sbb64",
1,
1,
0,
[ "@query" ],
0,
"c3d421f429b239ca329ad8a7528638a5"
],
[
"Vale.X64.Instructions_s.eval_Mul64",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"a015aff844c98ca3a5dd0d5cfe2e4be8"
],
[
"Vale.X64.Instructions_s.eval_Mulx64",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"f959ea44b3ba88432372279ca4e6a340"
],
[
"Vale.X64.Instructions_s.eval_IMul64",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"6eccd8765f44cc51b43847135104b4ba"
],
[
"Vale.X64.Instructions_s.eval_Paddd_raw",
1,
1,
0,
[ "@query" ],
0,
"005bfb416fa967554191f3d887158402"
],
[
"Vale.X64.Instructions_s.eval_Psrldq",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_FStar.Seq.Base.length"
],
0,
"eadecc1438fb1c45c11e25f01a9f3928"
],
[
"Vale.X64.Instructions_s.eval_Pcmpeqd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"4e91e49f894dec3891102824f6340611"
],
[
"Vale.X64.Instructions_s.eval_Pextrq",
1,
1,
0,
[ "@query" ],
0,
"946a15fd43b6b25f4b0e74901ab6fbd7"
],
[
"Vale.X64.Instructions_s.eval_Pinsrd",
1,
1,
0,
[ "@query" ],
0,
"852d642efcf505e23790a05573440e12"
],
[
"Vale.X64.Instructions_s.eval_Pinsrq",
1,
1,
0,
[ "@query" ],
0,
"85f8e76dd94ed9441ede49628d244287"
],
[
"Vale.X64.Instructions_s.eval_AESNI_keygen_assist",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"84f3ac2cece55a440538c1a5f144bf82"
],
[
"Vale.X64.Instructions_s.ins_SHA256_rnds2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"58383e24c55fe057f4dff3ad8445ca93"
],
[
"Vale.X64.Instructions_s.ins_SHA256_rnds2",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"f3b7419ae29a1b2515cf464a346781c3"
]
]
]
Computing file changes ...
