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.Stdcalls.X64.Cpuid.fst.hints
[
"���,\f\u001c\b\u0005��\f\u0005Cin",
[
[
"Vale.Stdcalls.X64.Cpuid.as_t",
1,
1,
0,
[ "@query" ],
0,
"cafe45f7f6b242ee02888221cd3673b4"
],
[
"Vale.Stdcalls.X64.Cpuid.as_normal_t",
1,
1,
0,
[ "@query" ],
0,
"440c7c9fc990bb353c017464fa25acaa"
],
[
"Vale.Stdcalls.X64.Cpuid.dom",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "equation_Prims.nat",
"equation_Vale.Interop.X64.max_stdcall",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"kinding_Vale.Interop.Base.td@tok", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Interop.X64.max_stdcall"
],
0,
"878972be7611a6901b2e4ee3734b9222"
],
[
"Vale.Stdcalls.X64.Cpuid.aesni_lemma'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"bool_inversion", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Interop.X64.regs_modified_stdcall",
"equation_Vale.Interop.X64.xmms_modified_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_aesni_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_aesni_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.aesni_post",
"equation_Vale.Stdcalls.X64.Cpuid.aesni_pre",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"function_token_typing_Vale.Interop.X64.xmms_modified_stdcall",
"function_token_typing_Vale.X64.MemoryAdapters.code_equiv",
"interpretation_Tm_abs_1cf6e44e46995818b6428c925e3f2794",
"interpretation_Tm_abs_b432cc9fe9671a9a5b62330c717b0bcc",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_8c094393c9c948dad8330534aa6d28dc",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"token_correspondence_Vale.Stdcalls.X64.Cpuid.aesni_post",
"token_correspondence_Vale.Stdcalls.X64.Cpuid.aesni_pre",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Lib.X64.Cpuidstdcall.va_lemma_check_aesni_stdcall",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok"
],
0,
"4f0b1e55b9c24b0e51f13dd9386e4b22"
],
[
"Vale.Stdcalls.X64.Cpuid.aesni_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_aesni_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_aesni_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.aesni_post",
"equation_Vale.Stdcalls.X64.Cpuid.aesni_pre",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_1cf6e44e46995818b6428c925e3f2794",
"interpretation_Tm_abs_b432cc9fe9671a9a5b62330c717b0bcc",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"typing_Vale.Interop.Assumptions.win"
],
0,
"7d501738c354a001b4c2af55a01daff7"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_aesni_t",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"1ba8d3cabdcebe21f040099da689eb4e"
],
[
"Vale.Stdcalls.X64.Cpuid.sha_lemma'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.X64_interpretation_Tm_arrow_2d6da19097b39247da65144806c55e59",
"Vale.Interop.X64_interpretation_Tm_arrow_2edbb0578f9dff3b4204c811921185bb",
"Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"bool_inversion", "disc_equation_FStar.Pervasives.Native.Some",
"eq2-interp", "equation_Prims.nat",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.X64.arg_reg_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Interop.X64.reg_nat",
"equation_Vale.Interop.X64.regs_modified_stdcall",
"equation_Vale.Interop.X64.xmms_modified_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_sha_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_sha_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.sha_post",
"equation_Vale.Stdcalls.X64.Cpuid.sha_pre",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.X64.__proj__Rel__item__of_arg",
"function_token_typing_Vale.Interop.X64.arg_of_register",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"function_token_typing_Vale.Interop.X64.xmms_modified_stdcall",
"int_typing",
"interpretation_Tm_abs_41bda6d2df9fb99a3f5d01c0e3af3c67",
"interpretation_Tm_abs_748060b958198eb04eff9a5acc6eff25",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.X64.Rel_of_reg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Interop.X64.Rel_of_reg",
"refinement_interpretation_Tm_refine_14a1655ad84ef9c5d11ecde28c3d6cd2",
"refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a",
"refinement_interpretation_Tm_refine_5035dbea9ab31384d60f7061d33efd0e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f9fee9e5191be0004d01d53ed010af6",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"token_correspondence_Vale.Interop.X64.__proj__Rel__item__of_reg",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"token_correspondence_Vale.Stdcalls.X64.Cpuid.sha_post",
"token_correspondence_Vale.Stdcalls.X64.Cpuid.sha_pre",
"typing_FStar.Pervasives.Native.__proj__Some__item__v",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Interop.X64.arg_reg_stdcall",
"typing_Vale.Interop.X64.max_stdcall",
"typing_Vale.Interop.X64.reg_nat",
"typing_Vale.Lib.X64.Cpuidstdcall.va_lemma_check_sha_stdcall",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok"
],
0,
"040af80cbc6bc432c309222ab0c76add"
],
[
"Vale.Stdcalls.X64.Cpuid.sha_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_sha_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_sha_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.sha_post",
"equation_Vale.Stdcalls.X64.Cpuid.sha_pre",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_41bda6d2df9fb99a3f5d01c0e3af3c67",
"interpretation_Tm_abs_748060b958198eb04eff9a5acc6eff25",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"typing_Vale.Interop.Assumptions.win"
],
0,
"7b5bc80aef1cd514f38c15273848de29"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_sha_t",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"3f4aa5066450b1ee7ea9ccf68733fdce"
],
[
"Vale.Stdcalls.X64.Cpuid.adx_lemma'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.X64_interpretation_Tm_arrow_2d6da19097b39247da65144806c55e59",
"Vale.Interop.X64_interpretation_Tm_arrow_2edbb0578f9dff3b4204c811921185bb",
"Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"bool_inversion", "disc_equation_FStar.Pervasives.Native.Some",
"eq2-interp", "equation_Prims.nat",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.X64.arg_reg_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Interop.X64.reg_nat",
"equation_Vale.Interop.X64.regs_modified_stdcall",
"equation_Vale.Interop.X64.xmms_modified_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_adx_bmi2_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_adx_bmi2_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.adx_post",
"equation_Vale.Stdcalls.X64.Cpuid.adx_pre",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.X64.__proj__Rel__item__of_arg",
"function_token_typing_Vale.Interop.X64.arg_of_register",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"function_token_typing_Vale.Interop.X64.xmms_modified_stdcall",
"int_typing",
"interpretation_Tm_abs_9e785546aeeb1131cce69857f79b82cb",
"interpretation_Tm_abs_cb413ff4b6a7acda0d3c3d073d6dbe9b",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.X64.Rel_of_reg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Interop.X64.Rel_of_reg",
"refinement_interpretation_Tm_refine_14a1655ad84ef9c5d11ecde28c3d6cd2",
"refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a",
"refinement_interpretation_Tm_refine_5035dbea9ab31384d60f7061d33efd0e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d2197822ab01455b16941a7ca4821242",
"token_correspondence_Vale.Interop.X64.__proj__Rel__item__of_reg",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"token_correspondence_Vale.Stdcalls.X64.Cpuid.adx_post",
"token_correspondence_Vale.Stdcalls.X64.Cpuid.adx_pre",
"typing_FStar.Pervasives.Native.__proj__Some__item__v",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Interop.X64.arg_reg_stdcall",
"typing_Vale.Interop.X64.max_stdcall",
"typing_Vale.Interop.X64.reg_nat",
"typing_Vale.Lib.X64.Cpuidstdcall.va_lemma_check_adx_bmi2_stdcall",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok"
],
0,
"4c8d9f5cf343c0b9ed4ef725d85dbb7a"
],
[
"Vale.Stdcalls.X64.Cpuid.adx_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_adx_bmi2_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_adx_bmi2_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.adx_post",
"equation_Vale.Stdcalls.X64.Cpuid.adx_pre",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_9e785546aeeb1131cce69857f79b82cb",
"interpretation_Tm_abs_cb413ff4b6a7acda0d3c3d073d6dbe9b",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"typing_Vale.Interop.Assumptions.win"
],
0,
"9228b712bb6ee05b72e549589fb32215"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_adx_t",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"4c91138f22a3076054745baf77fefdf8"
],
[
"Vale.Stdcalls.X64.Cpuid.avx_lemma'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.X64_interpretation_Tm_arrow_2d6da19097b39247da65144806c55e59",
"Vale.Interop.X64_interpretation_Tm_arrow_2edbb0578f9dff3b4204c811921185bb",
"Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"bool_inversion", "disc_equation_FStar.Pervasives.Native.Some",
"eq2-interp", "equation_Prims.nat",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.X64.arg_reg_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Interop.X64.reg_nat",
"equation_Vale.Interop.X64.regs_modified_stdcall",
"equation_Vale.Interop.X64.xmms_modified_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_avx_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_avx_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.avx_post",
"equation_Vale.Stdcalls.X64.Cpuid.avx_pre",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.X64.__proj__Rel__item__of_arg",
"function_token_typing_Vale.Interop.X64.arg_of_register",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"function_token_typing_Vale.Interop.X64.xmms_modified_stdcall",
"int_typing",
"interpretation_Tm_abs_2d811fb8f80869e30f3ce93e4ecd782f",
"interpretation_Tm_abs_fcfcb19c450f403851d3001d7bfeadd5",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.X64.Rel_of_reg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Interop.X64.Rel_of_reg",
"refinement_interpretation_Tm_refine_14a1655ad84ef9c5d11ecde28c3d6cd2",
"refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a",
"refinement_interpretation_Tm_refine_5035dbea9ab31384d60f7061d33efd0e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_f46cbcdb299e7c92aa89c215abe43559",
"token_correspondence_Vale.Interop.X64.__proj__Rel__item__of_reg",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"token_correspondence_Vale.Stdcalls.X64.Cpuid.avx_post",
"token_correspondence_Vale.Stdcalls.X64.Cpuid.avx_pre",
"typing_FStar.Pervasives.Native.__proj__Some__item__v",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Interop.X64.arg_reg_stdcall",
"typing_Vale.Interop.X64.max_stdcall",
"typing_Vale.Interop.X64.reg_nat",
"typing_Vale.Lib.X64.Cpuidstdcall.va_lemma_check_avx_stdcall",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok"
],
0,
"4ef1024adf4e2acc0d33e1367427dacb"
],
[
"Vale.Stdcalls.X64.Cpuid.avx_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_avx_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_avx_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.avx_post",
"equation_Vale.Stdcalls.X64.Cpuid.avx_pre",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_2d811fb8f80869e30f3ce93e4ecd782f",
"interpretation_Tm_abs_fcfcb19c450f403851d3001d7bfeadd5",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"typing_Vale.Interop.Assumptions.win"
],
0,
"c0e7d7d0fa8042af9981092bab362d0f"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_avx_t",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"8843ef607aac702065857f2bfb480b93"
],
[
"Vale.Stdcalls.X64.Cpuid.avx2_lemma'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.X64_interpretation_Tm_arrow_2d6da19097b39247da65144806c55e59",
"Vale.Interop.X64_interpretation_Tm_arrow_2edbb0578f9dff3b4204c811921185bb",
"Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"bool_inversion", "disc_equation_FStar.Pervasives.Native.Some",
"eq2-interp", "equation_Prims.nat",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.X64.arg_reg_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Interop.X64.reg_nat",
"equation_Vale.Interop.X64.regs_modified_stdcall",
"equation_Vale.Interop.X64.xmms_modified_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_avx2_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_avx2_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.avx2_post",
"equation_Vale.Stdcalls.X64.Cpuid.avx2_pre",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.X64.__proj__Rel__item__of_arg",
"function_token_typing_Vale.Interop.X64.arg_of_register",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"function_token_typing_Vale.Interop.X64.xmms_modified_stdcall",
"int_typing",
"interpretation_Tm_abs_23e31fb67826d4e157311c2ba98aeac3",
"interpretation_Tm_abs_3383cf9c0e84477a75de23c378823afa",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"proj_equation_Vale.Interop.X64.Rel_of_reg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Interop.X64.Rel_of_reg",
"refinement_interpretation_Tm_refine_14a1655ad84ef9c5d11ecde28c3d6cd2",
"refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a",
"refinement_interpretation_Tm_refine_5035dbea9ab31384d60f7061d33efd0e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7a0b0645876b219ba9242c1653f15d73",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"token_correspondence_Vale.Interop.X64.__proj__Rel__item__of_reg",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"token_correspondence_Vale.Stdcalls.X64.Cpuid.avx2_post",
"token_correspondence_Vale.Stdcalls.X64.Cpuid.avx2_pre",
"typing_FStar.Pervasives.Native.__proj__Some__item__v",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Interop.X64.arg_reg_stdcall",
"typing_Vale.Interop.X64.max_stdcall",
"typing_Vale.Interop.X64.reg_nat",
"typing_Vale.Lib.X64.Cpuidstdcall.va_lemma_check_avx2_stdcall",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok"
],
0,
"47cd81abdcf8f250b0eaa21191a50836"
],
[
"Vale.Stdcalls.X64.Cpuid.avx2_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_avx2_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_avx2_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.avx2_post",
"equation_Vale.Stdcalls.X64.Cpuid.avx2_pre",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_23e31fb67826d4e157311c2ba98aeac3",
"interpretation_Tm_abs_3383cf9c0e84477a75de23c378823afa",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"typing_Vale.Interop.Assumptions.win"
],
0,
"9557372eca3c6c16f306bac0c9c76c93"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_avx2_t",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"3717d7e95cf3e3eedb4611247865094e"
],
[
"Vale.Stdcalls.X64.Cpuid.movbe_lemma'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"bool_inversion", "eq2-interp",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Interop.X64.regs_modified_stdcall",
"equation_Vale.Interop.X64.xmms_modified_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_movbe_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_movbe_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.movbe_post",
"equation_Vale.Stdcalls.X64.Cpuid.movbe_pre",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"function_token_typing_Vale.Interop.X64.xmms_modified_stdcall",
"interpretation_Tm_abs_a3dcfeebbdc76d4aa377bee79af232cf",
"interpretation_Tm_abs_f2c3d8bea1a4eaf4e4f9aab26e07579e",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_0bbfc9567ef3356356e7ca7b7a67f189",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Lib.X64.Cpuidstdcall.va_lemma_check_movbe_stdcall",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok"
],
0,
"535580e9eeb7a9e2a0b0e5b1cc2991a3"
],
[
"Vale.Stdcalls.X64.Cpuid.movbe_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_movbe_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_movbe_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.movbe_post",
"equation_Vale.Stdcalls.X64.Cpuid.movbe_pre",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_a3dcfeebbdc76d4aa377bee79af232cf",
"interpretation_Tm_abs_f2c3d8bea1a4eaf4e4f9aab26e07579e",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"typing_Vale.Interop.Assumptions.win"
],
0,
"ebeb3a88af93f9f8602512c9ab61c5f7"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_movbe_t",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"42c199481577477ce42a892024fcce25"
],
[
"Vale.Stdcalls.X64.Cpuid.sse_lemma'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"bool_inversion", "eq2-interp",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Interop.X64.regs_modified_stdcall",
"equation_Vale.Interop.X64.xmms_modified_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_sse_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_sse_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.sse_post",
"equation_Vale.Stdcalls.X64.Cpuid.sse_pre",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"function_token_typing_Vale.Interop.X64.xmms_modified_stdcall",
"interpretation_Tm_abs_4c0a8303dd7538825f7c3c5a61243034",
"interpretation_Tm_abs_ec2bf1362a5ce1f622e3f7e3f2879ae1",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_774783f812cff7503fbf6ea97dbeb81d",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Lib.X64.Cpuidstdcall.va_lemma_check_sse_stdcall",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok"
],
0,
"eaaa1a0814e380542eda136410e7e0e2"
],
[
"Vale.Stdcalls.X64.Cpuid.sse_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_sse_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_sse_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.sse_post",
"equation_Vale.Stdcalls.X64.Cpuid.sse_pre",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_4c0a8303dd7538825f7c3c5a61243034",
"interpretation_Tm_abs_ec2bf1362a5ce1f622e3f7e3f2879ae1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"typing_Vale.Interop.Assumptions.win"
],
0,
"a40e2a7ed6eda2e81a8c14e25912d929"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_sse_t",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"eee57c93a703fbc6b85f7c03880c2626"
],
[
"Vale.Stdcalls.X64.Cpuid.rdrand_lemma'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"bool_inversion", "eq2-interp",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Interop.X64.regs_modified_stdcall",
"equation_Vale.Interop.X64.xmms_modified_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_rdrand_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_rdrand_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.rdrand_post",
"equation_Vale.Stdcalls.X64.Cpuid.rdrand_pre",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"function_token_typing_Vale.Interop.X64.xmms_modified_stdcall",
"interpretation_Tm_abs_03aad193b1698b0c0f9f1c4cd5d9d9b7",
"interpretation_Tm_abs_e898f80cadac726faae28295fc918f5e",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_7c6d46894cde6d36beb32fea22fad00f",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Lib.X64.Cpuidstdcall.va_lemma_check_rdrand_stdcall",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok"
],
0,
"d97371426348076e560e313168f58339"
],
[
"Vale.Stdcalls.X64.Cpuid.rdrand_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_ens_check_rdrand_stdcall",
"equation_Vale.Lib.X64.Cpuidstdcall.va_req_check_rdrand_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.rdrand_post",
"equation_Vale.Stdcalls.X64.Cpuid.rdrand_pre",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_03aad193b1698b0c0f9f1c4cd5d9d9b7",
"interpretation_Tm_abs_e898f80cadac726faae28295fc918f5e",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"typing_Vale.Interop.Assumptions.win"
],
0,
"bba6ec9198acc74317049ff172e722be"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_rdrand_t",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"3ba8a17a411a2868cca75e1ee44e14eb"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_aesni",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"c2c6546b63f9b1990d5b1f0f3fb3a458"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_sha",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"03e0e46ef15be3b70151c4e948baeb8d"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_adx",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"79a5b052d263ce059fbe4a0f12f96b54"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_avx",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"66dbaa0337c6d7e70b61493875269a33"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_avx2",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"f3e4f7f3fd4044d4b288e3820bbb9d57"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_movbe",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"f03c8ff989be651bf6d201158228bc8c"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_sse",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"2c84358643f26933c6b66a74b927a0c8"
],
[
"Vale.Stdcalls.X64.Cpuid.lowstar_rdrand",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.X64.MemoryAdapters.ins_equiv",
"function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv",
"kinding_Vale.Interop.Base.td@tok",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"typing_Vale.Stdcalls.X64.Cpuid.dom"
],
0,
"c44c5c3be997ac51be9679d0b0f92a9f"
]
]
]
Computing file changes ...
