[
  "�$��e�H��\u0002tʐ���",
  [
    [
      "X64.AESopt.aes_reqs",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "00ba2d73e61a0ff5bb68efce84d3fd4a"
    ],
    [
      "X64.AESopt.finish_aes_encrypt_le",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_AES_s.is_aes_key_LE",
        "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "7ed1eed0b9430c08c62fbb8490a5fec8"
    ],
    [
      "X64.AESopt.finish_aes_encrypt_le",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_AES_helpers.cipher_opaque",
        "equation_AES_s.aes_encrypt_LE_def",
        "equation_AES_s.key_to_round_keys_LE",
        "equation_GCTR.aes_encrypt_le", "equation_Types_s.quad32",
        "equation_Words_s.nat32", "fuel_guarded_inversion_Words_s.four",
        "function_token_typing_Opaque_s.make_opaque",
        "token_correspondence_AES_s.aes_encrypt_LE_def",
        "token_correspondence_AES_s.cipher"
      ],
      0,
      "fcd2dfe4acb89086db2637521753c130"
    ],
    [
      "X64.AESopt.finish_aes_encrypt_le",
      3,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_AES_s.AES_128",
        "disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
        "fuel_guarded_inversion_AES_s.algorithm"
      ],
      0,
      "5c02ec8ac1f555caa1478a956d233ae8"
    ],
    [
      "X64.AESopt.va_lemma_Load_two_lsb",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_Prims.Cons",
        "constructor_distinct_X64.Machine_s.Block",
        "constructor_distinct_X64.Machine_s.OReg",
        "constructor_distinct_X64.Machine_s.R11",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "data_typing_intro_X64.Vale.Decls.TReg@tok",
        "disc_equation_Prims.Cons", "disc_equation_X64.Machine_s.Block",
        "disc_equation_X64.Machine_s.OReg",
        "disc_equation_X64.Machine_s.Rsp", "eq2-interp",
        "equality_tok_X64.Machine_s.R11@tok", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Types_s.quad32",
        "equation_Words.Two_s.two_to_nat", "equation_Words_s.nat1",
        "equation_Words_s.nat32", "equation_Words_s.nat64",
        "equation_Words_s.natN", "equation_X64.AESopt.va_code_Load_two_lsb",
        "equation_X64.AESopt.va_transparent_code_Load_two_lsb",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_update_operand",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_upd_eq",
        "lemma_X64.Vale.Xmms.lemma_upd_ne", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "proj_equation_Prims.Cons_hd",
        "proj_equation_Prims.Cons_tl", "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_X64.Machine_s.Block_block",
        "proj_equation_X64.Machine_s.OReg_r",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "projection_inverse_Words_s.Mkfour_hi2",
        "projection_inverse_Words_s.Mkfour_hi3",
        "projection_inverse_Words_s.Mkfour_lo0",
        "projection_inverse_Words_s.Mktwo_hi",
        "projection_inverse_Words_s.Mktwo_lo",
        "projection_inverse_X64.Machine_s.Block_block",
        "projection_inverse_X64.Machine_s.Block_t_ins",
        "projection_inverse_X64.Machine_s.Block_t_ocmp",
        "projection_inverse_X64.Machine_s.OReg_r",
        "projection_inverse_X64.Vale.Decls.TReg_r",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_1bc5c4f392722fe6a26189e86f17c270",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Arch.Types.insert_nat64_opaque", "typing_Prims.pow2",
        "typing_Words_s.__proj__Mkfour__item__lo0",
        "typing_Words_s.int_to_natN", "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_update_operand",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.State.update_xmm", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Machine_s.R11@tok"
      ],
      0,
      "ce1227a93a7674d5a4abf2364a4b8059"
    ],
    [
      "X64.AESopt.va_wpMonotone_Load_two_lsb",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equality_tok_X64.Machine_s.R11@tok",
        "equation_X64.AESopt.va_wp_Load_two_lsb",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_operand_xmm",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_tok_X64.Machine_s.R11@tok", "unit_typing"
      ],
      0,
      "068ce28e5149ca28779d6b878e69a8ee"
    ],
    [
      "X64.AESopt.va_wpCompute_Load_two_lsb",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.AESopt.va_code_Load_two_lsb",
        "equation_X64.AESopt.va_wp_Load_two_lsb",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
      ],
      0,
      "7a55512d5a9f1dc48365d617c2345eda"
    ],
    [
      "X64.AESopt.va_wpProof_Load_two_lsb",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "9f8ca4550358d6a5eb30e34ed646f86a"
    ],
    [
      "X64.AESopt.va_wpProof_Load_two_lsb",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp", "equality_tok_X64.Machine_s.R11@tok",
        "equation_X64.AESopt.va_code_Load_two_lsb",
        "equation_X64.AESopt.va_wpCompute_Load_two_lsb",
        "equation_X64.AESopt.va_wp_Load_two_lsb",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.AESopt.va_wpCompute_Load_two_lsb",
        "typing_X64.Vale.Regs.sel", "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Machine_s.R11@tok", "unit_typing"
      ],
      0,
      "42793fc297eb58e7e84ff9c97fe3af7a"
    ],
    [
      "X64.AESopt.va_lemma_Load_one_lsb",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_Prims.Cons",
        "constructor_distinct_X64.Machine_s.Block",
        "constructor_distinct_X64.Machine_s.OReg",
        "constructor_distinct_X64.Machine_s.R11",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "data_typing_intro_X64.Vale.Decls.TReg@tok",
        "disc_equation_Prims.Cons", "disc_equation_X64.Machine_s.Block",
        "disc_equation_X64.Machine_s.OReg",
        "disc_equation_X64.Machine_s.Rsp", "eq2-interp",
        "equality_tok_X64.Machine_s.R11@tok", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Words.Two_s.two_to_nat",
        "equation_Words_s.nat32", "equation_X64.AESopt.va_code_Load_one_lsb",
        "equation_X64.AESopt.va_transparent_code_Load_one_lsb",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_operand_reg_opr64",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_update_operand",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_upd_eq",
        "lemma_X64.Vale.Xmms.lemma_upd_ne", "proj_equation_Prims.Cons_hd",
        "proj_equation_Prims.Cons_tl", "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_X64.Machine_s.Block_block",
        "proj_equation_X64.Machine_s.OReg_r",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "projection_inverse_Words_s.Mkfour_hi2",
        "projection_inverse_Words_s.Mkfour_hi3",
        "projection_inverse_Words_s.Mktwo_hi",
        "projection_inverse_Words_s.Mktwo_lo",
        "projection_inverse_X64.Machine_s.Block_block",
        "projection_inverse_X64.Machine_s.Block_t_ins",
        "projection_inverse_X64.Machine_s.Block_t_ocmp",
        "projection_inverse_X64.Machine_s.OReg_r",
        "projection_inverse_X64.Vale.Decls.TReg_r",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_1bc5c4f392722fe6a26189e86f17c270",
        "refinement_interpretation_Tm_refine_93c4793e88ba66df1f803c1610135c3a",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Prims.pow2", "typing_Words_s.int_to_natN",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_update_operand",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.State.update_xmm", "typing_X64.Vale.Xmms.sel",
        "typing_X64.Vale.Xmms.upd", "typing_tok_X64.Machine_s.R11@tok"
      ],
      0,
      "ebf9790c93cb1ca7d46f461ae275eba3"
    ],
    [
      "X64.AESopt.va_wpMonotone_Load_one_lsb",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equality_tok_X64.Machine_s.R11@tok",
        "equation_X64.AESopt.va_wp_Load_one_lsb",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_operand_xmm",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_tok_X64.Machine_s.R11@tok", "unit_typing"
      ],
      0,
      "d49a5629b1e3063267f778a55ddf450b"
    ],
    [
      "X64.AESopt.va_wpCompute_Load_one_lsb",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.AESopt.va_code_Load_one_lsb",
        "equation_X64.AESopt.va_wp_Load_one_lsb",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
      ],
      0,
      "c1b2c8d3d2aa67a95743c15020e703d4"
    ],
    [
      "X64.AESopt.va_wpProof_Load_one_lsb",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "ed6b37847dbc7b196a0af5a5f89fdbcc"
    ],
    [
      "X64.AESopt.va_wpProof_Load_one_lsb",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp", "equality_tok_X64.Machine_s.R11@tok",
        "equation_X64.AESopt.va_code_Load_one_lsb",
        "equation_X64.AESopt.va_wpCompute_Load_one_lsb",
        "equation_X64.AESopt.va_wp_Load_one_lsb",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.AESopt.va_wpCompute_Load_one_lsb",
        "typing_X64.Vale.Regs.sel", "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Machine_s.R11@tok", "unit_typing"
      ],
      0,
      "f20ac1b62889213cb50e54708cc8640d"
    ],
    [
      "X64.AESopt.va_lemma_Handle_ctr32",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_X64.Machine_s.R11",
        "disc_equation_X64.Machine_s.Rsp", "eq2-interp",
        "equality_tok_X64.Machine_s.R11@tok",
        "equation_Arch.Types.add_wrap_quad32", "equation_GCTR.inc32lite",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Types_s.add_wrap",
        "equation_Types_s.quad32", "equation_Types_s.quad32_xor",
        "equation_Words_s.nat32", "equation_Words_s.natN",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.State.state_eq",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "lemma_Arch.Types.lemma_reverse_bytes_quad32",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Machine_s.OReg_r",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_Words_s.Mkfour_hi2",
        "projection_inverse_Words_s.Mkfour_hi3",
        "projection_inverse_Words_s.Mkfour_lo0",
        "projection_inverse_Words_s.Mkfour_lo1",
        "projection_inverse_X64.Machine_s.OReg_r",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_GCTR.inc32lite", "typing_Prims.eq2",
        "typing_Types_s.add_wrap", "typing_Types_s.quad32",
        "typing_Types_s.reverse_bytes_quad32",
        "typing_Words_s.__proj__Mkfour__item__hi2",
        "typing_Words_s.__proj__Mkfour__item__hi3",
        "typing_Words_s.__proj__Mkfour__item__lo0",
        "typing_Words_s.__proj__Mkfour__item__lo1",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "unit_typing"
      ],
      0,
      "bb61d4fdaf9e9ba399f5f2eae8a573d4"
    ],
    [
      "X64.AESopt.va_wpMonotone_Handle_ctr32",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equality_tok_X64.Machine_s.R11@tok",
        "equation_X64.AESopt.va_wp_Handle_ctr32",
        "equation_X64.Machine_s.xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_tok_X64.Machine_s.R11@tok", "unit_typing"
      ],
      0,
      "3d4eda6fcd7448e444d7ac2c23bc0438"
    ],
    [
      "X64.AESopt.va_wpCompute_Handle_ctr32",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.AESopt.va_wp_Handle_ctr32",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "35e54d0a45f04909d6fed7ab70e9d862"
    ],
    [
      "X64.AESopt.va_wpProof_Handle_ctr32",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "ce19f53ad0eb98168729fdd3057e8403"
    ],
    [
      "X64.AESopt.va_wpProof_Handle_ctr32",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp", "equality_tok_X64.Machine_s.R11@tok",
        "equation_Prims.nat", "equation_Types_s.quad32",
        "equation_Words_s.nat32", "equation_Words_s.natN",
        "equation_X64.AESopt.va_wpCompute_Handle_ctr32",
        "equation_X64.AESopt.va_wp_Handle_ctr32",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.AESopt.va_wpCompute_Handle_ctr32",
        "typing_GCTR.inc32lite", "typing_Types_s.reverse_bytes_quad32",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Machine_s.R11@tok", "unit_typing"
      ],
      0,
      "fed40cff27db35263afc6ba2bf0f73d6"
    ],
    [
      "X64.AESopt.va_code_Loop6x_ctr_update",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_X64.Vale.Decls.TConst",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Vale.Decls.TStack",
        "equality_tok_X64.Machine_s.Rbx@tok", "primitive_Prims.op_BarBar",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "968ed3fa46a123865901e40c9719d498"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_ctr_update",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_X64.Vale.Decls.TConst",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Vale.Decls.TStack",
        "equality_tok_X64.Machine_s.Rbx@tok", "primitive_Prims.op_BarBar",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "d2201ef764da95817e977984c1526db2"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_ctr_update",
      2,
      1,
      0,
      [
        "@query", "constructor_distinct_X64.Vale.Decls.TConst",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Vale.Decls.TStack",
        "equality_tok_X64.Machine_s.Rbx@tok", "primitive_Prims.op_BarBar",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "a0c0d086d0a44c59a45b2ff76fff385b"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_ctr_update",
      3,
      1,
      0,
      [
        "@query", "constructor_distinct_X64.Vale.Decls.TConst",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Vale.Decls.TStack",
        "equality_tok_X64.Machine_s.Rbx@tok", "primitive_Prims.op_BarBar",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "9abd421105b7d90c30a81ed3e070c2ff"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_ctr_update",
      4,
      1,
      0,
      [
        "@query", "constructor_distinct_X64.Vale.Decls.TConst",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Vale.Decls.TStack",
        "equality_tok_X64.Machine_s.Rbx@tok", "primitive_Prims.op_BarBar",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "26689c2072242bc737d2ddbe29e8b121"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_ctr_update",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equation_Arch.Types.add_wrap_quad32", "equation_GCTR.inc32lite",
        "equation_GCTR_s.inc32", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Types_s.add_wrap",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.AESopt.aes_reqs", "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.State.state_eq",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "kinding_Words_s.four@tok",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_Words_s.Mkfour_hi2",
        "projection_inverse_Words_s.Mkfour_lo0",
        "projection_inverse_Words_s.Mkfour_lo1",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "string_typing", "typing_GCTR.inc32lite", "typing_Prims.eq2",
        "typing_Types_s.add_wrap", "typing_Types_s.quad32_xor",
        "typing_Types_s.reverse_bytes_quad32",
        "typing_Words_s.__proj__Mkfour__item__hi2",
        "typing_Words_s.__proj__Mkfour__item__hi3",
        "typing_Words_s.__proj__Mkfour__item__lo0",
        "typing_Words_s.__proj__Mkfour__item__lo1",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "typing_tok_X64.Machine_s.Rbx@tok", "unit_inversion", "unit_typing"
      ],
      0,
      "cd42b13474ca7840a236d35859cf4721"
    ],
    [
      "X64.AESopt.va_wpMonotone_Loop6x_ctr_update",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.Rbx@tok", "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wp_Loop6x_ctr_update",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_reg",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.Rbx@tok", "unit_typing"
      ],
      0,
      "6f4e42fc29fbf2fca989a00ea9623aac"
    ],
    [
      "X64.AESopt.va_wpCompute_Loop6x_ctr_update",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.AESopt.va_wp_Loop6x_ctr_update",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "2f632ca75c8056689b68c53a48e329b8"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_ctr_update",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "3a8cb7e286c6d2d2da46528f77e3cebc"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_ctr_update",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.Rbx@tok", "equation_AES_s.is_aes_key_LE",
        "equation_Prims.nat", "equation_Types_s.quad32",
        "equation_Words_s.nat32", "equation_Words_s.natN",
        "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wpCompute_Loop6x_ctr_update",
        "equation_X64.AESopt.va_wp_Loop6x_ctr_update",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "primitive_Prims.op_GreaterThanOrEqual",
        "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.AESopt.va_wpCompute_Loop6x_ctr_update",
        "typing_FStar.Seq.Base.length", "typing_GCTR.inc32lite",
        "typing_Types_s.quad32_xor", "typing_Types_s.reverse_bytes_quad32",
        "typing_Words_s.__proj__Mkfour__item__lo0",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.Rbx@tok", "unit_typing"
      ],
      0,
      "6244183724e255894e492b9c3141ea6c"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_preamble",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "15c58daccc2aa8797e675fe6468d99f6"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_preamble",
      2,
      1,
      0,
      [ "@query" ],
      0,
      "450ef21823ae2af6a1ba34c14d95ed4a"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_preamble",
      3,
      1,
      0,
      [ "@query" ],
      0,
      "6b3b14b432eb25fb40b01b7ba87f2f32"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_preamble",
      4,
      1,
      0,
      [ "@query" ],
      0,
      "b048b6c4a2f3b226a17ae14f19a60f0a"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_preamble",
      5,
      1,
      0,
      [ "@query" ],
      0,
      "024234d61aaa25b2a7cae9701f682fa2"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_preamble",
      6,
      1,
      0,
      [ "@query" ],
      0,
      "6578e9e2db0f681e1086489d05b49c87"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_preamble",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok", "equation_Types_s.quad32",
        "equation_Words_s.nat32", "equation_X64.AESopt.aes_reqs",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_45e5fdef08df05fe322ff9269c2cbb23"
      ],
      0,
      "0c49b94e05d11ec0edd6a2eee613fefb"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_preamble",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_AES_s.rounds.fuel_instrumented",
        "@fuel_irrelevance_AES_s.rounds.fuel_instrumented", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "constructor_distinct_AES_s.AES_128",
        "constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_AES_helpers.rounds_opaque", "equation_AES_s.round",
        "equation_GCTR.inc32lite", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_and",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Prop_s.prop0",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.AESopt.aes_reqs", "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.modifies_buffer_specific128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validDstAddrs128",
        "equation_X64.Vale.QuickCodes.range1",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_with_fuel_AES_s.rounds.fuel_instrumented",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "kinding_Words_s.four@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "lemma_X64.Memory.modifies_buffer_addr",
        "lemma_X64.Memory.modifies_buffer_elim",
        "lemma_X64.Memory.modifies_buffer_readable",
        "lemma_X64.Memory.modifies_valid_taint128",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_5bb8ca8bd1e34326f95f9f0f9a641acf",
        "refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
        "refinement_interpretation_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_interpretation_Tm_refine_fbd1322eaad6b0eab99798f0e8856c8e",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "token_correspondence_AES_s.rounds",
        "token_correspondence_Opaque_s.make_opaque",
        "typing_AES_helpers.rounds_opaque",
        "typing_AES_s.key_to_round_keys_LE", "typing_FStar.Seq.Base.index",
        "typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
        "typing_GCTR.inc32lite", "typing_Prims.eq2", "typing_Prims.l_and",
        "typing_Types_s.quad32_xor", "typing_Types_s.reverse_bytes_quad32",
        "typing_Words_s.__proj__Mkfour__item__lo0",
        "typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
        "typing_X64.Memory.buffer_readable",
        "typing_X64.Memory.buffer_write",
        "typing_X64.Memory.buffer_writeable", "typing_X64.Memory.loc_buffer",
        "typing_X64.Vale.Decls.modifies_buffer_specific128",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "typing_tok_AES_s.AES_128@tok",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.R8@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Secret@tok", "unit_inversion",
        "unit_typing"
      ],
      0,
      "dee44d431bad9d9528a2c8b5bb5bebb9"
    ],
    [
      "X64.AESopt.va_wp_Loop6x_preamble",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok", "equation_X64.AESopt.aes_reqs",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "9331c26264b63f84054b54e95ed8b623"
    ],
    [
      "X64.AESopt.va_wpMonotone_Loop6x_preamble",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.Rbx@tok", "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wp_Loop6x_preamble",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_reg",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.Rbx@tok", "unit_typing"
      ],
      0,
      "e9da7eb1dc67dc1ae929122aaf35559f"
    ],
    [
      "X64.AESopt.va_wpCompute_Loop6x_preamble",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.AESopt.va_wp_Loop6x_preamble",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "1894aa113f2e2462c3c20e37eae0a94d"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_preamble",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "9950d05cdc02d1e6759be50c54140c32"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_preamble",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.Rbx@tok", "equation_AES_s.is_aes_key_LE",
        "equation_Prims.nat", "equation_Types_s.quad32",
        "equation_Words_s.nat32", "equation_Words_s.natN",
        "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wpCompute_Loop6x_preamble",
        "equation_X64.AESopt.va_wp_Loop6x_preamble",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "kinding_Words_s.four@tok", "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "primitive_Prims.op_GreaterThanOrEqual",
        "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.AESopt.va_wpCompute_Loop6x_preamble",
        "typing_AES_helpers.rounds_opaque", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_GCTR.inc32lite",
        "typing_Types_s.quad32_xor", "typing_Types_s.reverse_bytes_quad32",
        "typing_Words_s.__proj__Mkfour__item__lo0",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.Rbx@tok", "unit_typing"
      ],
      0,
      "bb56846becd15ff2a0ccc1fdfc3945fa"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_plain",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_bbf6aaabf066c35e1c6263c0afb97782"
      ],
      0,
      "4a4a08ab77d3e31ce0649ee3ebf45dd4"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_plain",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_AES_s.rounds.fuel_instrumented",
        "@fuel_irrelevance_AES_s.rounds.fuel_instrumented", "@query",
        "AES_s_interpretation_Tm_arrow_064dee1312354c7b5865fa5195e69c07",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128",
        "constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equation_AES_helpers.rounds_opaque", "equation_AES_s.round",
        "equation_Prims.eq2", "equation_Prims.logical", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_X64.AESopt.aes_reqs",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCodes.range1",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_with_fuel_AES_s.rounds.fuel_instrumented",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_AES_s.rounds",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "kinding_Tm_arrow_064dee1312354c7b5865fa5195e69c07",
        "kinding_Words_s.four@tok",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_Equality",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "string_typing", "token_correspondence_AES_s.rounds",
        "token_correspondence_Opaque_s.make_opaque",
        "typing_AES_helpers.rounds_opaque", "typing_Opaque_s.make_opaque",
        "typing_Prims.eq2", "typing_X64.Memory.buffer_read",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.Rcx@tok", "unit_inversion", "unit_typing"
      ],
      0,
      "c466ef89c51e2b9aed39dcd70a68f663"
    ],
    [
      "X64.AESopt.va_wp_Loop6x_plain",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "33815da17e4dd685d4a551ccda489850"
    ],
    [
      "X64.AESopt.va_wpMonotone_Loop6x_plain",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok", "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wp_Loop6x_plain",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_xmm", "unit_typing"
      ],
      0,
      "bfde76edfb8cec9921309279988a6bf3"
    ],
    [
      "X64.AESopt.va_wpCompute_Loop6x_plain",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.AESopt.va_wp_Loop6x_plain",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "d55e34798fa35093054f567c671953ff"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_plain",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "b57f2caa8d92d70ce98f1578d235d526"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_plain",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wpCompute_Loop6x_plain",
        "equation_X64.AESopt.va_wp_Loop6x_plain",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.AESopt.va_wpCompute_Loop6x_plain",
        "typing_AES_helpers.rounds_opaque",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd", "unit_typing"
      ],
      0,
      "86fc2b986a31522cef3ebb93947eab11"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_step",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a4115a8651670d5c975ee9c0107164d2",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "8344336e7c3351bf9acc50237359e7ee"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_step",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_AES_s.rounds.fuel_instrumented",
        "@fuel_irrelevance_AES_s.rounds.fuel_instrumented", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128",
        "constructor_distinct_Interop.Types.TUInt128",
        "constructor_distinct_X64.Machine_s.R12",
        "constructor_distinct_X64.Machine_s.R13",
        "disc_equation_X64.Machine_s.Rsp", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_AES_helpers.rounds_opaque", "equation_AES_s.round",
        "equation_Prims.eq2", "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Prop_s.prop0",
        "equation_Types_s.quad32", "equation_Words_s.nat1",
        "equation_Words_s.nat32", "equation_Words_s.nat64",
        "equation_Words_s.natN", "equation_X64.AESopt.aes_reqs",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.modifies_buffer_specific128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_if",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.validDstAddrs128",
        "equation_X64.Vale.Decls.validSrcAddrsOffset128",
        "equation_X64.Vale.QuickCodes.range1",
        "equation_X64.Vale.State.state_eq",
        "equation_with_fuel_AES_s.rounds.fuel_instrumented",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "interpretation_Tm_abs_7de9de4ce40c4ef09e1222c646d4ae2e",
        "interpretation_Tm_abs_86acc984c8bb257ef46d29d7d1625394",
        "interpretation_Tm_abs_8d940294dd7dfa861a0650b209cbaa5c",
        "interpretation_Tm_abs_cd0b61e30476f8a91ec18a3c51e9865f",
        "interpretation_Tm_abs_ece100a30da5ef1508c6c7f4135ce97f",
        "kinding_Words_s.four@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "lemma_X64.Memory.loc_includes_refl",
        "lemma_X64.Memory.modifies_buffer_addr",
        "lemma_X64.Memory.modifies_buffer_readable",
        "lemma_X64.Memory.modifies_goal_directed_refl",
        "lemma_X64.Memory.modifies_goal_directed_trans",
        "lemma_X64.Memory.modifies_goal_directed_trans2",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThan", "proj_equation_X64.Machine_s.OReg_r",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_X64.Machine_s.OReg_r",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_5bb8ca8bd1e34326f95f9f0f9a641acf",
        "refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
        "refinement_interpretation_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "token_correspondence_AES_s.rounds",
        "token_correspondence_Opaque_s.make_opaque",
        "typing_AES_helpers.rounds_opaque",
        "typing_Arch.Types.insert_nat64_opaque",
        "typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
        "typing_Prims.eq2", "typing_Prims.l_and",
        "typing_Types_s.reverse_bytes_quad32",
        "typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
        "typing_X64.Memory.buffer_readable",
        "typing_X64.Memory.buffer_write",
        "typing_X64.Memory.buffer_writeable", "typing_X64.Memory.loc_buffer",
        "typing_X64.Vale.Decls.modifies_buffer_specific128",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rsp@tok", "unit_inversion", "unit_typing"
      ],
      0,
      "7df77e364c32cf5c98d55ec0e4fba9e7"
    ],
    [
      "X64.AESopt.va_wp_Loop6x_step",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "8e39b996a2f07215fb3f54b847b4ee03"
    ],
    [
      "X64.AESopt.va_wpMonotone_Loop6x_step",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok", "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wp_Loop6x_step",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_reg",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok", "unit_typing"
      ],
      0,
      "f22f2f161fc623f1835591545a9ae0cd"
    ],
    [
      "X64.AESopt.va_wpCompute_Loop6x_step",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.AESopt.va_wp_Loop6x_step",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "c574d8c829d4ed45a016cee22185860d"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_step",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "08b201bfec696bf83742c7533e559f41"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_step",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wpCompute_Loop6x_step",
        "equation_X64.AESopt.va_wp_Loop6x_step",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.AESopt.va_wpCompute_Loop6x_step",
        "typing_AES_helpers.rounds_opaque",
        "typing_X64.Vale.Decls.va_upd_ok", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok", "unit_typing"
      ],
      0,
      "1955f3d7108abfbb292bd29247c0ee09"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_round8",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_X64.AESopt.aes_reqs",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0761bfcd746a846ff436102b5ec81074",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "1c147a18bc25d419585fc05a6ff36cd9"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_round8",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_AES_s.rounds.fuel_instrumented",
        "@fuel_irrelevance_AES_s.rounds.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128",
        "constructor_distinct_Interop.Types.TUInt128",
        "constructor_distinct_X64.Machine_s.R12",
        "constructor_distinct_X64.Machine_s.R13",
        "disc_equation_X64.Machine_s.Rsp", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_AES_helpers.rounds_opaque", "equation_AES_s.round",
        "equation_Prims.eq2", "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Types_s.quad32",
        "equation_Words_s.nat32", "equation_Words_s.nat64",
        "equation_X64.AESopt.aes_reqs", "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_if",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.validSrcAddrsOffset128",
        "equation_X64.Vale.QuickCodes.range1",
        "equation_X64.Vale.State.state_eq",
        "equation_with_fuel_AES_s.rounds.fuel_instrumented",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32",
        "function_token_typing_Words_s.nat64", "int_inversion", "int_typing",
        "interpretation_Tm_abs_86acc984c8bb257ef46d29d7d1625394",
        "interpretation_Tm_abs_8d940294dd7dfa861a0650b209cbaa5c",
        "interpretation_Tm_abs_b363ac0f54118ceaaf81be2ede9b677f",
        "interpretation_Tm_abs_cb70b783f2aa66911456c1a189355281",
        "kinding_Words_s.four@tok",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_Equality", "proj_equation_X64.Machine_s.OReg_r",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_X64.Machine_s.OReg_r",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "token_correspondence_AES_s.rounds",
        "token_correspondence_Opaque_s.make_opaque",
        "typing_AES_helpers.rounds_opaque", "typing_Arch.Types.hi64",
        "typing_Arch.Types.lo64", "typing_Prims.eq2",
        "typing_Types_s.reverse_bytes_nat64",
        "typing_X64.Memory.buffer_read", "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.Rcx@tok", "unit_inversion", "unit_typing"
      ],
      0,
      "2525011aba0aa46484cfe70d16a9b48b"
    ],
    [
      "X64.AESopt.va_wp_Loop6x_round8",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok", "equation_X64.AESopt.aes_reqs",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "7fc8a022952ccd8321a939e653cd04fa"
    ],
    [
      "X64.AESopt.va_wpMonotone_Loop6x_round8",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok", "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wp_Loop6x_round8",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_reg",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok", "unit_typing"
      ],
      0,
      "03922e3e3d50203b1cdef292b805edb9"
    ],
    [
      "X64.AESopt.va_wpCompute_Loop6x_round8",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.AESopt.va_wp_Loop6x_round8",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "f564417435c9a99417da114e480e8016"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_round8",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "26c9a6a8178354ca65171ae30993dfe2"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_round8",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wpCompute_Loop6x_round8",
        "equation_X64.AESopt.va_wp_Loop6x_round8",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "kinding_Words_s.four@tok", "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.AESopt.va_wpCompute_Loop6x_round8",
        "typing_AES_helpers.rounds_opaque", "typing_FStar.Seq.Base.index",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok", "unit_typing"
      ],
      0,
      "a6d20d55be96a2aa3774223ff248635d"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_round9",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_X64.AESopt.aes_reqs",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_30d96b51d0a5d15d756fac5472edccaf",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "e61d2b40aba900808b2cab4b5956ae12"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_round9",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_AES_s.rounds.fuel_instrumented",
        "@fuel_irrelevance_AES_s.rounds.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128",
        "constructor_distinct_Interop.Types.TUInt128",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Vale.Decls.TReg", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_AES_helpers.rounds_opaque", "equation_AES_s.round",
        "equation_Prims.eq2", "equation_Prims.l_and",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Types_s.quad32",
        "equation_Types_s.quad32_xor", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_X64.AESopt.aes_reqs",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validSrcAddrsOffset128",
        "equation_X64.Vale.QuickCodes.range1",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_with_fuel_AES_s.rounds.fuel_instrumented",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32", "int_typing",
        "kinding_Words_s.four@tok", "l_and-interp",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_Equality",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_X64.Vale.Decls.TReg_r",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "token_correspondence_AES_s.rounds",
        "token_correspondence_Opaque_s.make_opaque",
        "typing_AES_helpers.rounds_opaque", "typing_Prims.eq2",
        "typing_X64.Memory.buffer_read", "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok", "unit_inversion", "unit_typing"
      ],
      0,
      "6894ae59219a03b7aa12013e6841fbf2"
    ],
    [
      "X64.AESopt.va_wp_Loop6x_round9",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok", "equation_X64.AESopt.aes_reqs",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "1d438559598631d23f1d3911a953026f"
    ],
    [
      "X64.AESopt.va_wpMonotone_Loop6x_round9",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok", "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wp_Loop6x_round9",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_xmm", "unit_typing"
      ],
      0,
      "a9f004ea81027ba2e85e0904af1959f4"
    ],
    [
      "X64.AESopt.va_wpCompute_Loop6x_round9",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.AESopt.va_wp_Loop6x_round9",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "6e20b27700fce31544fecc58973f7287"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_round9",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "eaae859d9d1ac7c28928f2627b25a1a3"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_round9",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wpCompute_Loop6x_round9",
        "equation_X64.AESopt.va_wp_Loop6x_round9",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.AESopt.va_wpCompute_Loop6x_round9",
        "typing_AES_helpers.rounds_opaque",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd", "unit_typing"
      ],
      0,
      "87c0a4a19d494c83f43dc4448e9d465f"
    ],
    [
      "X64.AESopt.va_lemma_load_one_msb",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_X64.Machine_s.R11",
        "data_typing_intro_Words_s.Mktwo@tok",
        "disc_equation_X64.Machine_s.Rsp", "eq2-interp",
        "equality_tok_X64.Machine_s.R11@tok",
        "equation_Arch.Types.insert_nat64_opaque", "equation_Prims.eq2",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
        "equation_Types_s.insert_nat64", "equation_Types_s.quad32",
        "equation_Words.Four_s.two_two_to_four",
        "equation_Words.Two_s.nat_to_two", "equation_Words.Two_s.two_insert",
        "equation_Words.Two_s.two_to_nat", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.State.state_eq",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Opaque_s.make_opaque",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "lemma_Arch.Types.lemma_insert_nat64_properties",
        "lemma_FStar.UInt.pow2_values",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Machine_s.OReg_r",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_Words_s.Mkfour_hi2",
        "projection_inverse_Words_s.Mkfour_hi3",
        "projection_inverse_Words_s.Mkfour_lo0",
        "projection_inverse_Words_s.Mkfour_lo1",
        "projection_inverse_Words_s.Mktwo_hi",
        "projection_inverse_Words_s.Mktwo_lo",
        "projection_inverse_X64.Machine_s.OReg_r",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "refinement_interpretation_Tm_refine_1bc5c4f392722fe6a26189e86f17c270",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "token_correspondence_Types_s.insert_nat64",
        "typing_Prims.pow2", "typing_Words.Two_s.two_to_nat",
        "typing_Words_s.int_to_natN", "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "unit_inversion", "unit_typing"
      ],
      0,
      "bf07eab2e2e3828d96e7f34d17a43446"
    ],
    [
      "X64.AESopt.va_wpMonotone_load_one_msb",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equality_tok_X64.Machine_s.R11@tok",
        "equation_X64.AESopt.va_wp_load_one_msb",
        "equation_X64.Machine_s.xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_tok_X64.Machine_s.R11@tok", "unit_typing"
      ],
      0,
      "d9cd5c00de361abe4b266e6c9b024bbc"
    ],
    [
      "X64.AESopt.va_wpCompute_load_one_msb",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.AESopt.va_wp_load_one_msb",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "dabbda084ef99603a80e00a4789f3627"
    ],
    [
      "X64.AESopt.va_wpProof_load_one_msb",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "0134dc3a2d3565a8208de0a6573784b4"
    ],
    [
      "X64.AESopt.va_wpProof_load_one_msb",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp", "equality_tok_X64.Machine_s.R11@tok",
        "equation_X64.AESopt.va_wpCompute_load_one_msb",
        "equation_X64.AESopt.va_wp_load_one_msb",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.AESopt.va_wpCompute_load_one_msb",
        "typing_X64.Vale.Decls.va_upd_ok", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Machine_s.R11@tok", "unit_typing"
      ],
      0,
      "e32ba0cbad17dd48bb1b977ae7623ba7"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_final",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_AES_s.AES_128",
        "disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
        "fuel_guarded_inversion_AES_s.algorithm",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "4329cc4d4fe6d1d0904fa0f5db5b834d"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_final",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_AES_s.AES_128",
        "disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
        "fuel_guarded_inversion_AES_s.algorithm",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "234353d6739d524ac866146b9be24408"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_final",
      3,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_AES_s.AES_128",
        "disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
        "fuel_guarded_inversion_AES_s.algorithm",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "cf8b80e4820e5ba944753741ff94aeae"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_final",
      4,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_AES_s.AES_128",
        "disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
        "fuel_guarded_inversion_AES_s.algorithm",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "c5e8606cdd6623804f07a21de834d6a6"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_final",
      5,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_AES_s.AES_128",
        "disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
        "fuel_guarded_inversion_AES_s.algorithm",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "b15baa98e1436b80f45d20dc1c608f12"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_final",
      6,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_AES_s.AES_128",
        "disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
        "fuel_guarded_inversion_AES_s.algorithm",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "282e8ca23e30718f2881bda8d6c84f10"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_final",
      7,
      1,
      0,
      [ "@query" ],
      0,
      "c2048867da553e045548a0eb061dfcdd"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_final",
      8,
      1,
      0,
      [ "@query" ],
      0,
      "4365aa005982958c3afc00f251530ccb"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_final",
      9,
      1,
      0,
      [ "@query" ],
      0,
      "6b9e15dc0de83569eac7e623eba7bdd2"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_final",
      10,
      1,
      0,
      [ "@query" ],
      0,
      "460eb6177562dc0c759ddaf12f064ded"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_final",
      11,
      1,
      0,
      [ "@query" ],
      0,
      "fcd4467247a3426ae2035e680f58fd5f"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x_final",
      12,
      1,
      0,
      [ "@query" ],
      0,
      "4a8607044a391d149fe86082bf93099f"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_final",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok", "equation_Types_s.quad32",
        "equation_Words_s.nat32", "equation_X64.AESopt.aes_reqs",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ff5e448c7b9a56585393459ba884bd5b"
      ],
      0,
      "466f372bdf0162f3c1a251358ebccef1"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_final",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "constructor_distinct_AES_s.AES_128",
        "constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_Arch.Types.add_wrap_quad32",
        "equation_GCTR.aes_encrypt_le", "equation_GCTR.inc32lite",
        "equation_GCTR_s.inc32", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_and",
        "equation_Prims.l_imp", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Prop_s.prop0", "equation_Types_s.add_wrap",
        "equation_Types_s.quad32", "equation_Words_s.nat1",
        "equation_Words_s.nat32", "equation_Words_s.nat64",
        "equation_Words_s.natN", "equation_X64.AESopt.aes_reqs",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.modifies_buffer_specific128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_if",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.validDstAddrs128",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.QuickCodes.range1",
        "equation_X64.Vale.State.state_eq",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "interpretation_Tm_abs_86acc984c8bb257ef46d29d7d1625394",
        "interpretation_Tm_abs_8d940294dd7dfa861a0650b209cbaa5c",
        "interpretation_Tm_abs_ece100a30da5ef1508c6c7f4135ce97f",
        "kinding_Words_s.four@tok", "l_and-interp", "l_imp-interp",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "lemma_X64.Memory.loc_includes_refl",
        "lemma_X64.Memory.modifies_buffer_addr",
        "lemma_X64.Memory.modifies_buffer_elim",
        "lemma_X64.Memory.modifies_buffer_readable",
        "lemma_X64.Memory.modifies_goal_directed_refl",
        "lemma_X64.Memory.modifies_goal_directed_trans",
        "lemma_X64.Memory.modifies_goal_directed_trans2",
        "lemma_X64.Memory.modifies_valid_taint128",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_Words_s.Mkfour_hi2",
        "projection_inverse_Words_s.Mkfour_hi3",
        "projection_inverse_Words_s.Mkfour_lo0",
        "projection_inverse_Words_s.Mkfour_lo1",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_5bb8ca8bd1e34326f95f9f0f9a641acf",
        "refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
        "refinement_interpretation_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_Arch.Types.insert_nat64_opaque",
        "typing_FStar.Seq.Base.index",
        "typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
        "typing_GCTR.aes_encrypt_le", "typing_Prims.eq2",
        "typing_Prims.l_and", "typing_Types_s.add_wrap",
        "typing_Types_s.quad32_xor", "typing_Types_s.reverse_bytes_quad32",
        "typing_Words_s.__proj__Mkfour__item__hi2",
        "typing_Words_s.__proj__Mkfour__item__hi3",
        "typing_Words_s.__proj__Mkfour__item__lo0",
        "typing_Words_s.__proj__Mkfour__item__lo1",
        "typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
        "typing_X64.Memory.buffer_readable",
        "typing_X64.Memory.buffer_write",
        "typing_X64.Memory.buffer_writeable", "typing_X64.Memory.loc_buffer",
        "typing_X64.Vale.Decls.modifies_buffer_specific128",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "typing_tok_AES_s.AES_128@tok",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R8@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok",
        "typing_tok_X64.Machine_s.Secret@tok", "unit_inversion",
        "unit_typing"
      ],
      0,
      "4e4576e57bd3682084181c36465ad5fe"
    ],
    [
      "X64.AESopt.va_wp_Loop6x_final",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok", "equation_X64.AESopt.aes_reqs",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "c6b1eb3fb3cb9258f3dd9aa2e19980cc"
    ],
    [
      "X64.AESopt.va_wpMonotone_Loop6x_final",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rsi@tok", "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wp_Loop6x_final",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_reg",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "f2fb10bbade6e90ee53f102fb4a133f4"
    ],
    [
      "X64.AESopt.va_wpCompute_Loop6x_final",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.AESopt.va_wp_Loop6x_final",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "e141b986f5c4c7315d4a60937efc4ebc"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_final",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "3a5387783ded7cfcb31b442dcdb1770e"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_final",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rsi@tok", "equation_GCTR.aes_encrypt_le",
        "equation_Prims.nat", "equation_Types_s.quad32",
        "equation_Words_s.nat32", "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wpCompute_Loop6x_final",
        "equation_X64.AESopt.va_wp_Loop6x_final",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32", "int_typing",
        "kinding_Words_s.four@tok", "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.AESopt.va_wpCompute_Loop6x_final",
        "typing_FStar.Seq.Base.index", "typing_GCTR.aes_encrypt_le",
        "typing_Types_s.quad32_xor", "typing_Types_s.reverse_bytes_quad32",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.State.update_reg", "typing_X64.Vale.Xmms.sel",
        "typing_X64.Vale.Xmms.upd", "typing_tok_AES_s.AES_128@tok",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "8a4b41cd48730e86c9e880d9d7018722"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_save_output",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "aee8b7ee53c9bd5f4a178d43ed377cff"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_save_output",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Prop_s.prop0",
        "equation_Types_s.quad32", "equation_Words_s.nat64",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.modifies_buffer_specific128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validDstAddrsOffset128",
        "equation_X64.Vale.QuickCodes.range1",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "lemma_FStar.Seq.Properties.slice_upd",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "lemma_X64.Memory.loc_includes_refl",
        "lemma_X64.Memory.modifies_buffer_addr",
        "lemma_X64.Memory.modifies_buffer_readable",
        "lemma_X64.Memory.modifies_goal_directed_refl",
        "lemma_X64.Memory.modifies_goal_directed_trans",
        "lemma_X64.Memory.modifies_goal_directed_trans2",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_5bb8ca8bd1e34326f95f9f0f9a641acf",
        "refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
        "refinement_interpretation_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "string_typing", "typing_FStar.Seq.Base.seq",
        "typing_FStar.Seq.Base.upd",
        "typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
        "typing_Prims.eq2", "typing_Prims.l_and", "typing_Types_s.quad32",
        "typing_Types_s.quad32_xor", "typing_Workarounds.slice_work_around",
        "typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
        "typing_X64.Memory.buffer_readable",
        "typing_X64.Memory.buffer_write",
        "typing_X64.Memory.buffer_writeable", "typing_X64.Memory.loc_buffer",
        "typing_X64.Vale.Decls.modifies_buffer_specific128",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "c5abcbf76c488da365fc2c7ca35cef03"
    ],
    [
      "X64.AESopt.va_wp_Loop6x_save_output",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "c08a9575a5368a2050981c83d73240ee"
    ],
    [
      "X64.AESopt.va_wpMonotone_Loop6x_save_output",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_X64.AESopt.va_wp_Loop6x_save_output",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_xmm", "unit_typing"
      ],
      0,
      "bcf22077df6e464db42b60b5264c85d7"
    ],
    [
      "X64.AESopt.va_wpCompute_Loop6x_save_output",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.AESopt.va_wp_Loop6x_save_output",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "21399808f8ce536a277ed5691c2f9c49"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_save_output",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "769f9f142170f79f12e1e04333d9bb1d"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_save_output",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp", "equation_Prims.nat",
        "equation_X64.AESopt.va_wpCompute_Loop6x_save_output",
        "equation_X64.AESopt.va_wp_Loop6x_save_output",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.AESopt.va_wpCompute_Loop6x_save_output",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.State.update_xmm", "typing_X64.Vale.Xmms.sel",
        "typing_X64.Vale.Xmms.upd", "unit_typing"
      ],
      0,
      "31e8340101100a71e41fa6c2699de8e2"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_partial",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_X64.AESopt.aes_reqs",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0f0d6ff57c990c11cdd21dda0051928e",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "14b4b0b3518adf014bf5dc65204cd00b"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x_partial",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128",
        "constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_AES_helpers.rounds_opaque", "equation_AES_s.is_aes_key_LE",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.l_and", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Prop_s.prop0", "equation_Types_s.quad32",
        "equation_Types_s.quad32_xor", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.AESopt.aes_reqs", "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.buffer_modifies_specific128",
        "equation_X64.Vale.Decls.modifies_buffer_specific128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.validDstAddrs128",
        "equation_X64.Vale.Decls.validSrcAddrsOffset128",
        "equation_X64.Vale.QuickCodes.range1",
        "equation_X64.Vale.State.state_eq",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Types_s.quad32_xor_def",
        "function_token_typing_Words_s.nat32",
        "function_token_typing_Words_s.nat64", "int_inversion", "int_typing",
        "kinding_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "kinding_Words_s.four@tok", "l_and-interp",
        "lemma_X64.Memory.loc_includes_refl",
        "lemma_X64.Memory.loc_includes_union_l_buffer",
        "lemma_X64.Memory.modifies_buffer_addr",
        "lemma_X64.Memory.modifies_buffer_elim",
        "lemma_X64.Memory.modifies_buffer_readable",
        "lemma_X64.Memory.modifies_goal_directed_refl",
        "lemma_X64.Memory.modifies_goal_directed_trans",
        "lemma_X64.Memory.modifies_goal_directed_trans2",
        "lemma_X64.Memory.modifies_valid_taint128",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple6__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple6__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple6__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple6__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple6__5",
        "projection_inverse_FStar.Pervasives.Native.Mktuple6__6",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_interpretation_Tm_refine_fbd1322eaad6b0eab99798f0e8856c8e",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "token_correspondence_Opaque_s.make_opaque",
        "typing_AES_s.key_to_round_keys_LE", "typing_Arch.Types.hi64",
        "typing_Arch.Types.lo64", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_GCTR.inc32lite",
        "typing_Opaque_s.make_opaque", "typing_Prims.eq2",
        "typing_Types_s.quad32_xor", "typing_Types_s.reverse_bytes_nat64",
        "typing_Types_s.reverse_bytes_quad32",
        "typing_X64.Memory.buffer_read", "typing_X64.Memory.loc_buffer",
        "typing_X64.Memory.loc_union", "typing_X64.Memory.modifies",
        "typing_X64.Vale.Decls.buffer_modifies_specific128",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "typing_tok_AES_s.AES_128@tok",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.R8@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok",
        "typing_tok_X64.Machine_s.Secret@tok", "unit_typing"
      ],
      0,
      "ef81eb5ad02d1712e91479551568faa8"
    ],
    [
      "X64.AESopt.va_wp_Loop6x_partial",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok", "equation_X64.AESopt.aes_reqs",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "68c83bfc90a230e07213522ebb77889a"
    ],
    [
      "X64.AESopt.va_wpMonotone_Loop6x_partial",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_AES_s.AES_128",
        "constructor_distinct_X64.Machine_s.R11",
        "constructor_distinct_X64.Machine_s.R12",
        "constructor_distinct_X64.Machine_s.R13",
        "constructor_distinct_X64.Machine_s.Rbx",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple6@tok",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.Rbx@tok", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wp_Loop6x_partial",
        "equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "kinding_Words_s.four@tok", "lemma_X64.Vale.Regs.lemma_upd_eq",
        "lemma_X64.Vale.Regs.lemma_upd_ne",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.Rbx@tok"
      ],
      0,
      "4d9f8b20acf4d834d20a9c3bbcf3aa2a"
    ],
    [
      "X64.AESopt.va_wpCompute_Loop6x_partial",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.AESopt.va_wp_Loop6x_partial",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "05f9f8e0b2e562735adc455421f65764"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_partial",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "95203e11d3c0d881b43e59f2fee6908a"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x_partial",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_AES_s.AES_128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.Rbx@tok", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_Words_s.natN", "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wpCompute_Loop6x_partial",
        "equation_X64.AESopt.va_wp_Loop6x_partial",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "primitive_Prims.op_GreaterThanOrEqual",
        "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.AESopt.va_wpCompute_Loop6x_partial",
        "typing_AES_helpers.rounds_opaque",
        "typing_Words_s.__proj__Mkfour__item__lo0",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.Rbx@tok"
      ],
      0,
      "083f174f2dad50d11fb2ab6db3b8813a"
    ],
    [
      "X64.AESopt.va_code_Loop6x",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_X64.Vale.Decls.TConst",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Vale.Decls.TStack",
        "equality_tok_X64.Machine_s.Rdx@tok", "primitive_Prims.op_BarBar",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "4dbe428d2378c7566c01c1312a361b5f"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_X64.Vale.Decls.TConst",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Vale.Decls.TStack",
        "equality_tok_X64.Machine_s.Rdx@tok", "equation_Prims.nat",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "48ae92e9baff1162fcf62f67760e87d2"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x",
      2,
      1,
      0,
      [
        "@query", "constructor_distinct_X64.Vale.Decls.TConst",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Vale.Decls.TStack",
        "equality_tok_X64.Machine_s.Rdx@tok", "primitive_Prims.op_BarBar",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "127c9a6ebf4738906ddc1748b08137ef"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x",
      3,
      1,
      0,
      [
        "@query", "constructor_distinct_X64.Vale.Decls.TConst",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Vale.Decls.TStack",
        "equality_tok_X64.Machine_s.Rdx@tok", "primitive_Prims.op_BarBar",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "0ba27cedb47ab8795e4daf634a8a77ac"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x",
      4,
      1,
      0,
      [
        "@query", "constructor_distinct_X64.Vale.Decls.TConst",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Vale.Decls.TStack",
        "equality_tok_X64.Machine_s.Rdx@tok", "primitive_Prims.op_BarBar",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "ec52fac5d30a580fe82a7b87064734d1"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x",
      5,
      1,
      0,
      [
        "@query", "constructor_distinct_X64.Vale.Decls.TConst",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Vale.Decls.TStack",
        "equality_tok_X64.Machine_s.Rdx@tok", "primitive_Prims.op_BarBar",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "f18897a97682a70e8000b1fb9aaf4e1b"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x",
      6,
      1,
      0,
      [
        "@query", "constructor_distinct_X64.Vale.Decls.TConst",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Vale.Decls.TStack",
        "equality_tok_X64.Machine_s.Rdx@tok", "primitive_Prims.op_BarBar",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "efba35348757dbe3297b3c0075a1fc02"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x",
      7,
      1,
      0,
      [
        "@query", "constructor_distinct_X64.Vale.Decls.TConst",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Vale.Decls.TStack",
        "equality_tok_X64.Machine_s.Rdx@tok", "primitive_Prims.op_BarBar",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "e43bd77d03a476a67558470f9ad5b05a"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x",
      8,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_X64.Vale.Decls.va_int_at_least",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_47109dd5837e560f72664f314778a899"
      ],
      0,
      "0b649d031e366dd40ce072ebe084b21d"
    ],
    [
      "X64.AESopt.va_qcode_Loop6x",
      9,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_X64.Vale.Decls.va_int_at_least",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_47109dd5837e560f72664f314778a899"
      ],
      0,
      "e4c3fca76d3f48a8b6b90d9f9154ed8c"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_X64.AESopt.aes_reqs",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_e365606f151599b3d5334779b2e56ca8"
      ],
      0,
      "6c5f2ac2dc9055e7e47be51abb155318"
    ],
    [
      "X64.AESopt.va_lemma_Loop6x",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "constructor_distinct_AES_s.AES_128",
        "constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.R10@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_AES_s.is_aes_key_LE", "equation_GCTR.aes_encrypt_BE",
        "equation_GCTR.inc32lite", "equation_GCTR.partial_seq_agreement",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.l_imp", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Prop_s.prop0", "equation_Types_s.quad32",
        "equation_Words_s.nat32", "equation_Words_s.nat64",
        "equation_Words_s.natN", "equation_X64.AESopt.aes_reqs",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.buffer_modifies_specific128",
        "equation_X64.Vale.Decls.modifies_buffer_specific128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validDstAddrs128",
        "equation_X64.Vale.Decls.validDstAddrsOffset128",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.Decls.validSrcAddrsOffset128",
        "equation_X64.Vale.QuickCodes.range1",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Words_s.nat32",
        "function_token_typing_Words_s.nat64", "int_inversion", "int_typing",
        "kinding_Words_s.four@tok", "l_imp-interp",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "lemma_X64.Memory.loc_disjoint_union_r",
        "lemma_X64.Memory.loc_includes_refl",
        "lemma_X64.Memory.loc_includes_union_l_buffer",
        "lemma_X64.Memory.loc_includes_union_r",
        "lemma_X64.Memory.modifies_buffer_addr",
        "lemma_X64.Memory.modifies_buffer_elim",
        "lemma_X64.Memory.modifies_buffer_readable",
        "lemma_X64.Memory.modifies_goal_directed_refl",
        "lemma_X64.Memory.modifies_goal_directed_trans",
        "lemma_X64.Memory.modifies_goal_directed_trans2",
        "lemma_X64.Memory.modifies_valid_taint128",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_Words_s.Mkfour_hi2",
        "projection_inverse_Words_s.Mkfour_hi3",
        "projection_inverse_Words_s.Mkfour_lo0",
        "projection_inverse_Words_s.Mkfour_lo1",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_6d2333afbb8ce899cd8937b56b09e98d",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_interpretation_Tm_refine_fbd1322eaad6b0eab99798f0e8856c8e",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_AES_s.key_to_round_keys_LE",
        "typing_FStar.Seq.Base.length", "typing_GCTR.aes_encrypt_BE",
        "typing_GCTR.inc32lite", "typing_Prims.eq2", "typing_Prims.l_imp",
        "typing_Types_s.quad32_xor", "typing_Types_s.reverse_bytes_quad32",
        "typing_Words_s.__proj__Mkfour__item__lo0",
        "typing_Workarounds.slice_work_around",
        "typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
        "typing_X64.Memory.loc_buffer", "typing_X64.Memory.loc_union",
        "typing_X64.Memory.modifies",
        "typing_X64.Vale.Decls.buffer_modifies_specific128",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "typing_tok_AES_s.AES_128@tok",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.R10@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.R15@tok",
        "typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
        "typing_tok_X64.Machine_s.Rax@tok",
        "typing_tok_X64.Machine_s.Rbp@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok",
        "typing_tok_X64.Machine_s.Secret@tok", "unit_inversion",
        "unit_typing"
      ],
      0,
      "958f60fdd93df67a5fc5c1aaceabe785"
    ],
    [
      "X64.AESopt.va_wp_Loop6x",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok", "equation_X64.AESopt.aes_reqs",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "8832504cfc00fab7c547c0989b0269e0"
    ],
    [
      "X64.AESopt.va_wpMonotone_Loop6x",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_AES_s.AES_128",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok", "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wp_Loop6x", "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_upd_reg",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "d4de3eed174ffc4f70082110e7e277e2"
    ],
    [
      "X64.AESopt.va_wpCompute_Loop6x",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.AESopt.va_wp_Loop6x",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "2060d6940ac4b176d4d781e9e101a5c1"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "55ba6fb05f76ada3d6f47ccccb6c1c66"
    ],
    [
      "X64.AESopt.va_wpProof_Loop6x",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_AES_s.AES_128", "eq2-interp",
        "equality_tok_AES_s.AES_128@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_X64.AESopt.aes_reqs",
        "equation_X64.AESopt.va_wpCompute_Loop6x",
        "equation_X64.AESopt.va_wp_Loop6x", "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_stack",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_stack",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.AESopt.va_wpCompute_Loop6x",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.State.update_reg", "typing_X64.Vale.Xmms.sel",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "35a52ee52c975ad589d1aa86d54f0c0a"
    ]
  ]
]