Revision 1539fc67ec7cd1f092967452d8ae47d170ca149b authored by Jonathan Protzenko on 24 April 2020, 23:18:32 UTC, committed by Jonathan Protzenko on 24 April 2020, 23:18:32 UTC
1 parent 56130dc
Hacl.Hash.MD.fst.hints
[
"�~�zq.�䉃��P0��",
[
[
"Hacl.Hash.MD.padding_round",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.len_v",
"equation_Spec.Hash.Definitions.pad_length",
"equation_Spec.Hash.Definitions.word_length", "int_inversion",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8a87b8a531982aadb85bf1f25e594833",
"typing_Spec.Hash.Definitions.len_v",
"typing_Spec.Hash.Definitions.pad_length",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"695dd169422db55b472f9ea4887c20e2"
],
[
"Hacl.Hash.MD.mod_sub_add",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"1310b76b4473eaed9f0a645149f4a441"
],
[
"Hacl.Hash.MD.mod_sub_add",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"7ed091065250b83451aa609c2dd17dfa"
],
[
"Hacl.Hash.MD.pad0_length_mod",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.len_length",
"equation_Spec.Hash.Definitions.pad0_length",
"equation_Spec.Hash.Definitions.word_length",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2043fe1d818aaeaa104a717402baf403",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Spec.Hash.Definitions.len_length",
"typing_Spec.Hash.Definitions.pad0_length",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"e5eed63f20989651839bbbf36d0503e8"
],
[
"Hacl.Hash.MD.pad_length_mod",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.pad_length",
"equation_Spec.Hash.Definitions.word_length",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"00d92ac20e4edb7f6d0b198da4fb254f"
],
[
"Hacl.Hash.MD.pad_length_bound",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_BoxInt",
"constructor_distinct_Tm_unit", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.len_length",
"equation_Spec.Hash.Definitions.len_v",
"equation_Spec.Hash.Definitions.pad0_length",
"equation_Spec.Hash.Definitions.pad_length",
"equation_Spec.Hash.Definitions.word_length", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"b2aa21ebf68061b5169cdb7315064763"
],
[
"Hacl.Hash.MD.len_add32",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"constructor_distinct_Tm_unit",
"disc_equation_Spec.Hash.Definitions.MD5",
"disc_equation_Spec.Hash.Definitions.SHA1",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U128@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.Int.Cast.uint32_to_uint64",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt128.n",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.len_t",
"equation_Spec.Hash.Definitions.len_v",
"equation_Spec.Hash.Definitions.max_input_length", "int_inversion",
"int_typing",
"interpretation_Tm_abs_71042ce475a96c7fa134177a01959d0b",
"interpretation_Tm_abs_c5cfacc785df376403b58f49cdaf22b6",
"primitive_Prims.op_Addition", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83283d1533f17b87318f0dd58e60907d",
"refinement_interpretation_Tm_refine_89263c8dd7df5c497acdada0682b1aab",
"refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.UInt.fits",
"typing_FStar.UInt128.uint64_to_uint128", "typing_FStar.UInt32.v",
"typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.len_v",
"typing_Spec.Hash.Definitions.max_input_length",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"50adc824356281d14f85915aec7d9ad0"
],
[
"Hacl.Hash.MD.mk_update_multi",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Spec.Agile.Hash_interpretation_Tm_arrow_9511bb3e8dd03332bdc255a2a2621d89",
"Spec.Hash.Definitions_interpretation_Tm_arrow_3919213edab5530de5a42c49ef9baf98",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"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_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.Definitions.block_len",
"equation_Hacl.Hash.Definitions.blocks_t",
"equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.bytes_block",
"equation_Spec.Hash.Definitions.bytes_blocks",
"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",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Spec.Agile.Hash.update", "int_inversion",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Ghost.reveal_hide", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv",
"lemma_Hacl.Hash.Lemmas.lemma_slice_ijk",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"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.live_gsub",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_Spec.Hash.Lemmas.update_multi_associative_",
"lemma_Spec.Hash.Lemmas.update_multi_update",
"lemma_Spec.Hash.Lemmas.update_multi_zero",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
"refinement_interpretation_Tm_refine_22ea23156c96d1f95a36c1bf3ce83086",
"refinement_interpretation_Tm_refine_2d9fe1ead8c24331bf3cb6801501c17b",
"refinement_interpretation_Tm_refine_313945d6e5dd9a1523b4f94bb56574eb",
"refinement_interpretation_Tm_refine_321b8c4d1f13b7a3c12bd2afd5e225ee",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_8123bca628cafe0c2db21c68d24b1c50",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_91c352d831715ed604553457a8078865",
"refinement_interpretation_Tm_refine_a80eb2ed78152ea57ef9b8fd6a9e440d",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c0a53502c2895aec13939500960c6000",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004",
"refinement_interpretation_Tm_refine_fdaf1d0e98b161e8e368c15419142c32",
"token_correspondence_Spec.Agile.Hash.update", "true_interp",
"typing_FStar.Ghost.reveal", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.empty",
"typing_FStar.Seq.Base.slice", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
"typing_Hacl.Hash.Definitions.block_len", "typing_Lib.IntTypes.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.Agile.Hash.update_multi",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.Definitions.word",
"typing_Spec.Hash.Definitions.word_length",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Spec.Hash.Definitions.MD5@tok"
],
0,
"af7c446836c4386344a3208621429a44"
],
[
"Hacl.Hash.MD.mk_update_last",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"equation_Prims.nat", "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_length", "int_inversion",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"0af210ca29b40d2d1fdc8cbf594ab6d6"
],
[
"Hacl.Hash.MD.mk_update_last",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_stack_region",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.Seq.Base.op_At_Bar", "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.Definitions.block_len",
"equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.bytes_blocks",
"equation_Spec.Hash.Definitions.len_length",
"equation_Spec.Hash.Definitions.len_v",
"equation_Spec.Hash.Definitions.pad0_length",
"equation_Spec.Hash.Definitions.pad_length",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.Hash.Incremental.update_last",
"equation_Spec.Hash.PadFinish.pad",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Ghost.reveal_hide",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.Seq.Properties.slice_slice",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_Hacl.Hash.Lemmas.lemma_slice",
"lemma_Hacl.Hash.Lemmas.lemma_slice_ijk",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_addr_gsub",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.frameOf_gsub",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"lemma_Spec.Hash.Lemmas.update_multi_associative_",
"lemma_Spec.Hash.Lemmas0.pad_invariant_block",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0941c9ff95557f2d53bc8f8179ab793e",
"refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
"refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2",
"refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_2043fe1d818aaeaa104a717402baf403",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_3e46b9b636901b521182d7f3235361f9",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_64db71038e8b1122a09ad7ad1ecc305a",
"refinement_interpretation_Tm_refine_69a8f7da28a283c569a2e6ee4ede1f73",
"refinement_interpretation_Tm_refine_709aff84c75b0fff77dcbf3b529649dd",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_78d39c902f3a2c7f5d1206d5336bcf09",
"refinement_interpretation_Tm_refine_7caba58cc379aae6aa2bd97bffb8c22b",
"refinement_interpretation_Tm_refine_8123bca628cafe0c2db21c68d24b1c50",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_850fe300f875565a60c2c1ce43a6fda4",
"refinement_interpretation_Tm_refine_8a87b8a531982aadb85bf1f25e594833",
"refinement_interpretation_Tm_refine_91c352d831715ed604553457a8078865",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_b61185bd7bfa9db1bf20ad7e18b96aab",
"refinement_interpretation_Tm_refine_bccf5300d87982e3ce0f7618196189a3",
"refinement_interpretation_Tm_refine_c0f2b55f3364ab26d055f27794c9eaaa",
"refinement_interpretation_Tm_refine_c473af663420011ee74a4f3a8de3e32a",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f2b58175e9c87f9d25c3e46e8ba928cd",
"refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004",
"refinement_interpretation_Tm_refine_fdaf1d0e98b161e8e368c15419142c32",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"true_interp", "typing_FStar.Map.contains",
"typing_FStar.Map.domain", "typing_FStar.Map.restrict",
"typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.is_stack_region",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_FStar.Set.complement",
"typing_FStar.Set.mem", "typing_FStar.Set.singleton",
"typing_FStar.Set.union", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.add", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.block_len",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union", "typing_Prims.pow2",
"typing_Spec.Agile.Hash.update_multi",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.Definitions.len_length",
"typing_Spec.Hash.Definitions.len_v",
"typing_Spec.Hash.Definitions.pad0_length",
"typing_Spec.Hash.Definitions.pad_length",
"typing_Spec.Hash.Definitions.word",
"typing_Spec.Hash.Definitions.word_length",
"typing_Spec.Hash.PadFinish.pad", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"54432751f5b96bd81f2e6f647cc30d0b"
],
[
"Hacl.Hash.MD.u32_to_len",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U128@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.Int.Cast.Full.uint64_to_uint128",
"equation_FStar.Int.Cast.uint32_to_uint64",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.v",
"equation_Spec.Hash.Definitions.len_t",
"equation_Spec.Hash.Definitions.len_v",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"interpretation_Tm_abs_71042ce475a96c7fa134177a01959d0b",
"interpretation_Tm_abs_c5cfacc785df376403b58f49cdaf22b6",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_89263c8dd7df5c497acdada0682b1aab",
"refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b",
"typing_FStar.Int.Cast.Full.uint64_to_uint128",
"typing_FStar.Int.Cast.uint32_to_uint64"
],
0,
"89ced91147b038161cb5a9f11589a2df"
],
[
"Hacl.Hash.MD.mk_hash",
1,
0,
0,
[ "@query" ],
0,
"b2b4fbc2579ed035b5adae1e9b7280d7"
],
[
"Hacl.Hash.MD.mk_hash",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.live_region",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.Seq.Properties.split", "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.Definitions.block_len",
"equation_Hacl.Hash.Definitions.hash_t",
"equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.bytes_blocks",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.init_t",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.Hash.Incremental.hash_incremental",
"equation_Spec.Hash.Incremental.update_last",
"equation_Spec.Hash.Lemmas.hash",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Ghost.reveal_hide",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_addr_gsub",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.frameOf_gsub",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"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.live_gsub",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Negation",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0dd7d82d89ad57ee72279b3caed814b3",
"refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
"refinement_interpretation_Tm_refine_11f5c63c78caccafb41a6490396f36ec",
"refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2",
"refinement_interpretation_Tm_refine_2db1238d4e682e6fb3f6f16c1128229b",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_7e55a624cd32632504c0da151085a132",
"refinement_interpretation_Tm_refine_8123bca628cafe0c2db21c68d24b1c50",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_91c352d831715ed604553457a8078865",
"refinement_interpretation_Tm_refine_9ca7807bfc284168a2426f4440262824",
"refinement_interpretation_Tm_refine_9e0a09a7bf94a5b88dd651f1cef8b834",
"refinement_interpretation_Tm_refine_b3e3751c3894f166dfde09b500dd73a6",
"refinement_interpretation_Tm_refine_b40fcd8f119b500a437777dd70ce3945",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f2b58175e9c87f9d25c3e46e8ba928cd",
"refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004",
"refinement_interpretation_Tm_refine_fdaf1d0e98b161e8e368c15419142c32",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"true_interp", "typing_FStar.Map.contains",
"typing_FStar.Map.domain", "typing_FStar.Map.restrict",
"typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.live_region",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.block_len",
"typing_Hacl.Hash.MD.u32_to_len", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Spec.Agile.Hash.init", "typing_Spec.Agile.Hash.update_multi",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.Definitions.block_word_length",
"typing_Spec.Hash.Definitions.hash_length",
"typing_Spec.Hash.Definitions.hash_word_length",
"typing_Spec.Hash.Definitions.state_word_length",
"typing_Spec.Hash.Definitions.word",
"typing_Spec.Hash.Definitions.word_length",
"typing_Spec.Hash.Incremental.hash_incremental",
"typing_Spec.Hash.Incremental.update_last",
"typing_Spec.Hash.Lemmas.hash", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"a199add909f34e7b3511f6d10dbb440c"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...