Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
X64.AESstdcall.fst.hints
[
">��Iu���O��i��",
[
[
"X64.AESstdcall.va_req_AESEncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"equation_Prims.l_and", "equation_Prims.squash",
"equation_Prims.subtype_of",
"l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"unit_typing"
],
0,
"ff47932bf6a97b21942f18302f08d40f"
],
[
"X64.AESstdcall.va_ens_AESEncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.l_and",
"equation_Prims.squash", "equation_Prims.subtype_of",
"equation_X64.AESstdcall.va_req_AESEncryptBlockStdcall",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validSrcAddrs128",
"fuel_guarded_inversion_X64.Vale.State.state",
"l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"unit_typing"
],
0,
"dbf1937e7f179a147398b3706640e76e"
],
[
"X64.AESstdcall.va_qcode_AESEncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Words_s.nat64", "equation_Words_s.natN",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad"
],
0,
"6b96ac31ce1ab04a3f7b1889462c094e"
],
[
"X64.AESstdcall.va_lemma_AESEncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"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_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat64",
"equation_Words_s.natN", "equation_X64.Vale.Decls.validSrcAddrs128",
"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_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_fdc852a9618fb4aec61213f1a577bb7c",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"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"
],
0,
"3aff8252d4adc3062eb235495fc3da02"
],
[
"X64.AESstdcall.va_lemma_AESEncryptBlockStdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"bool_inversion", "constructor_distinct_AES_s.AES_128",
"constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
"equality_tok_AES_s.AES_128@tok",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_Interop.Types.TUInt64@tok",
"equality_tok_X64.Machine_s.Public@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.Rsp@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_AES_s.aes_encrypt_LE_def", "equation_AES_s.cipher",
"equation_AES_s.key_to_round_keys_LE", "equation_Prims.eq2",
"equation_Prims.l_imp", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Prop_s.prop0", "equation_Types_s.quad32",
"equation_Words_s.nat32", "equation_Words_s.nat64",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128", "equation_X64.Memory.buffer64",
"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_xmm",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.Decls.valid_stack_slots",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"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_2844933a82876741a8e31b086bd1275e",
"interpretation_Tm_abs_42acf2b4bd61f7d087f311642b137700",
"interpretation_Tm_abs_44144a0b97e18fdd9f5d2af93d3a00d4",
"interpretation_Tm_abs_5d1b6dcf0c77908e08d25fd35682a6dd",
"interpretation_Tm_abs_6c5bc4fed00eef24fbbef441860c7e51",
"interpretation_Tm_abs_e7b42242d9c12fea100903f5ef74c36d",
"interpretation_Tm_abs_e988f1da8f33ba5baefc252f5430ac45",
"interpretation_Tm_abs_efed28e5237cc814be518263d6481a87",
"kinding_Words_s.four@tok", "l_imp-interp", "l_not-interp",
"lemma_X64.Memory.loc_includes_refl",
"lemma_X64.Memory.loc_includes_union_l_buffer",
"lemma_X64.Memory.modifies_buffer_addr",
"lemma_X64.Memory.modifies_buffer_elim",
"lemma_X64.Memory.modifies_buffer_readable",
"lemma_X64.Memory.modifies_goal_directed_refl",
"lemma_X64.Memory.modifies_goal_directed_trans",
"lemma_X64.Memory.modifies_goal_directed_trans2",
"lemma_X64.Memory.modifies_valid_taint128",
"lemma_X64.Memory.modifies_valid_taint64",
"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",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_interpretation_Tm_refine_fbd1322eaad6b0eab99798f0e8856c8e",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_AES_s.key_to_round_keys_LE",
"typing_AES_s.rounds", "typing_AES_s.shift_rows_LE",
"typing_AES_s.sub_bytes", "typing_FStar.Seq.Base.index",
"typing_Prims.eq2", "typing_Types_s.quad32_xor",
"typing_X64.Memory.buffer_addr", "typing_X64.Memory.buffer_read",
"typing_X64.Memory.loc_buffer", "typing_X64.Memory.loc_union",
"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_Interop.Types.TUInt64@tok",
"typing_tok_X64.Machine_s.Public@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.Rsp@tok",
"typing_tok_X64.Machine_s.Secret@tok", "unit_typing"
],
0,
"ba85960078bf554b38545026ddc98f97"
],
[
"X64.AESstdcall.va_wp_AESEncryptBlockStdcall",
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_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad",
"typing_X64.AES256_Tm_abs_0b85c5cdf81ff9d981d06a423bf17bd6",
"typing_X64.AES256_Tm_abs_494c4553ff5247f2c81506c212bacc26",
"typing_X64.AES256_Tm_abs_50ad851d36622cc25536b7edc233d114",
"typing_X64.AES256_Tm_abs_86b4602d570d0a24c17faa370bd6d79e",
"typing_X64.Vale.Decls.va_if", "unit_typing"
],
0,
"e9e49419f292d1d9045d13ac33183f62"
],
[
"X64.AESstdcall.va_wpMonotone_AESEncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_AES_s.AES_128",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R11@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R13@tok",
"equality_tok_X64.Machine_s.R14@tok",
"equality_tok_X64.Machine_s.R15@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rbp@tok",
"equality_tok_X64.Machine_s.Rbx@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Rsp@tok",
"equation_X64.AESstdcall.va_wp_AESEncryptBlockStdcall",
"equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_reg",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.update_reg",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R11@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R13@tok",
"typing_tok_X64.Machine_s.R14@tok",
"typing_tok_X64.Machine_s.R15@tok",
"typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rbp@tok",
"typing_tok_X64.Machine_s.Rbx@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"5d4700fa6109f9939026c87152fdfa5d"
],
[
"X64.AESstdcall.va_wpCompute_AESEncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Secret@tok",
"equation_X64.AESstdcall.va_wp_AESEncryptBlockStdcall",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.validSrcAddrs128",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"interpretation_Tm_abs_42acf2b4bd61f7d087f311642b137700",
"interpretation_Tm_abs_efed28e5237cc814be518263d6481a87",
"proj_equation_X64.Vale.State.Mkstate_mem",
"projection_inverse_BoxBool_proj_0", "unit_typing"
],
0,
"5908ea592a1dcce048b24cd250f03749"
],
[
"X64.AESstdcall.va_wpProof_AESEncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"0df21e08e9d69a65340e012efba46941"
],
[
"X64.AESstdcall.va_wpProof_AESEncryptBlockStdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_AES_s.AES_128", "eq2-interp",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R11@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R13@tok",
"equality_tok_X64.Machine_s.R14@tok",
"equality_tok_X64.Machine_s.R15@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rbp@tok",
"equality_tok_X64.Machine_s.Rbx@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Rsp@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_X64.AESstdcall.va_wpCompute_AESEncryptBlockStdcall",
"equation_X64.AESstdcall.va_wp_AESEncryptBlockStdcall",
"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.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_42acf2b4bd61f7d087f311642b137700",
"interpretation_Tm_abs_efed28e5237cc814be518263d6481a87",
"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_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESstdcall.va_wpCompute_AESEncryptBlockStdcall",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.update_reg", "typing_X64.Vale.Xmms.sel",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R11@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R13@tok",
"typing_tok_X64.Machine_s.R14@tok",
"typing_tok_X64.Machine_s.R15@tok",
"typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rbp@tok",
"typing_tok_X64.Machine_s.Rbx@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"8a2e2250f99798529f9afa7b2cab3615"
],
[
"X64.AESstdcall.va_req_aes_EncryptBlockBEStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"equation_Prims.l_and", "equation_Prims.squash",
"equation_Prims.subtype_of",
"l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"unit_typing"
],
0,
"e085116e8f0a1a76eb607ee34bb0c71f"
],
[
"X64.AESstdcall.va_ens_aes_EncryptBlockBEStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.l_and",
"equation_Prims.squash", "equation_Prims.subtype_of",
"equation_X64.AESstdcall.va_req_aes_EncryptBlockBEStdcall",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validSrcAddrs128",
"fuel_guarded_inversion_X64.Vale.State.state",
"l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"unit_typing"
],
0,
"d7a59ed68c6986a4fdfc61c254cab036"
],
[
"X64.AESstdcall.va_qcode_aes_EncryptBlockBEStdcall",
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,
"8e22e29bc81a62eb6dd2300be79ee280"
],
[
"X64.AESstdcall.va_lemma_aes_EncryptBlockBEStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"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_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat64",
"equation_Words_s.natN", "equation_X64.Vale.Decls.validSrcAddrs128",
"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_43580de98879f60203ee24975ed9b4ab",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"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"
],
0,
"4e24fd46822ec57dc1fd2a7ff9d655ae"
],
[
"X64.AESstdcall.va_lemma_aes_EncryptBlockBEStdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"bool_inversion", "constructor_distinct_AES_s.AES_128",
"constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_X64.Machine_s.Rax",
"disc_equation_X64.Machine_s.Rsp", "eq2-interp",
"equality_tok_AES_s.AES_128@tok",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_Interop.Types.TUInt64@tok",
"equality_tok_X64.Machine_s.Public@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Rsp@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_AES_s.key_to_round_keys_LE",
"equation_GCTR.aes_encrypt_BE", "equation_GCTR.aes_encrypt_le",
"equation_Prims.eq2", "equation_Prims.l_imp",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash", "equation_Prop_s.prop0",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.nat64",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128", "equation_X64.Memory.buffer64",
"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_xmm",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.Decls.valid_stack_slots",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_AES_s.aes_encrypt_LE_def",
"function_token_typing_Opaque_s.make_opaque",
"function_token_typing_Prims.__cache_version_number__",
"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_42acf2b4bd61f7d087f311642b137700",
"interpretation_Tm_abs_e988f1da8f33ba5baefc252f5430ac45",
"interpretation_Tm_abs_efed28e5237cc814be518263d6481a87",
"kinding_Words_s.four@tok", "l_and-interp", "l_imp-interp",
"l_not-interp", "lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Memory.loc_includes_refl",
"lemma_X64.Memory.loc_includes_union_l_buffer",
"lemma_X64.Memory.modifies_buffer_addr",
"lemma_X64.Memory.modifies_buffer_elim",
"lemma_X64.Memory.modifies_buffer_readable",
"lemma_X64.Memory.modifies_goal_directed_refl",
"lemma_X64.Memory.modifies_goal_directed_trans",
"lemma_X64.Memory.modifies_goal_directed_trans2",
"lemma_X64.Memory.modifies_valid_taint128",
"lemma_X64.Memory.modifies_valid_taint64",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"proj_equation_X64.Machine_s.OReg_r",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_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",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_AES_s.key_to_round_keys_LE",
"typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
"typing_GCTR.aes_encrypt_BE", "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.loc_union", "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_Interop.Types.TUInt64@tok",
"typing_tok_X64.Machine_s.Public@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.Rsp@tok",
"typing_tok_X64.Machine_s.Secret@tok", "unit_inversion",
"unit_typing"
],
0,
"5e08d84c10ed3cb93f287b1efe2baf61"
],
[
"X64.AESstdcall.va_wp_aes_EncryptBlockBEStdcall",
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_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad",
"typing_X64.AES256_Tm_abs_0b85c5cdf81ff9d981d06a423bf17bd6",
"typing_X64.AES256_Tm_abs_494c4553ff5247f2c81506c212bacc26",
"typing_X64.AES256_Tm_abs_50ad851d36622cc25536b7edc233d114",
"typing_X64.AES256_Tm_abs_86b4602d570d0a24c17faa370bd6d79e",
"typing_X64.Vale.Decls.va_if", "unit_typing"
],
0,
"69471b08bf79ee840f1e5a951b40d0a8"
],
[
"X64.AESstdcall.va_wpMonotone_aes_EncryptBlockBEStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_AES_s.AES_128",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R11@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R13@tok",
"equality_tok_X64.Machine_s.R14@tok",
"equality_tok_X64.Machine_s.R15@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rbp@tok",
"equality_tok_X64.Machine_s.Rbx@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Rsp@tok",
"equation_X64.AESstdcall.va_wp_aes_EncryptBlockBEStdcall",
"equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_reg",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.update_reg",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R11@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R13@tok",
"typing_tok_X64.Machine_s.R14@tok",
"typing_tok_X64.Machine_s.R15@tok",
"typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rbp@tok",
"typing_tok_X64.Machine_s.Rbx@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"92d0f05c97d7a637f7b71f843f13ccc4"
],
[
"X64.AESstdcall.va_wpCompute_aes_EncryptBlockBEStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Secret@tok",
"equation_X64.AESstdcall.va_wp_aes_EncryptBlockBEStdcall",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.validSrcAddrs128",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"interpretation_Tm_abs_42acf2b4bd61f7d087f311642b137700",
"interpretation_Tm_abs_efed28e5237cc814be518263d6481a87",
"proj_equation_X64.Vale.State.Mkstate_mem",
"projection_inverse_BoxBool_proj_0", "unit_typing"
],
0,
"94c842d0dd1d09211b41a379822e032b"
],
[
"X64.AESstdcall.va_wpProof_aes_EncryptBlockBEStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"96adef843df8a2db7343af7cc995336a"
],
[
"X64.AESstdcall.va_wpProof_aes_EncryptBlockBEStdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_AES_s.AES_128", "eq2-interp",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R11@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R13@tok",
"equality_tok_X64.Machine_s.R14@tok",
"equality_tok_X64.Machine_s.R15@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rbp@tok",
"equality_tok_X64.Machine_s.Rbx@tok",
"equality_tok_X64.Machine_s.Rcx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Rsp@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eqtype",
"equation_X64.AESstdcall.va_wpCompute_aes_EncryptBlockBEStdcall",
"equation_X64.AESstdcall.va_wp_aes_EncryptBlockBEStdcall",
"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.validSrcAddrs128",
"equation_X64.Vale.Decls.valid_stack_slots",
"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__",
"function_token_typing_Prims.int", "int_typing",
"interpretation_Tm_abs_42acf2b4bd61f7d087f311642b137700",
"interpretation_Tm_abs_efed28e5237cc814be518263d6481a87",
"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_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESstdcall.va_wpCompute_aes_EncryptBlockBEStdcall",
"typing_Tm_abs_42acf2b4bd61f7d087f311642b137700",
"typing_Tm_abs_efed28e5237cc814be518263d6481a87",
"typing_X64.Vale.Decls.va_if", "typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.update_reg", "typing_X64.Vale.Xmms.sel",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R11@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R13@tok",
"typing_tok_X64.Machine_s.R14@tok",
"typing_tok_X64.Machine_s.R15@tok",
"typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rbp@tok",
"typing_tok_X64.Machine_s.Rbx@tok",
"typing_tok_X64.Machine_s.Rcx@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsi@tok",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
],
0,
"ef3c3424d14797e249ef36208fa83a57"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...