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.X64.QuickCode.fst.hints
[
"�\u007fu��\u001dXY4Q?M�",
[
[
"Vale.X64.QuickCode.mod_t",
1,
1,
0,
[ "@query", "assumption_Vale.X64.Machine_s.reg__uu___haseq" ],
0,
"1d08f971017ac5e2c979ed4acddbfac8"
],
[
"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,
"007ff3c45693ee099a445aa58956e279"
],
[
"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,
"b59916cf71aa2b6307238ab2f8f60090"
],
[
"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,
"2c7f52cc24a5eb724a032cd298b60a17"
],
[
"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_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_memTaint",
"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",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCode.Mod_reg__0",
"typing_Vale.X64.QuickCode.uu___is_Mod_ok"
],
0,
"4f2a58677a3a451db0201608a4ec3c6e"
],
[
"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_memTaint",
"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,
"bfa60b5c7b314a97368a0a39aa257a0b"
],
[
"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,
"bfdb1cb573830da952a06f5fde0e3956"
],
[
"Vale.X64.QuickCode.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,
"43217db6fd231d73e36a7d3f339fd97b"
],
[
"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,
"cccd4524e9c8c207e963b91b2a550191"
],
[
"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.va_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,
"09fd2684b42d472dbe2f0df181ca5c9e"
],
[
"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,
"71906595f462abfd36286c26b56d462e"
],
[
"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,
"de91a8f9c1dbc8c384a0a5291cec8844"
],
[
"Vale.X64.QuickCode.mod_t",
1,
1,
0,
[ "@query", "assumption_Vale.X64.Machine_s.reg__uu___haseq" ],
0,
"6f8d6be687c3dcb241cca4351d158be9"
],
[
"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,
"2aa8e1035884d372c328520791561dcd"
],
[
"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,
"6f9951bdeaf8cd7cbe8faa8ce5ac8c95"
],
[
"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,
"0c97c0b768397c8c7d1e381b2d315f6a"
],
[
"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_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_memTaint",
"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",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCode.Mod_reg__0",
"typing_Vale.X64.QuickCode.uu___is_Mod_None"
],
0,
"b14f666a54eab0cd30c4728bfea02cd6"
],
[
"Vale.X64.QuickCode.mod_eq",
3,
1,
0,
[ "@query", "assumption_Vale.X64.QuickCode.mod_t__uu___haseq" ],
0,
"0bd744963e87332d1b470882478ce604"
],
[
"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_memTaint",
"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,
"43c172271d57edb3bf4862553984a997"
],
[
"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,
"7755ea06f7ad44c75e9e1f1740e3325a"
],
[
"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,
"f44642afb5b3ff18869e4e04c6ddd74f"
],
[
"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.va_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,
"46bc403df6c364912a1f8aeac300eecb"
],
[
"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,
"dccc8ca31e527268ff41995a81f9c9eb"
],
[
"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,
"6557b49f92c548db56af6a1b5a7f8db4"
]
]
]
Computing file changes ...
