Revision e56414221fb67ecff7d071497f8ba5d20e9c5ba9 authored by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC, committed by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC
1 parent db297bf
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,
"29aa7bdad4deb3f9472b3c63256eb50f"
],
[
"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,
"e314d68db7084381bc45d911c4279b73"
],
[
"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,
"10d12a268065449dea79a2f907caf9f7"
],
[
"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,
"2b7cb2c9c5df5947beb5c56c5a580145"
],
[
"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,
"3e919cd39fa6dcd493ea382a91fc250f"
],
[
"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,
"0ed0cf8876c5de56b27c6fe50ba493d4"
],
[
"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,
"848552a9a7d78cdcc233f7cf4a76fb80"
],
[
"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,
"fbf45cd8918caf21e16f223dc673adeb"
],
[
"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,
"e485bf2de3e89e4fd96fec0860378ba0"
],
[
"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,
"b7808d1d5ad47c6d8c3c44ae510026dd"
],
[
"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,
"308d0e2271722b8fce50059ebf9076e7"
],
[
"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,
"230fcf226eaa590989dc7334177f3ff5"
],
[
"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,
"68fd18cdaa8e69a3ebefbea611274ca0"
],
[
"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,
"b6ceba889e72a881795eabce1af3710e"
],
[
"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,
"3a8ee62106f476f52205bd84d2813b12"
],
[
"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,
"18740b0df4d021852bdcc5d6922e0a10"
],
[
"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,
"9c300a1e9534d0792d4a80361d96c680"
],
[
"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,
"9d31d5213423b1e7fab9b5398171009d"
],
[
"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,
"cb550d9496be02284dec16a68688eb4a"
],
[
"Vale.X64.QuickCode.mod_eq",
3,
1,
0,
[ "@query", "assumption_Vale.X64.QuickCode.mod_t__uu___haseq" ],
0,
"a6c8a4602edf60837ab07a6276f2468f"
],
[
"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,
"946b47d58f2029a7cccb682142ffcf2c"
],
[
"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,
"80b6ae0eabd83e499c4243141f3b289c"
],
[
"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,
"5b736a9ec9984c5ba492f543810b60de"
],
[
"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,
"af1cd51be2ebe30f90f96315762bba28"
],
[
"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,
"842ed88dc56be17a664ced1d23e1fec1"
],
[
"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,
"88b12492213ab397a0ab67fd39eb45ef"
]
]
]
Computing file changes ...
