Revision b5e85960e109efb08b9c65a4ab85c9b4ef926419 authored by Jay Bosamiya on 04 June 2019, 18:24:09 UTC, committed by Jay Bosamiya on 04 June 2019, 18:24:09 UTC
1 parent 2a5defc
Vale.Poly1305.Math.fst.hints
[
"\u0012#9z\u0014\u000fP��\u0000\u000eG����",
[
[
"Vale.Poly1305.Math.lowerUpper128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"39dc2367516869f88e6a8c15e9b47eee"
],
[
"Vale.Poly1305.Math.lemma_mul_div_comm",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"0ab196624385b98c069c9b667d0fb84b"
],
[
"Vale.Poly1305.Math.lemma_mul_div_comm",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"e8126bba29bc083fa522f4bc4176a81a"
],
[
"Vale.Poly1305.Math.lemma_exact_mul",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"64861f00b2792ff18ddcfbbf0c981ea7"
],
[
"Vale.Poly1305.Math.lemma_exact_mul",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"60e5890b9dac97ee7f4db54be464389f"
],
[
"Vale.Poly1305.Math.lemma_mul_div_sep",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"6f86d7eb5685c8c76673c02f754d58cf"
],
[
"Vale.Poly1305.Math.lemma_mul_div_sep",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"bb49208e705303d8b5d34d27e5c75338"
],
[
"Vale.Poly1305.Math.swap_add",
1,
1,
0,
[ "@query" ],
0,
"38626cd96eab31caff0d1c56c0ec21d8"
],
[
"Vale.Poly1305.Math.lemma_mul_increases",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"cb93eb6abf6f5e8ef959a3d3159626ea"
],
[
"Vale.Poly1305.Math.multiplication_order_lemma_int",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"07d31480f10f91fbb56eac7ccc6bf3ce"
],
[
"Vale.Poly1305.Math.multiplication_order_eq_lemma_int",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"958052bec566e455ec63dec0102adc9c"
],
[
"Vale.Poly1305.Math.lemma_poly_multiply",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
"equation_Prims.squash", "l_and-interp",
"primitive_Prims.op_GreaterThan",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"ea04863d3ed2a6eaafe8b4471ebe4186"
],
[
"Vale.Poly1305.Math.lemma_poly_multiply",
2,
0,
0,
[ "@query", "projection_inverse_BoxInt_proj_0", "true_interp" ],
0,
"ac9794bb913f5017aa9f58a55467accc"
],
[
"Vale.Poly1305.Math.lemma_poly_multiply",
3,
0,
0,
[ "@query" ],
0,
"6486f0d2b97e401a11feaa5b7ead9275"
],
[
"Vale.Poly1305.Math.lemma_poly_reduce",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"equation_Prims.squash", "int_inversion", "l_and-interp",
"primitive_Prims.op_GreaterThan",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"unit_typing"
],
0,
"f4c12bdd8b229a83e315f915dbf76dda"
],
[
"Vale.Poly1305.Math.lemma_poly_reduce",
2,
0,
0,
[ "@query", "projection_inverse_BoxInt_proj_0", "true_interp" ],
0,
"1c9b9b98b9032df08fb28be884d5c398"
],
[
"Vale.Poly1305.Math.lemma_poly_reduce",
3,
0,
0,
[ "@query" ],
0,
"04f6b04610d5b8884adca6dbc6cf15e3"
],
[
"Vale.Poly1305.Math.lemma_shr2_nat",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.udiv", "equation_FStar.UInt.uint_t",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Poly1305.Bitvectors.lemma_shr2",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"b3369612f457ab73795a5d182a751173"
],
[
"Vale.Poly1305.Math.lemma_shr4_nat",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.udiv", "equation_FStar.UInt.uint_t",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Poly1305.Bitvectors.lemma_shr4",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"10bcf903b8aa7ec4dcda3114135f32d0"
],
[
"Vale.Poly1305.Math.lemma_and_mod_n_nat",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.mod",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Poly1305.Bitvectors.lemma_and_mod_n",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Vale.Def.Types_s.iand"
],
0,
"1385611ac15ccd9d42eb1ace876ea4a2"
],
[
"Vale.Poly1305.Math.lemma_and_constants_nat",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"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.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Poly1305.Bitvectors.lemma_and_constants",
"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_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"c49a3e65c6df1827eb56e29547342df1"
],
[
"Vale.Poly1305.Math.lemma_clear_lower_2_nat",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.mul_mod",
"equation_FStar.UInt.size", "equation_FStar.UInt.udiv",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Poly1305.Bitvectors.lemma_clear_lower_2",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0722e9115d2a1be8d90527397d01011c",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_e49d79feeb1e96b29b0f01b06f8dac23",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.UInt.udiv", "typing_Vale.Def.Types_s.iand"
],
0,
"e2c8b09641fd6f0f04a76f019f6a43d3"
],
[
"Vale.Poly1305.Math.lemma_poly_constants_nat",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.mod",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Poly1305.Bitvectors.lemma_poly_constants",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"916707070a734d7beb38278d1c24c0e1"
],
[
"Vale.Poly1305.Math.lemma_and_commutes_nat",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"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_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_da98c95d2af35788da839c6c05bdbc1c",
"typing_Prims.pow2"
],
0,
"f3248cac1dc49778f62e937045709460"
],
[
"Vale.Poly1305.Math.lemma_poly_bits64",
1,
0,
0,
[ "@query" ],
0,
"63b80ceb9c0e468faa3f9777e89d71b2"
],
[
"Vale.Poly1305.Math.lemma_mul_strict_upper_bound",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0", "unit_inversion", "unit_typing"
],
0,
"e9058864e8c7c3944bda56cbf45013c4"
],
[
"Vale.Poly1305.Math.lemma_bytes_shift_power2",
1,
0,
0,
[ "@query" ],
0,
"199af5fba578956a64a9ece719d52b3d"
],
[
"Vale.Poly1305.Math.lemma_bytes_shift_power2",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"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_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_da98c95d2af35788da839c6c05bdbc1c",
"typing_Prims.pow2"
],
0,
"74ec0885b169be56af9dab56d1feffed"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "int_inversion",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87"
],
0,
"f2facbee24eee170f6e64f9304597c77"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod1",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_FStar.UInt.pow2_values", "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_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"009a35a6cf11f8ffd25fc8c805460e60"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod2",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_FStar.UInt.pow2_values", "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_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"bb4269442f62f4f9b742c5a99a388612"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod3",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_FStar.UInt.pow2_values", "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_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"b261f01a44ac6794ebd01c5d97e36eef"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod4",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_FStar.UInt.pow2_values", "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_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"217a0155747930861eb9419667038374"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod5",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_FStar.UInt.pow2_values", "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_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"a2d3410568e421bc208fc8dbabbd1b4c"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod6",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_FStar.UInt.pow2_values", "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_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"3d47206c2e82334f59b5dfdc11c07ee6"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod7",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_FStar.UInt.pow2_values", "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_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"5378e3fa00d5c4f68a953cc30153ec50"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod0",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.BitVector.logand_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.logand", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.mod",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
"typing_FStar.BitVector.logand_vec", "typing_FStar.UInt.to_vec"
],
0,
"f7fb92040ea0f6c260e2bf952890b222"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod0",
3,
1,
0,
[ "@query" ],
0,
"b0ef25339964413335688bae485ed43c"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod1",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.BitVector.logand_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.logand", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.mod",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"true_interp", "typing_FStar.BitVector.logand_vec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec"
],
0,
"ee27ae68b30d5b88ad5ce92bfe0e3df3"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod1",
3,
1,
0,
[ "@query" ],
0,
"7422d89c0f6c11c5999ff62dc403c962"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod2",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.BitVector.logand_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.logand", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.mod",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"true_interp", "typing_FStar.BitVector.logand_vec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec"
],
0,
"19d2c5a3d779ab2f7977c98ff462efa4"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod2",
3,
1,
0,
[ "@query" ],
0,
"8c4407dcdd8b59b1db1a94d67b5065fe"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod3",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.mod", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"true_interp", "typing_FStar.UInt.fits"
],
0,
"80c46e8700f16ad25e670568068556bc"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod3",
3,
1,
0,
[ "@query" ],
0,
"bb5a5e441404ae3bf684662f5b50d542"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod4",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.BitVector.logand_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.logand", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.mod",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"true_interp", "typing_FStar.BitVector.logand_vec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec"
],
0,
"111a7783086e83e7d8daf16d5326b678"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod4",
3,
1,
0,
[ "@query" ],
0,
"4559381b167514d343ae4f83f90be73e"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod5",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.mod", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"true_interp", "typing_FStar.UInt.fits"
],
0,
"b85605799f38c2721dc0d19b525e3d42"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod5",
3,
1,
0,
[ "@query" ],
0,
"ee3729a3550bd073f0be17803a6c2d69"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod6",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.mod", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"true_interp", "typing_FStar.UInt.fits"
],
0,
"e5f6a33548fa788008c0d696ce14c680"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod6",
3,
1,
0,
[ "@query" ],
0,
"5e858988952948f861a48634c15a70ca"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod7",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.mod", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"true_interp", "typing_FStar.UInt.fits"
],
0,
"fded4e2d8a8b7ab076d2d4bc96f03b1b"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod7",
3,
1,
0,
[ "@query" ],
0,
"5ffb6aa125b0102bcde0cdca7d18ad01"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Vale.Def.Types_s.ishl"
],
0,
"cdaf5c552ba74602425833e07bfae760"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"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.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "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_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_da98c95d2af35788da839c6c05bdbc1c",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.UInt.fits", "typing_Prims.pow2",
"typing_Vale.Def.Types_s.ishl"
],
0,
"08b7ee98eb2121302e42f790d005ab81"
],
[
"Vale.Poly1305.Math.lemma_mod_factors",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"true_interp"
],
0,
"fc7bdc12c2b4a6a7ebed00e85c05b60e"
],
[
"Vale.Poly1305.Math.lemma_mul_pos_pos_is_pos_inverse",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"unit_inversion", "unit_typing"
],
0,
"319def844cdfbbe19119d4e0404931aa"
],
[
"Vale.Poly1305.Math.lemma_mod_factor_lo",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"cedd41954839a1a03e78ff31ca91d881"
],
[
"Vale.Poly1305.Math.lemma_mod_power2_lo",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"equation_Prims.squash", "int_inversion", "l_and-interp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"unit_typing"
],
0,
"136528d526e6f894b46b9d08885a4e54"
],
[
"Vale.Poly1305.Math.lemma_mod_power2_lo",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Poly1305.Math.lowerUpper128",
"equation_Vale.Poly1305.Math.lowerUpper128_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Poly1305.Math.lowerUpper128",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_Vale.Poly1305.Math.lowerUpper128",
"typing_Prims.pow2"
],
0,
"8861f0e57bf0622406ef1a16dc1a5944"
],
[
"Vale.Poly1305.Math.lemma_power2_add64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"42332cf1a798f7c91bca96e15fa01720"
],
[
"Vale.Poly1305.Math.lemma_power2_add64",
2,
0,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"0afd22c9b61c39d7a6264da1086dd7ea"
],
[
"Vale.Poly1305.Math.lemma_part_bound1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"true_interp"
],
0,
"eeaa2ebd7d5d917a301e5f779a100957"
],
[
"Vale.Poly1305.Math.lemma_lt_le_trans",
1,
0,
0,
[ "@query" ],
0,
"fec35fbb15e263c3dc1b91cff9fe0b99"
],
[
"Vale.Poly1305.Math.lemma_part_bound2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"1cfda55219a79b747f8cfa9cbfc48727"
],
[
"Vale.Poly1305.Math.lemma_truncate_middle",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"6f26bccc3df46df6b2030531ec9c127d"
],
[
"Vale.Poly1305.Math.lemma_mod_breakdown",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"true_interp"
],
0,
"3886caf9682581c70f4dc79c2f668c06"
],
[
"Vale.Poly1305.Math.lemma_mod_breakdown",
2,
0,
0,
[ "@query" ],
0,
"4564e239117f52d33377f2923d1510c7"
],
[
"Vale.Poly1305.Math.lemma_mod_hi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"31c6d8702debf6dcaae918cdabec95de"
],
[
"Vale.Poly1305.Math.lemma_mod_hi",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Poly1305.Math.lowerUpper128",
"equation_Vale.Poly1305.Math.lowerUpper128_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Poly1305.Math.lowerUpper128",
"int_inversion", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"token_correspondence_Vale.Poly1305.Math.lowerUpper128"
],
0,
"55408811a02c135cdbc1db0012c2a08a"
],
[
"Vale.Poly1305.Math.lemma_poly_demod",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"36d204bfb1f179516727a670cc9632d3"
],
[
"Vale.Poly1305.Math.lemma_poly_demod",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"27d59fac9ae322ba3ef1293019a5af2e"
],
[
"Vale.Poly1305.Math.lemma_reduce128",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat128",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Poly1305.Math.lowerUpper128",
"equation_Vale.Poly1305.Math.lowerUpper128_opaque",
"equation_Vale.Poly1305.Math.lowerUpper192",
"equation_Vale.Poly1305.Math.lowerUpper192_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Poly1305.Spec_s.modp", "int_inversion",
"interpretation_Tm_abs_5db016923445dc04f45f3eecd28369fd",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"token_correspondence_Vale.Def.Opaque_s.make_opaque",
"token_correspondence_Vale.Poly1305.Math.lowerUpper128",
"token_correspondence_Vale.Poly1305.Math.lowerUpper192",
"typing_Vale.Poly1305.Math.lowerUpper128_opaque"
],
0,
"cdfc70c6da11f6115fe8c8e8eb44c3c2"
],
[
"Vale.Poly1305.Math.lemma_add_key",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.Def.Types_s.add_wrap",
"equation_Vale.Def.Words_s.nat128",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Poly1305.Math.lowerUpper128",
"equation_Vale.Poly1305.Math.lowerUpper128_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Poly1305.Spec_s.mod2_128",
"int_inversion", "int_typing",
"interpretation_Tm_abs_8d4a721d9c1a61032b3d240674a76040",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"token_correspondence_Vale.Def.Opaque_s.make_opaque",
"token_correspondence_Vale.Poly1305.Math.lowerUpper128",
"typing_Vale.Def.Types_s.add_wrap",
"typing_Vale.Poly1305.Math.lowerUpper128_opaque"
],
0,
"95d164e06d0f8f47dc1bb3f0d7bb0535"
],
[
"Vale.Poly1305.Math.lemma_lowerUpper128_and",
1,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "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.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat128",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Poly1305.Bitvectors.lowerUpper128u",
"equation_Vale.Poly1305.Math.lowerUpper128",
"equation_Vale.Poly1305.Math.lowerUpper128_opaque",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"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_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_Vale.Def.Opaque_s.make_opaque",
"token_correspondence_Vale.Poly1305.Math.lowerUpper128",
"typing_FStar.UInt.logand"
],
0,
"4b05bb53d19dceef2f3a72802ebe9e4e"
],
[
"Vale.Poly1305.Math.lemma_add_mod128",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Poly1305.Spec_s.mod2_128",
"int_inversion",
"interpretation_Tm_abs_8d4a721d9c1a61032b3d240674a76040",
"projection_inverse_BoxInt_proj_0"
],
0,
"a3d853c6b1802558d617ccdb06ea1862"
]
]
]
Computing file changes ...
