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.QuickCodes.fst.hints
[
"�[ �M�G�n\u000f_\u0013F!",
[
[
"Vale.X64.QuickCodes.label",
1,
1,
0,
[ "@query" ],
0,
"c95b56c8467e963e83e88d7b7443ac71"
],
[
"Vale.X64.QuickCodes.lemma_label_Type0",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"typing_Vale.X64.QuickCodes.label"
],
0,
"47e2245708219e915356d210f4bd9daa"
],
[
"Vale.X64.QuickCodes.lemma_label_bool",
1,
1,
1,
[ "@query" ],
0,
"63e5a82913653c18efeded8b2a8ceded"
],
[
"Vale.X64.QuickCodes.mods_contains1",
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,
"91df4e0c606d3f3e119c9a27dfa2e441"
],
[
"Vale.X64.QuickCodes.mods_contains",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
"binder_x_26920e03138cd27e3894dcce3ed826e9_1",
"data_typing_intro_Vale.X64.QuickCode.Mod_ok@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok", "fuel_guarded_inversion_Prims.list",
"subterm_ordering_Prims.Cons"
],
0,
"95679ca8d0244df04e8db96b1a31ca26"
],
[
"Vale.X64.QuickCodes.quickCodes",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"2fbfa2a6eb39e6c566c26ee8525eb890"
],
[
"Vale.X64.QuickCodes.__proj__QEmpty__item___0",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QEmpty",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_3bf1e58005ba552fb333da9a044d3e87"
],
0,
"c382281122adb2b95babcca3e1938db0"
],
[
"Vale.X64.QuickCodes.__proj__QSeq__item__b",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QSeq",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_a91a7f4d40ff1cab01209a19b453f3b9"
],
0,
"81c043ba3caf9302954b093c17feeb3a"
],
[
"Vale.X64.QuickCodes.__proj__QSeq__item__c",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QSeq",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_a91a7f4d40ff1cab01209a19b453f3b9"
],
0,
"cffafd7ae84def42c22b247bd4638955"
],
[
"Vale.X64.QuickCodes.__proj__QSeq__item__cs",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QSeq",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_a91a7f4d40ff1cab01209a19b453f3b9"
],
0,
"0f8c6817b7a89be6ff2285a82f7ab462"
],
[
"Vale.X64.QuickCodes.__proj__QSeq__item__r",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QSeq",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_a91a7f4d40ff1cab01209a19b453f3b9"
],
0,
"b4f8fc3f087e750652a14a39c4fc1921"
],
[
"Vale.X64.QuickCodes.__proj__QSeq__item__msg",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QSeq",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_a91a7f4d40ff1cab01209a19b453f3b9"
],
0,
"b14c7a65440cf80b28ebc06f9b071944"
],
[
"Vale.X64.QuickCodes.__proj__QSeq__item___5",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QSeq",
"proj_equation_Vale.X64.QuickCodes.QSeq_b",
"proj_equation_Vale.X64.QuickCodes.QSeq_c",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCodes.QSeq_b",
"projection_inverse_Vale.X64.QuickCodes.QSeq_c",
"refinement_interpretation_Tm_refine_a91a7f4d40ff1cab01209a19b453f3b9"
],
0,
"b69ccd5cb9090c885ea882b5cdbb3fa9"
],
[
"Vale.X64.QuickCodes.__proj__QSeq__item___6",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QSeq",
"proj_equation_Vale.X64.QuickCodes.QSeq_cs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCodes.QSeq_cs",
"refinement_interpretation_Tm_refine_a91a7f4d40ff1cab01209a19b453f3b9"
],
0,
"63328d22331a8c8221211d50c54c4ba8"
],
[
"Vale.X64.QuickCodes.__proj__QBind__item__b",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QBind",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_7d5c31cc88b5ced2af2f0af6163ab025"
],
0,
"ef0dbac4c7322c984368f3c1182f03f8"
],
[
"Vale.X64.QuickCodes.__proj__QBind__item__c",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QBind",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_7d5c31cc88b5ced2af2f0af6163ab025"
],
0,
"be82630ecca78d44b9eda2c9a172b18e"
],
[
"Vale.X64.QuickCodes.__proj__QBind__item__cs",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QBind",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_7d5c31cc88b5ced2af2f0af6163ab025"
],
0,
"d8e05197704400ec45ae7d81232e6648"
],
[
"Vale.X64.QuickCodes.__proj__QBind__item__r",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QBind",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_7d5c31cc88b5ced2af2f0af6163ab025"
],
0,
"7d32913d116eb69e070c8ab92e890519"
],
[
"Vale.X64.QuickCodes.__proj__QBind__item__msg",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QBind",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_7d5c31cc88b5ced2af2f0af6163ab025"
],
0,
"9c7ea56ca29f33b012a6332083be0399"
],
[
"Vale.X64.QuickCodes.__proj__QBind__item___5",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QBind",
"proj_equation_Vale.X64.QuickCodes.QBind_b",
"proj_equation_Vale.X64.QuickCodes.QBind_c",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCodes.QBind_b",
"projection_inverse_Vale.X64.QuickCodes.QBind_c",
"refinement_interpretation_Tm_refine_7d5c31cc88b5ced2af2f0af6163ab025"
],
0,
"541266963dad54e7869e107e5e9e7cbc"
],
[
"Vale.X64.QuickCodes.__proj__QBind__item___6",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QBind",
"proj_equation_Vale.X64.QuickCodes.QBind_b",
"proj_equation_Vale.X64.QuickCodes.QBind_cs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCodes.QBind_b",
"projection_inverse_Vale.X64.QuickCodes.QBind_cs",
"refinement_interpretation_Tm_refine_7d5c31cc88b5ced2af2f0af6163ab025"
],
0,
"c27c8f318f4d8989fa6497f7f4dffd93"
],
[
"Vale.X64.QuickCodes.__proj__QGetState__item__cs",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QGetState",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_4031209a8486d66d031d8a593c8e7fff"
],
0,
"008c6694a6b229e94f95aa0406ffeb21"
],
[
"Vale.X64.QuickCodes.__proj__QGetState__item___1",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QGetState",
"proj_equation_Vale.X64.QuickCodes.QGetState_cs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCodes.QGetState_cs",
"refinement_interpretation_Tm_refine_4031209a8486d66d031d8a593c8e7fff"
],
0,
"16cba52e5868db26b90e462d77b35a13"
],
[
"Vale.X64.QuickCodes.__proj__QPURE__item__cs",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QPURE",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_66a4a737a20620fc555cee70170fd74e"
],
0,
"ff16f8eedb338b11a6e0e1cd8ddc036b"
],
[
"Vale.X64.QuickCodes.__proj__QPURE__item__r",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QPURE",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_66a4a737a20620fc555cee70170fd74e"
],
0,
"903f947c6261a7a0ff34e9a3bd1d16d1"
],
[
"Vale.X64.QuickCodes.__proj__QPURE__item__msg",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QPURE",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_66a4a737a20620fc555cee70170fd74e"
],
0,
"465f3db00e1aaa55f3eb68367dd12c95"
],
[
"Vale.X64.QuickCodes.__proj__QPURE__item__pre",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QPURE",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_66a4a737a20620fc555cee70170fd74e"
],
0,
"ab12908db8b90757901e6189e399ba97"
],
[
"Vale.X64.QuickCodes.__proj__QPURE__item___4",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QPURE",
"proj_equation_Vale.X64.QuickCodes.QPURE_pre",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCodes.QPURE_pre",
"refinement_interpretation_Tm_refine_66a4a737a20620fc555cee70170fd74e",
"token_correspondence_Vale.X64.QuickCodes.__proj__QPURE__item__pre"
],
0,
"e946e91e15783b14f56c442a0ee945ed"
],
[
"Vale.X64.QuickCodes.__proj__QPURE__item___5",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QPURE",
"proj_equation_Vale.X64.QuickCodes.QPURE_cs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCodes.QPURE_cs",
"refinement_interpretation_Tm_refine_66a4a737a20620fc555cee70170fd74e"
],
0,
"bb2c42bdbbe527e50c2daf036fb5b893"
],
[
"Vale.X64.QuickCodes.__proj__QLemma__item__cs",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QLemma",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_5742cde477deec60e39fd91f3654dc27"
],
0,
"7d1ab17e7845738057f3df2204a1b626"
],
[
"Vale.X64.QuickCodes.__proj__QLemma__item__r",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QLemma",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_5742cde477deec60e39fd91f3654dc27"
],
0,
"0484bca1e085d11dac976f27fd792bee"
],
[
"Vale.X64.QuickCodes.__proj__QLemma__item__msg",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QLemma",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_5742cde477deec60e39fd91f3654dc27"
],
0,
"6e351122eacb150adb32928d514fcbce"
],
[
"Vale.X64.QuickCodes.__proj__QLemma__item__pre",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QLemma",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_5742cde477deec60e39fd91f3654dc27"
],
0,
"a2bd27adf8993a58fcdb2d9c9a34f676"
],
[
"Vale.X64.QuickCodes.__proj__QLemma__item__post",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QLemma",
"proj_equation_Vale.X64.QuickCodes.QLemma_pre",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCodes.QLemma_pre",
"refinement_interpretation_Tm_refine_5742cde477deec60e39fd91f3654dc27"
],
0,
"7ac8a71d5ab1207868647148a5da7d1f"
],
[
"Vale.X64.QuickCodes.__proj__QLemma__item___5",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"proj_equation_Vale.X64.QuickCodes.QLemma_pre",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"75b0254f10a1c1a841ca7bdfb8b94e3b"
],
[
"Vale.X64.QuickCodes.__proj__QLemma__item___5",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QLemma", "equation_Prims.squash",
"proj_equation_Vale.X64.QuickCodes.QLemma_post",
"proj_equation_Vale.X64.QuickCodes.QLemma_pre",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCodes.QLemma_post",
"projection_inverse_Vale.X64.QuickCodes.QLemma_pre",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_5742cde477deec60e39fd91f3654dc27",
"token_correspondence_Vale.X64.QuickCodes.__proj__QLemma__item__post"
],
0,
"a1260a6f907aec97619ab52250f91801"
],
[
"Vale.X64.QuickCodes.__proj__QLemma__item___6",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QLemma",
"proj_equation_Vale.X64.QuickCodes.QLemma_cs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCodes.QLemma_cs",
"refinement_interpretation_Tm_refine_5742cde477deec60e39fd91f3654dc27"
],
0,
"e4e4e767ceef890f8eaa3a162a43e371"
],
[
"Vale.X64.QuickCodes.__proj__QGhost__item__cs",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QGhost",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_e472aaae78391477fd73f5609049bdfb"
],
0,
"337003c3473c41ac5fad484c95ff27d7"
],
[
"Vale.X64.QuickCodes.__proj__QGhost__item__b",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QGhost",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_e472aaae78391477fd73f5609049bdfb"
],
0,
"e304a73cb80d6f8e2499947cfce5f9fc"
],
[
"Vale.X64.QuickCodes.__proj__QGhost__item__r",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QGhost",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_e472aaae78391477fd73f5609049bdfb"
],
0,
"fc46e6ebfbb746685ead9cb061d59705"
],
[
"Vale.X64.QuickCodes.__proj__QGhost__item__msg",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QGhost",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_e472aaae78391477fd73f5609049bdfb"
],
0,
"4747ce0c3f7842be1d02b58b74dea533"
],
[
"Vale.X64.QuickCodes.__proj__QGhost__item__pre",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QGhost",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_e472aaae78391477fd73f5609049bdfb"
],
0,
"abd11a13031e7ca1dba99fd713598f42"
],
[
"Vale.X64.QuickCodes.__proj__QGhost__item__post",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QGhost",
"proj_equation_Vale.X64.QuickCodes.QGhost_b",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCodes.QGhost_b",
"refinement_interpretation_Tm_refine_e472aaae78391477fd73f5609049bdfb"
],
0,
"8e0f5d30331a7b7ef2d26e7c2e0f11c0"
],
[
"Vale.X64.QuickCodes.__proj__QGhost__item___6",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QGhost",
"proj_equation_Vale.X64.QuickCodes.QGhost_b",
"proj_equation_Vale.X64.QuickCodes.QGhost_post",
"proj_equation_Vale.X64.QuickCodes.QGhost_pre",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCodes.QGhost_b",
"projection_inverse_Vale.X64.QuickCodes.QGhost_post",
"projection_inverse_Vale.X64.QuickCodes.QGhost_pre",
"refinement_interpretation_Tm_refine_e472aaae78391477fd73f5609049bdfb",
"token_correspondence_Vale.X64.QuickCodes.__proj__QGhost__item__post"
],
0,
"7bec63bb417e073082d5bece7b35138d"
],
[
"Vale.X64.QuickCodes.__proj__QGhost__item___7",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.QGhost",
"proj_equation_Vale.X64.QuickCodes.QGhost_b",
"proj_equation_Vale.X64.QuickCodes.QGhost_cs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.QuickCodes.QGhost_b",
"projection_inverse_Vale.X64.QuickCodes.QGhost_cs",
"refinement_interpretation_Tm_refine_e472aaae78391477fd73f5609049bdfb"
],
0,
"c2522da4981e08de9d6d45a048d4792c"
],
[
"Vale.X64.QuickCodes.wp",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_41eb46af108ce0d9ddf3b217c77e4436_1",
"binder_x_b91e708adc12161aa3247ce7e87e7caa_2",
"constructor_distinct_Prims.Cons",
"data_elim_Vale.X64.QuickCodes.QBind",
"data_elim_Vale.X64.QuickCodes.QGetState",
"data_elim_Vale.X64.QuickCodes.QGhost",
"data_elim_Vale.X64.QuickCodes.QLemma",
"data_elim_Vale.X64.QuickCodes.QPURE",
"data_elim_Vale.X64.QuickCodes.QSeq", "disc_equation_Prims.Cons",
"disc_equation_Vale.X64.QuickCodes.QBind",
"disc_equation_Vale.X64.QuickCodes.QEmpty",
"disc_equation_Vale.X64.QuickCodes.QGetState",
"disc_equation_Vale.X64.QuickCodes.QGhost",
"disc_equation_Vale.X64.QuickCodes.QLemma",
"disc_equation_Vale.X64.QuickCodes.QPURE",
"disc_equation_Vale.X64.QuickCodes.QSeq",
"equality_tok_Prims.LexTop@tok",
"fuel_guarded_inversion_Vale.X64.QuickCodes.quickCodes",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"subterm_ordering_Prims.Cons",
"subterm_ordering_Vale.X64.QuickCodes.QLemma",
"subterm_ordering_Vale.X64.QuickCodes.QPURE",
"typing_Vale.X64.QuickCodes.label"
],
0,
"7d56fe5f938ab66fcd25a7991e7ff0aa"
],
[
"Vale.X64.QuickCodes.wp",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "int_typing",
"projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
],
0,
"650b37726f199e226872a622a6611014"
],
[
"Vale.X64.QuickCodes.wp",
3,
1,
1,
[
"@MaxIFuel_assumption", "@query", "int_typing",
"projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
],
0,
"36eb998f9c614a44c029032f03a629ac"
],
[
"Vale.X64.QuickCodes.state_mod_eq",
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,
"7d0e17a28827053fda0751c6376ce59a"
],
[
"Vale.X64.QuickCodes.update_state_mods_refl",
1,
1,
1,
[
"@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",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
"binder_x_26920e03138cd27e3894dcce3ed826e9_0",
"binder_x_eb96f2119e19317ec6e3b596d5a46609_1", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_Vale.X64.QuickCode.Mod_reg",
"data_elim_Vale.X64.State.Mkvale_state",
"data_typing_intro_Vale.X64.QuickCode.Mod_ok@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_memTaint",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Decls.va_upd_stack",
"equation_Vale.X64.Decls.va_upd_stackTaint",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.set_vale_heap",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.update_state_mod",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.QuickCode.mod_t",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Flags.lemma_equal_elim",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"lemma_Vale.X64.Regs.lemma_upd_eq",
"lemma_Vale.X64.Regs.lemma_upd_ne",
"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_memTaint",
"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_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"typing_Vale.X64.QuickCode.update_state_mods",
"typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"d244dd2fb0a5fba79e902a51e6f22f6f"
],
[
"Vale.X64.QuickCodes.update_state_mods_not1",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"@fuel_correspondence_Vale.X64.QuickCodes.mods_contains1.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.QuickCodes.mods_contains1.fuel_instrumented",
"@query",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
"binder_x_26920e03138cd27e3894dcce3ed826e9_0",
"binder_x_7a2122c20d44fc80e093f4f4614be2e2_3",
"binder_x_eb96f2119e19317ec6e3b596d5a46609_1",
"binder_x_eb96f2119e19317ec6e3b596d5a46609_2", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_Vale.X64.QuickCode.Mod_reg",
"data_elim_Vale.X64.State.Mkvale_state",
"data_typing_intro_Vale.X64.QuickCode.Mod_ok@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_memTaint",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Decls.va_upd_stack",
"equation_Vale.X64.Decls.va_upd_stackTaint",
"equation_Vale.X64.QuickCode.update_state_mod",
"equation_Vale.X64.QuickCodes.state_mod_eq",
"equation_Vale.X64.State.update_reg",
"equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"equation_with_fuel_Vale.X64.QuickCodes.mods_contains1.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.QuickCode.mod_t",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Regs.lemma_upd_ne", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"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_memTaint",
"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_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"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_memTaint",
"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",
"refinement_interpretation_Tm_refine_ddc5344e9fbdb840fb693550a88dc8ff",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.X64.QuickCodes.mods_contains1.fuel_instrumented",
"typing_Vale.X64.QuickCode.mod_eq",
"typing_Vale.X64.QuickCode.update_state_mods",
"typing_Vale.X64.QuickCodes.mods_contains1",
"typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"d11e97eadcb77ceebd732f505569f561"
],
[
"Vale.X64.QuickCodes.update_state_mods_from1",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"@query", "equation_Vale.X64.QuickCodes.state_mod_eq",
"equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0"
],
0,
"26fd14231cac76f33eecf40b32d38296"
],
[
"Vale.X64.QuickCodes.update_state_mods_to1",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"@fuel_correspondence_Vale.X64.QuickCodes.mods_contains1.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.QuickCodes.mods_contains1.fuel_instrumented",
"@query",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
"binder_x_26920e03138cd27e3894dcce3ed826e9_0",
"binder_x_7a2122c20d44fc80e093f4f4614be2e2_3",
"binder_x_eb96f2119e19317ec6e3b596d5a46609_1",
"binder_x_eb96f2119e19317ec6e3b596d5a46609_2", "bool_inversion",
"constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.QuickCode.Mod_None",
"data_elim_Vale.X64.QuickCode.Mod_reg",
"data_elim_Vale.X64.State.Mkvale_state",
"data_typing_intro_Vale.X64.QuickCode.Mod_ok@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equality_tok_Vale.X64.QuickCode.Mod_None@tok",
"equation_Prims.l_not", "equation_Prims.squash",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_memTaint",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Decls.va_upd_stack",
"equation_Vale.X64.Decls.va_upd_stackTaint",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.set_vale_heap",
"equation_Vale.X64.QuickCode.update_state_mod",
"equation_Vale.X64.QuickCodes.state_mod_eq",
"equation_Vale.X64.State.update_reg",
"equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"equation_with_fuel_Vale.X64.QuickCodes.mods_contains1.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.QuickCode.mod_t",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "l_not-interp",
"l_or-interp", "lemma_Vale.X64.Regs.lemma_upd_eq",
"lemma_Vale.X64.Regs.lemma_upd_ne", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"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_memTaint",
"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_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"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_memTaint",
"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",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_ddc5344e9fbdb840fb693550a88dc8ff",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"token_correspondence_Vale.X64.QuickCodes.mods_contains1.fuel_instrumented",
"typing_Vale.X64.QuickCode.mod_eq",
"typing_Vale.X64.QuickCode.update_state_mods",
"typing_Vale.X64.QuickCodes.mods_contains1",
"typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_tok_Vale.X64.QuickCode.Mod_None@tok"
],
0,
"3bcb2255fa75d17d644a56bdca58b7bc"
],
[
"Vale.X64.QuickCodes.update_state_mods_from",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.QuickCodes.state_mod_eq",
"fuel_guarded_inversion_Vale.X64.QuickCode.mod_t"
],
0,
"fdbf12b428ab03a365edbedfd7fc7eb6"
],
[
"Vale.X64.QuickCodes.update_state_mods_to",
1,
1,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"@query", "constructor_distinct_Vale.X64.QuickCode.Mod_flags",
"constructor_distinct_Vale.X64.QuickCode.Mod_mem",
"constructor_distinct_Vale.X64.QuickCode.Mod_memTaint",
"constructor_distinct_Vale.X64.QuickCode.Mod_ok",
"constructor_distinct_Vale.X64.QuickCode.Mod_reg",
"constructor_distinct_Vale.X64.QuickCode.Mod_stack",
"constructor_distinct_Vale.X64.QuickCode.Mod_stackTaint",
"equality_tok_Vale.X64.QuickCode.Mod_flags@tok",
"equality_tok_Vale.X64.QuickCode.Mod_mem@tok",
"equality_tok_Vale.X64.QuickCode.Mod_memTaint@tok",
"equality_tok_Vale.X64.QuickCode.Mod_ok@tok",
"equality_tok_Vale.X64.QuickCode.Mod_stack@tok",
"equality_tok_Vale.X64.QuickCode.Mod_stackTaint@tok",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCodes.state_mod_eq",
"equation_Vale.X64.State.state_eq",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"projection_inverse_Vale.X64.QuickCode.Mod_reg__0",
"typing_Vale.X64.QuickCode.update_state_mods",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"c7bd43eb951a153e8a460e0cdc0f38d2"
],
[
"Vale.X64.QuickCodes.update_state_mods_trans",
1,
1,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"@query", "equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCodes.state_mod_eq",
"equation_Vale.X64.State.state_eq",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Flags.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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",
"typing_Vale.X64.QuickCode.update_state_mods",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"6dca85572e60d21272e6acbbf8af699b"
],
[
"Vale.X64.QuickCodes.update_state_mods_weaken1",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCodes.mods_contains.fuel_instrumented",
"@fuel_correspondence_Vale.X64.QuickCodes.mods_contains1.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.QuickCodes.mods_contains.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.QuickCodes.mods_contains1.fuel_instrumented",
"@query",
"Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
"binder_x_26920e03138cd27e3894dcce3ed826e9_0",
"binder_x_26920e03138cd27e3894dcce3ed826e9_1",
"binder_x_7a2122c20d44fc80e093f4f4614be2e2_4",
"binder_x_eb96f2119e19317ec6e3b596d5a46609_2",
"binder_x_eb96f2119e19317ec6e3b596d5a46609_3", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.QuickCode.Mod_None",
"data_typing_intro_Vale.X64.QuickCode.Mod_ok@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Vale.X64.QuickCode.Mod_None@tok",
"equation_Vale.X64.QuickCodes.state_mod_eq",
"equation_with_fuel_Vale.X64.QuickCodes.mods_contains.fuel_instrumented",
"equation_with_fuel_Vale.X64.QuickCodes.mods_contains1.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_ddc5344e9fbdb840fb693550a88dc8ff",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.X64.QuickCodes.mods_contains1.fuel_instrumented",
"typing_Vale.X64.QuickCode.mod_eq",
"typing_Vale.X64.QuickCodes.mods_contains",
"typing_Vale.X64.QuickCodes.mods_contains1",
"typing_tok_Vale.X64.QuickCode.Mod_None@tok", "unit_inversion",
"unit_typing"
],
0,
"6da63d63588a2f28e737f6d811d13b26"
],
[
"Vale.X64.QuickCodes.update_state_mods_weaken",
1,
1,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"@query", "equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.State.state_eq",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Flags.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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",
"typing_Vale.X64.QuickCode.update_state_mods",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"c235aa8d37b1c86980e91ee6f24d495a"
],
[
"Vale.X64.QuickCodes.call_QPURE",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_interpretation_Tm_arrow_92458cff82f9ffee1f6e26a1c0c579f3",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.QuickCodes_interpretation_Tm_arrow_2a3381d384e2722434518a0bfbf9e1c6",
"Vale.X64.QuickCodes_interpretation_Tm_arrow_b9ff16838ca14be79c4714dd5f2c76fe",
"equation_Prims.l_True", "equation_Prims.pure_post",
"equation_Prims.pure_post_",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_inversion", "true_interp",
"typing_Vale.X64.QuickCodes.label", "unit_typing"
],
0,
"ef32d64e66752a009c83bb49472852ef"
],
[
"Vale.X64.QuickCodes.wp_sound",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"@fuel_correspondence_Vale.X64.QuickCodes.wp.fuel_instrumented",
"@fuel_correspondence_Vale.X64.QuickCodes.wp_Bind.fuel_instrumented",
"@fuel_correspondence_Vale.X64.QuickCodes.wp_Seq.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.QuickCodes.wp.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.QuickCodes.wp_Bind.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.QuickCodes.wp_Seq.fuel_instrumented",
"@query",
"Vale.X64.QuickCode_interpretation_Tm_arrow_0d128dfda008d2ae08295ef66bd11d0c",
"Vale.X64.QuickCodes_interpretation_Tm_arrow_74a73da46d81cd90b8f01a4ee193c186",
"b2t_def", "binder_x_26920e03138cd27e3894dcce3ed826e9_3",
"binder_x_41eb46af108ce0d9ddf3b217c77e4436_1",
"binder_x_97dd616240a10d798be60579c1f54712_4",
"binder_x_b91e708adc12161aa3247ce7e87e7caa_2",
"binder_x_eb96f2119e19317ec6e3b596d5a46609_5",
"binder_x_fe28d8bcde588226b4e538b35321de05_0", "bool_inversion",
"constructor_distinct_Prims.Cons",
"constructor_distinct_Vale.X64.QuickCodes.QBind",
"constructor_distinct_Vale.X64.QuickCodes.QEmpty",
"constructor_distinct_Vale.X64.QuickCodes.QGetState",
"constructor_distinct_Vale.X64.QuickCodes.QGhost",
"constructor_distinct_Vale.X64.QuickCodes.QLemma",
"constructor_distinct_Vale.X64.QuickCodes.QPURE",
"constructor_distinct_Vale.X64.QuickCodes.QSeq",
"data_elim_Vale.X64.QuickCodes.QBind",
"data_elim_Vale.X64.QuickCodes.QEmpty",
"data_elim_Vale.X64.QuickCodes.QGetState",
"data_elim_Vale.X64.QuickCodes.QLemma",
"data_elim_Vale.X64.QuickCodes.QPURE",
"data_elim_Vale.X64.QuickCodes.QSeq", "disc_equation_Prims.Cons",
"disc_equation_Vale.X64.QuickCodes.QBind",
"disc_equation_Vale.X64.QuickCodes.QEmpty",
"disc_equation_Vale.X64.QuickCodes.QGetState",
"disc_equation_Vale.X64.QuickCodes.QGhost",
"disc_equation_Vale.X64.QuickCodes.QLemma",
"disc_equation_Vale.X64.QuickCodes.QPURE",
"disc_equation_Vale.X64.QuickCodes.QSeq", "equation_Prims.l_and",
"equation_Prims.squash",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.QuickCodes.wp_proc",
"equation_Vale.X64.State.state_eq",
"equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"equation_with_fuel_Vale.X64.QuickCodes.wp.fuel_instrumented",
"equation_with_fuel_Vale.X64.QuickCodes.wp_Bind.fuel_instrumented",
"equation_with_fuel_Vale.X64.QuickCodes.wp_Seq.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.QuickCode.quickCode",
"fuel_guarded_inversion_Vale.X64.QuickCodes.quickCodes",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_b4f9f1bdf5a6c223157c90a65b4b9a40",
"interpretation_Tm_abs_c8c3955c6d20d50ca51d19c6d5f0e657",
"l_and-interp", "l_imp-interp",
"l_quant_interp_304bab225187ac37ac9d69ad8b8c114a",
"l_quant_interp_77ce7dc2822dda058d24973d401dffa9",
"lemma_Vale.X64.Flags.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl",
"proj_equation_Vale.X64.QuickCode.QProc_mods",
"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_memTaint",
"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.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Vale.X64.QuickCode.QProc_c",
"projection_inverse_Vale.X64.QuickCode.QProc_mods",
"projection_inverse_Vale.X64.QuickCode.QProc_proof",
"projection_inverse_Vale.X64.QuickCode.QProc_wp",
"projection_inverse_Vale.X64.QuickCodes.QBind__5",
"projection_inverse_Vale.X64.QuickCodes.QBind__6",
"projection_inverse_Vale.X64.QuickCodes.QBind_a",
"projection_inverse_Vale.X64.QuickCodes.QBind_b",
"projection_inverse_Vale.X64.QuickCodes.QBind_c",
"projection_inverse_Vale.X64.QuickCodes.QBind_cs",
"projection_inverse_Vale.X64.QuickCodes.QBind_msg",
"projection_inverse_Vale.X64.QuickCodes.QBind_r",
"projection_inverse_Vale.X64.QuickCodes.QEmpty__0",
"projection_inverse_Vale.X64.QuickCodes.QEmpty_a",
"projection_inverse_Vale.X64.QuickCodes.QGetState__1",
"projection_inverse_Vale.X64.QuickCodes.QGetState_a",
"projection_inverse_Vale.X64.QuickCodes.QGetState_cs",
"projection_inverse_Vale.X64.QuickCodes.QGhost__6",
"projection_inverse_Vale.X64.QuickCodes.QGhost__7",
"projection_inverse_Vale.X64.QuickCodes.QGhost_b",
"projection_inverse_Vale.X64.QuickCodes.QGhost_cs",
"projection_inverse_Vale.X64.QuickCodes.QGhost_msg",
"projection_inverse_Vale.X64.QuickCodes.QGhost_post",
"projection_inverse_Vale.X64.QuickCodes.QGhost_pre",
"projection_inverse_Vale.X64.QuickCodes.QGhost_r",
"projection_inverse_Vale.X64.QuickCodes.QLemma__5",
"projection_inverse_Vale.X64.QuickCodes.QLemma__6",
"projection_inverse_Vale.X64.QuickCodes.QLemma_a",
"projection_inverse_Vale.X64.QuickCodes.QLemma_cs",
"projection_inverse_Vale.X64.QuickCodes.QLemma_msg",
"projection_inverse_Vale.X64.QuickCodes.QLemma_post",
"projection_inverse_Vale.X64.QuickCodes.QLemma_pre",
"projection_inverse_Vale.X64.QuickCodes.QLemma_r",
"projection_inverse_Vale.X64.QuickCodes.QPURE__4",
"projection_inverse_Vale.X64.QuickCodes.QPURE__5",
"projection_inverse_Vale.X64.QuickCodes.QPURE_a",
"projection_inverse_Vale.X64.QuickCodes.QPURE_cs",
"projection_inverse_Vale.X64.QuickCodes.QPURE_msg",
"projection_inverse_Vale.X64.QuickCodes.QPURE_pre",
"projection_inverse_Vale.X64.QuickCodes.QPURE_r",
"projection_inverse_Vale.X64.QuickCodes.QSeq__5",
"projection_inverse_Vale.X64.QuickCodes.QSeq__6",
"projection_inverse_Vale.X64.QuickCodes.QSeq_a",
"projection_inverse_Vale.X64.QuickCodes.QSeq_b",
"projection_inverse_Vale.X64.QuickCodes.QSeq_c",
"projection_inverse_Vale.X64.QuickCodes.QSeq_cs",
"projection_inverse_Vale.X64.QuickCodes.QSeq_msg",
"projection_inverse_Vale.X64.QuickCodes.QSeq_r",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"subterm_ordering_Prims.Cons",
"subterm_ordering_Vale.X64.QuickCodes.QLemma",
"subterm_ordering_Vale.X64.QuickCodes.QPURE",
"typing_Vale.X64.QuickCode.update_state_mods",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.mods_contains",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"0d69917daded41c21acac8330279fba5"
],
[
"Vale.X64.QuickCodes.qblock_proof",
1,
1,
1,
[ "@query", "equation_Vale.X64.QuickCodes.wp_block" ],
0,
"db65efaaf91b7da14f3267fbee300a11"
],
[
"Vale.X64.QuickCodes.qblock",
1,
1,
1,
[ "@query", "equation_Vale.X64.QuickCode.t_ensure" ],
0,
"7feb12ec1ddc45f2b02600a9ec0f59d3"
],
[
"Vale.X64.QuickCodes.qInlineIf_proof",
1,
1,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCodes.mods_contains.fuel_instrumented",
"@query", "bool_inversion", "equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.QuickCodes.if_code",
"equation_Vale.X64.QuickCodes.wp_InlineIf",
"fuel_guarded_inversion_Vale.X64.QuickCode.quickCode",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"proj_equation_Vale.X64.QuickCode.QProc_c",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"typing_Vale.X64.QuickCode.__proj__QProc__item__mods",
"typing_Vale.X64.QuickCodes.mods_contains"
],
0,
"55bb06724102b66b55655bbfe225fbef"
],
[
"Vale.X64.QuickCodes.qInlineIf",
1,
1,
1,
[
"@query", "equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.QuickCodes.if_code"
],
0,
"76bf0f8b41b107c61d05a0675880b704"
],
[
"Vale.X64.QuickCodes.cmp",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"d0b56bef844a00fc1304a0d04d970514"
],
[
"Vale.X64.QuickCodes.cmp",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"4d262dd687f321a9115510c46368a236"
],
[
"Vale.X64.QuickCodes.cmp",
3,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"05bd489413bed30b9a4f1d5b112b0c95"
],
[
"Vale.X64.QuickCodes.cmp",
4,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"2b9462726766b9b1ec101cae17240b23"
],
[
"Vale.X64.QuickCodes.cmp",
5,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"4b7949535aa5749e1636213fcd414821"
],
[
"Vale.X64.QuickCodes.cmp",
6,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"e1b0f96a9dc7d5d104bc019367b0ca62"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_eq__item__o1",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"c97f602bbfe04cc000f3b1515e0a14a1"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_eq__item__o1",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_eq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_79e3a6e70e67630cf427a80ed0a4e1d3"
],
0,
"663f79fc53edfe6398bff35f7978ef2d"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_eq__item__o2",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"1d8476327691849354d650960b29f5ec"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_eq__item__o2",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_eq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_79e3a6e70e67630cf427a80ed0a4e1d3"
],
0,
"4c4a0c7f47dc19db9afb43caf33c7f48"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_ne__item__o1",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"d9162167a728039b63e4f70ce6c7da9f"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_ne__item__o1",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_ne", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_cf3a5e84197e0dc095e3f4b6944c03ad"
],
0,
"f847abd6230465254be964831f03abf1"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_ne__item__o2",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"d5b0858cbdfa5d02773f67c86eeed7c2"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_ne__item__o2",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_ne", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_cf3a5e84197e0dc095e3f4b6944c03ad"
],
0,
"f701d1bb4cc30df06676bb259be32e5c"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_le__item__o1",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"88ddc812bbe69c26ddf4b423098d499a"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_le__item__o1",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_le", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_e81e0a8f29a0b7a0a0192b5e4daa0ea7"
],
0,
"69720f027d56be93493603dc0d93fbac"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_le__item__o2",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"673db531a0b218a757ed5b3be9f2b1f1"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_le__item__o2",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_le", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_e81e0a8f29a0b7a0a0192b5e4daa0ea7"
],
0,
"788f6a1fc870cf3893d38c7bd6a9568c"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_ge__item__o1",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"da8c4a667f28f39bfb1e63b106559893"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_ge__item__o1",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_ge", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_963c01ae6ff8fce053e3fb4c65517cf0"
],
0,
"2f86c1559fbb485f3a70d69029e7bf31"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_ge__item__o2",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"460fd0a88383a83a7b51ae0e91e058e8"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_ge__item__o2",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_ge", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_963c01ae6ff8fce053e3fb4c65517cf0"
],
0,
"906b2fe50c2ed2b3d53f3370acfa531f"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_lt__item__o1",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"dc23c7252c30f6d82d6afc9c84b4074c"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_lt__item__o1",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_lt", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_7a0baeddd930b9285f08819aa1aae3d9"
],
0,
"5fd2fa15c55be6bc67848f9b898e908a"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_lt__item__o2",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"b0bf575f54e48803629a4b29992be2ab"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_lt__item__o2",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_lt", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_7a0baeddd930b9285f08819aa1aae3d9"
],
0,
"bd4e86c377e3dfcb524577c59fbb40d8"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_gt__item__o1",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"95310facb4d62b919f2016924fb853b6"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_gt__item__o1",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_gt", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_d215a1997b8658bff7ac4ee881057f3a"
],
0,
"ea506a619f094506af5011f1fc8e78a3"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_gt__item__o2",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"3411bff6777227dc4dfca2f1d7c45c63"
],
[
"Vale.X64.QuickCodes.__proj__Cmp_gt__item__o2",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_gt", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_d215a1997b8658bff7ac4ee881057f3a"
],
0,
"c024a918010c1424e959660d546cee37"
],
[
"Vale.X64.QuickCodes.cmp_to_ocmp",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_eq",
"disc_equation_Vale.X64.QuickCodes.Cmp_ge",
"disc_equation_Vale.X64.QuickCodes.Cmp_gt",
"disc_equation_Vale.X64.QuickCodes.Cmp_le",
"disc_equation_Vale.X64.QuickCodes.Cmp_lt",
"disc_equation_Vale.X64.QuickCodes.Cmp_ne",
"fuel_guarded_inversion_Vale.X64.QuickCodes.cmp"
],
0,
"24a5ed3118ff21256e7e13d29649b289"
],
[
"Vale.X64.QuickCodes.valid_cmp",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_eq",
"disc_equation_Vale.X64.QuickCodes.Cmp_ge",
"disc_equation_Vale.X64.QuickCodes.Cmp_gt",
"disc_equation_Vale.X64.QuickCodes.Cmp_le",
"disc_equation_Vale.X64.QuickCodes.Cmp_lt",
"disc_equation_Vale.X64.QuickCodes.Cmp_ne",
"fuel_guarded_inversion_Vale.X64.QuickCodes.cmp"
],
0,
"326d6217707e43332fa6baeb55e41bf7"
],
[
"Vale.X64.QuickCodes.eval_cmp",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.QuickCodes.Cmp_eq",
"disc_equation_Vale.X64.QuickCodes.Cmp_ge",
"disc_equation_Vale.X64.QuickCodes.Cmp_gt",
"disc_equation_Vale.X64.QuickCodes.Cmp_le",
"disc_equation_Vale.X64.QuickCodes.Cmp_lt",
"disc_equation_Vale.X64.QuickCodes.Cmp_ne", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.X64.QuickCodes.cmp",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"fd0a3fc39ee4b19c96ca516fde9bb13c"
],
[
"Vale.X64.QuickCodes.qIf_proof",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.X64.QuickCodes.Cmp_eq",
"constructor_distinct_Vale.X64.QuickCodes.Cmp_ge",
"constructor_distinct_Vale.X64.QuickCodes.Cmp_gt",
"constructor_distinct_Vale.X64.QuickCodes.Cmp_le",
"constructor_distinct_Vale.X64.QuickCodes.Cmp_lt",
"constructor_distinct_Vale.X64.QuickCodes.Cmp_ne",
"disc_equation_Vale.X64.QuickCodes.Cmp_eq",
"disc_equation_Vale.X64.QuickCodes.Cmp_ge",
"disc_equation_Vale.X64.QuickCodes.Cmp_gt",
"disc_equation_Vale.X64.QuickCodes.Cmp_le",
"disc_equation_Vale.X64.QuickCodes.Cmp_lt",
"disc_equation_Vale.X64.QuickCodes.Cmp_ne",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.QuickCodes.cmp_to_ocmp",
"equation_Vale.X64.QuickCodes.eval_cmp",
"equation_Vale.X64.QuickCodes.valid_cmp",
"equation_Vale.X64.QuickCodes.wp_If",
"equation_Vale.X64.State.eval_operand",
"fuel_guarded_inversion_Vale.X64.QuickCode.quickCode",
"fuel_guarded_inversion_Vale.X64.QuickCodes.cmp",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "l_and-interp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_disEquality",
"proj_equation_Vale.X64.QuickCode.QProc_c",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.X64.QuickCodes.Cmp_eq_o1",
"projection_inverse_Vale.X64.QuickCodes.Cmp_eq_o2",
"projection_inverse_Vale.X64.QuickCodes.Cmp_ge_o1",
"projection_inverse_Vale.X64.QuickCodes.Cmp_ge_o2",
"projection_inverse_Vale.X64.QuickCodes.Cmp_gt_o1",
"projection_inverse_Vale.X64.QuickCodes.Cmp_gt_o2",
"projection_inverse_Vale.X64.QuickCodes.Cmp_le_o1",
"projection_inverse_Vale.X64.QuickCodes.Cmp_le_o2",
"projection_inverse_Vale.X64.QuickCodes.Cmp_lt_o1",
"projection_inverse_Vale.X64.QuickCodes.Cmp_lt_o2",
"projection_inverse_Vale.X64.QuickCodes.Cmp_ne_o1",
"projection_inverse_Vale.X64.QuickCodes.Cmp_ne_o2",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"typing_Vale.X64.Decls.eval_ocmp", "typing_Vale.X64.Decls.va_cmp_eq",
"typing_Vale.X64.Decls.va_cmp_ge", "typing_Vale.X64.Decls.va_cmp_gt",
"typing_Vale.X64.Decls.va_cmp_le", "typing_Vale.X64.Decls.va_cmp_lt",
"typing_Vale.X64.Decls.va_cmp_ne", "typing_Vale.X64.Decls.valid_ocmp"
],
0,
"ee3516626770af72032fe56404fde9c0"
],
[
"Vale.X64.QuickCodes.qIf",
1,
1,
1,
[ "@query", "equation_Vale.X64.QuickCode.t_ensure" ],
0,
"24ceab7a3771f3299b2e9542379a2578"
],
[
"Vale.X64.QuickCodes.qWhile_proof_rec",
1,
1,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCodes.mods_contains.fuel_instrumented",
"@query",
"Vale.X64.QuickCodes_interpretation_Tm_arrow_5ff11c0e8f366cbbe8245cc49215a32a",
"binder_x_0b3155f809aebd4145416b801f6c5395_5",
"binder_x_26920e03138cd27e3894dcce3ed826e9_6",
"binder_x_5be19c503dc123c73b0a0968efc19363_4",
"binder_x_6297ae5f737aaa6bc9dfa87506c2566c_3",
"binder_x_e09860b75d8922ab497a3e5bc9347578_11",
"binder_x_eb96f2119e19317ec6e3b596d5a46609_10",
"binder_x_fe28d8bcde588226b4e538b35321de05_1", "bool_inversion",
"constructor_distinct_Vale.X64.Machine_s.While",
"data_elim_Vale.X64.QuickCodes.Cmp_eq",
"data_elim_Vale.X64.QuickCodes.Cmp_ge",
"data_elim_Vale.X64.QuickCodes.Cmp_gt",
"data_elim_Vale.X64.QuickCodes.Cmp_le",
"data_elim_Vale.X64.QuickCodes.Cmp_lt",
"data_elim_Vale.X64.QuickCodes.Cmp_ne",
"disc_equation_Vale.X64.Machine_s.While",
"equality_tok_Prims.LexTop@tok", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.QuickCodes.cmp_to_ocmp",
"equation_Vale.X64.QuickCodes.eval_cmp",
"equation_Vale.X64.QuickCodes.valid_cmp",
"equation_Vale.X64.QuickCodes.wp_While",
"equation_Vale.X64.QuickCodes.wp_While_body",
"equation_Vale.X64.QuickCodes.wp_While_inv",
"fuel_guarded_inversion_Vale.X64.QuickCode.quickCode",
"fuel_guarded_inversion_Vale.X64.QuickCodes.cmp",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "l_and-interp",
"lemma_Vale.X64.Decls.lemma_cmp_eq",
"lemma_Vale.X64.Decls.lemma_cmp_ge",
"lemma_Vale.X64.Decls.lemma_cmp_gt",
"lemma_Vale.X64.Decls.lemma_cmp_le",
"lemma_Vale.X64.Decls.lemma_cmp_lt",
"lemma_Vale.X64.Decls.lemma_cmp_ne",
"lemma_Vale.X64.Decls.lemma_valid_cmp_eq",
"lemma_Vale.X64.Decls.lemma_valid_cmp_ge",
"lemma_Vale.X64.Decls.lemma_valid_cmp_gt",
"lemma_Vale.X64.Decls.lemma_valid_cmp_le",
"lemma_Vale.X64.Decls.lemma_valid_cmp_lt",
"lemma_Vale.X64.Decls.lemma_valid_cmp_ne",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_disEquality",
"proj_equation_Vale.X64.Machine_s.While_whileBody",
"proj_equation_Vale.X64.Machine_s.While_whileCond",
"proj_equation_Vale.X64.QuickCode.QProc_c",
"proj_equation_Vale.X64.QuickCode.QProc_mods",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.X64.Machine_s.While_t_ins",
"projection_inverse_Vale.X64.Machine_s.While_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.While_whileBody",
"projection_inverse_Vale.X64.Machine_s.While_whileCond",
"token_correspondence_Vale.X64.QuickCodes.wp_While_inv",
"typing_Vale.X64.Decls.eval_ocmp",
"typing_Vale.X64.Decls.valid_ocmp",
"typing_Vale.X64.QuickCode.__proj__QProc__item__mods",
"typing_Vale.X64.QuickCodes.cmp_to_ocmp",
"typing_Vale.X64.QuickCodes.mods_contains"
],
0,
"46d4f473d5f7ad142347871135a99cb6"
],
[
"Vale.X64.QuickCodes.qWhile_proof",
1,
1,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
"@query", "equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.State.state_eq",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Flags.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"typing_Vale.X64.QuickCode.update_state_mods",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"b3b6f159607554928c02d61972451349"
],
[
"Vale.X64.QuickCodes.qWhile",
1,
1,
1,
[ "@query", "equation_Vale.X64.QuickCode.t_ensure" ],
0,
"1e166ed33edd87d7c30cf69b2029ee0a"
],
[
"Vale.X64.QuickCodes.qAssertLemma",
1,
1,
1,
[ "@query" ],
0,
"d72379ee081a671c3779e72a53979c56"
],
[
"Vale.X64.QuickCodes.qAssertSquashLemma",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"834224cad313eccb291e944b90f025d7"
],
[
"Vale.X64.QuickCodes.qAssertByLemma",
1,
1,
1,
[ "@query" ],
0,
"59866df2aa8866ec338ec009669f39e7"
],
[
"Vale.X64.QuickCodes.wp_sound_code",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.QuickCode.t_ensure",
"fuel_guarded_inversion_Vale.X64.QuickCode.quickCode",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"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,
"e90686e85384624ded56f6ca14bed8af"
],
[
"Vale.X64.QuickCodes.regs_match_file",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_25f4b27a20f72ed456cefba9461105d5_2",
"binder_x_9bc66468c4c7ad1611e8748185d6e29f_3",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.X64.Machine_s.reg_file_id",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_46e1d323f68f206e5b156d1cf36df4aa",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"well-founded-ordering-on-nat"
],
0,
"53bc58ceb2841b41ebb43abbf0a25156"
],
[
"Vale.X64.QuickCodes.regs_match",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_b86c2548ce36a17f03fdb05cdd982de7_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0d7abd59d64d4ac197ae128854a17b2f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"24d40e03cf7392c932be5981f4a4664c"
],
[
"Vale.X64.QuickCodes.all_regs_match",
1,
1,
1,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"projection_inverse_BoxInt_proj_0"
],
0,
"4d889fff1e08b45c8da1cddb7bee1ddd"
],
[
"Vale.X64.QuickCodes.lemma_regs_match_file",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_f11fc4502473979ff90135832d872c59"
],
0,
"42286197e602c7bd6ead36ff06f3efcc"
],
[
"Vale.X64.QuickCodes.lemma_regs_match_file",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCodes.regs_match_file.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.QuickCodes.regs_match_file.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_25f4b27a20f72ed456cefba9461105d5_2",
"binder_x_9bc66468c4c7ad1611e8748185d6e29f_3",
"binder_x_e8c929cfff8c8fbabcf0223966249701_0",
"binder_x_e8c929cfff8c8fbabcf0223966249701_1", "eq2-interp",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_with_fuel_Vale.X64.QuickCodes.regs_match_file.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "l_and-interp",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_46e1d323f68f206e5b156d1cf36df4aa",
"refinement_interpretation_Tm_refine_4cd2cd249de1c01a346e065af2ec7c1e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"well-founded-ordering-on-nat"
],
0,
"f87e994d51ddd7da0cfbe243b1195217"
],
[
"Vale.X64.QuickCodes.lemma_regs_match",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_1a63608c72b38163339e0b28b15f37cd"
],
0,
"af2ad888971560db3b7904d0b83f928f"
],
[
"Vale.X64.QuickCodes.lemma_regs_match",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.QuickCodes.regs_match.fuel_instrumented",
"@fuel_correspondence_Vale.X64.QuickCodes.regs_match_file.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.QuickCodes.regs_match.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_b86c2548ce36a17f03fdb05cdd982de7_2",
"binder_x_e8c929cfff8c8fbabcf0223966249701_0",
"binder_x_e8c929cfff8c8fbabcf0223966249701_1",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_with_fuel_Vale.X64.QuickCodes.regs_match.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "l_and-interp",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0d7abd59d64d4ac197ae128854a17b2f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"1d6f0a0e752fceff18c3aecbbab1104f"
],
[
"Vale.X64.QuickCodes.lemma_state_match",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "data_elim_Vale.X64.Machine_s.Reg",
"equation_Prims.nat", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCodes.all_regs_match",
"equation_Vale.X64.QuickCodes.state_match",
"equation_Vale.X64.State.state_eq",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.X64.Machine_s.__proj__Reg__item__rf",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"2b560ab96a8b2b4055be1ad9e883a5d8"
],
[
"Vale.X64.QuickCodes.va_state_match",
1,
1,
1,
[ "@query" ],
0,
"24be31552c28203b8d119281ad2ecc6b"
],
[
"Vale.X64.QuickCodes.wp_sound_code_pre",
1,
1,
1,
[
"@query", "equation_Vale.X64.State.state_eta",
"lemma_Vale.X64.Regs.lemma_eta",
"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_memTaint",
"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_Vale.X64.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_memTaint",
"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.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"41ffa2df52fca299c9d2e45a34086ce9"
],
[
"Vale.X64.QuickCodes.wp_sound_code_wrap",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"data_elim_Vale.X64.State.Mkvale_state",
"equation_Vale.X64.Machine_s.memTaint_t",
"equation_Vale.X64.Memory.memtaint",
"equation_Vale.X64.State.state_eta",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Regs.lemma_eta",
"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_memTaint",
"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",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"eba8d2e9f60a8cf7ff6a30d55df40321"
],
[
"Vale.X64.QuickCodes.assert_normal",
1,
1,
1,
[ "@query" ],
0,
"939d1ac1845b07e7833cfea8b48508f4"
],
[
"Vale.X64.QuickCodes.wp_sound_code_norm",
1,
1,
1,
[ "@query" ],
0,
"4cbd5fe5a25edbea0d7aa183d96fb193"
]
]
]
Computing file changes ...
