https://github.com/project-everest/hacl-star
Tip revision: 4d41d4ec3acc48721e2966ccf1a9a9abdaadc719 authored by Chris Hawblitzel on 14 March 2019, 05:53:02 UTC
Disable X64.Leakage_Ins* to enable merge
Disable X64.Leakage_Ins* to enable merge
Tip revision: 4d41d4e
Hacl.Hash.Core.MD5.fst.hints
[
"��Q�(�i�4ސn��`",
[
[
"Hacl.Hash.Core.MD5._h0",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperStack.is_eternal_color",
"lemma_FStar.Monotonic.HyperHeap.lemma_root_has_color_zero",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2fbd657fe85bcb2423f9c7e5f9b3bcb5",
"typing_FStar.Monotonic.HyperHeap.root"
],
0,
"05554c0ada09ddf430f3f2e34d0b324a"
],
[
"Hacl.Hash.Core.MD5._t",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperStack.is_eternal_color",
"lemma_FStar.Monotonic.HyperHeap.lemma_root_has_color_zero",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2fbd657fe85bcb2423f9c7e5f9b3bcb5",
"typing_FStar.Monotonic.HyperHeap.root"
],
0,
"162ec338f76c256c9e743e2ffd98ff0f"
],
[
"Hacl.Hash.Core.MD5.alloca",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.init", "equation_Spec.MD5.init",
"function_token_typing_FStar.UInt32.t",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"refinement_interpretation_Tm_refine_70bcd2d516db6edb5890dc10eb12fb0c",
"refinement_interpretation_Tm_refine_aa86585edfb0db002b261380c0e511c3",
"refinement_interpretation_Tm_refine_ec9680eabfb427d5a90085305d7948b7",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq"
],
0,
"4015db2e3790daff9023e8a8dee763f2"
],
[
"Hacl.Hash.Core.MD5.h0",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.init_t",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.MD5.init", "equation_Spec.MD5.init_as_list",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_0fd54884acd945724a2f55cda62d88e6",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_813767747c3f0e109fa66360ce38071c",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_a89cf0b757190ce4d61d9916911df730",
"refinement_interpretation_Tm_refine_da64e4aba91526652a67b31cd7d1693d",
"typing_FStar.UInt32.v", "typing_Hacl.Hash.Core.MD5._h0",
"typing_LowStar.ImmutableBuffer.immutable_preorder",
"typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.MD5.init"
],
0,
"9023e1655e7f07a4d45fd52424d1dae7"
],
[
"Hacl.Hash.Core.MD5.t",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Spec.MD5.t", "equation_Spec.MD5.t_as_list",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_0fd54884acd945724a2f55cda62d88e6",
"refinement_interpretation_Tm_refine_55e405d903c2fc715cb8f93c7dace611",
"refinement_interpretation_Tm_refine_813767747c3f0e109fa66360ce38071c",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_da64e4aba91526652a67b31cd7d1693d",
"typing_FStar.UInt32.v", "typing_Hacl.Hash.Core.MD5._t",
"typing_LowStar.ImmutableBuffer.immutable_preorder",
"typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.MD5.t"
],
0,
"7ce8f07c7c96069f99d889085f453728"
],
[
"Hacl.Hash.Core.MD5.seq_index_upd",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Prims.squash",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"l_and-interp", "lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_upd", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"unit_typing"
],
0,
"b6fa6c4dc235392105212d4cd0f5825b"
],
[
"Hacl.Hash.Core.MD5.init",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.l_True",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.init_t",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.Hash.init", "equation_Spec.MD5.init",
"equation_Spec.MD5.init_as_list",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.Seq.Properties.slice_upd",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_324dc1ff6aedf7b620d34179e87c2223",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_46cbe09753b56b22de537dd7c6fddbc8",
"refinement_interpretation_Tm_refine_519bd340152be8f85d16e819a005a9a5",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_917191ca110d48a36137a0a62b78fea5",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
"refinement_interpretation_Tm_refine_d025a1a6d9e9ec08307855778ad2ac6e",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"true_interp", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Seq.Properties.seq_of_list",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.Hash.init",
"typing_Spec.MD5.init", "typing_Spec.MD5.init_as_list",
"typing_tok_Spec.Hash.Definitions.MD5@tok"
],
0,
"7db77e112614ee186b5c4dfdc699a9e6"
],
[
"Hacl.Hash.Core.MD5.round_op_gen",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Hacl.Hash.Core.MD5.abcd_idx",
"equation_Hacl.Hash.Core.MD5.abcd_t",
"equation_Hacl.Hash.Core.MD5.t_idx",
"equation_Hacl.Hash.Core.MD5.x_idx",
"equation_Hacl.Hash.Core.MD5.x_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_34cfc3e65d974470c7f676d22302b7b3",
"refinement_interpretation_Tm_refine_5fd76f96dd8842f1d4e9ef690b5c4ee7",
"refinement_interpretation_Tm_refine_6c1b893fe0d79dcf933f5889430f25bb",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_a89cf0b757190ce4d61d9916911df730",
"refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
"refinement_interpretation_Tm_refine_e3e8ea1e9949642ff56ce81b8d1c6463",
"typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder"
],
0,
"28b7a62a11f157c511e824074b55c3ce"
],
[
"Hacl.Hash.Core.MD5.round_op_gen",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Core.MD5.abcd_idx",
"equation_Hacl.Hash.Core.MD5.abcd_t",
"equation_Hacl.Hash.Core.MD5.op_Less_Less_Less",
"equation_Hacl.Hash.Core.MD5.t_idx",
"equation_Hacl.Hash.Core.MD5.x_idx",
"equation_Hacl.Hash.Core.MD5.x_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.l_True", "equation_Prims.logical",
"equation_Prims.nat", "equation_Spec.MD5.op_Less_Less_Less",
"equation_Spec.MD5.round_op_gen_aux",
"equation_Spec.SHA2.Constants.k224_256",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Spec.MD5.round_op_gen", "int_inversion",
"int_typing",
"interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
"lemma_FStar.Ghost.reveal_hide",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.UInt.pow2_values",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1b4dc61a8b19b4ed36cc1c60b8efb278",
"refinement_interpretation_Tm_refine_2c94428b02d1fe9586404298fbf5db26",
"refinement_interpretation_Tm_refine_34bb0b194a9118eee4422fb25d748bae",
"refinement_interpretation_Tm_refine_34cfc3e65d974470c7f676d22302b7b3",
"refinement_interpretation_Tm_refine_5fd76f96dd8842f1d4e9ef690b5c4ee7",
"refinement_interpretation_Tm_refine_6c1b893fe0d79dcf933f5889430f25bb",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_a89cf0b757190ce4d61d9916911df730",
"refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_e3e8ea1e9949642ff56ce81b8d1c6463",
"token_correspondence_Spec.MD5.round_op_gen_aux", "true_interp",
"typing_FStar.Seq.Base.seq", "typing_FStar.UInt32.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.SHA2.Constants.k224_256"
],
0,
"5d722cc9a6a3c9175ed3ab58d75e52e3"
],
[
"Hacl.Hash.Core.MD5.round1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equation_FStar.List.Tot.Properties.llist",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Hacl.Hash.Core.MD5.abcd_t",
"equation_Hacl.Hash.Core.MD5.ia", "equation_Hacl.Hash.Core.MD5.ib",
"equation_Hacl.Hash.Core.MD5.ic", "equation_Hacl.Hash.Core.MD5.id",
"equation_Hacl.Hash.Core.MD5.x_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.MD5.abcd_t", "equation_Spec.MD5.ia",
"equation_Spec.MD5.ib", "equation_Spec.MD5.ic",
"equation_Spec.MD5.id", "equation_Spec.MD5.round1_aux",
"equation_Spec.MD5.round1_op", "equation_Spec.SHA2.Constants.h224",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Spec.MD5.round1", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1b4dc61a8b19b4ed36cc1c60b8efb278",
"refinement_interpretation_Tm_refine_34cfc3e65d974470c7f676d22302b7b3",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_e3e8ea1e9949642ff56ce81b8d1c6463",
"refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d",
"token_correspondence_Spec.MD5.round1_aux", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.SHA2.Constants.h224",
"typing_Spec.SHA2.Constants.h224_l"
],
0,
"e2415f2f27787edfd7741689bc6c2694"
],
[
"Hacl.Hash.Core.MD5.round2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equation_FStar.List.Tot.Properties.llist",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Hacl.Hash.Core.MD5.abcd_t",
"equation_Hacl.Hash.Core.MD5.ia", "equation_Hacl.Hash.Core.MD5.ib",
"equation_Hacl.Hash.Core.MD5.ic", "equation_Hacl.Hash.Core.MD5.id",
"equation_Hacl.Hash.Core.MD5.x_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.MD5.abcd_t", "equation_Spec.MD5.ia",
"equation_Spec.MD5.ib", "equation_Spec.MD5.ic",
"equation_Spec.MD5.id", "equation_Spec.MD5.round2_aux",
"equation_Spec.MD5.round2_op", "equation_Spec.SHA2.Constants.h224",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Spec.MD5.round2", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1b4dc61a8b19b4ed36cc1c60b8efb278",
"refinement_interpretation_Tm_refine_34cfc3e65d974470c7f676d22302b7b3",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_e3e8ea1e9949642ff56ce81b8d1c6463",
"refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d",
"token_correspondence_Spec.MD5.round2_aux", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.SHA2.Constants.h224",
"typing_Spec.SHA2.Constants.h224_l"
],
0,
"00ef7e1bdba66b96c9eecbabb378e6e7"
],
[
"Hacl.Hash.Core.MD5.round3",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equation_FStar.List.Tot.Properties.llist",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Hacl.Hash.Core.MD5.abcd_t",
"equation_Hacl.Hash.Core.MD5.ia", "equation_Hacl.Hash.Core.MD5.ib",
"equation_Hacl.Hash.Core.MD5.ic", "equation_Hacl.Hash.Core.MD5.id",
"equation_Hacl.Hash.Core.MD5.x_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.MD5.abcd_t", "equation_Spec.MD5.ia",
"equation_Spec.MD5.ib", "equation_Spec.MD5.ic",
"equation_Spec.MD5.id", "equation_Spec.MD5.round3_aux",
"equation_Spec.MD5.round3_op", "equation_Spec.SHA2.Constants.h224",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Spec.MD5.round3", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1b4dc61a8b19b4ed36cc1c60b8efb278",
"refinement_interpretation_Tm_refine_34cfc3e65d974470c7f676d22302b7b3",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_e3e8ea1e9949642ff56ce81b8d1c6463",
"refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d",
"token_correspondence_Spec.MD5.round3_aux", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.SHA2.Constants.h224",
"typing_Spec.SHA2.Constants.h224_l"
],
0,
"9897aa87d49dc97d2dc94c2c6cecf66f"
],
[
"Hacl.Hash.Core.MD5.round4",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equation_FStar.List.Tot.Properties.llist",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Hacl.Hash.Core.MD5.abcd_t",
"equation_Hacl.Hash.Core.MD5.ia", "equation_Hacl.Hash.Core.MD5.ib",
"equation_Hacl.Hash.Core.MD5.ic", "equation_Hacl.Hash.Core.MD5.id",
"equation_Hacl.Hash.Core.MD5.x_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.MD5.abcd_t", "equation_Spec.MD5.ia",
"equation_Spec.MD5.ib", "equation_Spec.MD5.ic",
"equation_Spec.MD5.id", "equation_Spec.MD5.round4_aux",
"equation_Spec.MD5.round4_op", "equation_Spec.SHA2.Constants.h224",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Spec.MD5.round4", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1b4dc61a8b19b4ed36cc1c60b8efb278",
"refinement_interpretation_Tm_refine_34cfc3e65d974470c7f676d22302b7b3",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_e3e8ea1e9949642ff56ce81b8d1c6463",
"refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d",
"token_correspondence_Spec.MD5.round4_aux", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.SHA2.Constants.h224",
"typing_Spec.SHA2.Constants.h224_l"
],
0,
"01746f170f8e798b4701c93c2db41c43"
],
[
"Hacl.Hash.Core.MD5.rounds",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.lseq",
"equation_Hacl.Hash.Core.MD5.abcd_t",
"equation_Hacl.Hash.Core.MD5.x_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.MD5.abcd_t", "equation_Spec.MD5.rounds_aux",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Spec.MD5.rounds",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"refinement_interpretation_Tm_refine_1b4dc61a8b19b4ed36cc1c60b8efb278",
"refinement_interpretation_Tm_refine_34cfc3e65d974470c7f676d22302b7b3",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
"refinement_interpretation_Tm_refine_e3e8ea1e9949642ff56ce81b8d1c6463",
"token_correspondence_Spec.MD5.rounds_aux",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer"
],
0,
"31ad83f0c45ec2c4d5fed0dc900e1b82"
],
[
"Hacl.Hash.Core.MD5.overwrite",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Hacl.Hash.Core.MD5.abcd_idx",
"equation_Hacl.Hash.Core.MD5.ia", "equation_Hacl.Hash.Core.MD5.ib",
"equation_Hacl.Hash.Core.MD5.ic", "equation_Hacl.Hash.Core.MD5.id",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.l_True",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.MD5.abcd_t", "equation_Spec.MD5.ia",
"equation_Spec.MD5.ib", "equation_Spec.MD5.ic",
"equation_Spec.MD5.id", "equation_Spec.MD5.overwrite_aux",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Spec.MD5.overwrite", "int_typing",
"interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_46cbe09753b56b22de537dd7c6fddbc8",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_a89cf0b757190ce4d61d9916911df730",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_e56bee1b5a8151dc24fd5890afb6565c",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"token_correspondence_Spec.MD5.overwrite_aux", "true_interp",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Hacl.Hash.Core.MD5.ia", "typing_Hacl.Hash.Core.MD5.ib",
"typing_Hacl.Hash.Core.MD5.ic", "typing_Hacl.Hash.Core.MD5.id",
"typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_tok_Spec.Hash.Definitions.MD5@tok"
],
0,
"e1a2e019733f0f0719d8c40d07cc6f47"
],
[
"Hacl.Hash.Core.MD5.update'",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Hash.Core.MD5.abcd_t",
"equation_Hacl.Hash.Core.MD5.x_t",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.words_of_bytes",
"equation_Spec.Hash.Definitions.words_state", "equation_Spec.MD5.ia",
"equation_Spec.MD5.ib", "equation_Spec.MD5.ic",
"equation_Spec.MD5.id", "equation_Spec.MD5.update_aux",
"function_token_typing_FStar.Kremlin.Endianness.seq_uint32_of_le",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt8.t", "int_inversion",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1b4dc61a8b19b4ed36cc1c60b8efb278",
"refinement_interpretation_Tm_refine_34cfc3e65d974470c7f676d22302b7b3",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_e3e8ea1e9949642ff56ce81b8d1c6463",
"token_correspondence_Spec.Hash.Definitions.words_of_bytes",
"token_correspondence_Spec.MD5.update_aux",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.Hash.Definitions.block_length",
"typing_tok_Spec.Hash.Definitions.MD5@tok"
],
0,
"75a5a260056000964ecb3f152df6b738"
],
[
"Hacl.Hash.Core.MD5.update",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Spec.Hash.Definitions_interpretation_Tm_arrow_4b3c7766b835530fed880045baf8337f",
"Spec.Hash_interpretation_Tm_arrow_861a72617971f3b12b1b2ab67a981d41",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.init_t",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.update_t",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.Hash.update", "equation_Spec.MD5.init",
"equation_Spec.MD5.init_as_list",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Spec.Hash.update", "int_inversion",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1b4dc61a8b19b4ed36cc1c60b8efb278",
"refinement_interpretation_Tm_refine_4d0ae6b4ff35c0c8471d358291472299",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_79f632aa3673390dc46de32f66260b13",
"refinement_interpretation_Tm_refine_8b1d037da1bb7b9ff38b9e2a3954695d",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"token_correspondence_Spec.Hash.update",
"typing_FStar.Seq.Properties.seq_of_list",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_Spec.Hash.Definitions.block_length", "typing_Spec.MD5.init",
"typing_Spec.MD5.init_as_list",
"typing_tok_Spec.Hash.Definitions.MD5@tok"
],
0,
"5020a624ca45364390f6330e82b4f100"
]
]
]