[ "bj}h\u0003;p\u0006", [ [ "Vale.AES.X64.AES.va_req_KeyExpansionStdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "unit_typing" ], 0, "fd64698f55031bc3ea8fccef12af25f8" ], [ "Vale.AES.X64.AES.va_ens_KeyExpansionStdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013", "bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "eq2-interp", "equality_tok_Vale.AES.AES_s.AES_128@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Prims.l_and", "equation_Prims.squash", "equation_Prims.subtype_of", "equation_Vale.AES.AES_s.is_aes_key_LE", "equation_Vale.AES.X64.AES.va_req_KeyExpansionStdcall", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seqn", "equation_Vale.Def.Words_s.nat32", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Def.Words_s.nat32", "int_typing", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "primitive_Prims.op_Equality", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "typing_Vale.Def.Words.Seq_s.four_to_seq_LE", "typing_Vale.X64.Memory.buffer_read", "typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_tok_Vale.AES.AES_s.AES_128@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_typing" ], 0, "55bba5fee199bfefde1d78aa7125ebd5" ], [ "Vale.AES.X64.AES.va_lemma_KeyExpansionStdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013", "bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "eq2-interp", "equality_tok_Vale.AES.AES_s.AES_128@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Vale.AES.AES_s.is_aes_key_LE", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seqn", "equation_Vale.Def.Words_s.nat32", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.get_vale_heap", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Def.Words_s.nat32", "int_typing", "primitive_Prims.op_Equality", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_fbf0120317c1791ec21c0732ca73adf7", "typing_Vale.Def.Words.Seq_s.four_to_seq_LE", "typing_Vale.X64.Memory.buffer_read", "typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_tok_Vale.AES.AES_s.AES_128@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "3f36c839aad0a8d3e8f8bf2a4caee657" ], [ "Vale.AES.X64.AES.va_wp_KeyExpansionStdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013", "bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "eq2-interp", "equality_tok_Vale.AES.AES_s.AES_128@tok", "equality_tok_Vale.AES.AES_s.AES_256@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equation_Vale.AES.AES_s.is_aes_key_LE", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seqn", "equation_Vale.Def.Words_s.nat32", "equation_Vale.X64.Decls.va_if", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_heaplet", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.get_vale_heap", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Def.Words_s.nat32", "int_typing", "interpretation_Tm_abs_38d7eff540413c1542680da4920eb610", "interpretation_Tm_abs_b56408d008c29abd8498b9b17febc53e", "primitive_Prims.op_Equality", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_BoxBool_proj_0", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996", "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_c7ddb114a835e1819499f5805e85b51d", "typing_Vale.AES.AES256_helpers.make_AES256_key", "typing_Vale.Def.Words.Seq_s.four_to_seq_LE", "typing_Vale.X64.Memory.buffer_read", "typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_tok_Vale.AES.AES_s.AES_128@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok" ], 0, "c66e9dc1e304d867a8135de137480658" ], [ "Vale.AES.X64.AES.va_quick_KeyExpansionStdcall", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "d7f6e2156ddf2b0073036d92df3040df" ], [ "Vale.AES.X64.AES.va_lemma_AESEncryptBlock", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.X64.Decls.va_require_total", "fuel_guarded_inversion_Vale.Def.Words_s.four", "fuel_guarded_inversion_Vale.X64.State.vale_state", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_64a90b72eab8ec88bdd5838bbce5e2d0" ], 0, "79350539a66a26b69bdb01da493a376c" ], [ "Vale.AES.X64.AES.va_wp_AESEncryptBlock", 1, 1, 0, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "6ea6e657066a8749d6b15f2ae7ef51f5" ], [ "Vale.AES.X64.AES.va_quick_AESEncryptBlock", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3" ], 0, "14f700a0ed1ff9e20c16a94624dfef0a" ] ] ]