[ "zº,¢RD?¹_ɯ\",ãȺ", [ [ "EverCrypt.Hash.Incremental.agile_state", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing", "equation_EverCrypt.Hash.footprint", "equation_EverCrypt.Hash.freeable", "equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.preserves_freeable", "equation_EverCrypt.Hash.state", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing", "lemma_FStar.Map.lemma_ContainsDom", "lemma_LowStar.Monotonic.Buffer.freeable_length", "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.modifies_buffer_elim", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.state_s", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Set.singleton", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.get", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, "2950b8ddbd70e5f985c932b0dc9c0787" ], [ "EverCrypt.Hash.Incremental.mk_words_state", 1, 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_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.is_blake", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "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_2757a754fad112fc6be67efc7b2ef015", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "unit_typing" ], 0, "f0261fc29b3dcced437c3883572e6710" ], [ "EverCrypt.Hash.Incremental.evercrypt_hash", 1, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Signed", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "data_elim_FStar.Pervasives.Native.Mktuple2", "disc_equation_Lib.IntTypes.SEC", "disc_equation_Lib.IntTypes.U128", "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", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.block_len", "equation_EverCrypt.Hash.Incremental.mk_words_state", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.preserves_freeable", "equation_EverCrypt.Hash.repr_with_counter", "equation_EverCrypt.Hash.state", "equation_FStar.Integers.int_t", "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_FStar.UInt.uint_t", "equation_Hacl.Hash.Definitions.block_len", "equation_Hacl.Impl.Blake2.Core.size_block", "equation_Hacl.Streaming.Blake2.block_len", "equation_Hacl.Streaming.Blake2.finish_s", "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.spec_s", "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_Hacl.Streaming.Interface.stateful_unused", "equation_Hacl.Streaming.Interface.uint8", "equation_Hacl.Streaming.MD.max_input_length64", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.UpdateMulti.split_at_last_lazy", "equation_Lib.UpdateMulti.uint8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "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.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.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.init_t", "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.word_t", "equation_Spec.Hash.Definitions.words_state", "equation_Spec.Hash.Incremental.hash", "equation_Spec.Hash.Incremental.hash_incremental", "equation_Spec.Hash.Incremental.hash_incremental_body", "equation_Spec.Hash.Incremental.split_blocks", "equation_Spec.Hash.Incremental.update_last", "equation_Spec.Hash.Incremental.update_last_blake", "equation_Spec.Hash.PadFinish.finish", "equation_Spec.Hash.PadFinish.finish_blake", "equation_Spec.Hash.PadFinish.finish_md", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "interpretation_Tm_abs_7db19245573865e2013f96b9787edb72", "interpretation_Tm_abs_b2e90973e02ca16cb7aa657b99901054", "interpretation_Tm_abs_b59e5c7423f648d55dead7e585201d28", "interpretation_Tm_abs_ee58c7759db0726bd389b637e7e7044d", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "kinding_Spec.Hash.Definitions.hash_alg@tok", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "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_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_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_v", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_04f8d70b3f5c8790cd9838aeeee91b78", "refinement_interpretation_Tm_refine_256d797febc66cdef0ee2bba89810870", "refinement_interpretation_Tm_refine_30e6144473b54dee89b03bc9e962cecc", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7", "refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_547240b2475f155577e710689cbdcde0", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_5bb78822eec27c7306876cbb9e7a8ca4", "refinement_interpretation_Tm_refine_6a7ce5ffebe437a8c50d2933ef1a6d01", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_849b4b820be2f8ed1c6d924208decc78", "refinement_interpretation_Tm_refine_8a7310b273ce706888742618619c6357", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955", "refinement_interpretation_Tm_refine_91c352d831715ed604553457a8078865", "refinement_interpretation_Tm_refine_976c9ea07890642a05068e343bf6e5ad", "refinement_interpretation_Tm_refine_9c4e1f4f678d790dba1d07367641b209", "refinement_interpretation_Tm_refine_b4572befa63a13398faa00df7c1f0e57", "refinement_interpretation_Tm_refine_c2f916b98cea21c183e1c8b1e5deeafe", "refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_dc5f9a6f381c17eb82d69a92f2fb5d4c", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e42e5bc038f4e6968f6628cf51c8784e", "refinement_interpretation_Tm_refine_e5296080af465f5dfce37656410bc12d", "refinement_interpretation_Tm_refine_e673e79efef874bfd06939c5abb4ead4", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f302e1c5e7902e028b3edb61ef25df5a", "refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004", "refinement_interpretation_Tm_refine_f90cde0420ffb3b3ce11668f2f8aad38", "refinement_interpretation_Tm_refine_feafe3d31cdfba5960a17b2fc75354e5", "token_correspondence_EverCrypt.Hash.freeable", "token_correspondence_EverCrypt.Hash.state", "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__v", "true_interp", "typing_EverCrypt.Hash.Incremental.block_len", "typing_EverCrypt.Hash.Incremental.hash_len", "typing_EverCrypt.Hash.state_s", "typing_FStar.Ghost.reveal", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt.max_int", "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "typing_Hacl.Streaming.MD.max_input_length64", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.cast", "typing_Lib.IntTypes.maxint", "typing_Lib.IntTypes.op_At_Percent_Dot", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.length", "typing_Spec.AES.gf8", "typing_Spec.Agile.Hash.init", "typing_Spec.Agile.Hash.update_multi", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.max_extra_state", "typing_Spec.Hash.Incremental.hash", "typing_Spec.Hash.Incremental.hash_incremental", "typing_Spec.Hash.Incremental.split_blocks", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2B@tok", "typing_tok_Spec.Blake2.Blake2S@tok", "typing_tok_Spec.Hash.Definitions.Blake2B@tok", "typing_tok_Spec.Hash.Definitions.Blake2S@tok", "unit_inversion" ], 0, "2daa7b353c1435911daf67239e618ea0" ], [ "EverCrypt.Hash.Incremental.create_in", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t", "unit_typing" ], 0, "829bc8acf51a688ba79593018dc426aa" ], [ "EverCrypt.Hash.Incremental.init", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t", "unit_typing" ], 0, "ec62e14791ad538bd9cacdfe164b648c" ], [ "EverCrypt.Hash.Incremental.update", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t" ], 0, "fcfc264966e3dfd270b10bc770bfc10a" ], [ "EverCrypt.Hash.Incremental.finish_st", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t" ], 0, "221d9e469defeb2146cedc3e08e06d25" ], [ "EverCrypt.Hash.Incremental.finish_md5", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t" ], 0, "02205cf216aecdd7ff420f17c6295ace" ], [ "EverCrypt.Hash.Incremental.finish_sha1", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t" ], 0, "1ac279b2e0dc494050b1865e2e1f0009" ], [ "EverCrypt.Hash.Incremental.finish_sha224", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t" ], 0, "ca020c8c14b1c2d1fe14e2cfbebedcac" ], [ "EverCrypt.Hash.Incremental.finish_sha256", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t" ], 0, "a557b5180571e2009360fb0183e73b03" ], [ "EverCrypt.Hash.Incremental.finish_sha384", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t" ], 0, "3cab235bfbd2493cdeb49d1260c5145e" ], [ "EverCrypt.Hash.Incremental.finish_sha512", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t" ], 0, "f86c8ef587a2d6ddd4b5c1bd74f51c2a" ], [ "EverCrypt.Hash.Incremental.finish_blake2s", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t" ], 0, "b9c2011db3b6e9925dc20d6afe3032df" ], [ "EverCrypt.Hash.Incremental.finish_blake2b", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t" ], 0, "8bca1110f799c409020462e2ddbb17c0" ], [ "EverCrypt.Hash.Incremental.alg_of_state", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t" ], 0, "8692f9854976121233ba2730dca88df6" ], [ "EverCrypt.Hash.Incremental.finish", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t" ], 0, "d7f2abd14d1e179fa2aac2b5a2a63f55" ], [ "EverCrypt.Hash.Incremental.finish", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit", "disc_equation_Spec.Hash.Definitions.Blake2B", "disc_equation_Spec.Hash.Definitions.Blake2S", "disc_equation_Spec.Hash.Definitions.MD5", "disc_equation_Spec.Hash.Definitions.SHA1", "disc_equation_Spec.Hash.Definitions.SHA2_224", "disc_equation_Spec.Hash.Definitions.SHA2_256", "disc_equation_Spec.Hash.Definitions.SHA2_384", "disc_equation_Spec.Hash.Definitions.SHA2_512", "equation_Prims.nat", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_3792018f3bdd3cbbd9046b0a6ecae94b", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56af1e7994ff0aaa68ff9d2ad4090d42", "refinement_interpretation_Tm_refine_572be1aea4ca0cca2c3b0e3eb5cc2f98", "refinement_interpretation_Tm_refine_7d05d510ddde8c1c284cbb5648d4590f", "refinement_interpretation_Tm_refine_9daad2c2b91f611cd6351a627da92b9d", "refinement_interpretation_Tm_refine_9dba2c65a575f145d966f192cf47b851", "refinement_interpretation_Tm_refine_bf647634ec99edd15ba9bbca9f458d54", "refinement_interpretation_Tm_refine_c71fe479e0df26e839ee8ac4bef84a3f", "refinement_interpretation_Tm_refine_f6f2e281936060aef7e8e8c8673c0138", "refinement_interpretation_Tm_refine_feec09ab983c546c6618f0b99f633bbb", "typing_Spec.Hash.Definitions.word_length" ], 0, "2fbfe95cc754d433f95fc5db5bb586d6" ], [ "EverCrypt.Hash.Incremental.free", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t" ], 0, "7c95cc6c68cc92da626da179651eec87" ], [ "EverCrypt.Hash.Incremental.state", 1, 0, 0, [ "@query", "constructor_distinct_Hacl.Streaming.Interface.Erased", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "function_token_typing_EverCrypt.Hash.state", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "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", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "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", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t" ], 0, "1eb736b3e585023ad1785b93f6ad91fe" ] ] ]