Revision 5b2fbf3c4989a9b0587a00578f69f3041df3f957 authored by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC, committed by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC
1 parent d4ca892
Vale.AES.GHash.fst.hints
[
"� p�F�29��+�ʜ\b",
[
[
"Vale.AES.GHash.fun_seq_quad32_LE_poly128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
"int_inversion", "lemma_Vale.Math.Poly2.Bits.lemma_of_quad32_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303"
],
0,
"1b1098a7c6d8e26669620317e982106d"
],
[
"Vale.AES.GHash.ghash_poly",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Prims.LexTop@tok",
"int_typing", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
],
0,
"7754cb3d1f69758bd47400a1b362b939"
],
[
"Vale.AES.GHash.g_power",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"852aa0af8a0590e9949fb9e671349978"
],
[
"Vale.AES.GHash.lemma_g_power_1",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat",
"equation_with_fuel_Vale.AES.GHash.g_power.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"00d20c01e00e8e61d3b68ba0dd11ab6a"
],
[
"Vale.AES.GHash.lemma_g_power_n",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"fc5ab3b66be225e71af862fb04d63d18"
],
[
"Vale.AES.GHash.lemma_g_power_n",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.g_power.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Vale.AES.GHash.g_power.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"eb2b2107d9c025ef2edcdb1cb37b7415"
],
[
"Vale.AES.GHash.lemma_gf128_power",
1,
1,
0,
[
"@fuel_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
"@query", "equation_Vale.AES.GHash.gf128_power",
"equation_Vale.AES.GHash.shift_gf128_key_1"
],
0,
"d77d1b58f1b5a3780968f2f82c5c2216"
],
[
"Vale.AES.GHash.hkeys_reqs_priv",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Vale.Def.Types_s.quad32",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.Def.Types_s.quad32"
],
0,
"d4316a6ce21286e10d36052db051ab7c"
],
[
"Vale.AES.GHash.ghash_poly_unroll",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_ae567c2fb75be05905677af440075565_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"ffed2a34a21a957c1a6a08ba5239999a"
],
[
"Vale.AES.GHash.lemma_hkeys_reqs_pub_priv",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
"@fuel_correspondence_Vale.AES.OptPublic.g_power.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.g_power.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.OptPublic.g_power.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"b2t_def", "bool_inversion", "bool_typing", "eq2-interp",
"equation_Prims.nat", "equation_Vale.AES.GHash.gf128_power",
"equation_Vale.AES.GHash.hkeys_reqs_priv",
"equation_Vale.AES.GHash.shift_gf128_key_1",
"equation_Vale.AES.OptPublic.gf128_power",
"equation_Vale.AES.OptPublic.hkeys_reqs_pub",
"equation_Vale.AES.OptPublic.shift_gf128_key_1",
"equation_with_fuel_Vale.AES.GHash.g_power.fuel_instrumented",
"equation_with_fuel_Vale.AES.OptPublic.g_power.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"l_and-interp", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Math.Poly2.Bits_s.of_quad32"
],
0,
"bf5d30424b3fbc92a27f40d91c2f9194"
],
[
"Vale.AES.GHash.ghash_unroll",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_ae567c2fb75be05905677af440075565_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"a7ba35f382add4fea75acb033ef08995"
],
[
"Vale.AES.GHash.ghash_unroll_back",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_ae567c2fb75be05905677af440075565_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"25bca8d2f9b18e8c65b9bb71e538cebc"
],
[
"Vale.AES.GHash.lemma_ghash_unroll_back_forward_rec",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
"equation_Prims.squash", "primitive_Prims.op_LessThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d082c25ffbd7b6a53819c793e953bf49"
],
0,
"97773e8d1842b50b3fff780aca14b159"
],
[
"Vale.AES.GHash.lemma_ghash_unroll_back_forward_rec",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
"@fuel_correspondence_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.AES.GHash_interpretation_Tm_arrow_15ceef7ed9aea3b9eeb1e60e5343be5b",
"b2t_def", "binder_x_4926595fe3e8db262b015229c320f9d3_2",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_0",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
"binder_x_ae567c2fb75be05905677af440075565_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.AES.GHash.gf128_power",
"equation_Vale.AES.GHash.poly128",
"equation_with_fuel_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
"equation_with_fuel_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a377a1c538d267af6aae0d6b523b7c2b",
"refinement_interpretation_Tm_refine_f54be9bebc70c1c037e0ec20437e5c81",
"token_correspondence_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
"typing_Vale.AES.GHash.gf128_power",
"typing_Vale.AES.GHash.ghash_unroll",
"typing_Vale.AES.GHash.ghash_unroll_back",
"typing_Vale.Math.Poly2_s.mul", "well-founded-ordering-on-nat"
],
0,
"6ebf33e498547bda2f91edd77284a52d"
],
[
"Vale.AES.GHash.lemma_ghash_unroll_back_forward",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"31d686c8fcec94c0f37dca11a5bc64ba"
],
[
"Vale.AES.GHash.lemma_ghash_unroll_back_forward",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
"@fuel_correspondence_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat",
"equation_with_fuel_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
"equation_with_fuel_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.AES.GHash.ghash_unroll",
"typing_Vale.AES.GHash.ghash_unroll_back"
],
0,
"5c31247c4978817b8cbd209c38e066e1"
],
[
"Vale.AES.GHash.lemma_gf128_mul_rev_mod_rev",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.AES.GF128.gf128_mul_rev",
"equation_Vale.AES.GF128.mod_rev",
"equation_Vale.AES.GF128.shift_key_1",
"equation_Vale.AES.GF128_s.gf128_modulus",
"equation_Vale.AES.GF128_s.gf128_modulus_low_terms",
"equation_Vale.AES.GF128_s.gf128_mul",
"equation_Vale.AES.GHash.shift_gf128_key_1",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
"int_typing",
"interpretation_Tm_abs_91a45626d634360d0cb72d9b8d62e58c",
"lemma_Vale.Math.Poly2.Lemmas.lemma_mask_degree",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"lemma_Vale.Math.Poly2.lemma_add_degree",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303",
"refinement_interpretation_Tm_refine_fe6ca960360a1d9d67a3dd4cf32a29b0",
"typing_Tm_abs_91a45626d634360d0cb72d9b8d62e58c",
"typing_Vale.AES.GF128_s.gf128_modulus",
"typing_Vale.AES.GHash.shift_gf128_key_1",
"typing_Vale.Math.Poly2.mask", "typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.of_fun",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift",
"typing_Vale.Math.Poly2_s.zero"
],
0,
"1f85d7508fcfe250ef3e998eb91988d7"
],
[
"Vale.AES.GHash.lemma_ghash_poly_degree",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.ghash_poly.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.ghash_poly.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.AES.GHash_interpretation_Tm_arrow_15ceef7ed9aea3b9eeb1e60e5343be5b",
"binder_x_4926595fe3e8db262b015229c320f9d3_2",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_0",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
"binder_x_ae567c2fb75be05905677af440075565_3",
"binder_x_ae567c2fb75be05905677af440075565_4",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.AES.GF128.gf128_mul_rev",
"equation_Vale.AES.GHash.poly128",
"equation_with_fuel_Vale.AES.GHash.ghash_poly.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_f54be9bebc70c1c037e0ec20437e5c81",
"token_correspondence_Vale.AES.GHash.ghash_poly.fuel_instrumented",
"typing_Vale.AES.GF128_s.gf128_mul",
"typing_Vale.AES.GHash.ghash_poly", "typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.reverse", "well-founded-ordering-on-nat"
],
0,
"d6fa92e10486edd096e70da71e57d908"
],
[
"Vale.AES.GHash.lemma_ghash_poly_unroll_n",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_72db1aa12a11b9200241af01f87c606e"
],
0,
"a7f57952cc34b7529bd05d7c4b6747f3"
],
[
"Vale.AES.GHash.lemma_ghash_poly_unroll_n",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
"@fuel_correspondence_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.g_power.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_4926595fe3e8db262b015229c320f9d3_2",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_0",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
"binder_x_ae567c2fb75be05905677af440075565_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5", "equation_Prims.nat",
"equation_with_fuel_Vale.AES.GHash.g_power.fuel_instrumented",
"equation_with_fuel_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"5274949413864a49fc5ae9c5fb263665"
],
[
"Vale.AES.GHash.lemma_ghash_poly_unroll",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
"@fuel_correspondence_Vale.AES.GHash.ghash_poly.fuel_instrumented",
"@fuel_correspondence_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.ghash_poly.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_4926595fe3e8db262b015229c320f9d3_2",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_0",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
"binder_x_ae567c2fb75be05905677af440075565_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.AES.GF128.op_Star_Tilde",
"equation_with_fuel_Vale.AES.GHash.g_power.fuel_instrumented",
"equation_with_fuel_Vale.AES.GHash.ghash_poly.fuel_instrumented",
"equation_with_fuel_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.AES.GHash.g_power", "typing_Vale.AES.GHash.ghash_poly",
"well-founded-ordering-on-nat"
],
0,
"3b4540ee8d48e1fd7eee56ba0cec4625"
],
[
"Vale.AES.GHash.lemma_ghash_unroll_poly_unroll",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
"@fuel_correspondence_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
"@fuel_correspondence_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.AES.GHash_interpretation_Tm_arrow_15ceef7ed9aea3b9eeb1e60e5343be5b",
"binder_x_4926595fe3e8db262b015229c320f9d3_2",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_0",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
"binder_x_ae567c2fb75be05905677af440075565_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5", "equation_Prims.nat",
"equation_Vale.AES.GF128.gf128_mul_rev",
"equation_Vale.AES.GF128.op_Star_Tilde",
"equation_Vale.AES.GHash.gf128_power",
"equation_Vale.AES.GHash.poly128",
"equation_with_fuel_Vale.AES.GHash.g_power.fuel_instrumented",
"equation_with_fuel_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
"equation_with_fuel_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
"int_inversion", "int_typing",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"lemma_Vale.Math.Poly2.lemma_add_degree",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303",
"refinement_interpretation_Tm_refine_f54be9bebc70c1c037e0ec20437e5c81",
"token_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
"typing_Vale.AES.GF128_s.gf128_mul",
"typing_Vale.Math.Poly2_s.reverse", "well-founded-ordering-on-nat"
],
0,
"84a007f950b41b002151d98b98ecbdc1"
],
[
"Vale.AES.GHash.lemma_ghash_poly_of_unroll",
1,
1,
0,
[ "@query" ],
0,
"b35823258fc239dc088f8c664ea784cb"
],
[
"Vale.AES.GHash.lemma_add_manip",
1,
1,
0,
[ "@query" ],
0,
"8d02ab798d4123ccc935c8a3ba7c5fba"
],
[
"Vale.AES.GHash.ghash_incremental_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Lib.Seqs_s.all_but_last",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Equality", "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",
"typing_FStar.Seq.Base.length", "well-founded-ordering-on-nat"
],
0,
"52fb653a3adc7e93f160529e3109a075"
],
[
"Vale.AES.GHash.ghash_incremental_reveal",
1,
1,
0,
[ "@query" ],
0,
"f69a23b16c46e49e972504c823d8920a"
],
[
"Vale.AES.GHash.lemma_reverse_bytes_quad32_xor",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Lib.Seqs_s_interpretation_Tm_arrow_5ead088aae36f5466dc4f492316985f2",
"b2t_def", "bool_inversion", "bool_typing",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Def.Types_s.be_bytes_to_nat32",
"equation_Vale.Def.Types_s.nat32_to_be_bytes",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Types_s.quad32_xor_def",
"equation_Vale.Def.Types_s.reverse_bytes_nat32_def",
"equation_Vale.Def.Words.Four_s.four_reverse",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seq_to_four_BE",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Lib.Seqs_s.reverse_seq",
"equation_Vale.Math.Bits.lemmas_i2b_all",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Types_s.quad32_xor",
"function_token_typing_Vale.Def.Types_s.reverse_bytes_nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones",
"int_inversion", "int_typing",
"interpretation_Tm_abs_e33894a065c7d8cf9373282d9aa6a27c",
"l_quant_interp_48240b4f3858918eae686ff2a62a9fe7",
"l_quant_interp_ab92dcdc665fc6e1201234d45389b203",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8",
"lemma_Vale.Def.Words.Seq.nat_to_four_to_nat",
"lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxBitVec32_proj_0",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_a",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_0c91e66c97ed3054dc88c856ecfaebc1",
"refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e",
"refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
"refinement_interpretation_Tm_refine_637bf9344435626707effe179cd350a8",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c6a5ae056cb5a72f4660066bbd48d8bd",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_fae547c0c57b476075b6de4468df2cfa",
"token_correspondence_Vale.Def.Types_s.quad32_xor_def",
"token_correspondence_Vale.Def.Types_s.reverse_bytes_nat32_def",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
"typing_Prims.pow2",
"typing_Tm_abs_e33894a065c7d8cf9373282d9aa6a27c",
"typing_Vale.Def.Types_s.ixor",
"typing_Vale.Def.Types_s.nat32_to_be_bytes",
"typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
"typing_Vale.Def.Words.Seq_s.seq_to_four_BE",
"typing_Vale.Def.Words_s.int_to_natN",
"typing_Vale.Math.Bits.add_hide", "typing_Vale.Math.Bits.mul_hide",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2_s.degree"
],
0,
"ee2970868830b514e275cbae986d5f27"
],
[
"Vale.AES.GHash.lemma_ghash_incremental_poly_rec",
1,
1,
0,
[
"@query", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"887b288b5d7f7c91712f92e096cbb6c7"
],
[
"Vale.AES.GHash.lemma_ghash_incremental_poly_rec",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"@fuel_correspondence_Vale.AES.GHash.ghash_poly.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.ghash_poly.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_4926595fe3e8db262b015229c320f9d3_3",
"binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_2",
"binder_x_e97427d583e1f4d42a96b4bdd8dae147_0",
"binder_x_e97427d583e1f4d42a96b4bdd8dae147_1",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.last", "equation_Prims.nat",
"equation_Vale.AES.GF128.gf128_mul_rev",
"equation_Vale.AES.GF128.op_Star_Tilde",
"equation_Vale.AES.GF128_s.gf128_of_quad32",
"equation_Vale.AES.GF128_s.gf128_to_quad32",
"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_with_fuel_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"equation_with_fuel_Vale.AES.GHash.ghash_poly.fuel_instrumented",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"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_quant_interp_9d28f2c215748aabc91cf2d5039b0560",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan", "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_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"typing_FStar.Seq.Base.length", "typing_Vale.AES.GF128_s.gf128_mul",
"typing_Vale.AES.GF128_s.gf128_of_quad32",
"typing_Vale.AES.GF128_s.gf128_to_quad32",
"typing_Vale.Def.Types_s.quad32_xor",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Math.Poly2.Bits_s.of_quad32",
"typing_Vale.Math.Poly2_s.reverse", "well-founded-ordering-on-nat"
],
0,
"04ac20e3c65372783be4905a192e4a94"
],
[
"Vale.AES.GHash.lemma_ghash_incremental_poly",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.AES.GHash.fun_seq_quad32_LE_poly128",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.AES.GHash.ghash_incremental",
"function_token_typing_Vale.AES.GHash.ghash_incremental_def",
"int_inversion",
"interpretation_Tm_abs_2a4e5f30c6fdc83783b57e5a74d18144",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"token_correspondence_Vale.AES.GHash.fun_seq_quad32_LE_poly128"
],
0,
"14f4ee2587c8584b5b36137a1ab2669d"
],
[
"Vale.AES.GHash.lemma_ghash_incremental_def_0",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_with_fuel_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"primitive_Prims.op_Equality"
],
0,
"d922a93d170f92b1dec957d0138edf64"
],
[
"Vale.AES.GHash.ghash_incremental_to_ghash",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
"primitive_Prims.op_GreaterThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"8fe48c9354b40b2026c82ed1fed0a2be"
],
[
"Vale.AES.GHash.ghash_incremental_to_ghash",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
"primitive_Prims.op_GreaterThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"fa13bb866645060e0d3c2631d7b73c97"
],
[
"Vale.AES.GHash.ghash_incremental_to_ghash",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"@fuel_correspondence_Vale.AES.GHash_s.ghash_LE_def.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.GHash_s.ghash_LE_def.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_1",
"binder_x_e97427d583e1f4d42a96b4bdd8dae147_0",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.AES.GHash_s.ghash_plain_LE",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Lib.Seqs_s.all_but_last",
"equation_with_fuel_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"equation_with_fuel_Vale.AES.GHash_s.ghash_LE_def.fuel_instrumented",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.AES.GHash.ghash_incremental",
"function_token_typing_Vale.AES.GHash_s.ghash_LE",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_Vale.AES.GHash.lemma_ghash_incremental_def_0",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3cde0f73125500a52bff30114a1a1137",
"refinement_interpretation_Tm_refine_3e04674625ba1e90ddf6da6977508e33",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.AES.GHash.ghash_incremental_def",
"token_correspondence_Vale.AES.GHash_s.ghash_LE_def",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_Vale.Lib.Seqs_s.all_but_last", "typing_tok_Prims.LexTop@tok",
"well-founded-ordering-on-nat"
],
0,
"03934ebd862e1513a5ad008b4f98d333"
],
[
"Vale.AES.GHash.lemma_hash_append",
1,
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_e4836109f73687024ac3edd113084865",
"binder_x_cee79fb2a0b31329a2e2b29d477b66be_2",
"binder_x_cee79fb2a0b31329a2e2b29d477b66be_3",
"binder_x_e97427d583e1f4d42a96b4bdd8dae147_0",
"binder_x_e97427d583e1f4d42a96b4bdd8dae147_1",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.last", "equation_Prims.nat",
"equation_Vale.AES.GHash_s.ghash_plain_LE",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Lib.Seqs_s.all_but_last",
"equation_with_fuel_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.AES.GHash.ghash_incremental",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Vale.AES.GHash.lemma_ghash_incremental_def_0",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3cde0f73125500a52bff30114a1a1137",
"refinement_interpretation_Tm_refine_3e04674625ba1e90ddf6da6977508e33",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"token_correspondence_Vale.AES.GHash.ghash_incremental_def",
"typing_FStar.Seq.Base.length",
"typing_Vale.AES.GHash.ghash_incremental",
"typing_Vale.Lib.Seqs_s.all_but_last", "typing_tok_Prims.LexTop@tok",
"well-founded-ordering-on-nat"
],
0,
"5dda217a4195e3339a8d4be48b29f8e7"
],
[
"Vale.AES.GHash.lemma_ghash_incremental0_append",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
"equation_Vale.AES.GHash.ghash_incremental0",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar"
],
0,
"837dc05f94b73969e74df8f559c97924"
],
[
"Vale.AES.GHash.lemma_hash_append2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
"equation_Vale.AES.GHash.ghash_incremental0",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"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",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar"
],
0,
"cefa6f8024695b56b3f62597dc47b6c8"
],
[
"Vale.AES.GHash.lemma_hash_append3",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat32",
"kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
"typing_Vale.Def.Types_s.quad32"
],
0,
"150e7a1e256b7e9f71280eb8fc3ff797"
],
[
"Vale.AES.GHash.lemma_hash_append3",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.AES.GHash.ghash_incremental0",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"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",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
"unit_inversion", "unit_typing"
],
0,
"e5c5a5a2fcee2f536abdad6a8a7d1739"
],
[
"Vale.AES.GHash.ghash_incremental_bytes_pure_no_extra",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"kinding_Vale.Def.Words_s.four@tok",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_FStar.Seq.Base.length"
],
0,
"5481251cf79dff849ec6599ac58f23ca"
],
[
"Vale.AES.GHash.ghash_incremental_bytes_pure_no_extra",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "equation_Prims.nat",
"equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
"equation_Vale.AES.GCTR_s.pad_to_128_bits",
"equation_Vale.AES.GHash.ghash_incremental0",
"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",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_slice",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1"
],
0,
"ddd16d2d5be89daec6dd5114901788ea"
],
[
"Vale.AES.GHash.lemma_ghash_incremental_bytes_extra_helper",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "l_and-interp",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
"typing_Vale.Def.Types_s.le_quad32_to_bytes"
],
0,
"5fc735f4a4bca7d9ab54332b91eec4ca"
],
[
"Vale.AES.GHash.lemma_ghash_incremental_bytes_extra_helper",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"equation_FStar.Seq.Base.op_At_Bar",
"equation_FStar.Seq.Properties.split", "equation_Prims.nat",
"equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
"equation_Vale.AES.GCTR_s.pad_to_128_bits",
"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.nat8",
"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_create_len",
"lemma_FStar.Seq.Base.lemma_index_slice",
"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",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_06b9f0ab8ff3c0e49aa83954383f15a4",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_9490cfb1c0d2cc8b6f2817cf9207cbd0",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice",
"typing_Vale.AES.GCTR_s.pad_to_128_bits",
"typing_Vale.Def.Types_s.le_quad32_to_bytes"
],
0,
"65d3ad3969a5a848137eb85e700390a4"
],
[
"Vale.AES.GHash.lemma_ghash_incremental_bytes_extra_helper_alt",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
"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_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_Vale.Def.Types_s.le_quad32_to_bytes"
],
0,
"e80ed637ad94e404896a746666a6deea"
],
[
"Vale.AES.GHash.lemma_ghash_incremental_bytes_extra_helper_alt",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"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",
"primitive_Prims.op_Addition", "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_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.length"
],
0,
"a147a60786ed6bca19c1df96b7ade8d2"
],
[
"Vale.AES.GHash.lemma_ghash_registers",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
"equation_Prims.squash", "int_inversion", "l_and-interp",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"778b870494e374f9ca9ebdacc299bcda"
],
[
"Vale.AES.GHash.lemma_ghash_registers",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
"equation_Vale.AES.GHash.ghash_incremental0",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1a5730b11931d46761662d21375532a0",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length"
],
0,
"f06dea034b76b18a11d0cb18f80cd4fa"
]
]
]
Computing file changes ...
