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.Arch.Types.fsti.hints
[
"�?�}w\"��0>��u>3�",
[
[
"Vale.Arch.Types.lemma_nat_to_two32",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "int_typing",
"lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"9d0884a74d37398c4ecd8a9cf385e6ff"
],
[
"Vale.Arch.Types.lemma_equality_check_helper_2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"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_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"9cbec62eb812037ae39ff9f3dead4e37"
],
[
"Vale.Arch.Types.le_bytes_to_nat64_to_bytes",
1,
1,
0,
[ "@query" ],
0,
"b9a06270f0361b52af1063781441b00e"
],
[
"Vale.Arch.Types.le_nat64_to_bytes_to_nat64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_8333610bdce3cc23e40345e003cba619"
],
0,
"aaf7e0dbf866b599bad8ec670af9953e"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_empty",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"7b11fa39832f5af97a6d49a9c5b4f206"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes_one_quad",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"40446a3a8589e3108147e4a0a3ff2951"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes",
1,
1,
0,
[
"@query", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"projection_inverse_BoxInt_proj_0"
],
0,
"d062ea5589fc2af3e68fc51bdc40236c"
],
[
"Vale.Arch.Types.le_seq_quad32_to_bytes_to_seq_quad32",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0"
],
0,
"5a854c6f90b64ecc0b235fb512f070de"
],
[
"Vale.Arch.Types.le_quad32_to_bytes_to_quad32",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc"
],
0,
"8b2b70f7d0cc65ae1a5a110030f6875c"
],
[
"Vale.Arch.Types.seq_to_four_LE_is_seq_to_seq_four_LE",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seqn",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
],
0,
"4d82ac1c99890365db82acd51289a96b"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad_of_singleton",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc"
],
0,
"2131426dad15af9152b313068f4f90d4"
],
[
"Vale.Arch.Types.le_bytes_to_quad32_to_bytes",
1,
1,
0,
[ "@query" ],
0,
"f9c3f323b145f90fc74ffaad05cf2d51"
],
[
"Vale.Arch.Types.be_quad32_to_bytes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_init_len",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_029dc40463b676c106e396144db4f6f0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.four_to_seq_BE"
],
0,
"6922368793f0a0018b7870dee26e770e"
],
[
"Vale.Arch.Types.be_bytes_to_quad32_to_bytes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.Types.be_quad32_to_bytes",
"equation_Vale.Def.Words.Seq_s.seq16",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat8",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"typing_Vale.Arch.Types.be_quad32_to_bytes"
],
0,
"81d7e94345bb70cee3c56cc79d92e3a4"
],
[
"Vale.Arch.Types.slice_commutes_seq_four_to_seq_LE",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "kinding_Vale.Def.Words_s.four@tok",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
"refinement_interpretation_Tm_refine_49d153dee59f77aa2974f04c57015388",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a9d54547d44b88f605af20f5c4cd19dc",
"typing_FStar.Seq.Base.length",
"typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
],
0,
"1f79a52e21d16186b66f593e9795a59f"
],
[
"Vale.Arch.Types.slice_commutes_le_seq_quad32_to_bytes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3234ac1d1198c8b724cbaa98bc293002",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c064a9ee86fe2a45597a2563ec269cee"
],
0,
"ff934260161b603e34507b637256ca39"
],
[
"Vale.Arch.Types.slice_commutes_le_seq_quad32_to_bytes0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c064a9ee86fe2a45597a2563ec269cee"
],
0,
"465114f2937c35d4c4770364232e15a7"
],
[
"Vale.Arch.Types.append_distributes_le_bytes_to_seq_quad32",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Base.op_At_Bar",
"equation_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.Def.Words_s.nat8",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0"
],
0,
"e4e95c43614151e1d9d68c8802ccac48"
]
]
]
Computing file changes ...
