Revision aa211c2d5a40dd6969fe8a469fcadfd27e8c8fe3 authored by Jonathan Protzenko on 24 April 2020, 21:11:09 UTC, committed by Jonathan Protzenko on 24 April 2020, 21:11:09 UTC
1 parent 6f91754
Vale.Bignum.X64.fst.hints
[
"�v&��t��\u001d��\u0006Ե>w",
[
[
"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,
"4b7bd14005e1cea7b1b55b5f7263b9fd"
],
[
"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,
"24b8da745cb48e511fc69cbc1c11af0c"
],
[
"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,
"f7490a800fe0eb011beeb5fe32fced4e"
],
[
"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",
"equality_tok_Vale.X64.QuickCode.Mod_None@tok",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Bignum.X64.flags_t",
"equation_Vale.Bignum.X64.va_wp_Adcx_64",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Decls.upd_register",
"equation_Vale.X64.Decls.update_operand",
"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.Memory.vale_full_heap_equal",
"equation_Vale.X64.QuickCode.t_require",
"equation_Vale.X64.QuickCode.va_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.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"kinding_Vale.X64.QuickCode.mod_t@tok",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"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_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_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.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.Decls.update_operand",
"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.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"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,
"52ee583a177f15d5622961b260adb2e6"
],
[
"Vale.Bignum.X64.va_quick_Adcx_64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"77de7dfbd72b550efe2eb23ad63c11ff"
],
[
"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,
"9437bf7f4d7adce9742f820b810bc2cc"
],
[
"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",
"equality_tok_Vale.X64.QuickCode.Mod_None@tok",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Bignum.X64.flags_t",
"equation_Vale.Bignum.X64.va_wp_Adox_64",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Decls.upd_register",
"equation_Vale.X64.Decls.update_operand",
"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.Memory.vale_full_heap_equal",
"equation_Vale.X64.QuickCode.t_require",
"equation_Vale.X64.QuickCode.va_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.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"kinding_Vale.X64.QuickCode.mod_t@tok",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"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_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_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.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.X64.CPU_Features_s.adx_enabled",
"typing_Vale.X64.Decls.update_operand",
"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.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"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,
"05967f42b530aa54337c8dc6bf2fb370"
],
[
"Vale.Bignum.X64.va_quick_Adox_64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"692e9a926fc24b14c626fd07bd7bc1c9"
],
[
"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,
"d2325c1d822d3b2b15d1b3e40cb7e529"
]
]
]
Computing file changes ...
