[ "\\yA\".8t", [ [ "Hacl.HMAC.key_and_data_fits", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "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.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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", "equation_FStar.Integers.width_of_sw", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "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.max_input_length", "equation_Spec.Hash.Definitions.word_length", "equation_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "c5a80579add424562ce8fe807d890f40" ], [ "Hacl.HMAC.compute_st", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "function_token_typing_Lib.IntTypes.uint8", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_dd0acc6b0a6d213c976d90b31ff4bbf0", "refinement_interpretation_Tm_refine_e887a8e6ee6a76633ceebf23311c2363", "typing_LowStar.Buffer.trivial_preorder", "typing_Spec.Hash.Definitions.word_length" ], 0, "9f9bbe5a48f8386a73c8006892f4f029" ], [ "Hacl.HMAC.uu___19", 1, 2, 1, [ "@query" ], 0, "d2485981851f93c0977d1910cf5dc823" ], [ "Hacl.HMAC.xor_bytes_inplace", 1, 0, 0, [ "@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_83e736486cadca7ff9d6103e502326d5", "typing_LowStar.Buffer.trivial_preorder" ], 0, "5ea9b8ebeb078b5304d3e477cdf32880" ], [ "Hacl.HMAC.xor_bytes_inplace", 2, 0, 0, [ "@query" ], 0, "8f3c23169f675486cf96b0d4b20f5700" ], [ "Hacl.HMAC.xor_bytes_inplace", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_01772ef4ef24588ea822f3c5a1350e15", "refinement_interpretation_Tm_refine_3f413d7e41d584707b6b1feafc5c5082", "refinement_interpretation_Tm_refine_cfe562ce049cfd952f311212e2d19343" ], 0, "f0f59df6db2b4356c99914acf5a27346" ], [ "Hacl.HMAC.wrap_key_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint8", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_be9f9b7469d07f7dec61b636d3fadb10", "refinement_interpretation_Tm_refine_e49a6bb635c9e4626b8006826fdea8cd", "typing_Lib.IntTypes.bits", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.length", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "b086e1283cf1105bbddd4d888e68552d" ], [ "Hacl.HMAC.helper_smtpat", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W31", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W63", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W31@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W63@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.Pervasives.inversion", "equation_FStar.UInt.fits", "equation_FStar.UInt.lte", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lte", "equation_Hacl.Hash.Definitions.block_len", "equation_Hacl.Hash.Definitions.hash_len", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "int_inversion", "int_typing", "inversion-interp", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_91c352d831715ed604553457a8078865", "refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fac8acd534a7de583fb7b4a7fee7b4f4", "typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.block_len", "typing_Hacl.Hash.Definitions.hash_len", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "5e3bb6f5c7c7b1677eaab6e1395c082a" ], [ "Hacl.HMAC.mk_wrap_key", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "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_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "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_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.Integers.int_t", "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.lte", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lte", "equation_Hacl.HMAC.helper_smtpat", "equation_Hacl.HMAC.uu___19", "equation_Hacl.Hash.Definitions.block_len", "equation_Hacl.Hash.Definitions.hash_len", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.Agile.HMAC.wrap", "equation_Spec.Agile.Hash.init", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.init_t", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.words_state", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Hacl.HMAC.uu___19", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_LowStar.Buffer.trivial_preorder", "int_inversion", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "inversion-interp", "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Seq.Properties.slice_slice", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "lemma_LowStar.Monotonic.Buffer.len_gsub", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_gsub", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_45fb1fe6d11e460ce7fa5c267d49a18f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_875d097463520b31519fc89d2a587a98", "refinement_interpretation_Tm_refine_91c352d831715ed604553457a8078865", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_aa4b3d268075d84252df525db1f85524", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_be9f9b7469d07f7dec61b636d3fadb10", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_dc44250586a653608f9799fceb0f1ef9", "refinement_interpretation_Tm_refine_e49a6bb635c9e4626b8006826fdea8cd", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "true_interp", "typing_FStar.Ghost.reveal", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt32.sub", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.block_len", "typing_Hacl.Hash.Definitions.hash_len", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Prims.pow2", "typing_Spec.Agile.Hash.init", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.block_word_length", "typing_Spec.Hash.Definitions.hash_length", "typing_Spec.Hash.Definitions.state_word_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok", "unit_inversion", "unit_typing" ], 0, "125aaaef2e72b8770671fd05b6830407" ], [ "Hacl.HMAC.block_len_as_len", 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.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.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", "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_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "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_FStar.Int.Cast.Full.uint64_to_uint128", "equation_FStar.Int.Cast.uint32_to_uint64", "equation_Hacl.HMAC.uu___19", "equation_Hacl.Hash.Definitions.block_len", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.v", "equation_Prims.squash", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.len_t", "equation_Spec.Hash.Definitions.len_v", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_Hacl.HMAC.uu___19", "interpretation_Tm_abs_71042ce475a96c7fa134177a01959d0b", "interpretation_Tm_abs_c5cfacc785df376403b58f49cdaf22b6", "inversion-interp", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_89263c8dd7df5c497acdada0682b1aab", "refinement_interpretation_Tm_refine_91c352d831715ed604553457a8078865", "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b", "typing_FStar.Int.Cast.Full.uint64_to_uint128", "typing_FStar.Int.Cast.uint32_to_uint64", "typing_Hacl.Hash.Definitions.block_len", "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, "1aed1513d4f730dcb816c73f8505409e" ], [ "Hacl.HMAC.part2", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "function_token_typing_Lib.IntTypes.uint8", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_9ea1003aec0efc592ecf93af466e5872", "refinement_interpretation_Tm_refine_be9f9b7469d07f7dec61b636d3fadb10", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq" ], 0, "359e3acccd820de189d8b8f13d367a93" ], [ "Hacl.HMAC.update_multi_extra_state_eq'", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned", "equation_Prims.l_imp", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.max_extra_state", "l_imp-interp", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "10e0894bc61ad25d8acddf0eeb407eb5" ], [ "Hacl.HMAC.zero_to_len", 1, 0, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.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.U1", "constructor_distinct_Lib.IntTypes.U128", "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", "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_Lib.IntTypes.PUB@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.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_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.len_int_type", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "int_typing", "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_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_bdf26c5e5a33d51389e46e73076cb41b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.unsigned", "typing_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Spec.Blake2.Blake2B@tok" ], 0, "dcc811d7f995bfcfe3960af5dec17e99" ], [ "Hacl.HMAC.part2", 2, 0, 0, [ "@query" ], 0, "ed0f014f3a60730520fb1e45be0abc43" ], [ "Hacl.HMAC.part2", 3, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Spec.Hash.Definitions_interpretation_Tm_arrow_3ac874e39b1c409ba69a2358a6f73691", "Spec.Hash.Definitions_interpretation_Tm_arrow_700344b580b048f3613bf7b7b4c8e2a3", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.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.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.MD5", "data_typing_intro_Prims.Mkdtuple2@tok", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.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.MD5@tok", "equation_FStar.Int.Cast.uint32_to_uint64", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Pervasives.Native.snd", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.HMAC.block_len_as_len", "equation_Hacl.HMAC.zero_to_len", "equation_Hacl.Hash.Definitions.block_len", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.impl", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.m_spec", "equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.UpdateMulti.split_at_last_nb_rem", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.Hash.hash", "equation_Spec.Agile.Hash.init", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.extra_state_add_nat", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.extra_state_v", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.len_int_type", "equation_Spec.Hash.Definitions.len_t", "equation_Spec.Hash.Definitions.len_v", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.nat_to_extra_state", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state", "equation_Spec.Hash.Incremental.hash", "equation_Spec.Hash.Incremental.hash_incremental", "equation_Spec.Hash.Incremental.update_last", "equation_Spec.Hash.PadFinish.finish", "fuel_guarded_inversion_Lib.IntTypes.inttype", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "interpretation_Tm_abs_3d77c1d80c0e9e736cdcf018f4780b14", "interpretation_Tm_abs_71042ce475a96c7fa134177a01959d0b", "interpretation_Tm_abs_c5cfacc785df376403b58f49cdaf22b6", "kinding_Spec.Hash.Definitions.hash_alg@tok", "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_FStar.UInt64.vu_inv", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.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_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_04a9ebd495e7d8fd136248ca5b2886b6", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_11f5c63c78caccafb41a6490396f36ec", "refinement_interpretation_Tm_refine_17b5c82e827d21e595c1a46cf8137822", "refinement_interpretation_Tm_refine_362e2dfd5fc10941f1049c892a15d4e9", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_48c1b5b4c02ad49f0760911a9d4b1fb4", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_547240b2475f155577e710689cbdcde0", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_78b07d046e0e1b1d01748fe396158efe", "refinement_interpretation_Tm_refine_7c955506f48315c82b6ef24ec99f68c4", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_89263c8dd7df5c497acdada0682b1aab", "refinement_interpretation_Tm_refine_91c352d831715ed604553457a8078865", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9ea1003aec0efc592ecf93af466e5872", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_be9f9b7469d07f7dec61b636d3fadb10", "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e1893e719eb67a6fea41466940e12136", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Int.Cast.Full.uint64_to_uint128", "typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_FStar.UInt64.uint_to_t", "typing_FStar.UInt64.v", "typing_Hacl.HMAC.block_len_as_len", "typing_Hacl.HMAC.zero_to_len", "typing_Hacl.Hash.Definitions.block_len", "typing_Hacl.Hash.Definitions.impl_word", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.op_At_Percent_Dot", "typing_Lib.IntTypes.u128", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Lib.UpdateMulti.split_at_last_nb_rem", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.Agile.Hash.init", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.hash_length", "typing_Spec.Hash.Definitions.init_t", "typing_Spec.Hash.Definitions.len_int_type", "typing_Spec.Hash.Definitions.len_v", "typing_Spec.Hash.Definitions.max_input_length", "typing_Spec.Hash.Definitions.word", "typing_Spec.Hash.Definitions.word_length", "typing_Spec.Hash.Definitions.word_t", "typing_Spec.Hash.PadFinish.finish", "typing_Tm_abs_3d77c1d80c0e9e736cdcf018f4780b14", "typing_Tm_abs_c5cfacc785df376403b58f49cdaf22b6", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2B@tok", "typing_tok_Spec.Blake2.Blake2S@tok", "typing_tok_Spec.Hash.Definitions.MD5@tok", "unit_inversion" ], 0, "efa5b12e2551782485245f72494451b7" ], [ "Hacl.HMAC.part1", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U64", "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.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.HMAC.uu___19", "equation_Lib.IntTypes.uint8", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.squash", "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.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_Hacl.HMAC.uu___19", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Spec.AES.elem", "inversion-interp", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_9ea1003aec0efc592ecf93af466e5872", "refinement_interpretation_Tm_refine_be9f9b7469d07f7dec61b636d3fadb10", "refinement_interpretation_Tm_refine_d1e0fb3194452a905c73dd0c802a3ce8", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq" ], 0, "9051e24d218f875fe2b96b61f6b4b174" ], [ "Hacl.HMAC.part1", 2, 0, 0, [ "@query" ], 0, "5358587a059b183cc4b645c03d77b1e7" ], [ "Hacl.HMAC.part1", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.HMAC.uu___19", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.get_spec", "equation_Hacl.Hash.Definitions.hash_len", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.m_spec", "equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "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.hash_length", "equation_Spec.Hash.Definitions.hash_word_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_Hacl.HMAC.uu___19", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_LowStar.Buffer.trivial_preorder", "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "inversion-interp", "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_4", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "lemma_LowStar.Monotonic.Buffer.len_gsub", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_gsub", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "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_Prims.Mkdtuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_04a9ebd495e7d8fd136248ca5b2886b6", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9ea1003aec0efc592ecf93af466e5872", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_be9f9b7469d07f7dec61b636d3fadb10", "refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde", "refinement_interpretation_Tm_refine_d1e0fb3194452a905c73dd0c802a3ce8", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_Prims.pow2.fuel_instrumented", "true_interp", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.hash_len", "typing_Hacl.Impl.Blake2.Core.element_t", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.Hash.Definitions.hash_length", "typing_Spec.Hash.Definitions.word", "typing_tok_Spec.Blake2.Blake2B@tok", "typing_tok_Spec.Blake2.Blake2S@tok" ], 0, "d75e8df0e34e54f00aa4272b595e6a22" ], [ "Hacl.HMAC.block_len_positive", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2S", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.gt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gt", "equation_Hacl.HMAC.uu___19", "equation_Hacl.Hash.Definitions.block_len", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_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.block_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_Hacl.HMAC.uu___19", "int_typing", "inversion-interp", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_91c352d831715ed604553457a8078865", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.block_len", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.unsigned", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2S@tok" ], 0, "0bb4ac5d2f944551f6620addeaa828a4" ], [ "Hacl.HMAC.hash_lt_block", 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.U64", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equation_Hacl.HMAC.uu___19", "equation_Prims.squash", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_Hacl.HMAC.uu___19", "inversion-interp", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "624235187d0bb1122097e58a1515958d" ], [ "Hacl.HMAC.mk_compute", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W31", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W31@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equation_FStar.Pervasives.inversion", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "inversion-interp", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0" ], 0, "847042a3ca926b3507b2a5052ff342d7" ], [ "Hacl.HMAC.mk_compute", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "equality_tok_FStar.Integers.W128@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_stack_region", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_FStar.Seq.Base.op_At_Bar", "equation_FStar.UInt.fits", "equation_FStar.UInt.gt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gt", "equation_Hacl.HMAC.uu___19", "equation_Hacl.Hash.Definitions.block_len", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.get_spec", "equation_Hacl.Hash.Definitions.hash_len", "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_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.UpdateMulti.uint8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.HMAC.hmac", "equation_Spec.Agile.HMAC.keysized", "equation_Spec.Agile.HMAC.lbytes", "equation_Spec.Agile.HMAC.wrap", "equation_Spec.Agile.HMAC.xor", "equation_Spec.Agile.Hash.hash", "equation_Spec.Agile.Hash.update_multi", "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.bytes_blocks", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.init_t", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.PadFinish.finish", "equation_Spec.Hash.PadFinish.pad", "fuel_guarded_inversion_Prims.dtuple2", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Hacl.HMAC.uu___19", "function_token_typing_Lib.IntTypes.logxor", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_LowStar.Buffer.trivial_preorder", "function_token_typing_Prims.int", "function_token_typing_Spec.AES.elem", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "inversion-interp", "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.len_gsub", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_gsub", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.modifies_remove_new_locs", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05366f5ca3e541f743dee81ac7432346", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0a37bf974acc755a6e9139e70df487ed", "refinement_interpretation_Tm_refine_0bc360a5ac00fe13199bbc33aee6e518", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_16da5dd636ef303f4b4402f063fe1ef3", "refinement_interpretation_Tm_refine_16efc88e9604996ecc250c29d79634de", "refinement_interpretation_Tm_refine_23bfe440c509828a878245c97e027d03", "refinement_interpretation_Tm_refine_29c27ac7c716b2238749315b70c9eca3", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_3a83db907d3f22ca21d4739c54f5f3dc", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_442f983acb7c1dea69e3f74140aec586", "refinement_interpretation_Tm_refine_45fb1fe6d11e460ce7fa5c267d49a18f", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_516841552c075993547f605f17f21002", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6f930c9f83a3c6ef3b845dfdceffecfa", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_84b445a9be69afc52bd3400a259c3da3", "refinement_interpretation_Tm_refine_850fe300f875565a60c2c1ce43a6fda4", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "refinement_interpretation_Tm_refine_90e72dc1c8f4dbee5ee8383a856b01a0", "refinement_interpretation_Tm_refine_91c352d831715ed604553457a8078865", "refinement_interpretation_Tm_refine_9ca7807bfc284168a2426f4440262824", "refinement_interpretation_Tm_refine_a8192aab6c37e12d7944ac827ff38cf4", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_a9c350ddba306e523c3c5cd42b3c7c84", "refinement_interpretation_Tm_refine_b61185bd7bfa9db1bf20ad7e18b96aab", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_dd714287f0649cab02c8c744333cfbf5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e270172744dd496982994cf468253759", "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f2f0f2e9a5870778fa3e574677dadde8", "refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004", "refinement_interpretation_Tm_refine_fc53d5763564ace78ef2c4a24fe7bd2f", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Lib.IntTypes.logxor", "true_interp", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Map.sel", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_rid_ctr", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar", "typing_FStar.Set.complement", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.block_len", "typing_Hacl.Hash.Definitions.get_alg", "typing_Hacl.Hash.Definitions.get_spec", "typing_Hacl.Hash.Definitions.hash_len", "typing_Hacl.Hash.Definitions.impl_word", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.Agile.HMAC.xor", "typing_Spec.Agile.Hash.hash", "typing_Spec.Agile.Hash.init", "typing_Spec.Agile.Hash.update_multi", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.hash_length", "typing_Spec.Hash.Definitions.word", "typing_Spec.Hash.PadFinish.finish", "typing_Spec.Hash.PadFinish.finish_md", "typing_Spec.Hash.PadFinish.pad", "typing_Spec.Loops.seq_map", "typing_Spec.Loops.seq_map2", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Blake2.Blake2S@tok", "unit_inversion" ], 0, "60b5b1487f15baf231cc52f10ef3a824" ] ] ]