Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Vale.AES.GF128.fst.hints
[
"��\r�1�,C\"7<�����",
[
[
"Vale.AES.GF128.lemma_shift_left_1",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
"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.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.AES.GF128.quad32_shift_left_1",
"equation_Vale.Def.Types_s.quad32_xor",
"equation_Vale.Def.Types_s.quad32_xor_def",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits_s.to_quad32_def",
"equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
"equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"int_inversion", "int_typing",
"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_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.inverse_num_lemma",
"lemma_FStar.UInt.inverse_vec_lemma", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"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_0ca87202d8e02d1c00a86cd121980a4f",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_637bf9344435626707effe179cd350a8",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3571ca27e8115116dfd2d473dcbb7c0",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"token_correspondence_Prims.pow2.fuel_instrumented",
"token_correspondence_Vale.Def.Types_s.quad32_xor_def",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_FStar.UInt.fits", "typing_FStar.UInt.from_vec",
"typing_FStar.UInt.to_vec", "typing_Prims.pow2",
"typing_Vale.Def.Types_s.ishl", "typing_Vale.Def.Types_s.ishr",
"typing_Vale.Def.Types_s.ixor", "typing_Vale.Math.Poly2.ones",
"typing_Vale.Math.Poly2_s.degree",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift",
"typing_Vale.Math.Poly2_s.to_seq"
],
0,
"d9bf91aeaca4a10a72b4a870a8337675"
],
[
"Vale.AES.GF128.lemma_shift_2_left_1",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
"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.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.AES.GF128.quad32_shift_2_left_1",
"equation_Vale.Def.Types_s.quad32_xor",
"equation_Vale.Def.Types_s.quad32_xor_def",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits_s.to_quad32_def",
"equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
"equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool",
"function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones",
"int_inversion", "int_typing",
"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_FStar.UInt.inverse_vec_lemma", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
"lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree",
"lemma_Vale.Math.Poly2.lemma_mod_degree",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.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_0ca87202d8e02d1c00a86cd121980a4f",
"refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_637bf9344435626707effe179cd350a8",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3571ca27e8115116dfd2d473dcbb7c0",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"token_correspondence_Prims.pow2.fuel_instrumented",
"token_correspondence_Vale.Def.Opaque_s.make_opaque",
"token_correspondence_Vale.Def.Types_s.quad32_xor_def",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_FStar.UInt.fits", "typing_FStar.UInt.from_vec",
"typing_FStar.UInt.to_vec", "typing_Prims.pow2",
"typing_Vale.Def.Types_s.ishl", "typing_Vale.Def.Types_s.ishr",
"typing_Vale.Def.Types_s.ixor",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.ones", "typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.degree", "typing_Vale.Math.Poly2_s.div",
"typing_Vale.Math.Poly2_s.mod", "typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.mul",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift",
"typing_Vale.Math.Poly2_s.to_seq"
],
0,
"9d45612226fee3c501a60aaa94ebc5fb"
],
[
"Vale.AES.GF128.lemma_reverse_reverse",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Prims.nat", "int_inversion", "int_typing",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse"
],
0,
"75930bf9846cb1972d511987d662757c"
],
[
"Vale.AES.GF128.lemma_gf128_degree",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_Prims.nat", "equation_Vale.AES.GF128_s.gf128_modulus",
"equation_Vale.AES.GF128_s.gf128_modulus_low_terms",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"interpretation_Tm_abs_91a45626d634360d0cb72d9b8d62e58c",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_fe6ca960360a1d9d67a3dd4cf32a29b0",
"typing_Tm_abs_91a45626d634360d0cb72d9b8d62e58c",
"typing_Vale.AES.GF128_s.gf128_modulus_low_terms",
"typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.of_fun",
"typing_Vale.Math.Poly2_s.poly_index"
],
0,
"f709671f43df57addb623ed4737656a9"
],
[
"Vale.AES.GF128.lemma_gf128_constant_rev",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Vale.AES.GF128_interpretation_Tm_arrow_4fa58ffb11875158cb928c4b45c423ed",
"Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_67d1eb0e2b2b0432bd883bf79e9b388c",
"bool_inversion", "bool_typing", "equation_Prims.nat",
"equation_Vale.AES.GF128_s.gf128_modulus_low_terms",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Math.Poly2.Bits.of_nat32_zero",
"int_inversion", "int_typing",
"interpretation_Tm_abs_822c77d7be66c8cd8df630b78dd2fda3",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_4337ec945cb4c294d0e8ff2d420e64d7",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_fe6ca960360a1d9d67a3dd4cf32a29b0",
"typing_Tm_abs_822c77d7be66c8cd8df630b78dd2fda3",
"typing_Tm_abs_91a45626d634360d0cb72d9b8d62e58c",
"typing_Vale.AES.GF128_s.gf128_modulus_low_terms",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.of_fun",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift",
"typing_Vale.Math.Poly2_s.zero"
],
0,
"a0b8e600efb29d78b757a46540d39dc5"
],
[
"Vale.AES.GF128.lemma_quad32_double_hi_rev",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Prims.nat", "int_inversion", "int_typing",
"lemma_Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
"lemma_Vale.Math.Poly2.lemma_div_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2_s.div", "typing_Vale.Math.Poly2_s.mod",
"typing_Vale.Math.Poly2_s.monomial", "typing_Vale.Math.Poly2_s.mul",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse"
],
0,
"bae05bfb60f62081e526a83d51d12451"
],
[
"Vale.AES.GF128.lemma_gf128_mul",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_Prims.nat", "int_inversion",
"lemma_Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.div",
"typing_Vale.Math.Poly2_s.mod", "typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.mul", "typing_Vale.Math.Poly2_s.poly_index"
],
0,
"78f6c52e572c79a1c7e5d0548ee00875"
],
[
"Vale.AES.GF128.lemma_gf128_reduce",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"int_inversion", "lemma_Vale.Math.Poly2.lemma_add_degree",
"lemma_Vale.Math.Poly2.lemma_div_degree",
"lemma_Vale.Math.Poly2.lemma_mod_degree",
"lemma_Vale.Math.Poly2.lemma_mul_degree",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0", "typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.div", "typing_Vale.Math.Poly2_s.mod",
"typing_Vale.Math.Poly2_s.mul",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.zero"
],
0,
"7d8f36d30c0a88d8c84f5acbea7125b8"
],
[
"Vale.AES.GF128.lemma_gf128_reduce_rev",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"aea5043eb1d0dc45b895e8e9da1d9ad9"
],
[
"Vale.AES.GF128.lemma_gf128_reduce_rev",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Prims.nat", "equation_Prims.pos",
"int_inversion", "int_typing",
"lemma_Vale.AES.GF128.lemma_reverse_reverse",
"lemma_Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"lemma_Vale.Math.Poly2.lemma_add_degree",
"lemma_Vale.Math.Poly2.lemma_div_degree",
"lemma_Vale.Math.Poly2.lemma_mul_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.degree",
"typing_Vale.Math.Poly2_s.div", "typing_Vale.Math.Poly2_s.mod",
"typing_Vale.Math.Poly2_s.mul",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift"
],
0,
"aafab868de7ed258cae292596d91debc"
],
[
"Vale.AES.GF128.lemma_odd_reverse_shift_right",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"0c5d7dec3d3ccd668529b65598997a16"
],
[
"Vale.AES.GF128.lemma_odd_reverse_shift_right",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift"
],
0,
"f2e1c1cb55857c49b7a810db9f79c947"
],
[
"Vale.AES.GF128.lemma_mul_odd_reverse_shift_right",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"2db8d8d764d26e84f37099088069537b"
],
[
"Vale.AES.GF128.lemma_mul_odd_reverse_shift_right",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Vale.Math.Poly2_s.monomial", "typing_Vale.Math.Poly2_s.mul"
],
0,
"c0116922755f74c42f20028d2081158a"
],
[
"Vale.AES.GF128.lemma_mul_odd_reverse_shift_right_hi",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"3a93740070e139313056fcd3f51907a4"
],
[
"Vale.AES.GF128.lemma_mul_odd_reverse_shift_right_hi",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Vale.Math.Poly2_s.mul",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift", "typing_Vale.Math.Poly2_s.zero"
],
0,
"3c95496b1a493a81684fce2c6a246a18"
],
[
"Vale.AES.GF128.lemma_mul_odd_reverse_shift_right_lo_shift",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"d99f50fd65f9a63c5fbe828f6a660038"
],
[
"Vale.AES.GF128.lemma_mul_odd_reverse_shift_right_lo_shift",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Prims.nat", "equation_Prims.pos",
"int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Vale.Math.Poly2_s.mul", "typing_Vale.Math.Poly2_s.poly_index"
],
0,
"51ce9dca529bb4c924002352a5ffa085"
],
[
"Vale.AES.GF128.lemma_reduce_rev_hi",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"81db6ec5d4598491f295b490c92d03ef"
],
[
"Vale.AES.GF128.lemma_reduce_rev_hi",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Math.Poly2.swap", "int_inversion", "int_typing",
"lemma_Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
"lemma_Vale.Math.Poly2.lemma_add_degree",
"lemma_Vale.Math.Poly2.lemma_div_degree",
"lemma_Vale.Math.Poly2.lemma_mod_degree",
"lemma_Vale.Math.Poly2.lemma_mul_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.div",
"typing_Vale.Math.Poly2_s.mod", "typing_Vale.Math.Poly2_s.mul",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift"
],
0,
"d52aec468c7fb9e67b83bb604588915d"
],
[
"Vale.AES.GF128.lemma_swap_right",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_Vale.Math.Poly2.swap", "int_inversion", "int_typing",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0", "typing_Vale.Math.Poly2.mask",
"typing_Vale.Math.Poly2.swap", "typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift"
],
0,
"44788afdbe50226f7e8f9ae7e2a9b1b3"
],
[
"Vale.AES.GF128.lemma_reduce_rev_bits",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Math.Poly2.swap", "int_inversion", "int_typing",
"lemma_Vale.Math.Poly2.Lemmas.lemma_mask_degree",
"lemma_Vale.Math.Poly2.Lemmas.lemma_shift_degree",
"lemma_Vale.Math.Poly2.lemma_add_degree",
"lemma_Vale.Math.Poly2.lemma_mul_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Vale.Math.Poly2.mask", "typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.degree", "typing_Vale.Math.Poly2_s.mul",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift"
],
0,
"75d0823a0fc2ef8450dd5ed350740594"
],
[
"Vale.AES.GF128.lemma_reduce_rev",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"eacd77c4bed1325d0dbb42c4fd71c458"
],
[
"Vale.AES.GF128.lemma_reduce_rev",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Prims.nat", "int_inversion", "int_typing",
"lemma_Vale.Math.Poly2.Lemmas.lemma_mask_degree",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"lemma_Vale.Math.Poly2.Lemmas.lemma_shift_degree",
"lemma_Vale.Math.Poly2.lemma_add_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.mod",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift"
],
0,
"179d1bfcebfcb80d56a20b03073e74c8"
],
[
"Vale.AES.GF128.lemma_gf128_low_shift",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Vale.AES.GF128_interpretation_Tm_arrow_4fa58ffb11875158cb928c4b45c423ed",
"Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_67d1eb0e2b2b0432bd883bf79e9b388c",
"bool_inversion", "bool_typing", "equation_Prims.nat",
"equation_Vale.AES.GF128.gf128_low_shift",
"equation_Vale.AES.GF128_s.gf128_modulus_low_terms",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Math.Poly2.Bits.of_nat32_zero",
"int_inversion", "int_typing",
"interpretation_Tm_abs_822c77d7be66c8cd8df630b78dd2fda3",
"interpretation_Tm_abs_91a45626d634360d0cb72d9b8d62e58c",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"lemma_Vale.Math.Poly2.Lemmas.lemma_shift_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_4337ec945cb4c294d0e8ff2d420e64d7",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_fe6ca960360a1d9d67a3dd4cf32a29b0",
"typing_Tm_abs_822c77d7be66c8cd8df630b78dd2fda3",
"typing_Tm_abs_91a45626d634360d0cb72d9b8d62e58c",
"typing_Vale.AES.GF128.gf128_low_shift",
"typing_Vale.AES.GF128_s.gf128_modulus_low_terms",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.degree",
"typing_Vale.Math.Poly2_s.of_fun",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift",
"typing_Vale.Math.Poly2_s.zero"
],
0,
"7413d22067945059f7c770142f52cd66"
],
[
"Vale.AES.GF128.lemma_gf128_high_bit",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones",
"function_token_typing_Vale.Math.Poly2.Bits.of_nat32_zero",
"int_inversion", "int_typing",
"lemma_Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
"lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_4337ec945cb4c294d0e8ff2d420e64d7",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.degree",
"typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift", "typing_Vale.Math.Poly2_s.zero"
],
0,
"543c3f8c726742c525e276a9441425f7"
],
[
"Vale.AES.GF128.lemma_gf128_low_shift_1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Vale.AES.GF128_interpretation_Tm_arrow_4fa58ffb11875158cb928c4b45c423ed",
"Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_67d1eb0e2b2b0432bd883bf79e9b388c",
"bool_inversion", "bool_typing", "equation_Prims.nat",
"equation_Vale.AES.GF128.gf128_low_shift",
"equation_Vale.AES.GF128_s.gf128_modulus_low_terms",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Math.Poly2.Bits.of_nat32_zero",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_one_degree",
"int_inversion", "int_typing",
"interpretation_Tm_abs_822c77d7be66c8cd8df630b78dd2fda3",
"interpretation_Tm_abs_91a45626d634360d0cb72d9b8d62e58c",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"lemma_Vale.Math.Poly2.Lemmas.lemma_shift_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_4337ec945cb4c294d0e8ff2d420e64d7",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_aaa8221de098e46cfe83e5c3439e6ce8",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_fe6ca960360a1d9d67a3dd4cf32a29b0",
"typing_Tm_abs_822c77d7be66c8cd8df630b78dd2fda3",
"typing_Tm_abs_91a45626d634360d0cb72d9b8d62e58c",
"typing_Vale.AES.GF128.gf128_low_shift",
"typing_Vale.AES.GF128_s.gf128_modulus_low_terms",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.degree",
"typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.of_fun", "typing_Vale.Math.Poly2_s.one",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift",
"typing_Vale.Math.Poly2_s.zero"
],
0,
"5ff06403ec95749143a21aacf3f855a3"
],
[
"Vale.AES.GF128.lemma_gf128_mul_rev_commute",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.AES.GF128.gf128_mul_rev",
"equation_Vale.AES.GF128.op_Star_Tilde",
"equation_Vale.AES.GF128_s.gf128_mul", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2_s.reverse"
],
0,
"c72b8dfb74453c01ae083cce487472e7"
],
[
"Vale.AES.GF128.lemma_gf128_mul_rev_associate",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.AES.GF128.gf128_mul_rev",
"equation_Vale.AES.GF128.op_Star_Tilde",
"equation_Vale.AES.GF128_s.gf128_modulus",
"equation_Vale.AES.GF128_s.gf128_mul", "int_typing",
"lemma_Vale.AES.GF128.lemma_reverse_reverse",
"lemma_Vale.Math.Poly2.lemma_mod_degree",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.AES.GF128_s.gf128_modulus",
"typing_Vale.AES.GF128_s.gf128_mul", "typing_Vale.Math.Poly2_s.mul",
"typing_Vale.Math.Poly2_s.reverse"
],
0,
"376adc24ac3ca8f2f35c29a176db8077"
],
[
"Vale.AES.GF128.lemma_gf128_mul_rev_distribute_left",
1,
0,
0,
[
"@query", "equation_Vale.AES.GF128.gf128_mul_rev",
"equation_Vale.AES.GF128.op_Star_Tilde",
"equation_Vale.AES.GF128_s.gf128_mul",
"projection_inverse_BoxInt_proj_0"
],
0,
"8bc0781cea0415e4cb058855e030349c"
],
[
"Vale.AES.GF128.lemma_gf128_mul_rev_distribute_right",
1,
0,
0,
[ "@query" ],
0,
"31b761e38489ee645703faa26b4aa54e"
],
[
"Vale.AES.GF128.mod_rev",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"0ce8716ea0831576512fa29566305908"
],
[
"Vale.AES.GF128.lemma_add_mod_rev",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"equation_Vale.AES.GF128.mod_rev", "int_inversion", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"7e1988d51d22d9c0b73053661d5e2885"
],
[
"Vale.AES.GF128.shift_key_1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"0e0068b1d26cd271cf93cbaf3606daf1"
],
[
"Vale.AES.GF128.lemma_shift_key_1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"dbd7e6f95e8a46277dc35e76b92a17e5"
],
[
"Vale.AES.GF128.lemma_shift_key_1",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.AES.GF128.shift_key_1",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_Vale.Math.Poly2.Lemmas.lemma_shift_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.degree",
"typing_Vale.Math.Poly2_s.mod",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift",
"typing_Vale.Math.Poly2_s.zero"
],
0,
"dba082568a0365a237bbf822b1c1dd87"
],
[
"Vale.AES.GF128.lemma_test_high_bit",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"a68712ea298f9f8feee5f041fba3398c"
],
[
"Vale.AES.GF128.lemma_test_high_bit",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones",
"int_typing", "lemma_Vale.Math.Poly2.Lemmas.lemma_and_degree",
"lemma_Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
"lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.Bits_s.to_quad32",
"typing_Vale.Math.Poly2.poly_and", "typing_Vale.Math.Poly2_s.degree",
"typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift"
],
0,
"85b90544092cd97f6ae03875af50f0c7"
],
[
"Vale.AES.GF128.lemma_Mul128",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_Prims.nat", "int_inversion", "int_typing",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2.mask", "typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.monomial", "typing_Vale.Math.Poly2_s.mul",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift"
],
0,
"3363f90936fe97c1e5db9e43adb17391"
],
[
"Vale.AES.GF128.lemma_Mul128_accum",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2.mask", "typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.monomial", "typing_Vale.Math.Poly2_s.mul",
"typing_Vale.Math.Poly2_s.shift"
],
0,
"c42e69d15816b6aeb5e52baf6a356ae9"
]
]
]
Computing file changes ...
