Revision 182960367fc096d55cd17a4f5b700fd09c25ecf3 authored by Jay Bosamiya on 04 June 2019, 23:14:04 UTC, committed by Jay Bosamiya on 04 June 2019, 23:14:04 UTC
1 parent ce16bcb
Spec.SHA1.fst.hints
[
"E����{nGd\b^\u001f�ǩ�",
[
[
"Spec.SHA1.h0",
1,
8,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"data_elim_Prims.Cons", "data_typing_intro_Prims.Nil@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.SHA1.init_as_list",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_FStar.UInt32.t", "int_inversion",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.List.Tot.Base.length", "typing_Spec.SHA1.init_as_list"
],
0,
"052f4de5622dfd8473e4eb4503df08c0"
],
[
"Spec.SHA1.rotl",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_42cf8cb5aa2c0a99d2c5dc29ce6c326a",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.UInt32.v"
],
0,
"c5d09985d5ce2bd6d6a8889db59fd2b9"
],
[
"Spec.SHA1.w'",
1,
2,
1,
[
"@query", "equation_Spec.Hash.Definitions.block_word_length",
"projection_inverse_BoxInt_proj_0"
],
0,
"4abfb2accd384d3d5d99f1d9fe3bff6c"
],
[
"Spec.SHA1.w'",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_71b3f16ba9f0eb3066592b75d308ba96_1",
"binder_x_92de1847185cc5f1b59973b08596edb8_0",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.word",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2bdf76a122980851865ae1b103c3fe84",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"well-founded-ordering-on-nat"
],
0,
"3b757132f1a611818edc92cce557575a"
],
[
"Spec.SHA1.w",
1,
2,
1,
[
"@query", "equation_Spec.Hash.Definitions.block_word_length",
"projection_inverse_BoxInt_proj_0"
],
0,
"e599a8ea0fd5539decb52070e906cc16"
],
[
"Spec.SHA1.w",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_fcf81b40a69dfd9b96fd4983a9c5ead3"
],
0,
"9bdd98df84776f4db0b96e4efbe95d7c"
],
[
"Spec.SHA1.compute_w_post",
1,
2,
1,
[
"@query", "equation_Spec.Hash.Definitions.block_word_length",
"projection_inverse_BoxInt_proj_0"
],
0,
"c01f18d2dcb14639cfe6114cade0a413"
],
[
"Spec.SHA1.compute_w_post",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Seq.Properties.lseq",
"equation_Spec.Hash.Definitions.word",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
],
0,
"99b329240807f09f9cfa20fb703a7801"
],
[
"Spec.SHA1.compute_w_post_intro",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.squash",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.word",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"unit_typing"
],
0,
"e90239af322458c46a8431aaa6ad8e34"
],
[
"Spec.SHA1.compute_w_post_intro",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.nat",
"equation_Prims.squash", "equation_Spec.Hash.Definitions.word",
"equation_Spec.SHA1.compute_w_post", "int_inversion",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"e13e8a49bda6bee9e0a5aee83d420323"
],
[
"Spec.SHA1.compute_w_n'",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_word_length",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2bdf76a122980851865ae1b103c3fe84"
],
0,
"0e571b21ab8ded169f2e474efeb9236d"
],
[
"Spec.SHA1.compute_w_n'",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.SHA1.w_.fuel_instrumented",
"@fuel_irrelevance_Spec.SHA1.w_.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_with_fuel_Spec.SHA1.w_.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1c2959a863d18db568c6cfda54a658ae",
"refinement_interpretation_Tm_refine_2bdf76a122980851865ae1b103c3fe84",
"refinement_interpretation_Tm_refine_30faf32543af4bd46b1cf80de60a349b",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_bd242cf70fe5f9f66caae014a6ffba7b",
"refinement_interpretation_Tm_refine_d605b54d727cee55bcdcecc93b6e5517"
],
0,
"be97b5a42d6f8f117efdedffec387b8d"
],
[
"Spec.SHA1.compute_w_n",
1,
2,
1,
[
"@query", "equation_Spec.Hash.Definitions.block_word_length",
"projection_inverse_BoxInt_proj_0"
],
0,
"4d10f9e7799a400b7a7c2272a93cd1c9"
],
[
"Spec.SHA1.compute_w_n",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.SHA1.compute_w_post",
"refinement_interpretation_Tm_refine_2bdf76a122980851865ae1b103c3fe84",
"refinement_interpretation_Tm_refine_50f3dcb312c61cacd85d8a19ef243108",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
],
0,
"b11079aa57b9a8a406d1395488201c46"
],
[
"Spec.SHA1.compute_w_next",
1,
2,
1,
[
"@query", "equation_Spec.Hash.Definitions.block_word_length",
"projection_inverse_BoxInt_proj_0"
],
0,
"dec339f423b9918ff51620b46f0ab074"
],
[
"Spec.SHA1.compute_w_next",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Seq.Properties.lseq",
"equation_FStar.Seq.Properties.snoc", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.word",
"equation_Spec.SHA1.compute_w_post",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_2bdf76a122980851865ae1b103c3fe84",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.create", "typing_Spec.Hash.Definitions.word",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"5d78427b374c37def5d68cc06b9e88d0"
],
[
"Spec.SHA1.compute_w",
1,
2,
1,
[
"@query", "equation_Spec.Hash.Definitions.block_word_length",
"projection_inverse_BoxInt_proj_0"
],
0,
"31d1a85d3ef74bcb88b3c6f324c66cd2"
],
[
"Spec.SHA1.compute_w",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_16fb378db07c2fbac763a58283e8b1c7_2",
"binder_x_e22ba7a032a73f6d0678d3d186686631_1",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.SHA1.compute_w_post",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"well-founded-ordering-on-nat"
],
0,
"59178629c2caf59dfa6a8584bd88e30a"
],
[
"Spec.SHA1.word_block",
1,
2,
1,
[
"@query", "equation_Spec.Hash.Definitions.block_word_length",
"projection_inverse_BoxInt_proj_0"
],
0,
"661f44391dd4599f62d3434da4666bd6"
],
[
"Spec.SHA1.step3_body'_aux",
1,
2,
1,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"3f39915a131ba1dab1f68b4fac3bae41"
],
[
"Spec.SHA1.step3_body'_aux",
2,
8,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.words_state",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_25f99d2dc55047f2115a34e006469f3c",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.List.Tot.Base.length",
"typing_Spec.Hash.Definitions.word",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"e1f1372c061e41e9cdb56268b660984b"
],
[
"Spec.SHA1.step3_body_w_t",
1,
2,
1,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"61f7810688be498ec233b6c297bc74e6"
],
[
"Spec.SHA1.step3_body",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "equation_Spec.SHA1.w",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_98e90dd01a9230213bddcf71cc57f735",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"96ce71e8b147f546f303dcaac0c6d679"
],
[
"Spec.SHA1.index_compute_w",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.SHA1.compute_w_post",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_98e90dd01a9230213bddcf71cc57f735",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_dbaff4a0cfbdc2edd79e07677202bbe0"
],
0,
"13fd123b449890040860f987b5cc90ec"
],
[
"Spec.SHA1.step3_aux",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.SHA1.compute_w_post",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.empty", "typing_Spec.Hash.Definitions.word",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"96f43fa1b5370abde3b64197d0f84b33"
],
[
"Spec.SHA1.step4_aux",
1,
8,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"data_typing_intro_Prims.Nil@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.words_state",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.List.Tot.Base.length",
"typing_Spec.Hash.Definitions.word", "typing_Spec.SHA1.step3",
"typing_tok_Spec.Hash.Definitions.SHA1@tok"
],
0,
"cf7283d125363846fb57f3463868054e"
],
[
"Spec.SHA1.words_of_bytes_block",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_aea0761a74a760cff1f8062a9ec0daa3"
],
0,
"993c029a74ef9cabc5571b55f9a12057"
],
[
"Spec.SHA1.update",
1,
2,
1,
[ "@query" ],
0,
"6197316cae6c61d6acb8e0c74db2c558"
]
]
]
Computing file changes ...
