Revision 5b2fbf3c4989a9b0587a00578f69f3041df3f957 authored by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC, committed by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC
1 parent d4ca892
Vale.Stdcalls.X64.Cpuid.fsti.hints
[
"w��y\u0000��0�f���Bq",
[
[
"Vale.Stdcalls.X64.Cpuid.as_t",
1,
1,
0,
[ "@query" ],
0,
"be990e190f033172738e62b41b86e62e"
],
[
"Vale.Stdcalls.X64.Cpuid.as_normal_t",
1,
1,
0,
[ "@query" ],
0,
"931c094f5adc626c1c220919559d1801"
],
[
"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,
"703ed7f362dd32abf56c970ff4ba5927"
],
[
"Vale.Stdcalls.X64.Cpuid.aesni_lemma'",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"bool_inversion", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_Vale.X64.State.Mkvale_state",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"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.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"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.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"int_inversion", "int_typing",
"interpretation_Tm_abs_d07771aa29c035142df63d8f6144b563",
"interpretation_Tm_abs_edfe056e995c1c61bccfdf9346e14890",
"kinding_Vale.Interop.Base.td@tok",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_upd_ne", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"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_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_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Machine_s.Reg_r",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"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_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_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_FStar.List.Tot.Base.length",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Stdcalls.X64.Cpuid.dom",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg64", "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_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg"
],
0,
"350b0ca6110386f1dcb89a343ea90b91"
],
[
"Vale.Stdcalls.X64.Cpuid.aesni_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"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.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_d07771aa29c035142df63d8f6144b563",
"interpretation_Tm_abs_edfe056e995c1c61bccfdf9346e14890",
"lemma_Vale.X64.Memory.modifies_refl",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"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_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap"
],
0,
"5173c188e6dd4e42b08f67dc065f22aa"
],
[
"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,
"d16ef839dd3abac37d7c658cce675a06"
],
[
"Vale.Stdcalls.X64.Cpuid.sha_lemma'",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"bool_inversion", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_Vale.X64.State.Mkvale_state",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"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.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"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.dom",
"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.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"int_inversion", "int_typing",
"interpretation_Tm_abs_32aba5f8f45a9c50ca9e5f630e25288f",
"interpretation_Tm_abs_5a3b892f1ab55d8925828e5bfd96997d",
"kinding_Vale.Interop.Base.td@tok",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_upd_ne", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"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_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_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Machine_s.Reg_r",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"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_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_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_FStar.List.Tot.Base.length",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Stdcalls.X64.Cpuid.dom",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg64", "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_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg"
],
0,
"20ed21c117ae06f0ed95504ae0c3b94b"
],
[
"Vale.Stdcalls.X64.Cpuid.sha_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Prims.Nil",
"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.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_32aba5f8f45a9c50ca9e5f630e25288f",
"interpretation_Tm_abs_5a3b892f1ab55d8925828e5bfd96997d",
"lemma_Vale.X64.Memory.modifies_refl",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"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_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap"
],
0,
"cf76362b9d96cde975e9e14dab767889"
],
[
"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,
"0f1009b8f700b00c061717be8e795bdf"
],
[
"Vale.Stdcalls.X64.Cpuid.adx_lemma'",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"bool_inversion", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_Vale.X64.State.Mkvale_state",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"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.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"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.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"int_inversion", "int_typing",
"interpretation_Tm_abs_49f3309ccbe48ad4af482c34ef21c26d",
"interpretation_Tm_abs_c1a17a30f4afa64cc14307393bfb9ce5",
"kinding_Vale.Interop.Base.td@tok",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_upd_ne", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"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_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_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Machine_s.Reg_r",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"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_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_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_FStar.List.Tot.Base.length",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Stdcalls.X64.Cpuid.dom",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg64", "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_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg"
],
0,
"4ce62393a6680304fd8c0da8d05dc61b"
],
[
"Vale.Stdcalls.X64.Cpuid.adx_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Prims.Nil",
"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.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_49f3309ccbe48ad4af482c34ef21c26d",
"interpretation_Tm_abs_c1a17a30f4afa64cc14307393bfb9ce5",
"lemma_Vale.X64.Memory.modifies_refl",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"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_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap"
],
0,
"9562706de426ba3e8c028d727d182eda"
],
[
"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,
"aa07c5506233127bd5ec1692f39cff8c"
],
[
"Vale.Stdcalls.X64.Cpuid.avx_lemma'",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"bool_inversion", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_Vale.X64.State.Mkvale_state",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"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.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"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.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"int_inversion", "int_typing",
"interpretation_Tm_abs_117e8ce5a44d9fdbee9dfdb31df94e67",
"interpretation_Tm_abs_6c234e0d6e7f2419038a9e2f42f3ef36",
"kinding_Vale.Interop.Base.td@tok",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_upd_ne", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"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_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_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Machine_s.Reg_r",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"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_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_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_FStar.List.Tot.Base.length",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Stdcalls.X64.Cpuid.dom",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg64", "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_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg"
],
0,
"bb6556c75890feca81f5924bba903e1d"
],
[
"Vale.Stdcalls.X64.Cpuid.avx_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Prims.Nil",
"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.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_117e8ce5a44d9fdbee9dfdb31df94e67",
"interpretation_Tm_abs_6c234e0d6e7f2419038a9e2f42f3ef36",
"lemma_Vale.X64.Memory.modifies_refl",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"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_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap"
],
0,
"24ecc943419bff511a67ab3ebee98686"
],
[
"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,
"08debea8a8470432dd719fa7f679a28a"
],
[
"Vale.Stdcalls.X64.Cpuid.avx2_lemma'",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"bool_inversion", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_Vale.X64.State.Mkvale_state",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"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.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"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.Stdcalls.X64.Cpuid.dom",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"int_inversion", "int_typing",
"interpretation_Tm_abs_6aa7fc9e5fb483aab76d8defd980ef18",
"interpretation_Tm_abs_73064411638fa36ee0d737a852ea2532",
"kinding_Vale.Interop.Base.td@tok",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_upd_ne", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"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_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_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Machine_s.Reg_r",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"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_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_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_FStar.List.Tot.Base.length",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Stdcalls.X64.Cpuid.dom",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg64", "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_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg"
],
0,
"4bacacc1023513150c8bc6b25d779cef"
],
[
"Vale.Stdcalls.X64.Cpuid.avx2_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Prims.Nil",
"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.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_6aa7fc9e5fb483aab76d8defd980ef18",
"interpretation_Tm_abs_73064411638fa36ee0d737a852ea2532",
"lemma_Vale.X64.Memory.modifies_refl",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"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_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap"
],
0,
"e1000cc275f5a010d3612f34f012a14c"
],
[
"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,
"23f851e83b947c11a03875b6396aa654"
],
[
"Vale.Stdcalls.X64.Cpuid.movbe_lemma'",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"bool_inversion", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_Vale.X64.State.Mkvale_state",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"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.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"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.dom",
"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.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"int_inversion", "int_typing",
"interpretation_Tm_abs_0a4c56b8dfb6eb9649bed8d6c38893db",
"interpretation_Tm_abs_42670326e9cc5bb20f429293177396ba",
"kinding_Vale.Interop.Base.td@tok",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_upd_ne", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"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_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_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Machine_s.Reg_r",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"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_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_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_FStar.List.Tot.Base.length",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Stdcalls.X64.Cpuid.dom",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg64", "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_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg"
],
0,
"b443fd1bb28baa4d17f9bf7b44930691"
],
[
"Vale.Stdcalls.X64.Cpuid.movbe_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Prims.Nil",
"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.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_0a4c56b8dfb6eb9649bed8d6c38893db",
"interpretation_Tm_abs_42670326e9cc5bb20f429293177396ba",
"lemma_Vale.X64.Memory.modifies_refl",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"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_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap"
],
0,
"75e0c9b28ee250c22f086b3b5417adc8"
],
[
"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,
"395bf8fed3867786dcf315580d12c7b6"
],
[
"Vale.Stdcalls.X64.Cpuid.sse_lemma'",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"bool_inversion", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_Vale.X64.State.Mkvale_state",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"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.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"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.dom",
"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.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"int_inversion", "int_typing",
"interpretation_Tm_abs_7d37adc5c28e915b26787c70c705f090",
"interpretation_Tm_abs_ae95e611dd63e286122e66d49abcf3c0",
"kinding_Vale.Interop.Base.td@tok",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_upd_ne", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"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_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_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Machine_s.Reg_r",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"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_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_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_FStar.List.Tot.Base.length",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Stdcalls.X64.Cpuid.dom",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg64", "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_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg"
],
0,
"45d54dd328077cf3f7fae8ddb9889485"
],
[
"Vale.Stdcalls.X64.Cpuid.sse_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Prims.Nil",
"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.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_7d37adc5c28e915b26787c70c705f090",
"interpretation_Tm_abs_ae95e611dd63e286122e66d49abcf3c0",
"lemma_Vale.X64.Memory.modifies_refl",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"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_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap"
],
0,
"f31e5acb0c749375607224af0431d2ed"
],
[
"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,
"7b90b6d4d843d120ae4b3d032b889d02"
],
[
"Vale.Stdcalls.X64.Cpuid.rdrand_lemma'",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"bool_inversion", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_Vale.X64.State.Mkvale_state",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"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.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.X64.arity_ok",
"equation_Vale.Interop.X64.arity_ok_stdcall",
"equation_Vale.Interop.X64.max_stdcall",
"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.dom",
"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.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Interop.X64.regs_modified_stdcall",
"int_inversion", "int_typing",
"interpretation_Tm_abs_2dbfb6fe71629a1449b4c5fa6515f00a",
"interpretation_Tm_abs_420f231b6b80b469e098677fcd8fb976",
"kinding_Vale.Interop.Base.td@tok",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_upd_ne", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"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_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_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Machine_s.Reg_r",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"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_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_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"token_correspondence_Vale.Interop.X64.regs_modified_stdcall",
"token_correspondence_Vale.Interop.X64.xmms_modified_stdcall",
"typing_FStar.List.Tot.Base.length",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Stdcalls.X64.Cpuid.dom",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg64", "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_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg"
],
0,
"8d237349b068f5b94b71a0ca477636da"
],
[
"Vale.Stdcalls.X64.Cpuid.rdrand_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Prims.Nil",
"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.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"interpretation_Tm_abs_2dbfb6fe71629a1449b4c5fa6515f00a",
"interpretation_Tm_abs_420f231b6b80b469e098677fcd8fb976",
"lemma_Vale.X64.Memory.modifies_refl",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"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_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.X64.Memory.loc_none",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap"
],
0,
"4fa735d7d8ecb4e429a5984b93804f44"
],
[
"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,
"2ec77ed327307f91603cc6eaba8f2543"
]
]
]
Computing file changes ...
