Revision 0d9153dc34ee2dcf0821e3f21e825fc5bb8895b4 authored by Santiago Zanella-Beguelin on 11 December 2019, 17:46:08 UTC, committed by Santiago Zanella-Beguelin on 12 December 2019, 10:33:01 UTC
1 parent 7405f78
Vale.AES.X64.GHash.fst.hints
[
"\u0010Ƃ�\n�\u0000\u0000��ay\u0014/`!",
[
[
"Vale.AES.X64.GHash.get_last_slice_workaround",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647"
],
0,
"7cc596f98875a3ebeca8243a6bfcc1fe"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_Y0",
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.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_reg",
"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_heap_impl_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_typing",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"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_memTaint",
"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.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"string_typing", "typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_inversion", "unit_typing"
],
0,
"80ce6a07ca383bdaf3003b4c8f75972c"
],
[
"Vale.AES.X64.GHash.va_wpProof_compute_Y0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok", "eq2-interp",
"equation_Prims.nat", "equation_Vale.AES.X64.GHash.va_wp_compute_Y0",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"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_reg",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state",
"function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_memTaint",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_xmm",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_typing"
],
0,
"d206b188602c645265a598411b12bc2d"
],
[
"Vale.AES.X64.GHash.va_quick_compute_Y0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"036d1e1e7966bbb551dbe05c9816568b"
],
[
"Vale.AES.X64.GHash.va_lemma_ReduceMul128_LE",
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.logical", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.AES.GF128_s.gf128_to_quad32",
"equation_Vale.Def.Types_s.quad32",
"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_reg",
"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_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"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", "int_typing",
"lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"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_memTaint",
"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.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_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"string_typing", "typing_Vale.AES.GF128_s.gf128_to_quad32",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_typing"
],
0,
"b03f68b05afd972b2cb4a80125ae8163"
],
[
"Vale.AES.X64.GHash.va_wpProof_ReduceMul128_LE",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equation_Prims.nat",
"equation_Vale.AES.X64.GHash.va_wp_ReduceMul128_LE",
"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_reg",
"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_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_memTaint",
"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.AES.GF128_s.gf128_mul",
"typing_Vale.AES.GF128_s.gf128_to_quad32",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_typing"
],
0,
"e076c017ce2b4a8dce2e1fd588e01fba"
],
[
"Vale.AES.X64.GHash.va_quick_ReduceMul128_LE",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"3030e0bd5805c581572b783b25a8b516"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_ghash_incremental_register",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equation_FStar.Seq.Properties.last", "equation_Prims.eq2",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Vale.AES.GF128_s.gf128_of_quad32",
"equation_Vale.AES.GF128_s.gf128_to_quad32",
"equation_Vale.AES.GHash.ghash_incremental",
"equation_Vale.AES.GHash_s.gf128_mul_LE",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Lib.Seqs_s.all_but_last",
"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_reg",
"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_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_heap_impl_equal",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"equation_with_fuel_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_Vale.AES.GF128.lemma_reverse_reverse",
"lemma_Vale.AES.GHash.lemma_ghash_incremental_def_0",
"lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32",
"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_Equality", "primitive_Prims.op_Subtraction",
"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_memTaint",
"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.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_3e04674625ba1e90ddf6da6977508e33",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"string_typing",
"token_correspondence_Vale.AES.GHash.ghash_incremental_def",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.empty",
"typing_Prims.eq2", "typing_Vale.AES.GHash.ghash_incremental",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Lib.Seqs_s.all_but_last",
"typing_Vale.Math.Poly2.Bits_s.of_quad32",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.Machine_s.t_reg",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_inversion", "unit_typing"
],
0,
"1fa9d80fe6b0634b74d11167cfa3a2df"
],
[
"Vale.AES.X64.GHash.va_wpProof_compute_ghash_incremental_register",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equation_Prims.nat",
"equation_Vale.AES.X64.GHash.va_wp_compute_ghash_incremental_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_reg",
"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_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_memTaint",
"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.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_reg",
"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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg", "unit_typing"
],
0,
"1064412e3116c6f1dd2feaa7e50a32bd"
],
[
"Vale.AES.X64.GHash.va_quick_compute_ghash_incremental_register",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"42f5d8069de6df1882e24b9859b0ce2f"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_ghash_incremental_body0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_9ea7f180dd7be45141f353611a13c737",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"4557a8fd6197f80611436fb5e855f68e"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_ghash_incremental_body0",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_FStar.Seq.Properties.last", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_and",
"equation_Prims.l_imp", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.AES.GF128_s.gf128_of_quad32",
"equation_Vale.AES.GF128_s.gf128_to_quad32",
"equation_Vale.AES.GHash.ghash_incremental",
"equation_Vale.AES.GHash_s.gf128_mul_LE",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"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.Seqs_s.all_but_last",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"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.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.Memory.valid_buffer_read",
"equation_Vale.X64.QuickCodes.lexCons",
"equation_Vale.X64.QuickCodes.precedes_wrap",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.state_eta",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"equation_with_fuel_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
"l_imp-interp", "lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Seq.Properties.slice_slice",
"lemma_Vale.AES.GF128.lemma_reverse_reverse",
"lemma_Vale.AES.GHash.lemma_ghash_incremental_def_0",
"lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32",
"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.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"lemma_Vale.X64.Regs.lemma_eta", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"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_memTaint",
"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.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_memTaint",
"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_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_3e04674625ba1e90ddf6da6977508e33",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"string_typing",
"token_correspondence_Vale.AES.GHash.ghash_incremental_def",
"token_correspondence_Vale.Def.Opaque_s.make_opaque",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_Prims.eq2",
"typing_Prims.l_imp", "typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Lib.Seqs_s.all_but_last",
"typing_Vale.Math.Poly2.Bits_s.of_quad32",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.Decls.validSrcAddrs128",
"typing_Vale.X64.Machine_s.t_reg",
"typing_Vale.X64.Memory.buffer_addr",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.Memory.get_vale_heap",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.lexCons",
"typing_Vale.X64.QuickCodes.precedes_wrap",
"typing_Vale.X64.QuickCodes.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_memTaint",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_tok_Prims.LexTop@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_inversion",
"unit_typing", "well-founded-ordering-on-nat"
],
0,
"296707e22d74f077d122c07c0a5d8834"
],
[
"Vale.AES.X64.GHash.va_wp_compute_ghash_incremental_body0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"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.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"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_Vale.X64.State.Mkvale_state_vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"9bec33f3a73b057501adee593de80735"
],
[
"Vale.AES.X64.GHash.va_wpProof_compute_ghash_incremental_body0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.nat",
"equation_Vale.AES.X64.GHash.va_wp_compute_ghash_incremental_body0",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"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.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_memTaint",
"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_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_typing"
],
0,
"4beddc5168555199df0e2e44fb2ef357"
],
[
"Vale.AES.X64.GHash.va_quick_compute_ghash_incremental_body0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"a2b854d4d588fb47798a9a6ea3923043"
],
[
"Vale.AES.X64.GHash.va_code_compute_ghash_incremental_while0",
1,
1,
0,
[
"@query", "constructor_distinct_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.reg_64", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0"
],
0,
"5bb0b5f1f5551f740123079bae695dcf"
],
[
"Vale.AES.X64.GHash.va_qcode_compute_ghash_incremental_while0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_BarBar", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"72c2aa35b3914041be83b2aa13ae05ca"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_ghash_incremental_while0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5d3e35fd2c08cdbd7a2eb3316a904024",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"7720257a019a845b5845076fa5dd5534"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_ghash_incremental_while0",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_and",
"equation_Prims.l_imp", "equation_Prims.l_not",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Lib.Map16.sel16",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"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.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCodes.lexCons",
"equation_Vale.X64.QuickCodes.precedes_wrap",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.state_eta",
"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_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
"int_typing", "l_and-interp", "l_imp-interp", "l_not-interp",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"lemma_Vale.X64.Regs.lemma_eta", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_disEquality",
"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_memTaint",
"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.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_memTaint",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"string_typing", "typing_Prims.eq2", "typing_Prims.l_not",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.Decls.validSrcAddrs128",
"typing_Vale.X64.Memory.buffer_length",
"typing_Vale.X64.Memory.get_vale_heap",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.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_memTaint",
"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.TUInt128@tok",
"typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_typing"
],
0,
"aba02334b27366ec63d2f1d84090b327"
],
[
"Vale.AES.X64.GHash.va_wp_compute_ghash_incremental_while0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"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.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"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_Vale.X64.State.Mkvale_state_vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"56fa4039f302661458272583268f352e"
],
[
"Vale.AES.X64.GHash.va_wpProof_compute_ghash_incremental_while0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.nat",
"equation_Vale.AES.X64.GHash.va_wp_compute_ghash_incremental_while0",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"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.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_inversion",
"int_typing", "lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_memTaint",
"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.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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_typing"
],
0,
"fe59ef3d587e3a42c921be38acfdbaa8"
],
[
"Vale.AES.X64.GHash.va_quick_compute_ghash_incremental_while0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"c7a5e515edcd3dd52514487ef1f818f3"
],
[
"Vale.AES.X64.GHash.va_code_compute_ghash_incremental",
1,
1,
0,
[
"@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.reg_64", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0"
],
0,
"b7001ccffdf36d6e373c54a44cb24868"
],
[
"Vale.AES.X64.GHash.va_qcode_compute_ghash_incremental",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Machine_s.OConst",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.reg_64", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703"
],
0,
"cfc81526c5d85b32102e0d9d3c5a0d5a"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_ghash_incremental",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"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.TUInt128@tok",
"equation_Prims.l_imp", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"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.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_reg",
"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_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.get_vale_heap",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"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_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
"l_imp-interp", "lemma_FStar.Seq.Properties.slice_length",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"primitive_Prims.op_GreaterThan", "primitive_Prims.op_disEquality",
"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_memTaint",
"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.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_memTaint",
"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.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_typing"
],
0,
"4185f326651329effb22f0b7a1a8011c"
],
[
"Vale.AES.X64.GHash.va_wpProof_compute_ghash_incremental",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equation_Prims.nat",
"equation_Vale.AES.X64.GHash.va_wp_compute_ghash_incremental",
"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_reg",
"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_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_memTaint",
"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.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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg", "unit_typing"
],
0,
"9bc6205eda78827c8a81b0fb14bcc162"
],
[
"Vale.AES.X64.GHash.va_quick_compute_ghash_incremental",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"7604961cedc575c6e4d3bd31c08ea763"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_ghash_incremental_partial_body0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_376d7e0615587d28cba5a3d858eb672e",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"677e00103a85a0f5ea002b9bab3198a0"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_ghash_incremental_partial_body0",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_FStar.Seq.Properties.last", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_and",
"equation_Prims.l_imp", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.AES.GF128_s.gf128_of_quad32",
"equation_Vale.AES.GF128_s.gf128_to_quad32",
"equation_Vale.AES.GHash.ghash_incremental",
"equation_Vale.AES.GHash_s.gf128_mul_LE",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"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.Seqs_s.all_but_last",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"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.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.Memory.valid_buffer_read",
"equation_Vale.X64.QuickCodes.lexCons",
"equation_Vale.X64.QuickCodes.precedes_wrap",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.state_eta",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"equation_with_fuel_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
"l_imp-interp", "lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Seq.Properties.slice_slice",
"lemma_Vale.AES.GF128.lemma_reverse_reverse",
"lemma_Vale.AES.GHash.lemma_ghash_incremental_def_0",
"lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32",
"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.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"lemma_Vale.X64.Regs.lemma_eta", "lemma_Vale.X64.Regs.lemma_upd_ne",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"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_memTaint",
"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.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_memTaint",
"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_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_3e04674625ba1e90ddf6da6977508e33",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"string_typing",
"token_correspondence_Vale.AES.GHash.ghash_incremental_def",
"token_correspondence_Vale.Def.Opaque_s.make_opaque",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_Prims.eq2",
"typing_Prims.l_imp", "typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Lib.Seqs_s.all_but_last",
"typing_Vale.Math.Poly2.Bits_s.of_quad32",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg",
"typing_Vale.X64.Decls.validSrcAddrs128",
"typing_Vale.X64.Machine_s.t_reg",
"typing_Vale.X64.Memory.buffer_addr",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.Memory.get_vale_heap",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.lexCons",
"typing_Vale.X64.QuickCodes.precedes_wrap",
"typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
"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_memTaint",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.state_eta", "typing_tok_Prims.LexTop@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_inversion",
"unit_typing", "well-founded-ordering-on-nat"
],
0,
"77d6e3b0e1a7b82c11e365c5f4dd8d94"
],
[
"Vale.AES.X64.GHash.va_wp_compute_ghash_incremental_partial_body0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"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.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"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_Vale.X64.State.Mkvale_state_vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"fb755825a3d833cbfc16db95cb1c34d5"
],
[
"Vale.AES.X64.GHash.va_wpProof_compute_ghash_incremental_partial_body0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.nat",
"equation_Vale.AES.X64.GHash.va_wp_compute_ghash_incremental_partial_body0",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"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.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_upd_ne",
"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_memTaint",
"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_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_memTaint",
"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_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_typing"
],
0,
"c6a1855fd0afdf472ef8dea43b49af56"
],
[
"Vale.AES.X64.GHash.va_quick_compute_ghash_incremental_partial_body0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"167514721766ca0f3887ae51f5dcfc8c"
],
[
"Vale.AES.X64.GHash.va_code_compute_ghash_incremental_partial_while0",
1,
1,
0,
[
"@query", "constructor_distinct_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.reg_64", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0"
],
0,
"68ea9922163e52cf96c2d4c25ec5ca57"
],
[
"Vale.AES.X64.GHash.va_qcode_compute_ghash_incremental_partial_while0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_BarBar", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"255a48412aba5813f942e9a4ed2fd3ec"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_ghash_incremental_partial_while0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3a85a800df319eca5c1d1f4cc3b4633b",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"60eeb4d8f5f81005160608c06439a5b8"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_ghash_incremental_partial_while0",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_and",
"equation_Prims.l_imp", "equation_Prims.l_not",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"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.sel16",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"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.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCodes.lexCons",
"equation_Vale.X64.QuickCodes.precedes_wrap",
"equation_Vale.X64.State.state_eq",
"equation_Vale.X64.State.state_eta",
"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_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
"l_imp-interp", "l_not-interp",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"lemma_Vale.X64.Regs.lemma_eta", "lemma_Vale.X64.Regs.lemma_upd_ne",
"primitive_Prims.op_GreaterThan",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_disEquality",
"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_memTaint",
"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.X64.Machine_s.Reg_r",
"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_memTaint",
"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_414d0a9f578ab0048252f8c8f552b99f",
"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_Prims.eq2", "typing_Prims.l_not",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.Decls.va_upd_reg",
"typing_Vale.X64.Decls.validSrcAddrs128",
"typing_Vale.X64.Machine_s.t_reg",
"typing_Vale.X64.Memory.get_vale_heap",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.range1", "typing_Vale.X64.Regs.eta_sel",
"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_memTaint",
"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.TUInt128@tok",
"typing_tok_Vale.X64.Machine_s.Secret@tok", "unit_typing"
],
0,
"b348fa00635575a7d765425ff0ae6f89"
],
[
"Vale.AES.X64.GHash.va_wp_compute_ghash_incremental_partial_while0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"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.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"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_Vale.X64.State.Mkvale_state_vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"589cb17ce539e4e8b3d183588767a1d6"
],
[
"Vale.AES.X64.GHash.va_wpProof_compute_ghash_incremental_partial_while0",
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.TUInt128@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.nat",
"equation_Vale.AES.X64.GHash.va_wp_compute_ghash_incremental_partial_while0",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"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.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_upd_ne",
"primitive_Prims.op_LessThanOrEqual",
"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_memTaint",
"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.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_memTaint",
"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.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.Arch.HeapTypes_s.TUInt128@tok", "unit_typing"
],
0,
"cbd2e38677cbd45e34f9bf7a07b4044e"
],
[
"Vale.AES.X64.GHash.va_quick_compute_ghash_incremental_partial_while0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"0c24c244cf983327d21e61a9614c37e4"
],
[
"Vale.AES.X64.GHash.va_code_compute_ghash_incremental_partial",
1,
1,
0,
[
"@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.reg_64", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0"
],
0,
"3de7275e6df6c778d18efe09459fa96a"
],
[
"Vale.AES.X64.GHash.va_qcode_compute_ghash_incremental_partial",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Machine_s.OConst",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.reg_64", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703"
],
0,
"5c046fa8924b2e29b185caf68717d57f"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_ghash_incremental_partial",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"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.get_vale_heap", "int_inversion",
"int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4da9e3e3cdf294a1b8c8ba5f2e4418bb",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_FStar.Seq.Base.length",
"typing_Vale.X64.Memory.base_typ_as_vale_type",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"32a4e0a6923ce12e3c9a3d51103ba8e1"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_ghash_incremental_partial",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"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.TUInt128@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_and",
"equation_Prims.l_imp", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"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.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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"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.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"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_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
"l_imp-interp", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
"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_memTaint",
"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.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_memTaint",
"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_211facd8812fd94e95b65d3b8891b14a",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"string_typing", "typing_FStar.Seq.Base.length", "typing_Prims.eq2",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.Memory.buffer_addr",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.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.TUInt128@tok", "unit_typing"
],
0,
"1b853fe720410d29af106794b789a602"
],
[
"Vale.AES.X64.GHash.va_wp_compute_ghash_incremental_partial",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heap_impl",
"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.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_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.get_vale_heap",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_FStar.Seq.Base.length", "typing_Vale.X64.Regs.sel",
"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.TUInt128@tok"
],
0,
"5f16aa130c8110a962eeed742238a1c3"
],
[
"Vale.AES.X64.GHash.va_wpProof_compute_ghash_incremental_partial",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equation_Prims.nat",
"equation_Vale.AES.X64.GHash.va_wp_compute_ghash_incremental_partial",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"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_reg",
"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_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_inversion",
"int_typing", "lemma_Vale.X64.Regs.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_upd_ne",
"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_memTaint",
"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_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_memTaint",
"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_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.X64.Decls.va_upd_ok", "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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg", "unit_typing"
],
0,
"b608b3dbcbd69565e4fc5bb0cd441331"
],
[
"Vale.AES.X64.GHash.va_quick_compute_ghash_incremental_partial",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"efbf5ad8947b8ff341a99a091ea57774"
],
[
"Vale.AES.X64.GHash.va_lemma_ghash_incremental_bytes_no_extra",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat",
"equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"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.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8e7441eb3470d6382ef3f1d0fc91995d",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.get_vale_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"35ff73c4f35ab1c0077ace251fb5eb48"
],
[
"Vale.AES.X64.GHash.va_lemma_ghash_incremental_bytes_no_extra",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"constructor_distinct_Vale.X64.Machine_s.Block",
"disc_equation_Vale.X64.Machine_s.Block", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat",
"equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
"equation_Vale.AES.GCTR_s.pad_to_128_bits",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.Def.Types_s.quad32",
"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.X64.Decls.va_ensure_total",
"equation_Vale.X64.Decls.va_int_range",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Decls.va_upd_ok",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.State.state_eq",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"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_memTaint",
"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_Vale.X64.Machine_s.Block_block",
"projection_inverse_Vale.X64.Machine_s.Block_t_ins",
"projection_inverse_Vale.X64.Machine_s.Block_t_ocmp",
"refinement_interpretation_Tm_refine_4d38686bf695f79f110ce5aef057279f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_FStar.Seq.Base.length",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.buffer_length",
"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.TUInt128@tok"
],
0,
"bd188fafdc2119f1a69d2c744805d0cf"
],
[
"Vale.AES.X64.GHash.va_wp_ghash_incremental_bytes_no_extra",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat",
"equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"9bfb036add2c794c2aefa98430e33889"
],
[
"Vale.AES.X64.GHash.va_wpProof_ghash_incremental_bytes_no_extra",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp",
"equation_Vale.AES.X64.GHash.va_wp_ghash_incremental_bytes_no_extra",
"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_ok",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.t_ensure",
"equation_Vale.X64.State.state_eq",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Flags.lemma_equal_elim",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_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.State.Mkvale_state_vs_flags",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_memTaint",
"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",
"typing_Vale.X64.Decls.va_upd_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_typing"
],
0,
"3888ea43a7c836938b60d73f3ca57891"
],
[
"Vale.AES.X64.GHash.va_quick_ghash_incremental_bytes_no_extra",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"6f2cdf43d0806fe39cac4137c4899b7d"
],
[
"Vale.AES.X64.GHash.va_code_compute_pad_to_128_bits",
1,
1,
0,
[
"@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.reg_64", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0"
],
0,
"0730876473f7e6636b0a45ed7b00540c"
],
[
"Vale.AES.X64.GHash.va_qcode_compute_pad_to_128_bits",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"constructor_distinct_Vale.X64.Machine_s.OConst",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
"equation_Prims.pos", "equation_Prims.squash",
"equation_Vale.AES.GCTR_s.pad_to_128_bits",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"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",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_BarBar",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Machine_s.OReg_r",
"projection_inverse_Vale.X64.Machine_s.OReg_tc",
"projection_inverse_Vale.X64.Machine_s.OReg_tr",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_Vale.Def.Types_s.ishl", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"976daf3c3c2c756c582c4271a2d0b434"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_pad_to_128_bits",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_cb001d656f55c29990f0f250cc738631"
],
0,
"cf45bae2c2a3732d1371195380eba597"
],
[
"Vale.AES.X64.GHash.va_lemma_compute_pad_to_128_bits",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"eq2-interp", "equation_FStar.Seq.Base.op_At_Bar",
"equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.pos",
"equation_Prims.squash", "equation_Vale.AES.GCTR_s.pad_to_128_bits",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.CPU_Features_s.sse_enabled",
"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_ok",
"equation_Vale.X64.Decls.va_upd_reg",
"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.vale_heap_impl_equal",
"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_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_01038503ca215af03557c5e6ade0f6b5",
"interpretation_Tm_abs_e587835b2560428ec79171fb3516ccb3",
"l_and-interp", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Vale.Arch.Types.lemma_insert_nat64_properties",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"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_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"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_memTaint",
"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.X64.Machine_s.OReg_r",
"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_06b9f0ab8ff3c0e49aa83954383f15a4",
"refinement_interpretation_Tm_refine_211facd8812fd94e95b65d3b8891b14a",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"string_typing", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_Prims.pow2", "typing_Vale.AES.GCTR_s.pad_to_128_bits",
"typing_Vale.Def.Types_s.le_quad32_to_bytes",
"typing_Vale.X64.CPU_Features_s.sse_enabled",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_inversion", "unit_typing"
],
0,
"52964b7519df33399c58fa1d1c464d5c"
],
[
"Vale.AES.X64.GHash.va_wp_compute_pad_to_128_bits",
1,
1,
0,
[
"@query", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"edf3a45ef057ce38feda24600206355a"
],
[
"Vale.AES.X64.GHash.va_wpProof_compute_pad_to_128_bits",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equation_Prims.nat",
"equation_Vale.AES.X64.GHash.va_wp_compute_pad_to_128_bits",
"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_reg",
"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.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_memTaint",
"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.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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg", "unit_typing"
],
0,
"7d550cbc74aabe432a2a8066ae5f5b1a"
],
[
"Vale.AES.X64.GHash.va_quick_compute_pad_to_128_bits",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"eb8f4d489bfe840c5d449bf7edb9ab0b"
],
[
"Vale.AES.X64.GHash.va_qcode_ghash_incremental_bytes_register",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"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",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_Vale.X64.Machine_s.t_reg", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"352a5000b35b27083c6cf321fa7829c8"
],
[
"Vale.AES.X64.GHash.va_lemma_ghash_incremental_bytes_register",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"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",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_45315aa498c3aa6ad8040b7d44afe3ea",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_Vale.X64.Machine_s.t_reg", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"5adaf6f5b461450ef9115d64f1c3a475"
],
[
"Vale.AES.X64.GHash.va_lemma_ghash_incremental_bytes_register",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"eq2-interp", "equation_FStar.Seq.Base.op_At_Bar",
"equation_Prims.l_imp", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.AES.GCTR_s.pad_to_128_bits",
"equation_Vale.AES.GHash.ghash_incremental",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"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_reg",
"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_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_heap_impl_equal",
"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.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
"l_imp-interp", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"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_memTaint",
"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.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_211facd8812fd94e95b65d3b8891b14a",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"string_typing", "typing_FStar.Seq.Base.append",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"typing_Vale.X64.Machine_s.t_reg",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_inversion", "unit_typing"
],
0,
"ee3a1e4d0083c45afc54b84efb1291ee"
],
[
"Vale.AES.X64.GHash.va_wp_ghash_incremental_bytes_register",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
"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", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_Vale.X64.Machine_s.t_reg", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"66bc55b75bc604fb7c7c57df311f54b9"
],
[
"Vale.AES.X64.GHash.va_wpProof_ghash_incremental_bytes_register",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equation_Prims.nat",
"equation_Vale.AES.X64.GHash.va_wp_ghash_incremental_bytes_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_reg",
"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_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_memTaint",
"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.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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg", "unit_typing"
],
0,
"909e303f70a805227fd9552d365709c4"
],
[
"Vale.AES.X64.GHash.va_quick_ghash_incremental_bytes_register",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"7b7be8908911f35926e0fec4b299e286"
],
[
"Vale.AES.X64.GHash.va_qcode_ghash_incremental_bytes_extra",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Decls.va_int_range", "int_inversion",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_4d38686bf695f79f110ce5aef057279f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"40e424d43e2cf4cfa4b163b48cbd544c"
],
[
"Vale.AES.X64.GHash.va_lemma_ghash_incremental_bytes_extra",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "eq2-interp",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat",
"equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"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.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b7702e08d59d5a0604c9982ae1137368",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.get_vale_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"88b9733b06f12caf8ae3816a3f4ea0be"
],
[
"Vale.AES.X64.GHash.va_lemma_ghash_incremental_bytes_extra",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"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.TUInt128@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.l_imp",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.AES.GCTR_s.pad_to_128_bits",
"equation_Vale.AES.GHash.ghash_incremental",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"equation_Vale.Def.Types_s.quad32",
"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.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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"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.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.Memory.valid_buffer_read",
"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.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "l_and-interp", "l_imp-interp",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"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_memTaint",
"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.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_memTaint",
"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_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"string_typing", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.Memory.get_vale_heap",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.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.TUInt128@tok", "unit_inversion",
"unit_typing"
],
0,
"130e77217bed60d755c57c1ce8d92ba6"
],
[
"Vale.AES.X64.GHash.va_wp_ghash_incremental_bytes_extra",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.nat",
"equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"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.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"962b02f629d95de86ef043371327de8d"
],
[
"Vale.AES.X64.GHash.va_wpProof_ghash_incremental_bytes_extra",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equation_Prims.nat",
"equation_Vale.AES.X64.GHash.va_wp_ghash_incremental_bytes_extra",
"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_reg",
"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.get_vale_heap",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_memTaint",
"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.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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg", "unit_typing"
],
0,
"1c0d5d59e4dccee51956381c97f0c79d"
],
[
"Vale.AES.X64.GHash.va_quick_ghash_incremental_bytes_extra",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"1159997566478f11d304abde6919b287"
],
[
"Vale.AES.X64.GHash.va_code_ghash_incremental_bytes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Machine_s.OConst",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.reg_64", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703"
],
0,
"0139fb1d17570e5883e17e7427fcb965"
],
[
"Vale.AES.X64.GHash.va_qcode_ghash_incremental_bytes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Machine_s.OConst",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"disc_equation_Vale.X64.Machine_s.OStack", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"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",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_typing",
"primitive_Prims.op_BarBar",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
],
0,
"4a27079d22b76858981e322449c8b9d4"
],
[
"Vale.AES.X64.GHash.va_lemma_ghash_incremental_bytes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.nat",
"equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"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.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_FStar.Seq.Base.length",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.get_vale_heap", "typing_Vale.X64.Regs.sel",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"1d842f3759c697c95daa43b7429df6de"
],
[
"Vale.AES.X64.GHash.va_lemma_ghash_incremental_bytes",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"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.TUInt128@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.l_imp",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
"equation_Vale.AES.GHash.ghash_incremental0",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.Def.Types_s.quad32",
"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.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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"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.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"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_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
"l_imp-interp", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"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_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"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_memTaint",
"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.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_memTaint",
"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_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"string_typing", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.Memory.buffer_addr",
"typing_Vale.X64.Memory.buffer_as_seq",
"typing_Vale.X64.Memory.get_vale_heap",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.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.TUInt128@tok", "unit_inversion",
"unit_typing"
],
0,
"8a9ccd52b316d2297a92b78b93f0ff3c"
],
[
"Vale.AES.X64.GHash.va_wp_ghash_incremental_bytes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.nat",
"equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"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.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.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"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",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_FStar.Seq.Base.length",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.Decls.va_upd_flags",
"typing_Vale.X64.Decls.va_upd_reg64",
"typing_Vale.X64.Decls.va_upd_xmm",
"typing_Vale.X64.Memory.buffer_as_seq", "typing_Vale.X64.Regs.sel",
"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.TUInt128@tok"
],
0,
"4ddd9b4dc0b761cd9fa86756cb050aed"
],
[
"Vale.AES.X64.GHash.va_wpProof_ghash_incremental_bytes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equation_Prims.nat",
"equation_Vale.AES.X64.GHash.va_wp_ghash_incremental_bytes",
"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_reg",
"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_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_memTaint",
"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.X64.Decls.va_upd_reg64", "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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg", "unit_typing"
],
0,
"2139dc656c5bec5e62646416dc03bbeb"
],
[
"Vale.AES.X64.GHash.va_quick_ghash_incremental_bytes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"1f5fd853f77e46615673451dda1ad963"
],
[
"Vale.AES.X64.GHash.va_code_ghash_core",
1,
1,
0,
[
"@query", "constructor_distinct_Vale.X64.Machine_s.OConst",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.reg_64", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0"
],
0,
"fddd29244e0ca47c6477bf7501046488"
],
[
"Vale.AES.X64.GHash.va_qcode_ghash_core",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Machine_s.OConst",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.reg_64", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703"
],
0,
"511946fa510f6ec8b9ecfcd3752b6e72"
],
[
"Vale.AES.X64.GHash.va_lemma_ghash_core",
1,
1,
0,
[ "@query" ],
0,
"0e9f75d9144fbea274eeafcc22be6a5f"
],
[
"Vale.AES.X64.GHash.va_lemma_ghash_core",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
"eq2-interp", "equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Prims.l_imp", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"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_reg",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"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.get_vale_heap",
"equation_Vale.X64.Memory.vale_heap_impl_equal",
"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_Prims.__cache_version_number__",
"int_inversion", "int_typing", "l_and-interp", "l_imp-interp",
"lemma_Vale.X64.Flags.lemma_equal_intro",
"lemma_Vale.X64.QuickCodes.lemma_label_bool",
"lemma_Vale.X64.Regs.lemma_equal_intro",
"primitive_Prims.op_GreaterThan", "primitive_Prims.op_disEquality",
"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_memTaint",
"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.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_memTaint",
"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.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.QuickCodes.label",
"typing_Vale.X64.QuickCodes.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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"unit_inversion", "unit_typing"
],
0,
"f2ddbb742ccceaaa8c51ea075c7418c2"
],
[
"Vale.AES.X64.GHash.va_wp_ghash_core",
1,
1,
0,
[ "@query" ],
0,
"32289f5958dee4add74eb2315332ac25"
],
[
"Vale.AES.X64.GHash.va_wpProof_ghash_core",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
"equation_Prims.nat", "equation_Vale.AES.X64.GHash.va_wp_ghash_core",
"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_reg",
"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_heap_impl_equal",
"equation_Vale.X64.QuickCode.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.X64.State.vale_state", "int_typing",
"lemma_Vale.X64.Regs.lemma_equal_elim",
"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_memTaint",
"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_memTaint",
"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.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_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
"typing_Vale.X64.State.update_reg", "unit_typing"
],
0,
"6da2a4b070958464b417a62a5f4bb877"
],
[
"Vale.AES.X64.GHash.va_quick_ghash_core",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"44b3154b28ce05203bbc3c3f225b1295"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...