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
Lib.CurveLemmas.fst.hints
[
"~\u0002���v\u0017��jYu~�˒",
[
[
"Lib.CurveLemmas.eq_mask_logand_lemma",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"1d9a9f0434acbaa228af469e0b3c44d2"
],
[
"Lib.CurveLemmas.gte_mask_logand_lemma",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
"projection_inverse_BoxInt_proj_0"
],
0,
"185dc5e5b43f62094323ac52773ff6da"
],
[
"Lib.CurveLemmas.eq_mask_lemma",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"59200b9371fc17640820454006410a13"
],
[
"Lib.CurveLemmas.logand_lemma",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
"projection_inverse_BoxInt_proj_0"
],
0,
"ca119c7d58faebd2e3403d28a7928ac6"
],
[
"Lib.CurveLemmas.logor_disjoint64",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"refinement_interpretation_Tm_refine_5559606f09094ead7ac717cf41221ef7",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"11e7dd5db874bd6e4627a9a1907804e7"
],
[
"Lib.CurveLemmas.lemma_nat_from_uints64_le_4",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"722a9088f6790901b34c8b5e122a4aa8"
],
[
"Lib.CurveLemmas.lemma_nat_from_uints64_le_4",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"29cc37032f7ba32472fdb2589cc2e512"
],
[
"Lib.CurveLemmas.logxor_lemma",
1,
2,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"0c9f7d65c5fcefeab76c1a09310d2e6a"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...