[ "šÓýšòø•¿á\u007f<\u001bÛ\u0017Rm", [ [ "Hacl.Streaming.Blake2.extra_state_zero_element", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.to_hash_alg", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "inversion-interp", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.max_extra_state" ], 0, "c60666da1354177eea45aadec53cc21f" ], [ "Hacl.Streaming.Blake2.s_v", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S16", "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.U8", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Lib.IntTypes.int_t", "equation_Lib.Sequence.lseq", "equation_Prims.squash", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "inversion-interp", "projection_inverse_FStar.Integers.Signed__0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42" ], 0, "18837fccca642c91dd406239101f569b" ], [ "Hacl.Streaming.Blake2.state_to_lbuffer", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "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_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "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.Blake2S@tok", "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.Impl.Blake2.Core.element_t", "equation_Hacl.Impl.Blake2.Core.row_len", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.m_spec", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "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.length", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.mul_mod_lemma", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_AmpAmp", "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.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_dcc646d859645b3b81681154d4a0b5c6", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Hacl.Impl.Blake2.Core.element_t", "typing_Hacl.Impl.Blake2.Core.row_len", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2S@tok" ], 0, "d9c12afd735fcea4ad9c4f2f3157460b" ], [ "Hacl.Streaming.Blake2.stateful_blake2", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok", "disc_equation_Lib.IntTypes.U128", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "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_stack_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.HyperStack.ST.is_eternal_region", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "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.Impl.Blake2.Core.element_t", "equation_Hacl.Impl.Blake2.Core.row_len", "equation_Hacl.Impl.Blake2.Core.word_t", "equation_Hacl.Impl.Blake2.Generic.uu___580", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.get_state_p", "equation_Hacl.Streaming.Blake2.m_spec", "equation_Hacl.Streaming.Blake2.s", "equation_Hacl.Streaming.Blake2.s_v", "equation_Hacl.Streaming.Blake2.state_to_lbuffer", "equation_Hacl.Streaming.Blake2.state_v", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "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.uint32", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.Monotonic.Buffer.loc_in", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___580", "function_token_typing_Lib.IntTypes.uint32", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_LowStar.Buffer.trivial_preorder", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "inversion-interp", "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.HyperStack.ST.lemma_same_refs_in_stack_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Set.lemma_equal_elim", "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.freeable_disjoint_", "lemma_LowStar.Monotonic.Buffer.freeable_length", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_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_region_addresses_", "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_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "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_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.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_161e04719814801d293219f408210f95", "refinement_interpretation_Tm_refine_18e1720005e6b14344455745383f1fcd", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5763aee336d560ac45ffcfa0eb1cc8c3", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_dcc646d859645b3b81681154d4a0b5c6", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e4a2ee60b04d7524ee6074c1349a0213", "refinement_interpretation_Tm_refine_e5a1a9c78f5d9b71e68d3781dc6ee401", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f2727b186ee5282a2abec68f9ad829a4", "refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051", "refinement_interpretation_Tm_refine_fca4a5fafb9266418eded26977d9e89d", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "true_interp", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Hacl.Impl.Blake2.Core.element_t", "typing_Hacl.Impl.Blake2.Core.row_len", "typing_Hacl.Streaming.Blake2.get_state_p", "typing_Hacl.Streaming.Blake2.state_to_lbuffer", "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.lbuffer_t", "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.as_seq", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.len", "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_LowStar.Monotonic.Buffer.loc_unused_in", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@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, "9f970a34e446c93a319f9e520f173bf6" ], [ "Hacl.Streaming.Blake2.stateful_key_t", 1, 0, 0, [ "@query" ], 0, "48635e76de7e7edaef07bcf3d8f29ed8" ], [ "Hacl.Streaming.Blake2.buffer_to_stateful_key_t", 1, 0, 0, [ "@query" ], 0, "46ffb9cd369bdd582c22fa1b77162d56" ], [ "Hacl.Streaming.Blake2.buffer_to_stateful_key_t", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_2c287e3fad0611b6999e5cd2be8ebc78" ], 0, "1c6ddc1e24baec7a69f583bdb7ff29c7" ], [ "Hacl.Streaming.Blake2.unit_to_stateful_key_t", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Prims.squash", "equation_Spec.Blake2.max_key", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "inversion-interp", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "09f6576171f840fc0d8ca6c4b56036cd" ], [ "Hacl.Streaming.Blake2.stateful_key", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.gt", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gt", "equation_Hacl.Streaming.Blake2.buffer_to_stateful_key_t", "equation_Hacl.Streaming.Blake2.key_size_t", "equation_Hacl.Streaming.Blake2.stateful_key_t", "equation_Hacl.Streaming.Blake2.uint8", "equation_Hacl.Streaming.Blake2.unit_to_stateful_key_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.Monotonic.Buffer.loc_in", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_LowStar.Buffer.trivial_preorder", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Set.lemma_equal_refl", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "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_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_region_addresses_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_046dbf199eec68a71c30b821f4de1704", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_161e04719814801d293219f408210f95", "refinement_interpretation_Tm_refine_2c287e3fad0611b6999e5cd2be8ebc78", "refinement_interpretation_Tm_refine_32edb2e320ac0703021bc6351d113ffe", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_368f9a5efb11a17405f74635ed9eb5d8", "refinement_interpretation_Tm_refine_3c1ad0be1d0c74aa050d71a040e6d191", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4405ff39c1f32171611cd2b5a06a4135", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_5b03403a8d3fa4c655ec2b3c1e1359f8", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_cfb9b8efff012a5d01b2c0a9c1ac3ddf", "refinement_interpretation_Tm_refine_d1f6ab3c9413bf684a9eb45b3d1bbb29", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f4bbe0e970bf9be7bb7bbdaa57fe8237", "refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "true_interp", "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.Set.singleton", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.g_is_null", "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_unused_in", "typing_LowStar.Monotonic.Buffer.mnull", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok", "unit_inversion", "unit_typing" ], 0, "7c7bf35e130d8859f42b08db4e01cb7d" ], [ "Hacl.Streaming.Blake2.stateful_key_to_buffer", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Streaming.Blake2.key_size_t", "equation_Hacl.Streaming.Blake2.stateful_key_t", "equation_Hacl.Streaming.Blake2.uint8", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.trivial_preorder", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_Lib.IntTypes.uint8", "lemma_LowStar.Monotonic.Buffer.length_null_1", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2c287e3fad0611b6999e5cd2be8ebc78", "refinement_interpretation_Tm_refine_368f9a5efb11a17405f74635ed9eb5d8", "refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.mnull", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "5ad7fd6599d6ec2ff6840007eb33f6f9" ], [ "Hacl.Streaming.Blake2.max_total_hash_length", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "constructor_distinct_Spec.Hash.Definitions.MD5", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "int_typing", "inversion-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Spec.Blake2.Blake2B@tok" ], 0, "0a0e2f9e3d3650dda6181b3265c6ff02" ], [ "Hacl.Streaming.Blake2.block", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "b4010d3466595e258302ca3a5c81bb93" ], [ "Hacl.Streaming.Blake2.output_size", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Prims.squash", "equation_Spec.Blake2.max_output", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "inversion-interp", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "0c32571544165c14966cb23807fb0a17" ], [ "Hacl.Streaming.Blake2.output_len", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.output_size", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_output", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "int_typing", "inversion-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Streaming.Blake2.output_size", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "0e4d8c99266ff9c4c1df87e6aad5824a" ], [ "Hacl.Streaming.Blake2.blake2_prevlen", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "disc_equation_Lib.IntTypes.SEC", "disc_equation_Spec.Blake2.Blake2B", "disc_equation_Spec.Blake2.Blake2S", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.to_hash_alg", "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.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.to_hash_alg", "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", "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_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7", "refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e", "refinement_interpretation_Tm_refine_7d01b8454d0a329117a8ab05b13c5a1d", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f4d7e6f5a478db1f42b60de83a56490", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt64.v", "typing_Hacl.Streaming.Blake2.max_total_hash_length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.cast", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok", "typing_tok_Spec.Blake2.Blake2B@tok" ], 0, "b2d39a6b86b26185ec573897df563643" ], [ "Hacl.Streaming.Blake2.init_s", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S16", "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.U8", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.SEC@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.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.output_size", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_key", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "inversion-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned", "typing_Prims.pow2", "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, "71019c3e3927be69b8bbf562fcf7531d" ], [ "Hacl.Streaming.Blake2.update_multi_s", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@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.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "inversion-interp", "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "fd5f269becaadbc27806152e9092407a" ], [ "Hacl.Streaming.Blake2.update_multi_s", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@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.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "function_token_typing_Lib.IntTypes.uint8", "inversion-interp", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_457211c35b16423f6ffd5db69258bc09", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f4d7e6f5a478db1f42b60de83a56490", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Seq.Base.length", "typing_Hacl.Streaming.Blake2.max_total_hash_length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "6661091f06e49ae4f19ceac475a29bd7" ], [ "Hacl.Streaming.Blake2.update_last_s", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Lib.IntTypes.numbytes", "equation_Prims.squash", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "inversion-interp", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "279abf3f319a24ff20e284ab0a10b415" ], [ "Hacl.Streaming.Blake2.update_last_s", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@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.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "inversion-interp", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_12d712fcaa8c290364ac0ed0df317dd1", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f4d7e6f5a478db1f42b60de83a56490", "refinement_interpretation_Tm_refine_de27ea683ea46f55f2eff141dc36ea22", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Seq.Base.length", "typing_Hacl.Streaming.Blake2.max_total_hash_length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "27071c0c3ec4188faf37234f4d191ac3" ], [ "Hacl.Streaming.Blake2.finish_s", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.SEC@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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_FStar.Pervasives.Native.fst", "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.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.output_len", "equation_Hacl.Streaming.Blake2.output_size", "equation_Hacl.Streaming.Blake2.t", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state_", "equation_Spec.Hash.PadFinish.finish", "equation_Spec.Hash.PadFinish.finish_blake", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "int_typing", "inversion-interp", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_aebf0a5a4cc5a0edddd5cedf26878e34", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.v", "typing_Hacl.Streaming.Blake2.output_len", "typing_Hacl.Streaming.Blake2.output_size", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.Blake2.blake2_finish", "typing_Spec.Blake2.max_output", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.max_extra_state", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_Spec.Hash.Definitions.to_hash_alg", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Blake2.Blake2S@tok" ], 0, "e9eaca9b807f074f33d7f54ab77cddc8" ], [ "Hacl.Streaming.Blake2.spec_s", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@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.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.output_size", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_key", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.to_hash_alg", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "inversion-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f4d7e6f5a478db1f42b60de83a56490", "refinement_interpretation_Tm_refine_d809ea37958bf53fa7316915c3f1d8f6", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Streaming.Blake2.max_total_hash_length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned", "typing_Prims.pow2", "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, "a78383e16c417058a6d084e3f19e4459" ], [ "Hacl.Streaming.Blake2.update_multi_zero", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U1", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@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.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___580", "equation_Hacl.Streaming.Blake2.alg", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___580", "int_inversion", "inversion-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "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.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_12d712fcaa8c290364ac0ed0df317dd1", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned", "typing_Spec.AES.gf8", "typing_Spec.Blake2.size_block", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2S@tok" ], 0, "f7cf078311a0408cdf2eb98aa76769dc" ], [ "Hacl.Streaming.Blake2.update_multi_zero", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Lib.IntTypes.numbytes", "equation_Prims.squash", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "inversion-interp", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "496061bae19feb08cc1bf9c110b5b2c1" ], [ "Hacl.Streaming.Blake2.update_multi_zero", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S64", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@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.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_FStar.Pervasives.Native.fst", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Hacl.Streaming.Blake2.update_multi_s", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.to_hash_alg", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "int_inversion", "inversion-interp", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_12d712fcaa8c290364ac0ed0df317dd1", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f4d7e6f5a478db1f42b60de83a56490", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Streaming.Blake2.max_total_hash_length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "unit_inversion" ], 0, "bb0c458ce6d8c25482797e65beb85220" ], [ "Hacl.Streaming.Blake2.update_multi_associative", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@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.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "inversion-interp", "l_and-interp", "lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "9f20618c95fd71329dd15420e4d0ac6d" ], [ "Hacl.Streaming.Blake2.update_multi_associative", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_Hacl.Impl.Blake2.Generic.uu___590", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.blake2_prevlength", "equation_Hacl.Streaming.Blake2.key_size_ty", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.t", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Hacl.Streaming.Blake2.update_multi_s", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "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.extra_state", "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.max_input_length", "equation_Spec.Hash.Definitions.nat_to_extra_state", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.words_state", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___590", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "inversion-interp", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f4d7e6f5a478db1f42b60de83a56490", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_eb9e505f0d582211235517ab1ba1cbf8", "refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004", "typing_FStar.Seq.Base.length", "typing_Hacl.Streaming.Blake2.blake2_prevlength", "typing_Hacl.Streaming.Blake2.max_total_hash_length", "typing_Hacl.Streaming.Blake2.t", "typing_Hacl.Streaming.Blake2.to_hash_alg", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned", "typing_Spec.AES.gf8", "typing_Spec.Agile.Hash.update_multi", "typing_Spec.Blake2.size_block", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.extra_state", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Spec.Blake2.Blake2B@tok", "unit_inversion" ], 0, "5625ab9ddc2fa8c70e790d056c48fbc2" ], [ "Hacl.Streaming.Blake2.blake2_hash_incremental_s", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Streaming.Blake2.key_size_t", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_368f9a5efb11a17405f74635ed9eb5d8", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "aca59dc28b49ab4c02267e4337b87bf8" ], [ "Hacl.Streaming.Blake2.size_block_props", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "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.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Lib.IntTypes.numbytes", "equation_Prims.squash", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "int_inversion", "inversion-interp", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_Hacl.Streaming.Blake2.to_hash_alg", "typing_Spec.Hash.Definitions.block_length" ], 0, "6bc815502e2461cf4092b18877a064e7" ], [ "Hacl.Streaming.Blake2.blake2_hash_incremental_s", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "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", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_FStar.Pervasives.Native.fst", "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.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.finish_s", "equation_Hacl.Streaming.Blake2.index", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.output_len", "equation_Hacl.Streaming.Blake2.output_size", "equation_Hacl.Streaming.Blake2.t", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Hacl.Streaming.Blake2.update_last_s", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.UpdateMulti.split_at_last_nb_rem", "equation_Lib.UpdateMulti.uint8", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.words_state", "equation_Spec.Hash.Incremental.split_blocks", "equation_Spec.Hash.Incremental.update_last", "equation_Spec.Hash.Incremental.update_last_blake", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "inversion-interp", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_362e2dfd5fc10941f1049c892a15d4e9", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_7303eab65f6a4f1e287d2ffa90e90fe1", "refinement_interpretation_Tm_refine_8f4d7e6f5a478db1f42b60de83a56490", "refinement_interpretation_Tm_refine_cc936e5a549dcdc2e3f9713145143490", "refinement_interpretation_Tm_refine_d809ea37958bf53fa7316915c3f1d8f6", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.v", "typing_Hacl.Streaming.Blake2.max_total_hash_length", "typing_Hacl.Streaming.Blake2.output_len", "typing_Hacl.Streaming.Blake2.output_size", "typing_Hacl.Streaming.Blake2.t", "typing_Hacl.Streaming.Blake2.to_hash_alg", "typing_Lib.IntTypes.unsigned", "typing_Lib.UpdateMulti.split_at_last_lazy", "typing_Lib.UpdateMulti.split_at_last_nb_rem", "typing_Spec.AES.gf8", "typing_Spec.Blake2.max_output", "typing_Spec.Blake2.size_block", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.extra_state", "typing_Spec.Hash.Definitions.nat_to_extra_state", "typing_Spec.Hash.Definitions.to_hash_alg", "typing_Spec.Hash.PadFinish.finish", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2S@tok", "unit_inversion" ], 0, "35224f3b0f1f8fa5697a8fff280a2372" ], [ "Hacl.Streaming.Blake2.blake2_hash_incremental_s_is_hash_incremental", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "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.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "constructor_distinct_Tm_unit", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "inversion-interp", "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f4d7e6f5a478db1f42b60de83a56490", "refinement_interpretation_Tm_refine_d809ea37958bf53fa7316915c3f1d8f6", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Streaming.Blake2.max_total_hash_length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.len_length", "typing_Spec.Hash.Definitions.to_hash_alg" ], 0, "e0ac5c9f678a4fd58e6b190b0dc2e8d1" ], [ "Hacl.Streaming.Blake2.init_s_blake2_init_eq", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U1", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_FStar.List.Tot.Properties.llist", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.index", "equation_Hacl.Streaming.Blake2.init_s", "equation_Hacl.Streaming.Blake2.output_size", "equation_Hacl.Streaming.Blake2.t", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.ivTable", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.pub_word_t", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.nat_to_extra_state", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Incremental.blake2_init", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "int_typing", "inversion-interp", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_17b5c82e827d21e595c1a46cf8137822", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_576183a4f8267f6296f94f4827351efd", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d", "typing_FStar.List.Tot.Base.length", "typing_Hacl.Streaming.Blake2.to_hash_alg", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.secret", "typing_Lib.IntTypes.u128", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.index", "typing_Spec.AES.gf8", "typing_Spec.Blake2.ivTable", "typing_Spec.Blake2.list_iv_B", "typing_Spec.Blake2.pub_word_t", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.max_extra_state", "typing_Spec.Hash.Definitions.to_hash_alg", "typing_Spec.Hash.Definitions.word_t", "typing_tok_Lib.IntTypes.SEC@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", "unit_inversion" ], 0, "a744e445ebd333d23c835fb0fdef4b2e" ], [ "Hacl.Streaming.Blake2.blake2_hash_incremental_s_is_hash_incremental", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S64", "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.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.U128@tok", "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", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.blake2_hash_incremental_s", "equation_Hacl.Streaming.Blake2.finish_s", "equation_Hacl.Streaming.Blake2.index", "equation_Hacl.Streaming.Blake2.init_s", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.output_size", "equation_Hacl.Streaming.Blake2.t", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Hacl.Streaming.Blake2.update_last_s", "equation_Hacl.Streaming.Blake2.update_multi_s", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.words_state", "equation_Spec.Hash.Incremental.blake2_hash_incremental", "equation_Spec.Hash.Incremental.hash_incremental_body", "equation_Spec.Hash.Incremental.update_last", "equation_Spec.Hash.Incremental.update_last_blake", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "inversion-interp", "lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0fddf10ea7b43b4674b15f8bf150639f", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7303eab65f6a4f1e287d2ffa90e90fe1", "refinement_interpretation_Tm_refine_8f4d7e6f5a478db1f42b60de83a56490", "refinement_interpretation_Tm_refine_c1c2a975e8b358ee260bcebaaffadb8d", "refinement_interpretation_Tm_refine_d809ea37958bf53fa7316915c3f1d8f6", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.v", "typing_Hacl.Streaming.Blake2.blake2_hash_incremental_s", "typing_Hacl.Streaming.Blake2.max_total_hash_length", "typing_Hacl.Streaming.Blake2.output_len", "typing_Hacl.Streaming.Blake2.t", "typing_Lib.IntTypes.unsigned", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.extra_state", "typing_Spec.Hash.Definitions.max_extra_state", "typing_Spec.Hash.Definitions.nat_to_extra_state", "typing_Spec.Hash.Definitions.to_hash_alg", "typing_Spec.Hash.PadFinish.finish", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2S@tok", "unit_inversion", "unit_typing" ], 0, "e27452186feaf76f0ed1f954bb75adad" ], [ "Hacl.Streaming.Blake2.spec_is_incremental", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Spec.Blake2.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.block_len", "equation_Hacl.Streaming.Blake2.uint8", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.v", "equation_Lib.UpdateMulti.uint8", "equation_Prims.nat", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "function_token_typing_Lib.IntTypes.uint8", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_49cb56d09e90998adb34fba84ce94d00", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d809ea37958bf53fa7316915c3f1d8f6", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length", "typing_Hacl.Impl.Blake2.Core.size_block" ], 0, "c8d4031abd3739e6138ae747887f29c5" ], [ "Hacl.Streaming.Blake2.spec_is_incremental", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.blake2_hash_incremental_s", "equation_Hacl.Streaming.Blake2.block_len", "equation_Hacl.Streaming.Blake2.index", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.output_size", "equation_Hacl.Streaming.Blake2.spec_s", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.UpdateMulti.uint8", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Incremental.split_blocks", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "function_token_typing_Lib.IntTypes.uint8", "inversion-interp", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_refl", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_49cb56d09e90998adb34fba84ce94d00", "refinement_interpretation_Tm_refine_8f4d7e6f5a478db1f42b60de83a56490", "refinement_interpretation_Tm_refine_c1c2a975e8b358ee260bcebaaffadb8d", "refinement_interpretation_Tm_refine_d809ea37958bf53fa7316915c3f1d8f6", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Impl.Blake2.Core.size_block", "typing_Hacl.Streaming.Blake2.blake2_hash_incremental_s", "typing_Hacl.Streaming.Blake2.max_total_hash_length", "typing_Hacl.Streaming.Blake2.spec_s", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "unit_inversion", "unit_typing" ], 0, "15a62e2f24c00cd648c5cb99980c6c32" ], [ "Hacl.Streaming.Blake2.update_multi_eq", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___590", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.blake2_prevlength", "equation_Hacl.Streaming.Blake2.key_size_ty", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_key", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___590", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "inversion-interp", "l_and-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "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.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_12d712fcaa8c290364ac0ed0df317dd1", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_eb9e505f0d582211235517ab1ba1cbf8", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned", "typing_Spec.AES.gf8", "typing_Spec.Blake2.max_key", "typing_Spec.Blake2.size_block", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.to_hash_alg", "typing_tok_Spec.Blake2.Blake2B@tok" ], 0, "cd948686cf1ff224aaa9dee4953e52a8" ], [ "Hacl.Streaming.Blake2.update_multi_eq", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Lib.IntTypes.numbytes", "equation_Prims.squash", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "inversion-interp", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "aebc53b9a57cbc8873ed15156b36999b" ], [ "Hacl.Streaming.Blake2.update_multi_eq", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Seq.Properties.split", "equation_Hacl.Impl.Blake2.Generic.uu___578", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.blake2_prevlength", "equation_Hacl.Streaming.Blake2.key_size_ty", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Hacl.Streaming.Blake2.update_multi_s", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "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.nat_to_extra_state", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___578", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "inversion-interp", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Properties.slice_length", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_12d712fcaa8c290364ac0ed0df317dd1", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_eb9e505f0d582211235517ab1ba1cbf8", "typing_FStar.Seq.Base.length", "typing_Hacl.Streaming.Blake2.blake2_prevlength", "typing_Hacl.Streaming.Blake2.to_hash_alg", "typing_Lib.IntTypes.unsigned", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.extra_state_v", "typing_Spec.Hash.Definitions.to_hash_alg", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Spec.Blake2.Blake2B@tok" ], 0, "0a9759380fa0d53869c988b9cd017ee1" ], [ "Hacl.Streaming.Blake2.update_last_eq", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@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.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.t", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state_", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "inversion-interp", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_8f4d7e6f5a478db1f42b60de83a56490", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e3adcc1543c10320b4ee94eadb7ea8b3", "refinement_interpretation_Tm_refine_e8ecd956833cd8f5be790d2954f9212e", "typing_FStar.Seq.Base.length", "typing_Hacl.Streaming.Blake2.max_total_hash_length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.to_hash_alg" ], 0, "a18fa321bf33e4d41a08ce5e03a60ffc" ], [ "Hacl.Streaming.Blake2.update_last_eq", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Prims.squash", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "inversion-interp", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "bbe96ee198758e58829b1731ec23b43f" ], [ "Hacl.Streaming.Blake2.update_last_eq", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.t", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Hacl.Streaming.Blake2.update_last_s", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "equation_Lib.UpdateMulti.split_at_last_nb_rem", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.blake2_update_last", "equation_Spec.Blake2.block_s", "equation_Spec.Blake2.get_last_padded_block", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.split", "equation_Spec.Blake2.wt", "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_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.max_input_length", "equation_Spec.Hash.Definitions.nat_to_extra_state", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.words_state", "equation_Spec.Hash.Incremental.last_split_blake", "equation_Spec.Hash.Incremental.update_last", "equation_Spec.Hash.Incremental.update_last_blake", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "inversion-interp", "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_len_slice", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "lemma_Spec.Hash.Lemmas.update_multi_zero", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_19daddf86323ca762702438524546abe", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_362e2dfd5fc10941f1049c892a15d4e9", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_3f933d53eea19c88c15bd068de7d471e", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f4d7e6f5a478db1f42b60de83a56490", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_ccbef96ee6e044a9cf0b4353c2d1f06e", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e3adcc1543c10320b4ee94eadb7ea8b3", "refinement_interpretation_Tm_refine_e8ecd956833cd8f5be790d2954f9212e", "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7", "refinement_interpretation_Tm_refine_fb0099501b9f186363680bc5b17d3ddb", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_FStar.UInt.fits", "typing_Hacl.Streaming.Blake2.max_total_hash_length", "typing_Hacl.Streaming.Blake2.t", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.sub", "typing_Lib.Sequence.update_sub", "typing_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "typing_Lib.UpdateMulti.split_at_last_nb_rem", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.Blake2.size_block", "typing_Spec.Blake2.size_block_w", "typing_Spec.Blake2.split", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.extra_state", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.extra_state_v", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_Spec.Hash.Definitions.to_hash_alg", "typing_Spec.Hash.Incremental.last_split_blake", "typing_tok_Lib.IntTypes.SEC@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, "b5ce00899f7baa0915154f56bd4a781f" ], [ "Hacl.Streaming.Blake2.state_types_equalities", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2S", "disc_equation_Spec.Blake2.Blake2B", "disc_equation_Spec.Blake2.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "inversion-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "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, "e81b923277019c9b15ada43ddd93a1b5" ], [ "Hacl.Streaming.Blake2.mk_update_multi", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U1", "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", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@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", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.block_len", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.uint8", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "interpretation_Tm_abs_5dcb0e14151e6da19efbfec9cd88c57e", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "inversion-interp", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_49cb56d09e90998adb34fba84ce94d00", "refinement_interpretation_Tm_refine_6336ce235e473c764e1cb9a138a16eab", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_aa5778c7228801e751571427b8c15a1f", "refinement_interpretation_Tm_refine_c162bb2ecae963e12e3ba6f70c878b5a", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t", "typing_FStar.UInt64.v", "typing_Hacl.Impl.Blake2.Core.size_block", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "a3e9c904f74653590ff1e17a8f0b7955" ], [ "Hacl.Streaming.Blake2.mk_update_multi", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U1", "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", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@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", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.block_len", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "inversion-interp", "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_49cb56d09e90998adb34fba84ce94d00", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Impl.Blake2.Core.size_block", "typing_Lib.IntTypes.v", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "74b726943951f092a5a954816c36fef4" ], [ "Hacl.Streaming.Blake2.mk_update_multi", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "Hacl.Streaming.Blake2_interpretation_Tm_ghost_arrow_d6b77f5f8179e9d8797cfed6a4a7d522", "Lib.Buffer_interpretation_Tm_ghost_arrow_2dc959718e214e5c75a81c011c332cb9", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_FStar.Pervasives.pattern", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Blake2.Core.element_t", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Impl.Blake2.Generic.valid_m_spec", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.block_len", "equation_Hacl.Streaming.Blake2.get_state_p", "equation_Hacl.Streaming.Blake2.get_wv", "equation_Hacl.Streaming.Blake2.index", "equation_Hacl.Streaming.Blake2.m_spec", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.s", "equation_Hacl.Streaming.Blake2.s_v", "equation_Hacl.Streaming.Blake2.state_to_lbuffer", "equation_Hacl.Streaming.Blake2.state_v", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.t", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "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.union", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state_", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_FStar.Pervasives.pattern", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "function_token_typing_Lib.Buffer.as_seq", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "interpretation_Tm_abs_29b066510dba958c27a723c00f802089", "interpretation_Tm_abs_535f1be047e39f2cf4c3103479db20db", "interpretation_Tm_abs_8ecd20da60337ec2574d124597a72a56", "interpretation_Tm_abs_ed29ee0a960cc4f7fdfee77a42bf4f1c", "inversion-interp", "l_and-interp", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_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_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_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "proj_equation_Hacl.Streaming.Interface.Stateful_footprint", "proj_equation_Hacl.Streaming.Interface.Stateful_freeable", "proj_equation_Hacl.Streaming.Interface.Stateful_invariant", "proj_equation_Hacl.Streaming.Interface.Stateful_v", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Hacl.Streaming.Interface.Stateful_footprint", "projection_inverse_Hacl.Streaming.Interface.Stateful_freeable", "projection_inverse_Hacl.Streaming.Interface.Stateful_invariant", "projection_inverse_Hacl.Streaming.Interface.Stateful_v", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_10bddcde8a44864bd5096d0b0d773079", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_46241218e4ca445171aa042f43e614a4", "refinement_interpretation_Tm_refine_49cb56d09e90998adb34fba84ce94d00", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6336ce235e473c764e1cb9a138a16eab", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_8f4d7e6f5a478db1f42b60de83a56490", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_aa5778c7228801e751571427b8c15a1f", "refinement_interpretation_Tm_refine_c162bb2ecae963e12e3ba6f70c878b5a", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_dcc646d859645b3b81681154d4a0b5c6", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f80140907a599c7d383ad5b15092e36b", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__footprint", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__freeable", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__invariant", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__v", "token_correspondence_Lib.Buffer.as_seq", "token_correspondence_Lib.Buffer.op_Brack_Lens_Access", "typing_FStar.Ghost.reveal", "typing_FStar.Set.singleton", "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "typing_Hacl.Impl.Blake2.Core.element_t", "typing_Hacl.Impl.Blake2.Core.size_block", "typing_Hacl.Streaming.Blake2.get_state_p", "typing_Hacl.Streaming.Blake2.get_wv", "typing_Hacl.Streaming.Blake2.max_total_hash_length", "typing_Hacl.Streaming.Blake2.state_to_lbuffer", "typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Tm_abs_29b066510dba958c27a723c00f802089", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Blake2.Blake2B@tok", "typing_tok_Spec.Blake2.Blake2S@tok", "unit_inversion", "unit_typing" ], 0, "eae7efdf34c06e95eca86e60738e1d4b" ], [ "Hacl.Streaming.Blake2.mk_update_last", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U1", "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", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@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", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Blake2.Generic.uu___552", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.block_len", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.uint8", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___552", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "interpretation_Tm_abs_5dcb0e14151e6da19efbfec9cd88c57e", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "inversion-interp", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_49cb56d09e90998adb34fba84ce94d00", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_c162bb2ecae963e12e3ba6f70c878b5a", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f71ac7c5ffccf0fee599b5d533a5a810", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t", "typing_FStar.UInt64.v", "typing_Hacl.Impl.Blake2.Core.size_block", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "57cbb2da51d5260d9be7a056e90150ff" ], [ "Hacl.Streaming.Blake2.mk_update_last", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.block_len", "equation_Hacl.Streaming.Blake2.key_size_t", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.v", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "fuel_guarded_inversion_Spec.Blake2.alg", "lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_368f9a5efb11a17405f74635ed9eb5d8", "refinement_interpretation_Tm_refine_49cb56d09e90998adb34fba84ce94d00", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Hacl.Impl.Blake2.Core.size_block", "typing_Hacl.Streaming.Blake2.block_len" ], 0, "9377e064fde5ce507ee9c5f73747d1c9" ], [ "Hacl.Streaming.Blake2.mk_update_last", 3, 0, 1, [ "@MaxIFuel_assumption", "@query", "Hacl.Streaming.Blake2_interpretation_Tm_ghost_arrow_d6b77f5f8179e9d8797cfed6a4a7d522", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "data_elim_FStar.Pervasives.Native.Mktuple2", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Pervasives.pattern", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Blake2.Core.element_t", "equation_Hacl.Impl.Blake2.Generic.valid_m_spec", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.block_len", "equation_Hacl.Streaming.Blake2.get_state_p", "equation_Hacl.Streaming.Blake2.get_wv", "equation_Hacl.Streaming.Blake2.index", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.s", "equation_Hacl.Streaming.Blake2.s_v", "equation_Hacl.Streaming.Blake2.state_to_lbuffer", "equation_Hacl.Streaming.Blake2.state_v", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "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.union", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.length", "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.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.to_hash_alg", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_FStar.Pervasives.pattern", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "interpretation_Tm_abs_29b066510dba958c27a723c00f802089", "interpretation_Tm_abs_535f1be047e39f2cf4c3103479db20db", "interpretation_Tm_abs_8ecd20da60337ec2574d124597a72a56", "interpretation_Tm_abs_ed29ee0a960cc4f7fdfee77a42bf4f1c", "l_and-interp", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_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_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_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Hacl.Streaming.Interface.Stateful_footprint", "proj_equation_Hacl.Streaming.Interface.Stateful_freeable", "proj_equation_Hacl.Streaming.Interface.Stateful_invariant", "proj_equation_Hacl.Streaming.Interface.Stateful_v", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Hacl.Streaming.Interface.Stateful_footprint", "projection_inverse_Hacl.Streaming.Interface.Stateful_freeable", "projection_inverse_Hacl.Streaming.Interface.Stateful_invariant", "projection_inverse_Hacl.Streaming.Interface.Stateful_v", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_10bddcde8a44864bd5096d0b0d773079", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_46241218e4ca445171aa042f43e614a4", "refinement_interpretation_Tm_refine_49cb56d09e90998adb34fba84ce94d00", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f4d7e6f5a478db1f42b60de83a56490", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_c162bb2ecae963e12e3ba6f70c878b5a", "refinement_interpretation_Tm_refine_d8cfc6d2c86b48a27715cb097a17b9c5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f71ac7c5ffccf0fee599b5d533a5a810", "refinement_interpretation_Tm_refine_f80140907a599c7d383ad5b15092e36b", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__footprint", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__freeable", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__invariant", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__v", "token_correspondence_Lib.Buffer.as_seq", "token_correspondence_Lib.Buffer.op_Brack_Lens_Access", "typing_FStar.Ghost.reveal", "typing_FStar.Set.singleton", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "typing_Hacl.Impl.Blake2.Core.element_t", "typing_Hacl.Impl.Blake2.Core.size_block", "typing_Hacl.Streaming.Blake2.block_len", "typing_Hacl.Streaming.Blake2.max_total_hash_length", "typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar", "typing_Lib.Buffer.union", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Tm_abs_29b066510dba958c27a723c00f802089", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Blake2.Blake2B@tok", "unit_inversion", "unit_typing" ], 0, "5e5adce0d1da4f9781eee7c122d2e581" ], [ "Hacl.Streaming.Blake2.blocks_state_len", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Hacl.Impl.Blake2.Core.M128", "constructor_distinct_Hacl.Impl.Blake2.Core.M32", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U1", "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_Hacl.Impl.Blake2.Core.M128", "disc_equation_Hacl.Impl.Blake2.Core.M256", "disc_equation_Hacl.Impl.Blake2.Core.M32", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Hacl.Impl.Blake2.Core.M128@tok", "equality_tok_Hacl.Impl.Blake2.Core.M256@tok", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@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", "equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Blake2.Generic.is_valid_blake2_config", "equation_Hacl.Impl.Blake2.Generic.uu___580", "equation_Hacl.Impl.Blake2.Generic.valid_m_spec", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.block_len", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_Hacl.Impl.Blake2.Generic.uu___580", "int_inversion", "inversion-interp", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_49cb56d09e90998adb34fba84ce94d00", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f80140907a599c7d383ad5b15092e36b", "typing_FStar.UInt32.v", "typing_Hacl.Impl.Blake2.Core.size_block", "typing_Hacl.Impl.Blake2.Core.uu___is_M256", "typing_Hacl.Impl.Blake2.Generic.is_valid_blake2_config", "typing_Hacl.Streaming.Blake2.block_len", "typing_Lib.IntTypes.v", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "7f05ddd99a4db7ccfefa14e1de70fd1a" ], [ "Hacl.Streaming.Blake2.blake2", 1, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Hacl.Streaming.Blake2_interpretation_Tm_ghost_arrow_d6b77f5f8179e9d8797cfed6a4a7d522", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Hacl.Impl.Blake2.Core.M128", "constructor_distinct_Hacl.Impl.Blake2.Core.M32", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "data_elim_FStar.Pervasives.Native.Mktuple2", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.pattern", "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.Impl.Blake2.Core.element_t", "equation_Hacl.Impl.Blake2.Core.word_t", "equation_Hacl.Impl.Blake2.Generic.is_valid_blake2_config", "equation_Hacl.Impl.Blake2.Generic.valid_m_spec", "equation_Hacl.Streaming.Blake2.alg", "equation_Hacl.Streaming.Blake2.block_len", "equation_Hacl.Streaming.Blake2.finish_s", "equation_Hacl.Streaming.Blake2.get_state_p", "equation_Hacl.Streaming.Blake2.init_s", "equation_Hacl.Streaming.Blake2.m_spec", "equation_Hacl.Streaming.Blake2.max_input_length", "equation_Hacl.Streaming.Blake2.max_total_hash_length", "equation_Hacl.Streaming.Blake2.output_len", "equation_Hacl.Streaming.Blake2.output_size", "equation_Hacl.Streaming.Blake2.s", "equation_Hacl.Streaming.Blake2.s_v", "equation_Hacl.Streaming.Blake2.state_to_lbuffer", "equation_Hacl.Streaming.Blake2.state_v", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.to_hash_alg", "equation_Hacl.Streaming.Blake2.uint8", "equation_Hacl.Streaming.Interface.stateful_unused", "equation_Hacl.Streaming.Interface.uint8", "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_Brack_Lens_Access", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.uint32x4", "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.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.max_key", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.to_hash_alg", "equation_Spec.Hash.PadFinish.finish", "equation_Spec.Hash.PadFinish.finish_blake", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Hacl.Impl.Blake2.Core.m_spec", "fuel_guarded_inversion_Spec.Blake2.alg", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_FStar.Pervasives.pattern", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Lib.IntVector.uint32x4", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing", "interpretation_Tm_abs_29b066510dba958c27a723c00f802089", "interpretation_Tm_abs_535f1be047e39f2cf4c3103479db20db", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "interpretation_Tm_abs_7db19245573865e2013f96b9787edb72", "interpretation_Tm_abs_8ecd20da60337ec2574d124597a72a56", "interpretation_Tm_abs_ed29ee0a960cc4f7fdfee77a42bf4f1c", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "l_and-interp", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.Set.lemma_equal_refl", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_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_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_Hacl.Streaming.Interface.Stateful_footprint", "proj_equation_Hacl.Streaming.Interface.Stateful_freeable", "proj_equation_Hacl.Streaming.Interface.Stateful_invariant", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "proj_equation_Hacl.Streaming.Interface.Stateful_v", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Hacl.Streaming.Interface.Stateful_footprint", "projection_inverse_Hacl.Streaming.Interface.Stateful_freeable", "projection_inverse_Hacl.Streaming.Interface.Stateful_invariant", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "projection_inverse_Hacl.Streaming.Interface.Stateful_v", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ac2b4007c94552e03635cc31821302c", "refinement_interpretation_Tm_refine_0b0aeb68a62274a6c5f5a39a1a466f8c", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_23c582df37989460c100e3a2bbde52c6", "refinement_interpretation_Tm_refine_2a4904b476349cfd4de22ca77d2f566e", "refinement_interpretation_Tm_refine_32fe57c6bcbbfb253f7f116c209cfde3", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_49cb56d09e90998adb34fba84ce94d00", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_597135ceaa5d1cbae0601f8f856594fd", "refinement_interpretation_Tm_refine_5e6f4c66e8b210506341087f85036f30", "refinement_interpretation_Tm_refine_6f8547284f7509667b7b5db6e2e01d7a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8ab994d64f1e6398334df8dbed7689d8", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a7f9a44a9f7fed845ca96d40c86346a3", "refinement_interpretation_Tm_refine_aa9c538977d6d666b081f0758b57db16", "refinement_interpretation_Tm_refine_b430bdcd621305d352569d94bb0b00ed", "refinement_interpretation_Tm_refine_d8178ae1ae7c4266c8707475787a509d", "refinement_interpretation_Tm_refine_dcc646d859645b3b81681154d4a0b5c6", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e2016a034f07d48443e588d97828286f", "refinement_interpretation_Tm_refine_e5bb9132ccf3cace115e16da4e6f64a0", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f80140907a599c7d383ad5b15092e36b", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__footprint", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__freeable", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__invariant", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__v", "token_correspondence_Lib.Buffer.as_seq", "token_correspondence_Lib.Buffer.op_Brack_Lens_Access", "true_interp", "typing_FStar.Ghost.reveal", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Hacl.Impl.Blake2.Core.element_t", "typing_Hacl.Impl.Blake2.Core.size_block", "typing_Hacl.Impl.Blake2.Generic.is_valid_blake2_config", "typing_Hacl.Streaming.Blake2.block_len", "typing_Hacl.Streaming.Blake2.get_state_p", "typing_Hacl.Streaming.Blake2.output_len", "typing_Hacl.Streaming.Blake2.state_to_lbuffer", "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.int_t", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.AES.gf8", "typing_Spec.Blake2.max_output", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Tm_abs_29b066510dba958c27a723c00f802089", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@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", "unit_inversion", "unit_typing" ], 0, "d402f4d749e7b799031cf0f8fb5dd5e8" ], [ "Hacl.Streaming.Blake2.blake2s_32", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Blake2.Core.M32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2S", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Hacl.Impl.Blake2.Generic.is_valid_blake2_config", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "a7645f5bb34d4289c1b559372b867c8a" ], [ "Hacl.Streaming.Blake2.blake2b_32", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Blake2.Core.M32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2B", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equation_Hacl.Impl.Blake2.Generic.is_valid_blake2_config", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "c55459e81057bc561d3fbed331d3d604" ], [ "Hacl.Streaming.Blake2.blake2s_32_state", 1, 0, 0, [ "@query", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Hacl.Streaming.Blake2.blake2", "equation_Hacl.Streaming.Blake2.blake2s_32", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.unit_key", "equation_Hacl.Streaming.Interface.stateful_unused", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s" ], 0, "8664ee7379503f320e283f3dddc398b3" ], [ "Hacl.Streaming.Blake2.blake2b_32_state", 1, 0, 0, [ "@query", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equation_Hacl.Streaming.Blake2.blake2", "equation_Hacl.Streaming.Blake2.blake2b_32", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.unit_key", "equation_Hacl.Streaming.Interface.stateful_unused", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s" ], 0, "be3c3f9fad0fe9c75985b75e434f3135" ], [ "Hacl.Streaming.Blake2.blake2s_32_no_key_alloca", 1, 0, 0, [ "@query", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Hacl.Streaming.Blake2.blake2", "equation_Hacl.Streaming.Blake2.blake2s_32", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.unit_key", "equation_Hacl.Streaming.Interface.stateful_unused", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s" ], 0, "3ba46971370dfe9f15b294d1a368e79f" ], [ "Hacl.Streaming.Blake2.blake2s_32_no_key_create_in", 1, 0, 0, [ "@query", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Hacl.Streaming.Blake2.blake2", "equation_Hacl.Streaming.Blake2.blake2s_32", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.unit_key", "equation_Hacl.Streaming.Interface.stateful_unused", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s" ], 0, "8be544a058744db980e29214f44098b1" ], [ "Hacl.Streaming.Blake2.blake2s_32_no_key_init", 1, 0, 0, [ "@query", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Hacl.Streaming.Blake2.blake2", "equation_Hacl.Streaming.Blake2.blake2s_32", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.unit_key", "equation_Hacl.Streaming.Interface.stateful_unused", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s" ], 0, "46b84f588e1fa3388e7d3516fb961d2b" ], [ "Hacl.Streaming.Blake2.blake2s_32_no_key_update", 1, 0, 0, [ "@query", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Hacl.Streaming.Blake2.blake2", "equation_Hacl.Streaming.Blake2.blake2s_32", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.unit_key", "equation_Hacl.Streaming.Interface.stateful_unused", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s" ], 0, "b6aeba39ad08ab34087c89b45387b2c2" ], [ "Hacl.Streaming.Blake2.blake2s_32_no_key_finish", 1, 0, 0, [ "@query", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Hacl.Streaming.Blake2.blake2", "equation_Hacl.Streaming.Blake2.blake2s_32", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.unit_key", "equation_Hacl.Streaming.Interface.stateful_unused", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s" ], 0, "f258ec36dfd4caeba71e7a3241cffaa0" ], [ "Hacl.Streaming.Blake2.blake2s_32_no_key_free", 1, 0, 0, [ "@query", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Hacl.Streaming.Blake2.blake2", "equation_Hacl.Streaming.Blake2.blake2s_32", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.unit_key", "equation_Hacl.Streaming.Interface.stateful_unused", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s" ], 0, "6bb040078f4ddd6e334bbf12dcb3ca21" ], [ "Hacl.Streaming.Blake2.blake2b_32_no_key_alloca", 1, 0, 0, [ "@query", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equation_Hacl.Streaming.Blake2.blake2", "equation_Hacl.Streaming.Blake2.blake2b_32", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.unit_key", "equation_Hacl.Streaming.Interface.stateful_unused", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s" ], 0, "a64026125317f6cc3ceeb4654f523b4a" ], [ "Hacl.Streaming.Blake2.blake2b_32_no_key_create_in", 1, 0, 0, [ "@query", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equation_Hacl.Streaming.Blake2.blake2", "equation_Hacl.Streaming.Blake2.blake2b_32", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.unit_key", "equation_Hacl.Streaming.Interface.stateful_unused", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s" ], 0, "2e221985806dc0ffd7b432008ca7a327" ], [ "Hacl.Streaming.Blake2.blake2b_32_no_key_init", 1, 0, 0, [ "@query", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equation_Hacl.Streaming.Blake2.blake2", "equation_Hacl.Streaming.Blake2.blake2b_32", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.unit_key", "equation_Hacl.Streaming.Interface.stateful_unused", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s" ], 0, "6460360d5d5e6fd8b278ba10b0d09528" ], [ "Hacl.Streaming.Blake2.blake2b_32_no_key_update", 1, 0, 0, [ "@query", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equation_Hacl.Streaming.Blake2.blake2", "equation_Hacl.Streaming.Blake2.blake2b_32", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.unit_key", "equation_Hacl.Streaming.Interface.stateful_unused", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s" ], 0, "8c4a1ce4636cf585e94b830039081e08" ], [ "Hacl.Streaming.Blake2.blake2b_32_no_key_finish", 1, 0, 0, [ "@query", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equation_Hacl.Streaming.Blake2.blake2", "equation_Hacl.Streaming.Blake2.blake2b_32", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.unit_key", "equation_Hacl.Streaming.Interface.stateful_unused", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s" ], 0, "3e16072caa1dd874a92876df33dc7553" ], [ "Hacl.Streaming.Blake2.blake2b_32_no_key_free", 1, 0, 0, [ "@query", "equality_tok_Hacl.Impl.Blake2.Core.M32@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equation_Hacl.Streaming.Blake2.blake2", "equation_Hacl.Streaming.Blake2.blake2b_32", "equation_Hacl.Streaming.Blake2.stateful_blake2", "equation_Hacl.Streaming.Blake2.unit_key", "equation_Hacl.Streaming.Interface.stateful_unused", "interpretation_Tm_abs_6f8de90af7881fb0e7de7d0981cbe58f", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s" ], 0, "f8a250f339700428e4e7ff8f7056ac17" ] ] ]