[ "7$hl\u0001\u00025D\u0001", [ [ "EverCrypt.Hash.uu___1", 1, 0, 0, [ "@query" ], 0, "4684c9fc03447af08518fc9c3d4e2172" ], [ "EverCrypt.Hash.string_of_alg", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "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_EverCrypt.Hash.uu___1", "equation_Prims.squash", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "inversion-interp", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "f15013ef988fc1c7aa849e8346ca9cd6" ], [ "EverCrypt.Hash.broken_alg", 1, 0, 0, [ "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq" ], 0, "f879c2b16b9a3c5c1444edc731d79ac0" ], [ "EverCrypt.Hash.alg13", 1, 0, 0, [ "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq" ], 0, "6798f685bd0fc805de336ad36bd86eb1" ], [ "EverCrypt.Hash.uint32_fits_maxLength", 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_EverCrypt.Hash.uu___1", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.minint", "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.max_input_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "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", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.v", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "e159341e6a5abbfa11d0cd011a07a971" ], [ "EverCrypt.Hash.impl_of_alg", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.blake2_spec", "equation_EverCrypt.Hash.uu___1", "equation_Hacl.Hash.Definitions.m_spec", "equation_Prims.squash", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "inversion-interp", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_tok_Hacl.Impl.Blake2.Core.M32@tok", "unit_typing" ], 0, "38752c043f7ab37825d5fc48f4760bf6" ], [ "EverCrypt.Hash.__proj__MD5_s__item__p", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_EverCrypt.Hash.MD5_s", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_8007cc95e31283ec70894170e620c8b9" ], 0, "5fe7a1924133061264dbbc92dc8ccecb" ], [ "EverCrypt.Hash.__proj__SHA1_s__item__p", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_EverCrypt.Hash.SHA1_s", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_365674ad36822dbcb25c1243141f7b4a" ], 0, "4ce15b1ba001c08e62eba0af01d15a06" ], [ "EverCrypt.Hash.__proj__SHA2_224_s__item__p", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_EverCrypt.Hash.SHA2_224_s", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_ca18a58ab4d414f80248e3f3a4fb8b38" ], 0, "b831cfe0d142de43fb0c55d2a6bcb5d2" ], [ "EverCrypt.Hash.__proj__SHA2_256_s__item__p", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_EverCrypt.Hash.SHA2_256_s", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_c03ee29b1b15c93d78f1ddc22e14ee9e" ], 0, "5df326aaf9c097d477996209a97a821b" ], [ "EverCrypt.Hash.__proj__SHA2_384_s__item__p", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_EverCrypt.Hash.SHA2_384_s", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_99efc18aeab03ed24138e5c951959832" ], 0, "111a61f79126f41500b033cdd791991e" ], [ "EverCrypt.Hash.__proj__SHA2_512_s__item__p", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_EverCrypt.Hash.SHA2_512_s", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_3d72f362bdb97a0947d9a19041fd4bda" ], 0, "3a066dfa39e33b59dd7736602423e6cd" ], [ "EverCrypt.Hash.__proj__Blake2S_s__item__p", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_99517f988c380052b461abe7945fbc1f" ], 0, "d0711d6b685c29ea49c35f6d7ca1cdcb" ], [ "EverCrypt.Hash.__proj__Blake2B_s__item__p", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_bc7b15f64287acf30f25ad86e60fff67" ], 0, "bfa5651ea2db3a1ba9cee2f99e4871dd" ], [ "EverCrypt.Hash.mk_state_s", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.uu___1", "equation_Hacl.Hash.Definitions.state", "equation_Prims.squash", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "inversion-interp", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b" ], 0, "d49b412ed9988d4fb87c905c89906fa3" ], [ "EverCrypt.Hash.p", 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.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", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_elim_EverCrypt.Hash.Blake2B_s", "data_elim_EverCrypt.Hash.Blake2S_s", "data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s", "data_elim_EverCrypt.Hash.SHA2_224_s", "data_elim_EverCrypt.Hash.SHA2_256_s", "data_elim_EverCrypt.Hash.SHA2_384_s", "data_elim_EverCrypt.Hash.SHA2_512_s", "disc_equation_EverCrypt.Hash.Blake2B_s", "disc_equation_EverCrypt.Hash.Blake2S_s", "disc_equation_EverCrypt.Hash.MD5_s", "disc_equation_EverCrypt.Hash.SHA1_s", "disc_equation_EverCrypt.Hash.SHA2_224_s", "disc_equation_EverCrypt.Hash.SHA2_256_s", "disc_equation_EverCrypt.Hash.SHA2_384_s", "disc_equation_EverCrypt.Hash.SHA2_512_s", "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_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.impl_of_alg", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.state", "fuel_guarded_inversion_EverCrypt.Hash.state_s", "inversion-interp", "lemma_EverCrypt.Hash.invert_state_s", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Prims.Mkdtuple2__1", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b" ], 0, "7637049347aa7cb866173b0ce84a8932" ], [ "EverCrypt.Hash.loc_includes_union_l_footprint_s", 1, 0, 0, [ "@query" ], 0, "fd8db0cdcd1d933a2a9acf02819394b8" ], [ "EverCrypt.Hash.invariant", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_EverCrypt.Hash.state", "equation_LowStar.Buffer.pointer", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e" ], 0, "ff5d4b279ce1b9f33f5f98fb12f2311a" ], [ "EverCrypt.Hash.repr", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "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_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.state", "equation_EverCrypt.Hash.uu___1", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.impl", "equation_LowStar.Buffer.pointer", "equation_Prims.squash", "equation_Spec.Hash.Definitions.words_state_", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "inversion-interp", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Prims.Mkdtuple2__1", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "typing_EverCrypt.Hash.impl_of_alg" ], 0, "05a7f6f273b0a7234b0bf2179660263d" ], [ "EverCrypt.Hash.repr_with_counter", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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.U8", "constructor_distinct_Spec.Blake2.Blake2B", "disc_equation_Lib.IntTypes.SEC", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equation_EverCrypt.Hash.state", "equation_EverCrypt.Hash.uu___1", "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_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.is_blake", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "function_token_typing_FStar.Monotonic.Heap.heap", "inversion-interp", "kinding_EverCrypt.Hash.state_s@tok", "lemma_FStar.Map.lemma_ContainsDom", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_3afef912859361e9884ab51f5c9deddb", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Spec.Blake2.Blake2B@tok", "unit_typing" ], 0, "4640f9e4d49e4a3923c1807876bee274" ], [ "EverCrypt.Hash.alg_of_state", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_EverCrypt.Hash.Blake2B_s", "constructor_distinct_EverCrypt.Hash.Blake2S_s", "constructor_distinct_EverCrypt.Hash.MD5_s", "constructor_distinct_EverCrypt.Hash.SHA1_s", "constructor_distinct_EverCrypt.Hash.SHA2_224_s", "constructor_distinct_EverCrypt.Hash.SHA2_256_s", "constructor_distinct_EverCrypt.Hash.SHA2_384_s", "constructor_distinct_EverCrypt.Hash.SHA2_512_s", "data_elim_EverCrypt.Hash.Blake2B_s", "data_elim_EverCrypt.Hash.Blake2S_s", "data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s", "data_elim_EverCrypt.Hash.SHA2_224_s", "data_elim_EverCrypt.Hash.SHA2_256_s", "data_elim_EverCrypt.Hash.SHA2_384_s", "data_elim_EverCrypt.Hash.SHA2_512_s", "disc_equation_EverCrypt.Hash.Blake2B_s", "disc_equation_EverCrypt.Hash.Blake2S_s", "disc_equation_EverCrypt.Hash.MD5_s", "disc_equation_EverCrypt.Hash.SHA1_s", "disc_equation_EverCrypt.Hash.SHA2_224_s", "disc_equation_EverCrypt.Hash.SHA2_256_s", "disc_equation_EverCrypt.Hash.SHA2_384_s", "disc_equation_EverCrypt.Hash.SHA2_512_s", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.invariant", "fuel_guarded_inversion_EverCrypt.Hash.state_s", "inversion-interp", "kinding_Spec.Hash.Definitions.hash_alg@tok", "lemma_EverCrypt.Hash.invert_state_s", "projection_inverse_BoxBool_proj_0", "projection_inverse_EverCrypt.Hash.Blake2B_s_p", "projection_inverse_EverCrypt.Hash.Blake2S_s_p", "projection_inverse_EverCrypt.Hash.MD5_s_p", "projection_inverse_EverCrypt.Hash.SHA1_s_p", "projection_inverse_EverCrypt.Hash.SHA2_224_s_p", "projection_inverse_EverCrypt.Hash.SHA2_256_s_p", "projection_inverse_EverCrypt.Hash.SHA2_384_s_p", "projection_inverse_EverCrypt.Hash.SHA2_512_s_p", "refinement_interpretation_Tm_refine_976c9ea07890642a05068e343bf6e5ad", "typing_FStar.Ghost.reveal" ], 0, "119c8f74fa9872cc4cc2ea3adca1528c" ], [ "EverCrypt.Hash.fresh_is_disjoint", 1, 0, 0, [ "@query", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.loc_in", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2" ], 0, "6ed80e947d0ac5f3128383a81adcefa1" ], [ "EverCrypt.Hash.invariant_loc_in_footprint", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_typing", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.Hash.footprint", "equation_EverCrypt.Hash.footprint_s", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p", "equation_EverCrypt.Hash.state", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Monotonic.Buffer.get", "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_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "kinding_EverCrypt.Hash.state_s@tok", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.impl_of_alg", "typing_EverCrypt.Hash.p", "typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.impl_word", "typing_Lib.IntTypes.minint", "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_not_unused_in", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "4cbbad5c06f821341ed23b3ac9711151" ], [ "EverCrypt.Hash.frame_invariant", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "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_Hacl.Impl.Blake2.Core.M128", "constructor_distinct_Hacl.Impl.Blake2.Core.M256", "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.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", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "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_Hacl.Impl.Blake2.Core.M32@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", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.blake2_spec", "equation_EverCrypt.Hash.footprint", "equation_EverCrypt.Hash.footprint_s", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p", "equation_EverCrypt.Hash.repr", "equation_EverCrypt.Hash.repr_eq", "equation_EverCrypt.Hash.state", "equation_EverCrypt.Helpers.uint32_t", "equation_EverCrypt.Helpers.uint64_t", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_32", "equation_FStar.Integers.uint_64", "equation_Hacl.Hash.Definitions.as_seq", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.get_spec", "equation_Hacl.Hash.Definitions.impl", "equation_Hacl.Hash.Definitions.impl_state_length", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.m_spec", "equation_Hacl.Hash.Definitions.state", "equation_Hacl.Impl.Blake2.Core.element_t", "equation_Hacl.Impl.Blake2.Core.word_t", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state_", "fuel_guarded_inversion_EverCrypt.Hash.state_s", "fuel_guarded_inversion_Prims.dtuple2", "function_token_typing_FStar.Integers.uint_32", "function_token_typing_FStar.Integers.uint_64", "function_token_typing_Lib.IntTypes.pub_uint64", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "inversion-interp", "kinding_EverCrypt.Hash.state_s@tok", "lemma_EverCrypt.Hash.invert_state_s", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_Hacl.Impl.Blake2.Core.state_v_eq_lemma", "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", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.Hash.blake2_spec", "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.impl_of_alg", "typing_EverCrypt.Hash.p", "typing_EverCrypt.Hash.repr", "typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.impl_word", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.word", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Blake2.Blake2B@tok", "typing_tok_Spec.Blake2.Blake2S@tok" ], 0, "b799115900c871b6cd03f70b51c5e85b" ], [ "EverCrypt.Hash.frame_invariant_implies_footprint_preservation", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing", "equation_EverCrypt.Hash.footprint", "equation_EverCrypt.Hash.invariant", "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", "kinding_EverCrypt.Hash.state_s@tok", "lemma_FStar.Map.lemma_ContainsDom", "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", "projection_inverse_BoxInt_proj_0", "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_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, "41a6898152714f02c5e276880018f509" ], [ "EverCrypt.Hash.alloca", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Hacl.Impl.Blake2.Core_pretyping_738bced230d07a53885c00814ce7f1ee", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "b2t_def", "bool_inversion", "constructor_distinct_EverCrypt.Hash.Blake2B_s", "constructor_distinct_EverCrypt.Hash.Blake2S_s", "constructor_distinct_EverCrypt.Hash.MD5_s", "constructor_distinct_EverCrypt.Hash.SHA1_s", "constructor_distinct_EverCrypt.Hash.SHA2_224_s", "constructor_distinct_EverCrypt.Hash.SHA2_256_s", "constructor_distinct_EverCrypt.Hash.SHA2_384_s", "constructor_distinct_EverCrypt.Hash.SHA2_512_s", "constructor_distinct_FStar.Integers.Unsigned", "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.S8", "constructor_distinct_Lib.IntTypes.SEC", "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", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_elim_EverCrypt.Hash.MD5_s", "disc_equation_Lib.IntTypes.U128", "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", "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.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", "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", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.blake2_spec", "equation_EverCrypt.Hash.footprint", "equation_EverCrypt.Hash.footprint_s", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p", "equation_EverCrypt.Hash.state", "equation_EverCrypt.Hash.uu___1", "equation_EverCrypt.Helpers.uint64_t", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_64", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_stack_region", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.mul_mod", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.get_spec", "equation_Hacl.Hash.Definitions.impl_state_length", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.m_spec", "equation_Hacl.Hash.Definitions.state", "equation_Hacl.Impl.Blake2.Core.element_t", "equation_Hacl.Impl.Blake2.Core.row_len", "equation_Hacl.Impl.Blake2.Core.word_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mul_mod", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.loc_in", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "function_token_typing_FStar.Integers.uint_64", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.pub_uint64", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint32", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "inversion-interp", "kinding_EverCrypt.Hash.state_s@tok", "lemma_EverCrypt.Hash.invariant_loc_in_footprint", "lemma_EverCrypt.Hash.invert_state_s", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_addresses", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_1", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_addresses_", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "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_AmpAmp", "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_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_EverCrypt.Hash.Blake2B_s_p", "projection_inverse_EverCrypt.Hash.Blake2S_s_p", "projection_inverse_EverCrypt.Hash.MD5_s_p", "projection_inverse_EverCrypt.Hash.SHA1_s_p", "projection_inverse_EverCrypt.Hash.SHA2_224_s_p", "projection_inverse_EverCrypt.Hash.SHA2_256_s_p", "projection_inverse_EverCrypt.Hash.SHA2_384_s_p", "projection_inverse_EverCrypt.Hash.SHA2_512_s_p", "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_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_04eb755918cc11ccb5ae797e4500022c", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_09436ce1290d28cf92127b462e44babc", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_1bf02e9005a95b18ff0faba06f7dc87d", "refinement_interpretation_Tm_refine_1f97e6da8961faf277e1838ec84a85ed", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_48c1b5b4c02ad49f0760911a9d4b1fb4", "refinement_interpretation_Tm_refine_49cc39cb50c458a93564b0ab0a76913f", "refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8618df86656cf4c2bc98614452120307", "refinement_interpretation_Tm_refine_8db0302ca776c13bdca82b6705afa876", "refinement_interpretation_Tm_refine_8eaf80b6dc4ba7a97184cff448003a7e", "refinement_interpretation_Tm_refine_a50b3723327a6ede703df9aaf02fdc9f", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_interpretation_Tm_refine_cc7a5fb63cf1977ab55eb280405688d3", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.impl_of_alg", "typing_EverCrypt.Hash.p", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Seq.Base.index", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "typing_FStar.UInt32.mul_mod", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_FStar.UInt64.uint_to_t", "typing_Hacl.Hash.Definitions.impl_word", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mul_mod", "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.get", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_addresses", "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_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Hacl.Impl.Blake2.Core.M32@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Blake2.Blake2S@tok", "typing_tok_Spec.Hash.Definitions.Blake2B@tok", "typing_tok_Spec.Hash.Definitions.Blake2S@tok", "typing_tok_Spec.Hash.Definitions.MD5@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "typing_tok_Spec.Hash.Definitions.SHA2_384@tok", "typing_tok_Spec.Hash.Definitions.SHA2_512@tok" ], 0, "877644cf3164dae97cd208ed9a81d19c" ], [ "EverCrypt.Hash.create_in", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Hacl.Impl.Blake2.Core_pretyping_738bced230d07a53885c00814ce7f1ee", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "Spec.Hash.Definitions_interpretation_Tm_arrow_3ac874e39b1c409ba69a2358a6f73691", "b2t_def", "bool_inversion", "constructor_distinct_EverCrypt.Hash.Blake2B_s", "constructor_distinct_EverCrypt.Hash.Blake2S_s", "constructor_distinct_EverCrypt.Hash.MD5_s", "constructor_distinct_EverCrypt.Hash.SHA1_s", "constructor_distinct_EverCrypt.Hash.SHA2_224_s", "constructor_distinct_EverCrypt.Hash.SHA2_256_s", "constructor_distinct_EverCrypt.Hash.SHA2_384_s", "constructor_distinct_EverCrypt.Hash.SHA2_512_s", "constructor_distinct_FStar.Integers.Unsigned", "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_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.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", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_typing_intro_Prims.Mkdtuple2@tok", "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", "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_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", "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", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.blake2_spec", "equation_EverCrypt.Hash.footprint", "equation_EverCrypt.Hash.footprint_s", "equation_EverCrypt.Hash.freeable", "equation_EverCrypt.Hash.freeable_s", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p", "equation_EverCrypt.Hash.state", "equation_EverCrypt.Hash.uu___1", "equation_EverCrypt.Helpers.uint32_t", "equation_EverCrypt.Helpers.uint64_t", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.HyperStack.ST.is_eternal_region", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_32", "equation_FStar.Integers.uint_64", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_heap_color", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.mul_mod", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.get_spec", "equation_Hacl.Hash.Definitions.impl", "equation_Hacl.Hash.Definitions.impl_state_length", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.m_spec", "equation_Hacl.Hash.Definitions.state", "equation_Hacl.Impl.Blake2.Core.element_t", "equation_Hacl.Impl.Blake2.Core.row_len", "equation_Hacl.Impl.Blake2.Core.word_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mul_mod", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "function_token_typing_FStar.Integers.uint_32", "function_token_typing_FStar.Integers.uint_64", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.pub_uint64", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "interpretation_Tm_abs_3d77c1d80c0e9e736cdcf018f4780b14", "inversion-interp", "kinding_EverCrypt.Hash.state_s@tok", "kinding_Spec.Hash.Definitions.hash_alg@tok", "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.Base.lemma_index_create", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.freeable_length", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_addresses", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_1", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_addresses_", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "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_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_EverCrypt.Hash.Blake2B_s_p", "projection_inverse_EverCrypt.Hash.Blake2S_s_p", "projection_inverse_EverCrypt.Hash.MD5_s_p", "projection_inverse_EverCrypt.Hash.SHA1_s_p", "projection_inverse_EverCrypt.Hash.SHA2_224_s_p", "projection_inverse_EverCrypt.Hash.SHA2_256_s_p", "projection_inverse_EverCrypt.Hash.SHA2_384_s_p", "projection_inverse_EverCrypt.Hash.SHA2_512_s_p", "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_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_11a4f514eb4019327c6ce0d76a497764", "refinement_interpretation_Tm_refine_161e04719814801d293219f408210f95", "refinement_interpretation_Tm_refine_1f0b16ffe58d86a53a46319a2e5393a8", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_38669dac8bbbff1dfe23c07235ff0361", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_48c1b5b4c02ad49f0760911a9d4b1fb4", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8618df86656cf4c2bc98614452120307", "refinement_interpretation_Tm_refine_8bf8568fba1c5a91cf6130f7c28490de", "refinement_interpretation_Tm_refine_8f1089fa80a08423d7748a8368e610a3", "refinement_interpretation_Tm_refine_a6f4eaa35333a2521a7470f02bece5a4", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e674d1c7a673a293de1d272a02b82189", "refinement_interpretation_Tm_refine_e8554027bd7fdca2b80730414ef2f9ce", "refinement_interpretation_Tm_refine_e9c5fb85d1557055895bcdfc213e38da", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.Hash.blake2_spec", "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.impl_of_alg", "typing_EverCrypt.Hash.p", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.color", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.is_heap_color", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "typing_FStar.UInt32.mul_mod", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt64.uint_to_t", "typing_Hacl.Hash.Definitions.get_spec", "typing_Hacl.Hash.Definitions.impl_state_length", "typing_Hacl.Hash.Definitions.impl_word", "typing_Hacl.Impl.Blake2.Core.row_len", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.get", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_addresses", "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_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Tm_abs_3d77c1d80c0e9e736cdcf018f4780b14", "typing_tok_Hacl.Impl.Blake2.Core.M32@tok", "typing_tok_Lib.IntTypes.U8@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", "typing_tok_Spec.Hash.Definitions.MD5@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "typing_tok_Spec.Hash.Definitions.SHA2_384@tok", "typing_tok_Spec.Hash.Definitions.SHA2_512@tok" ], 0, "db78d78b441c5e1c3945edf2626798ff" ], [ "EverCrypt.Hash.create", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_FStar.HyperStack.ST.is_eternal_region", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_heap_color", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "function_token_typing_FStar.Monotonic.Heap.heap", "lemma_FStar.Map.lemma_ContainsDom", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_f759b00d0ea3017d744ed132c2ce48f4", "typing_FStar.Map.contains", "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" ], 0, "3b896087013107dd60f7605afa242a4d" ], [ "EverCrypt.Hash.init", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "bool_typing", "constructor_distinct_EverCrypt.Hash.Blake2B_s", "constructor_distinct_EverCrypt.Hash.Blake2S_s", "constructor_distinct_EverCrypt.Hash.MD5_s", "constructor_distinct_EverCrypt.Hash.SHA1_s", "constructor_distinct_EverCrypt.Hash.SHA2_224_s", "constructor_distinct_EverCrypt.Hash.SHA2_256_s", "constructor_distinct_EverCrypt.Hash.SHA2_384_s", "constructor_distinct_EverCrypt.Hash.SHA2_512_s", "constructor_distinct_FStar.Integers.Unsigned", "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_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.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", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_elim_EverCrypt.Hash.Blake2B_s", "data_elim_EverCrypt.Hash.Blake2S_s", "data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s", "data_elim_EverCrypt.Hash.SHA2_224_s", "data_elim_EverCrypt.Hash.SHA2_256_s", "data_elim_EverCrypt.Hash.SHA2_384_s", "data_elim_EverCrypt.Hash.SHA2_512_s", "data_typing_intro_Spec.Blake2.Blake2B@tok", "disc_equation_EverCrypt.Hash.Blake2B_s", "disc_equation_EverCrypt.Hash.Blake2S_s", "disc_equation_EverCrypt.Hash.MD5_s", "disc_equation_EverCrypt.Hash.SHA1_s", "disc_equation_EverCrypt.Hash.SHA2_224_s", "disc_equation_EverCrypt.Hash.SHA2_256_s", "disc_equation_EverCrypt.Hash.SHA2_384_s", "disc_equation_EverCrypt.Hash.SHA2_512_s", "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_Hacl.Impl.Blake2.Core.M32@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", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.blake2_spec", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.footprint", "equation_EverCrypt.Hash.footprint_s", "equation_EverCrypt.Hash.freeable", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p", "equation_EverCrypt.Hash.preserves_freeable", "equation_EverCrypt.Hash.repr", "equation_EverCrypt.Hash.state", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_32", "equation_FStar.Integers.uint_64", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Pervasives.Native.fst", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.get_spec", "equation_Hacl.Hash.Definitions.impl", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.m_spec", "equation_Hacl.Hash.Definitions.state", "equation_Hacl.Impl.Blake2.Core.element_t", "equation_Hacl.Impl.Blake2.Core.word_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "fuel_guarded_inversion_EverCrypt.Hash.state_s", "fuel_guarded_inversion_Prims.dtuple2", "function_token_typing_FStar.Integers.uint_32", "function_token_typing_FStar.Integers.uint_64", "function_token_typing_Lib.IntTypes.pub_uint64", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "kinding_EverCrypt.Hash.state_s@tok", "kinding_Spec.Hash.Definitions.hash_alg@tok", "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_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_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_EverCrypt.Hash.Blake2B_s_p", "projection_inverse_EverCrypt.Hash.Blake2S_s_p", "projection_inverse_EverCrypt.Hash.MD5_s_p", "projection_inverse_EverCrypt.Hash.SHA1_s_p", "projection_inverse_EverCrypt.Hash.SHA2_224_s_p", "projection_inverse_EverCrypt.Hash.SHA2_256_s_p", "projection_inverse_EverCrypt.Hash.SHA2_384_s_p", "projection_inverse_EverCrypt.Hash.SHA2_512_s_p", "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_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_36405dc5122bcdebe15723f1ee36a7b7", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4a250fae5c49229cf6bcc6a3069b80a8", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_8bc4e8f6e7ee09cbaa619d7dc4ee7b68", "refinement_interpretation_Tm_refine_976c9ea07890642a05068e343bf6e5ad", "refinement_interpretation_Tm_refine_9b1af48c1c55d17658e70eb2e7ad8075", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_ae3bc7fb874520269d69f03dfc4338e9", "refinement_interpretation_Tm_refine_baa9b5e7d2a6c97ee3007420baeb55fe", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_eea4feac1b785fce2f85492feeb100bc", "refinement_interpretation_Tm_refine_fbd0051d8d71ed03a228291982b893b2", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.Hash.footprint", "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.impl_of_alg", "typing_EverCrypt.Hash.p", "typing_FStar.Ghost.reveal", "typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.impl_word", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "a19509bd2029b66cff89122f3e94cf7b" ], [ "EverCrypt.Hash.k224_256", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_FStar.HyperStack.ST.is_eternal_region", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_heap_color", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "function_token_typing_FStar.Monotonic.Heap.heap", "lemma_FStar.Map.lemma_ContainsDom", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "typing_FStar.Map.contains", "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" ], 0, "d725e1f5e07cd944d867035243494d98" ], [ "EverCrypt.Hash.update_multi_256", 1, 0, 1, [ "@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_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "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", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "data_elim_FStar.Pervasives.Native.Mktuple2", "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_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.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.List.Tot.Properties.llist", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Preorder.preorder", "equation_FStar.Preorder.preorder_rel", "equation_FStar.Preorder.reflexive", "equation_Hacl.Hash.Definitions.as_seq", "equation_Hacl.Hash.Definitions.blocks_t", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.impl_state_length", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.ImmutableBuffer.immutable_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.op_Equals_Equals_Equals", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.Hash.update_multi", "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.state_word_length", "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.Definitions.words_state_", "equation_Spec.SHA2.Constants.k224_256", "equation_Vale.SHA.SHA_helpers.update_multi_transparent", "equation_Vale.SHA.SHA_helpers.word", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint32", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "interpretation_Tm_abs_b4ae3c8c313abed48b0c4141f8bc0016", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_Lib.IntTypes.v_injective", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Multiply", "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_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_3d4756c3efe273f271dc1668fa35a481", "refinement_interpretation_Tm_refine_616c81ebdee36baf7859f9a6257c731f", "refinement_interpretation_Tm_refine_6c495072e3dce62928f27adb19242e1b", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_a80eb2ed78152ea57ef9b8fd6a9e440d", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_bd10f09297e0e7dc08314f7d9211801c", "refinement_interpretation_Tm_refine_c3ebb95ccaafd1d34ce4f1080016cf61", "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b", "refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f4235ca35aeb7ebf867cf38b99ce6272", "refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004", "refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d", "typing_EverCrypt.Hash.k224_256", "typing_FStar.Pervasives.Native.fst", "typing_FStar.Seq.Properties.seq_of_list", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.ImmutableBuffer.immutable_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.AES.gf8", "typing_Spec.Agile.Hash.update_multi", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.extra_state", "typing_Spec.Hash.Definitions.word", "typing_Spec.Hash.Definitions.words_state_", "typing_Spec.SHA2.Constants.k224_256_l", "typing_Vale.Arch.BufferFriend.of_bytes", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "unit_inversion", "unit_typing" ], 0, "6d6c33d0d521dfcdf6a239fdeede2899" ], [ "EverCrypt.Hash.update_multi_224", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "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.S8", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "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.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_EverCrypt.Helpers.uint8_t", "equation_Hacl.Hash.Definitions.as_seq", "equation_Hacl.Hash.Definitions.blocks_t", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.impl_state_length", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.state_word_length", "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.Definitions.words_state_", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__a", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_5f99f4ca216fafb8ab5462a12ca7dbeb", "refinement_interpretation_Tm_refine_66c124f492ec193d4bbaa9a39421d6d4", "refinement_interpretation_Tm_refine_a80eb2ed78152ea57ef9b8fd6a9e440d", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f4235ca35aeb7ebf867cf38b99ce6272", "typing_LowStar.Buffer.trivial_preorder", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.word", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "unit_inversion", "unit_typing" ], 0, "0bcf27f366a59aac8f3975792093e34c" ], [ "EverCrypt.Hash.update2", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "function_token_typing_Lib.IntTypes.uint8", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "refinement_interpretation_Tm_refine_ee5e5ea36a8ac8879a333964d971b753", "typing_LowStar.Buffer.trivial_preorder" ], 0, "db72b806daf88f0d8ed20efd9553def1" ], [ "EverCrypt.Hash.update2", 2, 1, 1, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "Spec.Hash.Definitions_interpretation_Tm_arrow_3ac874e39b1c409ba69a2358a6f73691", "bool_typing", "constructor_distinct_EverCrypt.Hash.Blake2B_s", "constructor_distinct_EverCrypt.Hash.Blake2S_s", "constructor_distinct_EverCrypt.Hash.MD5_s", "constructor_distinct_EverCrypt.Hash.SHA1_s", "constructor_distinct_EverCrypt.Hash.SHA2_224_s", "constructor_distinct_EverCrypt.Hash.SHA2_256_s", "constructor_distinct_EverCrypt.Hash.SHA2_384_s", "constructor_distinct_EverCrypt.Hash.SHA2_512_s", "constructor_distinct_FStar.Integers.Unsigned", "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_Hacl.Impl.Blake2.Core.M128", "constructor_distinct_Hacl.Impl.Blake2.Core.M32", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S128", "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", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_elim_EverCrypt.Hash.Blake2B_s", "data_elim_EverCrypt.Hash.Blake2S_s", "data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s", "data_elim_EverCrypt.Hash.SHA2_224_s", "data_elim_EverCrypt.Hash.SHA2_256_s", "data_elim_EverCrypt.Hash.SHA2_384_s", "data_elim_EverCrypt.Hash.SHA2_512_s", "data_elim_Prims.Mkdtuple2", "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok", "data_typing_intro_Lib.IntTypes.U8@tok", "data_typing_intro_Spec.Blake2.Blake2B@tok", "disc_equation_EverCrypt.Hash.Blake2B_s", "disc_equation_EverCrypt.Hash.Blake2S_s", "disc_equation_EverCrypt.Hash.MD5_s", "disc_equation_EverCrypt.Hash.SHA1_s", "disc_equation_EverCrypt.Hash.SHA2_224_s", "disc_equation_EverCrypt.Hash.SHA2_256_s", "disc_equation_EverCrypt.Hash.SHA2_384_s", "disc_equation_EverCrypt.Hash.SHA2_512_s", "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_Hacl.Impl.Blake2.Core.M32@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", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.blake2_spec", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.footprint", "equation_EverCrypt.Hash.footprint_s", "equation_EverCrypt.Hash.freeable", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p", "equation_EverCrypt.Hash.preserves_freeable", "equation_EverCrypt.Hash.repr", "equation_EverCrypt.Hash.repr_with_counter", "equation_EverCrypt.Hash.state", "equation_EverCrypt.Hash.uu___1", "equation_EverCrypt.Helpers.uint32_t", "equation_EverCrypt.Helpers.uint64_t", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Int.Cast.Full.uint64_to_uint128", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_32", "equation_FStar.Integers.uint_64", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Pervasives.Native.fst", "equation_FStar.UInt128.n", "equation_Hacl.Hash.Definitions.as_seq", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.get_spec", "equation_Hacl.Hash.Definitions.impl", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.m_spec", "equation_Hacl.Hash.Definitions.state", "equation_Hacl.Impl.Blake2.Core.element_t", "equation_Hacl.Impl.Blake2.Core.word_t", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.cast", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.Hash.update", "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_block", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.to_blake_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_EverCrypt.Hash.state_s", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "function_token_typing_FStar.Integers.uint_32", "function_token_typing_FStar.Integers.uint_64", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.pub_uint64", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "interpretation_Tm_abs_3d77c1d80c0e9e736cdcf018f4780b14", "interpretation_Tm_abs_e3e4e6e500ae76ff6ad28ada6503a771", "inversion-interp", "kinding_EverCrypt.Hash.state_s@tok", "kinding_Spec.Hash.Definitions.hash_alg@tok", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_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_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_Spec.Hash.Lemmas.update_multi_update", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "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_EverCrypt.Hash.Blake2B_s_p", "projection_inverse_EverCrypt.Hash.Blake2S_s_p", "projection_inverse_EverCrypt.Hash.MD5_s_p", "projection_inverse_EverCrypt.Hash.SHA1_s_p", "projection_inverse_EverCrypt.Hash.SHA2_224_s_p", "projection_inverse_EverCrypt.Hash.SHA2_256_s_p", "projection_inverse_EverCrypt.Hash.SHA2_384_s_p", "projection_inverse_EverCrypt.Hash.SHA2_512_s_p", "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_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_313945d6e5dd9a1523b4f94bb56574eb", "refinement_interpretation_Tm_refine_375faf8fecbf524a5532f0557c79dc73", "refinement_interpretation_Tm_refine_37c93ce5bbd59eacadc2b1f547360369", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_66c124f492ec193d4bbaa9a39421d6d4", "refinement_interpretation_Tm_refine_7792679b3c450daf2a53ac4df195b5eb", "refinement_interpretation_Tm_refine_78db224f600b3acabdab42a044183b6c", "refinement_interpretation_Tm_refine_89555d185e6377fffaa1db1c14e08385", "refinement_interpretation_Tm_refine_a803b759f08d41207c176c52e6485f20", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_c2f916b98cea21c183e1c8b1e5deeafe", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_ee5e5ea36a8ac8879a333964d971b753", "refinement_interpretation_Tm_refine_f4235ca35aeb7ebf867cf38b99ce6272", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Spec.Agile.Hash.update", "typing_EverCrypt.Hash.footprint", "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.impl_of_alg", "typing_EverCrypt.Hash.p", "typing_EverCrypt.Hash.repr_with_counter", "typing_FStar.Ghost.reveal", "typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.as_seq", "typing_Hacl.Hash.Definitions.impl_word", "typing_Lib.IntTypes.unsigned", "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.len", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.words_state_", "typing_Tm_abs_3d77c1d80c0e9e736cdcf018f4780b14", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Hash.Definitions.Blake2S@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "typing_tok_Spec.Hash.Definitions.SHA2_384@tok", "typing_tok_Spec.Hash.Definitions.SHA2_512@tok" ], 0, "a53f20dbac10100b5148143e35411cd6" ], [ "EverCrypt.Hash.update", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.is_md", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_26ad11f87673edceb28824c1006925f0", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_ee5e5ea36a8ac8879a333964d971b753", "typing_LowStar.Buffer.trivial_preorder", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "unit_typing" ], 0, "843f0a5e35bebda60eb8b97ef2a89e52" ], [ "EverCrypt.Hash.update", 2, 0, 0, [ "@MaxIFuel_assumption", "@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.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "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_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.repr_with_counter", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.is_md", "kinding_Spec.Hash.Definitions.hash_alg@tok", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "refinement_interpretation_Tm_refine_26ad11f87673edceb28824c1006925f0", "typing_FStar.Ghost.reveal", "typing_Spec.Hash.Definitions.is_md" ], 0, "2293ee157d395120a20683d55f932d26" ], [ "EverCrypt.Hash.update_multi2", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "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.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "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_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_83e1a0ed8e967940f825c40ec86a30c4", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "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, "88efb11fb6af6dbebc8bf058e6b6a895" ], [ "EverCrypt.Hash.update_multi2", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_EverCrypt.Hash.e_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "kinding_Spec.Hash.Definitions.hash_alg@tok", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "typing_FStar.Ghost.reveal" ], 0, "ed2f6c79799a653ad72fd6fb004b5b1c" ], [ "EverCrypt.Hash.update_multi2", 3, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_EverCrypt.Hash.Blake2B_s", "constructor_distinct_EverCrypt.Hash.Blake2S_s", "constructor_distinct_EverCrypt.Hash.MD5_s", "constructor_distinct_EverCrypt.Hash.SHA1_s", "constructor_distinct_EverCrypt.Hash.SHA2_224_s", "constructor_distinct_EverCrypt.Hash.SHA2_256_s", "constructor_distinct_EverCrypt.Hash.SHA2_384_s", "constructor_distinct_EverCrypt.Hash.SHA2_512_s", "constructor_distinct_FStar.Integers.Unsigned", "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_Hacl.Impl.Blake2.Core.M128", "constructor_distinct_Hacl.Impl.Blake2.Core.M32", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S128", "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", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_elim_EverCrypt.Hash.Blake2B_s", "data_elim_EverCrypt.Hash.Blake2S_s", "data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s", "data_elim_EverCrypt.Hash.SHA2_224_s", "data_elim_EverCrypt.Hash.SHA2_256_s", "data_elim_EverCrypt.Hash.SHA2_384_s", "data_elim_EverCrypt.Hash.SHA2_512_s", "data_typing_intro_Lib.IntTypes.U8@tok", "data_typing_intro_Spec.Blake2.Blake2B@tok", "disc_equation_EverCrypt.Hash.Blake2B_s", "disc_equation_EverCrypt.Hash.Blake2S_s", "disc_equation_EverCrypt.Hash.MD5_s", "disc_equation_EverCrypt.Hash.SHA1_s", "disc_equation_EverCrypt.Hash.SHA2_224_s", "disc_equation_EverCrypt.Hash.SHA2_256_s", "disc_equation_EverCrypt.Hash.SHA2_384_s", "disc_equation_EverCrypt.Hash.SHA2_512_s", "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_Hacl.Impl.Blake2.Core.M32@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", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.blake2_spec", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.footprint", "equation_EverCrypt.Hash.footprint_s", "equation_EverCrypt.Hash.freeable", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p", "equation_EverCrypt.Hash.preserves_freeable", "equation_EverCrypt.Hash.repr", "equation_EverCrypt.Hash.repr_with_counter", "equation_EverCrypt.Hash.state", "equation_EverCrypt.Helpers.uint32_t", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Int.Cast.Full.uint64_to_uint128", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_32", "equation_FStar.Integers.uint_64", "equation_FStar.Monotonic.HyperStack.mem", "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_FStar.UInt128.n", "equation_Hacl.Hash.Definitions.block_len", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.get_spec", "equation_Hacl.Hash.Definitions.impl", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.m_spec", "equation_Hacl.Hash.Definitions.state", "equation_Hacl.Impl.Blake2.Core.element_t", "equation_Hacl.Impl.Blake2.Core.word_t", "equation_Lib.IntTypes.cast", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.Hash.update_multi", "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_int_type", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "fuel_guarded_inversion_EverCrypt.Hash.state_s", "fuel_guarded_inversion_Prims.dtuple2", "function_token_typing_FStar.Integers.uint_32", "function_token_typing_FStar.Integers.uint_64", "function_token_typing_Lib.IntTypes.pub_uint64", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "kinding_EverCrypt.Hash.state_s@tok", "kinding_Spec.Hash.Definitions.hash_alg@tok", "lemma_FStar.UInt.pow2_values", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "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_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "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_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_EverCrypt.Hash.Blake2B_s_p", "projection_inverse_EverCrypt.Hash.Blake2S_s_p", "projection_inverse_EverCrypt.Hash.MD5_s_p", "projection_inverse_EverCrypt.Hash.SHA1_s_p", "projection_inverse_EverCrypt.Hash.SHA2_224_s_p", "projection_inverse_EverCrypt.Hash.SHA2_256_s_p", "projection_inverse_EverCrypt.Hash.SHA2_384_s_p", "projection_inverse_EverCrypt.Hash.SHA2_512_s_p", "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_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0941c9ff95557f2d53bc8f8179ab793e", "refinement_interpretation_Tm_refine_375faf8fecbf524a5532f0557c79dc73", "refinement_interpretation_Tm_refine_37c93ce5bbd59eacadc2b1f547360369", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_430a5074f3a28dcbdb8a5c1f8b050b57", "refinement_interpretation_Tm_refine_45fb1fe6d11e460ce7fa5c267d49a18f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_66c124f492ec193d4bbaa9a39421d6d4", "refinement_interpretation_Tm_refine_74d1ae07763cf2ce5f26906c9df0d2cc", "refinement_interpretation_Tm_refine_7792679b3c450daf2a53ac4df195b5eb", "refinement_interpretation_Tm_refine_78db224f600b3acabdab42a044183b6c", "refinement_interpretation_Tm_refine_83e1a0ed8e967940f825c40ec86a30c4", "refinement_interpretation_Tm_refine_89555d185e6377fffaa1db1c14e08385", "refinement_interpretation_Tm_refine_91c352d831715ed604553457a8078865", "refinement_interpretation_Tm_refine_a803b759f08d41207c176c52e6485f20", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_c2f916b98cea21c183e1c8b1e5deeafe", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f4235ca35aeb7ebf867cf38b99ce6272", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.Hash.footprint", "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.impl_of_alg", "typing_EverCrypt.Hash.p", "typing_FStar.Ghost.reveal", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "typing_FStar.UInt32.div", "typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.block_len", "typing_Hacl.Hash.Definitions.impl_word", "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.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Hash.Definitions.Blake2B@tok", "typing_tok_Spec.Hash.Definitions.Blake2S@tok", "typing_tok_Spec.Hash.Definitions.MD5@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "typing_tok_Spec.Hash.Definitions.SHA2_384@tok", "typing_tok_Spec.Hash.Definitions.SHA2_512@tok" ], 0, "266ab362fcb40f220373c43233d9871e" ], [ "EverCrypt.Hash.update_multi", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.Hash.uu___1", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "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.is_md", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "inversion-interp", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_26ad11f87673edceb28824c1006925f0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_83e1a0ed8e967940f825c40ec86a30c4", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "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", "unit_typing" ], 0, "e4f17c32d102d578628f8df7e8120e16" ], [ "EverCrypt.Hash.update_multi", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.state", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.word_length", "kinding_EverCrypt.Hash.state_s@tok", "kinding_Spec.Hash.Definitions.hash_alg@tok", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_26ad11f87673edceb28824c1006925f0", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "typing_FStar.Ghost.reveal", "typing_LowStar.Buffer.trivial_preorder", "typing_Spec.Hash.Definitions.is_md" ], 0, "cd8f2150c9ad9c9eac6e724ad083baf5" ], [ "EverCrypt.Hash.update_multi", 3, 0, 0, [ "@MaxIFuel_assumption", "@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.U1", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "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_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.repr_with_counter", "equation_EverCrypt.Hash.state", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.is_md", "kinding_EverCrypt.Hash.state_s@tok", "kinding_Spec.Hash.Definitions.hash_alg@tok", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "refinement_interpretation_Tm_refine_26ad11f87673edceb28824c1006925f0", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "typing_FStar.Ghost.reveal", "typing_LowStar.Buffer.trivial_preorder", "typing_Spec.Hash.Definitions.is_md" ], 0, "db29c5d2409684ad88c6f27f9301d77c" ], [ "EverCrypt.Hash.update_last_256", 1, 0, 0, [ "@query", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_FStar.Integers.W64@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Hacl.Hash.Definitions.get_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Prims.Mkdtuple2__1" ], 0, "5c80db4a1e15e8e6c8ca489dd2660f73" ], [ "EverCrypt.Hash.update_last_256", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_FStar.Integers.W64@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.is_md", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "71d7916a9f7de8556ab2a1a3fbffc0a2" ], [ "EverCrypt.Hash.update_last_224", 1, 0, 0, [ "@query", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equation_Hacl.Hash.Definitions.get_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Mkdtuple2__1" ], 0, "ab2f3a36af34e651e45ea7ee7e68e512" ], [ "EverCrypt.Hash.update_last_224", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Seq.Base.op_At_Bar", "equation_Hacl.Hash.Definitions.as_seq", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.impl_state_length", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.secret", "equation_Lib.IntTypes.uint8", "equation_Lib.Sequence.seq", "equation_Lib.UpdateMulti.uint8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "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.extra_state", "equation_Spec.Hash.Definitions.extra_state_v", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.len_int_type", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.len_t", "equation_Spec.Hash.Definitions.len_v", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.nat_to_len", "equation_Spec.Hash.Definitions.pad0_length", "equation_Spec.Hash.Definitions.state_word_length", "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.Definitions.words_state_", "equation_Spec.Hash.Incremental.update_last", "equation_Spec.Hash.PadFinish.pad", "equation_Spec.Hash.PadFinish.pad_md", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "int_typing", "interpretation_Tm_abs_c5cfacc785df376403b58f49cdaf22b6", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_Lib.IntTypes.v_injective", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__a", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_77bf07a3a0c4b3d914a147a5c04a6a21", "refinement_interpretation_Tm_refine_850fe300f875565a60c2c1ce43a6fda4", "refinement_interpretation_Tm_refine_a2881f764d97beb430c306ca52f4dff1", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_b61185bd7bfa9db1bf20ad7e18b96aab", "refinement_interpretation_Tm_refine_c52afdf4bd7cdc22c74546c97a073e45", "refinement_interpretation_Tm_refine_ca05b89c5c1f41baab15b74f2530fe45", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_fad544f56a292641a3d8590d0d604210", "typing_FStar.Seq.Base.op_At_Bar", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.extra_state", "typing_Spec.Hash.Definitions.len_v", "typing_Spec.Hash.Definitions.word", "typing_Spec.Hash.Definitions.words_state_", "typing_Spec.Hash.PadFinish.pad", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "unit_inversion", "unit_typing" ], 0, "5623be6e5e7374a925ccac0265cf2149" ], [ "EverCrypt.Hash.update_last_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "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.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.uu___1", "equation_EverCrypt.Helpers.uint64_t", "equation_EverCrypt.Helpers.uint8_p", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Definitions.get_alg", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.words_state_", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "int_inversion", "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_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_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_73163ce533221c5584e99877041be5fe", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f1980e115ff7b450eede61343da80c07", "typing_FStar.UInt64.v", "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, "4b4f10f24fee56b1b0e41665a540a430" ], [ "EverCrypt.Hash.update_last_64", 1, 0, 0, [ "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq" ], 0, "7c9a12acaf4c20cd1d95c7e74153d2ad" ], [ "EverCrypt.Hash.update_last_64", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.uu___1", "equation_Prims.squash", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "inversion-interp", "kinding_Spec.Hash.Definitions.hash_alg@tok", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_b61fdb08b42ded14dde01fd9069f6f13", "typing_FStar.Ghost.reveal" ], 0, "2ed3330febcb4dadb127341b8baa1a6b" ], [ "EverCrypt.Hash.update_last_64", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "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", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "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.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.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.uu___1", "equation_EverCrypt.Helpers.uint32_t", "equation_EverCrypt.Helpers.uint64_t", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.int_t", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.impl_word", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.extra_state_v", "equation_Spec.Hash.Definitions.len_t", "equation_Spec.Hash.Definitions.len_v", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "interpretation_Tm_abs_c5cfacc785df376403b58f49cdaf22b6", "inversion-interp", "kinding_Spec.Hash.Definitions.hash_alg@tok", "primitive_Prims.op_Addition", "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_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2b2f4e7c9d5f0d19ac9fc0db9880b5a9", "refinement_interpretation_Tm_refine_2c07750362c8b962c72f8be62dda30cc", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_b61fdb08b42ded14dde01fd9069f6f13", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f1980e115ff7b450eede61343da80c07", "typing_EverCrypt.Hash.impl_of_alg", "typing_FStar.Ghost.reveal", "typing_Hacl.Hash.Definitions.get_alg", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.extra_state_v", "unit_inversion", "unit_typing" ], 0, "0a2b020d4e1f5d63201365642fcc2d6c" ], [ "EverCrypt.Hash.update_last_128", 1, 0, 0, [ "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq" ], 0, "9fd07a438071314c66150e7ece6a3bf8" ], [ "EverCrypt.Hash.update_last_128", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.uu___1", "equation_Prims.squash", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "inversion-interp", "kinding_Spec.Hash.Definitions.hash_alg@tok", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2ac41f66ed21301fcde631cc6029bf6b", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_FStar.Ghost.reveal" ], 0, "3fb6e98833e332b85d53d26954da7660" ], [ "EverCrypt.Hash.update_last_128", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "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", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@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.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.uu___1", "equation_EverCrypt.Helpers.uint64_t", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Int.Cast.Full.uint64_to_uint128", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.impl_word", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.extra_state_v", "equation_Spec.Hash.Definitions.len_t", "equation_Spec.Hash.Definitions.len_v", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "interpretation_Tm_abs_71042ce475a96c7fa134177a01959d0b", "inversion-interp", "kinding_Spec.Hash.Definitions.hash_alg@tok", "lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_Addition", "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_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2ac41f66ed21301fcde631cc6029bf6b", "refinement_interpretation_Tm_refine_2b2f4e7c9d5f0d19ac9fc0db9880b5a9", "refinement_interpretation_Tm_refine_2c07750362c8b962c72f8be62dda30cc", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_89263c8dd7df5c497acdada0682b1aab", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f1980e115ff7b450eede61343da80c07", "typing_EverCrypt.Hash.impl_of_alg", "typing_FStar.Ghost.reveal", "typing_FStar.Int.Cast.Full.uint64_to_uint128", "typing_Hacl.Hash.Definitions.get_alg", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.extra_state_v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok", "unit_inversion", "unit_typing" ], 0, "52fdaab8ca5fed37d934d3e36ec33967" ], [ "EverCrypt.Hash.state_s_to_words_state", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "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.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "disc_equation_Lib.IntTypes.SEC", "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.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.uu___1", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_Hacl.Hash.Definitions.get_alg", "equation_Lib.IntTypes.unsigned", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.words_state_", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "function_token_typing_FStar.Monotonic.Heap.heap", "inversion-interp", "lemma_FStar.Map.lemma_ContainsDom", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_3afef912859361e9884ab51f5c9deddb", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "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", "unit_typing" ], 0, "992f97ce8f3e0997715ef06de10cf728" ], [ "EverCrypt.Hash.update_last_with_internal_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "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.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.uu___1", "equation_EverCrypt.Helpers.uint64_t", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Definitions.get_alg", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "int_inversion", "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_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_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_657b9c32df30894b419c11a4fc7c106e", "refinement_interpretation_Tm_refine_7387af26a729d45660870a4413773cc8", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e4719a1714a1bcd6a836f552f9c437ef", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt64.v", "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, "fd0908e0e512653e19f233a40d91ead9" ], [ "EverCrypt.Hash.update_last_blake2s", 1, 0, 0, [ "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.S8", "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_Spec.Hash.Definitions.Blake2S@tok", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0" ], 0, "a33f881fd5a1b33a7b34c35e96b19576" ], [ "EverCrypt.Hash.update_last_blake2s", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S128", "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.U128", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "data_elim_EverCrypt.Hash.MD5_s", "data_typing_intro_Lib.IntTypes.U8@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.footprint_s", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.mk_state_s", "equation_EverCrypt.Hash.p", "equation_EverCrypt.Hash.state_s_to_words_state", "equation_EverCrypt.Helpers.uint64_t", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Pervasives.Native.fst", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.cast", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "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.Incremental.update_last", "fuel_guarded_inversion_EverCrypt.Hash.state_s", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "kinding_Spec.Hash.Definitions.hash_alg@tok", "lemma_FStar.Ghost.reveal_hide", "lemma_Lib.IntTypes.v_injective", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "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_trans_backwards", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "primitive_Prims.op_Addition", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_EverCrypt.Hash.Blake2S_s_p", "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_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_02dc417268b0f3cd8065ad570f075dc9", "refinement_interpretation_Tm_refine_16d396287a2869b7c03a6712a4f7a513", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_57baf92aa61a0b9188fe9fa5eed561f5", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_b61fdb08b42ded14dde01fd9069f6f13", "refinement_interpretation_Tm_refine_c4245ff932b6ecff56ef1dde5a1897f0", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.impl_of_alg", "typing_EverCrypt.Hash.mk_state_s", "typing_EverCrypt.Hash.p", "typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.impl_word", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "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_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Blake2.Blake2B@tok", "typing_tok_Spec.Hash.Definitions.Blake2S@tok" ], 0, "f89f56430ccb991b218cdb1b305e6602" ], [ "EverCrypt.Hash.update_last_blake2b", 1, 0, 0, [ "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, "65f8c977360732b2ba16da45e7a29131" ], [ "EverCrypt.Hash.update_last_blake2b", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "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_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_elim_EverCrypt.Hash.MD5_s", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@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.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.footprint_s", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.mk_state_s", "equation_EverCrypt.Hash.p", "equation_EverCrypt.Hash.state_s_to_words_state", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Int.Cast.Full.uint64_to_uint128", "equation_FStar.Pervasives.Native.fst", "equation_FStar.UInt128.n", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.cast", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "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.Incremental.update_last", "fuel_guarded_inversion_EverCrypt.Hash.state_s", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "inversion-interp", "lemma_EverCrypt.Hash.invert_state_s", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "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_trans_backwards", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "primitive_Prims.op_Addition", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_EverCrypt.Hash.Blake2B_s_p", "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_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0af911853ac29bd7db0d802109e184e3", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_72d3727f248b885b40a75bf37ceed448", "refinement_interpretation_Tm_refine_807076d57ee6ac14e7a2d7c3ffc73cf9", "refinement_interpretation_Tm_refine_89263c8dd7df5c497acdada0682b1aab", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f907d795c17e618418440bc16c79b624", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.impl_of_alg", "typing_EverCrypt.Hash.mk_state_s", "typing_EverCrypt.Hash.p", "typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.impl_word", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U1@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Hash.Definitions.Blake2B@tok" ], 0, "440ca80e6b3f652cb5a8271a5b2a6fc0" ], [ "EverCrypt.Hash.update_last2", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "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.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_EverCrypt.Hash.uu___1", "equation_EverCrypt.Helpers.uint64_t", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Definitions.get_alg", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "int_inversion", "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_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_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_6191ff643839ba34df44b09dbee98d83", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_b441e671b2416c2d1b332759d7ac0a00", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt64.v", "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, "2828a706b73c9da5b39935c70c520839" ], [ "EverCrypt.Hash.update_last2", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.uu___1", "equation_Prims.squash", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "inversion-interp", "kinding_Spec.Hash.Definitions.hash_alg@tok", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "typing_FStar.Ghost.reveal" ], 0, "efa6589a9f85c8b3c369e6a213fe4850" ], [ "EverCrypt.Hash.update_last2", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "b2t_def", "bool_typing", "constructor_distinct_EverCrypt.Hash.Blake2B_s", "constructor_distinct_EverCrypt.Hash.Blake2S_s", "constructor_distinct_EverCrypt.Hash.MD5_s", "constructor_distinct_EverCrypt.Hash.SHA1_s", "constructor_distinct_EverCrypt.Hash.SHA2_224_s", "constructor_distinct_EverCrypt.Hash.SHA2_256_s", "constructor_distinct_EverCrypt.Hash.SHA2_384_s", "constructor_distinct_EverCrypt.Hash.SHA2_512_s", "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_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S128", "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.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", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_elim_EverCrypt.Hash.Blake2B_s", "data_elim_EverCrypt.Hash.Blake2S_s", "data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s", "data_elim_EverCrypt.Hash.SHA2_224_s", "data_elim_EverCrypt.Hash.SHA2_256_s", "data_elim_EverCrypt.Hash.SHA2_384_s", "data_elim_EverCrypt.Hash.SHA2_512_s", "disc_equation_EverCrypt.Hash.Blake2B_s", "disc_equation_EverCrypt.Hash.Blake2S_s", "disc_equation_EverCrypt.Hash.MD5_s", "disc_equation_EverCrypt.Hash.SHA1_s", "disc_equation_EverCrypt.Hash.SHA2_224_s", "disc_equation_EverCrypt.Hash.SHA2_256_s", "disc_equation_EverCrypt.Hash.SHA2_384_s", "disc_equation_EverCrypt.Hash.SHA2_512_s", "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_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.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.footprint", "equation_EverCrypt.Hash.footprint_s", "equation_EverCrypt.Hash.freeable", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.mk_state_s", "equation_EverCrypt.Hash.p", "equation_EverCrypt.Hash.preserves_freeable", "equation_EverCrypt.Hash.repr", "equation_EverCrypt.Hash.repr_with_counter", "equation_EverCrypt.Hash.state", "equation_EverCrypt.Hash.state_s_to_words_state", "equation_EverCrypt.Helpers.uint32_t", "equation_EverCrypt.Helpers.uint64_t", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Pervasives.Native.fst", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "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.word", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Incremental.update_last", "fuel_guarded_inversion_EverCrypt.Hash.state_s", "function_token_typing_Lib.IntTypes.pub_uint64", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "inversion-interp", "kinding_EverCrypt.Hash.state_s@tok", "kinding_Spec.Hash.Definitions.hash_alg@tok", "lemma_EverCrypt.Hash.invert_state_s", "lemma_Lib.IntTypes.v_injective", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "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_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "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_EverCrypt.Hash.Blake2B_s_p", "projection_inverse_EverCrypt.Hash.Blake2S_s_p", "projection_inverse_EverCrypt.Hash.MD5_s_p", "projection_inverse_EverCrypt.Hash.SHA1_s_p", "projection_inverse_EverCrypt.Hash.SHA2_224_s_p", "projection_inverse_EverCrypt.Hash.SHA2_256_s_p", "projection_inverse_EverCrypt.Hash.SHA2_384_s_p", "projection_inverse_EverCrypt.Hash.SHA2_512_s_p", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2b2f4e7c9d5f0d19ac9fc0db9880b5a9", "refinement_interpretation_Tm_refine_2c07750362c8b962c72f8be62dda30cc", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4f7c020af435f80aaaf3f51bbdd26198", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_57baf92aa61a0b9188fe9fa5eed561f5", "refinement_interpretation_Tm_refine_6191ff643839ba34df44b09dbee98d83", "refinement_interpretation_Tm_refine_77bf07a3a0c4b3d914a147a5c04a6a21", "refinement_interpretation_Tm_refine_95ec05186d8878d328cecc3cd1a19898", "refinement_interpretation_Tm_refine_a2881f764d97beb430c306ca52f4dff1", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_b441e671b2416c2d1b332759d7ac0a00", "refinement_interpretation_Tm_refine_c2f916b98cea21c183e1c8b1e5deeafe", "refinement_interpretation_Tm_refine_d52f4e22b0939f51a08fc9a30b5f580a", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e56c57aef1e3e3d0440ea314b37eef24", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f907d795c17e618418440bc16c79b624", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.Hash.footprint", "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.impl_of_alg", "typing_EverCrypt.Hash.p", "typing_FStar.Ghost.reveal", "typing_FStar.Set.singleton", "typing_FStar.UInt32.t", "typing_FStar.UInt64.t", "typing_FStar.UInt64.v", "typing_Hacl.Hash.Definitions.impl_word", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.word_t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U1@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Hash.Definitions.SHA2_384@tok", "unit_inversion", "unit_typing" ], 0, "155f87a10ee2a5740d43725f3765fa5e" ], [ "EverCrypt.Hash.modulo_sub_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.Signed", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.Integers.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_Prims.int", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_a5e45e5366dd3f0120ddd2f82f92e757", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "bdf113a618b8cb7b716dc523c2adea42" ], [ "EverCrypt.Hash.modulo_sub_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.Signed", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_FStar.Integers.Signed", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.Integers.int_t", "equation_FStar.Integers.width_of_sw", "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_Prims.int", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "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_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955", "refinement_interpretation_Tm_refine_a5e45e5366dd3f0120ddd2f82f92e757", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "881a9abc2a02fb3696b902868de5c532" ], [ "EverCrypt.Hash.update_last", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.Helpers.uint64_t", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.is_md", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Spec.AES.elem", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_26ad11f87673edceb28824c1006925f0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ca524e8b1a445d963e32596f1b3827cf", "refinement_interpretation_Tm_refine_cb6956610e36c497712e91628f3f016e", "refinement_interpretation_Tm_refine_ce8961826e5e909d22aad978d7822e9d", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt64.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "unit_typing" ], 0, "18f1327c76168702c4294e542c0f65ef" ], [ "EverCrypt.Hash.update_last", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "function_token_typing_Lib.IntTypes.uint8", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ce8961826e5e909d22aad978d7822e9d", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.length" ], 0, "ca7bb7b4296714b6358f4070c351d00d" ], [ "EverCrypt.Hash.update_last", 3, 0, 0, [ "@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.S8", "constructor_distinct_Lib.IntTypes.SEC", "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.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "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.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_EverCrypt.Hash.repr_with_counter", "equation_EverCrypt.Hash.state", "equation_EverCrypt.Helpers.uint64_t", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Int.Cast.uint64_to_uint32", "equation_FStar.Integers.int_t", "equation_FStar.Seq.Base.op_At_Bar", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.mod", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Definitions.block_len", "equation_Hacl.Hash.Definitions.get_alg", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.felem", "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.extra_state", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.words_state_", "equation_Spec.Hash.Incremental.update_last", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "int_inversion", "int_typing", "kinding_EverCrypt.Hash.state_s@tok", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.v_injective", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "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_Division", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_26ad11f87673edceb28824c1006925f0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_91c352d831715ed604553457a8078865", "refinement_interpretation_Tm_refine_94d25b6e0041d543efd58300424ecc37", "refinement_interpretation_Tm_refine_a3e91433acc705e2c7f5ab6f610b2493", "refinement_interpretation_Tm_refine_cb6956610e36c497712e91628f3f016e", "refinement_interpretation_Tm_refine_cc33385e7b962bd2348f9f7560ada9de", "refinement_interpretation_Tm_refine_ce8961826e5e909d22aad978d7822e9d", "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_EverCrypt.Hash.repr", "typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.Int.Cast.uint64_to_uint32", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "typing_Hacl.Hash.Definitions.block_len", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.is_md", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Hash.Definitions.MD5@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok", "unit_typing" ], 0, "46c607af1f75fd5eeaf61cb809f7024f" ], [ "EverCrypt.Hash.finish", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.Monotonic.HyperStack.live_region", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "function_token_typing_Lib.IntTypes.uint8", "lemma_LowStar.Monotonic.Buffer.live_region_frameOf", "refinement_interpretation_Tm_refine_509b2edb605f806e987ffdd634bc26a4", "refinement_interpretation_Tm_refine_c2f916b98cea21c183e1c8b1e5deeafe", "typing_FStar.Monotonic.HyperStack.live_region", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.frameOf" ], 0, "f23a03abfbb2c39ff2470938af27bd1e" ], [ "EverCrypt.Hash.finish", 2, 0, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "Spec.Hash.PadFinish_interpretation_Tm_arrow_8e7de6c94fb45ba4829dbfed76bd6bd0", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_EverCrypt.Hash.Blake2B_s", "constructor_distinct_EverCrypt.Hash.Blake2S_s", "constructor_distinct_EverCrypt.Hash.MD5_s", "constructor_distinct_EverCrypt.Hash.SHA1_s", "constructor_distinct_EverCrypt.Hash.SHA2_224_s", "constructor_distinct_EverCrypt.Hash.SHA2_256_s", "constructor_distinct_EverCrypt.Hash.SHA2_384_s", "constructor_distinct_EverCrypt.Hash.SHA2_512_s", "constructor_distinct_FStar.Integers.Unsigned", "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_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.S8", "constructor_distinct_Lib.IntTypes.SEC", "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", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_elim_EverCrypt.Hash.Blake2B_s", "data_elim_EverCrypt.Hash.Blake2S_s", "data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s", "data_elim_EverCrypt.Hash.SHA2_224_s", "data_elim_EverCrypt.Hash.SHA2_256_s", "data_elim_EverCrypt.Hash.SHA2_384_s", "data_elim_EverCrypt.Hash.SHA2_512_s", "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok", "data_typing_intro_Spec.Blake2.Blake2B@tok", "disc_equation_EverCrypt.Hash.Blake2B_s", "disc_equation_EverCrypt.Hash.Blake2S_s", "disc_equation_EverCrypt.Hash.MD5_s", "disc_equation_EverCrypt.Hash.SHA1_s", "disc_equation_EverCrypt.Hash.SHA2_224_s", "disc_equation_EverCrypt.Hash.SHA2_256_s", "disc_equation_EverCrypt.Hash.SHA2_384_s", "disc_equation_EverCrypt.Hash.SHA2_512_s", "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_Hacl.Impl.Blake2.Core.M32@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", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.blake2_spec", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.footprint", "equation_EverCrypt.Hash.footprint_s", "equation_EverCrypt.Hash.freeable", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p", "equation_EverCrypt.Hash.preserves_freeable", "equation_EverCrypt.Hash.repr", "equation_EverCrypt.Hash.repr_with_counter", "equation_EverCrypt.Hash.state", "equation_EverCrypt.Helpers.uint32_t", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_32", "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.Hash.Definitions.as_seq", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.get_spec", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.m_spec", "equation_Hacl.Hash.Definitions.state", "equation_Hacl.Impl.Blake2.Core.element_t", "equation_Hacl.Impl.Blake2.Core.word_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size128_t", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "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.extra_state", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_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.Definitions.words_state_", "equation_Spec.Hash.PadFinish.finish", "equation_Spec.Hash.PadFinish.finish_blake", "fuel_guarded_inversion_EverCrypt.Hash.state_s", "function_token_typing_FStar.Integers.uint_32", "function_token_typing_FStar.Pervasives.pattern", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.size128_t", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Spec.Hash.PadFinish.finish", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing", "kinding_EverCrypt.Hash.state_s@tok", "kinding_Spec.Hash.Definitions.hash_alg@tok", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "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.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "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_EverCrypt.Hash.Blake2B_s_p", "projection_inverse_EverCrypt.Hash.Blake2S_s_p", "projection_inverse_EverCrypt.Hash.MD5_s_p", "projection_inverse_EverCrypt.Hash.SHA1_s_p", "projection_inverse_EverCrypt.Hash.SHA2_224_s_p", "projection_inverse_EverCrypt.Hash.SHA2_256_s_p", "projection_inverse_EverCrypt.Hash.SHA2_384_s_p", "projection_inverse_EverCrypt.Hash.SHA2_512_s_p", "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_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_375faf8fecbf524a5532f0557c79dc73", "refinement_interpretation_Tm_refine_37c93ce5bbd59eacadc2b1f547360369", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_509b2edb605f806e987ffdd634bc26a4", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_66c124f492ec193d4bbaa9a39421d6d4", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_7792679b3c450daf2a53ac4df195b5eb", "refinement_interpretation_Tm_refine_78db224f600b3acabdab42a044183b6c", "refinement_interpretation_Tm_refine_89555d185e6377fffaa1db1c14e08385", "refinement_interpretation_Tm_refine_a803b759f08d41207c176c52e6485f20", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_aebf0a5a4cc5a0edddd5cedf26878e34", "refinement_interpretation_Tm_refine_bdf26c5e5a33d51389e46e73076cb41b", "refinement_interpretation_Tm_refine_c2f916b98cea21c183e1c8b1e5deeafe", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f4235ca35aeb7ebf867cf38b99ce6272", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.Hash.footprint", "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.impl_of_alg", "typing_EverCrypt.Hash.p", "typing_FStar.Ghost.reveal", "typing_FStar.Set.singleton", "typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.as_seq", "typing_Hacl.Hash.Definitions.get_alg", "typing_Hacl.Hash.Definitions.impl_word", "typing_Lib.IntTypes.unsigned", "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.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.Blake2.blake2_finish", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.words_state_", "typing_Spec.Hash.PadFinish.finish", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Blake2.Blake2S@tok", "typing_tok_Spec.Hash.Definitions.Blake2B@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "typing_tok_Spec.Hash.Definitions.SHA2_512@tok", "unit_typing" ], 0, "4acf5c045c7e938ce5d6bf0076e26d73" ], [ "EverCrypt.Hash.free", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_typing", "constructor_distinct_EverCrypt.Hash.Blake2B_s", "constructor_distinct_EverCrypt.Hash.Blake2S_s", "constructor_distinct_EverCrypt.Hash.MD5_s", "constructor_distinct_EverCrypt.Hash.SHA1_s", "constructor_distinct_EverCrypt.Hash.SHA2_224_s", "constructor_distinct_EverCrypt.Hash.SHA2_256_s", "constructor_distinct_EverCrypt.Hash.SHA2_384_s", "constructor_distinct_EverCrypt.Hash.SHA2_512_s", "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.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", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_elim_EverCrypt.Hash.Blake2B_s", "data_elim_EverCrypt.Hash.Blake2S_s", "data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s", "data_elim_EverCrypt.Hash.SHA2_224_s", "data_elim_EverCrypt.Hash.SHA2_256_s", "data_elim_EverCrypt.Hash.SHA2_384_s", "data_elim_EverCrypt.Hash.SHA2_512_s", "disc_equation_EverCrypt.Hash.Blake2B_s", "disc_equation_EverCrypt.Hash.Blake2S_s", "disc_equation_EverCrypt.Hash.MD5_s", "disc_equation_EverCrypt.Hash.SHA1_s", "disc_equation_EverCrypt.Hash.SHA2_224_s", "disc_equation_EverCrypt.Hash.SHA2_256_s", "disc_equation_EverCrypt.Hash.SHA2_384_s", "disc_equation_EverCrypt.Hash.SHA2_512_s", "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.U8@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.footprint", "equation_EverCrypt.Hash.footprint_s", "equation_EverCrypt.Hash.freeable", "equation_EverCrypt.Hash.freeable_s", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p", "equation_EverCrypt.Hash.state", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.mem", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_EverCrypt.Hash.state_s", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "inversion-interp", "kinding_EverCrypt.Hash.state_s@tok", "kinding_Spec.Hash.Definitions.hash_alg@tok", "lemma_EverCrypt.Hash.invert_state_s", "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.Set.lemma_equal_elim", "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_union_l_", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_EverCrypt.Hash.Blake2B_s_p", "projection_inverse_EverCrypt.Hash.Blake2S_s_p", "projection_inverse_EverCrypt.Hash.MD5_s_p", "projection_inverse_EverCrypt.Hash.SHA1_s_p", "projection_inverse_EverCrypt.Hash.SHA2_224_s_p", "projection_inverse_EverCrypt.Hash.SHA2_256_s_p", "projection_inverse_EverCrypt.Hash.SHA2_384_s_p", "projection_inverse_EverCrypt.Hash.SHA2_512_s_p", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0557da5b18f4cd4283fc912f6e9077f6", "refinement_interpretation_Tm_refine_05989d7bd405a0042aa9b26f49855688", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_087e466f4a3929e74f15aa021e2ebf18", "refinement_interpretation_Tm_refine_380f4bd6a3f5fdc2178a57a6eccf131f", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_619144f87346fa6ca7386cabc29baebb", "refinement_interpretation_Tm_refine_a0b3003bf3a6f7558a637fc45c211d5e", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_bbea6ff4176a20dc12b591f149394151", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e08bded9da9026aa9fbab50b7d8d4b28", "refinement_interpretation_Tm_refine_ebc8cc740b465b6354f18667ed8b495f", "refinement_interpretation_Tm_refine_fa7ca3abd45f799dbcfa079f802dcd46", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.Hash.footprint", "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.impl_of_alg", "typing_EverCrypt.Hash.p", "typing_FStar.Ghost.reveal", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.impl_word", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "4ab2741c280767fe21a62381fe0171dc" ], [ "EverCrypt.Hash.copy", 1, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_EverCrypt.Hash.Blake2B_s", "constructor_distinct_EverCrypt.Hash.Blake2S_s", "constructor_distinct_EverCrypt.Hash.MD5_s", "constructor_distinct_EverCrypt.Hash.SHA1_s", "constructor_distinct_EverCrypt.Hash.SHA2_224_s", "constructor_distinct_EverCrypt.Hash.SHA2_256_s", "constructor_distinct_EverCrypt.Hash.SHA2_384_s", "constructor_distinct_EverCrypt.Hash.SHA2_512_s", "constructor_distinct_FStar.Integers.Unsigned", "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_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.S8", "constructor_distinct_Lib.IntTypes.SEC", "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", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "data_elim_EverCrypt.Hash.Blake2B_s", "data_elim_EverCrypt.Hash.Blake2S_s", "data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s", "data_elim_EverCrypt.Hash.SHA2_224_s", "data_elim_EverCrypt.Hash.SHA2_256_s", "data_elim_EverCrypt.Hash.SHA2_384_s", "data_elim_EverCrypt.Hash.SHA2_512_s", "data_typing_intro_Spec.Blake2.Blake2B@tok", "disc_equation_EverCrypt.Hash.Blake2B_s", "disc_equation_EverCrypt.Hash.Blake2S_s", "disc_equation_EverCrypt.Hash.MD5_s", "disc_equation_EverCrypt.Hash.SHA1_s", "disc_equation_EverCrypt.Hash.SHA2_224_s", "disc_equation_EverCrypt.Hash.SHA2_256_s", "disc_equation_EverCrypt.Hash.SHA2_384_s", "disc_equation_EverCrypt.Hash.SHA2_512_s", "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_Hacl.Impl.Blake2.Core.M32@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", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.blake2_spec", "equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.footprint", "equation_EverCrypt.Hash.footprint_s", "equation_EverCrypt.Hash.freeable", "equation_EverCrypt.Hash.impl_of_alg", "equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p", "equation_EverCrypt.Hash.preserves_freeable", "equation_EverCrypt.Hash.repr", "equation_EverCrypt.Hash.state", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_32", "equation_FStar.Integers.uint_64", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.mul_mod", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Definitions.as_seq", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.get_spec", "equation_Hacl.Hash.Definitions.impl_state_length", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.m_spec", "equation_Hacl.Hash.Definitions.state", "equation_Hacl.Impl.Blake2.Core.element_t", "equation_Hacl.Impl.Blake2.Core.row_len", "equation_Hacl.Impl.Blake2.Core.word_t", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mul_mod", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state_", "fuel_guarded_inversion_EverCrypt.Hash.state_s", "function_token_typing_FStar.Integers.uint_32", "function_token_typing_FStar.Integers.uint_64", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.pub_uint64", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_LowStar.Buffer.trivial_preorder", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "kinding_EverCrypt.Hash.state_s@tok", "kinding_Spec.Hash.Definitions.hash_alg@tok", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Hacl.Impl.Blake2.Core.state_v_eq_lemma", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_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_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_EverCrypt.Hash.Blake2B_s_p", "proj_equation_EverCrypt.Hash.Blake2S_s_p", "proj_equation_EverCrypt.Hash.MD5_s_p", "proj_equation_EverCrypt.Hash.SHA1_s_p", "proj_equation_EverCrypt.Hash.SHA2_224_s_p", "proj_equation_EverCrypt.Hash.SHA2_256_s_p", "proj_equation_EverCrypt.Hash.SHA2_384_s_p", "proj_equation_EverCrypt.Hash.SHA2_512_s_p", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_EverCrypt.Hash.Blake2B_s_p", "projection_inverse_EverCrypt.Hash.Blake2S_s_p", "projection_inverse_EverCrypt.Hash.MD5_s_p", "projection_inverse_EverCrypt.Hash.SHA1_s_p", "projection_inverse_EverCrypt.Hash.SHA2_224_s_p", "projection_inverse_EverCrypt.Hash.SHA2_256_s_p", "projection_inverse_EverCrypt.Hash.SHA2_384_s_p", "projection_inverse_EverCrypt.Hash.SHA2_512_s_p", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Prims.Mkdtuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_002cc45cc7435ec22a06b8b01e9250e1", "refinement_interpretation_Tm_refine_04b98a792d3654f1552cb92b12c3f7fb", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_2e293b6ace97401d0e766aabcf6dc308", "refinement_interpretation_Tm_refine_3395b2144f9b73926569c11752bea8bf", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4bf470ae8cf1b2736b7e2fd10dfea092", "refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_8618df86656cf4c2bc98614452120307", "refinement_interpretation_Tm_refine_89629ed6137432cee6a70ad72e4931ed", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_bcedd9b51365d0f9c1e934bef3a0c603", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_interpretation_Tm_refine_c1b731d3266f76004e98c91031483b47", "refinement_interpretation_Tm_refine_cdabcd3d11956be43e5ec4b7940ad476", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "true_interp", "typing_EverCrypt.Hash.footprint", "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.impl_of_alg", "typing_EverCrypt.Hash.p", "typing_EverCrypt.Hash.repr", "typing_FStar.Ghost.reveal", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "typing_FStar.UInt32.mul_mod", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.impl_state_length", "typing_Hacl.Hash.Definitions.impl_word", "typing_Hacl.Impl.Blake2.Core.row_len", "typing_Lib.Buffer.as_seq", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mul_mod", "typing_Lib.IntTypes.unsigned", "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.get", "typing_LowStar.Monotonic.Buffer.len", "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_tok_Hacl.Impl.Blake2.Core.M32@tok", "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", "typing_tok_Spec.Hash.Definitions.MD5@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "typing_tok_Spec.Hash.Definitions.SHA2_384@tok", "typing_tok_Spec.Hash.Definitions.SHA2_512@tok" ], 0, "36a421c2aca98ee69c3354f379775627" ], [ "EverCrypt.Hash.hash_256", 1, 0, 0, [ "@query" ], 0, "d107cb7c6bf3f41e2304a43ccba0533b" ], [ "EverCrypt.Hash.hash_256", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_FStar.Integers.W64@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.is_md", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "776ef94059332169fb8f0fb00dc572e6" ], [ "EverCrypt.Hash.hash_224", 1, 0, 0, [ "@query" ], 0, "c56067c47cddccf78823daf385a97280" ], [ "EverCrypt.Hash.hash_224", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.is_md", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "b21ed5ca2dd21c679f9eed16c92aad84" ], [ "EverCrypt.Hash.hash", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.HyperStack.live_region", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.live_region_frameOf", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_117a03ca3213deec9a5d7dc6b56bb4c1", "refinement_interpretation_Tm_refine_11f5c63c78caccafb41a6490396f36ec", "refinement_interpretation_Tm_refine_70a01283c9094ee10f0f0fa4ff6403d7", "typing_FStar.Monotonic.HyperStack.live_region", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.frameOf" ], 0, "854e88ae23f7105b2b708361933eea79" ], [ "EverCrypt.Hash.hash", 2, 0, 0, [ "@query" ], 0, "69f21f7638617420914d5b2dbd0e9ad6" ], [ "EverCrypt.Hash.hash", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.Unsigned", "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.S8", "constructor_distinct_Lib.IntTypes.SEC", "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", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "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", "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.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", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_EverCrypt.Hash.uu___1", "equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_Hacl.Hash.Definitions.get_alg", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.squash", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.Hash.hash", "equation_Spec.Blake2.max_output", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_EverCrypt.Hash.uu___1", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "int_inversion", "inversion-interp", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "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_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_117a03ca3213deec9a5d7dc6b56bb4c1", "refinement_interpretation_Tm_refine_11f5c63c78caccafb41a6490396f36ec", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3f43951dbbf8ded060b4996016a8dfd0", "refinement_interpretation_Tm_refine_70a01283c9094ee10f0f0fa4ff6403d7", "refinement_interpretation_Tm_refine_745e5e8cb9ad35e4cdeebe069a6aa515", "refinement_interpretation_Tm_refine_7dee8852a19715c9524d9f964bc908ae", "refinement_interpretation_Tm_refine_82c4dd0a3d12aab0e14c902a76d625c5", "refinement_interpretation_Tm_refine_83204c1e1f2f9b55ed7419191e68a1e2", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "refinement_interpretation_Tm_refine_b57a3b1863b23cb62783498632463b07", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_dd2785f2c71f831101131b2527d9320d", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f1024163b51fde1e1fdc06200ed04d58", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_Spec.AES.gf8", "typing_Spec.Agile.Hash.hash", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.hash_length", "typing_tok_Spec.Hash.Definitions.Blake2B@tok", "typing_tok_Spec.Hash.Definitions.Blake2S@tok", "typing_tok_Spec.Hash.Definitions.MD5@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "typing_tok_Spec.Hash.Definitions.SHA2_384@tok", "typing_tok_Spec.Hash.Definitions.SHA2_512@tok" ], 0, "3eef23d3427c379d710b3126cd0c9525" ] ] ]