[
  "^\u0002W䔄�����#�,��",
  [
    [
      "X64.Vale.InsAes.va_lemma_Pclmulqdq",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
        "@query",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
        "Prims_interpretation_Tm_arrow_e06752ba152f81447b312efcdf8f0e23",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "X64.Bytes_Semantics_s_interpretation_Tm_arrow_17742a16dc7ea8ebf4db7d06d09f33c0",
        "X64.Bytes_Semantics_s_interpretation_Tm_arrow_ee7017858cc0d7eacce54d227f2089c3",
        "X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
        "X64.Machine_s_interpretation_Tm_arrow_196f8dfca6d67b0bd046e19b6a5a08e6",
        "X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
        "X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_FStar.Pervasives.Native.Some",
        "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit",
        "constructor_distinct_X64.Bytes_Semantics_s.Pclmulqdq",
        "constructor_distinct_X64.Machine_s.Ins",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_X64.Bytes_Semantics_s.Pclmulqdq@tok",
        "data_typing_intro_X64.Taint_Semantics_s.TaintedIns@tok",
        "disc_equation_X64.Bytes_Semantics_s.MOVDQU",
        "disc_equation_X64.Bytes_Semantics_s.Mulx64",
        "disc_equation_X64.Bytes_Semantics_s.Push",
        "disc_equation_X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_X64.Machine_s.Public@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equation_Arch.Types.quad32_double_hi",
        "equation_Arch.Types.quad32_double_lo",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.on_dom",
        "equation_FStar.List.Tot.Base.op_At",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Types_s.quad32",
        "equation_Words.Four_s.four_to_two_two", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.nat8",
        "equation_X64.Bytes_Semantics_s.eval_ins",
        "equation_X64.Bytes_Semantics_s.update_xmm",
        "equation_X64.Bytes_Semantics_s.update_xmm_",
        "equation_X64.Machine_s.xmm", "equation_X64.Memory.memtaint",
        "equation_X64.Taint_Semantics_s.extract_operands",
        "equation_X64.Taint_Semantics_s.ins_obs",
        "equation_X64.Taint_Semantics_s.taint_eval_ins",
        "equation_X64.Taint_Semantics_s.tainted_code",
        "equation_X64.Vale.Decls.eval_code", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_fuel",
        "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_ok",
        "equation_X64.Vale.InsAes.va_code_Pclmulqdq",
        "equation_X64.Vale.InsAes.va_transparent_code_Pclmulqdq",
        "equation_X64.Vale.Lemmas.eval_code",
        "equation_X64.Vale.Lemmas.eval_ins",
        "equation_X64.Vale.Lemmas.state_eq_S",
        "equation_X64.Vale.Lemmas.state_eq_opt",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_X64.Vale.StateLemmas.state_of_S",
        "equation_X64.Vale.StateLemmas.state_to_S",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.unit",
        "function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
        "function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_1861e1dfbce217b81baf39da7dbe5796",
        "interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
        "interpretation_Tm_abs_4a1a6682764b8be475443da6650b9908",
        "interpretation_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
        "interpretation_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
        "interpretation_Tm_abs_670af97d1f975f383f2e3721377d2b05",
        "interpretation_Tm_abs_903982188305b836297ca9b101a106e0",
        "interpretation_Tm_abs_d2269df42a02340ac68914c195104ae6",
        "interpretation_Tm_abs_d882664a0b10396663ea993aaadb25ea",
        "kinding_X64.Bytes_Semantics_s.state@tok",
        "kinding_X64.Machine_s.observation@tok",
        "kinding_X64.Machine_s.operand@tok", "kinding_X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_FStar.List.Tot.Properties.append_l_nil",
        "lemma_X64.Memory_Sems.get_hs_heap",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.StateLemmas.lemma_to_flags",
        "lemma_X64.Vale.StateLemmas.lemma_to_memTaint",
        "lemma_X64.Vale.StateLemmas.lemma_to_ok",
        "lemma_X64.Vale.StateLemmas.lemma_to_reg",
        "lemma_X64.Vale.StateLemmas.lemma_to_trace",
        "lemma_X64.Vale.StateLemmas.lemma_to_xmm",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_upd_eq",
        "lemma_X64.Vale.Xmms.lemma_upd_ne", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_Words_s.Mktwo_hi", "proj_equation_Words_s.Mktwo_lo",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_flags",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_state",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_trace",
        "proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
        "proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
        "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.Some_a",
        "projection_inverse_FStar.Pervasives.Native.Some_v",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_Words_s.Mktwo_hi",
        "projection_inverse_Words_s.Mktwo_lo",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
        "projection_inverse_X64.Bytes_Semantics_s.Pclmulqdq_dst",
        "projection_inverse_X64.Bytes_Semantics_s.Pclmulqdq_imm",
        "projection_inverse_X64.Bytes_Semantics_s.Pclmulqdq_src",
        "projection_inverse_X64.Machine_s.Ins_ins",
        "projection_inverse_X64.Machine_s.Ins_t_ins",
        "projection_inverse_X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
        "projection_inverse_X64.Taint_Semantics_s.TaintedIns_i",
        "projection_inverse_X64.Taint_Semantics_s.TaintedIns_t",
        "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_06317ab318b717f15fdf594a5f399405",
        "refinement_interpretation_Tm_refine_2c90c44e0c3d494a57f4a23c91ef834a",
        "refinement_interpretation_Tm_refine_33d3ef68371378c171a37d999106817a",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
        "typing_Arch.Types.quad32_double_lo",
        "typing_FStar.Pervasives.Native.snd",
        "typing_Math.Poly2.Bits_s.of_double32",
        "typing_Math.Poly2.Bits_s.to_quad32", "typing_Math.Poly2_s.mul",
        "typing_Tm_abs_1861e1dfbce217b81baf39da7dbe5796",
        "typing_Tm_abs_4a1a6682764b8be475443da6650b9908",
        "typing_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
        "typing_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
        "typing_Tm_abs_91d6891d766466e9703afb13e7f1a1bf",
        "typing_Tm_abs_f705a29f07310120391898edc8e7c102",
        "typing_X64.CPU_Features_s.pclmulqdq_enabled",
        "typing_X64.Machine_s.xmm",
        "typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
        "typing_X64.Taint_Semantics_s.ins_obs",
        "typing_X64.Taint_Semantics_s.operand_obs_list",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.InsAes.va_transparent_code_Pclmulqdq",
        "typing_X64.Vale.Regs.of_fun",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "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_X64.Vale.State.update_xmm",
        "typing_X64.Vale.StateLemmas.state_to_S",
        "typing_X64.Vale.Xmms.of_fun", "typing_X64.Vale.Xmms.sel",
        "typing_tok_X64.Machine_s.Public@tok",
        "typing_tok_X64.Machine_s.Rax@tok", "unit_typing"
      ],
      0,
      "40229791f9a62b22ce857d1977317adc"
    ],
    [
      "X64.Vale.InsAes.va_wpMonotone_Pclmulqdq",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_X64.Vale.InsAes.va_wp_Pclmulqdq",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_operand_xmm", "unit_typing"
      ],
      0,
      "0d17b06d3a1490f8baf73e278848f397"
    ],
    [
      "X64.Vale.InsAes.va_wpCompute_Pclmulqdq",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.InsAes.va_code_Pclmulqdq",
        "equation_X64.Vale.InsAes.va_wp_Pclmulqdq",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "refinement_interpretation_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
      ],
      0,
      "90283d5d1a922dd99a260cfe1b2c22c4"
    ],
    [
      "X64.Vale.InsAes.va_wpProof_Pclmulqdq",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "0c8688c6b87918676a76eb1b1fabe527"
    ],
    [
      "X64.Vale.InsAes.va_wpProof_Pclmulqdq",
      2,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
        "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "X64.Vale.QuickCode_pretyping_5ef17715065c7f9c7618e13aa923e84c",
        "bool_inversion", "constructor_distinct_Prims.Nil",
        "constructor_distinct_X64.Vale.QuickCode.Mod_xmm",
        "data_typing_intro_Prims.Nil@tok", "eq2-interp",
        "equality_tok_X64.Vale.QuickCode.Mod_None@tok", "equation_Prims.nat",
        "equation_Types_s.double32", "equation_Words_s.nat32",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_fuel", "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_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.InsAes.va_code_Pclmulqdq",
        "equation_X64.Vale.InsAes.va_wpCompute_Pclmulqdq",
        "equation_X64.Vale.InsAes.va_wp_Pclmulqdq",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.QuickCode.va_mod_xmm",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_with_fuel_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "interpretation_Tm_abs_3426d37dde1640f4e2938890902550cc",
        "interpretation_Tm_abs_6f1ed8d6802a57b385878ce476855175",
        "kinding_X64.Vale.QuickCode.mod_t@tok",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.StateLemmas.lemma_to_flags",
        "lemma_X64.Vale.StateLemmas.lemma_to_ok",
        "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_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_X64.Vale.QuickCode.Mod_xmm__0",
        "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.Vale.InsAes.va_wpCompute_Pclmulqdq",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "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.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Vale.QuickCode.Mod_None@tok", "unit_typing"
      ],
      0,
      "148be5cc41090fc799b908ceee78e292"
    ],
    [
      "X64.Vale.InsAes.va_lemma_AESNI_enc",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
        "@query",
        "Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
        "Prims_interpretation_Tm_arrow_e06752ba152f81447b312efcdf8f0e23",
        "Prims_interpretation_Tm_arrow_fa4e3ee4a3dfa402363cd0693fcbfca4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "X64.Bytes_Semantics_s_interpretation_Tm_arrow_17742a16dc7ea8ebf4db7d06d09f33c0",
        "X64.Bytes_Semantics_s_interpretation_Tm_arrow_ee7017858cc0d7eacce54d227f2089c3",
        "X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
        "X64.Machine_s_interpretation_Tm_arrow_196f8dfca6d67b0bd046e19b6a5a08e6",
        "X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
        "X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit",
        "constructor_distinct_X64.Bytes_Semantics_s.AESNI_enc",
        "constructor_distinct_X64.Machine_s.Ins",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_X64.Bytes_Semantics_s.AESNI_enc@tok",
        "data_typing_intro_X64.Taint_Semantics_s.TaintedIns@tok",
        "disc_equation_X64.Bytes_Semantics_s.MOVDQU",
        "disc_equation_X64.Bytes_Semantics_s.Mulx64",
        "disc_equation_X64.Bytes_Semantics_s.Push",
        "disc_equation_X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_X64.Machine_s.Public@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.on_dom",
        "equation_FStar.List.Tot.Base.op_At",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Types_s.quad32",
        "equation_Types_s.quad32_xor", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.nat8",
        "equation_X64.Bytes_Semantics_s.eval_ins",
        "equation_X64.Bytes_Semantics_s.update_xmm",
        "equation_X64.Bytes_Semantics_s.update_xmm_",
        "equation_X64.Machine_s.xmm", "equation_X64.Memory.memtaint",
        "equation_X64.Taint_Semantics_s.extract_operands",
        "equation_X64.Taint_Semantics_s.ins_obs",
        "equation_X64.Taint_Semantics_s.taint_eval_ins",
        "equation_X64.Taint_Semantics_s.tainted_code",
        "equation_X64.Vale.Decls.eval_code", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_fuel",
        "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_ok",
        "equation_X64.Vale.InsAes.va_code_AESNI_enc",
        "equation_X64.Vale.InsAes.va_transparent_code_AESNI_enc",
        "equation_X64.Vale.Lemmas.eval_code",
        "equation_X64.Vale.Lemmas.eval_ins",
        "equation_X64.Vale.Lemmas.state_eq_S",
        "equation_X64.Vale.Lemmas.state_eq_opt",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_X64.Vale.StateLemmas.state_of_S",
        "equation_X64.Vale.StateLemmas.state_to_S",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Bytes_Semantics_s.state",
        "fuel_guarded_inversion_X64.Taint_Semantics_s.traceState",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Opaque_s.make_opaque",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.unit",
        "function_token_typing_Types_s.quad32_xor_def",
        "function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
        "function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
        "int_inversion",
        "interpretation_Tm_abs_1861e1dfbce217b81baf39da7dbe5796",
        "interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
        "interpretation_Tm_abs_4a1a6682764b8be475443da6650b9908",
        "interpretation_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
        "interpretation_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
        "interpretation_Tm_abs_903982188305b836297ca9b101a106e0",
        "interpretation_Tm_abs_d2269df42a02340ac68914c195104ae6",
        "interpretation_Tm_abs_e187ece364e76c4553832df69e1813be",
        "kinding_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "kinding_X64.Bytes_Semantics_s.state@tok",
        "kinding_X64.Machine_s.observation@tok",
        "kinding_X64.Machine_s.operand@tok", "kinding_X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_FStar.List.Tot.Properties.append_l_nil",
        "lemma_X64.Memory_Sems.get_hs_heap",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.StateLemmas.lemma_to_flags",
        "lemma_X64.Vale.StateLemmas.lemma_to_memTaint",
        "lemma_X64.Vale.StateLemmas.lemma_to_ok",
        "lemma_X64.Vale.StateLemmas.lemma_to_reg",
        "lemma_X64.Vale.StateLemmas.lemma_to_trace",
        "lemma_X64.Vale.StateLemmas.lemma_to_xmm",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_upd_eq",
        "lemma_X64.Vale.Xmms.lemma_upd_ne", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_flags",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_state",
        "proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
        "proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
        "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_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Some_v",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_X64.Bytes_Semantics_s.AESNI_enc_dst",
        "projection_inverse_X64.Bytes_Semantics_s.AESNI_enc_src",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
        "projection_inverse_X64.Machine_s.Ins_ins",
        "projection_inverse_X64.Machine_s.Ins_t_ins",
        "projection_inverse_X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
        "projection_inverse_X64.Taint_Semantics_s.TaintedIns_i",
        "projection_inverse_X64.Taint_Semantics_s.TaintedIns_t",
        "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_2c90c44e0c3d494a57f4a23c91ef834a",
        "refinement_interpretation_Tm_refine_33d3ef68371378c171a37d999106817a",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Opaque_s.make_opaque",
        "token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
        "token_correspondence_X64.Bytes_Semantics_s.update_xmm",
        "typing_AES_s.mix_columns_LE", "typing_AES_s.shift_rows_LE",
        "typing_AES_s.sub_bytes", "typing_FStar.Pervasives.Native.snd",
        "typing_Tm_abs_1861e1dfbce217b81baf39da7dbe5796",
        "typing_Tm_abs_4a1a6682764b8be475443da6650b9908",
        "typing_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
        "typing_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
        "typing_Tm_abs_91d6891d766466e9703afb13e7f1a1bf",
        "typing_X64.CPU_Features_s.aesni_enabled",
        "typing_X64.Machine_s.xmm",
        "typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
        "typing_X64.Taint_Semantics_s.ins_obs",
        "typing_X64.Taint_Semantics_s.operand_obs_list",
        "typing_X64.Taint_Semantics_s.taint_eval_ins",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.InsAes.va_transparent_code_AESNI_enc",
        "typing_X64.Vale.Regs.of_fun",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "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_X64.Vale.State.update_xmm",
        "typing_X64.Vale.StateLemmas.state_to_S", "typing_X64.Vale.Xmms.sel",
        "typing_tok_X64.Machine_s.Public@tok",
        "typing_tok_X64.Machine_s.Rax@tok", "unit_typing"
      ],
      0,
      "18ec377dd448c79b813ecff252d9b1f0"
    ],
    [
      "X64.Vale.InsAes.va_wpMonotone_AESNI_enc",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_X64.Vale.InsAes.va_wp_AESNI_enc",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_operand_xmm", "unit_typing"
      ],
      0,
      "ad33abcc73f26345e437b464a6c0e653"
    ],
    [
      "X64.Vale.InsAes.va_wpCompute_AESNI_enc",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.InsAes.va_code_AESNI_enc",
        "equation_X64.Vale.InsAes.va_wp_AESNI_enc",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "refinement_interpretation_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
      ],
      0,
      "59a336f0fbfd35c0f0e0545c8c3c678a"
    ],
    [
      "X64.Vale.InsAes.va_wpProof_AESNI_enc",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "56854f20db846db531e7e25b50fbdf74"
    ],
    [
      "X64.Vale.InsAes.va_wpProof_AESNI_enc",
      2,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
        "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "X64.Vale.QuickCode_pretyping_5ef17715065c7f9c7618e13aa923e84c",
        "bool_inversion", "constructor_distinct_Prims.Nil",
        "constructor_distinct_X64.Vale.QuickCode.Mod_xmm",
        "data_typing_intro_Prims.Nil@tok", "eq2-interp",
        "equality_tok_X64.Vale.QuickCode.Mod_None@tok", "equation_Prims.nat",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_fuel",
        "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_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.InsAes.va_code_AESNI_enc",
        "equation_X64.Vale.InsAes.va_wpCompute_AESNI_enc",
        "equation_X64.Vale.InsAes.va_wp_AESNI_enc",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.QuickCode.va_mod_xmm",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_with_fuel_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "kinding_X64.Vale.QuickCode.mod_t@tok",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.StateLemmas.lemma_to_flags",
        "lemma_X64.Vale.StateLemmas.lemma_to_ok",
        "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_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_X64.Vale.QuickCode.Mod_xmm__0",
        "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_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.Vale.InsAes.va_wpCompute_AESNI_enc",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "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.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Vale.QuickCode.Mod_None@tok", "unit_typing"
      ],
      0,
      "57d317db853cc6638f472fdc270d40e4"
    ],
    [
      "X64.Vale.InsAes.va_lemma_AESNI_enc_last",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
        "@query",
        "Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
        "Prims_interpretation_Tm_arrow_e06752ba152f81447b312efcdf8f0e23",
        "Prims_interpretation_Tm_arrow_fa4e3ee4a3dfa402363cd0693fcbfca4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "X64.Bytes_Semantics_s_interpretation_Tm_arrow_17742a16dc7ea8ebf4db7d06d09f33c0",
        "X64.Bytes_Semantics_s_interpretation_Tm_arrow_ee7017858cc0d7eacce54d227f2089c3",
        "X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
        "X64.Machine_s_interpretation_Tm_arrow_196f8dfca6d67b0bd046e19b6a5a08e6",
        "X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
        "X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit",
        "constructor_distinct_X64.Bytes_Semantics_s.AESNI_enc_last",
        "constructor_distinct_X64.Machine_s.Ins",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_X64.Bytes_Semantics_s.AESNI_enc_last@tok",
        "data_typing_intro_X64.Taint_Semantics_s.TaintedIns@tok",
        "disc_equation_X64.Bytes_Semantics_s.MOVDQU",
        "disc_equation_X64.Bytes_Semantics_s.Mulx64",
        "disc_equation_X64.Bytes_Semantics_s.Push",
        "disc_equation_X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_X64.Machine_s.Public@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.on_dom",
        "equation_FStar.List.Tot.Base.op_At",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Types_s.quad32",
        "equation_Types_s.quad32_xor", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.nat8",
        "equation_X64.Bytes_Semantics_s.eval_ins",
        "equation_X64.Bytes_Semantics_s.update_xmm",
        "equation_X64.Bytes_Semantics_s.update_xmm_",
        "equation_X64.Machine_s.xmm", "equation_X64.Memory.memtaint",
        "equation_X64.Taint_Semantics_s.extract_operands",
        "equation_X64.Taint_Semantics_s.ins_obs",
        "equation_X64.Taint_Semantics_s.taint_eval_ins",
        "equation_X64.Taint_Semantics_s.tainted_code",
        "equation_X64.Vale.Decls.eval_code", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_fuel",
        "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_ok",
        "equation_X64.Vale.InsAes.va_code_AESNI_enc_last",
        "equation_X64.Vale.InsAes.va_transparent_code_AESNI_enc_last",
        "equation_X64.Vale.Lemmas.eval_code",
        "equation_X64.Vale.Lemmas.eval_ins",
        "equation_X64.Vale.Lemmas.state_eq_S",
        "equation_X64.Vale.Lemmas.state_eq_opt",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_X64.Vale.StateLemmas.state_of_S",
        "equation_X64.Vale.StateLemmas.state_to_S",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Bytes_Semantics_s.state",
        "fuel_guarded_inversion_X64.Taint_Semantics_s.traceState",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Opaque_s.make_opaque",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.unit",
        "function_token_typing_Types_s.quad32_xor_def",
        "function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
        "function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
        "int_inversion",
        "interpretation_Tm_abs_1861e1dfbce217b81baf39da7dbe5796",
        "interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
        "interpretation_Tm_abs_4a1a6682764b8be475443da6650b9908",
        "interpretation_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
        "interpretation_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
        "interpretation_Tm_abs_903982188305b836297ca9b101a106e0",
        "interpretation_Tm_abs_cd8978bb9635d9a30ffa6c1af398a4af",
        "interpretation_Tm_abs_d2269df42a02340ac68914c195104ae6",
        "kinding_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "kinding_X64.Bytes_Semantics_s.state@tok",
        "kinding_X64.Machine_s.observation@tok",
        "kinding_X64.Machine_s.operand@tok", "kinding_X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_FStar.List.Tot.Properties.append_l_nil",
        "lemma_X64.Memory_Sems.get_hs_heap",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.StateLemmas.lemma_to_flags",
        "lemma_X64.Vale.StateLemmas.lemma_to_memTaint",
        "lemma_X64.Vale.StateLemmas.lemma_to_ok",
        "lemma_X64.Vale.StateLemmas.lemma_to_reg",
        "lemma_X64.Vale.StateLemmas.lemma_to_trace",
        "lemma_X64.Vale.StateLemmas.lemma_to_xmm",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_upd_eq",
        "lemma_X64.Vale.Xmms.lemma_upd_ne", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_flags",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_state",
        "proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
        "proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
        "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_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Some_v",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_X64.Bytes_Semantics_s.AESNI_enc_last_dst",
        "projection_inverse_X64.Bytes_Semantics_s.AESNI_enc_last_src",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
        "projection_inverse_X64.Machine_s.Ins_ins",
        "projection_inverse_X64.Machine_s.Ins_t_ins",
        "projection_inverse_X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
        "projection_inverse_X64.Taint_Semantics_s.TaintedIns_i",
        "projection_inverse_X64.Taint_Semantics_s.TaintedIns_t",
        "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_2c90c44e0c3d494a57f4a23c91ef834a",
        "refinement_interpretation_Tm_refine_33d3ef68371378c171a37d999106817a",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Opaque_s.make_opaque",
        "token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
        "token_correspondence_X64.Bytes_Semantics_s.update_xmm",
        "typing_AES_s.shift_rows_LE", "typing_AES_s.sub_bytes",
        "typing_FStar.Pervasives.Native.snd",
        "typing_Tm_abs_1861e1dfbce217b81baf39da7dbe5796",
        "typing_Tm_abs_4a1a6682764b8be475443da6650b9908",
        "typing_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
        "typing_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
        "typing_Tm_abs_91d6891d766466e9703afb13e7f1a1bf",
        "typing_X64.CPU_Features_s.aesni_enabled",
        "typing_X64.Machine_s.xmm",
        "typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
        "typing_X64.Taint_Semantics_s.ins_obs",
        "typing_X64.Taint_Semantics_s.operand_obs_list",
        "typing_X64.Taint_Semantics_s.taint_eval_ins",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.InsAes.va_transparent_code_AESNI_enc_last",
        "typing_X64.Vale.Regs.of_fun",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "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_X64.Vale.State.update_xmm",
        "typing_X64.Vale.StateLemmas.state_to_S", "typing_X64.Vale.Xmms.sel",
        "typing_tok_X64.Machine_s.Public@tok",
        "typing_tok_X64.Machine_s.Rax@tok", "unit_typing"
      ],
      0,
      "c8a713b27d105321a2f39b63c0bb1019"
    ],
    [
      "X64.Vale.InsAes.va_wpMonotone_AESNI_enc_last",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_X64.Vale.InsAes.va_wp_AESNI_enc_last",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_operand_xmm", "unit_typing"
      ],
      0,
      "d323ef55e12910765eb0119d4162f76d"
    ],
    [
      "X64.Vale.InsAes.va_wpCompute_AESNI_enc_last",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.InsAes.va_code_AESNI_enc_last",
        "equation_X64.Vale.InsAes.va_wp_AESNI_enc_last",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "refinement_interpretation_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
      ],
      0,
      "c4d8212b360402985ccf518c31a643a2"
    ],
    [
      "X64.Vale.InsAes.va_wpProof_AESNI_enc_last",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "01b04ed1eb5d6c1f683c05aae1077c82"
    ],
    [
      "X64.Vale.InsAes.va_wpProof_AESNI_enc_last",
      2,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
        "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "X64.Vale.QuickCode_pretyping_5ef17715065c7f9c7618e13aa923e84c",
        "bool_inversion", "constructor_distinct_Prims.Nil",
        "constructor_distinct_X64.Vale.QuickCode.Mod_xmm",
        "data_typing_intro_Prims.Nil@tok", "eq2-interp",
        "equality_tok_X64.Vale.QuickCode.Mod_None@tok", "equation_Prims.nat",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_fuel",
        "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_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.InsAes.va_code_AESNI_enc_last",
        "equation_X64.Vale.InsAes.va_wpCompute_AESNI_enc_last",
        "equation_X64.Vale.InsAes.va_wp_AESNI_enc_last",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.QuickCode.va_mod_xmm",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_with_fuel_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "kinding_X64.Vale.QuickCode.mod_t@tok",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.StateLemmas.lemma_to_flags",
        "lemma_X64.Vale.StateLemmas.lemma_to_ok",
        "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_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_X64.Vale.QuickCode.Mod_xmm__0",
        "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_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.Vale.InsAes.va_wpCompute_AESNI_enc_last",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "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.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Vale.QuickCode.Mod_None@tok", "unit_typing"
      ],
      0,
      "3235e8d571388d7ec49899f9ace7142e"
    ],
    [
      "X64.Vale.InsAes.va_lemma_AESNI_dec",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
        "@query",
        "Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
        "Prims_interpretation_Tm_arrow_e06752ba152f81447b312efcdf8f0e23",
        "Prims_interpretation_Tm_arrow_fa4e3ee4a3dfa402363cd0693fcbfca4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "X64.Bytes_Semantics_s_interpretation_Tm_arrow_17742a16dc7ea8ebf4db7d06d09f33c0",
        "X64.Bytes_Semantics_s_interpretation_Tm_arrow_ee7017858cc0d7eacce54d227f2089c3",
        "X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
        "X64.Machine_s_interpretation_Tm_arrow_196f8dfca6d67b0bd046e19b6a5a08e6",
        "X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
        "X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit",
        "constructor_distinct_X64.Bytes_Semantics_s.AESNI_dec",
        "constructor_distinct_X64.Machine_s.Ins",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_X64.Bytes_Semantics_s.AESNI_dec@tok",
        "data_typing_intro_X64.Taint_Semantics_s.TaintedIns@tok",
        "disc_equation_X64.Bytes_Semantics_s.MOVDQU",
        "disc_equation_X64.Bytes_Semantics_s.Mulx64",
        "disc_equation_X64.Bytes_Semantics_s.Push",
        "disc_equation_X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_X64.Machine_s.Public@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.on_dom",
        "equation_FStar.List.Tot.Base.op_At",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Types_s.quad32",
        "equation_Types_s.quad32_xor", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.nat8",
        "equation_X64.Bytes_Semantics_s.eval_ins",
        "equation_X64.Bytes_Semantics_s.update_xmm",
        "equation_X64.Bytes_Semantics_s.update_xmm_",
        "equation_X64.Machine_s.xmm", "equation_X64.Memory.memtaint",
        "equation_X64.Taint_Semantics_s.extract_operands",
        "equation_X64.Taint_Semantics_s.ins_obs",
        "equation_X64.Taint_Semantics_s.taint_eval_ins",
        "equation_X64.Taint_Semantics_s.tainted_code",
        "equation_X64.Vale.Decls.eval_code", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_fuel",
        "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_ok",
        "equation_X64.Vale.InsAes.va_code_AESNI_dec",
        "equation_X64.Vale.InsAes.va_transparent_code_AESNI_dec",
        "equation_X64.Vale.Lemmas.eval_code",
        "equation_X64.Vale.Lemmas.eval_ins",
        "equation_X64.Vale.Lemmas.state_eq_S",
        "equation_X64.Vale.Lemmas.state_eq_opt",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_X64.Vale.StateLemmas.state_of_S",
        "equation_X64.Vale.StateLemmas.state_to_S",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Bytes_Semantics_s.state",
        "fuel_guarded_inversion_X64.Taint_Semantics_s.traceState",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Opaque_s.make_opaque",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.unit",
        "function_token_typing_Types_s.quad32_xor_def",
        "function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
        "function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
        "int_inversion",
        "interpretation_Tm_abs_0d8936a0210dec35b2ba102aaf3b6a51",
        "interpretation_Tm_abs_1861e1dfbce217b81baf39da7dbe5796",
        "interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
        "interpretation_Tm_abs_4a1a6682764b8be475443da6650b9908",
        "interpretation_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
        "interpretation_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
        "interpretation_Tm_abs_903982188305b836297ca9b101a106e0",
        "interpretation_Tm_abs_d2269df42a02340ac68914c195104ae6",
        "kinding_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "kinding_X64.Bytes_Semantics_s.state@tok",
        "kinding_X64.Machine_s.observation@tok",
        "kinding_X64.Machine_s.operand@tok", "kinding_X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_FStar.List.Tot.Properties.append_l_nil",
        "lemma_X64.Memory_Sems.get_hs_heap",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.StateLemmas.lemma_to_flags",
        "lemma_X64.Vale.StateLemmas.lemma_to_memTaint",
        "lemma_X64.Vale.StateLemmas.lemma_to_ok",
        "lemma_X64.Vale.StateLemmas.lemma_to_reg",
        "lemma_X64.Vale.StateLemmas.lemma_to_trace",
        "lemma_X64.Vale.StateLemmas.lemma_to_xmm",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_upd_eq",
        "lemma_X64.Vale.Xmms.lemma_upd_ne", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_flags",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_state",
        "proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
        "proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
        "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_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Some_v",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_X64.Bytes_Semantics_s.AESNI_dec_dst",
        "projection_inverse_X64.Bytes_Semantics_s.AESNI_dec_src",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
        "projection_inverse_X64.Machine_s.Ins_ins",
        "projection_inverse_X64.Machine_s.Ins_t_ins",
        "projection_inverse_X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
        "projection_inverse_X64.Taint_Semantics_s.TaintedIns_i",
        "projection_inverse_X64.Taint_Semantics_s.TaintedIns_t",
        "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_2c90c44e0c3d494a57f4a23c91ef834a",
        "refinement_interpretation_Tm_refine_33d3ef68371378c171a37d999106817a",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Opaque_s.make_opaque",
        "token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
        "token_correspondence_X64.Bytes_Semantics_s.update_xmm",
        "typing_AES_s.inv_mix_columns_LE", "typing_AES_s.inv_shift_rows_LE",
        "typing_AES_s.inv_sub_bytes", "typing_FStar.Pervasives.Native.snd",
        "typing_Tm_abs_1861e1dfbce217b81baf39da7dbe5796",
        "typing_Tm_abs_4a1a6682764b8be475443da6650b9908",
        "typing_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
        "typing_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
        "typing_Tm_abs_91d6891d766466e9703afb13e7f1a1bf",
        "typing_X64.CPU_Features_s.aesni_enabled",
        "typing_X64.Machine_s.xmm",
        "typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
        "typing_X64.Taint_Semantics_s.ins_obs",
        "typing_X64.Taint_Semantics_s.operand_obs_list",
        "typing_X64.Taint_Semantics_s.taint_eval_ins",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.InsAes.va_transparent_code_AESNI_dec",
        "typing_X64.Vale.Regs.of_fun",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "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_X64.Vale.State.update_xmm",
        "typing_X64.Vale.StateLemmas.state_to_S", "typing_X64.Vale.Xmms.sel",
        "typing_tok_X64.Machine_s.Public@tok",
        "typing_tok_X64.Machine_s.Rax@tok", "unit_typing"
      ],
      0,
      "0d922d449667f37b5d2647b7bff63684"
    ],
    [
      "X64.Vale.InsAes.va_wpMonotone_AESNI_dec",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_X64.Vale.InsAes.va_wp_AESNI_dec",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_operand_xmm", "unit_typing"
      ],
      0,
      "4424911ce35e4b2a09e0b0099802e8d9"
    ],
    [
      "X64.Vale.InsAes.va_wpCompute_AESNI_dec",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.InsAes.va_code_AESNI_dec",
        "equation_X64.Vale.InsAes.va_wp_AESNI_dec",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "refinement_interpretation_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
      ],
      0,
      "bbe5bf75cf226f196d84e39804915a71"
    ],
    [
      "X64.Vale.InsAes.va_wpProof_AESNI_dec",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "ca3b3a2221f95b371be6bbf3b4c41b65"
    ],
    [
      "X64.Vale.InsAes.va_wpProof_AESNI_dec",
      2,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
        "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "X64.Vale.QuickCode_pretyping_5ef17715065c7f9c7618e13aa923e84c",
        "bool_inversion", "constructor_distinct_Prims.Nil",
        "constructor_distinct_X64.Vale.QuickCode.Mod_xmm",
        "data_typing_intro_Prims.Nil@tok", "eq2-interp",
        "equality_tok_X64.Vale.QuickCode.Mod_None@tok", "equation_Prims.nat",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_fuel",
        "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_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.InsAes.va_code_AESNI_dec",
        "equation_X64.Vale.InsAes.va_wpCompute_AESNI_dec",
        "equation_X64.Vale.InsAes.va_wp_AESNI_dec",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.QuickCode.va_mod_xmm",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_with_fuel_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "kinding_X64.Vale.QuickCode.mod_t@tok",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.StateLemmas.lemma_to_flags",
        "lemma_X64.Vale.StateLemmas.lemma_to_ok",
        "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_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_X64.Vale.QuickCode.Mod_xmm__0",
        "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_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.Vale.InsAes.va_wpCompute_AESNI_dec",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "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.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Vale.QuickCode.Mod_None@tok", "unit_typing"
      ],
      0,
      "fb95529357fb67d78260497628519fae"
    ],
    [
      "X64.Vale.InsAes.va_lemma_AESNI_dec_last",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
        "@query",
        "Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
        "Prims_interpretation_Tm_arrow_e06752ba152f81447b312efcdf8f0e23",
        "Prims_interpretation_Tm_arrow_fa4e3ee4a3dfa402363cd0693fcbfca4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "X64.Bytes_Semantics_s_interpretation_Tm_arrow_17742a16dc7ea8ebf4db7d06d09f33c0",
        "X64.Bytes_Semantics_s_interpretation_Tm_arrow_ee7017858cc0d7eacce54d227f2089c3",
        "X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
        "X64.Machine_s_interpretation_Tm_arrow_196f8dfca6d67b0bd046e19b6a5a08e6",
        "X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
        "X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit",
        "constructor_distinct_X64.Bytes_Semantics_s.AESNI_dec_last",
        "constructor_distinct_X64.Machine_s.Ins",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_X64.Bytes_Semantics_s.AESNI_dec_last@tok",
        "data_typing_intro_X64.Taint_Semantics_s.TaintedIns@tok",
        "disc_equation_X64.Bytes_Semantics_s.MOVDQU",
        "disc_equation_X64.Bytes_Semantics_s.Mulx64",
        "disc_equation_X64.Bytes_Semantics_s.Push",
        "disc_equation_X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_X64.Machine_s.Public@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.on_dom",
        "equation_FStar.List.Tot.Base.op_At",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Types_s.quad32",
        "equation_Types_s.quad32_xor", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.nat8",
        "equation_X64.Bytes_Semantics_s.eval_ins",
        "equation_X64.Bytes_Semantics_s.update_xmm",
        "equation_X64.Bytes_Semantics_s.update_xmm_",
        "equation_X64.Machine_s.xmm", "equation_X64.Memory.memtaint",
        "equation_X64.Taint_Semantics_s.extract_operands",
        "equation_X64.Taint_Semantics_s.ins_obs",
        "equation_X64.Taint_Semantics_s.taint_eval_ins",
        "equation_X64.Taint_Semantics_s.tainted_code",
        "equation_X64.Vale.Decls.eval_code", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_fuel",
        "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_ok",
        "equation_X64.Vale.InsAes.va_code_AESNI_dec_last",
        "equation_X64.Vale.InsAes.va_transparent_code_AESNI_dec_last",
        "equation_X64.Vale.Lemmas.eval_code",
        "equation_X64.Vale.Lemmas.eval_ins",
        "equation_X64.Vale.Lemmas.state_eq_S",
        "equation_X64.Vale.Lemmas.state_eq_opt",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_X64.Vale.StateLemmas.state_of_S",
        "equation_X64.Vale.StateLemmas.state_to_S",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Bytes_Semantics_s.state",
        "fuel_guarded_inversion_X64.Taint_Semantics_s.traceState",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Opaque_s.make_opaque",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.unit",
        "function_token_typing_Types_s.quad32_xor_def",
        "function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
        "function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
        "int_inversion",
        "interpretation_Tm_abs_1861e1dfbce217b81baf39da7dbe5796",
        "interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
        "interpretation_Tm_abs_4a1a6682764b8be475443da6650b9908",
        "interpretation_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
        "interpretation_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
        "interpretation_Tm_abs_6fc8dbe84a61f0bc1c4776e1b5f08e2e",
        "interpretation_Tm_abs_903982188305b836297ca9b101a106e0",
        "interpretation_Tm_abs_d2269df42a02340ac68914c195104ae6",
        "kinding_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "kinding_X64.Bytes_Semantics_s.state@tok",
        "kinding_X64.Machine_s.observation@tok",
        "kinding_X64.Machine_s.operand@tok", "kinding_X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_FStar.List.Tot.Properties.append_l_nil",
        "lemma_X64.Memory_Sems.get_hs_heap",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.StateLemmas.lemma_to_flags",
        "lemma_X64.Vale.StateLemmas.lemma_to_memTaint",
        "lemma_X64.Vale.StateLemmas.lemma_to_ok",
        "lemma_X64.Vale.StateLemmas.lemma_to_reg",
        "lemma_X64.Vale.StateLemmas.lemma_to_trace",
        "lemma_X64.Vale.StateLemmas.lemma_to_xmm",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_upd_eq",
        "lemma_X64.Vale.Xmms.lemma_upd_ne", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_flags",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_state",
        "proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
        "proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
        "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_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Some_v",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_X64.Bytes_Semantics_s.AESNI_dec_last_dst",
        "projection_inverse_X64.Bytes_Semantics_s.AESNI_dec_last_src",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
        "projection_inverse_X64.Machine_s.Ins_ins",
        "projection_inverse_X64.Machine_s.Ins_t_ins",
        "projection_inverse_X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
        "projection_inverse_X64.Taint_Semantics_s.TaintedIns_i",
        "projection_inverse_X64.Taint_Semantics_s.TaintedIns_t",
        "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_2c90c44e0c3d494a57f4a23c91ef834a",
        "refinement_interpretation_Tm_refine_33d3ef68371378c171a37d999106817a",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Opaque_s.make_opaque",
        "token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
        "token_correspondence_X64.Bytes_Semantics_s.update_xmm",
        "typing_AES_s.inv_shift_rows_LE", "typing_AES_s.inv_sub_bytes",
        "typing_FStar.Pervasives.Native.snd",
        "typing_Tm_abs_1861e1dfbce217b81baf39da7dbe5796",
        "typing_Tm_abs_4a1a6682764b8be475443da6650b9908",
        "typing_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
        "typing_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
        "typing_Tm_abs_91d6891d766466e9703afb13e7f1a1bf",
        "typing_X64.CPU_Features_s.aesni_enabled",
        "typing_X64.Machine_s.xmm",
        "typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
        "typing_X64.Taint_Semantics_s.ins_obs",
        "typing_X64.Taint_Semantics_s.operand_obs_list",
        "typing_X64.Taint_Semantics_s.taint_eval_ins",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.InsAes.va_transparent_code_AESNI_dec_last",
        "typing_X64.Vale.Regs.of_fun",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "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_X64.Vale.State.update_xmm",
        "typing_X64.Vale.StateLemmas.state_to_S", "typing_X64.Vale.Xmms.sel",
        "typing_tok_X64.Machine_s.Public@tok",
        "typing_tok_X64.Machine_s.Rax@tok", "unit_typing"
      ],
      0,
      "14dcac8e34639e2f5db9995b9b1a9f93"
    ],
    [
      "X64.Vale.InsAes.va_wpMonotone_AESNI_dec_last",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_X64.Vale.InsAes.va_wp_AESNI_dec_last",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_operand_xmm", "unit_typing"
      ],
      0,
      "c70c115ae4f4511873fc664e788917c7"
    ],
    [
      "X64.Vale.InsAes.va_wpCompute_AESNI_dec_last",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.InsAes.va_code_AESNI_dec_last",
        "equation_X64.Vale.InsAes.va_wp_AESNI_dec_last",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "refinement_interpretation_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
      ],
      0,
      "7d47f00979a6b2e858c2f8a55d4d9ef2"
    ],
    [
      "X64.Vale.InsAes.va_wpProof_AESNI_dec_last",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "009bc8c011c7b14fcb06a6cabab96e00"
    ],
    [
      "X64.Vale.InsAes.va_wpProof_AESNI_dec_last",
      2,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
        "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "X64.Vale.QuickCode_pretyping_5ef17715065c7f9c7618e13aa923e84c",
        "bool_inversion", "constructor_distinct_Prims.Nil",
        "constructor_distinct_X64.Vale.QuickCode.Mod_xmm",
        "data_typing_intro_Prims.Nil@tok", "eq2-interp",
        "equality_tok_X64.Vale.QuickCode.Mod_None@tok", "equation_Prims.nat",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_fuel",
        "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_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.InsAes.va_code_AESNI_dec_last",
        "equation_X64.Vale.InsAes.va_wpCompute_AESNI_dec_last",
        "equation_X64.Vale.InsAes.va_wp_AESNI_dec_last",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.QuickCode.va_mod_xmm",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_with_fuel_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "kinding_X64.Vale.QuickCode.mod_t@tok",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.StateLemmas.lemma_to_flags",
        "lemma_X64.Vale.StateLemmas.lemma_to_ok",
        "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_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_X64.Vale.QuickCode.Mod_xmm__0",
        "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_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.Vale.InsAes.va_wpCompute_AESNI_dec_last",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "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.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Vale.QuickCode.Mod_None@tok", "unit_typing"
      ],
      0,
      "86f0f07836c0c46102eb90602f57ffa3"
    ],
    [
      "X64.Vale.InsAes.va_lemma_AESNI_imc",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
        "@query",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
        "Prims_interpretation_Tm_arrow_e06752ba152f81447b312efcdf8f0e23",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "X64.Bytes_Semantics_s_interpretation_Tm_arrow_17742a16dc7ea8ebf4db7d06d09f33c0",
        "X64.Bytes_Semantics_s_interpretation_Tm_arrow_ee7017858cc0d7eacce54d227f2089c3",
        "X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
        "X64.Machine_s_interpretation_Tm_arrow_196f8dfca6d67b0bd046e19b6a5a08e6",
        "X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
        "X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit",
        "constructor_distinct_X64.Bytes_Semantics_s.AESNI_imc",
        "constructor_distinct_X64.Machine_s.Ins",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_X64.Bytes_Semantics_s.AESNI_imc@tok",
        "data_typing_intro_X64.Taint_Semantics_s.TaintedIns@tok",
        "disc_equation_X64.Bytes_Semantics_s.MOVDQU",
        "disc_equation_X64.Bytes_Semantics_s.Mulx64",
        "disc_equation_X64.Bytes_Semantics_s.Push",
        "disc_equation_X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_X64.Machine_s.Public@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.on_dom",
        "equation_FStar.List.Tot.Base.op_At",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Types_s.quad32",
        "equation_Words_s.nat32", "equation_Words_s.nat64",
        "equation_Words_s.nat8", "equation_X64.Bytes_Semantics_s.eval_ins",
        "equation_X64.Bytes_Semantics_s.update_xmm",
        "equation_X64.Bytes_Semantics_s.update_xmm_",
        "equation_X64.Machine_s.xmm", "equation_X64.Memory.memtaint",
        "equation_X64.Taint_Semantics_s.extract_operands",
        "equation_X64.Taint_Semantics_s.ins_obs",
        "equation_X64.Taint_Semantics_s.taint_eval_ins",
        "equation_X64.Taint_Semantics_s.tainted_code",
        "equation_X64.Vale.Decls.eval_code", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_fuel",
        "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_ok",
        "equation_X64.Vale.InsAes.va_code_AESNI_imc",
        "equation_X64.Vale.InsAes.va_transparent_code_AESNI_imc",
        "equation_X64.Vale.Lemmas.eval_code",
        "equation_X64.Vale.Lemmas.eval_ins",
        "equation_X64.Vale.Lemmas.state_eq_S",
        "equation_X64.Vale.Lemmas.state_eq_opt",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_X64.Vale.StateLemmas.state_of_S",
        "equation_X64.Vale.StateLemmas.state_to_S",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Bytes_Semantics_s.state",
        "fuel_guarded_inversion_X64.Taint_Semantics_s.traceState",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.unit",
        "function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
        "function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
        "int_inversion",
        "interpretation_Tm_abs_1861e1dfbce217b81baf39da7dbe5796",
        "interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
        "interpretation_Tm_abs_4a1a6682764b8be475443da6650b9908",
        "interpretation_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
        "interpretation_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
        "interpretation_Tm_abs_903982188305b836297ca9b101a106e0",
        "interpretation_Tm_abs_b5bf0359e228bdc60445d43151ffd49d",
        "interpretation_Tm_abs_d2269df42a02340ac68914c195104ae6",
        "kinding_X64.Bytes_Semantics_s.state@tok",
        "kinding_X64.Machine_s.observation@tok",
        "kinding_X64.Machine_s.operand@tok", "kinding_X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_FStar.List.Tot.Properties.append_l_nil",
        "lemma_X64.Memory_Sems.get_hs_heap",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.StateLemmas.lemma_to_flags",
        "lemma_X64.Vale.StateLemmas.lemma_to_memTaint",
        "lemma_X64.Vale.StateLemmas.lemma_to_ok",
        "lemma_X64.Vale.StateLemmas.lemma_to_reg",
        "lemma_X64.Vale.StateLemmas.lemma_to_trace",
        "lemma_X64.Vale.StateLemmas.lemma_to_xmm",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_upd_eq",
        "lemma_X64.Vale.Xmms.lemma_upd_ne", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_flags",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_state",
        "proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
        "proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
        "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_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Some_v",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_X64.Bytes_Semantics_s.AESNI_imc_dst",
        "projection_inverse_X64.Bytes_Semantics_s.AESNI_imc_src",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
        "projection_inverse_X64.Machine_s.Ins_ins",
        "projection_inverse_X64.Machine_s.Ins_t_ins",
        "projection_inverse_X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
        "projection_inverse_X64.Taint_Semantics_s.TaintedIns_i",
        "projection_inverse_X64.Taint_Semantics_s.TaintedIns_t",
        "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_2c90c44e0c3d494a57f4a23c91ef834a",
        "refinement_interpretation_Tm_refine_33d3ef68371378c171a37d999106817a",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
        "token_correspondence_X64.Bytes_Semantics_s.update_xmm",
        "typing_AES_s.inv_mix_columns_LE",
        "typing_FStar.Pervasives.Native.snd",
        "typing_Tm_abs_1861e1dfbce217b81baf39da7dbe5796",
        "typing_Tm_abs_4a1a6682764b8be475443da6650b9908",
        "typing_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
        "typing_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
        "typing_Tm_abs_91d6891d766466e9703afb13e7f1a1bf",
        "typing_X64.CPU_Features_s.aesni_enabled",
        "typing_X64.Machine_s.xmm",
        "typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
        "typing_X64.Taint_Semantics_s.ins_obs",
        "typing_X64.Taint_Semantics_s.operand_obs_list",
        "typing_X64.Taint_Semantics_s.taint_eval_ins",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.InsAes.va_transparent_code_AESNI_imc",
        "typing_X64.Vale.Regs.of_fun",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "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_X64.Vale.State.update_xmm",
        "typing_X64.Vale.StateLemmas.state_to_S", "typing_X64.Vale.Xmms.sel",
        "typing_tok_X64.Machine_s.Public@tok",
        "typing_tok_X64.Machine_s.Rax@tok", "unit_typing"
      ],
      0,
      "d5bb659832575c8b68130ae19a096e38"
    ],
    [
      "X64.Vale.InsAes.va_wpMonotone_AESNI_imc",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_X64.Vale.InsAes.va_wp_AESNI_imc",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_operand_xmm", "unit_typing"
      ],
      0,
      "90d6c59e39a75fc0dbe3ee4c54238be5"
    ],
    [
      "X64.Vale.InsAes.va_wpCompute_AESNI_imc",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.InsAes.va_code_AESNI_imc",
        "equation_X64.Vale.InsAes.va_wp_AESNI_imc",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "refinement_interpretation_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
      ],
      0,
      "b601b47b9ca440d10fc60c2476ceee85"
    ],
    [
      "X64.Vale.InsAes.va_wpProof_AESNI_imc",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "d943c15bf2347dbd7b183c28e9b67cf2"
    ],
    [
      "X64.Vale.InsAes.va_wpProof_AESNI_imc",
      2,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
        "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "X64.Vale.QuickCode_pretyping_5ef17715065c7f9c7618e13aa923e84c",
        "bool_inversion", "constructor_distinct_Prims.Nil",
        "constructor_distinct_X64.Vale.QuickCode.Mod_xmm",
        "data_typing_intro_Prims.Nil@tok", "eq2-interp",
        "equality_tok_X64.Vale.QuickCode.Mod_None@tok", "equation_Prims.nat",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_fuel",
        "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_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.InsAes.va_code_AESNI_imc",
        "equation_X64.Vale.InsAes.va_wpCompute_AESNI_imc",
        "equation_X64.Vale.InsAes.va_wp_AESNI_imc",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.QuickCode.va_mod_xmm",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_with_fuel_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "kinding_X64.Vale.QuickCode.mod_t@tok",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.StateLemmas.lemma_to_flags",
        "lemma_X64.Vale.StateLemmas.lemma_to_ok",
        "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_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_X64.Vale.QuickCode.Mod_xmm__0",
        "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_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.Vale.InsAes.va_wpCompute_AESNI_imc",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "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.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Vale.QuickCode.Mod_None@tok", "unit_typing"
      ],
      0,
      "6ce4bd07947ba29f82519882658f5265"
    ],
    [
      "X64.Vale.InsAes.va_lemma_AESNI_keygen_assist",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_X64.Machine_s.imm8",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_X64.Machine_s_Tm_refine_ed0c82b529ba35f1d88d0cb19afaf666"
      ],
      0,
      "051e5fe7336797497cacab0e0a96b205"
    ],
    [
      "X64.Vale.InsAes.va_lemma_AESNI_keygen_assist",
      2,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
        "@fuel_correspondence_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
        "@query",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
        "Prims_interpretation_Tm_arrow_e06752ba152f81447b312efcdf8f0e23",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "X64.Bytes_Semantics_s_interpretation_Tm_arrow_17742a16dc7ea8ebf4db7d06d09f33c0",
        "X64.Bytes_Semantics_s_interpretation_Tm_arrow_ee7017858cc0d7eacce54d227f2089c3",
        "X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
        "X64.Machine_s_interpretation_Tm_arrow_196f8dfca6d67b0bd046e19b6a5a08e6",
        "X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
        "X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit",
        "constructor_distinct_X64.Bytes_Semantics_s.AESNI_keygen_assist",
        "constructor_distinct_X64.Machine_s.Ins",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_X64.Bytes_Semantics_s.AESNI_keygen_assist@tok",
        "data_typing_intro_X64.Taint_Semantics_s.TaintedIns@tok",
        "disc_equation_X64.Bytes_Semantics_s.MOVDQU",
        "disc_equation_X64.Bytes_Semantics_s.Mulx64",
        "disc_equation_X64.Bytes_Semantics_s.Push",
        "disc_equation_X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_X64.Machine_s.Public@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.on_dom",
        "equation_FStar.List.Tot.Base.op_At",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Types_s.quad32",
        "equation_Words_s.nat32", "equation_Words_s.nat64",
        "equation_Words_s.nat8", "equation_X64.Bytes_Semantics_s.eval_ins",
        "equation_X64.Bytes_Semantics_s.update_xmm",
        "equation_X64.Bytes_Semantics_s.update_xmm_",
        "equation_X64.Machine_s.xmm", "equation_X64.Memory.memtaint",
        "equation_X64.Taint_Semantics_s.extract_operands",
        "equation_X64.Taint_Semantics_s.ins_obs",
        "equation_X64.Taint_Semantics_s.taint_eval_ins",
        "equation_X64.Taint_Semantics_s.tainted_code",
        "equation_X64.Vale.Decls.eval_code", "equation_X64.Vale.Decls.ins",
        "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_fuel",
        "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_ok",
        "equation_X64.Vale.InsAes.va_code_AESNI_keygen_assist",
        "equation_X64.Vale.InsAes.va_transparent_code_AESNI_keygen_assist",
        "equation_X64.Vale.Lemmas.eval_code",
        "equation_X64.Vale.Lemmas.eval_ins",
        "equation_X64.Vale.Lemmas.state_eq_S",
        "equation_X64.Vale.Lemmas.state_eq_opt",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_X64.Vale.StateLemmas.state_of_S",
        "equation_X64.Vale.StateLemmas.state_to_S",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
        "equation_with_fuel_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
        "fuel_guarded_inversion_X64.Bytes_Semantics_s.state",
        "fuel_guarded_inversion_X64.Taint_Semantics_s.traceState",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.unit",
        "function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
        "function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
        "int_inversion",
        "interpretation_Tm_abs_1861e1dfbce217b81baf39da7dbe5796",
        "interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
        "interpretation_Tm_abs_42310e55d108cbfc007dbdda1648048e",
        "interpretation_Tm_abs_4a1a6682764b8be475443da6650b9908",
        "interpretation_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
        "interpretation_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
        "interpretation_Tm_abs_903982188305b836297ca9b101a106e0",
        "interpretation_Tm_abs_d2269df42a02340ac68914c195104ae6",
        "kinding_X64.Bytes_Semantics_s.state@tok",
        "kinding_X64.Machine_s.observation@tok",
        "kinding_X64.Machine_s.operand@tok", "kinding_X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_FStar.List.Tot.Properties.append_l_nil",
        "lemma_X64.Memory_Sems.get_hs_heap",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.StateLemmas.lemma_to_flags",
        "lemma_X64.Vale.StateLemmas.lemma_to_memTaint",
        "lemma_X64.Vale.StateLemmas.lemma_to_ok",
        "lemma_X64.Vale.StateLemmas.lemma_to_reg",
        "lemma_X64.Vale.StateLemmas.lemma_to_trace",
        "lemma_X64.Vale.StateLemmas.lemma_to_xmm",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_upd_eq",
        "lemma_X64.Vale.Xmms.lemma_upd_ne", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_flags",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
        "proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
        "proj_equation_X64.Taint_Semantics_s.MktraceState_state",
        "proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
        "proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
        "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_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Some_v",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_X64.Bytes_Semantics_s.AESNI_keygen_assist__2",
        "projection_inverse_X64.Bytes_Semantics_s.AESNI_keygen_assist_dst",
        "projection_inverse_X64.Bytes_Semantics_s.AESNI_keygen_assist_src",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
        "projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
        "projection_inverse_X64.Machine_s.Ins_ins",
        "projection_inverse_X64.Machine_s.Ins_t_ins",
        "projection_inverse_X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
        "projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
        "projection_inverse_X64.Taint_Semantics_s.TaintedIns_i",
        "projection_inverse_X64.Taint_Semantics_s.TaintedIns_t",
        "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_2c90c44e0c3d494a57f4a23c91ef834a",
        "refinement_interpretation_Tm_refine_33d3ef68371378c171a37d999106817a",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
        "token_correspondence_X64.Bytes_Semantics_s.update_xmm",
        "typing_FStar.Pervasives.Native.snd",
        "typing_Tm_abs_1861e1dfbce217b81baf39da7dbe5796",
        "typing_Tm_abs_4a1a6682764b8be475443da6650b9908",
        "typing_Tm_abs_5ddf544b15726955644c2e2b7b9e7d8e",
        "typing_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
        "typing_Tm_abs_91d6891d766466e9703afb13e7f1a1bf",
        "typing_X64.CPU_Features_s.aesni_enabled",
        "typing_X64.Machine_s.xmm",
        "typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
        "typing_X64.Taint_Semantics_s.ins_obs",
        "typing_X64.Taint_Semantics_s.operand_obs_list",
        "typing_X64.Taint_Semantics_s.taint_eval_ins",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.InsAes.va_transparent_code_AESNI_keygen_assist",
        "typing_X64.Vale.Regs.of_fun",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "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_X64.Vale.State.update_xmm",
        "typing_X64.Vale.StateLemmas.state_to_S", "typing_X64.Vale.Xmms.sel",
        "typing_tok_X64.Machine_s.Public@tok",
        "typing_tok_X64.Machine_s.Rax@tok", "unit_typing"
      ],
      0,
      "811ffeed7d9666d231a16234a30bd9f8"
    ],
    [
      "X64.Vale.InsAes.va_wp_AESNI_keygen_assist",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_X64.Machine_s.imm8",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_X64.Machine_s_Tm_refine_ed0c82b529ba35f1d88d0cb19afaf666"
      ],
      0,
      "138bae5ef6bb7e509cca5d345ce3bd01"
    ],
    [
      "X64.Vale.InsAes.va_wpMonotone_AESNI_keygen_assist",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_X64.Vale.InsAes.va_wp_AESNI_keygen_assist",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_operand_xmm", "unit_typing"
      ],
      0,
      "8d4ed6139740cb8c17a4b57af02d9502"
    ],
    [
      "X64.Vale.InsAes.va_wpCompute_AESNI_keygen_assist",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.Machine_s.imm8", "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.ins", "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.InsAes.va_code_AESNI_keygen_assist",
        "equation_X64.Vale.InsAes.va_wp_AESNI_keygen_assist",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "refinement_interpretation_X64.Machine_s_Tm_refine_ed0c82b529ba35f1d88d0cb19afaf666",
        "refinement_interpretation_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
      ],
      0,
      "05f67bb50ff9ea3b14d632f4f896798d"
    ],
    [
      "X64.Vale.InsAes.va_wpProof_AESNI_keygen_assist",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "875c5f48cb15604faeaf5594d8a4ca48"
    ],
    [
      "X64.Vale.InsAes.va_wpProof_AESNI_keygen_assist",
      2,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
        "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "X64.Vale.QuickCode_pretyping_5ef17715065c7f9c7618e13aa923e84c",
        "bool_inversion", "constructor_distinct_Prims.Nil",
        "constructor_distinct_X64.Vale.QuickCode.Mod_xmm",
        "data_typing_intro_Prims.Nil@tok", "eq2-interp",
        "equality_tok_X64.Vale.QuickCode.Mod_None@tok", "equation_Prims.nat",
        "equation_X64.Machine_s.imm8", "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.ins", "equation_X64.Vale.Decls.ocmp",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_fuel",
        "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_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.InsAes.va_code_AESNI_keygen_assist",
        "equation_X64.Vale.InsAes.va_wpCompute_AESNI_keygen_assist",
        "equation_X64.Vale.InsAes.va_wp_AESNI_keygen_assist",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.QuickCode.va_mod_xmm",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_with_fuel_X64.Vale.QuickCode.update_state_mods.fuel_instrumented",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "kinding_X64.Vale.QuickCode.mod_t@tok",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.StateLemmas.lemma_to_flags",
        "lemma_X64.Vale.StateLemmas.lemma_to_ok",
        "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_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_X64.Vale.QuickCode.Mod_xmm__0",
        "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_X64.Machine_s_Tm_refine_ed0c82b529ba35f1d88d0cb19afaf666",
        "refinement_interpretation_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.Vale.InsAes.va_wpCompute_AESNI_keygen_assist",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "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.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Vale.QuickCode.Mod_None@tok", "unit_typing"
      ],
      0,
      "287aedb1b6e0499e3e474f54bee0063c"
    ]
  ]
]