Revision 724d1045f60f13d79df1afc5190955afdfa73ec1 authored by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC, committed by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC
Co-authored-by: @protz
1 parent ca37fbf
Vale.X64.Regs.fst.hints
[
",#\b>�)���\u001d������",
[
[
"Vale.X64.Regs.sel",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
"kinding_Vale.Def.Words_s.four@tok",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Lib.Map16.sel16", "typing_Vale.X64.Machine_s.n_regs"
],
0,
"b31ca3907e7532bc699efd2cc1ad34bc"
],
[
"Vale.X64.Regs.upd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"equation_Prims.nat", "equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file", "int_inversion",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.X64.Machine_s.n_regs"
],
0,
"231ef818cdc38373f56c35d3aa40f117"
],
[
"Vale.X64.Regs.eta",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "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.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_0233a8fa9dab68752b72fc7b92282347",
"refinement_interpretation_Tm_refine_09c71f8bf0211aae98d104f1b7a5ec29",
"refinement_interpretation_Tm_refine_133499ff74fb42166c14fa71c9de0eea",
"refinement_interpretation_Tm_refine_26eb76be4be69db887a85d42b1f2b300",
"refinement_interpretation_Tm_refine_38f357697d1871728b6efa5b2c6cde08",
"refinement_interpretation_Tm_refine_43c5913b2b7ffe79bfc84b338aebf2db",
"refinement_interpretation_Tm_refine_44029dc661215e748b7d118126bebb66",
"refinement_interpretation_Tm_refine_5547be08e4bf37ada42c4f9514d38ed6",
"refinement_interpretation_Tm_refine_561dadd74cf2df492c815a73732ca860",
"refinement_interpretation_Tm_refine_5f681121df65376329bcc4a806c6c40d",
"refinement_interpretation_Tm_refine_81c1990eca1445fdc599682f9293121b",
"refinement_interpretation_Tm_refine_8867d2dd49d971c543d8bd3f041f24b5",
"refinement_interpretation_Tm_refine_8c5ee1b914ba03e7354f7cc43de1b254",
"refinement_interpretation_Tm_refine_9ccaa6f5896e99675865f9c84a36e019",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_fd01003f793c223ce122405177249431",
"refinement_interpretation_Tm_refine_fe479871b3967d0c9b8d8614ccf88035"
],
0,
"7cde881e77e704806841f1ecc511dfa5"
],
[
"Vale.X64.Regs.of_fun",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"data_elim_Vale.X64.Machine_s.Reg", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Lib.Map16.map16",
"equation_Vale.Lib.Map16.map8", "equation_Vale.Lib.Map16.sel16",
"equation_Vale.Lib.Map16.sel2", "equation_Vale.Lib.Map16.sel4",
"equation_Vale.Lib.Map16.sel8",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"function_token_typing_Vale.X64.Regs.sel", "int_inversion",
"int_typing",
"interpretation_Tm_abs_944a3b8446322c416b889c89aea1ec5d",
"primitive_Prims.op_LessThan",
"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_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.X64.Machine_s.__proj__Reg__item__rf",
"typing_Vale.X64.Machine_s.n_regs"
],
0,
"15c688287f1d0c6860bfb2d6e0df2551"
],
[
"Vale.X64.Regs.lemma_upd_eq",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.map16",
"equation_Vale.Lib.Map16.map2", "equation_Vale.Lib.Map16.map4",
"equation_Vale.Lib.Map16.map8", "equation_Vale.Lib.Map16.sel16",
"equation_Vale.Lib.Map16.sel2", "equation_Vale.Lib.Map16.sel4",
"equation_Vale.Lib.Map16.sel8", "equation_Vale.Lib.Map16.upd16",
"equation_Vale.Lib.Map16.upd2", "equation_Vale.Lib.Map16.upd4",
"equation_Vale.Lib.Map16.upd8",
"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",
"fuel_guarded_inversion_Vale.Def.Words_s.four", "int_inversion",
"int_typing", "primitive_Prims.op_LessThan",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.X64.Machine_s.__proj__Reg__item__rf"
],
0,
"a48d7118d2c7d8908d17449a267fe695"
],
[
"Vale.X64.Regs.lemma_upd_ne",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"data_elim_Vale.X64.Machine_s.Reg", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.map16",
"equation_Vale.Lib.Map16.map2", "equation_Vale.Lib.Map16.map4",
"equation_Vale.Lib.Map16.map8", "equation_Vale.Lib.Map16.sel16",
"equation_Vale.Lib.Map16.sel2", "equation_Vale.Lib.Map16.sel4",
"equation_Vale.Lib.Map16.sel8", "equation_Vale.Lib.Map16.upd16",
"equation_Vale.Lib.Map16.upd2", "equation_Vale.Lib.Map16.upd4",
"equation_Vale.Lib.Map16.upd8", "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",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg", "int_inversion",
"int_typing", "primitive_Prims.op_LessThan",
"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",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.X64.Machine_s.__proj__Reg__item__rf",
"typing_Vale.X64.Machine_s.n_regs"
],
0,
"cb0ab0507c70c5766f5f0c476fcb63e1"
],
[
"Vale.X64.Regs.lemma_equal_intro",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat64",
"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.Regs.equal",
"equation_Vale.X64.Regs.regs_def",
"function_token_typing_Vale.Lib.Map16.sel",
"function_token_typing_Vale.X64.Regs.sel", "int_inversion",
"int_typing",
"interpretation_Tm_abs_0711a7b6edebe3f5670f053e65e8f8fa",
"interpretation_Tm_abs_846ee973e6d1a3108929d7bd977178e1",
"interpretation_Tm_abs_944a3b8446322c416b889c89aea1ec5d",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.X64.Machine_s.Reg_r",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64"
],
0,
"494ae8c6e5af6cf19019280174f5d040"
],
[
"Vale.X64.Regs.lemma_equal_elim",
1,
1,
0,
[ "@query", "eq2-interp", "equation_Vale.X64.Regs.equal" ],
0,
"4c6bd7590b6581488b7a040c39ad663e"
],
[
"Vale.X64.Regs.lemma_eta",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Lib.Map16.map16",
"equation_Vale.Lib.Map16.map2", "equation_Vale.Lib.Map16.map4",
"equation_Vale.Lib.Map16.map8", "equation_Vale.Lib.Map16.sel16",
"equation_Vale.Lib.Map16.sel2", "equation_Vale.Lib.Map16.sel4",
"equation_Vale.Lib.Map16.sel8",
"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",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"function_token_typing_Vale.X64.Regs.eta",
"function_token_typing_Vale.X64.Regs.sel", "int_inversion",
"int_typing",
"interpretation_Tm_abs_5b1e367a2d267a2ce46a13b4fa6586a8",
"interpretation_Tm_abs_944a3b8446322c416b889c89aea1ec5d",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"primitive_Prims.op_LessThan",
"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_Vale.X64.Machine_s.Reg_r",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"typing_Vale.X64.Machine_s.__proj__Reg__item__rf",
"typing_Vale.X64.Regs.eta", "typing_Vale.X64.Regs.eta_sel"
],
0,
"6167adedd5e31b33890dcdce2a55b2bb"
]
]
]
Computing file changes ...