[ "È$Ÿ\u0003Žƒþö²?Šx›‚?c", [ [ "Hacl.Hash.Core.SHA1._h0", 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, "f776522808cab33e59e1a0d449413ab1" ], [ "Hacl.Hash.Core.SHA1.legacy_alloca", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_typing", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA1", "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_FStar.Monotonic.HyperStack.is_stack_region", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Pervasives.pattern", "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.uint32", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Agile.Hash.init", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA1.h0", "equation_Spec.SHA1.init", "function_token_typing_FStar.Pervasives.pattern", "function_token_typing_Lib.IntTypes.uint32", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "primitive_Prims.op_GreaterThan", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Prims.Mkdtuple2__1", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4dd3fe13ba2ac81d13f00faa0949c051", "refinement_interpretation_Tm_refine_9ca7807bfc284168a2426f4440262824", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_ee8b234aa6cf07c6ef04345829148435", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Set.singleton", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_unused_in", "unit_typing" ], 0, "0b0866316b05b4c304d75c9b37b3473c" ], [ "Hacl.Hash.Core.SHA1.h0", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "constructor_distinct_Spec.Hash.Definitions.SHA1", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state_", "equation_Spec.SHA1.h0", "int_inversion", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_0207297b10867c240da10ed929d36896", "refinement_interpretation_Tm_refine_728e2b11bbc45a9bb5659524bb5e8df3", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.v", "typing_Hacl.Hash.Core.SHA1._h0", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.SHA1.h0" ], 0, "d631359d71227d7dce655b5db010f846" ], [ "Hacl.Hash.Core.SHA1.legacy_init", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA1", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "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.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.impl_state_length", "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.trivial_preorder", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.Hash.init", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state_", "equation_Spec.SHA1.h0", "equation_Spec.SHA1.init", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_LowStar.Buffer.trivial_preorder", "int_inversion", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Seq.Base.lemma_index_upd1", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Seq.Properties.slice_upd", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_Addition", "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_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_23191c2fbaaffdb92df408516c7c493b", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_3f6620efd5cc444f4942c3c8a9ee4671", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_9e5431dc8b1642920ee351bea45b8660", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f0a13c58175fb79a1af649f9f29634ff", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fbd0051d8d71ed03a228291982b893b2", "true_interp", "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", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.minint", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA1.h0", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok", "unit_inversion" ], 0, "8ea2228cd2247abed4985e61a76a6b41" ], [ "Hacl.Hash.Core.SHA1.w_inv'", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Hash.Definitions.SHA1@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.Hash.Core.SHA1.w_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.Hash.Definitions.word", "int_inversion", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.Hash.Definitions.word", "typing_tok_Spec.Hash.Definitions.SHA1@tok" ], 0, "d08d073fefd9c0b447eef75b99cacc9f" ], [ "Hacl.Hash.Core.SHA1.w_loop_inv", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA1", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "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.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Core.SHA1.block_t", "equation_Hacl.Hash.Core.SHA1.w_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "lemma_FStar.Map.lemma_ContainsDom", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "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", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe", "refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.word", "typing_Spec.Hash.Definitions.word_t", "typing_tok_Spec.Hash.Definitions.SHA1@tok" ], 0, "313cf6b14137642907adc6cdbc6ec1c8" ], [ "Hacl.Hash.Core.SHA1.w_inv_elim", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "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.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Core.SHA1.w_inv_", "equation_Hacl.Hash.Core.SHA1.w_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.Hash.Definitions.word", "function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion", "l_and-interp", "lemma_FStar.Map.lemma_ContainsDom", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.Hash.Definitions.word", "typing_tok_Spec.Hash.Definitions.SHA1@tok" ], 0, "3457f972b584e55298eca1e3ef3d82d3" ], [ "Hacl.Hash.Core.SHA1.w_loop_inv_elim", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA1", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "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.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Core.SHA1.block_t", "equation_Hacl.Hash.Core.SHA1.w_inv_", "equation_Hacl.Hash.Core.SHA1.w_loop_inv", "equation_Hacl.Hash.Core.SHA1.w_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "l_and-interp", "lemma_FStar.Map.lemma_ContainsDom", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe", "refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.word", "typing_Spec.Hash.Definitions.word_t", "typing_tok_Spec.Hash.Definitions.SHA1@tok" ], 0, "b25a0c545da50f65e1bbceac99198ae2" ], [ "Hacl.Hash.Core.SHA1.index_32_be'", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.SHA1", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.SHA1@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_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_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.Sequence.to_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.Blake2.wt", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.mul_lemma", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "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_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05eeb8a0f4055e228bd046054bddb62d", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86", "refinement_interpretation_Tm_refine_a2ab50b26a5c765696073ecc7252b93b", "refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.v", "typing_Lib.Buffer.as_seq", "typing_Lib.ByteSequence.uint_at_index_be", "typing_Lib.ByteSequence.uints_from_bytes_be", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.mul", "typing_Lib.IntTypes.numbytes", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.index", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.word", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2S@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok" ], 0, "4483574f449db798709746ad60cc0ccf" ], [ "Hacl.Hash.Core.SHA1.w_body_value", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Spec.SHA1.w_.fuel_instrumented", "@fuel_irrelevance_Spec.SHA1.w_.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA1", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits", "equation_FStar.UInt.lt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lt", "equation_Hacl.Hash.Core.SHA1.block_t", "equation_Hacl.Hash.Core.SHA1.w_inv_", "equation_Hacl.Hash.Core.SHA1.w_loop_inv", "equation_Hacl.Hash.Core.SHA1.w_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.rotval", "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_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA1.w", "equation_Spec.SHA1.word_block", "equation_with_fuel_Spec.SHA1.w_.fuel_instrumented", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0da46ef8643a6f8ea97a3358bc923338", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_2a9d64ff26e8ce8dfca85e1c63876c34", "refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef", "refinement_interpretation_Tm_refine_af3524604a4dfd4f05f8932c14c56d0d", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e94019ba296cc08a679d3ed9759b4476", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_05e15190c946858f68c69156f585f95a", "typing_FStar.Ghost.reveal", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Lib.ByteSequence.uints_from_bytes_be", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.block_word_length", "typing_Spec.Hash.Definitions.word", "typing_Spec.Hash.Definitions.word_t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok" ], 0, "f087e8d03585ffa3bce81eb319278c1e" ], [ "Hacl.Hash.Core.SHA1.lt_S_r", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "e763069ee6d4a4d09af2871660818c08" ], [ "Hacl.Hash.Core.SHA1.w_body", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA1", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Core.SHA1.block_t", "equation_Hacl.Hash.Core.SHA1.w_inv_", "equation_Hacl.Hash.Core.SHA1.w_loop_inv", "equation_Hacl.Hash.Core.SHA1.w_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_LowStar.Buffer.trivial_preorder", "int_inversion", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "l_and-interp", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.Seq.Base.lemma_index_upd1", "lemma_FStar.Seq.Base.lemma_index_upd2", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "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_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5fafc2da9e45e4cc64ee84722312dc27", "refinement_interpretation_Tm_refine_703a7d2fe02b9ca7064a2cc5d0ed1a46", "refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292", "refinement_interpretation_Tm_refine_e94019ba296cc08a679d3ed9759b4476", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_05e15190c946858f68c69156f585f95a", "true_interp", "typing_FStar.Ghost.reveal", "typing_FStar.UInt32.v", "typing_Lib.ByteSequence.uints_from_bytes_be", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.block_word_length", "typing_Spec.Hash.Definitions.word", "typing_Spec.Hash.Definitions.word_t", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok" ], 0, "c252c18b5c6e6f70efe1ab505845e394" ], [ "Hacl.Hash.Core.SHA1.w", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA1", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Core.SHA1.block_t", "equation_Hacl.Hash.Core.SHA1.w_inv", "equation_Hacl.Hash.Core.SHA1.w_inv_", "equation_Hacl.Hash.Core.SHA1.w_loop_inv", "equation_Hacl.Hash.Core.SHA1.w_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "l_and-interp", "lemma_FStar.Ghost.reveal_hide", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "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", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe", "refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef", "refinement_interpretation_Tm_refine_b87605c86393b1c8de25a0c93c8c3f2a", "refinement_interpretation_Tm_refine_d9a69009508517dad67f8347944dbb2f", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_05e15190c946858f68c69156f585f95a", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.word", "typing_Spec.Hash.Definitions.word_t", "typing_tok_Spec.Hash.Definitions.SHA1@tok" ], 0, "ff0db660a2a7d2fee0433f655c5ef40b" ], [ "Hacl.Hash.Core.SHA1.upd5", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat", "function_token_typing_LowStar.Buffer.trivial_preorder", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Base.lemma_index_upd1", "lemma_FStar.Seq.Base.lemma_index_upd2", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0575197a5bfbce094fbbc4752d6f0a83", "refinement_interpretation_Tm_refine_47f7d72cb804a2caca3569d60da54e94", "refinement_interpretation_Tm_refine_482b06e5a74271bbd8c3d69550d68f59", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_544f8a10e8878f55a9f2150d7d422a71", "refinement_interpretation_Tm_refine_93cc928978a8436a38153dd4de924396", "refinement_interpretation_Tm_refine_cadd301a6914616c995234a1c6ddfae6", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292", "true_interp", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, "8c6762d6fd67db452a4a8583e4916d1c" ], [ "Hacl.Hash.Core.SHA1.step3_body", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Ghost_interpretation_Tm_ghost_arrow_e2f4c1991753137c5a80c115428d0cef", "Spec.SHA1_interpretation_Tm_arrow_5179a47a8889eaf0f9b968a3cecd04b1", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Nil@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", "equality_tok_Spec.Hash.Definitions.SHA1@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.Hash.Core.SHA1.w_inv", "equation_Hacl.Hash.Core.SHA1.w_inv_", "equation_Hacl.Hash.Core.SHA1.w_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.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.rotval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Blake2.wt", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA1.step3_body__aux", "equation_Spec.SHA1.step3_body_w_t", "equation_Spec.SHA1.w", "equation_Spec.SHA1.word_block", "function_token_typing_FStar.Ghost.reveal", "function_token_typing_Spec.SHA1.step3_body_", "function_token_typing_Spec.SHA1.word_block", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "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_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0da46ef8643a6f8ea97a3358bc923338", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_2330bfff5710f734831dc0ce705b738d", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_457b459ca55b425569fac95945d04d19", "refinement_interpretation_Tm_refine_50f3dcb312c61cacd85d8a19ef243108", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_703a7d2fe02b9ca7064a2cc5d0ed1a46", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef", "refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fbd0051d8d71ed03a228291982b893b2", "token_correspondence_FStar.Ghost.reveal", "token_correspondence_Spec.SHA1.step3_body__aux", "typing_FStar.Ghost.reveal", "typing_FStar.Seq.Properties.seq_of_list", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA1.step3_body_w_t", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2S@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok" ], 0, "75e02ca9ec9530f6e53ec2f05954f797" ], [ "Hacl.Hash.Core.SHA1.zero_out", 1, 0, 0, [ "@query" ], 0, "0656904da63fb008a85a3552cf653e94" ], [ "Hacl.Hash.Core.SHA1.zero_out", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA1", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "function_token_typing_Lib.IntTypes.uint32", "function_token_typing_LowStar.Buffer.trivial_preorder", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_1dadea411cd6aea069a22f4ce6ad367e", "refinement_interpretation_Tm_refine_22ea23156c96d1f95a36c1bf3ce83086", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_85b64abb9c2f68e7bad1761e265ecae9", "refinement_interpretation_Tm_refine_879c0531660edf141e05adab3475474e", "refinement_interpretation_Tm_refine_f00f8a5027d18e4477fe20cd6a8e47aa", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "true_interp", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.Hash.Definitions.word", "typing_tok_Spec.Hash.Definitions.SHA1@tok" ], 0, "4265c16425451caa734a4c60b91cf37e" ], [ "Hacl.Hash.Core.SHA1.spec_step3_body_spec", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Hacl.Hash.Core.SHA1_interpretation_Tm_ghost_arrow_da60a61d14eb1c0331a4dc86bf2c2dca", "Prims_interpretation_Tm_ghost_arrow_0283b8a2a36bbec52abac4e3d837674a", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_Hacl.Hash.Core.SHA1.spec_step3_body", "equation_Prims.nat", "equation_Spec.Hash.Definitions.words_state_", "int_inversion", "interpretation_Tm_abs_62aaf056568631d5754c2c14b4a324fd", "refinement_interpretation_Tm_refine_457b459ca55b425569fac95945d04d19", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_785b445c1ccb59eaa8c666ff5bddec28", "typing_FStar.Ghost.elift1", "typing_Spec.Hash.Definitions.words_state_", "typing_Tm_abs_62aaf056568631d5754c2c14b4a324fd", "typing_tok_Spec.Hash.Definitions.SHA1@tok" ], 0, "7cdceb140a8af9371dc03863a20bf9bb" ], [ "Hacl.Hash.Core.SHA1.step3", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_interpretation_Tm_ghost_arrow_0283b8a2a36bbec52abac4e3d837674a", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "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", "disc_equation_Lib.IntTypes.U1", "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", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Core.SHA1.block_t", "equation_Hacl.Hash.Core.SHA1.w_inv", "equation_Hacl.Hash.Core.SHA1.w_inv_", "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.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "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_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.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.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA1.compute_w_post", "equation_Spec.SHA1.index_compute_w", "equation_Spec.SHA1.step3_aux", "equation_Spec.SHA1.step3_body", "equation_Spec.SHA1.step3_body_w_t", "equation_Spec.SHA1.word_block", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "function_token_typing_Spec.AES.elem", "function_token_typing_Spec.SHA1.step3", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "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_SelRestrict", "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.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.v_injective", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_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_refl", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "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_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6ba711c7854d10c818e9d6022d656341", "refinement_interpretation_Tm_refine_785b445c1ccb59eaa8c666ff5bddec28", "refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe", "refinement_interpretation_Tm_refine_85b64abb9c2f68e7bad1761e265ecae9", "refinement_interpretation_Tm_refine_95d2f32c9608a129985d09595b364fb2", "refinement_interpretation_Tm_refine_9ed44a6b10d62b880210b61e1a37244f", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_ac610c44db3499d978ac6426f5f2bbef", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_c15406b3d261dc8b803d00b30feb4a21", "refinement_interpretation_Tm_refine_cb09561566fe068316d5427c33177577", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_d9a69009508517dad67f8347944dbb2f", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_c53e9dfd29518a0fc0a25ae71ce08b98", "token_correspondence_FStar.Ghost.reveal", "token_correspondence_Spec.SHA1.index_compute_w", "token_correspondence_Spec.SHA1.step3_aux", "typing_FStar.Ghost.elift1", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_rid_ctr", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Seq.Base.empty", "typing_FStar.Set.complement", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA1.step3_body_w_t", "typing_Tm_abs_ed4cda90676a02d35713650cfe70afa7", "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.SHA1@tok" ], 0, "4991eacb9b6c8b43793434f1645403ec" ], [ "Hacl.Hash.Core.SHA1.step4", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "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", "disc_equation_Lib.IntTypes.U1", "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", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Hash.Core.SHA1.block_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.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "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.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.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.SHA1.step4_aux", "equation_Spec.SHA1.word_block", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Spec.AES.elem", "function_token_typing_Spec.SHA1.step4", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "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_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_8142c1c93b5055bbd3e479a8841d25fe", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_c15406b3d261dc8b803d00b30feb4a21", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fbd0051d8d71ed03a228291982b893b2", "token_correspondence_Spec.SHA1.step4_aux", "typing_FStar.UInt32.v", "typing_Lib.ByteSequence.uints_from_bytes_be", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.AES.gf8", "typing_Spec.Blake2.wt", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA1.step4", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2S@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok" ], 0, "4b61a0a3894fc80ea30ae460c28555bd" ], [ "Hacl.Hash.Core.SHA1.legacy_update", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Spec.Hash.Definitions.SHA1", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_Hacl.Hash.Definitions.as_seq", "equation_Hacl.Hash.Definitions.get_alg", "equation_Hacl.Hash.Definitions.impl_word", "equation_Hacl.Hash.Definitions.state", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.Hash.update", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.words_of_bytes", "equation_Spec.SHA1.update", "equation_Spec.SHA1.update_aux", "equation_Spec.SHA1.words_of_bytes_block", "function_token_typing_Lib.ByteSequence.uints_from_bytes_be", "function_token_typing_Lib.IntTypes.uint8", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_Prims.Mkdtuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_37c93ce5bbd59eacadc2b1f547360369", "refinement_interpretation_Tm_refine_40989d30627d8a53dce62abb1c22a810", "refinement_interpretation_Tm_refine_a8fa4255b4da3c02c368080086854c4b", "refinement_interpretation_Tm_refine_c15406b3d261dc8b803d00b30feb4a21", "token_correspondence_Spec.Agile.Hash.update", "token_correspondence_Spec.Hash.Definitions.words_of_bytes", "token_correspondence_Spec.SHA1.update_aux", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.Hash.Definitions.word", "typing_tok_Spec.Hash.Definitions.SHA1@tok", "unit_inversion" ], 0, "f24a8a06598a2831b195a32f381bf80c" ] ] ]