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.Bignum.X64.fst.hints
[
"���z��@�u� p����",
[
[
"Vale.Bignum.X64.reveal_flags",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"equation_Vale.Bignum.X64.bool_to_nat1",
"equation_Vale.Bignum.X64.flag_cf",
"equation_Vale.Bignum.X64.flag_of",
"equation_Vale.Bignum.X64.flags_t",
"function_token_typing_Prims.__cache_version_number__",
"primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0",
"typing_Vale.X64.Decls.cf", "typing_Vale.X64.Decls.overflow"
],
0,
"0d4f375b1d564a3f1fc2c8fa952f2510"
],
[
"Vale.Bignum.X64.lemma_add_hi_lo64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Bignum.Defs.add_hi_def",
"equation_Vale.Bignum.Defs.add_lo_def",
"equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Vale.Bignum.Defs.add_hi"
],
0,
"9eb3a88d84fbbffaf9f92e8e7949b15a"
],
[
"Vale.Bignum.X64.va_lemma_Adcx_64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"constructor_distinct_Prims.Cons",
"constructor_distinct_Vale.X64.Machine_s.Block",
"disc_equation_Prims.Cons", "disc_equation_Vale.X64.Machine_s.Block",
"eq2-interp", "equation_Prims.nat",
"equation_Vale.Bignum.Defs.add_hi_def",
"equation_Vale.Bignum.Defs.add_lo_def",
"equation_Vale.Bignum.X64.bool_to_nat1",
"equation_Vale.Bignum.X64.flag_cf",
"equation_Vale.Bignum.X64.flag_of",
"equation_Vale.Bignum.X64.flags_t",
"equation_Vale.Bignum.X64.maintain_of",
"equation_Vale.Bignum.X64.update_cf",
"equation_Vale.Def.Types_s.add_wrap",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_is_dst_opr64",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_update_operand",
"equation_Vale.X64.State.eval_operand",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"int_typing", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "proj_equation_Prims.Cons_hd",
"proj_equation_Prims.Cons_tl",
"proj_equation_Vale.X64.Machine_s.Block_block",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Vale.X64.Machine_s.Block_block",
"projection_inverse_Vale.X64.Machine_s.Block_t_ins",
"projection_inverse_Vale.X64.Machine_s.Block_t_ocmp",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
"refinement_interpretation_Tm_refine_29dae9dfe163386903401490df44e922",
"refinement_interpretation_Tm_refine_449c6217aeda38f4b46138844d86130d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f5b7985bc3c2bc5a5dee962352a41f5d",
"typing_Vale.Bignum.X64.flag_cf", "typing_Vale.Def.Types_s.add_wrap",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.Decls.maintained_of",
"typing_Vale.X64.Decls.updated_cf",
"typing_Vale.X64.Decls.va_is_dst_opr64",
"typing_Vale.X64.Decls.va_update_operand",
"typing_Vale.X64.Decls.valid_cf",
"typing_Vale.X64.InsBasic.va_code_Adcx64Wrap",
"typing_Vale.X64.InsBasic.va_lemma_Adcx64Wrap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.eval_operand"
],
0,
"dfc167d66554d96608a9f4c6bac27b77"
],
[
"Vale.Bignum.X64.va_wpProof_Adcx_64",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
"bool_inversion", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.QuickCode.Mod_reg",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equality_tok_Vale.X64.QuickCode.Mod_None@tok",
"equation_Vale.Bignum.X64.flags_t",
"equation_Vale.Bignum.X64.va_wp_Adcx_64",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_is_dst_opr64",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_operand_dst_opr64",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Decls.va_update_operand",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.State.eval_operand",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"kinding_Vale.X64.QuickCode.mod_t@tok",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.QuickCode.Mod_reg__0",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_memTaint",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.Decls.va_is_dst_opr64",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_update_operand",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.eval_operand",
"typing_tok_Vale.X64.QuickCode.Mod_None@tok", "unit_typing"
],
0,
"eb28e075c60938340532bafed4c53a76"
],
[
"Vale.Bignum.X64.va_quick_Adcx_64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"09526476f1b6e35fb85796fbd873a8f0"
],
[
"Vale.Bignum.X64.va_lemma_Adox_64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"constructor_distinct_Prims.Cons",
"constructor_distinct_Vale.X64.Machine_s.Block",
"disc_equation_Prims.Cons", "disc_equation_Vale.X64.Machine_s.Block",
"eq2-interp", "equation_Prims.nat",
"equation_Vale.Bignum.Defs.add_hi_def",
"equation_Vale.Bignum.Defs.add_lo_def",
"equation_Vale.Bignum.X64.bool_to_nat1",
"equation_Vale.Bignum.X64.flag_cf",
"equation_Vale.Bignum.X64.flag_of",
"equation_Vale.Bignum.X64.flags_t",
"equation_Vale.Bignum.X64.maintain_cf",
"equation_Vale.Bignum.X64.update_of",
"equation_Vale.Def.Types_s.add_wrap",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_is_dst_opr64",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_update_operand",
"equation_Vale.X64.State.eval_operand",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"int_typing", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "proj_equation_Prims.Cons_hd",
"proj_equation_Prims.Cons_tl",
"proj_equation_Vale.X64.Machine_s.Block_block",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Vale.X64.Machine_s.Block_block",
"projection_inverse_Vale.X64.Machine_s.Block_t_ins",
"projection_inverse_Vale.X64.Machine_s.Block_t_ocmp",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
"refinement_interpretation_Tm_refine_1d611ab70e7b74556741b4d59722e097",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_702be81f1408cfb1e18adbec13641d99",
"refinement_interpretation_Tm_refine_91b21bda257faf7d7870e0299e500a49",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Vale.Bignum.Defs.add_lo", "typing_Vale.Bignum.X64.flag_of",
"typing_Vale.Def.Types_s.add_wrap",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.Decls.maintained_cf",
"typing_Vale.X64.Decls.updated_of",
"typing_Vale.X64.Decls.va_is_dst_opr64",
"typing_Vale.X64.Decls.va_update_operand",
"typing_Vale.X64.Decls.valid_of",
"typing_Vale.X64.InsBasic.va_code_Adox64Wrap",
"typing_Vale.X64.InsBasic.va_lemma_Adox64Wrap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.eval_operand"
],
0,
"db880f5d3f5d68edd30abc0b4b91eee8"
],
[
"Vale.Bignum.X64.va_wpProof_Adox_64",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
"bool_inversion", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.QuickCode.Mod_reg",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equality_tok_Vale.X64.QuickCode.Mod_None@tok",
"equation_Vale.Bignum.X64.flags_t",
"equation_Vale.Bignum.X64.va_wp_Adox_64",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_is_dst_opr64",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_operand_dst_opr64",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Decls.va_update_operand",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.State.eval_operand",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"kinding_Vale.X64.QuickCode.mod_t@tok",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.QuickCode.Mod_reg__0",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_memTaint",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.Decls.va_is_dst_opr64",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_update_operand",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.eval_operand",
"typing_tok_Vale.X64.QuickCode.Mod_None@tok", "unit_typing"
],
0,
"2206fc787b6141942e6263e296b0f0e7"
],
[
"Vale.Bignum.X64.va_quick_Adox_64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"f9e351da2cd9ebdab167830874a5f649"
],
[
"Vale.Bignum.X64.va_lemma_Mulx_64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Prims.Cons",
"constructor_distinct_Vale.X64.Machine_s.Block",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"disc_equation_Prims.Cons", "disc_equation_Vale.X64.Machine_s.Block",
"eq2-interp", "equation_Prims.nat",
"equation_Vale.Bignum.Defs.mul_hi_def",
"equation_Vale.Bignum.Defs.mul_lo_def",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.State.eval_operand",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"int_typing", "proj_equation_Prims.Cons_hd",
"proj_equation_Prims.Cons_tl",
"proj_equation_Vale.X64.Machine_s.Block_block",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Vale.X64.Machine_s.Block_block",
"projection_inverse_Vale.X64.Machine_s.Block_t_ins",
"projection_inverse_Vale.X64.Machine_s.Block_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.eval_operand"
],
0,
"32cc79654581e8911759b8190cc7c528"
]
]
]
Computing file changes ...
