Revision 3f979cc1cb15a4491f8b804bbafeabeffe5a1ab1 authored by Aseem Rastogi on 09 April 2019, 11:31:34 UTC, committed by Aseem Rastogi on 09 April 2019, 11:31:34 UTC
1 parent 74a8710
Vale.Stdcalls.Aes.fst.hints
[
"\ta�ct�\rߖdy�E\u001f�\u0015",
[
[
"Vale.Stdcalls.Aes.as_t",
1,
1,
0,
[ "@query" ],
0,
"6a747a758624b47bbfb31029d6711772"
],
[
"Vale.Stdcalls.Aes.as_normal_t",
1,
1,
0,
[ "@query" ],
0,
"f5854a85e57c8715e898d98535abb1b6"
],
[
"Vale.Stdcalls.Aes.dom",
1,
1,
0,
[
"@query", "equation_Interop.X64.max_stdcall",
"projection_inverse_BoxInt_proj_0"
],
0,
"8df3aa4b2784144ff097ecb506085785"
],
[
"Vale.Stdcalls.Aes.key128_lemma'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"AES_s_pretyping_443f63aed29daed744644bd1799d3a91",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"X64.Machine_s_interpretation_Tm_arrow_196f8dfca6d67b0bd046e19b6a5a08e6",
"X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
"bool_inversion", "constructor_distinct_AES_s.AES_128",
"constructor_distinct_Interop.Types.TUInt8",
"constructor_distinct_X64.Machine_s.R12",
"constructor_distinct_X64.Machine_s.R13",
"constructor_distinct_X64.Machine_s.R14",
"constructor_distinct_X64.Machine_s.R15",
"constructor_distinct_X64.Machine_s.Rbp",
"constructor_distinct_X64.Machine_s.Rbx",
"constructor_distinct_X64.Machine_s.Rdi",
"constructor_distinct_X64.Machine_s.Rdx",
"constructor_distinct_X64.Machine_s.Rsi",
"constructor_distinct_X64.Machine_s.Rsp", "eq2-interp",
"equality_tok_AES_s.AES_128@tok",
"equality_tok_Interop.Types.TUInt8@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.Rax@tok",
"equality_tok_X64.Machine_s.Rbp@tok",
"equality_tok_X64.Machine_s.Rbx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Rsp@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_Interop.Types.view_n",
"equation_Interop.X64.regs_modified_stdcall",
"equation_Interop.X64.xmms_modified_stdcall", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.prop",
"equation_Prims.squash", "equation_Types_s.quad32",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Stdcalls.Aes.b128",
"equation_Vale.Stdcalls.Aes.key128_post",
"equation_Vale.Stdcalls.Aes.key128_pre", "equation_Words_s.nat32",
"equation_X64.AES.va_ens_KeyExpansionStdcall",
"equation_X64.AES.va_req_KeyExpansionStdcall",
"equation_X64.Machine_s.xmm",
"equation_X64.Taint_Semantics_s.tainted_code",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"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_Interop.X64.regs_modified_stdcall",
"function_token_typing_Interop.X64.xmms_modified_stdcall",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq",
"function_token_typing_X64.MemoryAdapters.code_equiv",
"int_inversion", "int_typing",
"interpretation_Tm_abs_0653c3e5ab290a922be608a06ca67d0f",
"interpretation_Tm_abs_3e5a867f6d725e93a58d4a1335442a98",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Regs.lemma_upd_ne",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_upd_ne", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_8cbf26bf9daa2f745252395fa946c64c",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_Interop.X64.regs_modified_stdcall",
"token_correspondence_Interop.X64.xmms_modified_stdcall",
"token_correspondence_Vale.Stdcalls.Aes.key128_post",
"token_correspondence_Vale.Stdcalls.Aes.key128_pre",
"typing_Interop.Assumptions.win", "typing_Interop.Types.view_n",
"typing_X64.AES.va_code_KeyExpansionStdcall",
"typing_X64.AES.va_lemma_KeyExpansionStdcall",
"typing_X64.CPU_Features_s.aesni_enabled",
"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_X64.Vale.Xmms.upd",
"typing_tok_AES_s.AES_128@tok",
"typing_tok_Interop.Types.TUInt8@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsp@tok"
],
0,
"9634af962c9be4b3b33af43515075a34"
],
[
"Vale.Stdcalls.Aes.key128_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"AES_s_pretyping_443f63aed29daed744644bd1799d3a91", "bool_inversion",
"constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_Interop.Types.TUInt8", "eq2-interp",
"equality_tok_AES_s.AES_128@tok",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_Interop.Types.TUInt8@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd",
"equation_Interop.Types.base_typ_as_type",
"equation_Interop.Types.view_n", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.prop",
"equation_Prims.squash", "equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.Stdcalls.Aes.b128",
"equation_Vale.Stdcalls.Aes.key128_post",
"equation_Vale.Stdcalls.Aes.key128_pre",
"equation_X64.AES.va_ens_KeyExpansionStdcall",
"equation_X64.AES.va_req_KeyExpansionStdcall",
"equation_X64.Memory.buffer128",
"equation_X64.Taint_Semantics_s.tainted_code",
"equation_X64.Vale.Decls.va_require_total",
"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.State.update_xmm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq",
"function_token_typing_X64.MemoryAdapters.code_equiv",
"interpretation_Tm_abs_0653c3e5ab290a922be608a06ca67d0f",
"interpretation_Tm_abs_3e5a867f6d725e93a58d4a1335442a98",
"lemma_X64.Memory.loc_includes_refl",
"lemma_X64.Memory.loc_includes_union_l_buffer",
"lemma_X64.Memory.modifies_goal_directed_refl",
"lemma_X64.Memory.modifies_goal_directed_trans",
"primitive_Prims.op_Equality",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_X64.Vale.State.Mkstate_mem",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"token_correspondence_Vale.Stdcalls.Aes.key128_post",
"token_correspondence_Vale.Stdcalls.Aes.key128_pre",
"typing_Interop.Assumptions.win",
"typing_Vale.AsLowStar.ValeSig.state_of",
"typing_X64.Memory.loc_buffer", "typing_X64.Memory.loc_none",
"typing_X64.Memory.loc_union",
"typing_X64.MemoryAdapters.as_vale_buffer",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_tok_AES_s.AES_128@tok",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_Interop.Types.TUInt8@tok"
],
0,
"227eb8e260d88124e4a48a0f32f8f483"
],
[
"Vale.Stdcalls.Aes.lowstar_key128_t",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "eq2-interp", "equation_Interop.Base.arg",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash",
"function_token_typing_X64.MemoryAdapters.ins_equiv",
"function_token_typing_X64.MemoryAdapters.ocmp_equiv",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"dce3314f47acf7678bb07559d811a277"
],
[
"Vale.Stdcalls.Aes.key256_lemma'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"AES_s_pretyping_443f63aed29daed744644bd1799d3a91",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"X64.Machine_s_interpretation_Tm_arrow_196f8dfca6d67b0bd046e19b6a5a08e6",
"X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
"bool_inversion", "constructor_distinct_AES_s.AES_128",
"constructor_distinct_AES_s.AES_256",
"constructor_distinct_Interop.Types.TUInt8",
"constructor_distinct_X64.Machine_s.R12",
"constructor_distinct_X64.Machine_s.R13",
"constructor_distinct_X64.Machine_s.R14",
"constructor_distinct_X64.Machine_s.R15",
"constructor_distinct_X64.Machine_s.R8",
"constructor_distinct_X64.Machine_s.R9",
"constructor_distinct_X64.Machine_s.Rbp",
"constructor_distinct_X64.Machine_s.Rbx",
"constructor_distinct_X64.Machine_s.Rcx",
"constructor_distinct_X64.Machine_s.Rdi",
"constructor_distinct_X64.Machine_s.Rdx",
"constructor_distinct_X64.Machine_s.Rsi",
"constructor_distinct_X64.Machine_s.Rsp", "eq2-interp",
"equality_tok_AES_s.AES_128@tok", "equality_tok_AES_s.AES_256@tok",
"equality_tok_Interop.Types.TUInt8@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.Rax@tok",
"equality_tok_X64.Machine_s.Rbp@tok",
"equality_tok_X64.Machine_s.Rbx@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Rsi@tok",
"equality_tok_X64.Machine_s.Rsp@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_Interop.Types.view_n",
"equation_Interop.X64.arg_of_register",
"equation_Interop.X64.reg_nat",
"equation_Interop.X64.regs_modified_stdcall",
"equation_Interop.X64.xmms_modified_stdcall", "equation_Prims.eq2",
"equation_Prims.nat", "equation_Prims.prop", "equation_Prims.squash",
"equation_Types_s.quad32",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.AsLowStar.ValeSig.vale_save_reg",
"equation_Vale.AsLowStar.ValeSig.vale_save_xmm",
"equation_Vale.Stdcalls.Aes.b128",
"equation_Vale.Stdcalls.Aes.key256_post",
"equation_Vale.Stdcalls.Aes.key256_pre", "equation_Words_s.nat32",
"equation_Words_s.natN",
"equation_X64.AES.va_ens_KeyExpansionStdcall",
"equation_X64.AES.va_req_KeyExpansionStdcall",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"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_Interop.X64.__proj__Rel__item__of_reg",
"function_token_typing_Interop.X64.regs_modified_stdcall",
"function_token_typing_Interop.X64.xmms_modified_stdcall",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq",
"int_inversion", "int_typing",
"interpretation_Tm_abs_2b0edda6f051544f797b3c0a18e66045",
"interpretation_Tm_abs_da2200f0571a15dadb2b6c039a9ba1ee",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Regs.lemma_upd_ne",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_upd_ne", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Interop.X64.Rel_of_reg",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Interop.X64.Rel_of_reg",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_8cbf26bf9daa2f745252395fa946c64c",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_Interop.X64.arg_of_register",
"token_correspondence_Interop.X64.regs_modified_stdcall",
"token_correspondence_Interop.X64.xmms_modified_stdcall",
"token_correspondence_Vale.Stdcalls.Aes.key256_post",
"token_correspondence_Vale.Stdcalls.Aes.key256_pre",
"typing_Interop.Assumptions.win", "typing_Interop.Types.view_n",
"typing_X64.AES.va_code_KeyExpansionStdcall",
"typing_X64.AES.va_lemma_KeyExpansionStdcall",
"typing_X64.CPU_Features_s.aesni_enabled",
"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_X64.Vale.Xmms.upd",
"typing_tok_AES_s.AES_128@tok", "typing_tok_AES_s.AES_256@tok",
"typing_tok_Interop.Types.TUInt8@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Rsp@tok"
],
0,
"bc2531344eebbcbedd16b706703b85ff"
],
[
"Vale.Stdcalls.Aes.key256_lemma",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_Interop.Types.TUInt8", "eq2-interp",
"equality_tok_AES_s.AES_256@tok",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_Interop.Types.TUInt8@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd",
"equation_Interop.Types.base_typ_as_type",
"equation_Interop.Types.view_n", "equation_Prims.eq2",
"equation_Prims.nat", "equation_Prims.prop", "equation_Prims.squash",
"equation_Vale.AsLowStar.ValeSig.fuel_of",
"equation_Vale.AsLowStar.ValeSig.state_of",
"equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall",
"equation_Vale.Stdcalls.Aes.b128",
"equation_Vale.Stdcalls.Aes.key256_post",
"equation_Vale.Stdcalls.Aes.key256_pre",
"equation_X64.AES.va_ens_KeyExpansionStdcall",
"equation_X64.AES.va_req_KeyExpansionStdcall",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_require_total",
"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.State.update_xmm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq",
"interpretation_Tm_abs_2b0edda6f051544f797b3c0a18e66045",
"interpretation_Tm_abs_da2200f0571a15dadb2b6c039a9ba1ee",
"lemma_X64.Memory.loc_includes_refl",
"lemma_X64.Memory.loc_includes_union_l_buffer",
"lemma_X64.Memory.modifies_goal_directed_refl",
"lemma_X64.Memory.modifies_goal_directed_trans",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"token_correspondence_Vale.Stdcalls.Aes.key256_post",
"token_correspondence_Vale.Stdcalls.Aes.key256_pre",
"typing_Interop.Assumptions.win",
"typing_Vale.AsLowStar.ValeSig.state_of",
"typing_X64.Memory.loc_buffer", "typing_X64.Memory.loc_none",
"typing_X64.Memory.loc_union",
"typing_X64.MemoryAdapters.as_vale_buffer",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_Interop.Types.TUInt8@tok"
],
0,
"0ece731e9c43c25563604afba6f7e13f"
],
[
"Vale.Stdcalls.Aes.lowstar_key256_t",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "eq2-interp", "equation_Interop.Base.arg",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.squash",
"function_token_typing_X64.MemoryAdapters.ins_equiv",
"function_token_typing_X64.MemoryAdapters.ocmp_equiv",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"a0383afd69b9081139149007668b3758"
],
[
"Vale.Stdcalls.Aes.lowstar_key128",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Interop.Base.arg", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.squash",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Interop.Base.arg",
"function_token_typing_X64.MemoryAdapters.ins_equiv",
"function_token_typing_X64.MemoryAdapters.ocmp_equiv",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"db4444378dffe26c3df395ce44c6f7a2"
],
[
"Vale.Stdcalls.Aes.lowstar_key256",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "eq2-interp",
"equation_Interop.Base.arg", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.squash",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Interop.Base.arg",
"function_token_typing_X64.MemoryAdapters.ins_equiv",
"function_token_typing_X64.MemoryAdapters.ocmp_equiv",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"98a9a9e20d90511c5858ffeb8a027135"
]
]
]
Computing file changes ...
