Revision 027cee49342e5e1ac0ccf4ca6e4b5b868e70a0a2 authored by Aseem Rastogi on 22 March 2020, 07:14:03 UTC, committed by Aseem Rastogi on 22 March 2020, 07:14:03 UTC
1 parent df0c85e
Vale.Math.Poly2.Words.fst.hints
[
"g�~�٨��k缪\u001f߆�",
[
[
"Vale.Math.Poly2.Words.lemma_quad32_zero",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
"function_token_typing_Vale.Math.Poly2.Bits.of_nat32_zero",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
"int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_disEquality", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_4337ec945cb4c294d0e8ff2d420e64d7",
"refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303",
"typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift", "typing_Vale.Math.Poly2_s.zero"
],
0,
"3bdb2fc76d2283be4c8dacaad32a066d"
],
[
"Vale.Math.Poly2.Words.lemma_quad32_ones",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
"function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones",
"int_inversion", "int_typing",
"lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.ones", "typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift"
],
0,
"f8068de95e7faf4d383dc72fb5cb617d"
],
[
"Vale.Math.Poly2.Words.lemma_add128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_Vale.Def.Types_s.quad32_xor_def",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
"function_token_typing_Vale.Def.Types_s.quad32_xor", "int_inversion",
"int_typing", "lemma_Vale.Math.Poly2.lemma_add_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"token_correspondence_Vale.Def.Types_s.quad32_xor_def",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.Bits.poly128_of_poly32s",
"typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift"
],
0,
"2ca631398a416da353696a9805ae1f95"
],
[
"Vale.Math.Poly2.Words.lemma_add_quad32",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"lemma_Vale.Math.Poly2.Bits.lemma_of_quad32_degree",
"lemma_Vale.Math.Poly2.Bits.lemma_to_of_quad32",
"lemma_Vale.Math.Poly2.lemma_add_degree",
"typing_Vale.Math.Poly2.Bits_s.of_quad32"
],
0,
"87d9d25616aae10d37e1a47e478221fe"
],
[
"Vale.Math.Poly2.Words.lemma_and128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"equation_Vale.Math.Poly2.Bits.poly128_of_poly32s", "int_inversion",
"int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.Bits.poly128_of_poly32s",
"typing_Vale.Math.Poly2.poly_and", "typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift"
],
0,
"35783e810f642322420c47dd5bc2598d"
],
[
"Vale.Math.Poly2.Words.lemma_and_quad32",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"lemma_Vale.Math.Poly2.Bits.lemma_of_quad32_degree",
"lemma_Vale.Math.Poly2.Bits.lemma_to_of_quad32",
"lemma_Vale.Math.Poly2.Lemmas.lemma_and_degree",
"typing_Vale.Math.Poly2.Bits_s.of_quad32"
],
0,
"5ef6c46c5789ddccbed7ad9483fd2d6b"
],
[
"Vale.Math.Poly2.Words.lemma_quad32_double_shift",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
"function_token_typing_Vale.Math.Poly2.Bits.of_nat32_zero",
"int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_4337ec945cb4c294d0e8ff2d420e64d7",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"typing_Vale.Math.Poly2.mask", "typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift", "typing_Vale.Math.Poly2_s.zero"
],
0,
"f8cd83b9a031bdba8340840d2f703cff"
],
[
"Vale.Math.Poly2.Words.lemma_quad32_double_swap",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
"bool_typing", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
"equation_Vale.Math.Poly2.swap", "int_inversion", "int_typing",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"typing_Vale.Math.Poly2.mask", "typing_Vale.Math.Poly2.swap",
"typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift"
],
0,
"5eacaf85f1d0819cc9ac880535776111"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...