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
Vale.AES.X64.AES128.fst.hints
[
"0�l�{M!8��y��\u001bo�",
[
[
"Vale.AES.X64.AES128.va_qcode_KeyExpansionRound",
1,
1,
0,
[ "@query" ],
0,
"761f9afd933f91712ec372fe8a91e5ee"
],
[
"Vale.AES.X64.AES128.va_lemma_KeyExpansionRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_16e840d41dc3e4674df596a1eae33fed"
],
0,
"1f5666614bfad34b410c4c84dbda485a"
],
[
"Vale.AES.X64.AES128.va_lemma_KeyExpansionRound",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.AES_helpers.expand_key_128_def.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.AES_helpers.expand_key_128_def.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.eq2", "equation_Prims.logical", "equation_Prims.nat",
"equation_Vale.AES.AES_helpers.quad32_shl32",
"equation_Vale.AES.AES_helpers.round_key_128",
"equation_Vale.AES.AES_helpers.simd_round_key_128",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Def.Prop_s.prop0",
"equation_Vale.Def.Types_s.bits_of_byte",
"equation_Vale.Def.Types_s.byte_to_twobits",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Types_s.select_word",
"equation_Vale.Def.Types_s.twobits",
"equation_Vale.Def.Words.Four_s.four_select",
"equation_Vale.Def.Words_s.nat2", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.get",
"equation_Vale.X64.Decls.modifies_buffer_specific128",
"equation_Vale.X64.Decls.upd_register",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem_heaplet",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Decls.validDstAddrs",
"equation_Vale.X64.Decls.validDstAddrs128",
"equation_Vale.X64.Decls.validSrcAddrs",
"equation_Vale.X64.InsVector.buffer128_write",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.memtaint",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.Memory.valid_buffer_read",
"equation_Vale.X64.Memory.valid_buffer_write",
"equation_Vale.X64.Memory.valid_layout_buffer",
"equation_Vale.X64.Memory.valid_taint_buf128",
"equation_Vale.X64.QuickCode.t_require",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg_xmm",
"equation_with_fuel_Vale.AES.AES_helpers.expand_key_128_def.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.AES.AES_helpers.expand_key_128",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Def.Words_s.nat2",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_Vale.Lib.Map16.lemma_equal_intro",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.Memory.modifies_buffer_addr",
"lemma_Vale.X64.Memory.modifies_valid_taint",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_41db9fdf9444e7dc3929e8f963c015c7",
"refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"string_typing",
"token_correspondence_Vale.AES.AES_helpers.expand_key_128_def",
"typing_Prims.eq2", "typing_Vale.AES.AES_helpers.expand_key_128",
"typing_Vale.AES.AES_helpers.round_key_128_rcon",
"typing_Vale.AES.AES_s.aes_rcon",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint",
"typing_Vale.Def.Types_s.byte_to_twobits",
"typing_Vale.Def.Types_s.select_word",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
"typing_Vale.Lib.Map16.sel",
"typing_Vale.X64.Decls.modifies_buffer_specific128",
"typing_Vale.X64.Decls.validDstAddrs128",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.Memory.buffer_write",
"typing_Vale.X64.Memory.loc_buffer",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.va_range1",
"typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_inversion",
"unit_typing"
],
0,
"84185d14b7e61a6f19d7657c4d2cc712"
],
[
"Vale.AES.X64.AES128.va_wp_KeyExpansionRound",
1,
1,
0,
[ "@query" ],
0,
"919169f2cc0d75bbbef6ace15108c3e5"
],
[
"Vale.AES.X64.AES128.va_wpProof_KeyExpansionRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"equation_Vale.AES.X64.AES128.va_wp_KeyExpansionRound",
"equation_Vale.Arch.HeapImpl.heaplet_id",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.X64.Decls.upd_register",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_mem_heaplet",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.set_vale_heap",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.QuickCode.t_require",
"equation_Vale.X64.QuickCode.va_t_ensure",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.AES.AES_helpers.expand_key_128",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd",
"typing_Vale.X64.Decls.va_upd_mem",
"typing_Vale.X64.Decls.va_upd_mem_heaplet",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.Regs.upd",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_typing"
],
0,
"fb7cda0d69f10d85f79a0c8fd2b2c8ab"
],
[
"Vale.AES.X64.AES128.va_quick_KeyExpansionRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"160284916e9f15f7a823aad6b775dda2"
],
[
"Vale.AES.X64.AES128.va_code_KeyExpansionRoundUnrolledRecursive",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_ae567c2fb75be05905677af440075565_0",
"equality_tok_Prims.LexTop@tok", "equation_Vale.AES.AES_s.aes_rcon",
"function_token_typing_Prims.__cache_version_number__",
"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", "well-founded-ordering-on-nat"
],
0,
"5ece98fc1c9832464ca8ad15cd72d273"
],
[
"Vale.AES.X64.AES128.va_codegen_success_KeyExpansionRoundUnrolledRecursive",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"binder_x_ae567c2fb75be05905677af440075565_0",
"equality_tok_Prims.LexTop@tok", "equation_Vale.AES.AES_s.aes_rcon",
"function_token_typing_Prims.__cache_version_number__",
"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", "typing_tok_Prims.LexTop@tok",
"well-founded-ordering-on-nat"
],
0,
"f709266ef5b6588b9478edcfebca925c"
],
[
"Vale.AES.X64.AES128.va_lemma_KeyExpansionRoundUnrolledRecursive",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_9693710b533826ca8622bc2d2972a931"
],
0,
"222743c090bd846f0878e4e01e7594c4"
],
[
"Vale.AES.X64.AES128.va_lemma_KeyExpansionRoundUnrolledRecursive",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_9693710b533826ca8622bc2d2972a931"
],
0,
"aa88b1724a1f2ecbb45472397e6ac782"
],
[
"Vale.AES.X64.AES128.va_lemma_KeyExpansionRoundUnrolledRecursive",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.AES_helpers.expand_key_128_def.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"binder_x_053894aba25fdc4e0df122563ef9b6f4_2",
"binder_x_ae567c2fb75be05905677af440075565_4",
"binder_x_cf077dd9b7968ef3165094b133137e66_3",
"binder_x_eb96f2119e19317ec6e3b596d5a46609_1", "bool_inversion",
"bool_typing", "constructor_distinct_Prims.Cons",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"constructor_distinct_Vale.X64.Machine_s.Block",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"disc_equation_Prims.Cons", "disc_equation_Vale.X64.Machine_s.Block",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat", "equation_Vale.AES.AES_s.aes_rcon",
"equation_Vale.Arch.HeapImpl.heaplet_id",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.X64.CPU_Features_s.sse_enabled",
"equation_Vale.X64.Decls.modifies_buffer_specific128",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_mem_heaplet",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Decls.validDstAddrs",
"equation_Vale.X64.Decls.validDstAddrs128",
"equation_Vale.X64.Decls.validSrcAddrs",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.set_vale_heap",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_xmm",
"equation_with_fuel_Vale.AES.AES_helpers.expand_key_128_def.fuel_instrumented",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.AES.AES_helpers.expand_key_128",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.Lib.Map16.lemma_equal_intro",
"lemma_Vale.Lib.Map16.lemma_other",
"lemma_Vale.Lib.Map16.lemma_self",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.Memory.loc_includes_refl",
"lemma_Vale.X64.Memory.modifies_goal_directed_refl",
"lemma_Vale.X64.Memory.modifies_goal_directed_trans",
"lemma_Vale.X64.Memory.modifies_goal_directed_trans2",
"lemma_Vale.X64.Memory.modifies_refl",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"lemma_Vale.X64.Regs.lemma_upd_eq",
"lemma_Vale.X64.Regs.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_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"proj_equation_Vale.X64.Machine_s.Block_block",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"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_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"projection_inverse_Vale.X64.Machine_s.Block_block",
"projection_inverse_Vale.X64.Machine_s.Block_t_ins",
"projection_inverse_Vale.X64.Machine_s.Block_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.Reg_r",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
"refinement_interpretation_Tm_refine_4904e188b491b2acdc826e9472665bc0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_84a81c538f345a56d2b6a2f70a725449",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"token_correspondence_Vale.AES.AES_helpers.expand_key_128_def",
"typing_Vale.AES.X64.AES128.va_code_KeyExpansionRoundUnrolledRecursive",
"typing_Vale.AES.X64.AES128.va_lemma_KeyExpansionRoundUnrolledRecursive",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Def.Words.Seq_s.four_to_seq_LE",
"typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd",
"typing_Vale.X64.CPU_Features_s.sse4_1_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_mem",
"typing_Vale.X64.Decls.va_upd_mem_heaplet",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_xmm",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.Memory.loc_buffer",
"typing_Vale.X64.Memory.set_vale_heap", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.Regs.upd",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg", "typing_tok_Prims.LexTop@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"well-founded-ordering-on-nat"
],
0,
"1e8fc97728c764c32b8743bec1ba70c5"
],
[
"Vale.AES.X64.AES128.va_wp_KeyExpansionRoundUnrolledRecursive",
1,
1,
0,
[ "@query" ],
0,
"5657b331d8bd8f36c167abf5e21cba1c"
],
[
"Vale.AES.X64.AES128.va_wpProof_KeyExpansionRoundUnrolledRecursive",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"equation_Vale.AES.X64.AES128.va_wp_KeyExpansionRoundUnrolledRecursive",
"equation_Vale.Arch.HeapImpl.heaplet_id",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.X64.Decls.upd_register",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_mem_heaplet",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.set_vale_heap",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.QuickCode.t_require",
"equation_Vale.X64.QuickCode.va_t_ensure",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"int_inversion", "int_typing",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_4904e188b491b2acdc826e9472665bc0",
"refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.AES.AES_helpers.expand_key_128",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.Decls.va_upd_mem",
"typing_Vale.X64.Decls.va_upd_mem_heaplet",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.Regs.upd",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_typing"
],
0,
"c7c1fbce3c61433ce01ac89e3c607b5f"
],
[
"Vale.AES.X64.AES128.va_quick_KeyExpansionRoundUnrolledRecursive",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"aaf78b92fc8757e84f66dc557fa97bf0"
],
[
"Vale.AES.X64.AES128.va_qcode_KeyExpansion128Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Tm_unit",
"disc_equation_Vale.AES.AES_s.AES_128",
"disc_equation_Vale.AES.AES_s.AES_192",
"disc_equation_Vale.AES.AES_s.AES_256", "eq2-interp",
"equation_Prims.nat", "equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.AES_s.nb", "equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6b9131a31b8a74e7093141d7985f063a",
"refinement_interpretation_Tm_refine_bdfa5c85c1bbce1fa77711624629a9fe",
"refinement_interpretation_Tm_refine_ec4cc42b2040d52d9e001ddd04314ad8",
"typing_FStar.Seq.Base.length"
],
0,
"902974e0635af5d1c7919cd8a39d940f"
],
[
"Vale.AES.X64.AES128.va_lemma_KeyExpansion128Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"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.Arch.HeapImpl.vale_heaplets",
"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.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.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
"refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Def.Words.Seq_s.four_to_seq_LE",
"typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"6252d0ed4c568fc6c2b5b80c962ddc14"
],
[
"Vale.AES.X64.AES128.va_lemma_KeyExpansion128Stdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.l_Forall", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.AES_s.nb",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Def.Prop_s.prop0", "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.Def.Words_s.nat64",
"equation_Vale.Lib.Map16.get",
"equation_Vale.X64.Decls.upd_register",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_mem_heaplet",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Decls.validDstAddrs",
"equation_Vale.X64.Decls.validDstAddrs128",
"equation_Vale.X64.Decls.validSrcAddrs",
"equation_Vale.X64.Decls.validSrcAddrs128",
"equation_Vale.X64.InsVector.buffer128_write",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.memtaint",
"equation_Vale.X64.Memory.set_vale_heap",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.Memory.valid_buffer_read",
"equation_Vale.X64.Memory.valid_buffer_write",
"equation_Vale.X64.Memory.valid_layout_buffer",
"equation_Vale.X64.Memory.valid_taint_buf128",
"equation_Vale.X64.QuickCode.t_require",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.AES.AES_s.key_to_round_keys_LE",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing",
"interpretation_Tm_abs_16970edc854832ef738a7e1d630e994c",
"interpretation_Tm_abs_20b2728456092d94542f8c7aee37a45d",
"interpretation_Tm_abs_2283cd4cea49ae80c702584e3efc5b6f",
"interpretation_Tm_abs_7ea5bd633d40850615341220b89135e8",
"interpretation_Tm_abs_8eaffd6bd22e15c2d46f8e73ccf4da62",
"interpretation_Tm_abs_9325ad5ee4a454fdd46359ab47e7d7ea",
"interpretation_Tm_abs_b2f6f633c17a28affc03d4ebcf205bfb",
"interpretation_Tm_abs_ce1a0300ac998db3015a4397c104a2fd",
"interpretation_Tm_abs_dc5afce1f3a4c6ae9eb55e201e289cbe",
"kinding_Vale.Def.Words_s.four@tok",
"l_quant_interp_2b17785628bd2c1a39dc28962acc0b95",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_Vale.Lib.Map16.lemma_equal_intro",
"lemma_Vale.Lib.Map16.lemma_other",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.Memory.loc_includes_refl",
"lemma_Vale.X64.Memory.modifies_buffer_addr",
"lemma_Vale.X64.Memory.modifies_goal_directed_refl",
"lemma_Vale.X64.Memory.modifies_goal_directed_trans",
"lemma_Vale.X64.Memory.modifies_goal_directed_trans2",
"lemma_Vale.X64.Memory.modifies_valid_taint",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_211facd8812fd94e95b65d3b8891b14a",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_41db9fdf9444e7dc3929e8f963c015c7",
"refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
"refinement_interpretation_Tm_refine_4904e188b491b2acdc826e9472665bc0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_86f4bbceadf6defbe5067ba30da00c17",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"string_typing",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint",
"typing_Vale.Def.Words.Seq_s.four_to_seq_LE",
"typing_Vale.Lib.Map16.sel",
"typing_Vale.X64.Decls.validDstAddrs128",
"typing_Vale.X64.Memory.buffer_addr",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.Memory.buffer_write",
"typing_Vale.X64.Memory.loc_buffer",
"typing_Vale.X64.Memory.modifies",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.va_range1",
"typing_Vale.X64.Regs.eta_sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_inversion"
],
0,
"2e9439dd79b201b9397f3928aa0369ec"
],
[
"Vale.AES.X64.AES128.va_wp_KeyExpansion128Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"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.Arch.HeapImpl.vale_heaplets",
"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.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.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
"refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Def.Words.Seq_s.four_to_seq_LE",
"typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"f1731e44ee5e08247cf93eedac9df398"
],
[
"Vale.AES.X64.AES128.va_wpProof_KeyExpansion128Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat",
"equation_Vale.AES.X64.AES128.va_wp_KeyExpansion128Stdcall",
"equation_Vale.Arch.HeapImpl.heaplet_id",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Decls.upd_register",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_mem_heaplet",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Decls.validDstAddrs",
"equation_Vale.X64.Decls.validDstAddrs128",
"equation_Vale.X64.Decls.validSrcAddrs",
"equation_Vale.X64.Decls.validSrcAddrs128",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.set_vale_heap",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.QuickCode.t_require",
"equation_Vale.X64.QuickCode.va_t_ensure",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
"interpretation_Tm_abs_7ea5bd633d40850615341220b89135e8",
"interpretation_Tm_abs_8eaffd6bd22e15c2d46f8e73ccf4da62",
"interpretation_Tm_abs_ce1a0300ac998db3015a4397c104a2fd",
"interpretation_Tm_abs_dc5afce1f3a4c6ae9eb55e201e289cbe",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_mem",
"typing_Vale.X64.Decls.va_upd_mem_heaplet",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg", "unit_typing"
],
0,
"f73550000f8728f6749ef4a8f1a2b65f"
],
[
"Vale.AES.X64.AES128.va_quick_KeyExpansion128Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"0627c928e0f726872b80b82e22849ac3"
],
[
"Vale.AES.X64.AES128.va_lemma_AES128EncryptRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"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", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6cc211018e51b4c8cff23e448d890abc"
],
0,
"2ba89ec08dd7fbea22a0ef4b652fc02d"
],
[
"Vale.AES.X64.AES128.va_lemma_AES128EncryptRound",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.AES_s.eval_rounds_def.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.AES_s.eval_rounds_def.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.eq2", "equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.AES.AES_s.eval_round",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Lib.Map16.get",
"equation_Vale.X64.CPU_Features_s.sse_enabled",
"equation_Vale.X64.Decls.upd_register",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Decls.validSrcAddrs",
"equation_Vale.X64.Decls.validSrcAddrs128",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.Memory.valid_buffer_read",
"equation_Vale.X64.Memory.valid_layout_buffer",
"equation_Vale.X64.Memory.valid_taint_buf128",
"equation_Vale.X64.QuickCode.t_require",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_xmm",
"equation_with_fuel_Vale.AES.AES_s.eval_rounds_def.fuel_instrumented",
"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.Arch.HeapImpl.vale_heap",
"int_inversion", "int_typing",
"lemma_Vale.Lib.Map16.lemma_equal_intro",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_4efd8dd7c0f50f53e2308e4a3404dfa9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"string_typing",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.X64.CPU_Features_s.sse_enabled",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.va_range1",
"typing_Vale.X64.Regs.eta_sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_inversion", "unit_typing"
],
0,
"a41279096cd424da542fcf5244875029"
],
[
"Vale.AES.X64.AES128.va_wp_AES128EncryptRound",
1,
1,
0,
[ "@query" ],
0,
"d88c5a3cf41a1cac0195cc8928f92111"
],
[
"Vale.AES.X64.AES128.va_wpProof_AES128EncryptRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"equation_Vale.AES.X64.AES128.va_wp_AES128EncryptRound",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.X64.CPU_Features_s.sse_enabled",
"equation_Vale.X64.Decls.upd_register",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.QuickCode.t_require",
"equation_Vale.X64.QuickCode.va_t_ensure",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"int_inversion", "int_typing",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_4efd8dd7c0f50f53e2308e4a3404dfa9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.AES.AES_s.eval_rounds_def",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.X64.CPU_Features_s.sse_enabled",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.Regs.upd",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_typing"
],
0,
"b494d3cb19beb052b4af064e35bb2a49"
],
[
"Vale.AES.X64.AES128.va_quick_AES128EncryptRound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"d4084ee6baf21e021564389b89a9d164"
],
[
"Vale.AES.X64.AES128.va_qcode_AES128EncryptBlock",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"debd0d9f7db9674d982de0a1746fc69b"
],
[
"Vale.AES.X64.AES128.va_lemma_AES128EncryptBlock",
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_74ee5d51291f0d079b5e144e2ec88f64"
],
0,
"e192971eb3be65cea4d6ed4a9c059260"
],
[
"Vale.AES.X64.AES128.va_lemma_AES128EncryptBlock",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.AES_s.eval_rounds_def.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.eq2", "equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Vale.AES.AES_s.aes_encrypt_LE_def",
"equation_Vale.AES.AES_s.eval_cipher_def",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Lib.Map16.get",
"equation_Vale.X64.CPU_Features_s.sse_enabled",
"equation_Vale.X64.Decls.upd_register",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Decls.validSrcAddrs",
"equation_Vale.X64.Decls.validSrcAddrs128",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.Memory.valid_buffer_read",
"equation_Vale.X64.Memory.valid_layout_buffer",
"equation_Vale.X64.Memory.valid_taint_buf128",
"equation_Vale.X64.QuickCode.t_require",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_xmm",
"equation_with_fuel_Vale.AES.AES_s.eval_rounds_def.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.AES.AES_s.aes_encrypt_LE",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
"lemma_Vale.Lib.Map16.lemma_equal_intro",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_4efd8dd7c0f50f53e2308e4a3404dfa9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"string_typing",
"token_correspondence_Vale.AES.AES_s.aes_encrypt_LE_def",
"typing_FStar.Seq.Base.length",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.X64.CPU_Features_s.sse_enabled",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.va_range1",
"typing_Vale.X64.Regs.eta_sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_inversion", "unit_typing"
],
0,
"d75e698c1896c5d996c6acaf165e59ab"
],
[
"Vale.AES.X64.AES128.va_wp_AES128EncryptBlock",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"7138f9187fe3f27242eb644abcd5cc8c"
],
[
"Vale.AES.X64.AES128.va_wpProof_AES128EncryptBlock",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"equality_tok_Vale.AES.AES_s.AES_128@tok", "equation_Prims.nat",
"equation_Vale.AES.X64.AES128.va_wp_AES128EncryptBlock",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.X64.CPU_Features_s.sse_enabled",
"equation_Vale.X64.Decls.upd_register",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.QuickCode.t_require",
"equation_Vale.X64.QuickCode.va_t_ensure",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.AES.AES_s.aes_encrypt_LE",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.X64.CPU_Features_s.sse_enabled",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_xmm", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.Regs.upd",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_tok_Vale.AES.AES_s.AES_128@tok", "unit_typing"
],
0,
"48f03b64886cad818184a9f8f4d62219"
],
[
"Vale.AES.X64.AES128.va_quick_AES128EncryptBlock",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"9372565401964ddef50002b8f2b0c809"
],
[
"Vale.AES.X64.AES128.va_qcode_AES128EncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_Vale.AES.AES_s.AES_128@tok", "equation_Prims.squash",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"87f74a97aebc1996afe6b451ad0f0833"
],
[
"Vale.AES.X64.AES128.va_lemma_AES128EncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.X64.Decls.va_int_range",
"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_0304b872cb88ace5290519d2df90385f",
"refinement_interpretation_Tm_refine_4d38686bf695f79f110ce5aef057279f"
],
0,
"485686e5abe5972f8a48fc4ad2a786c2"
],
[
"Vale.AES.X64.AES128.va_lemma_AES128EncryptBlockStdcall",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.eq2", "equation_Prims.logical", "equation_Prims.nat",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Lib.Map16.get",
"equation_Vale.X64.Decls.upd_register",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_mem_heaplet",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Decls.validDstAddrs",
"equation_Vale.X64.Decls.validDstAddrs128",
"equation_Vale.X64.Decls.validSrcAddrs",
"equation_Vale.X64.Decls.validSrcAddrs128",
"equation_Vale.X64.InsVector.buffer128_write",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.memtaint",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.Memory.valid_buffer_read",
"equation_Vale.X64.Memory.valid_buffer_write",
"equation_Vale.X64.Memory.valid_layout_buffer",
"equation_Vale.X64.Memory.valid_taint_buf128",
"equation_Vale.X64.QuickCode.t_require",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
"interpretation_Tm_abs_16970edc854832ef738a7e1d630e994c",
"interpretation_Tm_abs_7ea5bd633d40850615341220b89135e8",
"interpretation_Tm_abs_9325ad5ee4a454fdd46359ab47e7d7ea",
"interpretation_Tm_abs_ce1a0300ac998db3015a4397c104a2fd",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_Vale.Lib.Map16.lemma_equal_intro",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.Memory.modifies_buffer_addr",
"lemma_Vale.X64.Memory.modifies_valid_taint",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_41db9fdf9444e7dc3929e8f963c015c7",
"refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_dd592ff911d0f80cdf0ace6c4224ff73",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"string_typing", "typing_FStar.Seq.Base.length", "typing_Prims.eq2",
"typing_Vale.AES.AES_s.aes_encrypt_LE",
"typing_Vale.AES.AES_s.key_to_round_keys_LE",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint",
"typing_Vale.Lib.Map16.get", "typing_Vale.Lib.Map16.sel",
"typing_Vale.X64.Decls.validSrcAddrs128",
"typing_Vale.X64.Memory.buffer_addr",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.Memory.buffer_write",
"typing_Vale.X64.Memory.loc_buffer",
"typing_Vale.X64.Memory.modifies",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.va_range1",
"typing_Vale.X64.Regs.eta_sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_tok_Vale.AES.AES_s.AES_128@tok",
"typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_typing"
],
0,
"98a5d536e4969960894861edf90ea63a"
],
[
"Vale.AES.X64.AES128.va_wp_AES128EncryptBlockStdcall",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"8ae6ade9aacfcbc222b476a4b7525a35"
],
[
"Vale.AES.X64.AES128.va_wpProof_AES128EncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat",
"equation_Vale.AES.X64.AES128.va_wp_AES128EncryptBlockStdcall",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.CPU_Features_s.sse_enabled",
"equation_Vale.X64.Decls.upd_register",
"equation_Vale.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_mem_heaplet",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Decls.validDstAddrs",
"equation_Vale.X64.Decls.validDstAddrs128",
"equation_Vale.X64.Decls.validSrcAddrs",
"equation_Vale.X64.Decls.validSrcAddrs128",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Memory.set_vale_heap",
"equation_Vale.X64.Memory.vale_full_heap_equal",
"equation_Vale.X64.QuickCode.t_require",
"equation_Vale.X64.QuickCode.va_t_ensure",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
"interpretation_Tm_abs_7112983baaa4c9ef04184f03828d86e8",
"interpretation_Tm_abs_7ea5bd633d40850615341220b89135e8",
"interpretation_Tm_abs_8eaffd6bd22e15c2d46f8e73ccf4da62",
"interpretation_Tm_abs_ce1a0300ac998db3015a4397c104a2fd",
"interpretation_Tm_abs_dc5afce1f3a4c6ae9eb55e201e289cbe",
"interpretation_Tm_abs_e51c7d7b4f244bf176c4178b097c4b0e",
"lemma_Vale.Lib.Map16.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
"proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd",
"typing_Vale.X64.CPU_Features_s.sse_enabled",
"typing_Vale.X64.Regs.sel", "typing_Vale.X64.Regs.upd",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_typing"
],
0,
"e8b5bf242f6880336f2be4666c72db4c"
],
[
"Vale.AES.X64.AES128.va_quick_AES128EncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"f87f963345bd9cc7fd4ac9a70125d973"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...