Revision 9a1c35986c9ec0d91b29ce0fcc77700ae032310a authored by Aseem Rastogi on 01 April 2021, 08:46:33 UTC, committed by Aseem Rastogi on 01 April 2021, 08:46:33 UTC
1 parent 122750f
Vale.AES.GF128.fst.hints
[
"L>1;�\r���ɢt0���",
[
[
"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_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.Types_s.quad32_xor", "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_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_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_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.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,
"b8e3d2ed3467258b7af175600e0a24be"
],
[
"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_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.Def.Types_s.quad32_xor",
"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_degree_at_least",
"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.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.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,
"cac24dc30b76964b4b680e0ab8f5352d"
],
[
"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,
"650fba4d11d6f93a953b520e958f8905"
],
[
"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,
"a507ff5349880e49da7cebaa5fe8bdf0"
],
[
"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,
"4b979a86172266ac1bde96d112283c06"
],
[
"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,
"99815e62ec602ecf2509bf52f3147072"
],
[
"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,
"8b7c88509c5e5f6230397af2dc78a923"
],
[
"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,
"57093e59c542beba87752f649094bde8"
],
[
"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,
"734302343f20c18ecc45a21706cb01a7"
],
[
"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,
"45dfe8981935c091a5d6116510ab1fe0"
],
[
"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,
"6e1f1f309fb2563ceefe3693cd94c97f"
],
[
"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,
"1f110b4fb19134f0d71fb351e3f98e51"
],
[
"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,
"e62480b7b9ca232a5a79e2887d074625"
],
[
"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,
"2d509b32797f4b31d9a92d7d068f58fd"
],
[
"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,
"c84aba0358a54dfb55c993d3fc53ff82"
],
[
"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,
"5ffb7a3e987ca4a9516cac960020a4ce"
],
[
"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,
"53547a731e3b7d2e44c600f08688effd"
],
[
"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,
"46aebbc123e3dcf0e026636dd7349e2e"
],
[
"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,
"9ef59cb14b9ffcd9dd2fad33827041af"
],
[
"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,
"8ebffde228bc3b71c90b0e9ab6716bae"
],
[
"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,
"080b278bbdbb32fadff5d7bd2744768b"
],
[
"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,
"febbad0b5b0e317b16683119fb8a446f"
],
[
"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,
"203cf59606390bbd361902ae4b62ad53"
],
[
"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,
"9b56a532051bd2a660ac9e29d335c125"
],
[
"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,
"b993b33b1b23738b7de0476e0b10fe41"
],
[
"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,
"25e0890e0dc71c6af4102af2441fcc33"
],
[
"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,
"ffce790f1e6a966dbdf4ea0799398e29"
],
[
"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,
"a9579cc19866788c0938ba35a7a8676f"
],
[
"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,
"1d7ed81a5b33073b9fd76ec2c28ace16"
],
[
"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,
"e40f0d8e747e16904d119b2e8641a8e7"
],
[
"Vale.AES.GF128.lemma_gf128_mul_rev_distribute_right",
1,
0,
0,
[ "@query" ],
0,
"1b615947eab3dbade499d66f73bf28ba"
],
[
"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,
"4d33c45c32b3d268a9417228b30b9a2b"
],
[
"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,
"4d6f40be2bd5f65eafec0ed2248572fd"
],
[
"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,
"05f42b174cb2c44bace235a66a91e13f"
],
[
"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,
"cb1b1e152eb8e327807231b7fb2c8540"
],
[
"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,
"0577c418f92e052d948ebe80d6e3cac7"
],
[
"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,
"2408fb91e540ad1789ff8046f4b1c4ce"
],
[
"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,
"e98192a54f54ef9eeb86f6a065e88033"
],
[
"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,
"64c4614abb07827c0fe9cb44018f45db"
],
[
"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,
"85f78b295fb9e28dbc69b3d7f087d3b1"
]
]
]
Computing file changes ...
