Revision 724d1045f60f13d79df1afc5190955afdfa73ec1 authored by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC, committed by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC
Co-authored-by: @protz
1 parent ca37fbf
Vale.SHA.SHA_helpers.fsti.hints
[
"��/�:Z�\u0010Y'������",
[
[
"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,
"982caf72ef1897cee3b679518fc46133"
],
[
"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,
"ec717e0c6b8457fd007c55d0b2249a3a"
],
[
"Vale.SHA.SHA_helpers.lemma_repeat_range_0_vale",
1,
0,
0,
[ "@query" ],
0,
"f5b5f85cc64e86b18e5cb00e1d4f5ab7"
],
[
"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,
"62c2eb0b8f90802ab60a4007e71a492f"
],
[
"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,
"f4b21fa7f715d1499318a11ab0dce278"
],
[
"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,
"d0b64f4b0676d793e35d0d89bbf5130f"
],
[
"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,
"214481a9670e27e98bf56b93e3ec1e71"
],
[
"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,
"f87865ec2a615e2280f32fc676c799c2"
],
[
"Vale.SHA.SHA_helpers.ws_partial_reveal",
1,
0,
0,
[ "@query" ],
0,
"d99bc0e8e2562d00b860c4774e6f434e"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_msg1",
1,
0,
0,
[ "@query" ],
0,
"5d2277aa547d670794bc186d5249c9e3"
],
[
"Vale.SHA.SHA_helpers.lemma_sha256_msg2",
1,
0,
0,
[ "@query" ],
0,
"d1f6078e944b26221d535105100e3daf"
],
[
"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,
"8f13321c562d45d62d2cdd2660e553df"
],
[
"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,
"48cb0bf2a9df6a7a611210a3aa129836"
],
[
"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,
"bce435a6083c88ff1b9397b076849fe0"
],
[
"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,
"2fb6d2b39dfae5c68f13e83787106f3b"
],
[
"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,
"cb44039e174330a19b7297cc29de76b5"
],
[
"Vale.SHA.SHA_helpers.le_bytes_to_hash",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_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_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,
"67ee94bfec7a677b31c0b1546eae4339"
],
[
"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,
"a400e652e7edaaf9827673d1ce481381"
],
[
"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,
"a78e7457625c8b7ba131d0aa23080ace"
]
]
]
Computing file changes ...
