Revision b5e85960e109efb08b9c65a4ab85c9b4ef926419 authored by Jay Bosamiya on 04 June 2019, 18:24:09 UTC, committed by Jay Bosamiya on 04 June 2019, 18:24:09 UTC
1 parent 2a5defc
EverCrypt.Hash.fst.hints
[
"���[aw\u0005�0�,�\u001c���",
[
[
"EverCrypt.Hash.uu___1",
1,
0,
0,
[ "@query" ],
0,
"c64232a5fc3478634d9719fb2125febf"
],
[
"EverCrypt.Hash.string_of_alg",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Spec.Hash.Definitions.MD5",
"disc_equation_Spec.Hash.Definitions.SHA1",
"disc_equation_Spec.Hash.Definitions.SHA2_224",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_384",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equation_FStar.Pervasives.inversion",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"inversion-interp"
],
0,
"19d8c29890deec640fb9a70f45b7fe0b"
],
[
"EverCrypt.Hash.broken_alg",
1,
0,
0,
[ "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq" ],
0,
"8d2e1e9d6bd7f0a7709d622aa76ea0c7"
],
[
"EverCrypt.Hash.alg13",
1,
0,
0,
[ "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq" ],
0,
"c5c3c24d066222434fcbbba1807669e6"
],
[
"EverCrypt.Hash.uint32_fits_maxLength",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.Pervasives.inversion", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t",
"equation_Spec.Hash.Definitions.max_input_length",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"function_token_typing_Prims.__cache_version_number__",
"inversion-interp", "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_a347709bfeba48709474ad26f4f6be87",
"typing_FStar.UInt32.v"
],
0,
"b92619aba527ac47273e019014fd51d4"
],
[
"EverCrypt.Hash.__proj__MD5_s__item__p",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.Hash.MD5_s",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_8007cc95e31283ec70894170e620c8b9"
],
0,
"0000a0ed1613a4032224e82debd5b9fb"
],
[
"EverCrypt.Hash.__proj__SHA1_s__item__p",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.Hash.SHA1_s",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_365674ad36822dbcb25c1243141f7b4a"
],
0,
"eb149b7f923015007ba02736865d7cd5"
],
[
"EverCrypt.Hash.__proj__SHA2_224_s__item__p",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.Hash.SHA2_224_s",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_ca18a58ab4d414f80248e3f3a4fb8b38"
],
0,
"0b9253bc2ed609aa15c08fefe5f9b8af"
],
[
"EverCrypt.Hash.__proj__SHA2_256_s__item__p",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.Hash.SHA2_256_s",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_c03ee29b1b15c93d78f1ddc22e14ee9e"
],
0,
"da764af588c15fb922819ff6d9f1661f"
],
[
"EverCrypt.Hash.__proj__SHA2_384_s__item__p",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.Hash.SHA2_384_s",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_99efc18aeab03ed24138e5c951959832"
],
0,
"4eddd60a0793e85848011a4ffe6807b6"
],
[
"EverCrypt.Hash.__proj__SHA2_512_s__item__p",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.Hash.SHA2_512_s",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_3d72f362bdb97a0947d9a19041fd4bda"
],
0,
"96fd77e500edcdb68e33ceade5b1f1c9"
],
[
"EverCrypt.Hash.p",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "data_elim_EverCrypt.Hash.MD5_s",
"data_elim_EverCrypt.Hash.SHA1_s",
"data_elim_EverCrypt.Hash.SHA2_224_s",
"data_elim_EverCrypt.Hash.SHA2_256_s",
"data_elim_EverCrypt.Hash.SHA2_384_s",
"data_elim_EverCrypt.Hash.SHA2_512_s",
"disc_equation_EverCrypt.Hash.MD5_s",
"disc_equation_EverCrypt.Hash.SHA1_s",
"disc_equation_EverCrypt.Hash.SHA2_224_s",
"disc_equation_EverCrypt.Hash.SHA2_256_s",
"disc_equation_EverCrypt.Hash.SHA2_384_s",
"disc_equation_EverCrypt.Hash.SHA2_512_s",
"fuel_guarded_inversion_EverCrypt.Hash.state_s", "inversion-interp",
"lemma_EverCrypt.Hash.invert_state_s"
],
0,
"d54573c245287b31def102a3c48463d8"
],
[
"EverCrypt.Hash.loc_includes_union_l_footprint_s",
1,
0,
0,
[ "@query" ],
0,
"bf9214012a55eb12b8afab7534a2aabd"
],
[
"EverCrypt.Hash.invariant",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_EverCrypt.Hash.state",
"equation_LowStar.Buffer.pointer",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e"
],
0,
"63b7cefd1903c980f79c4ee20fb3ae10"
],
[
"EverCrypt.Hash.repr",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_EverCrypt.Hash.p",
"equation_EverCrypt.Hash.state",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Monotonic.Buffer.get",
"equation_Spec.Hash.Definitions.word",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2523390c9a3c6feeaafd4eb8b8df319e",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_EverCrypt.Hash.p", "typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder"
],
0,
"f072cb25a1b133f4b575b4d1bc142481"
],
[
"EverCrypt.Hash.fresh_is_disjoint",
1,
0,
0,
[
"@query", "equation_EverCrypt.Hash.fresh_loc",
"equation_EverCrypt.Hash.loc_in",
"equation_EverCrypt.Hash.loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2"
],
0,
"a2d515add2dd38318f8f790f4eac146e"
],
[
"EverCrypt.Hash.invariant_loc_in_footprint",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_typing",
"equation_EverCrypt.Hash.footprint",
"equation_EverCrypt.Hash.footprint_s",
"equation_EverCrypt.Hash.invariant",
"equation_EverCrypt.Hash.invariant_s",
"equation_EverCrypt.Hash.loc_in", "equation_EverCrypt.Hash.p",
"equation_EverCrypt.Hash.state",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_typing",
"kinding_EverCrypt.Hash.state_s@tok",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.p",
"typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.get",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in"
],
0,
"938417f06242d1bcf1850e0ec3d2df7f"
],
[
"EverCrypt.Hash.frame_invariant",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
"equation_Prims.squash", "l_and-interp",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"6e9e3026b6b4e363f146e694b4e05357"
],
[
"EverCrypt.Hash.frame_invariant",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "equation_EverCrypt.Hash.acc",
"equation_EverCrypt.Hash.footprint",
"equation_EverCrypt.Hash.footprint_s",
"equation_EverCrypt.Hash.invariant",
"equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p",
"equation_EverCrypt.Hash.repr", "equation_EverCrypt.Hash.repr_eq",
"equation_EverCrypt.Hash.state",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.words_state",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"kinding_EverCrypt.Hash.state_s@tok",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.p",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer"
],
0,
"566493f7e0777ce1b28952db88b9ef5d"
],
[
"EverCrypt.Hash.frame_invariant_implies_footprint_preservation",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "equation_EverCrypt.Hash.footprint",
"equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.state",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_typing",
"kinding_EverCrypt.Hash.state_s@tok",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"typing_EverCrypt.Hash.footprint_s", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.get",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer"
],
0,
"4f8abbebdd98cc823cea78bdcd58bc44"
],
[
"EverCrypt.Hash.alloca",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "constructor_distinct_EverCrypt.Hash.MD5_s",
"constructor_distinct_EverCrypt.Hash.SHA1_s",
"constructor_distinct_EverCrypt.Hash.SHA2_224_s",
"constructor_distinct_EverCrypt.Hash.SHA2_256_s",
"constructor_distinct_EverCrypt.Hash.SHA2_384_s",
"constructor_distinct_EverCrypt.Hash.SHA2_512_s",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"data_elim_EverCrypt.Hash.MD5_s",
"disc_equation_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.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_EverCrypt.Hash.footprint",
"equation_EverCrypt.Hash.footprint_s",
"equation_EverCrypt.Hash.fresh_loc",
"equation_EverCrypt.Hash.invariant",
"equation_EverCrypt.Hash.invariant_s",
"equation_EverCrypt.Hash.loc_in",
"equation_EverCrypt.Hash.loc_unused_in", "equation_EverCrypt.Hash.p",
"equation_EverCrypt.Hash.state",
"equation_EverCrypt.Helpers.uint64_t",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_stack_region",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Pervasives.inversion",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.uint_t",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype",
"equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_Lib.IntTypes.pub_uint64",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing", "inversion-interp",
"kinding_EverCrypt.Hash.state_s@tok",
"lemma_EverCrypt.Hash.invariant_loc_in_footprint",
"lemma_EverCrypt.Hash.invert_state_s",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_addresses",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_1",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_addresses_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.Hash.MD5_s_p",
"projection_inverse_EverCrypt.Hash.SHA1_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_224_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_256_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_384_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_512_s_p",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_0523d357087e80b28a8f4bff6aa1d8bc",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_838b1a9782c5991ea1f6e4d693679248",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_9c5977bcc27ba9eb1f57a080c457f330",
"refinement_interpretation_Tm_refine_a50b3723327a6ede703df9aaf02fdc9f",
"refinement_interpretation_Tm_refine_ab1c66d616bd85362b9722be318a8705",
"refinement_interpretation_Tm_refine_b272992b7d44ceac89264799a0045154",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_fd5dc2ec447eac759bd1a12519c2f7d2",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.p",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.is_stack_region",
"typing_FStar.Set.mem", "typing_FStar.Set.singleton",
"typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.get",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_unused_in",
"typing_Spec.Hash.Definitions.uu___is_MD5",
"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,
"c6f46f1d89537d582ba9a51681964516"
],
[
"EverCrypt.Hash.create_in",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "constructor_distinct_EverCrypt.Hash.MD5_s",
"constructor_distinct_EverCrypt.Hash.SHA1_s",
"constructor_distinct_EverCrypt.Hash.SHA2_224_s",
"constructor_distinct_EverCrypt.Hash.SHA2_256_s",
"constructor_distinct_EverCrypt.Hash.SHA2_384_s",
"constructor_distinct_EverCrypt.Hash.SHA2_512_s",
"constructor_distinct_FStar.Integers.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.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"data_elim_EverCrypt.Hash.MD5_s",
"disc_equation_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.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",
"equality_tok_Lib.IntTypes.U64@tok",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_EverCrypt.Hash.footprint",
"equation_EverCrypt.Hash.footprint_s",
"equation_EverCrypt.Hash.freeable",
"equation_EverCrypt.Hash.freeable_s",
"equation_EverCrypt.Hash.fresh_loc",
"equation_EverCrypt.Hash.invariant",
"equation_EverCrypt.Hash.invariant_s",
"equation_EverCrypt.Hash.loc_in",
"equation_EverCrypt.Hash.loc_unused_in", "equation_EverCrypt.Hash.p",
"equation_EverCrypt.Hash.state",
"equation_EverCrypt.Helpers.uint64_t",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_eternal_color",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Pervasives.inversion",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.size_t",
"equation_Lib.IntTypes.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype",
"equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt64.t",
"function_token_typing_Lib.IntTypes.pub_uint64",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_typing",
"inversion-interp", "kinding_EverCrypt.Hash.state_s@tok",
"lemma_EverCrypt.Hash.invert_state_s",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_singleton",
"lemma_FStar.Set.mem_subset",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_addresses",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_1",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_addresses_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.Hash.MD5_s_p",
"projection_inverse_EverCrypt.Hash.SHA1_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_224_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_256_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_384_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_512_s_p",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_24d605dd7e7c87a86a2bff6da7045457",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_550e2751586c4db052dd54634e1b552a",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_601254ebe274211073b2024a11d02039",
"refinement_interpretation_Tm_refine_85b5338ebee887f3315c86d2319cbda7",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c8e5a89d9482f65ae0d582d0b3cc57f4",
"refinement_interpretation_Tm_refine_de0454e4dac6aaab3ede16c58e9a90c3",
"refinement_interpretation_Tm_refine_e74daae1c920bb1b7bcd35b346339506",
"refinement_interpretation_Tm_refine_e9c5fb85d1557055895bcdfc213e38da",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.p",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.color",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.is_eternal_color",
"typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.word",
"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.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_unused_in",
"typing_Spec.Hash.Definitions.uu___is_MD5",
"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,
"566a26f0d71dfa4edf38cfc4ac1c2545"
],
[
"EverCrypt.Hash.create",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_eternal_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",
"lemma_FStar.Monotonic.HyperHeap.lemma_root_has_color_zero",
"primitive_Prims.op_LessThanOrEqual",
"refinement_interpretation_Tm_refine_2fbd657fe85bcb2423f9c7e5f9b3bcb5",
"refinement_interpretation_Tm_refine_601254ebe274211073b2024a11d02039",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"cc6d595f76243fda7748a7932c02ab79"
],
[
"EverCrypt.Hash.init",
1,
0,
0,
[ "@query" ],
0,
"cff76ebd456d2f1c3cffe699eec9a199"
],
[
"EverCrypt.Hash.init",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "constructor_distinct_EverCrypt.Hash.MD5_s",
"constructor_distinct_EverCrypt.Hash.SHA1_s",
"constructor_distinct_EverCrypt.Hash.SHA2_224_s",
"constructor_distinct_EverCrypt.Hash.SHA2_256_s",
"constructor_distinct_EverCrypt.Hash.SHA2_384_s",
"constructor_distinct_EverCrypt.Hash.SHA2_512_s",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s",
"data_elim_EverCrypt.Hash.SHA2_224_s",
"data_elim_EverCrypt.Hash.SHA2_256_s",
"data_elim_EverCrypt.Hash.SHA2_384_s",
"data_elim_EverCrypt.Hash.SHA2_512_s",
"disc_equation_EverCrypt.Hash.MD5_s",
"disc_equation_EverCrypt.Hash.SHA1_s",
"disc_equation_EverCrypt.Hash.SHA2_224_s",
"disc_equation_EverCrypt.Hash.SHA2_256_s",
"disc_equation_EverCrypt.Hash.SHA2_384_s",
"disc_equation_EverCrypt.Hash.SHA2_512_s",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_EverCrypt.Hash.acc0", "equation_EverCrypt.Hash.e_alg",
"equation_EverCrypt.Hash.footprint",
"equation_EverCrypt.Hash.footprint_s",
"equation_EverCrypt.Hash.freeable",
"equation_EverCrypt.Hash.invariant",
"equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p",
"equation_EverCrypt.Hash.preserves_freeable",
"equation_EverCrypt.Hash.repr", "equation_EverCrypt.Hash.state",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.init_t",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.Hash.init", "equation_Spec.SHA2.Constants.h224",
"equation_Spec.SHA2.Constants.h256", "equation_Spec.SHA2.h0",
"equation_Spec.SHA2.init",
"fuel_guarded_inversion_EverCrypt.Hash.state_s",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"inversion-interp", "kinding_EverCrypt.Hash.state_s@tok",
"kinding_Spec.Hash.Definitions.hash_alg@tok",
"lemma_EverCrypt.Hash.invert_state_s",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"projection_inverse_EverCrypt.Hash.MD5_s_p",
"projection_inverse_EverCrypt.Hash.SHA1_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_224_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_256_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_384_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_512_s_p",
"refinement_interpretation_Tm_refine_14354502053ec27032c0c2c904d8ef5f",
"refinement_interpretation_Tm_refine_195ea30d54ac9982b35901508f505d96",
"refinement_interpretation_Tm_refine_36d76b93acac87923db7157e2ebd41a7",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_46cbe09753b56b22de537dd7c6fddbc8",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_6bbdfb039a4208c820e81127497fe886",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_e31865e7dd2a0b044b24cacd3d9469a7",
"refinement_interpretation_Tm_refine_fbd4179bf3ba78511af32afca45a1d95",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_EverCrypt.Hash.footprint",
"typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.p",
"typing_FStar.Ghost.reveal", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.Hash.init", "typing_Spec.MD5.init",
"typing_Spec.SHA1.init", "typing_Spec.SHA2.Constants.h224",
"typing_Spec.SHA2.Constants.h256",
"typing_tok_Spec.Hash.Definitions.SHA2_384@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_512@tok"
],
0,
"8f70ecdceeaf75eea07978f0deff0009"
],
[
"EverCrypt.Hash.update_multi_256",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_FStar.List.Tot.Properties.llist",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Preorder.preorder",
"equation_FStar.Preorder.preorder_rel",
"equation_FStar.Preorder.reflexive",
"equation_Hacl.Hash.Definitions.blocks_t",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.ImmutableBuffer.immutable_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.logical",
"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_length",
"equation_Spec.SHA2.Constants.k224_256",
"equation_Vale.SHA.SHA_helpers.size_block_w_256",
"equation_Vale.SHA.SHA_helpers.update_multi_transparent",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t", "int_inversion",
"interpretation_Tm_abs_b333c99d6919700fbd31b164a13d8676",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Multiply",
"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_608d001a37b0b0d89198dc73ffc50461",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_b041622566c63972e1ac14219bbd2812",
"refinement_interpretation_Tm_refine_bd10f09297e0e7dc08314f7d9211801c",
"refinement_interpretation_Tm_refine_c10580e6367cbe43734ddd9241db2be2",
"refinement_interpretation_Tm_refine_c43881637fea8b5528f4439c75737f91",
"refinement_interpretation_Tm_refine_c6fb85953a2c0b350563653c2428eea2",
"refinement_interpretation_Tm_refine_c937ad38eafee45cc45d138ee3f48558",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Seq.Properties.seq_of_list",
"typing_Hacl.Hash.Core.SHA2.Constants.k224_256",
"typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.ImmutableBuffer.immutable_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.SHA2.Constants.k224_256_l",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"b8c0843e0a1c79a3879e29b3f0d8654f"
],
[
"EverCrypt.Hash.update_multi_224",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Hash.Definitions.blocks_t",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_82570b07cb96289a3265d65460b38f6c",
"refinement_interpretation_Tm_refine_b041622566c63972e1ac14219bbd2812",
"refinement_interpretation_Tm_refine_bf8427dbbe6830187406cfef6e0daa40",
"refinement_interpretation_Tm_refine_c6fb85953a2c0b350563653c2428eea2",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_tok_Spec.Hash.Definitions.SHA2_224@tok"
],
0,
"00dba8932addd32659016cd47a1e91eb"
],
[
"EverCrypt.Hash.update",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"function_token_typing_FStar.UInt8.t",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"refinement_interpretation_Tm_refine_644e3433e0b494a693e3a825167b19c2",
"refinement_interpretation_Tm_refine_cb4839c5fc21c325176ac01d054d7d89",
"typing_LowStar.Buffer.trivial_preorder"
],
0,
"5735655c34c87eb54aa8347bd983cb47"
],
[
"EverCrypt.Hash.update",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.Hash.update_multi.fuel_instrumented",
"@fuel_irrelevance_Spec.Hash.update_multi.fuel_instrumented",
"@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Spec.Hash.Definitions_interpretation_Tm_arrow_4b3c7766b835530fed880045baf8337f",
"Spec.Hash_interpretation_Tm_arrow_861a72617971f3b12b1b2ab67a981d41",
"bool_inversion", "bool_typing",
"constructor_distinct_EverCrypt.Hash.MD5_s",
"constructor_distinct_EverCrypt.Hash.SHA1_s",
"constructor_distinct_EverCrypt.Hash.SHA2_224_s",
"constructor_distinct_EverCrypt.Hash.SHA2_256_s",
"constructor_distinct_EverCrypt.Hash.SHA2_384_s",
"constructor_distinct_EverCrypt.Hash.SHA2_512_s",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s",
"data_elim_EverCrypt.Hash.SHA2_224_s",
"data_elim_EverCrypt.Hash.SHA2_256_s",
"data_elim_EverCrypt.Hash.SHA2_384_s",
"disc_equation_EverCrypt.Hash.MD5_s",
"disc_equation_EverCrypt.Hash.SHA1_s",
"disc_equation_EverCrypt.Hash.SHA2_224_s",
"disc_equation_EverCrypt.Hash.SHA2_256_s",
"disc_equation_EverCrypt.Hash.SHA2_384_s",
"disc_equation_EverCrypt.Hash.SHA2_512_s",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_EverCrypt.Hash.compress", "equation_EverCrypt.Hash.e_alg",
"equation_EverCrypt.Hash.footprint",
"equation_EverCrypt.Hash.footprint_s",
"equation_EverCrypt.Hash.freeable",
"equation_EverCrypt.Hash.invariant",
"equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p",
"equation_EverCrypt.Hash.preserves_freeable",
"equation_EverCrypt.Hash.repr", "equation_EverCrypt.Hash.state",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_64",
"equation_FStar.Monotonic.HyperStack.live_region",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.split",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_SHA_helpers.size_block_w_256",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.bytes_block",
"equation_Spec.Hash.Definitions.bytes_blocks",
"equation_Spec.Hash.Definitions.update_t",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.Hash.split_block", "equation_Spec.Hash.update",
"fuel_guarded_inversion_EverCrypt.Hash.state_s",
"function_token_typing_FStar.Integers.uint_64",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt64.t",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"function_token_typing_Spec.Hash.update",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"inversion-interp", "kinding_EverCrypt.Hash.state_s@tok",
"kinding_Spec.Hash.Definitions.hash_alg@tok",
"lemma_EverCrypt.Hash.invert_state_s",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.UInt32.uv_inv",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_Spec.Hash.Lemmas.update_multi_update",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.Hash.MD5_s_p",
"projection_inverse_EverCrypt.Hash.SHA1_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_224_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_256_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_384_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_512_s_p",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"refinement_interpretation_Tm_refine_168a5ae85cb58f4323fc557dd31e16f6",
"refinement_interpretation_Tm_refine_3865522cf7f163303cc0f7313f917b68",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4d0ae6b4ff35c0c8471d358291472299",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_644e3433e0b494a693e3a825167b19c2",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_79f632aa3673390dc46de32f66260b13",
"refinement_interpretation_Tm_refine_7ce9bdf3f89bf32d2d3e20761c8dfc87",
"refinement_interpretation_Tm_refine_85e8fbbc1f5880fbf17b23d5facbeed6",
"refinement_interpretation_Tm_refine_bf8427dbbe6830187406cfef6e0daa40",
"refinement_interpretation_Tm_refine_c6fb85953a2c0b350563653c2428eea2",
"refinement_interpretation_Tm_refine_cb4839c5fc21c325176ac01d054d7d89",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"token_correspondence_Spec.Hash.update",
"typing_EverCrypt.Hash.footprint",
"typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.p",
"typing_FStar.Ghost.reveal",
"typing_FStar.Monotonic.HyperStack.live_region",
"typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.update_multi", "typing_Spec.MD5.update",
"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,
"7d77b665b2380c1bcc7ef588ceb8157e"
],
[
"EverCrypt.Hash.update_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.Signed",
"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_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.v",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Pervasives.inversion",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.uint_t", "equation_LowStar.Buffer.buffer",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.word_length",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t", "inversion-interp",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"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_81babc7bb704ea6edf911c40f17498c0",
"refinement_interpretation_Tm_refine_cb4839c5fc21c325176ac01d054d7d89",
"typing_LowStar.Buffer.trivial_preorder"
],
0,
"0141d21803e9008dd3661e175bd9cfd8"
],
[
"EverCrypt.Hash.update_multi",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Winfinite",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_EverCrypt.Hash.e_alg", "equation_FStar.Integers.v",
"equation_FStar.Pervasives.inversion",
"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",
"inversion-interp", "kinding_Spec.Hash.Definitions.hash_alg@tok",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"typing_FStar.Ghost.reveal"
],
0,
"cb13956ae2be63c1a0c621a27bbc312b"
],
[
"EverCrypt.Hash.update_multi",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_EverCrypt.Hash.MD5_s",
"constructor_distinct_EverCrypt.Hash.SHA1_s",
"constructor_distinct_EverCrypt.Hash.SHA2_224_s",
"constructor_distinct_EverCrypt.Hash.SHA2_256_s",
"constructor_distinct_EverCrypt.Hash.SHA2_384_s",
"constructor_distinct_EverCrypt.Hash.SHA2_512_s",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s",
"data_elim_EverCrypt.Hash.SHA2_224_s",
"data_elim_EverCrypt.Hash.SHA2_256_s",
"data_elim_EverCrypt.Hash.SHA2_384_s",
"disc_equation_EverCrypt.Hash.MD5_s",
"disc_equation_EverCrypt.Hash.SHA1_s",
"disc_equation_EverCrypt.Hash.SHA2_224_s",
"disc_equation_EverCrypt.Hash.SHA2_256_s",
"disc_equation_EverCrypt.Hash.SHA2_384_s",
"disc_equation_EverCrypt.Hash.SHA2_512_s",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_EverCrypt.Hash.compress_many",
"equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.footprint",
"equation_EverCrypt.Hash.footprint_s",
"equation_EverCrypt.Hash.freeable",
"equation_EverCrypt.Hash.invariant",
"equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p",
"equation_EverCrypt.Hash.preserves_freeable",
"equation_EverCrypt.Hash.repr", "equation_EverCrypt.Hash.state",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_64",
"equation_FStar.Integers.v",
"equation_FStar.Monotonic.HyperStack.live_region",
"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.Definitions.block_len",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_SHA_helpers.size_block_w_256",
"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.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.words_state",
"fuel_guarded_inversion_EverCrypt.Hash.state_s",
"function_token_typing_FStar.Integers.uint_64",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt64.t",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing", "inversion-interp",
"kinding_EverCrypt.Hash.state_s@tok",
"kinding_Spec.Hash.Definitions.hash_alg@tok",
"lemma_EverCrypt.Hash.invert_state_s",
"lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.uv_inv",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.Hash.MD5_s_p",
"projection_inverse_EverCrypt.Hash.SHA1_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_224_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_256_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_384_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_512_s_p",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_168a5ae85cb58f4323fc557dd31e16f6",
"refinement_interpretation_Tm_refine_3865522cf7f163303cc0f7313f917b68",
"refinement_interpretation_Tm_refine_40c6f008a3f2c9d3927b30ab6308c9a2",
"refinement_interpretation_Tm_refine_40ffb9620b727a8620d61ad69490538f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4d0ae6b4ff35c0c8471d358291472299",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_6a4aaeeb4f7c11ebc609e181fdfcb714",
"refinement_interpretation_Tm_refine_6e3f78b75dbac4079b8eec2087da6bff",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_7ce9bdf3f89bf32d2d3e20761c8dfc87",
"refinement_interpretation_Tm_refine_814770d986f06f66b84225be16b5517a",
"refinement_interpretation_Tm_refine_81babc7bb704ea6edf911c40f17498c0",
"refinement_interpretation_Tm_refine_85e8fbbc1f5880fbf17b23d5facbeed6",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_bf8427dbbe6830187406cfef6e0daa40",
"refinement_interpretation_Tm_refine_c6fb85953a2c0b350563653c2428eea2",
"refinement_interpretation_Tm_refine_cb4839c5fc21c325176ac01d054d7d89",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_EverCrypt.Hash.footprint",
"typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.p",
"typing_FStar.Ghost.reveal",
"typing_FStar.Monotonic.HyperStack.live_region",
"typing_FStar.Set.singleton", "typing_FStar.UInt32.div",
"typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.block_len",
"typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.update_multi",
"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,
"aa32e98b8181b3a84d4b9af41dcb0b15"
],
[
"EverCrypt.Hash.update_last_256",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_SHA_helpers.block_length",
"equation_SHA_helpers.size_block_w_256",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.word_length",
"function_token_typing_SHA_helpers.block_length", "int_inversion",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0"
],
0,
"e34459d844742ac7c0bdc8ce287cb9ce"
],
[
"EverCrypt.Hash.update_last_256",
2,
0,
0,
[ "@query" ],
0,
"26d4deaf6a1a11467bf0f51b59a0053a"
],
[
"EverCrypt.Hash.update_last_224",
1,
0,
0,
[
"@query", "constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.word_length",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0"
],
0,
"fe618cf23839dba31e18077696eb0891"
],
[
"EverCrypt.Hash.update_last_224",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Base.op_At_Bar",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat",
"equation_SHA_helpers.size_block_w_256",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.len_len",
"equation_Spec.Hash.Definitions.len_length",
"equation_Spec.Hash.Definitions.len_v",
"equation_Spec.Hash.Definitions.max_input_length",
"equation_Spec.Hash.Definitions.pad0_length",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.Hash.Incremental.update_last",
"equation_Spec.Hash.PadFinish.pad",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
"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_156677950ba130498d26fd9f8eb20439",
"refinement_interpretation_Tm_refine_4645b1ee353232ac56962d0c23cf3dcb",
"refinement_interpretation_Tm_refine_5674c3490cd64d20efe8bd88eb9ca2fe",
"refinement_interpretation_Tm_refine_5eb9178be931e60a1509a24ddbdb817b",
"refinement_interpretation_Tm_refine_6e5b8a9cc8c2c36583c4a96eb915e856",
"refinement_interpretation_Tm_refine_769bca6664e27758984dec992912dbd0",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_77afd6307263994b249302243fef707c",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_bf8427dbbe6830187406cfef6e0daa40",
"refinement_interpretation_Tm_refine_c6fb85953a2c0b350563653c2428eea2",
"refinement_interpretation_Tm_refine_d52f7feda241b40a62710535ab4e1599",
"refinement_interpretation_Tm_refine_dc4e339075d1874e3be2dfcb68671ab7",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_FStar.Seq.Base.op_At_Bar",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.length",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.Definitions.len_v",
"typing_Spec.Hash.Definitions.word",
"typing_Spec.Hash.Incremental.update_last",
"typing_Spec.Hash.PadFinish.pad",
"typing_tok_Spec.Hash.Definitions.SHA2_224@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
],
0,
"eebe23b085699baef8a97e3184c0f12f"
],
[
"EverCrypt.Hash.update_last_st",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Winfinite",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_EverCrypt.Helpers.uint64_t",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.v",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer", "equation_Prims.nat",
"equation_SHA_helpers.size_block_w_256",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.word",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"refinement_interpretation_Tm_refine_811031f391a95ec77fc865af88582633",
"refinement_interpretation_Tm_refine_a5409fc05a543f82014baa3c642f2f03",
"refinement_interpretation_Tm_refine_b0e110a348ef0e95d5e4c945adf8178b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c236766c13680e7b1ff414836605791f",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_buffer"
],
0,
"a13d09d515fea4d023f10f3db9ba7f75"
],
[
"EverCrypt.Hash.update_last_64",
1,
0,
0,
[ "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq" ],
0,
"4fe451374e7c3b364ed1deb52b97908a"
],
[
"EverCrypt.Hash.update_last_64",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_Spec.Hash.Definitions.hash_alg__uu___haseq",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Winfinite",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_FStar.Integers.Signed__0",
"refinement_interpretation_Tm_refine_1ef7aeb8c575d47400472b58bef5ff15",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.length"
],
0,
"808c201ec2344ed12afb7466c732b743"
],
[
"EverCrypt.Hash.update_last_64",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_EverCrypt.Hash.compress_many",
"equation_EverCrypt.Hash.e_alg",
"equation_EverCrypt.Helpers.uint64_t",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Int.op_Slash",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_32",
"equation_FStar.Integers.v",
"equation_FStar.Monotonic.HyperStack.live_region",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Pervasives.inversion",
"equation_FStar.Seq.Base.op_At_Bar", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.mod", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t",
"equation_Hacl.Hash.Definitions.block_len",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.abs",
"equation_Prims.nat", "equation_SHA_helpers.size_block_w_256",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.len_length",
"equation_Spec.Hash.Definitions.len_t",
"equation_Spec.Hash.Definitions.len_v",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.Hash.Incremental.update_last",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"function_token_typing_FStar.Integers.uint_32",
"function_token_typing_FStar.UInt64.v",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "inversion-interp",
"kinding_Spec.Hash.Definitions.hash_alg@tok",
"lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.UInt.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Division",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "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_0722e9115d2a1be8d90527397d01011c",
"refinement_interpretation_Tm_refine_16f0129aadd41eff84672b7e1eed6c5e",
"refinement_interpretation_Tm_refine_1cdae3d9923a6b99f352d43f26640887",
"refinement_interpretation_Tm_refine_1ef7aeb8c575d47400472b58bef5ff15",
"refinement_interpretation_Tm_refine_40ffb9620b727a8620d61ad69490538f",
"refinement_interpretation_Tm_refine_41ae00a3e556b48ef5ab6c6b5dd15278",
"refinement_interpretation_Tm_refine_46e2c9ffa753fafb6a558e2a6fdc9631",
"refinement_interpretation_Tm_refine_55573c13df1ad79625a0017d3021d789",
"refinement_interpretation_Tm_refine_6e5b8a9cc8c2c36583c4a96eb915e856",
"refinement_interpretation_Tm_refine_764f2f3b42689189307765ed6d421efc",
"refinement_interpretation_Tm_refine_769bca6664e27758984dec992912dbd0",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_9bd11efd3d1b15018e7a1047644f241f",
"refinement_interpretation_Tm_refine_9f98e4c5a305b81c3cdab3041ec9362f",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_b74a7cc72b60e5ca6bf76621a35790c5",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c43881637fea8b5528f4439c75737f91",
"refinement_interpretation_Tm_refine_d52f7feda241b40a62710535ab4e1599",
"refinement_interpretation_Tm_refine_dc4e339075d1874e3be2dfcb68671ab7",
"refinement_interpretation_Tm_refine_f23851a2c6813e80c26b451b41a00ba5",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_FStar.Ghost.reveal",
"typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.Integers.v",
"typing_FStar.Monotonic.HyperStack.live_region",
"typing_FStar.UInt.mod", "typing_FStar.UInt32.v",
"typing_FStar.UInt64.rem", "typing_FStar.UInt64.sub",
"typing_FStar.UInt64.v", "typing_Hacl.Hash.Definitions.block_len",
"typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.Definitions.len_v",
"typing_Spec.Hash.Definitions.word_length",
"typing_Spec.Hash.Incremental.update_last",
"typing_Spec.Hash.PadFinish.pad",
"typing_tok_Spec.Hash.Definitions.MD5@tok"
],
0,
"83725e807d93889eb4610aa0023ef7e6"
],
[
"EverCrypt.Hash.update_last_128",
1,
0,
0,
[ "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq" ],
0,
"201141db6816ded619b37fde3cbc9297"
],
[
"EverCrypt.Hash.update_last_128",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_Spec.Hash.Definitions.hash_alg__uu___haseq",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Winfinite",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_FStar.Integers.Signed__0",
"refinement_interpretation_Tm_refine_1ef7aeb8c575d47400472b58bef5ff15",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.length"
],
0,
"a505b3b2506054a2265c7d3c79ddf78e"
],
[
"EverCrypt.Hash.update_last_128",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Integers_pretyping_6ad08c58c10cb742e34ff2d7d8900d61",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"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.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_EverCrypt.Hash.compress_many",
"equation_EverCrypt.Hash.e_alg",
"equation_EverCrypt.Helpers.uint64_t",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Int.op_Slash",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_64",
"equation_FStar.Integers.v",
"equation_FStar.Kremlin.Endianness.bytes",
"equation_FStar.Monotonic.HyperStack.live_region",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Base.op_At_Bar", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.mod", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt128.n",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.abs",
"equation_Prims.nat", "equation_Prims.pos",
"equation_SHA_helpers.block_length",
"equation_SHA_helpers.size_block_w_256",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.len_len",
"equation_Spec.Hash.Definitions.len_length",
"equation_Spec.Hash.Definitions.len_t",
"equation_Spec.Hash.Definitions.len_v",
"equation_Spec.Hash.Definitions.max_input_length",
"equation_Spec.Hash.Definitions.pad0_length",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.word_length",
"equation_Spec.Hash.Definitions.words_state",
"equation_Spec.Hash.Incremental.update_last",
"equation_Spec.Hash.PadFinish.pad",
"function_token_typing_FStar.Integers.uint_64",
"function_token_typing_FStar.UInt128.v",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"kinding_Spec.Hash.Definitions.hash_alg@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.UInt.pow2_values",
"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_region_frameOf",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Division",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "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",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_0722e9115d2a1be8d90527397d01011c",
"refinement_interpretation_Tm_refine_12b5b1a5c1daffe21a10c15e7bc1721a",
"refinement_interpretation_Tm_refine_16f0129aadd41eff84672b7e1eed6c5e",
"refinement_interpretation_Tm_refine_1cdae3d9923a6b99f352d43f26640887",
"refinement_interpretation_Tm_refine_1e62df159c33fd3091667f8254d1ab80",
"refinement_interpretation_Tm_refine_1ef7aeb8c575d47400472b58bef5ff15",
"refinement_interpretation_Tm_refine_22871ed0ff70fd094ad3e8d742624d47",
"refinement_interpretation_Tm_refine_40ffb9620b727a8620d61ad69490538f",
"refinement_interpretation_Tm_refine_41ae00a3e556b48ef5ab6c6b5dd15278",
"refinement_interpretation_Tm_refine_46e2c9ffa753fafb6a558e2a6fdc9631",
"refinement_interpretation_Tm_refine_55573c13df1ad79625a0017d3021d789",
"refinement_interpretation_Tm_refine_6e5b8a9cc8c2c36583c4a96eb915e856",
"refinement_interpretation_Tm_refine_769bca6664e27758984dec992912dbd0",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_7adc1f597c7c5411858381b6d96a831d",
"refinement_interpretation_Tm_refine_9bd11efd3d1b15018e7a1047644f241f",
"refinement_interpretation_Tm_refine_9f98e4c5a305b81c3cdab3041ec9362f",
"refinement_interpretation_Tm_refine_a01ca1f979511b6842a5eca25ddf0be3",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_b74a7cc72b60e5ca6bf76621a35790c5",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_bbd28fe9499d6bec097fdc331ddb917d",
"refinement_interpretation_Tm_refine_c43881637fea8b5528f4439c75737f91",
"refinement_interpretation_Tm_refine_d52f7feda241b40a62710535ab4e1599",
"refinement_interpretation_Tm_refine_dc4e339075d1874e3be2dfcb68671ab7",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_f23851a2c6813e80c26b451b41a00ba5",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"refinement_interpretation_Tm_refine_ff0b858fd0968c77ee0e65882024d41c",
"typing_FStar.Ghost.reveal",
"typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.Integers.v",
"typing_FStar.Kremlin.Endianness.n_to_be",
"typing_FStar.Monotonic.HyperStack.live_region",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt.mod",
"typing_FStar.UInt32.v", "typing_FStar.UInt64.rem",
"typing_FStar.UInt64.sub", "typing_FStar.UInt64.v",
"typing_FStar.UInt8.uint_to_t",
"typing_Hacl.Hash.Definitions.block_len",
"typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length", "typing_Prims.pow2",
"typing_SHA_helpers.block_length",
"typing_Spec.Hash.Definitions.block_length",
"typing_Spec.Hash.Definitions.len_len",
"typing_Spec.Hash.Definitions.len_v",
"typing_Spec.Hash.Definitions.pad0_length",
"typing_Spec.Hash.Definitions.word_length",
"typing_Spec.Hash.Incremental.update_last",
"typing_Spec.Hash.PadFinish.pad",
"typing_tok_Spec.Hash.Definitions.SHA2_384@tok"
],
0,
"bfba353a214445343fe1f6ced9e6b0c2"
],
[
"EverCrypt.Hash.update_last",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Winfinite",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_EverCrypt.Helpers.uint64_t",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.v",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_LowStar.Buffer.buffer",
"equation_Prims.nat", "equation_SHA_helpers.size_block_w_256",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.bytes",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"lemma_FStar.Seq.Base.lemma_len_append",
"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",
"projection_inverse_FStar.Integers.Signed__0",
"refinement_interpretation_Tm_refine_16002e30c32b0cab221a86373bd29b22",
"refinement_interpretation_Tm_refine_1ef7aeb8c575d47400472b58bef5ff15",
"refinement_interpretation_Tm_refine_46e2c9ffa753fafb6a558e2a6fdc9631",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_cb4839c5fc21c325176ac01d054d7d89",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.length"
],
0,
"76cb3474bbeb8cf33f9926fe7bc2785f"
],
[
"EverCrypt.Hash.update_last",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Winfinite",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_FStar.Integers.Signed__0",
"refinement_interpretation_Tm_refine_1ef7aeb8c575d47400472b58bef5ff15",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.length"
],
0,
"358ce5090d9ecc196e1438009b6cda8d"
],
[
"EverCrypt.Hash.update_last",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "constructor_distinct_EverCrypt.Hash.MD5_s",
"constructor_distinct_EverCrypt.Hash.SHA1_s",
"constructor_distinct_EverCrypt.Hash.SHA2_224_s",
"constructor_distinct_EverCrypt.Hash.SHA2_256_s",
"constructor_distinct_EverCrypt.Hash.SHA2_384_s",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s",
"data_elim_EverCrypt.Hash.SHA2_224_s",
"data_elim_EverCrypt.Hash.SHA2_256_s",
"data_elim_EverCrypt.Hash.SHA2_384_s",
"disc_equation_EverCrypt.Hash.MD5_s",
"disc_equation_EverCrypt.Hash.SHA1_s",
"disc_equation_EverCrypt.Hash.SHA2_224_s",
"disc_equation_EverCrypt.Hash.SHA2_256_s",
"disc_equation_EverCrypt.Hash.SHA2_384_s",
"disc_equation_EverCrypt.Hash.SHA2_512_s",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.footprint",
"equation_EverCrypt.Hash.footprint_s",
"equation_EverCrypt.Hash.freeable",
"equation_EverCrypt.Hash.invariant",
"equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p",
"equation_EverCrypt.Hash.preserves_freeable",
"equation_EverCrypt.Hash.repr", "equation_EverCrypt.Hash.state",
"equation_EverCrypt.Helpers.uint64_t",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.Monotonic.HyperStack.live_region",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype",
"equation_Prims.nat",
"fuel_guarded_inversion_EverCrypt.Hash.state_s",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt64.t",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"inversion-interp", "kinding_EverCrypt.Hash.state_s@tok",
"kinding_Spec.Hash.Definitions.hash_alg@tok",
"lemma_EverCrypt.Hash.invert_state_s",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"projection_inverse_EverCrypt.Hash.MD5_s_p",
"projection_inverse_EverCrypt.Hash.SHA1_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_224_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_256_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_384_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_512_s_p",
"refinement_interpretation_Tm_refine_168a5ae85cb58f4323fc557dd31e16f6",
"refinement_interpretation_Tm_refine_16f0129aadd41eff84672b7e1eed6c5e",
"refinement_interpretation_Tm_refine_1ef7aeb8c575d47400472b58bef5ff15",
"refinement_interpretation_Tm_refine_3865522cf7f163303cc0f7313f917b68",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4d0ae6b4ff35c0c8471d358291472299",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_85e8fbbc1f5880fbf17b23d5facbeed6",
"refinement_interpretation_Tm_refine_bf8427dbbe6830187406cfef6e0daa40",
"refinement_interpretation_Tm_refine_c6fb85953a2c0b350563653c2428eea2",
"refinement_interpretation_Tm_refine_cb4839c5fc21c325176ac01d054d7d89",
"refinement_interpretation_Tm_refine_f23851a2c6813e80c26b451b41a00ba5",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_EverCrypt.Hash.footprint",
"typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.p",
"typing_FStar.Ghost.reveal",
"typing_FStar.Monotonic.HyperStack.live_region",
"typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer"
],
0,
"1c9ef9dedfe3054eff93b935a62c16ac"
],
[
"EverCrypt.Hash.finish",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.Monotonic.HyperStack.mem",
"refinement_interpretation_Tm_refine_cb4839c5fc21c325176ac01d054d7d89"
],
0,
"b0112553d4505a5edb397aa7d6463e6e"
],
[
"EverCrypt.Hash.finish",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "constructor_distinct_EverCrypt.Hash.MD5_s",
"constructor_distinct_EverCrypt.Hash.SHA1_s",
"constructor_distinct_EverCrypt.Hash.SHA2_224_s",
"constructor_distinct_EverCrypt.Hash.SHA2_256_s",
"constructor_distinct_EverCrypt.Hash.SHA2_384_s",
"constructor_distinct_EverCrypt.Hash.SHA2_512_s",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s",
"data_elim_EverCrypt.Hash.SHA2_224_s",
"data_elim_EverCrypt.Hash.SHA2_256_s",
"data_elim_EverCrypt.Hash.SHA2_384_s",
"disc_equation_EverCrypt.Hash.MD5_s",
"disc_equation_EverCrypt.Hash.SHA1_s",
"disc_equation_EverCrypt.Hash.SHA2_224_s",
"disc_equation_EverCrypt.Hash.SHA2_256_s",
"disc_equation_EverCrypt.Hash.SHA2_384_s",
"disc_equation_EverCrypt.Hash.SHA2_512_s",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.extract",
"equation_EverCrypt.Hash.footprint",
"equation_EverCrypt.Hash.footprint_s",
"equation_EverCrypt.Hash.freeable",
"equation_EverCrypt.Hash.invariant",
"equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p",
"equation_EverCrypt.Hash.preserves_freeable",
"equation_EverCrypt.Hash.repr", "equation_EverCrypt.Hash.state",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.Integers.int_t",
"equation_FStar.Monotonic.HyperStack.live_region",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.words_state",
"fuel_guarded_inversion_EverCrypt.Hash.state_s",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"inversion-interp", "kinding_EverCrypt.Hash.state_s@tok",
"kinding_Spec.Hash.Definitions.hash_alg@tok",
"lemma_EverCrypt.Hash.invert_state_s",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"projection_inverse_EverCrypt.Hash.MD5_s_p",
"projection_inverse_EverCrypt.Hash.SHA1_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_224_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_256_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_384_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_512_s_p",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_046c9e96d509a0c02bc59935acfefae6",
"refinement_interpretation_Tm_refine_29b776c811ab44a2ce7ce481b2fb1c53",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_5e13560dc0e89670382e1eff4c1a9ce0",
"refinement_interpretation_Tm_refine_6718ce1399c58ece59ba7bf2dd6d2cc3",
"refinement_interpretation_Tm_refine_728264b7071e24aab9750c429b45ac02",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_89b6609407fda52ccd4b4dc14e6610ea",
"refinement_interpretation_Tm_refine_8a5f75de45e5993043db6aacd6582712",
"refinement_interpretation_Tm_refine_cb4839c5fc21c325176ac01d054d7d89",
"refinement_interpretation_Tm_refine_e9479aac75cd7e9f74bb1edbe70d426d",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_EverCrypt.Hash.footprint",
"typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.p",
"typing_FStar.Ghost.reveal",
"typing_FStar.Monotonic.HyperStack.live_region",
"typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.Hash.PadFinish.finish",
"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,
"137e3e77cb12478303bfe061d98aeda1"
],
[
"EverCrypt.Hash.free",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "constructor_distinct_EverCrypt.Hash.MD5_s",
"constructor_distinct_EverCrypt.Hash.SHA1_s",
"constructor_distinct_EverCrypt.Hash.SHA2_224_s",
"constructor_distinct_EverCrypt.Hash.SHA2_256_s",
"constructor_distinct_EverCrypt.Hash.SHA2_384_s",
"constructor_distinct_EverCrypt.Hash.SHA2_512_s",
"data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s",
"data_elim_EverCrypt.Hash.SHA2_224_s",
"data_elim_EverCrypt.Hash.SHA2_256_s",
"data_elim_EverCrypt.Hash.SHA2_384_s",
"data_elim_EverCrypt.Hash.SHA2_512_s",
"disc_equation_EverCrypt.Hash.MD5_s",
"disc_equation_EverCrypt.Hash.SHA1_s",
"disc_equation_EverCrypt.Hash.SHA2_224_s",
"disc_equation_EverCrypt.Hash.SHA2_256_s",
"disc_equation_EverCrypt.Hash.SHA2_384_s",
"disc_equation_EverCrypt.Hash.SHA2_512_s",
"equation_EverCrypt.Hash.e_alg", "equation_EverCrypt.Hash.footprint",
"equation_EverCrypt.Hash.footprint_s",
"equation_EverCrypt.Hash.freeable",
"equation_EverCrypt.Hash.freeable_s",
"equation_EverCrypt.Hash.invariant",
"equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p",
"equation_EverCrypt.Hash.state",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_Prims.eqtype", "equation_Prims.nat",
"fuel_guarded_inversion_EverCrypt.Hash.state_s",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"inversion-interp", "kinding_EverCrypt.Hash.state_s@tok",
"kinding_Spec.Hash.Definitions.hash_alg@tok",
"lemma_EverCrypt.Hash.invert_state_s",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"projection_inverse_EverCrypt.Hash.MD5_s_p",
"projection_inverse_EverCrypt.Hash.SHA1_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_224_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_256_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_384_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_512_s_p",
"refinement_interpretation_Tm_refine_1b3b914c1e59764d7562e03a4c16b28e",
"refinement_interpretation_Tm_refine_26e93f9cc692fc07798c1dcda5031cc8",
"refinement_interpretation_Tm_refine_2daecc255632d36816f684c1ba584bcf",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_420a882b033a20f84de0dc30583174da",
"refinement_interpretation_Tm_refine_4fcdd6b26f846aa6a48cff5154ac1ef8",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_92fd7bf80ef2e52bd7ed08870f08e0a3",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_b14cdbd9e17ea37a8374fc310aeac430",
"refinement_interpretation_Tm_refine_f79d1b626b0e43696ad583841aa787d5",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"typing_EverCrypt.Hash.footprint",
"typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.p",
"typing_FStar.Ghost.reveal", "typing_FStar.Map.contains",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer"
],
0,
"66a659cc56cdac875756918e7fb23b43"
],
[
"EverCrypt.Hash.copy",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Monotonic.HyperStack.mem",
"refinement_interpretation_Tm_refine_13d94ed18504b6bf09e657402f5e2fea"
],
0,
"988a7b6b84a8b17c189135f7ec5e6a67"
],
[
"EverCrypt.Hash.copy",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "constructor_distinct_EverCrypt.Hash.MD5_s",
"constructor_distinct_EverCrypt.Hash.SHA1_s",
"constructor_distinct_EverCrypt.Hash.SHA2_224_s",
"constructor_distinct_EverCrypt.Hash.SHA2_256_s",
"constructor_distinct_EverCrypt.Hash.SHA2_384_s",
"constructor_distinct_EverCrypt.Hash.SHA2_512_s",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"constructor_distinct_Spec.Hash.Definitions.SHA2_224",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"data_elim_EverCrypt.Hash.MD5_s", "data_elim_EverCrypt.Hash.SHA1_s",
"data_elim_EverCrypt.Hash.SHA2_224_s",
"data_elim_EverCrypt.Hash.SHA2_256_s",
"data_elim_EverCrypt.Hash.SHA2_384_s",
"disc_equation_EverCrypt.Hash.MD5_s",
"disc_equation_EverCrypt.Hash.SHA1_s",
"disc_equation_EverCrypt.Hash.SHA2_224_s",
"disc_equation_EverCrypt.Hash.SHA2_256_s",
"disc_equation_EverCrypt.Hash.SHA2_384_s",
"disc_equation_EverCrypt.Hash.SHA2_512_s",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_EverCrypt.Hash.acc", "equation_EverCrypt.Hash.e_alg",
"equation_EverCrypt.Hash.footprint",
"equation_EverCrypt.Hash.footprint_s",
"equation_EverCrypt.Hash.freeable",
"equation_EverCrypt.Hash.invariant",
"equation_EverCrypt.Hash.invariant_s", "equation_EverCrypt.Hash.p",
"equation_EverCrypt.Hash.preserves_freeable",
"equation_EverCrypt.Hash.repr", "equation_EverCrypt.Hash.state",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_32",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Hash.Definitions.state",
"equation_Hacl.Hash.Definitions.word",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype",
"equation_Prims.l_True", "equation_Prims.logical",
"equation_Prims.nat",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word",
"equation_Spec.Hash.Definitions.words_state",
"fuel_guarded_inversion_EverCrypt.Hash.state_s",
"function_token_typing_FStar.Integers.uint_32",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_typing",
"interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
"inversion-interp", "kinding_EverCrypt.Hash.state_s@tok",
"kinding_Spec.Hash.Definitions.hash_alg@tok",
"lemma_EverCrypt.Hash.invert_state_s",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"proj_equation_EverCrypt.Hash.MD5_s_p",
"proj_equation_EverCrypt.Hash.SHA1_s_p",
"proj_equation_EverCrypt.Hash.SHA2_224_s_p",
"proj_equation_EverCrypt.Hash.SHA2_256_s_p",
"proj_equation_EverCrypt.Hash.SHA2_384_s_p",
"proj_equation_EverCrypt.Hash.SHA2_512_s_p",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.Hash.MD5_s_p",
"projection_inverse_EverCrypt.Hash.SHA1_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_224_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_256_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_384_s_p",
"projection_inverse_EverCrypt.Hash.SHA2_512_s_p",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_09a3dd3323b981ddb44655c6e4bc1db3",
"refinement_interpretation_Tm_refine_0b89b275b68848e542012d6c5b3813d2",
"refinement_interpretation_Tm_refine_13d94ed18504b6bf09e657402f5e2fea",
"refinement_interpretation_Tm_refine_2523390c9a3c6feeaafd4eb8b8df319e",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_60659f08c87dd925056a8c28d7a78c1e",
"refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
"refinement_interpretation_Tm_refine_97d7f8803efb7aac2e636dda5403cc7a",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a968971763bda91f25c9a6bddf72c727",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_bb403432203287f0a2acfb7518a4b347",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
"true_interp", "typing_EverCrypt.Hash.footprint",
"typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.p",
"typing_EverCrypt.Hash.repr", "typing_FStar.Ghost.reveal",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Set.singleton", "typing_Hacl.Hash.Definitions.word",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.get",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"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,
"db1758899f6b8d6c39e4e41e5aa97a0e"
],
[
"EverCrypt.Hash.hash_256",
1,
0,
0,
[ "@query" ],
0,
"2cd2d2ca94263a78ca083c6220ef7e32"
],
[
"EverCrypt.Hash.hash_256",
2,
0,
0,
[ "@query" ],
0,
"ec11223abeb771ece80bd0c58bf19431"
],
[
"EverCrypt.Hash.hash_224",
1,
0,
0,
[ "@query" ],
0,
"0dbdf0ce6a3bd0ed7c9f07c02ea52019"
],
[
"EverCrypt.Hash.hash_224",
2,
0,
0,
[ "@query" ],
0,
"89829f08fdf8814d77428f7b0dde4f26"
],
[
"EverCrypt.Hash.hash",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Winfinite",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_EverCrypt.Helpers.uint32_t",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.Integers.int_t", "equation_FStar.UInt.uint_t",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"projection_inverse_FStar.Integers.Signed__0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_669b03be27e0961af1f2f8fb61bfb0b2",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len"
],
0,
"bdfe6ee88478e92cea314401b06e4b8d"
],
[
"EverCrypt.Hash.hash",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Winfinite",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.Integers.int_t", "equation_FStar.UInt.uint_t",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"projection_inverse_FStar.Integers.Signed__0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len"
],
0,
"f6325f34230b2a9ed5879cc845ac8bd2"
],
[
"EverCrypt.Hash.hash",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"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.W32@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Hash.Definitions.MD5@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_EverCrypt.Helpers.uint32_t",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t", "equation_FStar.Integers.v",
"equation_FStar.Monotonic.HyperStack.live_region",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Pervasives.inversion",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.max_input_length",
"equation_Spec.Hash.hash",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t", "inversion-interp",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_046c9e96d509a0c02bc59935acfefae6",
"refinement_interpretation_Tm_refine_2427c8f9ecea7a2c261ac9e2662737f3",
"refinement_interpretation_Tm_refine_669b03be27e0961af1f2f8fb61bfb0b2",
"refinement_interpretation_Tm_refine_7be4aae497b85689a212838715bc9f74",
"refinement_interpretation_Tm_refine_893672681d27705e287e6ea220ff5449",
"refinement_interpretation_Tm_refine_a05856fd66f21308730dff935c5b4b2c",
"refinement_interpretation_Tm_refine_b246c4889d2e2a782189865824902d78",
"refinement_interpretation_Tm_refine_c5e52a1d7fb67e5dce7cbae92608c0b8",
"refinement_interpretation_Tm_refine_d912210b9ef3df0b63653a03dbe8062b",
"refinement_interpretation_Tm_refine_e7e4ad7ee2ff8b7e6c08eeb365a3e84f",
"refinement_interpretation_Tm_refine_f14cb08023edf8a82ed80cdd026566c4",
"typing_FStar.Monotonic.HyperStack.live_region",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf", "typing_Spec.Hash.hash",
"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,
"c73a19e90d9f33381be7740fd54077aa"
]
]
]
Computing file changes ...
