https://github.com/project-everest/hacl-star
Tip revision: 4d41d4ec3acc48721e2966ccf1a9a9abdaadc719 authored by Chris Hawblitzel on 14 March 2019, 05:53:02 UTC
Disable X64.Leakage_Ins* to enable merge
Disable X64.Leakage_Ins* to enable merge
Tip revision: 4d41d4e
GF128.fst.hints
[
"���6y��C`�'#va\u001f�",
[
[
"GF128.lemma_of_double32_degree",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "data_elim_Words_s.Mktwo",
"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_Math.Poly2.Bits_s.of_double32_def",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Types_s.double32", "equation_Words_s.nat32",
"equation_Words_s.natN", "fuel_guarded_inversion_Words_s.two",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values",
"lemma_Math.Poly2.Lemmas.lemma_reverse_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d06334d9900dfdcfe1b36628485c60ea",
"typing_FStar.Seq.Base.append", "typing_FStar.UInt.fits",
"typing_FStar.UInt.to_vec", "typing_Math.Poly2_s.of_seq"
],
0,
"4b7e51387fdc0d04fbc807f2b874831a"
],
[
"GF128.lemma_of_quad32_degree",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "data_elim_Words_s.Mkfour",
"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_Math.Poly2.Bits_s.of_quad32_def", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Types_s.quad32",
"equation_Words_s.nat32", "equation_Words_s.natN",
"fuel_guarded_inversion_Words_s.four",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values",
"lemma_Math.Poly2.Lemmas.lemma_reverse_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d06334d9900dfdcfe1b36628485c60ea",
"typing_FStar.Seq.Base.append", "typing_FStar.UInt.fits",
"typing_FStar.UInt.to_vec", "typing_Math.Poly2_s.of_seq"
],
0,
"042f4bf570115d10861357d387744e02"
],
[
"GF128.lemma_to_of_quad32",
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_Math.Poly2.Bits_s.of_quad32_def",
"equation_Math.Poly2.Bits_s.to_quad32_def", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Words_s.nat32",
"equation_Words_s.natN",
"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", "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_num_lemma",
"lemma_FStar.UInt.inverse_vec_lemma", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_096be29ebf8a4e9c3a84b1f7e7850f09",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d06334d9900dfdcfe1b36628485c60ea",
"token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"typing_FStar.Seq.Base.append", "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_Math.Poly2.Bits_s.of_quad32_def",
"typing_Math.Poly2_s.of_seq", "typing_Math.Poly2_s.poly_index",
"typing_Math.Poly2_s.reverse", "typing_Math.Poly2_s.to_seq"
],
0,
"e05a748d5cf56d9cc8c814596f77d13c"
],
[
"GF128.lemma_of_to_quad32",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.to_vec.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.size",
"equation_FStar.UInt.uint_t",
"equation_Math.Poly2.Bits_s.of_quad32_def",
"equation_Math.Poly2.Bits_s.to_quad32_def", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"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", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_096be29ebf8a4e9c3a84b1f7e7850f09",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d06334d9900dfdcfe1b36628485c60ea",
"token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_FStar.UInt.fits",
"typing_FStar.UInt.from_vec",
"typing_Math.Poly2.Bits_s.of_quad32_def",
"typing_Math.Poly2.Bits_s.to_quad32_def",
"typing_Math.Poly2_s.of_seq", "typing_Math.Poly2_s.poly_index",
"typing_Math.Poly2_s.reverse", "typing_Math.Poly2_s.to_seq"
],
0,
"5686af9b91ed7f19c8a1f86aba931bc9"
],
[
"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_GF128.quad32_shift_left_1",
"equation_Math.Poly2.Bits_s.to_quad32_def", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Types_s.quad32_xor", "equation_Types_s.quad32_xor_def",
"equation_Words_s.nat32", "equation_Words_s.natN",
"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_Opaque_s.make_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool", "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_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_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_096be29ebf8a4e9c3a84b1f7e7850f09",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_93ef23291b8fc66eb20296c8c11ea6d9",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ab01006cf446ef70d7885ff128284715",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"token_correspondence_Prims.pow2.fuel_instrumented",
"token_correspondence_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_Math.Poly2_s.poly_index",
"typing_Math.Poly2_s.reverse", "typing_Math.Poly2_s.shift",
"typing_Math.Poly2_s.to_seq", "typing_Prims.pow2",
"typing_Types_s.ishl", "typing_Types_s.ishr", "typing_Types_s.ixor"
],
0,
"5b938f116b8a12eba6d8f54adebc39fd"
],
[
"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_f75731c55f9043e32f86307b15aa8254",
"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_GF128.quad32_shift_2_left_1",
"equation_Math.Poly2.Bits_s.to_quad32_def", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Types_s.quad32_xor", "equation_Types_s.quad32_xor_def",
"equation_Words_s.nat32", "equation_Words_s.natN",
"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", "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_Math.Poly2.Lemmas.lemma_monomial_degree",
"lemma_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_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_096be29ebf8a4e9c3a84b1f7e7850f09",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_93ef23291b8fc66eb20296c8c11ea6d9",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ab01006cf446ef70d7885ff128284715",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"token_correspondence_Opaque_s.make_opaque",
"token_correspondence_Prims.pow2.fuel_instrumented",
"token_correspondence_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_Math.Poly2_s.add",
"typing_Math.Poly2_s.div", "typing_Math.Poly2_s.mod",
"typing_Math.Poly2_s.monomial", "typing_Math.Poly2_s.mul",
"typing_Math.Poly2_s.poly_index", "typing_Math.Poly2_s.reverse",
"typing_Math.Poly2_s.shift", "typing_Math.Poly2_s.to_seq",
"typing_Prims.pow2", "typing_Types_s.ishl", "typing_Types_s.ishr",
"typing_Types_s.ixor"
],
0,
"5f93ed2aca96ff7b2230f670e353d016"
],
[
"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_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad",
"typing_Math.Poly2_s.poly_index", "typing_Math.Poly2_s.reverse"
],
0,
"423fd39c5a0a485bdbda022757e87b7c"
],
[
"GF128.lemma_gf128_degree",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_GF128_s.gf128_modulus",
"equation_GF128_s.gf128_modulus_low_terms", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"interpretation_Tm_abs_716d8adf6e9a0d31e273b653461d856b",
"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_1e148bc46768d27d87d368da0d7ed5ec",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_GF128_s.gf128_modulus_low_terms",
"typing_Math.Poly2_s.monomial", "typing_Math.Poly2_s.of_fun",
"typing_Math.Poly2_s.poly_index",
"typing_Tm_abs_716d8adf6e9a0d31e273b653461d856b"
],
0,
"9df79507fc08dbd9ad0ba214ebcdcc31"
],
[
"GF128.lemma_gf128_constant_rev",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.to_vec.fuel_instrumented", "@query",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.BitVector.zero_vec", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt.zero",
"equation_GF128_s.gf128_modulus_low_terms",
"equation_Math.Poly2.Bits_s.to_quad32_def", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.natN", "fuel_guarded_inversion_Words_s.four",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"interpretation_Tm_abs_b2e57656f0c98802f1367f08b4a4cfe4",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_slice",
"lemma_FStar.UInt.inverse_num_lemma",
"lemma_FStar.UInt.inverse_vec_lemma",
"lemma_FStar.UInt.zero_to_vec_lemma",
"lemma_GF128.lemma_reverse_reverse", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_096be29ebf8a4e9c3a84b1f7e7850f09",
"refinement_interpretation_Tm_refine_1e148bc46768d27d87d368da0d7ed5ec",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_93ef23291b8fc66eb20296c8c11ea6d9",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"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_FStar.UInt.zero",
"typing_GF128_s.gf128_modulus_low_terms",
"typing_Math.Poly2_s.of_fun", "typing_Math.Poly2_s.reverse",
"typing_Math.Poly2_s.to_seq",
"typing_Tm_abs_716d8adf6e9a0d31e273b653461d856b"
],
0,
"6a981f3c26f34fad51babeb550b05043"
],
[
"GF128.lemma_quad32_double_hi_rev",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_Math.Poly2.Lemmas.lemma_monomial_degree",
"lemma_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_ba523126f67e00e7cd55f0b92f16681d",
"typing_Math.Poly2_s.div", "typing_Math.Poly2_s.mod",
"typing_Math.Poly2_s.monomial", "typing_Math.Poly2_s.mul",
"typing_Math.Poly2_s.poly_index", "typing_Math.Poly2_s.reverse"
],
0,
"c27ce92f29d3f26ca6ca2f137c5d7956"
],
[
"GF128.lemma_gf128_mul",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_Prims.nat", "int_inversion",
"lemma_Math.Poly2.Lemmas.lemma_monomial_degree",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Math.Poly2_s.add", "typing_Math.Poly2_s.div",
"typing_Math.Poly2_s.mod", "typing_Math.Poly2_s.monomial",
"typing_Math.Poly2_s.mul", "typing_Math.Poly2_s.poly_index"
],
0,
"1668bf098cd34a55f66a9ef09d985b14"
],
[
"GF128.lemma_gf128_reduce",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "function_token_typing_Math.Poly2_s.zero",
"int_inversion", "lemma_Math.Poly2.lemma_add_degree",
"lemma_Math.Poly2.lemma_div_degree",
"lemma_Math.Poly2.lemma_mod_degree",
"lemma_Math.Poly2.lemma_mul_degree",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0", "typing_Math.Poly2_s.add",
"typing_Math.Poly2_s.div", "typing_Math.Poly2_s.mod",
"typing_Math.Poly2_s.mul", "typing_Math.Poly2_s.poly_index"
],
0,
"08b1180e37ea12b7f6d2b003419e2583"
],
[
"GF128.lemma_gf128_reduce_rev",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"eabcd08cd17763ce9752e859a73fdc40"
],
[
"GF128.lemma_gf128_reduce_rev",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_GF128.lemma_reverse_reverse",
"lemma_Math.Poly2.Lemmas.lemma_monomial_degree",
"lemma_Math.Poly2.lemma_add_degree",
"lemma_Math.Poly2.lemma_div_degree",
"lemma_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_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Math.Poly2_s.add", "typing_Math.Poly2_s.degree",
"typing_Math.Poly2_s.div", "typing_Math.Poly2_s.mod",
"typing_Math.Poly2_s.mul", "typing_Math.Poly2_s.poly_index",
"typing_Math.Poly2_s.reverse", "typing_Math.Poly2_s.shift"
],
0,
"68d847ee9cef1e7a0cc99cb484a75540"
]
]
]