Revision 493d130bb523940efde89a74951e7a449fec93b0 authored by Aymeric Fromherz on 24 March 2020, 14:39:08 UTC, committed by Aymeric Fromherz on 24 March 2020, 14:39:08 UTC
Vale.X64.QuickCode.fst.hints
[
"���R\\���H\u000efy\u0012<�",
[
[
"Vale.X64.QuickCode.mod_t",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_Vale.X64.Machine_s.reg__uu___haseq",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.heaplet_id",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"09b884aac0c0be90415fe270313f77bb"
],
[
"Vale.X64.QuickCode.__proj__Mod_reg__item___0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCode.Mod_reg",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_c6bd9cf894204793a059b43e4dcbf9cc"
],
0,
"51ce6379f02ad13fa4053474584d4b67"
],
[
"Vale.X64.QuickCode.__proj__Mod_mem_heaplet__item___0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCode.Mod_mem_heaplet",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_dae911842b85add82dc5578c02955df1"
],
0,
"61e2ad1bb93ba879da876d6cdbc2c814"
],
[
"Vale.X64.QuickCode.va_Mod_reg64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"c8f3ca5025df824004f70755dd98a428"
],
[
"Vale.X64.QuickCode.va_Mod_xmm",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_xmm",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"2c48160ad95953f0ec65d01df765bf9c"
],
[
"Vale.X64.QuickCode.mod_eq",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
"assumption_Vale.X64.Machine_s.reg__uu___haseq",
"assumption_Vale.X64.QuickCode.mod_t__uu___haseq", "bool_inversion",
"bool_typing",
"constructor_distinct_Vale.X64.QuickCode.Mod_mem_heaplet",
"constructor_distinct_Vale.X64.QuickCode.Mod_reg",
"data_typing_intro_Vale.X64.QuickCode.Mod_ok@tok",
"disc_equation_Vale.X64.QuickCode.Mod_None",
"disc_equation_Vale.X64.QuickCode.Mod_flags",
"disc_equation_Vale.X64.QuickCode.Mod_mem",
"disc_equation_Vale.X64.QuickCode.Mod_mem_heaplet",
"disc_equation_Vale.X64.QuickCode.Mod_mem_layout",
"disc_equation_Vale.X64.QuickCode.Mod_ok",
"disc_equation_Vale.X64.QuickCode.Mod_reg",
"disc_equation_Vale.X64.QuickCode.Mod_stack",
"disc_equation_Vale.X64.QuickCode.Mod_stackTaint",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.heaplet_id",
"fuel_guarded_inversion_Vale.X64.QuickCode.mod_t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCode.Mod_mem_heaplet__0",
"projection_inverse_Vale.X64.QuickCode.Mod_reg__0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.X64.QuickCode.uu___is_Mod_mem_layout",
"typing_Vale.X64.QuickCode.uu___is_Mod_ok"
],
0,
"944ea3c6787ded58f7315688fd807eed"
],
[
"Vale.X64.QuickCode.update_state_mod",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCode.Mod_None",
"disc_equation_Vale.X64.QuickCode.Mod_flags",
"disc_equation_Vale.X64.QuickCode.Mod_mem",
"disc_equation_Vale.X64.QuickCode.Mod_mem_heaplet",
"disc_equation_Vale.X64.QuickCode.Mod_mem_layout",
"disc_equation_Vale.X64.QuickCode.Mod_ok",
"disc_equation_Vale.X64.QuickCode.Mod_reg",
"disc_equation_Vale.X64.QuickCode.Mod_stack",
"disc_equation_Vale.X64.QuickCode.Mod_stackTaint",
"fuel_guarded_inversion_Vale.X64.QuickCode.mod_t"
],
0,
"397ed33a51dbe7135d6c59d2f5b0fdd0"
],
[
"Vale.X64.QuickCode.update_state_mods",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
"binder_x_26920e03138cd27e3894dcce3ed826e9_0",
"data_typing_intro_Vale.X64.QuickCode.Mod_ok@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"a2b75e2243755fdda9c843e0cb4096a0"
],
[
"Vale.X64.QuickCode.va_lemma_norm_mods",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"@query",
"equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state"
],
0,
"cbcfa224ad62ad82644b9ce9393931f4"
],
[
"Vale.X64.QuickCode.va_mod_dst_opr64",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"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.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand",
"projection_inverse_BoxInt_proj_0"
],
0,
"a1146a9fd48029b40d2c79f549f0a8f8"
],
[
"Vale.X64.QuickCode.va_mod_reg_opr64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OReg",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Decls.reg_operand",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802"
],
0,
"1548d1497dff6125b862a8da043fe04d"
],
[
"Vale.X64.QuickCode.va_mod_xmm",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_xmm",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"76ca968cf5a183fc3b19a1ac932a8e74"
],
[
"Vale.X64.QuickCode.__proj__QProc__item__proof",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_Vale.X64.QuickCode.quickCode",
"proj_equation_Vale.X64.QuickCode.QProc_c",
"proj_equation_Vale.X64.QuickCode.QProc_mods",
"proj_equation_Vale.X64.QuickCode.QProc_wp",
"projection_inverse_Vale.X64.QuickCode.QProc_c",
"projection_inverse_Vale.X64.QuickCode.QProc_mods",
"projection_inverse_Vale.X64.QuickCode.QProc_wp",
"token_correspondence_Vale.X64.QuickCode.__proj__QProc__item__wp"
],
0,
"a1a757cbeda82d3d91648f340cd2711d"
],
[
"Vale.X64.QuickCode.mod_t",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_Vale.X64.Machine_s.reg__uu___haseq",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.heaplet_id",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"303ed15e09127ee5bd94d15cb6f00adf"
],
[
"Vale.X64.QuickCode.__proj__Mod_reg__item___0",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCode.Mod_reg",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_c6bd9cf894204793a059b43e4dcbf9cc"
],
0,
"de232a7cf63870bd4bf9f02eb2732af5"
],
[
"Vale.X64.QuickCode.__proj__Mod_mem_heaplet__item___0",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCode.Mod_mem_heaplet",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_dae911842b85add82dc5578c02955df1"
],
0,
"aa2998b65c63c48c32ca9ed7dcc23923"
],
[
"Vale.X64.QuickCode.va_Mod_reg64",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"358d36e65e7bf69b03bfa4b0fccb2978"
],
[
"Vale.X64.QuickCode.va_Mod_xmm",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_xmm",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"00b490eb089b5d83fcb78f7ee32d78e5"
],
[
"Vale.X64.QuickCode.mod_eq",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
"assumption_Vale.X64.Machine_s.reg__uu___haseq",
"assumption_Vale.X64.QuickCode.mod_t__uu___haseq", "bool_inversion",
"bool_typing",
"constructor_distinct_Vale.X64.QuickCode.Mod_mem_heaplet",
"constructor_distinct_Vale.X64.QuickCode.Mod_reg",
"data_typing_intro_Vale.X64.QuickCode.Mod_ok@tok",
"disc_equation_Vale.X64.QuickCode.Mod_None",
"disc_equation_Vale.X64.QuickCode.Mod_flags",
"disc_equation_Vale.X64.QuickCode.Mod_mem",
"disc_equation_Vale.X64.QuickCode.Mod_mem_heaplet",
"disc_equation_Vale.X64.QuickCode.Mod_mem_layout",
"disc_equation_Vale.X64.QuickCode.Mod_ok",
"disc_equation_Vale.X64.QuickCode.Mod_reg",
"disc_equation_Vale.X64.QuickCode.Mod_stack",
"disc_equation_Vale.X64.QuickCode.Mod_stackTaint",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.heaplet_id",
"fuel_guarded_inversion_Vale.X64.QuickCode.mod_t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCode.Mod_mem_heaplet__0",
"projection_inverse_Vale.X64.QuickCode.Mod_reg__0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.X64.QuickCode.uu___is_Mod_None"
],
0,
"eace5f8667219b2f51f977b8555f7787"
],
[
"Vale.X64.QuickCode.mod_eq",
3,
1,
0,
[ "@query", "assumption_Vale.X64.QuickCode.mod_t__uu___haseq" ],
0,
"2f23545f1cf1aee6a0b8a16f8cdaca3c"
],
[
"Vale.X64.QuickCode.update_state_mod",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCode.Mod_None",
"disc_equation_Vale.X64.QuickCode.Mod_flags",
"disc_equation_Vale.X64.QuickCode.Mod_mem",
"disc_equation_Vale.X64.QuickCode.Mod_mem_heaplet",
"disc_equation_Vale.X64.QuickCode.Mod_mem_layout",
"disc_equation_Vale.X64.QuickCode.Mod_ok",
"disc_equation_Vale.X64.QuickCode.Mod_reg",
"disc_equation_Vale.X64.QuickCode.Mod_stack",
"disc_equation_Vale.X64.QuickCode.Mod_stackTaint",
"fuel_guarded_inversion_Vale.X64.QuickCode.mod_t"
],
0,
"6a53bfa731d16dda5ebc45004ac08e71"
],
[
"Vale.X64.QuickCode.update_state_mods",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
"binder_x_26920e03138cd27e3894dcce3ed826e9_0",
"data_typing_intro_Vale.X64.QuickCode.Mod_ok@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"c7cd1d33509aebe71ba0cda94f171cad"
],
[
"Vale.X64.QuickCode.va_mod_dst_opr64",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"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.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand",
"projection_inverse_BoxInt_proj_0"
],
0,
"4705e488ec02313f2e18a0b2fe66e818"
],
[
"Vale.X64.QuickCode.va_mod_reg_opr64",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OReg",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Decls.reg_operand",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802"
],
0,
"2000127797894b5eb9db30ec7e408690"
],
[
"Vale.X64.QuickCode.va_mod_xmm",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_xmm",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"163a966d38f59b22c4762887c964c687"
],
[
"Vale.X64.QuickCode.__proj__QProc__item__proof",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_Vale.X64.QuickCode.quickCode",
"proj_equation_Vale.X64.QuickCode.QProc_c",
"proj_equation_Vale.X64.QuickCode.QProc_mods",
"proj_equation_Vale.X64.QuickCode.QProc_wp",
"projection_inverse_Vale.X64.QuickCode.QProc_c",
"projection_inverse_Vale.X64.QuickCode.QProc_mods",
"projection_inverse_Vale.X64.QuickCode.QProc_wp",
"token_correspondence_Vale.X64.QuickCode.__proj__QProc__item__wp"
],
0,
"e8904494f354913b865fe72ee84e2d2e"
]
]
]
Computing file changes ...
