Revision 93281362ad4fa0df971a98b303733ad47f7ee0b5 authored by Jonathan Protzenko on 15 April 2020, 18:25:02 UTC, committed by Jonathan Protzenko on 15 April 2020, 18:25:02 UTC
1 parent 321f8c4
Vale.AES.X64.GF128_Init.fst.hints
[
"r\u0001�'Q\u0002S��(f{ƹJ�",
[
[
"Vale.AES.X64.GF128_Init.va_qcode_ShiftKey1_128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"2210ca7ab4281aceaea347c0eb085743"
],
[
"Vale.AES.X64.GF128_Init.va_lemma_ShiftKey1_128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"bool_typing", "constructor_distinct_Tm_unit",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.AES.GF128.shift_key_1",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"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.nat8", "equation_Vale.Def.Words_s.natN",
"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_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.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.State.state_eq",
"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.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Def.Words_s.nat2",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_one_degree",
"int_inversion", "int_typing",
"interpretation_Tm_abs_1c911fe8a74d6f22ca73211dc8888b9b",
"interpretation_Tm_abs_8dab9c6dd00969543976d382038931a0",
"lemma_Vale.Lib.Map16.lemma_equal_intro",
"lemma_Vale.Math.Poly2.Bits.lemma_of_quad32_degree",
"lemma_Vale.Math.Poly2.Bits.lemma_to_of_quad32",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"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",
"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.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_ok",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_aaa8221de098e46cfe83e5c3439e6ce8",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"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.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.Math.Poly2.Bits_s.of_quad32",
"typing_Vale.Math.Poly2.Bits_s.to_quad32",
"typing_Vale.Math.Poly2.poly_and", "typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift",
"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.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",
"unit_inversion", "unit_typing"
],
0,
"0fe87a437a9be7474ff2abbfa1286013"
],
[
"Vale.AES.X64.GF128_Init.va_wpProof_ShiftKey1_128",
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.GF128_Init.va_wp_ShiftKey1_128",
"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_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",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_one_degree",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_aaa8221de098e46cfe83e5c3439e6ce8",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"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,
"ab34268ad7ea05e582c8ea66bff3b2af"
],
[
"Vale.AES.X64.GF128_Init.va_quick_ShiftKey1_128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"6b4db1357c7f4f4c8170e56fc7a03fba"
],
[
"Vale.AES.X64.GF128_Init.va_lemma_ShiftKey1_gf128_power",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Def.Types_s.insert_nat32",
"equation_Vale.Def.Words.Four_s.four_insert",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"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_reg64",
"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_64",
"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.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", "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.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.OReg_r",
"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.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.OReg_r",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"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,
"9f6c1aae94dfb59b8f88c4fe637cb5b0"
],
[
"Vale.AES.X64.GF128_Init.va_wpProof_ShiftKey1_gf128_power",
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.GF128_Init.va_wp_ShiftKey1_gf128_power",
"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_ok",
"equation_Vale.X64.Decls.va_upd_reg64",
"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_64",
"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_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",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"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,
"d7ca9fe812b59af7b9f21fa1e6e31e95"
],
[
"Vale.AES.X64.GF128_Init.va_quick_ShiftKey1_gf128_power",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"7b606baaacfa39cc0571c3816795489e"
],
[
"Vale.AES.X64.GF128_Init.va_lemma_Gf128_powers",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"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.eqtype",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Vale.AES.GF128.op_Star_Tilde",
"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_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_flags",
"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.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.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"function_token_typing_Vale.Def.Words_s.nat64", "int_typing",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_upd",
"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.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_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",
"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_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_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_41db9fdf9444e7dc3929e8f963c015c7",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"string_typing", "typing_FStar.Seq.Base.upd", "typing_Prims.eq2",
"typing_Vale.AES.GHash.gf128_power",
"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.sel",
"typing_Vale.Math.Poly2.Bits_s.of_quad32",
"typing_Vale.Math.Poly2_s.poly",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"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.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,
"b2e14247cd1ba13a97c17b8984314440"
],
[
"Vale.AES.X64.GF128_Init.va_wpProof_Gf128_powers",
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.GF128_Init.va_wp_Gf128_powers",
"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_reg64",
"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_64",
"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",
"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.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,
"60ac1051bd2389e52f65ff7689d995db"
],
[
"Vale.AES.X64.GF128_Init.va_quick_Gf128_powers",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"a62622ecd8e1f89b0152d2422c7f2c40"
],
[
"Vale.AES.X64.GF128_Init.va_req_Keyhash_init",
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,
"2fe6723a5c4e4bbd45aaab8333279e17"
],
[
"Vale.AES.X64.GF128_Init.va_ens_Keyhash_init",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"equation_Prims.l_and", "equation_Prims.squash",
"equation_Prims.subtype_of",
"equation_Vale.AES.X64.GF128_Init.va_req_Keyhash_init",
"equation_Vale.X64.Decls.va_state_eq",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"unit_typing"
],
0,
"069268d26011c3c7a9948dceaf3a45c9"
],
[
"Vale.AES.X64.GF128_Init.va_qcode_Keyhash_init",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"94416b69bbca99caee92d79e40d18c29"
],
[
"Vale.AES.X64.GF128_Init.va_lemma_Keyhash_init",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Vale.X64.Decls.va_require_total",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"refinement_interpretation_Tm_refine_a5c7b042be3094d09e1325f52034d356"
],
0,
"c87fac56a0755328851903c0e5988839"
],
[
"Vale.AES.X64.GF128_Init.va_lemma_Keyhash_init",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Arch.HeapImpl_pretyping_4aa61432b04e23a2d66ceb8d22171f42",
"Vale.Arch.HeapImpl_pretyping_6646ba4902a38c8f85d79301e07488b2",
"b2t_def", "bool_inversion", "constructor_distinct_Prims.Cons",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.Arch.HeapImpl.Mkbuffer_info@tok",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equality_tok_Vale.Arch.HeapImpl.Immutable@tok",
"equality_tok_Vale.Arch.HeapImpl.Mutable@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.GHash.hkeys_reqs_priv",
"equation_Vale.Arch.HeapImpl.heaplet_id",
"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.Def.Words_s.natN", "equation_Vale.Lib.Map16.map2",
"equation_Vale.Lib.Map16.map4", "equation_Vale.Lib.Map16.sel2",
"equation_Vale.Lib.Map16.sel4", "equation_Vale.Lib.Map16.sel8",
"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_layout",
"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.InsMem.create_post",
"equation_Vale.X64.InsMem.heaplet_id_is_some",
"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_64",
"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.buffer_info_disjoint",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.init_heaplets_req",
"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",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap_layout",
"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",
"function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
"int_typing", "kinding_Vale.Arch.HeapImpl.buffer_info@tok",
"l_and-interp", "lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32",
"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.lemma_heaps_match",
"lemma_Vale.X64.Memory.modifies_buffer_addr",
"lemma_Vale.X64.Memory.modifies_buffer_readable",
"lemma_Vale.X64.Memory.modifies_valid_taint",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan",
"proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer",
"proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet",
"proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ",
"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.Machine_s.OReg_r",
"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_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer",
"projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet",
"projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_mutable",
"projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_taint",
"projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ",
"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.OReg_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_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_41db9fdf9444e7dc3929e8f963c015c7",
"refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_8de17eec3c1f64d75609148b2dff3180",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_dd592ff911d0f80cdf0ace6c4224ff73",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"string_typing",
"token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"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.AES.OptPublic.hkeys_reqs_pub",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"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_inner",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Lib.Map16.get", "typing_Vale.Lib.Map16.sel2",
"typing_Vale.Lib.Seqs.list_to_seq",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.Memory.buffer_write",
"typing_Vale.X64.Memory.get_vale_heap",
"typing_Vale.X64.Memory.layout_buffers",
"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.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.AES.AES_s.AES_128@tok",
"typing_tok_Vale.AES.AES_s.AES_256@tok",
"typing_tok_Vale.Arch.HeapImpl.Immutable@tok",
"typing_tok_Vale.Arch.HeapImpl.Mutable@tok",
"typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_inversion",
"unit_typing"
],
0,
"45b5717d29e44d44ec146273d92f1c4b"
],
[
"Vale.AES.X64.GF128_Init.va_wp_Keyhash_init",
1,
1,
0,
[ "@query" ],
0,
"bec584b84f4e52b4402de29eb64a6d90"
],
[
"Vale.AES.X64.GF128_Init.va_wpProof_Keyhash_init",
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.GF128_Init.va_wp_Keyhash_init",
"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_mem_layout",
"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_64",
"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.get_vale_heap",
"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.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.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
"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_mem_layout",
"typing_Vale.X64.Decls.va_upd_reg64",
"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,
"9b764e91a9cca5737b9ef0b094c77b23"
],
[
"Vale.AES.X64.GF128_Init.va_quick_Keyhash_init",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"5d8f971dcdf9edd74ebf062225a7d3c3"
]
]
]
Computing file changes ...
