Revision - b5e8596 - File at least verifies now; some lemmas broke though which we [...]

Revision b5e85960e109efb08b9c65a4ab85c9b4ef926419 authored by Jay Bosamiya on 04 June 2019, 18:24:09 UTC, committed by Jay Bosamiya on 04 June 2019, 18:24:09 UTC

File at least verifies now; some lemmas broke though which we need to fix

1 parent 2a5defc

Files
Changes

Permalinks

Vale.AES.X64.GCMencrypt.fst.hints

[
  "\u0013��A��夆z\u0003�G�YP",
  [
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass_blocks_body",
      1,
      1,
      0,
      [
        "@query", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "e07fa074020f494300fcf7d65ccf6845"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_one_pass_blocks_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "e600e47076b3ba507d775dd007b179bc"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_one_pass_blocks_body",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256",
        "constructor_distinct_Vale.Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_Prims.LexTop@tok",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_and",
        "equation_Prims.l_imp", "equation_Prims.logical",
        "equation_Prims.min", "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR.aes_encrypt_BE",
        "equation_Vale.AES.GCTR.aes_encrypt_le",
        "equation_Vale.AES.GCTR.gctr_partial",
        "equation_Vale.AES.GCTR_s.inc32",
        "equation_Vale.AES.GHash.ghash_incremental0",
        "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Decls.validDstAddrsOffset128",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrsOffset128",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.QuickCodes.lexCons",
        "equation_Vale.X64.QuickCodes.precedes_wrap",
        "equation_Vale.X64.QuickCodes.range1",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.state_eta",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Prims.l_and",
        "function_token_typing_Vale.AES.AES_s.aes_encrypt_LE_def",
        "function_token_typing_Vale.Def.Opaque_s.make_opaque",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Prims.equals@tok",
        "kinding_Vale.Def.Words_s.four@tok", "l_and-interp", "l_imp-interp",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_upd",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.Memory.loc_includes_refl",
        "lemma_Vale.X64.Memory.modifies_buffer_addr",
        "lemma_Vale.X64.Memory.modifies_buffer_elim",
        "lemma_Vale.X64.Memory.modifies_buffer_readable",
        "lemma_Vale.X64.Memory.modifies_goal_directed_refl",
        "lemma_Vale.X64.Memory.modifies_goal_directed_trans",
        "lemma_Vale.X64.Memory.modifies_goal_directed_trans2",
        "lemma_Vale.X64.Memory.modifies_valid_taint128",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Xmms.lemma_equal_intro",
        "lemma_Vale.X64.Xmms.lemma_eta", "primitive_Prims.op_Addition",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.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_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
        "refinement_interpretation_Tm_refine_09d9ae2b4f83e9874aa98bae7c20bcb4",
        "refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
        "refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
        "refinement_interpretation_Tm_refine_6d2333afbb8ce899cd8937b56b09e98d",
        "refinement_interpretation_Tm_refine_809440a2e49ae18d732467ba1f4c9c0b",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.op_At_Bar", "typing_FStar.Seq.Base.seq",
        "typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
        "typing_Prims.eq2", "typing_Prims.l_and", "typing_Prims.l_imp",
        "typing_Prims.squash", "typing_Vale.AES.GCTR.gctr_partial",
        "typing_Vale.AES.GCTR_s.inc32",
        "typing_Vale.AES.GHash.ghash_incremental0",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_Vale.Lib.Workarounds.slice_work_around",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.validDstAddrsOffset128",
        "typing_Vale.X64.Decls.validSrcAddrs128",
        "typing_Vale.X64.Decls.validSrcAddrsOffset128",
        "typing_Vale.X64.Memory.buffer_addr",
        "typing_Vale.X64.Memory.buffer_as_seq",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.Memory.buffer_readable",
        "typing_Vale.X64.Memory.buffer_write",
        "typing_Vale.X64.Memory.buffer_writeable",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.lexCons",
        "typing_Vale.X64.QuickCodes.precedes_wrap",
        "typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd",
        "typing_Vale.X64.State.__proj__Mkstate__item__flags",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__memTaint",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.State.state_eta", "typing_Vale.X64.Xmms.eta_sel",
        "typing_Vale.X64.Xmms.sel", "typing_tok_Prims.LexTop@tok",
        "typing_tok_Vale.AES.AES_s.AES_128@tok",
        "typing_tok_Vale.AES.AES_s.AES_256@tok",
        "typing_tok_Vale.Interop.Types.TUInt128@tok",
        "typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_inversion",
        "unit_typing", "well-founded-ordering-on-nat"
      ],
      0,
      "ebdd899349087fa468c1acd7691272a0"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "b2d009f4c54947b5c10f1e5b7cb1690c"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpMonotone_gcm_one_pass_blocks_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks_body",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm", "unit_typing"
      ],
      0,
      "e17755c59e6fabdb5126cf4792376dca"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass_blocks_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks_body",
        "equation_Vale.X64.Decls.va_require_total",
        "fuel_guarded_inversion_Vale.X64.State.state"
      ],
      0,
      "a3ad3bd122954b8161f1b67533a0a453"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_one_pass_blocks_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "605fbe977d1f6f23ddc43ee31fa897a9"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_one_pass_blocks_body",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Vale.AES.AES_s.AES_128", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass_blocks_body",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks_body",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Decls.validDstAddrsOffset128",
        "equation_Vale.X64.Decls.validSrcAddrsOffset128",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_Vale.X64.Memory.modifies_buffer_addr",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Xmms.lemma_equal_elim",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.X64.State.Mkstate_flags",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_stack",
        "projection_inverse_Vale.X64.State.Mkstate_stackTaint",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass_blocks_body",
        "typing_FStar.Seq.Base.length", "typing_Vale.AES.GCTR_s.inc32",
        "typing_Vale.AES.GHash.ghash_incremental0",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_Vale.Lib.Workarounds.slice_work_around",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm",
        "typing_Vale.X64.Memory.buffer_as_seq",
        "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.Regs.upd",
        "typing_Vale.X64.State.__proj__Mkstate__item__flags",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.sel",
        "typing_tok_Vale.Interop.Types.TUInt128@tok", "unit_typing"
      ],
      0,
      "a5540e10dc0d88146cfc2d6098767d69"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_code_gcm_one_pass_blocks_while",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "8e6fad40b537ef2785a5694c77f0a833"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass_blocks_while",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack", "equation_Prims.nat",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "fdec0866348b66e3ef86df2e19c35af7"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass_blocks_while",
      2,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "10a2ab0e153256dfe46cdeaa905138aa"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass_blocks_while",
      3,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "641f7f49370b8e4c2860355714da8e83"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_one_pass_blocks_while",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "45e0b14b5bf55af981c5079935e57076"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_one_pass_blocks_while",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "bool_typing", "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256",
        "constructor_distinct_Vale.Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_Prims.LexTop@tok",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_imp",
        "equation_Prims.l_not", "equation_Prims.logical",
        "equation_Prims.min", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR.gctr_partial",
        "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Decls.validDstAddrsOffset128",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrsOffset128",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.QuickCodes.lexCons",
        "equation_Vale.X64.QuickCodes.precedes_wrap",
        "equation_Vale.X64.QuickCodes.range1",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.state_eta",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Prims.l_and",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
        "int_typing", "kinding_Prims.equals@tok",
        "kinding_Vale.Def.Words_s.four@tok", "l_and-interp", "l_imp-interp",
        "l_not-interp", "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.Memory.modifies_buffer_addr",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Xmms.lemma_equal_intro",
        "lemma_Vale.X64.Xmms.lemma_eta", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.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_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_09d9ae2b4f83e9874aa98bae7c20bcb4",
        "refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "string_typing", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.seq", "typing_Prims.eq2",
        "typing_Prims.l_and", "typing_Prims.l_imp", "typing_Prims.l_not",
        "typing_Prims.squash", "typing_Vale.AES.GCTR.gctr_partial",
        "typing_Vale.AES.GCTR_s.inc32",
        "typing_Vale.AES.GHash.ghash_incremental0",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_Vale.Lib.Workarounds.slice_work_around",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.validDstAddrsOffset128",
        "typing_Vale.X64.Decls.validSrcAddrs128",
        "typing_Vale.X64.Decls.validSrcAddrsOffset128",
        "typing_Vale.X64.Memory.buffer_addr",
        "typing_Vale.X64.Memory.buffer_as_seq",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd",
        "typing_Vale.X64.State.__proj__Mkstate__item__flags",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__memTaint",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.State.state_eta", "typing_Vale.X64.Xmms.eta_sel",
        "typing_Vale.X64.Xmms.sel", "typing_tok_Vale.AES.AES_s.AES_128@tok",
        "typing_tok_Vale.AES.AES_s.AES_256@tok",
        "typing_tok_Vale.Interop.Types.TUInt128@tok",
        "typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_typing"
      ],
      0,
      "f684cc55606096f562bc5663bf95236a"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks_while",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "c38d66e1c9e7b4e53f68cdffa7e6fca5"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpMonotone_gcm_one_pass_blocks_while",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks_while",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm", "unit_typing"
      ],
      0,
      "d7f1e7fee6e456f9f249d93d255714ba"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass_blocks_while",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks_while",
        "equation_Vale.X64.Decls.va_require_total",
        "fuel_guarded_inversion_Vale.X64.State.state"
      ],
      0,
      "5ac73ea297bb99261b67a4f82da92dee"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_one_pass_blocks_while",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "dff8155e1c1b1f2d57843e19d8f5ad7a"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_one_pass_blocks_while",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.min",
        "equation_Prims.nat", "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR.gctr_partial",
        "equation_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass_blocks_while",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks_while",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Decls.validDstAddrsOffset128",
        "equation_Vale.X64.Decls.validSrcAddrsOffset128",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.Memory.modifies_buffer_addr",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Xmms.lemma_equal_elim",
        "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.X64.State.Mkstate_flags",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_stack",
        "projection_inverse_Vale.X64.State.Mkstate_stackTaint",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass_blocks_while",
        "typing_FStar.Seq.Base.length", "typing_Vale.AES.GCTR_s.inc32",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm",
        "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.Regs.upd",
        "typing_Vale.X64.State.__proj__Mkstate__item__flags",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.sel",
        "typing_tok_Vale.Interop.Types.TUInt128@tok", "unit_typing"
      ],
      0,
      "ddca19398efdc6b67b61e76dd4ef5bd8"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_one_pass_blocks",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs"
      ],
      0,
      "288c7c87b60af543a59fc30b52fe8a69"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_one_pass_blocks",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_imp",
        "equation_Prims.logical", "equation_Prims.min", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.AES.GCTR.gctr_partial",
        "equation_Vale.AES.GCTR_s.inc32",
        "equation_Vale.AES.GHash.ghash_incremental0",
        "equation_Vale.Def.Prop_s.prop0",
        "equation_Vale.Def.Types_s.insert_nat32",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Four_s.four_insert",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Decls.validDstAddrsOffset128",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrsOffset128",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.QuickCodes.range1",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "l_imp-interp", "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.Memory.modifies_buffer_addr",
        "lemma_Vale.X64.Memory.modifies_buffer_elim",
        "lemma_Vale.X64.Memory.modifies_refl",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Xmms.lemma_equal_intro",
        "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "proj_equation_Vale.X64.Machine_s.OReg_r",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_09d9ae2b4f83e9874aa98bae7c20bcb4",
        "refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.seq", "typing_Prims.eq2",
        "typing_Prims.l_and", "typing_Prims.l_imp",
        "typing_Vale.AES.GCTR.gctr_partial", "typing_Vale.AES.GCTR_s.inc32",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Lib.Workarounds.slice_work_around",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.validSrcAddrsOffset128",
        "typing_Vale.X64.Memory.buffer_addr",
        "typing_Vale.X64.Memory.buffer_as_seq",
        "typing_Vale.X64.Memory.buffer_length",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__memTaint",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.eta_sel", "typing_Vale.X64.Xmms.sel",
        "typing_tok_Vale.AES.AES_s.AES_128@tok",
        "typing_tok_Vale.AES.AES_s.AES_256@tok",
        "typing_tok_Vale.Interop.Types.TUInt128@tok",
        "typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_typing"
      ],
      0,
      "c16d1e90ab80369d2939fd535ec7c3e6"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.State.update_xmm",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Decls.va_upd_reg", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs"
      ],
      0,
      "8a20545ca9a6e4774a380f99259ae5ee"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpMonotone_gcm_one_pass_blocks",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "845e04a52b5aabcffc8489348d719c3e"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass_blocks",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks",
        "equation_Vale.X64.Decls.va_require_total",
        "fuel_guarded_inversion_Vale.X64.State.state"
      ],
      0,
      "2092e744841598629b49d073078d7037"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_one_pass_blocks",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "a8d84b74bcf1b677fa4c013fb54c631a"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_one_pass_blocks",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
        "bool_inversion", "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_192",
        "constructor_distinct_Vale.AES.AES_s.AES_256",
        "constructor_distinct_Vale.Interop.Types.TUInt128",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.QuickCode.Mod_reg@tok",
        "data_typing_intro_Vale.X64.QuickCode.Mod_xmm@tok", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_None@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_flags@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_mem@tok", "equation_Prims.min",
        "equation_Prims.nat", "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR.gctr_partial",
        "equation_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass_blocks",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Decls.validDstAddrsOffset128",
        "equation_Vale.X64.Decls.validSrcAddrsOffset128",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "kinding_Vale.X64.QuickCode.mod_t@tok",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.Memory.modifies_buffer_addr",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "lemma_Vale.X64.Xmms.lemma_equal_elim",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.X64.State.Mkstate_flags",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_stack",
        "projection_inverse_Vale.X64.State.Mkstate_stackTaint",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
        "refinement_interpretation_Tm_refine_4325f89bb999c11df0fee155e9f2ddc2",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass_blocks",
        "typing_FStar.Seq.Base.length",
        "typing_Vale.AES.X64.GCMencrypt.va_code_gcm_one_pass_blocks",
        "typing_Vale.AES.X64.GCMencrypt.va_lemma_gcm_one_pass_blocks",
        "typing_Vale.Lib.Workarounds.slice_work_around",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm",
        "typing_Vale.X64.Memory.buffer_as_seq",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.QuickCode.update_state_mods",
        "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd",
        "typing_Vale.X64.State.__proj__Mkstate__item__flags",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.sel", "typing_Vale.X64.Xmms.upd",
        "typing_tok_Vale.Interop.Types.TUInt128@tok",
        "typing_tok_Vale.X64.QuickCode.Mod_None@tok",
        "typing_tok_Vale.X64.QuickCode.Mod_flags@tok",
        "typing_tok_Vale.X64.QuickCode.Mod_mem@tok", "unit_typing"
      ],
      0,
      "f7c20c8b0566ecb059fe686889ed6795"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_code_gcm_one_pass_blocks_opt",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "5da548e42f28a70170f353b422ab788c"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass_blocks_opt",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs"
      ],
      0,
      "e580451c7c0737610c61b01a7f1fef22"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass_blocks_opt",
      2,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "5d9496666cc520b1b2b1fe48dcf110ab"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass_blocks_opt",
      3,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "11a50d9ffea5bf138efb79e01183bb81"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass_blocks_opt",
      4,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "5050b932ae749bc1c6372127ce6c732c"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass_blocks_opt",
      5,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "6f9af04089cd05cdc08f2cca83b1e833"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass_blocks_opt",
      6,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "36f09ad5e9ed266fb2ae22752b78f2af"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass_blocks_opt",
      7,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "a9995a2b072bd00d20ea9f28598fb2ee"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass_blocks_opt",
      8,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "6f4927297b3bfae98a148fe4b46a3972"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_one_pass_blocks_opt",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "923aa51971b2ee93c3c12e39d851b5fe"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_one_pass_blocks_opt",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
        "b2t_def", "bool_inversion",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256",
        "constructor_distinct_Vale.Interop.Types.TUInt128",
        "data_typing_intro_Vale.AES.AES_s.AES_192@tok", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_imp",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR_s.inc32",
        "equation_Vale.AES.GHash.ghash_incremental0",
        "equation_Vale.AES.X64.AESCTR.aes_reqs",
        "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.validDstAddrs128",
        "equation_Vale.X64.Decls.validDstAddrsOffset128",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrsOffset128",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.State.state_eq",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "l_and-interp", "l_imp-interp",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.Memory.loc_includes_refl",
        "lemma_Vale.X64.Memory.modifies_buffer_addr",
        "lemma_Vale.X64.Memory.modifies_buffer_elim",
        "lemma_Vale.X64.Memory.modifies_buffer_readable",
        "lemma_Vale.X64.Memory.modifies_goal_directed_refl",
        "lemma_Vale.X64.Memory.modifies_goal_directed_trans",
        "lemma_Vale.X64.Memory.modifies_goal_directed_trans2",
        "lemma_Vale.X64.Memory.modifies_valid_taint128",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Xmms.lemma_equal_intro",
        "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_09d9ae2b4f83e9874aa98bae7c20bcb4",
        "refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_FStar.Seq.Base.empty",
        "typing_FStar.Seq.Base.length", "typing_Prims.eq2",
        "typing_Prims.l_imp", "typing_Vale.AES.GCTR.gctr_partial",
        "typing_Vale.AES.GCTR_s.inc32",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Lib.Workarounds.slice_work_around",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.Decls.validSrcAddrs128",
        "typing_Vale.X64.Memory.base_typ_as_vale_type",
        "typing_Vale.X64.Memory.buffer_addr",
        "typing_Vale.X64.Memory.buffer_as_seq",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__memTaint",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.eta_sel", "typing_Vale.X64.Xmms.sel",
        "typing_tok_Vale.Interop.Types.TUInt128@tok",
        "typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_inversion",
        "unit_typing"
      ],
      0,
      "52e89cda306d1f36a465dbc95f196e6e"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks_opt",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "f40c53b0f5a2f49a328324b1531dd94e"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpMonotone_gcm_one_pass_blocks_opt",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks_opt",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "ed99f2de89db7dd398ee0c8a3a81b4a8"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass_blocks_opt",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks_opt",
        "equation_Vale.X64.Decls.va_require_total",
        "fuel_guarded_inversion_Vale.X64.State.state"
      ],
      0,
      "f334282764604f18cba1c084be1a4b20"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_one_pass_blocks_opt",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "0b136d3a2dcf1d301db606e0c4ed39ae"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_one_pass_blocks_opt",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_192",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass_blocks_opt",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass_blocks_opt",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Xmms.lemma_equal_elim",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.X64.State.Mkstate_flags",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_stack",
        "projection_inverse_Vale.X64.State.Mkstate_stackTaint",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass_blocks_opt",
        "typing_FStar.Seq.Base.length", "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.Regs.upd",
        "typing_Vale.X64.State.__proj__Mkstate__item__flags",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.sel", "unit_typing"
      ],
      0,
      "295a24b7877602dbf57fc4ab876d76e2"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_code_gcm_one_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_caaaba36aae265bf9eecb3d929f9607d"
      ],
      0,
      "72568a3469b5c9c2d9171a58db804b44"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_caaaba36aae265bf9eecb3d929f9607d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs"
      ],
      0,
      "dc3e99119f046d7cc9deef707ae8ff16"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_caaaba36aae265bf9eecb3d929f9607d"
      ],
      0,
      "cc446edf27461943f03cc797583fbb9d"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      3,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_caaaba36aae265bf9eecb3d929f9607d"
      ],
      0,
      "521e6852105e58909a7e2fe24b9e73e7"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      4,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "e1130e419c5c8f5b79b311f5cf0d63b0"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      5,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "4fa2e13713826646706045334149cf88"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      6,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "55481fa4a3249c3445a1d9b86930f864"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      7,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "9d67677bc5ca6e53b2b98e65b394daeb"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      8,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "a3a3e59230b8d52b5071117251d6f0c2"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      9,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "c2237be6037e3f7d1a827f426f4d4946"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      10,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "b59e34af5ad79a410e0b4ee1ffbdd65a"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      11,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "c432207fcded0b0e4bcdb17a39904fc7"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      12,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "c77185f04bfe1b928d06f80d14a1624f"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      13,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "7f6be187b6af296bbb26c624d463a74b"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      14,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "disc_equation_Vale.X64.Machine_s.OStack",
        "primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "f1d0e4cbb6431b8945aa159b5aa92d07"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_one_pass",
      15,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_FStar.Seq.Base.seq__uu___haseq", "b2t_def",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.AES.GCTR.make_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "haseqTm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
      ],
      0,
      "f2c21744a9c9f5ed9735582be5d85e1d"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_one_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "equation_Vale.AES.GCTR.make_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5e617a2d2450afcce9d1e38a7a0de32c",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "typing_FStar.Seq.Base.empty",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled"
      ],
      0,
      "7fedd8e7b4ae387d8012eb223e6c5df2"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_one_pass",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_and",
        "equation_Prims.l_imp", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
        "equation_Vale.AES.GCTR.make_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.gctr_encrypt_LE",
        "equation_Vale.AES.GCTR_s.inc32",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "equation_Vale.AES.GHash.ghash_incremental0",
        "equation_Vale.Def.Prop_s.prop0",
        "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.validDstAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.QuickCodes.range1",
        "equation_Vale.X64.State.state_eq",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "l_and-interp", "l_imp-interp",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.Memory.loc_includes_refl",
        "lemma_Vale.X64.Memory.modifies_buffer_addr",
        "lemma_Vale.X64.Memory.modifies_buffer_elim",
        "lemma_Vale.X64.Memory.modifies_buffer_readable",
        "lemma_Vale.X64.Memory.modifies_goal_directed_refl",
        "lemma_Vale.X64.Memory.modifies_goal_directed_trans",
        "lemma_Vale.X64.Memory.modifies_goal_directed_trans2",
        "lemma_Vale.X64.Memory.modifies_refl",
        "lemma_Vale.X64.Memory.modifies_valid_taint128",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Xmms.lemma_equal_intro",
        "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_09d9ae2b4f83e9874aa98bae7c20bcb4",
        "refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
        "refinement_interpretation_Tm_refine_96bb0d8f62049763acce37b8fe446653",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_FStar.Seq.Base.empty",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.seq",
        "typing_Prims.eq2", "typing_Prims.l_imp",
        "typing_Vale.AES.GCTR.make_gctr_plain_LE",
        "typing_Vale.AES.GCTR_s.gctr_encrypt_LE",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
        "typing_Vale.Lib.Workarounds.slice_work_around",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.Decls.validSrcAddrs128",
        "typing_Vale.X64.Memory.base_typ_as_vale_type",
        "typing_Vale.X64.Memory.buffer_addr",
        "typing_Vale.X64.Memory.buffer_as_seq",
        "typing_Vale.X64.Memory.buffer_length",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__memTaint",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.eta_sel", "typing_Vale.X64.Xmms.sel",
        "typing_tok_Vale.AES.AES_s.AES_256@tok",
        "typing_tok_Vale.Interop.Types.TUInt128@tok",
        "typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_inversion",
        "unit_typing"
      ],
      0,
      "5cd901b89633fa19340958ce759fa577"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "equation_Vale.AES.GCTR.make_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "typing_FStar.Seq.Base.empty",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok"
      ],
      0,
      "9f8b623f75489a9c0942078fb35a6f0c"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpMonotone_gcm_one_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "3b8c292a86a2de433604d19b5c242bb6"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass",
        "equation_Vale.X64.Decls.va_require_total",
        "fuel_guarded_inversion_Vale.X64.State.state"
      ],
      0,
      "1b5978fee740c6a66d1d6a7be6581bf8"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_one_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "6437b6cdf70949595dce73e28ba64809"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_one_pass",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_192",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_one_pass",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Xmms.lemma_equal_elim",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.X64.State.Mkstate_flags",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_stack",
        "projection_inverse_Vale.X64.State.Mkstate_stackTaint",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_one_pass",
        "typing_FStar.Seq.Base.length", "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__flags",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.sel", "unit_typing"
      ],
      0,
      "e0b2167ce706d0f33209a1a2edb21b07"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_core_part1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_816baa3f8e222aaee20ed3e2d3992880",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "b2t_def", "constructor_distinct_Tm_unit", "eq2-interp",
        "equation_Prims.nat", "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR.make_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "partial_app_typing_a5df2c69070e20952ad8c7ffdfbc7635",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955",
        "typing_Vale.Lib.Seqs_s.seq_map"
      ],
      0,
      "e96c3bb1ca15dbd6c8538f74a8010fd8"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_core_part1",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_49e1bcc308a31329f00baed943b7728c",
        "equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "equation_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_b836d39e81cfc717f7393f7117d32554",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_86c482bea7f4b3e185db7eb456de0b9f",
        "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
      ],
      0,
      "70ba70c94fd14bcf9d51a346989fdeff"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_core_part1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0dcc847086ca9fbf30570027cd5d25ed",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955"
      ],
      0,
      "ae0a83ae854eb10bd543c66a2a5ccb75"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_core_part1",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_interpretation_Tm_arrow_f82c3fb9ac6610efb97620a59b378092",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_49e1bcc308a31329f00baed943b7728c",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "b2t_def", "bool_inversion",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256",
        "constructor_distinct_Vale.Interop.Types.TUInt128",
        "data_typing_intro_Vale.Def.Words_s.Mkfour@tok", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok",
        "equation_FStar.Pervasives.Native.fst", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_and",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
        "equation_Vale.AES.GCTR_s.inc32",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.AES.GHash.ghash_incremental0",
        "equation_Vale.Arch.Types.be_quad32_to_bytes",
        "equation_Vale.Def.Prop_s.prop0",
        "equation_Vale.Def.Types_s.be_bytes_to_quad32",
        "equation_Vale.Def.Types_s.insert_nat32",
        "equation_Vale.Def.Types_s.insert_nat64",
        "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Four_s.four_insert",
        "equation_Vale.Def.Words.Four_s.four_to_two_two",
        "equation_Vale.Def.Words.Four_s.two_two_to_four",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "equation_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
        "equation_Vale.Def.Words.Two_s.nat_to_two",
        "equation_Vale.Def.Words.Two_s.two_insert",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Decls.validDstAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.QuickCodes.range1",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32",
        "function_token_typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_91bed3c70bcac4fa34e4de064d4ad6ff",
        "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_FStar.UInt.pow2_values",
        "lemma_Vale.Arch.Types.be_bytes_to_quad32_to_bytes",
        "lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE",
        "lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Xmms.lemma_equal_intro",
        "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "proj_equation_Vale.Def.Words_s.Mktwo_lo",
        "proj_equation_Vale.X64.Machine_s.OReg_r",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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.Mktuple4__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__4",
        "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_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_Vale.Def.Words_s.Mktwo_hi",
        "projection_inverse_Vale.Def.Words_s.Mktwo_lo",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_09d9ae2b4f83e9874aa98bae7c20bcb4",
        "refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_401f18bb990fc97a19859cdf0ccb81c7",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_4efdd8345d485e7dbe72183752bac011",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_96bb0d8f62049763acce37b8fe446653",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_b836d39e81cfc717f7393f7117d32554",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
        "refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
        "refinement_interpretation_Tm_refine_d752083afe9106c9349c58895c219f6f",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_FStar.Seq.Base.init",
        "typing_FStar.Seq.Base.length", "typing_Prims.eq2",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_86c482bea7f4b3e185db7eb456de0b9f",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955",
        "typing_Vale.AES.AES_s.aes_encrypt_LE_def",
        "typing_Vale.AES.GCTR_s.pad_to_128_bits",
        "typing_Vale.AES.GHash.ghash_incremental0",
        "typing_Vale.Def.Types_s.le_bytes_to_seq_quad32",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_Vale.Lib.Workarounds.slice_work_around",
        "typing_Vale.Math.Poly2.Bits.of_nat32",
        "typing_Vale.Math.Poly2_s.degree",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.Decls.validSrcAddrs128",
        "typing_Vale.X64.Memory.base_typ_as_vale_type",
        "typing_Vale.X64.Memory.buffer_addr",
        "typing_Vale.X64.Memory.buffer_as_seq",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__memTaint",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.eta_sel", "typing_Vale.X64.Xmms.sel",
        "typing_tok_Vale.AES.AES_s.AES_128@tok",
        "typing_tok_Vale.AES.AES_s.AES_256@tok",
        "typing_tok_Vale.Interop.Types.TUInt128@tok",
        "typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_inversion",
        "unit_typing"
      ],
      0,
      "1ab403f5547ecc39b8e76af81ce10434"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wp_gcm_core_part1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955"
      ],
      0,
      "e891bb975544982d20b3a60a5f1472ce"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpMonotone_gcm_core_part1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple4@tok",
        "equation_Prims.nat",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_core_part1",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm",
        "typing_Vale.X64.State.update_reg"
      ],
      0,
      "a5b19d1ef4d913782acf0a7b59c0f094"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_core_part1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_core_part1",
        "equation_Vale.X64.Decls.va_require_total",
        "fuel_guarded_inversion_Vale.X64.State.state"
      ],
      0,
      "2a0db0efca208959211f74c74665bafe"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_core_part1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "ef0551d4440e39034d2902130e362587"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_core_part1",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_49e1bcc308a31329f00baed943b7728c",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_816baa3f8e222aaee20ed3e2d3992880",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "bool_inversion", "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_192",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_core_part1",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_core_part1",
        "equation_Vale.Arch.Types.be_quad32_to_bytes",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq16",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_BE",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "equation_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE",
        "lemma_Vale.Def.Words.Seq.seq_to_seq_four_to_seq_LE",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Xmms.lemma_equal_elim",
        "partial_app_typing_a5df2c69070e20952ad8c7ffdfbc7635",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.State.Mkstate_xmms",
        "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.Mktuple6__1",
        "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_Vale.X64.State.Mkstate_flags",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_stack",
        "projection_inverse_Vale.X64.State.Mkstate_stackTaint",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_b836d39e81cfc717f7393f7117d32554",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_core_part1",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_86c482bea7f4b3e185db7eb456de0b9f",
        "typing_Tm_abs_98881f65bedf76039a7f6f8ab1c7c9b6",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955",
        "typing_Vale.Arch.Types.be_quad32_to_bytes",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
        "typing_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "typing_Vale.Lib.Seqs_s.seq_map",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__flags",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.sel"
      ],
      0,
      "5591df64c4dcb14c09f5c901920b6fff"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_make_length_quad",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs"
      ],
      0,
      "19a78f817e0c79be824b450f862eddbf"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_make_length_quad",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "bool_typing", "eq2-interp", "equation_Prims.eq2",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.QuickCodes.range1",
        "equation_Vale.X64.State.state_eq",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Xmms.lemma_equal_intro",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_09d9ae2b4f83e9874aa98bae7c20bcb4",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.eta_sel", "unit_typing"
      ],
      0,
      "8f28c18fa5a0cf98987091893ee66a66"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wp_gcm_make_length_quad",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Machine_s.reg",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs"
      ],
      0,
      "eb858c02ab8d887747c53882bd24feea"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpMonotone_gcm_make_length_quad",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_make_length_quad",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.State.update_reg",
        "typing_Vale.X64.State.update_xmm", "unit_typing"
      ],
      0,
      "80847665987c6f7fc877e74391c1fee6"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_make_length_quad",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_make_length_quad",
        "equation_Vale.X64.Decls.va_require_total",
        "fuel_guarded_inversion_Vale.X64.State.state"
      ],
      0,
      "9dd4505f198feef399a29fd75c286b94"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_make_length_quad",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "027f1792d5a2a90d3c0df27b16ad0cf4"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_make_length_quad",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp",
        "equation_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_make_length_quad",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_make_length_quad",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Xmms.lemma_equal_elim",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.X64.State.Mkstate_flags",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_stack",
        "projection_inverse_Vale.X64.State.Mkstate_stackTaint",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_make_length_quad",
        "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.Regs.upd",
        "typing_Vale.X64.State.__proj__Mkstate__item__flags",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.sel", "typing_Vale.X64.Xmms.upd", "unit_typing"
      ],
      0,
      "d05e225d0dd4dc424f0a8592ef4f3e06"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_core",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "37af31f417801eb84e1fa8093dac81d1"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_core",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.length", "typing_Vale.Def.Types_s.quad32"
      ],
      0,
      "63a2925bd02bcf439943bfad59858297"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_core",
      3,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_816baa3f8e222aaee20ed3e2d3992880",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "b2t_def", "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.AES.AES_s.AES_128", "eq2-interp",
        "equation_Prims.nat", "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.Arch.Types.be_quad32_to_bytes",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq16",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "partial_app_typing_a5df2c69070e20952ad8c7ffdfbc7635",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d752083afe9106c9349c58895c219f6f",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955",
        "typing_Vale.AES.GCTR_s.pad_to_128_bits",
        "typing_Vale.Arch.Types.be_quad32_to_bytes",
        "typing_Vale.Lib.Seqs_s.seq_map"
      ],
      0,
      "f8d9cd4813da84162d69d51ae57dccf8"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_core",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_18da83d917440e5811549d3cd21604a7",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955"
      ],
      0,
      "dd028785f729946b80edb2b1d45f4490"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_core",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "b2t_def", "bool_inversion",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256",
        "constructor_distinct_Vale.Interop.Types.TUInt128",
        "data_typing_intro_Vale.Def.Words_s.Mkfour@tok", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
        "equation_Prims.l_and", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
        "equation_Vale.AES.GCM_s.gcm_encrypt_LE",
        "equation_Vale.Def.Prop_s.prop0",
        "equation_Vale.Def.Types_s.insert_nat32",
        "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Four_s.four_insert",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.validDstAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.QuickCodes.range1",
        "equation_Vale.X64.State.state_eq",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.Memory.modifies_buffer_addr",
        "lemma_Vale.X64.Memory.modifies_buffer_elim",
        "lemma_Vale.X64.Memory.modifies_buffer_readable",
        "lemma_Vale.X64.Memory.modifies_valid_taint128",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Xmms.lemma_equal_intro",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "proj_equation_Vale.X64.Machine_s.OReg_r",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_09d9ae2b4f83e9874aa98bae7c20bcb4",
        "refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955",
        "typing_Vale.AES.AES_s.aes_encrypt_LE_def",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Lib.Workarounds.slice_work_around",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.Decls.validSrcAddrs128",
        "typing_Vale.X64.Memory.buffer_addr",
        "typing_Vale.X64.Memory.buffer_as_seq",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__memTaint",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.eta_sel",
        "typing_tok_Vale.AES.AES_s.AES_128@tok",
        "typing_tok_Vale.AES.AES_s.AES_256@tok",
        "typing_tok_Vale.Interop.Types.TUInt128@tok",
        "typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_inversion",
        "unit_typing"
      ],
      0,
      "044e12631a5d2b8ae4f734eb0ee4bb33"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wp_gcm_core",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955"
      ],
      0,
      "824faafad52c3a5ae1afcef05cac7b0a"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpMonotone_gcm_core",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_core",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "7e90077a4d8a8fd4c044626a98abc8ed"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_core",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_core",
        "equation_Vale.X64.Decls.va_require_total",
        "fuel_guarded_inversion_Vale.X64.State.state"
      ],
      0,
      "e5ad8c62ed826c42c07db2c0795226c1"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_core",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "d27c6a5944fc1717053549d157ddfcc3"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_core",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_816baa3f8e222aaee20ed3e2d3992880",
        "bool_inversion", "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_192",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_core",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_core",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Xmms.lemma_equal_elim",
        "partial_app_typing_a5df2c69070e20952ad8c7ffdfbc7635",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.X64.State.Mkstate_flags",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_stack",
        "projection_inverse_Vale.X64.State.Mkstate_stackTaint",
        "projection_inverse_Vale.X64.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_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_core",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Vale.Lib.Seqs_s.seq_map",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__flags",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.sel", "unit_typing"
      ],
      0,
      "71fe2be01b1427dbb89b985faf232247"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_encrypt_stdcall_inner",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c302b492a0bf222c1cee19691d79cca2",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955"
      ],
      0,
      "0c36543821dd4ecc407957ef76276bda"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_encrypt_stdcall_inner",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256",
        "constructor_distinct_Vale.Interop.Types.TUInt128",
        "constructor_distinct_Vale.Interop.Types.TUInt64", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equality_tok_Vale.Interop.Types.TUInt64@tok",
        "equality_tok_Vale.X64.Machine_s.Public@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_and",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
        "equation_Vale.Def.Prop_s.prop0",
        "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Decls.validDstAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.Machine_s.reg",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.QuickCodes.range1",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.Memory.loc_includes_refl",
        "lemma_Vale.X64.Memory.loc_includes_union_l_buffer",
        "lemma_Vale.X64.Memory.modifies_buffer_addr",
        "lemma_Vale.X64.Memory.modifies_buffer_elim",
        "lemma_Vale.X64.Memory.modifies_buffer_readable",
        "lemma_Vale.X64.Memory.modifies_goal_directed_refl",
        "lemma_Vale.X64.Memory.modifies_goal_directed_trans",
        "lemma_Vale.X64.Memory.modifies_goal_directed_trans2",
        "lemma_Vale.X64.Memory.modifies_valid_taint128",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Xmms.lemma_equal_intro",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
        "refinement_interpretation_Tm_refine_809440a2e49ae18d732467ba1f4c9c0b",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_FStar.Seq.Base.length",
        "typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
        "typing_Prims.l_and",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Lib.Workarounds.slice_work_around",
        "typing_Vale.X64.CPU_Features_s.aesni_enabled",
        "typing_Vale.X64.Decls.validSrcAddrs128",
        "typing_Vale.X64.Memory.base_typ_as_vale_type",
        "typing_Vale.X64.Memory.buffer_addr",
        "typing_Vale.X64.Memory.buffer_as_seq",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.Memory.buffer_readable",
        "typing_Vale.X64.Memory.buffer_write",
        "typing_Vale.X64.Memory.buffer_writeable",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.loc_union",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__memTaint",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_tok_Vale.Interop.Types.TUInt128@tok",
        "typing_tok_Vale.Interop.Types.TUInt64@tok",
        "typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_typing"
      ],
      0,
      "2b75a6ba97b743f8e1e132a6ce3085c8"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wp_gcm_encrypt_stdcall_inner",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955"
      ],
      0,
      "d2b5a6460224f4a046fbed4f9a35cc3b"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpMonotone_gcm_encrypt_stdcall_inner",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_encrypt_stdcall_inner",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "9851b3995ee5d977b6bf7f762d2af1bf"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_encrypt_stdcall_inner",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_encrypt_stdcall_inner",
        "equation_Vale.X64.Decls.va_require_total",
        "fuel_guarded_inversion_Vale.X64.State.state"
      ],
      0,
      "1690fda2122e5534a30ae993f9534c0c"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_encrypt_stdcall_inner",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "2e4e066c221350f0cfc3267b639b356e"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_encrypt_stdcall_inner",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_816baa3f8e222aaee20ed3e2d3992880",
        "bool_inversion", "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_192",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_encrypt_stdcall_inner",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_encrypt_stdcall_inner",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Xmms.lemma_equal_elim",
        "partial_app_typing_a5df2c69070e20952ad8c7ffdfbc7635",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.X64.State.Mkstate_flags",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_stack",
        "projection_inverse_Vale.X64.State.Mkstate_stackTaint",
        "projection_inverse_Vale.X64.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_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_encrypt_stdcall_inner",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Vale.Lib.Seqs_s.seq_map",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkstate__item__flags",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.sel", "unit_typing"
      ],
      0,
      "8650972b0a696f51de4e85cf42dc8626"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_encrypt_stdcall",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "52179710d2bd343eb9a88687da1c2766"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_encrypt_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.X64.Machine_s.Public@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_fb84d171d6d37c56bda612f21db76995",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955"
      ],
      0,
      "24b6782102626ed0056dcb5f4a129dcb"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_encrypt_stdcall",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_interpretation_Tm_arrow_fa4e3ee4a3dfa402363cd0693fcbfca4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "b2t_def", "bool_inversion",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256",
        "constructor_distinct_Vale.Interop.Types.TUInt128",
        "constructor_distinct_Vale.Interop.Types.TUInt64", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equality_tok_Vale.Interop.Types.TUInt64@tok",
        "equality_tok_Vale.X64.Machine_s.Public@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
        "equation_Prims.l_and", "equation_Prims.l_imp",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
        "equation_Vale.Arch.Types.hi64", "equation_Vale.Arch.Types.lo64",
        "equation_Vale.Def.Prop_s.prop0",
        "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.validDstAddrs128",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.QuickCodes.range1",
        "equation_Vale.X64.State.state_eq",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Arch.Types.hi64_def",
        "function_token_typing_Vale.Arch.Types.lo64_def",
        "function_token_typing_Vale.Def.Opaque_s.make_opaque",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat64",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "kinding_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "kinding_Vale.Def.Words_s.four@tok", "l_and-interp", "l_imp-interp",
        "l_not-interp", "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Stack_i.lemma_compose_free_stack64",
        "lemma_Vale.X64.Stack_i.lemma_correct_store_load_stack64",
        "lemma_Vale.X64.Stack_i.lemma_correct_store_load_taint_stack64",
        "lemma_Vale.X64.Stack_i.lemma_frame_store_load_stack64",
        "lemma_Vale.X64.Stack_i.lemma_frame_store_load_taint_stack64",
        "lemma_Vale.X64.Stack_i.lemma_free_stack_same_load64",
        "lemma_Vale.X64.Stack_i.lemma_free_stack_same_valid64",
        "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64",
        "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64",
        "lemma_Vale.X64.Stack_i.lemma_store_new_valid64",
        "lemma_Vale.X64.Stack_i.lemma_store_stack_same_valid64",
        "lemma_Vale.X64.Xmms.lemma_equal_intro",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.X64.Machine_s.OReg_r",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_stack",
        "projection_inverse_Vale.X64.State.Mkstate_stackTaint",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_09d9ae2b4f83e9874aa98bae7c20bcb4",
        "refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_4c6411da037541583c16876f5cc7dfe4",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing",
        "token_correspondence_Vale.Def.Opaque_s.make_opaque",
        "typing_FStar.Seq.Base.length", "typing_Prims.eq2",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955",
        "typing_Vale.Arch.Types.hi64", "typing_Vale.Arch.Types.lo64",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Lib.Workarounds.slice_work_around",
        "typing_Vale.X64.Decls.validSrcAddrs128",
        "typing_Vale.X64.Memory.buffer_addr",
        "typing_Vale.X64.Memory.buffer_as_seq",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.loc_union",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp",
        "typing_Vale.X64.Stack_i.store_stack64",
        "typing_Vale.X64.Stack_i.store_taint_stack64",
        "typing_Vale.X64.Stack_i.valid_src_stack64",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__memTaint",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__stack",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.eta_sel",
        "typing_tok_Vale.Interop.Types.TUInt128@tok",
        "typing_tok_Vale.Interop.Types.TUInt64@tok",
        "typing_tok_Vale.X64.Machine_s.Public@tok",
        "typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_typing"
      ],
      0,
      "a071a7cb8c0f3edb649516d97d511382"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wp_gcm_encrypt_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955"
      ],
      0,
      "274090157b51c6bce6e1b25a06dc29b6"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpMonotone_gcm_encrypt_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_encrypt_stdcall",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_stack",
        "typing_Vale.X64.Decls.va_upd_stackTaint",
        "typing_Vale.X64.Decls.va_upd_xmm",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "067c5704cfee34579945344980de9f2e"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_encrypt_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp", "equality_tok_Vale.X64.Machine_s.Public@tok",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_encrypt_stdcall",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "interpretation_Tm_abs_66f98bf01443a163a32ed74e878b1449",
        "interpretation_Tm_abs_be709b29b4f28d04784b98539d3ed7ab",
        "proj_equation_Vale.X64.State.Mkstate_mem", "unit_typing"
      ],
      0,
      "4d181d4aef066bf74cfd7225521dd6ac"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_encrypt_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "4bd5b9ea21f00a774d6784e950eb1ba9"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_encrypt_stdcall",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_816baa3f8e222aaee20ed3e2d3992880",
        "bool_inversion", "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_192",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.X64.Machine_s.Public@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_encrypt_stdcall",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_encrypt_stdcall",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_stack",
        "equation_Vale.X64.Decls.va_upd_stackTaint",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_66f98bf01443a163a32ed74e878b1449",
        "interpretation_Tm_abs_be709b29b4f28d04784b98539d3ed7ab",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Xmms.lemma_equal_elim",
        "partial_app_typing_a5df2c69070e20952ad8c7ffdfbc7635",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.X64.State.Mkstate_flags",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_stack",
        "projection_inverse_Vale.X64.State.Mkstate_stackTaint",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_4c6411da037541583c16876f5cc7dfe4",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_encrypt_stdcall",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Vale.Lib.Seqs_s.seq_map",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_stack",
        "typing_Vale.X64.Decls.va_upd_stackTaint",
        "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.Stack_i.init_rsp",
        "typing_Vale.X64.State.__proj__Mkstate__item__flags",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__stack",
        "typing_Vale.X64.State.__proj__Mkstate__item__stackTaint",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.sel", "unit_typing"
      ],
      0,
      "37d1489080501283f0bfe38812d071f7"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_req_gcm_encrypt2_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of",
        "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "unit_typing"
      ],
      0,
      "a3d38cfde4284c612364a8d9150e9353"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_ens_gcm_encrypt2_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256",
        "constructor_distinct_Vale.Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equation_Prims.l_and", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.X64.GCMencrypt.va_req_gcm_encrypt2_stdcall",
        "equation_Vale.Arch.Types.be_quad32_to_bytes",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq16",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_tok_Vale.Interop.Types.TUInt128@tok", "unit_typing"
      ],
      0,
      "e5bf9f8537db36124e880cdd7cff8a29"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_qcode_gcm_encrypt2_stdcall",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "9fbd543cc7beb863781be566cca7da0f"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_encrypt2_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256",
        "constructor_distinct_Vale.Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
        "equation_Vale.Arch.Types.be_quad32_to_bytes",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq16",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.X64.Decls.validDstAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_07e85b3f579351634cefc4b53b65a6f3",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_tok_Vale.Interop.Types.TUInt128@tok"
      ],
      0,
      "3c49826e038652b2da97af08db5af6d0"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_lemma_gcm_encrypt2_stdcall",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_interpretation_Tm_arrow_fa4e3ee4a3dfa402363cd0693fcbfca4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "b2t_def", "bool_inversion", "bool_typing",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256",
        "constructor_distinct_Vale.Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok",
        "equality_tok_Vale.X64.Machine_s.Public@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_and",
        "equation_Prims.l_imp", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
        "equation_Vale.Arch.Types.be_quad32_to_bytes",
        "equation_Vale.Arch.Types.hi64", "equation_Vale.Arch.Types.lo64",
        "equation_Vale.Def.Prop_s.prop0",
        "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq16",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Decls.validDstAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.QuickCodes.range1",
        "equation_Vale.X64.Stack_i.valid_stack_slot64",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Arch.Types.hi64_def",
        "function_token_typing_Vale.Arch.Types.lo64_def",
        "function_token_typing_Vale.Def.Opaque_s.make_opaque",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat64",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_62094ddb0a7b86f722ad4300322d62d5",
        "interpretation_Tm_abs_756fcc26be77e939e037175e05563ad5",
        "interpretation_Tm_abs_8bac9c131d2215555d160896e1b3ed64",
        "interpretation_Tm_abs_e5cbb4ae491791bf4d5a4c9197ecb047",
        "kinding_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "kinding_Vale.Def.Words_s.four@tok", "l_and-interp", "l_imp-interp",
        "l_not-interp", "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.Memory.loc_includes_refl",
        "lemma_Vale.X64.Memory.loc_includes_union_l_buffer",
        "lemma_Vale.X64.Memory.modifies_buffer_addr",
        "lemma_Vale.X64.Memory.modifies_buffer_elim",
        "lemma_Vale.X64.Memory.modifies_buffer_readable",
        "lemma_Vale.X64.Memory.modifies_goal_directed_refl",
        "lemma_Vale.X64.Memory.modifies_goal_directed_trans",
        "lemma_Vale.X64.Memory.modifies_goal_directed_trans2",
        "lemma_Vale.X64.Memory.modifies_valid_taint128",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Stack_i.lemma_compose_free_stack64",
        "lemma_Vale.X64.Stack_i.lemma_correct_store_load_stack64",
        "lemma_Vale.X64.Stack_i.lemma_correct_store_load_taint_stack64",
        "lemma_Vale.X64.Stack_i.lemma_frame_store_load_stack64",
        "lemma_Vale.X64.Stack_i.lemma_frame_store_load_taint_stack64",
        "lemma_Vale.X64.Stack_i.lemma_free_stack_same_load64",
        "lemma_Vale.X64.Stack_i.lemma_free_stack_same_valid64",
        "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64",
        "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64",
        "lemma_Vale.X64.Stack_i.lemma_store_new_valid64",
        "lemma_Vale.X64.Stack_i.lemma_store_stack_same_valid64",
        "lemma_Vale.X64.Xmms.lemma_equal_intro",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.X64.Machine_s.OReg_r",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_stack",
        "projection_inverse_Vale.X64.State.Mkstate_stackTaint",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_09d9ae2b4f83e9874aa98bae7c20bcb4",
        "refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_416d0f805341e247c88dc3b5c65a99d4",
        "refinement_interpretation_Tm_refine_4c6411da037541583c16876f5cc7dfe4",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
        "refinement_interpretation_Tm_refine_5a095228b42e02d151869a67c26c9d46",
        "refinement_interpretation_Tm_refine_809440a2e49ae18d732467ba1f4c9c0b",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing",
        "token_correspondence_Vale.Def.Opaque_s.make_opaque",
        "typing_FStar.Seq.Base.length",
        "typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
        "typing_Prims.eq2", "typing_Prims.l_and",
        "typing_Tm_abs_13753bb938b891fdfbf384b1a4ab366b",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_54b8de3c88d3a55b95472c72a59cbb84",
        "typing_Tm_abs_5999f86f25d0e89d9c17ed056edbd9ee",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955",
        "typing_Tm_abs_eb89030da729ba6848a11b6d8cfce1b7",
        "typing_Vale.AES.AES_s.key_to_round_keys_LE",
        "typing_Vale.Arch.Types.hi64", "typing_Vale.Arch.Types.lo64",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
        "typing_Vale.Lib.Workarounds.slice_work_around",
        "typing_Vale.X64.Decls.va_if", "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.validSrcAddrs128",
        "typing_Vale.X64.Memory.base_typ_as_vale_type",
        "typing_Vale.X64.Memory.buffer_as_seq",
        "typing_Vale.X64.Memory.buffer_length",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.Memory.buffer_readable",
        "typing_Vale.X64.Memory.buffer_write",
        "typing_Vale.X64.Memory.buffer_writeable",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.loc_union",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp",
        "typing_Vale.X64.Stack_i.store_stack64",
        "typing_Vale.X64.Stack_i.store_taint_stack64",
        "typing_Vale.X64.Stack_i.valid_src_stack64",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__memTaint",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__stack",
        "typing_Vale.X64.State.__proj__Mkstate__item__stackTaint",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.eta_sel",
        "typing_tok_Vale.Interop.Types.TUInt128@tok",
        "typing_tok_Vale.X64.Machine_s.Public@tok",
        "typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_typing"
      ],
      0,
      "5eac023760e0d985d3aee08114c4290a"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wp_gcm_encrypt2_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256",
        "constructor_distinct_Vale.Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.Interop.Types.TUInt128@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Arch.Types.be_quad32_to_bytes",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq16",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Tm_abs_b39953460d24ff94efd756bca22ff955",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_tok_Vale.Interop.Types.TUInt128@tok"
      ],
      0,
      "c700a47a2ed3f89658b62a7c49cd23bc"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpMonotone_gcm_encrypt2_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_encrypt2_stdcall",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_stack",
        "typing_Vale.X64.Decls.va_upd_stackTaint",
        "typing_Vale.X64.Decls.va_upd_xmm",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "2379e78835c15a318a570910934cfddd"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_encrypt2_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp", "equality_tok_Vale.X64.Machine_s.Secret@tok",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_encrypt2_stdcall",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.validDstAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "interpretation_Tm_abs_13753bb938b891fdfbf384b1a4ab366b",
        "interpretation_Tm_abs_1d0ea341528c48d92877010c57ce4ff9",
        "interpretation_Tm_abs_507f9cafead0b42f24bf04afe924f7a8",
        "interpretation_Tm_abs_54b8de3c88d3a55b95472c72a59cbb84",
        "interpretation_Tm_abs_5999f86f25d0e89d9c17ed056edbd9ee",
        "interpretation_Tm_abs_66f98bf01443a163a32ed74e878b1449",
        "interpretation_Tm_abs_79e3144b840e64bf1793423679505bba",
        "interpretation_Tm_abs_84d9a131ff4d9bba2a844d01c003f500",
        "interpretation_Tm_abs_ab9099bf78ce47359668367da17f9e41",
        "interpretation_Tm_abs_ae6250f4283913a9dc13608eff7f3dd7",
        "interpretation_Tm_abs_b69df0586b4aacb0493632ef0f172952",
        "interpretation_Tm_abs_b6ab4bccb25ffc708f834aa8d487e389",
        "interpretation_Tm_abs_be709b29b4f28d04784b98539d3ed7ab",
        "interpretation_Tm_abs_bf7e000956736ca2f750622e19e431e5",
        "interpretation_Tm_abs_e42707773e2a8180ca9b8055b23f329c",
        "interpretation_Tm_abs_eb89030da729ba6848a11b6d8cfce1b7",
        "proj_equation_Vale.X64.State.Mkstate_mem", "unit_typing"
      ],
      0,
      "0a75b8174823a0b5eb2ca4c4421fb5e0"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_encrypt2_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "9a0ff6850b31ba2fd3b59ceb05ac5298"
    ],
    [
      "Vale.AES.X64.GCMencrypt.va_wpProof_gcm_encrypt2_stdcall",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.Def.Words.Seq_s_interpretation_Tm_arrow_816baa3f8e222aaee20ed3e2d3992880",
        "bool_inversion", "constructor_distinct_Tm_unit",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_192",
        "constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_encrypt2_stdcall",
        "equation_Vale.AES.X64.GCMencrypt.va_wp_gcm_encrypt2_stdcall",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg",
        "equation_Vale.X64.Decls.va_upd_stack",
        "equation_Vale.X64.Decls.va_upd_stackTaint",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Decls.validDstAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Machine_s.reg", "equation_Vale.X64.Machine_s.xmm",
        "equation_Vale.X64.QuickCode.t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_xmm",
        "fuel_guarded_inversion_Vale.X64.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_13753bb938b891fdfbf384b1a4ab366b",
        "interpretation_Tm_abs_1d0ea341528c48d92877010c57ce4ff9",
        "interpretation_Tm_abs_507f9cafead0b42f24bf04afe924f7a8",
        "interpretation_Tm_abs_54b8de3c88d3a55b95472c72a59cbb84",
        "interpretation_Tm_abs_5999f86f25d0e89d9c17ed056edbd9ee",
        "interpretation_Tm_abs_66f98bf01443a163a32ed74e878b1449",
        "interpretation_Tm_abs_79e3144b840e64bf1793423679505bba",
        "interpretation_Tm_abs_84d9a131ff4d9bba2a844d01c003f500",
        "interpretation_Tm_abs_ab9099bf78ce47359668367da17f9e41",
        "interpretation_Tm_abs_ae6250f4283913a9dc13608eff7f3dd7",
        "interpretation_Tm_abs_b69df0586b4aacb0493632ef0f172952",
        "interpretation_Tm_abs_b6ab4bccb25ffc708f834aa8d487e389",
        "interpretation_Tm_abs_be709b29b4f28d04784b98539d3ed7ab",
        "interpretation_Tm_abs_bf7e000956736ca2f750622e19e431e5",
        "interpretation_Tm_abs_e42707773e2a8180ca9b8055b23f329c",
        "interpretation_Tm_abs_eb89030da729ba6848a11b6d8cfce1b7",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Xmms.lemma_equal_elim",
        "partial_app_typing_a5df2c69070e20952ad8c7ffdfbc7635",
        "proj_equation_Vale.X64.State.Mkstate_flags",
        "proj_equation_Vale.X64.State.Mkstate_mem",
        "proj_equation_Vale.X64.State.Mkstate_memTaint",
        "proj_equation_Vale.X64.State.Mkstate_ok",
        "proj_equation_Vale.X64.State.Mkstate_regs",
        "proj_equation_Vale.X64.State.Mkstate_stack",
        "proj_equation_Vale.X64.State.Mkstate_stackTaint",
        "proj_equation_Vale.X64.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_Vale.X64.State.Mkstate_flags",
        "projection_inverse_Vale.X64.State.Mkstate_mem",
        "projection_inverse_Vale.X64.State.Mkstate_memTaint",
        "projection_inverse_Vale.X64.State.Mkstate_ok",
        "projection_inverse_Vale.X64.State.Mkstate_regs",
        "projection_inverse_Vale.X64.State.Mkstate_stack",
        "projection_inverse_Vale.X64.State.Mkstate_stackTaint",
        "projection_inverse_Vale.X64.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_4c6411da037541583c16876f5cc7dfe4",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Vale.AES.X64.GCMencrypt.va_wpCompute_gcm_encrypt2_stdcall",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Vale.Lib.Seqs_s.seq_map",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg",
        "typing_Vale.X64.Decls.va_upd_stack",
        "typing_Vale.X64.Decls.va_upd_stackTaint",
        "typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.Stack_i.init_rsp",
        "typing_Vale.X64.State.__proj__Mkstate__item__flags",
        "typing_Vale.X64.State.__proj__Mkstate__item__mem",
        "typing_Vale.X64.State.__proj__Mkstate__item__ok",
        "typing_Vale.X64.State.__proj__Mkstate__item__regs",
        "typing_Vale.X64.State.__proj__Mkstate__item__stack",
        "typing_Vale.X64.State.__proj__Mkstate__item__stackTaint",
        "typing_Vale.X64.State.__proj__Mkstate__item__xmms",
        "typing_Vale.X64.Xmms.sel", "unit_typing"
      ],
      0,
      "16ec17d6beb6041f859a21351002a8fb"
    ]
  ]
]

Showing with 0 additions and 0 deletions (0 / 0 diffs computed)

Computing file changes ...