Revision cef6a8e821f55e71b791555d22b45bd3debc2596 authored by Jonathan Protzenko on 08 May 2020, 16:26:29 UTC, committed by GitHub on 08 May 2020, 16:26:29 UTC
OCaml API: Don't run unit tests which require unsupported features
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,
"5abadcef2a7bb8cf75541c84fe079535"
],
[
"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,
"ec514d3bcbeab6d8517b76c0e7f11c73"
],
[
"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,
"ec8f95eafb115b6caaff22fbd35c4260"
],
[
"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,
"86ab5a0c268062f4c312172f6a62638d"
],
[
"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,
"3316b64eb4846520bca1416b1aaf05f2"
],
[
"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,
"2c56e1749a2f7c74ed56a6cad5564892"
],
[
"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,
"945f99d80d0bb3d6465f984b344d1f26"
],
[
"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,
"91a33bd7675fd1ed0a7bb2ab47247ac9"
],
[
"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,
"fe27749a832c46549dc0e7647b7d35b9"
],
[
"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,
"1c11fea00cc431b216158127bcc2c5a7"
],
[
"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,
"f82c6f0f08218e15ad8d4caf415adad0"
],
[
"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,
"5b6f9ff4eb440390f0b606b0222b71aa"
],
[
"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,
"d0234df860161b1abd5e9996c8373602"
],
[
"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,
"aeba57f2da41b0edf46bbbaba1fe4559"
],
[
"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,
"fb0d9d552acd14ef3863acc4e7e5bcce"
],
[
"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,
"08d9fc9dfe1edb93c1dc3b69eeda6392"
],
[
"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,
"c710da967ea504b5d0c6b405af92159d"
],
[
"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,
"56113549844a64aa3bd43f39643be689"
],
[
"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,
"0a609f6d14645b19987f7232ef69c6b9"
],
[
"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,
"ceb03a3712f3d0f8e1f67c35ea427592"
],
[
"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,
"54c86f1fac0ddbb10cb36d41f2fef397"
],
[
"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,
"8d241f99cb461884ee79206a06936706"
],
[
"Vale.AES.GHash.lemma_ghash_poly_of_unroll",
1,
1,
0,
[ "@query" ],
0,
"daf91e325e20bbd3d229dcd2a0994e00"
],
[
"Vale.AES.GHash.lemma_add_manip",
1,
1,
0,
[ "@query" ],
0,
"8c9c60dd3ddb19915ea16efb20579ae9"
],
[
"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,
"c58b1c6aa4c06067e370b4b6f58433f3"
],
[
"Vale.AES.GHash.ghash_incremental_reveal",
1,
1,
0,
[ "@query" ],
0,
"19f29042266bd587204ca5c67761cb82"
],
[
"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,
"15ea68e8ea3b52e19a342eeac079206f"
],
[
"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,
"f45d87f946024443c808fba15f4cedbd"
],
[
"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,
"9e77a41fac65932b3b78c73d7f4622eb"
],
[
"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,
"f2a3574c6a5cbb97680ee9f861b856da"
],
[
"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,
"4f85e484287201d5a296a12b85aa87b9"
],
[
"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,
"8b11725011e9a7e612246dc3b1481983"
],
[
"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,
"0bef988d06a7f68007adb093e216e197"
],
[
"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,
"9a4864c1e1b8f7645a3ee68b7439dc06"
],
[
"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,
"1a5e74123cc5b2e89719341e37c495ac"
],
[
"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,
"9799a74c6d690b6aa9c7c3a4717d25ff"
],
[
"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,
"1c24a821bdd4899a9a119ed354ad6c1d"
],
[
"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,
"575dd678f0d53451b980ef32da673c44"
],
[
"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,
"034bbb873eecd8d24d2b2d0104366797"
],
[
"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,
"c4be357d9240a76545dab98698c672b2"
],
[
"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,
"322f65f0a437e39e393c38bf69de4c85"
],
[
"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,
"63a7e7002ab042cbe30328a896464914"
],
[
"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,
"dd7b54416b8b9e9b7c05d9f55643ac79"
],
[
"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,
"04b97ec478906e33bfb107a848054971"
],
[
"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,
"5fb66f01a66cc491096dc9b96f2afaed"
],
[
"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,
"a25c8a116d03b88d0dc2dc40f59c0f3c"
],
[
"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,
"c0bf43d873743330563ab79b0a1beeb8"
]
]
]
Computing file changes ...
