[
  "���,\f\u001c\b\u0005��\f\u0005Cin",
  [
    [
      "Vale.Stdcalls.X64.Cpuid.as_t",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "4c3cb62f01eeb9036edcf29f547272ba"
    ],
    [
      "Vale.Stdcalls.X64.Cpuid.as_normal_t",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "39d0172d330d7f9271690fa2363f3f44"
    ],
    [
      "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,
      "fef4c1080a3e2b237b67597432b9043e"
    ],
    [
      "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,
      "b0a3f0861713d16f6b4b135878d1cab6"
    ],
    [
      "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,
      "15d54d3b5efa50e33de3f3c184423071"
    ],
    [
      "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,
      "67eaaca6a51da6bf7da1382572bcbd10"
    ],
    [
      "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,
      "7582c72b42b2a3388d553a64aa67e453"
    ],
    [
      "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,
      "d5f4b8880ae89d1f09695597c5e0f7c7"
    ],
    [
      "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,
      "e9b37cc81542e790786792d56d9adec8"
    ],
    [
      "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,
      "2ca104a76f649dc173c8f473d2c305e5"
    ],
    [
      "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,
      "85c984dbedac57bcdc89798e3fe8eb19"
    ],
    [
      "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,
      "dd546559c26d749f9ef77959624b57e1"
    ],
    [
      "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,
      "7fdaa53ce2da9cee4a82d6656ac2ef66"
    ],
    [
      "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,
      "f283af642e926826f53a32dcd3ed5c5c"
    ],
    [
      "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,
      "4a369ffd5c20a266a37a5efe6f7d5eea"
    ],
    [
      "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,
      "198b533114774e2febf136a457fd8829"
    ],
    [
      "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,
      "37e419a49a9fa0e589ee6f1f342c466d"
    ],
    [
      "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,
      "e3113a1d8fa14c2fb18c118efe243c31"
    ],
    [
      "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,
      "9fcb2a84779be2e3e6e9b195181d07a2"
    ],
    [
      "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,
      "df18312a01c23a9a85986ec587796eb4"
    ],
    [
      "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,
      "9b08472caa3d2afb9500c5e6c764a231"
    ],
    [
      "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,
      "10c198978001e9fe7906c43e4bf825ee"
    ],
    [
      "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,
      "8754faa6f72523651905394d2d15a6cf"
    ],
    [
      "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,
      "e224d557cfb441a2bc0ffc78717d3362"
    ],
    [
      "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,
      "1b611b2919b58f133c6a2b71f4d75f47"
    ],
    [
      "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,
      "765d276bd1c1e15c4eaac24d301b7682"
    ],
    [
      "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,
      "7078b8c9cd8fac3201f4a377b42204ba"
    ],
    [
      "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,
      "81a13af88f106fdb32bc24f2a33135f7"
    ],
    [
      "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,
      "85bc686ce8f5b4638d49ae2917391ef3"
    ],
    [
      "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,
      "46da033a213638a482c554295f6ca32a"
    ],
    [
      "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,
      "b461d32e6fc9db5fe0e164a5342069df"
    ],
    [
      "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,
      "f426a56f71b1591ca55a66eac1c478c8"
    ],
    [
      "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,
      "ecddb052ee2642dfb173943a8ff46e45"
    ],
    [
      "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,
      "c06e5ae537ca51750547d36cca17c71f"
    ],
    [
      "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,
      "c947f3685fccb10dc9b849d253ecba57"
    ]
  ]
]