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
Spec.Frodo.Lemmas.fsti.hints
[
"bZ#���=�\"\u0000�H�ܪB",
[
[
"Spec.Frodo.Lemmas.lemma_frodo_sample2",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U16@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
"primitive_Prims.op_Modulus", "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_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_a636b6491af501737c1eb06142217342",
"refinement_interpretation_Tm_refine_f0b074bae5549342862ae97eac81867b",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U16@tok"
],
0,
"bbdefe360b75e98a7e2d2983d5c09191"
],
[
"Spec.Frodo.Lemmas.modulo_pow2_u16",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "lemma_Lib.IntTypes.v_mk_int",
"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_6f7719d2e9422e645682674727002c0b",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U16@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"07dd4becc2331206182a81d3d3e62935"
],
[
"Spec.Frodo.Lemmas.modulo_pow2_u32",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "lemma_Lib.IntTypes.v_mk_int",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0c1a7fcd8c5d6302f88f430256334c0e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"dbd30e5aceba330e8bfac489575e2180"
],
[
"Spec.Frodo.Lemmas.modulo_pow2_u64",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "lemma_Lib.IntTypes.v_mk_int",
"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_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_98174f2b2ba7d34bf74a02c913828046",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"798fe0b067529efff5224cd39480858a"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...