Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Vale.Math.Poly2.Bits.fst.hints
[
"\t��\u0000�\u0003��bg\u0015#�\f�:",
[
[
"Vale.Math.Poly2.Bits.lemma_to_of_uint",
1,
1,
0,
[ "@query" ],
0,
"100ada629178c38f86153e6df748f8a6"
],
[
"Vale.Math.Poly2.Bits.lemma_to_of_uint",
2,
1,
0,
[ "@query" ],
0,
"6549a2640ec17a294c1a3debbb5176ad"
],
[
"Vale.Math.Poly2.Bits.lemma_to_of_uint",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.to_vec.fuel_instrumented", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Math.Poly2.Bits_s.of_uint",
"equation_Vale.Math.Poly2.Bits_s.to_uint",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.UInt.inverse_num_lemma",
"lemma_FStar.UInt.inverse_vec_lemma", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_314f4939256b9382ebd3cc0ef0d441fb",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_d3571ca27e8115116dfd2d473dcbb7c0",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_Vale.Math.Poly2.Bits_s.of_uint",
"typing_Vale.Math.Poly2_s.of_seq",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.to_seq"
],
0,
"4194d076ed27852b188441c40d9f3d8e"
],
[
"Vale.Math.Poly2.Bits.of_nat",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "equation_Prims.nat",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"a56d5ab84ee07a156882a1f00d5dcb4a"
],
[
"Vale.Math.Poly2.Bits.of_uint_",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Equality",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"92199731bdafb0d1559b71d9a7bbed24"
],
[
"Vale.Math.Poly2.Bits.lemma_of_to_vec_zero",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.pos", "equation_Prims.squash",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_fb20ff935b2926a3089fc5c9313431e4",
"typing_Prims.pow2"
],
0,
"a9d4f719bceba6c11d263d8b6981de0c"
],
[
"Vale.Math.Poly2.Bits.lemma_of_to_vec_zero",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.to_vec.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "bool_inversion",
"bool_typing", "equality_tok_Prims.LexTop@tok",
"equation_FStar.BitVector.bv_t", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Prims.squash",
"equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c04cad0e7f59fee7be4217b5e3a7519b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
"typing_FStar.UInt.to_vec", "typing_Prims.pow2",
"well-founded-ordering-on-nat"
],
0,
"12b77d6305fcb4cfd0578c0f33ea5c20"
],
[
"Vale.Math.Poly2.Bits.lemma_of_uint_zero",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.to_vec.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Math.Poly2.Bits.of_uint_",
"equation_Vale.Math.Poly2.Bits_s.of_uint",
"equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_Vale.Math.Poly2.Bits.lemma_of_to_vec_zero",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_314f4939256b9382ebd3cc0ef0d441fb",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec",
"typing_Prims.pow2", "typing_Vale.Math.Poly2_s.of_seq",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.zero"
],
0,
"524e7c125254e601eb4d3201d0ab4a04"
],
[
"Vale.Math.Poly2.Bits.lemma_of_nat_of_uint",
1,
1,
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.squash",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"06a44525b6dd62fbe7248d15b6a6418c"
],
[
"Vale.Math.Poly2.Bits.lemma_of_nat_of_uint",
2,
1,
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.squash",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"cb30adc2ed7228c32d70b3b1f12c4b39"
],
[
"Vale.Math.Poly2.Bits.lemma_of_nat_of_uint",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_correspondence_Vale.Math.Poly2.Bits.of_nat.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Vale.Math.Poly2.Bits.of_nat.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "bool_inversion",
"bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Math.Poly2.Bits.of_uint_",
"equation_Vale.Math.Poly2.Bits_s.of_uint",
"equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"equation_with_fuel_Vale.Math.Poly2.Bits.of_nat.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_one_degree",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.UInt.pow2_values",
"lemma_Vale.Math.Poly2.Bits.lemma_of_to_vec_zero",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_314f4939256b9382ebd3cc0ef0d441fb",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_993ca4d69ac1564038979efdbade2d5a",
"refinement_interpretation_Tm_refine_aaa8221de098e46cfe83e5c3439e6ce8",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"token_correspondence_Vale.Math.Poly2.Bits.of_nat.fuel_instrumented",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec",
"typing_Vale.Math.Poly2.Bits.of_nat",
"typing_Vale.Math.Poly2_s.of_seq", "typing_Vale.Math.Poly2_s.one",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift", "well-founded-ordering-on-nat"
],
0,
"aa56c889e09d10c4040ec2fdf2333e9e"
],
[
"Vale.Math.Poly2.Bits.poly_nat_eq_rec",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"fc2ca2e0802fe9f2ade9a3ff00d07dfc"
],
[
"Vale.Math.Poly2.Bits.lemma_to_nat_rec",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Math.Poly2.Bits.of_nat.fuel_instrumented",
"@fuel_correspondence_Vale.Math.Poly2.Bits.poly_nat_eq_rec.fuel_instrumented",
"@fuel_irrelevance_Vale.Math.Poly2.Bits.of_nat.fuel_instrumented",
"@fuel_irrelevance_Vale.Math.Poly2.Bits.poly_nat_eq_rec.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4", "bool_inversion",
"bool_typing", "equation_Prims.nat",
"equation_with_fuel_Vale.Math.Poly2.Bits.of_nat.fuel_instrumented",
"equation_with_fuel_Vale.Math.Poly2.Bits.poly_nat_eq_rec.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_one_degree",
"int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_aaa8221de098e46cfe83e5c3439e6ce8",
"token_correspondence_Vale.Math.Poly2.Bits.of_nat.fuel_instrumented",
"typing_Vale.Math.Poly2.Bits.of_nat",
"typing_Vale.Math.Poly2.Bits.poly_nat_eq_rec",
"typing_Vale.Math.Poly2_s.one",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.shift", "well-founded-ordering-on-nat"
],
0,
"af89ef5294bf5b050b0b38cf9a85a9ab"
],
[
"Vale.Math.Poly2.Bits.lemma_to_nat",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Prims.nat", "int_inversion",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Math.Poly2.Bits.of_nat",
"typing_Vale.Math.Poly2_s.poly_index"
],
0,
"6504792e7b4af32a9a70a2606ed04583"
],
[
"Vale.Math.Poly2.Bits.of_nat32",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.of_uint_",
"equation_Vale.Math.Poly2.Bits_s.of_uint",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_314f4939256b9382ebd3cc0ef0d441fb",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec",
"typing_Vale.Math.Poly2_s.of_seq"
],
0,
"544be729ea11571ca7d5f6fb19ffbb7e"
],
[
"Vale.Math.Poly2.Bits.lemma_of_nat_of_uint32",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_020ad329ec2b3114865b73caf7eeb86c_0", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.of_nat32",
"equation_Vale.Math.Poly2.Bits.of_uint_",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"806d69b94ef1d1ea6fe8b7e3e28717b4"
],
[
"Vale.Math.Poly2.Bits.of_nat32_zero",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Math.Poly2.Bits.of_nat.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.of_nat32",
"equation_with_fuel_Vale.Math.Poly2.Bits.of_nat.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Vale.Math.Poly2.Bits.of_nat32"
],
0,
"407a42ca2fa3e69aa48627c82ac6e211"
],
[
"Vale.Math.Poly2.Bits.of_nat32_ones",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.of_nat32",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Vale.Math.Poly2.Bits.of_nat32"
],
0,
"ff1b2a4dafab3f5e004728faf0fc0800"
],
[
"Vale.Math.Poly2.Bits.of_nat32_eq",
1,
1,
0,
[ "@query" ],
0,
"038666c55d3b597af137860c1a3c7188"
],
[
"Vale.Math.Poly2.Bits.of_nat32_eq",
2,
1,
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_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.of_nat32",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_FStar.UInt.fits", "typing_Prims.pow2"
],
0,
"f7b69612a9cbbc445250f33857db314c"
],
[
"Vale.Math.Poly2.Bits.of_nat32_xor",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.of_nat32",
"equation_Vale.Math.Poly2.Bits.of_nat32_ones",
"equation_Vale.Math.Poly2.Bits_s.of_uint",
"equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ca87202d8e02d1c00a86cd121980a4f",
"refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e",
"refinement_interpretation_Tm_refine_314f4939256b9382ebd3cc0ef0d441fb",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_637bf9344435626707effe179cd350a8",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec",
"typing_Prims.pow2", "typing_Vale.Def.Types_s.ixor",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.degree",
"typing_Vale.Math.Poly2_s.of_seq",
"typing_Vale.Math.Poly2_s.poly_index"
],
0,
"293aba502ab5911f7018d687a2a8fe38"
],
[
"Vale.Math.Poly2.Bits.of_nat32_and",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.of_nat32",
"equation_Vale.Math.Poly2.Bits.of_nat32_ones",
"equation_Vale.Math.Poly2.Bits_s.of_uint",
"equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ca87202d8e02d1c00a86cd121980a4f",
"refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e",
"refinement_interpretation_Tm_refine_314f4939256b9382ebd3cc0ef0d441fb",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_637bf9344435626707effe179cd350a8",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec",
"typing_Prims.pow2", "typing_Vale.Def.Types_s.iand",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.poly_and", "typing_Vale.Math.Poly2_s.degree",
"typing_Vale.Math.Poly2_s.of_seq",
"typing_Vale.Math.Poly2_s.poly_index"
],
0,
"f77d77c4c8dfe2bedb0b220a293a98d8"
],
[
"Vale.Math.Poly2.Bits.lemma_poly128_extract_nat32s",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "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_Prims.nat",
"equation_Prims.pos", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.of_nat32",
"equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_FStar.UInt.fits", "typing_Prims.pow2",
"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"
],
0,
"3bbca89a32a4fb89135c7d683f837959"
],
[
"Vale.Math.Poly2.Bits.lemma_quad32_of_nat32s",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.of_nat32",
"equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
"equation_Vale.Math.Poly2.Bits_s.of_uint",
"equation_Vale.Math.Poly2.Bits_s.to_quad32_def",
"equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_one_degree",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.inverse_num_lemma",
"lemma_FStar.UInt.inverse_vec_lemma", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "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_314f4939256b9382ebd3cc0ef0d441fb",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_aaa8221de098e46cfe83e5c3439e6ce8",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3571ca27e8115116dfd2d473dcbb7c0",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.slice", "typing_FStar.UInt.fits",
"typing_FStar.UInt.from_vec", "typing_FStar.UInt.to_vec",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.of_seq",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift",
"typing_Vale.Math.Poly2_s.to_seq"
],
0,
"e88b3abee3c79d8e44bcde936fc06c7c"
],
[
"Vale.Math.Poly2.Bits.lemma_quad32_to_nat32s",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.of_nat32",
"equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
"equation_Vale.Math.Poly2.Bits_s.of_uint",
"equation_Vale.Math.Poly2.Bits_s.to_quad32_def",
"equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.inverse_vec_lemma", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "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_314f4939256b9382ebd3cc0ef0d441fb",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3571ca27e8115116dfd2d473dcbb7c0",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Seq.Base.slice", "typing_FStar.UInt.fits",
"typing_FStar.UInt.from_vec", "typing_FStar.UInt.to_vec",
"typing_Prims.pow2", "typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.Bits.poly128_of_nat32s",
"typing_Vale.Math.Poly2_s.add", "typing_Vale.Math.Poly2_s.of_seq",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift",
"typing_Vale.Math.Poly2_s.to_seq"
],
0,
"cc14911490430e999df7ddfdf3d93a50"
],
[
"Vale.Math.Poly2.Bits.lemma_quad32_extract_nat32s",
1,
1,
0,
[
"@query", "equation_Vale.Def.Words_s.nat32",
"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"
],
0,
"09d06fa6cbd41886dacee68c1ca0cde8"
],
[
"Vale.Math.Poly2.Bits.lemma_quad32_double",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.Types.quad32_double_hi",
"equation_Vale.Arch.Types.quad32_double_lo",
"equation_Vale.Def.Words.Four_s.four_to_two_two",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Math.Poly2.Bits_s.of_double32_def",
"equation_Vale.Math.Poly2.Bits_s.to_quad32_def",
"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_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.inverse_vec_lemma", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Math.Poly2.Lemmas.lemma_monomial_degree",
"lemma_Vale.Math.Poly2.lemma_div_degree",
"lemma_Vale.Math.Poly2.lemma_mod_degree",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Vale.Def.Words_s.Mktwo_hi",
"proj_equation_Vale.Def.Words_s.Mktwo_lo",
"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",
"projection_inverse_Vale.Def.Words_s.Mktwo_hi",
"projection_inverse_Vale.Def.Words_s.Mktwo_lo",
"refinement_interpretation_Tm_refine_314f4939256b9382ebd3cc0ef0d441fb",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_d3571ca27e8115116dfd2d473dcbb7c0",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_FStar.UInt.fits",
"typing_FStar.UInt.from_vec", "typing_Prims.pow2",
"typing_Vale.Arch.Types.quad32_double_hi",
"typing_Vale.Arch.Types.quad32_double_lo",
"typing_Vale.Math.Poly2.Bits_s.of_double32_def",
"typing_Vale.Math.Poly2.Bits_s.to_quad32_def",
"typing_Vale.Math.Poly2_s.div", "typing_Vale.Math.Poly2_s.mod",
"typing_Vale.Math.Poly2_s.monomial", "typing_Vale.Math.Poly2_s.mul",
"typing_Vale.Math.Poly2_s.of_seq",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.to_seq"
],
0,
"469469b005ce79516ebdd27e077dad18"
],
[
"Vale.Math.Poly2.Bits.lemma_of_double32_degree",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"data_elim_Vale.Def.Words_s.Mktwo", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Types_s.double32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits_s.of_double32_def",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Vale.Def.Words_s.two",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"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_314f4939256b9382ebd3cc0ef0d441fb",
"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",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.Seq.Base.append", "typing_FStar.UInt.fits",
"typing_FStar.UInt.to_vec", "typing_Prims.pow2",
"typing_Vale.Math.Poly2_s.of_seq"
],
0,
"4696be7d466b42207b7af9391d5bdcfe"
],
[
"Vale.Math.Poly2.Bits.lemma_of_quad32_degree",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"data_elim_Vale.Def.Words_s.Mkfour", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits_s.of_quad32_def",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"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_314f4939256b9382ebd3cc0ef0d441fb",
"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",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.Seq.Base.append", "typing_FStar.UInt.fits",
"typing_FStar.UInt.to_vec", "typing_Prims.pow2",
"typing_Vale.Math.Poly2_s.of_seq"
],
0,
"0e4780f4299f89849f6638477a920dbb"
],
[
"Vale.Math.Poly2.Bits.lemma_to_of_quad32",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_correspondence_Vale.Math.Poly2.Bits.of_nat.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Math.Poly2.Bits.of_nat32_ones",
"equation_Vale.Math.Poly2.Bits_s.of_quad32_def",
"equation_Vale.Math.Poly2.Bits_s.to_quad32_def",
"equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
"equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"equation_with_fuel_Vale.Math.Poly2.Bits.of_nat.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool",
"function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.inverse_num_lemma",
"lemma_FStar.UInt.inverse_vec_lemma", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"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_10fce5557d0593095ff373cff619471e",
"refinement_interpretation_Tm_refine_314f4939256b9382ebd3cc0ef0d441fb",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3571ca27e8115116dfd2d473dcbb7c0",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_FStar.UInt.fits",
"typing_FStar.UInt.from_vec", "typing_FStar.UInt.max_int",
"typing_FStar.UInt.to_vec", "typing_Prims.pow2",
"typing_Vale.Math.Poly2.Bits.of_nat32",
"typing_Vale.Math.Poly2.Bits_s.of_quad32_def",
"typing_Vale.Math.Poly2_s.of_seq",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.to_seq"
],
0,
"fd958c5c1ac76b62ecf6df2bb62e0b83"
],
[
"Vale.Math.Poly2.Bits.lemma_of_to_quad32",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Math.Poly2.Bits_s.of_quad32_def",
"equation_Vale.Math.Poly2.Bits_s.to_quad32_def",
"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_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_slice",
"lemma_FStar.UInt.inverse_vec_lemma", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_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_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_314f4939256b9382ebd3cc0ef0d441fb",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_d3571ca27e8115116dfd2d473dcbb7c0",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_FStar.UInt.fits", "typing_FStar.UInt.from_vec",
"typing_Prims.pow2", "typing_Vale.Math.Poly2.Bits_s.of_quad32_def",
"typing_Vale.Math.Poly2.Bits_s.to_quad32_def",
"typing_Vale.Math.Poly2_s.of_seq",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.to_seq"
],
0,
"0089fdbcedf915bb6a03c69afeb5a268"
],
[
"Vale.Math.Poly2.Bits.lemma_of_to_quad32_mask",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.to_vec.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Math.Poly2.Bits_s.of_quad32_def",
"equation_Vale.Math.Poly2.Bits_s.to_quad32_def",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.inverse_vec_lemma", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"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_314f4939256b9382ebd3cc0ef0d441fb",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_d3571ca27e8115116dfd2d473dcbb7c0",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_FStar.UInt.fits",
"typing_FStar.UInt.from_vec", "typing_Prims.pow2",
"typing_Vale.Math.Poly2.Bits_s.of_quad32_def",
"typing_Vale.Math.Poly2.Bits_s.to_quad32_def",
"typing_Vale.Math.Poly2.mask", "typing_Vale.Math.Poly2_s.of_seq",
"typing_Vale.Math.Poly2_s.poly_index",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.to_seq"
],
0,
"3036c6d817cabf677ff8047e4aa3d4e4"
]
]
]
Computing file changes ...
