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.AES.OptPublic.fst.hints
[
"�/b������M\u000eԟx��",
[
[
"Vale.AES.OptPublic.g_power",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"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,
"18478024d1aacde91a638c78a43a2da1"
],
[
"Vale.AES.OptPublic.hkeys_reqs_pub",
1,
1,
0,
[ "@query" ],
0,
"b582574ec341c198b9641ca6253610d8"
],
[
"Vale.AES.OptPublic.get_hkeys_reqs",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.OptPublic.g_power.fuel_instrumented",
"@query", "b2t_def", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil", "disc_equation_Prims.Cons",
"eq2-interp", "equation_FStar.List.Tot.Base.tail",
"equation_FStar.List.Tot.Base.tl",
"equation_FStar.Seq.Properties.cons",
"equation_FStar.Seq.Properties.head",
"equation_FStar.Seq.Properties.tail", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.AES.GF128.shift_key_1",
"equation_Vale.AES.GF128_s.gf128_modulus_low_terms",
"equation_Vale.AES.OptPublic.gf128_power",
"equation_Vale.AES.OptPublic.hkeys_reqs_pub",
"equation_Vale.AES.OptPublic.shift_gf128_key_1",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Properties.slice_slice",
"lemma_Vale.Math.Poly2.Lemmas.lemma_mask_degree",
"lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
"lemma_Vale.Math.Poly2.lemma_add_degree",
"primitive_Prims.op_Addition",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
"refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4a89f9b1422f729b7c6ab716d67c42b3",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.empty",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.head",
"typing_FStar.Seq.Properties.seq_of_list",
"typing_Vale.AES.GF128_s.gf128_modulus_low_terms",
"typing_Vale.AES.OptPublic.g_power",
"typing_Vale.AES.OptPublic.gf128_power",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Math.Poly2.Bits_s.of_quad32",
"typing_Vale.Math.Poly2.Bits_s.to_quad32",
"typing_Vale.Math.Poly2.mask", "typing_Vale.Math.Poly2_s.add",
"typing_Vale.Math.Poly2_s.monomial",
"typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift",
"typing_Vale.Math.Poly2_s.zero"
],
0,
"d752818cc26747ce0e75613288df3123"
],
[
"Vale.AES.OptPublic.lemma_of_quad32_inj",
1,
0,
0,
[ "@query" ],
0,
"dc47dd29c5030205d018e76841bf5975"
],
[
"Vale.AES.OptPublic.get_hkeys_reqs_injective",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.nat",
"equation_Vale.AES.OptPublic.hkeys_reqs_pub",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55"
],
0,
"4e704ca4ad7b415660a6fb38d5788d5d"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...