Revision aa1ca8698adfe929a9eff86ac143eaf90fc3e8ee authored by Jay Bosamiya on 03 June 2019, 21:51:38 UTC, committed by Jay Bosamiya on 03 June 2019, 21:51:38 UTC
1 parent 6055e85
Vale.AES.GHash.fst.hints
[
"J��I�K��\u0002O���I�",
[
[
"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_4fb9f86d722672850f4dd78575352362"
],
0,
"e11d55de36caa8bb4100b7e597f9e850"
],
[
"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,
"5a4fc03ec034e72771636c4203730bbd"
],
[
"Vale.AES.GHash.g_power",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_e22ba7a032a73f6d0678d3d186686631_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_ba523126f67e00e7cd55f0b92f16681d",
"well-founded-ordering-on-nat"
],
0,
"3c83713afeb45d60659fb94841df3de9"
],
[
"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_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"43eac44cb24de2dcebbb8241ab8099f2"
],
[
"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_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"4b7287742c7bc27a63b6f2a8650fff4f"
],
[
"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_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"b706d61564d7240dfcd069bde040de20"
],
[
"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,
"e9db3aa5ccae65bb19e3dc1809c68f11"
],
[
"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,
"ccb299d425cfca8baa2802069ef9ea84"
],
[
"Vale.AES.GHash.ghash_poly_unroll",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_6d0180d4fcd10237cf0d87dd345d77cc_3",
"binder_x_e22ba7a032a73f6d0678d3d186686631_4",
"binder_x_e22ba7a032a73f6d0678d3d186686631_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_ba523126f67e00e7cd55f0b92f16681d",
"well-founded-ordering-on-nat"
],
0,
"2eaada43932e3458fe2b1eb61b961962"
],
[
"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_ba523126f67e00e7cd55f0b92f16681d",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Math.Poly2.Bits_s.of_quad32"
],
0,
"6fb00a22d81e5350b6c3a3d86f24d11e"
],
[
"Vale.AES.GHash.ghash_unroll",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_6d0180d4fcd10237cf0d87dd345d77cc_3",
"binder_x_e22ba7a032a73f6d0678d3d186686631_4",
"binder_x_e22ba7a032a73f6d0678d3d186686631_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_ba523126f67e00e7cd55f0b92f16681d",
"well-founded-ordering-on-nat"
],
0,
"0db61a7a885d3b8002007d49b787c226"
],
[
"Vale.AES.GHash.ghash_unroll_back",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_6d0180d4fcd10237cf0d87dd345d77cc_3",
"binder_x_e22ba7a032a73f6d0678d3d186686631_4",
"binder_x_e22ba7a032a73f6d0678d3d186686631_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_ba523126f67e00e7cd55f0b92f16681d",
"well-founded-ordering-on-nat"
],
0,
"99e080df78c8fcd78e64010e79b2eb2e"
],
[
"Vale.AES.GHash.lemma_ghash_unroll_back_forward_rec",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_Prims.nat", "equation_Prims.squash",
"function_token_typing_Prims.__cache_version_number__",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2face2da719245e88584da663444e003",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"85207f9e1e4dd4882c350c08ed2d79e0"
],
[
"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_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_0",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
"binder_x_6d0180d4fcd10237cf0d87dd345d77cc_3",
"binder_x_9128235d2c2f41088ef12e2f5941e366_2",
"binder_x_e22ba7a032a73f6d0678d3d186686631_4",
"binder_x_e22ba7a032a73f6d0678d3d186686631_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_2620d7d5262d043519df28496291f0ec",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f841a8460c30c7c1239a21cda5e1b44c",
"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", "unit_typing",
"well-founded-ordering-on-nat"
],
0,
"d80dea034f0252c0337c9cf49a0b184f"
],
[
"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_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"847ae9116174664ca624b12109453487"
],
[
"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_ba523126f67e00e7cd55f0b92f16681d",
"typing_Vale.AES.GHash.ghash_unroll",
"typing_Vale.AES.GHash.ghash_unroll_back"
],
0,
"2b6780fc4f4224f79f6fec5d063d09e8"
],
[
"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_716d8adf6e9a0d31e273b653461d856b",
"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_4fb9f86d722672850f4dd78575352362",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_fb38b016ed2a00a384f64de88eaa8ebb",
"typing_Tm_abs_716d8adf6e9a0d31e273b653461d856b",
"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,
"b88a3cf5f8720bad6682c49c02e7f189"
],
[
"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_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_0",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
"binder_x_6d0180d4fcd10237cf0d87dd345d77cc_3",
"binder_x_6d0180d4fcd10237cf0d87dd345d77cc_4",
"binder_x_9128235d2c2f41088ef12e2f5941e366_2",
"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_2620d7d5262d043519df28496291f0ec",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"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,
"db8daccdc19ab1a3cc1a7602d0fea99d"
],
[
"Vale.AES.GHash.lemma_ghash_poly_unroll_n",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c23b8f20153bf4f37edc70734cf238e3"
],
0,
"8af4258c2c602a4d728bf020fadee9f6"
],
[
"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_502cb01ef05aa03f246ba4bf1abd0f3f_0",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
"binder_x_6d0180d4fcd10237cf0d87dd345d77cc_3",
"binder_x_9128235d2c2f41088ef12e2f5941e366_2",
"binder_x_e22ba7a032a73f6d0678d3d186686631_4",
"binder_x_e22ba7a032a73f6d0678d3d186686631_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_ba523126f67e00e7cd55f0b92f16681d",
"well-founded-ordering-on-nat"
],
0,
"3965a25a9ff2e8b91876a125b8d25fd3"
],
[
"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_502cb01ef05aa03f246ba4bf1abd0f3f_0",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
"binder_x_6d0180d4fcd10237cf0d87dd345d77cc_3",
"binder_x_9128235d2c2f41088ef12e2f5941e366_2",
"binder_x_e22ba7a032a73f6d0678d3d186686631_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_ba523126f67e00e7cd55f0b92f16681d",
"typing_Vale.AES.GHash.g_power", "typing_Vale.AES.GHash.ghash_poly",
"well-founded-ordering-on-nat"
],
0,
"2ef3e856397059e029f30a73868bac5a"
],
[
"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_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_0",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
"binder_x_6d0180d4fcd10237cf0d87dd345d77cc_3",
"binder_x_9128235d2c2f41088ef12e2f5941e366_2",
"binder_x_e22ba7a032a73f6d0678d3d186686631_4",
"binder_x_e22ba7a032a73f6d0678d3d186686631_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_2620d7d5262d043519df28496291f0ec",
"refinement_interpretation_Tm_refine_4fb9f86d722672850f4dd78575352362",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"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,
"c99e30da350785731c6ffa4343b4d90d"
],
[
"Vale.AES.GHash.lemma_ghash_poly_of_unroll",
1,
1,
0,
[ "@query" ],
0,
"fbe0ff0ca7ced41429cfb22f60926373"
],
[
"Vale.AES.GHash.lemma_add_manip",
1,
1,
0,
[ "@query" ],
0,
"0fb8f7e94c95d7742c9cb69826de9739"
],
[
"Vale.AES.GHash.ghash_incremental_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"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_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_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_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length", "well-founded-ordering-on-nat"
],
0,
"9a70a66257f35fbc23666cfba0343ca0"
],
[
"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_320365ceb6468c29e8eba757f3baa574",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Def.Words.Seq_s_interpretation_Tm_arrow_816baa3f8e222aaee20ed3e2d3992880",
"Vale.Lib.Seqs_s_interpretation_Tm_arrow_16ef5f8cd579d0100db603308677b251",
"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.l_Forall",
"equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
"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",
"equation_Vale.Def.Types_s.quad32_xor_def",
"equation_Vale.Def.Types_s.reverse_bytes_nat32",
"equation_Vale.Def.Types_s.reverse_bytes_nat32_def",
"equation_Vale.Def.Words.Four_s.four_reverse",
"equation_Vale.Def.Words.Four_s.nat_to_four",
"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_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words.Four_s.nat_to_four",
"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_ae6a984e63d148c37929f28597b3ef6c",
"l_quant_interp_af5417e203aad59fe552f0f70981775a",
"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",
"partial_app_typing_a5df2c69070e20952ad8c7ffdfbc7635",
"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_30c926ebf383bedbae82319bb48dcf51",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_401f18bb990fc97a19859cdf0ccb81c7",
"refinement_interpretation_Tm_refine_451ebe5126a63ea46b09b4b334a1ffe0",
"refinement_interpretation_Tm_refine_4efdd8345d485e7dbe72183752bac011",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ab01006cf446ef70d7885ff128284715",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c6a5ae056cb5a72f4660066bbd48d8bd",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_Vale.Def.Types_s.quad32_xor_def",
"token_correspondence_Vale.Def.Types_s.reverse_bytes_nat32_def",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_FStar.UInt.fits", "typing_Prims.pow2",
"typing_Tm_abs_ae6a984e63d148c37929f28597b3ef6c",
"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", "unit_typing"
],
0,
"f44c46f163745e3592185e022e1d0845"
],
[
"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,
"63889e50395c4a5bd8e57163c11a7040"
],
[
"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_611f4d9b9b7ca657fff97fd0b29bf02c_2",
"binder_x_9128235d2c2f41088ef12e2f5941e366_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.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",
"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_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"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,
"5901cbe99b814a44bac0bee625db0b93"
],
[
"Vale.AES.GHash.lemma_ghash_incremental_poly",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Vale.AES.GHash.fun_seq_quad32_LE_poly128",
"equation_Vale.AES.GHash.ghash_incremental",
"equation_Vale.AES.GHash.poly128",
"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.AES.GHash.ghash_incremental_def",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"int_inversion",
"interpretation_Tm_abs_dec3dbae72f9715ccf7c32fd2ebd6d7e",
"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,
"9083b59d265501f10bf62fe79046fb17"
],
[
"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,
"20f56a4ea47c016d073279cdd2173a98"
],
[
"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_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"a8f8397dd69ae20c302bef433029d0e7"
],
[
"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_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"c2ffa34e6b8a0e86c12c9d64ce5941e0"
],
[
"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",
"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.ghash_incremental",
"equation_Vale.AES.GHash_s.ghash_LE",
"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.Def.Opaque_s.make_opaque",
"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_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_3e04674625ba1e90ddf6da6977508e33",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"token_correspondence_Vale.AES.GHash.ghash_incremental_def",
"token_correspondence_Vale.AES.GHash_s.ghash_LE_def",
"typing_FStar.Seq.Base.length",
"typing_Vale.Lib.Seqs_s.all_but_last", "well-founded-ordering-on-nat"
],
0,
"4332592757a702233f21561dd7dc88f1"
],
[
"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",
"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.eqtype",
"equation_Prims.nat", "equation_Vale.AES.GHash.ghash_incremental",
"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.Def.Opaque_s.make_opaque",
"int_inversion", "int_typing",
"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_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_3e04674625ba1e90ddf6da6977508e33",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"token_correspondence_Vale.AES.GHash.ghash_incremental_def",
"typing_FStar.Seq.Base.length",
"typing_Vale.AES.GHash.ghash_incremental",
"typing_Vale.Def.Types_s.quad32",
"typing_Vale.Lib.Seqs_s.all_but_last", "well-founded-ordering-on-nat"
],
0,
"eb3c66ba909f5eb200e0a3bffe72966b"
],
[
"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_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar"
],
0,
"108d77294bfaf70d28c6c4a29b110750"
],
[
"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_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.op_At_Bar"
],
0,
"c41d119eb29ada76f5f27fa220c438ef"
],
[
"Vale.AES.GHash.lemma_hash_append3",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "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_Prims.__cache_version_number__",
"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_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
"typing_Vale.Def.Types_s.quad32", "unit_typing"
],
0,
"b6efff65d23d539e0956632af97d60bc"
],
[
"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_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
"unit_inversion", "unit_typing"
],
0,
"0465bdf8134ab3663eae2f91a04ef200"
],
[
"Vale.AES.GHash.ghash_incremental_bytes_pure_no_extra",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"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_Prims.__cache_version_number__",
"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_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length"
],
0,
"e03a6d432ff0a1098788839d4fda6c20"
],
[
"Vale.AES.GHash.ghash_incremental_bytes_pure_no_extra",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_FStar.Seq.Base.op_At_Bar", "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.le_seq_quad32_to_bytes",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"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_1581adb482c799e9ba4d4a9e29e70668",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d752083afe9106c9349c58895c219f6f",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_Vale.AES.GCTR_s.pad_to_128_bits",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"typing_Vale.Lib.Workarounds.slice_work_around"
],
0,
"37aa1a574795481b4471fcfa6d9ade1e"
],
[
"Vale.AES.GHash.lemma_ghash_incremental_bytes_extra_helper",
1,
1,
0,
[ "@query" ],
0,
"fb1c7b1e05068b3e4eb17088fd6c1d23"
],
[
"Vale.AES.GHash.lemma_ghash_incremental_bytes_extra_helper",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"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_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_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_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d752083afe9106c9349c58895c219f6f",
"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",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
],
0,
"206d873d42ebe5649826358414315dde"
],
[
"Vale.AES.GHash.lemma_ghash_incremental_bytes_extra_helper_alt",
1,
1,
0,
[ "@query" ],
0,
"7dd19bdb694be369c8831fc9f22f685c"
],
[
"Vale.AES.GHash.lemma_ghash_incremental_bytes_extra_helper_alt",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "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_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_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.length"
],
0,
"232c77b448ac6f0329101baf0d1cad7e"
],
[
"Vale.AES.GHash.lemma_ghash_registers",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"equation_Prims.nat", "equation_Prims.squash",
"function_token_typing_Prims.__cache_version_number__",
"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_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"unit_typing"
],
0,
"296dfbb1e21fdf5ea489611bc262b772"
],
[
"Vale.AES.GHash.lemma_ghash_registers",
2,
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_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_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_cdd15a61a8a8f4424284702869adc760",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.length"
],
0,
"955782ac5dd7d753123b42ca3cc04b7a"
]
]
]
Computing file changes ...
