[
  "Ä\t{\u000eSBêM>\\¶‚¤rcô",
  [
    [
      "X64.GCTRstdcall.va_req_gctr_bytes_stdcall128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.eq2", "equation_Prims.l_and",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "unit_typing"
      ],
      0,
      "a16aa04472be7d69b7dc7921f7232401"
    ],
    [
      "X64.GCTRstdcall.va_ens_gctr_bytes_stdcall128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "equation_GCTR.make_gctr_plain_LE",
        "equation_GCTR_s.is_gctr_plain_LE", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Prims.subtype_of", "equation_Words_s.nat64",
        "equation_Words_s.nat8", "equation_Words_s.natN",
        "equation_X64.GCTRstdcall.va_req_gctr_bytes_stdcall128",
        "equation_X64.Vale.Decls.va_state_eq",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat8", "int_inversion",
        "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "primitive_Prims.op_LessThan",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.empty",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok", "unit_typing"
      ],
      0,
      "5cdf7e959ed20771c27d09010671dd23"
    ],
    [
      "X64.GCTRstdcall.va_lemma_gctr_bytes_stdcall128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_GCTR.make_gctr_plain_LE",
        "equation_GCTR_s.is_gctr_plain_LE", "equation_Words_s.nat8",
        "function_token_typing_Words_s.nat8", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_84d5ff88da44c55fdccd6756c03a43a5",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "typing_FStar.Seq.Base.empty"
      ],
      0,
      "d19acf7c8e03f0ea392fc14a7ac701c7"
    ],
    [
      "X64.GCTRstdcall.va_lemma_gctr_bytes_stdcall128",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "constructor_distinct_AES_s.AES_128",
        "constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_Interop.Types.TUInt64@tok",
        "equality_tok_X64.Machine_s.Public@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_GCM_helpers.bytes_to_quad_size",
        "equation_GCTR.make_gctr_plain_LE",
        "equation_GCTR_s.gctr_encrypt_LE",
        "equation_GCTR_s.is_gctr_plain_LE", "equation_Prims.eq2",
        "equation_Prims.l_imp", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Prop_s.prop0", "equation_Words_s.nat64",
        "equation_Words_s.nat8", "equation_Words_s.natN",
        "equation_X64.Memory.buffer128", "equation_X64.Memory.buffer64",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_if",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validDstAddrs128",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.Decls.valid_stack_slots",
        "equation_X64.Vale.QuickCodes.range1",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat8", "int_inversion", "int_typing",
        "interpretation_Tm_abs_42acf2b4bd61f7d087f311642b137700",
        "interpretation_Tm_abs_e7b42242d9c12fea100903f5ef74c36d",
        "interpretation_Tm_abs_efed28e5237cc814be518263d6481a87",
        "l_imp-interp", "l_not-interp", "lemma_X64.Memory.loc_includes_refl",
        "lemma_X64.Memory.loc_includes_union_l_buffer",
        "lemma_X64.Memory.modifies_buffer_addr",
        "lemma_X64.Memory.modifies_buffer_elim",
        "lemma_X64.Memory.modifies_buffer_readable",
        "lemma_X64.Memory.modifies_goal_directed_refl",
        "lemma_X64.Memory.modifies_goal_directed_trans",
        "lemma_X64.Memory.modifies_goal_directed_trans2",
        "lemma_X64.Memory.modifies_valid_taint128",
        "lemma_X64.Memory.modifies_valid_taint64",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_LessThan",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_FStar.Seq.Base.empty",
        "typing_X64.Memory.buffer_addr", "typing_X64.Memory.buffer_read",
        "typing_X64.Memory.loc_buffer", "typing_X64.Memory.loc_union",
        "typing_X64.Memory.modifies",
        "typing_X64.Vale.Decls.validSrcAddrs128",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_Interop.Types.TUInt64@tok",
        "typing_tok_X64.Machine_s.Public@tok",
        "typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok",
        "typing_tok_X64.Machine_s.Secret@tok", "unit_typing"
      ],
      0,
      "96f02165419b7306c0158ccedc7808ca"
    ],
    [
      "X64.GCTRstdcall.va_wp_gctr_bytes_stdcall128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_X64.Machine_s.R10@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equation_GCTR.make_gctr_plain_LE",
        "equation_GCTR_s.is_gctr_plain_LE", "equation_Words_s.nat8",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "function_token_typing_Words_s.nat8", "primitive_Prims.op_LessThan",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "typing_FStar.Seq.Base.empty",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok"
      ],
      0,
      "58f2655b314f7a1034db7311fd25ddf4"
    ],
    [
      "X64.GCTRstdcall.va_wpMonotone_gctr_bytes_stdcall128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_X64.Machine_s.R10@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equation_X64.GCTRstdcall.va_wp_gctr_bytes_stdcall128",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_reg",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_X64.Machine_s.R10@tok",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.R15@tok",
        "typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
        "typing_tok_X64.Machine_s.Rax@tok",
        "typing_tok_X64.Machine_s.Rbp@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
      ],
      0,
      "03c5adb6130482d1faca713cb585fe4a"
    ],
    [
      "X64.GCTRstdcall.va_wpCompute_gctr_bytes_stdcall128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp", "equality_tok_X64.Machine_s.Secret@tok",
        "equation_X64.GCTRstdcall.va_wp_gctr_bytes_stdcall128",
        "equation_X64.Vale.Decls.va_if",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "interpretation_Tm_abs_42acf2b4bd61f7d087f311642b137700",
        "interpretation_Tm_abs_efed28e5237cc814be518263d6481a87",
        "unit_typing"
      ],
      0,
      "d50432bc15e730f7373f6a0ed5336a7d"
    ],
    [
      "X64.GCTRstdcall.va_wpProof_gctr_bytes_stdcall128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "e3a1d358edcfcbbf3e848cbc85368d17"
    ],
    [
      "X64.GCTRstdcall.va_wpProof_gctr_bytes_stdcall128",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128", "eq2-interp",
        "equality_tok_X64.Machine_s.R10@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Words_s.nat64",
        "equation_Words_s.natN",
        "equation_X64.GCTRstdcall.va_wpCompute_gctr_bytes_stdcall128",
        "equation_X64.GCTRstdcall.va_wp_gctr_bytes_stdcall128",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_if",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int", "int_inversion", "int_typing",
        "interpretation_Tm_abs_42acf2b4bd61f7d087f311642b137700",
        "interpretation_Tm_abs_efed28e5237cc814be518263d6481a87",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.GCTRstdcall.va_wpCompute_gctr_bytes_stdcall128",
        "typing_Tm_abs_42acf2b4bd61f7d087f311642b137700",
        "typing_Tm_abs_efed28e5237cc814be518263d6481a87",
        "typing_X64.Vale.Decls.va_if", "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.State.update_reg", "typing_X64.Vale.Xmms.sel",
        "typing_tok_X64.Machine_s.R10@tok",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.R15@tok",
        "typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
        "typing_tok_X64.Machine_s.Rax@tok",
        "typing_tok_X64.Machine_s.Rbp@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
      ],
      0,
      "cc28a082418d5bb79226d12fd5941f1d"
    ],
    [
      "X64.GCTRstdcall.va_req_inc32_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.eq2", "equation_Prims.l_and",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "unit_typing"
      ],
      0,
      "d587dac75bad8b782aae26cb7349c77b"
    ],
    [
      "X64.GCTRstdcall.va_ens_inc32_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of", "equation_X64.Vale.Decls.va_state_eq",
        "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "unit_typing"
      ],
      0,
      "b4ebb8b57078e8571886959f70bb30c1"
    ],
    [
      "X64.GCTRstdcall.va_lemma_inc32_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "constructor_distinct_Interop.Types.TUInt128",
        "constructor_distinct_X64.Machine_s.Rax",
        "disc_equation_X64.Machine_s.Rsp", "eq2-interp",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_Interop.Types.TUInt64@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_imp",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Prop_s.prop0",
        "equation_Types_s.insert_nat32", "equation_Types_s.quad32",
        "equation_Words.Four_s.four_insert", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128", "equation_X64.Memory.buffer64",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.valid_stack_slots",
        "equation_X64.Vale.State.state_eq",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Words_s.nat32", "int_typing", "l_and-interp",
        "l_imp-interp", "l_not-interp",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "lemma_X64.Memory.loc_includes_refl",
        "lemma_X64.Memory.loc_includes_union_l_buffer",
        "lemma_X64.Memory.modifies_goal_directed_refl",
        "lemma_X64.Memory.modifies_goal_directed_trans",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Machine_s.OReg_r",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_Words_s.Mkfour_hi2",
        "projection_inverse_Words_s.Mkfour_hi3",
        "projection_inverse_Words_s.Mkfour_lo1",
        "projection_inverse_X64.Machine_s.OReg_r",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5bb8ca8bd1e34326f95f9f0f9a641acf",
        "refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing",
        "typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
        "typing_GCTR_s.inc32", "typing_Prims.eq2", "typing_Prims.l_and",
        "typing_Types_s.quad32", "typing_Words_s.__proj__Mkfour__item__hi3",
        "typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
        "typing_X64.Memory.buffer_readable",
        "typing_X64.Memory.buffer_write",
        "typing_X64.Memory.buffer_writeable", "typing_X64.Memory.loc_buffer",
        "typing_X64.Memory.loc_union", "typing_X64.Memory.modifies",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_Interop.Types.TUInt64@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok", "unit_typing"
      ],
      0,
      "cb308fd37d6cb6fae6f175722eec1843"
    ],
    [
      "X64.GCTRstdcall.va_wpMonotone_inc32_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equality_tok_X64.Machine_s.R10@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equation_X64.GCTRstdcall.va_wp_inc32_stdcall",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_reg",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_X64.Machine_s.R10@tok",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.R15@tok",
        "typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
        "typing_tok_X64.Machine_s.Rax@tok",
        "typing_tok_X64.Machine_s.Rbp@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
      ],
      0,
      "3b3b68f0f4bd40a687254162a59a3111"
    ],
    [
      "X64.GCTRstdcall.va_wpCompute_inc32_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.GCTRstdcall.va_wp_inc32_stdcall",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "9be7fb089f6384219bef030272db549e"
    ],
    [
      "X64.GCTRstdcall.va_wpProof_inc32_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "2efb117be7f4e368437330065b7505a0"
    ],
    [
      "X64.GCTRstdcall.va_wpProof_inc32_stdcall",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp", "equality_tok_X64.Machine_s.R10@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equation_X64.GCTRstdcall.va_wpCompute_inc32_stdcall",
        "equation_X64.GCTRstdcall.va_wp_inc32_stdcall",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.GCTRstdcall.va_wpCompute_inc32_stdcall",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.State.update_reg", "typing_X64.Vale.Xmms.sel",
        "typing_tok_X64.Machine_s.R10@tok",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.R15@tok",
        "typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
        "typing_tok_X64.Machine_s.Rax@tok",
        "typing_tok_X64.Machine_s.Rbp@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
      ],
      0,
      "0887ab8001061bd302f2df56846149ec"
    ],
    [
      "X64.GCTRstdcall.va_req_gctr_bytes_extra_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of",
        "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "unit_typing"
      ],
      0,
      "25be695690f56dca9fce1dcbef131f6f"
    ],
    [
      "X64.GCTRstdcall.va_ens_gctr_bytes_extra_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "constructor_distinct_Interop.Types.TUInt128",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equation_GCTR.make_gctr_plain_LE",
        "equation_GCTR_s.is_gctr_plain_LE", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Prims.subtype_of", "equation_Types_s.quad32",
        "equation_Words_s.nat32", "equation_Words_s.nat64",
        "equation_Words_s.nat8", "equation_Words_s.natN",
        "equation_X64.GCTRstdcall.va_req_gctr_bytes_extra_stdcall",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_state_eq",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat8", "int_inversion",
        "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "lemma_Types_s.le_seq_quad32_to_bytes_length",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.empty", "typing_X64.Memory.buffer_as_seq",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_tok_Interop.Types.TUInt128@tok", "unit_typing"
      ],
      0,
      "bd7e970bf7defd5b988d9c8507867256"
    ],
    [
      "X64.GCTRstdcall.va_lemma_gctr_bytes_extra_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Interop.Types.TUInt128",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equation_AES_s.key_to_round_keys_LE",
        "equation_GCTR.make_gctr_plain_LE",
        "equation_GCTR_s.is_gctr_plain_LE", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.nat8",
        "equation_Words_s.natN", "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat8", "int_inversion",
        "lemma_Types_s.le_seq_quad32_to_bytes_length",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_8610154d8fdf22507988d98d14130773",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_fbd1322eaad6b0eab99798f0e8856c8e",
        "typing_AES_s.key_to_round_keys_LE", "typing_FStar.Seq.Base.empty",
        "typing_X64.CPU_Features_s.aesni_enabled",
        "typing_X64.Memory.buffer_as_seq", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_tok_AES_s.AES_128@tok",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok"
      ],
      0,
      "2ec36674d015e9f95cda8510062556c7"
    ],
    [
      "X64.GCTRstdcall.va_lemma_gctr_bytes_extra_stdcall",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "constructor_distinct_AES_s.AES_128",
        "constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_Interop.Types.TUInt64@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_GCTR.make_gctr_plain_LE",
        "equation_GCTR_s.is_gctr_plain_LE", "equation_Prims.eq2",
        "equation_Prims.l_False", "equation_Prims.l_and",
        "equation_Prims.l_imp", "equation_Prims.l_not",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Prop_s.prop0",
        "equation_Types_s.le_seq_quad32_to_bytes", "equation_Types_s.quad32",
        "equation_Words_s.nat64", "equation_Words_s.nat8",
        "equation_Words_s.natN", "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128", "equation_X64.Memory.buffer64",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validDstAddrs128",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.Decls.valid_stack_slots",
        "equation_X64.Vale.QuickCodes.range1",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat64",
        "function_token_typing_Words_s.nat8", "int_inversion",
        "kinding_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b", "l_and-interp",
        "l_imp-interp", "l_not-interp",
        "lemma_Types_s.le_seq_quad32_to_bytes_length",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "lemma_X64.Memory.loc_includes_refl",
        "lemma_X64.Memory.loc_includes_union_l_buffer",
        "lemma_X64.Memory.modifies_goal_directed_refl",
        "lemma_X64.Memory.modifies_goal_directed_trans",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_interpretation_Tm_refine_fbd1322eaad6b0eab99798f0e8856c8e",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_AES_s.key_to_round_keys_LE",
        "typing_FStar.Seq.Base.empty", "typing_Prims.eq2",
        "typing_Prims.l_imp", "typing_Prims.squash",
        "typing_X64.CPU_Features_s.aesni_enabled",
        "typing_X64.Memory.buffer_addr", "typing_X64.Memory.buffer_as_seq",
        "typing_X64.Memory.loc_buffer", "typing_X64.Memory.loc_union",
        "typing_X64.Memory.modifies", "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_tok_AES_s.AES_128@tok",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_Interop.Types.TUInt64@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.R15@tok",
        "typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
        "typing_tok_X64.Machine_s.Rbp@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok", "unit_inversion", "unit_typing"
      ],
      0,
      "619849088889fd4fe9cbfb191781ee83"
    ],
    [
      "X64.GCTRstdcall.va_wp_gctr_bytes_extra_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Interop.Types.TUInt128",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.R10@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equation_GCTR.make_gctr_plain_LE",
        "equation_GCTR_s.is_gctr_plain_LE", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat64",
        "equation_Words_s.nat8", "equation_Words_s.natN",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat8", "int_inversion",
        "lemma_Types_s.le_seq_quad32_to_bytes_length",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_fbd1322eaad6b0eab99798f0e8856c8e",
        "typing_AES_s.key_to_round_keys_LE", "typing_FStar.Seq.Base.empty",
        "typing_X64.Memory.buffer_as_seq",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_tok_AES_s.AES_128@tok",
        "typing_tok_Interop.Types.TUInt128@tok"
      ],
      0,
      "3ef1a3ef2d9f5929d31c58411fef4b32"
    ],
    [
      "X64.GCTRstdcall.va_wpMonotone_gctr_bytes_extra_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_X64.Machine_s.R10@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equation_X64.GCTRstdcall.va_wp_gctr_bytes_extra_stdcall",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_reg",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_X64.Machine_s.R10@tok",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.R15@tok",
        "typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
        "typing_tok_X64.Machine_s.Rax@tok",
        "typing_tok_X64.Machine_s.Rbp@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
      ],
      0,
      "40be613af68f75aad056515617eae667"
    ],
    [
      "X64.GCTRstdcall.va_wpCompute_gctr_bytes_extra_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.GCTRstdcall.va_wp_gctr_bytes_extra_stdcall",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "847c1ea8fa50052471a824d110271f7a"
    ],
    [
      "X64.GCTRstdcall.va_wpProof_gctr_bytes_extra_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "f530b82b81c850eb4a66d37275329824"
    ],
    [
      "X64.GCTRstdcall.va_wpProof_gctr_bytes_extra_stdcall",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128", "eq2-interp",
        "equality_tok_X64.Machine_s.R10@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.GCTRstdcall.va_wpCompute_gctr_bytes_extra_stdcall",
        "equation_X64.GCTRstdcall.va_wp_gctr_bytes_extra_stdcall",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.GCTRstdcall.va_wpCompute_gctr_bytes_extra_stdcall",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.State.update_reg", "typing_X64.Vale.Xmms.sel",
        "typing_tok_X64.Machine_s.R10@tok",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.R15@tok",
        "typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
        "typing_tok_X64.Machine_s.Rax@tok",
        "typing_tok_X64.Machine_s.Rbp@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
      ],
      0,
      "13130fa931656d87fde5413ea7b8a62d"
    ]
  ]
]