[
  "�]�I4���Š�1��ŗ",
  [
    [
      "Vale.X64.InsMem.va_code_Load64_buffer",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "27da757fd457d6a3fa68b4b00929c9c4"
    ],
    [
      "Vale.X64.InsMem.va_lemma_Load64_buffer",
      1,
      2,
      2,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@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_irrelevance_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
        "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
        "Prims_pretyping_3862c4e8ff39bfc3871b6a47e7ff5b2e",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Flags_interpretation_Tm_arrow_cdf1f6cd0d3b8802627536b71c7dc9b7",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_2eb22b38a6da10fb966327d892d8131d",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_798f93baee047c0793beddf8ae4ab551",
        "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",
        "b2t_def", "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.IOp64",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "constructor_distinct_Vale.X64.Instruction_s.Out",
        "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
        "constructor_distinct_Vale.X64.Machine_s.Ins",
        "constructor_distinct_Vale.X64.Machine_s.MReg",
        "constructor_distinct_Vale.X64.Machine_s.OMem",
        "data_elim_FStar.Pervasives.Native.Mktuple2",
        "data_elim_FStar.Pervasives.Native.Some", "data_elim_Prims.Cons",
        "data_elim_Vale.X64.Bytes_Code_s.Instr",
        "data_elim_Vale.X64.Instruction_s.InstrTypeRecord",
        "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
        "data_elim_Vale.X64.Machine_s.Ins",
        "data_elim_Vale.X64.Machine_s.MemAccess",
        "data_elim_Vale.X64.Machine_s.OReg",
        "data_elim_Vale.X64.State.Mkvale_state",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Instruction_s.InstrTypeRecord@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",
        "disc_equation_Vale.X64.Machine_s.OReg", "eq2-interp",
        "equality_tok_Vale.X64.Instruction_s.IOp64@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_heap_impl",
        "equation_Vale.Def.Words_s.nat64", "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.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_is_dst_opr64",
        "equation_Vale.X64.Decls.va_operand_reg_opr64",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.va_update_operand",
        "equation_Vale.X64.Decls.valid_mem_operand64",
        "equation_Vale.X64.Decls.valid_operand",
        "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_Mov64",
        "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_maddr",
        "equation_Vale.X64.Machine_Semantics_s.eval_operand",
        "equation_Vale.X64.Machine_Semantics_s.flags_t",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "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_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_obs",
        "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_operand64_preserve_flags__",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_64_",
        "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand64",
        "equation_Vale.X64.Machine_s.flag",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.operand64",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Machine_s.t_reg_to_int",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.memtaint",
        "equation_Vale.X64.Memory.vale_heap_impl_equal",
        "equation_Vale.X64.State.eval_maddr",
        "equation_Vale.X64.State.eval_operand",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "equation_Vale.X64.State.valid_maddr",
        "equation_Vale.X64.State.valid_src_operand",
        "equation_Vale.X64.StateLemmas.state_of_S",
        "equation_Vale.X64.StateLemmas.state_to_S",
        "equation_Vale.X64.Taint_Semantics.mk_ins",
        "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.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",
        "fuel_guarded_inversion_FStar.Pervasives.Native.option",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "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.int",
        "function_token_typing_Prims.unit",
        "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",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
        "interpretation_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
        "interpretation_Tm_abs_1f233bb62d19e8ce94de2fc1626a49a7",
        "interpretation_Tm_abs_4185c7ad5dc50a20deee59c126b9b37b",
        "interpretation_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
        "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "interpretation_Tm_abs_9eff9d103851337e0612359cac5d60b0",
        "interpretation_Tm_abs_a7fc7c3035a1a3dfe26ac53ca2f3dd49",
        "interpretation_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
        "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
        "kinding_FStar.Pervasives.Native.tuple2@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
        "kinding_Vale.X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_FStar.Pervasives.invertOption",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.InsLemmas.lemma_valid_buf_maddr64",
        "lemma_Vale.X64.InsLemmas.lemma_valid_src_operand64_and_taint",
        "lemma_Vale.X64.Memory_Sems.lemma_heap_get_heap",
        "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",
        "lemma_Vale.X64.StateLemmas.lemma_load_buffer_read64",
        "lemma_Vale.X64.StateLemmas.lemma_load_mem_get64",
        "lemma_Vale.X64.StateLemmas.lemma_to_eval_operand",
        "lemma_Vale.X64.StateLemmas.lemma_valid_buffer_read64",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Negation",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "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_memTaint",
        "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.OReg_r",
        "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_memTaint",
        "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.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_memTaint",
        "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.MReg_offset",
        "projection_inverse_Vale.X64.Machine_s.MReg_r",
        "projection_inverse_Vale.X64.Machine_s.OMem_m",
        "projection_inverse_Vale.X64.Machine_s.OMem_tc",
        "projection_inverse_Vale.X64.Machine_s.OMem_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_memTaint",
        "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_423a970236765465eb8eb63b6e1b8f53",
        "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
        "token_correspondence_Vale.X64.Instructions_s.eval_Mov64",
        "token_correspondence_Vale.X64.Machine_Semantics_s.instr_annotation@tok",
        "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_s.t_reg", "true_interp",
        "typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2",
        "typing_FStar.Pervasives.Native.snd",
        "typing_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
        "typing_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
        "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "typing_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "typing_Tm_abs_9eff9d103851337e0612359cac5d60b0",
        "typing_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
        "typing_Vale.X64.Decls.va_is_dst_opr64",
        "typing_Vale.X64.Decls.va_update_operand",
        "typing_Vale.X64.Flags.of_fun",
        "typing_Vale.X64.InsMem.va_code_Load64_buffer",
        "typing_Vale.X64.Instruction_s.instr_eval",
        "typing_Vale.X64.Instructions_s.ins_Mov64",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
        "typing_Vale.X64.Machine_Semantics_s.apply_option",
        "typing_Vale.X64.Machine_Semantics_s.eval_instr",
        "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.obs_operand_explicit",
        "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
        "typing_Vale.X64.Machine_s.operand64",
        "typing_Vale.X64.Memory.get_vale_heap",
        "typing_Vale.X64.Memory.valid_mem64", "typing_Vale.X64.Regs.of_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_memTaint",
        "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.eval_operand",
        "typing_Vale.X64.StateLemmas.state_to_S",
        "typing_tok_Vale.X64.Instruction_s.IOp64@tok",
        "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
        "unit_inversion", "unit_typing"
      ],
      0,
      "3001b20c8575b72d8b7be7119c59592c"
    ],
    [
      "Vale.X64.InsMem.va_wpProof_Load64_buffer",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
        "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
        "bool_inversion", "constructor_distinct_Prims.Cons",
        "constructor_distinct_Prims.Nil",
        "constructor_distinct_Vale.X64.QuickCode.Mod_reg",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok", "eq2-interp",
        "equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_is_dst_opr64",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_operand_dst_opr64",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_update_operand",
        "equation_Vale.X64.InsMem.va_wp_Load64_buffer",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Memory.vale_heap_impl_equal",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.QuickCode.update_state_mod",
        "equation_Vale.X64.QuickCode.va_mod_dst_opr64",
        "equation_Vale.X64.State.eval_operand",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "kinding_Vale.X64.QuickCode.mod_t@tok",
        "lemma_Vale.X64.Flags.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "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_memTaint",
        "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_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.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "projection_inverse_Vale.X64.QuickCode.Mod_reg__0",
        "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_memTaint",
        "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",
        "typing_Vale.X64.Decls.va_is_dst_opr64",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_update_operand",
        "typing_Vale.X64.QuickCode.va_mod_dst_opr64",
        "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.eval_operand",
        "typing_tok_Vale.X64.QuickCode.Mod_None@tok", "unit_typing"
      ],
      0,
      "1ac27d40ed3a3aea01b92e300a2385e1"
    ],
    [
      "Vale.X64.InsMem.va_quick_Load64_buffer",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "46df38f2300299007a5060c7f025dd92"
    ],
    [
      "Vale.X64.InsMem.va_code_Store64_buffer",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "fe5ebcf1c394a9030cd5b104b15be4bc"
    ],
    [
      "Vale.X64.InsMem.va_lemma_Store64_buffer",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@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",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
        "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Flags_interpretation_Tm_arrow_cdf1f6cd0d3b8802627536b71c7dc9b7",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100",
        "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",
        "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.Arch.HeapTypes_s.TUInt64",
        "constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
        "constructor_distinct_Vale.X64.Instruction_s.IOp64",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "constructor_distinct_Vale.X64.Instruction_s.Out",
        "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
        "constructor_distinct_Vale.X64.Machine_s.Ins",
        "constructor_distinct_Vale.X64.Machine_s.MReg",
        "constructor_distinct_Vale.X64.Machine_s.OMem",
        "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",
        "disc_equation_Vale.X64.Machine_s.Ins",
        "disc_equation_Vale.X64.Machine_s.OReg", "eq2-interp",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equality_tok_Vale.X64.Instruction_s.IOp64@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.logical",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Arch.HeapImpl.vale_heap_impl",
        "equation_Vale.Arch.MachineHeap_s.update_heap64",
        "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.buffer64_write",
        "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_operand_reg_opr64",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_mem",
        "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_Mov64",
        "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_maddr",
        "equation_Vale.X64.Machine_Semantics_s.eval_operand",
        "equation_Vale.X64.Machine_Semantics_s.flags_t",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "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_ins",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Machine_Semantics_s.regs_t",
        "equation_Vale.X64.Machine_Semantics_s.state_or_fail",
        "equation_Vale.X64.Machine_Semantics_s.update_mem_and_taint",
        "equation_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags__",
        "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand64",
        "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
        "equation_Vale.X64.Machine_s.flag",
        "equation_Vale.X64.Machine_s.operand64",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.t_reg_to_int",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.memtaint",
        "equation_Vale.X64.Memory.set_vale_heap",
        "equation_Vale.X64.Memory.vale_heap_impl_equal",
        "equation_Vale.X64.Memory.valid_buffer_read",
        "equation_Vale.X64.Memory.valid_buffer_write",
        "equation_Vale.X64.State.eval_operand",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.valid_src_operand",
        "equation_Vale.X64.StateLemmas.state_of_S",
        "equation_Vale.X64.StateLemmas.state_to_S",
        "equation_Vale.X64.Taint_Semantics.mk_ins",
        "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.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",
        "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.X64.Instruction_s.instr_out",
        "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.StateLemmas.same_heap_types",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
        "interpretation_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
        "interpretation_Tm_abs_1f233bb62d19e8ce94de2fc1626a49a7",
        "interpretation_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
        "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "interpretation_Tm_abs_a7fc7c3035a1a3dfe26ac53ca2f3dd49",
        "interpretation_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
        "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
        "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
        "kinding_Vale.X64.Machine_s.reg@tok", "l_and-interp",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_Vale.X64.Flags.lemma_equal_elim",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.Memory.modifies_valid_taint64",
        "lemma_Vale.X64.Memory_Sems.lemma_heap_get_heap",
        "lemma_Vale.X64.Memory_Sems.lemma_heap_upd_heap",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Stack_Sems.lemma_stack_from_to",
        "lemma_Vale.X64.StateLemmas.lemma_to_eval_operand",
        "lemma_Vale.X64.StateLemmas.lemma_valid_buffer_read64",
        "lemma_Vale.X64.StateLemmas.lemma_valid_mem_addr64",
        "primitive_Prims.op_AmpAmp",
        "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_memTaint",
        "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.OReg_r",
        "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_memTaint",
        "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_memTaint",
        "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.MReg_offset",
        "projection_inverse_Vale.X64.Machine_s.MReg_r",
        "projection_inverse_Vale.X64.Machine_s.OMem_m",
        "projection_inverse_Vale.X64.Machine_s.OMem_tc",
        "projection_inverse_Vale.X64.Machine_s.OMem_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_memTaint",
        "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_21546bbfcd6f29a8d6a0b4798ed975a5",
        "refinement_interpretation_Tm_refine_2c7ecebd8a41d0890aab4251b61d6458",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_423a970236765465eb8eb63b6e1b8f53",
        "refinement_interpretation_Tm_refine_4b8cb9d02d0425880fe398ab5d3efb72",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55",
        "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802",
        "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
        "token_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "token_correspondence_Vale.X64.Instructions_s.eval_Mov64",
        "token_correspondence_Vale.X64.Machine_s.t_reg", "true_interp",
        "typing_FStar.Pervasives.Native.snd",
        "typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
        "typing_Prims.l_and",
        "typing_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
        "typing_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
        "typing_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
        "typing_Tm_abs_e0e867a53fc7f6b2835d9063faee19ea",
        "typing_Vale.Arch.Heap.heap_get",
        "typing_Vale.Arch.MachineHeap_s.update_heap64",
        "typing_Vale.Arch.MachineHeap_s.valid_addr64",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Flags.of_fun",
        "typing_Vale.X64.InsMem.va_code_Store64_buffer",
        "typing_Vale.X64.Instruction_s.instr_eval",
        "typing_Vale.X64.Instructions_s.ins_Mov64",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_memTaint",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
        "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.update_n",
        "typing_Vale.X64.Machine_s.operand64",
        "typing_Vale.X64.Memory.buffer_readable",
        "typing_Vale.X64.Memory.buffer_write",
        "typing_Vale.X64.Memory.buffer_writeable",
        "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Regs.of_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_memTaint",
        "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.StateLemmas.state_to_S",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "typing_tok_Vale.X64.Instruction_s.IOp64@tok",
        "typing_tok_Vale.X64.Instruction_s.Out@tok",
        "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok", "unit_typing"
      ],
      0,
      "25715e2e63f537f2303a70da0d914c74"
    ],
    [
      "Vale.X64.InsMem.va_wpProof_Store64_buffer",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heap_impl",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
        "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_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.InsMem.va_wp_Store64_buffer",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.set_vale_heap",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.State.state_eq",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "lemma_Vale.X64.Flags.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "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_memTaint",
        "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_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.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_memTaint",
        "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",
        "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",
        "unit_typing"
      ],
      0,
      "4ff10be3b171855527a1b6c801b92019"
    ],
    [
      "Vale.X64.InsMem.va_quick_Store64_buffer",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "2def5f33c7d4f31de7d646fafcf0b81f"
    ],
    [
      "Vale.X64.InsMem.va_code_LoadBe64_buffer",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "7dc4986b0c53b5fbda67739e27374c49"
    ],
    [
      "Vale.X64.InsMem.va_lemma_LoadBe64_buffer",
      1,
      2,
      2,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@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_irrelevance_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.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_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Flags_interpretation_Tm_arrow_cdf1f6cd0d3b8802627536b71c7dc9b7",
        "Vale.X64.Instructions_s_interpretation_Tm_arrow_8dbf441b1c0ed3aaf19aa981c0b06c50",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_2eb22b38a6da10fb966327d892d8131d",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_798f93baee047c0793beddf8ae4ab551",
        "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",
        "b2t_def", "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.Arch.HeapTypes_s.TUInt64",
        "constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
        "constructor_distinct_Vale.X64.Instruction_s.IOp64",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "constructor_distinct_Vale.X64.Instruction_s.Out",
        "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
        "constructor_distinct_Vale.X64.Machine_s.Ins",
        "constructor_distinct_Vale.X64.Machine_s.MReg",
        "constructor_distinct_Vale.X64.Machine_s.OMem",
        "data_elim_FStar.Pervasives.Native.Mktuple2",
        "data_elim_FStar.Pervasives.Native.Some", "data_elim_Prims.Cons",
        "data_elim_Vale.X64.Bytes_Code_s.Instr",
        "data_elim_Vale.X64.Instruction_s.InstrTypeRecord",
        "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
        "data_elim_Vale.X64.Machine_s.Ins",
        "data_elim_Vale.X64.Machine_s.MemAccess",
        "data_elim_Vale.X64.Machine_s.OReg",
        "data_elim_Vale.X64.State.Mkvale_state",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Instruction_s.InstrTypeRecord@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",
        "disc_equation_Vale.X64.Machine_s.OReg", "eq2-interp",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equality_tok_Vale.X64.Instruction_s.IOp64@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_heap_impl",
        "equation_Vale.Def.Words_s.nat64", "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.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_is_dst_opr64",
        "equation_Vale.X64.Decls.va_operand_reg_opr64",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.va_update_operand",
        "equation_Vale.X64.Decls.valid_mem_operand64",
        "equation_Vale.X64.Decls.valid_operand",
        "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_MovBe64",
        "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_maddr",
        "equation_Vale.X64.Machine_Semantics_s.eval_operand",
        "equation_Vale.X64.Machine_Semantics_s.flags_t",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "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_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_obs",
        "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_operand64_preserve_flags__",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_",
        "equation_Vale.X64.Machine_Semantics_s.update_reg_64_",
        "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand64",
        "equation_Vale.X64.Machine_s.flag",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.operand64",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg_to_int",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.memtaint",
        "equation_Vale.X64.Memory.vale_heap_impl_equal",
        "equation_Vale.X64.State.eval_maddr",
        "equation_Vale.X64.State.eval_operand",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "equation_Vale.X64.State.valid_maddr",
        "equation_Vale.X64.State.valid_src_operand",
        "equation_Vale.X64.StateLemmas.state_of_S",
        "equation_Vale.X64.StateLemmas.state_to_S",
        "equation_Vale.X64.Taint_Semantics.mk_ins",
        "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.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",
        "fuel_guarded_inversion_FStar.Pervasives.Native.option",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "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.int",
        "function_token_typing_Prims.unit",
        "function_token_typing_Vale.X64.Instruction_s.instr_out",
        "function_token_typing_Vale.X64.Instructions_s.eval_MovBe64",
        "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",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
        "interpretation_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
        "interpretation_Tm_abs_1f233bb62d19e8ce94de2fc1626a49a7",
        "interpretation_Tm_abs_40cd8814e188ff9be1e1aaa5a9edeba0",
        "interpretation_Tm_abs_4185c7ad5dc50a20deee59c126b9b37b",
        "interpretation_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
        "interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "interpretation_Tm_abs_a7fc7c3035a1a3dfe26ac53ca2f3dd49",
        "interpretation_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
        "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
        "kinding_FStar.Pervasives.Native.tuple2@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
        "kinding_Vale.X64.Machine_s.reg@tok",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_FStar.Pervasives.invertOption",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.InsLemmas.lemma_valid_buf_maddr64",
        "lemma_Vale.X64.InsLemmas.lemma_valid_src_operand64_and_taint",
        "lemma_Vale.X64.Memory_Sems.lemma_heap_get_heap",
        "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",
        "lemma_Vale.X64.StateLemmas.lemma_load_buffer_read64",
        "lemma_Vale.X64.StateLemmas.lemma_load_mem_get64",
        "lemma_Vale.X64.StateLemmas.lemma_to_eval_operand",
        "lemma_Vale.X64.StateLemmas.lemma_valid_buffer_read64",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Negation",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "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_memTaint",
        "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.OReg_r",
        "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_memTaint",
        "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.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_memTaint",
        "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.MReg_offset",
        "projection_inverse_Vale.X64.Machine_s.MReg_r",
        "projection_inverse_Vale.X64.Machine_s.OMem_m",
        "projection_inverse_Vale.X64.Machine_s.OMem_tc",
        "projection_inverse_Vale.X64.Machine_s.OMem_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_memTaint",
        "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_423a970236765465eb8eb63b6e1b8f53",
        "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
        "token_correspondence_Vale.X64.Instructions_s.eval_MovBe64",
        "token_correspondence_Vale.X64.Machine_Semantics_s.instr_annotation@tok",
        "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_s.t_reg", "true_interp",
        "typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2",
        "typing_FStar.Pervasives.Native.snd",
        "typing_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
        "typing_Tm_abs_40cd8814e188ff9be1e1aaa5a9edeba0",
        "typing_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
        "typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
        "typing_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "typing_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
        "typing_Vale.X64.CPU_Features_s.movbe_enabled",
        "typing_Vale.X64.Decls.va_is_dst_opr64",
        "typing_Vale.X64.Decls.va_update_operand",
        "typing_Vale.X64.Flags.of_fun",
        "typing_Vale.X64.InsMem.va_code_LoadBe64_buffer",
        "typing_Vale.X64.Instruction_s.instr_eval",
        "typing_Vale.X64.Instructions_s.ins_MovBe64",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
        "typing_Vale.X64.Machine_Semantics_s.apply_option",
        "typing_Vale.X64.Machine_Semantics_s.eval_instr",
        "typing_Vale.X64.Machine_Semantics_s.eval_operand",
        "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.obs_operand_explicit",
        "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
        "typing_Vale.X64.Machine_s.operand64",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.Memory.get_vale_heap",
        "typing_Vale.X64.Memory.valid_mem64", "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_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_memTaint",
        "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.StateLemmas.state_to_S",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "typing_tok_Vale.X64.Instruction_s.IOp64@tok",
        "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
        "unit_inversion", "unit_typing"
      ],
      0,
      "d3945d6152a111a0ded918b10b011778"
    ],
    [
      "Vale.X64.InsMem.va_wpProof_LoadBe64_buffer",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
        "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
        "bool_inversion", "constructor_distinct_Prims.Cons",
        "constructor_distinct_Prims.Nil",
        "constructor_distinct_Vale.X64.QuickCode.Mod_reg",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok", "eq2-interp",
        "equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_is_dst_opr64",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_operand_dst_opr64",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_update_operand",
        "equation_Vale.X64.InsMem.va_wp_LoadBe64_buffer",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Memory.vale_heap_impl_equal",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.QuickCode.update_state_mod",
        "equation_Vale.X64.QuickCode.va_mod_dst_opr64",
        "equation_Vale.X64.State.eval_operand",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "kinding_Vale.X64.QuickCode.mod_t@tok",
        "lemma_Vale.X64.Flags.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "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_memTaint",
        "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_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.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "projection_inverse_Vale.X64.QuickCode.Mod_reg__0",
        "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_memTaint",
        "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",
        "typing_Vale.X64.Decls.va_is_dst_opr64",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_update_operand",
        "typing_Vale.X64.QuickCode.va_mod_dst_opr64",
        "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.eval_operand",
        "typing_tok_Vale.X64.QuickCode.Mod_None@tok", "unit_typing"
      ],
      0,
      "84339ec0eee38fc6ecfad738400efda8"
    ],
    [
      "Vale.X64.InsMem.va_quick_LoadBe64_buffer",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "df22038da4cbf797fdb774b913790594"
    ],
    [
      "Vale.X64.InsMem.va_code_StoreBe64_buffer",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "95ed360597adebfab950a8417d88d6a7"
    ],
    [
      "Vale.X64.InsMem.va_lemma_StoreBe64_buffer",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@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",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
        "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Flags_interpretation_Tm_arrow_cdf1f6cd0d3b8802627536b71c7dc9b7",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_00bdd4f610fcebb80d44d9e56b43a6b9",
        "Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100",
        "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",
        "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.Arch.HeapTypes_s.TUInt64",
        "constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
        "constructor_distinct_Vale.X64.Instruction_s.IOp64",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "constructor_distinct_Vale.X64.Instruction_s.Out",
        "constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
        "constructor_distinct_Vale.X64.Machine_s.Ins",
        "constructor_distinct_Vale.X64.Machine_s.MReg",
        "constructor_distinct_Vale.X64.Machine_s.OMem",
        "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",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_Vale.X64.Machine_s.Ins",
        "disc_equation_Vale.X64.Machine_s.OReg", "eq2-interp",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equality_tok_Vale.X64.Instruction_s.IOp64@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.logical",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Arch.HeapImpl.vale_heap_impl",
        "equation_Vale.Arch.MachineHeap_s.update_heap64",
        "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.buffer64_write",
        "equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins",
        "equation_Vale.X64.Decls.ocmp",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_fuel",
        "equation_Vale.X64.Decls.va_operand_reg_opr64",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_mem",
        "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_MovBe64",
        "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_maddr",
        "equation_Vale.X64.Machine_Semantics_s.eval_operand",
        "equation_Vale.X64.Machine_Semantics_s.flags_t",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "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_ins",
        "equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Machine_Semantics_s.regs_t",
        "equation_Vale.X64.Machine_Semantics_s.state_or_fail",
        "equation_Vale.X64.Machine_Semantics_s.update_mem_and_taint",
        "equation_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags__",
        "equation_Vale.X64.Machine_Semantics_s.valid_dst_operand64",
        "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
        "equation_Vale.X64.Machine_s.flag",
        "equation_Vale.X64.Machine_s.operand64",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.t_reg_to_int",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.memtaint",
        "equation_Vale.X64.Memory.set_vale_heap",
        "equation_Vale.X64.Memory.vale_heap_impl_equal",
        "equation_Vale.X64.Memory.valid_buffer_read",
        "equation_Vale.X64.Memory.valid_buffer_write",
        "equation_Vale.X64.State.eval_operand",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.valid_src_operand",
        "equation_Vale.X64.StateLemmas.state_of_S",
        "equation_Vale.X64.StateLemmas.state_to_S",
        "equation_Vale.X64.Taint_Semantics.mk_ins",
        "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.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",
        "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.X64.Instruction_s.instr_out",
        "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.StateLemmas.same_heap_types",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
        "interpretation_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
        "interpretation_Tm_abs_1f233bb62d19e8ce94de2fc1626a49a7",
        "interpretation_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
        "interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
        "interpretation_Tm_abs_a7fc7c3035a1a3dfe26ac53ca2f3dd49",
        "interpretation_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
        "interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
        "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
        "kinding_Vale.X64.Machine_s.reg@tok", "l_and-interp",
        "lemma_FStar.FunctionalExtensionality.feq_on_domain",
        "lemma_Vale.X64.Flags.lemma_equal_elim",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.Memory.modifies_refl",
        "lemma_Vale.X64.Memory.modifies_valid_taint64",
        "lemma_Vale.X64.Memory_Sems.lemma_heap_get_heap",
        "lemma_Vale.X64.Memory_Sems.lemma_heap_upd_heap",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Stack_Sems.lemma_stack_from_to",
        "lemma_Vale.X64.StateLemmas.lemma_to_eval_operand",
        "lemma_Vale.X64.StateLemmas.lemma_valid_buffer_read64",
        "lemma_Vale.X64.StateLemmas.lemma_valid_mem_addr64",
        "primitive_Prims.op_AmpAmp",
        "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_memTaint",
        "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.OReg_r",
        "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_memTaint",
        "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_memTaint",
        "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.MReg_offset",
        "projection_inverse_Vale.X64.Machine_s.MReg_r",
        "projection_inverse_Vale.X64.Machine_s.OMem_m",
        "projection_inverse_Vale.X64.Machine_s.OMem_tc",
        "projection_inverse_Vale.X64.Machine_s.OMem_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_memTaint",
        "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_21546bbfcd6f29a8d6a0b4798ed975a5",
        "refinement_interpretation_Tm_refine_2c7ecebd8a41d0890aab4251b61d6458",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_3b1a603d57602642cd8cec1a9fa6b2c7",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_423a970236765465eb8eb63b6e1b8f53",
        "refinement_interpretation_Tm_refine_4b8cb9d02d0425880fe398ab5d3efb72",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_83eb3110e9b0236ceecba75390ebeb55",
        "refinement_interpretation_Tm_refine_c55af5cefb01844d307de87b2d347802",
        "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
        "token_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "token_correspondence_Vale.X64.Instructions_s.eval_MovBe64",
        "token_correspondence_Vale.X64.Machine_s.t_reg", "true_interp",
        "typing_FStar.Pervasives.Native.snd",
        "typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
        "typing_Prims.l_and",
        "typing_Tm_abs_02710d3db89c8747cda60a5174528517",
        "typing_Tm_abs_14a3aa8102b38210dfdbec5a683db924",
        "typing_Tm_abs_420e19c3bc05c948529fe5a56f707d02",
        "typing_Tm_abs_a7fc7c3035a1a3dfe26ac53ca2f3dd49",
        "typing_Tm_abs_afea1bd1afc669e875290ba98b10bc60",
        "typing_Vale.Arch.Heap.heap_get",
        "typing_Vale.Arch.MachineHeap_s.update_heap64",
        "typing_Vale.Arch.MachineHeap_s.valid_addr64",
        "typing_Vale.X64.CPU_Features_s.movbe_enabled",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Flags.of_fun",
        "typing_Vale.X64.InsMem.va_code_StoreBe64_buffer",
        "typing_Vale.X64.Instruction_s.instr_eval",
        "typing_Vale.X64.Instructions_s.ins_MovBe64",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
        "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_memTaint",
        "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.instr_write_output_explicit",
        "typing_Vale.X64.Machine_Semantics_s.update_n",
        "typing_Vale.X64.Machine_s.operand64",
        "typing_Vale.X64.Memory.buffer_readable",
        "typing_Vale.X64.Memory.buffer_write",
        "typing_Vale.X64.Memory.buffer_writeable",
        "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Regs.of_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_memTaint",
        "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.eval_operand",
        "typing_Vale.X64.StateLemmas.state_to_S",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "typing_tok_Vale.X64.Instruction_s.IOp64@tok",
        "typing_tok_Vale.X64.Instruction_s.Out@tok",
        "typing_tok_Vale.X64.Instruction_s.PreserveFlags@tok", "unit_typing"
      ],
      0,
      "919636d5e290d0aef0067e0bc4fac564"
    ],
    [
      "Vale.X64.InsMem.va_wpProof_StoreBe64_buffer",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heap_impl",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
        "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_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.InsMem.va_wp_StoreBe64_buffer",
        "equation_Vale.X64.Machine_Semantics_s.ins",
        "equation_Vale.X64.Machine_Semantics_s.ocmp",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.set_vale_heap",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.State.state_eq",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "lemma_Vale.X64.Flags.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "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_memTaint",
        "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_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.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_memTaint",
        "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",
        "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",
        "unit_typing"
      ],
      0,
      "3bde5e48ffb9b4615042900be2fe2329"
    ],
    [
      "Vale.X64.InsMem.va_quick_StoreBe64_buffer",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.X64.Decls.va_fuel",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "671e43c6b78f205ca200ccdc72d73773"
    ]
  ]
]