Revision 0d9153dc34ee2dcf0821e3f21e825fc5bb8895b4 authored by Santiago Zanella-Beguelin on 11 December 2019, 17:46:08 UTC, committed by Santiago Zanella-Beguelin on 12 December 2019, 10:33:01 UTC
1 parent 7405f78
Vale.X64.QuickCodes.fst.hints
[
"�[ �M�G�n\u000f_\u0013F!",
[
[
"Vale.X64.QuickCodes.label",
1,
1,
0,
[ "@query" ],
0,
"9b855c2b6ff8965b4775cc455f584f39"
],
[
"Vale.X64.QuickCodes.lemma_label_Type0",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"typing_Vale.X64.QuickCodes.label"
],
0,
"eb7b821a908801f4a9d12540ceac892f"
],
[
"Vale.X64.QuickCodes.lemma_label_bool",
1,
1,
1,
[ "@query" ],
0,
"e3bb7ca9ec17ae192650949a86a7708f"
],
[
"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,
"f4a2717189ee1269b6a1080d32bafec4"
],
[
"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,
"06db3f49d7322b811ea049eb30bb69f3"
],
[
"Vale.X64.QuickCodes.quickCodes",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"a6c72a0184dbf2f868ca55f2010d0bed"
],
[
"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,
"b3619ced531632953e11f91531ac46b2"
],
[
"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,
"fe3b96f4895479e4b170ba39a79a2226"
],
[
"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,
"952c00d62383bc3c90950a5062d32e7a"
],
[
"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,
"e7f9e76a340bc1c967d730f816c39104"
],
[
"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,
"9038d30a87b0a5ae31541cc6daa1bac9"
],
[
"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,
"00392a2f4206209c76120f9109eea792"
],
[
"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,
"b832ac09fc82ad546826c3433eebbb5d"
],
[
"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,
"4e7e3b040606df48c7111c94f1fbf07a"
],
[
"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,
"ac52c5014ac70f46d4c42f36dceba5b7"
],
[
"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,
"ece1e849f35a059347ed861b0ffe3d52"
],
[
"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,
"02141e06a70e6b918da40b5186146a16"
],
[
"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,
"12390e1b29f2901bc2be10070a3950c9"
],
[
"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,
"0286287bf7a85f74d04d06f68f16e655"
],
[
"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,
"37ff5b90109e58ebfc58980985287dec"
],
[
"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,
"bd32e5c5b15088472e1e5f6774215e38"
],
[
"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,
"7c604df25b5f5eff0bdab56f981c1fe8"
],
[
"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,
"6ce87bb16dd8cb44676dc9258bd4b90d"
],
[
"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,
"58f3a8423be8f3caad158774f08c944a"
],
[
"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,
"1912e55f86a266d70850cb4559acec4b"
],
[
"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,
"724b0ac534e0e78c2096b376dcd961f8"
],
[
"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,
"59d7e1b3f44eadf5f9c75e8038448a58"
],
[
"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,
"69c6460a5b041ee8dbc262707eb34003"
],
[
"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,
"bc8cea5613333844583098c8efb3f246"
],
[
"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,
"d536b0c0cae270a238eb05aecedc4aca"
],
[
"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,
"2aac92b9fdf06953b988c4bc44afb8a8"
],
[
"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,
"9d37f04afeec11fbd1cc018e8daea6ad"
],
[
"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,
"d80e5b0e3582b3412c0631af8fc38b00"
],
[
"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,
"570f54eec209b09ca22c4e383c683814"
],
[
"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,
"d76c67ab2368f08646c53ab2238537d1"
],
[
"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,
"4be2183bc98b558f4033b865cd9ade42"
],
[
"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,
"754d4b9f7f50f2b59fd0de76f8d43bed"
],
[
"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,
"e916388e0cd28409cf2dab8a8d7607bc"
],
[
"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,
"c7278e90ac1ceaa4c41bd41100c7f8af"
],
[
"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,
"c13d4cd32235b1286c2ee551c946e697"
],
[
"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,
"a81488e98103dc959cda25c5a3938ffa"
],
[
"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,
"bbc9340e3ce7c7a43740cf1a985bab55"
],
[
"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,
"398642c1075d0e4fcdbe0fb445ea2724"
],
[
"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,
"b95e0c245f0972c0c6849ecc6b88d733"
],
[
"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,
"b0e4c4239e0c3db1ca24ade20989f079"
],
[
"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,
"a44573439fc0528adccfbc784da1491e"
],
[
"Vale.X64.QuickCodes.wp",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "int_typing",
"projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
],
0,
"8ec65c63e223d1c5f2a01471eab579cf"
],
[
"Vale.X64.QuickCodes.wp",
3,
1,
1,
[
"@MaxIFuel_assumption", "@query", "int_typing",
"projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
],
0,
"2a1a6ab9dae0566036e2fc284d57f0c5"
],
[
"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,
"62417d3190abc226062bf0fc47349c0f"
],
[
"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,
"70e4d2fbf384826df7b4d0052ec58c31"
],
[
"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,
"97addc00429bef715301b3bf85e7cfae"
],
[
"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,
"195e13a9d103675ea13135d7c500a2f3"
],
[
"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,
"9dc7e2be0e91530099ec976cdb964ba0"
],
[
"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,
"ef5f8e091f659dabac75c04344923016"
],
[
"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,
"35842930433447edca2310a781af7d95"
],
[
"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,
"ea768256c109bf49df9339c2f162b668"
],
[
"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,
"e6716025819c81d882dc7bdfedd7dc58"
],
[
"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,
"41d0a26dffb69ddbfa189f81faea0501"
],
[
"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,
"9249cb021262dde9c07512c310d11dca"
],
[
"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,
"08659f7ce7201e145aa97bb67ee7afc8"
],
[
"Vale.X64.QuickCodes.qblock_proof",
1,
1,
1,
[ "@query", "equation_Vale.X64.QuickCodes.wp_block" ],
0,
"38b2d097124054e81334b3768c7ca86d"
],
[
"Vale.X64.QuickCodes.qblock",
1,
1,
1,
[ "@query", "equation_Vale.X64.QuickCode.t_ensure" ],
0,
"c52f2a78638e007fcb62802be56e73cb"
],
[
"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,
"d8759bf3728bfaa5ebce01e47aab3766"
],
[
"Vale.X64.QuickCodes.qInlineIf",
1,
1,
1,
[
"@query", "equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.QuickCodes.if_code"
],
0,
"46119d264801f9f6ea85165e6b324987"
],
[
"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,
"51c52b78c325984c95f275fdb4696907"
],
[
"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,
"cc77869e2a5a755a52bc9a409f995f73"
],
[
"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,
"47b202af70a1deabe7b493d9667296f2"
],
[
"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,
"8a7c932101d08be6911e2ded2995b4ba"
],
[
"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,
"5cc687739dfc80ce01c78921aabe3a2a"
],
[
"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,
"f8733ecb87056e0d7f26e563dda54561"
],
[
"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,
"7a6cfa51b0189756e5fc13658367443d"
],
[
"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,
"c0b09dd341c17f05ae4bd9ba7a0f21c8"
],
[
"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,
"436193ee26a6074a833f43c5838b5bb4"
],
[
"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,
"672f50b22378ec3114412e6111317e63"
],
[
"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,
"c9f94fd7cdf56b5c80e852a92537e56c"
],
[
"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,
"22d7bdd5bdcf28d7a2ccfe41321c9fc6"
],
[
"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,
"de8bef0fd3da1505cdf27caf396e78f8"
],
[
"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,
"8deb867b31a753c8eea68474ad729029"
],
[
"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,
"f01362f2575b86a6b297fb5b7706586f"
],
[
"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,
"65fcd2c3115ca365749af1b0b5b0e7c0"
],
[
"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,
"72adf01868082e72285097434e9abefb"
],
[
"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,
"0604515a34e5920507a116556bbd4516"
],
[
"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,
"7836cb4c275824b55eab28f33831666e"
],
[
"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,
"343061c67e55f43a9cf98e00b6cfa39e"
],
[
"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,
"4743533d7e760f6c5d75cf4438bd1fe1"
],
[
"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,
"c5fe323f1652ddf8f20fb05acf414b4b"
],
[
"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,
"87d62c8e62a8b42f6ed57f3f2075427c"
],
[
"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,
"eed79fc1b25b917ec3a4f0e13434e135"
],
[
"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,
"227dbb6dc8ac0c3fe08b44532ffb562f"
],
[
"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,
"203cbd30308405ca42646c940093af4a"
],
[
"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,
"f733d66a1e63cf8687e06fb7e526f96a"
],
[
"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,
"0bc551f37daac7a4ed997eee90be7916"
],
[
"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,
"22fd395cd16559a93a4bdcf18bc8a25c"
],
[
"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,
"a3d7c074a31493a70d60ca94e21f0f5f"
],
[
"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,
"5f2e1358a5c07421952ac03375b08d6f"
],
[
"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,
"f68a4cd035f2d06cc2cbbb031bf6b663"
],
[
"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,
"e3c866ae97af0177f3720a9177bd0328"
],
[
"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,
"514fd71d5538aed9e0412eadd6f29676"
],
[
"Vale.X64.QuickCodes.qIf",
1,
1,
1,
[ "@query", "equation_Vale.X64.QuickCode.t_ensure" ],
0,
"b866a6707f647016d5cd1e3bc98de6db"
],
[
"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,
"14278fdef6a4c2beaf54037c35ac9a9d"
],
[
"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,
"f6b08170950a3a35804bcc86726cac0b"
],
[
"Vale.X64.QuickCodes.qWhile",
1,
1,
1,
[ "@query", "equation_Vale.X64.QuickCode.t_ensure" ],
0,
"e5d6bf1b2e13f9296d5730c6128aeae8"
],
[
"Vale.X64.QuickCodes.qAssertLemma",
1,
1,
1,
[ "@query" ],
0,
"cb12337c2d1667bcbf2bd309bf702b23"
],
[
"Vale.X64.QuickCodes.qAssertSquashLemma",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"5eb8cf9edda9b0b28edf143d9f1c95dc"
],
[
"Vale.X64.QuickCodes.qAssertByLemma",
1,
1,
1,
[ "@query" ],
0,
"dad15d29eb8757923b17ee595aabe4ea"
],
[
"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,
"c002403284fd47261e81e4e5e4581c7e"
],
[
"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,
"683d716c3a9422ae33b8fc096c182f12"
],
[
"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,
"7409c53ede23e6b9701877ba76420bf1"
],
[
"Vale.X64.QuickCodes.all_regs_match",
1,
1,
1,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"projection_inverse_BoxInt_proj_0"
],
0,
"3e4934724a84abd5efc2c4df27dd5c67"
],
[
"Vale.X64.QuickCodes.lemma_regs_match_file",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_f11fc4502473979ff90135832d872c59"
],
0,
"a1b4df93db5ee7ddc4e9ca5a1337855a"
],
[
"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,
"64e0b6b735917154631008907fc82b3e"
],
[
"Vale.X64.QuickCodes.lemma_regs_match",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_1a63608c72b38163339e0b28b15f37cd"
],
0,
"256078686cd4789eba57cf11cad59437"
],
[
"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,
"60c0df1d9458c465266187f0a1692dea"
],
[
"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,
"9f400c5e77f2d886f1b8300754525711"
],
[
"Vale.X64.QuickCodes.va_state_match",
1,
1,
1,
[ "@query" ],
0,
"f37ada9897ce89620e4e567e3235b692"
],
[
"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,
"333ef7b1e37717414e3606eaedc99f3e"
],
[
"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,
"db967ab0dcebf1a5de6bc515eb87239e"
],
[
"Vale.X64.QuickCodes.assert_normal",
1,
1,
1,
[ "@query" ],
0,
"8bbadb82f52ce23c0b2d0c88a0029c19"
],
[
"Vale.X64.QuickCodes.wp_sound_code_norm",
1,
1,
1,
[ "@query" ],
0,
"a860bb8df369938eaf787f0415716130"
]
]
]
Computing file changes ...
