Revision 1068d4afc039dbd12db6dbce298cdb0962d6d224 authored by Aymeric Fromherz on 01 April 2019, 04:39:20 UTC, committed by Aymeric Fromherz on 01 April 2019, 04:39:20 UTC
1 parent d7fe03c
X64.AES128.fst.hints
[
"��.\u001f[\u0013�v�2̹;R�\u000f",
[
[
"X64.AES128.va_qcode_KeyExpansionRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_X64.Machine_s.imm8",
"refinement_interpretation_Tm_refine_ed0c82b529ba35f1d88d0cb19afaf666"
],
0,
"4e59a95ca666ffc4d43d9e83968d4546"
],
[
"X64.AES128.va_lemma_KeyExpansionRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_9e6c4d1f47fc56330c9a82c5ea290690"
],
0,
"c3dc698f210395bdc9e5330ba10ed24f"
],
[
"X64.AES128.va_lemma_KeyExpansionRound",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_AES_helpers.expand_key_128_def.fuel_instrumented",
"@fuel_irrelevance_AES_helpers.expand_key_128_def.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_Tm_unit", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_AES_helpers.expand_key_128",
"equation_AES_helpers.quad32_shl32",
"equation_AES_helpers.round_key_128",
"equation_AES_helpers.simd_round_key_128", "equation_Prims.eq2",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prop_s.prop0", "equation_Types_s.bits_of_byte",
"equation_Types_s.byte_to_twobits", "equation_Types_s.quad32",
"equation_Types_s.select_word", "equation_Types_s.twobits",
"equation_Words.Four_s.four_select", "equation_Words_s.nat2",
"equation_Words_s.nat32", "equation_Words_s.nat64",
"equation_Words_s.nat8", "equation_Words_s.natN",
"equation_X64.Machine_s.imm8", "equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.modifies_buffer_specific128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"equation_with_fuel_AES_helpers.expand_key_128_def.fuel_instrumented",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat2",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"kinding_Words_s.four@tok", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Memory.modifies_buffer_addr",
"lemma_X64.Memory.modifies_buffer_readable",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_Words_s.Mkfour_hi2",
"proj_equation_Words_s.Mkfour_hi3",
"proj_equation_Words_s.Mkfour_lo0",
"proj_equation_Words_s.Mkfour_lo1",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_5bb8ca8bd1e34326f95f9f0f9a641acf",
"refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
"refinement_interpretation_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_ed0c82b529ba35f1d88d0cb19afaf666",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"string_typing",
"token_correspondence_AES_helpers.expand_key_128_def",
"token_correspondence_Opaque_s.make_opaque",
"typing_AES_helpers.expand_key_128",
"typing_AES_helpers.round_key_128_rcon", "typing_AES_s.aes_rcon",
"typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
"typing_Prims.eq2", "typing_Prims.l_and",
"typing_Types_s.byte_to_twobits", "typing_Types_s.select_word",
"typing_Words_s.__proj__Mkfour__item__hi2",
"typing_Words_s.__proj__Mkfour__item__hi3",
"typing_Words_s.__proj__Mkfour__item__lo1",
"typing_X64.CPU_Features_s.aesni_enabled",
"typing_X64.Memory.buffer_addr", "typing_X64.Memory.buffer_as_seq",
"typing_X64.Memory.buffer_read", "typing_X64.Memory.buffer_readable",
"typing_X64.Memory.buffer_write",
"typing_X64.Memory.buffer_writeable", "typing_X64.Memory.loc_buffer",
"typing_X64.Vale.Decls.modifies_buffer_specific128",
"typing_X64.Vale.Decls.validDstAddrs128",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Secret@tok", "unit_inversion",
"unit_typing"
],
0,
"31d695c26dd142b6578317695cca6920"
],
[
"X64.AES128.va_wp_KeyExpansionRound",
1,
1,
0,
[ "@query" ],
0,
"551cb37ae8be4de41a3b04a9b2d70f52"
],
[
"X64.AES128.va_wpMonotone_KeyExpansionRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_X64.AES128.va_wp_KeyExpansionRound",
"equation_X64.Machine_s.xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_xmm", "unit_typing"
],
0,
"d335fb8777ccf52c49d166c7a647a349"
],
[
"X64.AES128.va_wpCompute_KeyExpansionRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AES128.va_wp_KeyExpansionRound",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"4bb9e49709979e60cc7ebd101e087ab2"
],
[
"X64.AES128.va_wpProof_KeyExpansionRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"664cf1070e4d1f49bca1cbf48160a0a2"
],
[
"X64.AES128.va_wpProof_KeyExpansionRound",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat64",
"equation_Words_s.natN",
"equation_X64.AES128.va_wpCompute_KeyExpansionRound",
"equation_X64.AES128.va_wp_KeyExpansionRound",
"equation_X64.Machine_s.xmm", "equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.modifies_buffer_specific128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_X64.Memory.modifies_buffer_addr",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AES128.va_wpCompute_KeyExpansionRound",
"typing_AES_helpers.expand_key_128", "typing_X64.Memory.loc_buffer",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.update_xmm", "typing_X64.Vale.Xmms.sel",
"typing_X64.Vale.Xmms.upd", "typing_tok_Interop.Types.TUInt128@tok",
"unit_typing"
],
0,
"688de8c0cdfa2287d12f57eb58030864"
],
[
"X64.AES128.va_transparent_code_KeyExpansionRoundUnrolledRecursive",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_6d0180d4fcd10237cf0d87dd345d77cc_0",
"equation_AES_s.aes_rcon", "equation_Prims.nat",
"equation_Words_s.nat32", "equation_Words_s.natN", "int_inversion",
"int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad",
"refinement_interpretation_Words_s_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"typing_AES_s.aes_rcon", "well-founded-ordering-on-nat"
],
0,
"21af9a58e0b526f9592c790b6c2d0858"
],
[
"X64.AES128.va_transparent_code_KeyExpansionRoundUnrolledRecursive",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Prims.LexTop@tok",
"int_typing", "projection_inverse_BoxInt_proj_0",
"well-founded-ordering-on-nat"
],
0,
"d7edbd7b03a28ba59c64c776ef9d0d66"
],
[
"X64.AES128.va_lemma_KeyExpansionRoundUnrolledRecursive",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Words_s.nat32",
"refinement_interpretation_Tm_refine_af078a811023c82fb6e2aa84f40ff02e"
],
0,
"fb18df4bd685d382349b62e8de63d21d"
],
[
"X64.AES128.va_lemma_KeyExpansionRoundUnrolledRecursive",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Words_s.nat32",
"refinement_interpretation_Tm_refine_af078a811023c82fb6e2aa84f40ff02e"
],
0,
"2ff8bcb7e2337ef1f9f87443c49488ce"
],
[
"X64.AES128.va_lemma_KeyExpansionRoundUnrolledRecursive",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_AES_helpers.expand_key_128_def.fuel_instrumented",
"@fuel_correspondence_X64.AES128.va_code_KeyExpansionRoundUnrolledRecursive.fuel_instrumented",
"@fuel_correspondence_X64.AES128.va_transparent_code_KeyExpansionRoundUnrolledRecursive.fuel_instrumented",
"@fuel_irrelevance_X64.AES128.va_code_KeyExpansionRoundUnrolledRecursive.fuel_instrumented",
"@fuel_irrelevance_X64.AES128.va_transparent_code_KeyExpansionRoundUnrolledRecursive.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_661f8a7e3bd81eb0a2bc263395f5dddc_1",
"binder_x_6d0180d4fcd10237cf0d87dd345d77cc_4",
"binder_x_dc562848c16e0cba66fd6b1d2deb3252_2",
"binder_x_fe088cebb0ded7cb1ab9490a140fe934_3", "bool_inversion",
"bool_typing", "constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_Prims.Cons",
"constructor_distinct_X64.Machine_s.Block",
"disc_equation_Prims.Cons", "disc_equation_X64.Machine_s.Block",
"eq2-interp", "equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_AES_helpers.expand_key_128", "equation_AES_s.aes_rcon",
"equation_Prims.nat", "equation_Types_s.quad32",
"equation_Words_s.nat32", "equation_Words_s.natN",
"equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.modifies_buffer_specific128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"equation_with_fuel_AES_helpers.expand_key_128_def.fuel_instrumented",
"equation_with_fuel_X64.AES128.va_code_KeyExpansionRoundUnrolledRecursive.fuel_instrumented",
"equation_with_fuel_X64.AES128.va_transparent_code_KeyExpansionRoundUnrolledRecursive.fuel_instrumented",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Opaque_s.make_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"lemma_X64.Memory.loc_includes_refl",
"lemma_X64.Memory.modifies_buffer_addr",
"lemma_X64.Memory.modifies_goal_directed_refl",
"lemma_X64.Memory.modifies_goal_directed_trans",
"lemma_X64.Memory.modifies_goal_directed_trans2",
"lemma_X64.Memory.modifies_refl",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_upd_eq",
"lemma_X64.Vale.Xmms.lemma_upd_ne", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual", "proj_equation_Prims.Cons_hd",
"proj_equation_Prims.Cons_tl", "proj_equation_Words_s.Mkfour_hi2",
"proj_equation_Words_s.Mkfour_hi3",
"proj_equation_Words_s.Mkfour_lo0",
"proj_equation_Words_s.Mkfour_lo1",
"proj_equation_X64.Machine_s.Block_block",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_X64.Machine_s.Block_block",
"projection_inverse_X64.Machine_s.Block_t_ins",
"projection_inverse_X64.Machine_s.Block_t_ocmp",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_9b586769ce9055ff9a2af06f49d5ce52",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_cc8275a6b7ea31b70a4f3042d3d59809",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_AES_helpers.expand_key_128_def",
"token_correspondence_X64.AES128.va_code_KeyExpansionRoundUnrolledRecursive.fuel_instrumented",
"typing_AES_s.aes_rcon", "typing_Words.Seq_s.four_to_seq_LE",
"typing_X64.AES128.va_lemma_KeyExpansionRoundUnrolledRecursive",
"typing_X64.CPU_Features_s.aesni_enabled",
"typing_X64.Memory.buffer_read", "typing_X64.Memory.loc_buffer",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
"typing_tok_Interop.Types.TUInt128@tok",
"well-founded-ordering-on-nat"
],
0,
"4ccd6d373ad999c2b6c8d4a30d9b71e2"
],
[
"X64.AES128.va_wp_KeyExpansionRoundUnrolledRecursive",
1,
1,
0,
[ "@query" ],
0,
"e16c095d1be8dcbdde5707c471ce1bff"
],
[
"X64.AES128.va_wpMonotone_KeyExpansionRoundUnrolledRecursive",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_X64.AES128.va_wp_KeyExpansionRoundUnrolledRecursive",
"equation_X64.Machine_s.xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_xmm", "unit_typing"
],
0,
"726c1385723df3751ad31649a56ff547"
],
[
"X64.AES128.va_wpCompute_KeyExpansionRoundUnrolledRecursive",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_X64.AES128.va_code_KeyExpansionRoundUnrolledRecursive.fuel_instrumented",
"@query", "eq2-interp",
"equation_X64.AES128.va_wp_KeyExpansionRoundUnrolledRecursive",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion"
],
0,
"ea627bd90a9cd86037320c21daaeb30c"
],
[
"X64.AES128.va_wpProof_KeyExpansionRoundUnrolledRecursive",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"efd06519b28e2da4964b118bec1252c2"
],
[
"X64.AES128.va_wpProof_KeyExpansionRoundUnrolledRecursive",
2,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_X64.AES128.va_code_KeyExpansionRoundUnrolledRecursive.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_X64.AES128.va_wpCompute_KeyExpansionRoundUnrolledRecursive",
"equation_X64.AES128.va_wp_KeyExpansionRoundUnrolledRecursive",
"equation_X64.Machine_s.xmm", "equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_X64.Memory.modifies_buffer_addr",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AES128.va_wpCompute_KeyExpansionRoundUnrolledRecursive",
"typing_X64.Memory.loc_buffer", "typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_tok_Interop.Types.TUInt128@tok",
"unit_typing"
],
0,
"a21d53005ff2a2d6aa0c5f96bca21418"
],
[
"X64.AES128.va_qcode_KeyExpansion128Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Words_s.nat64", "equation_Words_s.natN",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad",
"refinement_interpretation_Words_s_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98"
],
0,
"08ebf02d9479160e00710a9e4c7f0f5b"
],
[
"X64.AES128.va_qcode_KeyExpansion128Stdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_AES_s.nb",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_9cb82c4ebe6abcb785bea99f8b687bdd",
"refinement_interpretation_Tm_refine_cc6b282658fa00092f7d9fca3f46a5ff"
],
0,
"d2ea3fe5fb048ea4237f2c4c79c9812a"
],
[
"X64.AES128.va_qcode_KeyExpansion128Stdcall",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Tm_unit", "disc_equation_AES_s.AES_128",
"disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
"eq2-interp", "equation_AES_s.is_aes_key_LE", "equation_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_inversion",
"refinement_interpretation_Tm_refine_5fd34245ddc7869ed9e5b41013d142e5",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length"
],
0,
"ba1d0c6a5fc471f9ccf3911a25964c9b"
],
[
"X64.AES128.va_qcode_KeyExpansion128Stdcall",
4,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Tm_unit", "disc_equation_AES_s.AES_128",
"disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
"eq2-interp", "equation_AES_s.is_aes_key_LE", "equation_Prims.nat",
"equation_Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_inversion",
"refinement_interpretation_Tm_refine_5fd34245ddc7869ed9e5b41013d142e5",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length"
],
0,
"b4e741992a000789849e4c28949d9c6b"
],
[
"X64.AES128.va_lemma_KeyExpansion128Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_AES_s.AES_128",
"constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
"equality_tok_AES_s.AES_128@tok",
"equality_tok_Interop.Types.TUInt128@tok",
"equation_AES_s.is_aes_key_LE", "equation_Types_s.quad32",
"equation_Words.Seq_s.seq4", "equation_Words.Seq_s.seqn",
"equation_Words_s.nat32",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_typing",
"proj_equation_X64.Vale.State.Mkstate_mem",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_9b586769ce9055ff9a2af06f49d5ce52",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"typing_Words.Seq_s.four_to_seq_LE", "typing_X64.Memory.buffer_read",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_tok_Interop.Types.TUInt128@tok"
],
0,
"1b084ff73e9ac74400990d2b8b822b8a"
],
[
"X64.AES128.va_lemma_KeyExpansion128Stdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_AES_s.AES_128",
"constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
"equality_tok_AES_s.AES_128@tok",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_AES_s.is_aes_key_LE",
"equation_AES_s.key_to_round_keys_LE",
"equation_AES_s.key_to_round_keys_LE_def", "equation_AES_s.nb",
"equation_Prims.eqtype", "equation_Prims.l_and",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash", "equation_Prop_s.prop0",
"equation_Types_s.quad32", "equation_Words.Seq_s.seq4",
"equation_Words.Seq_s.seqn", "equation_Words_s.nat32",
"equation_Words_s.nat64",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Opaque_s.make_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"interpretation_Tm_abs_11b846de738c2179f7d8a25fd5d8134c",
"interpretation_Tm_abs_178adea34d6d184de0dd7630dfe339be",
"interpretation_Tm_abs_1a66d9ca182b0d13ee08d2b4b97bb5fc",
"interpretation_Tm_abs_1d56deaaa71b4a0e09272738adc9090f",
"interpretation_Tm_abs_2844933a82876741a8e31b086bd1275e",
"interpretation_Tm_abs_5d1b6dcf0c77908e08d25fd35682a6dd",
"interpretation_Tm_abs_cf511aacfa266870cb915fb5be9ad81d",
"interpretation_Tm_abs_e988f1da8f33ba5baefc252f5430ac45",
"l_and-interp", "l_quant_interp_f583da302ed51c9e579cdff41a2c44cd",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Memory.loc_includes_refl",
"lemma_X64.Memory.modifies_buffer_addr",
"lemma_X64.Memory.modifies_buffer_readable",
"lemma_X64.Memory.modifies_goal_directed_refl",
"lemma_X64.Memory.modifies_goal_directed_trans",
"lemma_X64.Memory.modifies_goal_directed_trans2",
"lemma_X64.Memory.modifies_valid_taint128",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5bb8ca8bd1e34326f95f9f0f9a641acf",
"refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
"refinement_interpretation_Tm_refine_9b586769ce9055ff9a2af06f49d5ce52",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing",
"token_correspondence_AES_s.key_to_round_keys_LE_def",
"typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
"typing_Prims.l_Forall", "typing_Prims.l_and",
"typing_Tm_abs_78368066d9a990c770e0a965f98b616a",
"typing_Types_s.quad32", "typing_Words.Seq_s.four_to_seq_LE",
"typing_X64.Memory.buffer_addr", "typing_X64.Memory.buffer_as_seq",
"typing_X64.Memory.buffer_read", "typing_X64.Memory.buffer_readable",
"typing_X64.Memory.buffer_write",
"typing_X64.Memory.buffer_writeable", "typing_X64.Memory.loc_buffer",
"typing_X64.Memory.modifies",
"typing_X64.Vale.Decls.validDstAddrs128",
"typing_X64.Vale.Decls.validSrcAddrs128",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok",
"typing_tok_X64.Machine_s.Secret@tok", "unit_inversion",
"unit_typing"
],
0,
"cab5e1f44ddc5b9fe7e6da9f9350de68"
],
[
"X64.AES128.va_wp_KeyExpansion128Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_AES_s.AES_128",
"constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
"equality_tok_AES_s.AES_128@tok",
"equality_tok_Interop.Types.TUInt128@tok",
"equation_AES_s.is_aes_key_LE", "equation_Types_s.quad32",
"equation_Words.Seq_s.seq4", "equation_Words.Seq_s.seqn",
"equation_Words_s.nat32",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_typing",
"proj_equation_X64.Vale.State.Mkstate_mem",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_9b586769ce9055ff9a2af06f49d5ce52",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"typing_Words.Seq_s.four_to_seq_LE", "typing_X64.Memory.buffer_read",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_tok_Interop.Types.TUInt128@tok"
],
0,
"3a4ae1512ef4d1f59185866c6c591f2e"
],
[
"X64.AES128.va_wpMonotone_KeyExpansion128Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equality_tok_X64.Machine_s.Rdx@tok",
"equation_X64.AES128.va_wp_KeyExpansion128Stdcall",
"equation_X64.Machine_s.xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_tok_X64.Machine_s.Rdx@tok", "unit_typing"
],
0,
"14ed60ba8b2d7c1f587396ffaf480471"
],
[
"X64.AES128.va_wpCompute_KeyExpansion128Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Secret@tok",
"equation_Words_s.nat64",
"equation_X64.AES128.va_wp_KeyExpansion128Stdcall",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"fuel_guarded_inversion_X64.Vale.State.state",
"interpretation_Tm_abs_11b846de738c2179f7d8a25fd5d8134c",
"interpretation_Tm_abs_1a66d9ca182b0d13ee08d2b4b97bb5fc",
"interpretation_Tm_abs_1d56deaaa71b4a0e09272738adc9090f",
"interpretation_Tm_abs_cf511aacfa266870cb915fb5be9ad81d",
"proj_equation_X64.Vale.State.Mkstate_mem", "unit_typing"
],
0,
"eb0c9bd5173901dc9e2339002c99c8ca"
],
[
"X64.AES128.va_wpProof_KeyExpansion128Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"1910f7baf6784687d73bfccf6f816dc1"
],
[
"X64.AES128.va_wpProof_KeyExpansion128Stdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Words_s.nat64",
"equation_X64.AES128.va_wpCompute_KeyExpansion128Stdcall",
"equation_X64.AES128.va_wp_KeyExpansion128Stdcall",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"interpretation_Tm_abs_11b846de738c2179f7d8a25fd5d8134c",
"interpretation_Tm_abs_1a66d9ca182b0d13ee08d2b4b97bb5fc",
"interpretation_Tm_abs_1d56deaaa71b4a0e09272738adc9090f",
"interpretation_Tm_abs_cf511aacfa266870cb915fb5be9ad81d",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AES128.va_wpCompute_KeyExpansion128Stdcall",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_tok_X64.Machine_s.Rdx@tok",
"unit_typing"
],
0,
"018e75a9e5870b3ae6353c38c0d65964"
],
[
"X64.AES128.va_lemma_AES128EncryptRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"refinement_interpretation_Tm_refine_b198bd9efc097e953e03737e592b7e6e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"6d6d48987e1a5dc6e846dc0d0b9c87da"
],
[
"X64.AES128.va_lemma_AES128EncryptRound",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_AES_s.rounds.fuel_instrumented",
"@fuel_irrelevance_AES_s.rounds.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_AES_s.round",
"equation_Prims.eq2", "equation_Prims.logical", "equation_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"equation_with_fuel_AES_s.rounds.fuel_instrumented",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"kinding_Words_s.four@tok",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"primitive_Prims.op_Equality",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"string_typing", "typing_AES_s.rounds", "typing_Prims.eq2",
"typing_X64.CPU_Features_s.aesni_enabled",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
"typing_tok_X64.Machine_s.R8@tok", "unit_inversion", "unit_typing"
],
0,
"8e74c68c352ccfaf73508dd6459c3715"
],
[
"X64.AES128.va_wp_AES128EncryptRound",
1,
1,
0,
[ "@query" ],
0,
"4254c79f857ae5ef5f804b8a0784bc5e"
],
[
"X64.AES128.va_wpMonotone_AES128EncryptRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_X64.AES128.va_wp_AES128EncryptRound",
"equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.State.update_xmm", "unit_typing"
],
0,
"fe1eaa8635240f2912b9d126c30cde37"
],
[
"X64.AES128.va_wpCompute_AES128EncryptRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AES128.va_wp_AES128EncryptRound",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"a7fc15616b881e1d69f5b30edf711966"
],
[
"X64.AES128.va_wpProof_AES128EncryptRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"252e2234f5ce0b9f32539afe1acc377e"
],
[
"X64.AES128.va_wpProof_AES128EncryptRound",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Prims.nat", "equation_Types_s.quad32",
"equation_Words_s.nat32",
"equation_X64.AES128.va_wpCompute_AES128EncryptRound",
"equation_X64.AES128.va_wp_AES128EncryptRound",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AES128.va_wpCompute_AES128EncryptRound",
"typing_AES_s.rounds", "typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd", "unit_typing"
],
0,
"782f0b7d52417a7bf11cef197159a1ec"
],
[
"X64.AES128.va_qcode_AES128EncryptBlock",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"86d311f8398560f29ad9f3050635abd3"
],
[
"X64.AES128.va_lemma_AES128EncryptBlock",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_90ae01a890cdd020e0797ad7ddfeacf9"
],
0,
"4a09bf322b444f695c1d8c97f5127100"
],
[
"X64.AES128.va_lemma_AES128EncryptBlock",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_AES_s.rounds.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_AES_s.AES_128", "eq2-interp",
"equality_tok_AES_s.AES_128@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_AES_s.aes_encrypt_LE_def", "equation_AES_s.cipher",
"equation_AES_s.is_aes_key_LE", "equation_Prims.eq2",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"equation_with_fuel_AES_s.rounds.fuel_instrumented",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_typing",
"kinding_Words_s.four@tok",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"primitive_Prims.op_Equality",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_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_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"string_typing", "typing_AES_s.aes_encrypt_LE_def",
"typing_FStar.Seq.Base.length", "typing_Prims.eq2",
"typing_X64.CPU_Features_s.aesni_enabled",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
"typing_tok_AES_s.AES_128@tok", "typing_tok_X64.Machine_s.R8@tok",
"unit_inversion", "unit_typing"
],
0,
"468f9f930f66fe3d8a06a8b03c5dd7a3"
],
[
"X64.AES128.va_wp_AES128EncryptBlock",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"d7e95d29005c30be8fe950245134eac7"
],
[
"X64.AES128.va_wpMonotone_AES128EncryptBlock",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_X64.AES128.va_wp_AES128EncryptBlock",
"equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.State.update_xmm", "unit_typing"
],
0,
"fe435a0a508ef87107056b2b9066e382"
],
[
"X64.AES128.va_wpCompute_AES128EncryptBlock",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AES128.va_wp_AES128EncryptBlock",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"feb8edf2653d1dbaa84327ce1a65bdef"
],
[
"X64.AES128.va_wpProof_AES128EncryptBlock",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"52360aee1927ba0dfd5bfef92cfceddf"
],
[
"X64.AES128.va_wpProof_AES128EncryptBlock",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_AES_s.AES_128@tok", "equation_Prims.eq2",
"equation_Prims.squash", "equation_Types_s.quad32",
"equation_X64.AES128.va_wpCompute_AES128EncryptBlock",
"equation_X64.AES128.va_wp_AES128EncryptBlock",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Prims.equals",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AES128.va_wpCompute_AES128EncryptBlock",
"typing_AES_s.aes_encrypt_LE_def", "typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
"typing_tok_AES_s.AES_128@tok", "unit_typing"
],
0,
"9e624458110f21ad5c4676580df39cdc"
],
[
"X64.AES128.va_qcode_AES128EncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"equality_tok_AES_s.AES_128@tok", "equation_AES_s.is_aes_key_LE",
"equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"unit_typing"
],
0,
"7edbe80fef02464e49cb27271a5d5899"
],
[
"X64.AES128.va_lemma_AES128EncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_7c8e6c19124a9b2a04755ce299b5b085",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rsi@tok"
],
0,
"1e60d4f7568aab0c365b46dada2651e1"
],
[
"X64.AES128.va_lemma_AES128EncryptBlockStdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_AES_s.AES_128",
"constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
"equality_tok_AES_s.AES_128@tok",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_AES_s.aes_encrypt_LE_def",
"equation_AES_s.key_to_round_keys_LE", "equation_Prims.eq2",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prop_s.prop0", "equation_Types_s.quad32",
"equation_Words_s.nat32", "equation_Words_s.nat64",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.l_and",
"function_token_typing_Words_s.nat32", "int_typing",
"interpretation_Tm_abs_11b846de738c2179f7d8a25fd5d8134c",
"interpretation_Tm_abs_178adea34d6d184de0dd7630dfe339be",
"interpretation_Tm_abs_1a66d9ca182b0d13ee08d2b4b97bb5fc",
"interpretation_Tm_abs_e988f1da8f33ba5baefc252f5430ac45",
"kinding_Words_s.four@tok", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Memory.modifies_buffer_addr",
"lemma_X64.Memory.modifies_buffer_readable",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_5bb8ca8bd1e34326f95f9f0f9a641acf",
"refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_interpretation_Tm_refine_fbd1322eaad6b0eab99798f0e8856c8e",
"string_typing", "typing_AES_s.aes_encrypt_LE_def",
"typing_AES_s.key_to_round_keys_LE",
"typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
"typing_Prims.eq2", "typing_Prims.l_and",
"typing_X64.Memory.buffer_addr", "typing_X64.Memory.buffer_as_seq",
"typing_X64.Memory.buffer_read", "typing_X64.Memory.buffer_readable",
"typing_X64.Memory.buffer_write",
"typing_X64.Memory.buffer_writeable", "typing_X64.Memory.loc_buffer",
"typing_X64.Memory.modifies",
"typing_X64.Vale.Decls.validSrcAddrs128",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_tok_AES_s.AES_128@tok",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.R8@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok",
"typing_tok_X64.Machine_s.Secret@tok", "unit_typing"
],
0,
"1a21ec48a5095b56c7184e7649f507a7"
],
[
"X64.AES128.va_wp_AES128EncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"equation_Prims.nat", "equation_Words_s.nat64",
"equation_Words_s.natN", "equation_X64.Vale.Decls.va_if",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Words_s.nat64",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad",
"refinement_interpretation_Words_s_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"typing_X64.AES128_Tm_abs_0b85c5cdf81ff9d981d06a423bf17bd6",
"typing_X64.AES128_Tm_abs_494c4553ff5247f2c81506c212bacc26",
"typing_X64.AES128_Tm_abs_50ad851d36622cc25536b7edc233d114",
"typing_X64.AES128_Tm_abs_86b4602d570d0a24c17faa370bd6d79e",
"typing_X64.Vale.Decls.va_if", "unit_typing"
],
0,
"7b00e81f5ba1c73170ba65a0e85eede8"
],
[
"X64.AES128.va_wpMonotone_AES128EncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equality_tok_X64.Machine_s.R8@tok",
"equation_X64.AES128.va_wp_AES128EncryptBlockStdcall",
"equation_X64.Machine_s.xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_tok_X64.Machine_s.R8@tok", "unit_typing"
],
0,
"0fbaa7058608a02b2ce681dcbbe41f5e"
],
[
"X64.AES128.va_wpCompute_AES128EncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Secret@tok",
"equation_Words_s.nat64",
"equation_X64.AES128.va_wp_AES128EncryptBlockStdcall",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"fuel_guarded_inversion_X64.Vale.State.state",
"interpretation_Tm_abs_11b846de738c2179f7d8a25fd5d8134c",
"interpretation_Tm_abs_1a66d9ca182b0d13ee08d2b4b97bb5fc",
"interpretation_Tm_abs_1d56deaaa71b4a0e09272738adc9090f",
"interpretation_Tm_abs_37e6950d37c672ed920358e612e03225",
"interpretation_Tm_abs_5e1158cd2d105ad253ac372e98cd91e5",
"interpretation_Tm_abs_cf511aacfa266870cb915fb5be9ad81d",
"proj_equation_X64.Vale.State.Mkstate_mem", "unit_typing"
],
0,
"631c1dfaa74b7bb44c093f5338b797ab"
],
[
"X64.AES128.va_wpProof_AES128EncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"48635774f705df2566ffc1f73d640760"
],
[
"X64.AES128.va_wpProof_AES128EncryptBlockStdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Words_s.nat64",
"equation_X64.AES128.va_wpCompute_AES128EncryptBlockStdcall",
"equation_X64.AES128.va_wp_AES128EncryptBlockStdcall",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"interpretation_Tm_abs_11b846de738c2179f7d8a25fd5d8134c",
"interpretation_Tm_abs_1a66d9ca182b0d13ee08d2b4b97bb5fc",
"interpretation_Tm_abs_1d56deaaa71b4a0e09272738adc9090f",
"interpretation_Tm_abs_37e6950d37c672ed920358e612e03225",
"interpretation_Tm_abs_5e1158cd2d105ad253ac372e98cd91e5",
"interpretation_Tm_abs_cf511aacfa266870cb915fb5be9ad81d",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AES128.va_wpCompute_AES128EncryptBlockStdcall",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_tok_X64.Machine_s.R8@tok",
"unit_typing"
],
0,
"9394f7338ff86021b3d57e6f69210109"
]
]
]
Computing file changes ...
