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.SHA.SHA_helpers.fsti.hints
[
"���Vi�\u000bo\u001d�k�9�?j",
[
[
"Vale.SHA.SHA_helpers.bytes_blocks",
1,
0,
0,
[
"@query", "equation_Vale.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"projection_inverse_BoxInt_proj_0"
],
0,
"d226c7a257ae5fab35054c0ac5b90d60"
],
[
"Vale.SHA.SHA_helpers.repeat_range_vale",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6c6633917f79a67f4eaac4ed70320fc6"
],
0,
"5da5a1ac4de96d9f5153a6053a787c95"
],
[
"Vale.SHA.SHA_helpers.lemma_repeat_range_0_vale",
1,
0,
0,
[ "@query" ],
0,
"45cbd381fba3029f424ea70f05a08c9c"
],
[
"Vale.SHA.SHA_helpers.update_multi_opaque_vale",
1,
0,
0,
[
"@query", "equation_Vale.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"faa85440712eddf6686d6d66f0f9a1a0"
],
[
"Vale.SHA.SHA_helpers.make_hash",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.SHA.SHA_helpers.hash256",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
],
0,
"8f315afdc66904101ab85b4863c3603d"
],
[
"Vale.SHA.SHA_helpers.make_ordered_hash",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.SHA.SHA_helpers.hash256",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
],
0,
"0e7a6730d9724af92d48dbd6089e0b53"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_rnds2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.SHA.SHA_helpers.counter",
"l_and-interp", "primitive_Prims.op_LessThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b023f92fdc85789979f7b1f8b2bc8a31",
"typing_Vale.SHA.SHA_helpers.k"
],
0,
"1e3f0882619346fa5421f50ec384c7f8"
],
[
"Vale.SHA.SHA_helpers.ws_quad32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.SHA.SHA_helpers.counter",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"fc2770ba63a7f2090bd7b63ff6282e70"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_msg1",
1,
0,
0,
[ "@query" ],
0,
"2ca15cb76217125135f2c12b361b25dc"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_msg2",
1,
0,
0,
[ "@query" ],
0,
"f4a5ce4a15f28900c08ba5db08644ef1"
],
[
"Vale.SHA.SHA_helpers.k_reqs",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_07420f653b2652e2852306d7d9338f6d",
"refinement_interpretation_Tm_refine_b023f92fdc85789979f7b1f8b2bc8a31",
"typing_Vale.SHA.SHA_helpers.k"
],
0,
"599b0a87841acec102e1041f7fb56311"
],
[
"Vale.SHA.SHA_helpers.quads_to_block",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.SHA.SHA_helpers_interpretation_Tm_arrow_ccb4d7c44e4c8e6e26bfd3461142de18",
"equation_Prims.nat",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"function_token_typing_Vale.SHA.SHA_helpers.word", "int_typing",
"lemma_FStar.Seq.Base.lemma_init_len", "primitive_Prims.op_LessThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"d8a2e72b14f4a9793fb1573567a575e1"
],
[
"Vale.SHA.SHA_helpers.lemma_quads_to_block",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2b5485809f7439c44769748bbc713872",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"638557798f38ad46e20ec967b523ba80"
],
[
"Vale.SHA.SHA_helpers.update_multi_quads",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_0",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.split", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_e7547d4e3bc4c2d7d07f503e85b9b717",
"typing_FStar.Seq.Base.length", "well-founded-ordering-on-nat"
],
0,
"4585e617c93af7e7f9de9c2746814b74"
],
[
"Vale.SHA.SHA_helpers.lemma_update_multi_quads",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing", "equation_Prims.nat", "equation_Prims.squash",
"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",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8117376fa751a9089be3b927d5831062",
"typing_FStar.Seq.Base.length"
],
0,
"513d698d63e1db1fd6a98d6eb5d89d94"
],
[
"Vale.SHA.SHA_helpers.le_bytes_to_hash",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.SHA.SHA_helpers_interpretation_Tm_arrow_1ce1f604e3636d4aefb8e634e669999e",
"equation_Prims.nat",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"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_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.SHA.SHA_helpers.word", "int_typing",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_init_len",
"primitive_Prims.op_disEquality", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_35a56cb7608bf4720ad612ec0cf582b4",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Tm_abs_25aa5013196fbd0a35c92458222d0340",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
],
0,
"16773e9b691dc8a719102ca95b04cc85"
],
[
"Vale.SHA.SHA_helpers.lemma_hash_to_bytes",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"43f6fca9a60ec96f691fe69b2e02da0c"
],
[
"Vale.SHA.SHA_helpers.lemma_update_multi_opaque_vale_is_update_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
"equation_Vale.SHA.SHA_helpers.block_length",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"bd1f99e06279158529f2c660035c5ca7"
]
]
]
Computing file changes ...
