[ "8꣉bg", [ [ "Hacl.Hash.Core.Blake2.mk_init", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT", "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.SEC", "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.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "disc_equation_Lib.IntTypes.SEC", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "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.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Definitions.as_seq", "equation_Hacl.Hash.Definitions.const_nat_to_extra_state", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.get_spec", "equation_Hacl.Hash.Definitions.impl_state_length", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.initial_extra_state", "equation_Hacl.Hash.Definitions.m_spec", "equation_Hacl.Hash.Definitions.state", "equation_Hacl.Impl.Blake2.Core.element_t", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.Hash.init", "equation_Spec.Blake2.ivTable", "equation_Spec.Blake2.max_key", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.nat_to_word", "equation_Spec.Blake2.pub_word_t", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word_t", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "int_inversion", "int_typing", "inversion-interp", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_17b5c82e827d21e595c1a46cf8137822", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7", "refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e", "refinement_interpretation_Tm_refine_576183a4f8267f6296f94f4827351efd", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_dcb6398246d7420b589fcf1d75bb2ae8", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fedb9c9a0c1dc2a89888d40562fdee8b", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.initial_extra_state", "typing_Hacl.Impl.Blake2.Core.element_t", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.cast", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.op_At_Percent_Dot", "typing_Lib.IntTypes.secret", "typing_Lib.IntTypes.u128", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.index", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.length", "typing_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.Blake2.ivTable", "typing_Spec.Blake2.max_key", "typing_Spec.Blake2.pub_word_t", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_Spec.Hash.Definitions.word_t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Blake2.Blake2B@tok", "typing_tok_Spec.Blake2.Blake2S@tok" ], 0, "a3f24e84c31e29a3644ceddd5deba02c" ], [ "Hacl.Hash.Core.Blake2.state_p_to_state", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "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.U8", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "constructor_distinct_Spec.Hash.Definitions.MD5", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.get_spec", "equation_Hacl.Hash.Definitions.impl_state_length", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.m_spec", "equation_Hacl.Hash.Definitions.mk_impl", "equation_Hacl.Hash.Definitions.state", "equation_Hacl.Impl.Blake2.Core.element_t", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.v", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.to_blake_alg", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "typing_Spec.Hash.Definitions.to_blake_alg", "unit_typing" ], 0, "51de5e8488a69517653e6ece13393fce" ], [ "Hacl.Hash.Core.Blake2.mk_alloca", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "b2t_def", "bool_inversion", "constructor_distinct_Hacl.Impl.Blake2.Core.M128", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "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.U8", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@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.is_stack_region", "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.Core.Blake2.state_p_to_state", "equation_Hacl.Hash.Definitions.as_seq", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.get_spec", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.m_spec", "equation_Hacl.Hash.Definitions.mk_impl", "equation_Hacl.Hash.Definitions.state", "equation_Hacl.Impl.Blake2.Core.row_len", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.live", "equation_Lib.Buffer.stack_allocated", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.Hash.init", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.words_state_", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.mul_mod_lemma", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "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_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_82594d4068533b7192b2f88587f6a7b8", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9ca7807bfc284168a2426f4440262824", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.as_seq", "typing_Hacl.Hash.Definitions.impl_word", "typing_Hacl.Hash.Definitions.mk_impl", "typing_Hacl.Impl.Blake2.Core.row_len", "typing_Lib.IntTypes.mul_mod", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "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_unused_in", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2S@tok" ], 0, "b8b5e895b8c933824260704e33310d05" ], [ "Hacl.Hash.Core.Blake2.mk_update", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "Spec.Hash.Definitions_interpretation_Tm_arrow_3ac874e39b1c409ba69a2358a6f73691", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.Buffer.MUT", "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.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "data_typing_intro_Prims.Mkdtuple2@tok", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@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.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "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.Blake2.state_p_len", "equation_Hacl.Hash.Core.Blake2.state_p_to_state", "equation_Hacl.Hash.Definitions.as_seq", "equation_Hacl.Hash.Definitions.block_len", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.get_spec", "equation_Hacl.Hash.Definitions.impl", "equation_Hacl.Hash.Definitions.impl_state_length", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.m_spec", "equation_Hacl.Hash.Definitions.mk_impl", "equation_Hacl.Hash.Definitions.state", "equation_Hacl.Impl.Blake2.Core.block_p", "equation_Hacl.Impl.Blake2.Core.row_len", "equation_Hacl.Impl.Blake2.Core.size_block", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.op_Brack_Lens_Access", "equation_Lib.Buffer.stack_allocated", "equation_Lib.Buffer.union", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "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.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.Hash.update", "equation_Spec.Blake2.limb_t", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.extra_state_add_nat", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.extra_state_v", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.size_block", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word_length", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "function_token_typing_Spec.AES.elem", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "interpretation_Tm_abs_0a22db5cb809bc71916ebf6a3b18cd56", "interpretation_Tm_abs_3d77c1d80c0e9e736cdcf018f4780b14", "interpretation_Tm_abs_e3e4e6e500ae76ff6ad28ada6503a771", "kinding_Spec.Hash.Definitions.hash_alg@tok", "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.Map.lemma_equal_elim", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "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.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_Hacl.Impl.Blake2.Core.state_v_eq_lemma", "lemma_Lib.IntTypes.mul_mod_lemma", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "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_disjoint_union_r_", "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_includes_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer", "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_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_028e3d676128c000131df62014b3d4df", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_3387c784ff6d509c843148dfd3469211", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_7027b484d005b4a5862ad5fc5e060c20", "refinement_interpretation_Tm_refine_82594d4068533b7192b2f88587f6a7b8", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_91c352d831715ed604553457a8078865", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_d95c9886eac54874419434728dbe52f5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_ec724d57012ed9909a2433e971ebc061", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Lib.Buffer.as_seq", "token_correspondence_Lib.Buffer.op_Brack_Lens_Access", "token_correspondence_Spec.Agile.Hash.update", "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_tip", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.intersect", "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.Definitions.impl_state_length", "typing_Hacl.Hash.Definitions.impl_word", "typing_Hacl.Impl.Blake2.Core.row_len", "typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar", "typing_Lib.IntTypes.mul_mod", "typing_Lib.IntTypes.unsigned", "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.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.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.extra_state_add_nat", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_Spec.Hash.Definitions.word_length", "typing_Tm_abs_3d77c1d80c0e9e736cdcf018f4780b14", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2B@tok", "typing_tok_Spec.Blake2.Blake2S@tok" ], 0, "711c06f9c9264bac80b235472dce7e8c" ], [ "Hacl.Hash.Core.Blake2.init_blake2s_32", 1, 0, 0, [ "@query", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Spec.Hash.Definitions.is_blake", "projection_inverse_BoxBool_proj_0" ], 0, "4906d8de3f1a817c96c644d099b95404" ], [ "Hacl.Hash.Core.Blake2.alloca_blake2s_32", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.is_blake", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "5611335939274300b7a8a5841a16630e" ], [ "Hacl.Hash.Core.Blake2.update_blake2s_32", 1, 0, 0, [ "@query", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Spec.Hash.Definitions.is_blake", "projection_inverse_BoxBool_proj_0" ], 0, "e2a782386d86c87a8a24150b9cadd3b1" ], [ "Hacl.Hash.Core.Blake2.finish_blake2s_32", 1, 0, 0, [ "@query", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Spec.Hash.Definitions.is_blake", "projection_inverse_BoxBool_proj_0" ], 0, "5051111ab717dfeef89b44b4aec541cb" ], [ "Hacl.Hash.Core.Blake2.init_blake2b_32", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.is_blake", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.unsigned", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2S@tok" ], 0, "1d6f50a10d2c609a5a7cc5ae6be3cbc5" ], [ "Hacl.Hash.Core.Blake2.alloca_blake2b_32", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.is_blake", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.unsigned", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2S@tok" ], 0, "3aeec455c1672623a6815bf46c1f3ce9" ], [ "Hacl.Hash.Core.Blake2.update_blake2b_32", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.is_blake", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.unsigned", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2S@tok" ], 0, "623279d0ced748e1b4717e248d2b874d" ], [ "Hacl.Hash.Core.Blake2.finish_blake2b_32", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.is_blake", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "e6c43fd4d9cb018da6d4559cb4ae28b0" ] ] ]