[
  "1)\u0012)‹\rÝ`‰F‰¿íµI™",
  [
    [
      "Vale.X64.InsAes.va_code_Pclmulqdq",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "02b7481f28c5dc071081c8950b18499b"
    ],
    [
      "Vale.X64.InsAes.va_lemma_Pclmulqdq",
      1,
      4,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
        "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
        "Prims_pretyping_3862c4e8ff39bfc3871b6a47e7ff5b2e",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Instruction_s_pretyping_3f42fef2c19ae51071f07b756c9d8230",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_2eb22b38a6da10fb966327d892d8131d",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_798f93baee047c0793beddf8ae4ab551",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_9771d1081f8bb9d91c468417b1b9cba8",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_b72d599fc3c0eb1fc86c5d80a692be46",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_eabe638ef4af4b0ec65b4cf7bbb2dc65",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
        "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
        "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_FStar.Pervasives.Native.None",
        "constructor_distinct_FStar.Pervasives.Native.Some",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "constructor_distinct_Vale.X64.Instruction_s.IOpXmm",
        "constructor_distinct_Vale.X64.Instruction_s.InOut",
        "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
        "constructor_distinct_Vale.X64.Machine_Semantics_s.AnnotateNone",
        "constructor_distinct_Vale.X64.Machine_s.Ins",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "data_elim_FStar.Pervasives.Native.Mktuple2",
        "data_elim_FStar.Pervasives.Native.Some",
        "data_elim_Vale.Def.Words_s.Mkfour",
        "data_elim_Vale.X64.Bytes_Code_s.Instr",
        "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
        "data_elim_Vale.X64.Machine_s.Ins",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.Def.Words_s.Mktwo@tok",
        "data_typing_intro_Vale.X64.Instruction_s.InstrTypeRecord@tok",
        "data_typing_intro_Vale.X64.Machine_Semantics_s.AnnotateNone@tok",
        "data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "disc_equation_Vale.X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "equality_tok_Vale.X64.Instruction_s.InOut@tok",
        "equality_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.is_restricted",
        "equation_FStar.FunctionalExtensionality.restricted_t",
        "equation_FStar.Option.mapTot",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Arch.Types.quad32_double_hi",
        "equation_Vale.Arch.Types.quad32_double_lo",
        "equation_Vale.Def.Types_s.double32",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Four_s.four_to_two_two",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Instruction_s.arrow",
        "equation_Vale.X64.Instruction_s.instr_dep",
        "equation_Vale.X64.Instruction_s.instr_eval_t",
        "equation_Vale.X64.Instruction_s.instr_operand_t",
        "equation_Vale.X64.Instruction_s.instr_out",
        "equation_Vale.X64.Instruction_s.instr_val_t",
        "equation_Vale.X64.Instructions_s.eval_Pclmulqdq",
        "equation_Vale.X64.Lemmas.core_state",
        "equation_Vale.X64.Lemmas.eval_code",
        "equation_Vale.X64.Lemmas.eval_ins",
        "equation_Vale.X64.Lemmas.state_eq_S",
        "equation_Vale.X64.Lemmas.state_eq_opt",
        "equation_Vale.X64.Machine_Semantics_s.apply_option",
        "equation_Vale.X64.Machine_Semantics_s.bind_option",
        "equation_Vale.X64.Machine_Semantics_s.code",
        "equation_Vale.X64.Machine_Semantics_s.eval_instr",
        "equation_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "equation_Vale.X64.Machine_Semantics_s.flags_t",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ins_obs",
        "equation_Vale.X64.Machine_Semantics_s.instr_apply_eval",
        "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Machine_Semantics_s.operand_obs128",
        "equation_Vale.X64.Machine_Semantics_s.regs_t",
        "equation_Vale.X64.Machine_Semantics_s.st",
        "equation_Vale.X64.Machine_Semantics_s.state_or_fail",
        "equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_xmm_",
        "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
        "equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.operand128",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.memtaint",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Regs.regs_fun", "equation_Vale.X64.Regs.to_fun",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "equation_Vale.X64.StateLemmas.machine_state_eq",
        "equation_Vale.X64.StateLemmas.state_of_S",
        "equation_Vale.X64.StateLemmas.state_to_S",
        "equation_Vale.X64.Taint_Semantics.mk_ins",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.option",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
        "fuel_guarded_inversion_Vale.X64.Machine_s.reg",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.X64.Instruction_s.instr_out",
        "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "function_token_typing_Vale.X64.Machine_Semantics_s.apply_option",
        "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "function_token_typing_Vale.X64.Machine_s.t_reg",
        "function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
        "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
        "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "interpretation_Tm_abs_750cd84c19d6021329e09e972ff18351",
        "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
        "interpretation_Tm_abs_c7148522b68166228dab1bc5afbb5dd9",
        "interpretation_Tm_abs_d7e539669515a49f97544a169303f779",
        "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
        "kinding_Vale.X64.Machine_s.observation@tok",
        "kinding_Vale.X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.extensionality",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_upd_eq",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Stack_Sems.lemma_stack_from_to",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_Vale.Def.Words_s.Mktwo_hi",
        "proj_equation_Vale.Def.Words_s.Mktwo_lo",
        "proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_args",
        "proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_outs",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_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.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "projection_inverse_Vale.Def.Words_s.Mktwo_hi",
        "projection_inverse_Vale.Def.Words_s.Mktwo_lo",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
        "projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_havoc_flags",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_i",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "projection_inverse_Vale.X64.Machine_s.Ins_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.Machine_s.OReg_tc",
        "projection_inverse_Vale.X64.Machine_s.OReg_tr",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_455c88c400de1df6e8dcaa61565e84f9",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "token_correspondence_Vale.X64.Instructions_s.eval_Pclmulqdq",
        "token_correspondence_Vale.X64.Machine_Semantics_s.apply_option",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_s.t_reg",
        "typing_FStar.FunctionalExtensionality.on_domain",
        "typing_FStar.Pervasives.Native.snd",
        "typing_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
        "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "typing_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Math.Poly2.Bits_s.of_double32",
        "typing_Vale.Math.Poly2.Bits_s.to_quad32",
        "typing_Vale.Math.Poly2_s.mul",
        "typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Flags.to_fun",
        "typing_Vale.X64.InsAes.va_code_Pclmulqdq",
        "typing_Vale.X64.Instruction_s.__proj__InstrTypeRecord__item__args",
        "typing_Vale.X64.Instruction_s.__proj__InstrTypeRecord__item__outs",
        "typing_Vale.X64.Instruction_s.instr_eval",
        "typing_Vale.X64.Instruction_s.instr_operand_t",
        "typing_Vale.X64.Instruction_s.instr_operands_t",
        "typing_Vale.X64.Instructions_s.ins_Pclmulqdq",
        "typing_Vale.X64.Lemmas.code_modifies_ghost",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "typing_Vale.X64.Machine_Semantics_s.eval_instr",
        "typing_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "typing_Vale.X64.Machine_Semantics_s.instr_apply_eval",
        "typing_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts",
        "typing_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
        "typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "typing_Vale.X64.Machine_Semantics_s.machine_eval_code",
        "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "typing_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "typing_Vale.X64.Machine_s.operand128",
        "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.Regs.to_fun",
        "typing_Vale.X64.Stack_Sems.stack_to_s",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint",
        "typing_Vale.X64.State.update_reg",
        "typing_Vale.X64.State.update_reg_xmm",
        "typing_Vale.X64.StateLemmas.state_to_S",
        "typing_Vale.X64.Taint_Semantics.mk_ins",
        "typing_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
        "unit_inversion", "unit_typing"
      ],
      0,
      "998ed0d6e065946c5c4586dfcb5fd8fb"
    ],
    [
      "Vale.X64.InsAes.va_wpProof_Pclmulqdq",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_irrelevance_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
        "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
        "bool_inversion", "constructor_distinct_Prims.Nil",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_None@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_flags@tok",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.InsAes.va_wp_Pclmulqdq",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_0cca64a22b1f3bf8ab48b065fb4888e2",
        "interpretation_Tm_abs_9c486cf5a211320d36ff7b240d03b67f",
        "kinding_Vale.X64.QuickCode.mod_t@tok",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "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_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.QuickCode.update_state_mods",
        "typing_Vale.X64.QuickCode.va_mod_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.X64.QuickCode.Mod_None@tok",
        "typing_tok_Vale.X64.QuickCode.Mod_flags@tok", "unit_typing"
      ],
      0,
      "3bc9fa2a28693f477b20b8fc009ae3de"
    ],
    [
      "Vale.X64.InsAes.va_quick_Pclmulqdq",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "f34906f99fa780af6a9e72c9e8c9860b"
    ],
    [
      "Vale.X64.InsAes.va_code_VPclmulqdq",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "49664f03927b8d2ee9eb0dd815f05217"
    ],
    [
      "Vale.X64.InsAes.va_lemma_VPclmulqdq",
      1,
      4,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
        "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
        "Prims_pretyping_3862c4e8ff39bfc3871b6a47e7ff5b2e",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Instruction_s_pretyping_3f42fef2c19ae51071f07b756c9d8230",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_2eb22b38a6da10fb966327d892d8131d",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_798f93baee047c0793beddf8ae4ab551",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_9771d1081f8bb9d91c468417b1b9cba8",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_b72d599fc3c0eb1fc86c5d80a692be46",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_eabe638ef4af4b0ec65b4cf7bbb2dc65",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
        "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
        "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
        "bool_inversion", "bool_typing",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_FStar.Pervasives.Native.None",
        "constructor_distinct_FStar.Pervasives.Native.Some",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "constructor_distinct_Prims.list", "constructor_distinct_Prims.unit",
        "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "constructor_distinct_Vale.X64.Instruction_s.IOpXmm",
        "constructor_distinct_Vale.X64.Instruction_s.Out",
        "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
        "constructor_distinct_Vale.X64.Machine_Semantics_s.AnnotateNone",
        "constructor_distinct_Vale.X64.Machine_s.Ins",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "data_elim_FStar.Pervasives.Native.Mktuple2",
        "data_elim_FStar.Pervasives.Native.Some", "data_elim_Prims.Cons",
        "data_elim_Vale.Def.Words_s.Mkfour",
        "data_elim_Vale.X64.Bytes_Code_s.Instr",
        "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
        "data_elim_Vale.X64.Machine_s.Ins",
        "data_elim_Vale.X64.Machine_s.Reg",
        "data_elim_Vale.X64.State.Mkvale_state",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.Def.Words_s.Mktwo@tok",
        "data_typing_intro_Vale.X64.Instruction_s.InstrTypeRecord@tok",
        "data_typing_intro_Vale.X64.Machine_Semantics_s.AnnotateNone@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "disc_equation_Vale.X64.Machine_s.Ins",
        "equality_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "equality_tok_Vale.X64.Instruction_s.Out@tok",
        "equality_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.restricted_t",
        "equation_FStar.Option.mapTot",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Arch.Types.quad32_double_hi",
        "equation_Vale.Arch.Types.quad32_double_lo",
        "equation_Vale.Def.Types_s.double32",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Four_s.four_to_two_two",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Instruction_s.arrow",
        "equation_Vale.X64.Instruction_s.instr_dep",
        "equation_Vale.X64.Instruction_s.instr_eval_t",
        "equation_Vale.X64.Instruction_s.instr_operand_t",
        "equation_Vale.X64.Instruction_s.instr_out",
        "equation_Vale.X64.Instruction_s.instr_val_t",
        "equation_Vale.X64.Instructions_s.check_avx",
        "equation_Vale.X64.Instructions_s.eval_Pclmulqdq",
        "equation_Vale.X64.Instructions_s.eval_VPclmulqdq",
        "equation_Vale.X64.Lemmas.core_state",
        "equation_Vale.X64.Lemmas.eval_code",
        "equation_Vale.X64.Lemmas.eval_ins",
        "equation_Vale.X64.Lemmas.state_eq_S",
        "equation_Vale.X64.Lemmas.state_eq_opt",
        "equation_Vale.X64.Machine_Semantics_s.apply_option",
        "equation_Vale.X64.Machine_Semantics_s.bind_option",
        "equation_Vale.X64.Machine_Semantics_s.code",
        "equation_Vale.X64.Machine_Semantics_s.eval_instr",
        "equation_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ins_obs",
        "equation_Vale.X64.Machine_Semantics_s.instr_apply_eval",
        "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Machine_Semantics_s.operand_obs128",
        "equation_Vale.X64.Machine_Semantics_s.regs_t",
        "equation_Vale.X64.Machine_Semantics_s.st",
        "equation_Vale.X64.Machine_Semantics_s.state_or_fail",
        "equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_xmm_",
        "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
        "equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.operand128",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Regs.regs_fun", "equation_Vale.X64.Regs.to_fun",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "equation_Vale.X64.StateLemmas.machine_state_eq",
        "equation_Vale.X64.StateLemmas.state_of_S",
        "equation_Vale.X64.StateLemmas.state_to_S",
        "equation_Vale.X64.Taint_Semantics.mk_ins",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.option",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "fuel_guarded_inversion_Prims.list",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
        "fuel_guarded_inversion_Vale.X64.Machine_s.reg",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Prims.unit",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.X64.Instruction_s.instr_out",
        "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "function_token_typing_Vale.X64.Machine_Semantics_s.apply_option",
        "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "function_token_typing_Vale.X64.Machine_s.t_reg",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
        "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
        "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
        "interpretation_Tm_abs_d7e539669515a49f97544a169303f779",
        "interpretation_Tm_abs_d7fe487eb29581afc0726a2d517057b2",
        "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e",
        "kinding_Vale.Def.Words_s.four@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
        "kinding_Vale.X64.Machine_s.observation@tok",
        "kinding_Vale.X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_FStar.Pervasives.invertOption",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_upd_eq",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Stack_Sems.lemma_stack_from_to",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_Vale.Def.Words_s.Mktwo_hi",
        "proj_equation_Vale.Def.Words_s.Mktwo_lo",
        "proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_args",
        "proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_outs",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__b",
        "projection_inverse_FStar.Pervasives.Native.Some_a",
        "projection_inverse_FStar.Pervasives.Native.Some_v",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "projection_inverse_Vale.Def.Words_s.Mktwo_hi",
        "projection_inverse_Vale.Def.Words_s.Mktwo_lo",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
        "projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_havoc_flags",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_i",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "projection_inverse_Vale.X64.Machine_s.Ins_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.Machine_s.OReg_tc",
        "projection_inverse_Vale.X64.Machine_s.OReg_tr",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_455c88c400de1df6e8dcaa61565e84f9",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "token_correspondence_Vale.X64.Instructions_s.eval_VPclmulqdq",
        "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "token_correspondence_Vale.X64.Machine_Semantics_s.apply_option",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_s.t_reg",
        "typing_FStar.Pervasives.Native.snd",
        "typing_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
        "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "typing_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Math.Poly2.Bits_s.of_double32",
        "typing_Vale.Math.Poly2.Bits_s.to_quad32",
        "typing_Vale.Math.Poly2_s.mul",
        "typing_Vale.X64.CPU_Features_s.avx_enabled",
        "typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.InsAes.va_code_VPclmulqdq",
        "typing_Vale.X64.Instruction_s.__proj__InstrTypeRecord__item__args",
        "typing_Vale.X64.Instruction_s.__proj__InstrTypeRecord__item__outs",
        "typing_Vale.X64.Instruction_s.instr_eval",
        "typing_Vale.X64.Instruction_s.instr_operand_t",
        "typing_Vale.X64.Instruction_s.instr_operands_t",
        "typing_Vale.X64.Instruction_s.instr_operands_t_args",
        "typing_Vale.X64.Instructions_s.eval_Pclmulqdq",
        "typing_Vale.X64.Instructions_s.ins_VPclmulqdq",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "typing_Vale.X64.Machine_Semantics_s.apply_option",
        "typing_Vale.X64.Machine_Semantics_s.eval_instr",
        "typing_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "typing_Vale.X64.Machine_Semantics_s.instr_apply_eval",
        "typing_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts",
        "typing_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
        "typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "typing_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "typing_Vale.X64.Machine_s.operand128",
        "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.Regs.to_fun",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_Vale.X64.State.update_reg",
        "typing_Vale.X64.StateLemmas.state_to_S",
        "typing_Vale.X64.Taint_Semantics.mk_ins",
        "typing_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
        "unit_inversion", "unit_typing"
      ],
      0,
      "c7455d7bb88922a106cef8db7aea4987"
    ],
    [
      "Vale.X64.InsAes.va_wpProof_VPclmulqdq",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_irrelevance_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
        "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
        "bool_inversion", "constructor_distinct_Prims.Nil",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_None@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_flags@tok",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel", "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.InsAes.va_wp_VPclmulqdq",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_0cca64a22b1f3bf8ab48b065fb4888e2",
        "interpretation_Tm_abs_9c486cf5a211320d36ff7b240d03b67f",
        "kinding_Vale.X64.QuickCode.mod_t@tok",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "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_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.CPU_Features_s.avx_enabled",
        "typing_Vale.X64.QuickCode.update_state_mods",
        "typing_Vale.X64.QuickCode.va_mod_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.X64.QuickCode.Mod_None@tok",
        "typing_tok_Vale.X64.QuickCode.Mod_flags@tok", "unit_typing"
      ],
      0,
      "6fb5c8ced5f446741bd5480bdfc1155e"
    ],
    [
      "Vale.X64.InsAes.va_quick_VPclmulqdq",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "6f05ddd87769a5b9142184aed21bf2df"
    ],
    [
      "Vale.X64.InsAes.va_code_AESNI_enc",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "0185043bb9d1d5d641c6626350e03ba6"
    ],
    [
      "Vale.X64.InsAes.va_lemma_AESNI_enc",
      1,
      4,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
        "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Instructions_s_interpretation_Tm_arrow_8141953f97792aed3f5f72fe104fa09f",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
        "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
        "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
        "bool_inversion",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_FStar.Pervasives.Native.Some",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "constructor_distinct_Vale.X64.Instruction_s.IOpXmm",
        "constructor_distinct_Vale.X64.Instruction_s.InOut",
        "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
        "constructor_distinct_Vale.X64.Machine_Semantics_s.AnnotateNone",
        "constructor_distinct_Vale.X64.Machine_s.Ins",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Instruction_s.IOpEx@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "disc_equation_Vale.X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "equality_tok_Vale.X64.Instruction_s.InOut@tok",
        "equality_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.restricted_t",
        "equation_FStar.Option.mapTot",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Instruction_s.arrow",
        "equation_Vale.X64.Instruction_s.instr_dep",
        "equation_Vale.X64.Instruction_s.instr_operand_t",
        "equation_Vale.X64.Instruction_s.instr_out",
        "equation_Vale.X64.Instruction_s.instr_val_t",
        "equation_Vale.X64.Instructions_s.eval_AESNI_enc",
        "equation_Vale.X64.Lemmas.eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.apply_option",
        "equation_Vale.X64.Machine_Semantics_s.bind_option",
        "equation_Vale.X64.Machine_Semantics_s.code",
        "equation_Vale.X64.Machine_Semantics_s.eval_instr",
        "equation_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ins_obs",
        "equation_Vale.X64.Machine_Semantics_s.instr_apply_eval",
        "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "equation_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Machine_Semantics_s.operand_obs128",
        "equation_Vale.X64.Machine_Semantics_s.regs_t",
        "equation_Vale.X64.Machine_Semantics_s.state_or_fail",
        "equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_xmm_",
        "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
        "equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.operand128",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "equation_Vale.X64.StateLemmas.state_of_S",
        "equation_Vale.X64.StateLemmas.state_to_S",
        "equation_Vale.X64.Taint_Semantics.mk_ins",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "fuel_guarded_inversion_Vale.X64.Machine_s.reg",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.int",
        "function_token_typing_Prims.unit",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.X64.Instruction_s.instr_out",
        "function_token_typing_Vale.X64.Instructions_s.eval_AESNI_enc",
        "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "function_token_typing_Vale.X64.Machine_s.t_reg",
        "function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_typing",
        "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
        "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
        "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
        "interpretation_Tm_abs_c7148522b68166228dab1bc5afbb5dd9",
        "interpretation_Tm_abs_d7e539669515a49f97544a169303f779",
        "interpretation_Tm_abs_e4dec50f3d049bc1f46ba6e56c0638cc",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
        "kinding_Vale.X64.Machine_s.observation@tok",
        "kinding_Vale.X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_upd_eq",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Stack_Sems.lemma_stack_from_to",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_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.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
        "projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_havoc_flags",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_i",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "projection_inverse_Vale.X64.Machine_s.Ins_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.Machine_s.OReg_tc",
        "projection_inverse_Vale.X64.Machine_s.OReg_tr",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "token_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "token_correspondence_Vale.X64.Instructions_s.eval_AESNI_enc",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_s.t_reg",
        "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "typing_Vale.AES.AES_s.mix_columns_LE",
        "typing_Vale.AES.AES_s.shift_rows_LE",
        "typing_Vale.AES.AES_s.sub_bytes",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Def.Types_s.quad32_xor",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.InsAes.va_code_AESNI_enc",
        "typing_Vale.X64.Instruction_s.instr_eval",
        "typing_Vale.X64.Instructions_s.ins_AESNI_enc",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "typing_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "typing_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "typing_Vale.X64.Machine_s.operand128",
        "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_Vale.X64.State.update_reg_xmm",
        "typing_Vale.X64.StateLemmas.state_to_S",
        "typing_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "typing_tok_Vale.X64.Instruction_s.InOut@tok",
        "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok", "unit_typing"
      ],
      0,
      "db378daa67462a21aded3c0744861f01"
    ],
    [
      "Vale.X64.InsAes.va_wpProof_AESNI_enc",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
        "bool_inversion", "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_None@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_flags@tok",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.InsAes.va_wp_AESNI_enc",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "kinding_Vale.X64.QuickCode.mod_t@tok",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "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_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.QuickCode.update_state_mods",
        "typing_Vale.X64.QuickCode.va_mod_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.X64.QuickCode.Mod_None@tok",
        "typing_tok_Vale.X64.QuickCode.Mod_flags@tok", "unit_typing"
      ],
      0,
      "9ae692a0521f25ca33f202e80ec8cf65"
    ],
    [
      "Vale.X64.InsAes.va_quick_AESNI_enc",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "a253330ea86f446556cfdd3b9f90ce3d"
    ],
    [
      "Vale.X64.InsAes.va_code_VAESNI_enc",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "ed235941795846ef1d661a164d9483c2"
    ],
    [
      "Vale.X64.InsAes.va_lemma_VAESNI_enc",
      1,
      4,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
        "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
        "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
        "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
        "bool_inversion",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_FStar.Pervasives.Native.Some",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "constructor_distinct_Vale.X64.Instruction_s.IOpXmm",
        "constructor_distinct_Vale.X64.Instruction_s.Out",
        "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
        "constructor_distinct_Vale.X64.Machine_Semantics_s.AnnotateNone",
        "constructor_distinct_Vale.X64.Machine_s.Ins",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Instruction_s.IOpEx@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "disc_equation_Vale.X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "equality_tok_Vale.X64.Instruction_s.Out@tok",
        "equality_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.restricted_t",
        "equation_FStar.Option.mapTot",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Instruction_s.arrow",
        "equation_Vale.X64.Instruction_s.instr_dep",
        "equation_Vale.X64.Instruction_s.instr_operand_t",
        "equation_Vale.X64.Instruction_s.instr_out",
        "equation_Vale.X64.Instruction_s.instr_val_t",
        "equation_Vale.X64.Instructions_s.check_avx",
        "equation_Vale.X64.Instructions_s.eval_AESNI_enc",
        "equation_Vale.X64.Instructions_s.eval_VAESNI_enc",
        "equation_Vale.X64.Lemmas.eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.apply_option",
        "equation_Vale.X64.Machine_Semantics_s.bind_option",
        "equation_Vale.X64.Machine_Semantics_s.code",
        "equation_Vale.X64.Machine_Semantics_s.eval_instr",
        "equation_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ins_obs",
        "equation_Vale.X64.Machine_Semantics_s.instr_apply_eval",
        "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Machine_Semantics_s.operand_obs128",
        "equation_Vale.X64.Machine_Semantics_s.regs_t",
        "equation_Vale.X64.Machine_Semantics_s.state_or_fail",
        "equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_xmm_",
        "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
        "equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.operand128",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "equation_Vale.X64.StateLemmas.state_of_S",
        "equation_Vale.X64.StateLemmas.state_to_S",
        "equation_Vale.X64.Taint_Semantics.mk_ins",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "fuel_guarded_inversion_Vale.X64.Machine_s.reg",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.int",
        "function_token_typing_Prims.unit",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.X64.Instruction_s.instr_out",
        "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "function_token_typing_Vale.X64.Machine_s.t_reg",
        "function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_typing",
        "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
        "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "interpretation_Tm_abs_a391ea95f87f233dec95562a158a12df",
        "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
        "interpretation_Tm_abs_d7e539669515a49f97544a169303f779",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
        "kinding_Vale.X64.Machine_s.observation@tok",
        "kinding_Vale.X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_upd_eq",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Stack_Sems.lemma_stack_from_to",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_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.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
        "projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_havoc_flags",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_i",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "projection_inverse_Vale.X64.Machine_s.Ins_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.Machine_s.OReg_tc",
        "projection_inverse_Vale.X64.Machine_s.OReg_tr",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "token_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "token_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "token_correspondence_Vale.X64.Instructions_s.eval_VAESNI_enc",
        "token_correspondence_Vale.X64.Machine_Semantics_s.apply_option",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_s.t_reg",
        "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "typing_Vale.AES.AES_s.mix_columns_LE",
        "typing_Vale.AES.AES_s.shift_rows_LE",
        "typing_Vale.AES.AES_s.sub_bytes",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Def.Types_s.quad32_xor",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.CPU_Features_s.avx_enabled",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.InsAes.va_code_VAESNI_enc",
        "typing_Vale.X64.Instruction_s.instr_eval",
        "typing_Vale.X64.Instructions_s.eval_AESNI_enc",
        "typing_Vale.X64.Instructions_s.ins_VAESNI_enc",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "typing_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "typing_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "typing_Vale.X64.Machine_s.operand128",
        "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_Vale.X64.State.update_reg_xmm",
        "typing_Vale.X64.StateLemmas.state_to_S",
        "typing_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "typing_tok_Vale.X64.Instruction_s.Out@tok",
        "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok", "unit_typing"
      ],
      0,
      "6c1cce7243e304f6d4c763593be77020"
    ],
    [
      "Vale.X64.InsAes.va_wpProof_VAESNI_enc",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
        "bool_inversion", "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_None@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_flags@tok",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.InsAes.va_wp_VAESNI_enc",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "kinding_Vale.X64.QuickCode.mod_t@tok",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "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_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.CPU_Features_s.avx_enabled",
        "typing_Vale.X64.QuickCode.update_state_mods",
        "typing_Vale.X64.QuickCode.va_mod_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.X64.QuickCode.Mod_None@tok",
        "typing_tok_Vale.X64.QuickCode.Mod_flags@tok", "unit_typing"
      ],
      0,
      "f773e49463761bc53eb080691238aad9"
    ],
    [
      "Vale.X64.InsAes.va_quick_VAESNI_enc",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "b3e336eda03a03f4827f179fa320a9d9"
    ],
    [
      "Vale.X64.InsAes.va_code_AESNI_enc_last",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "ff38309d7791ff107caa5277b519967d"
    ],
    [
      "Vale.X64.InsAes.va_lemma_AESNI_enc_last",
      1,
      4,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
        "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Instructions_s_interpretation_Tm_arrow_8141953f97792aed3f5f72fe104fa09f",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
        "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
        "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
        "bool_inversion",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_FStar.Pervasives.Native.Some",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "constructor_distinct_Vale.X64.Instruction_s.IOpXmm",
        "constructor_distinct_Vale.X64.Instruction_s.InOut",
        "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
        "constructor_distinct_Vale.X64.Machine_Semantics_s.AnnotateNone",
        "constructor_distinct_Vale.X64.Machine_s.Ins",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Instruction_s.IOpEx@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "disc_equation_Vale.X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "equality_tok_Vale.X64.Instruction_s.InOut@tok",
        "equality_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.restricted_t",
        "equation_FStar.Option.mapTot",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Instruction_s.arrow",
        "equation_Vale.X64.Instruction_s.instr_dep",
        "equation_Vale.X64.Instruction_s.instr_operand_t",
        "equation_Vale.X64.Instruction_s.instr_out",
        "equation_Vale.X64.Instruction_s.instr_val_t",
        "equation_Vale.X64.Instructions_s.eval_AESNI_enc_last",
        "equation_Vale.X64.Lemmas.eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.apply_option",
        "equation_Vale.X64.Machine_Semantics_s.bind_option",
        "equation_Vale.X64.Machine_Semantics_s.code",
        "equation_Vale.X64.Machine_Semantics_s.eval_instr",
        "equation_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ins_obs",
        "equation_Vale.X64.Machine_Semantics_s.instr_apply_eval",
        "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "equation_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Machine_Semantics_s.operand_obs128",
        "equation_Vale.X64.Machine_Semantics_s.regs_t",
        "equation_Vale.X64.Machine_Semantics_s.state_or_fail",
        "equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_xmm_",
        "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
        "equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.operand128",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "equation_Vale.X64.StateLemmas.state_of_S",
        "equation_Vale.X64.StateLemmas.state_to_S",
        "equation_Vale.X64.Taint_Semantics.mk_ins",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "fuel_guarded_inversion_Vale.X64.Machine_s.reg",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.int",
        "function_token_typing_Prims.unit",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.X64.Instruction_s.instr_out",
        "function_token_typing_Vale.X64.Instructions_s.eval_AESNI_enc_last",
        "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "function_token_typing_Vale.X64.Machine_s.t_reg",
        "function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_typing",
        "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
        "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
        "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
        "interpretation_Tm_abs_c7148522b68166228dab1bc5afbb5dd9",
        "interpretation_Tm_abs_c8a4c720a2702f361d687f8fcc3f55c9",
        "interpretation_Tm_abs_d7e539669515a49f97544a169303f779",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
        "kinding_Vale.X64.Machine_s.observation@tok",
        "kinding_Vale.X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_upd_eq",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Stack_Sems.lemma_stack_from_to",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_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.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
        "projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_havoc_flags",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_i",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "projection_inverse_Vale.X64.Machine_s.Ins_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.Machine_s.OReg_tc",
        "projection_inverse_Vale.X64.Machine_s.OReg_tr",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "token_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "token_correspondence_Vale.X64.Instructions_s.eval_AESNI_enc_last",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_s.t_reg",
        "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "typing_Vale.AES.AES_s.shift_rows_LE",
        "typing_Vale.AES.AES_s.sub_bytes",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Def.Types_s.quad32_xor",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.InsAes.va_code_AESNI_enc_last",
        "typing_Vale.X64.Instruction_s.instr_eval",
        "typing_Vale.X64.Instructions_s.ins_AESNI_enc_last",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "typing_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "typing_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "typing_Vale.X64.Machine_s.operand128",
        "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_Vale.X64.State.update_reg_xmm",
        "typing_Vale.X64.StateLemmas.state_to_S",
        "typing_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "typing_tok_Vale.X64.Instruction_s.InOut@tok",
        "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok", "unit_typing"
      ],
      0,
      "93ff6724ea6718e3fd4b9629a4b8c414"
    ],
    [
      "Vale.X64.InsAes.va_wpProof_AESNI_enc_last",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
        "bool_inversion", "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_None@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_flags@tok",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.InsAes.va_wp_AESNI_enc_last",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "kinding_Vale.X64.QuickCode.mod_t@tok",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "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_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.QuickCode.update_state_mods",
        "typing_Vale.X64.QuickCode.va_mod_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.X64.QuickCode.Mod_None@tok",
        "typing_tok_Vale.X64.QuickCode.Mod_flags@tok", "unit_typing"
      ],
      0,
      "dc4ebd98788adf4deec62cc501253c0b"
    ],
    [
      "Vale.X64.InsAes.va_quick_AESNI_enc_last",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "6bbce024a17d126b7e95f16beb4892f2"
    ],
    [
      "Vale.X64.InsAes.va_code_VAESNI_enc_last",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "7a75a2a83d649d29dc04adeda597c587"
    ],
    [
      "Vale.X64.InsAes.va_lemma_VAESNI_enc_last",
      1,
      4,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
        "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
        "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
        "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
        "bool_inversion",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_FStar.Pervasives.Native.Some",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "constructor_distinct_Vale.X64.Instruction_s.IOpXmm",
        "constructor_distinct_Vale.X64.Instruction_s.Out",
        "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
        "constructor_distinct_Vale.X64.Machine_Semantics_s.AnnotateNone",
        "constructor_distinct_Vale.X64.Machine_s.Ins",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Instruction_s.IOpEx@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "disc_equation_Vale.X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "equality_tok_Vale.X64.Instruction_s.Out@tok",
        "equality_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.restricted_t",
        "equation_FStar.Option.mapTot",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Instruction_s.arrow",
        "equation_Vale.X64.Instruction_s.instr_dep",
        "equation_Vale.X64.Instruction_s.instr_operand_t",
        "equation_Vale.X64.Instruction_s.instr_out",
        "equation_Vale.X64.Instruction_s.instr_val_t",
        "equation_Vale.X64.Instructions_s.check_avx",
        "equation_Vale.X64.Instructions_s.eval_AESNI_enc_last",
        "equation_Vale.X64.Instructions_s.eval_VAESNI_enc_last",
        "equation_Vale.X64.Lemmas.eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.apply_option",
        "equation_Vale.X64.Machine_Semantics_s.bind_option",
        "equation_Vale.X64.Machine_Semantics_s.code",
        "equation_Vale.X64.Machine_Semantics_s.eval_instr",
        "equation_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ins_obs",
        "equation_Vale.X64.Machine_Semantics_s.instr_apply_eval",
        "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "equation_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Machine_Semantics_s.operand_obs128",
        "equation_Vale.X64.Machine_Semantics_s.regs_t",
        "equation_Vale.X64.Machine_Semantics_s.state_or_fail",
        "equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_xmm_",
        "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
        "equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.operand128",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "equation_Vale.X64.StateLemmas.state_of_S",
        "equation_Vale.X64.StateLemmas.state_to_S",
        "equation_Vale.X64.Taint_Semantics.mk_ins",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "fuel_guarded_inversion_Vale.X64.Machine_s.reg",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.int",
        "function_token_typing_Prims.unit",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.X64.Instruction_s.instr_out",
        "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "function_token_typing_Vale.X64.Machine_s.t_reg",
        "function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_typing",
        "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
        "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
        "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
        "interpretation_Tm_abs_d7e539669515a49f97544a169303f779",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
        "kinding_Vale.X64.Machine_s.observation@tok",
        "kinding_Vale.X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_upd_eq",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Stack_Sems.lemma_stack_from_to",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_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.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
        "projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_havoc_flags",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_i",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "projection_inverse_Vale.X64.Machine_s.Ins_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.Machine_s.OReg_tc",
        "projection_inverse_Vale.X64.Machine_s.OReg_tr",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "token_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "token_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "token_correspondence_Vale.X64.Instructions_s.eval_VAESNI_enc_last",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_s.t_reg",
        "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "typing_Vale.AES.AES_s.shift_rows_LE",
        "typing_Vale.AES.AES_s.sub_bytes",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Def.Types_s.quad32_xor",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.CPU_Features_s.avx_enabled",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.InsAes.va_code_VAESNI_enc_last",
        "typing_Vale.X64.Instruction_s.instr_eval",
        "typing_Vale.X64.Instructions_s.eval_AESNI_enc_last",
        "typing_Vale.X64.Instructions_s.ins_VAESNI_enc_last",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "typing_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "typing_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "typing_Vale.X64.Machine_s.operand128",
        "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_Vale.X64.State.update_reg_xmm",
        "typing_Vale.X64.StateLemmas.state_to_S",
        "typing_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "typing_tok_Vale.X64.Instruction_s.Out@tok",
        "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok", "unit_typing"
      ],
      0,
      "aa0bf4016775d7eafab7c74f829ad4c6"
    ],
    [
      "Vale.X64.InsAes.va_wpProof_VAESNI_enc_last",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
        "bool_inversion", "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_None@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_flags@tok",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.InsAes.va_wp_VAESNI_enc_last",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "kinding_Vale.X64.QuickCode.mod_t@tok",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "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_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.CPU_Features_s.avx_enabled",
        "typing_Vale.X64.QuickCode.update_state_mods",
        "typing_Vale.X64.QuickCode.va_mod_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.X64.QuickCode.Mod_None@tok",
        "typing_tok_Vale.X64.QuickCode.Mod_flags@tok", "unit_typing"
      ],
      0,
      "e22e98433d03c5ca316bc0cc128c37f8"
    ],
    [
      "Vale.X64.InsAes.va_quick_VAESNI_enc_last",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "f63884fd6e6359ab4dee4c80fdb4bf3c"
    ],
    [
      "Vale.X64.InsAes.va_code_AESNI_dec",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "73efc866a43b328da7885aefa46564df"
    ],
    [
      "Vale.X64.InsAes.va_lemma_AESNI_dec",
      1,
      4,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
        "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Instructions_s_interpretation_Tm_arrow_8141953f97792aed3f5f72fe104fa09f",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
        "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
        "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
        "bool_inversion",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_FStar.Pervasives.Native.Some",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "constructor_distinct_Vale.X64.Instruction_s.IOpXmm",
        "constructor_distinct_Vale.X64.Instruction_s.InOut",
        "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
        "constructor_distinct_Vale.X64.Machine_Semantics_s.AnnotateNone",
        "constructor_distinct_Vale.X64.Machine_s.Ins",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Instruction_s.IOpEx@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "disc_equation_Vale.X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "equality_tok_Vale.X64.Instruction_s.InOut@tok",
        "equality_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.restricted_t",
        "equation_FStar.Option.mapTot",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Instruction_s.arrow",
        "equation_Vale.X64.Instruction_s.instr_dep",
        "equation_Vale.X64.Instruction_s.instr_operand_t",
        "equation_Vale.X64.Instruction_s.instr_out",
        "equation_Vale.X64.Instruction_s.instr_val_t",
        "equation_Vale.X64.Instructions_s.eval_AESNI_dec",
        "equation_Vale.X64.Lemmas.eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.apply_option",
        "equation_Vale.X64.Machine_Semantics_s.bind_option",
        "equation_Vale.X64.Machine_Semantics_s.code",
        "equation_Vale.X64.Machine_Semantics_s.eval_instr",
        "equation_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ins_obs",
        "equation_Vale.X64.Machine_Semantics_s.instr_apply_eval",
        "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "equation_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Machine_Semantics_s.operand_obs128",
        "equation_Vale.X64.Machine_Semantics_s.regs_t",
        "equation_Vale.X64.Machine_Semantics_s.state_or_fail",
        "equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_xmm_",
        "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
        "equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.operand128",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "equation_Vale.X64.StateLemmas.state_of_S",
        "equation_Vale.X64.StateLemmas.state_to_S",
        "equation_Vale.X64.Taint_Semantics.mk_ins",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "fuel_guarded_inversion_Vale.X64.Machine_s.reg",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.int",
        "function_token_typing_Prims.unit",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.X64.Instruction_s.instr_out",
        "function_token_typing_Vale.X64.Instructions_s.eval_AESNI_dec",
        "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "function_token_typing_Vale.X64.Machine_s.t_reg",
        "function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_typing",
        "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
        "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
        "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "interpretation_Tm_abs_799946e30f28ac0a2472154ea618025d",
        "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
        "interpretation_Tm_abs_c7148522b68166228dab1bc5afbb5dd9",
        "interpretation_Tm_abs_d7e539669515a49f97544a169303f779",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
        "kinding_Vale.X64.Machine_s.observation@tok",
        "kinding_Vale.X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_upd_eq",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Stack_Sems.lemma_stack_from_to",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_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.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
        "projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_havoc_flags",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_i",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "projection_inverse_Vale.X64.Machine_s.Ins_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.Machine_s.OReg_tc",
        "projection_inverse_Vale.X64.Machine_s.OReg_tr",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "token_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "token_correspondence_Vale.X64.Instructions_s.eval_AESNI_dec",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_s.t_reg",
        "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "typing_Vale.AES.AES_s.inv_mix_columns_LE",
        "typing_Vale.AES.AES_s.inv_shift_rows_LE",
        "typing_Vale.AES.AES_s.inv_sub_bytes",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Def.Types_s.quad32_xor",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.InsAes.va_code_AESNI_dec",
        "typing_Vale.X64.Instruction_s.instr_eval",
        "typing_Vale.X64.Instructions_s.ins_AESNI_dec",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "typing_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "typing_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "typing_Vale.X64.Machine_s.operand128",
        "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_Vale.X64.State.update_reg_xmm",
        "typing_Vale.X64.StateLemmas.state_to_S",
        "typing_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "typing_tok_Vale.X64.Instruction_s.InOut@tok",
        "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok", "unit_typing"
      ],
      0,
      "90785e8b5356fdebcb0e407b34197962"
    ],
    [
      "Vale.X64.InsAes.va_wpProof_AESNI_dec",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
        "bool_inversion", "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_None@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_flags@tok",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.InsAes.va_wp_AESNI_dec",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "kinding_Vale.X64.QuickCode.mod_t@tok",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "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_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.QuickCode.update_state_mods",
        "typing_Vale.X64.QuickCode.va_mod_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.X64.QuickCode.Mod_None@tok",
        "typing_tok_Vale.X64.QuickCode.Mod_flags@tok", "unit_typing"
      ],
      0,
      "1e678badcca7b1a725d5e567ebb1cf45"
    ],
    [
      "Vale.X64.InsAes.va_quick_AESNI_dec",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "e1274b8d50d754f3e3f772c96e534a62"
    ],
    [
      "Vale.X64.InsAes.va_code_AESNI_dec_last",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "9dcbf18ae9c647b79633463058bf4c39"
    ],
    [
      "Vale.X64.InsAes.va_lemma_AESNI_dec_last",
      1,
      4,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
        "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Instructions_s_interpretation_Tm_arrow_8141953f97792aed3f5f72fe104fa09f",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
        "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
        "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
        "bool_inversion",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_FStar.Pervasives.Native.Some",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "constructor_distinct_Vale.X64.Instruction_s.IOpXmm",
        "constructor_distinct_Vale.X64.Instruction_s.InOut",
        "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
        "constructor_distinct_Vale.X64.Machine_Semantics_s.AnnotateNone",
        "constructor_distinct_Vale.X64.Machine_s.Ins",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Instruction_s.IOpEx@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "disc_equation_Vale.X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "equality_tok_Vale.X64.Instruction_s.InOut@tok",
        "equality_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.restricted_t",
        "equation_FStar.Option.mapTot",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Instruction_s.arrow",
        "equation_Vale.X64.Instruction_s.instr_dep",
        "equation_Vale.X64.Instruction_s.instr_operand_t",
        "equation_Vale.X64.Instruction_s.instr_out",
        "equation_Vale.X64.Instruction_s.instr_val_t",
        "equation_Vale.X64.Instructions_s.eval_AESNI_dec_last",
        "equation_Vale.X64.Lemmas.eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.apply_option",
        "equation_Vale.X64.Machine_Semantics_s.bind_option",
        "equation_Vale.X64.Machine_Semantics_s.code",
        "equation_Vale.X64.Machine_Semantics_s.eval_instr",
        "equation_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ins_obs",
        "equation_Vale.X64.Machine_Semantics_s.instr_apply_eval",
        "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "equation_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Machine_Semantics_s.operand_obs128",
        "equation_Vale.X64.Machine_Semantics_s.regs_t",
        "equation_Vale.X64.Machine_Semantics_s.state_or_fail",
        "equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_xmm_",
        "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
        "equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.operand128",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "equation_Vale.X64.StateLemmas.state_of_S",
        "equation_Vale.X64.StateLemmas.state_to_S",
        "equation_Vale.X64.Taint_Semantics.mk_ins",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "fuel_guarded_inversion_Vale.X64.Machine_s.reg",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.int",
        "function_token_typing_Prims.unit",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.X64.Instruction_s.instr_out",
        "function_token_typing_Vale.X64.Instructions_s.eval_AESNI_dec_last",
        "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "function_token_typing_Vale.X64.Machine_s.t_reg",
        "function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_typing",
        "interpretation_Tm_abs_03b0cee36e99b7f8d51a4e98a0fc6e02",
        "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
        "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
        "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
        "interpretation_Tm_abs_c7148522b68166228dab1bc5afbb5dd9",
        "interpretation_Tm_abs_d7e539669515a49f97544a169303f779",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
        "kinding_Vale.X64.Machine_s.observation@tok",
        "kinding_Vale.X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_upd_eq",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Stack_Sems.lemma_stack_from_to",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_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.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
        "projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_havoc_flags",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_i",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "projection_inverse_Vale.X64.Machine_s.Ins_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.Machine_s.OReg_tc",
        "projection_inverse_Vale.X64.Machine_s.OReg_tr",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "token_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "token_correspondence_Vale.X64.Instructions_s.eval_AESNI_dec_last",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_s.t_reg",
        "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "typing_Vale.AES.AES_s.inv_shift_rows_LE",
        "typing_Vale.AES.AES_s.inv_sub_bytes",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Def.Types_s.quad32_xor",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.InsAes.va_code_AESNI_dec_last",
        "typing_Vale.X64.Instruction_s.instr_eval",
        "typing_Vale.X64.Instructions_s.ins_AESNI_dec_last",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "typing_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "typing_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "typing_Vale.X64.Machine_s.operand128",
        "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_Vale.X64.State.update_reg_xmm",
        "typing_Vale.X64.StateLemmas.state_to_S",
        "typing_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "typing_tok_Vale.X64.Instruction_s.InOut@tok",
        "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok", "unit_typing"
      ],
      0,
      "c4fde59e29a977cc9168b94b2d543ed0"
    ],
    [
      "Vale.X64.InsAes.va_wpProof_AESNI_dec_last",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
        "bool_inversion", "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_None@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_flags@tok",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.InsAes.va_wp_AESNI_dec_last",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "kinding_Vale.X64.QuickCode.mod_t@tok",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "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_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.QuickCode.update_state_mods",
        "typing_Vale.X64.QuickCode.va_mod_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.X64.QuickCode.Mod_None@tok",
        "typing_tok_Vale.X64.QuickCode.Mod_flags@tok", "unit_typing"
      ],
      0,
      "100c033b3b084e0445f553bdbf13c08b"
    ],
    [
      "Vale.X64.InsAes.va_quick_AESNI_dec_last",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "4d4f41d668f427546d2d70cde367e6f1"
    ],
    [
      "Vale.X64.InsAes.va_code_AESNI_imc",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "b154365720cedd22efdf5e48efb8eb83"
    ],
    [
      "Vale.X64.InsAes.va_lemma_AESNI_imc",
      1,
      4,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
        "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Instructions_s_interpretation_Tm_arrow_1ebcbd1b890b1b45a64817c3e275bd2e",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
        "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
        "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
        "bool_inversion",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_FStar.Pervasives.Native.Some",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "constructor_distinct_Vale.X64.Instruction_s.IOpXmm",
        "constructor_distinct_Vale.X64.Instruction_s.Out",
        "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
        "constructor_distinct_Vale.X64.Machine_Semantics_s.AnnotateNone",
        "constructor_distinct_Vale.X64.Machine_s.Ins",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Instruction_s.IOpEx@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "disc_equation_Vale.X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "equality_tok_Vale.X64.Instruction_s.Out@tok",
        "equality_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.restricted_t",
        "equation_FStar.Option.mapTot",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Instruction_s.instr_dep",
        "equation_Vale.X64.Instruction_s.instr_operand_t",
        "equation_Vale.X64.Instruction_s.instr_out",
        "equation_Vale.X64.Instruction_s.instr_val_t",
        "equation_Vale.X64.Instructions_s.eval_AESNI_imc",
        "equation_Vale.X64.Lemmas.eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.apply_option",
        "equation_Vale.X64.Machine_Semantics_s.bind_option",
        "equation_Vale.X64.Machine_Semantics_s.code",
        "equation_Vale.X64.Machine_Semantics_s.eval_instr",
        "equation_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ins_obs",
        "equation_Vale.X64.Machine_Semantics_s.instr_apply_eval",
        "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Machine_Semantics_s.operand_obs128",
        "equation_Vale.X64.Machine_Semantics_s.regs_t",
        "equation_Vale.X64.Machine_Semantics_s.state_or_fail",
        "equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_xmm_",
        "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
        "equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.operand128",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "equation_Vale.X64.StateLemmas.state_of_S",
        "equation_Vale.X64.StateLemmas.state_to_S",
        "equation_Vale.X64.Taint_Semantics.mk_ins",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "fuel_guarded_inversion_Vale.X64.Machine_s.reg",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.int",
        "function_token_typing_Prims.unit",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.X64.Instruction_s.instr_out",
        "function_token_typing_Vale.X64.Instructions_s.eval_AESNI_imc",
        "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "function_token_typing_Vale.X64.Machine_s.t_reg",
        "function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_typing",
        "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
        "interpretation_Tm_abs_378a8cfeb83473cb9cd3333fd4b070c7",
        "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
        "interpretation_Tm_abs_d7e539669515a49f97544a169303f779",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
        "kinding_Vale.X64.Machine_s.observation@tok",
        "kinding_Vale.X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_upd_eq",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Stack_Sems.lemma_stack_from_to",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_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.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
        "projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_havoc_flags",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_i",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "projection_inverse_Vale.X64.Machine_s.Ins_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.Machine_s.OReg_tc",
        "projection_inverse_Vale.X64.Machine_s.OReg_tr",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "token_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "token_correspondence_Vale.X64.Instructions_s.eval_AESNI_imc",
        "token_correspondence_Vale.X64.Machine_Semantics_s.apply_option",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_s.t_reg",
        "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "typing_Vale.AES.AES_s.inv_mix_columns_LE",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.InsAes.va_code_AESNI_imc",
        "typing_Vale.X64.Instruction_s.instr_eval",
        "typing_Vale.X64.Instructions_s.ins_AESNI_imc",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "typing_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "typing_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "typing_Vale.X64.Machine_s.operand128",
        "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_Vale.X64.State.update_reg_xmm",
        "typing_Vale.X64.StateLemmas.state_to_S",
        "typing_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "typing_tok_Vale.X64.Instruction_s.Out@tok",
        "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok", "unit_typing"
      ],
      0,
      "99634884f6f0353eb73696c6c8983336"
    ],
    [
      "Vale.X64.InsAes.va_wpProof_AESNI_imc",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
        "bool_inversion", "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_None@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_flags@tok",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.InsAes.va_wp_AESNI_imc",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "kinding_Vale.X64.QuickCode.mod_t@tok",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "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_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.AES.AES_s.inv_mix_columns_LE",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.QuickCode.update_state_mods",
        "typing_Vale.X64.QuickCode.va_mod_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.X64.QuickCode.Mod_None@tok",
        "typing_tok_Vale.X64.QuickCode.Mod_flags@tok", "unit_typing"
      ],
      0,
      "0cc0d6d3990a07aef4a503f04772f353"
    ],
    [
      "Vale.X64.InsAes.va_quick_AESNI_imc",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "5533e96a3ef9f0bc8b4b6403f904057c"
    ],
    [
      "Vale.X64.InsAes.va_code_AESNI_keygen_assist",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "334e0899397cabdae48ee2aac0c1a8e9"
    ],
    [
      "Vale.X64.InsAes.va_lemma_AESNI_keygen_assist",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "e7100162bd7b0f1f9a2c3bbd8e22b7aa"
    ],
    [
      "Vale.X64.InsAes.va_lemma_AESNI_keygen_assist",
      2,
      4,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
        "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Instructions_s_interpretation_Tm_arrow_10bec452133c4c396002981b20d0f26f",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
        "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
        "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
        "bool_inversion",
        "constructor_distinct_FStar.Pervasives.Native.Mktuple2",
        "constructor_distinct_FStar.Pervasives.Native.Some",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "constructor_distinct_Vale.X64.Instruction_s.IOpXmm",
        "constructor_distinct_Vale.X64.Instruction_s.Out",
        "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
        "constructor_distinct_Vale.X64.Machine_Semantics_s.AnnotateNone",
        "constructor_distinct_Vale.X64.Machine_s.Ins",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
        "data_typing_intro_Vale.X64.Instruction_s.IOpEx@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "disc_equation_Vale.X64.Machine_s.Ins", "eq2-interp",
        "equality_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "equality_tok_Vale.X64.Instruction_s.Out@tok",
        "equality_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
        "equation_FStar.FunctionalExtensionality.feq",
        "equation_FStar.FunctionalExtensionality.restricted_t",
        "equation_FStar.Option.mapTot",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.state_inv",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Instruction_s.instr_dep",
        "equation_Vale.X64.Instruction_s.instr_operand_t",
        "equation_Vale.X64.Instruction_s.instr_out",
        "equation_Vale.X64.Instruction_s.instr_val_t",
        "equation_Vale.X64.Instructions_s.eval_AESNI_keygen_assist",
        "equation_Vale.X64.Lemmas.eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.apply_option",
        "equation_Vale.X64.Machine_Semantics_s.bind_option",
        "equation_Vale.X64.Machine_Semantics_s.code",
        "equation_Vale.X64.Machine_Semantics_s.eval_instr",
        "equation_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ins_obs",
        "equation_Vale.X64.Machine_Semantics_s.instr_apply_eval",
        "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "equation_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Machine_Semantics_s.operand_obs128",
        "equation_Vale.X64.Machine_Semantics_s.regs_t",
        "equation_Vale.X64.Machine_Semantics_s.state_or_fail",
        "equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_xmm_",
        "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
        "equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.operand128",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Regs.to_fun", "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "equation_Vale.X64.StateLemmas.state_of_S",
        "equation_Vale.X64.StateLemmas.state_to_S",
        "equation_Vale.X64.Taint_Semantics.mk_ins",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Lemmas.code_modifies_ghost.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "fuel_guarded_inversion_Vale.X64.Machine_s.reg",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.int",
        "function_token_typing_Prims.unit",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.X64.Instruction_s.instr_out",
        "function_token_typing_Vale.X64.Instructions_s.eval_AESNI_keygen_assist",
        "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "function_token_typing_Vale.X64.Machine_s.t_reg",
        "function_token_typing_Vale.X64.Memory_Sems.lemma_heap_impl",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
        "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
        "interpretation_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
        "interpretation_Tm_abs_d7e539669515a49f97544a169303f779",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
        "kinding_Vale.X64.Machine_s.observation@tok",
        "kinding_Vale.X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_upd_eq",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Stack_Sems.lemma_stack_from_to",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_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.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
        "projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
        "projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_havoc_flags",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_i",
        "projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
        "projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
        "projection_inverse_Vale.X64.Machine_s.Ins_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
        "projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.Machine_s.OReg_tc",
        "projection_inverse_Vale.X64.Machine_s.OReg_tr",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "token_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "token_correspondence_Vale.X64.Instructions_s.eval_AESNI_keygen_assist",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_args.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_Semantics_s.obs_inouts.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_s.t_reg",
        "typing_Tm_abs_6c306f6a24efa681d9f42f76d1aa10ba",
        "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "typing_Vale.AES.AES_s.rot_word_LE",
        "typing_Vale.AES.AES_s.sub_word",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Def.Types_s.ixor",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.InsAes.va_code_AESNI_keygen_assist",
        "typing_Vale.X64.Instruction_s.instr_eval",
        "typing_Vale.X64.Instructions_s.ins_AESNI_keygen_assist",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "typing_Vale.X64.Machine_Semantics_s.eval_mov128_op",
        "typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
        "typing_Vale.X64.Machine_Semantics_s.machine_eval_ins",
        "typing_Vale.X64.Machine_Semantics_s.obs_operand_explicit",
        "typing_Vale.X64.Machine_s.operand128",
        "typing_Vale.X64.Regs.of_fun", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_Vale.X64.State.update_reg_xmm",
        "typing_Vale.X64.StateLemmas.state_to_S",
        "typing_tok_Vale.X64.Instruction_s.IOpXmm@tok",
        "typing_tok_Vale.X64.Instruction_s.Out@tok",
        "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok", "unit_typing"
      ],
      0,
      "42a8df420fb98bd1716dd26d0a1b90b3"
    ],
    [
      "Vale.X64.InsAes.va_wp_AESNI_keygen_assist",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "cc2631a6564162a359583f59493fa12e"
    ],
    [
      "Vale.X64.InsAes.va_wpProof_AESNI_keygen_assist",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
        "bool_inversion", "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_None@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_flags@tok",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.InsAes.va_wp_AESNI_keygen_assist",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_xmm",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "kinding_Vale.X64.QuickCode.mod_t@tok",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "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_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.QuickCode.update_state_mods",
        "typing_Vale.X64.QuickCode.va_mod_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.X64.QuickCode.Mod_None@tok",
        "typing_tok_Vale.X64.QuickCode.Mod_flags@tok", "unit_typing"
      ],
      0,
      "3494aece6efd3e124398561cd5bc77a9"
    ],
    [
      "Vale.X64.InsAes.va_quick_AESNI_keygen_assist",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "253f1d58ff61376e7d56c268665f2115"
    ]
  ]
]