Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
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,
"a3153496130114db1f0c4f56c2a0d580"
],
[
"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,
"f811ca63613414dae8d24dabf8d62ad5"
],
[
"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,
"af520c9299ce4b642132cd50b21af58f"
],
[
"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,
"885135a115be2bd55cbe095b49891532"
],
[
"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,
"993e3a75f7686f3b5600e9c71c712db4"
],
[
"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,
"22e9d63c984cad00e1afbdbbdefca852"
],
[
"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,
"7e5fba02271d9483b5a77afff48825be"
],
[
"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,
"03e5a84bb0f4d154e496636acebc66f4"
],
[
"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,
"b551bf0a26ff3bc57f6e9fa2720fb620"
],
[
"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,
"6d5001559e97be0e297bc62a6418a965"
],
[
"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,
"43cd3d8e5aa59c581b339d029cf913ab"
],
[
"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,
"81f801f0f960c3ad7383ad5ee37cd272"
],
[
"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,
"77e6dee0cd55aee90afde8d815063b7d"
],
[
"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,
"cf6b0a2939e1ea96193e37a9184e7f95"
],
[
"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,
"95e23dd2942cd8c8f1a457a1feaf020e"
],
[
"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,
"e6b368d0d3423a7adfc773b90bddefe7"
],
[
"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,
"0a9576a1ff490c7cdc3a290b41cd632b"
],
[
"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,
"9c2a96ddcbbd85c785ae9652663b826b"
],
[
"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,
"fb44e63da8dad73f1e8eeb7ff1624c44"
],
[
"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,
"77e07ef7dae982bdcc46d3166ad0b12e"
],
[
"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,
"80f79d5f31d08a50d574637c2ecae818"
],
[
"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,
"23f8d677e9a2efce73005db56f8aa990"
],
[
"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,
"57be6fe056876fcb1526c3a560e3b9ce"
],
[
"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,
"85f8719be71b81fc470f1b56385fc9c9"
],
[
"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,
"98b8bfc660c271c5b75b8abc23b788a5"
],
[
"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,
"dc2e0369e0ee1a4289e62bb1ebb266cb"
],
[
"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,
"c88f3c311474df3e2af4bb3b0a0e90bc"
],
[
"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,
"71703f8a151c090b330c7d6e37b1809a"
],
[
"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,
"fe7b38a25d8e812404eb0ec515816a45"
],
[
"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,
"ccf716cb3c6a3f6e1da46cfeba35482e"
],
[
"Vale.AES.GF128.lemma_gf128_mul_rev_distribute_right",
1,
0,
0,
[ "@query" ],
0,
"192ee685fbe35bb8a4449c6e9ee6a71a"
],
[
"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,
"943513fc963db7c0ae408b0193005cf9"
],
[
"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,
"e489f30820d1eb1e4f6d8379f20801a5"
],
[
"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,
"e1ac89bafa5797d1d0a1774f40ca58e0"
],
[
"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,
"574ee04563ebbf6e71ef7439dd5b1da7"
],
[
"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,
"d398184c9c6a14cf6a28e5c9227bf3bf"
],
[
"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,
"c02f8482614afa7018d57ed0da6ce1b8"
],
[
"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,
"4b22cc12e2273d24037bc1685b23d7c2"
],
[
"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,
"031e691666a699248cde06046b37e4dc"
],
[
"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,
"9b26968cc6aba9e0a807e026bfcbf8b5"
]
]
]
Computing file changes ...
