Revision 3f979cc1cb15a4491f8b804bbafeabeffe5a1ab1 authored by Aseem Rastogi on 09 April 2019, 11:31:34 UTC, committed by Aseem Rastogi on 09 April 2019, 11:31:34 UTC
1 parent 74a8710
X64.AESopt2.fst.hints
[
"!z�f�u�:~x�ܶ\u001a\u007f�",
[
[
"X64.AESopt2.va_lemma_MulAdd_unroll",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_GHash.ghash_unroll_back.fuel_instrumented",
"@fuel_irrelevance_GHash.ghash_unroll_back.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_X64.Machine_s.Rax",
"constructor_distinct_X64.Vale.Decls.TReg",
"disc_equation_X64.Machine_s.Rsp",
"disc_equation_X64.Vale.Decls.TReg", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rsp@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Types_s.insert_nat32", "equation_Types_s.quad32",
"equation_Words.Four_s.four_insert", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.State.state_eq",
"equation_with_fuel_GHash.ghash_unroll_back.fuel_instrumented",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"interpretation_Tm_abs_26eff54f5f5a449ca54ef2e12357b017",
"interpretation_Tm_abs_38e974c73ddce5660029bd72a3f9dbbc",
"interpretation_Tm_abs_3bcbf9d1622fd266639b232cfb705adb",
"interpretation_Tm_abs_650145e36407b5ad4d8a535b68364744",
"lemma_Math.Poly2.Bits.lemma_of_quad32_degree",
"lemma_Math.Poly2.lemma_add_degree",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"primitive_Prims.op_Equality", "proj_equation_Words_s.Mkfour_hi2",
"proj_equation_Words_s.Mkfour_lo0",
"proj_equation_Words_s.Mkfour_lo1",
"proj_equation_X64.Machine_s.OReg_r",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Vale.Decls.TReg_r",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing",
"token_correspondence_GHash.ghash_unroll_back.fuel_instrumented",
"typing_GHash.shift_gf128_key_1",
"typing_Math.Poly2.Bits_s.of_quad32", "typing_Math.Poly2_s.add",
"typing_Math.Poly2_s.poly", "typing_Math.Poly2_s.shift",
"typing_Prims.eq2", "typing_X64.CPU_Features_s.pclmulqdq_enabled",
"typing_X64.Memory.buffer_read", "typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rsp@tok", "unit_inversion", "unit_typing"
],
0,
"00dab6d24aac9a874a94ef1635468316"
],
[
"X64.AESopt2.va_lemma_MulAdd_unroll",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_GHash.ghash_unroll_back.fuel_instrumented",
"@fuel_irrelevance_GHash.ghash_unroll_back.fuel_instrumented",
"@query",
"GHash_interpretation_Tm_arrow_cc4912c70cb58999a8cb59b402910c64",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_X64.Machine_s.Rax",
"constructor_distinct_X64.Vale.Decls.TReg",
"disc_equation_X64.Machine_s.Rsp",
"disc_equation_X64.Vale.Decls.TReg", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rbp@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_GHash.fun_seq_quad32_LE_poly128", "equation_GHash.poly128",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prims.squash", "equation_Types_s.insert_nat32",
"equation_Types_s.quad32", "equation_Words.Four_s.four_insert",
"equation_Words_s.nat32", "equation_Words_s.nat64",
"equation_X64.AESopt2.va_subscript_FStar__Seq__Base__seq",
"equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.State.state_eq",
"equation_with_fuel_GHash.ghash_unroll_back.fuel_instrumented",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_GHash.fun_seq_quad32_LE_poly128",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_typing",
"interpretation_Tm_abs_26eff54f5f5a449ca54ef2e12357b017",
"interpretation_Tm_abs_38e974c73ddce5660029bd72a3f9dbbc",
"interpretation_Tm_abs_39bbedc1165d2bde4c0ff4da57fc4dbf",
"interpretation_Tm_abs_3bcbf9d1622fd266639b232cfb705adb",
"interpretation_Tm_abs_650145e36407b5ad4d8a535b68364744",
"kinding_Words_s.four@tok",
"lemma_Math.Poly2.Bits.lemma_of_quad32_degree",
"lemma_Math.Poly2.lemma_add_degree",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Words_s.Mkfour_hi2",
"proj_equation_Words_s.Mkfour_lo0",
"proj_equation_Words_s.Mkfour_lo1",
"proj_equation_X64.Machine_s.OReg_r",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Vale.Decls.TReg_r",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_cc2dc5868e7fd4b2687688495de9766a",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing",
"token_correspondence_GHash.fun_seq_quad32_LE_poly128",
"typing_FStar.Seq.Base.length", "typing_GHash.ghash_unroll_back",
"typing_Math.Poly2.Bits_s.of_quad32", "typing_Math.Poly2_s.add",
"typing_Math.Poly2_s.poly", "typing_Math.Poly2_s.shift",
"typing_Prims.eq2", "typing_X64.CPU_Features_s.pclmulqdq_enabled",
"typing_X64.Memory.buffer_read", "typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rbp@tok", "unit_inversion", "unit_typing"
],
0,
"6e365c17cbd8c5d001fd338181268b1a"
],
[
"X64.AESopt2.va_wp_MulAdd_unroll",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"9f3f7359b880c02bd7a7dddc1a0ae266"
],
[
"X64.AESopt2.va_wpMonotone_MulAdd_unroll",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equality_tok_X64.Machine_s.Rax@tok",
"equation_X64.AESopt2.va_wp_MulAdd_unroll",
"equation_X64.Machine_s.xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_tok_X64.Machine_s.Rax@tok", "unit_typing"
],
0,
"589a3b68fa0307ebd9f09620160fa360"
],
[
"X64.AESopt2.va_wpCompute_MulAdd_unroll",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AESopt2.va_wp_MulAdd_unroll",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"eee882c3761b8973e59045e69dc67398"
],
[
"X64.AESopt2.va_wpProof_MulAdd_unroll",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"de0096a029f2b9fc5487bbd371c7bbdc"
],
[
"X64.AESopt2.va_wpProof_MulAdd_unroll",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Rax@tok",
"equation_X64.AESopt2.va_wpCompute_MulAdd_unroll",
"equation_X64.AESopt2.va_wp_MulAdd_unroll",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_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_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESopt2.va_wpCompute_MulAdd_unroll",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_tok_X64.Machine_s.Rax@tok",
"unit_typing"
],
0,
"f873bc9c89c0ba61d0f63443fdd9325c"
],
[
"X64.AESopt2.va_lemma_Reduce",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Prims.eq2", "equation_Prims.squash",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"interpretation_Tm_abs_3bcbf9d1622fd266639b232cfb705adb",
"interpretation_Tm_abs_c02d8f2f7b811f9e9b839ba8964b299e",
"lemma_Math.Poly2.Bits.lemma_of_quad32_degree",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_Math.Poly2_s.poly_index",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "unit_inversion", "unit_typing"
],
0,
"44865e761d164511d5efa2903b436c81"
],
[
"X64.AESopt2.va_wpMonotone_Reduce",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_X64.AESopt2.va_wp_Reduce", "equation_X64.Machine_s.xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_xmm", "unit_typing"
],
0,
"a033588996b71653327233f1b141cbec"
],
[
"X64.AESopt2.va_wpCompute_Reduce",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AESopt2.va_wp_Reduce",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"0a92893361d213e23f375b80d1cac0c7"
],
[
"X64.AESopt2.va_wpProof_Reduce",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"4bda840d9771fbaa7bca316e4d2c276d"
],
[
"X64.AESopt2.va_wpProof_Reduce",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_X64.AESopt2.va_wpCompute_Reduce",
"equation_X64.AESopt2.va_wp_Reduce", "equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_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_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESopt2.va_wpCompute_Reduce",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "unit_typing"
],
0,
"0632b83a479a37d24c28bd4116ce0079"
],
[
"X64.AESopt2.va_lemma_GhashUnroll6x",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"1cb196cc206133506bd6c61534c77a90"
],
[
"X64.AESopt2.va_lemma_GhashUnroll6x",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rbp@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_GF128.gf128_low_shift", "equation_GF128.mod_rev",
"equation_GF128_s.gf128_modulus",
"equation_GF128_s.gf128_modulus_low_terms", "equation_Prims.eq2",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.State.state_eq",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_typing",
"interpretation_Tm_abs_716d8adf6e9a0d31e273b653461d856b",
"kinding_Words_s.four@tok",
"lemma_Math.Poly2.Bits.lemma_of_quad32_degree",
"lemma_Math.Poly2.Bits.lemma_to_of_quad32",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_1e148bc46768d27d87d368da0d7ed5ec",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"string_typing", "typing_GHash.ghash_incremental",
"typing_Math.Poly2_s.of_fun", "typing_Prims.eq2",
"typing_Tm_abs_716d8adf6e9a0d31e273b653461d856b",
"typing_Types_s.reverse_bytes_quad32",
"typing_X64.CPU_Features_s.pclmulqdq_enabled",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
"typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rbp@tok", "unit_inversion", "unit_typing"
],
0,
"e7f2881ce8ea5e8ad73e55c327669e30"
],
[
"X64.AESopt2.va_wp_GhashUnroll6x",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"6ba3e78853b32d5c2312117edc730069"
],
[
"X64.AESopt2.va_wpMonotone_GhashUnroll6x",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equality_tok_X64.Machine_s.Rax@tok",
"equation_X64.AESopt2.va_wp_GhashUnroll6x",
"equation_X64.Machine_s.xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_tok_X64.Machine_s.Rax@tok", "unit_typing"
],
0,
"8dbbd6d1a570e9258ea42bd9f3f8ede6"
],
[
"X64.AESopt2.va_wpCompute_GhashUnroll6x",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AESopt2.va_wp_GhashUnroll6x",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"a015283f16aa26b322b2684149274ffa"
],
[
"X64.AESopt2.va_wpProof_GhashUnroll6x",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"28ab590b88625cf6fc757c1c6c90d393"
],
[
"X64.AESopt2.va_wpProof_GhashUnroll6x",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.Rax@tok",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_X64.AESopt2.va_wpCompute_GhashUnroll6x",
"equation_X64.AESopt2.va_wp_GhashUnroll6x",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_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_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESopt2.va_wpCompute_GhashUnroll6x",
"typing_GHash.ghash_incremental",
"typing_Types_s.reverse_bytes_quad32",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_tok_X64.Machine_s.Rax@tok",
"unit_typing"
],
0,
"9bd74c00f0cdc4fdc43c26f54be20774"
]
]
]
Computing file changes ...
