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.Bignum.Lemmas.fsti.hints
[
"��\u001c$�M���~~�Im�{",
[
[
"Vale.Bignum.Lemmas.seq_add_c",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_9a3bf8082924c76056d4f6da1c781914_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
"binder_x_cd266facd57b554ccc93fa79ab54a348_1",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"well-founded-ordering-on-nat"
],
0,
"af3bd52ab0ba61d8b44d3d3b47dfc5e7"
],
[
"Vale.Bignum.Lemmas.seq_add_i",
1,
1,
0,
[ "@query" ],
0,
"2be2d83ef6d25f9e1788c272608fb6c9"
],
[
"Vale.Bignum.Lemmas.seq_add",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Vale.Bignum.Lemmas_interpretation_Tm_arrow_c3d5b4c9a207f9ca5ebaa34010b705a3",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat1",
"equation_Vale.Def.Words_s.natN", "int_inversion",
"lemma_FStar.Seq.Base.lemma_init_len",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_cbe95f5a2b690e6ac92cc19518cf1415",
"typing_FStar.Seq.Base.length", "typing_Vale.Def.Words_s.natN"
],
0,
"386d2a90ba8b66b0768e5c6e9068fd68"
],
[
"Vale.Bignum.Lemmas.seq_scale_lo",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"b1963086316c557e48b36356c3c8ce4d"
],
[
"Vale.Bignum.Lemmas.seq_scale_lo",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Bignum.Lemmas_interpretation_Tm_arrow_59eaa5277515751de303a597beb3dd4a",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"lemma_FStar.Seq.Base.lemma_init_len", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_bb4a9973c8f99b57985a81227273102e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"7d35bee3859457cceb6c827085ed479b"
],
[
"Vale.Bignum.Lemmas.seq_scale_hi",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"03d92ce7031e57652de2c52d776ccfca"
],
[
"Vale.Bignum.Lemmas.seq_scale_hi",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Bignum.Lemmas_interpretation_Tm_arrow_59eaa5277515751de303a597beb3dd4a",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "lemma_FStar.Seq.Base.lemma_init_len",
"primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_bb4a9973c8f99b57985a81227273102e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"1a6e3ca5d739580566c45920f965c381"
],
[
"Vale.Bignum.Lemmas.seq_scale",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"866ff1fdeea45500674b887370916503"
],
[
"Vale.Bignum.Lemmas.seq_scale",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"equation_FStar.Pervasives.Native.fst", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"feec78888d31e67ced0cc90be33e2566"
],
[
"Vale.Bignum.Lemmas.lemma_sum_seq_left_right",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
"equation_Prims.squash", "l_and-interp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"de9a405b1ae886f57fc01c0a44c645d0"
],
[
"Vale.Bignum.Lemmas.seq_add_is",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_9a3bf8082924c76056d4f6da1c781914_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
"binder_x_cd266facd57b554ccc93fa79ab54a348_1",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Pervasives.Native.fst", "equation_Prims.l_True",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.l_True", "int_inversion", "int_typing",
"primitive_Prims.op_Equality",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"well-founded-ordering-on-nat"
],
0,
"23c99cc0ba0e97917c0453b9fd3d5073"
],
[
"Vale.Bignum.Lemmas.seq_add_is_norm",
1,
1,
0,
[ "@query" ],
0,
"8fbf4697ac6e1daa925688492cc6e7ea"
],
[
"Vale.Bignum.Lemmas.lemma_seq_add_is_norm",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "eq2-interp",
"equation_Prims.l_and", "equation_Prims.nat",
"equation_Prims.squash", "l_and-interp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"ceb6483c8dcea4a1aa05bcc5f8af1aa1"
],
[
"Vale.Bignum.Lemmas.lemma_seq_add",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.nat", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"dcaba89f8c5861419c0e02d9cfa139a2"
],
[
"Vale.Bignum.Lemmas.lemma_seq_scale_carry",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"1712b18c3c217d4af9b2d9c8b8123871"
],
[
"Vale.Bignum.Lemmas.lemma_seq_scale",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"0fae934350413401fb84893149555e0a"
],
[
"Vale.Bignum.Lemmas.ys_init",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_bb4a9973c8f99b57985a81227273102e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_FStar.Seq.Base.length", "typing_Vale.Def.Words_s.natN"
],
0,
"f844eda120b67ff4ef9024e44caf403b"
],
[
"Vale.Bignum.Lemmas.zs_init",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.natN", "int_inversion",
"primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_bb4a9973c8f99b57985a81227273102e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"07c222bd9d627e4d8d6b902952f4b77e"
],
[
"Vale.Bignum.Lemmas.init_ys",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Seq.Base.length", "typing_Vale.Def.Words_s.natN"
],
0,
"d597a6504656c6e135974a527cc4511a"
],
[
"Vale.Bignum.Lemmas.init_zs",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Seq.Base.length", "typing_Vale.Def.Words_s.natN"
],
0,
"baf9014ce5a48939d724fd64c8917cfa"
],
[
"Vale.Bignum.Lemmas.lemma_scale_add",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Bignum.Lemmas_interpretation_Tm_arrow_9cecc1e6381aab8ddca91566689c42b6",
"eq2-interp", "equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_init_len",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_64c7cdf80f5eb0b5f10cf9506fa04793",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_FStar.Seq.Base.length", "typing_Vale.Def.Words_s.natN"
],
0,
"afbec9e39ceb6f9d08c4dd8d37a3e01d"
]
]
]
Computing file changes ...
