[ "çd‹¼4¨<þ\u001e”`t\bx½Ÿ", [ [ "Test.Hash.main", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_EverCrypt.Hash.footprint", "equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.state", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.mem", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.get", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_FStar.Monotonic.Heap.heap", "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_stack_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt", "lemma_FStar.Set.lemma_equal_elim", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_ef69f133013e18d05e94f8542fb2b129", "typing_EverCrypt.Hash.footprint", "typing_EverCrypt.Hash.state_s", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "typing_tok_Spec.Hash.Definitions.SHA2_384@tok" ], 0, "d160dbd25eb7497b37ff9aef2efa84eb" ], [ "Test.Hash.test_incremental_api", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Hacl.Streaming.MD_interpretation_Tm_arrow_044c017c58feaf8aab37cff2118fb570", "bool_inversion", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Hacl.Streaming.Interface.Erased", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Hacl.Streaming.Interface.Erased@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_EverCrypt.Hash.Incremental.agile_state", "equation_EverCrypt.Hash.Incremental.evercrypt_hash", "equation_EverCrypt.Hash.Incremental.hash_len", "equation_EverCrypt.Hash.Incremental.hashed", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.HyperStack.ST.is_eternal_region", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "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.live_region", "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_Hacl.Hash.Definitions.hash_len", "equation_Hacl.Streaming.Functor.bytes", "equation_Hacl.Streaming.Functor.footprint", "equation_Hacl.Streaming.Functor.preserves_freeable", "equation_Hacl.Streaming.Functor.state_", "equation_Hacl.Streaming.Functor.uint8", "equation_Hacl.Streaming.Interface.optional_key", "equation_Hacl.Streaming.Interface.stateful_unused", "equation_Hacl.Streaming.MD.max_input_length64", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.Monotonic.Buffer.loc_in", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_EverCrypt.Hash.state", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Hacl.Streaming.MD.max_input_length64", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "interpretation_Tm_abs_5b0a5035fa5841c294d07b56f6db9e4b", "interpretation_Tm_abs_7db19245573865e2013f96b9787edb72", "interpretation_Tm_abs_d83a42cc5aa4f1e756aa03c5fe71bbb8", "interpretation_Tm_abs_f006d723251ddaabe831b91f6d482a4e", "kinding_Spec.Hash.Definitions.hash_alg@tok", "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_non_tip_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Monotonic.HyperStack.lemma_map_invariant", "lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors", "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.UInt32.uv_inv", "lemma_Hacl.Streaming.Functor.frame_invariant", "lemma_Hacl.Streaming.Functor.frame_seen", "lemma_Hacl.Streaming.Functor.invariant_loc_in_footprint", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.live_region_frameOf", "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_trans_backwards", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "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_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_Hacl.Streaming.Interface.Block_key", "proj_equation_Hacl.Streaming.Interface.Block_km", "proj_equation_Hacl.Streaming.Interface.Block_max_input_length", "proj_equation_Hacl.Streaming.Interface.Block_output_len", "proj_equation_Hacl.Streaming.Interface.Block_spec_s", "proj_equation_Hacl.Streaming.Interface.Block_state", "proj_equation_Hacl.Streaming.Interface.Stateful_footprint", "proj_equation_Hacl.Streaming.Interface.Stateful_invariant", "proj_equation_Hacl.Streaming.Interface.Stateful_s", "proj_equation_Hacl.Streaming.Interface.Stateful_t", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Hacl.Streaming.Interface.Block_key", "projection_inverse_Hacl.Streaming.Interface.Block_km", "projection_inverse_Hacl.Streaming.Interface.Block_max_input_length", "projection_inverse_Hacl.Streaming.Interface.Block_output_len", "projection_inverse_Hacl.Streaming.Interface.Block_spec_s", "projection_inverse_Hacl.Streaming.Interface.Block_state", "projection_inverse_Hacl.Streaming.Interface.Stateful_footprint", "projection_inverse_Hacl.Streaming.Interface.Stateful_invariant", "projection_inverse_Hacl.Streaming.Interface.Stateful_s", "projection_inverse_Hacl.Streaming.Interface.Stateful_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_038ead423eaeac9d1f99a478e977a313", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_29dae789cff2d2c963c0518de679b240", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_91ab4fbe024600fc5affdfcd022c9b32", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce", "refinement_interpretation_Tm_refine_d76979c3f3259a42f119e76969d444f7", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_ee8b234aa6cf07c6ef04345829148435", "refinement_interpretation_Tm_refine_f302e1c5e7902e028b3edb61ef25df5a", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_EverCrypt.Hash.Incremental.hash_len", "token_correspondence_Hacl.Streaming.Interface.__proj__Block__item__max_input_length", "token_correspondence_Hacl.Streaming.Interface.__proj__Block__item__output_len", "token_correspondence_Hacl.Streaming.Interface.__proj__Block__item__spec_s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__footprint", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__invariant", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__s", "token_correspondence_Hacl.Streaming.Interface.__proj__Stateful__item__t", "token_correspondence_Hacl.Streaming.MD.max_input_length64", "token_correspondence_Spec.Agile.Hash.hash", "true_interp", "typing_EverCrypt.Hash.Incremental.evercrypt_hash", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp", "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_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.empty", "typing_FStar.Seq.Properties.seq_of_list", "typing_FStar.Set.complement", "typing_FStar.Set.singleton", "typing_Hacl.Streaming.Functor.footprint", "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.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok" ], 0, "1df4b8e2463c3e13d3926ee9ae1e78d5" ] ] ]