Revision 5b2fbf3c4989a9b0587a00578f69f3041df3f957 authored by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC, committed by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC
1 parent d4ca892
Vale.Poly1305.Math.fst.hints
[
"�1xh��8(�\u0002�[�\u001e(s",
[
[
"Vale.Poly1305.Math.lowerUpper128_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"513c41e1704242b716e43a3069ec0055"
],
[
"Vale.Poly1305.Math.lowerUpper128_reveal",
1,
1,
0,
[ "@query" ],
0,
"7fd504c348b3efd3954dd90f55b0a62e"
],
[
"Vale.Poly1305.Math.lowerUpper192_reveal",
1,
1,
0,
[ "@query" ],
0,
"b80cb3b7ca70e1a3a30d24c4f1fe7c37"
],
[
"Vale.Poly1305.Math.lemma_mul_div_comm",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"b1a11f2e2edfe918d1cf5252e2a6ede1"
],
[
"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_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"e390f15dcd8cc80ce08eea3aecee792f"
],
[
"Vale.Poly1305.Math.lemma_exact_mul",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"c4bbe89f02c4e3f3471356032139f51e"
],
[
"Vale.Poly1305.Math.lemma_exact_mul",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"55582d07bbc274cd0bafb68624da9e50"
],
[
"Vale.Poly1305.Math.lemma_mul_div_sep",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"b142079893a23e50928c6eacd9170f20"
],
[
"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_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"855fb47a12a6404cf807ebe86bd1211c"
],
[
"Vale.Poly1305.Math.swap_add",
1,
1,
0,
[ "@query" ],
0,
"2757fc7c2d060e82192865b8ab9340b1"
],
[
"Vale.Poly1305.Math.lemma_mul_increases",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"084e9b45f665e103ef2dd8659ea548be"
],
[
"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_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"363ceb9bf5952cc87e2289938783d061"
],
[
"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_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"f7e934580e453149f59082ab79f9a21c"
],
[
"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_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"41bf220c14af4669c44b015e15b568d5"
],
[
"Vale.Poly1305.Math.lemma_poly_multiply",
2,
0,
0,
[ "@query", "projection_inverse_BoxInt_proj_0", "true_interp" ],
0,
"9ca316428f796c827a7a545f1d3cecf3"
],
[
"Vale.Poly1305.Math.lemma_poly_reduce",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
"int_inversion", "l_and-interp", "primitive_Prims.op_GreaterThan",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"219c5d983aaebdc22a340ac938f85595"
],
[
"Vale.Poly1305.Math.lemma_poly_reduce",
2,
0,
0,
[ "@query", "projection_inverse_BoxInt_proj_0", "true_interp" ],
0,
"09669b901dde54f9952233052d8ccd2d"
],
[
"Vale.Poly1305.Math.lemma_shr2_nat",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"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", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"7cde5e060d6fdfde1fc9720092d4eb1a"
],
[
"Vale.Poly1305.Math.lemma_shr4_nat",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"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", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"0092c9ffe83abf73d7cdc1742b421cc6"
],
[
"Vale.Poly1305.Math.lemma_and_mod_n_nat",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"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", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"be398fbdcab38289d3a7d89290779b79"
],
[
"Vale.Poly1305.Math.lemma_and_constants_nat",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@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", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_Prims.pow2"
],
0,
"af04a5e224ca919c6743753a51ef6e4c"
],
[
"Vale.Poly1305.Math.lemma_clear_lower_2_nat",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"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", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_e49d79feeb1e96b29b0f01b06f8dac23",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.udiv", "typing_Prims.pow2",
"typing_Vale.Def.Types_s.iand"
],
0,
"8b5abd325d22162683b178b4bdc92a8e"
],
[
"Vale.Poly1305.Math.lemma_poly_constants_nat",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"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", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"5b2fa0984ebbedd2b501a6c8b4e8e652"
],
[
"Vale.Poly1305.Math.lemma_and_commutes_nat",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "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_2897f455bd1a2e7bd7f8f1aa6ce63472",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Prims.pow2"
],
0,
"a17628c52201c358cdae416cb3895768"
],
[
"Vale.Poly1305.Math.lemma_poly_bits64",
1,
0,
0,
[ "@query" ],
0,
"a40b949a4421af90fbcaad2f48a9dc3b"
],
[
"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,
"87106f76c77f62e32cbba4009af1f88f"
],
[
"Vale.Poly1305.Math.lemma_bytes_shift_power2",
1,
0,
0,
[ "@query" ],
0,
"c47aedb0e7bcf1b7bb6d96b27fe3b79c"
],
[
"Vale.Poly1305.Math.lemma_bytes_shift_power2",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "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_2897f455bd1a2e7bd7f8f1aa6ce63472",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Prims.pow2"
],
0,
"73706e2946d7f7203b8f643496824188"
],
[
"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_f13070840248fced9d9d60d77bdae3ec"
],
0,
"ab8f6526585beefe60adde2e878c4c47"
],
[
"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",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "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_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"f3b31ee3c6035b521e0df764c73030d8"
],
[
"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",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "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_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"a4f89e73b8f1cf41d2c4b3a430e8006a"
],
[
"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",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "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_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"7e14fd99c36143801dc3e5991a5fae0c"
],
[
"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",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "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_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"3acf960dcb485174feaa80e605ff4f20"
],
[
"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",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "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_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"ec280c0dabe38aa74aa4f4224116c808"
],
[
"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",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "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_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"8834e018be4d99faa6ca82cb96898367"
],
[
"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",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "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_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"34707c8f2486db18ff14645bea2cc2fb"
],
[
"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",
"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", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
"typing_FStar.BitVector.logand_vec", "typing_FStar.UInt.to_vec"
],
0,
"1b483cced931a70e6cf6e1f2df5ff85b"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod0",
3,
1,
0,
[ "@query" ],
0,
"4d02babf86539fb87fff5898e0ed07be"
],
[
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"true_interp", "typing_FStar.BitVector.logand_vec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec"
],
0,
"ea4f4f0f08447a44db11abb0814c8272"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod1",
3,
1,
0,
[ "@query" ],
0,
"874d641cf1fbe406cad158b67fdae585"
],
[
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"true_interp", "typing_FStar.BitVector.logand_vec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec"
],
0,
"7a6185bea612567207cf3be72032d101"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod2",
3,
1,
0,
[ "@query" ],
0,
"3e24d3cf92bb99e9ef6411a23cb712f6"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod3",
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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"true_interp", "typing_FStar.BitVector.logand_vec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec"
],
0,
"e5b1f1ec5c09e511b9d33f4792c9ba1e"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod3",
3,
1,
0,
[ "@query" ],
0,
"c52ae74396974ef7bd4cb92b08b0a7cc"
],
[
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"true_interp", "typing_FStar.BitVector.logand_vec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec"
],
0,
"2278fef16ee52205e975f9fa054bc978"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod4",
3,
1,
0,
[ "@query" ],
0,
"91d384255c8b8163fb0a91229e1cd31f"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod5",
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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"true_interp", "typing_FStar.BitVector.logand_vec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec"
],
0,
"c48b93e64ac5a1e6a97b765dab1625a1"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod5",
3,
1,
0,
[ "@query" ],
0,
"709f19f2d7640e095cc6c05e27dd64ff"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod6",
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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"true_interp", "typing_FStar.BitVector.logand_vec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec"
],
0,
"b6d5d960af91dc72babe0d6bba02163e"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod6",
3,
1,
0,
[ "@query" ],
0,
"c296760eca8c1bcb82450743081eb33e"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod7",
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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"true_interp", "typing_FStar.BitVector.logand_vec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec"
],
0,
"0974d06b6ddc2184cb18f2c168170832"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod7",
3,
1,
0,
[ "@query" ],
0,
"ebeba7cd5f56f553477ea9f1ef7ecf5c"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"int_inversion", "int_typing", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Vale.Def.Types_s.ishl"
],
0,
"37fc054c331e0ec74fe3f77443e265f1"
],
[
"Vale.Poly1305.Math.lemma_bytes_and_mod",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"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_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.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"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_2897f455bd1a2e7bd7f8f1aa6ce63472",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"typing_FStar.BitVector.zero_vec", "typing_FStar.UInt.fits",
"typing_Prims.pow2"
],
0,
"8047c0ed352a9c5066d5f6e81493ddb1"
],
[
"Vale.Poly1305.Math.lemma_mod_factors",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"true_interp"
],
0,
"85f50fe2843e5c3b57ad5533b188e003"
],
[
"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_774ba3f728d91ead8ef40be66c9802e5",
"unit_inversion", "unit_typing"
],
0,
"4a8a4cb1919d41d00b9f4c97596605c1"
],
[
"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_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"22bc38584a011f230837060c7749f42c"
],
[
"Vale.Poly1305.Math.lemma_mod_power2_lo",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "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_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"611439c2a46fd7cccc51bbc471c49f31"
],
[
"Vale.Poly1305.Math.lemma_mod_power2_lo",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Poly1305.Math.lowerUpper128_def",
"function_token_typing_Vale.Poly1305.Math.lowerUpper128_def",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Poly1305.Math.lowerUpper128",
"typing_Prims.pow2"
],
0,
"dee836e213eae0e8c413b239959170da"
],
[
"Vale.Poly1305.Math.lemma_power2_add64",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"01672226572420e0ddb15bde2080f1ec"
],
[
"Vale.Poly1305.Math.lemma_power2_add64",
2,
0,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"8052372362475ceca7cc975f3d8c5169"
],
[
"Vale.Poly1305.Math.lemma_part_bound1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"true_interp"
],
0,
"1d7e354e4646655d1c8f44d1e6d5e0a7"
],
[
"Vale.Poly1305.Math.lemma_lt_le_trans",
1,
0,
0,
[ "@query" ],
0,
"ae3baa99b9d4c3465275dc5cff7c4d02"
],
[
"Vale.Poly1305.Math.lemma_part_bound2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"37dfbe7a98240e91c7a66a932ac0eea5"
],
[
"Vale.Poly1305.Math.lemma_truncate_middle",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"d6f99ca379e0976629a780aae30fbff6"
],
[
"Vale.Poly1305.Math.lemma_mod_breakdown",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"true_interp"
],
0,
"8b5cc8b804f68529721e623ed2df1551"
],
[
"Vale.Poly1305.Math.lemma_mod_breakdown",
2,
0,
0,
[ "@query" ],
0,
"0c8ac1b5cb7c380dab7069dd23a4afe5"
],
[
"Vale.Poly1305.Math.lemma_mod_hi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"int_inversion", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"0e10314753e845a8014bab54f6249d67"
],
[
"Vale.Poly1305.Math.lemma_mod_hi",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Poly1305.Math.lowerUpper128_def",
"function_token_typing_Vale.Poly1305.Math.lowerUpper128",
"function_token_typing_Vale.Poly1305.Math.lowerUpper128_def",
"int_inversion", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Poly1305.Math.lowerUpper128",
"token_correspondence_Vale.Poly1305.Math.lowerUpper128_def"
],
0,
"4b94e6aafa995375ef147ad74d274002"
],
[
"Vale.Poly1305.Math.lemma_poly_demod",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"ed5009b4c2d6b9e9ff12e934535f8eb9"
],
[
"Vale.Poly1305.Math.lemma_poly_demod",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"130d16b847ec2338db3b956a7ab57e56"
],
[
"Vale.Poly1305.Math.lemma_reduce128",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "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_def",
"equation_Vale.Poly1305.Math.lowerUpper192_def",
"function_token_typing_Vale.Poly1305.Math.lowerUpper128",
"function_token_typing_Vale.Poly1305.Math.lowerUpper192",
"function_token_typing_Vale.Poly1305.Spec_s.mod2_128",
"function_token_typing_Vale.Poly1305.Spec_s.modp", "int_inversion",
"interpretation_Tm_abs_05f13c916e3cc747d987f540ed36f6e0",
"interpretation_Tm_abs_9e8a6b1f613542ebb1af5a387aec2340",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Poly1305.Math.lowerUpper128_def",
"token_correspondence_Vale.Poly1305.Math.lowerUpper192_def",
"typing_Vale.Poly1305.Math.lowerUpper128"
],
0,
"1a1885278d2ab6da8ec6fe7a672c0770"
],
[
"Vale.Poly1305.Math.lemma_add_key",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "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_def",
"function_token_typing_Vale.Poly1305.Math.lowerUpper128",
"function_token_typing_Vale.Poly1305.Spec_s.mod2_128",
"int_inversion", "int_typing",
"interpretation_Tm_abs_9e8a6b1f613542ebb1af5a387aec2340",
"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_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Poly1305.Math.lowerUpper128_def",
"typing_Vale.Def.Types_s.add_wrap",
"typing_Vale.Poly1305.Math.lowerUpper128"
],
0,
"58bb26d3b8f4d44270fa1e11c1ddd244"
],
[
"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",
"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_def",
"function_token_typing_Vale.Poly1305.Math.lowerUpper128",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_Vale.Poly1305.Math.lowerUpper128_def",
"typing_FStar.UInt.fits", "typing_FStar.UInt.logand"
],
0,
"6d1aceb13f3501cca19d0cfd7202ca59"
],
[
"Vale.Poly1305.Math.lemma_add_mod128",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"function_token_typing_Vale.Poly1305.Spec_s.mod2_128",
"int_inversion",
"interpretation_Tm_abs_9e8a6b1f613542ebb1af5a387aec2340",
"projection_inverse_BoxInt_proj_0"
],
0,
"4cfb4a343a442b0475a81f095498800a"
]
]
]
Computing file changes ...
