Revision e56414221fb67ecff7d071497f8ba5d20e9c5ba9 authored by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC, committed by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC
1 parent db297bf
Vale.X64.InsVector.fsti.hints
[
"_�;\f\u0000��\u0013�\u0018/n\u0002�}�",
[
[
"Vale.X64.InsVector.buffer128_write",
1,
1,
0,
[ "@query" ],
0,
"fd3fe2152b6f5617ff7ed5ff67ceabdb"
],
[
"Vale.X64.InsVector.va_lemma_Mem128_lemma",
1,
1,
0,
[
"@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,
"66f8065a1767210fc01e78fa97b76b1f"
],
[
"Vale.X64.InsVector.va_wp_Mem128_lemma",
1,
1,
0,
[
"@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,
"73391a2c55a1639ec688b922bbdb8827"
],
[
"Vale.X64.InsVector.va_quick_Mem128_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"df2e151eb4a7acc519190594e3b0cc60"
],
[
"Vale.X64.InsVector.va_quick_Paddd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"abe68a90f2b0aa56ce949117361c5bb8"
],
[
"Vale.X64.InsVector.va_quick_VPaddd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"02359e6e41845478e88d585757d963db"
],
[
"Vale.X64.InsVector.va_quick_Pxor",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"c6ed967246373fce1ed337da93ae59c8"
],
[
"Vale.X64.InsVector.va_quick_Pand",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"e7af6564b613f105d527a5856541e31e"
],
[
"Vale.X64.InsVector.va_quick_VPxor",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"5a4175db8a88c2a399cebae4002a9b08"
],
[
"Vale.X64.InsVector.va_quick_Pslld",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"23c7e75d387256b99a4f42cb73f3098e"
],
[
"Vale.X64.InsVector.va_quick_Psrld",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"8dd21815da88de497bf342b427e271f8"
],
[
"Vale.X64.InsVector.va_quick_Palignr4",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"b909be7c8ad523c44b81142be59cc447"
],
[
"Vale.X64.InsVector.va_quick_Palignr8",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"e5dcd531911ade11f804785d525300ec"
],
[
"Vale.X64.InsVector.va_quick_VPalignr8",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"b9b3adedf9489f74434b56ab199ca566"
],
[
"Vale.X64.InsVector.va_quick_Shufpd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"9ec7a8329438fbf6549919a871192599"
],
[
"Vale.X64.InsVector.va_quick_VShufpd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"3b8b6b367ac8344fe578cc4f3d703e6e"
],
[
"Vale.X64.InsVector.va_quick_Pshufb",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"83c6aaa08128a60fe34b7ee1c8832579"
],
[
"Vale.X64.InsVector.va_quick_VPshufb",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"15279cd120bf26f86b43169c3d95cfb6"
],
[
"Vale.X64.InsVector.va_quick_PshufbStable",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"9864f2f1275b334f6898b8f6b20d614b"
],
[
"Vale.X64.InsVector.va_quick_PshufbDup",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"454f367c8b4865bb8bdb7bee0e2e753b"
],
[
"Vale.X64.InsVector.va_quick_Pshufb64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"179439193a2db4b845f4fbcf751bb3a8"
],
[
"Vale.X64.InsVector.va_quick_Pshufd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"ff2d595d2973372955556e5bb7cfd506"
],
[
"Vale.X64.InsVector.va_lemma_Pcmpeqd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"9386e0f497eb8fbbd66d1e68bb7ef261"
],
[
"Vale.X64.InsVector.va_wp_Pcmpeqd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
"interpretation_Tm_abs_262a5f17710225e0b3c94a9572fe18b9",
"interpretation_Tm_abs_2f6acf51d7aa232b5598822388ce5bc4",
"interpretation_Tm_abs_622687ae6d8eae13cda104371b7ab41b",
"interpretation_Tm_abs_74a09f6c4dec66416dabd66e39a59ccd",
"interpretation_Tm_abs_85480a653b709e89cb2b9a42aa163d1c",
"interpretation_Tm_abs_8d7c8ed27a8759d93726fcec20ed5c83",
"interpretation_Tm_abs_c40a6b972a14befd4ffe542bbae86d4a",
"interpretation_Tm_abs_d7459458ffbef2b7e2e0428d6325562a",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"b7aec6f17a35cc03deb2c5d25bbc0a2d"
],
[
"Vale.X64.InsVector.va_quick_Pcmpeqd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"3f2068bc815df164cc03206d2ac08278"
],
[
"Vale.X64.InsVector.va_quick_Pextrq",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"aa5d41d94491ae7555b69710a0504b78"
],
[
"Vale.X64.InsVector.va_lemma_Pinsrd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_814e3f7d08b3f084a269f773bed66cf0"
],
0,
"8c200a04273783e3c1e74eee76f42ee4"
],
[
"Vale.X64.InsVector.va_wp_Pinsrd",
1,
1,
0,
[ "@query" ],
0,
"d577e9134a26f05e10fe419f1fcec150"
],
[
"Vale.X64.InsVector.va_quick_Pinsrd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"b28aa862381a3662a154a0600d62b3a7"
],
[
"Vale.X64.InsVector.va_lemma_PinsrdImm",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_346e2545166a3f77b1951e566ddee134"
],
0,
"5594f2a0adaf69e75a004d31c5828693"
],
[
"Vale.X64.InsVector.va_wp_PinsrdImm",
1,
1,
0,
[ "@query" ],
0,
"0e97103cad4f2fa514c789527ad009cd"
],
[
"Vale.X64.InsVector.va_quick_PinsrdImm",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"0ebad327ed65f442930d099c81f9a8dc"
],
[
"Vale.X64.InsVector.va_lemma_Pinsrq",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_e4fd8d9df03695672f9a2ee4dde24e42"
],
0,
"7ed61898ca7dbf0df7f1b84efde38aa7"
],
[
"Vale.X64.InsVector.va_wp_Pinsrq",
1,
1,
0,
[ "@query" ],
0,
"5aa6fc091c9eb4dd38bbe9afdbe1d385"
],
[
"Vale.X64.InsVector.va_quick_Pinsrq",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"f614b7e1a0e2e478073665aeb99612af"
],
[
"Vale.X64.InsVector.va_lemma_PinsrqImm",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_cf1bf15c8540663689ef6a48ae625c5f"
],
0,
"7575baf14fb5d4768ddd9bc9dbe2bbd2"
],
[
"Vale.X64.InsVector.va_wp_PinsrqImm",
1,
1,
0,
[ "@query" ],
0,
"a5b72dbb369595d353b88bc81fcef196"
],
[
"Vale.X64.InsVector.va_quick_PinsrqImm",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"0496e39b27939f318ed7a44750f42020"
],
[
"Vale.X64.InsVector.va_quick_VPslldq4",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"f4269c1c5806ccaf4237c0a0a2c81c10"
],
[
"Vale.X64.InsVector.va_quick_Vpslldq8",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"f815d5bcd5fce4f24e68f9d1a934e6ff"
],
[
"Vale.X64.InsVector.va_quick_Vpsrldq8",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"b97ec6e684ea75f49bdb3107a251b137"
],
[
"Vale.X64.InsVector.va_quick_Mov128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"3ee8a2d4fb1e388719131a6cb5241e69"
],
[
"Vale.X64.InsVector.va_quick_Load128_buffer",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"9f045e20dd1002ce4cc83c6353c06681"
],
[
"Vale.X64.InsVector.va_quick_LoadBe64_buffer128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"cb91a9e352617a1615960044bb7cf85f"
],
[
"Vale.X64.InsVector.va_lemma_Store128_buffer",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Vale.X64.Memory.valid_buffer_read",
"equation_Vale.X64.Memory.valid_buffer_write", "int_inversion",
"refinement_interpretation_Tm_refine_d859d1ead5c115356bd724909fe88e79"
],
0,
"99d6d3b6be53978353b99822a0a0a478"
],
[
"Vale.X64.InsVector.va_wp_Store128_buffer",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Vale.X64.Memory.valid_buffer_read",
"equation_Vale.X64.Memory.valid_buffer_write", "int_inversion"
],
0,
"76a469649636753c55b9de777f945c33"
],
[
"Vale.X64.InsVector.va_quick_Store128_buffer",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"eb6001bebef62ed14b73523b31b372b6"
],
[
"Vale.X64.InsVector.va_lemma_Store64_buffer128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Vale.X64.Memory.valid_buffer_read",
"equation_Vale.X64.Memory.valid_buffer_write", "int_inversion",
"refinement_interpretation_Tm_refine_4c559e5c0a08dba34993fb42e758ab46"
],
0,
"62a4de9e0f5cfc795705338beff11cf4"
],
[
"Vale.X64.InsVector.va_wp_Store64_buffer128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_mem_heaplet",
"equation_Vale.X64.Memory.valid_buffer_read",
"equation_Vale.X64.Memory.valid_buffer_write", "int_inversion",
"interpretation_Tm_abs_54ccc32c2dffe4e7ae51f3f9cd75bf90",
"interpretation_Tm_abs_caa93468dabb32def2e17e98dcd23528",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok"
],
0,
"01fbeed468407e6d0ba5b05281dd02e8"
],
[
"Vale.X64.InsVector.va_quick_Store64_buffer128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"38d23cf85c8d5f0d8726bca40d3ef59f"
],
[
"Vale.X64.InsVector.va_quick_ZeroXmm",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"9e42a49ff008ef30d2accc4ffe374bdd"
],
[
"Vale.X64.InsVector.va_quick_InitPshufbMask",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"c8ec8d5b1c1b5084e04c788ecaf780fa"
],
[
"Vale.X64.InsVector.va_quick_InitPshufbStableMask",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"b7f88dc2e378ea28912ea184009a7ab1"
],
[
"Vale.X64.InsVector.va_quick_InitPshufbDupMask",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"8606badc0d252580249625cb3ea66e6e"
],
[
"Vale.X64.InsVector.va_quick_InitPshufb64Mask",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"76c365491543429e7f75111efee36f31"
],
[
"Vale.X64.InsVector.va_quick_XmmEqual",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"df51a2e443841f3fb8dada0bc0240423"
]
]
]
Computing file changes ...
